diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-17 17:40:34 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-17 17:40:40 -0500 |
commit | 12a1b56a7a6573ae5af47e9d9d6e757e70a6b7a1 (patch) | |
tree | c998399e536c044b2b1c43a94790b3fc02352ea8 /src/main/command_executor.cpp | |
parent | 3ad29c402d240432032b9ddf18d9133f438e1236 (diff) |
Add support for --dump-models option, in preparation for casc.
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r-- | src/main/command_executor.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f1742b549..556e51216 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -19,6 +19,8 @@ #include "main/main.h" +#include "smt/options.h" + namespace CVC4 { namespace main { @@ -64,6 +66,17 @@ 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); + } + } + } return status; } |