From 7b3b19f73ceb2168ced48d07a590c0f3be82a8d4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 31 Aug 2020 14:24:27 -0500 Subject: [PATCH] Simplify interface for computing relevant terms. (#4966) This is a followup to #4945 which simplifies the contract for computeRelevantTerms. --- src/theory/arith/theory_arith_private.cpp | 4 +- src/theory/arrays/theory_arrays.cpp | 23 +++-------- src/theory/arrays/theory_arrays.h | 8 ++-- src/theory/bv/bitblast/lazy_bitblaster.cpp | 3 +- src/theory/bv/bv_subtheory_algebraic.cpp | 3 +- src/theory/bv/bv_subtheory_core.cpp | 3 +- src/theory/datatypes/theory_datatypes.cpp | 23 ++--------- src/theory/datatypes/theory_datatypes.h | 10 ++--- src/theory/fp/theory_fp.cpp | 3 +- src/theory/sets/theory_sets.cpp | 5 ++- src/theory/sets/theory_sets.h | 3 +- src/theory/sets/theory_sets_private.cpp | 12 +----- src/theory/sets/theory_sets_private.h | 2 +- src/theory/strings/theory_strings.cpp | 3 +- src/theory/theory.cpp | 22 ++++++----- src/theory/theory.h | 46 +++++++++++----------- 16 files changed, 73 insertions(+), 100 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 8ca99d369..9a8ca733a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4140,8 +4140,8 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; std::set termSet; - d_containing.computeRelevantTerms(termSet); - + const std::set& irrKinds = m->getIrrelevantKinds(); + d_containing.computeAssertedTerms(termSet, irrKinds, true); // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b4a234748..3adcd4f49 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1090,19 +1090,11 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// -bool TheoryArrays::collectModelInfo(TheoryModel* m) +bool TheoryArrays::collectModelValues(TheoryModel* m, + const std::set& termSet) { - // Compute terms appearing in assertions and shared terms, and also - // include additional reads due to the RIntro1 and RIntro2 rules. - std::set termSet; - computeRelevantTerms(termSet); - - // Send the equality engine information to the model - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - return false; - } - + // termSet contains terms appearing in assertions and shared terms, and also + // includes additional reads due to the RIntro1 and RIntro2 rules. NodeManager* nm = NodeManager::currentNM(); // Compute arrays that we need to produce representatives for std::vector arrays; @@ -2263,13 +2255,8 @@ TrustNode TheoryArrays::expandDefinition(Node node) return TrustNode::null(); } -void TheoryArrays::computeRelevantTerms(std::set& termSet, - bool includeShared) +void TheoryArrays::computeRelevantTerms(std::set& termSet) { - // include all standard terms - std::set irrKinds; - computeRelevantTermsInternal(termSet, irrKinds, includeShared); - NodeManager* nm = NodeManager::currentNM(); // make sure RIntro1 reads are included in the relevant set of reads eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 8cbf826c1..9044b9950 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -264,7 +264,8 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// public: - bool collectModelInfo(TheoryModel* m) override; + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -480,11 +481,10 @@ class TheoryArrays : public Theory { Node getNextDecisionRequest(); /** - * Compute relevant terms. This includes additional select nodes for the + * Compute relevant terms. This includes select nodes for the * RIntro1 and RIntro2 rules. */ - void computeRelevantTerms(std::set& termSet, - bool includeShared = true) override; + void computeRelevantTerms(std::set& termSet) override; };/* class TheoryArrays */ }/* CVC4::theory::arrays namespace */ diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index c3a305952..83e286f10 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -540,7 +540,8 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { std::set termSet; - d_bv->computeRelevantTerms(termSet); + const std::set& irrKinds = m->getIrrelevantKinds(); + d_bv->computeAssertedTerms(termSet, irrKinds, true); for (std::set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { TNode var = *it; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e5a416a1b..80a6aeb86 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -715,7 +715,8 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n"; AlwaysAssert(!d_quickSolver->inConflict()); set termSet; - d_bv->computeRelevantTerms(termSet); + const std::set& irrKinds = model->getIrrelevantKinds(); + d_bv->computeAssertedTerms(termSet, irrKinds, true); // collect relevant terms that the bv theory abstracts to variables // (variables and parametric terms such as select apply_uf) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index d8f376a74..38c5cb482 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -354,7 +354,8 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) } } set termSet; - d_bv->computeRelevantTerms(termSet); + const std::set& irrKinds = m->getIrrelevantKinds(); + d_bv->computeAssertedTerms(termSet, irrKinds, true); if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) { return false; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a98c77a5d..4c8fa87ba 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1483,7 +1483,8 @@ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; } -bool TheoryDatatypes::collectModelInfo(TheoryModel* m) +bool TheoryDatatypes::collectModelValues(TheoryModel* m, + const std::set& termSet) { Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine->consistent() << std::endl; @@ -1491,17 +1492,6 @@ bool TheoryDatatypes::collectModelInfo(TheoryModel* m) printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; - std::set termSet; - - // Compute terms appearing in assertions and shared terms, and in inferred equalities - computeRelevantTerms(termSet); - - //combine the equality engine - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - return false; - } - //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator(d_equalityEngine); std::vector< Node > cons; @@ -2218,15 +2208,8 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { } } -void TheoryDatatypes::computeRelevantTerms(std::set& termSet, - bool includeShared) +void TheoryDatatypes::computeRelevantTerms(std::set& termSet) { - // Compute terms appearing in assertions and shared terms - std::set irrKinds; - // testers are not relevant for model construction - irrKinds.insert(APPLY_TESTER); - computeRelevantTermsInternal(termSet, irrKinds, includeShared); - Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..." << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 0d5df098d..211653125 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -288,7 +288,8 @@ private: TrustNode ppRewrite(TNode n) override; void notifySharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; void shutdown() override {} std::string identify() const override { @@ -347,11 +348,10 @@ private: TNode getRepresentative( TNode a ); /** - * Compute relevant terms. In addition to all terms in assertions and shared - * terms, this includes datatypes in non-singleton equivalence classes. + * Compute relevant terms. This includes datatypes in non-singleton + * equivalence classes. */ - void computeRelevantTerms(std::set& termSet, - bool includeShared = true) override; + void computeRelevantTerms(std::set& termSet) override; /** sygus symmetry breaking utility */ std::unique_ptr d_sygusExtension; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 4c59b1c06..5eb9e576d 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -1023,7 +1023,8 @@ bool TheoryFp::collectModelInfo(TheoryModel* m) { std::set relevantTerms; // Work out which variables are needed - computeRelevantTerms(relevantTerms); + 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/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 63ebacc23..0bf2ed2ea 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -98,9 +98,10 @@ void TheorySets::check(Effort e) { d_internal->check(e); } -bool TheorySets::collectModelInfo(TheoryModel* m) +bool TheorySets::collectModelValues(TheoryModel* m, + const std::set& termSet) { - return d_internal->collectModelInfo(m); + return d_internal->collectModelValues(m, termSet); } void TheorySets::computeCareGraph() { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a7fb31dab..a826a43af 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -60,7 +60,8 @@ class TheorySets : public Theory void notifySharedTerm(TNode) override; void check(Effort) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; void computeCareGraph() override; TrustNode explain(TNode) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3c9414606..78824636a 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1258,18 +1258,10 @@ std::string traceElements(const Node& set) } // namespace -bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) +bool TheorySetsPrivate::collectModelValues(TheoryModel* m, + const std::set& termSet) { Trace("sets-model") << "Set collect model info" << std::endl; - set termSet; - // Compute terms appearing in assertions and shared terms - d_external.computeRelevantTerms(termSet); - - // Assert equalities and disequalities to the model - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - return false; - } NodeManager* nm = NodeManager::currentNM(); std::map mvals; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index af780eadc..387d56de9 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -176,7 +176,7 @@ class TheorySetsPrivate { void check(Theory::Effort); - bool collectModelInfo(TheoryModel* m); + bool collectModelValues(TheoryModel* m, const std::set& termSet); void computeCareGraph(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0de0cc33c..846f9240d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -260,7 +260,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) std::set termSet; // Compute terms appearing in assertions and shared terms - computeRelevantTerms(termSet); + const std::set& irrKinds = m->getIrrelevantKinds(); + computeAssertedTerms(termSet, irrKinds); // assert the (relevant) portion of the equality engine to the model if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 66541a63e..d69c6edc5 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -359,8 +359,15 @@ std::unordered_set Theory::currentlySharedTerms() cons bool Theory::collectModelInfo(TheoryModel* m) { + // 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) @@ -375,7 +382,7 @@ bool Theory::collectModelInfo(TheoryModel* m) } void Theory::collectTerms(TNode n, - set& irrKinds, + const std::set& irrKinds, set& termSet) const { if (termSet.find(n) != termSet.end()) { @@ -396,13 +403,11 @@ void Theory::collectTerms(TNode n, } } -void Theory::computeRelevantTermsInternal(std::set& termSet, - std::set& irrKinds, - bool includeShared) const +void Theory::computeAssertedTerms(std::set& termSet, + const std::set& irrKinds, + bool includeShared) const { // Collect all terms appearing in assertions - irrKinds.insert(kind::EQUAL); - irrKinds.insert(kind::NOT); context::CDList::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); for (; assert_it != assert_it_end; ++assert_it) @@ -424,10 +429,9 @@ void Theory::computeRelevantTermsInternal(std::set& termSet, } } -void Theory::computeRelevantTerms(std::set& termSet, bool includeShared) +void Theory::computeRelevantTerms(std::set& termSet) { - std::set irrKinds; - computeRelevantTermsInternal(termSet, irrKinds, includeShared); + // by default, there are no additional relevant terms } bool Theory::collectModelValues(TheoryModel* m, const std::set& termSet) diff --git a/src/theory/theory.h b/src/theory/theory.h index c5fcf362c..039fdebf1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -182,27 +182,11 @@ class Theory { context::CDList d_sharedTerms; //---------------------------------- private collect model info - /** - * 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. - * - * 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. - * - * includeShared: Whether to include shared terms in termSet. Notice that - * shared terms are not influenced by irrKinds. - */ - void computeRelevantTermsInternal(std::set& termSet, - std::set& irrKinds, - bool includeShared = true) const; /** * Helper function for computeRelevantTerms */ void collectTerms(TNode n, - std::set& irrKinds, + const std::set& irrKinds, std::set& termSet) const; //---------------------------------- end private collect model info @@ -688,13 +672,29 @@ class Theory { */ virtual bool collectModelInfo(TheoryModel* m); /** - * Same as above, but with empty irrKinds. This version can be overridden - * by the theory, e.g. by restricting or extending the set of terms returned - * by computeRelevantTermsInternal, which is called by default with no - * irrKinds. + * 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. + */ + void computeAssertedTerms(std::set& termSet, + const std::set& irrKinds, + bool includeShared = true) const; + /** + * Compute terms that are not necessarily part of the assertions or + * shared terms that should be considered relevant, add them to termSet. */ - virtual void computeRelevantTerms(std::set& termSet, - bool includeShared = true); + virtual void computeRelevantTerms(std::set& termSet); /** * Collect model values, after equality information is added to the model. * The argument termSet is the set of relevant terms returned by -- 2.30.2