Cleanup and use propt::new_variables

Several places still locally had a for loop where each step performed a
call to propt::new_variable, which is all taken care of by
propt::new_variables(width). Also override this method in cnft to avoid
repeated calls to set_no_variables.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -534,9 +534,7 @@ exprt boolbvt::make_free_bv_expr(const typet &type)
 {
   const std::size_t width = boolbv_width(type);
   PRECONDITION(width != 0);
-  bvt bv(width);
-  for(auto &lit : bv)
-    lit = prop.new_variable();
+  bvt bv = prop.new_variables(width);
   return make_bv_expr(type, bv);
 }
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -128,8 +128,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     if(prop.has_set_to())
     {
       // free variables
-      for(std::size_t i=0; i<width; i++)
-        bv[i]=prop.new_variable();
+      bv = prop.new_variables(width);
 
       // add implications
 

src/solvers/flattening/boolbv_case.cpp

@@ -21,12 +21,8 @@ bvt boolbvt::convert_case(const exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  bvt bv;
-  bv.resize(width);
-
   // make it free variables
-  for(auto &literal : bv)
-    literal = prop.new_variable();
+  bvt bv = prop.new_variables(width);
 
   DATA_INVARIANT(
     operands.size() >= 3, "case should have at least three operands");

src/solvers/flattening/boolbv_cond.cpp

@@ -20,7 +20,6 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
     return conversion_failed(expr);
 
   bvt bv;
-  bv.resize(width);
 
   DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");
 
@@ -34,8 +33,7 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
     literalt cond_literal=const_literal(false);
 
     // make it free variables
-    for(auto &literal : bv)
-      literal = prop.new_variable();
+    bv = prop.new_variables(width);
 
     forall_operands(it, expr)
     {
@@ -60,6 +58,8 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
   }
   else
   {
+    bv.resize(width);
+
     // functional version -- go backwards
     for(std::size_t i=expr.operands().size(); i!=0; i-=2)
     {

src/solvers/flattening/boolbv_index.cpp

@@ -67,9 +67,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       else
       {
         // free variables
-        bv.reserve(width);
-        for(std::size_t i = 0; i < width; i++)
-          bv.push_back(prop.new_variable());
+        bv = prop.new_variables(width);
 
         record_array_index(expr);
 
@@ -219,10 +217,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     if(prop.has_set_to())
     {
       // free variables
-
-      bv.resize(width);
-      for(std::size_t i=0; i<width; i++)
-        bv[i]=prop.new_variable();
+      bv = prop.new_variables(width);
 
       // add implications
 
@@ -297,9 +292,6 @@ bvt boolbvt::convert_index(
   if(width==0)
     return conversion_failed(array);
 
-  bvt bv;
-  bv.resize(width);
-
   // TODO: If the underlying array can use one of the
   // improvements given above then it may be better to use
   // the array theory for short chains of updates and then
@@ -325,8 +317,8 @@ bvt boolbvt::convert_index(
     //       array.id()!=ID_array);
     // If not there are large improvements possible as above
 
-    for(std::size_t i=0; i<width; i++)
-      bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
+    std::size_t offset_int = numeric_cast_v<std::size_t>(offset);
+    return bvt(tmp.begin() + offset_int, tmp.begin() + offset_int + width);
   }
   else if(
     array.id() == ID_member || array.id() == ID_index ||
@@ -354,9 +346,6 @@ bvt boolbvt::convert_index(
   else
   {
     // out of bounds
-    for(std::size_t i=0; i<width; i++)
-      bv[i]=prop.new_variable();
+    return prop.new_variables(width);
   }
-
-  return bv;
 }

src/solvers/flattening/bv_pointers.cpp

@@ -341,13 +341,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_nondet_symbol)
   {
-    bvt bv;
-    bv.resize(bits);
-
-    for(auto &literal : bv)
-      literal = prop.new_variable();
-
-    return bv;
+    return prop.new_variables(bits);
   }
   else if(expr.id()==ID_typecast)
   {
@@ -576,11 +570,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     const bvt object_size_bv =
       bv_utils.zero_extension(convert_bv(object_size), width);
 
-    bvt bv;
-    bv.reserve(width);
-
-    for(std::size_t i = 0; i < width; ++i)
-      bv.push_back(prop.new_variable());
+    bvt bv = prop.new_variables(width);
 
     if(!same_object_bv[0].is_false())
     {
@@ -660,11 +650,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     // we postpone until we know the objects
     std::size_t width=boolbv_width(expr.type());
 
-    bvt bv;
-    bv.resize(width);
-
-    for(std::size_t i=0; i<width; i++)
-      bv[i]=prop.new_variable();
+    bvt bv = prop.new_variables(width);
 
     postponed_list.push_back(postponedt());
 

src/solvers/flattening/bv_utils.cpp

@@ -936,14 +936,8 @@ void bv_utilst::unsigned_divider(
   literalt is_not_zero=prop.lor(op1);
 
   // free variables for result of division
-
-  res.resize(width);
-  rem.resize(width);
-  for(std::size_t i=0; i<width; i++)
-  {
-    res[i]=prop.new_variable();
-    rem[i]=prop.new_variable();
-  }
+  res = prop.new_variables(width);
+  rem = prop.new_variables(width);
 
   // add implications
 
@@ -1166,9 +1160,7 @@ literalt bv_utilst::lt_or_le(
     size_t start;
     size_t i;
 
-    compareBelow.resize(bv0.size());
-    for(auto &literal : compareBelow)
-      literal = prop.new_variable();
+    compareBelow = prop.new_variables(bv0.size());
     result = prop.new_variable();
 
     if(rep==SIGNED)

src/solvers/flattening/equality.cpp

@@ -110,11 +110,7 @@ void equalityt::add_equality_constraints(const typestructt &typestruct)
   eq_bvs.resize(no_elements);
 
   for(std::size_t i=0; i<no_elements; i++)
-  {
-    eq_bvs[i].resize(bits);
-    for(std::size_t j=0; j<bits; j++)
-      eq_bvs[i][j]=prop.new_variable();
-  }
+    eq_bvs[i] = prop.new_variables(bits);
 
   // generate equality constraints
 

src/solvers/prop/prop.cpp

@@ -20,9 +20,9 @@ void propt::set_equal(literalt a, literalt b)
 bvt propt::new_variables(std::size_t width)
 {
   bvt result;
-  result.resize(width);
+  result.reserve(width);
   for(std::size_t i=0; i<width; i++)
-    result[i]=new_variable();
+    result.push_back(new_variable());
   return result;
 }
 

src/solvers/prop/prop.h

@@ -92,7 +92,7 @@ class propt
   virtual literalt new_variable()=0;
   virtual void set_variable_name(literalt, const irep_idt &) { }
   virtual size_t no_variables() const=0;
-  bvt new_variables(std::size_t width);
+  virtual bvt new_variables(std::size_t width);
 
   // solving
   virtual const std::string solver_text()=0;