Replace cout/cerr in solvers

src/cpp/cpp_typecheck_expr.cpp

@@ -11,7 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
-#include <cstdlib>
+#ifdef DEBUG
+#include <iostream>
+#endif
 
 #include <util/pointer_offset_size.h>
 #include <util/std_types.h>
@@ -20,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
 
 #include <util/c_types.h>
 #include <ansi-c/c_qualifiers.h>
@@ -69,25 +72,27 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr)
     typecheck_expr_explicit_constructor_call(expr);
   else if(expr.is_nil())
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got nil\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_code)
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got code\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_symbol)
   {
-    #if 0
-    std::cout << "E: " << expr.pretty() << '\n';
+    // ignore here
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got symbol\n";
-    abort();
-    #endif
+#endif
   }
   else if(expr.id()=="__is_base_of")
   {

src/goto-symex/goto_symex_state.cpp

@@ -50,12 +50,9 @@ void goto_symex_statet::level0t::operator()(
     return;
 
   const symbolt *s;
-
-  if(ns.lookup(obj_identifier, s))
-  {
-    std::cerr << "level0: failed to find " << obj_identifier << '\n';
-    abort();
-  }
+  const bool found_l0 = !ns.lookup(obj_identifier, s);
+  DATA_INVARIANT(
+    found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||

src/solvers/flattening/boolbv_add_sub.cpp

@@ -8,8 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 #include "../floatbv/float_utils.h"
@@ -38,12 +37,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     throw "operator "+expr.id_string()+" takes at least one operand";
 
   const exprt &op0=expr.op0();
-
-  if(op0.type()!=type)
-  {
-    std::cerr << expr.pretty() << '\n';
-    throw "add/sub with mixed types";
-  }
+  DATA_INVARIANT(
+    op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
   bvt bv=convert_bv(op0);
 
@@ -69,11 +64,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
       it=operands.begin()+1;
       it!=operands.end(); it++)
   {
-    if(it->type()!=type)
-    {
-      std::cerr << expr.pretty() << '\n';
-      throw "add/sub with mixed types";
-    }
+    DATA_INVARIANT(
+      it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
     const bvt &op=convert_bv(*it);
 

src/solvers/flattening/boolbv_case.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
+#include <util/invariant.h>
 
 bvt boolbvt::convert_case(const exprt &expr)
 {
@@ -49,15 +49,11 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     case COMPARE:
-      if(compare_bv.size()!=op.size())
-      {
-        std::cerr << "compare operand: " << compare_bv.size()
-                  << "\noperand: " << op.size() << '\n'
-                  << it->pretty()
-                  << '\n';
-
-        throw "size of compare operand does not match";
-      }
+      DATA_INVARIANT(
+        compare_bv.size() == op.size(),
+        std::string("size of compare operand does not match:\n") +
+          "compare operand: " + std::to_string(compare_bv.size()) +
+          "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
       compare_literal=bv_utils.equal(compare_bv, op);
       compare_literal=prop.land(!previous_compare, compare_literal);
@@ -68,15 +64,11 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     case VALUE:
-      if(bv.size()!=op.size())
-      {
-        std::cerr << "result size: " << bv.size()
-                  << "\noperand: " << op.size() << '\n'
-                  << it->pretty()
-                  << '\n';
-
-        throw "size of value operand does not match";
-      }
+      DATA_INVARIANT(
+        bv.size() == op.size(),
+        std::string("size of value operand does not match:\n") +
+          "result size: " + std::to_string(bv.size()) +
+          "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
       {
         literalt value_literal=bv_utils.equal(bv, op);

src/solvers/flattening/boolbv_cond.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
+#include <util/invariant.h>
 
 bvt boolbvt::convert_cond(const exprt &expr)
 {
@@ -51,15 +51,11 @@ bvt boolbvt::convert_cond(const exprt &expr)
       {
         const bvt &op=convert_bv(*it);
 
-        if(bv.size()!=op.size())
-        {
-          std::cerr << "result size: " << bv.size()
-                    << "\noperand: " << op.size() << '\n'
-                    << it->pretty()
-                    << '\n';
-
-          throw "size of value operand does not match";
-        }
+        DATA_INVARIANT(
+          bv.size() == op.size(),
+          std::string("size of value operand does not match:\n") +
+            "result size: " + std::to_string(bv.size()) +
+            "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
         literalt value_literal=bv_utils.equal(bv, op);
 

src/solvers/flattening/boolbv_equality.cpp

@@ -8,23 +8,22 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
-
 #include <util/std_expr.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
 
 #include <langapi/language_util.h>
 
 #include "flatten_byte_operators.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
-  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
-  {
-    std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
-    std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
-    throw "equality without matching types";
-  }
+  const bool is_base_type_eq =
+    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
+  DATA_INVARIANT(
+    is_base_type_eq,
+    std::string("equality without matching types:\n") + "######### lhs: " +
+      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty());
 
   // see if it is an unbounded array
   if(is_unbounded_array(expr.lhs().type()))
@@ -43,14 +42,12 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
   const bvt &bv0=convert_bv(expr.lhs());
   const bvt &bv1=convert_bv(expr.rhs());
 
-  if(bv0.size()!=bv1.size())
-  {
-    std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
-    std::cerr << "lhs size: " << bv0.size() << '\n';
-    std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
-    std::cerr << "rhs size: " << bv1.size() << '\n';
-    throw "unexpected size mismatch on equality";
-  }
+  DATA_INVARIANT(
+    bv0.size() == bv1.size(),
+    std::string("unexpected size mismatch on equality:\n") + "lhs: " +
+      expr.lhs().pretty() + '\n' + "lhs size: " + std::to_string(bv0.size()) +
+      '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
+      "rhs size: " + std::to_string(bv1.size()));
 
   if(bv0.empty())
   {
@@ -68,24 +65,23 @@ literalt boolbvt::convert_verilog_case_equality(
   // This is 4-valued comparison, i.e., z===z, x===x etc.
   // The result is always Boolean.
 
-  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
-  {
-    std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
-    std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
-    throw "verilog_case_equality without matching types";
-  }
+  const bool is_base_type_eq =
+    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
+  DATA_INVARIANT(
+    is_base_type_eq,
+    std::string("verilog_case_equality without matching types:\n") +
+      "######### lhs: " + expr.lhs().pretty() + '\n' +
+      "######### rhs: " + expr.rhs().pretty());
 
   const bvt &bv0=convert_bv(expr.lhs());
   const bvt &bv1=convert_bv(expr.rhs());
 
-  if(bv0.size()!=bv1.size())
-  {
-    std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
-    std::cerr << "lhs size: " << bv0.size() << '\n';
-    std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
-    std::cerr << "rhs size: " << bv1.size() << '\n';
-    throw "unexpected size mismatch on verilog_case_equality";
-  }
+  DATA_INVARIANT(
+    bv0.size() == bv1.size(),
+    std::string("unexpected size mismatch on verilog_case_equality:\n") +
+      "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
+      std::to_string(bv0.size()) + '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
+      "rhs size: " + std::to_string(bv1.size()));
 
   if(expr.id()==ID_verilog_case_inequality)
     return !bv_utils.equal(bv0, bv1);

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -88,12 +88,9 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
   bvt bv2=convert_bv(op2);
 
   const typet &type=ns.follow(expr.type());
-
-  if(op0.type()!=type || op1.type()!=type)
-  {
-    std::cerr << expr.pretty() << '\n';
-    throw "float op with mixed types";
-  }
+  DATA_INVARIANT(
+    op0.type() == type && op1.type() == type,
+    "float op with mixed types:\n" + expr.pretty());
 
   float_utilst float_utils(prop);
 

src/solvers/refinement/refine_arithmetic.cpp

@@ -226,8 +226,6 @@ void bv_refinementt::check_SAT(approximationt &a)
               << "==" << integer2binary(result.pack(), spec.width()) << eom;
     #endif
 
-    // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
-
     if(a.over_state<config_.max_node_refinement)
     {
       bvt r;

src/solvers/sat/cnf.cpp

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include "cnf.h"
 
 #include <algorithm>
-#include <cassert>
-#include <iostream>
 #include <set>
 
+#include <util/invariant.h>
+
 // #define VERBOSE
 
 /// Tseitin encoding of conjunction of two literals
@@ -426,22 +426,23 @@ bool cnft::process_clause(const bvt &bv, bvt &dest)
   for(const auto l : bv)
   {
     // we never use index 0
-    assert(l.var_no()!=0);
+    INVARIANT(l.var_no() != 0, "variable 0 must not be used");
 
     // we never use 'unused_var_no'
-    assert(l.var_no()!=literalt::unused_var_no());
+    INVARIANT(
+      l.var_no() != literalt::unused_var_no(),
+      "variable 'unused_var_no' must not be used");
 
     if(l.is_true())
       return true; // clause satisfied
 
     if(l.is_false())
       continue; // will remove later
 
-    if(l.var_no()>=_no_variables)
-      std::cout << "l.var_no()=" << l.var_no()
-                << " _no_variables=" << _no_variables << '\n';
-
-    assert(l.var_no()<_no_variables);
+    INVARIANT(
+      l.var_no() < _no_variables,
+      "unknown variable " + std::to_string(l.var_no()) +
+        " (no_variables = " + std::to_string(_no_variables) + " )");
   }
 
   // now copy