netlist conversion: track equivalent nodes

This augments the list of constraints on netlist nodes (netlist nodes that
have to evaluate to true) by a list of node equivalences.

This avoids the need for expensive re-discovery of such equivalences by
methods such as SAT sweeping.

Author: kroening

src/trans-netlist/aig.h

@@ -154,14 +154,27 @@ class aigt {
 
 std::ostream &operator<<(std::ostream &, const aigt &);
 
-class aig_plus_constraintst : public aigt {
+class aig_plus_constraintst : public aigt
+{
 public:
   typedef std::vector<literalt> constraintst;
   constraintst constraints;
 
-  void clear() {
+  // An equivalence between two nodes, given as literalt.
+  // This avoids the need to re-discover functionally
+  // equivalent nodes via SAT sweeping or the like.
+  // The use of constants true/false is allowed.
+  // These are redundantly stored as constraints as well.
+  using equivalencet = std::pair<literalt, literalt>;
+  using equivalencest = std::vector<equivalencet>;
+
+  equivalencest equivalences;
+
+  void clear()
+  {
     aigt::clear();
     constraints.clear();
+    equivalences.clear();
   }
 };
 

src/trans-netlist/aig_prop.cpp

@@ -112,17 +112,3 @@ literalt aig_prop_baset::lselect(literalt a, literalt b,
 
   return lor(land(a, b), land(neg(a), c));
 }
-
-void aig_prop_baset::set_equal(literalt a, literalt b) {
-#ifdef USE_AIG_COMPACT
-  // The compact encoding should reduce this
-  l_set_to_true(lequal(a, b));
-
-#else
-  // we produce two constraints:
-  // a|!b   !a|b
-
-  l_set_to_true(lor(pos(a), neg(b)));
-  l_set_to_true(lor(neg(a), pos(b)));
-#endif
-}

src/trans-netlist/aig_prop.h

@@ -39,7 +39,6 @@ class aig_prop_baset : public propt {
   literalt lequal(literalt a, literalt b) override;
   literalt limplies(literalt a, literalt b) override;
   literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
-  void set_equal(literalt a, literalt b) override;
 
   void l_set_to(literalt a, bool value) override
   {
@@ -71,18 +70,30 @@ class aig_prop_baset : public propt {
   aigt &dest;
 };
 
-class aig_prop_constraintt : public aig_prop_baset {
+class aig_prop_constraintt : public aig_prop_baset
+{
 public:
-  explicit aig_prop_constraintt(aig_plus_constraintst &_dest,
-                                message_handlert &message_handler)
-      : aig_prop_baset(_dest, message_handler), dest(_dest) {}
+  explicit aig_prop_constraintt(
+    aig_plus_constraintst &_dest,
+    message_handlert &message_handler)
+    : aig_prop_baset(_dest, message_handler), dest(_dest)
+  {
+  }
 
   aig_plus_constraintst &dest;
   bool has_set_to() const override { return true; }
 
   void lcnf(const bvt &clause) override { l_set_to_true(lor(clause)); }
 
-  void l_set_to(literalt a, bool value) override {
+  void set_equal(literalt a, literalt b) override
+  {
+    dest.equivalences.emplace_back(a, b);
+    dest.constraints.push_back(lequal(a, b));
+  }
+
+  void l_set_to(literalt a, bool value) override
+  {
+    dest.equivalences.emplace_back(a, const_literal(value));
     dest.constraints.push_back(a ^ !value);
   }