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 5759ec8563f34a4d47baa98a2cfcea6bcae71622..6bdc1abc9942ca22c08deec4b847d045bde89696 100644 (file)
--- 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 bf7d5ef3df344380d58e93ade15bc5e4086f7116..0aebee7b3f8d9dd97d07ef884a0e3ad939a1c990 100644 (file)
--- 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 21ecd196441f236590a5e22d2cd30eb5f2612251..2d32062e207af133f42201eb103b09a4f085aafe 100644 (file)
--- 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;