Remove {f,F}orall_literals

This was useful in the past, but with C++-11 we can use a ranged-for to avoid
the iterator altogether.

Author: tautschnig

.clang-format

@@ -34,8 +34,6 @@ ForEachMacros: [
   'Forall_goto_functions',
   'forall_goto_program_instructions',
   'Forall_goto_program_instructions',
-  'forall_literals',
-  'Forall_literals',
   'forall_operands',
   'Forall_operands',
   'forall_expr',

src/solvers/flattening/boolbv.cpp

@@ -142,13 +142,13 @@ boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
   cache_result.first->second = bv;
 
   // check
-  forall_literals(it, cache_result.first->second)
+  for(const auto &literal : cache_result.first->second)
   {
-    if(freeze_all && !it->is_constant())
-      prop.set_frozen(*it);
+    if(freeze_all && !literal.is_constant())
+      prop.set_frozen(literal);
 
     INVARIANT_WITH_DIAGNOSTICS(
-      it->var_no() != literalt::unused_var_no(),
+      literal.var_no() != literalt::unused_var_no(),
       "variable number must be different from the unused variable number",
       expr.find_source_location(),
       irep_pretty_diagnosticst(expr));

src/solvers/flattening/boolbv_array.cpp

@@ -36,8 +36,7 @@ bvt boolbvt::convert_array(const exprt &expr)
     {
       const bvt &tmp = convert_bv(*it, op_width);
 
-      forall_literals(it2, tmp)
-        bv.push_back(*it2);
+      bv.insert(bv.end(), tmp.begin(), tmp.end());
     }
 
     return bv;

src/solvers/flattening/boolbv_case.cpp

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

src/solvers/flattening/boolbv_complex.cpp

@@ -31,8 +31,7 @@ bvt boolbvt::convert_complex(const complex_exprt &expr)
   {
     const bvt &tmp = convert_bv(*it, op_width);
 
-    forall_literals(it2, tmp)
-      bv.push_back(*it2);
+    bv.insert(bv.end(), tmp.begin(), tmp.end());
   }
 
   return bv;

src/solvers/flattening/boolbv_cond.cpp

@@ -34,8 +34,8 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
     literalt cond_literal=const_literal(false);
 
     // make it free variables
-    Forall_literals(it, bv)
-      *it=prop.new_variable();
+    for(auto &literal : bv)
+      literal = prop.new_variable();
 
     forall_operands(it, expr)
     {

src/solvers/flattening/boolbv_map.cpp

@@ -93,7 +93,7 @@ void boolbv_mapt::get_literals(
     map_entry.literal_map.size() == width,
     "number of literals in the literal map shall equal the bitvector width");
 
-  Forall_literals(it, literals)
+  for(auto it = literals.begin(); it != literals.end(); ++it)
   {
     literalt &l=*it;
     const std::size_t bit=it-literals.begin();
@@ -127,7 +127,7 @@ void boolbv_mapt::set_literals(
 {
   map_entryt &map_entry=get_map_entry(identifier, type);
 
-  forall_literals(it, literals)
+  for(auto it = literals.begin(); it != literals.end(); ++it)
   {
     const literalt &literal=*it;
 

src/solvers/flattening/boolbv_typecast.cpp

@@ -64,8 +64,7 @@ bool boolbvt::type_conversion(
   {
     if(src_type==dest_type.subtype())
     {
-      forall_literals(it, src)
-      dest.push_back(*it);
+      dest.insert(dest.end(), src.begin(), src.end());
 
       // pad with zeros
       for(std::size_t i=src.size(); i<dest_width; i++)
@@ -208,8 +207,8 @@ bool boolbvt::type_conversion(
           INVARIANT(
             src_width == 1, "bitvector of type boolean shall have width one");
 
-          Forall_literals(it, dest)
-            *it=prop.land(*it, src[0]);
+          for(auto &literal : dest)
+            literal = prop.land(literal, src[0]);
 
           return false;
         }

src/solvers/flattening/boolbv_vector.cpp

@@ -29,8 +29,7 @@ bvt boolbvt::convert_vector(const vector_exprt &expr)
     {
       const bvt &tmp = convert_bv(*it, op_width);
 
-      forall_literals(it2, tmp)
-        bv.push_back(*it2);
+      bv.insert(bv.end(), tmp.begin(), tmp.end());
     }
   }
 

src/solvers/flattening/bv_pointers.cpp

@@ -243,8 +243,8 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     bvt bv;
     bv.resize(bits);
 
-    Forall_literals(it, bv)
-      *it=prop.new_variable();
+    for(auto &literal : bv)
+      literal = prop.new_variable();
 
     return bv;
   }