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 /src/smt/command.cpp | |
| 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).
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
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 |