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.

4 files changed, 69 insertions, 43 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index caae54e7a..c91b0455c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -118,12 +118,12 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options.getVerbosity() >= -1) {
-    status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
+    status = solverInvoke(d_solver.get(), cmd, d_options.getOut());
   } else {
-    status = smtEngineInvoke(d_smtEngine, cmd, nullptr);
+    status = solverInvoke(d_solver.get(), cmd, nullptr);
   }
 
-  Result res;
+  api::Result res;
   const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
   if(cs != nullptr) {
     d_result = res = cs->getResult();
@@ -149,34 +149,34 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
     if (d_options.getDumpModels()
-        && (res.asSatisfiabilityResult() == Result::SAT
-            || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE)))
+        && (res.isSat()
+            || (res.isSatUnknown()
+                && res.getResult().whyUnknown() == Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getDumpProofs()
-        && res.asSatisfiabilityResult() == Result::UNSAT)
+    if (d_options.getDumpProofs() && res.isUnsat())
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
     if (d_options.getDumpInstantiations()
         && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
-             && (res.asSatisfiabilityResult() == Result::SAT
-                 || (res.isUnknown()
-                     && res.whyUnknown() == Result::INCOMPLETE)))
-            || res.asSatisfiabilityResult() == Result::UNSAT))
+             && (res.isSat()
+                 || (res.isSatUnknown()
+                     && res.getResult().whyUnknown() == Result::INCOMPLETE)))
+            || res.isUnsat()))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (d_options.getDumpSynth() &&
-        res.asSatisfiabilityResult() == Result::UNSAT) {
+    if (d_options.getDumpSynth() && res.isUnsat())
+    {
       getterCommands.emplace_back(new GetSynthSolutionCommand());
     }
 
-    if (d_options.getDumpUnsatCores() &&
-        res.asSatisfiabilityResult() == Result::UNSAT) {
+    if (d_options.getDumpUnsatCores() && res.isUnsat())
+    {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
@@ -197,17 +197,21 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   return status;
 }
 
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
+bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out)
 {
-  if(out == NULL) {
-    cmd->invoke(smt);
-  } else {
-    cmd->invoke(smt, *out);
+  if (out == NULL)
+  {
+    cmd->invoke(solver);
+  }
+  else
+  {
+    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->getOption(commandName) == "0")
+  {
     return true;
   }
   return !cmd->fail();
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 92b0cd166..d7899020e 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -44,7 +44,7 @@ class CommandExecutor
   SmtEngine* d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
-  Result d_result;
+  api::Result d_result;
 
  public:
   CommandExecutor(Options& options);
@@ -67,7 +67,7 @@ class CommandExecutor
   /** Get a pointer to the solver object owned by this CommandExecutor. */
   api::Solver* getSolver() { return d_solver.get(); }
 
-  Result getResult() const { return d_result; }
+  api::Result getResult() const { return d_result; }
   void reset();
 
   StatisticsRegistry& getStatisticsRegistry() {
@@ -101,7 +101,7 @@ private:
 
 }; /* class CommandExecutor */
 
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
+bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out);
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 43529278b..9fff51b93 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -450,7 +450,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
     }
 
-    Result result;
+    api::Result result;
     if(status) {
       result = pExecutor->getResult();
       returnValue = 0;
@@ -467,7 +467,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     _exit(returnValue);
 #endif /* CVC4_COMPETITION_MODE */
 
-    ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+    ReferenceStat<api::Result> s_statSatResult("sat/unsat", result);
     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
                                        &s_statSatResult);
 
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 121513856..b798d03ee 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -309,34 +309,56 @@ restart:
   CommandSequence *cmd_seq = new CommandSequence();
   Command *cmd;
 
-  try {
-    while( (cmd = d_parser->nextCommand()) ) {
+  try
+  {
+    while ((cmd = d_parser->nextCommand()))
+    {
       cmd_seq->addCommand(cmd);
-      if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+      if (dynamic_cast<QuitCommand*>(cmd) != NULL)
+      {
         d_quit = true;
         break;
-      } else {
+      }
+      else
+      {
 #if HAVE_LIBEDITLINE
-        if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
-        } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
-        } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol());
-        } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
+        if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL)
+        {
+          s_declarations.insert(
+              dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+        }
+        else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL)
+        {
+          s_declarations.insert(
+              dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
+        }
+        else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL)
+        {
+          s_declarations.insert(
+              dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol());
+        }
+        else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL)
+        {
+          s_declarations.insert(
+              dynamic_cast<DefineSortCommand*>(cmd)->getSymbol());
         }
 #endif /* HAVE_LIBEDITLINE */
       }
     }
-  } catch(ParserEndOfFileException& pe) {
+  }
+  catch (ParserEndOfFileException& pe)
+  {
     line += "\n";
     goto restart;
-  } catch(ParserException& pe) {
+  }
+  catch (ParserException& pe)
+  {
     if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
     {
       d_out << "(error \"" << pe << "\")" << endl;
-    } else {
+    }
+    else
+    {
       d_out << pe << endl;
     }
     // We can't really clear out the sequence and abort the current line,
@@ -350,8 +372,8 @@ restart:
     // FIXME: does that mean e.g. that a pushed LET scope might not yet have
     // been popped?!
     //
-    //delete cmd_seq;
-    //cmd_seq = new CommandSequence();
+    // delete cmd_seq;
+    // cmd_seq = new CommandSequence();
   }
 
   return cmd_seq;