STP: Remove unused files.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100394 91177308-0d34-0410-b5e6-96231b3b80d8

10 files changed, 0 insertions, 2867 deletions

diff --git a/stp/AST/asttest.cpp b/stp/AST/asttest.cpp
deleted file mode 100644
index 57f3d20c..00000000
--- a/stp/AST/asttest.cpp
+++ /dev/null
@@ -1,29 +0,0 @@
-#include "AST.h"
-
-using namespace BEEV;
-
-int main()
-{
-
-  BeevMgr * bm = new BeevMgr();
-  ASTNode s1 = bm->CreateSymbol("foo");
-  s1 = bm->CreateSymbol("foo1");
-  s1 = bm->CreateSymbol("foo2");
-  ASTNode s2 = bm->CreateSymbol("bar");
-  cout << "s1" <<  s1 << endl;
-  cout << "s2" <<  s2 << endl;
-
-  ASTNode b1 = bm->CreateBVConst(5,12);
-  ASTNode b2 = bm->CreateBVConst(6,36);
-  cout << "b1: " <<  b1 << endl;
-  cout << "b2: " <<  b2 << endl;
-
-  ASTNode a1 = bm->CreateNode(EQ, s1, s2);
-  ASTNode a2 = bm->CreateNode(AND, s1, s2);
-  a1 = bm->CreateNode(OR, s1, s2);
-  ASTNode a3 = bm->CreateNode(IMPLIES, a1, a2);
-  ASTNode a4 = bm->CreateNode(IMPLIES, s1, a2);
-  cout << "a3" <<  a3 << endl;
-  cout << "a4" <<  a4 << endl;
-  return 0;
-}
diff --git a/stp/AST/bbtest.cpp b/stp/AST/bbtest.cpp
deleted file mode 100644
index 83aa6a4e..00000000
--- a/stp/AST/bbtest.cpp
+++ /dev/null
@@ -1,96 +0,0 @@
-#include "AST.h"
-
-using namespace BEEV;
-
-int main()
-{
-  const int size = 32;
-
-  BeevMgr *bm = new BeevMgr();
-  ASTNode s1 = bm->CreateSymbol("x");
-  s1.SetValueWidth(size);
-  cout << "s1" <<  s1 << endl;
-  ASTNode s2 = bm->CreateSymbol("y");
-  s2.SetValueWidth(size);
-  cout << "s2" <<  s2 << endl;
-  ASTNode s3 = bm->CreateSymbol("z");
-  s3.SetValueWidth(size);
-  cout << "s3" <<  s3 << endl;
-
-  ASTNode c1 = bm->CreateBVConst(size,0);
-  cout << "c1" <<  c1 << endl;
-  ASTVec bbc1 = bm->BBTerm(c1);
-  cout << "bitblasted c1 " << endl;
-  LispPrintVec(cout, bbc1, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode c2 = bm->CreateBVConst(size,1);
-  c2.SetValueWidth(size);
-  cout << "c2" <<  c2 << endl;
-  ASTVec bbc2 = bm->BBTerm(c2);
-  cout << "bitblasted c2 " << endl;
-  LispPrintVec(cout, bbc2, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode c3 = bm->CreateBVConst(size, 0xFFFFFFFF);
-  c3.SetValueWidth(size);
-  cout << "c3" <<  c3 << endl;
-  ASTVec bbc3 = bm->BBTerm(c3);
-  cout << "bitblasted c3 " << endl;
-  LispPrintVec(cout, bbc3, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode c4 = bm->CreateBVConst(size, 0xAAAAAAAA);
-  c4.SetValueWidth(size);
-  cout << "c4" <<  c4 << endl;
-  ASTVec bbc4 = bm->BBTerm(c4);
-  cout << "bitblasted c4 " << endl;
-  LispPrintVec(cout, bbc4, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-//   ASTNode b1 = bm->CreateBVConst(12);
-//   ASTNode b2 = bm->CreateBVConst(36);
-//   cout << "b1: " <<  b1 << endl;
-//   cout << "b2: " <<  b2 << endl;
-
-  ASTNode a1 = bm->CreateNode(BVPLUS, s1, s2);
-  a1.SetValueWidth(size);
-
-  ASTVec& bba1 = bm->BBTerm(a1);
-  cout << "bitblasted a1 " << endl;
-  LispPrintVec(cout, bba1, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode a2 = bm->CreateNode(BVPLUS, s1, s2, s3);
-  a1.SetValueWidth(2);
-
-  ASTVec& bba2 = bm->BBTerm(a2);
-  cout << "bitblasted a2 " << endl;
-  LispPrintVec(cout, bba2, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode a3 = bm->CreateNode(BVXOR, s1, s2);
-  a3.SetValueWidth(2);
-
-  ASTVec& bba3 = bm->BBTerm(a3);
-  cout << "bitblasted a3 " << endl;
-  LispPrintVec(cout, bba3, 0);
-  cout << endl;
-  bm->AlreadyPrintedSet.clear();
-
-  ASTNode a4 = bm->CreateNode(EQ, s1, s2);
-  ASTNode bba4 = bm->BBForm(a4);
-  cout << "bitblasted a4 " << endl << bba4 << endl;
-
-  ASTNode a5 = bm->CreateNode(BVLE, s1, s2);
-  ASTNode bba5 = bm->BBForm(a5);
-  cout << "bitblasted a5 " << endl << bba5 << endl;
-
-  return 0;
-}
diff --git a/stp/AST/cnftest.cpp b/stp/AST/cnftest.cpp
deleted file mode 100644
index 7ce270c8..00000000
--- a/stp/AST/cnftest.cpp
+++ /dev/null
@@ -1,47 +0,0 @@
-// -*- c++ -*-
-
-// Test program for CNF conversion.
-
-#include "AST.h"
-
-using namespace BEEV;
-
-int main()
-{
-  const int size = 1;
-  
-  BeevMgr *bm = new BeevMgr();
-  ASTNode s1 = bm->CreateSymbol("x");
-  s1.SetValueWidth(size);
-  
-  cout << "s1" <<  s1 << endl;
-  ASTNode s2 = bm->CreateSymbol("y");
-  s2.SetValueWidth(size);
-
-  cout << "s2" <<  s2 << endl;
-  ASTNode s3 = bm->CreateSymbol("z");
-  s3.SetValueWidth(size);
-  
-  cout << "s3" <<  s3 << endl;
-
-  ASTNode bbs1 = bm->BBForm(s1);
-  cout << "bitblasted s1" << endl << bbs1 << endl;
-  bm->PrintClauseList(cout, bm->ToCNF(bbs1));
-
-  ASTNode a2 = bm->CreateNode(AND, s1, s2);
-  ASTNode bba2 = bm->BBForm(a2);
-  cout << "bitblasted a2" << endl << bba2 << endl;
-  bm->PrintClauseList(cout, bm->ToCNF(bba2));
-
-  ASTNode a3 = bm->CreateNode(OR, s1, s2);
-  ASTNode bba3 = bm->BBForm(a3);
-  cout << "bitblasted a3" << endl << bba3 << endl;
-  bm->PrintClauseList(cout, bm->ToCNF(bba3));
-
-  ASTNode a4 = bm->CreateNode(EQ, s1, s2);
-  ASTNode bba4 = bm->BBForm(a4);
-  cout << "bitblasted a4 " << endl << bba4 << endl;
-
-  bm->PrintClauseList(cout, bm->ToCNF(bba4));
-
-}
diff --git a/stp/parser/Makefile b/stp/parser/Makefile
deleted file mode 100644
index 12483a26..00000000
--- a/stp/parser/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-include ../Makefile.common
-
-SRCS = lexPL.cpp parsePL.cpp let-funcs.cpp main.cpp
-OBJS = $(SRCS:.cpp=.o)
-LIBS = -L../AST -last -L../sat -lsatsolver -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
-
-all: parser 
-
-parser: lexPL.o parsePL.o let-funcs.o main.o 
-		$(CXX) $(CFLAGS) $(LDFLAGS) lexPL.o parsePL.o main.o let-funcs.o $(LIBS) -o parser
-
-main.o: parsePL_defs.h
-
-lexPL.cpp:	PL.lex parsePL_defs.h ../AST/AST.h
-		$(LEX) -olexPL.cpp PL.lex
-
-parsePL_defs.h: y.tab.h
-		@cp y.tab.h parsePL_defs.h
-parsePL.cpp: y.tab.c
-		@cp y.tab.c parsePL.cpp
-
-y.tab.c y.tab.h:	PL.y
-		$(YACC) PL.y
-
-
-clean:	
-		rm -rf *.o parsePL_defs.h *~ lexPL.cpp parsePL.cpp *.output parser y.tab.* lex.yy.c .#*
diff --git a/stp/parser/PL.lex b/stp/parser/PL.lex
deleted file mode 100644
index e9358a0e..00000000
--- a/stp/parser/PL.lex
+++ /dev/null
@@ -1,128 +0,0 @@
-%{
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-#include <iostream>
-#include "../AST/AST.h"
-#include "parsePL_defs.h"
-
-extern char *yytext;
-extern int yyerror (const char *msg);
-%}
-
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-%x	COMMENT
-%x	STRING_LITERAL
-LETTER	([a-zA-Z])
-HEX     ([0-9a-fA-F])
-BITS    ([0-1])
-DIGIT	([0-9])
-OPCHAR	(['?\_$])
-ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
-%%
-
-[()[\]{},.;:'!#?_=]  { return yytext[0];}
-
-[\n]             { /*Skip new line */ }
-[ \t\r\f]	 { /* skip whitespace */ }
-0b{BITS}+	 { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2,  2)); return BVCONST_TOK;}
-0bin{BITS}+	 { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4,  2)); return BVCONST_TOK;}
-0h{HEX}+         { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;}
-0hex{HEX}+       { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;}
-{DIGIT}+	 { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;}
-
-"%"		 { BEGIN COMMENT;}
-<COMMENT>"\n"	 { BEGIN INITIAL; /* return to normal mode */}
-<COMMENT>.	 { /* stay in comment mode */}
-
-"ARRAY"		 { return ARRAY_TOK; }
-"OF"		 { return OF_TOK; }
-"WITH"		 { return WITH_TOK; }
-"AND"		 { return AND_TOK;}
-"NAND"		 { return NAND_TOK;}
-"NOR"		 { return NOR_TOK;}
-"NOT"		 { return NOT_TOK; }
-"OR"		 { return OR_TOK; }
-"/="		 { return NEQ_TOK; }
- ":="            { return ASSIGN_TOK;}
-"=>"		 { return IMPLIES_TOK; }
-"<=>"		 { return IFF_TOK; }
-"XOR"		 { return XOR_TOK; }
-"IF"		 { return IF_TOK; }
-"THEN"		 { return THEN_TOK; }
-"ELSE"		 { return ELSE_TOK; }
-"ELSIF"		 { return ELSIF_TOK; }
-"END"		 { return END_TOK; }
-"ENDIF"		 { return ENDIF_TOK; }
-"BV"             { return BV_TOK;}
-"BITVECTOR"      { return BV_TOK;}
-"BOOLEAN"        { return BOOLEAN_TOK;}
-"<<"             { return BVLEFTSHIFT_TOK;}
-">>"             { return BVRIGHTSHIFT_TOK;}
-"BVPLUS"         { return BVPLUS_TOK;}
-"BVSUB"          { return BVSUB_TOK;}
-"BVUMINUS"       { return BVUMINUS_TOK;}
-"BVMULT"         { return BVMULT_TOK;}
-"BVDIV"          { return BVDIV_TOK;}
-"BVMOD"          { return BVMOD_TOK;}
-"SBVDIV"         { return SBVDIV_TOK;}
-"SBVMOD"         { return SBVMOD_TOK;}
-"~"              { return BVNEG_TOK;}
-"&"              { return BVAND_TOK;}
-"|"              { return BVOR_TOK;}
-"BVXOR"          { return BVXOR_TOK;}
-"BVNAND"         { return BVNAND_TOK;}
-"BVNOR"          { return BVNOR_TOK;}
-"BVXNOR"         { return BVXNOR_TOK;}
-"@"              { return BVCONCAT_TOK;}
-"BVLT"           { return BVLT_TOK;}
-"BVGT"           { return BVGT_TOK;}
-"BVLE"           { return BVLE_TOK;}
-"BVGE"           { return BVGE_TOK;}
-"BVSLT"          { return BVSLT_TOK;}
-"BVSGT"          { return BVSGT_TOK;}
-"BVSLE"          { return BVSLE_TOK;}
-"BVSGE"          { return BVSGE_TOK;}
-"BVSX"           { return BVSX_TOK;} 
-"SBVLT"          { return BVSLT_TOK;}
-"SBVGT"          { return BVSGT_TOK;}
-"SBVLE"          { return BVSLE_TOK;}
-"SBVGE"          { return BVSGE_TOK;}
-"SX"             { return BVSX_TOK;} 
-"BOOLEXTRACT"    { return BOOLEXTRACT_TOK;}
-"BOOLBV"         { return BOOL_TO_BV_TOK;}
-"ASSERT"	 { return ASSERT_TOK; }
-"QUERY"	         { return QUERY_TOK; }
-"FALSE"          { return FALSELIT_TOK;}
-"TRUE"           { return TRUELIT_TOK;}
-"IN"             { return IN_TOK;}
-"LET"            { return LET_TOK;}
-"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK;}
-"COUNTERMODEL"   { return COUNTEREXAMPLE_TOK;}
- "PUSH"          { return PUSH_TOK;}
- "POP"           { return POP_TOK;}
-
-(({LETTER})|(_)({ANYTHING}))({ANYTHING})*	{
-  BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); 
-
-  // 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.  
-  yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr));
-  //yylval.node = new BEEV::ASTNode(nptr);
-  if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE)
-    return FORMID_TOK;
-  else 
-    return TERMID_TOK;  
-}
-
-.                { yyerror("Illegal input character."); }
-%%
diff --git a/stp/parser/PL.y b/stp/parser/PL.y
deleted file mode 100644
index aa58aa4c..00000000
--- a/stp/parser/PL.y
+++ /dev/null
@@ -1,1006 +0,0 @@
-%{
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include "../AST/AST.h"
-using namespace std; 
-
-  // Suppress the bogus warning suppression in bison (it generates
-  // compile error)
-#undef __GNUC_MINOR__
-
-  extern int yylex(void);
-  extern char* yytext;
-  extern int yylineno;
-  int yyerror(const char *s) {
-    cout << "syntax error: line " << yylineno << "\n" << s << endl;    
-    BEEV::FatalError("");
-    return 1;			/* Dill: don't know what it should return */
-  };
-
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
-#define YYERROR_VERBOSE 1
-#define YY_EXIT_FAILURE -1
-%}
-
-%union {
-
-  unsigned int uintval;			/* for numerals in types. */
-  struct {
-    //stores the indexwidth and valuewidth
-    //indexwidth is 0 iff type is bitvector. positive iff type is
-    //array, and stores the width of the indexing bitvector
-    unsigned int indexwidth;
-    //width of the bitvector type
-    unsigned int valuewidth;
-  } indexvaluewidth;
-
-  //ASTNode,ASTVec
-  BEEV::ASTNode *node;
-  BEEV::ASTVec *vec;
-
-  //Hash_Map to hold Array Updates during parse A map from array index
-  //to array values. To support the WITH construct
-  BEEV::ASTNodeMap * Index_To_UpdateValue;
-};
-
-%start cmd
-
-%token	AND_TOK			"AND"
-%token	OR_TOK			"OR"
-%token	NOT_TOK			"NOT"
-%token	XOR_TOK			"XOR"
-%token	NAND_TOK		"NAND"
-%token	NOR_TOK			"NOR"
-%token	IMPLIES_TOK		"=>"
-%token	IFF_TOK			"<=>"
-
-%token	IF_TOK			"IF"
-%token	THEN_TOK		"THEN"
-%token	ELSE_TOK		"ELSE"
-%token	ELSIF_TOK		"ELSIF"
-%token	END_TOK			"END"
-%token	ENDIF_TOK		"ENDIF"
-%token	NEQ_TOK			"/="
-%token  ASSIGN_TOK              ":="
-
-%token  BV_TOK                  "BV"
-%token  BVLEFTSHIFT_TOK         "<<"
-%token  BVRIGHTSHIFT_TOK        ">>"
-%token  BVPLUS_TOK              "BVPLUS"
-%token  BVSUB_TOK               "BVSUB"
-%token  BVUMINUS_TOK            "BVUMINUS"
-%token  BVMULT_TOK              "BVMULT"
-
-%token  BVDIV_TOK               "BVDIV"
-%token  BVMOD_TOK               "BVMOD"
-%token  SBVDIV_TOK              "SBVDIV"
-%token  SBVMOD_TOK              "SBVMOD"
-
-
-%token  BVNEG_TOK               "~"
-%token  BVAND_TOK               "&"
-%token  BVOR_TOK                "|"
-%token  BVXOR_TOK               "BVXOR"
-%token  BVNAND_TOK              "BVNAND"
-%token  BVNOR_TOK               "BVNOR"
-%token  BVXNOR_TOK              "BVXNOR"
-%token  BVCONCAT_TOK            "@"
-
-%token  BVLT_TOK                "BVLT"
-%token  BVGT_TOK                "BVGT"
-%token  BVLE_TOK                "BVLE"
-%token  BVGE_TOK                "BVGE"
-
-%token  BVSLT_TOK               "BVSLT"
-%token  BVSGT_TOK               "BVSGT"
-%token  BVSLE_TOK               "BVSLE"
-%token  BVSGE_TOK               "BVSGE"
-%token  BOOL_TO_BV_TOK          "BOOLBV"
-%token  BVSX_TOK                "BVSX"
-%token  BOOLEXTRACT_TOK         "BOOLEXTRACT"
-%token  ASSERT_TOK              "ASSERT"
-%token  QUERY_TOK               "QUERY"
-
-%token  BOOLEAN_TOK             "BOOLEAN"
-%token  ARRAY_TOK               "ARRAY"
-%token  OF_TOK                  "OF"
-%token  WITH_TOK                "WITH"
-
-%token  TRUELIT_TOK             "TRUE"
-%token  FALSELIT_TOK            "FALSE"
-
-%token  IN_TOK                  "IN"
-%token  LET_TOK                 "LET"
-//%token  COUNTEREXAMPLE_TOK      "COUNTEREXAMPLE"
-%token  PUSH_TOK                "PUSH"
-%token  POP_TOK                 "POP"
-
-%left IN_TOK
-%left XOR_TOK
-%left IFF_TOK
-%right IMPLIES_TOK
-%left OR_TOK
-%left AND_TOK
-%left NAND_TOK
-%left NOR_TOK
-%left NOT_TOK
-%left BVCONCAT_TOK
-%left BVOR_TOK
-%left BVAND_TOK
-%left BVXOR_TOK
-%left BVNAND_TOK
-%left BVNOR_TOK
-%left BVXNOR_TOK
-%left BVNEG_TOK
-%left BVLEFTSHIFT_TOK BVRIGHTSHIFT_TOK
-%left WITH_TOK
-
-%nonassoc '=' NEQ_TOK ASSIGN_TOK
-%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK
-%nonassoc BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK BVSX_TOK
-%nonassoc '[' 
-%nonassoc '{' '.' '('
-%nonassoc BV_TOK
-
-%type <vec>  Exprs FORM_IDs reverseFORM_IDs
-%type <vec>  Asserts 
-%type <node> Expr Formula IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr
-%type <Index_To_UpdateValue> Updates
-
-%type <indexvaluewidth>  BvType BoolType ArrayType Type 
-
-%token <node> BVCONST_TOK
-%token <node> TERMID_TOK FORMID_TOK COUNTEREXAMPLE_TOK
-%token <uintval> NUMERAL_TOK
-
-%%
-
-cmd             :      other_cmd
-                |      other_cmd counterexample
-                ; 
-
-counterexample  :      COUNTEREXAMPLE_TOK ';'
-                       {
-			 BEEV::print_counterexample = true;			 
-			 BEEV::globalBeevMgr_for_parser->PrintCounterExample(true);
-		       }                              
-                ;
-
-other_cmd       :      other_cmd1
-                |      Query 
-                       { 
-			 BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$1); 
-			 delete $1;
-		       }
-                |      VarDecls Query 
-                       { 
-			 BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$2); 
-			 delete $2;
-		       }
-                |      other_cmd1 Query
-                       {
-			 BEEV::ASTVec aaa = BEEV::globalBeevMgr_for_parser->GetAsserts();
-			 if(aaa.size() == 0)
-			   yyerror("Fatal Error: parsing:  GetAsserts() call: no assertions: ");
-			 if(aaa.size() == 1)
-			   BEEV::globalBeevMgr_for_parser->TopLevelSAT(aaa[0],*$2);
-			 else  		   
-			   BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,aaa),*$2);
-			 delete $2;
-		       }
-                ;
-
-other_cmd1      :     VarDecls Asserts
-                      {
-			delete $2;
-                      }                 
-                |     Asserts
-                      {
-			delete $1;
-		      }
-                |     other_cmd1 VarDecls Asserts
-                      {
-                        delete $3;
-                      }
-                ;
-
-/* push            :     PUSH_TOK */
-/*                       { */
-/* 			BEEV::globalBeevMgr_for_parser->Push(); */
-/*                       } */
-/*                 | */
-/*                 ; */
-
-/* pop             :     POP_TOK */
-/*                       { */
-/* 			BEEV::globalBeevMgr_for_parser->Pop(); */
-/*                       } */
-/*                 | */
-/*                 ; */
-
-Asserts         :      Assert 
-                       {
-			 $$ = new BEEV::ASTVec;
-			 $$->push_back(*$1);
-			 BEEV::globalBeevMgr_for_parser->AddAssert(*$1);
-			 delete $1;
-                       }
-                |      Asserts Assert
-                       {
-			 $1->push_back(*$2);
-			 BEEV::globalBeevMgr_for_parser->AddAssert(*$2);
-			 $$ = $1;
-			 delete $2;
-		       }
-                ;
-
-Assert          :      ASSERT_TOK Formula ';' { $$ = $2; }                
-                ;
-
-Query           :      QUERY_TOK Formula ';' { BEEV::globalBeevMgr_for_parser->AddQuery(*$2); $$ = $2;}
-                ; 
-
-
-/* Grammar for Variable Declaration */
-VarDecls	:      VarDecl ';'
-                       {
-                       }
-                |      VarDecls  VarDecl ';'
-                       {
-		       }
-		;
-
-VarDecl		:      FORM_IDs ':' Type 
-                       {
-			 for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {
-			   BEEV::_parser_symbol_table.insert(*i);
-			   i->SetIndexWidth($3.indexwidth);
-			   i->SetValueWidth($3.valuewidth);
-
-			   //FIXME: HACK_ATTACK. this vector was hacked into the code to
-			   //support a special request by Dawson' group. They want the
-			   //counterexample to be printed in the order of variables declared.
-			   BEEV::globalBeevMgr_for_parser->_special_print_set.push_back(*i);
-			 }
-			 delete $1;
-		       }
-                |      FORM_IDs ':' Type '=' Expr
-		       {
-			 //do type checking. if doesn't pass then abort
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-			 if($3.indexwidth != $5->GetIndexWidth())
-			   yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			 if($3.valuewidth != $5->GetValueWidth())
-			   yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			 
-			 for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {			   
-			   //set the valuewidth of the identifier
-			   i->SetValueWidth($5->GetValueWidth());
-			   i->SetIndexWidth($5->GetIndexWidth());
-			   
-			   BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5);
-			   delete $5;
-			 }
-		       }
-                |      FORM_IDs ':' Type '=' Formula
-                       {
-			 //do type checking. if doesn't pass then abort
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-			 if($3.indexwidth != $5->GetIndexWidth())
-			   yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			 if($3.valuewidth != $5->GetValueWidth())
-			   yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			 
-			 for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {			   
-			   //set the valuewidth of the identifier
-			   i->SetValueWidth($5->GetValueWidth());
-			   i->SetIndexWidth($5->GetIndexWidth());
-			   
-			   BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5);
-			   delete $5;
-			 }
-		       }                
-		;
-
-reverseFORM_IDs  :      FORMID_TOK
-                       {
-			 $$ = new BEEV::ASTVec;		        
-			 $$->push_back(*$1);
-			 delete $1;
-                       }
-                |      FORMID_TOK ',' reverseFORM_IDs
-                       {
-			 $3->push_back(*$1);
-			 $$ = $3;
-			 delete $1;
-                       }
-                ;
-
-FORM_IDs         :     reverseFORM_IDs
-                      {
-			$$ = new BEEV::ASTVec($1->rbegin(),$1->rend());
-			delete $1;
-                      }
-                ;
-
-/* Grammar for Types */
-Type		:      BvType { $$ = $1; }
-                |      BoolType { $$ = $1; }
-                |      ArrayType { $$ = $1; }
-		;		
-
-BvType          :      BV_TOK '(' NUMERAL_TOK ')' 
-                       {
-                         /*((indexwidth is 0) && (valuewidth>0)) iff type is BV*/
-			 $$.indexwidth = 0;
-			 unsigned int length = $3;
-			 if(length > 0) {
-			   $$.valuewidth = length;
-			 }
-			 else
-			  BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
-		       }
-                ;
-BoolType        :      BOOLEAN_TOK
-                       {
-			 $$.indexwidth = 0;
-			 $$.valuewidth = 0;
-		       }
-                ;
-ArrayType       :      ARRAY_TOK BvType OF_TOK BvType
-                       {
-			 $$.indexwidth = $2.valuewidth;
-			 $$.valuewidth = $4.valuewidth;
-		       }
-                ;
-
-/*Grammar for ITEs which are a type of Term*/
-IfExpr	        :      IF_TOK Formula THEN_TOK Expr ElseRestExpr 
-                       {
-			 unsigned int width = $4->GetValueWidth();
-			 if (width != $5->GetValueWidth())
-			   yyerror("Width mismatch in IF-THEN-ELSE");			 
-			 if($4->GetIndexWidth() != $5->GetIndexWidth())
-			   yyerror("Width mismatch in IF-THEN-ELSE");
-
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2);
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4);
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5));
-			 $$->SetIndexWidth($5->GetIndexWidth());
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$);
-			 delete $2;
-			 delete $4;
-			 delete $5;
-		      }
-		;
-
-ElseRestExpr	:      ELSE_TOK Expr ENDIF_TOK  { $$ = $2; }
-                |      ELSIF_TOK Expr THEN_TOK Expr ElseRestExpr 
-                       {
-			 unsigned int width = $2->GetValueWidth();
-			 if (width != $4->GetValueWidth() || width != $5->GetValueWidth())
-			   yyerror("Width mismatch in IF-THEN-ELSE");
-			 if ($2->GetIndexWidth() != $4->GetValueWidth() || $2->GetIndexWidth() != $5->GetValueWidth())
-			   yyerror("Width mismatch in IF-THEN-ELSE");
-
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2);
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4);
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);			
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5));
-			 $$->SetIndexWidth($5->GetIndexWidth());
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$);
-			 delete $2;
-			 delete $4;
-			 delete $5;
-		       }
-		;
-
-/* Grammar for formulas */
-Formula		:     '(' Formula ')' { $$ = $2; }
-		|      FORMID_TOK {  $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;}
-                |      BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')'
-                       {
-			 unsigned int width = $3->GetValueWidth();
-			 if(0 > (unsigned)$5 || width <= (unsigned)$5)
-			   yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range");
-			 
-			 BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
-			 BEEV::ASTNode low =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,1,*$3,hi,low));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0);			 
-			 BEEV::ASTNode * out = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ,*n,zero));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*out);
-
-			 $$ = out;
-			 delete $3;
-                       }
-                |      Expr '=' Expr 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-			 delete $3;
-		       } 
-		|      Expr NEQ_TOK Expr 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NEQ, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-			 delete $3;
-		       }
-		|      NOT_TOK Formula 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$2));
-			 delete $2;
-		       }
-		|      Formula OR_TOK Formula %prec OR_TOK 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       } 
-		|      Formula NOR_TOK Formula
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOR, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       } 
-		|      Formula AND_TOK Formula %prec AND_TOK 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       }
-		|      Formula NAND_TOK Formula
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NAND, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       }
-		|      Formula IMPLIES_TOK Formula
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       }
-		|      Formula IFF_TOK Formula
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       } 
-		|      Formula XOR_TOK Formula
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$1, *$3));
-			 delete $1;
-			 delete $3;
-		       } 
-	        |      BVLT_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVGT_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVLE_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVGE_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVSLT_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVSGT_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVSLE_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVSGE_TOK '(' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-		|      IfForm
-		|      TRUELIT_TOK 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); 
-			 $$->SetIndexWidth(0); 
-			 $$->SetValueWidth(0);
-                       }
-		|      FALSELIT_TOK 
-                       { 
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); 
-			 $$->SetIndexWidth(0); 
-			 $$->SetValueWidth(0);
-		       }
-
-                |      LET_TOK LetDecls IN_TOK Formula
-                       {
-			 $$ = $4;
-			 //Cleanup the LetIDToExprMap
-			 BEEV::globalBeevMgr_for_parser->CleanupLetIDMap();
-		       }
-                ;
-
-/*Grammar for ITEs which are Formulas */
-IfForm	        :      IF_TOK Formula THEN_TOK Formula ElseRestForm 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5));
-			 delete $2;
-			 delete $4;
-			 delete $5;
-		      }
-		;
-
-ElseRestForm	:      ELSE_TOK Formula ENDIF_TOK  { $$ = $2; }
-                |      ELSIF_TOK Formula THEN_TOK Formula ElseRestForm 
-                       {
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5));
-			 delete $2;
-			 delete $4;
-			 delete $5;
-		       }
-		;
-
-/*Grammar for a list of expressions*/
-Exprs		:      Expr 
-                       {
-			 $$ = new BEEV::ASTVec;
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$1);
-			 $$->push_back(*$1);
-			 delete $1;
-		       }
-                |      Exprs ',' Expr 
-                       {
-			 $1->push_back(*$3);
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-			 $$ = $1; 
-			 delete $3;
-		       }
-		;
-
-/* Grammar for Expr */
-Expr		:      TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;}
-                |      '(' Expr ')' { $$ = $2; }
-	        |      BVCONST_TOK { $$ = $1; }
-                |      BOOL_TO_BV_TOK '(' Formula ')'		
-                       {
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-			 BEEV::ASTNode one = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,1);
-			 BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0);
-
-			 //return ITE(*$3, length(1), 0bin1, 0bin0)
-			 $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,1,*$3,one,zero));
-			 delete $3;
-                       }
-		|      Expr '[' Expr ']' 
-                       {			 
-			 // valuewidth is same as array, indexwidth is 0.
-			 unsigned int width = $1->GetValueWidth();
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $1;
-			 delete $3;
-		       }
-                |      Expr '(' Expr ')' //array read but in the form of a uninterpreted function application
-                       {
-			 // valuewidth is same as array, indexwidth is 0.
-			 unsigned int width = $1->GetValueWidth();
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $1;
-			 delete $3;
-		       }
-	        |      Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']' 
-                       {
-			 int width = $3 - $5 + 1;
-			 if (width < 0)
-			   yyerror("Negative width in extract");
-			 
-			 if((unsigned)$3 >= $1->GetValueWidth() || (unsigned)$5 < 0)
-			   yyerror("Parsing: Wrong width in BVEXTRACT\n");			 
-
-			 BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3);
-			 BEEV::ASTNode low =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$1,hi,low));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-		       }
-	        |      BVNEG_TOK Expr 
-                       {
-			 unsigned int width = $2->GetValueWidth();
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNEG, width, *$2));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $2;
-		       }
-	        |      Expr BVAND_TOK Expr 
-                       {
-			 unsigned int width = $1->GetValueWidth();
-			 if (width != $3->GetValueWidth()) {
-			   yyerror("Width mismatch in AND");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-			 delete $3;
-		       }
-	        |      Expr BVOR_TOK Expr 
-                       {
-			 unsigned int width = $1->GetValueWidth();
-			 if (width != $3->GetValueWidth()) {
-			   yyerror("Width mismatch in OR");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$1, *$3)); 
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-			 delete $3;
-		       }
-	        |      BVXOR_TOK '(' Expr ',' Expr ')' 
-                       {
-			 unsigned int width = $3->GetValueWidth();
-			 if (width != $5->GetValueWidth()) {
-			   yyerror("Width mismatch in XOR");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVNAND_TOK '(' Expr ',' Expr ')' 
-                       {
-			 unsigned int width = $3->GetValueWidth();
-			 if (width != $5->GetValueWidth()) {
-			   yyerror("Width mismatch in NAND");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $3;
-			 delete $5;
-		       }
-                |      BVNOR_TOK '(' Expr ',' Expr ')' 
-                       {
-			 unsigned int width = $3->GetValueWidth();
-			 if (width != $5->GetValueWidth()) {
-			   yyerror("Width mismatch in NOR");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $3;
-			 delete $5;
-		       }
-	        |      BVXNOR_TOK '(' Expr ',' Expr ')' 
-                       {
-			 unsigned int width = $3->GetValueWidth();
-			 if (width != $5->GetValueWidth()) {
-			   yyerror("Width mismatch in NOR");
-			 }
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXNOR, width, *$3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $3;
-			 delete $5;
-		       }
-                |      BVSX_TOK '(' Expr ',' NUMERAL_TOK ')' 
-                       {
-			 //width of the expr which is being sign
-			 //extended. $5 is the resulting length of the
-			 //signextended expr
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-			 if($3->GetValueWidth() == $5) {
-			   $$ = $3;
-			 }
-			 else {
-			   BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$5);
-			   BEEV::ASTNode *n =  
-			     new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX, $5,*$3,width));
-			   BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			   $$ = n;
-			   delete $3;
-			 }
-		       }
-	        |      Expr BVCONCAT_TOK Expr 
-                       {
-			 unsigned int width = $1->GetValueWidth() + $3->GetValueWidth();
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$1, *$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 
-			 delete $1;
-			 delete $3;
-		       }
-                |      Expr BVLEFTSHIFT_TOK NUMERAL_TOK 
-                       {
-			 BEEV::ASTNode zero_bits = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3);
-			 BEEV::ASTNode * n = 
-			   new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,
-											$1->GetValueWidth() + $3, *$1, zero_bits));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $1;
-                       }
-                |      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK 
-                       {
-			 BEEV::ASTNode len = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3);
-			 unsigned int w = $1->GetValueWidth();
-
-			 //the amount by which you are rightshifting
-			 //is less-than/equal-to the length of input
-			 //bitvector
-			 if((unsigned)$3 < w) {
-			   BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1);
-			   BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$3);
-			   BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$1,hi,low);
-			   BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,len, extract));
-			   BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			   $$ = n;
-			 } 
-			 else
-			   $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateZeroConst(w));			 
-
-			 delete $1;
-                       }
-                |      BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, $3, *$5));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-                       }
-                |      BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-			 delete $7;
-                       }
-                |      BVUMINUS_TOK '(' Expr ')' 
-                       {
-			 unsigned width = $3->GetValueWidth();
-			 BEEV::ASTNode * n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$3));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $3;
-                       }
-                |      BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-			 delete $7;
-		       }
-                |      BVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVDIV, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-			 delete $7;
-		       }
-                |      BVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMOD, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-			 delete $7;
-		       }
-                |      SBVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVDIV, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-
-			 delete $5;
-			 delete $7;
-		       }
-                |      SBVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' 
-                       {
-			 BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVMOD, $3, *$5, *$7));
-			 BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-			 $$ = n;
-			 delete $5;
-			 delete $7;
-		       }        
-		|      IfExpr { $$ = $1; }
-                |      ArrayUpdateExpr
-                |      LET_TOK LetDecls IN_TOK Expr
-                       {
-			 $$ = $4;
-			 //Cleanup the LetIDToExprMap
-			 //BEEV::globalBeevMgr_for_parser->CleanupLetIDMap();
-		       }
-		;
-
-/*Grammar for Array Update Expr*/
-ArrayUpdateExpr : Expr WITH_TOK Updates
-                  {
-		    BEEV::ASTNode * result;
-		    unsigned int width = $1->GetValueWidth();
-
-		    BEEV::ASTNodeMap::iterator it = $3->begin();
-		    BEEV::ASTNodeMap::iterator itend = $3->end();
-		    result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE,
-							      width,
-							      *$1,
-							      (*it).first,
-							      (*it).second));
-		    result->SetIndexWidth($1->GetIndexWidth());
-		    BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result);
-		    for(it++;it!=itend;it++) {
-		      result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE,
-								width,
-								*result,
-								(*it).first,
-								(*it).second));
-		      result->SetIndexWidth($1->GetIndexWidth());
-		      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result);
-		    }
-		    BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result);
-		    $$ = result;
-		    delete $3;
-                  }
-                ;
-
-Updates         : '[' Expr ']' ASSIGN_TOK Expr 
-                  {
-		    $$ = new BEEV::ASTNodeMap();
-		    (*$$)[*$2] = *$5;		    
-                  }
-                | Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr 
-                  {		    
-		    (*$1)[*$4] = *$7;
-                  }
-                ;
-
-/*Grammar for LET Expr*/
-LetDecls	:	LetDecl 
-		|	LetDecls ',' LetDecl 
-		;
-
-LetDecl		:	FORMID_TOK '=' Expr 
-                        {
-			  //Expr must typecheck
-			  BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-
-			  //set the valuewidth of the identifier
-			  $1->SetValueWidth($3->GetValueWidth());
-			  $1->SetIndexWidth($3->GetIndexWidth());
-
-			  //populate the hashtable from LET-var -->
-			  //LET-exprs and then process them:
-			  //
-			  //1. ensure that LET variables do not clash
-			  //1. with declared variables.
-			  //
-			  //2. Ensure that LET variables are not
-			  //2. defined more than once
-			  BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3);
-			  delete $1;
-			  delete $3;
-			}
-                |	FORMID_TOK ':' Type '=' Expr
-			{
-			  //do type checking. if doesn't pass then abort
-			  BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-			  
-			  if($3.indexwidth != $5->GetIndexWidth())
-			    yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			  if($3.valuewidth != $5->GetValueWidth())
-			    yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-
-			  //set the valuewidth of the identifier
-			  $1->SetValueWidth($5->GetValueWidth());
-			  $1->SetIndexWidth($5->GetIndexWidth());
-
-			  BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5);
-			  delete $1;
-			  delete $5;
-			}
-                |       FORMID_TOK '=' Formula
-                        {
-			  //Expr must typecheck
-			  BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-
-			  //set the valuewidth of the identifier
-			  $1->SetValueWidth($3->GetValueWidth());
-			  $1->SetIndexWidth($3->GetIndexWidth());
-
-			  //Do LET-expr management
-			  BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3);
-			  delete $1;
-			  delete $3;
-			}
-                |	FORMID_TOK ':' Type '=' Formula
-			{
-			  //do type checking. if doesn't pass then abort
-			  BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-
-			  if($3.indexwidth != $5->GetIndexWidth())
-			    yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-			  if($3.valuewidth != $5->GetValueWidth())
-			    yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
-
-			  //set the valuewidth of the identifier
-			  $1->SetValueWidth($5->GetValueWidth());
-			  $1->SetIndexWidth($5->GetIndexWidth());
-
-			  //Do LET-expr management
-			  BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5);
-			  delete $1;
-			  delete $5;
-			}                
-		;
-
-%%
diff --git a/stp/parser/let-funcs.cpp b/stp/parser/let-funcs.cpp
deleted file mode 100644
index 1de10492..00000000
--- a/stp/parser/let-funcs.cpp
+++ /dev/null
@@ -1,85 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include "../AST/AST.h"
-#include <stdlib.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
-  //
-  //1. if the Let-var is already defined in the LET scope, then the
-  //1. function returns an error.
-  //
-  //2. if the Let-var is already declared variable in the input, then
-  //2. the function returns an error
-  //
-  //3. otherwise add the <var,letExpr> pair to the _letid_expr table.
-  void BeevMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) {
-    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 in this LET scope: v =", var);
-    }
-
-    if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) {
-      FatalError("LetExprMgr:This var is already declared. cannot redeclare as a letvar: v =", var);
-    }
-
-    _letid_expr_map[var] = letExpr;   
-  }
-
-  //this function looksup the "var to letexpr map" and returns the
-  //corresponding letexpr. if there is no letexpr, then it simply
-  //returns the var.
-  ASTNode BeevMgr::ResolveID(const ASTNode& v) {
-    if(v.GetKind() != SYMBOL) {
-      return v;
-    }
-
-    if(_parser_symbol_table.find(v) != _parser_symbol_table.end()) {
-      return v;
-    }
-
-    ASTNodeMap::iterator it;
-    if((it =_letid_expr_map.find(v)) != _letid_expr_map.end()) {
-      if(it->second == ASTUndefined) 
-	FatalError("Unresolved Identifier: ",v);
-      else
-	return it->second;
-    }
-
-    //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
-    //'v' is undefined. 
-    //
-    //declared variables also get stored in this map, but there value
-    //is ASTUndefined. This is really a hack. I don't know how to get
-    //rid of this hack.
-    _letid_expr_map[v] = ASTUndefined;
-    return v;    
-  }
-  
-  // This function simply cleans up the LetID -> LetExpr Map.   
-  void BeevMgr::CleanupLetIDMap(void) { 
-    ASTNodeMap::iterator it = _letid_expr_map.begin();
-    ASTNodeMap::iterator itend = _letid_expr_map.end();
-    for(;it!=itend;it++) {
-      if(it->second != ASTUndefined) {
-	it->first.SetValueWidth(0);
-	it->first.SetIndexWidth(0);
-      }
-    }
-    _letid_expr_map.clear();
-  }
-};
diff --git a/stp/parser/main.cpp b/stp/parser/main.cpp
deleted file mode 100644
index ed251ed3..00000000
--- a/stp/parser/main.cpp
+++ /dev/null
@@ -1,181 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <algorithm>
-#include <ctime>
-#include <unistd.h>
-#include <signal.h>
-//#include <zlib.h>
-#include <stdio.h>
-#include "../AST/AST.h"
-#include "parsePL_defs.h"
-#include "../sat/Solver.h"
-#include "../sat/SolverTypes.h"
-#include "../sat/VarOrder.h"
-
-#include <unistd.h>
-
-#ifdef EXT_HASH_MAP
-  using namespace __gnu_cxx;
-#endif
-
-/* GLOBAL FUNCTION: parser
- */
-extern int yyparse();
-//extern int smtlibparse();
-
-/* GLOBAL VARS: Some global vars for the Main function.
- *
- */
-const char * prog = "stp";
-int linenum  = 1;
-const char * usage = "Usage: %s [-option] [infile]\n";
-std::string helpstring = "\n\n";
-
-// Amount of memory to ask for at beginning of main.
-static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
-
-// Used only in smtlib lexer/parser
-BEEV::ASTNode SingleBitOne;
-BEEV::ASTNode SingleBitZero;
-
-/******************************************************************************
- * MAIN FUNCTION: 
- *
- * step 0. Parse the input into an ASTVec.
- * step 1. Do BV Rewrites
- * step 2. Bitblasts the ASTNode.
- * step 3. Convert to CNF
- * step 4. Convert to SAT
- * step 5. Call SAT to determine if input is SAT or UNSAT
- ******************************************************************************/
-int main(int argc, char ** argv) {
-  char * infile;
-  extern FILE *yyin;
-
-  // Grab some memory from the OS upfront to reduce system time when individual
-  // hash tables are being allocated
-
-  if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) {
-    // FIXME: figure out how to get and print the real error message.
-    BEEV::FatalError("Initial allocation of memory failed.");
-  }
-  
-  //populate the help string
-  helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
-  helpstring +=  "-w  : switch wordlevel solver off (optimizations are ON by default)\n";
-  helpstring +=  "-a  : switch optimizations off (optimizations are ON by default)\n";
-  helpstring +=  "-s  : print function statistics\n";
-  helpstring +=  "-v  : print nodes \n";
-  helpstring +=  "-c  : construct counterexample\n";
-  helpstring +=  "-d  : check counterexample\n";
-  helpstring +=  "-p  : print counterexample\n";
-  helpstring +=  "-x  : flatten nested XORs\n";
-  helpstring +=  "-h  : help\n";
-
-  for(int i=1; i < argc;i++) {
-    if(argv[i][0] == '-')
-      switch(argv[i][1]) {
-      case 'a' :
-	BEEV::optimize = false;
-	BEEV::wordlevel_solve = false;
-	break;
-      case 'b':
-	BEEV::print_STPinput_back = true;
-	break;
-      case 'c':
-	BEEV::construct_counterexample = true;
-	break;
-      case 'd':
-	BEEV::construct_counterexample = true;
-	BEEV::check_counterexample = true;
-	break;
-      case 'e':
-	BEEV::variable_activity_optimize = true;
-	break;
-      case 'f':
-	BEEV::smtlib_parser_enable = true;
-	break;
-      case 'h':
-	fprintf(stderr,usage,prog);
-	cout << helpstring;
-	//BEEV::FatalError("");
-	return -1;
-	break;
-      case 'l' :
-	BEEV::linear_search = true;
-	break;
-      case 'n':
-	BEEV::print_output = true;
-	break;
-      case 'p':
-	BEEV::print_counterexample = true;
-	break;
-      case 'q':
-	BEEV::print_arrayval_declaredorder = true;
-	break;
-      case 'r':
-	BEEV::arrayread_refinement = false;
-	break;
-      case 's' :
-	BEEV::stats = true;
-	break;
-      case 'u':
-	BEEV::arraywrite_refinement = false;
-	break;
-      case 'v' :
-	BEEV::print_nodes = true;
-	break;
-      case 'w':
-	BEEV::wordlevel_solve = false;
-	break;
-      case 'x':
-	BEEV::xor_flatten = true;
-	break;
-      case 'z':
-	BEEV::print_sat_varorder = true;
-	break;
-      default:
-	fprintf(stderr,usage,prog);
-	cout << helpstring;
-	//BEEV::FatalError("");
-	return -1;
-	break;
-      }
-    else {
-      infile = argv[i];
-      yyin = fopen(infile,"r");
-      if(yyin == NULL) {
-	fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
-	BEEV::FatalError("");
-      }
-    }
-  }
-
-#ifdef NATIVE_C_ARITH
-#else
-  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); 
-  if(0 != c) {
-    cout << CONSTANTBV::BitVector_Error(c) << endl;
-    return 0;
-  }
-#endif           
-
-  //want to print the output always from the commandline. 
-  BEEV::print_output = true;
-  BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr();  
-
-  SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1);
-  SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1);
-  //BEEV::smtlib_parser_enable = true;
-  yyparse();
-}//end of Main
diff --git a/stp/parser/smtlib.lex b/stp/parser/smtlib.lex
deleted file mode 100644
index a03ae94e..00000000
--- a/stp/parser/smtlib.lex
+++ /dev/null
@@ -1,232 +0,0 @@
-%{
-  /********************************************************************
-   * AUTHORS: Vijay Ganesh, David L. Dill
-   *
-   * BEGIN DATE: July, 2006
-   *
-   * This file is modified version of the CVCL's smtlib.lex file. Please
-   * see CVCL license below
-   ********************************************************************/
-  
-  /********************************************************************
-   * \file smtlib.lex
-   * 
-   * Author: Sergey Berezin, Clark Barrett
-   * 
-   * Created: Apr 30 2005
-   *
-   * <hr>
-   * Copyright (C) 2004 by the Board of Trustees of Leland Stanford
-   * Junior University and by New York University. 
-   *
-   * License to use, copy, modify, sell and/or distribute this software
-   * and its documentation for any purpose is hereby granted without
-   * royalty, subject to the terms and conditions defined in the \ref
-   * LICENSE file provided with this distribution.  In particular:
-   *
-   * - The above copyright notice and this permission notice must appear
-   * in all copies of the software and related documentation.
-   *
-   * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
-   * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
-   * 
-   * <hr>
-   ********************************************************************/
-  // -*- c++ -*-
-#include <iostream>
-#include "../AST/AST.h"
-#include "parsePL_defs.h"
-  
-  extern char *yytext;
-  extern int yyerror (char *msg);
-  
-  // File-static (local to this file) variables and functions
-  static std::string _string_lit;
-  
-  static char escapeChar(char c) {
-    switch(c) {
-    case 'n': return '\n';
-    case 't': return '\t';
-    default: return c;
-    }
-  }      
-
-  extern BEEV::ASTNode SingleBitOne;
-  extern BEEV::ASTNode SingleBitZero;
-
-/* Changed for smtlib speedup */
-/* bv{DIGIT}+      { yylval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(yytext+2, 10)); return BVCONST_TOK;} */
-
-%}
-
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
-%x	COMMENT
-%x	STRING_LITERAL
-%x      USER_VALUE
-
-LETTER	([a-zA-Z])
-DIGIT	([0-9])
-OPCHAR	(['\.\_]) 
-ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
-
-%%
-[ \n\t\r\f]	{ /* sk'ip whitespace */ }
-{DIGIT}+	{ yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; }
-
-
-bv{DIGIT}+	{ yylval.ullval = strtoull(yytext+2, NULL, 10); return BVCONST_TOK; }
-
-bit{DIGIT}+     {
-  		   char c = yytext[3];
-		   if (c == '1') {
-		     yylval.node = new BEEV::ASTNode(SingleBitOne);
-		   }
-		   else {
-		     yylval.node = new BEEV::ASTNode(SingleBitZero);
-		   }
-		   return BITCONST_TOK;
-		};
-
-
-";"		{ BEGIN COMMENT; }
-<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */}
-<COMMENT>.	{ /* stay in comment mode */ }
-
-<INITIAL>"\""		{ BEGIN STRING_LITERAL;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<STRING_LITERAL>"\\".	{ /* escape characters (like \n or \") */
-                          _string_lit.insert(_string_lit.end(),
-                                             escapeChar(yytext[1])); }
-<STRING_LITERAL>"\""	{ BEGIN INITIAL; /* return to normal mode */
-			  yylval.str = new std::string(_string_lit);
-                          return STRING_TOK; }
-<STRING_LITERAL>.	{ _string_lit.insert(_string_lit.end(),*yytext); }
-
-
-<INITIAL>"{"		{ BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<USER_VALUE>"\\"[{}] { /* escape characters */
-                          _string_lit.insert(_string_lit.end(),yytext[1]); }
-
-<USER_VALUE>"}"	        { BEGIN INITIAL; /* return to normal mode */
-			  yylval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');}
-<USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*yytext); }
-
-"BitVec"        { return BITVEC_TOK;}
-"Array"         { return ARRAY_TOK;}
-"true"          { return TRUE_TOK; }
-"false"         { return FALSE_TOK; }
-"not"           { return NOT_TOK; }
-"implies"       { return IMPLIES_TOK; }
-"ite"           { return ITE_TOK;}
-"if_then_else"  { return IF_THEN_ELSE_TOK; }
-"and"           { return AND_TOK; }
-"or"            { return OR_TOK; }
-"xor"           { return XOR_TOK; }
-"iff"           { return IFF_TOK; }
-"let"           { return LET_TOK; }
-"flet"          { return FLET_TOK; }
-"notes"         { return NOTES_TOK; }
-"cvc_command"   { return CVC_COMMAND_TOK; }
-"sorts"         { return SORTS_TOK; }
-"funs"          { return FUNS_TOK; }
-"preds"         { return PREDS_TOK; }
-"extensions"    { return EXTENSIONS_TOK; }
-"definition"    { return DEFINITION_TOK; }
-"axioms"        { return AXIOMS_TOK; }
-"logic"         { return LOGIC_TOK; }
-"sat"           { return SAT_TOK; }
-"unsat"         { return UNSAT_TOK; }
-"unknown"       { return UNKNOWN_TOK; }
-"assumption"    { return ASSUMPTION_TOK; }
-"formula"       { return FORMULA_TOK; }
-"status"        { return STATUS_TOK; }
-"difficulty"    { return DIFFICULTY_TOK; }
-"benchmark"     { return BENCHMARK_TOK; }
-"source"        { return SOURCE_TOK;}
-"category"      { return CATEGORY_TOK;} 
-"extrasorts"    { return EXTRASORTS_TOK; }
-"extrafuns"     { return EXTRAFUNS_TOK; }
-"extrapreds"    { return EXTRAPREDS_TOK; }
-"language"      { return LANGUAGE_TOK; }
-"distinct"      { return DISTINCT_TOK; }
-"select"        { return SELECT_TOK; }
-"store"         { return STORE_TOK; }
-":"             { return COLON_TOK; }
-"\["            { return LBRACKET_TOK; }
-"\]"            { return RBRACKET_TOK; }
-"("             { return LPAREN_TOK; }
-")"             { return RPAREN_TOK; }
-"$"             { return DOLLAR_TOK; }
-"?"             { return QUESTION_TOK; }
-"="             {return EQ_TOK;}
-
-"nand"		{ return NAND_TOK;}
-"nor"		{ return NOR_TOK;}
-"/="		{ return NEQ_TOK; }
- ":="           { return ASSIGN_TOK;}
-"shift_left0"   { return BVLEFTSHIFT_TOK;}
-"bvshl"         { return BVLEFTSHIFT_1_TOK;}
-"shift_right0"  { return BVRIGHTSHIFT_TOK;}
-"bvlshr"        { return BVRIGHTSHIFT_1_TOK;}
-"bvadd"         { return BVPLUS_TOK;}
-"bvsub"         { return BVSUB_TOK;}
-"bvnot"         { return BVNOT_TOK;}
-"bvmul"         { return BVMULT_TOK;}
-"bvdiv"         { return BVDIV_TOK;}
-"bvmod"         { return BVMOD_TOK;}
-"bvneg"         { return BVNEG_TOK;}
-"bvand"         { return BVAND_TOK;}
-"bvor"          { return BVOR_TOK;}
-"bvxor"         { return BVXOR_TOK;}
-"bvnand"        { return BVNAND_TOK;}
-"bvnor"         { return BVNOR_TOK;}
-"bvxnor"        { return BVXNOR_TOK;}
-"concat"        { return BVCONCAT_TOK;}
-"extract"       { return BVEXTRACT_TOK;}
-"bvlt"          { return BVLT_TOK;}
-"bvgt"          { return BVGT_TOK;}
-"bvleq"         { return BVLE_TOK;}
-"bvgeq"         { return BVGE_TOK;}
-"bvult"         { return BVLT_TOK;}
-"bvugt"         { return BVGT_TOK;}
-"bvuleq"        { return BVLE_TOK;}
-"bvugeq"        { return BVGE_TOK;}
-"bvule"         { return BVLE_TOK;}
-"bvuge"         { return BVGE_TOK;}
-
-"bvslt"         { return BVSLT_TOK;}
-"bvsgt"         { return BVSGT_TOK;}
-"bvsleq"        { return BVSLE_TOK;}
-"bvsgeq"        { return BVSGE_TOK;}
-"bvsle"         { return BVSLE_TOK;}
-"bvsge"         { return BVSGE_TOK;}
-
-"sign_extend"   { return BVSX_TOK;} 
-"boolextract"   { return BOOLEXTRACT_TOK;}
-"boolbv"        { return BOOL_TO_BV_TOK;}
-
-(({LETTER})|(_)({ANYTHING}))({ANYTHING})*	{
-  BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); 
-
-  // 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.  
-  yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr));
-  //yylval.node = new BEEV::ASTNode(nptr);
-  if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE)
-    return FORMID_TOK;
-  else 
-    return TERMID_TOK;  
-}
-. { yyerror("Illegal input character."); }
-%%
diff --git a/stp/parser/smtlib.y b/stp/parser/smtlib.y
deleted file mode 100644
index 0aa22dee..00000000
--- a/stp/parser/smtlib.y
+++ /dev/null
@@ -1,1036 +0,0 @@
-%{
-  /********************************************************************
-   * AUTHORS: Vijay Ganesh, David L. Dill
-   *
-   * BEGIN DATE: July, 2006
-   *
-   * This file is modified version of the CVCL's smtlib.y file. Please
-   * see CVCL license below
-   ********************************************************************/
-  
-  /********************************************************************
-   *
-   * \file smtlib.y
-   * 
-   * Author: Sergey Berezin, Clark Barrett
-   * 
-   * Created: Apr 30 2005
-   *
-   * <hr>
-   * Copyright (C) 2004 by the Board of Trustees of Leland Stanford
-   * Junior University and by New York University. 
-   *
-   * License to use, copy, modify, sell and/or distribute this software
-   * and its documentation for any purpose is hereby granted without
-   * royalty, subject to the terms and conditions defined in the \ref
-   * LICENSE file provided with this distribution.  In particular:
-   *
-   * - The above copyright notice and this permission notice must appear
-   * in all copies of the software and related documentation.
-   *
-   * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
-   * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
-   * 
-   * <hr>
-   ********************************************************************/
-  // -*- c++ -*-
-
-#include "../AST/AST.h"
-  using namespace std; 
-  
-  // Suppress the bogus warning suppression in bison (it generates
-  // compile error)
-#undef __GNUC_MINOR__
-  
-  extern char* yytext;
-  extern int yylineno;
-  
-  //int yylineno;
-
-  extern int yylex(void);
-
-  int yyerror(char *s) {
-    //yylineno = 0;
-    cout << "syntax error: line " << yylineno << "\n" << s << endl;
-    cout << "  token: " << yytext << endl;
-    BEEV::FatalError("");
-    return 1;
-  }
-
-  BEEV::ASTNode query;
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 104857600
-#define YYERROR_VERBOSE 1
-#define YY_EXIT_FAILURE -1
-%}
-
-%union {  
-  // FIXME: Why is this not an UNSIGNED int?
-  int uintval;			/* for numerals in types. */
-
-  // for BV32 BVCONST 
-  unsigned long long ullval;
-
-  struct {
-    //stores the indexwidth and valuewidth
-    //indexwidth is 0 iff type is bitvector. positive iff type is
-    //array, and stores the width of the indexing bitvector
-    unsigned int indexwidth;
-    //width of the bitvector type
-    unsigned int valuewidth;
-  } indexvaluewidth;
-
-  //ASTNode,ASTVec
-  BEEV::ASTNode *node;
-  BEEV::ASTVec *vec;
-  std::string *str;
-};
-
-%start cmd
-
-%type <indexvaluewidth> sort_symb sort_symbs
-%type <node> status
-%type <vec> bench_attributes an_formulas
-
-%type <node> benchmark bench_name bench_attribute
-%type <node> an_term an_nonbvconst_term an_formula 
-
-%type <node> var fvar logic_name
-%type <str> user_value
-
-%token <uintval> NUMERAL_TOK
-%token <ullval> BVCONST_TOK
-%token <node> BITCONST_TOK
-%token <node> FORMID_TOK TERMID_TOK 
-%token <str> STRING_TOK
-%token <str> USER_VAL_TOK
-%token SOURCE_TOK
-%token CATEGORY_TOK
-%token DIFFICULTY_TOK
-%token BITVEC_TOK
-%token ARRAY_TOK
-%token SELECT_TOK
-%token STORE_TOK
-%token TRUE_TOK
-%token FALSE_TOK
-%token NOT_TOK
-%token IMPLIES_TOK
-%token ITE_TOK
-%token IF_THEN_ELSE_TOK
-%token AND_TOK
-%token OR_TOK
-%token XOR_TOK
-%token IFF_TOK
-%token EXISTS_TOK
-%token FORALL_TOK
-%token LET_TOK
-%token FLET_TOK
-%token NOTES_TOK
-%token CVC_COMMAND_TOK
-%token SORTS_TOK
-%token FUNS_TOK
-%token PREDS_TOK
-%token EXTENSIONS_TOK
-%token DEFINITION_TOK
-%token AXIOMS_TOK
-%token LOGIC_TOK
-%token COLON_TOK
-%token LBRACKET_TOK
-%token RBRACKET_TOK
-%token LPAREN_TOK
-%token RPAREN_TOK
-%token SAT_TOK
-%token UNSAT_TOK
-%token UNKNOWN_TOK
-%token ASSUMPTION_TOK
-%token FORMULA_TOK
-%token STATUS_TOK
-%token BENCHMARK_TOK
-%token EXTRASORTS_TOK
-%token EXTRAFUNS_TOK
-%token EXTRAPREDS_TOK
-%token LANGUAGE_TOK
-%token DOLLAR_TOK
-%token QUESTION_TOK
-%token DISTINCT_TOK
-%token SEMICOLON_TOK
-%token EOF_TOK
-%token EQ_TOK
-/*BV SPECIFIC TOKENS*/
-%token NAND_TOK
-%token NOR_TOK
-%token NEQ_TOK
-%token ASSIGN_TOK
-%token BV_TOK
-%token BOOLEAN_TOK
-%token BVLEFTSHIFT_TOK
-%token BVLEFTSHIFT_1_TOK
-%token BVRIGHTSHIFT_TOK
-%token BVRIGHTSHIFT_1_TOK
-%token BVPLUS_TOK
-%token BVSUB_TOK
-%token BVNOT_TOK //bvneg in CVCL
-%token BVMULT_TOK
-%token BVDIV_TOK
-%token BVMOD_TOK
-%token BVNEG_TOK //bvuminus in CVCL
-%token BVAND_TOK
-%token BVOR_TOK
-%token BVXOR_TOK
-%token BVNAND_TOK
-%token BVNOR_TOK
-%token BVXNOR_TOK
-%token BVCONCAT_TOK
-%token BVLT_TOK
-%token BVGT_TOK
-%token BVLE_TOK
-%token BVGE_TOK
-%token BVSLT_TOK
-%token BVSGT_TOK
-%token BVSLE_TOK
-%token BVSGE_TOK
-%token BVSX_TOK 
-%token BOOLEXTRACT_TOK
-%token BOOL_TO_BV_TOK
-%token BVEXTRACT_TOK
-
-%left LBRACKET_TOK RBRACKET_TOK
-
-%%
-
-cmd:
-    benchmark
-    {
-      if($1 != NULL) {
-	BEEV::globalBeevMgr_for_parser->TopLevelSAT(*$1,query);
-	delete $1;
-      }
-      YYACCEPT;
-    }
-;
-
-benchmark:
-    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
-    {
-      if($4 != NULL){
-	if($4->size() > 1) 
-	  $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,*$4));
-	else
-	  $$ = new BEEV::ASTNode((*$4)[0]);	  
-	delete $4;
-      }
-      else {
-	$$ = NULL;
-      }
-    }
-/*   | EOF_TOK */
-/*     { */
-/*     } */
-;
-
-bench_name:
-    FORMID_TOK
-    {
-    }
-;
-
-bench_attributes:
-    bench_attribute
-    {
-      $$ = new BEEV::ASTVec;
-      if ($1 != NULL) {
-	$$->push_back(*$1);
-	BEEV::globalBeevMgr_for_parser->AddAssert(*$1);
-	delete $1;
-      }
-    }
-  | bench_attributes bench_attribute
-    {
-      if ($1 != NULL && $2 != NULL) {
-	$1->push_back(*$2);
-	BEEV::globalBeevMgr_for_parser->AddAssert(*$2);
-	$$ = $1;
-	delete $2;
-      }
-    }
-;
-
-bench_attribute:
-    COLON_TOK ASSUMPTION_TOK an_formula
-    {
-      //assumptions are like asserts
-      $$ = $3;
-    }
-  | COLON_TOK FORMULA_TOK an_formula
-    {
-      //the query
-      query = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT,*$3);
-      BEEV::globalBeevMgr_for_parser->AddQuery(query);
-      //dummy true
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE));
-      
-      
-    }
-  | COLON_TOK STATUS_TOK status
-    {
-      $$ = NULL;
-    }
-  | COLON_TOK LOGIC_TOK logic_name
-    {
-      if (!(0 == strcmp($3->GetName(),"QF_UFBV")  ||
-            0 == strcmp($3->GetName(),"QF_AUFBV"))) {
-	yyerror("Wrong input logic:");
-      }
-      $$ = NULL;
-    }
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK var_decls RPAREN_TOK
-    {
-      $$ = NULL;
-    }
-  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK
-    {
-      $$ = NULL;
-    }
-  | annotation 
-    {
-      $$ = NULL;
-    }
-;
-
-logic_name:
-    FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = $1;
-    }
-  | FORMID_TOK
-    {
-      $$ = $1;
-    }
-;
-
-status:
-    SAT_TOK { $$ = NULL; }
-  | UNSAT_TOK { $$ = NULL; }
-  | UNKNOWN_TOK { $$ = NULL; }
-;
-
-
-/* annotations: */
-/*     annotation */
-/*     { */
-/*     } */
-/*   | annotations annotation */
-/*     { */
-/*     } */
-/*   ; */
-  
-annotation:
-    attribute 
-    {
-    }
-  | attribute user_value 
-    {
-    }
-;
-
-user_value:
-    USER_VAL_TOK
-    {
-      //cerr << "Printing user_value: " << *$1 << endl;
-    }
-;
-
-attribute:
-    COLON_TOK SOURCE_TOK
-    {
-    }
-   | COLON_TOK CATEGORY_TOK
-    {
-    }
-   | COLON_TOK DIFFICULTY_TOK 
-;
-
-sort_symbs:
-    sort_symb 
-    {
-      //a single sort symbol here means either a BitVec or a Boolean
-      $$.indexwidth = $1.indexwidth;
-      $$.valuewidth = $1.valuewidth;
-    }
-  | sort_symb sort_symb
-    {
-      //two sort symbols mean f: type --> type
-      $$.indexwidth = $1.valuewidth;
-      $$.valuewidth = $2.valuewidth;
-    }
-;
-
-var_decls:
-    var_decl
-    {
-    }
-//  | LPAREN_TOK var_decl RPAREN_TOK
-  |
-    var_decls var_decl
-    {
-    }
-;
-
-var_decl:
-    LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK
-    {
-      BEEV::_parser_symbol_table.insert(*$2);
-      //Sort_symbs has the indexwidth/valuewidth. Set those fields in
-      //var
-      $2->SetIndexWidth($3.indexwidth);
-      $2->SetValueWidth($3.valuewidth);
-    }
-   | LPAREN_TOK FORMID_TOK RPAREN_TOK
-    {
-      BEEV::_parser_symbol_table.insert(*$2);
-      //Sort_symbs has the indexwidth/valuewidth. Set those fields in
-      //var
-      $2->SetIndexWidth(0);
-      $2->SetValueWidth(0);
-    }
-;
-
-an_formulas:
-    an_formula
-    {
-      $$ = new BEEV::ASTVec;
-      if ($1 != NULL) {
-	$$->push_back(*$1);
-	delete $1;
-      }
-    }
-  |
-    an_formulas an_formula
-    {
-      if ($1 != NULL && $2 != NULL) {
-	$1->push_back(*$2);
-	$$ = $1;
-	delete $2;
-      }
-    }
-;
-
-an_formula:   
-    TRUE_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); 
-      $$->SetIndexWidth(0); 
-      $$->SetValueWidth(0);
-    }
-  | FALSE_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); 
-      $$->SetIndexWidth(0); 
-      $$->SetValueWidth(0);
-    }
-  | fvar
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedEQ(*$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK
-    {
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$4));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $3;
-      delete $4;      
-    }
-  | LPAREN_TOK an_formula RPAREN_TOK
-    {
-      $$ = $2;
-    }
-  | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$3));
-      delete $3;
-    }
-  | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$3, *$4));
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$3, *$4, *$5));
-      delete $3;
-      delete $4;
-      delete $5;
-    }
-  | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$3));
-      delete $3;
-    }
-  | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$3));
-      delete $3;
-    }
-  | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$3, *$4));
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$3, *$4));
-      delete $3;
-      delete $4;
-    }
-  | letexpr_mgmt an_formula RPAREN_TOK
-  //| letexpr_mgmt an_formula annotations RPAREN_TOK
-    {
-      $$ = $2;
-      //Cleanup the LetIDToExprMap
-      BEEV::globalBeevMgr_for_parser->CleanupLetIDMap();			 
-    }
-;
-
-letexpr_mgmt: 
-    LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
-    {
-     //Expr must typecheck
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6);
-      
-      //set the valuewidth of the identifier
-      $5->SetValueWidth($6->GetValueWidth());
-      $5->SetIndexWidth($6->GetIndexWidth());
-      
-      //populate the hashtable from LET-var -->
-      //LET-exprs and then process them:
-      //
-      //1. ensure that LET variables do not clash
-      //1. with declared variables.
-      //
-      //2. Ensure that LET variables are not
-      //2. defined more than once
-      BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6);
-      delete $5;
-      delete $6;      
-   }
- | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK 
-   {
-     //Expr must typecheck
-     BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6);
-     
-     //set the valuewidth of the identifier
-     $5->SetValueWidth($6->GetValueWidth());
-     $5->SetIndexWidth($6->GetIndexWidth());
-     
-     //Do LET-expr management
-     BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6);
-     delete $5;
-     delete $6;     
-   }
-
-/* an_terms: */
-/*     an_term */
-/*     { */
-/*     } */
-/*   | an_terms an_term */
-/*     { */
-/*     } */
-/* ; */
-
-an_term:
-    BVCONST_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(64, $1));
-    }
-  | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($3, $1));
-    }
-  | an_nonbvconst_term
-  ;
-
-an_nonbvconst_term: 
-    BITCONST_TOK { $$ = $1; }
-  | var
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1));
-      delete $1;
-    }
-  | LPAREN_TOK an_term RPAREN_TOK
-  //| LPAREN_TOK an_term annotations RPAREN_TOK
-    {
-      $$ = $2;
-      //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(*$2));
-      //delete $2;
-    }
-  | LPAREN_TOK TERMID_TOK an_term RPAREN_TOK
-    {
-      //ARRAY READ
-      // valuewidth is same as array, indexwidth is 0.
-      BEEV::ASTNode in = *$2;
-      BEEV::ASTNode m = *$3;
-      unsigned int width = in.GetValueWidth();
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, in, m));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  | SELECT_TOK an_term an_term
-    {
-      //ARRAY READ
-      // valuewidth is same as array, indexwidth is 0.
-      BEEV::ASTNode array = *$2;
-      BEEV::ASTNode index = *$3;
-      unsigned int width = array.GetValueWidth();
-      BEEV::ASTNode * n = 
-	new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, array, index));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  | STORE_TOK an_term an_term an_term
-    {
-      //ARRAY WRITE
-      unsigned int width = $4->GetValueWidth();
-      BEEV::ASTNode array = *$2;
-      BEEV::ASTNode index = *$3;
-      BEEV::ASTNode writeval = *$4;
-      BEEV::ASTNode write_term = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE,width,array,index,writeval);
-      write_term.SetIndexWidth($2->GetIndexWidth());
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(write_term);
-      BEEV::ASTNode * n = new BEEV::ASTNode(write_term);
-      $$ = n;
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-/*   | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK BVCONST_TOK */
-/*     { */
-/*       // This special case is when we have an extract on top of a constant bv, which happens */
-/*       // almost all the time in the smt syntax. */
-
-/*       // $3 is high, $5 is low.  They are ints (why not unsigned? See uintval) */
-/*       int hi  =  $3; */
-/*       int low =  $5; */
-/*       int width = hi - low + 1; */
-
-/*       if (width < 0) */
-/* 	yyerror("Negative width in extract"); */
-
-/*       unsigned long long int val = $7; */
-
-/*       // cut and past from BV32 const evaluator */
-
-/*       unsigned long long int mask1 = 0xffffffffffffffffLL; */
-
-/*       mask1 >>= 64-(hi+1); */
-      
-/*       //extract val[hi:0] */
-/*       val &= mask1; */
-/*       //extract val[hi:low] */
-/*       val >>= low; */
-
-/*       // val is the desired BV32. */
-/*       BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(width, val)); */
-/*       $$ = n; */
-/*     } */
-  | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term
-    {
-      int width = $3 - $5 + 1;
-      if (width < 0)
-	yyerror("Negative width in extract");
-      
-      if((unsigned)$3 >= $7->GetValueWidth() || (unsigned)$5 < 0)
-	yyerror("Parsing: Wrong width in BVEXTRACT\n");			 
-      
-      BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3);
-      BEEV::ASTNode low =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
-      BEEV::ASTNode output = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$7,hi,low);
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(output));
-      BEEV::globalBeevMgr_for_parser->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");
-      
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2);
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3);
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4);
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedTermITE(*$2, *$3, *$4));
-      //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,width,*$2, *$3, *$4));
-      $$->SetIndexWidth($4->GetIndexWidth());
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$);
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  |  BVCONCAT_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth() + $3->GetValueWidth();
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      
-      delete $2;
-      delete $3;
-    }
-  |  BVNOT_TOK an_term
-    {
-      //this is the BVNEG (term) in the CVCL language
-      unsigned int width = $2->GetValueWidth();
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNEG, width, *$2));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-    }
-  |  BVNEG_TOK an_term
-    {
-      //this is the BVUMINUS term in CVCL langauge
-      unsigned width = $2->GetValueWidth();
-      BEEV::ASTNode * n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$2));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-    }
-  |  BVAND_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in AND");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVOR_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in OR");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$2, *$3)); 
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVXOR_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in XOR");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVSUB_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in BVSUB");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = 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");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-
-    }
-  |  BVMULT_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in BVMULT");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVNAND_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in BVNAND");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$2, *$3));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVNOR_TOK an_term an_term 
-    {
-      unsigned int width = $2->GetValueWidth();
-      if (width != $3->GetValueWidth()) {
-	yyerror("Width mismatch in BVNOR");
-      }
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$2, *$3)); 
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
-  |  BVLEFTSHIFT_TOK an_term NUMERAL_TOK 
-    {
-      unsigned int w = $2->GetValueWidth();
-      if((unsigned)$3 < w) {
-	BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0);
-	BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-$3-1);
-	BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0);
-	BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low);
-	BEEV::ASTNode * n = 
-	  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros));
-	BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-	$$ = n;
-      }
-      else
-	$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      delete $2;
-    }
-   |  BVLEFTSHIFT_1_TOK an_term an_term 
-    {
-      unsigned int w = $2->GetValueWidth();
-      unsigned int shift_amt = GetUnsignedConst(*$3);
-      if((unsigned)shift_amt < w) {
-	BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0);
-	BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-shift_amt-1);
-	BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0);
-	BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low);
-	BEEV::ASTNode * n = 
-	  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros));
-	BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-	$$ = n;
-      }
-      else {
-	$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      }
-      delete $2;
-      //delete $3;
-    }
-  |  BVRIGHTSHIFT_TOK an_term NUMERAL_TOK 
-    {
-      BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0);
-      unsigned int w = $2->GetValueWidth();
-      
-      //the amount by which you are rightshifting
-      //is less-than/equal-to the length of input
-      //bitvector
-      if((unsigned)$3 < w) {
-	BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1);
-	BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$3);
-	BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low);
-	BEEV::ASTNode * n = 
-	  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract));
-	BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-	$$ = n;
-      }
-      else {
-	$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      }
-      delete $2;
-    }
-   |  BVRIGHTSHIFT_1_TOK an_term an_term 
-    {
-      unsigned int shift_amt = GetUnsignedConst(*$3);
-      BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0);
-      unsigned int w = $2->GetValueWidth();
-      
-      //the amount by which you are rightshifting
-      //is less-than/equal-to the length of input
-      //bitvector
-      if((unsigned)shift_amt < w) {
-	BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1);
-	BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,shift_amt);
-	BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low);
-	BEEV::ASTNode * n = 
-	  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract));
-	BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-	$$ = n;
-      }
-      else {
-	$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      }
-      delete $2;
-    }
-  |  BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
-    {
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
-      unsigned w = $5->GetValueWidth() + $3;
-      BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w);
-      BEEV::ASTNode *n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX,w,*$5,width));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $5;
-    }
-;
-  
-sort_symb:
-    BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      // Just return BV width.  If sort is BOOL, width is 0.
-      // Otherwise, BITVEC[w] returns w. 
-      //
-      //((indexwidth is 0) && (valuewidth>0)) iff type is BV
-      $$.indexwidth = 0;
-      unsigned int length = $3;
-      if(length > 0) {
-	$$.valuewidth = length;
-      }
-      else {
-	BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
-      }
-    }
-   | ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      unsigned int index_len = $3;
-      unsigned int value_len = $5;
-      if(index_len > 0) {
-	$$.indexwidth = $3;
-      }
-      else {
-	BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
-      }
-
-      if(value_len > 0) {
-	$$.valuewidth = $5;
-      }
-      else {
-	BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
-      }
-    }
-;
-
-var:
-    FORMID_TOK 
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); 
-      delete $1;      
-    }
-   | TERMID_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1));
-      delete $1;
-    }
-   | QUESTION_TOK TERMID_TOK
-    {
-      $$ = $2;
-    }
-;
-
-fvar:
-    DOLLAR_TOK FORMID_TOK
-    {
-      $$ = $2; 
-    }
-  | FORMID_TOK
-    {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); 
-      delete $1;      
-    }   
-;
-%%