SMV: separate type checking and type propagation

This splits up type checking (language semantics) from type propagation (an
optimisation).

regression/smv/boolean/boolean_expected1.desc

@@ -1,7 +1,7 @@
 CORE
 boolean_expected1.smv
 
-^file boolean_expected1\.smv line 3: expected 0 or 1 here, but got 10$
+^file boolean_expected1\.smv line 3: Expected expression of type `boolean', but got expression `10', which is of type `10..10'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/boolean/boolean_expected2.desc

@@ -1,7 +1,7 @@
 CORE
 boolean_expected2.smv
 
-^file boolean_expected2\.smv line 5: expected 0 or 1 here, but got 5$
+^file boolean_expected2\.smv line 5: Expected expression of type `boolean', but got expression `5', which is of type `5..5'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/boolean/boolean_expected3.desc

@@ -1,7 +1,7 @@
 CORE
 boolean_expected3.smv
 
-^file boolean_expected3\.smv line 3: expected 0 or 1 here, but got 3$
+^file boolean_expected3\.smv line 3: Expected expression of type `boolean', but got expression `3', which is of type `3..3'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/boolean/boolean_expected4.desc

@@ -1,7 +1,7 @@
 CORE
 boolean_expected4.smv
 
-^file boolean_expected4\.smv line 6: expected 0 or 1 here, but got 5$
+^file boolean_expected4\.smv line 6: Expected expression of type `boolean', but got expression `5', which is of type `5..5'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

src/smvlang/Makefile

@@ -1,5 +1,11 @@
-SRC = smv_language.cpp smv_parser.cpp smv_typecheck.cpp expr2smv.cpp \
-      smv_y.tab.cpp lex.yy.cpp smv_parse_tree.cpp
+SRC = smv_language.cpp \
+      smv_parser.cpp \
+      smv_typecheck.cpp \
+      expr2smv.cpp \
+      smv_y.tab.cpp \
+      lex.yy.cpp \
+      smv_parse_tree.cpp \
+      smv_range.cpp
 
 include ../config.inc
 include ../common

src/smvlang/smv_range.cpp

@@ -0,0 +1,14 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "smv_range.h"
+
+std::ostream &operator<<(std::ostream &out, const smv_ranget &range)
+{
+  return out << range.from << ".." << range.to;
+}

src/smvlang/smv_range.h

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 
+#include <iosfwd>
+
 class smv_ranget
 {
 public:
@@ -58,32 +60,30 @@ class smv_ranget
     return from == to;
   }
 
-  smv_ranget &operator+(const smv_ranget &other)
+  smv_ranget operator+(const smv_ranget &other) const
   {
-    from += other.from;
-    to += other.to;
-    return *this;
+    return {from + other.from, to + other.to};
   }
 
-  smv_ranget &operator-(const smv_ranget &other)
+  smv_ranget operator-(const smv_ranget &other) const
   {
-    from -= other.from;
-    to -= other.to;
-    return *this;
+    return {from - other.from, to - other.to};
   }
 
-  smv_ranget &operator*(const smv_ranget &other)
+  smv_ranget operator*(const smv_ranget &other) const
   {
     mp_integer p1 = from * other.from;
     mp_integer p2 = from * other.to;
     mp_integer p3 = to * other.from;
     mp_integer p4 = to * other.to;
 
-    from = std::min(p1, std::min(p2, std::min(p3, p4)));
-    to = std::max(p1, std::max(p2, std::max(p3, p4)));
+    mp_integer from = std::min(p1, std::min(p2, std::min(p3, p4)));
+    mp_integer to = std::max(p1, std::max(p2, std::max(p3, p4)));
 
-    return *this;
+    return {std::move(from), std::move(to)};
   }
+
+  friend std::ostream &operator<<(std::ostream &, const smv_ranget &);
 };
 
 #endif // CPROVER_SMV_RANGE_H