From: Andrew Reynolds Date: Mon, 12 Apr 2021 21:55:44 +0000 (-0500) Subject: Fix computation of whether a type is finite (#6312) X-Git-Tag: cvc5-1.0.0~1922 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76f495646c0e3a95f2474c5d746bc61ece18f89f;p=cvc5.git Fix computation of whether a type is finite (#6312) This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite. Fixes #4260, fixes #6100 (that benchmark now says unknown without an error). --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 47b376151..b29647311 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3462,7 +3462,9 @@ bool Datatype::isFinite() const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line - return d_dtype->isFinite(); + // we assume that finite model finding is disabled by passing false as the + // second argument + return isCardinalityClassFinite(d_dtype->getCardinalityClass(), false); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 73f760170..66331f5c7 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -488,64 +488,44 @@ bool DType::computeCardinalityRecSingleton( return true; } -bool DType::isFinite(TypeNode t) const +CardinalityClass DType::getCardinalityClass(TypeNode t) const { Trace("datatypes-init") << "DType::isFinite " << std::endl; Assert(isResolved()); Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); // is this already in the cache ? - if (d_self.getAttribute(DTypeFiniteComputedAttr())) + std::map::const_iterator it = d_cardClass.find(t); + if (it != d_cardClass.end()) { - return d_self.getAttribute(DTypeFiniteAttr()); + return it->second; } + // it is the max cardinality class of a constructor, with base case ONE + // if we have one constructor and FINITE otherwise. + CardinalityClass c = d_constructors.size() == 1 ? CardinalityClass::ONE + : CardinalityClass::FINITE; for (std::shared_ptr ctor : d_constructors) { - if (!ctor->isFinite(t)) - { - d_self.setAttribute(DTypeFiniteComputedAttr(), true); - d_self.setAttribute(DTypeFiniteAttr(), false); - return false; - } + CardinalityClass cc = ctor->getCardinalityClass(t); + c = maxCardinalityClass(c, cc); } - d_self.setAttribute(DTypeFiniteComputedAttr(), true); - d_self.setAttribute(DTypeFiniteAttr(), true); - return true; + d_cardClass[t] = c; + return c; } -bool DType::isFinite() const +CardinalityClass DType::getCardinalityClass() const { Assert(isResolved() && !isParametric()); - return isFinite(d_self); + return getCardinalityClass(d_self); } -bool DType::isInterpretedFinite(TypeNode t) const +bool DType::isFinite(TypeNode t, bool fmfEnabled) const { - Trace("datatypes-init") << "DType::isInterpretedFinite " << std::endl; - Assert(isResolved()); - Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); - // is this already in the cache ? - if (d_self.getAttribute(DTypeUFiniteComputedAttr())) - { - return d_self.getAttribute(DTypeUFiniteAttr()); - } - // start by assuming it is not - d_self.setAttribute(DTypeUFiniteComputedAttr(), true); - d_self.setAttribute(DTypeUFiniteAttr(), false); - for (std::shared_ptr ctor : d_constructors) - { - if (!ctor->isInterpretedFinite(t)) - { - return false; - } - } - d_self.setAttribute(DTypeUFiniteComputedAttr(), true); - d_self.setAttribute(DTypeUFiniteAttr(), true); - return true; + return isCardinalityClassFinite(getCardinalityClass(t), fmfEnabled); } -bool DType::isInterpretedFinite() const + +bool DType::isFinite(bool fmfEnabled) const { - Assert(isResolved() && !isParametric()); - return isInterpretedFinite(d_self); + return isFinite(d_self, fmfEnabled); } bool DType::isWellFounded() const diff --git a/src/expr/dtype.h b/src/expr/dtype.h index cee95cdc6..2837e37af 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -47,32 +47,6 @@ struct DTypeConsIndexTag { }; typedef expr::Attribute DTypeConsIndexAttr; -/** Attribute true for datatype types that are finite. */ -struct DTypeFiniteTag -{ -}; -typedef expr::Attribute DTypeFiniteAttr; -/** Attribute true when we have computed whether a datatype type is finite */ -struct DTypeFiniteComputedTag -{ -}; -typedef expr::Attribute DTypeFiniteComputedAttr; -/** - * Attribute true for datatype types that are interpreted as finite (see - * TypeNode::isInterpretedFinite). - */ -struct DTypeUFiniteTag -{ -}; -typedef expr::Attribute DTypeUFiniteAttr; -/** - * Attribute true when we have computed whether a datatype type is interpreted - * as finite. - */ -struct DTypeUFiniteComputedTag -{ -}; -typedef expr::Attribute DTypeUFiniteComputedAttr; // ----------------------- end datatype attributes class DTypeConstructor; @@ -282,30 +256,31 @@ class DType Cardinality getCardinality() const; /** - * Return true iff this DType has finite cardinality. If the - * datatype is not well-founded, this method returns false. The + * Return the cardinality class of the datatype. The * DType must be resolved or an assertion is violated. * * The version of this method that takes type t is required * for parametric datatypes, where t is an instantiated * parametric datatype type whose datatype is this class. */ - bool isFinite(TypeNode t) const; - bool isFinite() const; + CardinalityClass getCardinalityClass(TypeNode t) const; + CardinalityClass getCardinalityClass() const; /** - * Return true iff this DType is finite (all constructors are - * finite, i.e., there are finitely many ground terms) under the - * assumption that unintepreted sorts are finite. If the - * datatype is not well-founded, this method returns false. The + * Return true iff this DType has finite cardinality. If the + * datatype is not well-founded, this method returns false. The * DType must be resolved or an assertion is violated. * - * The versions of these methods that takes type t is required + * The version of this method that takes type t is required * for parametric datatypes, where t is an instantiated * parametric datatype type whose datatype is this class. + * + * @param t The (instantiated) datatype type we are computing finiteness for + * @param fmfEnabled Whether finite model finding is enabled + * @return true if finite model finding is enabled */ - bool isInterpretedFinite(TypeNode t) const; - bool isInterpretedFinite() const; + bool isFinite(TypeNode t, bool fmfEnabled=false) const; + bool isFinite(bool fmfEnabled=false) const; /** is well-founded * @@ -640,6 +615,8 @@ class DType /** cache of shared selectors for this datatype */ mutable std::map > > d_sharedSel; + /** A cache for getCardinalityClass. */ + mutable std::map d_cardClass; }; /* class DType */ /** diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index debb66ef4..8d6194b06 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -158,34 +158,28 @@ Cardinality DTypeConstructor::getCardinality(TypeNode t) const return c; } -bool DTypeConstructor::isFinite(TypeNode t) const +CardinalityClass DTypeConstructor::getCardinalityClass(TypeNode t) const { - std::pair cinfo = computeCardinalityInfo(t); - return cinfo.first == CardinalityType::FINITE; -} - -bool DTypeConstructor::isInterpretedFinite(TypeNode t) const -{ - std::pair cinfo = computeCardinalityInfo(t); - return cinfo.first != CardinalityType::INFINITE; + std::pair cinfo = computeCardinalityInfo(t); + return cinfo.first; } bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const { - std::pair cinfo = computeCardinalityInfo(t); + std::pair cinfo = computeCardinalityInfo(t); return cinfo.second; } -std::pair -DTypeConstructor::computeCardinalityInfo(TypeNode t) const +std::pair DTypeConstructor::computeCardinalityInfo( + TypeNode t) const { - std::map >::iterator it = + std::map >::iterator it = d_cardInfo.find(t); if (it != d_cardInfo.end()) { return it->second; } - std::pair ret(CardinalityType::FINITE, false); + std::pair ret(CardinalityClass::ONE, false); std::vector instTypes; std::vector paramTypes; bool isParam = t.isParametricDatatype(); @@ -204,27 +198,16 @@ DTypeConstructor::computeCardinalityInfo(TypeNode t) const instTypes.begin(), instTypes.end()); } - if (tc.isFinite()) - { - // do nothing - } - else if (tc.isInterpretedFinite()) - { - if (ret.first == CardinalityType::FINITE) - { - // not simply finite, it depends on uninterpreted sorts being finite - ret.first = CardinalityType::INTERPRETED_FINITE; - } - } - else + // get the current cardinality class + CardinalityClass cctc = tc.getCardinalityClass(); + // update ret.first to the max cardinality class + ret.first = maxCardinalityClass(ret.first, cctc); + if (cctc != CardinalityClass::INFINITE) { - // infinite implies the constructor is infinite cardinality - ret.first = CardinalityType::INFINITE; - continue; + // if the argument is (interpreted) finite and external, set the flag + // for indicating it has a finite external argument + ret.second = ret.second || !tc.isDatatype(); } - // if the argument is (interpreted) finite and external, set the flag - // for indicating it has a finite external argument - ret.second = ret.second || !tc.isDatatype(); } d_cardInfo[t] = ret; return ret; diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index 368d4cbde..55d940d91 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -24,6 +24,7 @@ #include "expr/dtype_selector.h" #include "expr/node.h" #include "expr/type_node.h" +#include "util/cardinality_class.h" namespace cvc5 { @@ -147,18 +148,15 @@ class DTypeConstructor Cardinality getCardinality(TypeNode t) const; /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite). This function can - * only be called for resolved constructors. - */ - bool isFinite(TypeNode t) const; - /** - * Return true iff this constructor is finite (it is nullary or - * each of its argument types are finite) under assumption - * uninterpreted sorts are finite. This function can - * only be called for resolved constructors. + * Return the cardinality class, which indicates if the type has cardinality + * one, is finite or infinite, possibly dependent on uninterpreted sorts being + * finite. + * + * Note that the cardinality of a constructor is equivalent to asking how + * many applications of this constructor exist. */ - bool isInterpretedFinite(TypeNode t) const; + CardinalityClass getCardinalityClass(TypeNode t) const; + /** * Has finite external argument type. This returns true if this constructor * has an argument type that is not a datatype and is interpreted as a @@ -237,17 +235,6 @@ class DTypeConstructor void toStream(std::ostream& out) const; private: - /** Constructor cardinality type */ - enum class CardinalityType - { - // the constructor is finite - FINITE, - // the constructor is interpreted-finite (finite under the assumption that - // uninterpreted sorts are finite) - INTERPRETED_FINITE, - // the constructor is infinte - INFINITE - }; /** resolve * * This resolves (initializes) the constructor. For details @@ -311,7 +298,7 @@ class DTypeConstructor * type t, and a Boolean indicating whether the constructor has any arguments * that have finite external type. */ - std::pair computeCardinalityInfo(TypeNode t) const; + std::pair computeCardinalityInfo(TypeNode t) const; /** compute shared selectors * This computes the maps d_sharedSelectors and d_sharedSelectorIndex. */ @@ -351,7 +338,7 @@ class DTypeConstructor */ mutable std::map > d_sharedSelectorIndex; /** A cache for computeCardinalityInfo. */ - mutable std::map > d_cardInfo; + mutable std::map > d_cardInfo; }; /* class DTypeConstructor */ /** diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 2da1b7ad2..3c0316405 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -65,160 +65,123 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } -/** Attribute true for types that are finite */ -struct IsFiniteTag +/** Attribute true for types that have cardinality one */ +struct TypeCardinalityClassTag { }; -typedef expr::Attribute IsFiniteAttr; -/** Attribute true for types which we have computed the above attribute */ -struct IsFiniteComputedTag -{ -}; -typedef expr::Attribute IsFiniteComputedAttr; +typedef expr::Attribute + TypeCardinalityClassAttr; -/** Attribute true for types that are interpreted as finite */ -struct IsInterpretedFiniteTag -{ -}; -typedef expr::Attribute IsInterpretedFiniteAttr; -/** Attribute true for types which we have computed the above attribute */ -struct IsInterpretedFiniteComputedTag -{ -}; -typedef expr::Attribute - IsInterpretedFiniteComputedAttr; - -bool TypeNode::isFinite() { return isFiniteInternal(false); } - -bool TypeNode::isInterpretedFinite() -{ - return isFiniteInternal(options::finiteModelFind()); -} - -bool TypeNode::isFiniteInternal(bool usortFinite) +CardinalityClass TypeNode::getCardinalityClass() { // check it is already cached - if (usortFinite) - { - if (getAttribute(IsInterpretedFiniteComputedAttr())) - { - return getAttribute(IsInterpretedFiniteAttr()); - } - } - else if (getAttribute(IsFiniteComputedAttr())) + if (hasAttribute(TypeCardinalityClassAttr())) { - return getAttribute(IsFiniteAttr()); + return static_cast( + getAttribute(TypeCardinalityClassAttr())); } - bool ret = false; + CardinalityClass ret = CardinalityClass::INFINITE; if (isSort()) { - ret = usortFinite; + ret = CardinalityClass::INTERPRETED_ONE; } else if (isBoolean() || isBitVector() || isFloatingPoint() || isRoundingMode()) { - ret = true; + ret = CardinalityClass::FINITE; } - else if (isString() || isRegExp() || isSequence() || isReal()) + else if (isString() || isRegExp() || isSequence() || isReal() || isBag()) { - ret = false; + ret = CardinalityClass::INFINITE; } else { // recursive case (this may be a parametric sort), we assume infinite for - // the moment here to prevent infinite loops - if (usortFinite) - { - setAttribute(IsInterpretedFiniteAttr(), false); - setAttribute(IsInterpretedFiniteComputedAttr(), true); - } - else - { - setAttribute(IsFiniteAttr(), false); - setAttribute(IsFiniteComputedAttr(), true); - } + // the moment here to prevent infinite loops, which may occur when + // computing the cardinality of datatype types with foreign types + setAttribute(TypeCardinalityClassAttr(), static_cast(ret)); + if (isDatatype()) { TypeNode tn = *this; const DType& dt = getDType(); - ret = usortFinite ? dt.isInterpretedFinite(tn) : dt.isFinite(tn); + ret = dt.getCardinalityClass(tn); } else if (isArray()) { - TypeNode tnc = getArrayConstituentType(); - if (!tnc.isFiniteInternal(usortFinite)) + ret = getArrayConstituentType().getCardinalityClass(); + if (ret == CardinalityClass::FINITE + || ret == CardinalityClass::INTERPRETED_FINITE) + { + CardinalityClass cci = getArrayIndexType().getCardinalityClass(); + // arrays with both finite element types, we take the max with its + // index type. + ret = maxCardinalityClass(ret, cci); + } + // else, array types whose element type is INFINITE, ONE, or + // INTERPRETED_ONE have the same cardinality class as their range. + } + else if (isSet()) + { + CardinalityClass cc = getSetElementType().getCardinalityClass(); + if (cc == CardinalityClass::ONE) { - // arrays with constituent type that is infinite are infinite - ret = false; + // 1 -> 2 + ret = CardinalityClass::FINITE; } - else if (getArrayIndexType().isFiniteInternal(usortFinite)) + else if (ret == CardinalityClass::INTERPRETED_ONE) { - // arrays with both finite constituent and index types are finite - ret = true; + // maybe 1 -> maybe finite + ret = CardinalityClass::INTERPRETED_FINITE; } else { - // If the consistuent type of the array has cardinality one, then the - // array type has cardinality one, independent of the index type. - ret = tnc.getCardinality().isOne(); + // finite or infinite is unchanged + ret = cc; } } - else if (isSet()) - { - ret = getSetElementType().isFiniteInternal(usortFinite); - } - else if (isBag()) - { - // there are infinite bags for all element types - ret = false; - } else if (isFunction()) { - ret = true; - TypeNode tnr = getRangeType(); - if (!tnr.isFiniteInternal(usortFinite)) - { - ret = false; - } - else + ret = getRangeType().getCardinalityClass(); + if (ret == CardinalityClass::FINITE + || ret == CardinalityClass::INTERPRETED_FINITE) { + // we may have a larger cardinality class based on the + // arguments of the function std::vector argTypes = getArgTypes(); - for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) { - if (!argTypes[i].isFiniteInternal(usortFinite)) - { - ret = false; - break; - } - } - if (!ret) - { - // similar to arrays, functions are finite if their range type - // has cardinality one, regardless of the arguments. - ret = tnr.getCardinality().isOne(); + CardinalityClass cca = argTypes[i].getCardinalityClass(); + ret = maxCardinalityClass(ret, cca); } } + // else, function types whose range type is INFINITE, ONE, or + // INTERPRETED_ONE have the same cardinality class as their range. + } + else if (isConstructor()) + { + // notice that we require computing the cardinality class of the + // constructor type, which is equivalent to asking how many + // constructor applications of the given constructor exist. This + // is used in several places in the decision procedure for datatypes. + // The cardinality starts with one. + ret = CardinalityClass::ONE; + // we may have a larger cardinality class based on the + // arguments of the constructor + std::vector argTypes = getArgTypes(); + for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) + { + CardinalityClass cca = argTypes[i].getCardinalityClass(); + ret = maxCardinalityClass(ret, cca); + } } else { - // all types should be handled above + // all types we care about should be handled above Assert(false); - // by default, compute the exact cardinality for the type and check - // whether it is finite. This should be avoided in general, since - // computing cardinalities for types can be highly expensive. - ret = getCardinality().isFinite(); } } - if (usortFinite) - { - setAttribute(IsInterpretedFiniteAttr(), ret); - setAttribute(IsInterpretedFiniteComputedAttr(), true); - } - else - { - setAttribute(IsFiniteAttr(), ret); - setAttribute(IsFiniteComputedAttr(), true); - } + setAttribute(TypeCardinalityClassAttr(), static_cast(ret)); return ret; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9b2f4b4d0..dab7fd394 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -30,6 +30,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "util/cardinality.h" +#include "util/cardinality_class.h" namespace cvc5 { @@ -407,19 +408,14 @@ public: * @return a finite or infinite cardinality */ Cardinality getCardinality() const; - - /** - * Is this type finite? This assumes uninterpreted sorts have infinite - * cardinality. - */ - bool isFinite(); - /** - * Is this type interpreted as finite. - * If finite model finding is enabled, this assumes all uninterpreted sorts - * are interpreted as finite. + * Get the cardinality class of this type node. The cardinality class + * is static for each type node and does not depend on the state of the + * solver. For details on cardinality classes, see util/cardinality_class.h + * + * @return the cardinality class */ - bool isInterpretedFinite(); + CardinalityClass getCardinalityClass(); /** is closed enumerable type * @@ -712,13 +708,6 @@ public: private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); - /** - * Is this type interpreted as finite. - * If the flag usortFinite is true, this assumes all uninterpreted sorts - * are interpreted as finite. - */ - bool isFiniteInternal(bool usortFinite); - /** * Indents the given stream a given amount of spaces. * 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 { 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 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 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::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 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 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::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::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 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::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::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 diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index c7f7e780c..ea4ece8dd 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -29,6 +29,8 @@ libcvc4_add_sources( bool.h cardinality.cpp cardinality.h + cardinality_class.cpp + cardinality_class.h dense_map.h divisible.cpp divisible.h diff --git a/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2 b/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2 new file mode 100644 index 000000000..bdd5e3347 --- /dev/null +++ b/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic AUFNIA) +(declare-sort S0 0) +(declare-const a (Array Int S0)) +(declare-const b (Array Int S0)) +(assert (distinct b a)) +(check-sat)