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 #include <cstring>
15 
16 #include <util/mp_arith.h>
17 
19 {
20  break_lines=false;
21  qbf_tmp_file="qube.qdimacs";
22 }
23 
25 {
26 }
27 
28 const std::string qbf_qube_coret::solver_text()
29 {
30  return "QuBE w/ toplevel assignments";
31 }
32 
34 {
35  if(no_clauses()==0)
37 
38  {
39  messaget::status() << "QuBE: "
40  << no_variables() << " variables, "
41  << no_clauses() << " clauses" << eom;
42  }
43 
44  std::string result_tmp_file="qube.out";
45 
46  {
47  std::ofstream out(qbf_tmp_file.c_str());
48 
49  // write it
50  break_lines=false;
51  write_qdimacs_cnf(out);
52  }
53 
54  std::string options="";
55 
56  // solve it
57  int res=system((
58  "QuBE "+options+" "+qbf_tmp_file+" > "+result_tmp_file).c_str());
59  CHECK_RETURN(0==res);
60 
61  bool result=false;
62 
63  // read result
64  {
65  std::ifstream in(result_tmp_file.c_str());
66 
67  bool result_found=false;
68  while(in)
69  {
70  std::string line;
71 
72  std::getline(in, line);
73 
74  if(line!="" && line[line.size()-1]=='\r')
75  line.resize(line.size()-1);
76 
77  if(line[0]=='V')
78  {
79  mp_integer b(line.substr(2).c_str());
80  if(b<0)
81  assignment[integer2unsigned(b.negate())]=false;
82  else
84  }
85  else if(line=="s cnf 1")
86  {
87  result=true;
88  result_found=true;
89  break;
90  }
91  else if(line=="s cnf 0")
92  {
93  result=false;
94  result_found=true;
95  break;
96  }
97  }
98 
99  if(!result_found)
100  {
101  messaget::error() << "QuBE failed: unknown result" << eom;
102  return resultt::P_ERROR;
103  }
104  }
105 
106  int remove_result=remove(result_tmp_file.c_str());
107  if(remove_result!=0)
108  {
109  messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
110  return resultt::P_ERROR;
111  }
112 
113  remove_result=remove(qbf_tmp_file.c_str());
114  if(remove_result!=0)
115  {
116  messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
117  return resultt::P_ERROR;
118  }
119 
120  if(result)
121  {
122  messaget::status() << "QuBE: TRUE" << eom;
123  return resultt::P_SATISFIABLE;
124  }
125  else
126  {
127  messaget::status() << "QuBE: FALSE" << eom;
129  }
130 }
131 
133 {
134  throw "not supported";
135 }
136 
138 {
139  throw "not supported";
140 }
BigInt mp_integer
Definition: mp_arith.h:22
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
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual ~qbf_qube_coret()
mstreamt & error() const
Definition: message.h:302
assignmentt assignment
Definition: qbf_qube_core.h:21
virtual const std::string solver_text()
resultt
Definition: prop.h:96
virtual size_t no_clauses() const
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14