cprover
cnf.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CNF Generation, via Tseitin
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cnf.h"
13 
14 #include <algorithm>
15 #include <set>
16 
17 #include <util/invariant.h>
18 
19 // #define VERBOSE
20 
26 {
27  // a*b=c <==> (a + o')( b + o')(a'+b'+o)
28  bvt lits(2);
29 
30  lits[0]=pos(a);
31  lits[1]=neg(o);
32  lcnf(lits);
33 
34  lits[0]=pos(b);
35  lits[1]=neg(o);
36  lcnf(lits);
37 
38  lits.clear();
39  lits.reserve(3);
40  lits.push_back(neg(a));
41  lits.push_back(neg(b));
42  lits.push_back(pos(o));
43  lcnf(lits);
44 }
45 
49 {
50  // a+b=c <==> (a' + c)( b' + c)(a + b + c')
51  bvt lits(2);
52 
53  lits[0]=neg(a);
54  lits[1]=pos(o);
55  lcnf(lits);
56 
57  lits[0]=neg(b);
58  lits[1]=pos(o);
59  lcnf(lits);
60 
61  lits.resize(3);
62  lits[0]=pos(a);
63  lits[1]=pos(b);
64  lits[2]=neg(o);
65  lcnf(lits);
66 }
67 
71 {
72  // a xor b = o <==> (a' + b' + o')
73  // (a + b + o' )
74  // (a' + b + o)
75  // (a + b' + o)
76  bvt lits(3);
77 
78  lits[0]=neg(a);
79  lits[1]=neg(b);
80  lits[2]=neg(o);
81  lcnf(lits);
82 
83  lits[0]=pos(a);
84  lits[1]=pos(b);
85  lits[2]=neg(o);
86  lcnf(lits);
87 
88  lits[0]=neg(a);
89  lits[1]=pos(b);
90  lits[2]=pos(o);
91  lcnf(lits);
92 
93  lits[0]=pos(a);
94  lits[1]=neg(b);
95  lits[2]=pos(o);
96  lcnf(lits);
97 }
98 
102 {
103  // a Nand b = o <==> (a + o)( b + o)(a' + b' + o')
104  bvt lits(2);
105 
106  lits[0]=pos(a);
107  lits[1]=pos(o);
108  lcnf(lits);
109 
110  lits[0]=pos(b);
111  lits[1]=pos(o);
112  lcnf(lits);
113 
114  lits.resize(3);
115  lits[0]=neg(a);
116  lits[1]=neg(b);
117  lits[2]=neg(o);
118  lcnf(lits);
119 }
120 
124 {
125  // a Nor b = o <==> (a' + o')( b' + o')(a + b + o)
126  bvt lits(2);
127 
128  lits[0]=neg(a);
129  lits[1]=neg(o);
130  lcnf(lits);
131 
132  lits[0]=neg(b);
133  lits[1]=neg(o);
134  lcnf(lits);
135 
136  lits.resize(3);
137  lits[0]=pos(a);
138  lits[1]=pos(b);
139  lits[2]=pos(o);
140  lcnf(lits);
141 }
142 
146 {
147  gate_xor(a, b, !o);
148 }
149 
153 {
154  gate_or(!a, b, o);
155 }
156 
161 {
162  if(bv.empty())
163  return const_literal(true);
164  if(bv.size()==1)
165  return bv[0];
166  if(bv.size()==2)
167  return land(bv[0], bv[1]);
168 
169  for(const auto &l : bv)
170  if(l.is_false())
171  return l;
172 
173  if(is_all(bv, const_literal(true)))
174  return const_literal(true);
175 
176  bvt new_bv=eliminate_duplicates(bv);
177 
178  bvt lits(2);
179  literalt literal=new_variable();
180  lits[1]=neg(literal);
181 
182  for(const auto &l : new_bv)
183  {
184  lits[0]=pos(l);
185  lcnf(lits);
186  }
187 
188  lits.clear();
189  lits.reserve(new_bv.size()+1);
190 
191  for(const auto &l : new_bv)
192  lits.push_back(neg(l));
193 
194  lits.push_back(pos(literal));
195  lcnf(lits);
196 
197  return literal;
198 }
199 
204 {
205  if(bv.empty())
206  return const_literal(false);
207  if(bv.size()==1)
208  return bv[0];
209  if(bv.size()==2)
210  return lor(bv[0], bv[1]);
211 
212  for(const auto &l : bv)
213  if(l.is_true())
214  return l;
215 
216  if(is_all(bv, const_literal(false)))
217  return const_literal(false);
218 
219  bvt new_bv=eliminate_duplicates(bv);
220 
221  bvt lits(2);
222  literalt literal=new_variable();
223  lits[1]=pos(literal);
224 
225  for(const auto &l : new_bv)
226  {
227  lits[0]=neg(l);
228  lcnf(lits);
229  }
230 
231  lits.clear();
232  lits.reserve(new_bv.size()+1);
233 
234  for(const auto &l : new_bv)
235  lits.push_back(pos(l));
236 
237  lits.push_back(neg(literal));
238  lcnf(lits);
239 
240  return literal;
241 }
242 
247 {
248  if(bv.empty())
249  return const_literal(false);
250  if(bv.size()==1)
251  return bv[0];
252  if(bv.size()==2)
253  return lxor(bv[0], bv[1]);
254 
255  literalt literal=const_literal(false);
256 
257  for(const auto &l : bv)
258  literal=lxor(l, literal);
259 
260  return literal;
261 }
262 
266 {
267  if(a.is_true() || b.is_false())
268  return b;
269  if(b.is_true() || a.is_false())
270  return a;
271  if(a==b)
272  return a;
273 
275  gate_and(a, b, o);
276  return o;
277 }
278 
282 {
283  if(a.is_false() || b.is_true())
284  return b;
285  if(b.is_false() || a.is_true())
286  return a;
287  if(a==b)
288  return a;
289 
291  gate_or(a, b, o);
292  return o;
293 }
294 
298 {
299  if(a.is_false())
300  return b;
301  if(b.is_false())
302  return a;
303  if(a.is_true())
304  return !b;
305  if(b.is_true())
306  return !a;
307  if(a==b)
308  return const_literal(false);
309  if(a==!b)
310  return const_literal(true);
311 
313  gate_xor(a, b, o);
314  return o;
315 }
316 
320 {
321  return !land(a, b);
322 }
323 
327 {
328  return !lor(a, b);
329 }
330 
332 {
333  return !lxor(a, b);
334 }
335 
337 {
338  return lor(!a, b);
339 }
340 
341 // Tino observed slow-downs up to 50% with OPTIMAL_COMPACT_ITE.
342 
343 #define COMPACT_ITE
344 // #define OPTIMAL_COMPACT_ITE
345 
347 {
348  // a?b:c = (a AND b) OR (/a AND c)
349  if(a.is_constant())
350  return a.sign() ? b : c;
351  if(b==c)
352  return b;
353 
354  if(b.is_constant())
355  return b.sign() ? lor(a, c) : land(!a, c);
356  if(c.is_constant())
357  return c.sign() ? lor(!a, b) : land(a, b);
358 
359  #ifdef COMPACT_ITE
360 
361  // (a+c'+o) (a+c+o') (a'+b'+o) (a'+b+o')
362 
364 
365  bvt lits;
366 
367  lcnf(a, !c, o);
368  lcnf(a, c, !o);
369  lcnf(!a, !b, o);
370  lcnf(!a, b, !o);
371 
372  #ifdef OPTIMAL_COMPACT_ITE
373  // additional clauses to enable better propagation
374  lcnf(b, c, !o);
375  lcnf(!b, !c, o);
376  #endif
377 
378  return o;
379 
380  #else
381  return lor(land(a, b), land(!a, c));
382  #endif
383 }
384 
388 {
389  literalt l;
390  l.set(_no_variables, false);
391 
393 
394  return l;
395 }
396 
401 {
402  std::set<literalt> s;
403 
404  bvt dest;
405  dest.reserve(bv.size());
406 
407  for(const auto &l : bv)
408  if(s.insert(l).second)
409  dest.push_back(l);
410 
411  return dest;
412 }
413 
416 bool cnft::process_clause(const bvt &bv, bvt &dest)
417 {
418  dest.clear();
419 
420  // empty clause! this is UNSAT
421  if(bv.empty())
422  return false;
423 
424  // first check simple things
425 
426  for(const auto &l : bv)
427  {
428  // we never use index 0
429  INVARIANT(l.var_no() != 0, "variable 0 must not be used");
430 
431  // we never use 'unused_var_no'
432  INVARIANT(
433  l.var_no() != literalt::unused_var_no(),
434  "variable 'unused_var_no' must not be used");
435 
436  if(l.is_true())
437  return true; // clause satisfied
438 
439  if(l.is_false())
440  continue; // will remove later
441 
442  INVARIANT(
443  l.var_no() < _no_variables,
444  "unknown variable " + std::to_string(l.var_no()) +
445  " (no_variables = " + std::to_string(_no_variables) + " )");
446  }
447 
448  // now copy
449  dest.clear();
450  dest.reserve(bv.size());
451 
452  for(const auto &l : bv)
453  {
454  if(l.is_false())
455  continue; // remove
456 
457  dest.push_back(l);
458  }
459 
460  // now sort
461  std::sort(dest.begin(), dest.end());
462 
463  // eliminate duplicates and find occurrences of a variable
464  // and its negation
465 
466  if(dest.size()>=2)
467  {
468  bvt::iterator it=dest.begin();
469  literalt previous=*it;
470 
471  for(it++;
472  it!=dest.end();
473  ) // no it++
474  {
475  literalt l=*it;
476 
477  // prevent duplicate literals
478  if(l==previous)
479  it=dest.erase(it);
480  else if(previous==!l)
481  return true; // clause satisfied trivially
482  else
483  {
484  previous=l;
485  it++;
486  }
487  }
488  }
489 
490  return false;
491 }
cnft::lnand
virtual literalt lnand(literalt a, literalt b) override
Definition: cnf.cpp:319
pos
literalt pos(literalt a)
Definition: literal.h:194
cnft::gate_xor
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
Definition: cnf.cpp:70
cnft::process_clause
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
bvt
std::vector< literalt > bvt
Definition: literal.h:201
cnft::lnor
virtual literalt lnor(literalt a, literalt b) override
Definition: cnf.cpp:326
invariant.h
cnft::gate_equal
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
Definition: cnf.cpp:145
cnft::lxor
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.
Definition: cnf.cpp:246
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
cnft::gate_nor
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
Definition: cnf.cpp:123
cnft::land
virtual literalt land(literalt a, literalt b) override
Definition: cnf.cpp:265
literalt::unused_var_no
static var_not unused_var_no()
Definition: literal.h:176
cnft::gate_or
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
Definition: cnf.cpp:48
cnft::is_all
static bool is_all(const bvt &bv, literalt l)
Definition: cnf.h:60
literalt::is_true
bool is_true() const
Definition: literal.h:156
cnft::lor
virtual literalt lor(literalt a, literalt b) override
Definition: cnf.cpp:281
cnft::set_no_variables
virtual void set_no_variables(size_t no)
Definition: cnf.h:42
cnft::new_variable
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
Definition: cnf.cpp:387
cnft::limplies
virtual literalt limplies(literalt a, literalt b) override
Definition: cnf.cpp:336
cnft::gate_implies
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
Definition: cnf.cpp:152
cnft::eliminate_duplicates
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
Definition: cnf.cpp:400
literalt::is_false
bool is_false() const
Definition: literal.h:161
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
cnft::lselect
virtual literalt lselect(literalt a, literalt b, literalt c) override
Definition: cnf.cpp:346
literalt::sign
bool sign() const
Definition: literal.h:88
cnft::gate_and
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
Definition: cnf.cpp:25
literalt::set
void set(var_not _l)
Definition: literal.h:93
cnft::gate_nand
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
Definition: cnf.cpp:101
literalt
Definition: literal.h:26
cnft::_no_variables
size_t _no_variables
Definition: cnf.h:56
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
neg
literalt neg(literalt a)
Definition: literal.h:193
cnf.h
CNF Generation, via Tseitin.
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
validation_modet::INVARIANT
@ INVARIANT
cnft::lequal
virtual literalt lequal(literalt a, literalt b) override
Definition: cnf.cpp:331