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/theory/quantifiers/term_enumeration.h | |
parent | 44355002ddea45c8b1abd5b20437b7940c90e6fc (diff) |
Make isClosedEnumerable a member of TypeNode (#2434)
Diffstat (limited to 'src/theory/quantifiers/term_enumeration.h')
-rw-r--r-- | src/theory/quantifiers/term_enumeration.h | 24 |
1 files changed, 9 insertions, 15 deletions
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 */ |