From d1cdf6f1719c3d56590ef6305f70f376f4d80b57 Mon Sep 17 00:00:00 2001 From: Guy Date: Mon, 25 Jul 2016 17:20:14 -0700 Subject: [PATCH] Propagate the usage of proof let maps into constant disequality proofs --- src/proof/array_proof.cpp | 14 ++++++++------ src/proof/theory_proof.cpp | 20 ++++++-------------- src/proof/theory_proof.h | 4 ++-- src/proof/uf_proof.cpp | 2 +- 4 files changed, 17 insertions(+), 23 deletions(-) diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 63758e573..ccc072eca 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -305,7 +305,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, out << " "; ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), - n1[1].toExpr()); + n1[1].toExpr(), + map); } out << "))" << std::endl; @@ -585,7 +586,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n[0].toExpr(), - n[1].toExpr()); + n[1].toExpr(), + map); return pf->d_node; } @@ -948,7 +950,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // subproof already shows constant = t3 Assert(t3 == subproof[1]); out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr()); + tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr(), map); out << " "; out << ss.str(); out << ")"; @@ -956,7 +958,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(t2 == subproof[1]); out << "(negsymm _ _ _ "; out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr()); + tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr(), map); out << " "; out << ss.str(); out << "))"; @@ -968,7 +970,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // subproof already shows constant = t3 Assert(t3 == subproof[0]); out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr()); + tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr(), map); out << " "; out << "(symm _ _ _ " << ss.str() << ")"; out << ")"; @@ -976,7 +978,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(t2 == subproof[0]); out << "(negsymm _ _ _ "; out << "(negtrans _ _ _ _ "; - tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr()); + tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr(), map); out << " "; out << "(symm _ _ _ " << ss.str() << ")"; out << "))"; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 8c74d0c2c..9753844a1 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -126,12 +126,12 @@ void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryI d_exprToTheoryIds[term].insert(id); } -void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { +void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { Assert(c1.isConst()); Assert(c2.isConst()); Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2)); - getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2); + getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2, globalLetMap); } void TheoryProofEngine::registerTerm(Expr term) { @@ -992,13 +992,6 @@ void TheoryProof::printTheoryLemmaProof(std::vector& lemma, Assert(!oc.d_lemma.isNull()); Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl; - // Original, as in Liana's branch - // Trace("pf::tp") << "; asserting " << oc.d_lemma[1].negate() << std::endl; - // th->assertFact(oc.d_lemma[1].negate(), false); - // th->check(theory::Theory::EFFORT_FULL); - - // Altered version, to handle OR lemmas - if (oc.d_lemma.getKind() == kind::OR) { Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl; for (unsigned i = 0; i < oc.d_lemma.getNumChildren(); ++i) { @@ -1087,7 +1080,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe } // The let map should already have the current expression. - ProofLetMap::const_iterator it = map.find(currentExpression.toExpr()); + ProofLetMap::const_iterator it = map.find(term); if (it != map.end()) { unsigned id = it->second.id; unsigned count = it->second.count; @@ -1178,15 +1171,14 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector& lemma, Unreachable("No boolean lemmas yet!"); } -void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { +void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { // By default, we just print a trust statement. Specific theories can implement // better proofs. - ProofLetMap emptyMap; os << "(trust_f (not (= _ "; - d_proofEngine->printBoundTerm(c1, os, emptyMap); + d_proofEngine->printBoundTerm(c1, os, globalLetMap); os << " "; - d_proofEngine->printBoundTerm(c2, os, emptyMap); + d_proofEngine->printBoundTerm(c2, os, globalLetMap); os << ")))"; } diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 968d46e68..c622fabee 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -149,7 +149,7 @@ public: void markTermForFutureRegistration(Expr term, theory::TheoryId id); - void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); virtual void treatBoolsAsFormulas(bool value) {}; @@ -286,7 +286,7 @@ public: * * @param term */ - virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); /** * Print a proof for the equivalence of n1 and n2. * diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index e122a46bc..17faf0f7d 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -264,7 +264,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << ss.str(); out << " "; - ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr()); + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr(), map); out << "))" << std::endl; } -- 2.30.2