From 47a084552a39f4612fcec921708718a34465a20c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2020 18:27:17 -0500 Subject: TrustNode throughout TheoryEngine --- src/prop/theory_proxy.cpp | 3 +- src/theory/shared_terms_database.cpp | 22 -------------- src/theory/theory_engine.cpp | 58 ++++++++++++++++++++++-------------- src/theory/theory_engine.h | 7 +++-- 4 files changed, 42 insertions(+), 48 deletions(-) diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 38c99f551..0cdad4fdf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -79,7 +79,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { LemmaProofRecipe* proofRecipe = NULL; PROOF(proofRecipe = new LemmaProofRecipe;); - Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + theory::TrustNode tte = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + Node theoryExplanation = tte.getNode(); PROOF({ ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 6d87530cb..c0ba11f72 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -218,28 +218,6 @@ bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) { return true; } -static Node mkAnd(const std::vector& conjunctions) { - Assert(conjunctions.size() > 0); - - std::set all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - NodeBuilder<> conjunction(kind::AND); - std::set::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - void SharedTermsDatabase::checkForConflict() { if (d_inConflict) { d_inConflict = false; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b2793fac9..7a0c68f37 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1542,8 +1542,8 @@ static Node mkExplanation(const std::vector& explanation) { return conjunction; } - -Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { + +theory::TrustNode TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1598,7 +1598,7 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe } }); - return explanation; + return texplanation; } Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl; @@ -1615,8 +1615,8 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe TheoryId explainer = nodeExplainerPair.d_theory; // Create the workplace for explanations - std::vector explanationVector; - explanationVector.push_back(d_propagationMap[toExplain]); + std::vector vec; + vec.push_back(d_propagationMap[toExplain]); // Process the explanation if (proofRecipe) { Node emptyNode; @@ -1626,15 +1626,15 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe proofRecipe->addBaseAssertion(node); } - getExplanation(explanationVector, proofRecipe); - Node explanation = mkExplanation(explanationVector); + TrustNode texplanation = getExplanation(vec, proofRecipe); + Node explanation = texplanation.getNode(); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return explanation; + return texplanation; } -Node TheoryEngine::getExplanation(TNode node) { +theory::TrustNode TheoryEngine::getExplanation(TNode node) { LemmaProofRecipe *dontCareRecipe = NULL; return getExplanationAndRecipe(node, dontCareRecipe); } @@ -1764,14 +1764,23 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // if proofNew is enabled, then d_lazyProof contains a proof of n. - /* - Node lemma = node; - if (negated) + if (options::proofNew()) { - lemma = lemma.negate(); + Node lemma = node; + if (negated) + { + lemma = lemma.negate(); + } + if (!d_lazyProof->hasStep(lemma) && !d_lazyProof->hasGenerator(lemma)) + { + Trace("te-proof") << "No proof for lemma: " << lemma << std::endl; + Trace("te-proof-warn") << "WARNING: No proof for lemma: " << lemma << std::endl; + } + else + { + Trace("te-proof") << "Proof for lemma: " << lemma << std::endl; + } } - Assert (!options::proofNew() || d_lazyProof->hasStep(lemma)); - */ AssertionPipeline additionalLemmas; @@ -1827,10 +1836,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { + Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; // if proofNew is enabled, then d_lazyProof contains a proof of conflict.negate() - //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate())); + //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) || d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH); - Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; @@ -1862,13 +1871,13 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations - std::vector explanationVector; - explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + std::vector vec; + vec.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); // Process the explanation - getExplanation(explanationVector, proofRecipe); + TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); - Node fullConflict = mkExplanation(explanationVector); + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); @@ -1954,7 +1963,7 @@ void TheoryEngine::staticInitializeBVOptions( } } -void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { +theory::TrustNode TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); unsigned i = 0; // Index of the current literal we are processing @@ -2131,6 +2140,11 @@ void TheoryEngine::getExplanation(std::vector& explanationVector } } }); + + + Node exp = mkExplanation(explanationVector); + // FIXME + return theory::TrustNode::mkTrustLemma(exp,nullptr); } void TheoryEngine::setUserAttribute(const std::string& attr, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index cd3e8e122..77f597845 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -51,6 +51,7 @@ #include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" +#include "theory/trust_node.h" namespace CVC4 { @@ -514,7 +515,7 @@ class TheoryEngine { * theory that sent the literal. The lemmaProofRecipe will contain a list * of the explanation steps required to produce the original node. */ - void getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); + theory::TrustNode getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); public: @@ -635,13 +636,13 @@ public: /** * Returns an explanation of the node propagated to the SAT solver. */ - Node getExplanation(TNode node); + theory::TrustNode getExplanation(TNode node); /** * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); + theory::TrustNode getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); /** * collect model info -- cgit v1.2.3 From e3347e0f2664a69c3799ab0f5db09a751282add2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2020 18:29:06 -0500 Subject: Fix format --- src/theory/shared_terms_database.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index ccee94c8d..5abf0b281 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -35,7 +35,7 @@ class TheoryEngine; class SharedTermsDatabase : public context::ContextNotifyObj { -public: + public: /** A container for a list of shared terms */ typedef std::vector shared_terms_list; @@ -43,7 +43,7 @@ public: /** The iterator to go through the shared terms list */ typedef shared_terms_list::const_iterator shared_terms_iterator; -private: + private: /** Some statistics */ IntStat d_statSharedTerms; @@ -72,7 +72,7 @@ private: typedef context::CDHashSet RegisteredEqualitiesSet; RegisteredEqualitiesSet d_registeredEqualities; -private: + private: /** This method removes all the un-necessary stuff from the maps */ void backtrack(); @@ -162,7 +162,7 @@ private: */ void checkForConflict(); -public: + public: SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context, context::UserContext* userContext, @@ -256,7 +256,7 @@ public: */ theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } -protected: + protected: /** Pointer to the lazy proof of TheoryEngine */ LazyCDProof* d_lazyPf; -- cgit v1.2.3 From 4c8209e654e0dd8643458c9264f30b996dd5906a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2020 18:29:28 -0500 Subject: Format --- src/prop/theory_proxy.cpp | 3 +- src/theory/shared_terms_database.cpp | 15 ++++---- src/theory/shared_terms_database.h | 22 +++++------- src/theory/strings/core_solver.cpp | 32 +++++++++-------- src/theory/strings/infer_proof_cons.cpp | 6 ++-- src/theory/strings/proof_checker.cpp | 4 +-- src/theory/theory_engine.cpp | 64 ++++++++++++++++++++------------- src/theory/theory_engine.h | 13 ++++--- src/theory/uf/eq_proof.h | 3 +- src/theory/uf/equality_engine.cpp | 12 +++++-- 10 files changed, 102 insertions(+), 72 deletions(-) diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 0cdad4fdf..2c6d22d27 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -79,7 +79,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { LemmaProofRecipe* proofRecipe = NULL; PROOF(proofRecipe = new LemmaProofRecipe;); - theory::TrustNode tte = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + theory::TrustNode tte = + d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); Node theoryExplanation = tte.getNode(); PROOF({ diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index c0ba11f72..735f0703c 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -27,7 +27,8 @@ namespace CVC4 { SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context, context::UserContext* userContext, - ProofNodeManager* pnm, LazyCDProof* lcp) + ProofNodeManager* pnm, + LazyCDProof* lcp) : ContextNotifyObj(context), d_statSharedTerms("theory::shared_terms", 0), d_addedSharedTermsSize(context, 0), @@ -36,11 +37,12 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, d_registeredEqualities(context), d_EENotify(*this), d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true), - d_pfee(context,userContext,d_equalityEngine,pnm, lcp!=nullptr), + d_pfee(context, userContext, d_equalityEngine, pnm, lcp != nullptr), d_theoryEngine(theoryEngine), d_inConflict(context, false), d_conflictPolarity(), - d_lazyPf(lcp) { + d_lazyPf(lcp) +{ smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } @@ -203,7 +205,7 @@ void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode re { Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; // Add it to the equality engine - //d_equalityEngine.assertEquality(equality, polarity, reason); + // d_equalityEngine.assertEquality(equality, polarity, reason); d_pfee.assertAssume(reason); // Check for conflict checkForConflict(); @@ -227,7 +229,7 @@ void SharedTermsDatabase::checkForConflict() { conflict = conflict.notNode(); } TrustNode trnc = d_pfee.assertConflict(conflict); - if (d_lazyPf!=nullptr) + if (d_lazyPf != nullptr) { // add the step to the proof Node ckey = TrustNode::getConflictKeyValue(trnc.getNode()); @@ -248,7 +250,8 @@ bool SharedTermsDatabase::isKnown(TNode literal) const { } } -theory::TrustNode SharedTermsDatabase::explain(TNode literal) { +theory::TrustNode SharedTermsDatabase::explain(TNode literal) +{ TrustNode trn = d_pfee.explain(literal); return trn; } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 5abf0b281..9bd00962f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -20,23 +20,21 @@ #include #include "context/cdhashset.h" +#include "expr/lazy_proof.h" #include "expr/node.h" +#include "expr/proof_node_manager.h" #include "theory/theory.h" +#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" -#include "theory/trust_node.h" -#include "expr/proof_node_manager.h" #include "util/statistics_registry.h" -#include "expr/lazy_proof.h" namespace CVC4 { class TheoryEngine; class SharedTermsDatabase : public context::ContextNotifyObj { - public: - /** A container for a list of shared terms */ typedef std::vector shared_terms_list; @@ -44,7 +42,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { typedef shared_terms_list::const_iterator shared_terms_iterator; private: - /** Some statistics */ IntStat d_statSharedTerms; @@ -73,7 +70,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { RegisteredEqualitiesSet d_registeredEqualities; private: - /** This method removes all the un-necessary stuff from the maps */ void backtrack(); @@ -118,7 +114,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { /** Equality engine */ theory::eq::EqualityEngine d_equalityEngine; - + /** Proof equality engine */ theory::eq::ProofEqEngine d_pfee; @@ -163,10 +159,11 @@ class SharedTermsDatabase : public context::ContextNotifyObj { void checkForConflict(); public: - - SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context, - context::UserContext* userContext, - ProofNodeManager* pnm, LazyCDProof* lcp); + SharedTermsDatabase(TheoryEngine* theoryEngine, + context::Context* context, + context::UserContext* userContext, + ProofNodeManager* pnm, + LazyCDProof* lcp); ~SharedTermsDatabase(); /** @@ -257,7 +254,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } protected: - /** Pointer to the lazy proof of TheoryEngine */ LazyCDProof* d_lazyPf; /** diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index cc73da8f2..87d861cf2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -773,17 +773,20 @@ Node CoreSolver::getConclusion(Node x, { // we can assume its length is greater than zero Node emp = Word::mkEmptyWord(sk1.getType()); - conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(), - nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0)))); + conc = nm->mkNode( + AND, + conc, + sk1.eqNode(emp).negate(), + nm->mkNode( + GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConst(Rational(0)))); } } - else if (rule==PfRule::CONCAT_CSPLIT) + else if (rule == PfRule::CONCAT_CSPLIT) { - Assert (y.isConst()); + Assert(y.isConst()); size_t yLen = Word::getLength(y); - Node firstChar = yLen == 1 ? y - : (isRev ? Word::suffix(y, 1) - : Word::prefix(y, 1)); + Node firstChar = + yLen == 1 ? y : (isRev ? Word::suffix(y, 1) : Word::prefix(y, 1)); Node sk = skc->mkSkolemCached( x, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, @@ -792,17 +795,15 @@ Node CoreSolver::getConclusion(Node x, conc = x.eqNode(isRev ? utils::mkNConcat(sk, firstChar) : utils::mkNConcat(firstChar, sk)); } - else if (rule==PfRule::CONCAT_CPROP) + else if (rule == PfRule::CONCAT_CPROP) { // expect (str.++ z c1) and c2 - Assert (x.getKind()==STRING_CONCAT && x.getNumChildren()==2); + Assert(x.getKind() == STRING_CONCAT && x.getNumChildren() == 2); Node z = x[isRev ? 1 : 0]; Node c1 = x[isRev ? 0 : 1]; - Assert (c1.isConst()); + Assert(c1.isConst()); Node c2 = y; - Assert (c2.isConst()); - - + Assert(c2.isConst()); } return conc; @@ -1556,11 +1557,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k SkolemCache* skc = d_termReg.getSkolemCache(); std::vector newSkolems; - iinfo.d_conc = getConclusion(nc,nfcv[index],PfRule::CONCAT_CSPLIT,isRev,skc,newSkolems); + iinfo.d_conc = getConclusion( + nc, nfcv[index], PfRule::CONCAT_CSPLIT, isRev, skc, newSkolems); NormalForm::getExplanationForPrefixEq( nfi, nfj, index, index, iinfo.d_ant); iinfo.d_ant.push_back(expNonEmpty); - Assert(newSkolems.size()==1); + Assert(newSkolems.size() == 1); iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]); iinfo.d_id = Inference::SSPLIT_CST; iinfo.d_idRev = isRev; diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 9af4dc565..891f23cd2 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -48,7 +48,7 @@ void InferProofCons::notifyFact(const InferInfo& ii) Trace("strings-ipc-debug") << "...duplicate!" << std::endl; return; } - if (fact.getKind()==EQUAL) + if (fact.getKind() == EQUAL) { Node symFact = fact[1].eqNode(fact[0]); if (d_lazyFactMap.find(symFact) != d_lazyFactMap.end()) @@ -1012,9 +1012,9 @@ std::shared_ptr InferProofCons::getProofFor(Node fact) CDProof pf(d_pnm); // get the inference NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact); - if (it==d_lazyFactMap.end()) + if (it == d_lazyFactMap.end()) { - if (fact.getKind()==EQUAL) + if (fact.getKind() == EQUAL) { // Use the symmetric fact. There is no need to explictly make a // SYMM proof, as this is handled by CDProof::mkProof below. diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index a5a22dfa0..3b06ea447 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -307,8 +307,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id, std::vector newSkolems; Node kt0 = ProofSkolemCache::getSkolemForm(t0); Node ks0 = ProofSkolemCache::getSkolemForm(s0); - Node conc = CoreSolver::getConclusion( - kt0, ks0, id, isRev, &skc, newSkolems); + Node conc = + CoreSolver::getConclusion(kt0, ks0, id, isRev, &skc, newSkolems); conc = ProofSkolemCache::getWitnessForm(conc); return conc; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7a0c68f37..789bc8cb1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -197,8 +197,12 @@ TheoryEngine::TheoryEngine(context::Context* context, d_logicInfo(logicInfo), d_pchecker(new ProofChecker), d_pNodeManager(new ProofNodeManager(d_pchecker.get())), - d_lazyProof(options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr), - d_sharedTerms(this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()), + d_lazyProof( + options::proofNew() + ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) + : nullptr), + d_sharedTerms( + this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()), d_masterEqualityEngine(nullptr), d_masterEENotify(*this), d_quantEngine(nullptr), @@ -1542,8 +1546,10 @@ static Node mkExplanation(const std::vector& explanation) { return conjunction; } - -theory::TrustNode TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { + +theory::TrustNode TheoryEngine::getExplanationAndRecipe( + TNode node, LemmaProofRecipe* proofRecipe) +{ Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1634,7 +1640,8 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRe return texplanation; } -theory::TrustNode TheoryEngine::getExplanation(TNode node) { +theory::TrustNode TheoryEngine::getExplanation(TNode node) +{ LemmaProofRecipe *dontCareRecipe = NULL; return getExplanationAndRecipe(node, dontCareRecipe); } @@ -1745,7 +1752,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). // spendResource(); - + // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl; @@ -1774,14 +1781,15 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, if (!d_lazyProof->hasStep(lemma) && !d_lazyProof->hasGenerator(lemma)) { Trace("te-proof") << "No proof for lemma: " << lemma << std::endl; - Trace("te-proof-warn") << "WARNING: No proof for lemma: " << lemma << std::endl; + Trace("te-proof-warn") + << "WARNING: No proof for lemma: " << lemma << std::endl; } else { Trace("te-proof") << "Proof for lemma: " << lemma << std::endl; } } - + AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe @@ -1808,10 +1816,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++ i) { + for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++i) + { Node rewritten = Rewriter::rewrite(additionalLemmas[i]); additionalLemmas.replace(i, rewritten); - d_propEngine->assertLemma(additionalLemmas[i], i==0 && negated, removable, rule, node); + d_propEngine->assertLemma( + additionalLemmas[i], i == 0 && negated, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1837,9 +1847,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; - // if proofNew is enabled, then d_lazyProof contains a proof of conflict.negate() - //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) || d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH); - + // if proofNew is enabled, then d_lazyProof contains a proof of + // conflict.negate() + // Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) || + // d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH); Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; @@ -1872,7 +1883,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations std::vector vec; - vec.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + vec.push_back( + NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); // Process the explanation TrustNode tnc = getExplanation(vec, proofRecipe); @@ -1963,7 +1975,10 @@ void TheoryEngine::staticInitializeBVOptions( } } -theory::TrustNode TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { +theory::TrustNode TheoryEngine::getExplanation( + std::vector& explanationVector, + LemmaProofRecipe* proofRecipe) +{ Assert(explanationVector.size() > 0); unsigned i = 0; // Index of the current literal we are processing @@ -2064,15 +2079,17 @@ theory::TrustNode TheoryEngine::getExplanation(std::vector& expl if (toExplain.d_theory == THEORY_BUILTIN) { texplanation = d_sharedTerms.explain(toExplain.d_node); - Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << texplanation.getNode() << std::endl; + Debug("theory::explain") + << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " + << texplanation.getNode() << std::endl; } else { - texplanation = - theoryOf(toExplain.d_theory)->explain(toExplain.d_node); - Debug("theory::explain") << "\tTerm was propagated by owner theory: " - << theoryOf(toExplain.d_theory)->getId() - << ". Explanation: " << texplanation.getNode() << std::endl; + texplanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); + Debug("theory::explain") + << "\tTerm was propagated by owner theory: " + << theoryOf(toExplain.d_theory)->getId() + << ". Explanation: " << texplanation.getNode() << std::endl; } Node explanation = texplanation.getNode(); @@ -2140,11 +2157,10 @@ theory::TrustNode TheoryEngine::getExplanation(std::vector& expl } } }); - - + Node exp = mkExplanation(explanationVector); // FIXME - return theory::TrustNode::mkTrustLemma(exp,nullptr); + return theory::TrustNode::mkTrustLemma(exp, nullptr); } void TheoryEngine::setUserAttribute(const std::string& attr, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 77f597845..edd2a1a12 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -45,13 +45,13 @@ #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" #include "theory/theory.h" +#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" -#include "theory/trust_node.h" namespace CVC4 { @@ -157,7 +157,7 @@ class TheoryEngine { */ std::shared_ptr d_lazyProof; //--------------------------------- end new proofs - + /** * The database of shared terms. */ @@ -515,9 +515,11 @@ class TheoryEngine { * theory that sent the literal. The lemmaProofRecipe will contain a list * of the explanation steps required to produce the original node. */ - theory::TrustNode getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); + theory::TrustNode getExplanation( + std::vector& explanationVector, + LemmaProofRecipe* lemmaProofRecipe); -public: + public: /** * Signal the start of a new round of assertion preprocessing @@ -642,7 +644,8 @@ public: * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - theory::TrustNode getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); + theory::TrustNode getExplanationAndRecipe(TNode node, + LemmaProofRecipe* proofRecipe); /** * collect model info diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index 42783d31f..49529aa2f 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -97,7 +97,8 @@ class EqProof CDProof* p, std::unordered_set& assumptions) const; - bool buildTransitivityChain(Node conclusion, std::vector& premises) const; + bool buildTransitivityChain(Node conclusion, + std::vector& premises) const; // returns whether it did reordering void maybeAddSymmOrTrueIntroToProof(unsigned i, diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 504f43d72..ae7477480 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -456,7 +456,11 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { +bool EqualityEngine::assertPredicate(TNode t, + bool polarity, + TNode reason, + unsigned pid) +{ Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead"; TNode b = polarity ? d_true : d_false; @@ -469,7 +473,11 @@ bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig return true; } -bool EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { +bool EqualityEngine::assertEquality(TNode eq, + bool polarity, + TNode reason, + unsigned pid) +{ Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything -- cgit v1.2.3 From c73da9dbc8f320443ae3fa350f328bd290494455 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 May 2020 10:50:13 -0500 Subject: Clarifying trust node interface, working on TheoryEngine --- src/theory/eager_proof_generator.cpp | 6 ++-- src/theory/proof_engine_output_channel.cpp | 6 ++-- src/theory/shared_terms_database.cpp | 13 +++---- src/theory/shared_terms_database.h | 5 +-- src/theory/strings/core_solver.cpp | 4 +-- src/theory/theory_engine.cpp | 52 +++++++++++++++++++-------- src/theory/theory_engine.h | 3 ++ src/theory/trust_node.cpp | 57 ++++++++++++------------------ src/theory/trust_node.h | 44 ++++++++++++++++------- 9 files changed, 110 insertions(+), 80 deletions(-) diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index c2080f20e..1b8d4ceb0 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -30,7 +30,7 @@ void EagerProofGenerator::setProofForConflict(Node conf, std::shared_ptr pf) { // Normalize based on key - Node ckey = TrustNode::getConflictKeyValue(conf); + Node ckey = TrustNode::getConflictProven(conf); d_proofs[ckey] = pf; } @@ -38,7 +38,7 @@ void EagerProofGenerator::setProofForLemma(Node lem, std::shared_ptr pf) { // Normalize based on key - Node lkey = TrustNode::getLemmaKeyValue(lem); + Node lkey = TrustNode::getLemmaProven(lem); d_proofs[lkey] = pf; } @@ -47,7 +47,7 @@ void EagerProofGenerator::setProofForPropExp(TNode lit, std::shared_ptr pf) { // Normalize based on key - Node pekey = TrustNode::getPropExpKeyValue(lit, exp); + Node pekey = TrustNode::getPropExpProven(lit, exp); d_proofs[pekey] = pf; } diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp index 4f35a7639..20dbd4ef0 100644 --- a/src/theory/proof_engine_output_channel.cpp +++ b/src/theory/proof_engine_output_channel.cpp @@ -33,7 +33,7 @@ void ProofEngineOutputChannel::trustedConflict(TrustNode pconf) Node conf = pconf.getNode(); if (d_lazyPf != nullptr) { - Node ckey = TrustNode::getConflictKeyValue(conf); + Node ckey = pconf.getProven(); ProofGenerator* pfg = pconf.getGenerator(); // may or may not have supplied a generator if (pfg != nullptr) @@ -60,10 +60,10 @@ LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem, { Assert(plem.getKind() == TrustNodeKind::LEMMA); TNode lem = plem.getNode(); - ProofGenerator* pfg = plem.getGenerator(); if (d_lazyPf != nullptr) { - Node lkey = TrustNode::getLemmaKeyValue(lem); + Node lkey = plem.getProven(); + ProofGenerator* pfg = plem.getGenerator(); // may or may not have supplied a generator if (pfg != nullptr) { diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 735f0703c..b34742876 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -201,12 +201,12 @@ bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { } } -void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) +void SharedTermsDatabase::assertLiteral(TNode lit) { - Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; + Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertLiteral(" << lit << ")" << endl; // Add it to the equality engine // d_equalityEngine.assertEquality(equality, polarity, reason); - d_pfee.assertAssume(reason); + d_pfee.assertAssume(lit); // Check for conflict checkForConflict(); } @@ -229,12 +229,7 @@ void SharedTermsDatabase::checkForConflict() { conflict = conflict.notNode(); } TrustNode trnc = d_pfee.assertConflict(conflict); - if (d_lazyPf != nullptr) - { - // add the step to the proof - Node ckey = TrustNode::getConflictKeyValue(trnc.getNode()); - d_lazyPf->addLazyStep(ckey, &d_pfee); - } + d_theoryEngine->processTrustNode(trnc); d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 9bd00962f..a6e198d3c 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -167,9 +167,10 @@ class SharedTermsDatabase : public context::ContextNotifyObj { ~SharedTermsDatabase(); /** - * Asserts the equality to the shared terms database, + * Asserts the literal lit to the shared terms database, where lit is + * an equality or disequality. */ - void assertEquality(TNode equality, bool polarity, TNode reason); + void assertLiteral(TNode lit); /** * Return whether the equality is alreday known to the engine diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 87d861cf2..e5411c296 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1012,14 +1012,14 @@ void CoreSolver::getNormalForms(Node eqc, if (!StringsEntail::canConstantContainList(c, nf.d_nf, firstc, lastc)) { Node n = nf.d_base; + std::vector< Node > exp; //conflict Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl; //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] ) - std::vector< Node > exp; - d_bsolver.explainConstantEqc(n,eqc,exp); // Notice although not implemented, this can be minimized based on // firstc/lastc, normal_forms_exp_depend. exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end()); + d_bsolver.explainConstantEqc(n,eqc,exp); Node conc = d_false; d_im.sendInference(exp, conc, Inference::N_NCTN); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 789bc8cb1..eba1c5594 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -131,7 +131,7 @@ std::string getTheoryString(theory::TheoryId id) void TheoryEngine::finishInit() { // if we are using the new proofs module - if (options::proofNew()) + if (d_lazyProof!=nullptr) { // ask the theories to populate the proof checking rules in the checker for (TheoryId theoryId = theory::THEORY_FIRST; @@ -641,7 +641,16 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), + Node split = equality.orNode(equality.notNode()); + if (d_lazyProof!=nullptr) + { + std::vector pfChildren; + std::vector pfArgs; + pfArgs.push_back(equality); + d_lazyProof->addStep(split, PfRule::SPLIT, pfChildren, pfArgs); + } + + lemma(split, RULE_INVALID, false, false, @@ -1209,18 +1218,12 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - // Polarity of the assertion - bool polarity = assertion.getKind() != kind::NOT; - - // Atom of the assertion - TNode atom = polarity ? assertion : assertion[0]; - // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(atom.getKind() == kind::EQUAL) - << "atom should be an EQUALity, not `" << atom << "'"; + Assert(assertion.getKind() == kind::EQUAL || (assertion.getKind()==kind::NOT && assertion[0].getKind()==kind::EQUAL)) + << "atom should be an EQUALity, not `" << assertion << "'"; if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { - d_sharedTerms.assertEquality(atom, polarity, assertion); + d_sharedTerms.assertLiteral(assertion); } return; } @@ -1261,7 +1264,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - Assert(atom.getKind() == kind::EQUAL); + Assert(assertion.getKind() == kind::EQUAL || (assertion.getKind()==kind::NOT && assertion[0].getKind()==kind::EQUAL)); // Normalize Node normalizedLiteral = Rewriter::rewrite(assertion); @@ -1770,8 +1773,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, << CheckSatCommand(n.toExpr()); } - // if proofNew is enabled, then d_lazyProof contains a proof of n. - if (options::proofNew()) + // if d_lazyProof is enabled, then d_lazyProof contains a proof of n. + if (d_lazyProof!=nullptr) { Node lemma = node; if (negated) @@ -1844,12 +1847,31 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } +void TheoryEngine::processTrustNode(theory::TrustNode trn) +{ + if (d_lazyProof==nullptr) + { + // proofs not enabled + return; + } + ProofGenerator* pfg = trn.getGenerator(); + // may or may not have supplied a generator + if (pfg != nullptr) + { + Node p = trn.getProven(); + // if we have, add it to the lazy proof object + d_lazyProof->addLazyStep(p, pfg); + // generator should have a proof for p + Assert(pfg->hasProofFor(p)); + } +} + void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; // if proofNew is enabled, then d_lazyProof contains a proof of // conflict.negate() - // Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) || + // Assert (d_lazyProof==nullptr || d_lazyProof->hasStep(conflict.negate()) || // d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH); Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index edd2a1a12..4039e7343 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -360,6 +360,9 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo); + + /** Process trust node */ + void processTrustNode(theory::TrustNode trn); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 4c6246888..3239c543a 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -39,22 +39,25 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk) TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g) { + Node ckey = getConflictProven(conf); // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(getConflictKeyValue(conf))); - return TrustNode(TrustNodeKind::CONFLICT, conf, g); + Assert(g == nullptr || g->hasProofFor(ckey)); + return TrustNode(TrustNodeKind::CONFLICT, ckey, g); } TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g) { + Node lkey = getLemmaProven(lem); // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(getLemmaKeyValue(lem))); - return TrustNode(TrustNodeKind::LEMMA, lem, g); + Assert(g == nullptr || g->hasProofFor(lkey)); + return TrustNode(TrustNodeKind::LEMMA, lkey, g); } TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g) { - Assert(g == nullptr || g->hasProofFor(getPropExpKeyValue(lit, exp))); - return TrustNode(TrustNodeKind::PROP_EXP, exp, g); + Node pekey = getPropExpProven(lit, exp); + Assert(g == nullptr || g->hasProofFor(pekey)); + return TrustNode(TrustNodeKind::PROP_EXP, pekey, g); } TrustNode TrustNode::null() @@ -62,50 +65,36 @@ TrustNode TrustNode::null() return TrustNode(TrustNodeKind::INVALID, Node::null()); } -TrustNode::TrustNode(TrustNodeKind tnk, Node n, ProofGenerator* g) - : d_tnk(tnk), d_node(n), d_gen(g) +TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) + : d_tnk(tnk), d_proven(p), d_gen(g) { // does not make sense to provide null node with generator - Assert(!d_node.isNull() || d_gen == nullptr); + Assert(!d_proven.isNull() || d_gen == nullptr); } TrustNodeKind TrustNode::getKind() const { return d_tnk; } -Node TrustNode::getNode() const { return d_node; } +Node TrustNode::getNode() const { + return d_tnk==TrustNodeKind::LEMMA ? d_proven : d_proven[0]; +} +Node TrustNode::getProven() const { + return d_proven; + +} ProofGenerator* TrustNode::getGenerator() const { return d_gen; } -bool TrustNode::isNull() const { return d_node.isNull(); } +bool TrustNode::isNull() const { return d_proven.isNull(); } -Node TrustNode::getConflictKeyValue(Node conf) { return conf.negate(); } +Node TrustNode::getConflictProven(Node conf) { return conf.negate(); } -Node TrustNode::getLemmaKeyValue(Node lem) { return lem; } +Node TrustNode::getLemmaProven(Node lem) { return lem; } -Node TrustNode::getPropExpKeyValue(TNode lit, Node exp) +Node TrustNode::getPropExpProven(TNode lit, Node exp) { - if (exp.isConst()) - { - Assert(exp.getConst()); - return lit; - } return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit); } -Node TrustNode::getKeyValue(TrustNodeKind tnk, Node exp, Node conc) -{ - if (conc.isConst()) - { - Assert(!conc.getConst()); - return exp.negate(); - } - if (exp.isConst()) - { - Assert(exp.getConst()); - return conc; - } - return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); -} - std::ostream& operator<<(std::ostream& out, TrustNode n) { out << "(trust " << n.getNode() << ")"; diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index 3ced7efe9..2bf1f770f 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -87,28 +87,48 @@ class TrustNode ~TrustNode() {} /** get kind */ TrustNodeKind getKind() const; - /** get node */ + /** get node + * + * This is the node that is used in a common interface, either: + * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict, + * (2) A valid T-formula lem to pass to OutputChannel::lemma, or + * (3) A conjunction of literals exp to return in Theory::explain(lit). + * + * Notice that this node does not necessarily correspond to a valid formula. + * The call getProven() below retrieves a valid formula corresponding to + * the above calls. + */ Node getNode() const; + /** get proven + * + * This is the corresponding formula that is proven by the proof generator + * for the above cases: + * (1) (not conf), for conflicts, + * (2) lem, for lemmas, + * (3) (=> exp lit), for propagations from explanations. + * + * When constructing this trust node, the proof generator should be able to + * provide a proof for this fact. + */ + Node getProven() const; /** get generator */ ProofGenerator* getGenerator() const; /** is null? */ bool isNull() const; - /** Get the node key for which conflict calls are cached */ - static Node getConflictKeyValue(Node conf); - /** Get the node key for which lemma calls are cached */ - static Node getLemmaKeyValue(Node lem); - /** Get the node key for which explanations for propagations are cached */ - static Node getPropExpKeyValue(TNode lit, Node exp); - /** Get the node key for the exp => conc */ - static Node getKeyValue(TrustNodeKind tnk, Node exp, Node conc); + /** Get the proven formula corresponding to a conflict call */ + static Node getConflictProven(Node conf); + /** Get the proven formula corresponding to a lemma call */ + static Node getLemmaProven(Node lem); + /** Get the proven formula corresponding to explanations for propagation*/ + static Node getPropExpProven(TNode lit, Node exp); private: - TrustNode(TrustNodeKind tnk, Node n, ProofGenerator* g = nullptr); + TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr); /** The kind */ TrustNodeKind d_tnk; - /** The node */ - Node d_node; + /** The proven node */ + Node d_proven; /** The generator */ ProofGenerator* d_gen; }; -- cgit v1.2.3 From 6d8b0c1ab090df93101b5c7fb350b469f7537419 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 May 2020 12:24:02 -0500 Subject: More --- src/theory/theory_engine.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index eba1c5594..955745783 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1606,7 +1606,8 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( proofRecipe->addStep(proofStep); } }); - + // it came directly from the theory, it is ready to be processed + processTrustNode(texplanation); return texplanation; } @@ -1636,16 +1637,16 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( } TrustNode texplanation = getExplanation(vec, proofRecipe); - Node explanation = texplanation.getNode(); - - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; + // the trust node was processed within getExplanation return texplanation; } theory::TrustNode TheoryEngine::getExplanation(TNode node) { LemmaProofRecipe *dontCareRecipe = NULL; + // the trust node was processed within getExplanationAndRecipe return getExplanationAndRecipe(node, dontCareRecipe); } @@ -1911,6 +1912,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Process the explanation TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); + + // TODO: convert proof here? + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); -- cgit v1.2.3 From ff08fb79edda20c4374d2757d52cff9552f4013a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 May 2020 12:24:20 -0500 Subject: Format --- src/theory/shared_terms_database.cpp | 3 ++- src/theory/strings/core_solver.cpp | 4 ++-- src/theory/theory_engine.cpp | 34 +++++++++++++++++----------------- src/theory/theory_engine.h | 3 +-- src/theory/trust_node.cpp | 10 ++++------ src/theory/trust_node.h | 8 ++++---- 6 files changed, 30 insertions(+), 32 deletions(-) diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index b34742876..723e20a16 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -203,7 +203,8 @@ bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { void SharedTermsDatabase::assertLiteral(TNode lit) { - Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertLiteral(" << lit << ")" << endl; + Debug("shared-terms-database::assert") + << "SharedTermsDatabase::assertLiteral(" << lit << ")" << endl; // Add it to the equality engine // d_equalityEngine.assertEquality(equality, polarity, reason); d_pfee.assertAssume(lit); diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index e5411c296..27e2520b8 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1012,14 +1012,14 @@ void CoreSolver::getNormalForms(Node eqc, if (!StringsEntail::canConstantContainList(c, nf.d_nf, firstc, lastc)) { Node n = nf.d_base; - std::vector< Node > exp; + std::vector exp; //conflict Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl; //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] ) // Notice although not implemented, this can be minimized based on // firstc/lastc, normal_forms_exp_depend. exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end()); - d_bsolver.explainConstantEqc(n,eqc,exp); + d_bsolver.explainConstantEqc(n, eqc, exp); Node conc = d_false; d_im.sendInference(exp, conc, Inference::N_NCTN); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 955745783..d3b0611c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -131,7 +131,7 @@ std::string getTheoryString(theory::TheoryId id) void TheoryEngine::finishInit() { // if we are using the new proofs module - if (d_lazyProof!=nullptr) + if (d_lazyProof != nullptr) { // ask the theories to populate the proof checking rules in the checker for (TheoryId theoryId = theory::THEORY_FIRST; @@ -642,20 +642,15 @@ void TheoryEngine::combineTheories() { Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; Node split = equality.orNode(equality.notNode()); - if (d_lazyProof!=nullptr) + if (d_lazyProof != nullptr) { std::vector pfChildren; std::vector pfArgs; pfArgs.push_back(equality); d_lazyProof->addStep(split, PfRule::SPLIT, pfChildren, pfArgs); } - - lemma(split, - RULE_INVALID, - false, - false, - false, - carePair.d_theory); + + lemma(split, RULE_INVALID, false, false, false, carePair.d_theory); // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark @@ -1220,7 +1215,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(assertion.getKind() == kind::EQUAL || (assertion.getKind()==kind::NOT && assertion[0].getKind()==kind::EQUAL)) + Assert(assertion.getKind() == kind::EQUAL + || (assertion.getKind() == kind::NOT + && assertion[0].getKind() == kind::EQUAL)) << "atom should be an EQUALity, not `" << assertion << "'"; if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { d_sharedTerms.assertLiteral(assertion); @@ -1264,7 +1261,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - Assert(assertion.getKind() == kind::EQUAL || (assertion.getKind()==kind::NOT && assertion[0].getKind()==kind::EQUAL)); + Assert(assertion.getKind() == kind::EQUAL + || (assertion.getKind() == kind::NOT + && assertion[0].getKind() == kind::EQUAL)); // Normalize Node normalizedLiteral = Rewriter::rewrite(assertion); @@ -1638,7 +1637,8 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( TrustNode texplanation = getExplanation(vec, proofRecipe); - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " + << texplanation.getNode() << endl; // the trust node was processed within getExplanation return texplanation; } @@ -1775,7 +1775,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // if d_lazyProof is enabled, then d_lazyProof contains a proof of n. - if (d_lazyProof!=nullptr) + if (d_lazyProof != nullptr) { Node lemma = node; if (negated) @@ -1850,7 +1850,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, void TheoryEngine::processTrustNode(theory::TrustNode trn) { - if (d_lazyProof==nullptr) + if (d_lazyProof == nullptr) { // proofs not enabled return; @@ -1866,7 +1866,7 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn) Assert(pfg->hasProofFor(p)); } } - + void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; @@ -1912,9 +1912,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Process the explanation TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); - + // TODO: convert proof here? - + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4039e7343..c3759ca52 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -360,7 +360,7 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo); - + /** Process trust node */ void processTrustNode(theory::TrustNode trn); @@ -523,7 +523,6 @@ class TheoryEngine { LemmaProofRecipe* lemmaProofRecipe); public: - /** * Signal the start of a new round of assertion preprocessing */ diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 3239c543a..62213aade 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -74,14 +74,12 @@ TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) TrustNodeKind TrustNode::getKind() const { return d_tnk; } -Node TrustNode::getNode() const { - return d_tnk==TrustNodeKind::LEMMA ? d_proven : d_proven[0]; +Node TrustNode::getNode() const +{ + return d_tnk == TrustNodeKind::LEMMA ? d_proven : d_proven[0]; } -Node TrustNode::getProven() const { - return d_proven; - -} +Node TrustNode::getProven() const { return d_proven; } ProofGenerator* TrustNode::getGenerator() const { return d_gen; } bool TrustNode::isNull() const { return d_proven.isNull(); } diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index 2bf1f770f..8d3548bd5 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -88,25 +88,25 @@ class TrustNode /** get kind */ TrustNodeKind getKind() const; /** get node - * + * * This is the node that is used in a common interface, either: * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict, * (2) A valid T-formula lem to pass to OutputChannel::lemma, or * (3) A conjunction of literals exp to return in Theory::explain(lit). - * + * * Notice that this node does not necessarily correspond to a valid formula. * The call getProven() below retrieves a valid formula corresponding to * the above calls. */ Node getNode() const; /** get proven - * + * * This is the corresponding formula that is proven by the proof generator * for the above cases: * (1) (not conf), for conflicts, * (2) lem, for lemmas, * (3) (=> exp lit), for propagations from explanations. - * + * * When constructing this trust node, the proof generator should be able to * provide a proof for this fact. */ -- cgit v1.2.3 From 3b662c0aa0d035248ee805a87a6d54990c05795f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 16 May 2020 14:04:16 -0500 Subject: Comments sketching --- src/theory/theory_engine.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d3b0611c0..90f852f03 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1913,7 +1913,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); - // TODO: convert proof here? + // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln + // Prove ~( E1 ^ ... ^ En ) + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; @@ -2019,6 +2021,7 @@ theory::TrustNode TheoryEngine::getExplanation( } }); + std::vector trNodes; while (i < explanationVector.size()) { // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; @@ -2117,6 +2120,12 @@ theory::TrustNode TheoryEngine::getExplanation( << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << texplanation.getNode() << std::endl; } + // process the trust node here + if (d_lazyProof!=nullptr) + { + processTrustNode(texplanation); + trNodes.push_back(texplanation); + } Node explanation = texplanation.getNode(); Debug("theory::explain") @@ -2185,7 +2194,14 @@ theory::TrustNode TheoryEngine::getExplanation( }); Node exp = mkExplanation(explanationVector); - // FIXME + + if (d_lazyProof!=nullptr) + { + // FIXME + // We have E1 => l1 ^ ... En => ln. + // Need to prove E1 ^ ... ^ En => ( l1 ^ ... ^ ln ) + } + return theory::TrustNode::mkTrustLemma(exp, nullptr); } -- cgit v1.2.3 From d31d5deb2eeca185cf041ffa980f54168601cf19 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 09:41:58 -0500 Subject: Configurable substitution, working on TheoryEngine. --- src/expr/proof_node_manager.cpp | 98 ++++++++++++++++ src/expr/proof_node_manager.h | 6 + src/theory/builtin/proof_checker.cpp | 201 +++++++++++++++++++------------- src/theory/builtin/proof_checker.h | 47 +++++--- src/theory/builtin/proof_kinds | 4 +- src/theory/strings/infer_proof_cons.cpp | 48 +++++--- src/theory/strings/infer_proof_cons.h | 13 ++- src/theory/theory_engine.cpp | 81 ++++++++++--- src/theory/uf/proof_equality_engine.cpp | 6 +- 9 files changed, 361 insertions(+), 143 deletions(-) diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index f15e43553..d9a2d1711 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -60,6 +60,104 @@ std::shared_ptr ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, children, args, fact); } +std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr pf, + std::vector& assumps, + bool ensureClosed) +{ + std::vector> pfChildren; + pfChildren.push_back(pf); + if (!ensureClosed) + { + return mkNode(PfRule::SCOPE, pfChildren, assumps); + } + Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl; + // we first ensure the assumptions are flattened + std::unordered_set ac; + for (const TNode& a : assumps) + { + if (a.getKind() == AND) + { + ac.insert(a.begin(), a.end()); + } + else + { + ac.insert(a); + } + } + // The free assumptions of the proof + std::map> famap; + pf->getFreeAssumptionsMap(famap); + std::unordered_set acu; + std::unordered_set::iterator itf; + for (const std::pair>& fa : famap) + { + Node a = fa.first; + if (ac.find(a) != ac.end()) + { + // already covered by an assumption + acu.insert(a); + continue; + } + // otherwise it may be due to symmetry? + bool polarity = a.getKind() != NOT; + Node aeq = polarity ? a : a[0]; + if (aeq.getKind() == EQUAL) + { + Node aeqSym = aeq[1].eqNode(aeq[0]); + aeqSym = polarity ? aeqSym : aeqSym.notNode(); + itf = ac.find(aeqSym); + if (itf != ac.end()) + { + Trace("pnm-scope") + << "- reorient assumption " << aeqSym << " via " << a << " for " + << fa.second.size() << " proof nodes" << std::endl; + std::shared_ptr pfaa = mkAssume(aeqSym); + for (ProofNode* pfs : fa.second) + { + Assert(pfs->getResult() == a); + // must correct the orientation on this leaf + std::vector> children; + children.push_back(pfaa); + std::vector args; + args.push_back(a); + updateNode( + pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(aeqSym); + continue; + } + } + // All free assumptions should be arguments to SCOPE. + std::stringstream ss; + pf->printDebug(ss); + ss << std::endl << "Free assumption: " << a << std::endl; + for (const Node& aprint : ac) + { + ss << "- assumption: " << aprint << std::endl; + } + AlwaysAssert(false) + << "Generated a proof that is not closed by the scope: " << ss.str() + << std::endl; + } + if (acu.size() < ac.size()) + { + // All assumptions should match a free assumption; if one does not, then + // the explanation could have been smaller. + for (const Node& a : ac) + { + if (acu.find(a) == acu.end()) + { + Notice() << "ProofNodeManager::mkScope: assumption " << a + << " does not match a free assumption in proof" << std::endl; + } + } + } + assumps.clear(); + assumps.insert(assumps.end(), acu.begin(), acu.end()); + return mkNode(PfRule::SCOPE, pfChildren, assumps); +} + bool ProofNodeManager::updateNode( ProofNode* pn, PfRule id, diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 9904a78ec..7cf6574cb 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -80,6 +80,12 @@ class ProofNodeManager Node expected = Node::null()); /** Make assume */ std::shared_ptr mkAssume(Node fact); + /** Make scope */ + std::shared_ptr mkScope(std::shared_ptr pf, + std::vector& assumps, + bool ensureClosed = true + ); + /** * This method updates pn to be a proof of the form ( children, args ), * while maintaining its d_proven field. This method returns false if this diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index ddc222ffb..b57bb112b 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -22,23 +22,30 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -const char* toString(RewriterId id) +const char* toString(MethodId id) { switch (id) { - case RewriterId::REWRITE: return "REWRITE"; - case RewriterId::REWRITE_EQ_EXT: return "REWRITE_EQ_EXT"; - case RewriterId::IDENTITY: return "IDENTITY"; - default: return "RewriterId::Unknown"; + case MethodId::RW_REWRITE: return "RW_REWRITE"; + case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT"; + case MethodId::RW_IDENTITY: return "RW_IDENTITY"; + case MethodId::SB_DEFAULT: return "SB_DEFAULT"; + case MethodId::SB_PREDICATE: return "SB_PREDICATE"; + default: return "MethodId::Unknown"; }; } -std::ostream& operator<<(std::ostream& out, RewriterId id) +std::ostream& operator<<(std::ostream& out, MethodId id) { out << toString(id); return out; } +Node mkMethodId(MethodId id) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast(id))); +} + namespace builtin { void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) @@ -55,109 +62,128 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::THEORY_LEMMA, nullptr); } -Node BuiltinProofRuleChecker::applyRewrite(Node n, RewriterId id) +Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) { Node nk = ProofSkolemCache::getSkolemForm(n); - Node nkr = applyRewriteExternal(n, id); + Node nkr = applyRewriteExternal(n, idr); return ProofSkolemCache::getWitnessForm(nkr); } -Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp) +Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) { if (exp.isNull() || exp.getKind() != EQUAL) { return Node::null(); } Node nk = ProofSkolemCache::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp); + Node nks = applySubstitutionExternal(nk, exp, ids); return ProofSkolemCache::getWitnessForm(nks); } Node BuiltinProofRuleChecker::applySubstitution(Node n, - const std::vector& exp) + const std::vector& exp, MethodId ids) { Node nk = ProofSkolemCache::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp); + Node nks = applySubstitutionExternal(nk, exp, ids); return ProofSkolemCache::getWitnessForm(nks); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( - Node n, const std::vector& exp, RewriterId id) + Node n, const std::vector& exp, MethodId ids, MethodId idr) { Node nk = ProofSkolemCache::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp); - Node nksr = applyRewriteExternal(nks, id); + Node nks = applySubstitutionExternal(nk, exp, ids); + Node nksr = applyRewriteExternal(nks, idr); return ProofSkolemCache::getWitnessForm(nksr); } -Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, RewriterId id) +Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) { Trace("builtin-pfcheck-debug") - << "applyRewriteExternal (" << id << "): " << n << std::endl; + << "applyRewriteExternal (" << idr << "): " << n << std::endl; // index determines the kind of rewriter - if (id == RewriterId::REWRITE) + if (idr == MethodId::RW_REWRITE) { return Rewriter::rewrite(n); } - else if (id == RewriterId::REWRITE_EQ_EXT) + else if (idr == MethodId::RW_REWRITE_EQ_EXT) { Node ret = Rewriter::rewriteEqualityExt(n); // also rewrite return Rewriter::rewrite(ret); } - else if (id == RewriterId::IDENTITY) + else if (idr == MethodId::RW_IDENTITY) { // does nothing return n; } // unknown rewriter Assert(false) - << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " << id + << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " << idr << std::endl; return n; } -Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, Node exp) +Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, Node exp, MethodId ids) { - Assert(!exp.isNull() && exp.getKind() == EQUAL); + Assert(!exp.isNull()); Node expk = ProofSkolemCache::getSkolemForm(exp); - TNode var = expk[0]; - TNode subs = expk[1]; + TNode var, subs; + if (ids==MethodId::SB_DEFAULT) + { + if (expk.getKind()!=EQUAL) + { + return Node::null(); + } + var = expk[0]; + subs = expk[1]; + } + else if (ids==MethodId::SB_PREDICATE) + { + bool polarity = expk.getKind()!=NOT; + var = polarity ? expk : expk[0]; + subs = NodeManager::currentNM()->mkConst(polarity); + } + else + { + Assert(false) + << "BuiltinProofRuleChecker::applySubstitutionExternal: no substitution for " << ids + << std::endl; + } return n.substitute(var, subs); } Node BuiltinProofRuleChecker::applySubstitutionExternal( - Node n, const std::vector& exp) + Node n, const std::vector& exp, MethodId ids) { Node curr = n; // apply substitution one at a time, in reverse order for (size_t i = 0, nexp = exp.size(); i < nexp; i++) { - if (exp[nexp - 1 - i].isNull() || exp[nexp - 1 - i].getKind() != EQUAL) + if (exp[nexp - 1 - i].isNull()) { return Node::null(); } - curr = applySubstitutionExternal(curr, exp[nexp - 1 - i]); + curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids); + if (curr.isNull()) + { + break; + } } return curr; } -bool BuiltinProofRuleChecker::getRewriterId(TNode n, RewriterId& i) +bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i) { uint32_t index; if (!getIndex(n, index)) { return false; } - i = static_cast(index); + i = static_cast(index); return true; } -Node BuiltinProofRuleChecker::mkRewriterId(RewriterId i) -{ - return NodeManager::currentNM()->mkConst(Rational(static_cast(i))); -} - Node BuiltinProofRuleChecker::checkInternal(PfRule id, const std::vector& children, const std::vector& args) @@ -189,7 +215,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::SUBS) { Assert(children.size() > 0); - Assert(args.size() == 1); + Assert(1 <= args.size() && args.size() <= 2); + MethodId ids = MethodId::SB_DEFAULT; + if (args.size()==2 && !getMethodId(args[1], ids)) + { + return Node::null(); + } std::vector exp; for (size_t i = 0, nchild = children.size(); i < nchild; i++) { @@ -201,7 +232,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::REWRITE) { Assert(children.empty()); - Assert(args.size() == 1); + Assert(1 <= args.size() && args.size() <= 2); + MethodId ids = MethodId::RW_REWRITE; + if (args.size()==2 && !getMethodId(args[1], ids)) + { + return Node::null(); + } Node res = applyRewrite(args[0]); return args[0].eqNode(res); } @@ -211,18 +247,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, // (TRANS // (SUBS P1 ... Pn t) // (REWRITE )) - Assert(1 <= args.size() && args.size() <= 2); - RewriterId idRewriter = RewriterId::REWRITE; - if (args.size() >= 2) + Assert(1 <= args.size() && args.size() <= 3); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) { - if (!getRewriterId(args[1], idRewriter)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[1] << std::endl; - return Node::null(); - } + return Node::null(); } - Node res = applySubstitutionRewrite(args[0], children, idRewriter); + Node res = applySubstitutionRewrite(args[0], children, idr); return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_PRED_INTRO) @@ -232,18 +263,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, // NOTE: technically a macro: // (TRUE_ELIM // (MACRO_SR_EQ_INTRO [0])) - Assert(1 <= args.size() && args.size() <= 2); - RewriterId idRewriter = RewriterId::REWRITE; - if (args.size() >= 2) + Assert(1 <= args.size() && args.size() <= 3); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) { - if (!getRewriterId(args[1], idRewriter)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[1] << std::endl; - return Node::null(); - } + return Node::null(); } - Node res = applySubstitutionRewrite(args[0], children, idRewriter); + Node res = applySubstitutionRewrite(args[0], children, ids, idr); if (res.isNull()) { return Node::null(); @@ -264,7 +290,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " << args.size() << std::endl; Assert(children.size() >= 1); - Assert(args.size() <= 1); + Assert(args.size() <= 2); // NOTE: technically a macro: // (TRUE_ELIM // (TRANS @@ -272,17 +298,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, // (TRUE_INTRO [0]))) std::vector exp; exp.insert(exp.end(), children.begin() + 1, children.end()); - RewriterId idRewriter = RewriterId::REWRITE; - if (0 < args.size()) + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 0)) { - if (!getRewriterId(args[0], idRewriter)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[0] << std::endl; - return Node::null(); - } + return Node::null(); } - Node res1 = applySubstitutionRewrite(children[0], exp, idRewriter); + Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr); Trace("builtin-pfcheck") << "Returned " << res1 << std::endl; return res1; } @@ -291,24 +312,19 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " << args.size() << std::endl; Assert(children.size() >= 1); - Assert(args.size() <= 2); + Assert(1 <= args.size() && args.size() <= 3); Assert(args[0].getType().isBoolean()); - std::vector exp; - exp.insert(exp.end(), children.begin() + 1, children.end()); - RewriterId idRewriter = RewriterId::REWRITE; - if (1 < args.size()) + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) { - if (!getRewriterId(args[1], idRewriter)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[1] << std::endl; - return Node::null(); - } + return Node::null(); } - Node res1 = applySubstitutionRewrite(children[0], exp, idRewriter); + std::vector exp; + exp.insert(exp.end(), children.begin() + 1, children.end()); + Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr); // Trace("builtin-pfcheck") // << "Returned " << res1 << std::endl; - Node res2 = applySubstitutionRewrite(args[0], exp, idRewriter); + Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr); // Trace("builtin-pfcheck") // << "Returned " << res2 << " from " << args[0] << std::endl; // can rewrite the witness forms @@ -334,6 +350,31 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } +bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, MethodId& ids, MethodId& idr, size_t index) +{ + ids = MethodId::SB_DEFAULT; + idr = MethodId::RW_REWRITE; + if (args.size() > index) + { + if (!getMethodId(args[index], ids)) + { + Trace("builtin-pfcheck") + << "Failed to get id from " << args[index] << std::endl; + return false; + } + } + if (args.size() >= index+1) + { + if (!getMethodId(args[index+1], idr)) + { + Trace("builtin-pfcheck") + << "Failed to get id from " << args[index+1] << std::endl; + return false; + } + } + return true; +} + } // namespace builtin } // namespace theory } // namespace CVC4 diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 7c6f29354..9291bbf9f 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -24,26 +24,36 @@ namespace CVC4 { namespace theory { -/** Identifiers for rewriters. +/** Identifiers for rewriters and substitutions. * * A "rewriter" is abstractly a method from Node to Node, where the output * is semantically equivalent to the input. The identifiers below list * various methods that have this contract. This identifier is used * in a number of the builtin rules. + * + * A substitution is a method for turning a formula into */ -enum class RewriterId : uint32_t +enum class MethodId : uint32_t { + //---------------------------- Rewriters // Rewriter::rewrite(n) - REWRITE, + RW_REWRITE, // Rewriter::rewriteExtEquality(n) - REWRITE_EQ_EXT, + RW_REWRITE_EQ_EXT, // identity - IDENTITY, + RW_IDENTITY, + //---------------------------- Substitutions + // (= x y) is interpreted as x -> y, using Node::substitute(...) + SB_DEFAULT, + // (= x y) is interpreted as (= x y) -> true, using Node::substitute(...) + SB_PREDICATE, }; /** Converts a rewriter id to a string. */ -const char* toString(RewriterId id); +const char* toString(MethodId id); /** Write a rewriter id to out */ -std::ostream& operator<<(std::ostream& out, RewriterId id); +std::ostream& operator<<(std::ostream& out, MethodId id); +/** Make a method id node */ +Node mkMethodId(MethodId id); namespace builtin { @@ -62,7 +72,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * @param id The identifier of the rewriter. * @return The rewritten form of n. */ - static Node applyRewrite(Node n, RewriterId id = RewriterId::REWRITE); + static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** * Apply substitution on n (in witness form). This encapsulates the exact * behavior of a SUBS step in a proof. Substitution is on the Skolem form of @@ -73,8 +83,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * substitution * @return The substituted form of n. */ - static Node applySubstitution(Node n, Node exp); - static Node applySubstitution(Node n, const std::vector& exp); + static Node applySubstitution(Node n, Node exp, + MethodId ids = MethodId::SB_DEFAULT); + static Node applySubstitution(Node n, const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT); /** Apply substitution + rewriting * * Combines the above two steps. @@ -87,11 +99,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ static Node applySubstitutionRewrite(Node n, const std::vector& exp, - RewriterId id = RewriterId::REWRITE); + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); /** get a rewriter Id from a node, return false if we fail */ - static bool getRewriterId(TNode n, RewriterId& i); - /** Make a rewriter id node */ - static Node mkRewriterId(RewriterId i); + static bool getMethodId(TNode n, MethodId& i); /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; @@ -101,17 +112,19 @@ class BuiltinProofRuleChecker : public ProofRuleChecker Node checkInternal(PfRule id, const std::vector& children, const std::vector& args) override; + /** get method ids */ + bool getMethodIds(const std::vector& args, MethodId& ids, MethodId& idr, size_t index); /** * Apply rewrite (on Skolem form). id is the identifier of the rewriter. */ - static Node applyRewriteExternal(Node n, RewriterId id = RewriterId::REWRITE); + static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE); /** * Apply substitution for n (on Skolem form), where exp is an equality * (or set of equalities) in Witness form. Returns the result of * n * { exp[0] -> exp[1] } in Skolem form. */ - static Node applySubstitutionExternal(Node n, Node exp); - static Node applySubstitutionExternal(Node n, const std::vector& exp); + static Node applySubstitutionExternal(Node n, Node exp, MethodId ids); + static Node applySubstitutionExternal(Node n, const std::vector& exp, MethodId ids); }; } // namespace builtin diff --git a/src/theory/builtin/proof_kinds b/src/theory/builtin/proof_kinds index 404dfbc06..eb9643ec3 100644 --- a/src/theory/builtin/proof_kinds +++ b/src/theory/builtin/proof_kinds @@ -38,7 +38,7 @@ proofrule SCOPE 1 1: ::CVC4::theory::builtin::BuiltinProofRuleChecker // ======== Substitution // Children: (P1:(= x1 t1), ..., Pn:(= xn tn)) -// Arguments: (t) +// Arguments: (t, id?) // --------------------------------------------------------------- // Conclusion: (= t t.substitute(xn,tn). ... .substitute(x1,t1)) // Notice that the orientation of the premises matters. @@ -46,7 +46,7 @@ proofrule SUBS 1: 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker // ======== Rewrite // Children: none -// Arguments: (t) +// Arguments: (t, id?) // ---------------------------------------- // Conclusion: (= t Rewriter::rewrite(t)) proofrule REWRITE 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 891f23cd2..bad121d65 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -168,8 +168,9 @@ Node InferProofCons::convert(Inference infer, case Inference::INFER_EMP: { // need the "extended equality rewrite" - ps.d_args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId( - RewriterId::REWRITE_EQ_EXT)); + MethodId ids = MethodId::SB_DEFAULT; + MethodId idr = MethodId::RW_REWRITE_EQ_EXT; + addMethodIds(ps.d_args, ids, idr); ps.d_rule = PfRule::MACRO_SR_PRED_ELIM; } break; @@ -306,7 +307,7 @@ Node InferProofCons::convert(Inference infer, // possibly be done by CONCAT_EQ with !isRev. std::vector cexp; if (convertPredTransform( - mainEqCeq, conc, cexp, RewriterId::REWRITE_EQ_EXT)) + mainEqCeq, conc, cexp, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT)) { Trace("strings-ipc-core") << "Transformed to " << conc << " via pred transform" << std::endl; @@ -901,7 +902,8 @@ bool InferProofCons::convertLengthPf(Node lenReq, bool InferProofCons::convertPredTransform(Node src, Node tgt, const std::vector& exp, - RewriterId id) + MethodId ids, + MethodId idr) { // symmetric equalities if (isSymm(src, tgt)) @@ -914,10 +916,7 @@ bool InferProofCons::convertPredTransform(Node src, // try to prove that tgt rewrites to src children.insert(children.end(), exp.begin(), exp.end()); args.push_back(tgt); - if (id != RewriterId::REWRITE) - { - args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id)); - } + addMethodIds(args,ids,idr); Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); if (res.isNull()) { @@ -926,7 +925,7 @@ bool InferProofCons::convertPredTransform(Node src, } Trace("strings-ipc-debug") << "InferProofCons::convertPredTransform: success " << src - << " == " << tgt << " under " << exp << " via " << id << std::endl; + << " == " << tgt << " under " << exp << " via " << ids << "/" << idr << std::endl; // should definitely have concluded tgt Assert(res == tgt); return true; @@ -934,14 +933,12 @@ bool InferProofCons::convertPredTransform(Node src, bool InferProofCons::convertPredIntro(Node tgt, const std::vector& exp, - RewriterId id) + MethodId ids, + MethodId idr) { std::vector args; args.push_back(tgt); - if (id != RewriterId::REWRITE) - { - args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id)); - } + addMethodIds(args,ids,idr); Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); if (res.isNull()) { @@ -953,16 +950,14 @@ bool InferProofCons::convertPredIntro(Node tgt, Node InferProofCons::convertPredElim(Node src, const std::vector& exp, - RewriterId id) + MethodId ids, + MethodId idr) { std::vector children; children.push_back(src); children.insert(children.end(), exp.begin(), exp.end()); std::vector args; - if (id != RewriterId::REWRITE) - { - args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id)); - } + addMethodIds(args,ids,idr); Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); if (isSymm(src, srcRew)) { @@ -972,6 +967,21 @@ Node InferProofCons::convertPredElim(Node src, return srcRew; } +void InferProofCons::addMethodIds(std::vector& args, + MethodId ids, + MethodId idr) +{ + bool ndefRewriter = (idr != MethodId::RW_REWRITE); + if (ids != MethodId::SB_DEFAULT || ndefRewriter) + { + args.push_back(mkMethodId(ids)); + } + if (ndefRewriter) + { + args.push_back(mkMethodId(idr)); + } +} + Node InferProofCons::convertTrans(Node eqa, Node eqb) { if (eqa.getKind() != EQUAL || eqb.getKind() != EQUAL) diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 612e67693..f5bb57996 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -126,17 +126,24 @@ class InferProofCons : public ProofGenerator bool convertPredTransform(Node src, Node tgt, const std::vector& exp, - RewriterId id = RewriterId::REWRITE); + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); /** */ bool convertPredIntro(Node tgt, const std::vector& exp, - RewriterId id = RewriterId::REWRITE); + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); /** */ Node convertPredElim(Node src, const std::vector& exp, - RewriterId id = RewriterId::REWRITE); + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); + /** Add method ids */ + void addMethodIds(std::vector& args, + MethodId ids, + MethodId idr); /** */ Node convertTrans(Node eqa, Node eqb); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 90f852f03..b571fc2b8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2007,8 +2007,15 @@ theory::TrustNode TheoryEngine::getExplanation( std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { - Assert(explanationVector.size() > 0); - + Assert(explanationVector.size() == 1); + + Node conclusion = explanationVector[0].d_node; + std::unique_ptr lcp; + if (d_lazyProof!=nullptr) + { + // FIXME + //lcp.reset(new LazyCDProof(d_pNodeManager.get())); + } unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping @@ -2021,7 +2028,6 @@ theory::TrustNode TheoryEngine::getExplanation( } }); - std::vector trNodes; while (i < explanationVector.size()) { // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; @@ -2032,15 +2038,20 @@ theory::TrustNode TheoryEngine::getExplanation( << toExplain.d_theory << endl; // If a true constant or a negation of a false constant we can ignore it - if (toExplain.d_node.isConst() && toExplain.d_node.getConst()) - { - ++ i; - continue; - } - if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() - && !toExplain.d_node[0].getConst()) + if ((toExplain.d_node.isConst() && toExplain.d_node.getConst()) || + (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst())) { ++ i; + if (lcp!=nullptr) + { + // ------------------MACRO_SR_PRED_INTRO + // toExplain.d_node + std::vector children; + std::vector args; + args.push_back(toExplain.d_node); + lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + } continue; } @@ -2058,12 +2069,27 @@ theory::TrustNode TheoryEngine::getExplanation( Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.d_node << " got from " << toExplain.d_theory << endl; - for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k) + size_t nchild = toExplain.d_node.getNumChildren(); + for (size_t k = 0; k < nchild; ++k) { NodeTheoryPair newExplain( toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } + if (lcp!=nullptr) + { + // toExplain.d_node[0] ... toExplain.d_node[n] + // --------------------------------------------MACRO_BSR_PRED_INTRO + // toExplain.d_node + std::vector children; + for (size_t k = 0; k < nchild; ++k) + { + children.push_back(toExplain.d_node[k]); + } + std::vector args; + args.push_back(toExplain.d_node); + lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + } ++ i; continue; } @@ -2098,7 +2124,7 @@ theory::TrustNode TheoryEngine::getExplanation( } } }) - + // FIXME continue; } } @@ -2120,11 +2146,20 @@ theory::TrustNode TheoryEngine::getExplanation( << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << texplanation.getNode() << std::endl; } - // process the trust node here - if (d_lazyProof!=nullptr) + if (lcp!=nullptr) { - processTrustNode(texplanation); - trNodes.push_back(texplanation); + // ----------- Via theory + // exp => lit exp + // ---------------------------------MACRO_BSR_PRED_TRANSFORM + // lit + Node proven = texplanation.getProven(); + lcp->addLazyStep(proven,texplanation.getGenerator()); + std::vector children; + children.push_back(proven); + children.push_back(texplanation.getNode()); + std::vector args; + args.push_back(toExplain.d_node); + lcp->addStep(toExplain.d_node,PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } Node explanation = texplanation.getNode(); @@ -2195,11 +2230,19 @@ theory::TrustNode TheoryEngine::getExplanation( Node exp = mkExplanation(explanationVector); - if (d_lazyProof!=nullptr) + if (lcp!=nullptr) { + Assert (lcp!=nullptr); // FIXME - // We have E1 => l1 ^ ... En => ln. - // Need to prove E1 ^ ... ^ En => ( l1 ^ ... ^ ln ) + // get the proof for conclusion + std::shared_ptr pfConc = lcp->mkProof(conclusion); + std::vector scopeAssumps; + for (size_t k = 0, esize = explanationVector.size(); k < esize; ++ k) + { + scopeAssumps.push_back(explanationVector[k].d_node); + } + // call the scope method of proof node manager + std::shared_ptr pf = d_pNodeManager->mkScope(pfConc, scopeAssumps); } return theory::TrustNode::mkTrustLemma(exp, nullptr); diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index d600a546b..13a1d581c 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -394,9 +394,6 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, // assumption (= y x). We modify the proof leaves to account for this // below. - // The free assumptions of the proof - std::map> famap; - pfConc->getFreeAssumptionsMap(famap); // we first ensure the assumptions are flattened std::unordered_set ac; for (const TNode& a : assumps) @@ -410,6 +407,9 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, ac.insert(a); } } + // The free assumptions of the proof + std::map> famap; + pfConc->getFreeAssumptionsMap(famap); std::unordered_set acu; std::unordered_set::iterator itf; for (const std::pair>& fa : famap) -- cgit v1.2.3 From 30bc3db1f7dee1f89baea8706e5966cb13b8948c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 09:43:02 -0500 Subject: Format --- src/expr/proof_node_manager.cpp | 27 ++++++++++---------- src/expr/proof_node_manager.h | 5 ++-- src/theory/builtin/proof_checker.cpp | 40 +++++++++++++++++------------- src/theory/builtin/proof_checker.h | 23 +++++++++++------ src/theory/strings/infer_proof_cons.cpp | 27 +++++++++++--------- src/theory/strings/infer_proof_cons.h | 4 +-- src/theory/theory_engine.cpp | 44 ++++++++++++++++++--------------- 7 files changed, 93 insertions(+), 77 deletions(-) diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index d9a2d1711..f1ec78aab 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -60,9 +60,10 @@ std::shared_ptr ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, children, args, fact); } -std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr pf, - std::vector& assumps, - bool ensureClosed) +std::shared_ptr ProofNodeManager::mkScope( + std::shared_ptr pf, + std::vector& assumps, + bool ensureClosed) { std::vector> pfChildren; pfChildren.push_back(pf); @@ -108,9 +109,9 @@ std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr itf = ac.find(aeqSym); if (itf != ac.end()) { - Trace("pnm-scope") - << "- reorient assumption " << aeqSym << " via " << a << " for " - << fa.second.size() << " proof nodes" << std::endl; + Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a + << " for " << fa.second.size() << " proof nodes" + << std::endl; std::shared_ptr pfaa = mkAssume(aeqSym); for (ProofNode* pfs : fa.second) { @@ -120,8 +121,7 @@ std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr children.push_back(pfaa); std::vector args; args.push_back(a); - updateNode( - pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } Trace("pnm-scope") << "...finished" << std::endl; acu.insert(aeqSym); @@ -136,9 +136,8 @@ std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr { ss << "- assumption: " << aprint << std::endl; } - AlwaysAssert(false) - << "Generated a proof that is not closed by the scope: " << ss.str() - << std::endl; + AlwaysAssert(false) << "Generated a proof that is not closed by the scope: " + << ss.str() << std::endl; } if (acu.size() < ac.size()) { @@ -149,15 +148,15 @@ std::shared_ptr ProofNodeManager::mkScope(std::shared_ptr if (acu.find(a) == acu.end()) { Notice() << "ProofNodeManager::mkScope: assumption " << a - << " does not match a free assumption in proof" << std::endl; + << " does not match a free assumption in proof" << std::endl; } } } assumps.clear(); - assumps.insert(assumps.end(), acu.begin(), acu.end()); + assumps.insert(assumps.end(), acu.begin(), acu.end()); return mkNode(PfRule::SCOPE, pfChildren, assumps); } - + bool ProofNodeManager::updateNode( ProofNode* pn, PfRule id, diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 7cf6574cb..527f2562d 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -83,9 +83,8 @@ class ProofNodeManager /** Make scope */ std::shared_ptr mkScope(std::shared_ptr pf, std::vector& assumps, - bool ensureClosed = true - ); - + bool ensureClosed = true); + /** * This method updates pn to be a proof of the form ( children, args ), * while maintaining its d_proven field. This method returns false if this diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index b57bb112b..b05dbf7e7 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -81,7 +81,8 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) } Node BuiltinProofRuleChecker::applySubstitution(Node n, - const std::vector& exp, MethodId ids) + const std::vector& exp, + MethodId ids) { Node nk = ProofSkolemCache::getSkolemForm(n); Node nks = applySubstitutionExternal(nk, exp, ids); @@ -119,36 +120,38 @@ Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) } // unknown rewriter Assert(false) - << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " << idr - << std::endl; + << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " + << idr << std::endl; return n; } -Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, Node exp, MethodId ids) +Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, + Node exp, + MethodId ids) { Assert(!exp.isNull()); Node expk = ProofSkolemCache::getSkolemForm(exp); TNode var, subs; - if (ids==MethodId::SB_DEFAULT) + if (ids == MethodId::SB_DEFAULT) { - if (expk.getKind()!=EQUAL) + if (expk.getKind() != EQUAL) { return Node::null(); } var = expk[0]; subs = expk[1]; } - else if (ids==MethodId::SB_PREDICATE) + else if (ids == MethodId::SB_PREDICATE) { - bool polarity = expk.getKind()!=NOT; + bool polarity = expk.getKind() != NOT; var = polarity ? expk : expk[0]; subs = NodeManager::currentNM()->mkConst(polarity); } else { - Assert(false) - << "BuiltinProofRuleChecker::applySubstitutionExternal: no substitution for " << ids - << std::endl; + Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no " + "substitution for " + << ids << std::endl; } return n.substitute(var, subs); } @@ -217,7 +220,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(children.size() > 0); Assert(1 <= args.size() && args.size() <= 2); MethodId ids = MethodId::SB_DEFAULT; - if (args.size()==2 && !getMethodId(args[1], ids)) + if (args.size() == 2 && !getMethodId(args[1], ids)) { return Node::null(); } @@ -234,7 +237,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(children.empty()); Assert(1 <= args.size() && args.size() <= 2); MethodId ids = MethodId::RW_REWRITE; - if (args.size()==2 && !getMethodId(args[1], ids)) + if (args.size() == 2 && !getMethodId(args[1], ids)) { return Node::null(); } @@ -350,7 +353,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } -bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, MethodId& ids, MethodId& idr, size_t index) +bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, + MethodId& ids, + MethodId& idr, + size_t index) { ids = MethodId::SB_DEFAULT; idr = MethodId::RW_REWRITE; @@ -363,12 +369,12 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, Method return false; } } - if (args.size() >= index+1) + if (args.size() >= index + 1) { - if (!getMethodId(args[index+1], idr)) + if (!getMethodId(args[index + 1], idr)) { Trace("builtin-pfcheck") - << "Failed to get id from " << args[index+1] << std::endl; + << "Failed to get id from " << args[index + 1] << std::endl; return false; } } diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 9291bbf9f..afd9bad5a 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -30,8 +30,8 @@ namespace theory { * is semantically equivalent to the input. The identifiers below list * various methods that have this contract. This identifier is used * in a number of the builtin rules. - * - * A substitution is a method for turning a formula into + * + * A substitution is a method for turning a formula into */ enum class MethodId : uint32_t { @@ -83,10 +83,12 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * substitution * @return The substituted form of n. */ - static Node applySubstitution(Node n, Node exp, - MethodId ids = MethodId::SB_DEFAULT); - static Node applySubstitution(Node n, const std::vector& exp, - MethodId ids = MethodId::SB_DEFAULT); + static Node applySubstitution(Node n, + Node exp, + MethodId ids = MethodId::SB_DEFAULT); + static Node applySubstitution(Node n, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT); /** Apply substitution + rewriting * * Combines the above two steps. @@ -113,7 +115,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker const std::vector& children, const std::vector& args) override; /** get method ids */ - bool getMethodIds(const std::vector& args, MethodId& ids, MethodId& idr, size_t index); + bool getMethodIds(const std::vector& args, + MethodId& ids, + MethodId& idr, + size_t index); /** * Apply rewrite (on Skolem form). id is the identifier of the rewriter. */ @@ -124,7 +129,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * n * { exp[0] -> exp[1] } in Skolem form. */ static Node applySubstitutionExternal(Node n, Node exp, MethodId ids); - static Node applySubstitutionExternal(Node n, const std::vector& exp, MethodId ids); + static Node applySubstitutionExternal(Node n, + const std::vector& exp, + MethodId ids); }; } // namespace builtin diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index bad121d65..281b1abff 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -306,8 +306,11 @@ Node InferProofCons::convert(Inference infer, // optimization in processSimpleNEq. Alternatively, this could // possibly be done by CONCAT_EQ with !isRev. std::vector cexp; - if (convertPredTransform( - mainEqCeq, conc, cexp, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT)) + if (convertPredTransform(mainEqCeq, + conc, + cexp, + MethodId::SB_DEFAULT, + MethodId::RW_REWRITE_EQ_EXT)) { Trace("strings-ipc-core") << "Transformed to " << conc << " via pred transform" << std::endl; @@ -916,16 +919,16 @@ bool InferProofCons::convertPredTransform(Node src, // try to prove that tgt rewrites to src children.insert(children.end(), exp.begin(), exp.end()); args.push_back(tgt); - addMethodIds(args,ids,idr); + addMethodIds(args, ids, idr); Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); if (res.isNull()) { // failed to apply return false; } - Trace("strings-ipc-debug") - << "InferProofCons::convertPredTransform: success " << src - << " == " << tgt << " under " << exp << " via " << ids << "/" << idr << std::endl; + Trace("strings-ipc-debug") << "InferProofCons::convertPredTransform: success " + << src << " == " << tgt << " under " << exp + << " via " << ids << "/" << idr << std::endl; // should definitely have concluded tgt Assert(res == tgt); return true; @@ -938,7 +941,7 @@ bool InferProofCons::convertPredIntro(Node tgt, { std::vector args; args.push_back(tgt); - addMethodIds(args,ids,idr); + addMethodIds(args, ids, idr); Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); if (res.isNull()) { @@ -950,14 +953,14 @@ bool InferProofCons::convertPredIntro(Node tgt, Node InferProofCons::convertPredElim(Node src, const std::vector& exp, - MethodId ids, + MethodId ids, MethodId idr) { std::vector children; children.push_back(src); children.insert(children.end(), exp.begin(), exp.end()); std::vector args; - addMethodIds(args,ids,idr); + addMethodIds(args, ids, idr); Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); if (isSymm(src, srcRew)) { @@ -967,9 +970,9 @@ Node InferProofCons::convertPredElim(Node src, return srcRew; } -void InferProofCons::addMethodIds(std::vector& args, - MethodId ids, - MethodId idr) +void InferProofCons::addMethodIds(std::vector& args, + MethodId ids, + MethodId idr) { bool ndefRewriter = (idr != MethodId::RW_REWRITE); if (ids != MethodId::SB_DEFAULT || ndefRewriter) diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index f5bb57996..ed38fdb96 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -141,9 +141,7 @@ class InferProofCons : public ProofGenerator MethodId ids = MethodId::SB_DEFAULT, MethodId idr = MethodId::RW_REWRITE); /** Add method ids */ - void addMethodIds(std::vector& args, - MethodId ids, - MethodId idr); + void addMethodIds(std::vector& args, MethodId ids, MethodId idr); /** */ Node convertTrans(Node eqa, Node eqb); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b571fc2b8..3b1c5bfaa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1915,7 +1915,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln // Prove ~( E1 ^ ... ^ En ) - Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; @@ -2008,13 +2007,13 @@ theory::TrustNode TheoryEngine::getExplanation( LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() == 1); - + Node conclusion = explanationVector[0].d_node; std::unique_ptr lcp; - if (d_lazyProof!=nullptr) + if (d_lazyProof != nullptr) { // FIXME - //lcp.reset(new LazyCDProof(d_pNodeManager.get())); + // lcp.reset(new LazyCDProof(d_pNodeManager.get())); } unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping @@ -2038,19 +2037,21 @@ theory::TrustNode TheoryEngine::getExplanation( << toExplain.d_theory << endl; // If a true constant or a negation of a false constant we can ignore it - if ((toExplain.d_node.isConst() && toExplain.d_node.getConst()) || - (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() - && !toExplain.d_node[0].getConst())) + if ((toExplain.d_node.isConst() && toExplain.d_node.getConst()) + || (toExplain.d_node.getKind() == kind::NOT + && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst())) { ++ i; - if (lcp!=nullptr) + if (lcp != nullptr) { // ------------------MACRO_SR_PRED_INTRO // toExplain.d_node std::vector children; std::vector args; args.push_back(toExplain.d_node); - lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); } continue; } @@ -2076,7 +2077,7 @@ theory::TrustNode TheoryEngine::getExplanation( toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } - if (lcp!=nullptr) + if (lcp != nullptr) { // toExplain.d_node[0] ... toExplain.d_node[n] // --------------------------------------------MACRO_BSR_PRED_INTRO @@ -2088,7 +2089,8 @@ theory::TrustNode TheoryEngine::getExplanation( } std::vector args; args.push_back(toExplain.d_node); - lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); } ++ i; continue; @@ -2146,20 +2148,21 @@ theory::TrustNode TheoryEngine::getExplanation( << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << texplanation.getNode() << std::endl; } - if (lcp!=nullptr) + if (lcp != nullptr) { // ----------- Via theory // exp => lit exp // ---------------------------------MACRO_BSR_PRED_TRANSFORM // lit Node proven = texplanation.getProven(); - lcp->addLazyStep(proven,texplanation.getGenerator()); + lcp->addLazyStep(proven, texplanation.getGenerator()); std::vector children; children.push_back(proven); children.push_back(texplanation.getNode()); std::vector args; args.push_back(toExplain.d_node); - lcp->addStep(toExplain.d_node,PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } Node explanation = texplanation.getNode(); @@ -2229,22 +2232,23 @@ theory::TrustNode TheoryEngine::getExplanation( }); Node exp = mkExplanation(explanationVector); - - if (lcp!=nullptr) + + if (lcp != nullptr) { - Assert (lcp!=nullptr); + Assert(lcp != nullptr); // FIXME // get the proof for conclusion std::shared_ptr pfConc = lcp->mkProof(conclusion); std::vector scopeAssumps; - for (size_t k = 0, esize = explanationVector.size(); k < esize; ++ k) + for (size_t k = 0, esize = explanationVector.size(); k < esize; ++k) { scopeAssumps.push_back(explanationVector[k].d_node); } // call the scope method of proof node manager - std::shared_ptr pf = d_pNodeManager->mkScope(pfConc, scopeAssumps); + std::shared_ptr pf = + d_pNodeManager->mkScope(pfConc, scopeAssumps); } - + return theory::TrustNode::mkTrustLemma(exp, nullptr); } -- cgit v1.2.3 From 1ee18ab1b0e6648fdd614742c841128079e6ec27 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 11:15:55 -0500 Subject: More --- src/expr/proof.cpp | 7 +++++++ src/expr/proof.h | 6 ++++++ src/theory/builtin/proof_checker.cpp | 2 +- src/theory/strings/infer_proof_cons.cpp | 13 +++--------- src/theory/strings/infer_proof_cons.h | 2 -- src/theory/theory_engine.cpp | 37 ++++++++++++++++++++------------- 6 files changed, 39 insertions(+), 28 deletions(-) diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 8ec55d1f5..dda2ccd2d 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -381,4 +381,11 @@ bool CDProof::isAssumption(ProofNode* pn) return false; } +bool CDProof::isSame(TNode f, TNode g) +{ + return f == g + || (f.getKind() == EQUAL && g.getKind() == EQUAL + && f[0] == g[1] && f[1] == g[0]); +} + } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index e5b2775d9..20bbb4996 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -206,6 +206,12 @@ class CDProof /** Get the proof manager for this proof */ ProofNodeManager* getManager() const; + /** + * Is same? Returns true if f and g are the same formula, or if they are + * symmetric equalities. If two nodes f and g are the same, then a proof for + * f suffices as a proof for g according to this class. + */ + static bool isSame(TNode f, TNode g); protected: typedef context::CDHashMap, NodeHashFunction> NodeProofNodeMap; diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index b05dbf7e7..8c47bc060 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -369,7 +369,7 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, return false; } } - if (args.size() >= index + 1) + if (args.size() > index + 1) { if (!getMethodId(args[index + 1], idr)) { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 281b1abff..49a697592 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -261,7 +261,7 @@ Node InferProofCons::convert(Inference infer, ps.d_children.begin() + mainEqIndex); Node mainEqSRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, emptyVec); - if (isSymm(mainEqSRew, mainEq)) + if (CDProof::isSame(mainEqSRew, mainEq)) { Trace("strings-ipc-core") << "...undo step" << std::endl; // not necessary @@ -909,7 +909,7 @@ bool InferProofCons::convertPredTransform(Node src, MethodId idr) { // symmetric equalities - if (isSymm(src, tgt)) + if (CDProof::isSame(src, tgt)) { return true; } @@ -962,7 +962,7 @@ Node InferProofCons::convertPredElim(Node src, std::vector args; addMethodIds(args, ids, idr); Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); - if (isSymm(src, srcRew)) + if (CDProof::isSame(src, srcRew)) { d_psb.popStep(); return src; @@ -1010,13 +1010,6 @@ Node InferProofCons::convertTrans(Node eqa, Node eqb) return Node::null(); } -bool InferProofCons::isSymm(Node src, Node tgt) -{ - return src == tgt - || (src.getKind() == EQUAL && tgt.getKind() == EQUAL - && src[0] == tgt[1] && src[1] == tgt[0]); -} - ProofStepBuffer* InferProofCons::getBuffer() { return &d_psb; } std::shared_ptr InferProofCons::getProofFor(Node fact) diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index ed38fdb96..18f2d0b61 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -145,8 +145,6 @@ class InferProofCons : public ProofGenerator /** */ Node convertTrans(Node eqa, Node eqb); - /** Is symm */ - static bool isSymm(Node src, Node tgt); /** the proof node manager */ ProofNodeManager* d_pnm; /** The lazy fact map */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3b1c5bfaa..965cd4e72 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2013,7 +2013,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (d_lazyProof != nullptr) { // FIXME - // lcp.reset(new LazyCDProof(d_pNodeManager.get())); + //lcp.reset(new LazyCDProof(d_pNodeManager.get())); } unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping @@ -2061,6 +2061,7 @@ theory::TrustNode TheoryEngine::getExplanation( { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; + // it will be a free assumption in the proof continue; } @@ -2080,7 +2081,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (lcp != nullptr) { // toExplain.d_node[0] ... toExplain.d_node[n] - // --------------------------------------------MACRO_BSR_PRED_INTRO + // --------------------------------------------MACRO_SR_PRED_INTRO // toExplain.d_node std::vector children; for (size_t k = 0; k < nchild; ++k) @@ -2089,6 +2090,7 @@ theory::TrustNode TheoryEngine::getExplanation( } std::vector args; args.push_back(toExplain.d_node); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); } @@ -2150,19 +2152,24 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { - // ----------- Via theory - // exp => lit exp - // ---------------------------------MACRO_BSR_PRED_TRANSFORM - // lit - Node proven = texplanation.getProven(); - lcp->addLazyStep(proven, texplanation.getGenerator()); - std::vector children; - children.push_back(proven); - children.push_back(texplanation.getNode()); - std::vector args; - args.push_back(toExplain.d_node); - lcp->addStep( - toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + // if not a trivial explanation + if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node)) + { + // ----------- Via theory + // exp => lit exp + // ---------------------------------MACRO_SR_PRED_TRANSFORM + // lit + Node proven = texplanation.getProven(); + lcp->addLazyStep(proven, texplanation.getGenerator()); + std::vector children; + children.push_back(proven); + children.push_back(texplanation.getNode()); + std::vector args; + args.push_back(toExplain.d_node); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + } } Node explanation = texplanation.getNode(); -- cgit v1.2.3 From 1edcc8f0896701d754ed811d8358de50c2e2ecd3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 13:19:39 -0500 Subject: Proofs for getExplanation --- src/theory/theory_engine.cpp | 35 +++++++++++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 965cd4e72..93a3f286d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2012,8 +2012,8 @@ theory::TrustNode TheoryEngine::getExplanation( std::unique_ptr lcp; if (d_lazyProof != nullptr) { - // FIXME - //lcp.reset(new LazyCDProof(d_pNodeManager.get())); + Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl; + lcp.reset(new LazyCDProof(d_pNodeManager.get())); } unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping @@ -2045,6 +2045,7 @@ theory::TrustNode TheoryEngine::getExplanation( ++ i; if (lcp != nullptr) { + Trace("te-proof-exp") << "- explain " << toExplain.d_node << " trivially..." << std::endl; // ------------------MACRO_SR_PRED_INTRO // toExplain.d_node std::vector children; @@ -2062,6 +2063,7 @@ theory::TrustNode TheoryEngine::getExplanation( Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; // it will be a free assumption in the proof + Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl; continue; } @@ -2080,6 +2082,7 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { + Trace("te-proof-exp") << "- AND expand " << toExplain.d_node << std::endl; // toExplain.d_node[0] ... toExplain.d_node[n] // --------------------------------------------MACRO_SR_PRED_INTRO // toExplain.d_node @@ -2128,7 +2131,15 @@ theory::TrustNode TheoryEngine::getExplanation( } } }) - // FIXME + if (lcp !=nullptr) + { + if (!CDProof::isSame(toExplain.d_node,(*find).second.d_node)) + { + Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl; + // does this ever happen? + Assert(false); + } + } continue; } } @@ -2152,6 +2163,7 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { + Trace("te-proof-exp") << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node << " by " << texplanation.getNode() << std::endl; // if not a trivial explanation if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node)) { @@ -2160,7 +2172,22 @@ theory::TrustNode TheoryEngine::getExplanation( // ---------------------------------MACRO_SR_PRED_TRANSFORM // lit Node proven = texplanation.getProven(); - lcp->addLazyStep(proven, texplanation.getGenerator()); + if (texplanation.getGenerator()!=nullptr) + { + lcp->addLazyStep(proven, texplanation.getGenerator()); + } + else + { + Trace("te-proof-exp") << "...trust THEORY_LEMMA" << std::endl; + // otherwise, trusted theory lemma + std::vector children; + std::vector args; + args.push_back(proven); + unsigned tid = static_cast(toExplain.d_theory); + Node tidn = NodeManager::currentNM()->mkConst(Rational(tid)); + args.push_back(tidn); + lcp->addStep(proven,PfRule::THEORY_LEMMA,children,args); + } std::vector children; children.push_back(proven); children.push_back(texplanation.getNode()); -- cgit v1.2.3 From a111a1d64da6e763a63f0b0b29046ef8f81b2599 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 15:32:39 -0500 Subject: TheoryEngineProofGenerator, proper explanations for getExplantaion --- src/CMakeLists.txt | 2 + src/theory/proof_engine_output_channel.cpp | 40 ++------------ src/theory/shared_terms_database.cpp | 2 +- src/theory/theory_engine.cpp | 72 ++++++++++++++++++------- src/theory/theory_engine.h | 18 ++++++- src/theory/theory_engine_proof_generator.cpp | 81 ++++++++++++++++++++++++++++ src/theory/theory_engine_proof_generator.h | 53 ++++++++++++++++++ 7 files changed, 209 insertions(+), 59 deletions(-) create mode 100644 src/theory/theory_engine_proof_generator.cpp create mode 100644 src/theory/theory_engine_proof_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2ac73f067..6deaea082 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -748,6 +748,8 @@ libcvc4_add_sources( theory/theory.h theory/theory_engine.cpp theory/theory_engine.h + theory/theory_engine_proof_generator.cpp + theory/theory_engine_proof_generator.h theory/theory_id.cpp theory/theory_id.h theory/theory_model.cpp diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp index 20dbd4ef0..82363ff9b 100644 --- a/src/theory/proof_engine_output_channel.cpp +++ b/src/theory/proof_engine_output_channel.cpp @@ -30,25 +30,8 @@ ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine, void ProofEngineOutputChannel::trustedConflict(TrustNode pconf) { Assert(pconf.getKind() == TrustNodeKind::CONFLICT); - Node conf = pconf.getNode(); - if (d_lazyPf != nullptr) - { - Node ckey = pconf.getProven(); - ProofGenerator* pfg = pconf.getGenerator(); - // may or may not have supplied a generator - if (pfg != nullptr) - { - ++d_statistics.trustedConflicts; - // if we have, add it to the lazy proof object - d_lazyPf->addLazyStep(ckey, pfg); - Assert(pfg->hasProofFor(ckey)); - } - else - { - // if none provided, do a very coarse-grained step - addTheoryLemmaStep(ckey); - } - } + d_engine->processTrustNode(pconf, d_theory); + TNode conf = pconf.getNode(); // now, call the normal interface to conflict conflict(conf); } @@ -59,25 +42,8 @@ LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem, bool sendAtoms) { Assert(plem.getKind() == TrustNodeKind::LEMMA); + d_engine->processTrustNode(plem, d_theory); TNode lem = plem.getNode(); - if (d_lazyPf != nullptr) - { - Node lkey = plem.getProven(); - ProofGenerator* pfg = plem.getGenerator(); - // may or may not have supplied a generator - if (pfg != nullptr) - { - ++d_statistics.trustedLemmas; - // if we have, add it to the lazy proof object - d_lazyPf->addLazyStep(lkey, pfg); - Assert(pfg->hasProofFor(lkey)); - } - else - { - // if none provided, do a very coarse-grained step - addTheoryLemmaStep(lkey); - } - } // now, call the normal interface for lemma return OutputChannel::lemma(lem, removable, preprocess, sendAtoms); } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 723e20a16..ac27a5820 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -230,7 +230,7 @@ void SharedTermsDatabase::checkForConflict() { conflict = conflict.notNode(); } TrustNode trnc = d_pfee.assertConflict(conflict); - d_theoryEngine->processTrustNode(trnc); + d_theoryEngine->processTrustNode(trnc, THEORY_BUILTIN); d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 93a3f286d..7a1e34bef 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,6 +52,7 @@ #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" #include "util/resource_manager.h" +#include "theory/theory_engine_proof_generator.h" using namespace std; @@ -201,6 +202,7 @@ TheoryEngine::TheoryEngine(context::Context* context, options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr), + d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)), d_sharedTerms( this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()), d_masterEqualityEngine(nullptr), @@ -1605,8 +1607,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( proofRecipe->addStep(proofStep); } }); - // it came directly from the theory, it is ready to be processed - processTrustNode(texplanation); return texplanation; } @@ -1639,7 +1639,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; - // the trust node was processed within getExplanation return texplanation; } @@ -1848,7 +1847,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } -void TheoryEngine::processTrustNode(theory::TrustNode trn) +void TheoryEngine::processTrustNode(theory::TrustNode trn, + theory::TheoryId from) { if (d_lazyProof == nullptr) { @@ -1856,15 +1856,29 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn) return; } ProofGenerator* pfg = trn.getGenerator(); + Node p = trn.getProven(); // may or may not have supplied a generator if (pfg != nullptr) { - Node p = trn.getProven(); // if we have, add it to the lazy proof object d_lazyProof->addLazyStep(p, pfg); // generator should have a proof for p Assert(pfg->hasProofFor(p)); } + else + { + // all BUILTIN should be handled + Assert (from!=THEORY_BUILTIN); + // untrusted theory lemma + std::vector children; + std::vector args; + args.push_back(p); + unsigned tid = static_cast(from); + Node tidn = NodeManager::currentNM()->mkConst(Rational(tid)); + args.push_back(tidn); + // add the step, should always succeed; + d_lazyProof->addStep(p, PfRule::THEORY_LEMMA, children, args); + } } void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { @@ -1913,8 +1927,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); - // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln - // Prove ~( E1 ^ ... ^ En ) + // FIXME: have ~( F ) and E => F, prove ~( E ) Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; @@ -2009,7 +2022,9 @@ theory::TrustNode TheoryEngine::getExplanation( Assert(explanationVector.size() == 1); Node conclusion = explanationVector[0].d_node; - std::unique_ptr lcp; + std::shared_ptr lcp; + bool simpleExplain = true; + TrustNode simpleTrn; if (d_lazyProof != nullptr) { Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl; @@ -2053,6 +2068,7 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(toExplain.d_node); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + simpleExplain = false; } continue; } @@ -2096,6 +2112,7 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + simpleExplain = false; } ++ i; continue; @@ -2138,6 +2155,7 @@ theory::TrustNode TheoryEngine::getExplanation( Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl; // does this ever happen? Assert(false); + simpleExplain = false; } } continue; @@ -2196,6 +2214,20 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + if (simpleExplain) + { + if (simpleTrn.isNull()) + { + // as an optimization, it may be a simple explanation, so we + // remember the trust node for now + simpleTrn = texplanation; + } + else + { + // multiple theories involved, not simple + simpleExplain = false; + } + } } } Node explanation = texplanation.getNode(); @@ -2269,18 +2301,20 @@ theory::TrustNode TheoryEngine::getExplanation( if (lcp != nullptr) { - Assert(lcp != nullptr); - // FIXME - // get the proof for conclusion - std::shared_ptr pfConc = lcp->mkProof(conclusion); - std::vector scopeAssumps; - for (size_t k = 0, esize = explanationVector.size(); k < esize; ++k) + // doesn't work currently due to reordering of assumptions + /* + if (simpleExplain) { - scopeAssumps.push_back(explanationVector[k].d_node); - } - // call the scope method of proof node manager - std::shared_ptr pf = - d_pNodeManager->mkScope(pfConc, scopeAssumps); + // single call to a theory's explain method, skip the proof generator + Assert (!simpleTrn.isNull()); + Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl; + return simpleTrn; + } + */ + // store in the proof generator + TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp); + // return the trust node + return trn; } return theory::TrustNode::mkTrustLemma(exp, nullptr); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c3759ca52..de4b17f8c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -58,6 +58,7 @@ namespace CVC4 { class ResourceManager; class LemmaProofRecipe; class LazyCDProof; +class TheoryEngineProofGenerator; /** * A pair of a theory and a node. This is used to mark the flow of @@ -156,6 +157,8 @@ class TheoryEngine { * This stores instructions for how to construct proofs for all theory lemmas. */ std::shared_ptr d_lazyProof; + /** The proof generator */ + std::shared_ptr d_tepg; //--------------------------------- end new proofs /** @@ -361,8 +364,19 @@ class TheoryEngine { bool preprocess, theory::TheoryId atomsTo); - /** Process trust node */ - void processTrustNode(theory::TrustNode trn); + /** + * Process trust node. This method ensures that the proof for the proven node + * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained + * by this class, referencing the proof generator of the trust node. The + * argument from specifies the theory responsible for this trust node. If + * no generator is provided, then a (eager) THEORY_LEMMA step is added to + * the lazy proof. + * + * @param trn The trust node to process + * @param from The id of the theory responsible for the trust node. + */ + void processTrustNode(theory::TrustNode trn, + theory::TheoryId from); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp new file mode 100644 index 000000000..af737e53b --- /dev/null +++ b/src/theory/theory_engine_proof_generator.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file theory_engine_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The theory engine proof generator + **/ + +#include "theory/theory_engine_proof_generator.h" + +using namespace CVC4::kind; + +namespace CVC4 +{ + +TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u) : d_pnm(pnm), d_proofs(u) +{ + +} + +theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp, std::shared_ptr lpf) +{ + theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit,exp,this); + Node p = trn.getProven(); + // should not already be proven + NodeLazyCDProofMap::iterator it = d_proofs.find(p); + if (it!=d_proofs.end()) + { + Assert(false); + } + else + { + // we will prove this + d_proofs.insert(p, lpf); + } + return trn; +} + +std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) +{ + Assert (f.getKind()==IMPLIES && f.getNumChildren()==2); + NodeLazyCDProofMap::iterator it = d_proofs.find(f); + if (it==d_proofs.end()) + { + return nullptr; + } + std::shared_ptr lcp = (*it).second; + // finalize it via scope + std::vector scopeAssumps; + if (f[0].getKind()==AND) + { + for (const Node& fc : f[0]) + { + scopeAssumps.push_back(fc); + } + } + else + { + scopeAssumps.push_back(f[1]); + } + Node conclusion = f[1]; + + // get the proof for conclusion + std::shared_ptr pfb = lcp->mkProof(conclusion); + // call the scope method of proof node manager + std::shared_ptr pf = d_pnm->mkScope(pfb, scopeAssumps); + return pf; +} + +std::string TheoryEngineProofGenerator::identify() const +{ + return "TheoryEngineProofGenerator"; +} + +} diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h new file mode 100644 index 000000000..0dd6e0dd8 --- /dev/null +++ b/src/theory/theory_engine_proof_generator.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file theory_engine.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The theory engine proof generator + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H +#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H + +#include + +#include "expr/lazy_proof.h" +#include "expr/proof_node_manager.h" +#include "expr/proof_generator.h" +#include "context/cdhashmap.h" +#include "context/context.h" +#include "theory/trust_node.h" + +namespace CVC4 { + +class TheoryEngineProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap, NodeHashFunction> + NodeLazyCDProofMap; + public: + TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); + ~TheoryEngineProofGenerator(){} + /** Set proof */ + theory::TrustNode mkTrustExplain(TNode lit, Node exp, std::shared_ptr lpf); + /** Get proof for */ + std::shared_ptr getProofFor(Node f) override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override; + private: + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_pnm; + /** Map from formulas to lazy CD proofs */ + NodeLazyCDProofMap d_proofs; +}; + +} + +#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */ -- cgit v1.2.3 From 6a3b1cfa8d6f1797964b855b34f94afd13d0246b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 15:56:46 -0500 Subject: Merge proof engine output channel into engine output channel --- src/CMakeLists.txt | 2 - src/README | 1 - src/theory/eager_proof_generator.cpp | 1 - src/theory/engine_output_channel.cpp | 21 +++++++ src/theory/engine_output_channel.h | 24 ++++++++ src/theory/proof_engine_output_channel.cpp | 66 -------------------- src/theory/proof_engine_output_channel.h | 99 ------------------------------ src/theory/shared_terms_database.cpp | 8 +-- src/theory/shared_terms_database.h | 5 +- src/theory/theory_engine.cpp | 15 ++++- src/theory/theory_engine.h | 10 ++- src/theory/trust_node.cpp | 1 - 12 files changed, 67 insertions(+), 186 deletions(-) delete mode 100644 src/theory/proof_engine_output_channel.cpp delete mode 100644 src/theory/proof_engine_output_channel.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6deaea082..f5be109ed 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -450,8 +450,6 @@ libcvc4_add_sources( theory/logic_info.cpp theory/logic_info.h theory/output_channel.h - theory/proof_engine_output_channel.cpp - theory/proof_engine_output_channel.h theory/quantifiers/alpha_equivalence.cpp theory/quantifiers/alpha_equivalence.h theory/quantifiers/anti_skolem.cpp diff --git a/src/README b/src/README index c7a940837..1de6ac991 100644 --- a/src/README +++ b/src/README @@ -80,7 +80,6 @@ PRs: (6) Split EngineOutputChannel from TheoryEngine to its own file (7) Add LazyCDProof and ProofGenerator (8) Add TrustNode -(9) Add ProofEngineOutputChannel - Add EagerProofGenerator (10) ProofEqEngine (11) TheoryEngine proof checker initialize diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index 1b8d4ceb0..0dc87e6ba 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -15,7 +15,6 @@ #include "theory/eager_proof_generator.h" #include "expr/proof_node_manager.h" -#include "theory/proof_engine_output_channel.h" namespace CVC4 { namespace theory { diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 176d08acf..b473ffc56 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -298,5 +298,26 @@ void EngineOutputChannel::handleUserAttribute(const char* attr, d_engine->handleUserAttribute(attr, t); } +void EngineOutputChannel::trustedConflict(TrustNode pconf) +{ + Assert(pconf.getKind() == TrustNodeKind::CONFLICT); + d_engine->processTrustNode(pconf, d_theory); + TNode conf = pconf.getNode(); + // now, call the normal interface to conflict + conflict(conf); +} + +LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, + bool removable, + bool preprocess, + bool sendAtoms) +{ + Assert(plem.getKind() == TrustNodeKind::LEMMA); + d_engine->processTrustNode(plem, d_theory); + TNode lem = plem.getNode(); + // now, call the normal interface for lemma + return OutputChannel::lemma(lem, removable, preprocess, sendAtoms); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 1699795a1..1be4ec1d3 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -31,6 +31,10 @@ namespace theory { /** * An output channel for Theory that passes messages back to a TheoryEngine * for a given Theory. + * + * Notice that is has interfaces trustedConflict and trustedLemma which are + * used for ensuring that proof generators are associated with the lemmas + * and conflicts sent on this output channel. */ class EngineOutputChannel : public theory::OutputChannel { @@ -63,6 +67,26 @@ class EngineOutputChannel : public theory::OutputChannel void handleUserAttribute(const char* attr, theory::Theory* t) override; + /** + * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method + * sends conf on the output channel of this class whose proof can be generated + * by the generator pfg. It calls TheoryEngine::processTrustNode, + * which ensures that the generator pfg is associated with conf in the + * lazy proof owned by the theory engine of this class. + */ + void trustedConflict(TrustNode pconf) override; + /** + * Let plem be the pair (Node lem, ProofGenerator * pfg). + * Send lem on the output channel of this class whose proof can be generated + * by the generator pfg. Apart from pfg, the interface for this method is + * the same as OutputChannel. It calls TheoryEngine::processTrustNode, + * which ensures that the generator pfg is associated with lem in the + * lazy proof owned by the theory engine of this class. + */ + LemmaStatus trustedLemma(TrustNode plem, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) override; protected: /** * Statistics for a particular theory. diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp deleted file mode 100644 index 82363ff9b..000000000 --- a/src/theory/proof_engine_output_channel.cpp +++ /dev/null @@ -1,66 +0,0 @@ -/********************* */ -/*! \file proof_engine_output_channel.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The Evaluator class - ** - ** The Evaluator class. - **/ - -#include "theory/proof_engine_output_channel.h" - -#include "expr/lazy_proof.h" - -namespace CVC4 { -namespace theory { - -ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine, - theory::TheoryId theory, - LazyCDProof* lpf) - : EngineOutputChannel(engine, theory), d_lazyPf(lpf) -{ -} -void ProofEngineOutputChannel::trustedConflict(TrustNode pconf) -{ - Assert(pconf.getKind() == TrustNodeKind::CONFLICT); - d_engine->processTrustNode(pconf, d_theory); - TNode conf = pconf.getNode(); - // now, call the normal interface to conflict - conflict(conf); -} - -LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem, - bool removable, - bool preprocess, - bool sendAtoms) -{ - Assert(plem.getKind() == TrustNodeKind::LEMMA); - d_engine->processTrustNode(plem, d_theory); - TNode lem = plem.getNode(); - // now, call the normal interface for lemma - return OutputChannel::lemma(lem, removable, preprocess, sendAtoms); -} - -bool ProofEngineOutputChannel::addTheoryLemmaStep(Node f) -{ - Assert(d_lazyPf != nullptr); - Assert(!f.isNull()); - std::vector children; - std::vector args; - args.push_back(f); - unsigned tid = static_cast(d_theory); - Node tidn = NodeManager::currentNM()->mkConst(Rational(tid)); - args.push_back(tidn); - // add the step, should always succeed; - return d_lazyPf->addStep(f, PfRule::THEORY_LEMMA, children, args); -} - -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/proof_engine_output_channel.h b/src/theory/proof_engine_output_channel.h deleted file mode 100644 index 1b1beb84d..000000000 --- a/src/theory/proof_engine_output_channel.h +++ /dev/null @@ -1,99 +0,0 @@ -/********************* */ -/*! \file proof_engine_output_channel.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The proof output channel class - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H -#define CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H - -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "theory/engine_output_channel.h" - -namespace CVC4 { - -class LazyCDProof; - -namespace theory { - -/** - * TODO: merge with engine output channel - * - * A layer on top of an output channel to ensure proofs are constructed and - * available for conflicts and lemmas that may require proofs. It is - * intended to be owned by TheoryEngine and passed as reference to each of - * its Theory solvers. Its use can be summarized in two parts: - * - * (1) Theory objects should use the output calls to methods in this class, - * e.g. trustedConflict(...), trustedLemma(...). - * - * (2) This class is responsible for adding proof steps to the provide proof - * object that correspond to steps. - * - * It is implemented by requiring that calls to conflict(...) provide an - * pointer to a proof generator object, as part of the TrustNode pair. - * - * In more detail, when a call to - * ProofOutputChannel::trustedConflict(TrustNode(conf, pfg)) - * is made - */ -class ProofEngineOutputChannel : public EngineOutputChannel -{ - typedef context::CDHashMap - NodeProofGenMap; - - public: - ProofEngineOutputChannel(TheoryEngine* engine, - theory::TheoryId theory, - LazyCDProof* lpf); - ~ProofEngineOutputChannel() {} - /** - * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method - * sends conf on the output channel of this class whose proof can be generated - * by the generator pfg. It stores the mapping - * getConflictKeyValue(conf) |-> pfg - * as a (lazy) step in the lazy proof object owned by this class. - */ - void trustedConflict(TrustNode pconf) override; - /** - * Let plem be the pair (Node lem, ProofGenerator * pfg). - * Send lem on the output channel of this class whose proof can be generated - * by the generator pfg. Apart from pfg, the interface for this method is - * the same as OutputChannel. It stores the mapping - * getLemmaKeyValue(lem) |-> pfg - * as a (lazy) step in the lazy proof object owned by this class. - */ - LemmaStatus trustedLemma(TrustNode plem, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) override; - - private: - /** Pointer to the lazy proof - * - * This object stores the mapping between formulas (conflicts or lemmas) - * and the proof generator provided for them. - */ - LazyCDProof* d_lazyPf; - /** - * Add coarse grained THEORY_LEMMA step for formula f that is the key of - * a lemma or conflict being sent out on the output channel of this class. - */ - bool addTheoryLemmaStep(Node f); -}; - -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__PROOF_OUTPUT_CHANNEL_H */ diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index ac27a5820..16afb0817 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -23,12 +23,11 @@ using namespace CVC4::theory; namespace CVC4 { -// below, proofs are enabled in d_pfee if we are provided a lazy proof SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm, - LazyCDProof* lcp) + bool pfEnabled) : ContextNotifyObj(context), d_statSharedTerms("theory::shared_terms", 0), d_addedSharedTermsSize(context, 0), @@ -37,11 +36,10 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, d_registeredEqualities(context), d_EENotify(*this), d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true), - d_pfee(context, userContext, d_equalityEngine, pnm, lcp != nullptr), + d_pfee(context, userContext, d_equalityEngine, pnm, pfEnabled), d_theoryEngine(theoryEngine), d_inConflict(context, false), - d_conflictPolarity(), - d_lazyPf(lcp) + d_conflictPolarity() { smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index a6e198d3c..88664544b 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -20,7 +20,6 @@ #include #include "context/cdhashset.h" -#include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof_node_manager.h" #include "theory/theory.h" @@ -163,7 +162,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm, - LazyCDProof* lcp); + bool pfEnabled); ~SharedTermsDatabase(); /** @@ -255,8 +254,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } protected: - /** Pointer to the lazy proof of TheoryEngine */ - LazyCDProof* d_lazyPf; /** * This method gets called on backtracks from the context manager. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7a1e34bef..ce9ac3da7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -204,7 +204,7 @@ TheoryEngine::TheoryEngine(context::Context* context, : nullptr), d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)), d_sharedTerms( - this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()), + this, context, userContext, d_pNodeManager.get(), d_lazyProof!=nullptr), d_masterEqualityEngine(nullptr), d_masterEENotify(*this), d_quantEngine(nullptr), @@ -1793,6 +1793,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } } + // FIXME + std::shared_ptr lcp; + if (d_lazyProof != nullptr) + { + Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node << std::endl; + lcp.reset(new LazyCDProof(d_pNodeManager.get())); + } + AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe @@ -1928,6 +1936,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); // FIXME: have ~( F ) and E => F, prove ~( E ) + if (d_lazyProof!=nullptr) + { + + } + Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index de4b17f8c..be5206461 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -38,13 +38,13 @@ #include "theory/atom_requests.h" #include "theory/decision_manager.h" #include "theory/interrupted.h" -#include "theory/proof_engine_output_channel.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" #include "theory/sort_inference.h" #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" #include "theory/theory.h" +#include "theory/engine_output_channel.h" #include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" @@ -256,10 +256,8 @@ class TheoryEngine { */ context::CDHashSet d_hasPropagated; - /** - * Output channels for individual theories. - */ - theory::ProofEngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; + /** Output channels for individual theories. */ + theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; /** * Are we in conflict. @@ -420,7 +418,7 @@ class TheoryEngine { { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = - new theory::ProofEngineOutputChannel(this, theoryId, d_lazyProof.get()); + new theory::EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 62213aade..8cb2a1f95 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -15,7 +15,6 @@ #include "theory/trust_node.h" #include "expr/proof_generator.h" -#include "theory/proof_engine_output_channel.h" namespace CVC4 { namespace theory { -- cgit v1.2.3 From bdf0df6cd504454669bc9a8c7057fcac00bf079b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 15:57:04 -0500 Subject: Format --- src/expr/proof.cpp | 4 +- src/expr/proof.h | 3 +- src/theory/engine_output_channel.cpp | 6 +-- src/theory/engine_output_channel.h | 3 +- src/theory/shared_terms_database.cpp | 2 +- src/theory/theory_engine.cpp | 56 ++++++++++++++++------------ src/theory/theory_engine.h | 12 +++--- src/theory/theory_engine_proof_generator.cpp | 23 ++++++------ src/theory/theory_engine_proof_generator.h | 23 +++++++----- 9 files changed, 74 insertions(+), 58 deletions(-) diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index dda2ccd2d..15e996684 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -384,8 +384,8 @@ bool CDProof::isAssumption(ProofNode* pn) bool CDProof::isSame(TNode f, TNode g) { return f == g - || (f.getKind() == EQUAL && g.getKind() == EQUAL - && f[0] == g[1] && f[1] == g[0]); + || (f.getKind() == EQUAL && g.getKind() == EQUAL && f[0] == g[1] + && f[1] == g[0]); } } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index 20bbb4996..2ff3604f8 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -206,12 +206,13 @@ class CDProof /** Get the proof manager for this proof */ ProofNodeManager* getManager() const; - /** + /** * Is same? Returns true if f and g are the same formula, or if they are * symmetric equalities. If two nodes f and g are the same, then a proof for * f suffices as a proof for g according to this class. */ static bool isSame(TNode f, TNode g); + protected: typedef context::CDHashMap, NodeHashFunction> NodeProofNodeMap; diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index b473ffc56..9e4e56543 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -308,9 +308,9 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) } LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, - bool removable, - bool preprocess, - bool sendAtoms) + bool removable, + bool preprocess, + bool sendAtoms) { Assert(plem.getKind() == TrustNodeKind::LEMMA); d_engine->processTrustNode(plem, d_theory); diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 1be4ec1d3..2d07d3f63 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -31,7 +31,7 @@ namespace theory { /** * An output channel for Theory that passes messages back to a TheoryEngine * for a given Theory. - * + * * Notice that is has interfaces trustedConflict and trustedLemma which are * used for ensuring that proof generators are associated with the lemmas * and conflicts sent on this output channel. @@ -87,6 +87,7 @@ class EngineOutputChannel : public theory::OutputChannel bool removable = false, bool preprocess = false, bool sendAtoms = false) override; + protected: /** * Statistics for a particular theory. diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 16afb0817..43950383b 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -27,7 +27,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm, - bool pfEnabled) + bool pfEnabled) : ContextNotifyObj(context), d_statSharedTerms("theory::shared_terms", 0), d_addedSharedTermsSize(context, 0), diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ce9ac3da7..982931d4a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -48,11 +48,11 @@ #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_engine_proof_generator.h" #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" #include "util/resource_manager.h" -#include "theory/theory_engine_proof_generator.h" using namespace std; @@ -202,9 +202,13 @@ TheoryEngine::TheoryEngine(context::Context* context, options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr), - d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)), - d_sharedTerms( - this, context, userContext, d_pNodeManager.get(), d_lazyProof!=nullptr), + d_tepg( + new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)), + d_sharedTerms(this, + context, + userContext, + d_pNodeManager.get(), + d_lazyProof != nullptr), d_masterEqualityEngine(nullptr), d_masterEENotify(*this), d_quantEngine(nullptr), @@ -1797,10 +1801,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, std::shared_ptr lcp; if (d_lazyProof != nullptr) { - Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node << std::endl; + Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node + << std::endl; lcp.reset(new LazyCDProof(d_pNodeManager.get())); } - + AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe @@ -1856,7 +1861,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } void TheoryEngine::processTrustNode(theory::TrustNode trn, - theory::TheoryId from) + theory::TheoryId from) { if (d_lazyProof == nullptr) { @@ -1876,7 +1881,7 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn, else { // all BUILTIN should be handled - Assert (from!=THEORY_BUILTIN); + Assert(from != THEORY_BUILTIN); // untrusted theory lemma std::vector children; std::vector args; @@ -1936,11 +1941,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); // FIXME: have ~( F ) and E => F, prove ~( E ) - if (d_lazyProof!=nullptr) + if (d_lazyProof != nullptr) { - } - Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; @@ -2040,7 +2043,8 @@ theory::TrustNode TheoryEngine::getExplanation( TrustNode simpleTrn; if (d_lazyProof != nullptr) { - Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl; + Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion + << std::endl; lcp.reset(new LazyCDProof(d_pNodeManager.get())); } unsigned i = 0; // Index of the current literal we are processing @@ -2073,7 +2077,8 @@ theory::TrustNode TheoryEngine::getExplanation( ++ i; if (lcp != nullptr) { - Trace("te-proof-exp") << "- explain " << toExplain.d_node << " trivially..." << std::endl; + Trace("te-proof-exp") + << "- explain " << toExplain.d_node << " trivially..." << std::endl; // ------------------MACRO_SR_PRED_INTRO // toExplain.d_node std::vector children; @@ -2111,7 +2116,8 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { - Trace("te-proof-exp") << "- AND expand " << toExplain.d_node << std::endl; + Trace("te-proof-exp") + << "- AND expand " << toExplain.d_node << std::endl; // toExplain.d_node[0] ... toExplain.d_node[n] // --------------------------------------------MACRO_SR_PRED_INTRO // toExplain.d_node @@ -2161,11 +2167,13 @@ theory::TrustNode TheoryEngine::getExplanation( } } }) - if (lcp !=nullptr) + if (lcp != nullptr) { - if (!CDProof::isSame(toExplain.d_node,(*find).second.d_node)) + if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node)) { - Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl; + Trace("te-proof-exp") + << "- t-explained cached: " << toExplain.d_node << " by " + << (*find).second.d_node << std::endl; // does this ever happen? Assert(false); simpleExplain = false; @@ -2194,7 +2202,9 @@ theory::TrustNode TheoryEngine::getExplanation( } if (lcp != nullptr) { - Trace("te-proof-exp") << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node << " by " << texplanation.getNode() << std::endl; + Trace("te-proof-exp") + << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node + << " by " << texplanation.getNode() << std::endl; // if not a trivial explanation if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node)) { @@ -2203,7 +2213,7 @@ theory::TrustNode TheoryEngine::getExplanation( // ---------------------------------MACRO_SR_PRED_TRANSFORM // lit Node proven = texplanation.getProven(); - if (texplanation.getGenerator()!=nullptr) + if (texplanation.getGenerator() != nullptr) { lcp->addLazyStep(proven, texplanation.getGenerator()); } @@ -2217,7 +2227,7 @@ theory::TrustNode TheoryEngine::getExplanation( unsigned tid = static_cast(toExplain.d_theory); Node tidn = NodeManager::currentNM()->mkConst(Rational(tid)); args.push_back(tidn); - lcp->addStep(proven,PfRule::THEORY_LEMMA,children,args); + lcp->addStep(proven, PfRule::THEORY_LEMMA, children, args); } std::vector children; children.push_back(proven); @@ -2320,12 +2330,12 @@ theory::TrustNode TheoryEngine::getExplanation( { // single call to a theory's explain method, skip the proof generator Assert (!simpleTrn.isNull()); - Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl; - return simpleTrn; + Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << + std::endl; return simpleTrn; } */ // store in the proof generator - TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp); + TrustNode trn = d_tepg->mkTrustExplain(conclusion, exp, lcp); // return the trust node return trn; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index be5206461..a5b9c393f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -37,6 +37,7 @@ #include "smt/command.h" #include "theory/atom_requests.h" #include "theory/decision_manager.h" +#include "theory/engine_output_channel.h" #include "theory/interrupted.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" @@ -44,7 +45,6 @@ #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" #include "theory/theory.h" -#include "theory/engine_output_channel.h" #include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" @@ -362,19 +362,18 @@ class TheoryEngine { bool preprocess, theory::TheoryId atomsTo); - /** + /** * Process trust node. This method ensures that the proof for the proven node * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained * by this class, referencing the proof generator of the trust node. The * argument from specifies the theory responsible for this trust node. If * no generator is provided, then a (eager) THEORY_LEMMA step is added to * the lazy proof. - * + * * @param trn The trust node to process * @param from The id of the theory responsible for the trust node. */ - void processTrustNode(theory::TrustNode trn, - theory::TheoryId from); + void processTrustNode(theory::TrustNode trn, theory::TheoryId from); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); @@ -417,8 +416,7 @@ class TheoryEngine { inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); - d_theoryOut[theoryId] = - new theory::EngineOutputChannel(this, theoryId); + d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index af737e53b..144fe0cc2 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -16,21 +16,22 @@ using namespace CVC4::kind; -namespace CVC4 -{ +namespace CVC4 { -TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u) : d_pnm(pnm), d_proofs(u) +TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, + context::UserContext* u) + : d_pnm(pnm), d_proofs(u) { - } -theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp, std::shared_ptr lpf) +theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( + TNode lit, Node exp, std::shared_ptr lpf) { - theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit,exp,this); + theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); Node p = trn.getProven(); // should not already be proven NodeLazyCDProofMap::iterator it = d_proofs.find(p); - if (it!=d_proofs.end()) + if (it != d_proofs.end()) { Assert(false); } @@ -44,16 +45,16 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) { - Assert (f.getKind()==IMPLIES && f.getNumChildren()==2); + Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2); NodeLazyCDProofMap::iterator it = d_proofs.find(f); - if (it==d_proofs.end()) + if (it == d_proofs.end()) { return nullptr; } std::shared_ptr lcp = (*it).second; // finalize it via scope std::vector scopeAssumps; - if (f[0].getKind()==AND) + if (f[0].getKind() == AND) { for (const Node& fc : f[0]) { @@ -78,4 +79,4 @@ std::string TheoryEngineProofGenerator::identify() const return "TheoryEngineProofGenerator"; } -} +} // namespace CVC4 diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 0dd6e0dd8..c81a2c09b 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -19,35 +19,40 @@ #include -#include "expr/lazy_proof.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_generator.h" #include "context/cdhashmap.h" #include "context/context.h" +#include "expr/lazy_proof.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" #include "theory/trust_node.h" namespace CVC4 { class TheoryEngineProofGenerator : public ProofGenerator { - typedef context::CDHashMap, NodeHashFunction> - NodeLazyCDProofMap; + typedef context:: + CDHashMap, NodeHashFunction> + NodeLazyCDProofMap; + public: TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); - ~TheoryEngineProofGenerator(){} + ~TheoryEngineProofGenerator() {} /** Set proof */ - theory::TrustNode mkTrustExplain(TNode lit, Node exp, std::shared_ptr lpf); + theory::TrustNode mkTrustExplain(TNode lit, + Node exp, + std::shared_ptr lpf); /** Get proof for */ std::shared_ptr getProofFor(Node f) override; /** Identify this generator (for debugging, etc..) */ std::string identify() const override; + private: /** The proof manager, used for allocating new ProofNode objects */ ProofNodeManager* d_pnm; /** Map from formulas to lazy CD proofs */ NodeLazyCDProofMap d_proofs; }; - -} + +} // namespace CVC4 #endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */ -- cgit v1.2.3 From afc01bf9df9a36b6c8f83ff9706cfa349da8d24a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 16:56:25 -0500 Subject: Connect explained conflicts --- src/theory/theory_engine.cpp | 22 +++++++++++++++++++--- src/theory/theory_engine_proof_generator.cpp | 2 ++ src/theory/trust_node.cpp | 2 +- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 982931d4a..3b6ffd6de 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1937,15 +1937,31 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); // Process the explanation - TrustNode tnc = getExplanation(vec, proofRecipe); + TrustNode tncExp = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); + Node fullConflict = tncExp.getNode(); - // FIXME: have ~( F ) and E => F, prove ~( E ) if (d_lazyProof != nullptr) { + if (fullConflict!=conflict) + { + // store the explicit step + processTrustNode(tncExp, THEORY_BUILTIN); + } + Node fullConflictNeg = fullConflict.notNode(); + // ------------------------- explained ---------- from theory + // fullConflict => conflict ~conflict + // ----------------------------------------------- MACRO_SR_PRED_TRANSFORM + // ~fullConflict + std::vector children; + children.push_back(tncExp.getProven()); + children.push_back(conflict.notNode()); + std::vector args; + args.push_back(fullConflictNeg); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); + d_lazyProof->addStep(fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } - Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 144fe0cc2..c11378e04 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -29,6 +29,7 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( { theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); Node p = trn.getProven(); + Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); // should not already be proven NodeLazyCDProofMap::iterator it = d_proofs.find(p); if (it != d_proofs.end()) @@ -45,6 +46,7 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) { + // should only ask this generator for proofs of implications Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2); NodeLazyCDProofMap::iterator it = d_proofs.find(f); if (it == d_proofs.end()) diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 8cb2a1f95..ff3e89154 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -83,7 +83,7 @@ ProofGenerator* TrustNode::getGenerator() const { return d_gen; } bool TrustNode::isNull() const { return d_proven.isNull(); } -Node TrustNode::getConflictProven(Node conf) { return conf.negate(); } +Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } Node TrustNode::getLemmaProven(Node lem) { return lem; } -- cgit v1.2.3