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