diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-04-23 17:38:48 +0100 |
commit | 0daf670d46ec2e781c2060b41449f2787b6e8f66 (patch) | |
tree | 7f1870bc621407a3c387ab6eb3dc77db529355dc /src/smt/smt_engine.h | |
parent | c604492260d0555bdb3cac5ba0863b7223f21777 (diff) |
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7c5c45e42..de9b8127d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -186,6 +186,13 @@ class CVC4_PUBLIC SmtEngine { std::vector<Command*> d_dumpCommands; /** + *A vector of command definitions to be imported in the new + *SmtEngine when checking unsat-cores. + */ +#ifdef CVC4_PROOF + std::vector<Command*> d_defineCommands; +#endif + /** * The logic we're in. */ LogicInfo d_logic; @@ -261,6 +268,11 @@ class CVC4_PUBLIC SmtEngine { void checkProof(); /** + * Check that an unsatisfiable core is indeed unsatisfiable. + */ + void checkUnsatCore(); + + /** * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ |