diff options
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r-- | src/main/command_executor.cpp | 39 |
1 files changed, 21 insertions, 18 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 556e51216..9ee896107 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,11 +24,12 @@ namespace CVC4 { namespace main { -CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options): +CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : d_exprMgr(exprMgr), d_smtEngine(SmtEngine(&exprMgr)), d_options(options), - d_stats("driver") { + d_stats("driver"), + d_result() { } bool CommandExecutor::doCommand(Command* cmd) @@ -58,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd) } } -bool CommandExecutor::doCommandSingleton(Command *cmd) +bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; if(d_options[options::verbosity] >= -1) { @@ -66,25 +67,27 @@ bool CommandExecutor::doCommandSingleton(Command *cmd) } else { status = smtEngineInvoke(&d_smtEngine, cmd, NULL); } - //dump the model if option is set - if(status && d_options[options::produceModels] && d_options[options::dumpModels]) { - CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd); - if(cs != NULL) { - if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT || - (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){ - Command * gm = new GetModelCommand; - status = doCommandSingleton(gm); - } - } + Result res; + CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd); + if(cs != NULL) { + d_result = res = cs->getResult(); + } + QueryCommand* q = dynamic_cast<QueryCommand*>(cmd); + if(q != NULL) { + d_result = res = q->getResult(); + } + // dump the model if option is set + if( status && + d_options[options::produceModels] && + d_options[options::dumpModels] && + ( res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { + Command* gm = new GetModelCommand(); + status = doCommandSingleton(gm); } return status; } -std::string CommandExecutor::getSmtEngineStatus() -{ - return d_smtEngine.getInfo("status").getValue(); -} - bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) { if(out == NULL) { |