Merge pull request #7122 from tautschnig/cleanup/zeros

bv_utilst::zeros: code cleanup, use more widely

Author: kroening

src/solvers/flattening/boolbv_div.cpp

@@ -37,8 +37,7 @@ bvt boolbvt::convert_div(const div_exprt &expr)
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
-    bvt zeros;
-    zeros.resize(fraction_bits, const_literal(false));
+    bvt zeros = bv_utils.zeros(fraction_bits);
 
     // add fraction_bits least-significant bits
     op0.insert(op0.begin(), zeros.begin(), zeros.end());

src/solvers/flattening/bv_utils.cpp

@@ -615,10 +615,10 @@ literalt bv_utilst::overflow_negate(const bvt &bv)
   // a overflow on unary- can only happen with the smallest
   // representable number 100....0
 
-  bvt zeros(bv);
-  zeros.erase(--zeros.end());
+  bvt should_be_zeros(bv);
+  should_be_zeros.pop_back();
 
-  return prop.land(bv[bv.size()-1], !prop.lor(zeros));
+  return prop.land(bv[bv.size() - 1], !prop.lor(should_be_zeros));
 }
 
 void bv_utilst::incrementer(
@@ -715,13 +715,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
   for(std::size_t sum=0; sum<op0.size(); sum++)
     if(op0[sum]!=const_literal(false))
     {
-      bvt tmpop;
-
+      bvt tmpop = zeros(sum);
       tmpop.reserve(op0.size());
 
-      for(std::size_t idx=0; idx<sum; idx++)
-        tmpop.push_back(const_literal(false));
-
       for(std::size_t idx=sum; idx<op0.size(); idx++)
         tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
 
@@ -746,13 +742,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
   for(std::size_t bit=0; bit<op0.size(); bit++)
     if(op0[bit]!=const_literal(false))
     {
-      bvt pp;
-
-      pp.reserve(op0.size());
-
       // zeros according to weight
-      for(std::size_t idx=0; idx<bit; idx++)
-        pp.push_back(const_literal(false));
+      bvt pp = zeros(bit);
+      pp.reserve(op0.size());
 
       for(std::size_t idx=bit; idx<op0.size(); idx++)
         pp.push_back(prop.land(op1[idx-bit], op0[bit]));

src/solvers/flattening/bv_utils.h

@@ -191,9 +191,7 @@ class bv_utilst
 
   static bvt zeros(std::size_t new_size)
   {
-    bvt result;
-    result.resize(new_size, const_literal(false));
-    return result;
+    return bvt(new_size, const_literal(false));
   }
 
   void set_equal(const bvt &a, const bvt &b);