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 #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 {
84  assert(false);
85  return tvt(false);
86 }
87 
88 const std::string qbf_bdd_coret::solver_text()
89 {
90  return "QBF/BDD/CORE";
91 }
92 
94 {
95  {
96  status() << solver_text() << ": "
97  << std::to_string(no_variables()) << " variables, "
98  << std::to_string(matrix->nodeCount()) << " nodes" << eom;
99  }
100 
101  model_bdds.resize(no_variables()+1, NULL);
102 
103  // Eliminate variables
104  for(auto it=quantifiers.rbegin();
105  it!=quantifiers.rend();
106  it++)
107  {
108  unsigned var=it->var_no;
109 
110  if(it->type==quantifiert::typet::EXISTENTIAL)
111  {
112  #if 0
113  std::cout << "BDD E: " << var << ", " <<
114  matrix->nodeCount() << " nodes\n";
115  #endif
116 
117  BDD *model=new BDD();
118  const BDD &varbdd=*bdd_variable_map[var];
119  *model=matrix->AndAbstract(
120  varbdd.Xnor(bdd_manager->bddOne()),
121  varbdd);
122  model_bdds[var]=model;
123 
124  *matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
125  }
126  else if(it->type==quantifiert::typet::UNIVERSAL)
127  {
128  #if 0
129  std::cout << "BDD A: " << var << ", " <<
130  matrix->nodeCount() << " nodes\n";
131  #endif
132 
133  *matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
134  }
135  else
136  throw "unquantified variable";
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 {
155  throw "nyi";
156 }
157 
159 {
160  throw "nyi";
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;
272  if(!find_quantifier(l, q))
273  throw "no model for unquantified variable";
274 
275  // universal?
276  if(q.type==quantifiert::typet::UNIVERSAL)
277  {
278  assert(l.var_no()!=0);
279  variable_mapt::const_iterator it=variable_map.find(l.var_no());
280 
281  if(it==variable_map.end())
282  throw "variable map error";
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  assert(q.type==quantifiert::typet::EXISTENTIAL);
298 
299  function_cachet::const_iterator it=function_cache.find(l.var_no());
300  if(it!=function_cache.end())
301  {
302  #if 0
303  std::cout << "CACHE HIT for " << l.dimacs() << '\n';
304  #endif
305 
306  if(l.sign())
307  return not_exprt(it->second);
308  else
309  return it->second;
310  }
311 
312  // no cached function, so construct one
313 
314  assert(model_bdds[l.var_no()]!=NULL);
315  BDD &model=*model_bdds[l.var_no()];
316 
317  #if 0
318  std::cout << "Model " << l.var_no() << '\n';
319  model.PrintMinterm();
320  #endif
321 
322  int *cube;
323  DdGen *generator;
324 
326 
327  Cudd_ForeachPrime(
328  bdd_manager->getManager(),
329  model.getNode(),
330  model.getNode(),
331  generator,
332  cube)
333  {
334  and_exprt prime;
335 
336  #if 0
337  std::cout << "CUBE: ";
338  for(signed i=0; i<bdd_manager->ReadSize(); i++)
339  std::cout << cube[i];
340  std::cout << '\n';
341  #endif
342 
343  for(signed i=0; i<bdd_manager->ReadSize(); i++)
344  {
345  if(quantifiers[i].var_no==l.var_no())
346  break; // is this sound?
347 
348  if(cube[i]!=2)
349  {
350  exprt subf=f_get(literalt(quantifiers[i].var_no, (cube[i]==1)));
351  prime.move_to_operands(subf);
352  }
353  }
354 
355  simplify_extractbits(prime);
356 
357  if(prime.operands().empty())
358  result.copy_to_operands(true_exprt());
359  else if(prime.operands().size()==1)
360  result.move_to_operands(prime.op0());
361  else
362  result.move_to_operands(prime);
363  }
364 
365  cube=NULL; // cube is free'd by nextCube
366 
367  exprt final;
368 
369  if(result.operands().empty())
370  final=false_exprt();
371  else if(result.operands().size()==1)
372  final=result.op0();
373  else
374  final=result;
375 
376  function_cache[l.var_no()]=final;
377 
378  if(l.sign())
379  return not_exprt(final);
380  else
381  return final;
382  }
383 }
384 
386 {
387  const BDD &model=*model_bdds[a.var_no()];
388 
389  if(model==bdd_manager->bddZero())
391  else if(model==bdd_manager->bddOne())
393  else
395 }
virtual bool is_in_core(literalt l) const
Boolean negation.
Definition: std_expr.h:3228
variable_mapt variable_map
Definition: qdimacs_core.h:30
virtual void lcnf(const bvt &bv)
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
virtual resultt prop_solve()
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)
Definition: expr.cpp:22
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:272
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:4486
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:3037
boolean AND
Definition: std_expr.h:2255
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:4497
Unbounded, signed integers.
Definition: std_types.h:70
literalt const_literal(bool value)
Definition: literal.h:187
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
Base class for all expressions.
Definition: expr.h:42
void compress_certificate(void)
bool sign() const
Definition: literal.h:87
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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: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
std::vector< literalt > bvt
Definition: literal.h:200
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2989