From f9899f4ffc081369f419b8572a5aa397fbaa428a Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 6 Jul 2016 16:41:33 -0700 Subject: [PATCH] A few proof bugs fixed --- src/proof/array_proof.cpp | 68 +++++++++++++++++-- src/proof/theory_proof.cpp | 56 ++++++++++----- .../arrays/array_proof_reconstruction.cpp | 4 +- src/theory/uf/equality_engine.cpp | 3 +- 4 files changed, 104 insertions(+), 27 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()); diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 6dfd14157..8dd7fe782 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -60,7 +60,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, // or ((a[i]:=t)[k] == a[k]) because (i != k). if (proof) { - if (a.getNumChildren() == 2) { + if (a.getKind() == kind::SELECT) { // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k). // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be @@ -156,7 +156,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, proof->d_children.push_back(childProof); } else { - // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), + // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), Node indexOne = a; Node indexTwo = b; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 25b12f75f..09d348584 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -393,7 +393,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) { - Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; + Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), reason = " << reason << ", pid = " << pid << std::endl; if (d_done) { return; @@ -1204,7 +1204,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): adding: " << reason << std::endl; Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; - Node a = d_nodes[currentNode]; Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; -- 2.30.2