return kind::getCardinality(*this);
}
+/** Attribute true for types that are finite */
+struct IsFiniteTag
+{
+};
+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;
+
/** 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<IsInterpretedFiniteTag, bool> IsInterpretedFiniteAttr;
typedef expr::Attribute<IsInterpretedFiniteComputedTag, bool>
IsInterpretedFiniteComputedAttr;
+bool TypeNode::isFinite() { return isFiniteInternal(false); }
+
bool TypeNode::isInterpretedFinite()
+{
+ return isFiniteInternal(options::finiteModelFind());
+}
+
+bool TypeNode::isFiniteInternal(bool usortFinite)
{
// check it is already cached
- if (!getAttribute(IsInterpretedFiniteComputedAttr()))
+ if (usortFinite)
{
- bool isInterpretedFinite = false;
- if (isSort())
+ if (getAttribute(IsInterpretedFiniteComputedAttr()))
{
- // If the finite model finding flag is set, we treat uninterpreted sorts
- // as finite. If it is not set, we treat them implicitly as infinite
- // sorts (that is, their cardinality is not constrained to be finite).
- isInterpretedFinite = options::finiteModelFind();
+ return getAttribute(IsInterpretedFiniteAttr());
}
- else if (isBitVector() || isFloatingPoint())
+ }
+ else if (getAttribute(IsFiniteComputedAttr()))
+ {
+ return getAttribute(IsFiniteAttr());
+ }
+ bool ret = false;
+ if (isSort())
+ {
+ ret = usortFinite;
+ }
+ else if (isBoolean() || isBitVector() || isFloatingPoint())
+ {
+ ret = true;
+ }
+ else if (isString() || isRegExp() || isReal())
+ {
+ ret = false;
+ }
+ else
+ {
+ // recursive case (this may be a parametric sort), we assume infinite for
+ // the moment here to prevent infinite loops
+ if (usortFinite)
{
- isInterpretedFinite = true;
+ setAttribute(IsInterpretedFiniteAttr(), false);
+ setAttribute(IsInterpretedFiniteComputedAttr(), true);
}
- else if (isDatatype())
+ else
+ {
+ setAttribute(IsFiniteAttr(), false);
+ setAttribute(IsFiniteComputedAttr(), true);
+ }
+ if (isDatatype())
{
TypeNode tn = *this;
const Datatype& dt = getDatatype();
- isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
+ ret = usortFinite ? dt.isInterpretedFinite(tn.toType())
+ : dt.isFinite(tn.toType());
}
else if (isArray())
{
TypeNode tnc = getArrayConstituentType();
- if (!tnc.isInterpretedFinite())
+ if (!tnc.isFiniteInternal(usortFinite))
{
// arrays with consistuent type that is infinite are infinite
- isInterpretedFinite = false;
+ ret = false;
}
- else if (getArrayIndexType().isInterpretedFinite())
+ else if (getArrayIndexType().isFiniteInternal(usortFinite))
{
// arrays with both finite consistuent and index types are finite
- isInterpretedFinite = true;
+ ret = true;
}
else
{
// If the consistuent type of the array has cardinality one, then the
// array type has cardinality one, independent of the index type.
- isInterpretedFinite = tnc.getCardinality().isOne();
+ ret = tnc.getCardinality().isOne();
}
}
else if (isSet())
{
- isInterpretedFinite = getSetElementType().isInterpretedFinite();
+ ret = getSetElementType().isFiniteInternal(usortFinite);
}
else if (isFunction())
{
- isInterpretedFinite = true;
+ ret = true;
TypeNode tnr = getRangeType();
- if (!tnr.isInterpretedFinite())
+ if (!tnr.isFiniteInternal(usortFinite))
{
- isInterpretedFinite = false;
+ ret = false;
}
else
{
std::vector<TypeNode> argTypes = getArgTypes();
for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
{
- if (!argTypes[i].isInterpretedFinite())
+ if (!argTypes[i].isFiniteInternal(usortFinite))
{
- isInterpretedFinite = false;
+ ret = false;
break;
}
}
- if (!isInterpretedFinite)
+ if (!ret)
{
// similar to arrays, functions are finite if their range type
// has cardinality one, regardless of the arguments.
- isInterpretedFinite = tnr.getCardinality().isOne();
+ ret = tnr.getCardinality().isOne();
}
}
}
else
{
+ // all types 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.
- isInterpretedFinite = getCardinality().isFinite();
+ ret = getCardinality().isFinite();
}
- setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite);
+ }
+ if (usortFinite)
+ {
+ setAttribute(IsInterpretedFiniteAttr(), ret);
setAttribute(IsInterpretedFiniteComputedAttr(), true);
- return isInterpretedFinite;
}
- return getAttribute(IsInterpretedFiniteAttr());
+ else
+ {
+ setAttribute(IsFiniteAttr(), ret);
+ setAttribute(IsFiniteComputedAttr(), true);
+ }
+ return ret;
}
/** Attribute true for types that are closed enumerable */
projects / cvc5.git / commitdiff