Partial cleanup in solver code

src/solvers/flattening/arrays.cpp

@@ -34,7 +34,7 @@ void arrayst::record_array_index(const index_exprt &index)
   // we are not allowed to put the index directly in the
   //   entry for the root of the equivalence class
   //   because this map is accessed during building the error trace
-  std::size_t number=arrays.number(index.array());
+  const std::size_t number = arrays.number(index.array());
   index_map[number].insert(index.index());
   update_indices.insert(number);
 }
@@ -45,14 +45,9 @@ literalt arrayst::record_array_equality(
   const exprt &op0=equality.op0();
   const exprt &op1=equality.op1();
 
-  // check types
-  if(!base_type_eq(op0.type(), op1.type(), ns))
-  {
-    prop.error() << equality.pretty() << messaget::eom;
-    DATA_INVARIANT(
-      false,
-      "record_array_equality got equality without matching types");
-  }
+  DATA_INVARIANT(
+    base_type_eq(op0.type(), op1.type(), ns),
+    "record_array_equality should get matching types");
 
   DATA_INVARIANT(
     ns.follow(op0.type()).id()==ID_array,
@@ -62,7 +57,7 @@ literalt arrayst::record_array_equality(
 
   array_equalities.back().f1=op0;
   array_equalities.back().f2=op1;
-  array_equalities.back().l=SUB::equality(op0, op1);
+  array_equalities.back().l = baset::equality(op0, op1);
 
   arrays.make_union(op0, op1);
   collect_arrays(op0);

src/solvers/flattening/arrays.h

@@ -27,17 +27,18 @@ class update_exprt;
 
 class arrayst:public equalityt
 {
+private:
+  typedef equalityt baset;
+
 public:
   arrayst(const namespacet &_ns, propt &_prop);
 
   void post_process() override
   {
     post_process_arrays();
-    SUB::post_process();
+    baset::post_process();
   }
 
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef equalityt SUB;
 
   literalt record_array_equality(const equal_exprt &expr);
   void record_array_index(const index_exprt &expr);

src/solvers/flattening/boolbv.cpp

@@ -29,15 +29,13 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/floatbv/float_utils.h>
 #include <solvers/lowering/expr_lowering.h>
 
-bool boolbvt::literal(
-  const exprt &expr,
-  const std::size_t bit,
-  literalt &dest) const
+optionalt<literalt>
+boolbvt::literal(const exprt &expr, const std::size_t bit) const
 {
   if(expr.type().id()==ID_bool)
   {
     assert(bit==0);
-    return prop_conv_solvert::literal(expr, dest);
+    return prop_conv_solvert::literal(expr);
   }
   else
   {
@@ -50,16 +48,15 @@ bool boolbvt::literal(
         map.mapping.find(identifier);
 
       if(it_m==map.mapping.end())
-        return true;
+        return {};
 
       const boolbv_mapt::map_entryt &map_entry=it_m->second;
 
       assert(bit<map_entry.literal_map.size());
       if(!map_entry.literal_map[bit].is_set)
-        return true;
+        return {};
 
-      dest=map_entry.literal_map[bit].l;
-      return false;
+      return map_entry.literal_map[bit].l;
     }
     else if(expr.id()==ID_index)
     {
@@ -76,7 +73,7 @@ bool boolbvt::literal(
 
       std::size_t offset=integer2unsigned(index*element_width);
 
-      return literal(index_expr.array(), bit+offset, dest);
+      return literal(index_expr.array(), bit + offset);
     }
     else if(expr.id()==ID_member)
     {
@@ -96,7 +93,7 @@ bool boolbvt::literal(
         const typet &subtype=it->type();
 
         if(it->get_name()==component_name)
-          return literal(expr.op0(), bit+offset, dest);
+          return literal(expr.op0(), bit + offset);
 
         std::size_t element_width=boolbv_width(subtype);
 
@@ -564,7 +561,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
       return const_literal(true);
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
 
 bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
@@ -605,7 +602,7 @@ void boolbvt::set_to(const exprt &expr, bool 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);
+  baset::set_to(expr, value);
 }
 
 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
@@ -640,17 +637,9 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   if(unbounded_array==unbounded_arrayt::U_ALL)
     return true;
 
-  const exprt &size=to_array_type(type).size();
-
-  mp_integer s;
-  if(to_integer(size, s))
-    return true;
-
-  if(unbounded_array==unbounded_arrayt::U_AUTO)
-    if(s>MAX_FLATTENED_ARRAY_SIZE)
-      return true;
-
-  return false;
+  const auto s = numeric_cast<mp_integer>(to_array_type(type).size());
+  return !s.has_value() || (unbounded_array == unbounded_arrayt::U_AUTO &&
+                            *s > MAX_FLATTENED_ARRAY_SIZE);
 }
 
 void boolbvt::print_assignment(std::ostream &out) const

src/solvers/flattening/boolbv.h

@@ -53,22 +53,19 @@ class boolbvt:public arrayst
 
   void clear_cache() override
   {
-    SUB::clear_cache();
+    baset::clear_cache();
     bv_cache.clear();
   }
 
   void post_process() override
   {
     post_process_quantifiers();
     functions.post_process();
-    SUB::post_process();
+    baset::post_process();
   }
 
   // get literals for variables/expressions, if available
-  virtual bool literal(
-    const exprt &expr,
-    std::size_t bit,
-    literalt &literal) const;
+  virtual optionalt<literalt> literal(const exprt &expr, std::size_t bit) const;
 
   using arrayst::literal;
 
@@ -103,7 +100,7 @@ class boolbvt:public arrayst
   virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
 
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef arrayst SUB;
+  typedef arrayst baset;
 
   void conversion_failed(const exprt &expr, bvt &bv)
   {

src/solvers/flattening/boolbv_add_sub.cpp

@@ -26,39 +26,30 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
      type.id()!=ID_vector)
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(type);
-
+  const std::size_t width = boolbv_width(type);
   if(width==0)
     return conversion_failed(expr);
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "operator "+expr.id_string()+" takes at least one operand";
-
+  INVARIANT(
+    !operands.empty(),
+    "operator " + expr.id_string() + " takes at least one operand");
   const exprt &op0=expr.op0();
   DATA_INVARIANT(
     op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
   bvt bv=convert_bv(op0);
 
-  if(bv.size()!=width)
-    throw "convert_add_sub: unexpected operand 0 width";
-
-  bool subtract=(expr.id()==ID_minus ||
-                 expr.id()=="no-overflow-minus");
-
-  bool no_overflow=(expr.id()=="no-overflow-plus" ||
-                    expr.id()=="no-overflow-minus");
+  const typet arithmetic_type =
+    (type.id() == ID_vector || type.id() == ID_complex)
+      ? ns.follow(type.subtype())
+      : type;
 
-  typet arithmetic_type=
-    (type.id()==ID_vector || type.id()==ID_complex)?
-      ns.follow(type.subtype()):type;
-
-  bv_utilst::representationt rep=
-    (arithmetic_type.id()==ID_signedbv ||
-     arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED:
-                                       bv_utilst::representationt::UNSIGNED;
+  const bv_utilst::representationt rep =
+    (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
+      ? bv_utilst::representationt::SIGNED
+      : bv_utilst::representationt::UNSIGNED;
 
   for(exprt::operandst::const_iterator
       it=operands.begin()+1;
@@ -75,13 +66,12 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     if(type.id()==ID_vector || type.id()==ID_complex)
     {
       const typet &subtype=ns.follow(type.subtype());
+      const std::size_t sub_width = boolbv_width(subtype);
+      INVARIANT(
+        sub_width != 0 && width % sub_width == 0,
+        "convert_add_sub: unexpected vector operand width");
 
-      std::size_t sub_width=boolbv_width(subtype);
-
-      if(sub_width==0 || width%sub_width!=0)
-        throw "convert_add_sub: unexpected vector operand width";
-
-      std::size_t size=width/sub_width;
+      const std::size_t size = width / sub_width;
       bv.resize(width);
 
       for(std::size_t i=0; i<size; i++)

src/solvers/flattening/boolbv_array.cpp

@@ -6,39 +6,30 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
 bvt boolbvt::convert_array(const exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
+  const std::size_t width = boolbv_width(expr.type());
   if(width==0)
     return conversion_failed(expr);
 
   if(expr.type().id()==ID_array)
   {
-    assert(expr.has_operands());
+    INVARIANT(expr.has_operands(), "array should have operands");
     const exprt::operandst &operands=expr.operands();
-    assert(!operands.empty());
-    std::size_t op_width=width/operands.size();
-
+    const std::size_t op_width = width / operands.size();
     bvt bv;
     bv.reserve(width);
 
-    forall_expr(it, operands)
+    for(const exprt &op : operands)
     {
-      const bvt &tmp=convert_bv(*it);
-
-      if(tmp.size()!=op_width)
-        throw "convert_array: unexpected operand width";
-
-      forall_literals(it2, tmp)
-        bv.push_back(*it2);
+      const bvt &tmp = convert_bv(op);
+      CHECK_RETURN(tmp.size() == op_width);
+      bv.insert(bv.end(), tmp.begin(), tmp.end());
     }
 
     return bv;
   }
-
   return conversion_failed(expr);
 }

src/solvers/flattening/boolbv_array_of.cpp

@@ -13,16 +13,11 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 {
-  if(expr.type().id()!=ID_array)
-    throw "array_of must be array-typed";
-
   const array_typet &array_type=to_array_type(expr.type());
-
   if(is_unbounded_array(array_type))
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(array_type);
-
+  const std::size_t width = boolbv_width(array_type);
   if(width==0)
   {
     // A zero-length array is acceptable;
@@ -34,29 +29,25 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   }
 
   const exprt &array_size=array_type.size();
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  mp_integer size;
-
-  if(to_integer(array_size, size))
+  if(!size)
     return conversion_failed(expr);
 
   const bvt &tmp=convert_bv(expr.op0());
 
   bvt bv;
   bv.resize(width);
-
-  if(size*tmp.size()!=width)
-    throw "convert_array_of: unexpected operand width";
+  CHECK_RETURN(*size * tmp.size() == width);
 
   std::size_t offset=0;
-
   for(mp_integer i=0; i<size; i=i+1)
   {
     for(std::size_t j=0; j<tmp.size(); j++, offset++)
       bv[offset]=tmp[j];
   }
 
-  assert(offset==bv.size());
+  INVARIANT(offset == bv.size(), "final offset should correspond to size");
 
   return bv;
 }

src/solvers/flattening/boolbv_bv_rel.cpp

@@ -46,7 +46,7 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
         else if(rel==ID_gt)
           return float_utils.relation(bv0, float_utilst::relt::GT, bv1);
         else
-          return SUB::convert_rest(expr);
+          return baset::convert_rest(expr);
       }
       else if((op0.type().id()==ID_range &&
                op1.type()==op0.type()) ||
@@ -109,5 +109,5 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }

src/solvers/flattening/boolbv_extractbit.cpp

@@ -50,7 +50,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     std::size_t width_op1=boolbv_width(operands[1].type());
 
     if(width_op0==0 || width_op1==0)
-      return SUB::convert_rest(expr);
+      return baset::convert_rest(expr);
 
     std::size_t index_width = std::max(address_bits(width_op0), width_op1);
     unsignedbv_typet index_type(index_width);
@@ -90,5 +90,5 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }

src/solvers/flattening/boolbv_get.cpp

@@ -62,7 +62,7 @@ exprt boolbvt::get(const exprt &expr) const
     }
   }
 
-  return SUB::get(expr);
+  return baset::get(expr);
 }
 
 exprt boolbvt::bv_get_rec(