From 3589ffa88b622341e358e831ee3f1f48a5f58b8f Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 25 Sep 2016 18:10:23 -0700 Subject: Deleting the intermediate command singleton. --- src/main/command_executor.cpp | 40 ++++++++++++++++++---------------------- 1 file 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; -- cgit v1.2.3