diff options
author | Guy <katz911@gmail.com> | 2016-07-06 16:41:33 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-06 16:41:33 -0700 |
commit | f9899f4ffc081369f419b8572a5aa397fbaa428a (patch) | |
tree | 2d48cf1e799e3336229ce34d0344ca3733a54a45 /src/proof | |
parent | e3f06d67aec4c423530002562e556f265f249123 (diff) |
A few proof bugs fixed
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/array_proof.cpp | 68 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 56 |
2 files changed, 101 insertions, 23 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 484bc70c8..18e01728b 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -637,6 +637,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. + if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -900,7 +901,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // inner index != outer index // t3 is the outer index - Assert(pf->d_children.size() == 1); std::stringstream ss; Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); @@ -915,22 +915,76 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, tp->printTerm(t4.toExpr(), out, map); out << " "; + Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node << ". t3 is: " << t3 << std::endl << "subproof is: " << subproof << std::endl; Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; - if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); + // The subproof needs to show that t2 != t3. This can either be a direct disequality, + // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant. + if (subproof.getKind() == kind::NOT) { + // The subproof is for t2 != t3 (or t3 != t2) + if (subproof[0][1] == t3) { + Debug("pf::array") << "Dont need symmetry!" << std::endl; + out << ss.str(); + } else { + Debug("pf::array") << "Need symmetry!" << std::endl; + out << "(negsymm _ _ _ " << ss.str() << ")"; + } } else { - Debug("pf::array") << "Need symmetry!" << std::endl; - out << "(negsymm _ _ _ " << ss.str() << ")"; + // Either t2 or t3 is a constant. + Assert(subproof.getKind() == kind::EQUAL); + Assert(subproof[0].isConst() || subproof[1].isConst()); + Assert(t2.isConst() || t3.isConst()); + Assert(!(t2.isConst() && t3.isConst())); + + bool t2IsConst = t2.isConst(); + if (subproof[0].isConst()) { + if (t2IsConst) { + // (t3 == subproof[1]) == subproof[0] != t2 + // goal is t2 != t3 + // subproof already shows constant = t3 + Assert(t3 == subproof[1]); + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr()); + out << " "; + out << ss.str(); + out << ")"; + } else { + Assert(t2 == subproof[1]); + out << "(negsymm _ _ _ "; + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr()); + out << " "; + out << ss.str(); + out << "))"; + } + } else { + if (t2IsConst) { + // (t3 == subproof[0]) == subproof[1] != t2 + // goal is t2 != t3 + // subproof already shows constant = t3 + Assert(t3 == subproof[0]); + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr()); + out << " "; + out << "(symm _ _ _ " << ss.str() << ")"; + out << ")"; + } else { + Assert(t2 == subproof[0]); + out << "(negsymm _ _ _ "; + out << "(negtrans _ _ _ _ "; + tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr()); + out << " "; + out << "(symm _ _ _ " << ss.str() << ")"; + out << "))"; + } + } } out << ")"; - return ret; } else { Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index d12b561a6..f0f333598 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -135,17 +135,17 @@ void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, } void TheoryProofEngine::registerTerm(Expr term) { - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; + Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; if (d_registrationCache.count(term)) { return; } - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; + Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl; + Debug("pf::tp::register") << "Term's theory( " << term << " ) = " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -165,7 +165,7 @@ void TheoryProofEngine::registerTerm(Expr term) { // A special case: the array theory needs to know of every skolem, even if // it belongs to another theory (e.g., a BV skolem) if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) { - Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl; + Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering a non-array skolem: " << term << std::endl; getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term); } @@ -632,15 +632,27 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, clause_expr[k] = missingAssertion->toExpr(); std::ostringstream rewritten; - rewritten << "(or_elim_1 _ _ "; - rewritten << "(not_not_intro _ "; - rewritten << pm->getLitName(explanation); - rewritten << ") (iff_elim_1 _ _ "; - rewritten << d_assertionToRewrite[missingAssertion->negate()]; - rewritten << "))"; + + if (missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) { + rewritten << "(or_elim_2 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_2 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + } + else { + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + } Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << ", explanation = " << explanation << std::endl << std::endl; pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); @@ -742,15 +754,27 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, currentClauseExpr[k] = missingAssertion->toExpr(); std::ostringstream rewritten; - rewritten << "(or_elim_1 _ _ "; - rewritten << "(not_not_intro _ "; - rewritten << pm->getLitName(explanation); - rewritten << ") (iff_elim_1 _ _ "; - rewritten << d_assertionToRewrite[missingAssertion->negate()]; - rewritten << "))"; + + if (missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) { + rewritten << "(or_elim_2 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_2 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + } + else { + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + } Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << "explanation = " << explanation << std::endl << std::endl; pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); |