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).
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;
}
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<TypeNode, CardinalityClass>::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<DTypeConstructor> 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<DTypeConstructor> 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
{
};
typedef expr::Attribute<DTypeConsIndexTag, size_t> DTypeConsIndexAttr;
-/** Attribute true for datatype types that are finite. */
-struct DTypeFiniteTag
-{
-};
-typedef expr::Attribute<DTypeFiniteTag, bool> DTypeFiniteAttr;
-/** Attribute true when we have computed whether a datatype type is finite */
-struct DTypeFiniteComputedTag
-{
-};
-typedef expr::Attribute<DTypeFiniteComputedTag, bool> DTypeFiniteComputedAttr;
-/**
- * Attribute true for datatype types that are interpreted as finite (see
- * TypeNode::isInterpretedFinite).
- */
-struct DTypeUFiniteTag
-{
-};
-typedef expr::Attribute<DTypeUFiniteTag, bool> DTypeUFiniteAttr;
-/**
- * Attribute true when we have computed whether a datatype type is interpreted
- * as finite.
- */
-struct DTypeUFiniteComputedTag
-{
-};
-typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
// ----------------------- end datatype attributes
class DTypeConstructor;
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
*
/** cache of shared selectors for this datatype */
mutable std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >
d_sharedSel;
+ /** A cache for getCardinalityClass. */
+ mutable std::map<TypeNode, CardinalityClass> d_cardClass;
}; /* class DType */
/**
return c;
}
-bool DTypeConstructor::isFinite(TypeNode t) const
+CardinalityClass DTypeConstructor::getCardinalityClass(TypeNode t) const
{
- std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
- return cinfo.first == CardinalityType::FINITE;
-}
-
-bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
-{
- std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
- return cinfo.first != CardinalityType::INFINITE;
+ std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
+ return cinfo.first;
}
bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
{
- std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+ std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
return cinfo.second;
}
-std::pair<DTypeConstructor::CardinalityType, bool>
-DTypeConstructor::computeCardinalityInfo(TypeNode t) const
+std::pair<CardinalityClass, bool> DTypeConstructor::computeCardinalityInfo(
+ TypeNode t) const
{
- std::map<TypeNode, std::pair<CardinalityType, bool> >::iterator it =
+ std::map<TypeNode, std::pair<CardinalityClass, bool> >::iterator it =
d_cardInfo.find(t);
if (it != d_cardInfo.end())
{
return it->second;
}
- std::pair<CardinalityType, bool> ret(CardinalityType::FINITE, false);
+ std::pair<CardinalityClass, bool> ret(CardinalityClass::ONE, false);
std::vector<TypeNode> instTypes;
std::vector<TypeNode> paramTypes;
bool isParam = t.isParametricDatatype();
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;
#include "expr/dtype_selector.h"
#include "expr/node.h"
#include "expr/type_node.h"
+#include "util/cardinality_class.h"
namespace cvc5 {
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
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
* type t, and a Boolean indicating whether the constructor has any arguments
* that have finite external type.
*/
- std::pair<CardinalityType, bool> computeCardinalityInfo(TypeNode t) const;
+ std::pair<CardinalityClass, bool> computeCardinalityInfo(TypeNode t) const;
/** compute shared selectors
* This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
*/
*/
mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
/** A cache for computeCardinalityInfo. */
- mutable std::map<TypeNode, std::pair<CardinalityType, bool> > d_cardInfo;
+ mutable std::map<TypeNode, std::pair<CardinalityClass, bool> > d_cardInfo;
}; /* class DTypeConstructor */
/**
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<IsFiniteTag, bool> IsFiniteAttr;
-/** Attribute true for types which we have computed the above attribute */
-struct IsFiniteComputedTag
-{
-};
-typedef expr::Attribute<IsFiniteComputedTag, bool> IsFiniteComputedAttr;
+typedef expr::Attribute<TypeCardinalityClassTag, uint64_t>
+ TypeCardinalityClassAttr;
-/** Attribute true for types that are interpreted as finite */
-struct IsInterpretedFiniteTag
-{
-};
-typedef expr::Attribute<IsInterpretedFiniteTag, bool> IsInterpretedFiniteAttr;
-/** Attribute true for types which we have computed the above attribute */
-struct IsInterpretedFiniteComputedTag
-{
-};
-typedef expr::Attribute<IsInterpretedFiniteComputedTag, bool>
- 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<CardinalityClass>(
+ 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<uint64_t>(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<TypeNode> 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<TypeNode> 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<uint64_t>(ret));
return ret;
}
#include "expr/kind.h"
#include "expr/metakind.h"
#include "util/cardinality.h"
+#include "util/cardinality_class.h"
namespace cvc5 {
* @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
*
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.
*
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
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 ) ){
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)
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;
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.
// 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;
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() ){
// 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;
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;
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() ){
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())
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))
{
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
// 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())
{
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
{
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;
}
{
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;
}
// 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;
// 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);
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);
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,
}
for (const Node& set : getOrderedSetsEqClasses())
{
- if (!set.getType().isInterpretedFinite())
+ if (!d_state.isFiniteType(set.getType()))
{
continue;
}
{
Assert(tn.isSequence());
TypeNode etn = tn.getSequenceElementType();
- if (etn.isInterpretedFinite())
+ if (d_state.isFiniteType(etn))
{
// infinite cardinality, we are fine
return;
* 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))
// 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;
}
TheoryIdSet visitedTheories = (*find).second;
- return isAlreadyVisited(visitedTheories, current, parent);
+ return isAlreadyVisited(d_engine, visitedTheories, current, parent);
}
void PreRegisterVisitor::visit(TNode current, TNode parent) {
// 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);
}
TheoryIdSet visitedTheories = (*find).second;
- return isAlreadyVisited(visitedTheories, current, parent);
+ return isAlreadyVisited(d_engine, visitedTheories, current, parent);
}
void SharedTermsVisitor::visit(TNode current, TNode parent) {
}
}
+bool TheoryEngine::isFiniteType(TypeNode tn) const
+{
+ return isCardinalityClassFinite(tn.getCardinalityClass(),
+ options::finiteModelFind());
+}
+
void TheoryEngine::spendResource(Resource r)
{
d_resourceManager->spendResource(r);
*/
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 */
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())
{
{
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;
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
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
return d_valuation.factsEnd(tid);
}
+bool TheoryState::isFiniteType(TypeNode tn) const
+{
+ return d_valuation.isFiniteType(tn);
+}
+
Valuation& TheoryState::getValuation() { return d_valuation; }
} // namespace theory
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();
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")
return theory->facts_end();
}
+bool Valuation::isFiniteType(TypeNode tn) const
+{
+ return d_engine->isFiniteType(tn);
+}
+
} // namespace theory
} // namespace cvc5
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
bool.h
cardinality.cpp
cardinality.h
+ cardinality_class.cpp
+ cardinality_class.h
dense_map.h
divisible.cpp
divisible.h
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff