diff options
author | Tim King <taking@google.com> | 2016-09-25 18:10:23 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-09-25 18:17:03 -0700 |
commit | 3589ffa88b622341e358e831ee3f1f48a5f58b8f (patch) | |
tree | 65b63c8da3287a266a99aa86480b6b6b8408ebee /src/main | |
parent | 260c6cfecb47e1b426e982399d98e6e0d964a8e8 (diff) |
Deleting the intermediate command singleton.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 40 |
1 files changed, 18 insertions, 22 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 320be701d..f9055f56c 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -129,47 +129,43 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } // dump the model/proof/unsat core if option is set - if(status) { + if (status) { Command* g = NULL; - if( d_options.getProduceModels() && - d_options.getDumpModels() && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { + if (d_options.getProduceModels() && d_options.getDumpModels() && + (res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) { g = new GetModelCommand(); } - if( d_options.getProof() && - d_options.getDumpProofs() && - res.asSatisfiabilityResult() == Result::UNSAT ) { + if (d_options.getProof() && d_options.getDumpProofs() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetProofCommand(); } - if( d_options.getDumpInstantiations() && - ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || - res.asSatisfiabilityResult() == Result::UNSAT ) ) - { + if (d_options.getDumpInstantiations() && + ((d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && + (res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) || + res.asSatisfiabilityResult() == Result::UNSAT)) { g = new GetInstantiationsCommand(); } - if( d_options.getDumpSynth() && - res.asSatisfiabilityResult() == Result::UNSAT ) - { + if (d_options.getDumpSynth() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetSynthSolutionCommand(); } - if( d_options.getDumpUnsatCores() && - res.asSatisfiabilityResult() == Result::UNSAT ) - { + if (d_options.getDumpUnsatCores() && + res.asSatisfiabilityResult() == Result::UNSAT) { g = new GetUnsatCoreCommand(); } - if(g != NULL) { + if (g != NULL) { // set no time limit during dumping if applicable - if( d_options.getForceNoLimitCpuWhileDump() ){ + if (d_options.getForceNoLimitCpuWhileDump()) { setNoLimitCPU(); } status = doCommandSingleton(g); + delete g; } } return status; |