Merge pull request #5787 from tautschnig/forall-literals

Remove {f,F}orall_literals

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;
   }

src/solvers/flattening/bv_utils.cpp

@@ -560,10 +560,10 @@ void bv_utilst::incrementer(
 {
   carry_out=carry_in;
 
-  Forall_literals(it, bv)
+  for(auto &literal : bv)
   {
-    literalt new_carry=prop.land(carry_out, *it);
-    *it=prop.lxor(*it, carry_out);
+    literalt new_carry = prop.land(carry_out, literal);
+    literal = prop.lxor(literal, carry_out);
     carry_out=new_carry;
   }
 }
@@ -579,8 +579,8 @@ bvt bv_utilst::incrementer(const bvt &bv, literalt carry_in)
 bvt bv_utilst::inverted(const bvt &bv)
 {
   bvt result=bv;
-  Forall_literals(it, result)
-    *it=!*it;
+  for(auto &literal : result)
+    literal = !literal;
   return result;
 }
 
@@ -1167,7 +1167,8 @@ literalt bv_utilst::lt_or_le(
     size_t i;
 
     compareBelow.resize(bv0.size());
-    Forall_literals(it, compareBelow) { (*it) = prop.new_variable(); }
+    for(auto &literal : compareBelow)
+      literal = prop.new_variable();
     result = prop.new_variable();
 
     if(rep==SIGNED)
@@ -1309,9 +1310,11 @@ literalt bv_utilst::rel(
 
 bool bv_utilst::is_constant(const bvt &bv)
 {
-  forall_literals(it, bv)
-    if(!it->is_constant())
+  for(const auto &literal : bv)
+  {
+    if(!literal.is_constant())
       return false;
+  }
 
   return true;
 }

src/solvers/prop/literal.h

@@ -200,12 +200,4 @@ inline bool is_true (const literalt &l) { return (l.is_true()); }
 // bit-vectors
 typedef std::vector<literalt> bvt;
 
-#define forall_literals(it, bv) \
-  for(bvt::const_iterator it=(bv).begin(), it_end=(bv).end(); \
-      it!=it_end; ++it)
-
-#define Forall_literals(it, bv) \
-  for(bvt::iterator it=(bv).begin(); \
-      it!=(bv).end(); ++it)
-
 #endif // CPROVER_SOLVERS_PROP_LITERAL_H

src/solvers/prop/prop_minimize.cpp

@@ -85,8 +85,8 @@ literalt prop_minimizet::constraint()
   {
     exprt::operandst disjuncts;
     disjuncts.reserve(or_clause.size());
-    forall_literals(it, or_clause)
-      disjuncts.push_back(literal_exprt(*it));
+    for(const auto &literal : or_clause)
+      disjuncts.push_back(literal_exprt(literal));
 
     return prop_conv.convert(disjunction(disjuncts));
   }

src/solvers/refinement/refine_arrays.cpp

@@ -114,9 +114,9 @@ void bv_refinementt::freeze_lazy_constraints()
     for(const auto &symbol : find_symbols(constraint.lazy))
     {
       const bvt bv=convert_bv(symbol);
-      forall_literals(b_it, bv)
-        if(!b_it->is_constant())
-          prop.set_frozen(*b_it);
+      for(const auto &literal : bv)
+        if(!literal.is_constant())
+          prop.set_frozen(literal);
     }
   }
 }

src/solvers/sat/cnf.h

@@ -59,9 +59,11 @@ class cnft:public propt
 
   static bool is_all(const bvt &bv, literalt l)
   {
-    forall_literals(it, bv)
-      if(*it!=l)
+    for(const auto &literal : bv)
+    {
+      if(literal != l)
         return false;
+    }
     return true;
   }
 };

src/solvers/sat/external_sat.cpp

@@ -52,9 +52,11 @@ void external_satt::write_cnf_file(std::string cnf_file)
     dimacs_cnft::write_dimacs_clause(c, out, false);
 
   // output the assumption clauses
-  forall_literals(it, assumptions)
-    if(!it->is_constant())
-      out << it->dimacs() << " 0\n";
+  for(const auto &literal : assumptions)
+  {
+    if(!literal.is_constant())
+      out << literal.dimacs() << " 0\n";
+  }
 
   out.close();
 }

src/solvers/sat/satcheck_glucose.cpp

@@ -28,9 +28,11 @@ void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
 {
   dest.capacity(bv.size());
 
-  forall_literals(it, bv)
-    if(!it->is_false())
-      dest.push(Glucose::mkLit(it->var_no(), it->sign()));
+  for(const auto &literal : bv)
+  {
+    if(!literal.is_false())
+      dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
+  }
 }
 
 template<typename T>
@@ -103,13 +105,16 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
   {
     add_variables();
 
-    forall_literals(it, bv)
+    for(const auto &literal : bv)
     {
-      if(it->is_true())
+      if(literal.is_true())
         return;
-      else if(!it->is_false())
+      else if(!literal.is_false())
+      {
         INVARIANT(
-          it->var_no() < (unsigned)solver->nVars(), "variable not added yet");
+          literal.var_no() < (unsigned)solver->nVars(),
+          "variable not added yet");
+      }
     }
 
     Glucose::vec<Glucose::Lit> c;
@@ -171,9 +176,11 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
       // if assumptions contains false, we need this to be UNSAT
       bool has_false = false;
 
-      forall_literals(it, assumptions)
-        if(it->is_false())
+      for(const auto &literal : assumptions)
+      {
+        if(literal.is_false())
           has_false = true;
+      }
 
       if(has_false)
       {
@@ -271,8 +278,11 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
 {
   assumptions=bv;
 
-  forall_literals(it, assumptions)
-    INVARIANT(!it->is_constant(), "assumption literals must not be constant");
+  for(const auto &literal : assumptions)
+  {
+    INVARIANT(
+      !literal.is_constant(), "assumption literals must not be constant");
+  }
 }
 
 satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(

src/solvers/sat/satcheck_ipasir.cpp

@@ -71,21 +71,24 @@ const std::string satcheck_ipasirt::solver_text()
 
 void satcheck_ipasirt::lcnf(const bvt &bv)
 {
-  forall_literals(it, bv)
+  for(const auto &literal : bv)
   {
-    if(it->is_true())
+    if(literal.is_true())
       return;
-    else if(!it->is_false())
-      INVARIANT(it->var_no()<(unsigned)no_variables(),
-             "reject out of bound variables");
+    else if(!literal.is_false())
+    {
+      INVARIANT(
+        literal.var_no() < (unsigned)no_variables(),
+        "reject out of bound variables");
+    }
   }
 
-  forall_literals(it, bv)
+  for(const auto &literal : bv)
   {
-    if(!it->is_false())
+    if(!literal.is_false())
     {
       // add literal with correct sign
-      ipasir_add(solver, it->dimacs());
+      ipasir_add(solver, literal.dimacs());
     }
   }
   ipasir_add(solver, 0); // terminate clause
@@ -129,9 +132,11 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
   }
   else
   {
-    forall_literals(it, assumptions)
-      if(!it->is_false())
-        ipasir_assume(solver, it->dimacs());
+    for(const auto &literal : assumptions)
+    {
+      if(!literal.is_false())
+        ipasir_assume(solver, literal.dimacs());
+    }
 
     // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
     int solver_state = ipasir_solve(solver);

src/solvers/sat/satcheck_lingeling.cpp

@@ -55,8 +55,8 @@ void satcheck_lingelingt::lcnf(const bvt &bv)
   if(process_clause(bv, new_bv))
     return;
 
-  forall_literals(it, new_bv)
-    lgladd(solver, it->dimacs());
+  for(const auto &literal : new_bv)
+    lgladd(solver, literal.dimacs());
 
   lgladd(solver, 0);
 
@@ -77,8 +77,8 @@ propt::resultt satcheck_lingelingt::do_prop_solve()
 
   std::string msg;
 
-  forall_literals(it, assumptions)
-    lglassume(solver, it->dimacs());
+  for(const auto &literal : assumptions)
+    lglassume(solver, literal.dimacs());
 
   const int res=lglsat(solver);
   CHECK_RETURN(res == 10 || res == 20);