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

@@ -685,7 +685,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());
@@ -942,6 +942,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.cpp

@@ -23,6 +23,7 @@ Function: smv_parse_treet::swap
 void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
 {
   smv_parse_tree.modules.swap(modules);
+  smv_parse_tree.enum_set.swap(enum_set);
 }
 
 /*******************************************************************\

src/smvlang/smv_parse_tree.h

@@ -287,9 +287,11 @@ class smv_parse_treet
     }
 
     mc_varst vars;
-    enum_sett enum_set;
   };
-   
+
+  // 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

@@ -1895,7 +1895,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;