SMV: typechecking for unary minus

Author: kroening

regression/ebmc/range_type/range_type8.desc

@@ -6,4 +6,4 @@ range_type8.smv
 ^SIGNAL=0$
 --
 --
-We do not have type checking for unary minus.
+We do not have solver support for unary minus on ranges.

src/smvlang/smv_typecheck.cpp

@@ -82,7 +82,12 @@ class smv_typecheckt:public typecheckt
     smv_ranget():from(0), to(0)
     {
     }
-  
+
+    smv_ranget(mp_integer _from, mp_integer _to)
+      : from(std::move(_from)), to(std::move(_to))
+    {
+    }
+
     mp_integer from, to;
 
     bool is_contained_in(const smv_ranget &other) const
@@ -141,6 +146,12 @@ class smv_typecheckt:public typecheckt
 
       return *this;
     }
+
+    // unary minus
+    smv_ranget operator-() const
+    {
+      return smv_ranget{-to, -from};
+    }
   };
 
   smv_ranget convert_type(const typet &type);
@@ -822,6 +833,29 @@ void smv_typecheckt::typecheck(
       throw 0;
     }
   }
+  else if(expr.id() == ID_unary_minus)
+  {
+    typecheck_op(expr, type, mode);
+
+    if(expr.operands().size() != 1)
+    {
+      error().source_location = expr.find_source_location();
+      error() << "Expected one operand for " << expr.id() << eom;
+      throw 0;
+    }
+
+    if(type.is_nil())
+    {
+      if(expr.type().id() == ID_range || expr.type().id() == ID_bool)
+      {
+        // find proper type for precise arithmetic
+        smv_ranget smv_range_op =
+          convert_type(to_unary_minus_expr(expr).op().type());
+        smv_ranget new_range = -smv_range_op;
+        new_range.to_type(expr.type());
+      }
+    }
+  }
   else if(expr.id()==ID_constant)
   {
     if(expr.type().id()==ID_integer)