From b848e5a94e0d73214ec4cbcba4a08c0da2f239d5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Oct 2021 14:00:09 -0500 Subject: [PATCH] Move isFiniteType from theory engine to Env (#7287) In preparation for breaking more dependencies on TheoryEngine. --- src/smt/env.cpp | 7 ++++ src/smt/env.h | 18 ++++++++++ src/theory/datatypes/sygus_extension.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 4 +-- src/theory/quantifiers/fmf/model_engine.cpp | 2 +- src/theory/quantifiers/quant_split.cpp | 2 +- src/theory/sep/theory_sep.cpp | 4 +-- src/theory/sets/cardinality_extension.cpp | 6 ++-- src/theory/shared_solver.cpp | 4 +-- src/theory/strings/base_solver.cpp | 2 +- src/theory/strings/theory_strings.cpp | 2 +- src/theory/term_registration_visitor.cpp | 33 ++++++++++++++----- src/theory/term_registration_visitor.h | 30 ++++++++--------- src/theory/theory_engine.cpp | 6 ---- src/theory/theory_engine.h | 19 ----------- src/theory/theory_model_builder.cpp | 13 +++----- src/theory/theory_model_builder.h | 5 --- src/theory/theory_state.cpp | 5 --- src/theory/theory_state.h | 5 --- src/theory/uf/ho_extension.cpp | 2 +- src/theory/valuation.cpp | 5 --- src/theory/valuation.h | 5 --- 23 files changed, 83 insertions(+), 100 deletions(-) diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 3267702fb..dafd13d98 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -19,6 +19,7 @@ #include "context/context.h" #include "expr/node.h" #include "options/base_options.h" +#include "options/quantifiers_options.h" #include "options/smt_options.h" #include "printer/printer.h" #include "proof/conv_proof_generator.h" @@ -212,4 +213,10 @@ Node Env::rewriteViaMethod(TNode n, MethodId idr) return n; } +bool Env::isFiniteType(TypeNode tn) const +{ + return isCardinalityClassFinite(tn.getCardinalityClass(), + d_options.quantifiers.finiteModelFind); +} + } // namespace cvc5 diff --git a/src/smt/env.h b/src/smt/env.h index 8d2b1636e..1974408ad 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -205,6 +205,24 @@ class Env */ Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE); + //---------------------- information about cardinality of types + /** + * Is the cardinality of type tn finite? This method depends on whether + * finite model finding is enabled. If finite model finding is enabled, then + * we assume that all uninterpreted sorts have finite cardinality. + * + * Notice that if finite model finding is enabled, this method returns true + * if tn is an uninterpreted sort. It also returns true for the sort + * (Array Int U) where U is an uninterpreted sort. This type + * is finite if and only if U has cardinality one; for cases like this, + * we conservatively return that tn has finite cardinality. + * + * This method does *not* depend on the state of the theory engine, e.g. + * if U in the above example currently is entailed to have cardinality >1 + * based on the assertions. + */ + bool isFiniteType(TypeNode tn) const; + private: /* Private initialization ------------------------------------------------- */ diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 78ff93c1a..d3e711c32 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -788,7 +788,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, TypeNode tnc = children[c1].getType(); // we may only apply this symmetry breaking scheme (which introduces // disequalities) if the types are infinite. - if (tnc == children[c2].getType() && !d_state.isFiniteType(tnc)) + if (tnc == children[c2].getType() && !d_env.isFiniteType(tnc)) { Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); // notice that this symmetry breaking still allows for diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a1c6942a5..c892ffc11 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1239,7 +1239,7 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m, for( unsigned i=0; ifirst]; // if the data type is finite - if (!d_state.isFiniteType(data_type)) + if (!d_env.isFiniteType(data_type)) { continue; } diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 184214724..4e4ee78a8 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -89,7 +89,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) { NodeManager* nm = NodeManager::currentNM(); TypeNode setType = nm->mkSetType(t); - bool finiteType = d_state.isFiniteType(t); + bool finiteType = d_env.isFiniteType(t); // skip infinite types that do not have univset terms if (!finiteType && d_state.getUnivSetEqClass(setType).isNull()) { @@ -1002,7 +1002,7 @@ void CardinalityExtension::mkModelValueElementsFor( TheoryModel* model) { TypeNode elementType = eqc.getType().getSetElementType(); - bool elementTypeFinite = d_state.isFiniteType(elementType); + bool elementTypeFinite = d_env.isFiniteType(elementType); if (isModelValueBasic(eqc)) { std::map::iterator it = d_eqc_to_card_term.find(eqc); @@ -1090,7 +1090,7 @@ void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model) } for (const Node& set : getOrderedSetsEqClasses()) { - if (!d_state.isFiniteType(set.getType())) + if (!d_env.isFiniteType(set.getType())) { continue; } diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index a503c5595..7d457051b 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -35,8 +35,8 @@ SharedSolver::SharedSolver(Env& env, TheoryEngine& te) d_te(te), d_logicInfo(logicInfo()), d_sharedTerms(env, &d_te), - d_preRegistrationVisitor(&te, context()), - d_sharedTermsVisitor(&te, d_sharedTerms, context()), + d_preRegistrationVisitor(env, &te), + d_sharedTermsVisitor(env, &te, d_sharedTerms), d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager()) { } diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 3c825e4ae..e5de8ce16 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -534,7 +534,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, { Assert(tn.isSequence()); TypeNode etn = tn.getSequenceElementType(); - if (!d_state.isFiniteType(etn)) + if (!d_env.isFiniteType(etn)) { // infinite cardinality, we are fine return; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3eac3ca1a..ac6d9b611 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -498,7 +498,7 @@ bool TheoryStrings::collectModelInfoType( c = sel->getCurrent(); // if we are a sequence with infinite element type if (tn.isSequence() - && !d_state.isFiniteType(tn.getSequenceElementType())) + && !d_env.isFiniteType(tn.getSequenceElementType())) { // Make a skeleton instead. In particular, this means that // a value: diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 7f669e36d..0ce07c867 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -41,7 +41,7 @@ std::string PreRegisterVisitor::toString() const { * current. This method is used by PreRegisterVisitor and SharedTermsVisitor * below. */ -bool isAlreadyVisited(TheoryEngine* te, +bool isAlreadyVisited(Env& env, TheoryIdSet visitedTheories, TNode current, TNode parent) @@ -70,7 +70,7 @@ bool isAlreadyVisited(TheoryEngine* te, // do we need to consider the type? TypeNode type = current.getType(); - if (currentTheoryId == parentTheoryId && !te->isFiniteType(type)) + if (currentTheoryId == parentTheoryId && !env.isFiniteType(type)) { // current and parent are the same theory, and we are infinite, return true return true; @@ -79,6 +79,11 @@ bool isAlreadyVisited(TheoryEngine* te, return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories); } +PreRegisterVisitor::PreRegisterVisitor(Env& env, TheoryEngine* engine) + : EnvObj(env), d_engine(engine), d_visited(context()) +{ +} + bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; @@ -103,7 +108,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(d_engine, visitedTheories, current, parent); + return isAlreadyVisited(d_env, visitedTheories, current, parent); } void PreRegisterVisitor::visit(TNode current, TNode parent) { @@ -119,7 +124,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { // call the preregistration on current, parent or type theories and update // visitedTheories. The set of preregistering theories coincides with // visitedTheories here. - preRegister(d_engine, visitedTheories, current, parent, visitedTheories); + preRegister( + d_env, d_engine, visitedTheories, current, parent, visitedTheories); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent @@ -131,7 +137,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Assert(alreadyVisited(current, parent)); } -void PreRegisterVisitor::preRegister(TheoryEngine* te, +void PreRegisterVisitor::preRegister(Env& env, + TheoryEngine* te, TheoryIdSet& visitedTheories, TNode current, TNode parent, @@ -152,7 +159,7 @@ void PreRegisterVisitor::preRegister(TheoryEngine* te, // Note that if enclosed by different theories it's shared, for example, // in read(a, f(a)), f(a) should be shared with integers. TypeNode type = current.getType(); - if (currentTheoryId != parentTheoryId || te->isFiniteType(type)) + if (currentTheoryId != parentTheoryId || env.isFiniteType(type)) { // preregister with the type's theory, if necessary TheoryId typeTheoryId = Theory::theoryOf(type); @@ -214,6 +221,16 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te, void PreRegisterVisitor::start(TNode node) {} +SharedTermsVisitor::SharedTermsVisitor(Env& env, + TheoryEngine* te, + SharedTermsDatabase& sharedTerms) + : EnvObj(env), + d_engine(te), + d_sharedTerms(sharedTerms), + d_preregistered(context()) +{ +} + std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); @@ -247,7 +264,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(d_engine, visitedTheories, current, parent); + return isAlreadyVisited(d_env, visitedTheories, current, parent); } void SharedTermsVisitor::visit(TNode current, TNode parent) { @@ -261,7 +278,7 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { // preregister the term with the current, parent or type theories, as needed PreRegisterVisitor::preRegister( - d_engine, visitedTheories, current, parent, preregTheories); + d_env, d_engine, visitedTheories, current, parent, preregTheories); // Record the new theories that we visited d_visited[current] = visitedTheories; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 86ab160d8..3fed2c321 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -18,11 +18,12 @@ #pragma once +#include + #include "context/context.h" +#include "smt/env_obj.h" #include "theory/shared_terms_database.h" -#include - namespace cvc5 { class TheoryEngine; @@ -38,8 +39,8 @@ class TheoryEngine; * Computation of the set of theories in the original term are computed in the alreadyVisited method * so as no to skip any theories. */ -class PreRegisterVisitor { - +class PreRegisterVisitor : protected EnvObj +{ /** The engine */ TheoryEngine* d_engine; @@ -59,10 +60,7 @@ class PreRegisterVisitor { /** required to instantiate template for NodeVisitor */ using return_type = void; - PreRegisterVisitor(TheoryEngine* engine, context::Context* c) - : d_engine(engine), d_visited(c) - { - } + PreRegisterVisitor(Env& env, TheoryEngine* engine); /** * Returns true is current has already been pre-registered with both current @@ -102,7 +100,8 @@ class PreRegisterVisitor { * If there is no theory sharing, this coincides with visitedTheories. * Otherwise, visitedTheories may be a subset of preregTheories. */ - static void preRegister(TheoryEngine* te, + static void preRegister(Env& env, + TheoryEngine* te, theory::TheoryIdSet& visitedTheories, TNode current, TNode parent, @@ -121,13 +120,13 @@ class PreRegisterVisitor { theory::TheoryIdSet preregTheories); }; - /** * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has * been visited already, we need to visit it again, since we need to associate it with both atoms. */ -class SharedTermsVisitor { +class SharedTermsVisitor : protected EnvObj +{ using TNodeVisitedMap = std::unordered_map; using TNodeToTheorySetMap = context::CDHashMap; /** @@ -144,12 +143,9 @@ class SharedTermsVisitor { /** required to instantiate template for NodeVisitor */ using return_type = void; - SharedTermsVisitor(TheoryEngine* te, - SharedTermsDatabase& sharedTerms, - context::Context* c) - : d_engine(te), d_sharedTerms(sharedTerms), d_preregistered(c) - { - } + SharedTermsVisitor(Env& env, + TheoryEngine* te, + SharedTermsDatabase& sharedTerms); /** * Returns true is current has already been pre-registered with both current and parent theories. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 13a812bb2..1e7116ac4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1941,12 +1941,6 @@ std::pair TheoryEngine::entailmentCheck(options::TheoryOfMode mode, } } -bool TheoryEngine::isFiniteType(TypeNode tn) const -{ - return isCardinalityClassFinite(tn.getCardinalityClass(), - options::finiteModelFind()); -} - void TheoryEngine::spendResource(Resource r) { d_env.getResourceManager()->spendResource(r); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3807b926d..0a9b67979 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -390,25 +390,6 @@ class TheoryEngine : protected EnvObj */ std::pair entailmentCheck(options::TheoryOfMode mode, TNode lit); - //---------------------- information about cardinality of types - /** - * Is the cardinality of type tn finite? This method depends on whether - * finite model finding is enabled. If finite model finding is enabled, then - * we assume that all uninterpreted sorts have finite cardinality. - * - * Notice that if finite model finding is enabled, this method returns true - * if tn is an uninterpreted sort. It also returns true for the sort - * (Array Int U) where U is an uninterpreted sort. This type - * is finite if and only if U has cardinality one; for cases like this, - * we conservatively return that tn has finite cardinality. - * - * This method does *not* depend on the state of the theory engine, e.g. - * if U in the above example currently is entailed to have cardinality >1 - * based on the assertions. - */ - bool isFiniteType(TypeNode tn) const; - //---------------------- end information about cardinality of types - theory::SortInference* getSortInference() { return d_sortInfer.get(); } /** Prints the assertions to the debug stream */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index bbe1588d6..ac177a114 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -275,12 +275,6 @@ bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, return false; } -bool TheoryEngineModelBuilder::isFiniteType(TypeNode tn) const -{ - return isCardinalityClassFinite(tn.getCardinalityClass(), - options::finiteModelFind()); -} - bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const { if (tn.isSort()) @@ -844,8 +838,9 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) if (t.isDatatype()) { const DType& dt = t.getDType(); - isCorecursive = dt.isCodatatype() - && (!isFiniteType(t) || dt.isRecursiveSingleton(t)); + isCorecursive = + dt.isCodatatype() + && (!d_env.isFiniteType(t) || dt.isRecursiveSingleton(t)); } #ifdef CVC5_ASSERTIONS bool isUSortFiniteRestricted = false; @@ -922,7 +917,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) n = itAssigner->second.getNextAssignment(); Assert(!n.isNull()); } - else if (t.isSort() || !isFiniteType(t)) + else if (t.isSort() || !d_env.isFiniteType(t)) { // If its interpreted as infinite, we get a fresh value that does // not occur in the model. diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index dd11a3d2e..a604d0402 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -299,11 +299,6 @@ class TheoryEngineModelBuilder : protected EnvObj bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m); //------------------------------------end for codatatypes - /** - * Is the given type constrained to be finite? This depends on whether - * finite model finding is enabled. - */ - bool isFiniteType(TypeNode tn) const; //---------------------------------for debugging finite model finding /** does type tn involve an uninterpreted sort? */ bool involvesUSort(TypeNode tn) const; diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 484e27ead..08ad20e01 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -162,11 +162,6 @@ context::CDList::const_iterator TheoryState::factsEnd(TheoryId tid) return d_valuation.factsEnd(tid); } -bool TheoryState::isFiniteType(TypeNode tn) const -{ - return d_valuation.isFiniteType(tn); -} - Valuation& TheoryState::getValuation() { return d_valuation; } } // namespace theory diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index e8da3ad39..4d2c29e1b 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -100,11 +100,6 @@ class TheoryState : protected EnvObj context::CDList::const_iterator factsBegin(TheoryId tid); /** The beginning iterator of facts for theory tid.*/ context::CDList::const_iterator factsEnd(TheoryId tid); - /** - * Is the cardinality of type tn finite? This method depends on whether - * finite model finding is enabled. For details, see theory_engine.h. - */ - bool isFiniteType(TypeNode tn) const; /** Get the underlying valuation class */ Valuation& getValuation(); diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 925805332..096a47c86 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -215,7 +215,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) hasFunctions = true; // if during collect model, must have an infinite type // if not during collect model, must have a finite type - if (d_state.isFiniteType(tn) != isCollectModel) + if (d_env.isFiniteType(tn) != isCollectModel) { func_eqcs[tn].push_back(eqc); Trace("uf-ho-debug") diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 621f89539..bd7a3872c 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -232,10 +232,5 @@ context::CDList::const_iterator Valuation::factsEnd(TheoryId tid) return theory->facts_end(); } -bool Valuation::isFiniteType(TypeNode tn) const -{ - return d_engine->isFiniteType(tn); -} - } // namespace theory } // namespace cvc5 diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 2b95829e0..f1b14da76 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -231,11 +231,6 @@ public: context::CDList::const_iterator factsBegin(TheoryId tid); /** The beginning iterator of facts for theory tid.*/ context::CDList::const_iterator factsEnd(TheoryId tid); - /** - * Is the cardinality of type tn finite? This method depends on whether - * finite model finding is enabled. For details, see theory_engine.h. - */ - bool isFiniteType(TypeNode tn) const; };/* class Valuation */ } // namespace theory -- 2.30.2