Merge pull request #5787 from tautschnig/forall-literals

tautschnig · web-flow · commit eb148ebabf0c · 2021-01-26T17:46:31.000+01:00
Remove {f,F}orall_literals
diff --git a/.clang-format b/.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',
diff --git a/src/solvers/flattening/boolbv.cpp b/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));
diff --git a/src/solvers/flattening/boolbv_array.cpp b/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;
diff --git a/src/solvers/flattening/boolbv_case.cpp b/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");
diff --git a/src/solvers/flattening/boolbv_complex.cpp b/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;
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/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)
     {
diff --git a/src/solvers/flattening/boolbv_map.cpp b/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;
 
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/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;
         }
diff --git a/src/solvers/flattening/boolbv_vector.cpp b/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());
     }
   }
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/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;
   }
diff --git a/src/solvers/flattening/bv_utils.cpp b/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;
 }
diff --git a/src/solvers/prop/literal.h b/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
diff --git a/src/solvers/prop/prop_minimize.cpp b/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));
   }
diff --git a/src/solvers/refinement/refine_arrays.cpp b/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);
     }
   }
 }
diff --git a/src/solvers/sat/cnf.h b/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;
   }
 };
diff --git a/src/solvers/sat/external_sat.cpp b/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();
 }
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/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(
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/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);
diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/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);
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp

Original file line number	Diff line number	Diff line change
`@@ -36,8 +36,7 @@ bvt boolbvt::convert_array(const exprt &expr)`
`36`	`36`	`{`
`37`	`37`	`const bvt &tmp = convert_bv(*it, op_width);`
`38`	`38`
`39`		`- forall_literals(it2, tmp)`
`40`		`- bv.push_back(*it2);`
	`39`	`+ bv.insert(bv.end(), tmp.begin(), tmp.end());`
`41`	`40`	`}`
`42`	`41`
`43`	`42`	`return bv;`
Original file line number	Diff line number	Diff line change
`@@ -31,8 +31,7 @@ bvt boolbvt::convert_complex(const complex_exprt &expr)`
`31`	`31`	`{`
`32`	`32`	`const bvt &tmp = convert_bv(*it, op_width);`
`33`	`33`
`34`		`- forall_literals(it2, tmp)`
`35`		`- bv.push_back(*it2);`
	`34`	`+ bv.insert(bv.end(), tmp.begin(), tmp.end());`
`36`	`35`	`}`
`37`	`36`
`38`	`37`	`return bv;`
Original file line number	Diff line number	Diff line change
`@@ -34,8 +34,8 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)`
`34`	`34`	`literalt cond_literal=const_literal(false);`
`35`	`35`
`36`	`36`	`// make it free variables`
`37`		`- Forall_literals(it, bv)`
`38`		`- *it=prop.new_variable();`
	`37`	`+ for(auto &literal : bv)`
	`38`	`+ literal = prop.new_variable();`
`39`	`39`
`40`	`40`	`forall_operands(it, expr)`
`41`	`41`	`{`
Original file line number	Diff line number	Diff line change
`@@ -93,7 +93,7 @@ void boolbv_mapt::get_literals(`
`93`	`93`	`map_entry.literal_map.size() == width,`
`94`	`94`	`"number of literals in the literal map shall equal the bitvector width");`
`95`	`95`
`96`		`- Forall_literals(it, literals)`
	`96`	`+ for(auto it = literals.begin(); it != literals.end(); ++it)`
`97`	`97`	`{`
`98`	`98`	`literalt &l=*it;`
`99`	`99`	`const std::size_t bit=it-literals.begin();`
`@@ -127,7 +127,7 @@ void boolbv_mapt::set_literals(`
`127`	`127`	`{`
`128`	`128`	`map_entryt &map_entry=get_map_entry(identifier, type);`
`129`	`129`
`130`		`- forall_literals(it, literals)`
	`130`	`+ for(auto it = literals.begin(); it != literals.end(); ++it)`
`131`	`131`	`{`
`132`	`132`	`const literalt &literal=*it;`
`133`	`133`
Original file line number	Diff line number	Diff line change
`@@ -64,8 +64,7 @@ bool boolbvt::type_conversion(`
`64`	`64`	`{`
`65`	`65`	`if(src_type==dest_type.subtype())`
`66`	`66`	`{`
`67`		`- forall_literals(it, src)`
`68`		`- dest.push_back(*it);`
	`67`	`+ dest.insert(dest.end(), src.begin(), src.end());`
`69`	`68`
`70`	`69`	`// pad with zeros`
`71`	`70`	`for(std::size_t i=src.size(); i<dest_width; i++)`
`@@ -208,8 +207,8 @@ bool boolbvt::type_conversion(`
`208`	`207`	`INVARIANT(`
`209`	`208`	`src_width == 1, "bitvector of type boolean shall have width one");`
`210`	`209`
`211`		`- Forall_literals(it, dest)`
`212`		`- it=prop.land(it, src[0]);`
	`210`	`+ for(auto &literal : dest)`
	`211`	`+ literal = prop.land(literal, src[0]);`
`213`	`212`
`214`	`213`	`return false;`
`215`	`214`	`}`
Original file line number	Diff line number	Diff line change
`@@ -29,8 +29,7 @@ bvt boolbvt::convert_vector(const vector_exprt &expr)`
`29`	`29`	`{`
`30`	`30`	`const bvt &tmp = convert_bv(*it, op_width);`
`31`	`31`
`32`		`- forall_literals(it2, tmp)`
`33`		`- bv.push_back(*it2);`
	`32`	`+ bv.insert(bv.end(), tmp.begin(), tmp.end());`
`34`	`33`	`}`
`35`	`34`	`}`
`36`	`35`
Original file line number	Diff line number	Diff line change
`@@ -243,8 +243,8 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)`
`243`	`243`	`bvt bv;`
`244`	`244`	`bv.resize(bits);`
`245`	`245`
`246`		`- Forall_literals(it, bv)`
`247`		`- *it=prop.new_variable();`
	`246`	`+ for(auto &literal : bv)`
	`247`	`+ literal = prop.new_variable();`
`248`	`248`
`249`	`249`	`return bv;`
`250`	`250`	`}`