diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 18:52:02 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 18:52:02 -0400 |
| commit | 7f885c4e79501827e70fe14683152af85c5f8bfd (patch) | |
| tree | f4d39106870e15789e89723e2e5249541a1dcf8b /src/main | |
| parent | 3377b80f8ade22c4e7b2e4885d88b66a44306133 (diff) | |
Some minor cleanup.
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/command_executor.cpp | 21 | ||||
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 2 |
2 files changed, 12 insertions, 11 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 4bbfe2762..52522d591 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -47,7 +47,6 @@ void setNoLimitCPU() { #endif /* ! __WIN32__ */ } - void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString); CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : @@ -128,17 +127,19 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { g = new GetModelCommand(); - } else if( d_options[options::proof] && - d_options[options::dumpProofs] && - res.asSatisfiabilityResult() == Result::UNSAT ) { + } + if( d_options[options::proof] && + d_options[options::dumpProofs] && + res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetProofCommand(); - } else if( d_options[options::dumpInstantiations] && - ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && - ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || - res.asSatisfiabilityResult() == Result::UNSAT ) ) { + } + if( d_options[options::dumpInstantiations] && + ( ( 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 ) { + } + if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetUnsatCoreCommand(); } if(g != NULL) { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 7d35a443a..6e10c9a8a 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -11,7 +11,7 @@ ** ** \brief An additional layer between commands and invoking them. ** - ** The portfolio executer branches check-sat queries to several + ** The portfolio executor branches check-sat queries to several ** threads. **/ |