Merge pull request #8537 from diffblue/smt2-range-fix

SMT2: range_type fixes

Author: kroening

Diff for: src/solvers/smt2/smt2_conv.cpp

@@ -517,11 +517,14 @@ constant_exprt smt2_convt::parse_literal(
     std::size_t width=boolbv_width(type);
     return constant_exprt(integer2bvrep(value, width), type);
   }
-  else if(type.id()==ID_integer ||
-          type.id()==ID_range)
+  else if(type.id() == ID_integer)
   {
     return from_integer(value, type);
   }
+  else if(type.id() == ID_range)
+  {
+    return from_integer(value + to_range_type(type).get_from(), type);
+  }
   else
     UNREACHABLE_BECAUSE(
       "smt2_convt::parse_literal should not be of unsupported type " +
@@ -1317,17 +1320,26 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_unary_minus)
   {
     const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
+    const auto &type = expr.type();
 
     if(
-      unary_minus_expr.type().id() == ID_rational ||
-      unary_minus_expr.type().id() == ID_integer ||
-      unary_minus_expr.type().id() == ID_real)
+      type.id() == ID_rational || type.id() == ID_integer ||
+      type.id() == ID_real)
     {
       out << "(- ";
       convert_expr(unary_minus_expr.op());
       out << ")";
     }
-    else if(unary_minus_expr.type().id() == ID_floatbv)
+    else if(type.id() == ID_range)
+    {
+      auto &range_type = to_range_type(type);
+      PRECONDITION(type == unary_minus_expr.op().type());
+      // turn -x into 0-x
+      auto minus_expr =
+        minus_exprt{range_type.zero_expr(), unary_minus_expr.op()};
+      convert_expr(minus_expr);
+    }
+    else if(type.id() == ID_floatbv)
     {
       // this has no rounding mode
       if(use_FPA_theory)
@@ -3764,7 +3776,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
   }
   else if(
     expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
-    expr.type().id() == ID_fixedbv || expr.type().id() == ID_range)
+    expr.type().id() == ID_fixedbv)
   {
     // These could be chained, i.e., need not be binary,
     // but at least MathSat doesn't like that.
@@ -3781,6 +3793,31 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
       convert_plus(to_plus_expr(make_binary(expr)));
     }
   }
+  else if(expr.type().id() == ID_range)
+  {
+    auto &range_type = to_range_type(expr.type());
+
+    // These could be chained, i.e., need not be binary,
+    // but at least MathSat doesn't like that.
+    if(expr.operands().size() == 2)
+    {
+      // add: lhs + from + rhs + from - from = lhs + rhs + from
+      mp_integer from = range_type.get_from();
+      const auto size = range_type.get_to() - range_type.get_from() + 1;
+      const auto width = address_bits(size);
+
+      out << "(bvadd ";
+      convert_expr(expr.op0());
+      out << " (bvadd ";
+      convert_expr(expr.op1());
+      out << " (_ bv" << range_type.get_from() << ' ' << width
+          << ")))"; // bv, bvadd, bvadd
+    }
+    else
+    {
+      convert_plus(to_plus_expr(make_binary(expr)));
+    }
+  }
   else if(expr.type().id() == ID_floatbv)
   {
     // Floating-point additions should have be been converted
@@ -4018,6 +4055,22 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
         "unsupported operand types for -: " + expr.op0().type().id_string() +
         " and " + expr.op1().type().id_string());
   }
+  else if(expr.type().id() == ID_range)
+  {
+    auto &range_type = to_range_type(expr.type());
+
+    // sub: lhs + from - (rhs + from) - from = lhs - rhs - from
+    mp_integer from = range_type.get_from();
+    const auto size = range_type.get_to() - range_type.get_from() + 1;
+    const auto width = address_bits(size);
+
+    out << "(bvsub (bvsub ";
+    convert_expr(expr.op0());
+    out << ' ';
+    convert_expr(expr.op1());
+    out << ") (_ bv" << range_type.get_from() << ' ' << width
+        << "))"; // bv, bvsub
+  }
   else
     UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
 }

Diff for: src/util/std_types.cpp

@@ -165,6 +165,23 @@ void bitvector_typet::width(const mp_integer &width)
   set_width(numeric_cast_v<std::size_t>(width));
 }
 
+bool range_typet::includes(const mp_integer &singleton) const
+{
+  return get_from() <= singleton && singleton <= get_to();
+}
+
+constant_exprt range_typet::one_expr() const
+{
+  PRECONDITION(includes(1));
+  return constant_exprt{ID_1, *this};
+}
+
+constant_exprt range_typet::zero_expr() const
+{
+  PRECONDITION(includes(0));
+  return constant_exprt{ID_0, *this};
+}
+
 void range_typet::set_from(const mp_integer &from)
 {
   set(ID_from, integer2string(from));

Diff for: src/util/std_types.h

@@ -1012,6 +1012,9 @@ class range_typet:public typet
 
   mp_integer get_from() const;
   mp_integer get_to() const;
+  bool includes(const mp_integer &) const;
+  constant_exprt zero_expr() const;
+  constant_exprt one_expr() const;
 
   void set_from(const mp_integer &_from);
   void set_to(const mp_integer &to);