cprover
qbf_skizzo_core.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 
10 #include <cassert>
11 #include <fstream>
12 
13 #include <util/string2int.h>
14 
15 #include <cuddObj.hh> // CUDD Library
16 
18 // FIX FOR THE CUDD LIBRARY
19 
20 inline DdNode *DD::getNode() const
21 {
22  return node;
23 } // DD::getNode
26 #include <dddmp.h>
27 
28 #include "qbf_skizzo_core.h"
29 
32 {
33  // skizzo crashes on broken lines
34  break_lines=false;
35  qbf_tmp_file="sKizzo.qdimacs";
36 }
37 
39 {
40 }
41 
42 const std::string qbf_skizzo_coret::solver_text()
43 {
44  return "Skizzo/Core";
45 }
46 
48 {
49  // sKizzo crashes on empty instances
50  if(no_clauses()==0)
52 
53  {
54  std::string msg=
55  "Skizzo: "+
56  std::to_string(no_variables())+" variables, "+
57  std::to_string(no_clauses())+" clauses";
58  messaget::status() << msg << messaget::eom;
59  }
60 
61  std::string result_tmp_file="sKizzo.out";
62 
63  {
64  std::ofstream out(qbf_tmp_file.c_str());
65 
66  // write it
67  break_lines=false;
68  write_qdimacs_cnf(out);
69  }
70 
71  std::string options="";
72 
73  // solve it
74  system((
75  "sKizzo -log "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
76 
77  bool result=false;
78 
79  // read result
80  {
81  std::ifstream in(result_tmp_file.c_str());
82 
83  bool result_found=false;
84  while(in)
85  {
86  std::string line;
87 
88  std::getline(in, line);
89 
90  if(line!="" && line[line.size()-1]=='\r')
91  line.resize(line.size()-1);
92 
93  if(line=="The instance evaluates to TRUE.")
94  {
95  result=true;
96  result_found=true;
97  break;
98  }
99  else if(line=="The instance evaluates to FALSE.")
100  {
101  result=false;
102  result_found=true;
103  break;
104  }
105  }
106 
107  if(!result_found)
108  {
109  messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
110  return resultt::P_ERROR;
111  }
112  }
113 
114  remove(result_tmp_file.c_str());
115  remove(qbf_tmp_file.c_str());
116 
117  if(result)
118  {
119  messaget::status() << "Skizzo: TRUE" << messaget::eom;
120 
121  if(get_certificate())
122  return resultt::P_ERROR;
123 
124  return resultt::P_SATISFIABLE;
125  }
126  else
127  {
128  messaget::status() << "Skizzo: FALSE" << messaget::eom;
130  }
131 }
132 
134 {
135  throw "nyi";
136 }
137 
139 {
140  throw "nyi";
141 }
142 
144 {
145  std::string result_tmp_file="ozziKs.out";
146  std::string options="-dump qbm=bdd";
147  std::string log_file=qbf_tmp_file+".sKizzo.log";
148 
149  system((
150  "ozziKs "+options+" "+log_file+" > "+result_tmp_file).c_str());
151 
152  // read result
153  bool result=false;
154  {
155  std::ifstream in(result_tmp_file.c_str());
156  std::string key=" [OK, VALID,";
157 
158  while(in)
159  {
160  std::string line;
161 
162  std::getline(in, line);
163 
164  if(line!="" && line[line.size()-1]=='\r')
165  line.resize(line.size()-1);
166 
167  if(line.compare(0, key.size(), key)==0)
168  {
169  result=true;
170  break;
171  }
172  }
173  }
174 
175  if(!result)
176  {
177  messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
178  return true;
179  }
180 
181  remove(result_tmp_file.c_str());
182  remove(log_file.c_str());
183 
184  // certificate reconstruction done, now let's load it from the .qbm file
185 
186  int n_e;
187  std::vector<int> e_list;
188  int e_max=0;
189 
190  // check header
191  result=false;
192  {
193  std::ifstream in((qbf_tmp_file+".qbm").c_str());
194  std::string key="# existentials[";
195 
196  std::string line;
197  std::getline(in, line);
198 
199  assert(line=="# QBM file, 1.3");
200 
201  while(in)
202  {
203  std::getline(in, line);
204 
205  if(line!="" && line[line.size()-1]=='\r')
206  line.resize(line.size()-1);
207 
208  if(line.compare(0, key.size(), key)==0)
209  {
210  result=true;
211  break;
212  }
213  }
214 
215  size_t ob=line.find('[');
216  std::string n_es=line.substr(ob+1, line.find(']')-ob-1);
217  n_e=unsafe_string2int(n_es);
218  assert(n_e!=0);
219 
220  e_list.resize(n_e);
221  std::string e_lists=line.substr(line.find(':')+2);
222 
223  for(int i=0; i<n_e; i++)
224  {
225  size_t space=e_lists.find(' ');
226 
227  int cur=unsafe_string2int(e_lists.substr(0, space));
228  assert(cur!=0);
229 
230  e_list[i]=cur;
231  if(cur>e_max)
232  e_max=cur;
233 
234  e_lists=e_lists.substr(space+1);
235  }
236 
237  if(!result)
238  throw "existential mapping from sKizzo missing";
239 
240  in.close();
241 
242  // workaround for long comments
243  system((
244  "sed -e \"s/^#.*$/# no comment/\" -i "+qbf_tmp_file+".qbm").c_str());
245  }
246 
247 
248  {
249  DdNode **bdds;
250  std::string bdd_file=qbf_tmp_file+".qbm";
251 
252  // dddmp insists on a non-const string here...
253  // The linter insists on compile time constant for arrays
254  char filename[bdd_file.size()+1]; // NOLINT(*)
255  snprintf(filename, bdd_file.size()+1, "%s", bdd_file.c_str());
256 
257  bdd_manager->AutodynEnable(CUDD_REORDER_SIFT);
258 
259  int nroots=
260  Dddmp_cuddBddArrayLoad(
261  bdd_manager->getManager(),
262  DDDMP_ROOT_MATCHLIST,
263  NULL,
264  DDDMP_VAR_MATCHIDS,
265  NULL,
266  NULL,
267  NULL,
268  DDDMP_MODE_DEFAULT,
269  filename,
270  NULL,
271  &bdds);
272 
273  assert(nroots=2*n_e); // ozziKs documentation guarantees that.
274 
275  model_bdds.resize(e_max+1, NULL);
276 
277  for(unsigned i=0; i<e_list.size(); i++)
278  {
279  int cur=e_list[i];
280  DdNode *posNode=bdds[2*i];
281  DdNode *negNode=bdds[2*i+1];
282 
283  if(Cudd_DagSize(posNode)<=Cudd_DagSize(negNode))
284  model_bdds[cur]=new BDD(*bdd_manager, posNode);
285  else
286  model_bdds[cur]=new BDD(*bdd_manager, Cudd_Not(negNode));
287  }
288 
289  // tell CUDD that we don't need those BDDs anymore.
290  for(int i=0; i<nroots; i++)
291  Cudd_Deref(bdds[i]);
292 
293  free(bdds);
294  bdds=NULL;
295  remove(bdd_file.c_str());
296  remove((qbf_tmp_file+".qbm").c_str());
297  }
298 
299 
300  return false;
301 }
mstreamt & result()
Definition: message.h:233
virtual ~qbf_skizzo_coret()
mstreamt & status()
Definition: message.h:238
model_bddst model_bdds
Definition: qbf_bdd_core.h:27
bool break_lines
Definition: dimacs_cnf.h:36
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void free(void *)
bool get_certificate(void)
virtual modeltypet m_get(literalt a) const
resultt
Definition: prop.h:94
virtual size_t no_clauses() const
virtual bool is_in_core(literalt l) const
mstreamt & error()
Definition: message.h:223
virtual resultt prop_solve()
virtual size_t no_variables() const override
Definition: cnf.h:38
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
virtual const std::string solver_text()
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14
std::string qbf_tmp_file