From 5c062833d435e3dde5db3a8223c379a3e8cca520 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 22 Sep 2020 22:12:17 -0500
Subject: 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.
---
 src/main/command_executor.cpp | 46 +++++++++++++++++++++++--------------------
 1 file changed, 25 insertions(+), 21 deletions(-)

(limited to 'src/main/command_executor.cpp')

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();
-- 
cgit v1.2.3