cprover
qbf_qube.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 #include "qbf_qube.h"
10 
11 #include <cstdlib>
12 #include <fstream>
13 
14 #include <util/invariant.h>
15 
17 {
18  // skizzo crashes on broken lines
19  break_lines=false;
20 }
21 
23 {
24 }
25 
27 {
29 }
30 
31 const std::string qbf_qubet::solver_text()
32 {
33  return "QuBE";
34 }
35 
37 {
38  // sKizzo crashes on empty instances
39  if(no_clauses()==0)
41 
42  {
43  messaget::status() <<
44  "QuBE: " <<
45  no_variables() << " variables, " <<
46  no_clauses() << " clauses" << eom;
47  }
48 
49  std::string qbf_tmp_file="qube.qdimacs";
50  std::string result_tmp_file="qube.out";
51 
52  {
53  std::ofstream out(qbf_tmp_file.c_str());
54 
55  // write it
56  write_qdimacs_cnf(out);
57  }
58 
59  std::string options="";
60 
61  // solve it
62  int res=system(
63  ("QuBE "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
64  CHECK_RETURN(0==res);
65 
66  bool result=false;
67 
68  // read result
69  {
70  std::ifstream in(result_tmp_file.c_str());
71 
72  bool result_found=false;
73  while(in)
74  {
75  std::string line;
76 
77  std::getline(in, line);
78 
79  if(line!="" && line[line.size()-1]=='\r')
80  line.resize(line.size()-1);
81 
82  if(line=="s cnf 0")
83  {
84  result=true;
85  result_found=true;
86  break;
87  }
88  else if(line=="s cnf 1")
89  {
90  result=false;
91  result_found=true;
92  break;
93  }
94  }
95 
96  if(!result_found)
97  {
98  messaget::error() << "QuBE failed: unknown result" << eom;
99  return resultt::P_ERROR;
100  }
101  }
102 
103  if(result)
104  {
105  messaget::status() << "QuBE: TRUE" << eom;
106  return resultt::P_SATISFIABLE;
107  }
108  else
109  {
110  messaget::status() << "QuBE: FALSE" << eom;
112  }
113 
114  return resultt::P_ERROR;
115 }
virtual resultt prop_solve()
Definition: qbf_qube.cpp:36
bool break_lines
Definition: dimacs_cnf.h:39
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
virtual tvt l_get(literalt a) const
Definition: qbf_qube.cpp:26
Definition: threeval.h:19
mstreamt & error() const
Definition: message.h:386
resultt
Definition: prop.h:96
virtual size_t no_clauses() const
static eomt eom
Definition: message.h:284
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
virtual const std::string solver_text()
Definition: qbf_qube.cpp:31
virtual ~qbf_qubet()
Definition: qbf_qube.cpp:22
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:15