From d972bd973320ed3b4c7a41ff6a16e76f754d7f58 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 3 Oct 2020 06:11:02 -0500 Subject: [PATCH] Standardization of Theory (#5181) This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo. --- src/theory/arith/congruence_manager.cpp | 4 -- src/theory/arith/congruence_manager.h | 3 - src/theory/arith/theory_arith.cpp | 7 +- src/theory/arith/theory_arith.h | 2 +- src/theory/arith/theory_arith_private.cpp | 1 - src/theory/arrays/theory_arrays.cpp | 1 - src/theory/bv/theory_bv.cpp | 5 -- src/theory/fp/theory_fp.cpp | 7 +- src/theory/fp/theory_fp.h | 3 +- src/theory/model_manager_distributed.cpp | 7 +- src/theory/sets/theory_sets_private.cpp | 1 - src/theory/strings/theory_strings.cpp | 1 - src/theory/theory.cpp | 85 +++++------------------ src/theory/theory.h | 47 ++++--------- src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 2 +- test/unit/theory/theory_engine_white.h | 1 - 17 files changed, 47 insertions(+), 132 deletions(-) diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 465128b1b..f2db70d90 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -477,10 +477,6 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ d_ee->assertEquality(eq, true, reason); } -void ArithCongruenceManager::addSharedTerm(Node x){ - d_ee->addTriggerTerm(x, THEORY_ARITH); -} - bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; } std::vector andComponents(TNode an) diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 6115fec8a..44a2b9df6 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -217,9 +217,6 @@ public: void equalsConstant(ConstraintCP eq); void equalsConstant(ConstraintCP lb, ConstraintCP ub); - - void addSharedTerm(Node x); - private: class Statistics { public: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 434d2e1c8..bddc8ebcc 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -219,12 +219,9 @@ void TheoryArith::propagate(Effort e) { d_internal->propagate(e); } -bool TheoryArith::collectModelInfo(TheoryModel* m) +bool TheoryArith::collectModelInfo(TheoryModel* m, + const std::set& termSet) { - std::set termSet; - // Work out which variables are needed - const std::set& irrKinds = m->getIrrelevantKinds(); - computeAssertedTerms(termSet, irrKinds); // this overrides behavior to not assert equality engine return collectModelValues(m, termSet); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 8555156a5..6b279c9ed 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -91,7 +91,7 @@ class TheoryArith : public Theory { void propagate(Effort e) override; TrustNode explain(TNode n) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelInfo(TheoryModel* m, const std::set& termSet) override; /** * Collect model values in m based on the relevant terms given by termSet. */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 557072319..bb6ab0b9c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1076,7 +1076,6 @@ void TheoryArithPrivate::notifySharedTerm(TNode n) if(n.isConst()){ d_partialModel.invalidateDelta(); } - d_congruenceManager.addSharedTerm(n); if(!n.isConst() && !isSetup(n)){ Polynomial poly = Polynomial::parsePolynomial(n); Polynomial::iterator it = poly.begin(); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 5dee75a6c..3270c1c07 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -852,7 +852,6 @@ void TheoryArrays::notifySharedTerm(TNode t) Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::notifySharedTerm(" << t << ")" << std::endl; - d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS); if (t.getType().isArray()) { d_sharedArrays.insert(t); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 857d4d6fb..79a20c9c9 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -209,11 +209,6 @@ TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); } void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); - // temporary, will be built into Theory::addSharedTerm - if (d_equalityEngine != nullptr) - { - d_equalityEngine->addTriggerTerm(t, THEORY_BV); - } } void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 863f9a5a6..037b083f4 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -1019,12 +1019,9 @@ Node TheoryFp::getModelValue(TNode var) { return d_conv.getValue(d_valuation, var); } -bool TheoryFp::collectModelInfo(TheoryModel* m) +bool TheoryFp::collectModelInfo(TheoryModel* m, + const std::set& relevantTerms) { - std::set relevantTerms; - // Work out which variables are needed - const std::set& irrKinds = m->getIrrelevantKinds(); - computeAssertedTerms(relevantTerms, irrKinds); // this override behavior to not assert equality engine return collectModelValues(m, relevantTerms); } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 16d984011..42c009893 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -75,7 +75,8 @@ class TheoryFp : public Theory { //--------------------------------- end standard check Node getModelValue(TNode var) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelInfo(TheoryModel* m, + const std::set& relevantTerms) override; /** Collect model values in m based on the relevant terms given by * relevantTerms */ bool collectModelValues(TheoryModel* m, diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 5ea2799c5..7d121af53 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -78,7 +78,12 @@ bool ModelManagerDistributed::prepareModel() Theory* t = d_te.theoryOf(theoryId); Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << std::endl; - if (!t->collectModelInfo(d_model)) + // collect the asserted terms + std::set termSet; + collectAssertedTerms(theoryId, termSet); + // also get relevant terms + t->computeRelevantTerms(termSet); + if (!t->collectModelInfo(d_model, termSet)) { Trace("model-builder") << "ModelManagerDistributed: fail collect model info" << std::endl; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 1a0b1b1e2..51f49ad1d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1275,7 +1275,6 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) d_equalityEngine->addTriggerPredicate(node); } break; - case kind::CARD: d_equalityEngine->addTriggerTerm(node, THEORY_SETS); break; default: d_equalityEngine->addTerm(node); break; } } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 309b85503..0375fd311 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -163,7 +163,6 @@ void TheoryStrings::notifySharedTerm(TNode t) { Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " " << t.getType().isBoolean() << endl; - d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS); if (options::stringExp()) { d_esolver.addSharedTerm(t); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index cdcec52e3..2a471ec0d 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -273,13 +273,7 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) void Theory::notifySharedTerm(TNode n) { - // TODO (project #39): this will move to addSharedTerm, as every theory with - // an equality does this in their notifySharedTerm method. - // if we have an equality engine, add the trigger term - if (d_equalityEngine != nullptr) - { - d_equalityEngine->addTriggerTerm(n, d_id); - } + // do nothing } void Theory::computeCareGraph() { @@ -357,18 +351,8 @@ std::unordered_set Theory::currentlySharedTerms() cons return currentlyShared; } -bool Theory::collectModelInfo(TheoryModel* m) +bool Theory::collectModelInfo(TheoryModel* m, const std::set& termSet) { - // NOTE: the computation of termSet will be moved to model manager - // and passed as an argument to collectModelInfo. - std::set termSet; - // Compute terms appearing in assertions and shared terms - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); - const std::set& irrKinds = tm->getIrrelevantKinds(); - computeAssertedTerms(termSet, irrKinds, true); - // Compute additional relevant terms (theory-specific) - computeRelevantTerms(termSet); // if we are using an equality engine, assert it to the model if (d_equalityEngine != nullptr) { @@ -381,54 +365,6 @@ bool Theory::collectModelInfo(TheoryModel* m) return collectModelValues(m, termSet); } -void Theory::collectTerms(TNode n, - const std::set& irrKinds, - set& termSet) const -{ - if (termSet.find(n) != termSet.end()) { - return; - } - Kind nk = n.getKind(); - if (irrKinds.find(nk) == irrKinds.end()) - { - Trace("theory::collectTerms") - << "Theory::collectTerms: adding " << n << endl; - termSet.insert(n); - } - if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n)) - { - for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - collectTerms(*child_it, irrKinds, termSet); - } - } -} - -void Theory::computeAssertedTerms(std::set& termSet, - const std::set& irrKinds, - bool includeShared) const -{ - // Collect all terms appearing in assertions - context::CDList::const_iterator assert_it = facts_begin(), - assert_it_end = facts_end(); - for (; assert_it != assert_it_end; ++assert_it) - { - collectTerms(*assert_it, irrKinds, termSet); - } - - if (!includeShared) - { - return; - } - // Add terms that are shared terms - std::set kempty; - context::CDList::const_iterator shared_it = shared_terms_begin(), - shared_it_end = shared_terms_end(); - for (; shared_it != shared_it_end; ++shared_it) - { - collectTerms(*shared_it, kempty, termSet); - } -} - void Theory::computeRelevantTerms(std::set& termSet) { // by default, there are no additional relevant terms @@ -532,18 +468,24 @@ void Theory::check(Effort level) // standard calls for resource, stats d_out->spendResource(ResourceManager::Resource::TheoryCheckStep); TimerStat::CodeTimer checkTimer(d_checkTime); + Trace("theory-check") << "Theory::preCheck " << level << " " << d_id + << std::endl; // pre-check at level if (preCheck(level)) { // check aborted for a theory-specific reason return; } + Assert(d_theoryState != nullptr); + Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl; // process the pending fact queue while (!done() && !d_theoryState->isInConflict()) { // Get the next assertion from the fact queue Assertion assertion = get(); TNode fact = assertion.d_assertion; + Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id + << std::endl; bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; // call the pre-notify method @@ -552,6 +494,8 @@ void Theory::check(Effort level) // handled in theory-specific way that doesn't involve equality engine continue; } + Trace("theory-check") << "Theory::assert " << fact << " " << d_id + << std::endl; // Theories that don't have an equality engine should always return true // for preNotifyFact Assert(d_equalityEngine != nullptr); @@ -564,11 +508,15 @@ void Theory::check(Effort level) { d_equalityEngine->assertPredicate(atom, polarity, fact); } + Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id + << std::endl; // notify the theory of the new fact, which is not internal notifyFact(atom, polarity, fact, false); } + Trace("theory-check") << "Theory::postCheck " << d_id << std::endl; // post-check at level postCheck(level); + Trace("theory-check") << "Theory::finish check " << d_id << std::endl; } bool Theory::preCheck(Effort level) { return false; } @@ -596,6 +544,11 @@ void Theory::addSharedTerm(TNode n) d_sharedTerms.push_back(n); // now call theory-specific method notifySharedTerm notifySharedTerm(n); + // if we have an equality engine, add the trigger term + if (d_equalityEngine != nullptr) + { + d_equalityEngine->addTriggerTerm(n, d_id); + } } eq::EqualityEngine* Theory::getEqualityEngine() diff --git a/src/theory/theory.h b/src/theory/theory.h index bc6c995a7..6f6c863df 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -179,15 +179,6 @@ class Theory { */ context::CDList d_sharedTerms; - //---------------------------------- private collect model info - /** - * Helper function for computeRelevantTerms - */ - void collectTerms(TNode n, - const std::set& irrKinds, - std::set& termSet) const; - //---------------------------------- end private collect model info - /** * Construct a Theory. * @@ -491,6 +482,16 @@ class Theory { /** Get the decision manager associated to this theory. */ DecisionManager* getDecisionManager() { return d_decManager; } + /** + * @return The theory state associated with this theory. + */ + TheoryState* getTheoryState() { return d_theoryState; } + + /** + * @return The theory inference manager associated with this theory. + */ + TheoryInferenceManager* getInferenceManager() { return d_inferManager; } + /** * Expand definitions in the term node. This returns a term that is * equivalent to node. It wraps this term in a TrustNode of kind @@ -600,11 +601,8 @@ class Theory { * * Theories that use this check method must use an official theory * state object (d_theoryState). - * - * TODO (project #39): this method should be non-virtual, once all theories - * conform to the new standard */ - virtual void check(Effort level = EFFORT_FULL); + void check(Effort level = EFFORT_FULL); /** * Pre-check, called before the fact queue of the theory is processed. * If this method returns false, then the theory will process its fact @@ -662,28 +660,9 @@ class Theory { * then calls computeModelValues. * * TODO (project #39): this method should be non-virtual, once all theories - * conform to the new standard - */ - virtual bool collectModelInfo(TheoryModel* m); - /** - * Scans the current set of assertions and shared terms top-down - * until a theory-leaf is reached, and adds all terms found to - * termSet. This is used by collectModelInfo to delimit the set of - * terms that should be used when constructing a model. - * - * @param irrKinds The kinds of terms that appear in assertions that should *not* - * be included in termSet. Note that the kinds EQUAL and NOT are always - * treated as irrelevant kinds. - * - * @param includeShared Whether to include shared terms in termSet. Notice that - * shared terms are not influenced by irrKinds. - * - * TODO (project #39): this method will be deleted. The version in - * model manager will be used. + * conform to the new standard, delete, move to model manager distributed. */ - void computeAssertedTerms(std::set& termSet, - const std::set& irrKinds, - bool includeShared = true) const; + virtual bool collectModelInfo(TheoryModel* m, const std::set& termSet); /** * Compute terms that are not necessarily part of the assertions or * shared terms that should be considered relevant, add them to termSet. diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 94477d1e8..2d0a80599 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -444,7 +444,7 @@ bool TheoryModel::assertPredicate(TNode a, bool polarity) /** assert equality engine */ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, - set* termSet) + const std::set* termSet) { Assert(d_equalityEngine->consistent()); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 00b2107bd..b1401c074 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -110,7 +110,7 @@ public: * is consistent after asserting the equality engine to this model. */ bool assertEqualityEngine(const eq::EqualityEngine* ee, - std::set* termSet = NULL); + const std::set* termSet = NULL); /** assert skeleton * * This method gives a "skeleton" for the model value of the equivalence diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 39849da3a..8a99946e5 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -151,7 +151,6 @@ class FakeTheory : public Theory void preRegisterTerm(TNode) override { Unimplemented(); } void registerTerm(TNode) { Unimplemented(); } - void check(Theory::Effort) override { Unimplemented(); } void propagate(Theory::Effort) override { Unimplemented(); } TrustNode explain(TNode) override { -- 2.30.2