cprover
aig_prop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "aig_prop.h"
10 
11 #include <set>
12 #include <stack>
13 
14 // Tries to compact AIGs corresponding to xor and equality
15 // Needed to match the performance of the native CNF back-end.
16 #define USE_AIG_COMPACT
17 
18 // Use the Plaisted-Greenbaum encoding, again, needed to match the
19 // native CNF back-end.
20 #define USE_PG
21 
23 {
24  literalt literal=const_literal(true);
25 
26  // Introduces N-1 extra nodes for N bits
27  // See convert_node for where this overhead is removed
28  forall_literals(it, bv)
29  literal=land(*it, literal);
30 
31  return literal;
32 }
33 
35 {
36  literalt literal=const_literal(true);
37 
38  // Introduces N-1 extra nodes for N bits
39  // See convert_node for where this overhead is removed
40  forall_literals(it, bv)
41  literal=land(neg(*it), literal);
42 
43  return neg(literal);
44 }
45 
47 {
48  literalt literal=const_literal(false);
49 
50  forall_literals(it, bv)
51  literal=lxor(*it, literal);
52 
53  return literal;
54 }
55 
57 {
58  if(a.is_true() || b.is_false())
59  return b;
60  if(b.is_true() || a.is_false())
61  return a;
62 
63  if(a==neg(b))
64  return const_literal(false);
65  if(a==b)
66  return a;
67 
68  return dest.new_and_node(a, b);
69 }
70 
72 {
73  return neg(land(neg(a), neg(b))); // De Morgan's
74 }
75 
77 {
78  if(a.is_false())
79  return b;
80  if(b.is_false())
81  return a;
82  if(a.is_true())
83  return neg(b);
84  if(b.is_true())
85  return neg(a);
86 
87  if(a==b)
88  return const_literal(false);
89  if(a==neg(b))
90  return const_literal(true);
91 
92  // This produces up to three nodes!
93  // See convert_node for where this overhead is removed
94  return lor(land(a, neg(b)), land(neg(a), b));
95 }
96 
98 {
99  return !land(a, b);
100 }
101 
103 {
104  return !lor(a, b);
105 }
106 
108 {
109  return !lxor(a, b);
110 }
111 
113 {
114  return lor(neg(a), b);
115 }
116 
118 { // a?b:c=(a AND b) OR (/a AND c)
119  if(a.is_true())
120  return b;
121  if(a.is_false())
122  return c;
123  if(b==c)
124  return b;
125 
126  // This produces unnecessary clauses and variables
127  // See convert_node for where this overhead is removed
128 
129  return lor(land(a, b), land(neg(a), c));
130 }
131 
133 {
134 #ifdef USE_AIG_COMPACT
135  // The compact encoding should reduce this
136  l_set_to_true(lequal(a, b));
137 
138 #else
139  // we produce two constraints:
140  // a|!b !a|b
141 
142  l_set_to_true(lor(pos(a), neg(b)));
143  l_set_to_true(lor(neg(a), pos(b)));
144 #endif
145 }
146 
148 {
149  return solver.l_get(a);
150 }
151 
153 {
154  status() << "converting AIG, "
155  << aig.nodes.size() << " nodes" << eom;
156  convert_aig();
157 
158  return solver.prop_solve();
159 }
160 
165  std::vector<bool> &n_pos,
166  std::vector<bool> &n_neg)
167 {
168  std::stack<literalt> queue;
169 
170  // Get phases of constraints
171  for(aig_plus_constraintst::constraintst::const_iterator
172  c_it=aig.constraints.begin();
173  c_it!=aig.constraints.end();
174  c_it++)
175  queue.push(*c_it);
176 
177  while(!queue.empty())
178  {
179  literalt l=queue.top();
180  queue.pop();
181 
182  if(l.is_constant())
183  continue;
184 
185  bool sign=l.sign();
186  unsigned var_no=l.var_no();
187 
188  // already set?
189  if(sign?n_neg[var_no]:n_pos[var_no])
190  continue; // done already
191 
192  // set
193  sign?n_neg[var_no]=1:n_pos[var_no]=1;
194 
195  const aigt::nodet &node=aig.nodes[var_no];
196 
197  if(node.is_and())
198  {
199  queue.push(node.a^sign);
200  queue.push(node.b^sign);
201  }
202  }
203 
204  // Count
205  unsigned pos_only=0, neg_only=0, mixed=0;
206 
207  for(unsigned n=0; n<aig.nodes.size(); n++)
208  {
209  if(aig.nodes[n].is_and())
210  {
211  if(n_neg[n] && n_pos[n])
212  mixed++;
213  else if(n_pos[n])
214  pos_only++;
215  else if(n_neg[n])
216  neg_only++;
217  }
218  }
219 
220  statistics() << "Pos only: " << pos_only << "\n"
221  << "Neg only: " << neg_only << "\n"
222  << "Mixed: " << mixed << eom;
223 }
224 
225 
230  std::vector<unsigned> &p_usage_count,
231  std::vector<unsigned> &n_usage_count)
232 {
233  for(aig_plus_constraintst::constraintst::const_iterator
234  c_it=aig.constraints.begin();
235  c_it!=aig.constraints.end();
236  c_it++)
237  {
238  if(!((*c_it).is_constant()))
239  {
240  if((*c_it).sign())
241  {
242  ++n_usage_count[(*c_it).var_no()];
243  }
244  else
245  {
246  ++p_usage_count[(*c_it).var_no()];
247  }
248  }
249  }
250 
251  for(unsigned n=0; n<aig.nodes.size(); n++)
252  {
253  const aigt::nodet &node=aig.nodes[n];
254 
255  if(node.is_and())
256  {
257  if(node.a.sign())
258  {
259  ++n_usage_count[node.a.var_no()];
260  }
261  else
262  {
263  ++p_usage_count[node.a.var_no()];
264  }
265 
266  if(node.b.sign())
267  {
268  ++n_usage_count[node.b.var_no()];
269  }
270  else
271  {
272  ++p_usage_count[node.b.var_no()];
273  }
274  }
275  }
276 
277 
278  #if 1
279  // Compute stats
280  unsigned unused=0;
281  unsigned usedOncePositive=0;
282  unsigned usedOnceNegative=0;
283  unsigned usedTwicePositive=0;
284  unsigned usedTwiceNegative=0;
285  unsigned usedTwiceMixed=0;
286  unsigned usedThreeTimes=0;
287  unsigned usedMore=0;
288 
289  for(unsigned n=0; n<aig.nodes.size(); n++)
290  {
291  switch(p_usage_count[n] + n_usage_count[n])
292  {
293  case 0: ++unused; break;
294  case 1:
295  if(p_usage_count[n]==1)
296  ++usedOncePositive;
297  else
298  ++usedOnceNegative;
299  break;
300 
301  case 2 :
302  if(p_usage_count[n]>=2)
303  {
304  ++usedTwicePositive;
305  }
306  else if(n_usage_count[n]>=2)
307  {
308  ++usedTwiceNegative;
309  }
310  else
311  {
312  assert(p_usage_count[n]==1 && n_usage_count[n]==1);
313  ++usedTwiceMixed;
314  }
315  break;
316  case 3: ++usedThreeTimes; break;
317  default: ++usedMore; break;
318  }
319  }
320 
321  statistics() << "Unused: " << unused << " "
322  << "Used once: " << usedOncePositive + usedOnceNegative
323  << " (P: " << usedOncePositive
324  << ", N: " << usedOnceNegative << ") "
325  << "Used twice: "
326  << usedTwicePositive + usedTwiceNegative + usedTwiceMixed
327  << " (P: " << usedTwicePositive
328  << ", N: " << usedTwiceNegative
329  << ", M: " << usedTwiceMixed << ") "
330  << "Used three times: " << usedThreeTimes << " "
331  << "Used more: " << usedMore
332  << eom;
333  #endif
334 }
335 
341  unsigned n,
342  const aigt::nodet &node,
343  bool n_pos, bool n_neg,
344  std::vector<unsigned> &p_usage_count,
345  std::vector<unsigned> &n_usage_count)
346 {
347  if(p_usage_count[n]>0 || n_usage_count[n]>0)
348  {
349  literalt o=literalt(n, false);
350  bvt body(2);
351  body[0]=node.a;
352  body[1]=node.b;
353 
354 #ifdef USE_AIG_COMPACT
355  // Inline positive literals
356  // This should remove the overhead introduced by land and lor for bvt
357 
358  for(bvt::size_type i=0; i < body.size(); i++)
359  {
360  literalt l=body[i];
361 
362  if(!l.sign() && // Used positively...
363  aig.nodes[l.var_no()].is_and() && // ... is a gate ...
364  p_usage_count[l.var_no()] == 1 && // ... only used here.
365  n_usage_count[l.var_no()] == 0)
366  {
367  const aigt::nodet &rep=aig.nodes[l.var_no()];
368  body[i]=rep.a;
369  body.push_back(rep.b);
370  --i; // Repeat the process
371  --p_usage_count[l.var_no()]; // Supress generation of inlined node
372  }
373  }
374 
375  // TODO : Could check the array for duplicates / complementary literals
376  // but this should be found by the SAT preprocessor.
377  // TODO : Likewise could find things that are constrained, esp the output
378  // and backwards constant propagate. Again may not be worth it.
379 
380  // lxor and lselect et al. are difficult to express in AIGs.
381  // Doing so introduces quite a bit of overhead.
382  // This should recognise the AIGs they produce and
383  // handle them in a more efficient way.
384 
385  // Recognise something of the form:
386  //
387  // neg(o)=lor(land(a,b), land(neg(a),c))
388  // o =land(lneg(land(a,b)), lneg(land(neg(a),c)))
389  //
390  // Note that lxor and lselect generate the negation of this
391  // but will still be recognised because the negation is
392  // recorded where it is used
393 
394  if(body.size() == 2 && body[0].sign() && body[1].sign())
395  {
396  const aigt::nodet &left=aig.nodes[body[0].var_no()];
397  const aigt::nodet &right=aig.nodes[body[1].var_no()];
398 
399  if(left.is_and() && right.is_and())
400  {
401  if(left.a==neg(right.a))
402  {
403  if(p_usage_count[body[0].var_no()]==0 &&
404  n_usage_count[body[0].var_no()]==1 &&
405  p_usage_count[body[1].var_no()]==0 &&
406  n_usage_count[body[1].var_no()]==1)
407  {
408  bvt lits(3);
409 
410  if(n_neg)
411  {
412  lits[0]=left.a;
413  lits[1]=right.b;
414  lits[2]=o;
415  solver.lcnf(lits);
416 
417  lits[0]=neg(left.a);
418  lits[1]=left.b;
419  lits[2]=o;
420  solver.lcnf(lits);
421  }
422 
423  if(n_pos)
424  {
425  lits[0]=left.a;
426  lits[1]=neg(right.b);
427  lits[2]=neg(o);
428  solver.lcnf(lits);
429 
430  lits[0]=neg(left.a);
431  lits[1]=neg(left.b);
432  lits[2]=neg(o);
433  solver.lcnf(lits);
434  }
435 
436  // Supress generation
437  --n_usage_count[body[0].var_no()];
438  --n_usage_count[body[1].var_no()];
439 
440  return;
441  }
442  }
443  }
444  }
445 
446 
447  // Likewise, carry has an improved encoding which is generated
448  // by the CNF encoding
449  if(body.size() == 3 && body[0].sign() && body[1].sign() && body[2].sign())
450  {
451  const aigt::nodet &left=aig.nodes[body[0].var_no()];
452  const aigt::nodet &mid=aig.nodes[body[1].var_no()];
453  const aigt::nodet &right=aig.nodes[body[2].var_no()];
454 
455  if(left.is_and() && mid.is_and() && right.is_and())
456  {
457  if(p_usage_count[body[0].var_no()]==0 &&
458  n_usage_count[body[0].var_no()]==1 &&
459  p_usage_count[body[1].var_no()]==0 &&
460  n_usage_count[body[1].var_no()]==1 &&
461  p_usage_count[body[2].var_no()]==0 &&
462  n_usage_count[body[2].var_no()]==1)
463  {
464  literalt a=left.a;
465  literalt b=left.b;
466  literalt c=mid.a;
467 
468  if(a==right.b && b==mid.b && c==right.a)
469  {
470  // A (negative) carry -- 1 if at most one input is 1
471  bvt lits(3);
472 
473  if(n_neg)
474  {
475  lits[0]=a;
476  lits[1]=b;
477  lits[2]=o;
478  solver.lcnf(lits);
479 
480  lits[0]=a;
481  lits[1]=c;
482  lits[2]=o;
483  solver.lcnf(lits);
484 
485  lits[0]=b;
486  lits[1]=c;
487  lits[2]=o;
488  solver.lcnf(lits);
489  }
490 
491  if(n_pos)
492  {
493  lits[0]=neg(a);
494  lits[1]=neg(b);
495  lits[2]=neg(o);
496  solver.lcnf(lits);
497 
498  lits[0]=neg(a);
499  lits[1]=neg(c);
500  lits[2]=neg(o);
501  solver.lcnf(lits);
502 
503  lits[0]=neg(b);
504  lits[1]=neg(c);
505  lits[2]=neg(o);
506  solver.lcnf(lits);
507  }
508 
509  // Supress generation
510  --n_usage_count[body[0].var_no()];
511  --n_usage_count[body[1].var_no()];
512  --n_usage_count[body[2].var_no()];
513 
514  return;
515  }
516  }
517  }
518  }
519 
520  // TODO : these special cases are fragile and could be improved.
521  // They don't handle cases where the construction is partially constant
522  // folded. Also the usage constraints are sufficient for improvement
523  // but reductions may still be possible with looser restrictions.
524 #endif
525 
526  if(n_pos)
527  {
528  bvt lits(2);
529  lits[1]=neg(o);
530 
531  forall_literals(it, body)
532  {
533  lits[0]=pos(*it);
534  solver.lcnf(lits);
535  }
536  }
537 
538  if(n_neg)
539  {
540  bvt lits;
541 
542  forall_literals(it, body)
543  lits.push_back(neg(*it));
544 
545  lits.push_back(pos(o));
546  solver.lcnf(lits);
547  }
548  }
549 }
550 
552 {
553  // 1. Do variables
554  while(solver.no_variables()<=aig.nodes.size())
556 
557  // Usage count for inlining
558 
559  std::vector<unsigned> p_usage_count;
560  std::vector<unsigned> n_usage_count;
561  p_usage_count.resize(aig.nodes.size(), 0);
562  n_usage_count.resize(aig.nodes.size(), 0);
563 
564  this->usage_count(p_usage_count, n_usage_count);
565 
566 
567  #ifdef USE_PG
568  // Get phases
569  std::vector<bool> n_pos, n_neg;
570  n_pos.resize(aig.nodes.size(), false);
571  n_neg.resize(aig.nodes.size(), false);
572 
573  this->compute_phase(n_pos, n_neg);
574  #endif
575 
576  // 2. Do nodes
577  for(std::size_t n=aig.nodes.size() - 1; n!=0; n--)
578  {
579  if(aig.nodes[n].is_and())
580  {
581 #ifdef USE_PG
582  convert_node(
583  n, aig.nodes[n], n_pos[n], n_neg[n], p_usage_count, n_usage_count);
584 #else
585  convert_node(n, aig.nodes[n], true, true, p_usage_count, n_usage_count);
586 #endif
587  }
588  }
589  // Skip zero as it is not used or a valid literal
590 
591 
592  // 3. Do constraints
593  for(const auto &c_it : aig.constraints)
594  solver.l_set_to(c_it, true);
595 
596  // HACK!
597  aig.nodes.clear();
598 }
literalt land(literalt a, literalt b) override
Definition: aig_prop.cpp:56
literalt lnor(literalt a, literalt b) override
Definition: aig_prop.cpp:102
resultt prop_solve() override
Definition: aig_prop.cpp:152
literalt b
Definition: aig.h:24
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
mstreamt & status()
Definition: message.h:238
literalt lxor(literalt a, literalt b) override
Definition: aig_prop.cpp:76
literalt pos(literalt a)
Definition: literal.h:193
void set_equal(literalt a, literalt b) override
asserts a==b in the propositional formula
Definition: aig_prop.cpp:132
unsignedbv_typet size_type()
Definition: c_types.cpp:57
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
#define forall_literals(it, bv)
Definition: literal.h:199
void l_set_to_true(literalt a)
Definition: prop.h:47
propt & solver
Definition: aig_prop.h:118
bool is_and() const
Definition: aig.h:30
virtual literalt new_variable()=0
literalt lnand(literalt a, literalt b) override
Definition: aig_prop.cpp:97
literalt a
Definition: aig.h:24
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:42
literalt new_and_node(literalt a, literalt b)
Definition: aig.h:114
virtual size_t no_variables() const =0
bool is_true() const
Definition: literal.h:155
void convert_aig()
Definition: aig_prop.cpp:551
Definition: aig.h:21
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
literalt lselect(literalt a, literalt b, literalt c) override
Definition: aig_prop.cpp:117
resultt
Definition: prop.h:94
mstreamt & statistics()
Definition: message.h:243
literalt lequal(literalt a, literalt b) override
Definition: aig_prop.cpp:107
literalt const_literal(bool value)
Definition: literal.h:187
void convert_node(unsigned n, const aigt::nodet &node, bool n_pos, bool n_neg, std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count)
Convert one AIG node, including special handling of a couple of cases.
Definition: aig_prop.cpp:340
void usage_count(std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count)
Compact encoding for single usage variable.
Definition: aig_prop.cpp:229
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
virtual tvt l_get(literalt a) const =0
literalt neg(literalt a)
Definition: literal.h:192
virtual resultt prop_solve()=0
void compute_phase(std::vector< bool > &n_pos, std::vector< bool > &n_neg)
Compute the phase information needed for Plaisted-Greenbaum encoding.
Definition: aig_prop.cpp:164
aigt & dest
Definition: aig_prop.h:64
tvt l_get(literalt a) const override
Definition: aig_prop.cpp:147
literalt limplies(literalt a, literalt b) override
Definition: aig_prop.cpp:112
literalt lor(literalt a, literalt b) override
Definition: aig_prop.cpp:71
aig_plus_constraintst aig
Definition: aig_prop.h:99
nodest nodes
Definition: aig.h:65
constraintst constraints
Definition: aig.h:148
std::vector< literalt > bvt
Definition: literal.h:197
bool is_false() const
Definition: literal.h:160