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 | |
parent | 3ad29c402d240432032b9ddf18d9133f438e1236 (diff) |
Add support for --dump-models option, in preparation for casc.
-rw-r--r-- | src/main/command_executor.cpp | 13 | ||||
-rw-r--r-- | src/smt/options | 2 |
2 files changed, 15 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; } diff --git a/src/smt/options b/src/smt/options index 2680f4105..e5f9c2eaf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal support the get-value and get-model commands option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions +option dumpModels --dump-models bool :default false + output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation # this is just a placeholder for later; it doesn't show up in command-line options listings |