SMV: set type

This fixes typechecking for set literals, assignments from set literals to
variables of the element type, and typechecking for the "in" set membership
operator.

Author: kroening

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

@@ -902,6 +902,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/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);

src/smvlang/smv_typecheck.cpp

@@ -1232,6 +1232,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "signed operand must have unsigned word type";
     }
   }
+  else if(expr.id() == ID_smv_set)
+  {
+    // a set literal
+    expr.type() = typet{ID_smv_set};
+  }
   else
   {
     throw errort().with_location(expr.find_source_location())