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 <cassert>
12 #include <fstream>
13 
14 #include <util/arith_tools.h>
15 #include <util/std_expr.h>
16 
17 #include <langapi/language_util.h>
18 
19 #include <cuddObj.hh> // CUDD Library
20 
22 // FIX FOR THE CUDD LIBRARY
23 
24 inline DdNode *DD::getNode() const
25 {
26  return node;
27 } // DD::getNode
31 #include "qbf_bdd_core.h"
32 
34 {
35  bdd_manager=new Cudd(0, 0);
36 }
37 
39 {
40  for(const BDD* model : model_bdds)
41  {
42  if(model)
43  delete model;
44  }
45  model_bdds.clear();
46 
47  delete(bdd_manager);
48  bdd_manager=NULL;
49 }
50 
52 {
54 
55  if(!is_quantified(l))
56  add_quantifier(quantifiert::typet::EXISTENTIAL, l);
57 
58  return l;
59 }
60 
62 {
63  matrix=new BDD();
64  *matrix=bdd_manager->bddOne();
65 }
66 
68 {
69  for(const BDD* variable : bdd_variable_map)
70  {
71  if(variable)
72  delete variable;
73  }
74  bdd_variable_map.clear();
75 
76  if(matrix)
77  {
78  delete(matrix);
79  matrix=NULL;
80  }
81 }
82 
84 {
85  assert(false);
86  return tvt(false);
87 }
88 
89 const std::string qbf_bdd_coret::solver_text()
90 {
91  return "QBF/BDD/CORE";
92 }
93 
95 {
96  {
97  status() << solver_text() << ": "
98  << std::to_string(no_variables()) << " variables, "
99  << std::to_string(matrix->nodeCount()) << " nodes" << eom;
100  }
101 
102  model_bdds.resize(no_variables()+1, NULL);
103 
104  // Eliminate variables
105  for(auto it=quantifiers.rbegin();
106  it!=quantifiers.rend();
107  it++)
108  {
109  unsigned var=it->var_no;
110 
111  if(it->type==quantifiert::typet::EXISTENTIAL)
112  {
113  #if 0
114  std::cout << "BDD E: " << var << ", " <<
115  matrix->nodeCount() << " nodes\n";
116  #endif
117 
118  BDD *model=new BDD();
119  const BDD &varbdd=*bdd_variable_map[var];
120  *model=matrix->AndAbstract(
121  varbdd.Xnor(bdd_manager->bddOne()),
122  varbdd);
123  model_bdds[var]=model;
124 
125  *matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
126  }
127  else if(it->type==quantifiert::typet::UNIVERSAL)
128  {
129  #if 0
130  std::cout << "BDD A: " << var << ", " <<
131  matrix->nodeCount() << " nodes\n";
132  #endif
133 
134  *matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
135  }
136  else
137  throw "unquantified variable";
138  }
139 
140  if(*matrix==bdd_manager->bddOne())
141  {
143  return resultt::P_SATISFIABLE;
144  }
145  else if(*matrix==bdd_manager->bddZero())
146  {
147  model_bdds.clear();
149  }
150  else
151  return resultt::P_ERROR;
152 }
153 
155 {
156  throw "nyi";
157 }
158 
160 {
161  throw "nyi";
162 }
163 
165 {
167 
168  bdd_variable_map.resize(res.var_no()+1, NULL);
169  BDD &var=*(new BDD());
170  var=bdd_manager->bddVar();
171  bdd_variable_map[res.var_no()]=&var;
172 
173  return res;
174 }
175 
176 void qbf_bdd_coret::lcnf(const bvt &bv)
177 {
178  bvt new_bv;
179 
180  if(process_clause(bv, new_bv))
181  return;
182 
183  BDD clause(bdd_manager->bddZero());
184 
185  for(const literalt &l : new_bv)
186  {
187  BDD v(*bdd_variable_map[l.var_no()]);
188 
189  if(l.sign())
190  v=~v;
191 
192  clause|=v;
193  }
194 
195  *matrix&=clause;
196 }
197 
199 {
200  literalt nl=new_variable();
201 
202  BDD abdd(*bdd_variable_map[a.var_no()]);
203  BDD bbdd(*bdd_variable_map[b.var_no()]);
204 
205  if(a.sign())
206  abdd=~abdd;
207  if(b.sign())
208  bbdd=~bbdd;
209 
210  *bdd_variable_map[nl.var_no()]|=abdd | bbdd;
211 
212  return nl;
213 }
214 
216 {
217  for(const literalt &literal : bv)
218  {
219  if(literal==const_literal(true))
220  return literal;
221  }
222 
223  literalt nl=new_variable();
224 
225  BDD &orbdd=*bdd_variable_map[nl.var_no()];
226 
227  for(const literalt &literal : bv)
228  {
229  if(literal==const_literal(false))
230  continue;
231 
232  BDD v(*bdd_variable_map[literal.var_no()]);
233  if(literal.sign())
234  v=~v;
235 
236  orbdd|=v;
237  }
238 
239  return nl;
240 }
241 
243 {
244  status() << "Compressing Certificate" << eom;
245 
246  for(auto it=quantifiers.begin(); it!=quantifiers.end(); it++)
247  {
248  if(it->type==quantifiert::typet::EXISTENTIAL)
249  {
250  const BDD &var=*bdd_variable_map[it->var_no];
251  const BDD &model=*model_bdds[it->var_no];
252 
253  if(model==bdd_manager->bddOne() ||
254  model==bdd_manager->bddZero())
255  {
256  for(auto it2=it; it2!=quantifiers.end(); it2++)
257  {
258  BDD &model2=*model_bdds[it2->var_no];
259 
260  if(model==bdd_manager->bddZero())
261  model2=model2.AndAbstract(~var, var);
262  else
263  model2=model2.AndAbstract(var, var);
264  }
265  }
266  }
267  }
268 }
269 
271 {
272  quantifiert q;
273  if(!find_quantifier(l, q))
274  throw "no model for unquantified variable";
275 
276  // universal?
277  if(q.type==quantifiert::typet::UNIVERSAL)
278  {
279  assert(l.var_no()!=0);
280  variable_mapt::const_iterator it=variable_map.find(l.var_no());
281 
282  if(it==variable_map.end())
283  throw "variable map error";
284 
285  const exprt &sym=it->second.first;
286  unsigned index=it->second.second;
287 
288  exprt extract_expr(ID_extractbit, typet(ID_bool));
289  extract_expr.copy_to_operands(sym);
290 
291  typet uint_type(ID_unsignedbv);
292  uint_type.set(ID_width, 32);
293  extract_expr.copy_to_operands(from_integer(index, uint_type));
294 
295  if(l.sign())
296  extract_expr.negate();
297 
298  return extract_expr;
299  }
300  else
301  {
302  // skolem functions for existentials
303  assert(q.type==quantifiert::typet::EXISTENTIAL);
304 
305  function_cachet::const_iterator it=function_cache.find(l.var_no());
306  if(it!=function_cache.end())
307  {
308  #if 0
309  std::cout << "CACHE HIT for " << l.dimacs() << '\n';
310  #endif
311 
312  if(l.sign())
313  return not_exprt(it->second);
314  else
315  return it->second;
316  }
317 
318  // no cached function, so construct one
319 
320  assert(model_bdds[l.var_no()]!=NULL);
321  BDD &model=*model_bdds[l.var_no()];
322 
323  #if 0
324  std::cout << "Model " << l.var_no() << '\n';
325  model.PrintMinterm();
326  #endif
327 
328  int *cube;
329  DdGen *generator;
330 
332 
333  Cudd_ForeachPrime(
334  bdd_manager->getManager(),
335  model.getNode(),
336  model.getNode(),
337  generator,
338  cube)
339  {
340  exprt prime=and_exprt();
341 
342  #if 0
343  std::cout << "CUBE: ";
344  for(signed i=0; i<bdd_manager->ReadSize(); i++)
345  std::cout << cube[i];
346  std::cout << '\n';
347  #endif
348 
349  for(signed i=0; i<bdd_manager->ReadSize(); i++)
350  {
351  if(quantifiers[i].var_no==l.var_no())
352  break; // is this sound?
353 
354  if(cube[i]!=2)
355  {
356  exprt subf=f_get(literalt(quantifiers[i].var_no, (cube[i]==1)));
357  prime.move_to_operands(subf);
358  }
359  }
360 
361  simplify_extractbits(prime);
362 
363  if(prime.operands().empty())
364  result.copy_to_operands(true_exprt());
365  else if(prime.operands().size()==1)
366  result.move_to_operands(prime.op0());
367  else
368  result.move_to_operands(prime);
369  }
370 
371  cube=NULL; // cube is free'd by nextCube
372 
373  exprt final;
374 
375  if(result.operands().empty())
376  final=false_exprt();
377  else if(result.operands().size()==1)
378  final=result.op0();
379  else
380  final=result;
381 
382  function_cache[l.var_no()]=final;
383 
384  if(l.sign())
385  return not_exprt(final);
386  else
387  return final;
388  }
389 }
390 
392 {
393  const BDD &model=*model_bdds[a.var_no()];
394 
395  if(model==bdd_manager->bddZero())
397  else if(model==bdd_manager->bddOne())
399  else
401 }
The type of an expression.
Definition: type.h:20
virtual bool is_in_core(literalt l) const
mstreamt & result()
Definition: message.h:233
Boolean negation.
Definition: std_expr.h:2648
variable_mapt variable_map
Definition: qdimacs_core.h:30
virtual void lcnf(const bvt &bv)
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
virtual resultt prop_solve()
mstreamt & status()
Definition: message.h:238
virtual const std::string solver_text()
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 copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
bool is_quantified(const literalt l) const
int dimacs() const
Definition: literal.h:116
model_bddst model_bdds
Definition: qbf_bdd_core.h:27
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
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:3742
boolean AND
Definition: std_expr.h:1852
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:94
virtual ~qbf_bdd_certificatet(void)
bool find_quantifier(const literalt l, quantifiert &q) const
The boolean constant false.
Definition: std_expr.h:3753
literalt const_literal(bool value)
Definition: literal.h:187
Base class for all expressions.
Definition: expr.h:46
void compress_certificate(void)
bool sign() const
Definition: literal.h:87
virtual const exprt f_get(literalt l)
void negate()
Definition: expr.cpp:165
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:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:197
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214