diff options
Diffstat (limited to 'src/expr/dtype.h')
| -rw-r--r-- | src/expr/dtype.h | 65 |
1 files changed, 63 insertions, 2 deletions
diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 08fe9965b..fea51cd36 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -2,9 +2,9 @@ /*! \file dtype.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -287,6 +287,16 @@ class DType * violated. */ bool isWellFounded() const; + /** + * Does this datatype have nested recursion? This is true if this datatype + * definition contains itself as an alien subfield type, or a variant + * of itself as an alien subfield type (if this datatype is parametric). + * For details see getAlienSubfieldTypes below. + * + * Notice that a type having no nested recursion may have a subfield type that + * has nested recursion. + */ + bool hasNestedRecursion() const; /** is recursive singleton * @@ -489,6 +499,51 @@ class DType * Helper for mkGroundTerm and mkGroundValue above. */ Node mkGroundTermInternal(TypeNode t, bool isValue) const; + /** + * This method is used to get alien subfield types of this datatype. + * + * A subfield type T of a datatype type D is a type such that a value of + * type T may appear as a subterm of a value of type D. + * + * An *alien* subfield type T of a datatype type D is a type such that a + * value v of type T may appear as a subterm of a value of D, and moreover + * v occurs as a strict subterm of a non-datatype term in that value. + * + * For example, the alien subfield types of T in: + * T -> Emp | Container(s : (Set List)) + * List -> nil | cons( head : Int, tail: List) + * are { List, Int }. Notice that Int is an alien subfield type since it + * appears as a subfield type of List, and List is an alien subfield type + * of T. In other words, Int is an alien subfield type due to the above + * definition due to the term (Container (singleton (cons 0 nil))), where + * 0 occurs as a subterm of (singleton (cons 0 nil)). The non-strict + * subfield types of T in this example are { (Set List) }. + * + * For example, the alien subfield types of T in: + * T -> Emp | Container(s : List) + * List -> nil | cons( head : (Set T), tail: List) + * are { T, List, (Set T) }. Notice that T is an alien subfield type of itself + * since List is a subfield type of T and T is an alien subfield type of List. + * Furthermore, List and (Set T) are also alien subfield types of T since + * List is a subfield type of T and T is an alien subfield type of itself. + * + * For example, the alien subfield types of T in: + * T -> Emp | Container(s : (Array Int T)) + * are { T, Int }, where we assume that values of (Array U1 U2) are + * constructed from values of U1 and U2, for all types U1, U2. The non-strict + * subfield types of T in this example are { (Array Int T) }. + * + * @param types The set of types to append the alien subfield types to, + * @param processed The datatypes (cached using d_self) we have processed. If + * the range of this map is true, we have processed the datatype with + * isAlienPos = true. + * @param isAlienPos Whether we are in an alien subfield type position. This + * flag is true if we have traversed beneath a non-datatype type constructor. + */ + void getAlienSubfieldTypes( + std::unordered_set<TypeNode, TypeNodeHashFunction>& types, + std::map<TypeNode, bool>& processed, + bool isAlienPos) const; /** name of this datatype */ std::string d_name; /** the type parameters of this datatype (if this is a parametric datatype) @@ -543,6 +598,12 @@ class DType * not. */ mutable int d_wellFounded; + /** + * Cache of whether this datatype has nested recursion, where 0 means we have + * not computed this information, 1 means it has nested recursion, -1 means it + * does not. + */ + mutable int d_nestedRecursion; /** cache of ground term for this datatype */ mutable std::map<TypeNode, Node> d_groundTerm; /** cache of ground values for this datatype */ |