diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-09 19:15:30 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-09 17:15:30 +0000 |
| commit | cd34574f476827c11e1f0d9a33141a04b5175696 (patch) | |
| tree | a1adab1b8613e3418e462681f5705ba290fe2af3 | |
| parent | e9d650f668bf044b2baad5328d80e64522454c50 (diff) | |
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).
| -rw-r--r-- | src/main/command_executor.cpp | 8 | ||||
| -rw-r--r-- | src/smt/command.cpp | 11 | ||||
| -rw-r--r-- | src/smt/command.h | 1 |
3 files changed, 13 insertions, 7 deletions
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; |