Merge pull request #1175 from diffblue/smv-set

SMV: set type

Author: kroening

regression/smv/expressions/smv_set2.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE broken-smt-backend
 smv_set2.smv
---bdd
-^\[spec1\] x in my_set: PROVED$
-^EXIT=0$
+
+^\[spec1\] x in \{ 1, 2 \}: REFUTED$
+^\[spec2\] x in 1 \| x in 2: REFUTED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The smv_setin operator is not implemented.

regression/smv/expressions/smv_set2.smv

@@ -1,9 +1,10 @@
 MODULE main
 
-DEFINE my_set := {1, 2};
-
 VAR x : 1..3;
 ASSIGN init(x) := {1, 2, 3};
        next(x) := x;
 
-SPEC x in my_set;
+SPEC x in {1, 2};
+
+-- the rhs set can be a singleton
+SPEC (x in 1) | (x in 2);

regression/smv/expressions/smv_set3.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_set3.smv
+--bdd
+^\[spec1\] x in my_set: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The smv_setin operator does not work with symbols on the RHS.

src/hw_cbmc_irep_ids.h

@@ -23,6 +23,7 @@ IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_resize)
+IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)

src/smvlang/expr2smv.cpp

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
-Function: expr2smvt::convert_nondet_choice
+Function: expr2smvt::convert_smv_set
 
   Inputs:
 
@@ -25,7 +25,7 @@ Function: expr2smvt::convert_nondet_choice
 
 \*******************************************************************/
 
-expr2smvt::resultt expr2smvt::convert_nondet_choice(const exprt &src)
+expr2smvt::resultt expr2smvt::convert_smv_set(const exprt &src)
 {
   std::string dest = "{ ";
 
@@ -656,6 +656,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id() == ID_mod)
     return convert_binary(to_mod_expr(src), src.id_string(), precedencet::MULT);
 
+  else if(src.id() == ID_smv_set)
+    return convert_smv_set(src);
+
   else if(src.id() == ID_smv_setin)
     return convert_binary(to_binary_expr(src), "in", precedencet::IN);
 
@@ -788,19 +791,13 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id()==ID_constant)
     return convert_constant(to_constant_expr(src));
 
-  else if(src.id()=="smv_nondet_choice")
-    return convert_nondet_choice(src);
-
-  else if(src.id() == ID_constraint_select_one)
-    return convert_nondet_choice(src);
-
   else if(src.id()==ID_nondet_bool)
   {
-    exprt nondet_choice_expr("smv_nondet_choice");
-    nondet_choice_expr.operands().clear();
-    nondet_choice_expr.operands().push_back(false_exprt());
-    nondet_choice_expr.operands().push_back(true_exprt());
-    return convert_nondet_choice(nondet_choice_expr);
+    exprt smv_set_expr(ID_smv_set);
+    smv_set_expr.operands().clear();
+    smv_set_expr.operands().push_back(false_exprt());
+    smv_set_expr.operands().push_back(true_exprt());
+    return convert_smv_set(smv_set_expr);
   }
 
   else if(src.id()==ID_cond)
@@ -902,6 +899,10 @@ std::string type2smv(const typet &type, const namespacet &ns)
   {
     return type.get_string(ID_from) + ".." + type.get_string(ID_to);
   }
+  else if(type.id() == ID_smv_set)
+  {
+    return "set";
+  }
   else if(type.id()=="submodule")
   {
     auto code = type.get_string(ID_identifier);

src/smvlang/expr2smv_class.h

@@ -85,7 +85,7 @@ class expr2smvt
 
   virtual resultt convert_rec(const exprt &);
 
-  resultt convert_nondet_choice(const exprt &);
+  resultt convert_smv_set(const exprt &);
 
   resultt convert_binary(
     const binary_exprt &src,

src/smvlang/parser.y

@@ -176,7 +176,6 @@ static void new_module(YYSTYPE &module)
 %token LTLWFF_Token	"LTLWFF"
 %token PSLWFF_Token	"PSLWFF"
 %token COMPWFF_Token	"COMPWFF"
-%token IN_Token		"IN"
 %token MIN_Token	"MIN"
 %token MAX_Token	"MAX"
 %token MIRROR_Token	"MIRROR"
@@ -289,7 +288,7 @@ static void new_module(YYSTYPE &module)
 %left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token H_Token O_Token S_Token T_Token X_Token Y_Token Z_Token EBF_Token ABF_Token EBG_Token ABG_Token
 %left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
 %left  union_Token
-%left  IN_Token NOTIN_Token
+%left  in_Token
 %left  mod_Token /* Precedence from CMU SMV, different from NuSMV */
 %left  LTLT_Token GTGT_Token
 %left  PLUS_Token MINUS_Token
@@ -673,7 +672,7 @@ formula    : term
 term       : variable_identifier
            | next_Token '(' term ')'  { init($$, ID_smv_next); mto($$, $3); }
            | '(' formula ')'          { $$=$2; }
-           | '{' formula_list '}'     { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
+           | '{' formula_list '}'     { $$=$2; stack_expr($$).id(ID_smv_set); }
            | INC_Token '(' term ')'   { init($$, "inc"); mto($$, $3); }
            | DEC_Token '(' term ')'   { init($$, "dec"); mto($$, $3); }
            | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
@@ -709,8 +708,7 @@ term       : variable_identifier
            | term GT_Token       term { binary($$, $1, ID_gt, $3); }
            | term GE_Token       term { binary($$, $1, ID_ge, $3); }
            | term union_Token    term { binary($$, $1, ID_smv_union, $3); }
-           | term IN_Token       term { binary($$, $1, ID_smv_setin, $3); }
-           | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3); }
+           | term in_Token       term { binary($$, $1, ID_smv_setin, $3); }
            | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
            | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
            | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }

src/smvlang/scanner.l

@@ -101,7 +101,6 @@ void newlocation(YYSTYPE &x)
 "LTLWFF"	token(LTLWFF_Token);
 "PSLWFF"	token(PSLWFF_Token);
 "COMPWFF"	token(COMPWFF_Token);
-"IN"		token(IN_Token);
 "MIN"		token(MIN_Token);
 "MAX"		token(MAX_Token);
 "MIRROR"	token(MIRROR_Token);