From 528361252150b9734809271a7f00e198fdc593ef Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 23 Apr 2021 13:28:10 +0000
Subject: [PATCH] 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.
---
 src/solvers/flattening/boolbv.cpp             |  4 +---
 .../flattening/boolbv_byte_extract.cpp        |  3 +--
 src/solvers/flattening/boolbv_case.cpp        |  6 +-----
 src/solvers/flattening/boolbv_cond.cpp        |  6 +++---
 src/solvers/flattening/boolbv_index.cpp       | 21 +++++--------------
 src/solvers/flattening/bv_pointers.cpp        | 20 +++---------------
 src/solvers/flattening/bv_utils.cpp           | 14 +++----------
 src/solvers/flattening/equality.cpp           |  6 +-----
 src/solvers/prop/prop.cpp                     |  4 ++--
 src/solvers/prop/prop.h                       |  2 +-
 src/solvers/sat/cnf.cpp                       | 18 ++++++++++++++--
 src/solvers/sat/cnf.h                         |  1 +
 12 files changed, 38 insertions(+), 67 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index a29414a760a..cc389edb31d 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/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);
 }
 
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 868f393ba3b..1a787ff7208 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/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
 
diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp
index f3455b8cec4..4f8eef21ef6 100644
--- a/src/solvers/flattening/boolbv_case.cpp
+++ b/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");
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
index 9c7d15e8465..d7d546d374d 100644
--- a/src/solvers/flattening/boolbv_cond.cpp
+++ b/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)
     {
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 5feb1513a85..0b2cec1dba2 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/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;
 }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 87715064791..ffa04ad35ed 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/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());
 
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index d03d3f5ff86..21ef59a8ffa 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/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)
diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp
index e07bf114eed..5add319eef2 100644
--- a/src/solvers/flattening/equality.cpp
+++ b/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
 
diff --git a/src/solvers/prop/prop.cpp b/src/solvers/prop/prop.cpp
index 2f2a03f78e2..b8a01e242dd 100644
--- a/src/solvers/prop/prop.cpp
+++ b/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;
 }
 
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index 2a861b8e6c2..36e4b0f02c1 100644
--- a/src/solvers/prop/prop.h
+++ b/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;
diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp
index dafe98ef818..66b294b005f 100644
--- a/src/solvers/sat/cnf.cpp
+++ b/src/solvers/sat/cnf.cpp
@@ -385,14 +385,28 @@ literalt cnft::lselect(literalt a, literalt b, literalt c)
 /// \return New variable as literal
 literalt cnft::new_variable()
 {
-  literalt l;
-  l.set(_no_variables, false);
+  literalt l(_no_variables, false);
 
   set_no_variables(_no_variables+1);
 
   return l;
 }
 
+/// Generate a vector of new variables.
+/// \return Vector of new variables.
+bvt cnft::new_variables(std::size_t width)
+{
+  bvt result;
+  result.reserve(width);
+
+  for(std::size_t i = _no_variables; i < _no_variables + width; ++i)
+    result.emplace_back(i, false);
+
+  set_no_variables(_no_variables + width);
+
+  return result;
+}
+
 /// eliminate duplicates from given vector of literals
 /// \par parameters: set of literals given as vector
 /// \return set of literals, duplicates removed
diff --git a/src/solvers/sat/cnf.h b/src/solvers/sat/cnf.h
index e675fc196f0..58c0d6efa75 100644
--- a/src/solvers/sat/cnf.h
+++ b/src/solvers/sat/cnf.h
@@ -38,6 +38,7 @@ class cnft:public propt
   // a?b:c
   virtual literalt lselect(literalt a, literalt b, literalt c) override;
   virtual literalt new_variable() override;
+  bvt new_variables(std::size_t width) override;
   virtual size_t no_variables() const override { return _no_variables; }
   virtual void set_no_variables(size_t no) { _no_variables=no; }
   virtual size_t no_clauses() const=0;