Merge pull request #3038 from hannes-steffenhagen-diffblue/feature-invariant_cleanup-flattening-boolbv_equality

Feature invariant cleanup flattening/boolbv_equality.cpp

Author: tautschnig

src/solvers/flattening/boolbv_equality.cpp

@@ -19,13 +19,11 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
   const bool is_base_type_eq =
     base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
-  if(!is_base_type_eq)
-  {
-    const std::string error_msg =
-      std::string("equality without matching types:\n") + "######### lhs: " +
-      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty();
-    throw bitvector_conversion_exceptiont(error_msg, expr);
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    is_base_type_eq,
+    "types of expressions on each side of equality should match",
+    irep_pretty_diagnosticst{expr.lhs()},
+    irep_pretty_diagnosticst{expr.rhs()});
 
   // see if it is an unbounded array
   if(is_unbounded_array(expr.lhs().type()))
@@ -41,24 +39,25 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
     return record_array_equality(expr);
   }
 
-  const bvt &bv0=convert_bv(expr.lhs());
-  const bvt &bv1=convert_bv(expr.rhs());
+  const bvt &lhs_bv = convert_bv(expr.lhs());
+  const bvt &rhs_bv = convert_bv(expr.rhs());
 
-  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()));
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    lhs_bv.size() == rhs_bv.size(),
+    "sizes of lhs and rhs bitvectors should match",
+    irep_pretty_diagnosticst{expr.lhs()},
+    "lhs size: " + std::to_string(lhs_bv.size()),
+    irep_pretty_diagnosticst{expr.rhs()},
+    "rhs size: " + std::to_string(rhs_bv.size()));
 
-  if(bv0.empty())
+  if(lhs_bv.empty())
   {
     // An empty bit-vector comparison. It's not clear
     // what this is meant to say.
     return prop.new_variable();
   }
 
-  return bv_utils.equal(bv0, bv1);
+  return bv_utils.equal(lhs_bv, rhs_bv);
 }
 
 literalt boolbvt::convert_verilog_case_equality(
@@ -69,24 +68,25 @@ literalt boolbvt::convert_verilog_case_equality(
 
   const bool is_base_type_eq =
     base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
-  DATA_INVARIANT(
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
     is_base_type_eq,
-    std::string("verilog_case_equality without matching types:\n") +
-      "######### lhs: " + expr.lhs().pretty() + '\n' +
-      "######### rhs: " + expr.rhs().pretty());
+    "lhs and rhs types should match in verilog_case_equality",
+    irep_pretty_diagnosticst{expr.lhs()},
+    irep_pretty_diagnosticst{expr.rhs()});
 
-  const bvt &bv0=convert_bv(expr.lhs());
-  const bvt &bv1=convert_bv(expr.rhs());
+  const bvt &lhs_bv = convert_bv(expr.lhs());
+  const bvt &rhs_bv = convert_bv(expr.rhs());
 
-  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()));
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    lhs_bv.size() == rhs_bv.size(),
+    "bitvector arguments to verilog_case_equality should have the same size",
+    irep_pretty_diagnosticst{expr.lhs()},
+    "lhs size: " + std::to_string(lhs_bv.size()),
+    irep_pretty_diagnosticst{expr.rhs()},
+    "rhs size: " + std::to_string(rhs_bv.size()));
 
   if(expr.id()==ID_verilog_case_inequality)
-    return !bv_utils.equal(bv0, bv1);
+    return !bv_utils.equal(lhs_bv, rhs_bv);
   else
-    return bv_utils.equal(bv0, bv1);
+    return bv_utils.equal(lhs_bv, rhs_bv);
 }