Merge pull request #2950 from danpoe/refactor/error-handling-solvers-prop

Error handling cleanup in solvers/prop

Author: danpoe

src/solvers/prop/bdd_expr.cpp

@@ -11,15 +11,16 @@ Author: Michael Tautschnig, [email protected]
 
 #include "bdd_expr.h"
 
-#include <util/std_expr.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
+#include <util/invariant.h>
+#include <util/std_expr.h>
 
 #include <sstream>
 
 mini_bddt bdd_exprt::from_expr_rec(const exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
+  PRECONDITION(expr.type().id() == ID_bool);
 
   if(expr.is_constant())
     return expr.is_false() ? bdd_mgr.False() : bdd_mgr.True();
@@ -29,7 +30,9 @@ mini_bddt bdd_exprt::from_expr_rec(const exprt &expr)
           expr.id()==ID_or ||
           expr.id()==ID_xor)
   {
-    assert(expr.operands().size()>=2);
+    DATA_INVARIANT(
+      expr.operands().size() >= 2,
+      "logical and, or, and xor expressions have at least two operands");
     exprt bin_expr=make_binary(expr);
 
     mini_bddt op0=from_expr_rec(bin_expr.op0());
@@ -103,7 +106,7 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const
   }
 
   node_mapt::const_iterator entry=node_map.find(r.var());
-  assert(entry!=node_map.end());
+  CHECK_RETURN(entry != node_map.end());
   const exprt &n_expr=entry->second;
 
   if(r.low().is_false())

src/solvers/prop/literal_expr.h

@@ -48,7 +48,9 @@ class literal_exprt:public predicate_exprt
 */
 inline const literal_exprt &to_literal_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_literal && !expr.has_operands());
+  PRECONDITION(expr.id() == ID_literal);
+  DATA_INVARIANT(
+    !expr.has_operands(), "literal expression should not have operands");
   return static_cast<const literal_exprt &>(expr);
 }
 
@@ -57,7 +59,9 @@ inline const literal_exprt &to_literal_expr(const exprt &expr)
 */
 inline literal_exprt &to_literal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_literal && !expr.has_operands());
+  PRECONDITION(expr.id() == ID_literal);
+  DATA_INVARIANT(
+    !expr.has_operands(), "literal expression should not have operands");
   return static_cast<literal_exprt &>(expr);
 }
 

src/solvers/prop/minimize.cpp

@@ -93,7 +93,7 @@ literalt prop_minimizet::constraint()
 void prop_minimizet::operator()()
 {
   // we need to use assumptions
-  assert(prop_conv.has_set_assumptions());
+  PRECONDITION(prop_conv.has_set_assumptions());
 
   _iterations=0;
   _number_satisfied=0;

src/solvers/prop/prop_conv.cpp

@@ -35,7 +35,7 @@ void prop_convt::set_frozen(const bvt &bv)
 
 bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
 {
-  assert(expr.type().id()==ID_bool);
+  PRECONDITION(expr.type().id() == ID_bool);
 
   const irep_idt &identifier = expr.get_identifier();
 
@@ -197,10 +197,13 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   {
     if(expr.is_true())
       return const_literal(true);
-    else if(expr.is_false())
-      return const_literal(false);
     else
-      throw "unknown boolean constant: "+expr.pretty();
+    {
+      INVARIANT(
+        expr.is_false(),
+        "constant expression of type bool should be either true or false");
+      return const_literal(false);
+    }
   }
   else if(expr.id()==ID_symbol)
   {
@@ -216,22 +219,23 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   }
   else if(expr.id()==ID_implies)
   {
-    if(op.size()!=2)
-      throw "implication takes two operands";
-
-    return prop.limplies(convert(op[0]), convert(op[1]));
+    const implies_exprt &implies_expr = to_implies_expr(expr);
+    return prop.limplies(
+      convert(implies_expr.op0()), convert(implies_expr.op1()));
   }
   else if(expr.id()==ID_if)
   {
-    if(op.size()!=3)
-      throw "if takes three operands";
-
-    return prop.lselect(convert(op[0]), convert(op[1]), convert(op[2]));
+    const if_exprt &if_expr = to_if_expr(expr);
+    return prop.lselect(
+      convert(if_expr.cond()),
+      convert(if_expr.true_case()),
+      convert(if_expr.false_case()));
   }
   else if(expr.id()==ID_constraint_select_one)
   {
-    if(op.size()<2)
-      throw "constraint_select_one takes at least two operands";
+    DATA_INVARIANT(
+      op.size() >= 2,
+      "constraint_select_one should have at least two operands");
 
     std::vector<literalt> op_bv;
     op_bv.resize(op.size());
@@ -427,9 +431,10 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
         // set_to_false
         if(expr.id()==ID_implies) // !(a=>b)  ==  (a && !b)
         {
-          assert(expr.operands().size()==2);
-          set_to_true(expr.op0());
-          set_to_false(expr.op1());
+          const implies_exprt &implies_expr = to_implies_expr(expr);
+
+          set_to_true(implies_expr.op0());
+          set_to_false(implies_expr.op1());
           return;
         }
         else if(expr.id()==ID_or) // !(a || b)  ==  (!a && !b)