diff options
author | Guy <katz911@gmail.com> | 2016-07-15 16:48:25 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-15 16:48:25 -0700 |
commit | 378475e685d514ec47347a9f27a2825391f9b207 (patch) | |
tree | 520757bb2da753201e7e643bc47d1a116edf0ef3 /src/theory | |
parent | c0af8cf1c1e3edca35bb7ae4edf1831ebdee0abd (diff) |
The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 913a6800b..b4c6c97cd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -91,6 +91,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, Node emptyNode; LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode); + proofRecipe->setOriginalLemma(lemma); + Node rewritten; if (lemma.getKind() == kind::OR) { for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { @@ -156,7 +158,7 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); - + //initialize the model if( d_logicInfo.isQuantified() ) { d_curr_model = d_quantEngine->getModel(); |