Merge pull request #706 from diffblue/smv_set1

SMV: IDs and test for set operators

Author: kroening

regression/ebmc/smv/smv_set1.desc

@@ -0,0 +1,8 @@
+CORE
+smv_set1.smv
+--bdd
+^\[.*\] x != 3: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_set1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x : 1..3;
+ASSIGN init(x) := {1, 2};
+       next(x) := x;
+
+SPEC x != 3;

src/hw_cbmc_irep_ids.h

@@ -17,6 +17,9 @@ IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
+IREP_ID_ONE(smv_setin)
+IREP_ID_ONE(smv_setnotin)
+IREP_ID_ONE(smv_union)
 IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)

src/smvlang/expr2smv.cpp

@@ -464,6 +464,15 @@ bool expr2smvt::convert(
     return convert_binary(
       src, dest, src.id_string(), precedence = precedencet::MULT);
 
+  else if(src.id() == ID_smv_setin)
+    return convert_binary(src, dest, "in", precedence = precedencet::IN);
+
+  else if(src.id() == ID_smv_setnotin)
+    return convert_binary(src, dest, "notin", precedence = precedencet::IN);
+
+  else if(src.id() == ID_smv_union)
+    return convert_binary(src, dest, "union", precedence = precedencet::UNION);
+
   else if(src.id()==ID_lt || src.id()==ID_gt ||
           src.id()==ID_le || src.id()==ID_ge)
     return convert_binary(
@@ -528,6 +537,9 @@ bool expr2smvt::convert(
   else if(src.id()=="smv_nondet_choice")
     return convert_nondet_choice(src, dest, precedence);
 
+  else if(src.id() == ID_constraint_select_one)
+    return convert_nondet_choice(src, dest, precedence);
+
   else if(src.id()==ID_nondet_bool)
   {
     exprt nondet_choice_expr("smv_nondet_choice");

src/smvlang/parser.y

@@ -482,9 +482,9 @@ term       : variable_name
            | term LE_Token       term { binary($$, $1, ID_le, $3, bool_typet{}); }
            | term GT_Token       term { binary($$, $1, ID_gt,  $3, bool_typet{}); }
            | term GE_Token       term { binary($$, $1, ID_ge, $3, bool_typet{}); }
-           | term UNION_Token    term { binary($$, $1, "smv_union", $3, bool_typet{}); }
-           | term IN_Token       term { binary($$, $1, "smv_setin", $3, bool_typet{}); }
-           | term NOTIN_Token    term { binary($$, $1, "smv_setnotin", $3, bool_typet{}); }
+           | term UNION_Token    term { binary($$, $1, ID_smv_union, $3, bool_typet{}); }
+           | term IN_Token       term { binary($$, $1, ID_smv_setin, $3, bool_typet{}); }
+           | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3, bool_typet{}); }
            ;
 
 formula_list: formula { init($$); mto($$, $1); }

src/smvlang/smv_typecheck.cpp

@@ -989,11 +989,11 @@ void smv_typecheckt::typecheck(
   else if(expr.id()==ID_typecast)
   {
   }
-  else if(expr.id()=="smv_setin")
+  else if(expr.id() == ID_smv_setin)
   {
     expr.type()=bool_typet();
   }
-  else if(expr.id()=="smv_setnotin")
+  else if(expr.id() == ID_smv_setnotin)
   {
     expr.type()=bool_typet();
   }