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  extractbit_exprt extract_expr(sym, from_integer(index, integer_typet()));
202 
203  if(l.sign())
204  extract_expr = to_extractbit_expr(boolean_negate(extract_expr));
205 
206  return extract_expr;
207  }
208 
209  function_cachet::const_iterator it=function_cache.find(l.var_no());
210  if(it!=function_cache.end())
211  {
212  #if 0
213  std::cout << "CACHE HIT for " << l.dimacs() << '\n';
214  #endif
215 
216  if(l.sign())
217  return not_exprt(it->second);
218  else
219  return it->second;
220  }
221  else
222  {
223  WitnessStack *wsp=squolem->getModelFunction(Literal(l.dimacs()));
224  exprt res;
225 
226  if(wsp==NULL || wsp->empty())
227  {
228 // res=exprt(ID_nondet_bool, typet(ID_bool));
229  res=false_exprt(); // just set it to zero
230  }
231  else if(wsp->pSize<=wsp->nSize)
232  res=f_get_cnf(wsp);
233  else
234  res=f_get_dnf(wsp);
235 
236  function_cache[l.var_no()]=res;
237 
238  if(l.sign())
239  return not_exprt(res);
240  else
241  return res;
242  }
243 }
244 
245 const exprt qbf_squolem_coret::f_get_cnf(WitnessStack *wsp)
246 {
247  Clause *p=wsp->negWits;
248 
249  if(!p)
250  return exprt(ID_true, typet(ID_bool));
251 
252  exprt::operandst operands;
253 
254  while(p!=NULL)
255  {
256  or_exprt clause;
257 
258  for(unsigned i=0; i<p->size; i++)
259  {
260  const Literal &lit=p->literals[i];
261  exprt subf=f_get(literalt(var(lit), isPositive(lit))); // negated!
262  if(find(clause.operands().begin(), clause.operands().end(), subf)==
263  clause.operands().end())
264  clause.move_to_operands(subf);
265  }
266 
267  if(clause.operands().empty())
268  clause=false_exprt();
269  else if(clause.operands().size()==1)
270  {
271  const exprt tmp=clause.op0();
272  clause=tmp;
273  }
274 
275  #if 0
276  std::cout << "CLAUSE: " << clause << '\n';
277  #endif
278 
279  operands.push_back(clause);
280 
281  p=p->next;
282  }
283 
284  return and_exprt(operands);
285 }
286 
287 const exprt qbf_squolem_coret::f_get_dnf(WitnessStack *wsp)
288 {
289  Clause *p=wsp->posWits;
290 
291  if(!p)
292  return exprt(ID_false, typet(ID_bool));
293 
294  exprt::operandst operands;
295 
296  while(p!=NULL)
297  {
298  and_exprt cube;
299 
300  for(unsigned i=0; i<p->size; i++)
301  {
302  const Literal &lit=p->literals[i];
303  exprt subf=f_get(literalt(var(lit), !isPositive(lit)));
304  if(find(cube.operands().begin(), cube.operands().end(), subf)==
305  cube.operands().end())
306  cube.move_to_operands(subf);
307 
308  simplify_extractbits(cube);
309  }
310 
311  if(cube.operands().empty())
312  cube=true_exprt();
313  else if(cube.operands().size()==1)
314  {
315  const exprt tmp=cube.op0();
316  cube=tmp;
317  }
318 
319  #if 0
320  std::cout << "CUBE: " << cube << '\n';
321  #endif
322 
323  operands.push_back(cube);
324 
325  p=p->next;
326  }
327 
328  return or_exprt(operands);
329 }
The type of an expression.
Definition: type.h:22
virtual const std::string solver_text()
Boolean negation.
Definition: std_expr.h:3228
variable_mapt variable_map
Definition: qdimacs_core.h:30
virtual void add_quantifier(const quantifiert &quantifier)
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
virtual modeltypet m_get(literalt a) const
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 move_to_operands(exprt &expr)
Definition: expr.cpp:22
virtual ~qbf_squolem_coret()
int dimacs() const
Definition: literal.h:116
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
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:4486
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Definition: qdimacs_cnf.cpp:69
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:3037
bool is_true() const
Definition: literal.h:155
boolean AND
Definition: std_expr.h:2255
API to expression classes.
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:96
virtual size_t no_clauses() const
virtual void set_no_variables(size_t no)
The boolean constant false.
Definition: std_expr.h:4497
Squolem Backend (with Proofs)
std::vector< exprt > operandst
Definition: expr.h:45
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Unbounded, signed integers.
Definition: std_types.h:70
virtual void write_qdimacs_cnf(std::ostream &out)
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
Base class for all expressions.
Definition: expr.h:42
bool sign() const
Definition: literal.h:87
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual const exprt f_get(literalt l)
void set_debug_filename(const std::string &str)
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:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:126
const exprt f_get_cnf(WitnessStack *wsp)
std::vector< literalt > bvt
Definition: literal.h:200
virtual bool is_in_core(literalt l) const
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2989
bool is_false() const
Definition: literal.h:160