SMV: remove vars member in parse tree

The variables are now stored as items, in the order in the source file, and
this auxiliary member is no longer needed.

Author: kroening

src/smvlang/parser.y

@@ -553,18 +553,6 @@ ltl_specification:
            ;
 
 extern_var : variable_identifier EQUAL_Token STRING_Token
-           {
-             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
-             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-
-             if(var.identifier!=irep_idt())
-             {
-               yyerror("variable `"+id2string(identifier)+"' already declared extern");
-               YYERROR;
-             }
-             else
-               var.identifier=stack_expr($3).id_string();
-           }
            ;
 
 var_list   : var_decl
@@ -574,8 +562,6 @@ var_list   : var_decl
 module_parameter: identifier
            {
              const irep_idt &identifier=stack_expr($1).id();
-             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-             var.var_class=smv_parse_treet::mc_vart::ARGUMENT;
              PARSER.module->parameters.push_back(identifier);
            }
            ;
@@ -684,9 +670,6 @@ enum_element: IDENTIFIER_Token
 
 var_decl   : variable_identifier ':' type_specifier ';'
            {
-             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
-             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-             (void)var;
              PARSER.module->add_var(stack_expr($1), stack_type($3));
            }
            ;
@@ -708,9 +691,6 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
            }
            | assignment_var BECOMES_Token formula ';'
            {
-             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
-             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-             (void)var;
              PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
@@ -729,9 +709,6 @@ defines:     define
 
 define     : assignment_var BECOMES_Token formula ';'
            {
-             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
-             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-             (void)var;
              PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
@@ -939,7 +916,6 @@ variable_identifier: complex_identifier
 
              init($$, ID_smv_identifier);
              stack_expr($$).set(ID_identifier, id);
-             PARSER.module->vars[id];
            }
            ;
 

src/smvlang/smv_parse_tree.h

@@ -18,20 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 class smv_parse_treet
 {
 public:
-
-  struct mc_vart
-  {
-    typedef enum { UNKNOWN, DECLARED, DEFINED, ARGUMENT } var_classt;
-    var_classt var_class;
-    typet type;
-    irep_idt identifier;
-    
-    mc_vart():var_class(UNKNOWN), type(typet(ID_bool))
-    {
-    }
-  };
-   
-  typedef std::unordered_map<irep_idt, mc_vart, irep_id_hash> mc_varst;
   typedef std::unordered_set<irep_idt, irep_id_hash> enum_sett;
 
   struct modulet
@@ -286,7 +272,6 @@ class smv_parse_treet
       items.emplace_back(itemt::ENUM, std::move(expr), std::move(location));
     }
 
-    mc_varst vars;
     enum_sett enum_set;
   };