Sketch of refactoring the Commands to use new APInewApiForCommands

This commit is a sketch of how we can transform `Command`s to use the
new API and transform the parser bit-by-bit. The overall idea is that
`Command::invoke()` now takes an `Solver*` as an argument instead of an
`SmtEngine*`. The default implementation `Command::invoke()` just calls
the old implementation. As an example, the PR transforms the
`GetValueCommand`.

14 files changed, 172 insertions, 109 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be7c5c665..21644ed55 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -26,8 +26,10 @@
 #include "expr/type.h"
 #include "options/main_options.h"
 #include "options/options.h"
+#include "options/smt_options.h"
 #include "smt/model.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "util/random.h"
 #include "util/result.h"
 #include "util/utility.h"
@@ -55,6 +57,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {DISTINCT, CVC4::Kind::DISTINCT},
     {VARIABLE, CVC4::Kind::VARIABLE},
     {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+    {SEXPR, CVC4::Kind::SEXPR},
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
     {CHAIN, CVC4::Kind::CHAIN},
@@ -303,6 +306,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::DISTINCT, DISTINCT},
         {CVC4::Kind::VARIABLE, VARIABLE},
         {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+        {CVC4::Kind::SEXPR, SEXPR},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
         {CVC4::Kind::CHAIN, CHAIN},
@@ -2870,13 +2874,29 @@ Term Solver::getValue(Term term) const
   // CHECK:
   // NodeManager::fromExprManager(d_exprMgr)
   // == NodeManager::fromExprManager(expr.getExprManager())
-  return d_smtEngine->getValue(*term.d_expr);
+
+  smt::SmtScope scope(d_smtEngine.get());
+
+  Expr e = term.getExpr();
+  Term request = Term(
+      options::expandDefinitions() ? d_smtEngine->expandDefinitions(e) : e);
+  Term value = Term(d_smtEngine->getValue(e));
+  if (value.getSort().isInteger() && request.getSort().isReal()
+      && !request.getSort().isInteger())
+  {
+    // Need to wrap in division-by-one so that output printers know this
+    // is an integer-looking constant that really should be output as
+    // a rational.  Necessary for SMT-LIB standards compliance.
+    value = mkTerm(DIVISION, value, mkConst(CONST_RATIONAL, 1));
+  }
+
+  return mkTerm(SEXPR, request, value);
 }
 
 /**
  *  ( get-value ( <term>+ ) )
  */
-std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
+Term Solver::getValue(const std::vector<Term>& terms) const
 {
   // CHECK:
   // for e in exprs:
@@ -2885,10 +2905,9 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   std::vector<Term> res;
   for (const Term& t : terms)
   {
-    /* Can not use emplace_back here since constructor is private. */
-    res.push_back(Term(d_smtEngine->getValue(*t.d_expr)));
+    res.emplace_back(getValue(t));
   }
-  return res;
+  return mkTerm(SEXPR, res);
 }
 
 /**
@@ -2976,5 +2995,19 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
  */
 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
 
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+std::vector<Term> Solver::exprVectorToTerms(const std::vector<Expr>& exprs)
+{
+  std::vector<Term> terms;
+  for (const Expr& expr : exprs)
+  {
+    terms.emplace_back(expr);
+  }
+  return terms;
+}
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index fc07a1cd7..ff7b67149 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2520,16 +2520,20 @@ class CVC4_PUBLIC Solver
    * Get the value of the given term.
    * SMT-LIB: ( get-value ( <term> ) )
    * @param term the term for which the value is queried
-   * @return the value of the given term
+   * @return a pair (t v) where t is \p term (or its expanded definition) and v
+   * is an equivalent value term according to the current model
    */
   Term getValue(Term term) const;
+
   /**
    * Get the values of the given terms.
    * SMT-LIB: ( get-value ( <term>+ ) )
    * @param terms the terms for which the value is queried
-   * @return the values of the given terms
+   * @return a sequnece of pairs ((t1 v1) ... (tn vn)) where each ti
+   * corresponds to one of the \p terms (or its expanded definition) and vi is
+   * is an equivalent value term according to the current model
    */
-  std::vector<Term> getValue(const std::vector<Term>& terms) const;
+  Term getValue(const std::vector<Term>& terms) const;
 
   /**
    * Pop (a) level(s) from the assertion stack.
@@ -2595,6 +2599,10 @@ class CVC4_PUBLIC Solver
   // to the new API. !!!
   SmtEngine* getSmtEngine(void) const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  static std::vector<Term> exprVectorToTerms(const std::vector<Expr>& exprs);
+
  private:
   /* Helper to convert a vector of internal types to sorts. */
   std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index f91f934f9..0162e4697 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -149,9 +149,9 @@ enum CVC4_PUBLIC Kind : int32_t
 #if 0
   /* Skolem variable (internal only) */
   SKOLEM,
+#endif
   /* Symbolic expression (any arity) */
   SEXPR,
-#endif
   /**
    * Lambda expression.
    * Parameters: 2
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 40c31de99..8ce514181 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -118,9 +118,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options.getVerbosity() >= -1) {
-    status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
+    status = smtEngineInvoke(d_solver, cmd, d_options.getOut());
   } else {
-    status = smtEngineInvoke(d_smtEngine, cmd, NULL);
+    status = smtEngineInvoke(d_solver, cmd, NULL);
   }
 
   Result res;
@@ -192,17 +192,18 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   return status;
 }
 
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
+bool smtEngineInvoke(api::Solver* solver, Command* cmd, std::ostream* out)
 {
   if(out == NULL) {
-    cmd->invoke(smt);
+    cmd->invoke(solver);
   } else {
-    cmd->invoke(smt, *out);
+    cmd->invoke(solver, *out);
   }
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =
       std::string("command-verbosity:") + cmd->getCommandName();
-  if(smt->getOption(commandName).getIntegerValue() == 0) {
+  if (solver->getSmtEngine()->getOption(commandName).getIntegerValue() == 0)
+  {
     return true;
   }
   return !cmd->fail();
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index f8c6e6e5a..0152284ca 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -99,7 +99,7 @@ private:
 
 };/* class CommandExecutor */
 
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
+bool smtEngineInvoke(api::Solver* smt, Command* cmd, std::ostream* out);
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index ba75d5ff7..0b80fbd62 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -228,7 +228,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
     std::ostream* winnersOut =  d_options.getVerbosity() >= -1 ?
         (d_threadOptions[d_lastWinner]).getOut() : NULL;
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut);
+    bool ret =
+        smtEngineInvoke(d_solvers[d_lastWinner], cmdExported, winnersOut);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
@@ -297,8 +298,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ?
           d_threadOptions[i].getOut() : NULL;
 
-      fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i],
-                           current_out_or_null);
+      fns[i] = boost::bind(
+          smtEngineInvoke, d_solvers[i], seqs[i], current_out_or_null);
     }
 
     assert(d_channelsIn.size() == d_numThreads
@@ -408,8 +409,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
         cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]));
     std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ?
         d_threadOptions[d_lastWinner].getOut() : NULL;
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported,
-                               winner_out_if_verbose);
+    bool ret = smtEngineInvoke(
+        d_solvers[d_lastWinner], cmdExported, winner_out_if_verbose);
     if(d_lastWinner != 0){
       delete cmdExported;
     }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d9b0f622b..77de8d0c2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -112,6 +112,7 @@ namespace CVC4 {
 #include <unordered_set>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
@@ -403,7 +404,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
-      { cmd->reset(new GetValueCommand(terms)); }
+      { 
+        cmd->reset(new GetValueCommand(api::Solver::exprVectorToTerms(terms))); 
+      }
     | ~LPAREN_TOK
       { PARSER_STATE->parseError("The get-value command expects a list of "
                                  "terms.  Perhaps you forgot a pair of "
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 6b88a109c..e31ab44bc 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -20,6 +20,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"  // for ExprSetDepth etc..
 #include "expr/expr.h" // for ExprSetDepth etc..
 #include "expr/node_manager_attributes.h" // for VarNameAttr
 #include "options/language.h" // for LANG_AST
@@ -340,8 +341,8 @@ static void toStream(std::ostream& out, const SimplifyCommand* c)
 static void toStream(std::ostream& out, const GetValueCommand* c)
 {
   out << "GetValue( << ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  const vector<api::Term>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<api::Term>(out, ", "));
   out << ">> )";
 }
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6fa7eadeb..44d664878 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -24,11 +24,12 @@
 #include <typeinfo>
 #include <vector>
 
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "printer/dagification_visitor.h"
+#include "api/cvc4cpp.h"                   // for ExprSetDepth etc..
+#include "expr/expr.h"                     // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "options/language.h"              // for LANG_AST
 #include "options/smt_options.h"
+#include "printer/dagification_visitor.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 #include "smt_util/node_visitor.h"
@@ -1345,10 +1346,12 @@ static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
 
 static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
 {
-  const vector<Expr>& terms = c->getTerms();
+  const vector<api::Term>& terms = c->getTerms();
   Assert(!terms.empty());
   out << "GET_VALUE ";
-  copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
+  copy(terms.begin(),
+       terms.end() - 1,
+       ostream_iterator<api::Term>(out, ";\nGET_VALUE "));
   out << terms.back() << ";";
 }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b71e9d4c4..fa49d8973 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -21,6 +21,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/node_manager_attributes.h"
 #include "options/language.h"
 #include "options/smt_options.h"
@@ -1754,8 +1755,8 @@ static void toStream(std::ostream& out, const SimplifyCommand* c)
 static void toStream(std::ostream& out, const GetValueCommand* c)
 {
   out << "(get-value ( ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  const vector<api::Term>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<api::Term>(out, " "));
   out << "))";
 }
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 5198ea2d1..cd0383d3e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,6 +38,7 @@
 #include "util/utility.h"
 
 using namespace std;
+using namespace CVC4::api;
 
 namespace CVC4 {
 
@@ -185,6 +186,21 @@ bool Command::interrupted() const
          && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 }
 
+void Command::invoke(Solver* solver) { invoke(solver->getSmtEngine()); }
+
+void Command::invoke(Solver* solver, std::ostream& out)
+{
+  invoke(solver);
+  if (!(isMuted() && ok()))
+  {
+    printResult(out,
+                solver->getSmtEngine()
+                    ->getOption("command-verbosity:" + getCommandName())
+                    .getIntegerValue()
+                    .toUnsignedInt());
+  }
+}
+
 void Command::invoke(SmtEngine* smtEngine, std::ostream& out)
 {
   invoke(smtEngine);
@@ -197,6 +213,13 @@ void Command::invoke(SmtEngine* smtEngine, std::ostream& out)
   }
 }
 
+void Command::invoke(SmtEngine* smtEngine)
+{
+  // A command should either override this method or override
+  // `Command::invoke(Solver*)` to not call this method.
+  Unimplemented();
+}
+
 std::string Command::toString() const
 {
   std::stringstream ss;
@@ -235,7 +258,8 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
 
 EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
 std::string EmptyCommand::getName() const { return d_name; }
-void EmptyCommand::invoke(SmtEngine* smtEngine)
+
+void EmptyCommand::invoke(Solver* solver)
 {
   /* empty commands have no implementation */
   d_commandStatus = CommandSuccess::instance();
@@ -256,18 +280,19 @@ std::string EmptyCommand::getCommandName() const { return "empty"; }
 
 EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 std::string EchoCommand::getOutput() const { return d_output; }
-void EchoCommand::invoke(SmtEngine* smtEngine)
+void EchoCommand::invoke(Solver* solver)
 {
   /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out)
+void EchoCommand::invoke(Solver* solver, std::ostream& out)
 {
   out << d_output << std::endl;
   d_commandStatus = CommandSuccess::instance();
   printResult(out,
-              smtEngine->getOption("command-verbosity:" + getCommandName())
+              solver->getSmtEngine()
+                  ->getOption("command-verbosity:" + getCommandName())
                   .getIntegerValue()
                   .toUnsignedInt());
 }
@@ -1031,11 +1056,11 @@ void CommandSequence::addCommand(Command* cmd)
 }
 
 void CommandSequence::clear() { d_commandSequence.clear(); }
-void CommandSequence::invoke(SmtEngine* smtEngine)
+void CommandSequence::invoke(Solver* solver)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
   {
-    d_commandSequence[d_index]->invoke(smtEngine);
+    d_commandSequence[d_index]->invoke(solver);
     if (!d_commandSequence[d_index]->ok())
     {
       // abort execution
@@ -1049,11 +1074,11 @@ void CommandSequence::invoke(SmtEngine* smtEngine)
   d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out)
+void CommandSequence::invoke(Solver* solver, std::ostream& out)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
   {
-    d_commandSequence[d_index]->invoke(smtEngine, out);
+    d_commandSequence[d_index]->invoke(solver, out);
     if (!d_commandSequence[d_index]->ok())
     {
       // abort execution
@@ -1646,43 +1671,24 @@ std::string ExpandDefinitionsCommand::getCommandName() const
 /* class GetValueCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-GetValueCommand::GetValueCommand(Expr term) : d_terms()
+GetValueCommand::GetValueCommand(Term term) : d_terms()
 {
   d_terms.push_back(term);
 }
 
-GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
+GetValueCommand::GetValueCommand(const std::vector<Term>& terms)
     : d_terms(terms)
 {
   PrettyCheckArgument(
       terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
 }
 
-const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
-void GetValueCommand::invoke(SmtEngine* smtEngine)
+const std::vector<Term>& GetValueCommand::getTerms() const { return d_terms; }
+void GetValueCommand::invoke(Solver* solver)
 {
   try
   {
-    vector<Expr> result;
-    ExprManager* em = smtEngine->getExprManager();
-    NodeManager* nm = NodeManager::fromExprManager(em);
-    for (const Expr& e : d_terms)
-    {
-      Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
-      smt::SmtScope scope(smtEngine);
-      Node request = Node::fromExpr(
-          options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
-      Node value = Node::fromExpr(smtEngine->getValue(e));
-      if (value.getType().isInteger() && request.getType() == nm->realType())
-      {
-        // Need to wrap in division-by-one so that output printers know this
-        // is an integer-looking constant that really should be output as
-        // a rational.  Necessary for SMT-LIB standards compliance.
-        value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
-      }
-      result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
-    }
-    d_result = em->mkExpr(kind::SEXPR, result);
+    d_result = solver->getValue(d_terms);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)
@@ -1699,7 +1705,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
   }
 }
 
-Expr GetValueCommand::getResult() const { return d_result; }
+Term GetValueCommand::getResult() const { return d_result; }
 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
 {
   if (!ok())
@@ -1716,15 +1722,14 @@ void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* GetValueCommand::exportTo(ExprManager* exprManager,
                                    ExprManagerMapCollection& variableMap)
 {
-  vector<Expr> exportedTerms;
-  for (std::vector<Expr>::const_iterator i = d_terms.begin();
-       i != d_terms.end();
-       ++i)
+  vector<Term> exportedTerms;
+  for (const Term& term : d_terms)
   {
-    exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
+    exportedTerms.emplace_back(
+        term.getExpr().exportTo(exprManager, variableMap));
   }
   GetValueCommand* c = new GetValueCommand(exportedTerms);
-  c->d_result = d_result.exportTo(exprManager, variableMap);
+  c->d_result = Term(d_result.getExpr().exportTo(exprManager, variableMap));
   return c;
 }
 
diff --git a/src/smt/command.h b/src/smt/command.h
index f7824c1aa..656cfd7d3 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -28,6 +28,7 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/type.h"
@@ -186,22 +187,6 @@ class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus
 
 class CVC4_PUBLIC Command
 {
- protected:
-  /**
-   * This field contains a command status if the command has been
-   * invoked, or NULL if it has not.  This field is either a
-   * dynamically-allocated pointer, or it's a pointer to the singleton
-   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
-   * it avoids the need to dynamically allocate memory in the common
-   * case of a successful command.
-   */
-  const CommandStatus* d_commandStatus;
-
-  /**
-   * True if this command is "muted"---i.e., don't print "success" on
-   * successful execution.
-   */
-  bool d_muted;
 
  public:
   typedef CommandPrintSuccess printsuccess;
@@ -211,8 +196,8 @@ class CVC4_PUBLIC Command
 
   virtual ~Command();
 
-  virtual void invoke(SmtEngine* smtEngine) = 0;
-  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+  virtual void invoke(api::Solver* solver);
+  virtual void invoke(api::Solver* solver, std::ostream& out);
 
   void toStream(std::ostream& out,
                 int toDepth = -1,
@@ -267,6 +252,29 @@ class CVC4_PUBLIC Command
   virtual Command* clone() const = 0;
 
  protected:
+  /*
+   * The following methods are for backwards compatibility *ONLY*. They are
+   * required while we update the commands to use the new API.
+   */
+  virtual void invoke(SmtEngine* smtEngine);
+  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+
+  /**
+   * This field contains a command status if the command has been
+   * invoked, or NULL if it has not.  This field is either a
+   * dynamically-allocated pointer, or it's a pointer to the singleton
+   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
+   * it avoids the need to dynamically allocate memory in the common
+   * case of a successful command.
+   */
+  const CommandStatus* d_commandStatus;
+
+  /**
+   * True if this command is "muted"---i.e., don't print "success" on
+   * successful execution.
+   */
+  bool d_muted;
+
   class ExportTransformer
   {
     ExprManager* d_exprManager;
@@ -292,7 +300,7 @@ class CVC4_PUBLIC EmptyCommand : public Command
  public:
   EmptyCommand(std::string name = "");
   std::string getName() const;
-  void invoke(SmtEngine* smtEngine) override;
+  void invoke(api::Solver* solver) override;
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
@@ -309,8 +317,8 @@ class CVC4_PUBLIC EchoCommand : public Command
 
   std::string getOutput() const;
 
-  void invoke(SmtEngine* smtEngine) override;
-  void invoke(SmtEngine* smtEngine, std::ostream& out) override;
+  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, std::ostream& out) override;
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
@@ -905,16 +913,16 @@ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
 class CVC4_PUBLIC GetValueCommand : public Command
 {
  protected:
-  std::vector<Expr> d_terms;
-  Expr d_result;
+  std::vector<api::Term> d_terms;
+  api::Term d_result;
 
  public:
-  GetValueCommand(Expr term);
-  GetValueCommand(const std::vector<Expr>& terms);
+  GetValueCommand(api::Term term);
+  GetValueCommand(const std::vector<api::Term>& terms);
 
-  const std::vector<Expr>& getTerms() const;
-  Expr getResult() const;
-  void invoke(SmtEngine* smtEngine) override;
+  const std::vector<api::Term>& getTerms() const;
+  api::Term getResult() const;
+  void invoke(api::Solver* solver) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
@@ -1372,8 +1380,8 @@ class CVC4_PUBLIC CommandSequence : public Command
   void addCommand(Command* cmd);
   void clear();
 
-  void invoke(SmtEngine* smtEngine) override;
-  void invoke(SmtEngine* smtEngine, std::ostream& out) override;
+  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, std::ostream& out) override;
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9a0d969d8..83206264f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2497,7 +2497,7 @@ void SmtEngine::defineFunction(Expr func,
       c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
   PROOF(if (options::checkUnsatCores()) {
-    d_defineCommands.push_back(c.clone());
+    d_defineCommands.push_back(static_cast<DefineFunctionCommand*>(c.clone()));
   });
 
   // type check body
@@ -4359,12 +4359,10 @@ void SmtEngine::checkUnsatCore() {
   SmtEngine coreChecker(d_exprManager);
   coreChecker.setLogic(getLogicInfo());
 
-  PROOF(
-  std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
-  for (; itg != d_defineCommands.end();  ++itg) {
-    (*itg)->invoke(&coreChecker);
-  }
-  );
+  PROOF(std::vector<DefineFunctionCommand*>::const_iterator itg =
+            d_defineCommands.begin();
+        for (; itg != d_defineCommands.end();
+             ++itg) { (*itg)->invoke(&coreChecker); });
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5aa59fad7..54899ec32 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -53,6 +53,7 @@ typedef NodeTemplate<false> TNode;
 struct NodeHashFunction;
 
 class Command;
+class DefineFunctionCommand;
 class GetModelCommand;
 
 class SmtEngine;
@@ -197,7 +198,7 @@ class CVC4_PUBLIC SmtEngine {
    * A vector of command definitions to be imported in the new
    * SmtEngine when checking unsat-cores.
    */
-  std::vector<Command*> d_defineCommands;
+  std::vector<DefineFunctionCommand*> d_defineCommands;
 
   /**
    * The logic we're in.