Merge pull request #1950 from romainbrenguier/refactor/prop_conv_straightforward

Partial solver cleanup (straightforward changes)

Author: romainbrenguier

src/cbmc/bv_cbmc.cpp

@@ -20,13 +20,11 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
     throw 0;
   }
 
-  exprt new_cycle;
   const exprt &old_cycle=expr.op0();
   const exprt &cycle_var=expr.op1();
   const exprt &bound=expr.op2();
   const exprt &predicate=expr.op3();
-
-  make_free_bv_expr(expr.type(), new_cycle);
+  const exprt new_cycle = make_free_bv_expr(expr.type());
 
   mp_integer bound_value;
   if(to_integer(bound, bound_value))
@@ -98,18 +96,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
 
 bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr)
 {
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor_symbol expected to have one operand" << eom;
-    throw 0;
-  }
-
-  exprt result;
+  PRECONDITION(expr.operands().size() == 1);
   const exprt &bound=expr.op0();
-
-  make_free_bv_expr(expr.type(), result);
-
+  const exprt result = make_free_bv_expr(expr.type());
   // constraint: result<=bound
 
   set_to_true(binary_relation_exprt(result, ID_le, bound));

src/solvers/flattening/boolbv.cpp

@@ -631,54 +631,33 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
 
 void boolbvt::set_to(const exprt &expr, bool value)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    error() << "boolbvt::set_to got non-boolean operand: "
-            << expr.pretty() << eom;
-    throw 0;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
-  if(value)
-  {
-    if(expr.id()==ID_equal)
-    {
-      if(!boolbv_set_equality_to_true(to_equal_expr(expr)))
-        return;
-    }
-  }
-
-  return SUB::set_to(expr, value);
+  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
+  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
+    return;
+  SUB::set_to(expr, value);
 }
 
-void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
+exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
 {
-  dest=exprt(ID_bv_literals, type);
+  exprt dest(ID_bv_literals, type);
   irept::subt &bv_sub=dest.add(ID_bv).get_sub();
-
   bv_sub.resize(bv.size());
 
   for(std::size_t i=0; i<bv.size(); i++)
     bv_sub[i].id(std::to_string(bv[i].get()));
+  return dest;
 }
 
-void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
+exprt boolbvt::make_free_bv_expr(const typet &type)
 {
-  std::size_t width=boolbv_width(type);
-
-  if(width==0)
-  {
-    error() << "failed to get width of " << type.pretty() << eom;
-    throw 0;
-  }
-
-  bvt bv;
-  bv.resize(width);
-
-  // make result free variables
-  Forall_literals(it, bv)
-    *it=prop.new_variable();
-
-  make_bv_expr(type, bv, dest);
+  const std::size_t width = boolbv_width(type);
+  PRECONDITION(width != 0);
+  bvt bv(width);
+  for(auto &lit : bv)
+    lit = prop.new_variable();
+  return make_bv_expr(type, bv);
 }
 
 bool boolbvt::is_unbounded_array(const typet &type) const
@@ -708,12 +687,8 @@ bool boolbvt::is_unbounded_array(const typet &type) const
 void boolbvt::print_assignment(std::ostream &out) const
 {
   arrayst::print_assignment(out);
-
-  for(const auto &it : map.mapping)
-  {
-    out << it.first << "="
-        << it.second.get_value(prop) << '\n';
-  }
+  for(const auto &pair : map.mapping)
+    out << pair.first << "=" << pair.second.get_value(prop) << '\n';
 }
 
 void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest)

src/solvers/flattening/boolbv.h

@@ -99,7 +99,7 @@ class boolbvt:public arrayst
   boolbv_mapt map;
 
   // overloading
-  virtual literalt convert_rest(const exprt &expr) override;
+  literalt convert_rest(const exprt &expr) override;
   virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
 
   // NOLINTNEXTLINE(readability/identifiers)
@@ -176,8 +176,8 @@ class boolbvt:public arrayst
   virtual bvt convert_function_application(
     const function_application_exprt &expr);
 
-  virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
-  virtual void make_free_bv_expr(const typet &type, exprt &dest);
+  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
+  virtual exprt make_free_bv_expr(const typet &type);
 
   void convert_with(
     const typet &type,

src/solvers/prop/prop.h

@@ -87,7 +87,7 @@ class propt:public messaget, public prop_assignmentt
 
   // variables
   virtual literalt new_variable()=0;
-  virtual void set_variable_name(literalt a, const std::string &name) { }
+  virtual void set_variable_name(literalt a, const irep_idt &name) { }
   virtual size_t no_variables() const=0;
   bvt new_variables(std::size_t width);
 

src/solvers/prop/prop_conv.cpp

@@ -7,40 +7,30 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "prop_conv.h"
-
-#include <cassert>
-#include <cstdlib>
-#include <map>
-
-#include <util/std_expr.h>
-#include <util/symbol.h>
-#include <util/threeval.h>
-
-#include "prop.h"
-#include "literal_expr.h"
+#include <algorithm>
 
 /// determine whether a variable is in the final conflict
 bool prop_convt::is_in_conflict(literalt l) const
 {
-  assert(false);
+  UNREACHABLE;
   return false;
 }
 
 void prop_convt::set_assumptions(const bvt &)
 {
-  assert(false);
+  UNREACHABLE;
 }
 
 void prop_convt::set_frozen(const literalt)
 {
-  assert(false);
+  UNREACHABLE;
 }
 
 void prop_convt::set_frozen(const bvt &bv)
 {
-  for(unsigned i=0; i<bv.size(); i++)
-    if(!bv[i].is_constant())
-      set_frozen(bv[i]);
+  for(const auto &bit : bv)
+    if(!bit.is_constant())
+      set_frozen(bit);
 }
 
 bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
@@ -65,17 +55,14 @@ bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
 
 literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
 {
-  std::pair<symbolst::iterator, bool> result=
+  auto result =
     symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
 
   if(!result.second)
     return result.first->second;
 
-  // produce new variable
   literalt literal=prop.new_variable();
-
-  // set the name of the new variable
-  prop.set_variable_name(literal, id2string(identifier));
+  prop.set_variable_name(literal, identifier);
 
   // insert
   result.first->second=literal;
@@ -183,10 +170,9 @@ literalt prop_conv_solvert::convert(const exprt &expr)
       prop.set_frozen(literal);
     return literal;
   }
-  // check cache first
 
-  std::pair<cachet::iterator, bool> result=
-    cache.insert(std::pair<exprt, literalt>(expr, literalt()));
+  // check cache first
+  auto result = cache.insert({expr, literalt()});
 
   if(!result.second)
     return result.first->second;
@@ -208,13 +194,7 @@ literalt prop_conv_solvert::convert(const exprt &expr)
 
 literalt prop_conv_solvert::convert_bool(const exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    std::string msg="prop_convt::convert_bool got "
-                    "non-boolean expression: ";
-    msg+=expr.pretty();
-    throw msg;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
   const exprt::operandst &op=expr.operands();
 
@@ -280,8 +260,9 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
           expr.id()==ID_nor || expr.id()==ID_nand)
   {
-    if(op.empty())
-      throw "operator `"+expr.id_string()+"' takes at least one operand";
+    INVARIANT(
+      !op.empty(),
+      "operator `" + expr.id_string() + "' takes at least one operand");
 
     bvt bv;
 
@@ -304,16 +285,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   }
   else if(expr.id()==ID_not)
   {
-    if(op.size()!=1)
-      throw "not takes one operand";
-
+    INVARIANT(op.size() == 1, "not takes one operand");
     return !convert(op.front());
   }
   else if(expr.id()==ID_equal || expr.id()==ID_notequal)
   {
-    if(op.size()!=2)
-      throw "equality takes two operands";
-
+    INVARIANT(op.size() == 2, "equality takes two operands");
     bool equal=(expr.id()==ID_equal);
 
     if(op[0].type().id()==ID_bool &&
@@ -387,24 +364,14 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
 
 void prop_conv_solvert::set_to(const exprt &expr, bool value)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    std::string msg="prop_convt::set_to got "
-                    "non-boolean expression: ";
-    msg+=expr.pretty();
-    throw msg;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
-  bool boolean=true;
-
-  forall_operands(it, expr)
-    if(it->type().id()!=ID_bool)
-    {
-      boolean=false;
-      break;
-    }
+  const bool has_only_boolean_operands = std::all_of(
+    expr.operands().begin(),
+    expr.operands().end(),
+    [](const exprt &expr) { return expr.type().id() == ID_bool; });
 
-  if(boolean)
+  if(has_only_boolean_operands)
   {
     if(expr.id()==ID_not)
     {
@@ -507,16 +474,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   statistics() << "Solving with " << prop.solver_text() << eom;
 
-  propt::resultt result=prop.prop_solve();
-
-  switch(result)
+  switch(prop.prop_solve())
   {
     case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
     case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
     default: return resultt::D_ERROR;
   }
-
-  return resultt::D_ERROR;
 }
 
 exprt prop_conv_solvert::get(const exprt &expr) const
@@ -534,19 +497,17 @@ exprt prop_conv_solvert::get(const exprt &expr) const
     }
   }
 
-  exprt tmp=expr;
-
-  Forall_operands(it, tmp)
+  exprt tmp = expr;
+  for(auto &op : tmp.operands())
   {
-    exprt tmp_op=get(*it);
-    it->swap(tmp_op);
+    exprt tmp_op = get(op);
+    op.swap(tmp_op);
   }
-
   return tmp;
 }
 
 void prop_conv_solvert::print_assignment(std::ostream &out) const
 {
-  for(const auto &it : symbols)
-    out << it.first << " = " << prop.l_get(it.second) << "\n";
+  for(const auto &symbol : symbols)
+    out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
 }