return getAttribute(IsInterpretedFiniteAttr());
}
+/** Attribute true for types that are closed enumerable */
+struct IsClosedEnumerableTag
+{
+};
+struct IsClosedEnumerableComputedTag
+{
+};
+typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
+typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
+ IsClosedEnumerableComputedAttr;
+
+bool TypeNode::isClosedEnumerable()
+{
+ // check it is already cached
+ if (!getAttribute(IsClosedEnumerableComputedAttr()))
+ {
+ bool ret = true;
+ if (isArray() || isSort() || isCodatatype() || isFunction())
+ {
+ ret = false;
+ }
+ else if (isSet())
+ {
+ ret = getSetElementType().isClosedEnumerable();
+ }
+ else if (isDatatype())
+ {
+ // avoid infinite loops: initially set to true
+ setAttribute(IsClosedEnumerableAttr(), ret);
+ setAttribute(IsClosedEnumerableComputedAttr(), true);
+ TypeNode tn = *this;
+ const Datatype& dt = getDatatype();
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+ if (tn != ctn && !ctn.isClosedEnumerable())
+ {
+ ret = false;
+ break;
+ }
+ }
+ if (!ret)
+ {
+ break;
+ }
+ }
+ }
+ setAttribute(IsClosedEnumerableAttr(), ret);
+ setAttribute(IsClosedEnumerableComputedAttr(), true);
+ return ret;
+ }
+ return getAttribute(IsClosedEnumerableAttr());
+}
+
bool TypeNode::isFirstClass() const {
return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) &&
getKind() != kind::CONSTRUCTOR_TYPE &&
*/
bool isInterpretedFinite();
+ /** is closed enumerable type
+ *
+ * This returns true if this type has an enumerator that produces constants
+ * that are fully handled by CVC4's quantifier-free theory solvers. Examples
+ * of types that are not closed enumerable are:
+ * (1) uninterpreted sorts,
+ * (2) arrays,
+ * (3) codatatypes,
+ * (4) functions,
+ * (5) parametric sorts involving any of the above.
+ */
+ bool isClosedEnumerable();
+
/**
* Is this a first-class type?
* First-class types are types for which:
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
- d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
+ d_closed_enum_type = tn.isClosedEnumerable();
}
bool Instantiator::processEqualTerm(CegInstantiator* ci,
for( unsigned i=0; i<n.getNumChildren(); i++ ){
vec.push_back( 0 );
TypeNode tn = n[i].getType();
- if (te->isClosedEnumerableType(tn))
+ if (tn.isClosedEnumerable())
{
types.push_back( tn );
}else{
if (d_model_basis_term.find(tn) == d_model_basis_term.end())
{
Node mbt;
- if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+ if (tn.isClosedEnumerable())
{
mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
}
Node Instantiate::getTermForType(TypeNode tn)
{
- if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+ if (tn.isClosedEnumerable())
{
return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
}
return d_enum_terms[tn][index];
}
-bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
-{
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
- d_typ_closed_enum.find(tn);
- if (it == d_typ_closed_enum.end())
- {
- d_typ_closed_enum[tn] = true;
- bool ret = true;
- if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
- {
- ret = false;
- }
- else if (tn.isSet())
- {
- ret = isClosedEnumerableType(tn.getSetElementType());
- }
- else if (tn.isDatatype())
- {
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for (unsigned i = 0; i < dt.getNumConstructors(); i++)
- {
- for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
- {
- TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
- if (tn != ctn && !isClosedEnumerableType(ctn))
- {
- ret = false;
- break;
- }
- }
- if (!ret)
- {
- break;
- }
- }
- }
-
- // other parametric sorts go here
-
- d_typ_closed_enum[tn] = ret;
- return ret;
- }
- else
- {
- return it->second;
- }
-}
-
-// checks whether a type is closed enumerable and is reasonably small enough (<1000)
-// such that all of its domain elements can be enumerated
bool TermEnumeration::mayComplete(TypeNode tn)
{
std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
d_may_complete.find(tn);
if (it == d_may_complete.end())
{
- bool mc = false;
- if (isClosedEnumerableType(tn) && tn.isInterpretedFinite())
- {
- Cardinality c = tn.getCardinality();
- if (!c.isLargeFinite())
- {
- NodeManager* nm = NodeManager::currentNM();
- Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
- // check if less than fixed upper bound, default 1000
- Node oth = nm->mkConst(Rational(options::fmfTypeCompletionThresh()));
- Node eq = nm->mkNode(LEQ, card, oth);
- eq = Rewriter::rewrite(eq);
- mc = eq.isConst() && eq.getConst<bool>();
- }
- }
+ // cache
+ bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
d_may_complete[tn] = mc;
return mc;
}
- else
+ return it->second;
+}
+
+bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
+{
+ bool mc = false;
+ if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
{
- return it->second;
+ Cardinality c = tn.getCardinality();
+ if (!c.isLargeFinite())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+ // check if less than fixed upper bound
+ Node oth = nm->mkConst(Rational(maxCard));
+ Node eq = nm->mkNode(LEQ, card, oth);
+ eq = Rewriter::rewrite(eq);
+ mc = eq.isConst() && eq.getConst<bool>();
+ }
}
+ return mc;
}
} /* CVC4::theory::quantifiers namespace */
~TermEnumeration() {}
/** get i^th term for type tn */
Node getEnumerateTerm(TypeNode tn, unsigned i);
- /** is closed enumerable type
- *
- * This returns true if this type has an enumerator that produces
- * constants that are handled by ground theory solvers.
- * Examples of types that are not closed enumerable are:
- * (1) uninterpreted sorts,
- * (2) arrays,
- * (3) codatatypes,
- * (4) parametric sorts involving any of the above.
- */
- bool isClosedEnumerableType(TypeNode tn);
/** may complete type
*
- * Returns true if the type tn is closed
- * enumerable, and is small enough
- * for finite model finding to enumerate it,
- * by some heuristic (current cardinality < 1000).
+ * Returns true if the type tn is closed enumerable, is interpreted as a
+ * finite type, and has cardinality less than some reasonable value
+ * (currently < 1000). This method caches the results of whether each type
+ * may be completed.
*/
bool mayComplete(TypeNode tn);
+ /**
+ * Static version of the above method where maximum cardinality is
+ * configurable.
+ */
+ static bool mayComplete(TypeNode tn, unsigned cardMax);
private:
/** ground terms enumerated for types */
projects / cvc5.git / commitdiff