* Rename let-funcs.cpp to LetMgr.cpp

* Move the letMgr into the ParserInterface class. This means it's not in scope until the program exits, instead just during parsing.
* The smt-lib parser makes all its calls into STP via the ParserInterface class.
* Updated the smt-lib parser to use the typing node factory. Explicit calls to BVTypeCheck() are not longer required so have been removed.
* Removed some redundant type checks from the smt-lib parser.
* Updated the cvc parser to use the letmgr in the ParserInterface object.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@662 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index e0b59f0b9ca649048b66ff2795e967cf9140bd34..72d186ea28c44f306e89fc2f1e382a06bc3ac810 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -13,7 +13,7 @@
 #OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
-OPTIMIZE      = -O3               # Maximum optimization
+OPTIMIZE      = -O3 -g               # Maximum optimization
 #CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 

diff --git a/scripts/run_cvc_tests.pl b/scripts/run_cvc_tests.pl
index 366ce0e722c38efe3352a7eedb38d4f0ad576591..db797ee7d8055664828aa9788f8dce4a899d5297 100755 (executable)
--- a/scripts/run_cvc_tests.pl
+++ b/scripts/run_cvc_tests.pl
@@ -78,7 +78,7 @@ my %optionsDefault = ("level" => 4,
                      # Runtime limit; 0 = no limit
                      "time" => 180,
                      # Additional command line options to stp
-                     "stpOptions" => "-d -t");
+                     "stpOptions" => "-d -t ");
 
 # Database of command line options.  Initially, they are undefined
 my %options = ();

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h
index f2f8d0b422cbe5ffef8dd3317496aebc3effd77d..ddbe7639268e4cda65ef86e6e50eda8f6a5ca91c 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.h
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h
@@ -31,7 +31,7 @@ class SimplifyingNodeFactory: public NodeFactory
 {
 
 private:
-       HashingNodeFactory& hashing;
+       NodeFactory& hashing;
        BEEV::STPMgr& bm; // Only here until the const evaluator is pulled out.
 
        const ASTNode& ASTTrue;
@@ -61,7 +61,7 @@ public:
        virtual BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children);
 
 
-       SimplifyingNodeFactory(HashingNodeFactory& raw_, BEEV::STPMgr& bm_)
+       SimplifyingNodeFactory(NodeFactory& raw_, BEEV::STPMgr& bm_)
        :hashing(raw_), bm(bm_), ASTTrue(bm.ASTTrue), ASTFalse(bm.ASTFalse), ASTUndefined(bm.ASTUndefined)
        {
                simplifier = new Simplifier(&bm);

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 8e1f519c8c2803cf5fa0cca0fd17df90efb0cdb4..99470808de34967f70718edffd08b279cc967cbb 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -16,7 +16,7 @@
 #include "../simplifier/bvsolver.h"
 #include "../simplifier/simplifier.h"
 #include "../to-sat/ToSAT.h"
-#include "../parser/let-funcs.h"
+#include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 
 /********************************************************************

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index dc34c200d49e56c0469c0b71559bb5998e7ab5e7..2dd71fcccbe9380729f07442ed546a20a6f08909 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -12,7 +12,6 @@
 
 #include "UserDefinedFlags.h"
 #include "../AST/AST.h"
-#include "../parser/let-funcs.h"
 #include "../AST/NodeFactory/HashingNodeFactory.h"
 
 namespace BEEV
@@ -98,9 +97,6 @@ namespace BEEV
     // The query for the current logical context.
     ASTNode _current_query;    
 
-    // Manager for let variables
-    LETMgr * letmgr;
-    
     // Ptr to class that reports on the running time of various parts
     // of the code
     RunTimes * runTimes;
@@ -190,17 +186,10 @@ namespace BEEV
       ASTFalse     = CreateNode(FALSE);
       ASTTrue      = CreateNode(TRUE); 
       ASTUndefined = CreateNode(UNDEFINED);
-      letmgr       = new LETMgr(ASTUndefined);
       runTimes     = new RunTimes();
       _current_query = ASTUndefined;
       UserFlags.num_absrefine = 2;
     }    
-
-    //Return ptr to let-variables manager (see parser/let-funcs.h)
-    LETMgr * GetLetMgr(void)
-    {
-      return letmgr;
-    }
     
     RunTimes * GetRunTimes(void)
     {
@@ -348,6 +337,7 @@ namespace BEEV
      ****************************************************************/
 
     // For printing purposes
+    // Not filled in by the smtlib parser.
     ASTVec ListOfDeclaredVars;
     
     // Table for DAG printing.
@@ -418,7 +408,6 @@ namespace BEEV
         }
       _asserts.clear();
 
-      delete letmgr;
       delete runTimes;
           
       _interior_unique_table.clear();

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index cd5400fa6e789306358a17f670122197b48954cc..78f7d9d8ad4d7a4c4f7d33aca01ff34dd4e20a02 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -12,6 +12,7 @@
 #include <assert.h>
 #include "fdstream.h"
 #include "../printer/printers.h"
+#include "../parser/ParserInterface.h"
 
 //These typedefs lower the effort of using the keyboard to type (too
 //many overloaded meanings of the word type)
@@ -1760,6 +1761,10 @@ Expr vc_parseExpr(VC vc, const char* infile) {
     return 0;
   }
 
+  BEEV::ParserInterface pi(*b, b->defaultNodeFactory);
+  BEEV::parserInterface = &pi;
+
+
   BEEV::ASTVec * AssertsQuery = new BEEV::ASTVec;
   if (b->UserFlags.smtlib_parser_flag) 
     {

diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp
index 101f7d38d18b256e0b04a7cccebea4b3a85c0996..5a91d716d36b4c5a8f4967fff64ac023bd9989c1 100644 (file)
--- a/src/main/Globals.cpp
+++ b/src/main/Globals.cpp
@@ -15,10 +15,13 @@ namespace BEEV
 {
   enum inputStatus input_status = NOT_DECLARED;
 
-  //global BEEVMGR for the parser. Use exclusively for parsing
+  //Originally just used by the parser, now used elesewhere.
   STP     * GlobalSTP;
   STPMgr  * ParserBM;
 
+  // Used exclusively for parsing.
+  ParserInterface * parserInterface;
+
   void (*vc_error_hdlr)(const char* err_msg) = NULL;
 
   // This is reusable empty vector, for representing empty children

diff --git a/src/main/Globals.h b/src/main/Globals.h
index 847c7ddf4664df25ba3b165ded58a32a43893742..c72bb627b2a7a211727b347ea16c9904fba22474 100644 (file)
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -39,6 +39,7 @@ namespace BEEV
   class ASTBVConst;
   class BVSolver;
   class STP;
+  class ParserInterface;
 
   /***************************************************************
    * ENUM TYPES
@@ -77,6 +78,7 @@ namespace BEEV
   //Useful global variables. Use for parsing only
   extern  STP * GlobalSTP;
   extern  STPMgr * ParserBM;
+  extern ParserInterface * parserInterface;
 
   //Some constant global vars for the Main function. Once they are
   //set, these globals will remain constants. These vars are not used

diff --git a/src/main/main.cpp b/src/main/main.cpp
index e7944fc02eeac264e89b1c61ee77f932a925987b..b7f5f84918956d485ea65f603b1cdb7e60700aa4 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -11,6 +11,9 @@
 #include "../printer/printers.h"
 #include "../STPManager/STPManager.h"
 #include "../STPManager/STP.h"
+#include "../AST/NodeFactory/TypeChecker.h"
+#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
+#include "../parser/ParserInterface.h"
 
 #ifdef EXT_HASH_MAP
 using namespace __gnu_cxx;
@@ -327,20 +330,39 @@ int main(int argc, char ** argv) {
     cout << CONSTANTBV::BitVector_Error(c) << endl;
     return 0;
   }
-  
+
   bm->GetRunTimes()->start(RunTimes::Parsing);
   if (bm->UserFlags.smtlib_parser_flag)
     {
-      smtparse((void*)AssertsQuery);
+         // Wrap a typchecking node factory around the default node factory.
+         // every node created is typechecked.
+         TypeChecker nf(*bm->defaultNodeFactory,*bm);
+
+         // Changes need to be made to the constant evaluator to get this working.
+         //SimplifyingNodeFactory nf3(nf,*bm);
+         ParserInterface pi(*bm, &nf);
+         parserInterface = &pi;
+
+         smtparse((void*)AssertsQuery);
       smtlex_destroy();
+
+      parserInterface = NULL;
+
     }
   else
     {
-      cvcparse((void*)AssertsQuery);
+         ParserInterface pi(*bm, bm->defaultNodeFactory);
+         parserInterface = &pi;
+
+
+         cvcparse((void*)AssertsQuery);
       cvclex_destroy();
+
+      parserInterface = NULL;
     }
   bm->GetRunTimes()->stop(RunTimes::Parsing);
 
+
   if(((ASTVec*)AssertsQuery)->empty())
     {
       FatalError("Input is Empty. Please enter some asserts and query\n");

diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index 2b43b5b452a35452f7d2612d2b9a45d319fdcb2d..deb231cdb31f8017f084136091e68d4ab19a54c2 100644 (file)
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -10,6 +10,7 @@
 #include <iostream>
 #include "parser.h"
 #include "parseCVC_defs.h"
+#include "ParserInterface.h"
 
   using namespace std;
   using namespace BEEV;  
@@ -127,7 +128,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
   // type determination in the lexer, but it's easier than rewriting
   // the whole grammar to eliminate the term/formula distinction.  
   cvclval.node = 
-    new BEEV::ASTNode((BEEV::ParserBM->GetLetMgr())->ResolveID(nptr));
+    new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr));
   //cvclval.node = new BEEV::ASTNode(nptr);
   if ((cvclval.node)->GetType() == BOOLEAN_TYPE)
     return FORMID_TOK;

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index eeb4a1dc3b91ff4ef0308b95b0b83a0087692f44..2a2982584ef8f11bada7416a6b8e0d25f382d0d6 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -9,6 +9,7 @@
    ********************************************************************/
   
 #include "parser.h"
+#include "ParserInterface.h"
 
   using namespace std; 
   using namespace BEEV;
@@ -175,11 +176,11 @@
 
 cmd             :      other_cmd
 {
-  _parser_symbol_table.clear();
+  parserInterface->letMgr._parser_symbol_table.clear();
 }
 |      other_cmd counterexample
 {
-  _parser_symbol_table.clear(); 
+  parserInterface->letMgr._parser_symbol_table.clear(); 
 }
 ; 
 
@@ -298,7 +299,7 @@ VarDecls        :      VarDecl ';'
 VarDecl         :      FORM_IDs ':' Type 
 {
   for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {
-    _parser_symbol_table.insert(*i);
+    parserInterface->letMgr._parser_symbol_table.insert(*i);
     i->SetIndexWidth($3.indexwidth);
     i->SetValueWidth($3.valuewidth);
     ParserBM->ListOfDeclaredVars.push_back(*i);
@@ -319,7 +320,7 @@ VarDecl         :      FORM_IDs ':' Type
     i->SetValueWidth($5->GetValueWidth());
     i->SetIndexWidth($5->GetIndexWidth());
                            
-    ParserBM->GetLetMgr()->LetExprMgr(*i,*$5);
+    parserInterface->letMgr.LetExprMgr(*i,*$5);
     delete $5;
   }
 }
@@ -337,7 +338,7 @@ VarDecl         :      FORM_IDs ':' Type
     i->SetValueWidth($5->GetValueWidth());
     i->SetIndexWidth($5->GetIndexWidth());
                            
-    ParserBM->GetLetMgr()->LetExprMgr(*i,*$5);
+    parserInterface->letMgr.LetExprMgr(*i,*$5);
     delete $5;
   }
 }                
@@ -368,7 +369,7 @@ ForDecl         :      FORMID_TOK ':' Type
 {
   $1->SetIndexWidth($3.indexwidth);
   $1->SetValueWidth($3.valuewidth);
-  _parser_symbol_table.insert(*$1);
+  parserInterface->letMgr._parser_symbol_table.insert(*$1);
   $$ = $1;                      
 }
 
@@ -452,7 +453,7 @@ Formula         :     '(' Formula ')'
 }
 |      FORMID_TOK 
 {  
-  $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1;
+  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); delete $1;
 }
 |      FORMID_TOK '(' Expr ')' 
 {
@@ -687,7 +688,7 @@ Formula         :     '(' Formula ')'
 {
   $$ = $4;
   //Cleanup the LetIDToExprMap
-  ParserBM->GetLetMgr()->CleanupLetIDMap();
+  parserInterface->letMgr.CleanupLetIDMap();
 }
 ;
 
@@ -729,7 +730,7 @@ Exprs           :      Expr
 ;
 
 /* Grammar for Expr */
-Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1;}
+Expr            :      TERMID_TOK { $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); delete $1;}
 |      '(' Expr ')' { $$ = $2; }
 |      BVCONST_TOK { $$ = $1; }
 |      BOOL_TO_BV_TOK '(' Formula ')'           
@@ -1169,7 +1170,7 @@ LetDecl         :       FORMID_TOK '=' Expr
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3);
+  parserInterface->letMgr.LetExprMgr(*$1,*$3);
   delete $1;
   delete $3;
 }
@@ -1187,7 +1188,7 @@ LetDecl         :       FORMID_TOK '=' Expr
   $1->SetValueWidth($5->GetValueWidth());
   $1->SetIndexWidth($5->GetIndexWidth());
 
-  ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5);
+  parserInterface->letMgr.LetExprMgr(*$1,*$5);
   delete $1;
   delete $5;
 }
@@ -1201,7 +1202,7 @@ LetDecl         :       FORMID_TOK '=' Expr
   $1->SetIndexWidth($3->GetIndexWidth());
 
   //Do LET-expr management
-  ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3);
+  parserInterface->letMgr.LetExprMgr(*$1,*$3);
   delete $1;
   delete $3;
 }
@@ -1220,7 +1221,7 @@ LetDecl         :       FORMID_TOK '=' Expr
   $1->SetIndexWidth($5->GetIndexWidth());
 
   //Do LET-expr management
-  ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5);
+  parserInterface->letMgr.LetExprMgr(*$1,*$5);
   delete $1;
   delete $5;
 }                

diff --git a/src/parser/let-funcs.cpp b/src/parser/LetMgr.cpp
similarity index 85%
rename from src/parser/let-funcs.cpp
rename to src/parser/LetMgr.cpp
index 807d5f3329839b3197218a925ad167f26ab3587b..c9f75fcd8e9c82ba4582544670f6c55639672ffb 100644 (file)
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/LetMgr.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -8,13 +8,9 @@
  ********************************************************************/
 
 #include <stdlib.h>
-#include "let-funcs.h"
+#include "LetMgr.h"
 
 namespace BEEV {
-  //external parser table for declared symbols. Only symbols which are
-  //declared are stored here.
-  ASTNodeSet _parser_symbol_table;
-
   // FUNC: This function maintains a map between LET-var names and
   // LET-expressions
   //
@@ -27,7 +23,7 @@ namespace BEEV {
   //3. otherwise add the <var,letExpr> pair to the _letid_expr table.
   void LETMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) 
   {
-    ASTNodeMap::iterator it;
+         ASTNodeMap::iterator it;
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
       FatalError("LetExprMgr:The LET-var v has already been defined"\
@@ -39,7 +35,7 @@ namespace BEEV {
                  "cannot redeclare as a letvar: v =", var);
     }
 
-    (*_letid_expr_map)[var] = letExpr;   
+    (*_letid_expr_map)[var] = letExpr;
   }//end of LetExprMgr()
 
   //this function looksup the "var to letexpr map" and returns the
@@ -47,10 +43,7 @@ namespace BEEV {
   //returns the var.
   ASTNode LETMgr::ResolveID(const ASTNode& v) 
   {
-    if (_letid_expr_map == NULL)
-      InitializeLetIDMap();
-
-    if(v.GetKind() != SYMBOL) {
+       if (v.GetKind() != SYMBOL) {
       return v;
     }
 
@@ -64,7 +57,7 @@ namespace BEEV {
         FatalError("ResolveID :: Unresolved Identifier: ",v);
       else
         return it->second;
-    }//end of ResolveID()
+    }
 
     //this is to mark the let-var as undefined. the let var is defined
     //only after the LetExprMgr has completed its work, and until then
@@ -80,11 +73,14 @@ namespace BEEV {
   // This function simply cleans up the LetID -> LetExpr Map.   
   void LETMgr::CleanupLetIDMap(void) 
   { 
-    // ext/hash_map::clear() is very expensive on big empty lists. shortcut. 
+    // ext/hash_map::clear() is very expensive on big empty maps. shortcut.
     if (_letid_expr_map->size()  ==0)
       return;
 
 
+    // I don't know what this does. Commenting it out and all the regression
+    // tests still pass.
+#if 0
     ASTNodeMap::iterator it = _letid_expr_map->begin();
     ASTNodeMap::iterator itend = _letid_expr_map->end();
     for(;it!=itend;it++) {
@@ -93,10 +89,11 @@ namespace BEEV {
         it->first.SetIndexWidth(0);
       }
     }
+#endif
 
     // May contain lots of buckets, so reset.
     delete _letid_expr_map;
-    _letid_expr_map = new ASTNodeMap();
+    InitializeLetIDMap();
   }//end of CleanupLetIDMap()
 
   void LETMgr::InitializeLetIDMap(void)

diff --git a/src/parser/let-funcs.h b/src/parser/LetMgr.h
similarity index 61%
rename from src/parser/let-funcs.h
rename to src/parser/LetMgr.h
index b7ac39dabbafcf618c286a6d034932ea091021ed..e63a224fcbb80d0d83780ba04544f38bc5ed9f95 100644 (file)
--- a/src/parser/let-funcs.h
+++ b/src/parser/LetMgr.h
@@ -1,14 +1,14 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 
-#ifndef LET_H
-#define LET_H
+#ifndef LETMGR_H
+#define LETMGR_H
 
 #include "../AST/AST.h"
 namespace BEEV
@@ -18,18 +18,27 @@ namespace BEEV
   {
   private:
 
-    // MAP: This map is from bound IDs that occur in LETs to
+    const ASTNode& ASTUndefined;
+
+       // MAP: This map is from bound IDs that occur in LETs to
     // expression. The map is useful in checking replacing the IDs
-    // with the corresponding expressions.
+    // with the corresponding expressions. As soon as the brackets
+       // that close a let expression is reached, it is emptied by
+    // a call to CleanupLetIDMap().
     ASTNodeMap *_letid_expr_map;
-    ASTNode ASTUndefined;
-      
+
+    //Allocate LetID map
+    void InitializeLetIDMap(void);
+
   public:
       
+    ASTNodeSet _parser_symbol_table;
+
     LETMgr(ASTNode undefined)
+    : ASTUndefined(undefined)
     {
-      _letid_expr_map = new ASTNodeMap();
-      ASTUndefined = undefined;
+       assert(!undefined.IsNull());
+       InitializeLetIDMap();
     }
 
     ~LETMgr()
@@ -42,14 +51,11 @@ namespace BEEV
     //Functions that are used to manage LET expressions
     void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
       
-    //Delete Letid Map
+    //Delete Letid Map. Called when we move onto the expression after (let ... )
     void CleanupLetIDMap(void);
-      
-    //Allocate LetID map
-    void InitializeLetIDMap(void);
-      
+
     //Substitute Let-vars with LetExprs
-    ASTNode SubstituteLetExpr(ASTNode inExpr);
+    //ASTNode SubstituteLetExpr(ASTNode inExpr);
   };// End of class LETMgr
 }; //end of namespace
 

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 541c0774714cef045df3cfdb37a1dd606850ff9e..c55ee8cbbdd2072b19a9ec922da312bf5c6cd5b9 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -3,7 +3,7 @@ include ../../scripts/Makefile.common
 LEX=flex
 YACC=bison -d -y --debug -v
 
-SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp
+SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp LetMgr.cpp
 OBJS = $(SRCS:.cpp=.o)
 LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
 CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
@@ -34,4 +34,4 @@ parseSM%_defs.h parseSM%.cpp:smtlib.y
 
 
 clean: 
-       rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* cvc.tab.* lex.yy.c .#*
\ No newline at end of file
+       rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* cvc.tab.* lex.yy.c libparser.a .#*

diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex
index 4c6e953765ef1f1a52782d0e56b8788ce36e6bad..6b26e9aa6eb94fa3003a7f2d50c3c309c571f79a 100644 (file)
--- a/src/parser/smtlib.lex
+++ b/src/parser/smtlib.lex
@@ -36,6 +36,7 @@
 #include <iostream>
 #include "parser.h"
 #include "parseSMT_defs.h"
+#include "ParserInterface.h"
 
   using namespace std;
   using namespace BEEV;
@@ -81,10 +82,10 @@ ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
 bit{DIGIT}+     {
                   char c = smttext[3];
                   if (c == '1') {
-                    smtlval.node = new BEEV::ASTNode(ParserBM->CreateOneConst(1));
+                    smtlval.node = new BEEV::ASTNode(parserInterface->CreateOneConst(1));
                   }
                   else {
-                    smtlval.node = new BEEV::ASTNode(ParserBM->CreateZeroConst(1));
+                    smtlval.node = new BEEV::ASTNode(parserInterface->CreateZeroConst(1));
                   }
                   return BITCONST_TOK;
                };
@@ -221,12 +222,12 @@ bit{DIGIT}+     {
 "boolbv"        { return BOOL_TO_BV_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = ParserBM->CreateSymbol(smttext); 
+  BEEV::ASTNode nptr = parserInterface->CreateSymbol(smttext); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting
   // the whole grammar to eliminate the term/formula distinction.  
-  smtlval.node = new BEEV::ASTNode((ParserBM->GetLetMgr())->ResolveID(nptr));
+  smtlval.node = new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr));
   //smtlval.node = new BEEV::ASTNode(nptr);
   if ((smtlval.node)->GetType() == BOOLEAN_TYPE)
     return FORMID_TOK;

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index 7166cab0b970e78600e0f6c2832a2add9f2985e5..2482b48fa4e670253df460fdf5c5aedc67cbb76d 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -35,7 +35,7 @@
    ********************************************************************/
   // -*- c++ -*-
 
-#include "parser.h"
+#include "ParserInterface.h"
 
   using namespace std; 
   using namespace BEEV;
@@ -48,8 +48,6 @@
   extern int smtlineno;
   extern int smtlex(void);
 
-  //BEEV::BeevMgr * ParserBM = GlobalSTP->bm;
-  
   int yyerror(const char *s) {
     cout << "syntax error: line " << smtlineno << "\n" << s << endl;
     cout << "  token: " << smttext << endl;
@@ -212,7 +210,7 @@ benchmark
   ASTNode assumptions;
   if($1 == NULL) 
     {
-      assumptions = ParserBM->CreateNode(TRUE);
+      assumptions = parserInterface->CreateNode(TRUE);
     } 
   else 
     {
@@ -221,13 +219,13 @@ benchmark
       
   if(query.IsNull()) 
     {
-      query = ParserBM->CreateNode(FALSE);
+      query = parserInterface->CreateNode(FALSE);
     }
 
   ((ASTVec*)AssertsQuery)->push_back(assumptions);
   ((ASTVec*)AssertsQuery)->push_back(query);
   delete $1;
-  _parser_symbol_table.clear();
+  parserInterface->letMgr._parser_symbol_table.clear();
   YYACCEPT;
 }
 ;
@@ -237,7 +235,7 @@ LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
 {
   if($4 != NULL){
     if($4->size() > 1) 
-      $$ = new ASTNode(ParserBM->CreateNode(AND,*$4));
+      $$ = new ASTNode(parserInterface->nf->CreateNode(AND,*$4));
     else
       $$ = new ASTNode((*$4)[0]);         
     delete $4;
@@ -263,7 +261,7 @@ bench_attribute
   $$ = new ASTVec;
   if ($1 != NULL) {
     $$->push_back(*$1);
-    ParserBM->AddAssert(*$1);
+    parserInterface->AddAssert(*$1);
     delete $1;
   }
 }
@@ -271,7 +269,7 @@ bench_attribute
 {
   if ($1 != NULL && $2 != NULL) {
     $1->push_back(*$2);
-    ParserBM->AddAssert(*$2);
+    parserInterface->AddAssert(*$2);
     $$ = $1;
     delete $2;
   }
@@ -415,23 +413,19 @@ var_decls var_decl
 var_decl:
 LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK
 {
-  _parser_symbol_table.insert(*$2);
+  parserInterface->letMgr._parser_symbol_table.insert(*$2);
   //Sort_symbs has the indexwidth/valuewidth. Set those fields in
   //var
   $2->SetIndexWidth($3.indexwidth);
   $2->SetValueWidth($3.valuewidth);
-  if(ParserBM->UserFlags.print_STPinput_back_flag)
-    ParserBM->ListOfDeclaredVars.push_back(*$2);
 }
 | LPAREN_TOK FORMID_TOK RPAREN_TOK
 {
-  _parser_symbol_table.insert(*$2);
+  parserInterface->letMgr._parser_symbol_table.insert(*$2);
   //Sort_symbs has the indexwidth/valuewidth. Set those fields in
   //var
   $2->SetIndexWidth(0);
   $2->SetValueWidth(0);
-  if(ParserBM->UserFlags.print_STPinput_back_flag)
-    ParserBM->ListOfDeclaredVars.push_back(*$2);
 }
 ;
 
@@ -458,15 +452,15 @@ an_formulas an_formula
 an_formula:   
 TRUE_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(TRUE)); 
-  $$->SetIndexWidth(0); 
-  $$->SetValueWidth(0);
+  $$ = new ASTNode(parserInterface->CreateNode(TRUE)); 
+  assert(0 == $$->GetIndexWidth()); 
+  assert(0 == $$->GetValueWidth());
 }
 | FALSE_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(FALSE)); 
-  $$->SetIndexWidth(0); 
-  $$->SetValueWidth(0);
+  $$ = new ASTNode(parserInterface->CreateNode(FALSE)); 
+  assert(0 == $$->GetIndexWidth()); 
+  assert(0 == $$->GetValueWidth());
 }
 | fvar
 {
@@ -475,8 +469,7 @@ TRUE_TOK
 | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode((GlobalSTP->simp)->CreateSimplifiedEQ(*$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(EQ,*$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -491,9 +484,8 @@ TRUE_TOK
   for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
       it!=itend; it++) {
     for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
-      ASTNode * n = new ASTNode(ParserBM->CreateNode(NOT, ParserBM->CreateNode(EQ, *it, *it2)));
+      ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(EQ, *it, *it2)));
 
-      BVTypeCheck(*n);
           
       forms.push_back(*n); 
     }
@@ -504,7 +496,7 @@ TRUE_TOK
  
   $$ = (forms.size() == 1) ?
     new ASTNode(forms[0]) :
-    new ASTNode(ParserBM->CreateNode(AND, forms));
+    new ASTNode(parserInterface->nf->CreateNode(AND, forms));
 
   delete $3;
 }
@@ -512,8 +504,7 @@ TRUE_TOK
 | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLT, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -521,8 +512,7 @@ TRUE_TOK
 | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLE, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -530,8 +520,7 @@ TRUE_TOK
 | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGT, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -539,8 +528,7 @@ TRUE_TOK
 | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGE, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -548,8 +536,7 @@ TRUE_TOK
 | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLT, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -557,8 +544,7 @@ TRUE_TOK
 | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLE, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -566,8 +552,7 @@ TRUE_TOK
 | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGT, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -575,8 +560,7 @@ TRUE_TOK
 | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGE, *$3, *$4));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -587,41 +571,41 @@ TRUE_TOK
 }
 | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(NOT, *$3));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(NOT, *$3));
   delete $3;
 }
 | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(IMPLIES, *$3, *$4));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(IMPLIES, *$3, *$4));
   delete $3;
   delete $4;
 }
 | LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedFormulaITE(*$3, *$4, *$5));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(ITE, *$3, *$4, *$5));
   delete $3;
   delete $4;
   delete $5;
 }
 | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(AND, *$3));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(AND, *$3));
   delete $3;
 }
 | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(OR, *$3));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(OR, *$3));
   delete $3;
 }
 | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(XOR, *$3, *$4));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(XOR, *$3, *$4));
   delete $3;
   delete $4;
 }
 | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateNode(IFF, *$3, *$4));
+  $$ = new ASTNode(parserInterface->nf->CreateNode(IFF, *$3, *$4));
   delete $3;
   delete $4;
 }
@@ -630,15 +614,13 @@ TRUE_TOK
 {
   $$ = $2;
   //Cleanup the LetIDToExprMap
-  ParserBM->GetLetMgr()->CleanupLetIDMap();                      
+  parserInterface->letMgr.CleanupLetIDMap();                      
 }
 ;
 
 letexpr_mgmt: 
 LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
 {
-  //Expr must typecheck
-  BVTypeCheck(*$6);
       
   //set the valuewidth of the identifier
   $5->SetValueWidth($6->GetValueWidth());
@@ -652,21 +634,21 @@ LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6);
+  parserInterface->letMgr.LetExprMgr(*$5,*$6);
+  
   delete $5;
   delete $6;      
 }
 | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK 
 {
   //Expr must typecheck
-  BVTypeCheck(*$6);
      
   //set the valuewidth of the identifier
   $5->SetValueWidth($6->GetValueWidth());
   $5->SetIndexWidth($6->GetIndexWidth());
      
   //Do LET-expr management
-  ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6);
+  parserInterface->letMgr.LetExprMgr(*$5,*$6);
   delete $5;
   delete $6;     
 }
@@ -694,11 +676,11 @@ an_terms an_term
 an_term:
 BVCONST_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateBVConst($1, 10, 32));
+  $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32));
 }
 | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 {
-  $$ = new ASTNode(ParserBM->CreateBVConst($1,10,$3));
+  $$ = new ASTNode(parserInterface->CreateBVConst($1,10,$3));
   delete $1;
 }
 | an_nonbvconst_term
@@ -708,14 +690,14 @@ an_nonbvconst_term:
 BITCONST_TOK { $$ = $1; }
 | var
 {
-  $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1));
+  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
   delete $1;
 }
 | LPAREN_TOK an_term RPAREN_TOK
   //| LPAREN_TOK an_term annotations RPAREN_TOK
 {
   $$ = $2;
-  //$$ = new ASTNode(ParserBM->SimplifyTerm(*$2));
+  //$$ = new ASTNode(parserInterface->SimplifyTerm(*$2));
   //delete $2;
 }
 | SELECT_TOK an_term an_term
@@ -726,8 +708,7 @@ BITCONST_TOK { $$ = $1; }
   ASTNode index = *$3;
   unsigned int width = array.GetValueWidth();
   ASTNode * n = 
-    new ASTNode(ParserBM->CreateTerm(READ, width, array, index));
-  BVTypeCheck(*n);
+    new ASTNode(parserInterface->nf->CreateTerm(READ, width, array, index));
   $$ = n;
   delete $2;
   delete $3;
@@ -739,9 +720,7 @@ BITCONST_TOK { $$ = $1; }
   ASTNode array = *$2;
   ASTNode index = *$3;
   ASTNode writeval = *$4;
-  ASTNode write_term = ParserBM->CreateTerm(WRITE,width,array,index,writeval);
-  write_term.SetIndexWidth($2->GetIndexWidth());
-  BVTypeCheck(write_term);
+  ASTNode write_term = parserInterface->nf->CreateArrayTerm(WRITE,$2->GetIndexWidth(),width,array,index,writeval);
   ASTNode * n = new ASTNode(write_term);
   $$ = n;
   delete $2;
@@ -757,43 +736,26 @@ BITCONST_TOK { $$ = $1; }
   if((unsigned)$3 >= $7->GetValueWidth())
     yyerror("Parsing: Wrong width in BVEXTRACT\n");                      
       
-  ASTNode hi  =  ParserBM->CreateBVConst(32, $3);
-  ASTNode low =  ParserBM->CreateBVConst(32, $5);
-  ASTNode output = ParserBM->CreateTerm(BVEXTRACT, width, *$7,hi,low);
+  ASTNode hi  =  parserInterface->CreateBVConst(32, $3);
+  ASTNode low =  parserInterface->CreateBVConst(32, $5);
+  ASTNode output = parserInterface->nf->CreateTerm(BVEXTRACT, width, *$7,hi,low);
   ASTNode * n = new ASTNode(output);
-  BVTypeCheck(*n);
   $$ = n;
   delete $7;
 }
 |  ITE_TOK an_formula an_term an_term 
 {
-  unsigned int width = $3->GetValueWidth();
-  if (width != $4->GetValueWidth()) {
-    cerr << *$3;
-    cerr << *$4;
-    yyerror("Width mismatch in IF-THEN-ELSE");
-  }                      
-  if($3->GetIndexWidth() != $4->GetIndexWidth())
-    yyerror("Width mismatch in IF-THEN-ELSE");
-      
-  BVTypeCheck(*$2);
-  BVTypeCheck(*$3);
-  BVTypeCheck(*$4);
-  $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedTermITE(*$2, *$3, *$4));
-  //$$ = new ASTNode(ParserBM->CreateTerm(ITE,width,*$2, *$3, *$4));
-  $$->SetIndexWidth($4->GetIndexWidth());
-  BVTypeCheck(*$$);
+  const unsigned int width = $3->GetValueWidth();
+  $$ = new ASTNode(parserInterface->nf->CreateArrayTerm(ITE,$4->GetIndexWidth(), width,*$2, *$3, *$4));      
   delete $2;
   delete $3;
   delete $4;
 }
 |  BVCONCAT_TOK an_term an_term 
 {
-  unsigned int width = $2->GetValueWidth() + $3->GetValueWidth();
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, width, *$2, *$3));
-  BVTypeCheck(*n);
+  const unsigned int width = $2->GetValueWidth() + $3->GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT, width, *$2, *$3));
   $$ = n;
-      
   delete $2;
   delete $3;
 }
@@ -801,8 +763,7 @@ BITCONST_TOK { $$ = $1; }
 {
   //this is the BVNEG (term) in the CVCL language
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, *$2));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, *$2));
   $$ = n;
   delete $2;
 }
@@ -810,19 +771,14 @@ BITCONST_TOK { $$ = $1; }
 {
   //this is the BVUMINUS term in CVCL langauge
   unsigned width = $2->GetValueWidth();
-  ASTNode * n =  new ASTNode(ParserBM->CreateTerm(BVUMINUS,width,*$2));
-  BVTypeCheck(*n);
+  ASTNode * n =  new ASTNode(parserInterface->nf->CreateTerm(BVUMINUS,width,*$2));
   $$ = n;
   delete $2;
 }
 |  BVAND_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in AND");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVAND, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -830,11 +786,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in OR");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVOR, width, *$2, *$3)); 
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3)); 
   $$ = n;
   delete $2;
   delete $3;
@@ -842,11 +794,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVXOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in XOR");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXOR, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVXOR, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -858,13 +806,12 @@ BITCONST_TOK { $$ = $1; }
        
       unsigned int width = $2->GetValueWidth();
       ASTNode * n = new ASTNode(
-      ParserBM->CreateTerm( BVOR, width,
-     ParserBM->CreateTerm(BVAND, width, *$2, *$3),
-     ParserBM->CreateTerm(BVAND, width,
-            ParserBM->CreateTerm(BVNEG, width, *$2),
-        ParserBM->CreateTerm(BVNEG, width, *$3)
+      parserInterface->nf->CreateTerm( BVOR, width,
+     parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3),
+     parserInterface->nf->CreateTerm(BVAND, width,
+            parserInterface->nf->CreateTerm(BVNEG, width, *$2),
+        parserInterface->nf->CreateTerm(BVNEG, width, *$3)
      )));
-      BVTypeCheck(*n);
 
       $$ = n;
       delete $2;
@@ -875,12 +822,11 @@ BITCONST_TOK { $$ = $1; }
   {
        
 
-       ASTNode * n = new ASTNode(ParserBM->CreateTerm(ITE, 1, 
-       ParserBM->CreateNode(EQ, *$2, *$3),
-       ParserBM->CreateOneConst(1),
-       ParserBM->CreateZeroConst(1)));
+       ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(ITE, 1, 
+       parserInterface->nf->CreateNode(EQ, *$2, *$3),
+       parserInterface->CreateOneConst(1),
+       parserInterface->CreateZeroConst(1)));
        
-       BVTypeCheck(*n);
       $$ = n;
       delete $2;
       delete $3;
@@ -889,24 +835,16 @@ BITCONST_TOK { $$ = $1; }
     
 |  BVSUB_TOK an_term an_term 
 {
-  unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVSUB");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSUB, width, *$2, *$3));
-  BVTypeCheck(*n);
+  const unsigned int width = $2->GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSUB, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
 }
 |  BVPLUS_TOK an_term an_term 
 {
-  unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVPLUS");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, width, *$2, *$3));
-  BVTypeCheck(*n);
+  const unsigned int width = $2->GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -914,12 +852,8 @@ BITCONST_TOK { $$ = $1; }
 }
 |  BVMULT_TOK an_term an_term 
 {
-  unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVMULT");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMULT, width, *$2, *$3));
-  BVTypeCheck(*n);
+  const unsigned int width = $2->GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMULT, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -928,11 +862,7 @@ BITCONST_TOK { $$ = $1; }
 |      BVDIV_TOK an_term an_term  
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVDIV");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVDIV, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVDIV, width, *$2, *$3));
   $$ = n;
 
   delete $2;
@@ -941,11 +871,7 @@ BITCONST_TOK { $$ = $1; }
 |      BVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVMOD");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMOD, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMOD, width, *$2, *$3));
   $$ = n;
 
   delete $2;
@@ -954,11 +880,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVDIV_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in SBVDIV");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVDIV, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVDIV, width, *$2, *$3));
   $$ = n;
 
   delete $2;
@@ -967,11 +889,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVREM_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in SBVREM");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVREM, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVREM, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -979,11 +897,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in SBVMOD");
-  }
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVMOD, width, *$2, *$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVMOD, width, *$2, *$3));
   $$ = n;
   delete $2;
   delete $3;
@@ -991,11 +905,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVNAND_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  if (width != $3->GetValueWidth()) {
-    yyerror("Width mismatch in BVNAND");
-  }
-      ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, ParserBM->CreateTerm(BVAND, width, *$2, *$3)));
-      BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3)));
   $$ = n;
   delete $2;
   delete $3;
@@ -1003,8 +913,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVNOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-      ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, ParserBM->CreateTerm(BVOR, width, *$2, *$3))); 
-      BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3))); 
   $$ = n;
   delete $2;
   delete $3;
@@ -1013,8 +922,7 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting left by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVLEFTSHIFT,w,*$2,*$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVLEFTSHIFT,w,*$2,*$3));
   $$ = n;
   delete $2;
 }
@@ -1022,8 +930,7 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3));
   $$ = n;
   delete $2;
 }
@@ -1031,14 +938,12 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting arithmetic right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSRSHIFT,w,*$2,*$3));
-  BVTypeCheck(*n);
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSRSHIFT,w,*$2,*$3));
   $$ = n;
   delete $2;
 }
 |  BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
 {
-  BVTypeCheck(*$5);
       
   ASTNode *n;
   unsigned width = $5->GetValueWidth();
@@ -1049,14 +954,14 @@ BITCONST_TOK { $$ = $1; }
     }
   else if (rotate < width)
     {
-      ASTNode high = ParserBM->CreateBVConst(32,width-1);
-      ASTNode zero = ParserBM->CreateBVConst(32,0);
-      ASTNode cut = ParserBM->CreateBVConst(32,width-rotate);
-      ASTNode cutMinusOne = ParserBM->CreateBVConst(32,width-rotate-1);
+      ASTNode high = parserInterface->CreateBVConst(32,width-1);
+      ASTNode zero = parserInterface->CreateBVConst(32,0);
+      ASTNode cut = parserInterface->CreateBVConst(32,width-rotate);
+      ASTNode cutMinusOne = parserInterface->CreateBVConst(32,width-rotate-1);
 
-      ASTNode top =  ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,high, cut);
-      ASTNode bottom =  ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,cutMinusOne,zero);
-      n =  new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top));
+      ASTNode top =  parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$5,high, cut);
+      ASTNode bottom =  parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$5,cutMinusOne,zero);
+      n =  new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
       delete $5;
     }
   else
@@ -1065,13 +970,11 @@ BITCONST_TOK { $$ = $1; }
       yyerror("Rotate must be strictly less than the width.");
     }
       
-  BVTypeCheck(*n);
   $$ = n;
       
 }
 |  BVROTATE_RIGHT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
 {
-  BVTypeCheck(*$5);
       
   ASTNode *n;
   unsigned width = $5->GetValueWidth();
@@ -1082,14 +985,14 @@ BITCONST_TOK { $$ = $1; }
     }
   else if (rotate < width)
     {
-      ASTNode high = ParserBM->CreateBVConst(32,width-1);
-      ASTNode zero = ParserBM->CreateBVConst(32,0);
-      ASTNode cut = ParserBM->CreateBVConst(32,rotate); 
-      ASTNode cutMinusOne = ParserBM->CreateBVConst(32,rotate-1);
+      ASTNode high = parserInterface->CreateBVConst(32,width-1);
+      ASTNode zero = parserInterface->CreateBVConst(32,0);
+      ASTNode cut = parserInterface->CreateBVConst(32,rotate); 
+      ASTNode cutMinusOne = parserInterface->CreateBVConst(32,rotate-1);
 
-      ASTNode bottom =  ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,cutMinusOne, zero);
-      ASTNode top =  ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,high,cut);
-      n =  new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top));
+      ASTNode bottom =  parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$5,cutMinusOne, zero);
+      ASTNode top =  parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$5,high,cut);
+      n =  new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
       delete $5;
     }
   else
@@ -1098,13 +1001,11 @@ BITCONST_TOK { $$ = $1; }
       yyerror("Rotate must be strictly less than the width.");
     }
       
-  BVTypeCheck(*n);
   $$ = n;
       
 }
    |  BVREPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
     {
-      BVTypeCheck(*$5);
          unsigned count = $3;
          if (count < 1)
                FatalError("One or more repeats please");
@@ -1114,30 +1015,25 @@ BITCONST_TOK { $$ = $1; }
       
       for (unsigned i =1; i < count; i++)
       {
-         n = ParserBM->CreateTerm(BVCONCAT,w*(i+1),n,*$5);
-         BVTypeCheck(n);
+         n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$5);
       }
       $$ = new ASTNode(n);
     }
 |  BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
 {
-  BVTypeCheck(*$5);
   unsigned w = $5->GetValueWidth() + $3;
-  ASTNode width = ParserBM->CreateBVConst(32,w);
-  ASTNode *n =  new ASTNode(ParserBM->CreateTerm(BVSX,w,*$5,width));
-  BVTypeCheck(*n);
+  ASTNode width = parserInterface->CreateBVConst(32,w);
+  ASTNode *n =  new ASTNode(parserInterface->nf->CreateTerm(BVSX,w,*$5,width));
   $$ = n;
   delete $5;
 }
 | BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
 {
-  BVTypeCheck(*$5);
   if (0 != $3)
     {
       unsigned w = $5->GetValueWidth() + $3;
-      ASTNode leading_zeroes = ParserBM->CreateZeroConst($3);
-      ASTNode *n =  new ASTNode(ParserBM->CreateTerm(BVCONCAT,w,leading_zeroes,*$5));
-      BVTypeCheck(*n);
+      ASTNode leading_zeroes = parserInterface->CreateZeroConst($3);
+      ASTNode *n =  new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,w,leading_zeroes,*$5));
       $$ = n;
       delete $5;
     }
@@ -1186,12 +1082,12 @@ BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 var:
 FORMID_TOK 
 {
-  $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); 
+  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); 
   delete $1;      
 }
 | TERMID_TOK
 {
-  $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1));
+  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
   delete $1;
 }
 | QUESTION_TOK TERMID_TOK
@@ -1207,7 +1103,7 @@ DOLLAR_TOK FORMID_TOK
 }
 | FORMID_TOK
 {
-  $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); 
+  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); 
   delete $1;      
 }   
 ;