diff options
Diffstat (limited to 'src/theory')
22 files changed, 118 insertions, 38 deletions
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 6e7a5c0a8..d4dbdf82d 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -786,7 +786,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() && !tnc.isInterpretedFinite()) + if (tnc == children[c2].getType() && !d_state.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 7242407cc..60fd87731 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -218,7 +218,7 @@ void TheoryDatatypes::postCheck(Effort level) const DType& dt = tt.getDType(); Trace("datatypes-debug") << "Datatype " << dt.getName() << " is " - << dt.isInterpretedFinite(tt) << " " + << dt.getCardinalityClass(tt) << " " << dt.isRecursiveSingleton(tt) << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton( tt ) ){ @@ -273,14 +273,21 @@ void TheoryDatatypes::postCheck(Effort level) int consIndex = -1; int fconsIndex = -1; bool needSplit = true; - for( unsigned int j=0; j<pcons.size(); j++ ) { + for (size_t j = 0, psize = pcons.size(); j < psize; j++) + { if( pcons[j] ) { if( consIndex==-1 ){ consIndex = j; } Trace("datatypes-debug") << j << " compute finite..." << std::endl; - bool ifin = dt[j].isInterpretedFinite(tt); + // Notice that we split here on all datatypes except the + // truly infinite ones. It is possible to also not split + // on those that are interpreted-finite when finite model + // finding is disabled, but as a heuristic we choose to split + // on those too. + bool ifin = dt[j].getCardinalityClass(tt) + != CardinalityClass::INFINITE; Trace("datatypes-debug") << "...returned " << ifin << std::endl; if (!ifin) @@ -1327,8 +1334,9 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m, for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ for( unsigned i=0; i<pcons.size(); i++ ){ - //must try the infinite ones first - bool cfinite = dt[ i ].isInterpretedFinite( tt ); + // must try the infinite ones first + bool cfinite = + d_state.isFiniteType(dt[i].getSpecializedConstructorType(tt)); if( pcons[i] && (r==1)==cfinite ){ neqc = utils::getInstCons(eqc, dt, i); break; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index f7a6f26f3..6cb2fdce9 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -199,7 +199,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is " << d_type << std::endl; Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton(d_type); - Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type) + Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type) << std::endl; // Start with the ground term constructed via mkGroundValue, which does // a traversal over the structure of the datatype to find a finite term. @@ -312,7 +312,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ // or other cases if (prevSize == d_size_limit || (d_size_limit == 0 && d_datatype.isCodatatype()) - || !d_datatype.isInterpretedFinite(d_type)) + || d_datatype.getCardinalityClass(d_type) + == CardinalityClass::INFINITE) { d_size_limit++; d_ctor = 0; diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 044183756..fbee35f3d 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -63,7 +63,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { bool hasCyclesDt(const DType& dt) { - return dt.isRecursiveSingleton(d_type) || !dt.isFinite(d_type); + return dt.isRecursiveSingleton(d_type) + || dt.getCardinalityClass(d_type) == CardinalityClass::INFINITE; } bool hasCycles( TypeNode tn ){ if( tn.isDatatype() ){ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index a4f4170fa..b0f6e63bf 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -357,7 +357,7 @@ void BoundedIntegers::checkOwnership(Node f) // supported for finite element types #1123). Regardless, this is // typically not a limitation since this variable can be bound in a // standard way below since its type is finite. - if (!v.getType().isInterpretedFinite()) + if (!d_qstate.isFiniteType(v.getType())) { setBoundedVar(f, v, BOUND_SET_MEMBER); setBoundVar = true; @@ -417,7 +417,7 @@ void BoundedIntegers::checkOwnership(Node f) for( unsigned i=0; i<f[0].getNumChildren(); i++) { if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){ TypeNode tn = f[0][i].getType(); - if ((tn.isSort() && tn.isInterpretedFinite()) + if ((tn.isSort() && d_qstate.isFiniteType(tn)) || d_qreg.getQuantifiersBoundInference().mayComplete(tn)) { success = true; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index e935ee694..585032dc4 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -133,7 +133,7 @@ void ModelEngine::registerQuantifier( Node f ){ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ TypeNode tn = f[0][i].getType(); if( !tn.isSort() ){ - if (!tn.isInterpretedFinite()) + if (!d_qstate.isFiniteType(tn)) { if( tn.isInteger() ){ if( !options::fmfBound() ){ diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index 7b184bf0d..1fbf53761 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -48,8 +48,14 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn) bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) { + if (!tn.isClosedEnumerable()) + { + return false; + } bool mc = false; - if (tn.isClosedEnumerable() && tn.isInterpretedFinite()) + // we cannot use FMF to complete interpreted types, thus we pass + // false for fmfEnabled here + if (isCardinalityClassFinite(tn.getCardinalityClass(), false)) { Cardinality c = tn.getCardinality(); if (!c.isLargeFinite()) diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index be384d1aa..cc2525b78 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -52,6 +52,7 @@ void QuantDSplit::checkOwnership(Node q) for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ TypeNode tn = q[0][i].getType(); if( tn.isDatatype() ){ + bool isFinite = d_qstate.isFiniteType(tn); const DType& dt = tn.getDType(); if (dt.isRecursiveSingleton(tn)) { @@ -62,14 +63,14 @@ void QuantDSplit::checkOwnership(Node q) if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG) { // split if it is a finite datatype - doSplit = dt.isInterpretedFinite(tn); + doSplit = isFinite; } else if (options::quantDynamicSplit() == options::QuantDSplitMode::DEFAULT) { if (!qbi.isFiniteBound(q, q[0][i])) { - if (dt.isInterpretedFinite(tn)) + if (isFinite) { // split if goes from being unhandled -> handled by finite // instantiation. An example is datatypes with uninterpreted sort diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index c0fb17dab..83a4276ab 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -773,8 +773,10 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // have we run out of constructor classes for this size? if (d_ccCons.empty()) { - // check whether we should terminate - if (d_tn.isInterpretedFinite()) + // check whether we should terminate, which notice always treats + // uninterpreted sorts as infinite, since we do not put bounds on them + // in our enumeration. + if (isCardinalityClassFinite(d_tn.getCardinalityClass(), false)) { if (ncc == tc.getNumConstructorClasses()) { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 05547aa8a..301299f11 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -202,7 +202,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "_"; //m->d_comment_str << "_"; TypeEnumerator te_range( data_type ); - if( data_type.isInterpretedFinite() ){ + if (d_state.isFiniteType(data_type)) + { pto_children.push_back( *te_range ); }else{ //must enumerate until we find one that is not explicitly pointed to @@ -820,7 +821,7 @@ void TheorySep::postCheck(Effort level) { TypeNode data_type = d_loc_to_data_type[it->first]; // if the data type is finite - if (!data_type.isInterpretedFinite()) + if (!d_state.isFiniteType(data_type)) { continue; } diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 8ba3cd9ea..a9a7429b4 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -85,8 +85,9 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) { NodeManager* nm = NodeManager::currentNM(); TypeNode setType = nm->mkSetType(t); + bool finiteType = d_state.isFiniteType(t); // skip infinite types that do not have univset terms - if (!t.isInterpretedFinite() && d_state.getUnivSetEqClass(setType).isNull()) + if (!finiteType && d_state.getUnivSetEqClass(setType).isNull()) { return; } @@ -96,7 +97,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) // cardinality of an interpreted finite type t is infinite when t // is infinite without --fmf - if (t.isInterpretedFinite() && card.isInfinite()) + if (finiteType && card.isInfinite()) { // TODO (#1123): support uninterpreted sorts with --finite-model-find std::stringstream message; @@ -126,7 +127,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) // get all equivalent classes of type t vector<Node> representatives = d_state.getSetsEqClasses(t); - if (t.isInterpretedFinite()) + if (finiteType) { Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality())); Node cardUniv = nm->mkNode(kind::CARD, proxy); @@ -998,6 +999,7 @@ void CardinalityExtension::mkModelValueElementsFor( TheoryModel* model) { TypeNode elementType = eqc.getType().getSetElementType(); + bool elementTypeFinite = d_state.isFiniteType(elementType); if (isModelValueBasic(eqc)) { std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc); @@ -1018,14 +1020,14 @@ void CardinalityExtension::mkModelValueElementsFor( Assert(els.size() <= vu); NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - if (elementType.isInterpretedFinite()) + if (elementTypeFinite) { // get all members of this finite type collectFiniteTypeSetElements(model); } while (els.size() < vu) { - if (elementType.isInterpretedFinite()) + if (elementTypeFinite) { // At this point we are sure the formula is satisfiable and all // cardinality constraints are satisfied. Since this type is finite, @@ -1085,7 +1087,7 @@ void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model) } for (const Node& set : getOrderedSetsEqClasses()) { - if (!set.getType().isInterpretedFinite()) + if (!d_state.isFiniteType(set.getType())) { continue; } diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 61d0818c6..6ee88b298 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -539,7 +539,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, { Assert(tn.isSequence()); TypeNode etn = tn.getSequenceElementType(); - if (etn.isInterpretedFinite()) + if (d_state.isFiniteType(etn)) { // infinite cardinality, we are fine return; diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index e546e6937..7f669e36d 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -41,7 +41,10 @@ std::string PreRegisterVisitor::toString() const { * current. This method is used by PreRegisterVisitor and SharedTermsVisitor * below. */ -bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent) +bool isAlreadyVisited(TheoryEngine* te, + TheoryIdSet visitedTheories, + TNode current, + TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) @@ -67,7 +70,7 @@ bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent) // do we need to consider the type? TypeNode type = current.getType(); - if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite()) + if (currentTheoryId == parentTheoryId && !te->isFiniteType(type)) { // current and parent are the same theory, and we are infinite, return true return true; @@ -100,7 +103,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(visitedTheories, current, parent); + return isAlreadyVisited(d_engine, visitedTheories, current, parent); } void PreRegisterVisitor::visit(TNode current, TNode parent) { @@ -149,7 +152,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 || type.isInterpretedFinite()) + if (currentTheoryId != parentTheoryId || te->isFiniteType(type)) { // preregister with the type's theory, if necessary TheoryId typeTheoryId = Theory::theoryOf(type); @@ -244,7 +247,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(visitedTheories, current, parent); + return isAlreadyVisited(d_engine, visitedTheories, current, parent); } void SharedTermsVisitor::visit(TNode current, TNode parent) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8c030351b..55c782f2f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1907,6 +1907,12 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode, } } +bool TheoryEngine::isFiniteType(TypeNode tn) const +{ + return isCardinalityClassFinite(tn.getCardinalityClass(), + options::finiteModelFind()); +} + void TheoryEngine::spendResource(Resource r) { d_resourceManager->spendResource(r); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4da9a38dd..b43488fa8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -631,6 +631,24 @@ class TheoryEngine { */ std::pair<bool, Node> 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 private: /** Dump the assertions to the dump */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 8396361bf..2103c3997 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -273,7 +273,13 @@ bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, return false; } -bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) +bool TheoryEngineModelBuilder::isFiniteType(TypeNode tn) const +{ + return isCardinalityClassFinite(tn.getCardinalityClass(), + options::finiteModelFind()); +} + +bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const { if (tn.isSort()) { @@ -837,7 +843,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) { const DType& dt = t.getDType(); isCorecursive = dt.isCodatatype() - && (!dt.isFinite(t) || dt.isRecursiveSingleton(t)); + && (!isFiniteType(t) || dt.isRecursiveSingleton(t)); } #ifdef CVC5_ASSERTIONS bool isUSortFiniteRestricted = false; @@ -914,13 +920,13 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) n = itAssigner->second.getNextAssignment(); Assert(!n.isNull()); } - else if (t.isSort() || !t.isInterpretedFinite()) + else if (t.isSort() || !isFiniteType(t)) { // If its interpreted as infinite, we get a fresh value that does // not occur in the model. // Note we also consider uninterpreted sorts to be infinite here - // regardless of whether isInterpretedFinite is true (which is true - // for uninterpreted sorts iff finite model finding is enabled). + // regardless of whether the cardinality class of t is + // CardinalityClass::INTERPRETED_FINITE. // This is required because the UF solver does not explicitly // assign uninterpreted constants to equivalence classes in its // collectModelValues method. Doing so would have the same effect diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 5652dc7ab..2ed8e2be6 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -299,9 +299,14 @@ class TheoryEngineModelBuilder 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); + bool involvesUSort(TypeNode tn) const; /** is v an excluded value based on uninterpreted sorts? * This gives an assertion failure in the case that v contains * an uninterpreted constant whose index is out of the bounds diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index e6d36033a..5ac5e6ae9 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -172,6 +172,11 @@ context::CDList<Assertion>::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 850f42da0..933f44d2b 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -101,6 +101,11 @@ class TheoryState context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid); /** The beginning iterator of facts for theory tid.*/ context::CDList<Assertion>::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 edd61fd2a..13709c2ab 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -212,7 +212,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 (tn.isInterpretedFinite() != isCollectModel) + if (d_state.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 c72c4e487..937fcd5fa 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -220,5 +220,10 @@ context::CDList<Assertion>::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 af7e4205e..9eaf24616 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -215,6 +215,11 @@ public: context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid); /** The beginning iterator of facts for theory tid.*/ context::CDList<Assertion>::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 |