Merge pull request #902 from diffblue/smt-typecheck-cleanup

SMV typechecker cleanup

src/hw_cbmc_irep_ids.h

@@ -17,6 +17,7 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_setin)

src/smvlang/parser.y

@@ -377,10 +377,10 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
            {
              binary($$, $3, ID_equal, $6, bool_typet{});
 
-             if(stack_expr($1).id()=="next")
+             if(stack_expr($1).id()==ID_smv_next)
              {
                exprt &op=to_binary_expr(stack_expr($$)).op0();
-               unary_exprt tmp("smv_next", std::move(op));
+               unary_exprt tmp(ID_smv_next, std::move(op));
                tmp.swap(op);
                PARSER.module->add_trans(stack_expr($$));
              }
@@ -393,7 +393,7 @@ assignment_var: variable_name
            ;
 
 assignment_head: init_Token { init($$, ID_init); }
-               | NEXT_Token { init($$, "next"); }
+               | NEXT_Token { init($$, ID_smv_next); }
                ;
 
 defines:     define
@@ -439,7 +439,7 @@ formula    : term
            ;
 
 term       : variable_name
-           | NEXT_Token '(' term ')'  { init($$, "smv_next"); mto($$, $3); }
+           | NEXT_Token '(' term ')'  { init($$, ID_smv_next); mto($$, $3); }
            | '(' formula ')'          { $$=$2; }
            | '{' formula_list '}'     { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
            | INC_Token '(' term ')'   { init($$, "inc"); mto($$, $3); }

src/smvlang/smv_range.h

@@ -0,0 +1,89 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_RANGE_H
+#define CPROVER_SMV_RANGE_H
+
+#include <util/arith_tools.h>
+
+class smv_ranget
+{
+public:
+  smv_ranget() : from(0), to(0)
+  {
+  }
+
+  smv_ranget(mp_integer _from, mp_integer _to)
+    : from(std::move(_from)), to(std::move(_to))
+  {
+    PRECONDITION(_from <= _to);
+  }
+
+  mp_integer from, to;
+
+  bool is_contained_in(const smv_ranget &other) const
+  {
+    if(other.from > from)
+      return false;
+    if(other.to < to)
+      return false;
+    return true;
+  }
+
+  void make_union(const smv_ranget &other)
+  {
+    mp_min(from, other.from);
+    mp_max(to, other.to);
+  }
+
+  void to_type(typet &dest) const
+  {
+    dest = typet(ID_range);
+    dest.set(ID_from, integer2string(from));
+    dest.set(ID_to, integer2string(to));
+  }
+
+  bool is_bool() const
+  {
+    return from == 0 && to == 1;
+  }
+
+  bool is_singleton() const
+  {
+    return from == to;
+  }
+
+  smv_ranget &operator+(const smv_ranget &other)
+  {
+    from += other.from;
+    to += other.to;
+    return *this;
+  }
+
+  smv_ranget &operator-(const smv_ranget &other)
+  {
+    from -= other.from;
+    to -= other.to;
+    return *this;
+  }
+
+  smv_ranget &operator*(const smv_ranget &other)
+  {
+    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)));
+
+    return *this;
+  }
+};
+
+#endif // CPROVER_SMV_RANGE_H