SMV: move logic that distinguishes enums and vars to type checker

This moves the logic that distinguishes enums and variables from the parser
to the type checker.

This will enable distinguishing complex identifiers with square brackets
[...] from the index operator.

Author: kroening

src/smvlang/parser.y

@@ -952,32 +952,8 @@ identifier : IDENTIFIER_Token
 variable_identifier: complex_identifier
            {
              auto id = merge_complex_identifier(stack_expr($1));
-
-             bool is_enum=(PARSER.module->enum_set.find(id)!=
-                           PARSER.module->enum_set.end());
-             bool is_var=(PARSER.module->vars.find(id)!=
-                          PARSER.module->vars.end());
-
-             if(is_var && is_enum)
-             {
-               yyerror("identifier `"+id2string(id)+"' is ambiguous");
-               YYERROR;
-             }
-             else if(is_enum)
-             {
-               init($$, ID_constant);
-               stack_expr($$).type()=typet(ID_smv_enumeration);
-               stack_expr($$).set(ID_value, id);
-             }
-             else // not an enum, probably a variable
-             {
-               init($$, ID_smv_identifier);
-               stack_expr($$).set(ID_identifier, id);
-               auto var_it = PARSER.module->vars.find(id);
-               if(var_it!= PARSER.module->vars.end())
-                 stack_expr($$).type()=var_it->second.type;
-               //PARSER.module->vars[stack_expr($1).id()];
-             }
+             init($$, ID_smv_identifier);
+             stack_expr($$).set(ID_identifier, id);
            }
            | STRING_Token
            {

src/smvlang/smv_typecheck.cpp

@@ -1708,10 +1708,21 @@ void smv_typecheckt::convert(exprt &expr)
     DATA_INVARIANT(
       identifier.find("::") == std::string::npos, "conversion is done once");
 
-    std::string id = module + "::var::" + identifier;
+    // enum or variable?
+    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    {
+      std::string id = module + "::var::" + identifier;
 
-    expr.set(ID_identifier, id);
-    expr.id(ID_symbol);
+      expr.set(ID_identifier, id);
+      expr.id(ID_symbol);
+    }
+    else
+    {
+      expr.id(ID_constant);
+      expr.type() = typet(ID_smv_enumeration);
+      expr.set(ID_value, identifier);
+      expr.remove(ID_identifier);
+    }
   }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")