New iterator macro forall_literals, Forall_literals

kroening · kroening · commit 1009ce712c27 · 2012-02-28T09:48:56.000Z
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1052 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
diff --git a/src/solvers/cvc/cvc_prop.cpp b/src/solvers/cvc/cvc_prop.cpp
@@ -205,10 +205,10 @@ literalt cvc_propt::land(const bvt &bv)
 
   literalt literal=def_cvc_literal();
 
-  for(unsigned int i=0; i<bv.size(); ++i)
+  forall_literals(it, bv)
   {
-    if(i!=0) out << " AND ";
-    out << cvc_literal(bv[i]);
+    if(it!=bv.begin()) out << " AND ";
+    out << cvc_literal(*it);
   }
   
   out << ";" << std::endl << std::endl;
@@ -234,10 +234,10 @@ literalt cvc_propt::lor(const bvt &bv)
 
   literalt literal=def_cvc_literal();
 
-  for(unsigned int i=0; i<bv.size(); ++i)
+  forall_literals(it, bv)
   {
-    if(i!=0) out << " OR ";
-    out << cvc_literal(bv[i]);
+    if(it!=bv.begin()) out << " OR ";
+    out << cvc_literal(*it);
   }
   
   out << ";" << std::endl << std::endl;
@@ -265,8 +265,8 @@ literalt cvc_propt::lxor(const bvt &bv)
 
   literalt literal=const_literal(false);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=lxor(bv[i], literal);
+  forall_literals(it, bv)
+    literal=lxor(*it, literal);
 
   return literal;
 }
diff --git a/src/solvers/dplib/dplib_prop.cpp b/src/solvers/dplib/dplib_prop.cpp
@@ -190,10 +190,10 @@ literalt dplib_propt::land(const bvt &bv)
 
   literalt literal=def_dplib_literal();
 
-  for(unsigned int i=0; i<bv.size(); ++i)
+  forall_literals(it, bv)
   {
-    if(i!=0) out << " & ";
-    out << dplib_literal(bv[i]);
+    if(it!=bv.begin()) out << " & ";
+    out << dplib_literal(*it);
   }
   
   out << std::endl << std::endl;
@@ -219,10 +219,10 @@ literalt dplib_propt::lor(const bvt &bv)
 
   literalt literal=def_dplib_literal();
 
-  for(unsigned int i=0; i<bv.size(); ++i)
+  forall_literals(it, bv)
   {
-    if(i!=0) out << " | ";
-    out << dplib_literal(bv[i]);
+    if(it!=bv.begin()) out << " | ";
+    out << dplib_literal(*it);
   }
   
   out << std::endl << std::endl;
@@ -250,8 +250,8 @@ literalt dplib_propt::lxor(const bvt &bv)
 
   literalt literal=const_literal(false);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=lxor(bv[i], literal);
+  forall_literals(it, bv)
+    literal=lxor(*it, literal);
 
   return literal;
 }
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -153,8 +153,8 @@ void boolbvt::convert_bv(const exprt &expr, bvt &bv)
   convert_bitvector(expr, bv);
   
   // check
-  for(unsigned i=0; i<bv.size(); i++)
-    if(bv[i].var_no()==literalt::unused_var_no())
+  forall_literals(it, bv)
+    if(it->var_no()==literalt::unused_var_no())
     {
       std::cout << "unused_var_no: " << expr.pretty() << std::endl;
       assert(false);
@@ -516,9 +516,9 @@ void boolbvt::convert_symbol(const exprt &expr, bvt &bv)
     for(unsigned i=0; i<width; i++)
       bv[i]=map.get_literal(identifier, i, expr.type());
 
-    for(unsigned i=0; i<width; i++)
-      if(bv[i].var_no()>=prop.no_variables() &&
-        !bv[i].is_constant()) { std::cout << identifier << std::endl; abort(); }
+    forall_literals(it, bv)
+      if(it->var_no()>=prop.no_variables() &&
+        !it->is_constant()) { std::cout << identifier << std::endl; abort(); }
   }
 }
    
@@ -841,8 +841,8 @@ void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
   bv.resize(width);
 
   // make result free variables
-  for(unsigned i=0; i<bv.size(); i++)
-    bv[i]=prop.new_variable();
+  Forall_literals(it, bv)
+    *it=prop.new_variable();
 
   make_bv_expr(type, bv, dest);
 }
diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp
@@ -34,8 +34,8 @@ void boolbvt::convert_case(const exprt &expr, bvt &bv)
   bv.resize(width);
 
   // make it free variables
-  for(unsigned i=0; i<bv.size(); i++)
-    bv[i]=prop.new_variable();
+  Forall_literals(it, bv)
+    *it=prop.new_variable();
 
   if(operands.size()<3)
     throw "case takes at least three operands";
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
@@ -34,8 +34,8 @@ void boolbvt::convert_cond(const exprt &expr, bvt &bv)
   bv.resize(width);
 
   // make it free variables
-  for(unsigned i=0; i<bv.size(); i++)
-    bv[i]=prop.new_variable();
+  Forall_literals(it, bv)
+    *it=prop.new_variable();
 
   if(operands.size()<2)
     throw "cond takes at least two operands";
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
@@ -135,8 +135,8 @@ void boolbvt::convert_typecast(const exprt &expr, bvt &bv)
 
           assert(op_width==1);
           
-          for(unsigned i=0; i<bv.size(); i++)
-            bv[i]=prop.land(bv[i], op_bv[0]);
+          Forall_literals(it, bv)
+            *it=prop.land(*it, op_bv[0]);
             
           return;
         }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -318,8 +318,8 @@ void bv_pointerst::convert_pointer_type(const exprt &expr, bvt &bv)
   }
   else if(expr.id()==ID_nondet_symbol)
   {
-    for(unsigned i=0; i<bits; i++)
-      bv[i]=prop.new_variable();
+    Forall_literals(it, bv)
+      *it=prop.new_variable();
 
     return;
   }
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
@@ -707,10 +707,10 @@ void bv_utilst::incrementer(
 {
   carry_out=carry_in;
 
-  for(unsigned i=0; i<bv.size(); i++)
+  Forall_literals(it, bv)
   {
-    literalt new_carry=prop.land(carry_out, bv[i]);
-    bv[i]=prop.lxor(bv[i], carry_out);
+    literalt new_carry=prop.land(carry_out, *it);
+    *it=prop.lxor(*it, carry_out);
     carry_out=new_carry;
   }
 }
@@ -750,8 +750,8 @@ Function: bv_utilst::invert
 bvt bv_utilst::inverted(const bvt &bv)
 {
   bvt result=bv;
-  for(unsigned i=0; i<bv.size(); i++)
-    result[i]=prop.lnot(result[i]);
+  Forall_literals(it, result)
+    *it=prop.lnot(*it);
   return result;
 }
 
@@ -1311,8 +1311,8 @@ Function: bv_utilst::is_constant
 
 bool bv_utilst::is_constant(const bvt &bv)
 {
-  for(unsigned i=0; i<bv.size(); i++)
-    if(bv[i]!=const_literal(false) && bv[i]!=const_literal(true))
+  forall_literals(it, bv)
+    if(!it->is_constant())
       return false;
 
   return true;
diff --git a/src/solvers/prop/aig_prop.cpp b/src/solvers/prop/aig_prop.cpp
@@ -119,8 +119,8 @@ literalt aig_propt::land(const bvt &bv)
 {
   literalt literal=const_literal(true);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=land(bv[i], literal);
+  forall_literals(it, bv)
+    literal=land(*it, literal);
 
   return literal;
 }
@@ -141,8 +141,8 @@ literalt aig_propt::lor(const bvt &bv)
 {
   literalt literal=const_literal(false);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=lor(bv[i], literal);
+  forall_literals(it, bv)
+    literal=lor(*it, literal);
 
   return literal;
 }
@@ -163,8 +163,8 @@ literalt aig_propt::lxor(const bvt &bv)
 {
   literalt literal=const_literal(false);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=lxor(bv[i], literal);
+  forall_literals(it, bv)
+    literal=lxor(*it, literal);
 
   return literal;
 }
diff --git a/src/solvers/prop/literal.h b/src/solvers/prop/literal.h
@@ -185,4 +185,13 @@ literalt pos(literalt a);
 
 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
diff --git a/src/solvers/qbf/qbf_bdd_core.cpp b/src/solvers/qbf/qbf_bdd_core.cpp
@@ -385,21 +385,19 @@ Function: qbf_bdd_coret::lor
 
 literalt qbf_bdd_coret::lor(const bvt &bv)
 {   
-  for(unsigned long i=0; i<bv.size(); i++)
-  {
-    if(bv[i]==const_literal(true))
+  forall_literals(it, bv)
+    if(*it==const_literal(true))
       return const_literal(true);
-  }
   
   literalt nl = new_variable();
   
   std::cout << "LORX" << std::endl;
   
   BDD &orbdd = *bdd_variable_map[nl.var_no()];
 
-  for(unsigned long i=0; i<bv.size(); i++)
+  forall_literals(it, bv)
   {
-    literalt l=bv[i];
+    literalt l=*it;
     
     if(l==const_literal(false))
       continue;
diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp
@@ -296,8 +296,8 @@ literalt cnft::land(const bvt &bv)
   if(bv.size()==1) return bv[0];
   if(bv.size()==2) return land(bv[0], bv[1]);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    if(bv[i]==const_literal(false))
+  forall_literals(it, bv)
+    if(*it==const_literal(false))
       return const_literal(false);
 
   if(is_all(bv, const_literal(true)))
@@ -309,20 +309,20 @@ literalt cnft::land(const bvt &bv)
 
   literalt literal=new_variable();
 
-  for(unsigned int i=0; i<new_bv.size(); ++i)
+  forall_literals(it, new_bv)
   {
     bvt lits;
     lits.reserve(2);
-    lits.push_back(pos(new_bv[i]));
+    lits.push_back(pos(*it));
     lits.push_back(neg(literal));
     lcnf(lits);
   }
 
   bvt lits;
   lits.reserve(new_bv.size()+1);
 
-  for(unsigned int i=0; i<new_bv.size(); ++i)
-    lits.push_back(neg(new_bv[i]));
+  forall_literals(it, new_bv)
+    lits.push_back(neg(*it));
 
   lits.push_back(pos(literal));
   lcnf(lits);
@@ -348,8 +348,8 @@ literalt cnft::lor(const bvt &bv)
   if(bv.size()==1) return bv[0];
   if(bv.size()==2) return lor(bv[0], bv[1]);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    if(bv[i]==const_literal(true))
+  forall_literals(it, bv)
+    if(*it==const_literal(true))
       return const_literal(true);
 
   if(is_all(bv, const_literal(false)))
@@ -361,20 +361,20 @@ literalt cnft::lor(const bvt &bv)
 
   literalt literal=new_variable();
 
-  for(unsigned int i=0; i<new_bv.size(); ++i)
+  forall_literals(it, new_bv)
   {
     bvt lits;
     lits.reserve(2);
-    lits.push_back(neg(new_bv[i]));
+    lits.push_back(neg(*it));
     lits.push_back(pos(literal));
     lcnf(lits);
   }
 
   bvt lits;
   lits.reserve(new_bv.size()+1);
 
-  for(unsigned int i=0; i<new_bv.size(); ++i)
-    lits.push_back(pos(new_bv[i]));
+  forall_literals(it, new_bv)
+    lits.push_back(pos(*it));
 
   lits.push_back(neg(literal));
   lcnf(lits);
@@ -402,8 +402,8 @@ literalt cnft::lxor(const bvt &bv)
 
   literalt literal=const_literal(false);
 
-  for(unsigned i=0; i<bv.size(); i++)
-    literal=lxor(bv[i], literal);
+  forall_literals(it, bv)
+    literal=lxor(*it, literal);
 
   return literal;
 }
diff --git a/src/solvers/sat/cnf.h b/src/solvers/sat/cnf.h
@@ -51,8 +51,8 @@ class cnft:public propt
 
   static bool is_all(const bvt &bv, literalt l)
   {
-    for(unsigned i=0; i<bv.size(); i++)
-      if(bv[i]!=l) return false;
+    forall_literals(it, bv)
+      if(*it!=l) return false;
     return true;
   }
 };
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
@@ -39,8 +39,8 @@ void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
 {
   dest.growTo(bv.size());
   
-  for(unsigned i=0; i<bv.size(); i++)
-    dest[i]=Minisat::mkLit(bv[i].var_no(), bv[i].sign());
+  forall_literals(it, bv)
+    dest[it-bv.begin()]=Minisat::mkLit(it->var_no(), it->sign());
 }
 
 /*******************************************************************\
@@ -167,8 +167,8 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
   Minisat::vec<Minisat::Lit> c;
   convert(new_bv, c);
 
-  for(unsigned i=0; i<new_bv.size(); i++)
-    assert(new_bv[i].var_no()<(unsigned)solver->nVars());
+  forall_literals(it, new_bv)
+    assert(it->var_no()<(unsigned)solver->nVars());
 
   solver->addClause(c);
 
@@ -375,9 +375,7 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
 {
   assumptions=bv;
 
-  for(bvt::const_iterator it=assumptions.begin();
-      it!=assumptions.end();
-      it++)
+  forall_literals(it, assumptions)
     assert(!it->is_constant());
 }
 
diff --git a/src/solvers/smt1/smt1_prop.cpp b/src/solvers/smt1/smt1_prop.cpp
diff --git a/src/solvers/smt2/smt2_prop.cpp b/src/solvers/smt2/smt2_prop.cpp

Original file line number	Diff line number	Diff line change
`@@ -205,10 +205,10 @@ literalt cvc_propt::land(const bvt &bv)`
`205`	`205`
`206`	`206`	`literalt literal=def_cvc_literal();`
`207`	`207`
`208`		`- for(unsigned int i=0; i<bv.size(); ++i)`
	`208`	`+ forall_literals(it, bv)`
`209`	`209`	`{`
`210`		`- if(i!=0) out << " AND ";`
`211`		`- out << cvc_literal(bv[i]);`
	`210`	`+ if(it!=bv.begin()) out << " AND ";`
	`211`	`+ out << cvc_literal(*it);`
`212`	`212`	`}`
`213`	`213`
`214`	`214`	`out << ";" << std::endl << std::endl;`
`@@ -234,10 +234,10 @@ literalt cvc_propt::lor(const bvt &bv)`
`234`	`234`
`235`	`235`	`literalt literal=def_cvc_literal();`
`236`	`236`
`237`		`- for(unsigned int i=0; i<bv.size(); ++i)`
	`237`	`+ forall_literals(it, bv)`
`238`	`238`	`{`
`239`		`- if(i!=0) out << " OR ";`
`240`		`- out << cvc_literal(bv[i]);`
	`239`	`+ if(it!=bv.begin()) out << " OR ";`
	`240`	`+ out << cvc_literal(*it);`
`241`	`241`	`}`
`242`	`242`
`243`	`243`	`out << ";" << std::endl << std::endl;`
`@@ -265,8 +265,8 @@ literalt cvc_propt::lxor(const bvt &bv)`
`265`	`265`
`266`	`266`	`literalt literal=const_literal(false);`
`267`	`267`
`268`		`- for(unsigned i=0; i<bv.size(); i++)`
`269`		`- literal=lxor(bv[i], literal);`
	`268`	`+ forall_literals(it, bv)`
	`269`	`+ literal=lxor(*it, literal);`
`270`	`270`
`271`	`271`	`return literal;`
`272`	`272`	`}`
Original file line number	Diff line number	Diff line change
`@@ -190,10 +190,10 @@ literalt dplib_propt::land(const bvt &bv)`
`190`	`190`
`191`	`191`	`literalt literal=def_dplib_literal();`
`192`	`192`
`193`		`- for(unsigned int i=0; i<bv.size(); ++i)`
	`193`	`+ forall_literals(it, bv)`
`194`	`194`	`{`
`195`		`- if(i!=0) out << " & ";`
`196`		`- out << dplib_literal(bv[i]);`
	`195`	`+ if(it!=bv.begin()) out << " & ";`
	`196`	`+ out << dplib_literal(*it);`
`197`	`197`	`}`
`198`	`198`
`199`	`199`	`out << std::endl << std::endl;`
`@@ -219,10 +219,10 @@ literalt dplib_propt::lor(const bvt &bv)`
`219`	`219`
`220`	`220`	`literalt literal=def_dplib_literal();`
`221`	`221`
`222`		`- for(unsigned int i=0; i<bv.size(); ++i)`
	`222`	`+ forall_literals(it, bv)`
`223`	`223`	`{`
`224`		`- if(i!=0) out << " \| ";`
`225`		`- out << dplib_literal(bv[i]);`
	`224`	`+ if(it!=bv.begin()) out << " \| ";`
	`225`	`+ out << dplib_literal(*it);`
`226`	`226`	`}`
`227`	`227`
`228`	`228`	`out << std::endl << std::endl;`
`@@ -250,8 +250,8 @@ literalt dplib_propt::lxor(const bvt &bv)`
`250`	`250`
`251`	`251`	`literalt literal=const_literal(false);`
`252`	`252`
`253`		`- for(unsigned i=0; i<bv.size(); i++)`
`254`		`- literal=lxor(bv[i], literal);`
	`253`	`+ forall_literals(it, bv)`
	`254`	`+ literal=lxor(*it, literal);`
`255`	`255`
`256`	`256`	`return literal;`
`257`	`257`	`}`
Original file line number	Diff line number	Diff line change
`@@ -135,8 +135,8 @@ void boolbvt::convert_typecast(const exprt &expr, bvt &bv)`
`135`	`135`
`136`	`136`	`assert(op_width==1);`
`137`	`137`
`138`		`- for(unsigned i=0; i<bv.size(); i++)`
`139`		`- bv[i]=prop.land(bv[i], op_bv[0]);`
	`138`	`+ Forall_literals(it, bv)`
	`139`	`+ it=prop.land(it, op_bv[0]);`
`140`	`140`
`141`	`141`	`return;`
`142`	`142`	`}`
Original file line number	Diff line number	Diff line change
`@@ -318,8 +318,8 @@ void bv_pointerst::convert_pointer_type(const exprt &expr, bvt &bv)`
`318`	`318`	`}`
`319`	`319`	`else if(expr.id()==ID_nondet_symbol)`
`320`	`320`	`{`
`321`		`- for(unsigned i=0; i<bits; i++)`
`322`		`- bv[i]=prop.new_variable();`
	`321`	`+ Forall_literals(it, bv)`
	`322`	`+ *it=prop.new_variable();`
`323`	`323`
`324`	`324`	`return;`
`325`	`325`	`}`
Original file line number	Diff line number	Diff line change
`@@ -707,10 +707,10 @@ void bv_utilst::incrementer(`
`707`	`707`	`{`
`708`	`708`	`carry_out=carry_in;`
`709`	`709`
`710`		`- for(unsigned i=0; i<bv.size(); i++)`
	`710`	`+ Forall_literals(it, bv)`
`711`	`711`	`{`
`712`		`- literalt new_carry=prop.land(carry_out, bv[i]);`
`713`		`- bv[i]=prop.lxor(bv[i], carry_out);`
	`712`	`+ literalt new_carry=prop.land(carry_out, *it);`
	`713`	`+ it=prop.lxor(it, carry_out);`
`714`	`714`	`carry_out=new_carry;`
`715`	`715`	`}`
`716`	`716`	`}`
`@@ -750,8 +750,8 @@ Function: bv_utilst::invert`
`750`	`750`	`bvt bv_utilst::inverted(const bvt &bv)`
`751`	`751`	`{`
`752`	`752`	`bvt result=bv;`
`753`		`- for(unsigned i=0; i<bv.size(); i++)`
`754`		`- result[i]=prop.lnot(result[i]);`
	`753`	`+ Forall_literals(it, result)`
	`754`	`+ it=prop.lnot(it);`
`755`	`755`	`return result;`
`756`	`756`	`}`
`757`	`757`
`@@ -1311,8 +1311,8 @@ Function: bv_utilst::is_constant`
`1311`	`1311`
`1312`	`1312`	`bool bv_utilst::is_constant(const bvt &bv)`
`1313`	`1313`	`{`
`1314`		`- for(unsigned i=0; i<bv.size(); i++)`
`1315`		`- if(bv[i]!=const_literal(false) && bv[i]!=const_literal(true))`
	`1314`	`+ forall_literals(it, bv)`
	`1315`	`+ if(!it->is_constant())`
`1316`	`1316`	`return false;`
`1317`	`1317`
`1318`	`1318`	`return true;`
Original file line number	Diff line number	Diff line change
`@@ -119,8 +119,8 @@ literalt aig_propt::land(const bvt &bv)`
`119`	`119`	`{`
`120`	`120`	`literalt literal=const_literal(true);`
`121`	`121`
`122`		`- for(unsigned i=0; i<bv.size(); i++)`
`123`		`- literal=land(bv[i], literal);`
	`122`	`+ forall_literals(it, bv)`
	`123`	`+ literal=land(*it, literal);`
`124`	`124`
`125`	`125`	`return literal;`
`126`	`126`	`}`
`@@ -141,8 +141,8 @@ literalt aig_propt::lor(const bvt &bv)`
`141`	`141`	`{`
`142`	`142`	`literalt literal=const_literal(false);`
`143`	`143`
`144`		`- for(unsigned i=0; i<bv.size(); i++)`
`145`		`- literal=lor(bv[i], literal);`
	`144`	`+ forall_literals(it, bv)`
	`145`	`+ literal=lor(*it, literal);`
`146`	`146`
`147`	`147`	`return literal;`
`148`	`148`	`}`
`@@ -163,8 +163,8 @@ literalt aig_propt::lxor(const bvt &bv)`
`163`	`163`	`{`
`164`	`164`	`literalt literal=const_literal(false);`
`165`	`165`
`166`		`- for(unsigned i=0; i<bv.size(); i++)`
`167`		`- literal=lxor(bv[i], literal);`
	`166`	`+ forall_literals(it, bv)`
	`167`	`+ literal=lxor(*it, literal);`
`168`	`168`
`169`	`169`	`return literal;`
`170`	`170`	`}`
Original file line number	Diff line number	Diff line change
`@@ -51,8 +51,8 @@ class cnft:public propt`
`51`	`51`
`52`	`52`	`static bool is_all(const bvt &bv, literalt l)`
`53`	`53`	`{`
`54`		`- for(unsigned i=0; i<bv.size(); i++)`
`55`		`- if(bv[i]!=l) return false;`
	`54`	`+ forall_literals(it, bv)`
	`55`	`+ if(*it!=l) return false;`
`56`	`56`	`return true;`
`57`	`57`	`}`
`58`	`58`	`};`
Original file line number	Diff line number	Diff line change
`@@ -39,8 +39,8 @@ void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)`
`39`	`39`	`{`
`40`	`40`	`dest.growTo(bv.size());`
`41`	`41`
`42`		`- for(unsigned i=0; i<bv.size(); i++)`
`43`		`- dest[i]=Minisat::mkLit(bv[i].var_no(), bv[i].sign());`
	`42`	`+ forall_literals(it, bv)`
	`43`	`+ dest[it-bv.begin()]=Minisat::mkLit(it->var_no(), it->sign());`
`44`	`44`	`}`
`45`	`45`
`46`	`46`	`/*******************************************************************\`
`@@ -167,8 +167,8 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)`
`167`	`167`	`Minisat::vec<Minisat::Lit> c;`
`168`	`168`	`convert(new_bv, c);`
`169`	`169`
`170`		`- for(unsigned i=0; i<new_bv.size(); i++)`
`171`		`- assert(new_bv[i].var_no()<(unsigned)solver->nVars());`
	`170`	`+ forall_literals(it, new_bv)`
	`171`	`+ assert(it->var_no()<(unsigned)solver->nVars());`
`172`	`172`
`173`	`173`	`solver->addClause(c);`
`174`	`174`
`@@ -375,9 +375,7 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)`
`375`	`375`	`{`
`376`	`376`	`assumptions=bv;`
`377`	`377`
`378`		`- for(bvt::const_iterator it=assumptions.begin();`
`379`		`- it!=assumptions.end();`
`380`		`- it++)`
	`378`	`+ forall_literals(it, assumptions)`
`381`	`379`	`assert(!it->is_constant());`
`382`	`380`	`}`
`383`	`381`