Use invariant instead of printing error message to cerr

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,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
-
 #include <util/std_expr.h>
 #include <util/base_type.h>
 #include <util/invariant.h>
@@ -44,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())
   {
@@ -80,14 +76,12 @@ literalt boolbvt::convert_verilog_case_equality(
   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);