Make boolbv_mapt::get_literals return a bvt

This avoids callers creating a bvt just so that get_literals can copy
its own bvt into the caller's bvt.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -377,13 +377,10 @@ bvt boolbvt::convert_symbol(const exprt &expr)
   const typet &type=expr.type();
   std::size_t width=boolbv_width(type);
 
-  bvt bv;
-  bv.resize(width);
-
   const irep_idt &identifier = expr.get(ID_identifier);
   CHECK_RETURN(!identifier.empty());
 
-  map.get_literals(identifier, type, bv);
+  bvt bv = map.get_literals(identifier, type, width);
 
   INVARIANT_WITH_DIAGNOSTICS(
     std::all_of(

src/solvers/flattening/boolbv_index.cpp

@@ -57,8 +57,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
         {
           std::size_t width = boolbv_width(array_type);
-          bvt unused(width);
-          map.get_literals(final_array.get(ID_identifier), array_type, unused);
+          (void)map.get_literals(
+            final_array.get(ID_identifier), array_type, width);
         }
 
         // make sure we have the index in the cache
@@ -77,8 +77,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
         {
           std::size_t width = boolbv_width(array_type);
-          bvt unused(width);
-          map.get_literals(array.get(ID_identifier), array_type, unused);
+          (void)map.get_literals(array.get(ID_identifier), array_type, width);
         }
 
         // make sure we have the index in the cache

src/solvers/flattening/boolbv_map.cpp

@@ -38,10 +38,10 @@ void boolbv_mapt::show(std::ostream &out) const
     out << pair.first << "=" << pair.second.get_value(prop) << '\n';
 }
 
-void boolbv_mapt::get_literals(
+const bvt &boolbv_mapt::get_literals(
   const irep_idt &identifier,
   const typet &type,
-  bvt &literals)
+  std::size_t width)
 {
   std::pair<mappingt::iterator, bool> result=
     mapping.insert(std::pair<irep_idt, map_entryt>(
@@ -52,9 +52,9 @@ void boolbv_mapt::get_literals(
   if(result.second)
   { // actually inserted
     map_entry.type=type;
-    map_entry.literal_map.reserve(literals.size());
+    map_entry.literal_map.reserve(width);
 
-    for(std::size_t bit = 0; bit < literals.size(); ++bit)
+    for(std::size_t bit = 0; bit < width; ++bit)
     {
       map_entry.literal_map.push_back(prop.new_variable());
 
@@ -66,10 +66,10 @@ void boolbv_mapt::get_literals(
   }
 
   INVARIANT(
-    map_entry.literal_map.size() == literals.size(),
+    map_entry.literal_map.size() == width,
     "number of literals in the literal map shall equal the bitvector width");
 
-  literals = map_entry.literal_map;
+  return map_entry.literal_map;
 }
 
 void boolbv_mapt::set_literals(

src/solvers/flattening/boolbv_map.h

@@ -37,10 +37,10 @@ class boolbv_mapt
 
   void show(std::ostream &out) const;
 
-  void get_literals(
+  const bvt &get_literals(
     const irep_idt &identifier,
     const typet &type,
-    bvt &literals);
+    std::size_t width);
 
   void set_literals(
     const irep_idt &identifier,

src/solvers/flattening/bv_pointers.cpp

@@ -231,12 +231,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
     const typet &type=expr.type();
 
-    bvt bv;
-    bv.resize(bits);
-
-    map.get_literals(identifier, type, bv);
-
-    return bv;
+    return map.get_literals(identifier, type, bits);
   }
   else if(expr.id()==ID_nondet_symbol)
   {