From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 9 Jun 2021 17:15:30 +0000 (+0200)
Subject: Push complex check inside GetInstantiationsCommand (#6715)
X-Git-Tag: cvc5-1.0.0~1619
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd34574f476827c11e1f0d9a33141a04b5175696;p=cvc5.git

Push complex check inside GetInstantiationsCommand (#6715)

This PR pushes a rather complex check from the CommandExecutor inside the GetInstantiationsCommand.
The aim is to only use the instFormatMode option in the library (command.cpp) but not the main driver (command_executor.cpp).
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5759ec856..6bdc1abc9 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -173,13 +173,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     }
 
     if (options::getDumpInstantiations(d_options)
-        && ((options::getInstFormatMode(d_options)
-                 != options::InstFormatMode::SZS
-             && (res.isSat()
-                 || (res.isSatUnknown()
-                     && res.getUnknownExplanation()
-                            == api::Result::INCOMPLETE)))
-            || isResultUnsat))
+        && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bf7d5ef3d..0aebee7b3 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -31,6 +31,7 @@
 #include "expr/symbol_manager.h"
 #include "expr/type_node.h"
 #include "options/options.h"
+#include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
@@ -2041,6 +2042,16 @@ void GetProofCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
+bool GetInstantiationsCommand::isEnabled(api::Solver* solver,
+                                         const api::Result& res)
+{
+  return (solver->getOptions().printer.instFormatMode
+              != options::InstFormatMode::SZS
+          && (res.isSat()
+              || (res.isSatUnknown()
+                  && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
+         || res.isUnsat() || res.isEntailed();
+}
 void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
diff --git a/src/smt/command.h b/src/smt/command.h
index 21ecd1964..2d32062e2 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1077,6 +1077,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command
  public:
   GetInstantiationsCommand();
 
+  static bool isEnabled(api::Solver* solver, const api::Result& res);
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;