cprover
qbf_bdd_core.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 #include <solvers/prop/literal.h>
10 
11 #include <fstream>
12 
13 #include <util/arith_tools.h>
14 #include <util/invariant.h>
15 #include <util/std_expr.h>
16 #include <util/expr_util.h>
17 
18 #include <cuddObj.hh> // CUDD Library
19 
21 // FIX FOR THE CUDD LIBRARY
22 
23 inline DdNode *DD::getNode() const
24 {
25  return node;
26 } // DD::getNode
30 #include "qbf_bdd_core.h"
31 
33 {
34  bdd_manager=new Cudd(0, 0);
35 }
36 
38 {
39  for(const BDD* model : model_bdds)
40  {
41  if(model)
42  delete model;
43  }
44  model_bdds.clear();
45 
46  delete(bdd_manager);
47  bdd_manager=NULL;
48 }
49 
51 {
53 
54  if(!is_quantified(l))
55  add_quantifier(quantifiert::typet::EXISTENTIAL, l);
56 
57  return l;
58 }
59 
61 {
62  matrix=new BDD();
63  *matrix=bdd_manager->bddOne();
64 }
65 
67 {
68  for(const BDD* variable : bdd_variable_map)
69  {
70  if(variable)
71  delete variable;
72  }
73  bdd_variable_map.clear();
74 
75  if(matrix)
76  {
77  delete(matrix);
78  matrix=NULL;
79  }
80 }
81 
83 {
85 }
86 
87 const std::string qbf_bdd_coret::solver_text()
88 {
89  return "QBF/BDD/CORE";
90 }
91 
93 {
94  {
95  status() << solver_text() << ": "
96  << std::to_string(no_variables()) << " variables, "
97  << std::to_string(matrix->nodeCount()) << " nodes" << eom;
98  }
99 
100  model_bdds.resize(no_variables()+1, NULL);
101 
102  // Eliminate variables
103  for(auto it=quantifiers.rbegin();
104  it!=quantifiers.rend();
105  it++)
106  {
107  unsigned var=it->var_no;
108 
109  if(it->type==quantifiert::typet::EXISTENTIAL)
110  {
111  #if 0
112  std::cout << "BDD E: " << var << ", " <<
113  matrix->nodeCount() << " nodes\n";
114  #endif
115 
116  BDD *model=new BDD();
117  const BDD &varbdd=*bdd_variable_map[var];
118  *model=matrix->AndAbstract(
119  varbdd.Xnor(bdd_manager->bddOne()),
120  varbdd);
121  model_bdds[var]=model;
122 
123  *matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
124  }
125  else
126  {
127  INVARIANT(
128  it->type == quantifiert::typet::UNIVERSAL,
129  "only handles quantified variables");
130  #if 0
131  std::cout << "BDD A: " << var << ", " <<
132  matrix->nodeCount() << " nodes\n";
133  #endif
134 
135  *matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
136  }
137  }
138 
139  if(*matrix==bdd_manager->bddOne())
140  {
142  return resultt::P_SATISFIABLE;
143  }
144  else if(*matrix==bdd_manager->bddZero())
145  {
146  model_bdds.clear();
148  }
149  else
150  return resultt::P_ERROR;
151 }
152 
154 {
156 }
157 
159 {
161 }
162 
164 {
166 
167  bdd_variable_map.resize(res.var_no()+1, NULL);
168  BDD &var=*(new BDD());
169  var=bdd_manager->bddVar();
170  bdd_variable_map[res.var_no()]=&var;
171 
172  return res;
173 }
174 
175 void qbf_bdd_coret::lcnf(const bvt &bv)
176 {
177  bvt new_bv;
178 
179  if(process_clause(bv, new_bv))
180  return;
181 
182  BDD clause(bdd_manager->bddZero());
183 
184  for(const literalt &l : new_bv)
185  {
186  BDD v(*bdd_variable_map[l.var_no()]);
187 
188  if(l.sign())
189  v=~v;
190 
191  clause|=v;
192  }
193 
194  *matrix&=clause;
195 }
196 
198 {
199  literalt nl=new_variable();
200 
201  BDD abdd(*bdd_variable_map[a.var_no()]);
202  BDD bbdd(*bdd_variable_map[b.var_no()]);
203 
204  if(a.sign())
205  abdd=~abdd;
206  if(b.sign())
207  bbdd=~bbdd;
208 
209  *bdd_variable_map[nl.var_no()]|=abdd | bbdd;
210 
211  return nl;
212 }
213 
215 {
216  for(const literalt &literal : bv)
217  {
218  if(literal==const_literal(true))
219  return literal;
220  }
221 
222  literalt nl=new_variable();
223 
224  BDD &orbdd=*bdd_variable_map[nl.var_no()];
225 
226  for(const literalt &literal : bv)
227  {
228  if(literal==const_literal(false))
229  continue;
230 
231  BDD v(*bdd_variable_map[literal.var_no()]);
232  if(literal.sign())
233  v=~v;
234 
235  orbdd|=v;
236  }
237 
238  return nl;
239 }
240 
242 {
243  status() << "Compressing Certificate" << eom;
244 
245  for(auto it=quantifiers.begin(); it!=quantifiers.end(); it++)
246  {
247  if(it->type==quantifiert::typet::EXISTENTIAL)
248  {
249  const BDD &var=*bdd_variable_map[it->var_no];
250  const BDD &model=*model_bdds[it->var_no];
251 
252  if(model==bdd_manager->bddOne() ||
253  model==bdd_manager->bddZero())
254  {
255  for(auto it2=it; it2!=quantifiers.end(); it2++)
256  {
257  BDD &model2=*model_bdds[it2->var_no];
258 
259  if(model==bdd_manager->bddZero())
260  model2=model2.AndAbstract(~var, var);
261  else
262  model2=model2.AndAbstract(var, var);
263  }
264  }
265  }
266  }
267 }
268 
270 {
271  quantifiert q;
273  !find_quantifier(l, q), "no model for unquantified variables");
274 
275  // universal?
276  if(q.type==quantifiert::typet::UNIVERSAL)
277  {
278  INVARIANT(l.var_no() != 0, "input literal wasn't properly initialized");
279  variable_mapt::const_iterator it=variable_map.find(l.var_no());
280 
281  INVARIANT(
282  it != variable_map.end(), "variable not found in the variable map");
283 
284  const exprt &sym=it->second.first;
285  unsigned index=it->second.second;
286 
287  extractbit_exprt extract_expr(sym, from_integer(index, integer_typet()));
288 
289  if(l.sign())
290  extract_expr = to_extractbit_expr(boolean_negate(extract_expr));
291 
292  return extract_expr;
293  }
294  else
295  {
296  // skolem functions for existentials
297  INVARIANT(
298  q.type == quantifiert::typet::EXISTENTIAL,
299  "only quantified literals are supported");
300 
301  function_cachet::const_iterator it=function_cache.find(l.var_no());
302  if(it!=function_cache.end())
303  {
304  #if 0
305  std::cout << "CACHE HIT for " << l.dimacs() << '\n';
306  #endif
307 
308  if(l.sign())
309  return not_exprt(it->second);
310  else
311  return it->second;
312  }
313 
314  // no cached function, so construct one
315 
316  INVARIANT(
317  model_bdds[l.var_no()] != nullptr,
318  "there must be a model BDD for the literal");
319  BDD &model=*model_bdds[l.var_no()];
320 
321  #if 0
322  std::cout << "Model " << l.var_no() << '\n';
323  model.PrintMinterm();
324  #endif
325 
326  int *cube;
327  DdGen *generator;
328 
330 
331  Cudd_ForeachPrime(
332  bdd_manager->getManager(),
333  model.getNode(),
334  model.getNode(),
335  generator,
336  cube)
337  {
338  and_exprt prime;
339 
340  #if 0
341  std::cout << "CUBE: ";
342  for(signed i=0; i<bdd_manager->ReadSize(); i++)
343  std::cout << cube[i];
344  std::cout << '\n';
345  #endif
346 
347  for(signed i=0; i<bdd_manager->ReadSize(); i++)
348  {
349  if(quantifiers[i].var_no==l.var_no())
350  break; // is this sound?
351 
352  if(cube[i]!=2)
353  {
354  exprt subf=f_get(literalt(quantifiers[i].var_no, (cube[i]==1)));
355  prime.move_to_operands(subf);
356  }
357  }
358 
359  simplify_extractbits(prime);
360 
361  if(prime.operands().empty())
362  result.copy_to_operands(true_exprt());
363  else if(prime.operands().size()==1)
364  result.move_to_operands(prime.op0());
365  else
366  result.move_to_operands(prime);
367  }
368 
369  cube=NULL; // cube is free'd by nextCube
370 
371  exprt final;
372 
373  if(result.operands().empty())
374  final=false_exprt();
375  else if(result.operands().size()==1)
376  final=result.op0();
377  else
378  final=result;
379 
380  function_cache[l.var_no()]=final;
381 
382  if(l.sign())
383  return not_exprt(final);
384  else
385  return final;
386  }
387 }
388 
390 {
391  const BDD &model=*model_bdds[a.var_no()];
392 
393  if(model==bdd_manager->bddZero())
395  else if(model==bdd_manager->bddOne())
397  else
399 }
virtual bool is_in_core(literalt l) const
Boolean negation.
Definition: std_expr.h:3308
variable_mapt variable_map
Definition: qdimacs_core.h:30
virtual void lcnf(const bvt &bv)
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
virtual resultt prop_solve()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual const std::string solver_text()
Deprecated expression utility functions.
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
void simplify_extractbits(exprt &expr) const
virtual tvt l_get(literalt a) const
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
bool is_quantified(const literalt l) const
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:439
int dimacs() const
Definition: literal.h:116
model_bddst model_bdds
Definition: qbf_bdd_core.h:27
virtual literalt lor(literalt a, literalt b)
virtual void add_quantifier(const quantifiert &quantifier)
Definition: qdimacs_cnf.h:63
virtual tvt l_get(literalt a) const
virtual modeltypet m_get(literalt a) const
bdd_variable_mapt bdd_variable_map
Definition: qbf_bdd_core.h:47
The Boolean constant true.
Definition: std_expr.h:4443
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:3127
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
Definition: cnf.cpp:387
function_cachet function_cache
Definition: qbf_bdd_core.h:30
resultt
Definition: prop.h:96
virtual ~qbf_bdd_certificatet(void)
bool find_quantifier(const literalt l, quantifiert &q) const
The Boolean constant false.
Definition: std_expr.h:4452
Unbounded, signed integers (mathematical integers, not bitvectors)
static eomt eom
Definition: message.h:284
literalt const_literal(bool value)
Definition: literal.h:187
#define UNIMPLEMENTED
Definition: invariant.h:497
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
Base class for all expressions.
Definition: expr.h:54
void compress_certificate(void)
bool sign() const
Definition: literal.h:87
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
virtual const exprt f_get(literalt l)
quantifierst quantifiers
Definition: qdimacs_cnf.h:61
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual ~qbf_bdd_coret()
virtual size_t no_variables() const override
Definition: cnf.h:38
operandst & operands()
Definition: expr.h:78
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:127
std::vector< literalt > bvt
Definition: literal.h:200
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3080