Refactor Commands to use the Public API. (#5105)

This is work towards eliminating the Expr layer. This PR does the following:

Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.

5 files changed, 78 insertions, 111 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d1aaa3d15..5f959c660 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -704,13 +704,12 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   bool formCommaFlag = true;
 }
     /* our bread & butter */
-  : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f.getExpr())); }
+  : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); }
 
-  | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f.getExpr())); }
+  | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f)); }
   | CHECKSAT_TOK formula[f]?
     {
-      cmd->reset(f.isNull() ? new CheckSatCommand()
-                            : new CheckSatCommand(f.getExpr()));
+      cmd->reset(f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f));
     }
     /* options */
   | OPTION_TOK
@@ -764,7 +763,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     END_TOK
     { PARSER_STATE->popScope();
       cmd->reset(new DatatypeDeclarationCommand(
-          api::sortVectorToTypes(PARSER_STATE->bindMutualDatatypeTypes(dts))));
+          PARSER_STATE->bindMutualDatatypeTypes(dts)));
     }
 
   | CONTEXT_TOK
@@ -789,7 +788,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     { UNSUPPORTED("GET_OP command"); }
 
   | GET_VALUE_TOK formula[f]
-    { cmd->reset(new GetValueCommand(f.getExpr())); }
+    { cmd->reset(new GetValueCommand(f)); }
 
   | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON
     type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET
@@ -823,7 +822,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
             )
 
   | TRANSFORM_TOK formula[f]
-    { cmd->reset(new SimplifyCommand(f.getExpr())); }
+    { cmd->reset(new SimplifyCommand(f)); }
 
   | PRINT_TOK formula[f]
     { UNSUPPORTED("PRINT command"); }
@@ -936,8 +935,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
           PARSER_STATE->parseError("Type mismatch in definition");
         }
       }
-      cmd->reset(
-          new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true));
+      cmd->reset(new DefineFunctionRecCommand(funcs, formals, formulas, true));
     }
   | toplevelDeclaration[cmd]
   ;
@@ -1059,7 +1057,7 @@ declareTypes[std::unique_ptr<CVC4::Command>* cmd,
         // behavior here.
         PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
         api::Sort sort = PARSER_STATE->mkSort(*i);
-        Command* decl = new DeclareTypeCommand(*i, 0, sort.getType());
+        Command* decl = new DeclareSortCommand(*i, 0, sort);
         seq->addCommand(decl);
       }
       cmd->reset(seq.release());
@@ -1125,8 +1123,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
             if(topLevel) {
               api::Term func =
                   PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
-              Command* decl =
-                  new DeclareFunctionCommand(*i, func.getExpr(), t.getType());
+              Command* decl = new DeclareFunctionCommand(*i, func, t);
               seq->addCommand(decl);
             } else {
               PARSER_STATE->bindBoundVar(*i, t);
@@ -1156,8 +1153,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
               api::Sort(SOLVER, t.getType()),
               ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
           PARSER_STATE->defineVar(*i, f);
-          Command* decl =
-              new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true);
+          Command* decl = new DefineFunctionCommand(*i, func, f, true);
           seq->addCommand(decl);
         }
       }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 65f72eb28..232723fc0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -263,10 +263,10 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       unsigned arity = AntlrInput::tokenToUnsigned(n);
       if(arity == 0) {
         api::Sort type = PARSER_STATE->mkSort(name);
-        cmd->reset(new DeclareTypeCommand(name, 0, type.getType()));
+        cmd->reset(new DeclareSortCommand(name, 0, type));
       } else {
         api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
-        cmd->reset(new DeclareTypeCommand(name, arity, type.getType()));
+        cmd->reset(new DeclareSortCommand(name, arity, type));
       }
     }
   | /* sort definition */
@@ -287,8 +287,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       // Do NOT call mkSort, since that creates a new sort!
       // This name is not its own distinct sort, it's an alias.
       PARSER_STATE->defineParameterizedType(name, sorts, t);
-      cmd->reset(new DefineTypeCommand(
-          name, api::sortVectorToTypes(sorts), t.getType()));
+      cmd->reset(new DefineSortCommand(name, sorts, t));
     }
   | /* function declaration */
     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -314,8 +313,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       {
         api::Term func =
             PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
-        cmd->reset(
-            new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
+        cmd->reset(new DeclareFunctionCommand(name, func, t));
       }
     }
   | /* function definition */
@@ -334,8 +332,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
             ++i) {
           sorts.push_back((*i).second);
         }
-        t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
       }
+
+      t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
       PARSER_STATE->pushScope(true);
       terms = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
@@ -354,19 +353,15 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       // we allow overloading for function definitions
       api::Term func = PARSER_STATE->bindVar(name, t,
                                       ExprManager::VAR_FLAG_DEFINED, true);
-      cmd->reset(
-          new DefineFunctionCommand(name,
-                                    func.getExpr(),
-                                    api::termVectorToExprs(terms),
-                                    expr.getExpr(),
-                                    PARSER_STATE->getGlobalDeclarations()));
+      cmd->reset(new DefineFunctionCommand(
+          name, func, terms, expr, PARSER_STATE->getGlobalDeclarations()));
     }
   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
-      { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); }
+      { cmd->reset(new GetValueCommand(terms)); }
     | ~LPAREN_TOK
       { PARSER_STATE->parseError("The get-value command expects a list of "
                                  "terms.  Perhaps you forgot a pair of "
@@ -381,13 +376,13 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     { PARSER_STATE->clearLastNamedTerm(); }
     term[expr, expr2]
     { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
-      cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore));
+      cmd->reset(new AssertCommand(expr, inUnsatCore));
       if(inUnsatCore) {
         // set the expression name, if there was a named term
         std::pair<api::Term, std::string> namedTerm =
             PARSER_STATE->lastNamedTerm();
-        Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(),
-                                                     namedTerm.second);
+        Command* csen =
+            new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
@@ -407,12 +402,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       }
     | { expr = api::Term(); }
     )
-    { cmd->reset(new CheckSatCommand(expr.getExpr())); }
+    { cmd->reset(new CheckSatCommand(expr)); }
   | /* check-sat-assuming */
     CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
       {
-        cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms)));
+        cmd->reset(new CheckSatAssumingCommand(terms));
       }
     | ~LPAREN_TOK
       { PARSER_STATE->parseError("The check-sat-assuming command expects a "
@@ -558,7 +553,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
     sortSymbol[t,CHECK_DECLARED]
     {
       api::Term var = PARSER_STATE->bindBoundVar(name, t);
-      cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
+      cmd.reset(new DeclareSygusVarCommand(name, var, t));
     }
   | /* synth-fun */
     ( SYNTH_FUN_TOK { isInv = false; }
@@ -590,7 +585,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
     }
     term[expr, expr2]
     { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
-      cmd.reset(new SygusConstraintCommand(expr.getExpr()));
+      cmd.reset(new SygusConstraintCommand(expr));
     }
   | /* inv-constraint */
     INV_CONSTRAINT_TOK
@@ -788,7 +783,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
     { // allow overloading here
       api::Term c =
           PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
-      cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); }
+      cmd->reset(new DeclareFunctionCommand(name, c, t)); }
 
     /* get model */
   | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -831,7 +826,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
         expr = PARSER_STATE->mkHoApply( expr, flattenVars );
       }
       cmd->reset(new DefineFunctionRecCommand(
-          SOLVER, func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
+          func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
     }
   | DEFINE_FUNS_REC_TOK
     { PARSER_STATE->checkThatLogicIsSet();}
@@ -894,12 +889,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
             "Number of functions defined does not match number listed in "
             "define-funs-rec"));
       }
-      cmd->reset(
-          new DefineFunctionRecCommand(SOLVER,
-                                       funcs,
-                                       formals,
-                                       func_defs,
-                                       PARSER_STATE->getGlobalDeclarations()));
+      cmd->reset(new DefineFunctionRecCommand(
+          funcs, formals, func_defs, PARSER_STATE->getGlobalDeclarations()));
     }
   ;
 
@@ -935,7 +926,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
       { PARSER_STATE->checkUserSymbol(name);
         api::Sort type = PARSER_STATE->mkSort(name);
-        seq->addCommand(new DeclareTypeCommand(name, 0, type.getType()));
+        seq->addCommand(new DeclareSortCommand(name, 0, type));
       }
     )+
     RPAREN_TOK
@@ -960,8 +951,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         // allow overloading
         api::Term func =
             PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
-        seq->addCommand(
-            new DeclareFunctionCommand(name, func.getExpr(), tt.getType()));
+        seq->addCommand(new DeclareFunctionCommand(name, func, tt));
         sorts.clear();
       }
     )+
@@ -981,8 +971,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         // allow overloading
         api::Term func =
             PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
-        seq->addCommand(
-            new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
+        seq->addCommand(new DeclareFunctionCommand(name, func, t));
         sorts.clear();
       }
     )+
@@ -997,11 +986,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       {
         api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
                                         ExprManager::VAR_FLAG_DEFINED);
-        cmd->reset(
-            new DefineFunctionCommand(name,
-                                      func.getExpr(),
-                                      e.getExpr(),
-                                      PARSER_STATE->getGlobalDeclarations()));
+        cmd->reset(new DefineFunctionCommand(
+            name, func, e, PARSER_STATE->getGlobalDeclarations()));
       }
     | // (define (f (v U) ...) t)
       LPAREN_TOK
@@ -1031,12 +1017,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         }
         api::Term func = PARSER_STATE->bindVar(name, tt,
                                         ExprManager::VAR_FLAG_DEFINED);
-        cmd->reset(
-            new DefineFunctionCommand(name,
-                                      func.getExpr(),
-                                      api::termVectorToExprs(terms),
-                                      e.getExpr(),
-                                      PARSER_STATE->getGlobalDeclarations()));
+        cmd->reset(new DefineFunctionCommand(
+            name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
       }
     )
   | // (define-const x U t)
@@ -1057,23 +1039,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       // permitted)
       api::Term func = PARSER_STATE->bindVar(name, t,
                                       ExprManager::VAR_FLAG_DEFINED);
-      cmd->reset(
-          new DefineFunctionCommand(name,
-                                    func.getExpr(),
-                                    api::termVectorToExprs(terms),
-                                    e.getExpr(),
-                                    PARSER_STATE->getGlobalDeclarations()));
+      cmd->reset(new DefineFunctionCommand(
+          name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
     }
 
   | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[e,e2]
-    { cmd->reset(new SimplifyCommand(e.getExpr())); }
+    { cmd->reset(new SimplifyCommand(e)); }
   | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[e,e2]
-    { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); }
+    { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
   | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[e,e2]
-    { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); }
+    { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
   | GET_ABDUCT_TOK {
       PARSER_STATE->checkThatLogicIsSet();
     }
@@ -1083,7 +1061,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetAbductCommand(SOLVER, name, e, g));
+      cmd->reset(new GetAbductCommand(name, e, g));
     }
   | GET_INTERPOL_TOK {
       PARSER_STATE->checkThatLogicIsSet();
@@ -1094,7 +1072,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetInterpolCommand(SOLVER, name, e, g));
+      cmd->reset(new GetInterpolCommand(name, e, g));
     }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
@@ -1107,7 +1085,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 
   | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,e] RPAREN_TOK
-      { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); }
+      { cmd->reset(new BlockModelValuesCommand(terms)); }
     | ~LPAREN_TOK
       { PARSER_STATE->parseError("The block-model-value command expects a list "
                                  "of terms.  Perhaps you forgot a pair of "
@@ -1138,8 +1116,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
     cmd->reset(new DatatypeDeclarationCommand(
-      api::sortVectorToTypes(
-        PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
+        PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
   }
   ;
 
@@ -1271,8 +1248,7 @@ datatypesDef[bool isCo,
     }
     PARSER_STATE->popScope();
     cmd->reset(new DatatypeDeclarationCommand(
-      api::sortVectorToTypes(
-        PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
+        PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
   }
   ;
 
@@ -1847,8 +1823,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
       api::Sort boolType = SOLVER->getBooleanSort();
       api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
       retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
-      Command* c = new SetUserAttributeCommand(
-          attr_name, avar.getExpr(), api::termVectorToExprs(values));
+      Command* c = new SetUserAttributeCommand(attr_name, avar, values);
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
@@ -1858,7 +1833,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
       api::Term avar = SOLVER->mkConst(boolType, sexpr.toString());
       attr = std::string(":qid");
       retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
-      Command* c = new SetUserAttributeCommand("qid", avar.getExpr());
+      Command* c = new SetUserAttributeCommand("qid", avar);
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
@@ -1868,8 +1843,12 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
       api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
       std::string name = sexpr.getValue();
       // bind name to expr with define-fun
-      Command* c = new DefineNamedFunctionCommand(
-          name, func.getExpr(), std::vector<Expr>(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations());
+      Command* c =
+          new DefineNamedFunctionCommand(name,
+                                         func,
+                                         std::vector<api::Term>(),
+                                         expr,
+                                         PARSER_STATE->getGlobalDeclarations());
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 387117335..e7bb8795c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -525,8 +525,8 @@ std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
 {
   Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
   d_smt2->popScope();
-  return std::unique_ptr<Command>(new SynthFunCommand(
-      d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
+  return std::unique_ptr<Command>(
+      new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
 }
 
 std::unique_ptr<Command> Smt2::invConstraint(
@@ -556,8 +556,7 @@ std::unique_ptr<Command> Smt2::invConstraint(
     terms.push_back(getVariable(name));
   }
 
-  return std::unique_ptr<Command>(
-      new SygusInvConstraintCommand(api::termVectorToExprs(terms)));
+  return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
 }
 
 Command* Smt2::setLogic(std::string name, bool fromCommand)
@@ -776,8 +775,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
                               const std::vector<api::Term>& ntSymbols)
 {
-  d_allocGrammars.emplace_back(new api::Grammar(
-      std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols))));
+  d_allocGrammars.emplace_back(
+      new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols)));
   return d_allocGrammars.back().get();
 }
 
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 050a23320..b99376685 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -161,10 +161,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      CVC4::api::Term 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.getExpr(), name);
+        Command* csen = new SetExpressionNameCommand(aexpr, name);
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
@@ -178,7 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       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.getExpr(), name);
+        Command* csen = new SetExpressionNameCommand(aexpr, name);
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
@@ -194,7 +194,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
         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.getExpr(), name);
+          Command* csen = new SetExpressionNameCommand(aexpr, name);
           csen->setMuted(true);
           PARSER_STATE->preemptCommand(csen);
         }
@@ -219,7 +219,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
         if (!aexpr.isNull())
         {
           // set the expression name (e.g. used with unsat core printing)
-          Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
+          Command* csen = new SetExpressionNameCommand(aexpr, name);
           csen->setMuted(true);
           PARSER_STATE->preemptCommand(csen);
         }
@@ -255,7 +255,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants();
       if( !aexpr.isNull() )
       {
-        seq->addCommand(new AssertCommand(aexpr.getExpr(), false));
+        seq->addCommand(new AssertCommand(aexpr, false));
       }
 
       std::string filename = PARSER_STATE->getInput()->getInputStreamName();
@@ -268,7 +268,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       }
       seq->addCommand(new SetInfoCommand("filename", SExpr(filename)));
       if(PARSER_STATE->hasConjecture()) {
-        seq->addCommand(new QueryCommand(SOLVER->mkFalse().getExpr()));
+        seq->addCommand(new QueryCommand(SOLVER->mkFalse()));
       } else {
         seq->addCommand(new CheckSatCommand());
       }
@@ -967,7 +967,7 @@ thfAtomTyping[CVC4::Command*& cmd]
         {
           // as yet, it's undeclared
           api::Sort atype = PARSER_STATE->mkSort(name);
-          cmd = new DeclareTypeCommand(name, 0, atype.getType());
+          cmd = new DeclareSortCommand(name, 0, atype);
         }
       }
     | parseThfType[type]
@@ -1007,8 +1007,7 @@ thfAtomTyping[CVC4::Command*& cmd]
           {
             freshExpr = PARSER_STATE->bindVar(name, type);
           }
-          cmd = new DeclareFunctionCommand(
-              name, freshExpr.getExpr(), type.getType());
+          cmd = new DeclareFunctionCommand(name, freshExpr, type);
         }
       }
     )
@@ -1320,7 +1319,7 @@ tffTypedAtom[CVC4::Command*& cmd]
         } else {
           // as yet, it's undeclared
           api::Sort atype = PARSER_STATE->mkSort(name);
-          cmd = new DeclareTypeCommand(name, 0, atype.getType());
+          cmd = new DeclareSortCommand(name, 0, atype);
         }
       }
     | parseType[type]
@@ -1339,8 +1338,7 @@ tffTypedAtom[CVC4::Command*& cmd]
         } else {
           // as yet, it's undeclared
           CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type);
-          cmd =
-              new DeclareFunctionCommand(name, aexpr.getExpr(), type.getType());
+          cmd = new DeclareFunctionCommand(name, aexpr, type);
         }
       }
     )
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 8f75cf8d3..066970fe3 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -76,8 +76,7 @@ void Tptp::addTheory(Theory theory) {
     {
       std::string d_unsorted_name = "$$unsorted";
       d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
-      preemptCommand(
-          new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType()));
+      preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted));
     }
     // propositionnal
     defineType("Bool", d_solver->getBooleanSort());
@@ -243,8 +242,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p)
     api::Sort t =
         p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
     expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
-    preemptCommand(
-        new DeclareFunctionCommand(p.d_name, expr.getExpr(), t.getType()));
+    preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
   }
   return expr;
 }
@@ -288,8 +286,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
           p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
       t = d_solver->mkFunctionSort(sorts, t);
       v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
-      preemptCommand(
-          new DeclareFunctionCommand(p.d_name, v.getExpr(), t.getType()));
+      preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
     }
     // args might be rationals, in which case we need to create
     // distinct constants of the "unsorted" sort to represent them
@@ -394,13 +391,11 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr)
     // Conversion from rational to unsorted
     t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
     d_rtu_op = d_solver->mkConst(t, "$$rtu");
-    preemptCommand(
-        new DeclareFunctionCommand("$$rtu", d_rtu_op.getExpr(), t.getType()));
+    preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
     // Conversion from unsorted to rational
     t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
     d_utr_op = d_solver->mkConst(t, "$$utr");
-    preemptCommand(
-        new DeclareFunctionCommand("$$utr", d_utr_op.getExpr(), t.getType()));
+    preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
   }
   // Add the inverse in order to show that over the elements that
   // appear in the problem there is a bijection between unsorted and
@@ -410,7 +405,7 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr)
     d_r_converted.insert(expr);
     api::Term eq = d_solver->mkTerm(
         api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret));
-    preemptCommand(new AssertCommand(eq.getExpr()));
+    preemptCommand(new AssertCommand(eq));
   }
   return api::Term(ret);
 }
@@ -506,7 +501,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr,
   if( expr.isNull() ){
     return new EmptyCommand("Untreated role for expression");
   }else{
-    return new AssertCommand(expr.getExpr(), inUnsatCore);
+    return new AssertCommand(expr, inUnsatCore);
   }
 }