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/proof/proof_manager.cpp | |
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/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d155630e5..43328e1de 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -69,6 +69,7 @@ ProofManager::~ProofManager() { } ProofManager* ProofManager::currentPM() { + Assert(PROOF_ON(), "Cannot call ProofManager when proofs are off"); return smt::currentProofManager(); } @@ -292,6 +293,36 @@ void ProofManager::traceUnsatCore() { } } +void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) { + d_satProof->constructProof(); + + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_satProof->collectClausesUsed(used_inputs, used_lemmas); + + IdToSatClause::const_iterator it; + + for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { + std::set<Node> lemma; + for(unsigned i = 0; i < it->second->size(); ++i) { + prop::SatLiteral lit = (*(it->second))[i]; + Node node = getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + lemma.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = getCnfProof()->getProofRecipe(lemma); + + if (recipe.simpleLemma() && recipe.getTheory() == theory) { + lemmas.push_back(recipe.getOriginalLemma()); + } + } +} + void ProofManager::addAssertion(Expr formula) { Debug("proof:pm") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); |