diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 12:35:00 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 12:35:00 +0200 |
| commit | 83f91b92090ef0231156560f337affc6e5c2a33f (patch) | |
| tree | d0fe321ce4a6d29742688b9e8a5eaec859bd60ed /src/main/command_executor.cpp | |
| parent | e9fb730333b2719cddaa0a9209aa7953d7f30b0b (diff) | |
Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation. Print --dump-instantiations on sat/unknown.
Diffstat (limited to 'src/main/command_executor.cpp')
| -rw-r--r-- | src/main/command_executor.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index fee7e23a2..4bbfe2762 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,6 +22,7 @@ #include "main/options.h" #include "smt/options.h" +#include "printer/options.h" #ifndef __WIN32__ # include <sys/resource.h> @@ -132,7 +133,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetProofCommand(); } else if( d_options[options::dumpInstantiations] && - res.asSatisfiabilityResult() == Result::UNSAT ) { + ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) { g = new GetInstantiationsCommand(); } else if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { |