Merge pull request #592 from ccadar/remove-SMT

Removing unused lib/SMT directory

7 files changed, 0 insertions, 1694 deletions

diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3
deleted file mode 100644
index a70d12d5..00000000
--- a/lib/SMT/LICENSE.CVC3
+++ /dev/null
@@ -1,53 +0,0 @@
-/*!\page LICENSE LICENSE
-
-Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior
-University, New York University, and the University of Iowa, hereafter
-designated as the Copyright Owners.
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without modification,
-are permitted provided that the following conditions are met:
-
-* Redistributions of source code must retain the above copyright notice, this
-list of conditions and the following disclaimer.
-* Redistributions in binary form must reproduce the above copyright notice,
-this list of conditions and the following disclaimer in the documentation
-and/or other materials provided with the distribution.
-* Neither the names of the Copyright Owners nor the names of any contributors
-may be used to endorse or promote products derived from this software
-without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY
-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
-ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-Note:
-
-The following files contain code whose copyright does not belong to the
-Copyright Owners.  However, separate copyright notices in these files give
-express permission to copy, use, modify, sell, or distribute the code.  Please
-see the copyright notices in the individual files for details.
-
-<pre>
-src/include/fdstream.h
-src/include/hash_map.h
-src/include/hash_fun.h
-src/include/hash_set.h
-src/include/hash_table.h
-src/sat/minisat_varorder.h
-src/sat/minisat_solver.cpp
-src/sat/minisat_heap.h
-src/sat/minisat_types.h
-src/sat/minisat_solver.h
-src/sat/minisat_global.h
-</pre>
-
-*/
diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile
deleted file mode 100644
index 92ec8018..00000000
--- a/lib/SMT/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-#===-- lib/SMT/Makefile ------------------------------------*- Makefile -*--===#
-
-LEVEL=../..
-
-LIBRARYNAME=kleaverSMT
-DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
-
-include $(LEVEL)/Makefile.common
-
-# Gross, but I don't want to build proper rules for this, and I don't want users
-# to have to have bison/flex, so for now require developers to make these
-# manually (at least initially).
-
-smtlib_parser.cpp smtlib_parser.h: smtlib.y
-	bison -d -o smtlib_parser.cpp -p smtlib smtlib.y
-	mv smtlib_parser.hpp smtlib_parser.h	
-	perl -pi -e 's/union/struct/g' smtlib_parser.cpp
-	perl -pi -e 's/union/struct/g' smtlib_parser.h
-
-
-smtlib_lexer.cpp: smtlib.lex smtlib_parser.h
-	flex -I -Psmtlib -osmtlib_lexer.cpp smtlib.lex
-	perl -pi -e 's/union/struct/g' smtlib_lexer.cpp
-
-.PHONY: regen
-regen: smtlib_lexer.cpp smtlib_parser.cpp smtlib_parser.h
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
deleted file mode 100644
index 19ce5af7..00000000
--- a/lib/SMT/SMTParser.cpp
+++ /dev/null
@@ -1,245 +0,0 @@
-//===-- SMTParser.cpp -----------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "SMTParser.h"
-
-#include "klee/ExprBuilder.h"
-#include "klee/Solver.h"
-#include "klee/Constraints.h"
-#include "expr/Parser.h"
-
-#include <fstream>
-#include <string>
-#include <sstream>
-#include <cassert>
-#include <stack>
-
-//#define DEBUG
-
-using namespace klee;
-using namespace klee::expr;
-
-extern int smtlibparse(); 
-extern void *smtlib_createBuffer(int);
-extern void smtlib_deleteBuffer(void *);
-extern void smtlib_switchToBuffer(void *);
-extern int smtlib_bufSize(void);
-extern void smtlib_setInteractive(bool);
-
-SMTParser* SMTParser::parserTemp = NULL;
-
-SMTParser::SMTParser(const std::string _filename, 
-		     ExprBuilder* _builder) : fileName(_filename),
-					      lineNum(1),
-					      done(false),
-					      satQuery(NULL),
-					      bvSize(0),
-					      queryParsed(false),
-					      builder(_builder) {
-  is = new ifstream(fileName.c_str());
-  
-  // Initial empty environments
-  varEnvs.push(VarEnv());
-  fvarEnvs.push(FVarEnv());
-}
-
-void SMTParser::Parse() {
-  SMTParser::parserTemp = this;
-
-  void *buf = smtlib_createBuffer(smtlib_bufSize());
-  smtlib_switchToBuffer(buf);
-  smtlib_setInteractive(false);
-  smtlibparse();
-  //xcout << "Parsed successfully.\n";
-}
-
-Decl* SMTParser::ParseTopLevelDecl() {
-  return new QueryCommand(assumptions, builder->Not(satQuery),
-			  std::vector<ExprHandle>(), 
-			  std::vector<const Array*>());
-}
-
-bool SMTParser::Solve() {
-  // FIXME: Support choice of solver.
-  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true;
-  Solver *S, *STP = S = 
-    UseDummySolver ? createDummySolver() : new STPSolver(true);
-  if (UseSTPQueryKQueryLog)
-    S = createKQueryLoggingSolver(S, "stp-queries.kquery");
-  if (UseFastCexSolver)
-    S = createFastCexSolver(S);
-  S = createCexCachingSolver(S);
-  S = createCachingSolver(S);
-  S = createIndependentSolver(S);
-  if (0)
-    S = createValidatingSolver(S, STP);
-
-  Decl *D = this->ParseTopLevelDecl();
-  if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
-    //llvm::cout << "Query " << ":\t";
-
-    assert("FIXME: Support counterexample query commands!");
-    if (QC->Values.empty() && QC->Objects.empty()) {
-      bool result;
-      if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
-			result)) {
-	//std::cout << (result ? "VALID" : "INVALID") << "\n";
-	return result;	
-      }
-    }
-  }
-  llvm::cout << "FAIL";
-  exit(1);
-}
-
-
-// XXX: give more info
-int SMTParser::Error(const string& msg) {
-  llvm::errs() << SMTParser::parserTemp->fileName << ":"
-               << SMTParser::parserTemp->lineNum << ": " << msg << "\n";
-  exit(1);
-  return 0;
-}
-
-
-int SMTParser::StringToInt(const std::string& s) {
-  std::stringstream str(s);
-  int x;
-  str >> x;
-  assert(str);
-  return x;
-}
-
-
-ExprHandle SMTParser::CreateAnd(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->And(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->And(kids[i], r);
-  return r;
-}
-
-ExprHandle SMTParser::CreateOr(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->Or(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->Or(kids[i], r);
-  return r;
-}
-
-ExprHandle SMTParser::CreateXor(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->Xor(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->Xor(kids[i], r);
-  return r;
-}
-
-
-void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
-  // for now, only allow variables which are multiples of 8
-  if (w % 8 != 0) {
-    cout << "BitVec not multiple of 8 (" << w << ").  Need to update code.\n";
-    exit(1);
-  }
-  
-#ifdef DEBUG
-  std::cout << "Declaring " << name << " of width " << w << "\n";
-#endif
-  
-  const Array *arr = Array::CreateArray(name, w / 8);
-  
-  ref<Expr> *kids = new ref<Expr>[w/8];
-  for (unsigned i=0; i < w/8; i++)
-    kids[i] = builder->Read(UpdateList(arr, NULL), 
-			    builder->Constant(i, 32));
-  ref<Expr> var = ConcatExpr::createN(w/8, kids); // XXX: move to builder?
-  delete [] kids;
-  
-  AddVar(name, var);
-}
-
-
-ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
-  assert(base == 2 || base == 10 || base == 16);
-  llvm::APInt ap(w, val.c_str(), val.length(), base);
-  
-  return klee::ConstantExpr::alloc(ap);
-}
-
-
-void SMTParser::PushVarEnv() {
-#ifdef DEBUG
-  cout << "Pushing new var env\n";
-#endif
-  varEnvs.push(VarEnv(varEnvs.top()));
-}
-
-void SMTParser::PopVarEnv() {
-#ifdef DEBUG
-  cout << "Popping var env\n";
-#endif
-  varEnvs.pop();
-}
-
-void SMTParser::AddVar(std::string name, ExprHandle val) {
-#ifdef DEBUG
-  cout << "Adding (" << name << ", " << val << ") to current var env.\n";
-#endif
-  varEnvs.top()[name] = val;
-}
-
-ExprHandle SMTParser::GetVar(std::string name) {
-  VarEnv top = varEnvs.top();
-  if (top.find(name) == top.end()) {
-    llvm::errs() << "Cannot find variable ?" << name << "\n";
-    exit(1);
-  }
-  return top[name];
-}
-
-
-void SMTParser::PushFVarEnv() {
-  fvarEnvs.push(FVarEnv(fvarEnvs.top()));
-}
-
-void SMTParser::PopFVarEnv(void) {
-#ifdef DEBUG
-  cout << "Popping fvar env\n";
-#endif
-  fvarEnvs.pop();
-}
-
-void SMTParser::AddFVar(std::string name, ExprHandle val) {
-#ifdef DEBUG
-  cout << "Adding (" << name << ", " << val << ") to current fvar env.\n";
-#endif
-  fvarEnvs.top()[name] = val;
-}
-
-ExprHandle SMTParser::GetFVar(std::string name) {
-  FVarEnv top = fvarEnvs.top();
-  if (top.find(name) == top.end()) {
-    llvm::errs() << "Cannot find fvar $" << name << "\n";
-    exit(1);
-  }
-  return top[name];
-}
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
deleted file mode 100644
index ac84e74c..00000000
--- a/lib/SMT/SMTParser.h
+++ /dev/null
@@ -1,92 +0,0 @@
-//===-- SMTParser.h -------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-
-#ifndef SMT_PARSER_H
-#define SMT_PARSER_H
-
-#include "expr/Parser.h"
-
-#include <map>
-#include <stack>
-#include <string>
-
-namespace klee {
-  class ExprBuilder;
-  
-namespace expr {
-
-class SMTParser : public klee::expr::Parser {
-  private:
-    void *buf;
-    
- public:
-  /* For interacting w/ the actual parser, should make this nicer */
-  static SMTParser* parserTemp;
-  std::string fileName;
-  std::istream* is;
-  int lineNum;
-  bool done;
-  bool arraysEnabled;
-  
-  std::vector<ExprHandle> assumptions;
-  klee::expr::ExprHandle satQuery;
-
-  int bvSize;
-  bool queryParsed;
-  
-  klee::ExprBuilder *builder;
-    
-  SMTParser(const std::string filename, ExprBuilder *builder);
-  
-  virtual klee::expr::Decl *ParseTopLevelDecl();
-  bool Solve();
-  
-  virtual void SetMaxErrors(unsigned N) { }
-  
-  virtual unsigned GetNumErrors() const {  return 1; }
-  
-  virtual ~SMTParser() {}
-  
-  void Parse(void);
-  
-  int Error(const std::string& s);
-  
-  int StringToInt(const std::string& s);
-  ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
-  
-  void DeclareExpr(std::string name, Expr::Width w);
-  
-  ExprHandle CreateAnd(std::vector<ExprHandle>);
-  ExprHandle CreateOr(std::vector<ExprHandle>);
-  ExprHandle CreateXor(std::vector<ExprHandle>);
-  
-
-  typedef std::map<const std::string, ExprHandle> VarEnv;
-  typedef std::map<const std::string, ExprHandle> FVarEnv;
-
-  std::stack<VarEnv> varEnvs;
-  std::stack<FVarEnv> fvarEnvs;
-
-  void PushVarEnv(void);
-  void PopVarEnv(void);
-  void AddVar(std::string name, ExprHandle val); // to current var env
-  ExprHandle GetVar(std::string name); // from current var env
-
-  void PushFVarEnv(void);
-  void PopFVarEnv(void);
-  void AddFVar(std::string name, ExprHandle val); // to current fvar env
-  ExprHandle GetFVar(std::string name); // from current fvar env
-};
-
-}
-}
-
-#endif
-
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
deleted file mode 100644
index 31fa311d..00000000
--- a/lib/SMT/main.cpp
+++ /dev/null
@@ -1,40 +0,0 @@
-#include "SMTParser.h"
-
-#include "klee/ExprBuilder.h"
-
-using namespace klee;
-
-int main(int argc, char** argv) {
-  if (argc != 2) {
-    cout << "Usage: " << argv[0] << " <smt-filename>\n";
-    return 1;
-  }
-  
-  enum BuilderKinds {
-    DefaultBuilder,
-    ConstantFoldingBuilder,
-    SimplifyingBuilder
-  } BuilderKind = SimplifyingBuilder;
-
-  ExprBuilder *Builder = 0;
-  switch (BuilderKind) {
-  case DefaultBuilder:
-    Builder = createDefaultExprBuilder();
-    break;
-  case ConstantFoldingBuilder:
-    Builder = createDefaultExprBuilder();
-    Builder = createConstantFoldingExprBuilder(Builder);
-    break;
-  case SimplifyingBuilder:
-    Builder = createDefaultExprBuilder();
-    Builder = createConstantFoldingExprBuilder(Builder);
-    Builder = createSimplifyingExprBuilder(Builder);
-    break;
-  }
-  
-  klee::expr::SMTParser smtParser(argv[1], Builder);
-  smtParser.Parse();
-  int result = smtParser.Solve();
-  
-  cout << (result ? "UNSAT":"SAT") << "\n"; 
-}
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
deleted file mode 100644
index c614c683..00000000
--- a/lib/SMT/smtlib.lex
+++ /dev/null
@@ -1,263 +0,0 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.lex
- * 
- * Author: Clark Barrett
- * 
- * Created: 2005
- *
- * <hr>
- *
- * 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.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-
-#include <iostream>
-#include "SMTParser.h"
-#include "smtlib_parser.h"
-
-using namespace klee;
-using namespace klee::expr;
-
-extern int smtlib_inputLine;
-extern char *smtlibtext;
-
-extern int smtliberror (const char *msg);
-
-static int smtlibinput(std::istream& is, char* buf, int size) {
-  int res;
-  if(is) {
-    // Set the terminator char to 0
-    is.getline(buf, size-1, 0);
-    // If failbit is set, but eof is not, it means the line simply
-    // didn't fit; so we clear the state and keep on reading.
-    bool partialStr = is.fail() && !is.eof();
-    if(partialStr)
-      is.clear();
-
-    for(res = 0; res<size && buf[res] != 0; res++) ;
-    if(res == size) smtliberror("Lexer bug: overfilled the buffer");
-    if(!partialStr) { // Insert \n into the buffer
-      buf[res++] = '\n';
-      buf[res] = '\0';
-    }
-  } else {
-    res = YY_NULL;
-  }
-  return res;
-}
-
-// Redefine the input buffer function to read from an istream
-#define YY_INPUT(buf,result,max_size) \
-  result = smtlibinput(*SMTParser::parserTemp->is, buf, max_size);
-
-int smtlib_bufSize() { return YY_BUF_SIZE; }
-YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
-
-/* some wrappers for methods that need to refer to a struct.
-   These are used by SMTParser. */
-void *smtlib_createBuffer(int sz) {
-  return (void *)smtlib_create_buffer(NULL, sz);
-}
-void smtlib_deleteBuffer(void *buf_state) {
-  smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
-}
-void smtlib_switchToBuffer(void *buf_state) {
-  smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
-}
-void *smtlib_bufState() {
-  return (void *)smtlib_buf_state();
-}
-
-void smtlib_setInteractive(bool is_interactive) {
-  yy_set_interactive(is_interactive);
-}
-
-// 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;
-   }
- }
-
-// for now, we don't have subranges.  
-//
-// ".."		{ return DOTDOT_TOK; }
-/*OPCHAR	(['!#?\_$&\|\\@])*/
-
-%}
-
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
-%x	COMMENT
-%x	STRING_LITERAL
-%x      USER_VALUE
-%s      PAT_MODE
-
-LETTER	([a-zA-Z])
-DIGIT	([0-9])
-OPCHAR	(['\.\_])
-IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
-%%
-
-[\n]            { SMTParser::parserTemp->lineNum++; }
-[ \t\r\f]	{ /* skip whitespace */ }
-
-{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
-
-";"		{ BEGIN COMMENT; }
-<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  SMTParser::parserTemp->lineNum++; }
-<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(smtlibtext[1])); }
-<STRING_LITERAL>"\""	{ BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return STRING_TOK; }
-<STRING_LITERAL>.	{ _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-<INITIAL>":pat"		{ BEGIN PAT_MODE;
-                          return PAT_TOK;}
-<PAT_MODE>"}"	        { BEGIN INITIAL; 
-                          return RCURBRACK_TOK; }
-<INITIAL>"{"		{ BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<USER_VALUE>"\\"[{}] { /* escape characters */
-                          _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
-
-<USER_VALUE>"}"	        { BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-
-<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
-                          SMTParser::parserTemp->lineNum++; }
-<USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-"BitVec"        { return BITVEC_TOK; }
-
-"true"          { return TRUE_TOK; }
-"false"         { return FALSE_TOK; }
-"ite"           { return ITE_TOK; }
-"not"           { return NOT_TOK; }
-"implies"       { return IMPLIES_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; }
-"exists"        { return EXISTS_TOK; }
-"forall"        { return FORALL_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; }
-"benchmark"     { return BENCHMARK_TOK; }
-"extrasorts"    { return EXTRASORTS_TOK; }
-"extrafuns"     { return EXTRAFUNS_TOK; }
-"extrapreds"    { return EXTRAPREDS_TOK; }
-"language"      { return LANGUAGE_TOK; }
-"distinct"      { return DISTINCT_TOK; }
-":pattern"      { return PAT_TOK; } 
-":"             { return COLON_TOK; }
-"\["            { return LBRACKET_TOK; }
-"\]"            { return RBRACKET_TOK; }
-"{"             { return LCURBRACK_TOK;}
-"}"             { return RCURBRACK_TOK;}
-"("             { return LPAREN_TOK; }
-")"             { return RPAREN_TOK; }
-"$"             { return DOLLAR_TOK; }
-"?"             { return QUESTION_TOK; }
-
-
-"bit0"          { return BIT0_TOK; }
-"bit1"          { return BIT1_TOK; }
-
-"concat"        { return BVCONCAT_TOK; }
-"extract"       { return BVEXTRACT_TOK; }
-
-"bvnot"         { return BVNOT_TOK; }
-"bvand"         { return BVAND_TOK; }
-"bvor"          { return BVOR_TOK; }
-"bvneg"         { return BVNEG_TOK; }
-"bvnand"        { return BVNAND_TOK; }
-"bvnor"         { return BVNOR_TOK; }
-"bvxor"         { return BVXOR_TOK; }
-"bvxnor"        { return BVXNOR_TOK; }
-
-"="             { return EQ_TOK; }
-"bvcomp"        { return BVCOMP_TOK; }
-"bvult"         { return BVULT_TOK; }
-"bvule"         { return BVULE_TOK; }
-"bvugt"         { return BVUGT_TOK; }
-"bvuge"         { return BVUGE_TOK; }
-"bvslt"         { return BVSLT_TOK; }
-"bvsle"         { return BVSLE_TOK; }
-"bvsgt"         { return BVSGT_TOK; }
-"bvsge"         { return BVSGE_TOK; }
-
-"bvadd"         { return BVADD_TOK; }
-"bvsub"         { return BVSUB_TOK; }
-"bvmul"         { return BVMUL_TOK; }
-"bvudiv"        { return BVUDIV_TOK; }
-"bvurem"        { return BVUREM_TOK; }
-"bvsdiv"        { return BVSDIV_TOK; }
-"bvsrem"        { return BVSREM_TOK; }
-"bvsmod"        { return BVSMOD_TOK; }
-
-"bvshl"         { return BVSHL_TOK; }
-"bvlshr"        { return BVLSHR_TOK; }
-"bvashr"        { return BVASHR_TOK; }
-
-"repeat"        { return REPEAT_TOK; }
-"zero_extend"   { return ZEXT_TOK; }
-"sign_extend"   { return SEXT_TOK; }
-"rotate_left"   { return ROL_TOK; }
-"rotate_right"  { return ROR_TOK; }
-
-
-"bv"[0-9]+              { smtliblval.str = new std::string(smtlibtext); return BV_TOK; }
-"bvbin"[0-1]+	        { smtliblval.str = new std::string(smtlibtext); return BVBIN_TOK; }
-"bvhex"[0-9,A-F,a-f]+	{ smtliblval.str = new std::string(smtlibtext); return BVHEX_TOK; }
-
-
-({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
-
-<<EOF>>         { return EOF_TOK; }
-
-. { smtliberror("Illegal input character."); }
-%%
-
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
deleted file mode 100644
index eb3b3890..00000000
--- a/lib/SMT/smtlib.y
+++ /dev/null
@@ -1,974 +0,0 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.y
- * 
- * Author: Clark Barrett
- * 
- * Created: Apr 30 2005
- *
- * <hr>
- *
- * 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.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* 
-   This file contains the bison code for the parser that reads in CVC
-   commands in SMT-LIB language.
-*/
-
-#include "SMTParser.h"
-#include "klee/Expr.h"
-#include "klee/ExprBuilder.h"
-
-#include <sstream>
-
-using namespace klee;
-using namespace klee::expr;
-
-// Define shortcuts for various things
-#define PARSER SMTParser::parserTemp
-#define BUILDER SMTParser::parserTemp->builder
-#define DONE SMTParser::parserTemp->done
-#define ASSUMPTIONS SMTParser::parserTemp->assumptions
-#define QUERY SMTParser::parserTemp->satQuery
-
-#define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled)
-#define BVSIZE (SMTParser::parserTemp->bvSize)
-#define QUERYPARSED SMTParser::parserTemp->queryParsed
-
-// Suppress the bogus warning suppression in bison (it generates
-// compile error)
-#undef __GNUC_MINOR__
-
-/* stuff that lives in smtlib.lex */
-extern int smtliblex(void);
-
-int smtliberror(const char *s)
-{
-  return SMTParser::parserTemp->Error(s);
-}
-
-
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
-
-%}
-
-/*
-%union {
-  std::string *str;
-  std::vector<std::string> *strvec;
-  CVC3::Expr *node;
-  std::vector<CVC3::Expr> *vec;
-  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
-};
-*/
-
-%union {
-  std::string *str;
-  klee::expr::ExprHandle node;
-  std::vector<klee::expr::ExprHandle> *vec;
-};
-
-
-%start cmd
-
-/* strings are for better error messages.  
-   "_TOK" is so macros don't conflict with kind names */
-/*
-%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls
-%type <vec> an_formulas quant_vars an_terms fun_symb patterns
-%type <node> pattern 
-%type <node> benchmark bench_name bench_attribute
-%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig
-%type <node> an_formula quant_var an_atom prop_atom
-%type <node> an_term basic_term sort_symb pred_symb
-%type <node> var fvar
-%type <str> logic_name quant_symb connective user_value attribute annotation
-%type <strvec> annotations
-%type <pat_ann> patterns_annotations
-*/
-
-%type <node> an_formula an_logical_formula an_atom prop_atom
-%type <vec> an_formulas
-%type <node> an_term basic_term constant
-%type <node> an_fun an_arithmetic_fun an_bitwise_fun
-%type <node> an_pred
-%type <str> logic_name status attribute user_value annotation annotations 
-%type <str> var fvar symb
-
-%token <str> NUMERAL_TOK
-%token <str> SYM_TOK
-%token <str> STRING_TOK
-%token <str> AR_SYMB
-%token <str> USER_VAL_TOK
-
-%token <str> BV_TOK
-%token <str> BVBIN_TOK
-%token <str> BVHEX_TOK
-
-%token BITVEC_TOK
-
-%token TRUE_TOK
-%token FALSE_TOK
-%token ITE_TOK
-%token NOT_TOK
-%token IMPLIES_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 LCURBRACK_TOK
-%token RCURBRACK_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 PAT_TOK
-
-
-%token BIT0_TOK
-%token BIT1_TOK
-
-%token BVCONCAT_TOK
-%token BVEXTRACT_TOK
-
-%token BVNOT_TOK
-%token BVAND_TOK
-%token BVOR_TOK
-%token BVNEG_TOK
-%token BVNAND_TOK
-%token BVNOR_TOK
-%token BVXOR_TOK
-%token BVXNOR_TOK
-
-%token EQ_TOK
-%token BVCOMP_TOK
-%token BVULT_TOK
-%token BVULE_TOK
-%token BVUGT_TOK
-%token BVUGE_TOK
-%token BVSLT_TOK
-%token BVSLE_TOK
-%token BVSGT_TOK
-%token BVSGE_TOK
-
-%token BVADD_TOK
-%token BVSUB_TOK
-%token BVMUL_TOK
-%token BVUDIV_TOK
-%token BVUREM_TOK
-%token BVSDIV_TOK
-%token BVSREM_TOK
-%token BVSMOD_TOK
-%token BVSHL_TOK
-%token BVLSHR_TOK
-%token BVASHR_TOK
-
-%token REPEAT_TOK
-%token ZEXT_TOK
-%token SEXT_TOK
-%token ROL_TOK
-%token ROR_TOK
-
-%%
-
-cmd:
-    benchmark
-    {
-      YYACCEPT;
-    }
-;
-
-benchmark:
-    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { }
-
-  | EOF_TOK
-    { 
-      DONE = true;
-    }
-;
-
-bench_name:
-    SYM_TOK { }
-;
-
-bench_attributes:
-    bench_attribute { }
-
-  | bench_attributes bench_attribute { }
-;
-
-bench_attribute:
-    COLON_TOK ASSUMPTION_TOK an_formula
-    {
-      ASSUMPTIONS.push_back($3);
-    }
-
-  | COLON_TOK FORMULA_TOK an_formula 
-    {
-      QUERYPARSED = true;
-      QUERY = $3;
-    }
-
-  | COLON_TOK STATUS_TOK status { }
-
-  | COLON_TOK LOGIC_TOK logic_name 
-    {
-      if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") {
-	llvm::errs() << "ERROR: Logic " << *$3 << " not supported.";
-	exit(1);
-      }
-
-      if (*$3 == "QF_AUFBV")
-        ARRAYSENABLED = true;
-    }
-/*
-  | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK
-    { 
-      // XXX?
-    }
-*/
-
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK
-    {
-      PARSER->DeclareExpr(*$5, atoi($8->c_str()));
-    }
-/*
-  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
-    {
-      //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
-      //delete $4;
-    }
-*/
-  | COLON_TOK NOTES_TOK STRING_TOK
-    {  }
-
-  | COLON_TOK CVC_COMMAND_TOK STRING_TOK
-    {  }
-
-  | annotation
-    {  }
-;
-
-
-logic_name  :
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      BVSIZE = atoi($3->c_str());
-      delete $3;
-      $$ = $1;
-    }
-  | SYM_TOK
-    {
-      $$ = $1;
-    }
-;
-
-status:
-    SAT_TOK { }
-  | UNSAT_TOK { }
-  | UNKNOWN_TOK { }
-;
-
-/*
-sort_symbs:
-    sort_symb 
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | sort_symbs sort_symb
-    { 
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decls:
-    fun_symb_decl
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    fun_symb_decls fun_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decl:
-    LPAREN_TOK fun_sig annotations
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK fun_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
-;
-
-fun_sig:
-    fun_symb sort_symbs
-    {
-      if ($2->size() == 1) {
-        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0]));
-      }
-      else {
-        CVC3::Expr tmp(VC->listExpr("_ARROW", *$2));
-        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp));
-      }
-      delete $1;
-      delete $2;
-    }
-;
-
-pred_symb_decls:
-    pred_symb_decl
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    pred_symb_decls pred_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-pred_symb_decl:
-    LPAREN_TOK pred_sig annotations
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK pred_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
-;
-
-pred_sig:
-    pred_symb sort_symbs
-    {
-      std::vector<CVC3::Expr> tmp(*$2);
-      tmp.push_back(VC->idExpr("_BOOLEAN"));
-      CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp));
-      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2));
-      delete $1;
-      delete $2;
-    }
-  | pred_symb
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1),
-                                       VC->idExpr("_BOOLEAN")));
-      delete $1;
-    }
-;
-*/
-
-
-an_formulas:
-    an_formula
-    {
-      $$ = new std::vector<klee::expr::ExprHandle>;
-      $$->push_back($1);
-    }
-  |
-    an_formulas an_formula
-    {
-      $1->push_back($2);
-      $$ = $1;
-    }
-;
-
-
-an_logical_formula:
-
-    LPAREN_TOK NOT_TOK an_formula annotations
-    {
-      $$ = BUILDER->Not($3);
-    }
-
-  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
-    {
-      $$ = Expr::createImplies($3, $4);  // XXX: move to builder?
-    }
-
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations
-    {
-      $$ = BUILDER->Select($3, $4, $5);
-    }
-
-  | LPAREN_TOK AND_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateAnd(*$3);
-    }
-
-  | LPAREN_TOK OR_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateOr(*$3);
-    }
-
-  | LPAREN_TOK XOR_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateXor(*$3);
-    }
-
-  | LPAREN_TOK IFF_TOK an_formula an_formula annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
-;
-
-
-an_formula:
-    an_atom
-    {
-      $$ = $1;
-    }
-
-  | an_logical_formula
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK
-        { 
-	  PARSER->PushVarEnv();
-	  PARSER->AddVar(*$4, $5); 
-	} 
-    an_formula annotations
-    {
-      $$ = $8;
-      PARSER->PopVarEnv();
-    }
-
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK 
-        { 
-	  PARSER->PushFVarEnv();
-	  PARSER->AddFVar(*$4, $5); 
-	} 
-    an_formula annotations
-    {
-      $$ = $8;
-      PARSER->PopFVarEnv();
-    }
-;
-
-
-
-an_atom:
-    prop_atom 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK prop_atom annotations 
-    {
-      $$ = $2;
-    }
-  
-  | an_pred
-    {
-      $$ = $1;
-    }
-
-/*
-  | LPAREN_TOK DISTINCT_TOK an_terms annotations
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
-
-//       std::vector<CVC3::Expr> tmp;
-//       tmp.push_back(*$2);
-//       tmp.insert(tmp.end(), $3->begin(), $3->end());
-//       $$ = new CVC3::Expr(VC->listExpr(tmp));
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-//         tmp.push_back(($3)[i])
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
-//       std::vector<CVC3::Expr> tmp;
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-    }
-*/
-;
-
-prop_atom:
-    TRUE_TOK
-    {
-      $$ = BUILDER->Constant(1, 1);
-    }
-
-  | FALSE_TOK
-    { 
-      $$ = BUILDER->Constant(0, 1);;
-    }
-
-  | fvar
-    {
-      $$ = PARSER->GetFVar(*$1);
-    }
-;  
-
-
-an_pred:
-    LPAREN_TOK EQ_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
-
-  | LPAREN_TOK BVULT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ult($3, $4);
-    }
-
-  | LPAREN_TOK BVULE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ule($3, $4);
-    }
-
-  | LPAREN_TOK BVUGT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ugt($3, $4);
-    }
-
-  | LPAREN_TOK BVUGE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Uge($3, $4);
-    }
-
-  | LPAREN_TOK BVSLT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Slt($3, $4);
-    }
-
-  | LPAREN_TOK BVSLE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sle($3, $4);
-    }
-
-  | LPAREN_TOK BVSGT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sgt($3, $4);
-    }
-
-  | LPAREN_TOK BVSGE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sge($3, $4);
-    }
-;
-
-
-an_arithmetic_fun:
-
-    LPAREN_TOK BVNEG_TOK an_term annotations
-    {
-      smtliberror("bvneg not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK BVADD_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Add($3, $4);
-    }
-
-  | LPAREN_TOK BVSUB_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sub($3, $4);
-    }
-
-  | LPAREN_TOK BVMUL_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Mul($3, $4);
-    }
-
-  | LPAREN_TOK BVUDIV_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->UDiv($3, $4);
-    }
-
-  | LPAREN_TOK BVUREM_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->URem($3, $4);
-    }
-
-  | LPAREN_TOK BVSDIV_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->SDiv($3, $4);
-    }
-
-  | LPAREN_TOK BVSREM_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->SRem($3, $4);
-    }
-
-  | LPAREN_TOK BVSMOD_TOK an_term an_term annotations
-    {
-      smtliberror("bvsmod not supported yet");
-      $$ = NULL; // TODO
-    }
-;
-
-
-an_bitwise_fun:
-    LPAREN_TOK BVNOT_TOK an_term annotations
-    {
-      $$ = BUILDER->Not($3);
-    }
-
-  | LPAREN_TOK BVAND_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->And($3, $4);
-    }
-
-  | LPAREN_TOK BVOR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Or($3, $4);
-    }
-
-  | LPAREN_TOK BVXOR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Xor($3, $4);
-    }
-
-  | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
-    {      
-      smtliberror("bvxnor not supported yet");
-      $$ = NULL;  // TODO
-    }
-
-  | LPAREN_TOK BVSHL_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Shl($3, $4);
-    }
-
-  | LPAREN_TOK BVLSHR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->LShr($3, $4);
-    }
-
-  | LPAREN_TOK BVASHR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->AShr($3, $4);
-    }
-
-  | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("rotate_left not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("rotate_right not supported yet");
-      $$ = NULL; // TODO
-    }
- 
-  | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      $$ = BUILDER->ZExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
-    }
-
-  | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      $$ = BUILDER->SExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
-    }
-
-  | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Concat($3, $4);
-    }
-
-  | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("repeat not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      int off = PARSER->StringToInt(*$6);
-      $$ = BUILDER->Extract($8, off, PARSER->StringToInt(*$4) - off + 1);
-    }
-;
-
-
-an_fun:
-    an_logical_formula
-    {
-      $$ = $1;
-    }
-
-  | an_pred
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK BVCOMP_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
- 
-  | an_arithmetic_fun
-    {
-      $$ = $1;
-    }
-
-  | an_bitwise_fun
-    {
-      $$ = $1;
-    }
-
-/*
-      else if (ARRAYSENABLED && *$1 == "select") {
-        $$->push_back(VC->idExpr("_READ"));
-      }
-      else if (ARRAYSENABLED && *$1 == "store") {
-        $$->push_back(VC->idExpr("_WRITE"));
-      }
-*/
-;
-
-constant:
-    BIT0_TOK
-    {
-      $$ = PARSER->GetConstExpr("0", 2, 1);
-    }
-
-  | BIT1_TOK
-    {
-      $$ = PARSER->GetConstExpr("1", 2, 1);
-    }
-
-  | BVBIN_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(5), 2, $1->length()-5);
-    }
-  | BVHEX_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(5), 16, ($1->length()-5)*4);
-    }
-  | BV_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(2), 10, PARSER->StringToInt(*$3));
-    }
-;
-
-
-an_term:
-    basic_term 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK basic_term annotations 
-    {
-      $$ = $2;
-      delete $3;
-    }
-
-  | an_fun
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations
-    {
-      $$ = BUILDER->Select($3, $4, $5);
-    }
-;
-
-
-basic_term:
-    constant 
-    {
-      $$ = $1;
-    }
-
-  | var
-    {
-      $$ = PARSER->GetVar(*$1);
-    }
-  | symb
-    {
-      $$ = PARSER->GetVar(*$1);
-    }
-;
-
-
-
-annotations:
-    RPAREN_TOK { }
-  | annotation annotations { }
-;
-
-annotation:
-    attribute { }
-
-  | attribute user_value {  }
-;
-
-user_value:
-    USER_VAL_TOK  
-    {
-      delete $1;
-    }
-;
-
-/*
-sort_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && *$1 == "BitVec") {
-        $$ = new CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3)));
-      }
-      delete $1;
-      delete $3;
-    }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && ARRAYSENABLED && *$1 == "Array") {
-        $$ = new CVC3::Expr(VC->listExpr("_ARRAY",
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)),
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$5))));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5)));
-      }
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK 
-    { 
-      if (*$1 == "Real") {
-	$$ = new CVC3::Expr(VC->idExpr("_REAL"));
-      } else if (*$1 == "Int") {
-	$$ = new CVC3::Expr(VC->idExpr("_INT"));
-      } else {
-	$$ = new CVC3::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-;
-
-*/
-
-/*
-fun_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        int i = 2;
-        while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-        if ((*$1)[i] == '\0') {
-          $$->push_back(VC->idExpr("_BVCONST"));
-          $$->push_back(VC->ratExpr($1->substr(2), 10));
-        }
-        else $$->push_back(VC->idExpr(*$1));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      delete $1;
-      delete $3;
-    }
-;
-*/
-
-attribute:
-    COLON_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-
-var:
-    QUESTION_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-
-fvar:
-    DOLLAR_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-symb:
-    SYM_TOK
-    {
-      $$ = $1;
-    }
-
-%%