From 95bba975fd13261ca8854d9fb30d03fc7447eb80 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Sep 2020 11:11:48 -0500 Subject: [PATCH] Minor updates to theory inference manager (#5004) These updates are inspired by the current inference manager for sets. --- src/theory/datatypes/theory_datatypes.cpp | 14 ++++---- src/theory/inference_manager_buffered.cpp | 5 ++- src/theory/theory_inference_manager.cpp | 42 ++++++++++++++--------- src/theory/theory_inference_manager.h | 31 +++++++++++------ 4 files changed, 55 insertions(+), 37 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 78b6d81c2..5253414a9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -170,7 +170,7 @@ void TheoryDatatypes::postCheck(Effort level) return; } else if (level == EFFORT_FULL && !d_state.isInConflict() - && !d_im.hasAddedLemma() && !d_valuation.needCheck()) + && !d_im.hasSentLemma() && !d_valuation.needCheck()) { //check for cycles Assert(!d_im.hasPendingFact()); @@ -180,11 +180,11 @@ void TheoryDatatypes::postCheck(Effort level) checkCycles(); Trace("datatypes-proc") << "...finish check cycles" << std::endl; d_im.process(); - if (d_state.isInConflict() || d_im.hasAddedLemma()) + if (d_state.isInConflict() || d_im.hasSentLemma()) { return; } - } while (d_im.hasAddedFact()); + } while (d_im.hasSentFact()); //check for splits Trace("datatypes-debug") << "Check for splits " << endl; @@ -329,7 +329,7 @@ void TheoryDatatypes::postCheck(Effort level) } ++eqcs_i; } - if (d_im.hasAddedLemma()) + if (d_im.hasSentLemma()) { // clear pending facts: we added a lemma, so internal inferences are // no longer necessary @@ -342,11 +342,11 @@ void TheoryDatatypes::postCheck(Effort level) Trace("datatypes-debug") << "Flush pending facts..." << std::endl; d_im.process(); } - } while (!d_state.isInConflict() && !d_im.hasAddedLemma() - && d_im.hasAddedFact()); + } while (!d_state.isInConflict() && !d_im.hasSentLemma() + && d_im.hasSentFact()); Trace("datatypes-debug") << "Finished, conflict=" << d_state.isInConflict() - << ", lemmas=" << d_im.hasAddedLemma() << std::endl; + << ", lemmas=" << d_im.hasSentLemma() << std::endl; if (!d_state.isInConflict()) { Trace("dt-model-debug") << std::endl; diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 8d7dd2abc..8a7713121 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -76,8 +76,7 @@ void InferenceManagerBuffered::addPendingFact( void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol) { - // must ensure rewritten - lit = Rewriter::rewrite(lit); + // it is the responsibility of the caller to ensure lit is rewritten d_pendingReqPhase[lit] = pol; } @@ -109,7 +108,7 @@ void InferenceManagerBuffered::doPendingPhaseRequirements() // process the pending require phase calls for (const std::pair& prp : d_pendingReqPhase) { - d_out.requirePhase(prp.first, prp.second); + requirePhase(prp.first, prp.second); } d_pendingReqPhase.clear(); } diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 3abe530f1..9405a8162 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -221,41 +221,41 @@ bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) return d_lemmasSent.find(lem) != d_lemmasSent.end(); } -uint32_t TheoryInferenceManager::numAddedLemmas() const +uint32_t TheoryInferenceManager::numSentLemmas() const { return d_numCurrentLemmas; } -bool TheoryInferenceManager::hasAddedLemma() const +bool TheoryInferenceManager::hasSentLemma() const { return d_numCurrentLemmas != 0; } -void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp) +bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp) { - processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr); + return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr); } -void TheoryInferenceManager::assertInternalFact(TNode atom, +bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, const std::vector& args) { Assert(id != PfRule::UNKNOWN); - processInternalFact(atom, pol, id, exp, args, nullptr); + return processInternalFact(atom, pol, id, exp, args, nullptr); } -void TheoryInferenceManager::assertInternalFact(TNode atom, +bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, const std::vector& exp, ProofGenerator* pg) { Assert(pg != nullptr); - processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg); + return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg); } -void TheoryInferenceManager::processInternalFact(TNode atom, +bool TheoryInferenceManager::processInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, @@ -267,8 +267,9 @@ void TheoryInferenceManager::processInternalFact(TNode atom, // call the pre-notify fact method with preReg = false, isInternal = true if (d_theory.preNotifyFact(atom, pol, expn, false, true)) { - // handled in a theory-specific way that doesn't require equality engine - return; + // Handled in a theory-specific way that doesn't require equality engine, + // notice we return true, indicating that the fact was processed. + return true; } Assert(d_ee != nullptr); Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: " @@ -276,15 +277,16 @@ void TheoryInferenceManager::processInternalFact(TNode atom, d_numCurrentFacts++; // Now, assert the fact. How to do so depends on whether proofs are enabled. // If no proof production, or no proof rule was given + bool ret = false; if (d_pfee == nullptr || id == PfRule::UNKNOWN) { if (atom.getKind() == kind::EQUAL) { - d_ee->assertEquality(atom, pol, expn); + ret = d_ee->assertEquality(atom, pol, expn); } else { - d_ee->assertPredicate(atom, pol, expn); + ret = d_ee->assertPredicate(atom, pol, expn); } // Must reference count the equality and its explanation, which is not done // by the equality engine. Notice that we do *not* need to do this for @@ -304,18 +306,19 @@ void TheoryInferenceManager::processInternalFact(TNode atom, if (pg != nullptr) { // use the proof generator interface - d_pfee->assertFact(lit, expn, pg); + ret = d_pfee->assertFact(lit, expn, pg); } else { // use the explict proof step interface - d_pfee->assertFact(lit, id, expn, args); + ret = d_pfee->assertFact(lit, id, expn, args); } } // call the notify fact method with isInternal = true d_theory.notifyFact(atom, pol, expn, true); Trace("infer-manager") << "TheoryInferenceManager::finished assertInternalFact" << std::endl; + return ret; } void TheoryInferenceManager::explain(TNode n, std::vector& assumptions) @@ -361,12 +364,12 @@ Node TheoryInferenceManager::mkExplainPartial( return NodeManager::currentNM()->mkAnd(assumps); } -uint32_t TheoryInferenceManager::numAddedFacts() const +uint32_t TheoryInferenceManager::numSentFacts() const { return d_numCurrentFacts; } -bool TheoryInferenceManager::hasAddedFact() const +bool TheoryInferenceManager::hasSentFact() const { return d_numCurrentFacts != 0; } @@ -381,5 +384,10 @@ bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p) return true; } +void TheoryInferenceManager::requirePhase(TNode n, bool pol) +{ + return d_out.requirePhase(n, pol); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 2ddcd0985..7e5ef6dec 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -214,9 +214,9 @@ class TheoryInferenceManager */ virtual bool hasCachedLemma(TNode lem, LemmaProperty p); /** The number of lemmas we have sent since the last call to reset */ - uint32_t numAddedLemmas() const; + uint32_t numSentLemmas() const; /** Have we added a lemma since the last call to reset? */ - bool hasAddedLemma() const; + bool hasSentLemma() const; //--------------------------------------- internal facts /** * Assert internal fact. This is recommended method for asserting "internal" @@ -229,8 +229,10 @@ class TheoryInferenceManager * @param atom The atom of the fact to assert * @param pol Its polarity * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid. + * @return true if the fact was processed, i.e. it was asserted to the + * equality engine or preNotifyFact returned true. */ - void assertInternalFact(TNode atom, bool pol, TNode exp); + bool assertInternalFact(TNode atom, bool pol, TNode exp); /** * Assert internal fact, with a proof step justification. Notice that if * proofs are not enabled in this inference manager, then this asserts @@ -241,8 +243,10 @@ class TheoryInferenceManager * @param id The proof rule identifier of the proof step * @param exp Its explanation, interpreted as a conjunction * @param args The arguments of the proof step + * @return true if the fact was processed, i.e. it was asserted to the + * equality engine or preNotifyFact returned true. */ - void assertInternalFact(TNode atom, + bool assertInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, @@ -257,22 +261,29 @@ class TheoryInferenceManager * @param pg The proof generator for this step. If non-null, pg must be able * to provide a proof concluding (~) atom from free asumptions in exp in * the remainder of the current SAT context. + * @return true if the fact was processed, i.e. it was asserted to the + * equality engine or preNotifyFact returned true. */ - void assertInternalFact(TNode atom, + bool assertInternalFact(TNode atom, bool pol, const std::vector& exp, ProofGenerator* pg); /** The number of internal facts we have added since the last call to reset */ - uint32_t numAddedFacts() const; + uint32_t numSentFacts() const; /** Have we added a internal fact since the last call to reset? */ - bool hasAddedFact() const; - + bool hasSentFact() const; + //--------------------------------------- phase requirements + /** + * Set that literal n has SAT phase requirement pol, that is, it should be + * decided with polarity pol, for details see OutputChannel::requirePhase. + */ + void requirePhase(TNode n, bool pol); protected: /** * Process internal fact. This is a common helper method for the - * assertInternalFact variants above. + * assertInternalFact variants above. Returns true if the fact was processed. */ - void processInternalFact(TNode atom, + bool processInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, -- 2.30.2