Migrate a majority of the functionality in parsers to the new API (#3838)

This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.

Remaining tasks:

Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.

Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.

This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.

1 files changed, 345 insertions, 334 deletions

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index afa072e6d..2568101c4 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -73,12 +73,12 @@ using namespace CVC4::parser;
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE
 #define PARSER_STATE ((Tptp*)LEXER->super)
-#undef EXPR_MANAGER
-#define EXPR_MANAGER PARSER_STATE->getExprManager()
-#undef MK_EXPR
-#define MK_EXPR EXPR_MANAGER->mkExpr
-#undef MK_CONST
-#define MK_CONST EXPR_MANAGER->mkConst
+#undef SOLVER
+#define SOLVER PARSER_STATE->getSolver()
+#undef MK_TERM
+#define MK_TERM SOLVER->mkTerm
+#undef MK_TERM
+#define MK_TERM SOLVER->mkTerm
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
 }/* @lexer::postinclude */
@@ -101,6 +101,7 @@ using namespace CVC4::parser;
 #include <iterator>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
@@ -118,21 +119,18 @@ using namespace CVC4::parser;
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE
 #define PARSER_STATE ((Tptp*)PARSER->super)
-#undef EXPR_MANAGER
-#define EXPR_MANAGER PARSER_STATE->getExprManager()
-#undef MK_EXPR
-#define MK_EXPR EXPR_MANAGER->mkExpr
-#undef MK_EXPR_ASSOCIATIVE
-#define MK_EXPR_ASSOCIATIVE EXPR_MANAGER->mkAssociative
-#undef MK_CONST
-#define MK_CONST EXPR_MANAGER->mkConst
+#undef SOLVER
+#define SOLVER PARSER_STATE->getSolver()
+#undef MK_TERM
+#define MK_TERM SOLVER->mkTerm
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
 }/* parser::postinclude */
 
 /**
  * Parses an expression.
- * @return the parsed expression, or the Null Expr if we've reached the end of the input
+ * @return the parsed expression, or the Null CVC4::api::Term if we've reached
+ * the end of the input
  */
 parseExpr returns [CVC4::parser::tptp::myExpr expr]
   : cnfFormula[expr]
@@ -145,7 +143,7 @@ parseExpr returns [CVC4::parser::tptp::myExpr expr]
  */
 parseCommand returns [CVC4::Command* cmd = NULL]
 @declarations {
-  Expr expr;
+  CVC4::api::Term expr;
   Tptp::FormulaRole fr;
   std::string name, inclSymbol;
   ParseOp p;
@@ -156,17 +154,17 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     PARSER_STATE->pushScope(); }
     cnfFormula[expr]
   { PARSER_STATE->popScope();
-    std::vector<Expr> bvl = PARSER_STATE->getFreeVar();
+    std::vector<api::Term> bvl = PARSER_STATE->getFreeVar();
     if(!bvl.empty()) {
-      expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr);
+      expr = MK_TERM(api::FORALL,MK_TERM(api::BOUND_VAR_LIST,bvl),expr);
     };
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      Expr aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
+      CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
       if( !aexpr.isNull() ){
         // set the expression name (e.g. used with unsat core printing)
-        Command* csen = new SetExpressionNameCommand(aexpr, name);
+        Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
@@ -177,10 +175,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); }
     fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      Expr aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
+      CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
       if( !aexpr.isNull() ){
         // set the expression name (e.g. used with unsat core printing)
-        Command* csen = new SetExpressionNameCommand(aexpr, name);
+        Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
@@ -193,10 +191,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); }
       tffFormula[expr] (COMMA_TOK anything*)?
       {
-        Expr aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
+        CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
         if( !aexpr.isNull() ){
           // set the expression name (e.g. used with unsat core printing)
-          Command* csen = new SetExpressionNameCommand(aexpr, name);
+          Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
           csen->setMuted(true);
           PARSER_STATE->preemptCommand(csen);
         }
@@ -217,11 +215,11 @@ parseCommand returns [CVC4::Command* cmd = NULL]
           PARSER_STATE->parseError("Top level expression must be a formula");
         }
         expr = p.d_expr;
-        Expr aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
+        CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
         if (!aexpr.isNull())
         {
           // set the expression name (e.g. used with unsat core printing)
-          Command* csen = new SetExpressionNameCommand(aexpr, name);
+          Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
           csen->setMuted(true);
           PARSER_STATE->preemptCommand(csen);
         }
@@ -254,10 +252,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     {
       CommandSequence* seq = new CommandSequence();
       // assert that all distinct constants are distinct
-      Expr aexpr = PARSER_STATE->getAssertionDistinctConstants();
+      CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants();
       if( !aexpr.isNull() )
       {
-        seq->addCommand(new AssertCommand(aexpr, false));
+        seq->addCommand(new AssertCommand(aexpr.getExpr(), false));
       }
 
       std::string filename = PARSER_STATE->getInput()->getInputStreamName();
@@ -270,7 +268,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       }
       seq->addCommand(new SetInfoCommand("filename", SExpr(filename)));
       if(PARSER_STATE->hasConjecture()) {
-        seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
+        seq->addCommand(new QueryCommand(SOLVER->mkFalse().getExpr()));
       } else {
         seq->addCommand(new CheckSatCommand());
       }
@@ -308,33 +306,33 @@ formulaRole[CVC4::parser::Tptp::FormulaRole& role]
 /* It can parse a little more than the cnf grammar: false and true can appear.
  * Normally only false can appear and only at top level. */
 
-cnfFormula[CVC4::Expr& expr]
+cnfFormula[CVC4::api::Term& expr]
   : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK
   | cnfDisjunction[expr]
 ;
 
-cnfDisjunction[CVC4::Expr& expr]
+cnfDisjunction[CVC4::api::Term& expr]
 @declarations {
-  std::vector<Expr> args;
+  std::vector<api::Term> args;
 }
   : cnfLiteral[expr] { args.push_back(expr); }
     ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )*
     { if(args.size() > 1) {
-        expr = MK_EXPR_ASSOCIATIVE(kind::OR, args);
+        expr = MK_TERM(api::OR, args);
       } // else its already in the expr
     }
 ;
 
-cnfLiteral[CVC4::Expr& expr]
+cnfLiteral[CVC4::api::Term& expr]
   : atomicFormula[expr]
-  | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); }
+  | NOT_TOK atomicFormula[expr] { expr = MK_TERM(api::NOT, expr); }
   ;
 
-atomicFormula[CVC4::Expr& expr]
+atomicFormula[CVC4::api::Term& expr]
 @declarations {
-  Expr expr2;
+  CVC4::api::Term expr2;
   std::string name;
-  std::vector<CVC4::Expr> args;
+  std::vector<CVC4::api::Term> args;
   bool equal;
   ParseOp p;
 }
@@ -346,15 +344,15 @@ atomicFormula[CVC4::Expr& expr]
         args.clear();
         args.push_back(expr);
         args.push_back(expr2);
-        ParseOp p1(kind::EQUAL);
+        ParseOp p1(api::EQUAL);
         expr = PARSER_STATE->applyParseOp(p1, args);
         if (!equal)
         {
-          expr = MK_EXPR(kind::NOT, expr);
+          expr = MK_TERM(api::NOT, expr);
         }
       }
     | { // predicate
-        p.d_type = EXPR_MANAGER->booleanType();
+        p.d_type = SOLVER->getBooleanSort();
         expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
                             : PARSER_STATE->applyParseOp(p, args);
       }
@@ -368,11 +366,11 @@ atomicFormula[CVC4::Expr& expr]
        args.clear();
        args.push_back(expr);
        args.push_back(expr2);
-       ParseOp p1(kind::EQUAL);
+       ParseOp p1(api::EQUAL);
        expr = PARSER_STATE->applyParseOp(p1, args);
        if (!equal)
        {
-         expr = MK_EXPR(kind::NOT, expr);
+         expr = MK_TERM(api::NOT, expr);
        }
      }
     )
@@ -382,17 +380,17 @@ atomicFormula[CVC4::Expr& expr]
       { // equality/disequality between terms
         args.push_back(expr);
         args.push_back(expr2);
-        p.d_kind = kind::EQUAL;
+        p.d_kind = api::EQUAL;
         expr = PARSER_STATE->applyParseOp(p, args);
         if (!equal)
         {
-          expr = MK_EXPR(kind::NOT, expr);
+          expr = MK_TERM(api::NOT, expr);
         }
       }
     )?
   | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)
     {
-      p.d_type = EXPR_MANAGER->booleanType();
+      p.d_type = SOLVER->getBooleanSort();
       expr = PARSER_STATE->applyParseOp(p, args);
     }
   | definedProp[expr]
@@ -400,9 +398,9 @@ atomicFormula[CVC4::Expr& expr]
 
 thfAtomicFormula[CVC4::ParseOp& p]
 @declarations {
-  Expr expr2;
+  CVC4::api::Term expr2;
   std::string name;
-  std::vector<CVC4::Expr> args;
+  std::vector<CVC4::api::Term> args;
   bool equal;
 }
   : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
@@ -419,11 +417,11 @@ thfAtomicFormula[CVC4::ParseOp& p]
         args.clear();
         args.push_back(p.d_expr);
         args.push_back(expr2);
-        ParseOp p1(kind::EQUAL);
+        ParseOp p1(api::EQUAL);
         p.d_expr = PARSER_STATE->applyParseOp(p1, args);
         if (!equal)
         {
-          p.d_expr = MK_EXPR(kind::NOT, p.d_expr);
+          p.d_expr = MK_TERM(api::NOT, p.d_expr);
         }
       }
     )?
@@ -432,7 +430,7 @@ thfAtomicFormula[CVC4::ParseOp& p]
   | conditionalTerm[p.d_expr]
   | thfDefinedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)?
     {
-      p.d_type = EXPR_MANAGER->booleanType();
+      p.d_type = SOLVER->getBooleanSort();
       if (!args.empty())
       {
         p.d_expr = PARSER_STATE->applyParseOp(p, args);
@@ -444,130 +442,130 @@ thfAtomicFormula[CVC4::ParseOp& p]
 //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
 //%----Note: "defined" means a word starting with one $ and "system" means $$.
 
-definedProp[CVC4::Expr& expr]
-  : TRUE_TOK { expr = MK_CONST(bool(true)); }
-  | FALSE_TOK  { expr = MK_CONST(bool(false)); }
+definedProp[CVC4::api::Term& expr]
+  : TRUE_TOK { expr = SOLVER->mkTrue(); }
+  | FALSE_TOK  { expr = SOLVER->mkFalse(); }
   ;
 
 definedPred[CVC4::ParseOp& p]
   : '$less'
     {
-      p.d_kind = kind::LT;
+      p.d_kind = api::LT;
     }
   | '$lesseq'
     {
-      p.d_kind = kind::LEQ;
+      p.d_kind = api::LEQ;
     }
   | '$greater'
     {
-      p.d_kind = kind::GT;
+      p.d_kind = api::GT;
     }
   | '$greatereq'
     {
-      p.d_kind = kind::GEQ;
+      p.d_kind = api::GEQ;
     }
   | '$is_rat'
     // a real n is a rational if there exists q,r integers such that
     //   to_real(q) = n*to_real(r),
     // where r is non-zero.
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
-      Expr qr = MK_EXPR(kind::TO_REAL, q);
-      Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
-      Expr rr = MK_EXPR(kind::TO_REAL, r);
-      Expr body =
-          MK_EXPR(kind::AND,
-                  MK_EXPR(kind::NOT,
-                          MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))),
-                  MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr)));
-      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r);
-      body = MK_EXPR(kind::EXISTS, bvl, body);
-      Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n);
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body);
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term q = SOLVER->mkVar(SOLVER->getIntegerSort(), "Q");
+      api::Term qr = MK_TERM(api::TO_REAL, q);
+      api::Term r = SOLVER->mkVar(SOLVER->getIntegerSort(), "R");
+      api::Term rr = MK_TERM(api::TO_REAL, r);
+      api::Term body =
+          MK_TERM(api::AND,
+                  MK_TERM(api::NOT,
+                          MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                  MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
+      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      body = MK_TERM(api::EXISTS, bvl, body);
+      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
   | '$is_int'
     {
-      p.d_kind = kind::IS_INTEGER;
+      p.d_kind = api::IS_INTEGER;
     }
   | '$distinct'
     {
-      p.d_kind = kind::DISTINCT;
+      p.d_kind = api::DISTINCT;
     }
   | AND_TOK
     {
-      p.d_kind = kind::AND;
+      p.d_kind = api::AND;
     }
   | IMPLIES_TOK
     {
-      p.d_kind = kind::IMPLIES;
+      p.d_kind = api::IMPLIES;
     }
   | OR_TOK
     {
-      p.d_kind = kind::OR;
+      p.d_kind = api::OR;
     }
   ;
 
 thfDefinedPred[CVC4::ParseOp& p]
   : '$less'
      {
-       p.d_kind = kind::LT;
+       p.d_kind = api::LT;
      }
   | '$lesseq'
     {
-      p.d_kind = kind::LEQ;
+      p.d_kind = api::LEQ;
     }
   | '$greater'
     {
-      p.d_kind = kind::GT;
+      p.d_kind = api::GT;
     }
   | '$greatereq'
     {
-      p.d_kind = kind::GEQ;
+      p.d_kind = api::GEQ;
     }
   | '$is_rat'
     // a real n is a rational if there exists q,r integers such that
     //   to_real(q) = n*to_real(r),
     // where r is non-zero.
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
-      Expr qr = MK_EXPR(kind::TO_REAL, q);
-      Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
-      Expr rr = MK_EXPR(kind::TO_REAL, r);
-      Expr body = MK_EXPR(
-          kind::AND,
-          MK_EXPR(kind::NOT,
-                  MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))),
-          MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr)));
-      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r);
-      body = MK_EXPR(kind::EXISTS, bvl, body);
-      Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n);
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body);
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term q = SOLVER->mkVar(SOLVER->getIntegerSort(), "Q");
+      api::Term qr = MK_TERM(api::TO_REAL, q);
+      api::Term r = SOLVER->mkVar(SOLVER->getIntegerSort(), "R");
+      api::Term rr = MK_TERM(api::TO_REAL, r);
+      api::Term body = MK_TERM(
+          api::AND,
+          MK_TERM(api::NOT,
+                  MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+          MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
+      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      body = MK_TERM(api::EXISTS, bvl, body);
+      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
   | '$is_int'
     {
-      p.d_kind = kind::IS_INTEGER;
+      p.d_kind = api::IS_INTEGER;
     }
   | '$distinct'
     {
-      p.d_kind = kind::DISTINCT;
+      p.d_kind = api::DISTINCT;
     }
   | LPAREN_TOK
     (
       AND_TOK
       {
-        p.d_kind = kind::AND;
+        p.d_kind = api::AND;
       }
     | OR_TOK
       {
-        p.d_kind = kind::OR;
+        p.d_kind = api::OR;
       }
     | IMPLIES_TOK
       {
-        p.d_kind = kind::IMPLIES;
+        p.d_kind = api::IMPLIES;
       }
     )
     RPAREN_TOK
@@ -579,152 +577,152 @@ definedFun[CVC4::ParseOp& p]
 }
   : '$uminus'
     {
-      p.d_kind = kind::UMINUS;
+      p.d_kind = api::UMINUS;
     }
   | '$sum'
     {
-      p.d_kind = kind::PLUS;
+      p.d_kind = api::PLUS;
     }
   | '$difference'
     {
-      p.d_kind = kind::MINUS;
+      p.d_kind = api::MINUS;
     }
   | '$product'
     {
-      p.d_kind = kind::MULT;
+      p.d_kind = api::MULT;
     }
   | '$quotient'
     {
-      p.d_kind = kind::DIVISION;
+      p.d_kind = api::DIVISION;
     }
   | ( '$quotient_e' { remainder = false; }
     | '$remainder_e' { remainder = true; }
     )
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
-      Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
-      expr = MK_EXPR(kind::ITE,
-                     MK_EXPR(kind::GEQ, d, MK_CONST(Rational(0))),
-                     MK_EXPR(kind::TO_INTEGER, expr),
-                     MK_EXPR(kind::UMINUS,
-                             MK_EXPR(kind::TO_INTEGER,
-                                     MK_EXPR(kind::UMINUS, expr))));
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term expr = MK_TERM(api::DIVISION, n, d);
+      expr = MK_TERM(api::ITE,
+                     MK_TERM(api::GEQ, d, SOLVER->mkReal(0)),
+                     MK_TERM(api::TO_INTEGER, expr),
+                     MK_TERM(api::UMINUS,
+                             MK_TERM(api::TO_INTEGER,
+                                     MK_TERM(api::UMINUS, expr))));
       if (remainder)
       {
-        expr = MK_EXPR(
-            kind::TO_INTEGER,
-            MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
+        expr = MK_TERM(
+            api::TO_INTEGER,
+            MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
       }
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
     }
   | ( '$quotient_t' { remainder = false; }
     | '$remainder_t' { remainder = true; }
     )
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
-      Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
-      expr = MK_EXPR(kind::ITE,
-                     MK_EXPR(kind::GEQ, expr, MK_CONST(Rational(0))),
-                     MK_EXPR(kind::TO_INTEGER, expr),
-                     MK_EXPR(kind::UMINUS,
-                             MK_EXPR(kind::TO_INTEGER,
-                                     MK_EXPR(kind::UMINUS, expr))));
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term expr = MK_TERM(api::DIVISION, n, d);
+      expr = MK_TERM(api::ITE,
+                     MK_TERM(api::GEQ, expr, SOLVER->mkReal(0)),
+                     MK_TERM(api::TO_INTEGER, expr),
+                     MK_TERM(api::UMINUS,
+                             MK_TERM(api::TO_INTEGER,
+                                     MK_TERM(api::UMINUS, expr))));
       if (remainder)
       {
-        expr = MK_EXPR(
-            kind::TO_INTEGER,
-            MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
+        expr = MK_TERM(
+            api::TO_INTEGER,
+            MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
       }
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
     }
   | ( '$quotient_f' { remainder = false; }
     | '$remainder_f' { remainder = true; }
     )
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
-      Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
-      expr = MK_EXPR(kind::TO_INTEGER, expr);
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term expr = MK_TERM(api::DIVISION, n, d);
+      expr = MK_TERM(api::TO_INTEGER, expr);
       if (remainder)
       {
-        expr = MK_EXPR(kind::TO_INTEGER,
-                       MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
+        expr = MK_TERM(api::TO_INTEGER,
+                       MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
       }
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
     }
   | '$floor'
     {
-      p.d_kind = kind::TO_INTEGER;
+      p.d_kind = api::TO_INTEGER;
     }
   | '$ceiling'
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
-      Expr expr = MK_EXPR(kind::UMINUS,
-                          MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n)));
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term expr = MK_TERM(api::UMINUS,
+                          MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n)));
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
     }
   | '$truncate'
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
-      Expr expr =
-          MK_EXPR(kind::ITE,
-                  MK_EXPR(kind::GEQ, n, MK_CONST(Rational(0))),
-                  MK_EXPR(kind::TO_INTEGER, n),
-                  MK_EXPR(kind::UMINUS,
-                          MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n))));
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term expr =
+          MK_TERM(api::ITE,
+                  MK_TERM(api::GEQ, n, SOLVER->mkReal(0)),
+                  MK_TERM(api::TO_INTEGER, n),
+                  MK_TERM(api::UMINUS,
+                          MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n))));
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
     }
   | '$round'
     {
-      Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
-      Expr decPart = MK_EXPR(kind::MINUS, n, MK_EXPR(kind::TO_INTEGER, n));
-      Expr expr = MK_EXPR(
-          kind::ITE,
-          MK_EXPR(kind::LT, decPart, MK_CONST(Rational(1, 2))),
+      api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
+      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term decPart = MK_TERM(api::MINUS, n, MK_TERM(api::TO_INTEGER, n));
+      api::Term expr = MK_TERM(
+          api::ITE,
+          MK_TERM(api::LT, decPart, SOLVER->mkReal(1, 2)),
           // if decPart < 0.5, round down
-          MK_EXPR(kind::TO_INTEGER, n),
-          MK_EXPR(kind::ITE,
-                  MK_EXPR(kind::GT, decPart, MK_CONST(Rational(1, 2))),
+          MK_TERM(api::TO_INTEGER, n),
+          MK_TERM(api::ITE,
+                  MK_TERM(api::GT, decPart, SOLVER->mkReal(1, 2)),
                   // if decPart > 0.5, round up
-                  MK_EXPR(kind::TO_INTEGER,
-                          MK_EXPR(kind::PLUS, n, MK_CONST(Rational(1)))),
+                  MK_TERM(api::TO_INTEGER,
+                          MK_TERM(api::PLUS, n, SOLVER->mkReal(1))),
                   // if decPart == 0.5, round to nearest even integer:
                   // result is: to_int(n/2 + .5) * 2
-                  MK_EXPR(kind::MULT,
-                          MK_EXPR(kind::TO_INTEGER,
-                                  MK_EXPR(kind::PLUS,
-                                          MK_EXPR(kind::DIVISION_TOTAL,
+                  MK_TERM(api::MULT,
+                          MK_TERM(api::TO_INTEGER,
+                                  MK_TERM(api::PLUS,
+                                          MK_TERM(api::DIVISION,
                                                   n,
-                                                  MK_CONST(Rational(2))),
-                                          MK_CONST(Rational(1, 2)))),
-                          MK_CONST(Rational(2)))));
-      p.d_kind = kind::LAMBDA;
-      p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+                                                  SOLVER->mkReal(2)),
+                                          SOLVER->mkReal(1, 2))),
+                          SOLVER->mkReal(2))));
+      p.d_kind = api::LAMBDA;
+      p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
       }
   | '$to_int'
     {
-      p.d_kind = kind::TO_INTEGER;
+      p.d_kind = api::TO_INTEGER;
     }
   | '$to_rat'
     {
-      p.d_kind = kind::TO_REAL;
+      p.d_kind = api::TO_REAL;
     }
   | '$to_real'
     {
-      p.d_kind = kind::TO_REAL;
+      p.d_kind = api::TO_REAL;
     }
   ;
 
@@ -736,16 +734,16 @@ equalOp[bool& equal]
   | DISEQUAL_TOK { equal = false; }
   ;
 
-term[CVC4::Expr& expr]
+term[CVC4::api::Term& expr]
   : functionTerm[expr]
   | conditionalTerm[expr]
   | simpleTerm[expr]
   | letTerm[expr]
   ;
 
-letTerm[CVC4::Expr& expr]
+letTerm[CVC4::api::Term& expr]
 @declarations {
-  CVC4::Expr lhs, rhs;
+  CVC4::api::Term lhs, rhs;
 }
   : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); }
     tffLetFormulaDefn[lhs, rhs] COMMA_TOK
@@ -764,14 +762,14 @@ letTerm[CVC4::Expr& expr]
   ;
 
 /* Not an application */
-simpleTerm[CVC4::Expr& expr]
+simpleTerm[CVC4::api::Term& expr]
   : variable[expr]
   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
   | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); }
   ;
 
 /* Not an application */
-thfSimpleTerm[CVC4::Expr& expr]
+thfSimpleTerm[CVC4::api::Term& expr]
   : NUMBER { expr = PARSER_STATE->d_tmp_expr; }
   | DISTINCT_OBJECT
     {
@@ -780,9 +778,9 @@ thfSimpleTerm[CVC4::Expr& expr]
     }
   ;
 
-functionTerm[CVC4::Expr& expr]
+functionTerm[CVC4::api::Term& expr]
 @declarations {
-  std::vector<CVC4::Expr> args;
+  std::vector<CVC4::api::Term> args;
   ParseOp p;
 }
   : plainTerm[expr]
@@ -792,18 +790,18 @@ functionTerm[CVC4::Expr& expr]
     }
   ;
 
-conditionalTerm[CVC4::Expr& expr]
+conditionalTerm[CVC4::api::Term& expr]
 @declarations {
-  CVC4::Expr expr2, expr3;
+  CVC4::api::Term expr2, expr3;
 }
   : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK
-    { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, expr2, expr3); }
+    { expr = MK_TERM(api::ITE, expr, expr2, expr3); }
   ;
 
-plainTerm[CVC4::Expr& expr]
+plainTerm[CVC4::api::Term& expr]
 @declarations {
   std::string name;
-  std::vector<Expr> args;
+  std::vector<api::Term> args;
   ParseOp p;
 }
   : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
@@ -813,22 +811,22 @@ plainTerm[CVC4::Expr& expr]
     }
   ;
 
-arguments[std::vector<CVC4::Expr>& args]
+arguments[std::vector<CVC4::api::Term>& args]
 @declarations {
-  Expr expr;
+  CVC4::api::Term expr;
 }
   :
   term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )*
   ;
 
-variable[CVC4::Expr& expr]
+variable[CVC4::api::Term& expr]
   : UPPER_WORD
     {
       std::string name = AntlrInput::tokenText($UPPER_WORD);
       if(!PARSER_STATE->cnf() || PARSER_STATE->isDeclared(name)) {
         expr = PARSER_STATE->getVariable(name);
       } else {
-        expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
+        expr = PARSER_STATE->bindBoundVar(name, PARSER_STATE->d_unsorted);
         if(PARSER_STATE->cnf()) PARSER_STATE->addFreeVar(expr);
       }
     }
@@ -836,35 +834,35 @@ variable[CVC4::Expr& expr]
 
 /*******/
 /* FOF */
-fofFormula[CVC4::Expr& expr] : fofLogicFormula[expr] ;
+fofFormula[CVC4::api::Term& expr] : fofLogicFormula[expr] ;
 
-fofLogicFormula[CVC4::Expr& expr]
+fofLogicFormula[CVC4::api::Term& expr]
 @declarations {
   tptp::NonAssoc na;
-  std::vector< Expr > args;
-  Expr expr2;
+  std::vector< CVC4::api::Term > args;
+  CVC4::api::Term expr2;
 }
   : fofUnitaryFormula[expr]
     ( // Non-associative: <=> <~> ~& ~|
       ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
         { switch(na) {
            case tptp::NA_IFF:
-             expr = MK_EXPR(kind::EQUAL,expr,expr2);
+             expr = MK_TERM(api::EQUAL,expr,expr2);
              break;
            case tptp::NA_REVIFF:
-             expr = MK_EXPR(kind::XOR,expr,expr2);
+             expr = MK_TERM(api::XOR,expr,expr2);
              break;
            case tptp::NA_IMPLIES:
-             expr = MK_EXPR(kind::IMPLIES,expr,expr2);
+             expr = MK_TERM(api::IMPLIES,expr,expr2);
              break;
            case tptp::NA_REVIMPLIES:
-             expr = MK_EXPR(kind::IMPLIES,expr2,expr);
+             expr = MK_TERM(api::IMPLIES,expr2,expr);
              break;
            case tptp::NA_REVOR:
-             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2));
+             expr = MK_TERM(api::NOT,MK_TERM(api::OR,expr,expr2));
              break;
            case tptp::NA_REVAND:
-             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2));
+             expr = MK_TERM(api::NOT,MK_TERM(api::AND,expr,expr2));
              break;
           }
         }
@@ -872,38 +870,38 @@ fofLogicFormula[CVC4::Expr& expr]
     | // N-ary and &
       ( { args.push_back(expr); }
         ( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); }
+        { expr = MK_TERM(api::AND, args); }
       )
     | // N-ary or |
       ( { args.push_back(expr); }
         ( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); }
+        { expr = MK_TERM(api::OR, args); }
       )
     )?
   ;
 
-fofUnitaryFormula[CVC4::Expr& expr]
+fofUnitaryFormula[CVC4::api::Term& expr]
 @declarations {
-  Kind kind;
-  std::vector< Expr > bv;
+  api::Kind kind;
+  std::vector< CVC4::api::Term > bv;
 }
   : atomicFormula[expr]
   | LPAREN_TOK fofLogicFormula[expr] RPAREN_TOK
-  | NOT_TOK fofUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
+  | NOT_TOK fofUnitaryFormula[expr] { expr = MK_TERM(api::NOT,expr); }
   | // Quantified
     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
     ( bindvariable[expr] { bv.push_back(expr); }
       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK fofUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
     }
   ;
 
-bindvariable[CVC4::Expr& expr]
+bindvariable[CVC4::api::Term& expr]
   : UPPER_WORD
     { std::string name = AntlrInput::tokenText($UPPER_WORD);
-      expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
+      expr = PARSER_STATE->bindBoundVar(name, PARSER_STATE->d_unsorted);
     }
   ;
 
@@ -916,19 +914,19 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na]
   | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; }
   ;
 
-folQuantifier[CVC4::Kind& kind]
-  : FORALL_TOK { kind = kind::FORALL; }
-  | EXISTS_TOK { kind = kind::EXISTS; }
+folQuantifier[CVC4::api::Kind& kind]
+  : FORALL_TOK { kind = api::FORALL; }
+  | EXISTS_TOK { kind = api::EXISTS; }
   ;
 
 /*******/
 /* THF */
 
-thfQuantifier[CVC4::Kind& kind]
-  : FORALL_TOK { kind = kind::FORALL; }
-  | EXISTS_TOK { kind = kind::EXISTS; }
-  | LAMBDA_TOK { kind = kind::LAMBDA; }
-  | CHOICE_TOK { kind = kind::CHOICE; }
+thfQuantifier[CVC4::api::Kind& kind]
+  : FORALL_TOK { kind = api::FORALL; }
+  | EXISTS_TOK { kind = api::EXISTS; }
+  | LAMBDA_TOK { kind = api::LAMBDA; }
+  | CHOICE_TOK { kind = api::CHOICE; }
   | DEF_DESC_TOK
     {
       UNSUPPORTED("Description quantifier");
@@ -942,8 +940,8 @@ thfQuantifier[CVC4::Kind& kind]
 thfAtomTyping[CVC4::Command*& cmd]
 // for now only supports mapping types (i.e. no applied types)
 @declarations {
-  CVC4::Expr expr;
-  CVC4::Type type;
+  CVC4::api::Term expr;
+  CVC4::api::Sort type;
   std::string name;
 }
   : LPAREN_TOK thfAtomTyping[cmd] RPAREN_TOK
@@ -965,8 +963,8 @@ thfAtomTyping[CVC4::Command*& cmd]
         else
         {
           // as yet, it's undeclared
-          Type atype = PARSER_STATE->mkSort(name);
-          cmd = new DeclareTypeCommand(name, 0, atype);
+          api::Sort atype = PARSER_STATE->mkSort(name);
+          cmd = new DeclareTypeCommand(name, 0, atype.getType());
         }
       }
     | parseThfType[type]
@@ -980,7 +978,7 @@ thfAtomTyping[CVC4::Command*& cmd]
         }
         else if (PARSER_STATE->isDeclared(name, SYM_VARIABLE))
         {
-          if (type == PARSER_STATE->getVariable(name).getType())
+          if (type == PARSER_STATE->getVariable(name).getSort())
           {
             // duplicate declaration is fine, they're compatible
             cmd = new EmptyCommand("compatible redeclaration of constant "
@@ -997,16 +995,17 @@ thfAtomTyping[CVC4::Command*& cmd]
         else
         {
           // as of yet, it's undeclared
-          CVC4::Expr freshExpr;
+          CVC4::api::Term freshExpr;
           if (type.isFunction())
           {
-            freshExpr = PARSER_STATE->mkVar(name, type);
+            freshExpr = PARSER_STATE->bindVar(name, type);
           }
           else
           {
-            freshExpr = PARSER_STATE->mkVar(name, type);
+            freshExpr = PARSER_STATE->bindVar(name, type);
           }
-          cmd = new DeclareFunctionCommand(name, freshExpr, type);
+          cmd = new DeclareFunctionCommand(
+              name, freshExpr.getExpr(), type.getType());
         }
       }
     )
@@ -1015,9 +1014,9 @@ thfAtomTyping[CVC4::Command*& cmd]
 thfLogicFormula[CVC4::ParseOp& p]
 @declarations {
   tptp::NonAssoc na;
-  std::vector<Expr> args;
+  std::vector<CVC4::api::Term> args;
   std::vector<ParseOp> p_args;
-  Expr expr2;
+  CVC4::api::Term expr2;
   bool equal;
   ParseOp p1;
 }
@@ -1032,13 +1031,13 @@ thfLogicFormula[CVC4::ParseOp& p]
         {
           // make p.d_expr with a lambda of the same type as p1.d_expr
           p.d_expr =
-              PARSER_STATE->mkLambdaWrapper(p.d_kind, p1.d_expr.getType());
+              PARSER_STATE->mkLambdaWrapper(p.d_kind, p1.d_expr.getSort());
         }
         else if (p1.d_expr.isNull() && !p.d_expr.isNull())
         {
           // make p1.d_expr with a lambda of the same type as p.d_expr
           p1.d_expr =
-              PARSER_STATE->mkLambdaWrapper(p1.d_kind, p.d_expr.getType());
+              PARSER_STATE->mkLambdaWrapper(p1.d_kind, p.d_expr.getSort());
         }
         else if (p.d_expr.isNull() && p1.d_expr.isNull())
         {
@@ -1048,10 +1047,10 @@ thfLogicFormula[CVC4::ParseOp& p]
         }
         args.push_back(p.d_expr);
         args.push_back(p1.d_expr);
-        p.d_expr = MK_EXPR(kind::EQUAL, args);
+        p.d_expr = MK_TERM(api::EQUAL, args);
         if (!equal)
         {
-          p.d_expr = MK_EXPR(kind::NOT, p.d_expr);
+          p.d_expr = MK_TERM(api::NOT, p.d_expr);
         }
       }
     | // Non-associative: <=> <~> ~& ~|
@@ -1065,24 +1064,24 @@ thfLogicFormula[CVC4::ParseOp& p]
         switch (na)
         {
           case tptp::NA_IFF:
-            p.d_expr = MK_EXPR(kind::EQUAL, p.d_expr, p1.d_expr);
+            p.d_expr = MK_TERM(api::EQUAL, p.d_expr, p1.d_expr);
             break;
           case tptp::NA_REVIFF:
-            p.d_expr = MK_EXPR(kind::XOR, p.d_expr, p1.d_expr);
+            p.d_expr = MK_TERM(api::XOR, p.d_expr, p1.d_expr);
             break;
           case tptp::NA_IMPLIES:
-            p.d_expr = MK_EXPR(kind::IMPLIES, p.d_expr, p1.d_expr);
+            p.d_expr = MK_TERM(api::IMPLIES, p.d_expr, p1.d_expr);
             break;
           case tptp::NA_REVIMPLIES:
-            p.d_expr = MK_EXPR(kind::IMPLIES, p1.d_expr, p.d_expr);
+            p.d_expr = MK_TERM(api::IMPLIES, p1.d_expr, p.d_expr);
             break;
           case tptp::NA_REVOR:
             p.d_expr =
-                MK_EXPR(kind::NOT, MK_EXPR(kind::OR, p.d_expr, p1.d_expr));
+                MK_TERM(api::NOT, MK_TERM(api::OR, p.d_expr, p1.d_expr));
             break;
           case tptp::NA_REVAND:
             p.d_expr =
-                MK_EXPR(kind::NOT, MK_EXPR(kind::AND, p.d_expr, p1.d_expr));
+                MK_TERM(api::NOT, MK_TERM(api::AND, p.d_expr, p1.d_expr));
             break;
         }
       }
@@ -1107,7 +1106,7 @@ thfLogicFormula[CVC4::ParseOp& p]
           }
         )+
         {
-          p.d_expr = MK_EXPR_ASSOCIATIVE(kind::AND, args);
+          p.d_expr = MK_TERM(api::AND, args);
         }
       )
     | // N-ary or |
@@ -1131,7 +1130,7 @@ thfLogicFormula[CVC4::ParseOp& p]
           }
         )+
         {
-          p.d_expr = MK_EXPR_ASSOCIATIVE(kind::OR, args);
+          p.d_expr = MK_TERM(api::OR, args);
         }
       )
     | // N-ary @ |
@@ -1191,19 +1190,19 @@ thfLogicFormula[CVC4::ParseOp& p]
             // lambda must have type ti
             args.push_back(PARSER_STATE->mkLambdaWrapper(
                 p_args[i].d_kind,
-                (static_cast<FunctionType>(p.d_expr.getType()))
-                    .getArgTypes()[i - 1]));
+                p.d_expr.getSort()
+                    .getFunctionDomainSorts()[i - 1]));
           }
           for (unsigned i = 0, size = args.size(); i < size; ++i)
           {
-            p.d_expr = MK_EXPR(kind::HO_APPLY, p.d_expr, args[i]);
+            p.d_expr = MK_TERM(api::HO_APPLY, p.d_expr, args[i]);
           }
         }
       }
     )?
   ;
 
-thfTupleForm[std::vector<CVC4::Expr>& args]
+thfTupleForm[std::vector<CVC4::api::Term>& args]
 @declarations {
   ParseOp p;
 }
@@ -1228,9 +1227,9 @@ thfTupleForm[std::vector<CVC4::Expr>& args]
 
 thfUnitaryFormula[CVC4::ParseOp& p]
 @declarations {
-  Kind kind;
-  std::vector< Expr > bv;
-  Expr expr;
+  api::Kind kind;
+  std::vector< CVC4::api::Term > bv;
+  CVC4::api::Term expr;
   bool equal;
   ParseOp p1;
 }
@@ -1241,7 +1240,7 @@ thfUnitaryFormula[CVC4::ParseOp& p]
     RPAREN_TOK
   | NOT_TOK
     {
-      p.d_kind = kind::NOT;
+      p.d_kind = api::NOT;
     }
     (
      thfUnitaryFormula[p1]
@@ -1250,7 +1249,7 @@ thfUnitaryFormula[CVC4::ParseOp& p]
        {
          PARSER_STATE->parseError("NOT must be applied to a formula");
        }
-       std::vector<Expr> args{p1.d_expr};
+       std::vector<api::Term> args{p1.d_expr};
        p.d_expr = PARSER_STATE->applyParseOp(p, args);
      }
     )?
@@ -1282,9 +1281,9 @@ thfUnitaryFormula[CVC4::ParseOp& p]
       // see documentation of mkFlatFunctionType for how it's done
       //
       // flatten body via flattening its type
-      std::vector<Type> sorts;
-      std::vector<Expr> flattenVars;
-      PARSER_STATE->mkFlatFunctionType(sorts, expr.getType(), flattenVars);
+      std::vector<api::Sort> sorts;
+      std::vector<api::Term> flattenVars;
+      PARSER_STATE->mkFlatFunctionType(sorts, expr.getSort(), flattenVars);
       if (!flattenVars.empty())
       {
         // apply body of lambda to flatten vars
@@ -1292,18 +1291,18 @@ thfUnitaryFormula[CVC4::ParseOp& p]
         // add variables to BOUND_VAR_LIST
         bv.insert(bv.end(), flattenVars.begin(), flattenVars.end());
       }
-      p.d_expr = MK_EXPR(p.d_kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+      p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
     }
   ;
 
 /*******/
 /* TFF */
-tffFormula[CVC4::Expr& expr] : tffLogicFormula[expr];
+tffFormula[CVC4::api::Term& expr] : tffLogicFormula[expr];
 
 tffTypedAtom[CVC4::Command*& cmd]
 @declarations {
-  CVC4::Expr expr;
-  CVC4::Type type;
+  CVC4::api::Term expr;
+  CVC4::api::Sort type;
   std::string name;
 }
   : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK
@@ -1317,8 +1316,8 @@ tffTypedAtom[CVC4::Command*& cmd]
           PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort");
         } else {
           // as yet, it's undeclared
-          Type atype = PARSER_STATE->mkSort(name);
-          cmd = new DeclareTypeCommand(name, 0, atype);
+          api::Sort atype = PARSER_STATE->mkSort(name);
+          cmd = new DeclareTypeCommand(name, 0, atype.getType());
         }
       }
     | parseType[type]
@@ -1327,7 +1326,7 @@ tffTypedAtom[CVC4::Command*& cmd]
           PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a sort");
           cmd = new EmptyCommand("compatible redeclaration of sort " + name);
         } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
-          if(type == PARSER_STATE->getVariable(name).getType()) {
+          if(type == PARSER_STATE->getVariable(name).getSort()) {
             // duplicate declaration is fine, they're compatible
             cmd = new EmptyCommand("compatible redeclaration of constant " + name);
           } else {
@@ -1336,40 +1335,41 @@ tffTypedAtom[CVC4::Command*& cmd]
           }
         } else {
           // as yet, it's undeclared
-          CVC4::Expr aexpr = PARSER_STATE->mkVar(name, type);
-          cmd = new DeclareFunctionCommand(name, aexpr, type);
+          CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type);
+          cmd =
+              new DeclareFunctionCommand(name, aexpr.getExpr(), type.getType());
         }
       }
     )
   ;
 
-tffLogicFormula[CVC4::Expr& expr]
+tffLogicFormula[CVC4::api::Term& expr]
 @declarations {
   tptp::NonAssoc na;
-  std::vector< Expr > args;
-  Expr expr2;
+  std::vector< CVC4::api::Term > args;
+  CVC4::api::Term expr2;
 }
   : tffUnitaryFormula[expr]
     ( // Non Assoc <=> <~> ~& ~|
       ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
         { switch(na) {
            case tptp::NA_IFF:
-             expr = MK_EXPR(kind::EQUAL,expr,expr2);
+             expr = MK_TERM(api::EQUAL,expr,expr2);
              break;
            case tptp::NA_REVIFF:
-             expr = MK_EXPR(kind::XOR,expr,expr2);
+             expr = MK_TERM(api::XOR,expr,expr2);
              break;
            case tptp::NA_IMPLIES:
-             expr = MK_EXPR(kind::IMPLIES,expr,expr2);
+             expr = MK_TERM(api::IMPLIES,expr,expr2);
              break;
            case tptp::NA_REVIMPLIES:
-             expr = MK_EXPR(kind::IMPLIES,expr2,expr);
+             expr = MK_TERM(api::IMPLIES,expr2,expr);
              break;
            case tptp::NA_REVOR:
-             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2));
+             expr = MK_TERM(api::NOT,MK_TERM(api::OR,expr,expr2));
              break;
            case tptp::NA_REVAND:
-             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2));
+             expr = MK_TERM(api::NOT,MK_TERM(api::AND,expr,expr2));
              break;
           }
         }
@@ -1377,35 +1377,35 @@ tffLogicFormula[CVC4::Expr& expr]
     | // And &
       ( { args.push_back(expr); }
         ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::AND,args); }
+        { expr = MK_TERM(api::AND,args); }
       )
     | // Or |
       ( { args.push_back(expr); }
         ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::OR,args); }
+        { expr = MK_TERM(api::OR,args); }
       )
     )?
   ;
 
-tffUnitaryFormula[CVC4::Expr& expr]
+tffUnitaryFormula[CVC4::api::Term& expr]
 @declarations {
-  Kind kind;
-  std::vector< Expr > bv;
-  Expr lhs, rhs;
+  api::Kind kind;
+  std::vector< CVC4::api::Term > bv;
+  CVC4::api::Term lhs, rhs;
 }
   : atomicFormula[expr]
   | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK
-  | NOT_TOK tffUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
+  | NOT_TOK tffUnitaryFormula[expr] { expr = MK_TERM(api::NOT,expr); }
   | // Quantified
     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
     ( tffbindvariable[expr] { bv.push_back(expr); }
       ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK tffUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
     }
   | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
-    { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, lhs, rhs); }
+    { expr = MK_TERM(api::ITE, expr, lhs, rhs); }
   | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
     tffLetTermDefn[lhs, rhs] COMMA_TOK
     tffFormula[expr]
@@ -1422,79 +1422,88 @@ tffUnitaryFormula[CVC4::Expr& expr]
     RPAREN_TOK
   ;
 
-tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+tffLetTermDefn[CVC4::api::Term& lhs, CVC4::api::Term& rhs]
 @declarations {
-  std::vector<CVC4::Expr> bvlist;
+  std::vector<CVC4::api::Term> bvlist;
 }
   : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
     tffLetTermBinding[bvlist, lhs, rhs]
   ;
 
-tffLetTermBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
+                  CVC4::api::Term& lhs,
+                  CVC4::api::Term& rhs]
   : term[lhs] EQUAL_TOK term[rhs]
-    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
-      rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
-      lhs = lhs.getOperator();
-    }
+  {
+    PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
+    std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    lhs = api::Term(lhs.getExpr().getOperator());
+  }
   | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;
 
-tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+tffLetFormulaDefn[CVC4::api::Term& lhs, CVC4::api::Term& rhs]
 @declarations {
-  std::vector<CVC4::Expr> bvlist;
+  std::vector<CVC4::api::Term> bvlist;
 }
   : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
     tffLetFormulaBinding[bvlist, lhs, rhs]
   ;
 
-tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
+                     CVC4::api::Term& lhs,
+                     CVC4::api::Term& rhs]
+
   : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs]
-    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
-      rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
-      lhs = lhs.getOperator();
-    }
+  {
+    PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
+    std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    lhs = api::Term(lhs.getExpr().getOperator());
+  }
   | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;
 
-thfBindVariable[CVC4::Expr& expr]
+thfBindVariable[CVC4::api::Term& expr]
 @declarations {
   std::string name;
-  CVC4::Type type = PARSER_STATE->d_unsorted;
+  CVC4::api::Sort type = PARSER_STATE->d_unsorted;
 }
   : UPPER_WORD
     { name = AntlrInput::tokenText($UPPER_WORD); }
     ( COLON_TOK parseThfType[type] )?
     {
-      expr = PARSER_STATE->mkBoundVar(name, type);
+      expr = PARSER_STATE->bindBoundVar(name, type);
     }
   ;
 
 
-tffbindvariable[CVC4::Expr& expr]
+tffbindvariable[CVC4::api::Term& expr]
 @declarations {
-  CVC4::Type type = PARSER_STATE->d_unsorted;
+  CVC4::api::Sort type = PARSER_STATE->d_unsorted;
 }
   : UPPER_WORD
     ( COLON_TOK parseType[type] )?
     { std::string name = AntlrInput::tokenText($UPPER_WORD);
-      expr = PARSER_STATE->mkBoundVar(name, type);
+      expr = PARSER_STATE->bindBoundVar(name, type);
     }
   ;
 
 // bvlist is accumulative; it can already contain elements
 // on the way in, which are left undisturbed
-tffVariableList[std::vector<CVC4::Expr>& bvlist]
+tffVariableList[std::vector<CVC4::api::Term>& bvlist]
 @declarations {
-  CVC4::Expr e;
+  CVC4::api::Term e;
 }
   : tffbindvariable[e] { bvlist.push_back(e); }
     ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )*
   ;
 
-parseThfType[CVC4::Type& type]
+parseThfType[CVC4::api::Sort& type]
 // assumes only mapping types (arrows), no tuple type
 @declarations {
-  std::vector<CVC4::Type> sorts;
+  std::vector<CVC4::api::Sort> sorts;
 }
   : thfType[type] { sorts.push_back(type); }
     (
@@ -1507,24 +1516,24 @@ parseThfType[CVC4::Type& type]
       }
       else
       {
-        Type range = sorts.back();
+        api::Sort range = sorts.back();
         sorts.pop_back();
         type = PARSER_STATE->mkFlatFunctionType(sorts, range);
       }
     }
   ;
 
-thfType[CVC4::Type& type]
+thfType[CVC4::api::Sort& type]
 // assumes only mapping types (arrows), no tuple type
   : simpleType[type]
     | LPAREN_TOK parseThfType[type] RPAREN_TOK
     | LBRACK_TOK { UNSUPPORTED("Tuple types"); } parseThfType[type] RBRACK_TOK
   ;
 
-parseType[CVC4::Type & type]
+parseType[CVC4::api::Sort & type]
 @declarations
 {
-  std::vector<CVC4::Type> v;
+  std::vector<CVC4::api::Sort> v;
 }
   : simpleType[type]
   | ( simpleType[type] { v.push_back(type); }
@@ -1533,23 +1542,22 @@ parseType[CVC4::Type & type]
       RPAREN_TOK
     )
     ARROW_TOK simpleType[type]
-    { v.push_back(type);
-      type = EXPR_MANAGER->mkFunctionType(v);
+    { type = SOLVER->mkFunctionSort(v,type);
     }
   ;
 
 // non-function types
-simpleType[CVC4::Type& type]
+simpleType[CVC4::api::Sort& type]
 @declarations {
   std::string name;
 }
   : DEFINED_SYMBOL
     { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL);
       if(s == "\$i") type = PARSER_STATE->d_unsorted;
-      else if(s == "\$o") type = EXPR_MANAGER->booleanType();
-      else if(s == "\$int") type = EXPR_MANAGER->integerType();
-      else if(s == "\$rat") type = EXPR_MANAGER->realType();
-      else if(s == "\$real") type = EXPR_MANAGER->realType();
+      else if(s == "\$o") type = SOLVER->getBooleanSort();
+      else if(s == "\$int") type = SOLVER->getIntegerSort();
+      else if(s == "\$rat") type = SOLVER->getRealSort();
+      else if(s == "\$real") type = SOLVER->getRealSort();
       else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here");
       else PARSER_STATE->parseError("unknown defined type `" + s + "'");
     }
@@ -1736,12 +1744,13 @@ NUMBER
   bool posE = true;
 }
   : ( SIGN[pos]? num=DECIMAL
-      { Integer i(AntlrInput::tokenText($num));
-        Rational r = pos ? i : -i;
-        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+      { std::stringstream ss;
+        ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num);
+        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
       }
     | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
-      { std::string snum = AntlrInput::tokenText($num);
+      {
+        std::string snum = AntlrInput::tokenText($num);
         std::string sden = AntlrInput::tokenText($den);
         /* compute the numerator */
         Integer inum(snum + sden);
@@ -1758,12 +1767,14 @@ NUMBER
         else if(exp == dec) r = Rational(inum);
         else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec));
         else r = Rational(inum, Integer(10).pow(dec - exp));
-        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+        std::stringstream ss;
+        ss << r;
+        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
       }
     | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
-      { Integer inum(AntlrInput::tokenText($num));
-        Integer iden(AntlrInput::tokenText($den));
-        PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden));
+      { std::stringstream ss;
+        ss << AntlrInput::tokenText($num) << "/" << AntlrInput::tokenText($den);
+        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
       }
     )
     { if(PARSER_STATE->cnf() || PARSER_STATE->fof()) {