about summary refs log tree commit diff homepage
path: root/stp/parser/smtlib.y
diff options
context:
space:
mode:
Diffstat (limited to 'stp/parser/smtlib.y')
-rw-r--r--stp/parser/smtlib.y1036
1 files changed, 0 insertions, 1036 deletions
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;      
-    }   
-;
-%%