SMV: enums are global

SMV's enum name space is global, i.e., crosses modules.

This moves the resolution of identifier to variables or enums from the
parser to the typechecking phase.

Author: kroening

src/smvlang/parser.y

@@ -676,7 +676,7 @@ enum_list  : enum_element
 enum_element: IDENTIFIER_Token
            {
              $$=$1;
-             PARSER.module->enum_set.insert(stack_expr($1).id_string());
+             PARSER.parse_tree.enum_set.insert(stack_expr($1).id_string());
 
              exprt expr(ID_smv_identifier);
              expr.set(ID_identifier, stack_expr($1).id());
@@ -951,6 +951,7 @@ identifier : IDENTIFIER_Token
 
 variable_identifier: complex_identifier
            {
+             // Could be a variable, or an enum
              auto id = merge_complex_identifier(stack_expr($1));
              init($$, ID_smv_identifier);
              stack_expr($$).set(ID_identifier, id);

src/smvlang/smv_parse_tree.h

@@ -274,11 +274,13 @@ class smv_parse_treet
     }
 
     mc_varst vars;
-    enum_sett enum_set;
 
     std::list<irep_idt> ports;
   };
-   
+
+  // enums are global
+  enum_sett enum_set;
+
   typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;
 
   modulest modules;

src/smvlang/smv_typecheck.cpp

@@ -1709,7 +1709,8 @@ void smv_typecheckt::convert(exprt &expr)
       identifier.find("::") == std::string::npos, "conversion is done once");
 
     // enum or variable?
-    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    if(
+      smv_parse_tree.enum_set.find(identifier) == smv_parse_tree.enum_set.end())
     {
       std::string id = module + "::var::" + identifier;