Partial parser for booleans

1 files changed, 98 insertions, 1730 deletions

diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index 012f468eb..71809b049 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -16,6 +16,10 @@
 #include "cvc4.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
+#include "cvc4_expr.h"
+#include "expr/expr_builder.h"
+#include "expr/expr_manager.h"
+#include "util/command.h"
 //#include "rational.h"
 
 // Exported shared data
@@ -29,6 +33,7 @@ namespace CVC4 {
 #define TMP CVC4::parser::parserState
 #define EXPR CVC4::parser::parserState->expr
 #define VC (CVC4::parser::parserState->vc)
+#define EM (CVC4::parser::parserState->exprManager)
 #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -46,136 +51,26 @@ int PLerror(const char *s)
   return CVC4::parser::parserState->error(ss.str());
 }
 
-
-namespace CVC4 {
-
-// File-static auxiliary funcion to wrap accessors upto the index i
-// (not inclusive) around "e".  Used to rebuild the UPDATE expressions.
-static Expr wrapAccessors(const Expr& e,
-			  const std::vector<Expr>& accessors,
-			  const int i) {
-  DebugAssert((int)accessors.size() >= i, "wrapAccessors: too few accessors");
-  Expr res(e);
-  for(int j=0; j<i; j++) {
-    const Expr& acc = accessors[j];
-    switch(acc.getKind()) {
-    case ID: // Datatype: apply the accessor directly to 'res'
-      res = VC->listExpr(acc, res);
-      break;
-    case RAW_LIST:
-      DebugAssert(acc.arity() == 2 && acc[0].getKind() == ID,
-		  "PL.y: wrong number of arguments in the accessor of WITH: "
-		  +acc.toString());
-      res = VC->listExpr(acc[0], res, acc[1]);
-      break;
-    default:
-      DebugAssert(false, "PL.y: Bad accessor in WITH: "+acc.toString());
-    }
-  }
-  return res;
-}
-
-// Convert a complex WITH statement into a bunch of nested simple UPDATEs
-
-// Updator "e1 WITH accessors := e2" is represented as
-// (e1 (accessor1 accessor2 ... ) e2), where the accessors are:
-// (READ idx)
-// ID (datatype constructor's argument)
-// (RECORD_SELECT ID)
-// and (TUPLE_SELECT num).
- 
-// We rebuild this into nested RECORD_UPDATE, WRITE,
-// TUPLE_UPDATE, and DATATYPE_UPDATE expressions.  For example:
-//
-// e WITH [idx] car.f := newVal  is transformed into
-// e WITH [idx] := (e[idx] WITH car := (car(e[idx]) WITH .f := newVal))
-// which is represented as
-// (WRITE e idx
-//        (DATATYPE_UPDATE (READ e idx) car
-//                         (RECORD_UPDATE (car (READ e idx)) f newVal))).
-// Here "car" and "f" are identifiers (ID "car") and (ID "f").
-
-static Expr PLprocessUpdate(const CVC4::Expr& e,
-			    const CVC4::Expr& update) {
-  TRACE("parser verbose", "PLprocessUpdate(", e, ") {");
-  DebugAssert(update.arity() == 2,"PL.y: Bad WITH statement: "
-	      +update.toString());
-  // Rebuild accessors: resolve ID in (READ (ID "name")) and leave
-  // the rest alone
-  TRACE("parser verbose", "PLprocessUpdate: update[0] = ", update[0], "");
-  std::vector<Expr> acc;
-  for(Expr::iterator i=update[0].begin(), iend=update[0].end(); i!=iend; ++i) {
-    TRACE("parser verbose", "*i = ", *i, "");
-    acc.push_back(*i);
-  }
-  TRACE("parser verbose", "acc.size() = ", acc.size(), "");
-  TRACE("parser verbose", "accessors = ", VC->listExpr(acc), "");
-  // 'res' serves as the accumulator of updators; initially it is
-  // newVal (which is update[1]).  We run through accessors in reverse
-  // order, wrapping this accumulator with the corresponding
-  // updators.
-  Expr res(update[1]);
-  // Rebuilding the original expression "e"
-  // The main loop
-  for(int i=acc.size()-1; i>=0; i--) {
-    Expr ac(acc[i]);  // The current accessor
-    TRACE("parser verbose", "ac["+int2string(i)+"] = ", ac, "");
-    // "e" with all preceding accessors
-    Expr tmp(wrapAccessors(e, acc, i));
-    TRACE("parser verbose", "tmp = ", tmp, "");
-    switch(ac.getKind()) {
-    case ID: // Datatype update
-      res = VC->listExpr("_DATATYPE_UPDATE", tmp, ac, res);
-      break;
-    case RAW_LIST: {
-      const std::string& kind = ac[0][0].getString();
-      if(kind == "_READ") // Array update
-	res = VC->listExpr("_WRITE", tmp, ac[1], res);
-      else if(kind == "_RECORD_SELECT") // Record update
-	res = VC->listExpr("_RECORD_UPDATE", tmp, ac[1], res);
-      else if(kind == "_TUPLE_SELECT") // Tuple element
-	res = VC->listExpr("_TUPLE_UPDATE", tmp, ac[1], res);
-      else
-	DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString());
-      break;
-    }
-    default:
-      DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString());
-    }
-  }
-  TRACE("parser verbose", "PLprocessUpdate => ", res, " }");
-  return res;
-}
-
-
-// Process a vector of simultaneous updates (from a single WITH)
-static Expr PLprocessUpdates(const CVC4::Expr& e,
-			     const std::vector<CVC4::Expr>& updates,
-			     size_t idx=0) {
-  // Processed all the updates
-  if(idx >= updates.size()) return e;
-  return PLprocessUpdates(PLprocessUpdate(e, updates[idx]), updates, idx+1);
-}
-
-
-
-} // end of namespace CVC4
-
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 10485760
 /* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */
 #define YYERROR_VERBOSE 1
+
+using namespace CVC4;
+
 %}
 
 %union {
   std::string *str;
-  CVC4::Expr *node;
+  CVC4::Expr *expr;
+  CVC4::Command *cmd;
   std::vector<CVC4::Expr> *vec;
   int kind;
 };
 
 
-%start cmd
+// %start cmd
+%start Query
 
 /* strings are for better error messages.  
    "_TOK" is so macros don't conflict with kind names */
@@ -360,1625 +255,98 @@ static Expr PLprocessUpdates(const CVC4::Expr& e,
 %nonassoc '{' '.' '('
 %nonassoc BITVECTOR_TOK
 
-%type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors
-%type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls 
-%type <vec> Exprs AndExpr OrExpr Pattern Patterns
-%type <vec> RecordEntries UpdatePosition Updates
-
-%type <node> Type /* IndexType */ TypeNotIdentifier TypeDef
-%type <node> DataType SingleDataType Constructor
-%type <node> FunctionType RecordType Real Int BitvectorType
-%type <node> FieldDecl TupleType
-%type <node> ArrayType ScalarType SubType BasicType SubrangeType 
-%type <node> LeftBound RightBound
-%type <node> Expr Conditional UpdatePositionNode Update Lambda
-%type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral 
-%type <node> LetDecl LetExpr LetDeclsNode 
-%type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
-%type <node> BoundVarDecl BoundVarDeclNode VarDecl
-%type <node> ConstDecl TypeDecl 
-%type <node> Identifier StringLiteral Numeral Binary Hex
-
-%type <node> Assert Query Help Dbg Trace Option  
-%type <node> Transform Print Call Echo DumpCommand
-%type <node> Include Where Push Pop PopTo
-%type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute
-%type <node> other_cmd
-%type <node> Arith_Var_Order
+// %type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors
+// %type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls 
+// %type <vec> Exprs AndExpr OrExpr Pattern Patterns
+// %type <vec> RecordEntries UpdatePosition Updates
+
+// %type <node> Type /* IndexType */ TypeNotIdentifier TypeDef
+// %type <node> DataType SingleDataType Constructor
+// %type <node> FunctionType RecordType Real Int BitvectorType
+// %type <node> FieldDecl TupleType
+// %type <node> ArrayType ScalarType SubType BasicType SubrangeType 
+// %type <node> LeftBound RightBound
+%type <expr> Expr // Conditional UpdatePositionNode Update Lambda
+// %type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral 
+// %type <node> LetDecl LetExpr LetDeclsNode 
+// %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
+// %type <node> BoundVarDecl BoundVarDeclNode VarDecl
+// %type <node> ConstDecl TypeDecl 
+ // %type <expr> Identifier // StringLiteral Numeral Binary Hex
+
+ // %type <cmd> cmd Assert Query // Help Dbg Trace Option  
+%type <cmd> Query // Help Dbg Trace Option  
+// %type <node> Transform Print Call Echo DumpCommand
+// %type <node> Include Where Push Pop PopTo
+// %type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute
+// %type <node> other_cmd
+// %type <node> Arith_Var_Order
 
 %token <str> ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK
 
 %%
 
-cmd             :       TypeDecl ';'
-                        {
-			  EXPR = *$1;
-			  delete $1;
-			  YYACCEPT;
-			}
-                |       ConstDecl ';'
-                        {
-			  EXPR = *$1;
-			  delete $1;
-			  YYACCEPT;
-			}
-                |       other_cmd ';' {
-			  EXPR = *$1;
-			  delete $1;
-			  YYACCEPT;
-			}
-                |       ';'
-                        {
-			  EXPR = CVC4::Expr();
-			  YYACCEPT;
-			}
-                |       DONE_TOK 
-                        {
-			  TMP->done = true;
-			  EXPR = CVC4::Expr();
-			  YYACCEPT;
-			}
-                ;
-
-other_cmd       :       Assert { $$ = $1; }
-                |       Query { $$ = $1; }
-                |       Dbg { $$ = $1; }
-                |       Trace { $$ = $1; }
-                |       Option { $$ = $1; }
-                |       Help { $$ = $1; }
-                |       Transform { $$ = $1; }
-                |       Print { $$ = $1; }
-                |       Call { $$ = $1; }
-                |       Echo { $$ = $1; }
-                |       Include { $$ = $1; }
-                |       DumpCommand { $$ = $1; }
-                |       Where { $$ = $1; }
-                |       Push { $$ = $1; }
-                |       Pop { $$ = $1; }
-                |       PopTo { $$ = $1; }
-                |       Context { $$ = $1; }
-                |       Substitute { $$ = $1; }
-                |       Get_Child { $$ = $1; }
-                |       Get_Op { $$ = $1; }
-                |       Get_Type { $$ = $1; }
-                |       Check_Type { $$ = $1; }
-                |       Forget { $$ = $1; }
-                |       Arith_Var_Order { $$ = $1; }
-                ;
-
-Arith_Var_Order :       ARITH_VAR_ORDER_TOK '(' Exprs ')'
-                        {
-                            $$ = new CVC4::Expr(VC->listExpr("_ARITH_VAR_ORDER", *$3));
-                            delete $3;
-                        }
-                ;
-
-Assert          :       ASSERT_TOK Expr { 
-
-                          $$ = new CVC4::Expr(VC->listExpr("_ASSERT", *$2));
-			  delete $2;
-                        }
-                ;
-
-Query           :       QUERY_TOK Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_QUERY", *$2));
-			  delete $2;
-                        }
-                |       CHECKSAT_TOK Expr {
-                          $$ = new CVC4::Expr(VC->listExpr("_CHECKSAT", *$2));
-                          delete $2;
-                        }
-                |       CHECKSAT_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CHECKSAT")));
-                        }
-                |       CONTINUE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTINUE")));
-                        }
-                |       RESTART_TOK Expr {
-                          $$ = new CVC4::Expr(VC->listExpr("_RESTART", *$2));
-                          delete $2;
-                        }
-                ;
-Dbg             :       DBG_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_DBG", *$2));
-			  delete $2;
-                        }
-                |       DBG_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DBG")));
-		}
-                ;
-Trace           :       TRACE_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_TRACE", *$2));
-			  delete $2;
-                        }
-                |       UNTRACE_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_UNTRACE", *$2));
-			  delete $2;
-                        }
-                ;
-Option          :       OPTION_TOK StringLiteral Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_OPTION",  *$2, *$3));
-			  delete $2;
-			  delete $3;
-                        }
-                |       OPTION_TOK StringLiteral MINUS_TOK Numeral {
-			  CVC4::Rational value= -$4->getRational();
-                          CVC4::Expr e = CVC4::Expr(VC->ratExpr(value.toString()));
-                          $$ = new CVC4::Expr(VC->listExpr("_OPTION",  *$2, e));
-			  delete $2;
-			  delete $4;
-                        }
-                |       OPTION_TOK StringLiteral StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_OPTION",  *$2,  *$3));
-			  delete $2;
-			  delete $3;
-                        }
-                ;
-Help            :       HELP_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_HELP", *$2));
-			  delete $2;
-                        }
-                |       HELP_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_HELP")));
-		}
-                ;
-
-Transform       :       TRANSFORM_TOK Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_TRANSFORM", *$2));
-			  delete $2;
-                        }
-                ;
-
-Print           :       PRINT_TOK Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2));
-			  delete $2;
-                        }
-                |       PRINT_TYPE_TOK Type { 
-                          $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2));
-			  delete $2;
-                        }
-                ;
-
-Call            :       CALL_TOK Identifier Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_CALL", *$2, *$3));
-			  delete $2;
-			  delete $3;
-                        }
-                ;
-
-Echo            :       ECHO_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_ECHO", *$2));
-			  delete $2;
-                        }
-                |       ECHO_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ECHO")));
-                        }
-                ;
-
-Include         :       INCLUDE_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_INCLUDE",  *$2));
-			  delete $2;
-                        }
-                ;
-
-DumpCommand     :       DUMP_PROOF_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_PROOF")));
-                        }
-                |       DUMP_ASSUMPTIONS_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_ASSUMPTIONS")));
-                        }
-                |       DUMP_SIG_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_SIG")));
-                        }
-                |       DUMP_TCC_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC")));
-                        }
-                |       DUMP_TCC_ASSUMPTIONS_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_ASSUMPTIONS")));
-                        }
-                |       DUMP_TCC_PROOF_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_PROOF")));
-                        }
-                |       DUMP_CLOSURE_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE")));
-                        }
-                |       DUMP_CLOSURE_PROOF_TOK { 
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE_PROOF")));
-                        }
-                ;
-
-Where           :       WHERE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_WHERE")));
-               		}
-                |       ASSERTIONS_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSERTIONS")));
-               		}
-                |       ASSUMPTIONS_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSUMPTIONS")));
-               		}
-                |       COUNTEREXAMPLE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTEREXAMPLE")));
-               		}
-                |       COUNTERMODEL_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTERMODEL")));
-               		}
-                ;
-Push            :       PUSH_TOK Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_PUSH", *$2));
-			  delete $2;
-                        }
-                |       PUSH_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH")));
-		        }
-                |       PUSH_SCOPE_TOK Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_PUSH_SCOPE", *$2));
-			  delete $2;
-                        }
-                |       PUSH_SCOPE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH_SCOPE")));
-		        }
-                ;
-Pop             :       POP_TOK Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_POP", *$2));
-			  delete $2;
-                        }
-                |       POP_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP")));
-		        }
-                |       POP_SCOPE_TOK Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_POP_SCOPE", *$2));
-			  delete $2;
-                        }
-                |       POP_SCOPE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP_SCOPE")));
-		        }
-                ;
-PopTo           :       POPTO_TOK Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_POPTO", *$2));
-			  delete $2;
-                        }
-                |       POPTO_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO")));
-		        }
-                |       POPTO_SCOPE_TOK Numeral {
-                          $$ = new CVC4::Expr(VC->listExpr("_POPTO_SCOPE", *$2));
-			  delete $2;
-                        }
-                |       POPTO_SCOPE_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO_SCOPE")));
-		        }
-                |       RESET_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_RESET")));
-		        }
-                ;
-Context         :       CONTEXT_TOK StringLiteral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_CONTEXT",  *$2));
-			  delete $2;
-                        }
-                |       CONTEXT_TOK {
-                          $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTEXT")));
-		        }
-                ;
-Forget          :       FORGET_TOK Identifier { 
-                          $$ = new CVC4::Expr(VC->listExpr("_FORGET", *$2));
-			  delete $2;
-                        }
-                ;
-Get_Type        :       GET_TYPE_TOK Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_GET_TYPE", *$2));
-			  delete $2;
-                        }
-                ;
-Check_Type      :       CHECK_TYPE_TOK Expr ':' Type { 
-                          $$ = new CVC4::Expr(VC->listExpr("_CHECK_TYPE",*$2, *$4));
-			  delete $2;
-			  delete $4;
-                        }
-                ;
-Get_Child       :       GET_CHILD_TOK Expr Numeral { 
-                          $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2, *$3));
-			  delete $2;
-			  delete $3;
-                        }
-                ;
-Get_Op          :       GET_OP_TOK Expr { 
-                          $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2));
-			  delete $2;
-                        }
-                ;
-Substitute      :       SUBSTITUTE_TOK Identifier ':' Type '=' Expr '[' Identifier ASSIGN_TOK Expr ']' { 
-                          std::vector<CVC4::Expr> tmp;
-			  tmp.push_back(*$2);
-			  tmp.push_back(*$4);
-			  tmp.push_back(*$6);
-			  tmp.push_back(*$8);
-			  tmp.push_back(*$10);
-                          $$ = new CVC4::Expr(VC->listExpr("_SUBSTITUTE", tmp));
-			  delete $2;
-			  delete $4;
-			  delete $6;
-			  delete $8;
-			  delete $10;
-                        }
-                ;
-Identifier      :       ID_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr(*$1));
-			  delete $1;
-			}
-                ;
-StringLiteral   :       STRINGLIT_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->stringExpr(*$1));
-			  delete $1;
-			}
-                ;
-Numeral         :       NUMERAL_TOK
-                        {
-  			  $$ = new CVC4::Expr(VC->ratExpr((*$1)));
-  			  delete $1;
-			}
-                ;
-
-Binary          :       BINARY_TOK
-                        {
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_BVCONST", VC->stringExpr(*$1)));
-			  delete $1;
-                        }
-                ;
-
-
-Hex             :       HEX_TOK
-                        {
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_BVCONST", VC->stringExpr(*$1), VC->ratExpr(16)));
-			  delete $1;
-                        }
-                ;
-
-
-/* Grammar for Types */
-
-Type		:	Identifier { $$ = $1; }
-		|	TypeNotIdentifier { $$ = $1; }
-		;
-
-TypeNotIdentifier:      ArrayType { $$ = $1; }
-		|	FunctionType { $$ = $1; }
-                |	BasicType { $$ = $1; }
-		|	SubrangeType { $$ = $1; }
-		|	TupleType { $$ = $1; }
-		|	RecordType { $$ = $1; }
-		|	TypeLetExpr { $$ = $1; }
-                |       BitvectorType {$$ = $1;}
-                |       SubType { $$ = $1; }
-                |       '(' Type ')' { $$ = $2; }
-		;
-
-TypeDef		:	Type { $$ = $1; }
-		|	ScalarType { $$ = $1; }
-		;
-
-DataType	:       DATATYPE_TOK SingleDataTypes END_TOK
-			{
-			  $$ = new CVC4::Expr(
-                            VC->listExpr("_TYPEDEF",
-                                         VC->listExpr("_DATATYPE", *$2)));
-			  delete $2;
-			}
-		;
-
-SingleDataTypes :       SingleDataType
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	SingleDataTypes ',' SingleDataType
-		        { 
-			  $1->push_back(*$3); 
-                          $$ = $1;
-		          delete $3;
-			}
-		;
-
-SingleDataType  :       Identifier '=' Constructors
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, VC->listExpr(*$3)));
-			  delete $1;
-			  delete $3;
-                        }
-                ;
-
-Constructors	:	Constructor 
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1; 
-			}
-		|	Constructors MID_TOK Constructor 
-		        { 
-			  $1->push_back(*$3); 
-                          $$ = $1; 
-		          delete $3; 
-			}
-		;
-
-Constructor	:	Identifier 
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1; 
-			}
-		|	Identifier '(' VarDecls ')'
-			{
-                          CVC4::Expr tmp = VC->listExpr(*$3);
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, tmp));
-			  delete $1; delete $3;
-			}
-		;
-
-VarDecls	:	VarDecl
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	VarDecls ',' VarDecl 
-                        {
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-VarDecl		:	Identifier ':' Type
-			{ 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		;
-
-FunctionType	:	'[' Type ARROW_TOK Type ']'
-			{
-                          // Old style functions
-                          $$ = new CVC4::Expr(VC->listExpr("_OLD_ARROW", *$2, *$4));
-                          delete $2; delete $4;
-			}
-                |       Type ARROW_TOK Type
-			{
-			  std::vector<CVC4::Expr> temp;
-			  temp.push_back(*$1);
-			  temp.push_back(*$3);
-
-			  $$ = new CVC4::Expr(VC->listExpr("_ARROW", temp));
-			  delete $1; delete $3; 
-			}
-                |       '(' TypeList ')' ARROW_TOK Type
-			{
-			  $2->push_back(*$5);
-			  $$ = new CVC4::Expr(VC->listExpr("_ARROW", *$2));
-			  delete $2; delete $5; 
-			}
-		;
-
-RecordType	:	SQHASH_TOK FieldDecls HASHSQ_TOK
-			{
-			  $$ = new CVC4::Expr(VC->listExpr(*$2));
-			  delete $2;
-			}
-		;
+// cmd:       
+//     Assert { $$ = $1; }
+//  |  Query { $$ = $1; }
 
-FieldDecls	:	FieldDecl 
-                        { 
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(VC->idExpr("_RECORD_TYPE"));
-			  $$->push_back(*$1); 
-			  delete $1; 
-                        }
-		|	FieldDecls ',' FieldDecl 
-                        { 
-			  $1->push_back(*$3); 
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
+// Assert:
+//     ASSERT_TOK Expr { 
+//         $$ = NULL; // new CVC3::Expr(VC->listExpr("_ASSERT", *$2));
+//         // delete $2;
+//     } ;
 
-FieldDecl	:	Identifier ':' Type 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		;
-
-TupleType	:	'[' TypeList ']' 
-                         {
-			   $$ = new CVC4::Expr(VC->listExpr("_TUPLE_TYPE", *$2));
-			   delete $2;
-			 }
-		;
-
-TypeList	:	Type ',' Type
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-                          $$->push_back(*$3);
-			  delete $1;
-                          delete $3;
-			}
-		|	TypeList ',' Type 
-                        {
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-/* IndexType       :       SubrangeType { $$ = $1; } */
-/*                 |       Real /\* WART: maybe change to INTEGER when we */
-/* 				get that working? *\/ */
-/*                 |       Int */
-/*                         { $$ = $1; } */
-/*                 |       Identifier { $$ = $1; } */
-/*                 ; */
-
-ArrayType	:	ARRAY_TOK Type OF_TOK Type 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_ARRAY", *$2, *$4));
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-ScalarType	:	'{' IDs '}'
-			 {
-			   std::vector<CVC4::Expr>::iterator theIter = $2->begin();
-			   $2->insert(theIter, VC->idExpr("_SCALARTYPE"));
-			   $$ = new CVC4::Expr(VC->listExpr(*$2));
-			   delete $2;
-			 }
-		;
-
-SubType         :       SUBTYPE_TOK '(' Expr ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3));
-			  delete $3;
-			}
-                |       SUBTYPE_TOK '(' Expr ',' Expr ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3, *$5));
-                          delete $3;
-                          delete $5;
-                        }
-                ;
-
-BasicType	:       BOOLEAN_TOK 
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr("_BOOLEAN"));
-			}
-		|	Real
-		|       Int
-		;
-		
-BitvectorType   :       BITVECTOR_TOK '(' Numeral ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_BITVECTOR", *$3));
-			  delete $3;
-			}
-                ;
-
-Real            :       REAL_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr("_REAL"));
-			}
-                ;
-
-Int             :       INT_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr("_INT"));
-                        }
-                ;
-SubrangeType	:	'[' LeftBound DOTDOT_TOK RightBound ']'
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_SUBRANGE", *$2, *$4));
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-LeftBound	:	'_' 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_NEGINF")));
-			}
-		|	Numeral { $$ = $1; }
-                |       MINUS_TOK Numeral {
-                          CVC4::Rational value= -$2->getRational();
-			  $$ = new CVC4::Expr(VC->ratExpr(value.toString()));
-			  delete $2;
-                        }
-		;
-
-RightBound	:	'_' 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POSINF")));
-			}
-		|	Numeral { $$ = $1; }
-                |       MINUS_TOK Numeral {
-                          CVC4::Rational value= -$2->getRational();
-			  $$ = new CVC4::Expr(VC->ratExpr(value.toString()));
-			  delete $2;
-                        }
-		;
-
-/* right recursive to eliminate a conflict.  Reverses order? */
-reverseIDs	:	Identifier 
-                        { 
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	Identifier ',' reverseIDs 
-                        {
-			  $3->push_back(*$1);
-			  $$ = $3; 
-			  delete $1;
-			}
-		;
-
-IDs             :       reverseIDs
-                        {
-			  $$ = new std::vector<CVC4::Expr>($1->rbegin(),
-							   $1->rend());
-			  delete $1;
-			}
-                ;
-
-/* Grammar for exprs */
-
-Expr		:	Identifier { $$ = $1; }
-		|	Numeral { $$ = $1; }
-	        |       Binary { $$ = $1; }
-	        |       Hex { $$ = $1; }
-		|	Expr '(' Exprs ')'
-			{
-			  std::vector<CVC4::Expr> tmp;
-			  tmp.push_back(*$1);
-			  tmp.insert(tmp.end(), $3->begin(), $3->end());
-			  $$ = new CVC4::Expr(VC->listExpr(tmp));
-			  delete $1;
-			  delete $3;
-			}
-                |       SIMULATE_TOK '(' Exprs ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_SIMULATE", *$3));
-			  delete $3;
-			}
-		|	Expr '[' Expr ']' 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_READ", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr '.' Identifier 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_RECORD_SELECT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr '.' Numeral
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_TUPLE_SELECT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr WITH_TOK Updates
-			{
-			  $$ = new CVC4::Expr(CVC4::PLprocessUpdates(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Lambda { $$ = $1; }
-		|	QuantExpr { $$ = $1; }
-		|	LetExpr { $$ = $1; }
-
-		|	ArrayLiteral { $$ = $1; }
-
-		|	RecordLiteral { $$ = $1; }
-		|	TupleLiteral { $$ = $1; }
-		|	Conditional { $$ = $1; }
-
-		|	TRUELIT_TOK 
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR"));
-			}
-		|	FALSELIT_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR"));
-			}
-
-		|	MINUS_TOK Expr %prec UMINUS_TOK 
-			{
-			  if ($2->isRational())
-			  {
-			    CVC4::Rational value= -$2->getRational();
-			    $$= new CVC4::Expr(VC->ratExpr(value.toString()));
-			  }
-			  else
-			    $$ = new CVC4::Expr(VC->listExpr("_UMINUS", *$2));
-			  delete $2;
-			}
-		|	NOT_TOK Expr 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_NOT", *$2));
-			  delete $2;
-			}
-		|	IS_INTEGER_TOK Expr 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_IS_INTEGER", *$2));
-			  delete $2;
-			}
-		|	TCC_TOK '(' Expr ')'
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_TCC", *$3));
-			  delete $3;
-			}
-		|	Expr '=' Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_EQ", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-		|	Expr NEQ_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_NEQ", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr XOR_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_XOR", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-		|	OrExpr %prec OR_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_OR", *$1));
-			  delete $1;
-			} 
-		|	AndExpr %prec AND_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_AND", *$1));
-			  delete $1;
-			}
-		|	Expr IMPLIES_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_IMPLIES", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr IFF_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_IFF", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-		|	Expr PLUS_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_PLUS", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr MINUS_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_MINUS", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-                |       Expr MULT_TOK '(' Expr ',' Expr ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_TRANS_CLOSURE",
-							   *$1, *$4, *$6));
-			  delete $1;
-			  delete $4;
-			  delete $6;
-			}
-		|	Expr MULT_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_MULT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-		|	Expr POW_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_POW", *$3, *$1));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr DIV_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_DIVIDE", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			} 
-// 		|	Expr INTDIV_TOK Expr 
-//                         {
-// 			  $$ = new CVC4::Expr(VC->listExpr("_INTDIV", *$1, *$3));
-// 			  delete $1;
-// 			  delete $3;
-// 			} 
-// 		|	Expr MOD_TOK Expr 
-//                         {
-// 			  $$ = new CVC4::Expr(VC->listExpr("_MOD", *$1, *$3));
-// 			  delete $1;
-// 			  delete $3;
-// 			}
-		|	Expr GT_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_GT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr GE_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_GE", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	FLOOR_TOK '(' Expr ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_FLOOR", *$3));
-			  delete $3;
-			}
-		|	Expr LT_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_LT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Expr LE_TOK Expr 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_LE", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-                |       '(' Expr ')' 
-                         {
-			   $$ = $2;
-			 }
-	        |       BVNEG_TOK Expr
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_BVNEG", *$2));
-			  delete $2;
-			}
-	        |       Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']'
-			{
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_EXTRACT", VC->ratExpr(*$3),
-                                          VC->ratExpr(*$5), *$1));
-			  delete $1;
-			  delete $3;
-  			  delete $5;
-			}
-	        |       Expr BVAND_TOK Expr
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVAND", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-	        |       Expr MID_TOK Expr
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVOR", *$1, *$3)); 
-			  delete $1;
-			  delete $3;
-			}
-                |       Expr LEFTSHIFT_TOK NUMERAL_TOK
-                        {
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_LEFTSHIFT", *$1, VC->ratExpr(*$3)));
-			  delete $1;
-			  delete $3;
-                        }
-                |       Expr RIGHTSHIFT_TOK NUMERAL_TOK
-                        {
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_RIGHTSHIFT", *$1, VC->ratExpr(*$3)));
-			  delete $1;
-			  delete $3;
-                        }
-	        |       BVXOR_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVXOR", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVNAND_TOK '(' Expr ',' Expr ')' 
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVNAND", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-                |       BVNOR_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVNOR", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-                |       BVCOMP_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVCOMP", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVXNOR_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVXNOR", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-                |       SX_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_SX",*$3,VC->ratExpr(*$5)));
-			  delete $3;
-  			  delete $5;
-		        }
-                |       BVZEROEXTEND_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_BVZEROEXTEND",VC->ratExpr(*$5),*$3));
-			  delete $3;
-  			  delete $5;
-                        }
-                |       BVREPEAT_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_BVREPEAT",VC->ratExpr(*$5),*$3));
-			  delete $3;
-  			  delete $5;
-                        }
-                |       BVROTL_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_BVROTL",VC->ratExpr(*$5),*$3));
-			  delete $3;
-  			  delete $5;
-                        }
-                |       BVROTR_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_BVROTR",VC->ratExpr(*$5),*$3));
-			  delete $3;
-  			  delete $5;
-                        }
-	        |       BVLT_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVLT", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVGT_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVGT", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVLE_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVLE", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVGE_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVGE", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-
-	        |       BVSLT_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVSLT", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVSGT_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVSGT", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVSLE_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVSLE", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       BVSGE_TOK '(' Expr ',' Expr ')'
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVSGE", *$3, *$5));
-			  delete $3;
-			  delete $5;
-			}
-	        |       Expr CONCAT_TOK Expr
-	                {
-			  $$ = new CVC4::Expr(VC->listExpr("_CONCAT", *$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-                |      INTTOBV_TOK '(' Expr ',' NUMERAL_TOK ',' NUMERAL_TOK ')'
-			{
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_INTTOBV", *$3, VC->ratExpr(*$5),
-					  VC->ratExpr(*$7)));
-			  delete $3;
-			  delete $5;
-			  delete $7;
-			}
-                |       BVTOINT_TOK '(' Expr ')'
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_BVTOINT", *$3));
-			  delete $3;
-                        }
-                |       BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')'
-                        {
-			  //FIXME: this function is not to be exposed
-			  //to the user counterexamples containing
-			  //this function can be translated into
-			  //BV-EXTRACT and comparison with 0 or 1
-			  $$ = new CVC4::Expr(VC->listExpr("_BOOLEXTRACT", *$3,
-                                              VC->ratExpr(*$5)));
-			  delete $3;
-  			  delete $5;
-                        }
-                |       BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')'
-                        {
-			  std::vector<CVC4::Expr> k;
-			  k.push_back(VC->ratExpr(*$3));
-			  k.insert(k.end(), $5->begin(), $5->end()); 
-			  $$ = new CVC4::Expr(VC->listExpr("_BVPLUS", k));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVSUB", VC->ratExpr(*$3), *$5, *$7));
-			  delete $3;
-			  delete $5;
-			  delete $7;
-                        }
-                |       BVUDIV_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVUDIV", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVSDIV_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVSDIV", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVUREM_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVUREM", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVSREM_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVSREM", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVSMOD_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVSMOD", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVSHL_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVSHL", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVASHR_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVASHR", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVLSHR_TOK '(' Expr ',' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr
-                           (VC->listExpr("_BVLSHR", *$3, *$5));
-			  delete $3;
-			  delete $5;
-                        }
-                |       BVUMINUS_TOK '(' Expr ')'
-                        {
-			  $$ =  new CVC4::Expr(VC->listExpr("_BVUMINUS", *$3));
-			  delete $3;
-                        }
-                |       BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')'
-                        {
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_BVMULT", VC->ratExpr(*$3), *$5, *$7));
-			  delete $3;
-			  delete $5;
-			  delete $7;
-                        }
-                |       DISTINCT_TOK '(' Exprs ')'
-                        {
-                          $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3));
-                          delete $3;
-                        }
-		;
-AndExpr		:      AndExpr AND_TOK Expr
-                        {
-			  $1->push_back(*$3);
-                          $$ = $1;
-			  delete $3;
-			}
-
-                 |      Expr AND_TOK Expr
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  $$->push_back(*$3);
-			  delete $1;
-			  delete $3;
-                        }
-                ;
-
-
-OrExpr		:       OrExpr OR_TOK Expr
-                        {
-			  $1->push_back(*$3);
-                          $$ = $1;
-			  delete $3;
-			}
-
-                |	Expr OR_TOK Expr
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  $$->push_back(*$3);
-			  delete $1;
-			  delete $3;
-                        }
-                ;
-Conditional	:	IF_TOK Expr THEN_TOK Expr ElseRest 
-			{
-			  $5->push_back(VC->listExpr(*$2, *$4));
-			  $5->push_back(VC->idExpr("_COND"));
-			  /* at this point, the list for ElseRest is 
-			     in reverse order from what it should be. */
-			  std::vector<CVC4::Expr> tmp;
-			  tmp.insert(tmp.end(), $5->rbegin(), $5->rend());
-			  $$ = new CVC4::Expr(VC->listExpr(tmp));
-			  delete $2;
-			  delete $4;
-			  delete $5;
-			}
-		;
-
-ElseRest	:	ELSE_TOK Expr ENDIF_TOK 
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-	                  $$->push_back(VC->listExpr("_ELSE",*$2));
-			  delete $2;
-			}
-		|	ELSIF_TOK Expr THEN_TOK Expr ElseRest 
-			{
-			  /* NOTE that we're getting the list built
-			     up in the reverse order here.  We'll fix
-			     things when we produce a Conditional. */
-			  $5->push_back(VC->listExpr(*$2, *$4));
-			  $$ = $5;
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-Exprs		:	Expr 
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	Exprs ',' Expr 
-                        {
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-
-Pattern		:	PATTERN_TOK '(' Exprs ')' ':'
-                        {
-			  $$ = $3;
-			}
-
-Patterns	:	Pattern
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(VC->listExpr(*$1));
-			  delete $1;
-			}
-		|	Patterns Pattern
-                        {
-			  $1->push_back(VC->listExpr(*$2));
-			  $$ = $1; 
-			  delete $2;
-			}
-		;
-
-Update          :       UpdatePositionNode ASSIGN_TOK Expr
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-                ;
-
-Updates         :       Update
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-                |       Updates ',' Update
-                        {
-			  $$->push_back(*$3);
-			  delete $3;
-			}
-                ;
-
-UpdatePositionNode :    UpdatePosition 
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1;
-			}
-                ;
-
-UpdatePosition	:	'[' Expr ']' 
-			{
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(VC->listExpr("_READ", *$2));
-			  delete $2;
-			}
-                |       Identifier
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	'.' Identifier 
-			{
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(VC->listExpr("_RECORD_SELECT", *$2));
-			  delete $2;
-			}
-		|	'.' Numeral 
-			{
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(VC->listExpr("_TUPLE_SELECT", *$2));
-			  delete $2;
-			}
- 		|	UpdatePosition '[' Expr ']' 
-                        {
-			  $1->push_back(VC->listExpr("_READ", *$3));
-			  $$ = $1;
-			  delete $3;
-			}
-		|	UpdatePosition Identifier 
-                        {
-			  $1->push_back(*$2);
-			  $$ = $1;
-			  delete $2;
-			}
-		|	UpdatePosition '.' Identifier 
-                        {
-			  $1->push_back(VC->listExpr("_RECORD_SELECT",*$3));
-			  $$ = $1;
-			  delete $3;
-			}
-		|	UpdatePosition '.' Numeral 
-                        {
-			  $1->push_back(VC->listExpr("_TUPLE_SELECT", *$3));
-			  $$ = $1;
-			  delete $3;
-			}
-		;
-
-Lambda		:	LAMBDA_TOK '(' BoundVarDecls ')' ':' Expr 
-                        %prec ASSIGN_TOK
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_LAMBDA", 
-			                                   VC->listExpr(*$3), (*$6)));
-			  delete $3;
-			  delete $6;
-			}
-                ;
-QuantExpr	:	FORALL_TOK '(' BoundVarDecls ')' ':'  Expr
-		        %prec FORALL_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_FORALL", 
-			                                   VC->listExpr(*$3), *$6));
-			  delete $3;
-			  delete $6;
-			}
-                |	FORALL_TOK '(' BoundVarDecls ')' ':' Patterns Expr
-		        %prec FORALL_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_FORALL", 
-			                                   VC->listExpr(*$3), *$7,
-							   VC->listExpr(*$6)));
-			  delete $3;
-			  delete $6;
-			  delete $7;
-			}
-		|	EXISTS_TOK '(' BoundVarDecls ')' ':'  Expr
-		        %prec EXISTS_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_EXISTS", 
-			                                   VC->listExpr(*$3), (*$6)));
-			  delete $3;
-			  delete $6;
-			}
-		;
-                |	EXISTS_TOK '(' BoundVarDecls ')' ':' Patterns Expr
-		        %prec EXISTS_TOK
-                        {
-			  $$ = new CVC4::Expr(VC->listExpr("_EXISTS", 
-			                                   VC->listExpr(*$3), *$7,
-							   VC->listExpr(*$6)));
-			  delete $3;
-			  delete $6;
-			  delete $7;
-			}
-
-ArrayLiteral		: ARRAY_TOK '(' BoundVarDecl ')' ':' Expr 
-                        %prec ASSIGN_TOK
-			{
-			  $$ = new CVC4::Expr
-			    (VC->listExpr("_ARRAY_LITERAL", *$3, *$6));
-			  delete $3;
-			  delete $6;
-			}
-                ;
-RecordLiteral	:	PARENHASH_TOK RecordEntries HASHPAREN_TOK 
-			{
-			  $2->insert($2->begin(), VC->idExpr("_RECORD"));
-			  $$ = new CVC4::Expr(VC->listExpr(*$2));
-			  delete $2;
-			}
-		;
-
-RecordEntries	:	RecordEntry 
-                        { 
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1); 
-			  delete $1;
-			}
-		|	RecordEntries ',' RecordEntry 
-                        { 
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-RecordEntry	:	Identifier ASSIGN_TOK Expr 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-		;
-
-TupleLiteral	:	'(' Exprs ',' Expr ')' 
-                        {
-			  $2->push_back(*$4);
-			  $2->insert($2->begin(),VC->idExpr("_TUPLE"));
-			  $$ = new CVC4::Expr(VC->listExpr(*$2));
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-LetDeclsNode    :       LetDecls
-                        { 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1;
-			}
-                ;
-LetDecls	:	LetDecl { 
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-                        }
-		|	LetDecls ',' LetDecl 
-                        { 
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-LetDecl		:	Identifier '=' Expr 
-			{ 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1,*$3));
-			  delete $1;
-			  delete $3;
-			}
-                |       Identifier ':' Type '=' Expr
-			{ 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1,*$5));
-			  delete $1;
-			  delete $3;
-			  delete $5;
-			}
-		;
-
-LetExpr		:	LET_TOK LetDeclsNode IN_TOK Expr 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4));
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-TypeLetDeclsNode :      TypeLetDecls
-                        { 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1;
-			}
-                ;
-TypeLetDecls	:	TypeLetDecl { 
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-                        }
-		|	TypeLetDecls ',' TypeLetDecl 
-                        { 
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-TypeLetDecl	:	Identifier '=' Type 
-			{ 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
-			  delete $1;
-			  delete $3;
-			}
-                |       Identifier ':' TYPE_TOK '=' Type
-			{ 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1,*$5));
-			  delete $1;
-			  delete $5;
-			}
-		;
-
-TypeLetExpr	:	LET_TOK TypeLetDeclsNode IN_TOK Type 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4));
-			  delete $2;
-			  delete $4;
-			}
-		;
-
-BoundVarDecl	:	IDs ':' Type 
-			{
-			  $1->push_back(*$3);
-			  delete $3;
-			  $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1;
-			
-			}
-		;
-
-BoundVarDecls	:	BoundVarDecl 
-                        {
-			  $$ = new std::vector<CVC4::Expr>;
-			  $$->push_back(*$1);
-			  delete $1;
-			}
-		|	BoundVarDecls ',' BoundVarDecl 
-                        {
-			  $1->push_back(*$3);
-			  $$ = $1; 
-			  delete $3;
-			}
-		;
-
-BoundVarDeclNode:	BoundVarDecls 
-                        { 
-			  $$ = new CVC4::Expr(VC->listExpr(*$1));
-			  delete $1;
-			}
-                ;
-
-ConstDecl	:	Identifier ':' Type '=' Expr 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_CONST",
-							   *$1, *$3, *$5));
-			  delete $1;
-			  delete $3;
-			  delete $5;
-			}
-		|	Identifier ':' Type
-			{
-			  $$ =new CVC4::Expr
-			    (VC->listExpr("_CONST", VC->listExpr(*$1), *$3));
-			  delete $1;
-			  delete $3;
-			}
-		|	Identifier '(' BoundVarDeclNode ')' ':' Type '=' Expr
-			{
-			  std::vector<CVC4::Expr> tmp;
-			  tmp.push_back(VC->idExpr("_DEFUN"));
-			  tmp.push_back(*$1);
-			  tmp.push_back(*$3);
-			  tmp.push_back(*$6);
-			  tmp.push_back(*$8);
-			  $$ = new CVC4::Expr(VC->listExpr(tmp));
-			  delete $1;
-			  delete $3;
-			  delete $6;
-			  delete $8;
-			}
-		|	Identifier '(' BoundVarDeclNode ')' ':' Type
-			{
-			  std::vector<CVC4::Expr> tmp;
-			  tmp.push_back(VC->idExpr("_DEFUN"));
-			  tmp.push_back(*$1);
-			  tmp.push_back(*$3);
-			  tmp.push_back(*$6);
-			  $$ = new CVC4::Expr(VC->listExpr(tmp));
-			  delete $1;
-			  delete $3;
-			  delete $6;
-			}
-                |       Identifier ',' IDs ':' Type
-                        {
-			  $3->insert($3->begin(), *$1);
-			  $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$3), *$5));
-			  delete $1;
-			  delete $3;
-			  delete $5;
-			}
-		;
+Query:
+    QUERY_TOK Expr { 
+        $$ = NULL; // exprManager->mkExpr(Kind.TRUE);
+    }
+  | CHECKSAT_TOK Expr {
+      $$ = NULL; //new CVC3::Expr(VC->listExpr("_CHECKSAT", *$2));
+      //      delete $2;
+    }
+  | CHECKSAT_TOK {
+      $$ = NULL;
+      // new CVC3::Expr(VC->listExpr(VC->idExpr("_CHECKSAT")));
+    } ;
+
+Expr:	
+//    Identifier { $$ = $1; }
+//  | 
+    TRUELIT_TOK {
+      $$ = new Expr(EM->mkExpr(TRUE));
+    }
+  | FALSELIT_TOK {
+      $$ = new Expr(EM->mkExpr(FALSE));
+    }
+  | Expr OR_TOK Expr {
+      $$ = new Expr(EM->mkExpr(OR, *$1, *$3));
+      delete $1;
+      delete $3;
+    } 
+  | Expr AND_TOK Expr {
+      $$ = new Expr(EM->mkExpr(AND, *$1, *$3));
+      delete $1;
+      delete $3;
+    } 
+		// |	Expr IMPLIES_TOK Expr 
+                //         {
+		// 	  $$ = new CVC3::Expr(VC->listExpr("_IMPLIES", *$1, *$3));
+		// 	  delete $1;
+		// 	  delete $3;
+		// 	}
+		// |	Expr IFF_TOK Expr 
+                //         {
+		// 	  $$ = new CVC3::Expr(VC->listExpr("_IFF", *$1, *$3));
+		// 	  delete $1;
+		// 	  delete $3;
+		// 	} 
+;
+
+
+// Identifier:
+//     ID_TOK {
+//         $$ = EM->mkExpr(VARIABLE, *$1);
+//         delete $1;
+//     }
 
-TypeDecl        :       DataType { $$ = $1; }
-                |       Identifier ':' TYPE_TOK '=' TypeDef 
-			{
-			  $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", *$1, *$5));
-			  delete $1;
-			  delete $5;
-			}
-                |       Identifier ':' TYPE_TOK
-			{
-			  $$ =new CVC4::Expr(VC->listExpr("_TYPE", *$1));
-			  delete $1;
-			}
-                |       Identifier ',' IDs ':' TYPE_TOK
-                        {
-			  std::vector<CVC4::Expr> tmp;
-			  tmp.push_back(*$1);
-			  tmp.insert(tmp.end(), $3->begin(), $3->end());
-			  $$ = new CVC4::Expr(VC->listExpr("_TYPE", tmp));
-			  delete $1;
-			  delete $3;
-			}
-		;
 %%