SMT2: implement unary minus on ranges

This implements unary minus on the range type in the SMT2 backend.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1320,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)

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));

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);