diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-07 10:42:41 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-09-07 10:42:41 -0500 |
commit | b8baaa9730b2d4fa4d42587c3a1b701e77c6f78a (patch) | |
tree | a5f6957fce0723c9e22ae75bb17a4f1a96aae449 /src/expr | |
parent | 44355002ddea45c8b1abd5b20437b7940c90e6fc (diff) |
Make isClosedEnumerable a member of TypeNode (#2434)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/type_node.cpp | 56 | ||||
-rw-r--r-- | src/expr/type_node.h | 13 |
2 files changed, 69 insertions, 0 deletions
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<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 && 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: |