Merge pull request #987 from diffblue/smv_ranget_cleanup

SMV: cleanup `smv_ranget`

Author: kroening

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,16 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "smv_range.h"
+
+#include <ostream>
+
+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:
@@ -41,11 +43,14 @@ class smv_ranget
     mp_max(to, other.to);
   }
 
-  void to_type(typet &dest) const
+  typet to_type() const
   {
-    dest = typet(ID_range);
-    dest.set(ID_from, integer2string(from));
-    dest.set(ID_to, integer2string(to));
+    return range_typet{from, to};
+  }
+
+  static smv_ranget from_type(const range_typet &src)
+  {
+    return {src.get_from(), src.get_to()};
   }
 
   bool is_bool() const
@@ -58,32 +63,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

src/smvlang/smv_typecheck.cpp

@@ -472,14 +472,10 @@ smv_ranget smv_typecheckt::convert_type(const typet &src)
   }
   else if(src.id()==ID_range)
   {
-    auto from = string2integer(src.get_string(ID_from));
-    auto to = string2integer(src.get_string(ID_to));
+    dest = smv_ranget::from_type(to_range_type(src));
 
-    if(from > to)
+    if(dest.from > dest.to)
       throw errort().with_location(src.source_location()) << "range is empty";
-
-    dest.from = from;
-    dest.to = to;
   }
   else if(src.id()==ID_enumeration)
   {
@@ -548,9 +544,7 @@ typet smv_typecheckt::type_union(
   }
   else
   {
-    typet tmp;
-    range1.to_type(tmp);
-    return tmp;
+    return range1.to_type();
   }
 }
 
@@ -744,7 +738,7 @@ void smv_typecheckt::typecheck_expr_rec(
         else
           assert(false);
 
-        new_range.to_type(expr.type());
+        expr.type() = new_range.to_type();
       }
     }
     else if(dest_type.id() != ID_range)
@@ -762,9 +756,7 @@ void smv_typecheckt::typecheck_expr_rec(
 
       if(dest_type.is_nil())
       {
-        expr.type()=typet(ID_range);
-        expr.type().set(ID_from, integer2string(int_value));
-        expr.type().set(ID_to, integer2string(int_value));
+        expr.type() = range_typet{int_value, int_value};
       }
       else
       {