diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 10:11:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 10:11:03 -0500 |
commit | 929610135bfdce0aca858821e0862759f45386cd (patch) | |
tree | 9cdf5f4e541d37c0c215fe5b8225a882c8bf7b7b /src | |
parent | b2eb6967b632de8ecd863f733c1a5392136753e9 (diff) |
Equality engine interface
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 17 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 6 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 43 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.h | 2 |
6 files changed, 49 insertions, 32 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 102e8b27d..3eaf2c17d 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -42,6 +42,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) { Trace("strings-ipc-debug") << "InferProofCons::notifyFact: " << ii << std::endl; + if (d_lazyFactMap.find(ii.d_conc)!=d_lazyFactMap.end()) + { + Trace("strings-ipc-debug") << "...duplicate!" << std::endl; + return; + } std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii); d_lazyFactMap.insert(ii.d_conc, iic); } diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index f64aba521..33f4c8f67 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -348,11 +348,13 @@ void InferenceManager::doPendingFacts() preProcessFact(fact); if (!d_recExplain) { - // notify fact - d_ipc->notifyFact(ii); // assert to equality engine using proof generator interface for // assertFact. - d_pfee->assertFact(fact, cexp, d_ipc.get()); + if (d_pfee->assertFact(fact, cexp, d_ipc.get())) + { + // notify fact if the above call asserted a new fact + d_ipc->notifyFact(ii); + } } else { diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 00ddcbf68..56f081151 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -459,8 +459,14 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un void 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"; - assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); + TNode b = polarity ? d_true : d_false; + if (hasTerm(t) && areEqual(t,b)) + { + return false; + } + assertEqualityInternal(t, b, reason, pid); propagate(); + return true; } void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { @@ -468,7 +474,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig if (polarity) { // If two terms are already equal, don't assert anything if (hasTerm(eq[0]) && hasTerm(eq[1]) && areEqual(eq[0], eq[1])) { - return; + return false; } // Add equality between terms assertEqualityInternal(eq[0], eq[1], reason, pid); @@ -476,7 +482,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig } else { // If two terms are already dis-equal, don't assert anything if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) { - return; + return false; } // notify the theory @@ -490,7 +496,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig propagate(); if (d_done) { - return; + return true; } // If both have constant representatives, we don't notify anyone @@ -499,7 +505,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig EqualityNodeId aClassId = getEqualityNode(a).getFind(); EqualityNodeId bClassId = getEqualityNode(b).getFind(); if (d_isConstant[aClassId] && d_isConstant[bClassId]) { - return; + return true; } // If we are adding a disequality, notify of the shared term representatives @@ -551,6 +557,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig } } } + return true; } TNode EqualityEngine::getRepresentative(TNode t) const { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 366a986db..5d6801c7b 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -809,8 +809,9 @@ public: * @param polarity true if asserting the predicate, false if * asserting the negated predicate * @param reason the reason to keep for building explanations + * @return true if a new fact was asserted, false if this call was a no-op. */ - void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); + bool assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Adds an equality eq with the given polarity to the database. @@ -819,8 +820,9 @@ public: * @param polarity true if asserting the equality, false if * asserting the negated equality * @param reason the reason to keep for building explanations + * @return true if a new fact was asserted, false if this call was a no-op. */ - void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); + bool assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Returns the current representative of the term t. diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index b2bf09219..6838c9568 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -54,13 +54,9 @@ bool ProofEqEngine::assertAssume(TNode lit) // explanation. Notice we do not reference count atom/lit. if (atom.getKind() == EQUAL) { - d_ee.assertEquality(atom, polarity, lit); + return d_ee.assertEquality(atom, polarity, lit); } - else - { - d_ee.assertPredicate(atom, polarity, lit); - } - return true; + return d_ee.assertPredicate(atom, polarity, lit); } bool ProofEqEngine::assertFact(Node lit, @@ -82,8 +78,7 @@ bool ProofEqEngine::assertFact(Node lit, // second, assert it to the equality engine Node reason = mkAnd(exp); - assertFactInternal(atom, polarity, reason); - return true; + return assertFactInternal(atom, polarity, reason); } bool ProofEqEngine::assertFact(Node lit, @@ -107,8 +102,7 @@ bool ProofEqEngine::assertFact(Node lit, bool polarity = lit.getKind() != NOT; // second, assert it to the equality engine - assertFactInternal(atom, polarity, exp); - return true; + return assertFactInternal(atom, polarity, exp); } bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb) @@ -125,8 +119,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb) bool polarity = lit.getKind() != NOT; // second, assert it to the equality engine - assertFactInternal(atom, polarity, exp); - return true; + return assertFactInternal(atom, polarity, exp); } bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg) @@ -141,8 +134,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg) Node atom = lit.getKind() == NOT ? lit[0] : lit; bool polarity = lit.getKind() != NOT; // second, assert it to the equality engine - assertFactInternal(atom, polarity, exp); - return true; + return assertFactInternal(atom, polarity, exp); } TrustNode ProofEqEngine::assertConflict(Node lit) @@ -464,7 +456,11 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, std::stringstream ss; pfConc->printDebug(ss); ss << std::endl << "Free assumption: " << a << std::endl; - AlwaysAssert(false) << "Generated a non-closed proof: " << ss.str() + 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()) @@ -563,21 +559,26 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, return TrustNode::null(); } -void ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason) +bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason) { Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity << " " << reason << std::endl; + bool ret; if (atom.getKind() == EQUAL) { - d_ee.assertEquality(atom, polarity, reason); + ret = d_ee.assertEquality(atom, polarity, reason); } else { - d_ee.assertPredicate(atom, polarity, reason); + ret = d_ee.assertPredicate(atom, polarity, reason); + } + if (ret) + { + // must reference count the new atom and explanation + d_keep.insert(atom); + d_keep.insert(reason); } - // must reference count the new atom and explanation - d_keep.insert(atom); - d_keep.insert(reason); + return ret; } bool ProofEqEngine::addProofStep(Node lit, diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 983aec708..9c18eeb25 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -164,7 +164,7 @@ class ProofEqEngine : public EagerProofGenerator const std::vector<Node>& exp, const std::vector<Node>& args); /** Assert internal */ - void assertFactInternal(TNode pred, bool polarity, TNode reason); + bool assertFactInternal(TNode pred, bool polarity, TNode reason); /** assert lemma internal */ TrustNode assertLemmaInternal(Node conc, const std::vector<Node>& exp, |