cprover
qbf_squolem_core.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Squolem Backend (with proofs)
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
11 
12 #include "qbf_squolem_core.h"
13 
14 #include <algorithm>
15 
16 #include <util/std_expr.h>
17 #include <util/arith_tools.h>
18 
19 #include <util/c_types.h> // uint type for indices
20 
22 {
23  setup();
24 }
25 
27 {
28  quantifiers.clear();
29  clauses.clear();
30  early_decision=false;
31  variable_map.clear();
32  squolem=new Squolem2();
33 
34 // squolem->options.set_extractCoreVariables(true);
35 // squolem->options.set_saveCertificate(true);
36  squolem->options.set_keepModelFunctions(true);
37  squolem->options.set_keepResolutionProof(false);
38  squolem->options.set_freeOnExit(true);
39 // squolem->options.set_useExpansion(true);
40  squolem->options.set_debugFilename("debug.qdimacs");
41  squolem->options.set_saveDebugFile(true);
42  squolem->options.set_compressModel(true);
43 // squolem->options.set_showStatus(true);
44 // squolem->options.set_predictOnLiteralBound(true);
45 }
46 
48 {
49  squolem->reset();
50  delete(squolem);
51  squolem=NULL;
52  setup();
53 }
54 
56 {
57  squolem->reset();
58  delete(squolem);
59  squolem=NULL;
60 }
61 
63 {
64  if(a.is_true())
66  else if(a.is_false())
68  else if(squolem->modelIsTrue(a.var_no()))
70  else if(squolem->modelIsFalse(a.var_no()) ||
71  squolem->modelIsDontCare(a.var_no()))
73  else
75 }
76 
77 const std::string qbf_squolem_coret::solver_text()
78 {
79  return "Squolem (Certifying)";
80 }
81 
83 {
84  {
85  std::string msg=
86  "Squolem: "+
87  std::to_string(no_variables())+" variables, "+
88  std::to_string(no_clauses())+" clauses";
89  messaget::status() << msg << messaget::eom;
90  }
91 
92  squolem->endOfOriginals();
93  bool result=squolem->decide();
94 
95  if(result)
96  {
97  messaget::status() << "Squolem: VALID" << messaget::eom;
98  return P_SATISFIABLE;
99  }
100  else
101  {
102  messaget::status() << "Squolem: INVALID" << messaget::eom;
103  return P_UNSATISFIABLE;
104  }
105 
106  return P_ERROR;
107 }
108 
110 {
111  return squolem->inCore(l.var_no());
112 }
113 
115 {
116  if(squolem->modelIsTrue(a.var_no()))
117  return M_TRUE;
118  else if(squolem->modelIsFalse(a.var_no()))
119  return M_FALSE;
120  else if(squolem->modelIsComplex(a.var_no()))
121  return M_COMPLEX;
122  else
123  return M_DONTCARE;
124 }
125 
127 {
128  if(early_decision)
129  return; // we don't need no more...
130 
131  bvt new_bv;
132 
133  if(process_clause(bv, new_bv))
134  return;
135 
136  if(new_bv.empty())
137  {
138  early_decision=true;
139  return;
140  }
141 
142  std::vector<Literal> buffer(new_bv.size());
143  unsigned long i=0;
144  do
145  {
146  buffer[i]=new_bv[i].dimacs();
147  i++;
148  }
149  while(i<new_bv.size());
150 
151  if(!squolem->addClause(buffer))
152  early_decision=true;
153 }
154 
156 {
157  squolem->quantifyVariableInner(
158  quantifier.var_no,
159  quantifier.type==quantifiert::UNIVERSAL);
160 
161  qdimacs_cnft::add_quantifier(quantifier); // necessary?
162 }
163 
165 {
166  squolem->setLastVariable(no+1);
168 }
169 
171  const quantifiert::typet type,
172  const literalt l)
173 {
175  squolem->requantifyVariable(l.var_no(), type==quantifiert::UNIVERSAL);
176 }
177 
178 void qbf_squolem_coret::set_debug_filename(const std::string &str)
179 {
180  squolem->options.set_debugFilename(str.c_str());
181 }
182 
184 {
185  squolem->saveQCNF(out);
186 }
187 
189 {
190  if(squolem->isUniversal(l.var_no()))
191  {
192  assert(l.var_no()!=0);
193  variable_mapt::const_iterator it=variable_map.find(l.var_no());
194 
195  if(it==variable_map.end())
196  throw "variable map error";
197 
198  const exprt &sym=it->second.first;
199  unsigned index=it->second.second;
200 
201  exprt extract_expr(ID_extractbit, typet(ID_bool));
202  extract_expr.copy_to_operands(sym);
203  typet uint_type(ID_unsignedbv);
204  uint_type.set(ID_width, 32);
205  extract_expr.copy_to_operands(from_integer(index, uint_type));
206 
207  if(l.sign())
208  extract_expr.negate();
209 
210  return extract_expr;
211  }
212 
213  function_cachet::const_iterator it=function_cache.find(l.var_no());
214  if(it!=function_cache.end())
215  {
216  #if 0
217  std::cout << "CACHE HIT for " << l.dimacs() << '\n';
218  #endif
219 
220  if(l.sign())
221  return not_exprt(it->second);
222  else
223  return it->second;
224  }
225  else
226  {
227  WitnessStack *wsp=squolem->getModelFunction(Literal(l.dimacs()));
228  exprt res;
229 
230  if(wsp==NULL || wsp->empty())
231  {
232 // res=exprt(ID_nondet_bool, typet(ID_bool));
233  res=false_exprt(); // just set it to zero
234  }
235  else if(wsp->pSize<=wsp->nSize)
236  res=f_get_cnf(wsp);
237  else
238  res=f_get_dnf(wsp);
239 
240  function_cache[l.var_no()]=res;
241 
242  if(l.sign())
243  return not_exprt(res);
244  else
245  return res;
246  }
247 }
248 
249 const exprt qbf_squolem_coret::f_get_cnf(WitnessStack *wsp)
250 {
251  Clause *p=wsp->negWits;
252 
253  if(!p)
254  return exprt(ID_true, typet(ID_bool));
255 
256  exprt::operandst operands;
257 
258  while(p!=NULL)
259  {
260  exprt clause=or_exprt();
261 
262  for(unsigned i=0; i<p->size; i++)
263  {
264  const Literal &lit=p->literals[i];
265  exprt subf=f_get(literalt(var(lit), isPositive(lit))); // negated!
266  if(find(clause.operands().begin(), clause.operands().end(), subf)==
267  clause.operands().end())
268  clause.move_to_operands(subf);
269  }
270 
271  if(clause.operands().empty())
272  clause=false_exprt();
273  else if(clause.operands().size()==1)
274  {
275  const exprt tmp=clause.op0();
276  clause=tmp;
277  }
278 
279  #if 0
280  std::cout << "CLAUSE: " << clause << '\n';
281  #endif
282 
283  operands.push_back(clause);
284 
285  p=p->next;
286  }
287 
288  return and_exprt(operands);
289 }
290 
291 const exprt qbf_squolem_coret::f_get_dnf(WitnessStack *wsp)
292 {
293  Clause *p=wsp->posWits;
294 
295  if(!p)
296  return exprt(ID_false, typet(ID_bool));
297 
298  exprt::operandst operands;
299 
300  while(p!=NULL)
301  {
302  exprt cube=and_exprt();
303 
304  for(unsigned i=0; i<p->size; i++)
305  {
306  const Literal &lit=p->literals[i];
307  exprt subf=f_get(literalt(var(lit), !isPositive(lit)));
308  if(find(cube.operands().begin(), cube.operands().end(), subf)==
309  cube.operands().end())
310  cube.move_to_operands(subf);
311 
312  simplify_extractbits(cube);
313  }
314 
315  if(cube.operands().empty())
316  cube=true_exprt();
317  else if(cube.operands().size()==1)
318  {
319  const exprt tmp=cube.op0();
320  cube=tmp;
321  }
322 
323  #if 0
324  std::cout << "CUBE: " << cube << '\n';
325  #endif
326 
327  operands.push_back(cube);
328 
329  p=p->next;
330  }
331 
332  return or_exprt(operands);
333 }
The type of an expression.
Definition: type.h:20
virtual const std::string solver_text()
mstreamt & result()
Definition: message.h:233
Boolean negation.
Definition: std_expr.h:2648
variable_mapt variable_map
Definition: qdimacs_core.h:30
virtual void add_quantifier(const quantifiert &quantifier)
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
virtual modeltypet m_get(literalt a) const
mstreamt & status()
Definition: message.h:238
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
void simplify_extractbits(exprt &expr) const
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
virtual ~qbf_squolem_coret()
int dimacs() const
Definition: literal.h:116
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void add_quantifier(const quantifiert &quantifier)
Definition: qdimacs_cnf.h:63
const exprt f_get_dnf(WitnessStack *wsp)
The boolean constant true.
Definition: std_expr.h:3742
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.cpp:69
bool is_true() const
Definition: literal.h:155
boolean AND
Definition: std_expr.h:1852
API to expression classes.
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
virtual size_t no_clauses() const
virtual void set_no_variables(size_t no)
The boolean constant false.
Definition: std_expr.h:3753
Squolem Backend (with Proofs)
std::vector< exprt > operandst
Definition: expr.h:49
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual void write_qdimacs_cnf(std::ostream &out)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
Base class for all expressions.
Definition: expr.h:46
bool sign() const
Definition: literal.h:87
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
virtual const exprt f_get(literalt l)
void set_debug_filename(const std::string &str)
void negate()
Definition: expr.cpp:165
function_cachet function_cache
virtual void lcnf(const bvt &bv)
quantifierst quantifiers
Definition: qdimacs_cnf.h:61
virtual size_t no_variables() const override
Definition: cnf.h:38
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const exprt f_get_cnf(WitnessStack *wsp)
std::vector< literalt > bvt
Definition: literal.h:197
virtual bool is_in_core(literalt l) const
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_false() const
Definition: literal.h:160