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;
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());
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);
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;