remove dependency on string_refinement_invariantt

The refinement solver a part of the string solver, but can live on its own,
and thus, shouldn't use its exception class.

Author: Daniel Kroening

src/solvers/refinement/refine_arithmetic.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/arith_tools.h>
 
-#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/floatbv/float_utils.h>
 
 // Parameters
@@ -167,10 +166,7 @@ void bv_refinementt::check_SAT(approximationt &a)
 
   if(type.id()==ID_floatbv)
   {
-    // these are all ternary
-    INVARIANT(
-      a.expr.operands().size()==3,
-      string_refinement_invariantt("all floatbv typed exprs are ternary"));
+    const auto &float_op = to_ieee_float_op_expr(a.expr);
 
     if(a.over_state==MAX_STATE)
       return;
@@ -182,7 +178,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     o1.unpack(a.op1_value);
 
     // get actual rounding mode
-    exprt rounding_mode_expr = get(a.expr.op2());
+    exprt rounding_mode_expr = get(float_op.rounding_mode());
     const std::size_t rounding_mode_int =
       numeric_cast_v<std::size_t>(rounding_mode_expr);
     ieee_floatt::rounding_modet rounding_mode =
@@ -279,8 +275,7 @@ void bv_refinementt::check_SAT(approximationt &a)
   {
     // these are all binary
     INVARIANT(
-      a.expr.operands().size()==2,
-      string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
+      a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
 
     // already full interpretation?
     if(a.over_state>0)

src/solvers/refinement/refine_arrays.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/find_symbols.h>
 
-#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/sat/satcheck.h>
 
 /// generate array constraints
@@ -55,9 +54,6 @@ void bv_refinementt::arrays_overapproximated()
     if(current.id()==ID_implies)
     {
       implies_exprt imp=to_implies_expr(current);
-      DATA_INVARIANT(
-        imp.operands().size()==2,
-        string_refinement_invariantt("implies must have two operands"));
       exprt implies_simplified=get(imp.op0());
       if(implies_simplified==false_exprt())
       {
@@ -70,8 +66,7 @@ void bv_refinementt::arrays_overapproximated()
     {
       or_exprt orexp=to_or_expr(current);
       INVARIANT(
-        orexp.operands().size()==2,
-        string_refinement_invariantt("only treats the case of a binary or"));
+        orexp.operands().size() == 2, "only treats the case of a binary or");
       exprt o1=get(orexp.op0());
       exprt o2=get(orexp.op1());
       if(o1==true_exprt() || o2 == true_exprt())
@@ -95,10 +90,7 @@ void bv_refinementt::arrays_overapproximated()
       lazy_array_constraints.erase(it++);
       break;
     default:
-      INVARIANT(
-        false,
-        string_refinement_invariantt("error in array over approximation "
-          "check"));
+      INVARIANT(false, "error in array over approximation check");
     }
   }