Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


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

7 files changed, 2695 insertions, 0 deletions

diff --git a/stp/parser/Makefile b/stp/parser/Makefile
new file mode 100644
index 00000000..8211c825
--- /dev/null
+++ b/stp/parser/Makefile
@@ -0,0 +1,27 @@
+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) -o lexPL.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
new file mode 100644
index 00000000..e9358a0e
--- /dev/null
+++ b/stp/parser/PL.lex
@@ -0,0 +1,128 @@
+%{
+/********************************************************************
+ * 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
new file mode 100644
index 00000000..aa58aa4c
--- /dev/null
+++ b/stp/parser/PL.y
@@ -0,0 +1,1006 @@
+%{
+/********************************************************************
+ * 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
new file mode 100644
index 00000000..1de10492
--- /dev/null
+++ b/stp/parser/let-funcs.cpp
@@ -0,0 +1,85 @@
+/********************************************************************
+ * 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
new file mode 100644
index 00000000..ed251ed3
--- /dev/null
+++ b/stp/parser/main.cpp
@@ -0,0 +1,181 @@
+/********************************************************************
+ * 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
new file mode 100644
index 00000000..a03ae94e
--- /dev/null
+++ b/stp/parser/smtlib.lex
@@ -0,0 +1,232 @@
+%{
+  /********************************************************************
+   * 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
new file mode 100644
index 00000000..0aa22dee
--- /dev/null
+++ b/stp/parser/smtlib.y
@@ -0,0 +1,1036 @@
+%{
+  /********************************************************************
+   * 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;      
+    }   
+;
+%%