netlist conversion: track equivalent nodes

This replaces the list of constraints on netlist nodes (netlist nodes that
have to evaluate to true) by a list of node equivalences.  This is more
compact when node equivalences have to be generated, as the AIG nodes for
lhs<->rhs do not have to be generated.

Author: kroening

src/ebmc/bdd_engine.cpp

@@ -930,7 +930,7 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr)
 
     assert(expr.type().id()==ID_bool);
 
-    aig_prop_constraintt aig_prop(netlist, message.get_message_handler());
+    aig_prop_equivalencest aig_prop(netlist, message.get_message_handler());
 
     literalt l = instantiate_convert(
       aig_prop, netlist.var_map, expr, ns, message.get_message_handler());
@@ -989,16 +989,20 @@ void bdd_enginet::build_BDDs()
       literalt next=netlist.var_map.get_next(v.first);
       transition_BDDs.push_back(aig2bdd(next, BDDs)==v.second.next);
     }
-  
-  // general AIG conditions
-  for(literalt l : netlist.constraints)
-    constraints_BDDs.push_back(aig2bdd(l, BDDs));
-    
-  // initial state conditions
+
+  // AIG equivalences
+  for(auto &[lhs, rhs] : netlist.equivalences)
+    constraints_BDDs.push_back(aig2bdd(lhs, BDDs) == aig2bdd(rhs, BDDs));
+
+  // initial state constraints
   for(literalt l : netlist.initial)
     initial_BDDs.push_back(aig2bdd(l, BDDs));
-    
-  // transition conditions
+
+  // invar constraints
+  for(literalt l : netlist.invar)
+    constraints_BDDs.push_back(aig2bdd(l, BDDs));
+
+  // transition constraints
   for(literalt l : netlist.transition)
     transition_BDDs.push_back(aig2bdd(l, BDDs));
 

src/ic3/r0ead_input.cc

@@ -217,12 +217,13 @@ void CompInfo::form_var_nums()
   ================================================*/
 void ic3_enginet::add_verilog_conv_constrs()
 {
+  PRECONDITION(netlist.equivalences.empty());
 
-  for(literalt lit : netlist.constraints) {
+  for(literalt lit : netlist.invar)
+  {
     if (lit.is_constant()) continue;
     std::cout << "constraint literal " << lit.get() << "\n";
      Ci.Init_clits.insert(lit.get());
   }
 
-
 } /* end of function add_verlig_conv_constrs */

src/ic3/r1ead_input.cc

@@ -52,7 +52,7 @@ void ic3_enginet::find_prop_lit()
   }
   assert(Oper.type().id()==ID_bool);
 
-  aig_prop_constraintt aig_prop(netlist, message.get_message_handler());
+  aig_prop_equivalencest aig_prop(netlist, message.get_message_handler());
 
   symbol_tablet symbol_table{};
   const namespacet ns(symbol_table);

src/trans-netlist/aig.h

@@ -103,14 +103,20 @@ class aigt {
 
 std::ostream &operator<<(std::ostream &, const aigt &);
 
-class aig_plus_constraintst : public aigt {
+class aig_plus_equivalencest : public aigt
+{
 public:
-  typedef std::vector<literalt> constraintst;
-  constraintst constraints;
+  // An equivalence between two nodes, given as literalt.
+  // The use of constants true/false is allowed.
+  using equivalencet = std::pair<literalt, literalt>;
+  using equivalencest = std::vector<equivalencet>;
 
-  void clear() {
+  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,19 +70,29 @@ class aig_prop_baset : public propt {
   aigt &dest;
 };
 
-class aig_prop_constraintt : public aig_prop_baset {
+class aig_prop_equivalencest : 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_equivalencest(
+    aig_plus_equivalencest &_dest,
+    message_handlert &message_handler)
+    : aig_prop_baset(_dest, message_handler), dest(_dest)
+  {
+  }
 
-  aig_plus_constraintst &dest;
+  aig_plus_equivalencest &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 {
-    dest.constraints.push_back(a ^ !value);
+  void set_equal(literalt a, literalt b) override
+  {
+    dest.equivalences.emplace_back(a, b);
+  }
+
+  void l_set_to(literalt a, bool value) override
+  {
+    dest.equivalences.emplace_back(a, const_literal(value));
   }
 
   void set_assignment(literalt a, bool value) override {}

src/trans-netlist/netlist.cpp

@@ -65,12 +65,14 @@ void netlistt::print(std::ostream &out) const
 
   out << '\n';
 
-  out << "State invariant constraints: " << '\n';
+  out << "AIG equivalences: " << '\n';
 
-  for(auto &c : constraints)
+  for(auto &c : equivalences)
   {
     out << "  ";
-    print(out, c);
+    print(out, c.first);
+    out << '=';
+    print(out, c.second);
     out << '\n';
   }
 

src/trans-netlist/netlist.h

@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 #include <variant>
 
-class netlistt:public aig_plus_constraintst
+class netlistt : public aig_plus_equivalencest
 {
 public:
   var_mapt var_map;
@@ -52,6 +52,7 @@ class netlistt:public aig_plus_constraintst
   // additional constraints, given as netlist literals
   // these are implicit conjunctions
   bvt initial;
+  bvt invar;
   bvt transition;
 
   // Map from property ID to a netlist property,

src/trans-netlist/smv_netlist.cpp

@@ -244,15 +244,28 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   }
 
   out << '\n';
-  out << "-- in-state constraints" << '\n';
+  out << "-- AIG equivalences" << '\n';
   out << '\n';
 
-  for(auto &constraint_l : netlist.constraints)
+  for(auto &constraint_l : netlist.equivalences)
   {
-    if(!constraint_l.is_true())
+    out << "INVAR ";
+    print_smv(netlist, out, constraint_l.first);
+    out << "<->";
+    print_smv(netlist, out, constraint_l.second);
+    out << '\n';
+  }
+
+  out << '\n';
+  out << "-- INVAR" << '\n';
+  out << '\n';
+
+  for(auto &invar_l : netlist.invar)
+  {
+    if(!invar_l.is_true())
     {
       out << "INVAR ";
-      print_smv(netlist, out, constraint_l);
+      print_smv(netlist, out, invar_l);
       out << '\n';
     }
   }

src/trans-netlist/trans_to_netlist.cpp

@@ -65,7 +65,7 @@ class convert_trans_to_netlistt:public messaget
   symbol_table_baset &symbol_table;
   const namespacet ns;
   netlistt &dest;
-  aig_prop_constraintt aig_prop;
+  aig_prop_equivalencest aig_prop;
   netlist_boolbvt solver;
 
   literalt new_input();
@@ -285,8 +285,8 @@ void convert_trans_to_netlistt::operator()(
   // do the remaining transition constraints
   convert_constraints();
 
-  dest.constraints.insert(
-    dest.constraints.end(), invar_constraints.begin(), invar_constraints.end());
+  dest.invar.insert(
+    dest.invar.end(), invar_constraints.begin(), invar_constraints.end());
 
   dest.transition.insert(
     dest.transition.end(),