From 3854199d0253d2fc40963f7e7abc4f72b6ea62b5 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 20 Dec 2024 16:28:54 +0000
Subject: [PATCH] SMV: typechecking for unary minus

---
 regression/ebmc/range_type/range_type8.desc |  2 +-
 src/smvlang/smv_range.h                     |  6 ++++++
 src/smvlang/smv_typecheck.cpp               | 23 +++++++++++++++++++++
 3 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/regression/ebmc/range_type/range_type8.desc b/regression/ebmc/range_type/range_type8.desc
index 8d55f699..5bd3adb6 100644
--- a/regression/ebmc/range_type/range_type8.desc
+++ b/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.
diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h
index 4fec7772..768a34ac 100644
--- a/src/smvlang/smv_range.h
+++ b/src/smvlang/smv_range.h
@@ -84,6 +84,12 @@ class smv_ranget
 
     return *this;
   }
+
+  // unary minus
+  smv_ranget operator-() const
+  {
+    return smv_ranget{-to, -from};
+  }
 };
 
 #endif // CPROVER_SMV_RANGE_H
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 6549716f..b0ec1ff3 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -752,6 +752,29 @@ void smv_typecheckt::typecheck_expr_rec(
         << "Expected number type for " << to_string(expr);
     }
   }
+  else if(expr.id() == ID_unary_minus)
+  {
+    typecheck_op(expr, dest_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(dest_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)