diff options
| -rw-r--r-- | src/proof/proof_manager.cpp | 17 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 29 |
2 files changed, 30 insertions, 16 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a86991963..3249ed19d 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -41,6 +41,15 @@ namespace CVC4 { +std::string nodeSetToString(const std::set<Node>& nodes) { + std::ostringstream os; + std::set<Node>::const_iterator it; + for (it = nodes.begin(); it != nodes.end(); ++it) { + os << *it << " "; + } + return os.str(); +} + std::string append(const std::string& str, uint64_t num) { std::ostringstream os; os << str << num; @@ -315,17 +324,23 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod IdToSatClause::const_iterator it; std::set<Node> seen; + Debug("pf::lemmasUnsatCore") << "Dumping all lemmas in unsat core" << std::endl; for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { std::set<Node> lemma = satClauseToNodeSet(it->second); + Debug("pf::lemmasUnsatCore") << nodeSetToString(lemma); // TODO: we should be able to drop the "haveProofRecipe" check. // however, there are some rewrite issues with the arith solver, resulting // in non-registered recipes. For now we assume no one is requesting arith lemmas. LemmaProofRecipe recipe; - if (!getCnfProof()->haveProofRecipe(lemma)) + if (!getCnfProof()->haveProofRecipe(lemma)) { + Debug("pf::lemmasUnsatCore") << "\t[no recipe]" << std::endl; continue; + } recipe = getCnfProof()->getProofRecipe(lemma); + Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe.getTheory() + << ", original = " << recipe.getOriginalLemma() << "]" << std::endl; if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) == seen.end()) { lemmas.push_back(recipe.getOriginalLemma()); seen.insert(recipe.getOriginalLemma()); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bd0b467f2..94281156f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -106,19 +106,18 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori lemma = d_engine->preprocess(lemma); bool negated = (lemma.getKind() == kind::NOT); - if (negated) - lemma = lemma[0]; + Node nnLemma = negated ? lemma[0] : lemma; - switch (lemma.getKind()) { + switch (nnLemma.getKind()) { case kind::AND: if (!negated) { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - registerLemmaRecipe(lemma[i], originalLemma, false, theoryId); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); } else { NodeBuilder<> builder(kind::OR); - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - builder << lemma[i].negate(); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + builder << nnLemma[i].negate(); Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder; registerLemmaRecipe(disjunction, originalLemma, false, theoryId); @@ -127,21 +126,21 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori case kind::IFF: if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); } else { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); } break; case kind::ITE: if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId); } else { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId); } break; |