cprover
qbf_qube_core.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 #include "qbf_qube_core.h"
10 
11 #include <cassert>
12 #include <cstdlib>
13 #include <fstream>
14 
15 #include <util/mp_arith.h>
16 
18 {
19  break_lines=false;
20  qbf_tmp_file="qube.qdimacs";
21 }
22 
24 {
25 }
26 
27 const std::string qbf_qube_coret::solver_text()
28 {
29  return "QuBE w/ toplevel assignments";
30 }
31 
33 {
34  if(no_clauses()==0)
36 
37  {
38  messaget::status() << "QuBE: "
39  << no_variables() << " variables, "
40  << no_clauses() << " clauses" << eom;
41  }
42 
43  std::string result_tmp_file="qube.out";
44 
45  {
46  std::ofstream out(qbf_tmp_file.c_str());
47 
48  // write it
49  break_lines=false;
50  write_qdimacs_cnf(out);
51  }
52 
53  std::string options="";
54 
55  // solve it
56  int res=system((
57  "QuBE "+options+" "+qbf_tmp_file+" > "+result_tmp_file).c_str());
58  assert(0==res);
59 
60  bool result=false;
61 
62  // read result
63  {
64  std::ifstream in(result_tmp_file.c_str());
65 
66  bool result_found=false;
67  while(in)
68  {
69  std::string line;
70 
71  std::getline(in, line);
72 
73  if(line!="" && line[line.size()-1]=='\r')
74  line.resize(line.size()-1);
75 
76  if(line[0]=='V')
77  {
78  mp_integer b(line.substr(2).c_str());
79  if(b<0)
80  assignment[integer2unsigned(b.negate())]=false;
81  else
83  }
84  else if(line=="s cnf 1")
85  {
86  result=true;
87  result_found=true;
88  break;
89  }
90  else if(line=="s cnf 0")
91  {
92  result=false;
93  result_found=true;
94  break;
95  }
96  }
97 
98  if(!result_found)
99  {
100  messaget::error() << "QuBE failed: unknown result" << eom;
101  return resultt::P_ERROR;
102  }
103  }
104 
105  remove(result_tmp_file.c_str());
106  remove(qbf_tmp_file.c_str());
107 
108  if(result)
109  {
110  messaget::status() << "QuBE: TRUE" << eom;
111  return resultt::P_SATISFIABLE;
112  }
113  else
114  {
115  messaget::status() << "QuBE: FALSE" << eom;
117  }
118 }
119 
121 {
122  throw "not supported";
123 }
124 
126 {
127  throw "not supported";
128 }
mstreamt & result()
Definition: message.h:233
BigInt mp_integer
Definition: mp_arith.h:19
mstreamt & status()
Definition: message.h:238
std::string qbf_tmp_file
Definition: qbf_qube_core.h:18
virtual bool is_in_core(literalt l) const
bool break_lines
Definition: dimacs_cnf.h:36
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual ~qbf_qube_coret()
assignmentt assignment
Definition: qbf_qube_core.h:21
virtual const std::string solver_text()
resultt
Definition: prop.h:94
virtual size_t no_clauses() const
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
mstreamt & error()
Definition: message.h:223
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14