Revert "Remove bv_utils::set_equal as it ought to be avoided"

This reverts commit 90ba9f9d2c0e61287723199f06304becd5a4d24d.

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -28,6 +28,13 @@ 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,6 +196,8 @@ 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,12 +124,6 @@ void equalityt::add_equality_constraints(const typestructt &typestruct)
     const bvt &bv1=eq_bvs[it->first.first];
     const bvt &bv2=eq_bvs[it->first.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);
+    prop.set_equal(bv_utils.equal(bv1, bv2), it->second);
   }
 }

src/solvers/prop/prop.h

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

src/solvers/sat/cnf.cpp

@@ -196,64 +196,6 @@ 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,7 +28,6 @@ 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,11 +82,6 @@ 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();