From: Andrew Reynolds Date: Fri, 7 Sep 2018 15:42:41 +0000 (-0500) Subject: Make isClosedEnumerable a member of TypeNode (#2434) X-Git-Tag: cvc5-1.0.0~4671 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8baaa9730b2d4fa4d42587c3a1b701e77c6f78a;p=cvc5.git Make isClosedEnumerable a member of TypeNode (#2434) --- diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 6616f470f..b54290612 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -165,6 +165,62 @@ bool TypeNode::isInterpretedFinite() return getAttribute(IsInterpretedFiniteAttr()); } +/** Attribute true for types that are closed enumerable */ +struct IsClosedEnumerableTag +{ +}; +struct IsClosedEnumerableComputedTag +{ +}; +typedef expr::Attribute IsClosedEnumerableAttr; +typedef expr::Attribute + 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 && diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9cb6efc29..5b0caf659 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -429,6 +429,19 @@ public: */ 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: diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index b90d98ca6..46649154e 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -29,7 +29,6 @@ #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" @@ -1645,7 +1644,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st 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, diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 69f89021b..0dc704219 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1088,7 +1088,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< for( unsigned i=0; iisClosedEnumerableType(tn)) + if (tn.isClosedEnumerable()) { types.push_back( tn ); }else{ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 1e3116f43..0eec40de2 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -317,7 +317,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn) 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); } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index eab05f454..24f418b0c 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -491,7 +491,7 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) Node Instantiate::getTermForType(TypeNode tn) { - if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn)) + if (tn.isClosedEnumerable()) { return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); } diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 34b9d7e81..8e3219768 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -53,84 +53,38 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) return d_enum_terms[tn][index]; } -bool TermEnumeration::isClosedEnumerableType(TypeNode tn) -{ - std::unordered_map::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::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(); - } - } + // 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(); + } } + return mc; } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index cede77dbe..cf25335f4 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -42,25 +42,19 @@ class TermEnumeration ~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 */