Remove bv_utils::set_equal as it ought to be avoided

Instead of the dance of creating free variables and then setting them
equal to the result of some circuit just pass in the known output
signals and create the circuit using those directly.

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -28,13 +28,6 @@ literalt bv_utilst::is_one(const bvt &bv)
   return prop.land(is_zero(tmp), bv[0]);
 }
 
-void bv_utilst::set_equal(const bvt &a, const bvt &b)
-{
-  PRECONDITION(a.size() == b.size());
-  for(std::size_t i=0; i<a.size(); i++)
-    prop.set_equal(a[i], b[i]);
-}
-
 bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last)
 {
   // preconditions

src/solvers/flattening/bv_utils.h

@@ -196,8 +196,6 @@ class bv_utilst
     return result;
   }
 
-  void set_equal(const bvt &a, const bvt &b);
-
   // if cond holds, a has to be equal to b
   void cond_implies_equal(literalt cond, const bvt &a, const bvt &b);
 

src/solvers/flattening/equality.cpp

@@ -124,6 +124,12 @@ void equalityt::add_equality_constraints(const typestructt &typestruct)
     const bvt &bv1=eq_bvs[it->first.first];
     const bvt &bv2=eq_bvs[it->first.second];
 
-    prop.set_equal(bv_utils.equal(bv1, bv2), it->second);
+    bvt equal_bv;
+    equal_bv.resize(bv1.size());
+
+    for(std::size_t i = 0; i < bv1.size(); i++)
+      equal_bv[i] = prop.lequal(bv1[i], bv2[i]);
+
+    prop.gate_bv_and(equal_bv, it->second);
   }
 }

src/solvers/prop/prop.h

@@ -32,6 +32,7 @@ class propt
   virtual literalt land(literalt a, literalt b)=0;
   virtual literalt lor(literalt a, literalt b)=0;
   virtual literalt land(const bvt &bv)=0;
+  virtual void gate_bv_and(const bvt &bv, literalt output) = 0;
   virtual literalt lor(const bvt &bv)=0;
   virtual literalt lxor(literalt a, literalt b)=0;
   virtual literalt lxor(const bvt &bv)=0;

src/solvers/refinement/refine_arithmetic.cpp

@@ -270,7 +270,8 @@ void bv_refinementt::check_SAT(approximationt &a)
         UNREACHABLE;
 
       CHECK_RETURN(r.size()==res.size());
-      bv_utils.set_equal(r, res);
+      for(std::size_t i = 0; i < r.size(); i++)
+        prop.set_equal(r[i], res[i]);
     }
   }
   else if(type.id()==ID_signedbv ||
@@ -338,7 +339,9 @@ void bv_refinementt::check_SAT(approximationt &a)
       else
         UNREACHABLE;
 
-      bv_utils.set_equal(r, a.result_bv);
+      CHECK_RETURN(r.size() == a.result_bv.size());
+      for(std::size_t i = 0; i < r.size(); i++)
+        prop.set_equal(r[i], a.result_bv[i]);
     }
     else
       UNREACHABLE;

src/solvers/sat/cnf.cpp

@@ -196,6 +196,64 @@ literalt cnft::land(const bvt &bv)
   return literal;
 }
 
+/// Tseitin encoding of conjunction between multiple literals
+/// \param bv: Any number of inputs to the AND gate
+/// \param output: Output signal of the circuit
+void cnft::gate_bv_and(const bvt &bv, literalt output)
+{
+  if(bv.empty())
+  {
+    lcnf({output});
+    return;
+  }
+  if(bv.size() == 1)
+  {
+    lcnf(bv[0], !output);
+    lcnf(!bv[0], output);
+    return;
+  }
+  if(bv.size() == 2)
+  {
+    gate_and(bv[0], bv[1], output);
+    return;
+  }
+
+  for(const auto &l : bv)
+  {
+    if(l.is_false())
+    {
+      lcnf({!output});
+      return;
+    }
+  }
+
+  if(is_all(bv, const_literal(true)))
+  {
+    lcnf({output});
+    return;
+  }
+
+  bvt new_bv = eliminate_duplicates(bv);
+
+  bvt lits(2);
+  lits[1] = neg(output);
+
+  for(const auto &l : new_bv)
+  {
+    lits[0] = pos(l);
+    lcnf(lits);
+  }
+
+  lits.clear();
+  lits.reserve(new_bv.size() + 1);
+
+  for(const auto &l : new_bv)
+    lits.push_back(neg(l));
+
+  lits.push_back(pos(output));
+  lcnf(lits);
+}
+
 /// Tseitin encoding of disjunction between multiple literals
 /// \par parameters: Any number of inputs to the OR gate
 /// \return Output signal of the OR gate as literal

src/solvers/sat/cnf.h

@@ -28,6 +28,7 @@ class cnft:public propt
   virtual literalt land(literalt a, literalt b) override;
   virtual literalt lor(literalt a, literalt b) override;
   virtual literalt land(const bvt &bv) override;
+  void gate_bv_and(const bvt &bv, literalt output) override;
   virtual literalt lor(const bvt &bv) override;
   virtual literalt lxor(const bvt &bv) override;
   virtual literalt lxor(literalt a, literalt b) override;

unit/solvers/bdd/miniBDD/miniBDD.cpp

@@ -82,6 +82,11 @@ class bdd_propt : public propt
     return to_literal(result);
   }
 
+  void gate_bv_and(const bvt &bv, literalt output) override
+  {
+    UNREACHABLE;
+  }
+
   literalt lor(const bvt &bv) override
   {
     mini_bddt result = mgr.False();