diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 4 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 11 | ||||
-rw-r--r-- | src/expr/datatype.cpp | 6 | ||||
-rw-r--r-- | src/expr/datatype.h | 6 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 167 | ||||
-rw-r--r-- | src/expr/dtype.h | 61 | ||||
-rw-r--r-- | src/expr/node_algorithm.cpp | 8 | ||||
-rw-r--r-- | src/expr/type_matcher.cpp | 5 | ||||
-rw-r--r-- | src/options/datatypes_options.toml | 9 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 22 |
10 files changed, 281 insertions, 18 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 164df0631..2c65f1ca6 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2191,6 +2191,10 @@ bool Datatype::isRecord() const { return d_dtype->isRecord(); } bool Datatype::isFinite() const { return d_dtype->isFinite(); } bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); } +bool Datatype::hasNestedRecursion() const +{ + return d_dtype->hasNestedRecursion(); +} std::string Datatype::toString() const { return d_dtype->getName(); } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 73e3ed856..adf3691ab 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1673,6 +1673,17 @@ class CVC4_PUBLIC Datatype bool isWellFounded() const; /** + * Does this datatype have nested recursion? This method returns false if a + * value of this datatype includes a subterm of its type that is nested + * beneath a non-datatype type constructor. For example, a datatype + * T containing a constructor having a selector with range type (Set T) has + * nested recursion. + * + * @return true if this datatype has nested recursion + */ + bool hasNestedRecursion() const; + + /** * @return a string representation of this datatype */ std::string toString() const; diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 3925e1434..b33580b09 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -406,6 +406,12 @@ bool Datatype::isWellFounded() const return d_internal->isWellFounded(); } +bool Datatype::hasNestedRecursion() const +{ + ExprManagerScope ems(d_self); + return d_internal->hasNestedRecursion(); +} + Expr Datatype::mkGroundTerm(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 0f99499ce..daef7cc94 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -705,6 +705,12 @@ class CVC4_PUBLIC Datatype { * This datatype must be resolved or an exception is thrown. */ bool isWellFounded() const; + /** has nested recursion + * + * Return true iff this datatype has nested recursion. + * This datatype must be resolved or an exception is thrown. + */ + bool hasNestedRecursion() const; /** is recursive singleton * diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index f16b193ce..ff9880b94 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -14,6 +14,7 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" +#include "expr/type_matcher.h" using namespace CVC4::kind; @@ -32,7 +33,8 @@ DType::DType(std::string name, bool isCo) d_sygusAllowConst(false), d_sygusAllowAll(false), d_card(CardinalityUnknown()), - d_wellFounded(0) + d_wellFounded(0), + d_nestedRecursion(0) { } @@ -49,7 +51,8 @@ DType::DType(std::string name, const std::vector<TypeNode>& params, bool isCo) d_sygusAllowConst(false), d_sygusAllowAll(false), d_card(CardinalityUnknown()), - d_wellFounded(0) + d_wellFounded(0), + d_nestedRecursion(0) { } @@ -471,21 +474,26 @@ bool DType::isInterpretedFinite() const bool DType::isWellFounded() const { - Trace("datatypes-init") << "DType::isWellFounded " << std::endl; Assert(isResolved()); - if (d_wellFounded == 0) + if (d_wellFounded != 0) { - std::vector<TypeNode> processing; - if (computeWellFounded(processing)) - { - d_wellFounded = 1; - } - else - { - d_wellFounded = -1; - } + // already computed + return d_wellFounded == 1; } - return d_wellFounded == 1; + Trace("datatypes-init") << "DType::isWellFounded " << getName() << std::endl; + std::vector<TypeNode> processing; + if (!computeWellFounded(processing)) + { + // not well-founded since no ground term can be constructed + Trace("datatypes-init") << "DType::isWellFounded: false for " << getName() + << " due to no ground terms." << std::endl; + d_wellFounded = -1; + return false; + } + Trace("datatypes-init") << "DType::isWellFounded: true for " << getName() + << std::endl; + d_wellFounded = 1; + return true; } bool DType::computeWellFounded(std::vector<TypeNode>& processing) const @@ -557,6 +565,137 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const return groundTerm; } +void DType::getAlienSubfieldTypes( + std::unordered_set<TypeNode, TypeNodeHashFunction>& types, + std::map<TypeNode, bool>& processed, + bool isAlienPos) const +{ + std::map<TypeNode, bool>::iterator it = processed.find(d_self); + if (it != processed.end()) + { + if (it->second || (!isAlienPos && !it->second)) + { + // already processed as an alien subfield type, or already processed + // as a non-alien subfield type and isAlienPos is false. + return; + } + } + processed[d_self] = isAlienPos; + for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) + { + for (unsigned j = 0, nargs = ctor->getNumArgs(); j < nargs; ++j) + { + TypeNode tn = ctor->getArgType(j); + if (tn.isDatatype()) + { + // special case for datatypes, we must recurse to collect subfield types + if (!isAlienPos) + { + // since we aren't adding it to types below, we add its alien + // subfield types here. + const DType& dt = tn.getDType(); + dt.getAlienSubfieldTypes(types, processed, false); + } + if (tn.isParametricDatatype() && !isAlienPos) + { + // (instantiated) parametric datatypes have an AST structure: + // (PARAMETRIC_DATATYPE D T1 ... Tn) + // where D is the uninstantiated datatype type. We should not view D + // as an alien subfield type of tn. Thus, we need a special case here + // which ignores the first child, when isAlienPos is false. + for (unsigned i = 1, nchild = tn.getNumChildren(); i < nchild; i++) + { + expr::getComponentTypes(tn[i], types); + } + continue; + } + } + // we are in a case where tn is not a datatype, we add all (alien) + // component types to types below. + bool hasTn = types.find(tn) != types.end(); + Trace("datatypes-init") + << "Collect subfield types " << tn << ", hasTn=" << hasTn + << ", isAlienPos=" << isAlienPos << std::endl; + expr::getComponentTypes(tn, types); + if (!isAlienPos && !hasTn) + { + // the top-level type is added by getComponentTypes, so remove it if it + // was not already listed in types + Assert(types.find(tn) != types.end()); + types.erase(tn); + } + } + } + // Now, go back and add all alien subfield types from datatypes if + // not done so already. This is because getComponentTypes does not + // recurse into subfield types of datatypes. + for (const TypeNode& sstn : types) + { + if (sstn.isDatatype()) + { + const DType& dt = sstn.getDType(); + dt.getAlienSubfieldTypes(types, processed, true); + } + } +} + +bool DType::hasNestedRecursion() const +{ + if (d_nestedRecursion != 0) + { + return d_nestedRecursion == 1; + } + Trace("datatypes-init") << "Compute simply recursive for " << getName() + << std::endl; + // get the alien subfield types of this datatype + std::unordered_set<TypeNode, TypeNodeHashFunction> types; + std::map<TypeNode, bool> processed; + getAlienSubfieldTypes(types, processed, false); + if (Trace.isOn("datatypes-init")) + { + Trace("datatypes-init") << "Alien subfield types: " << std::endl; + for (const TypeNode& t : types) + { + Trace("datatypes-init") << "- " << t << std::endl; + } + } + // does types contain self? + if (types.find(d_self) != types.end()) + { + Trace("datatypes-init") + << "DType::hasNestedRecursion: true for " << getName() + << " due to alien subfield type" << std::endl; + // has nested recursion since it has itself as an alien subfield type. + d_nestedRecursion = 1; + return true; + } + // If it is parametric, this type may match with an alien subfield type (e.g. + // we may have a field (T Int) for parametric datatype (T x) where x + // is a type parameter). Thus, we check whether the self type matches any + // alien subfield type using the TypeMatcher utility. + if (isParametric()) + { + for (const TypeNode& t : types) + { + TypeMatcher m(d_self); + Trace("datatypes-init") << " " << t << std::endl; + if (m.doMatching(d_self, t)) + { + Trace("datatypes-init") + << "DType::hasNestedRecursion: true for " << getName() + << " due to parametric strict component type, " << d_self + << " matching " << t << std::endl; + d_nestedRecursion = 1; + return true; + } + } + } + Trace("datatypes-init") << "DType::hasNestedRecursion: false for " + << getName() << std::endl; + d_nestedRecursion = -1; + return false; +} + Node getSubtermWithType(Node e, TypeNode t, bool isTop) { if (!isTop && e.getType() == t) diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 08fe9965b..f9c4eff9c 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -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 */ diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 44430f072..358023647 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -622,13 +622,13 @@ void getComponentTypes( TypeNode curr = toProcess.back(); toProcess.pop_back(); // if not already visited - if (types.find(t) == types.end()) + if (types.find(curr) == types.end()) { - types.insert(t); + types.insert(curr); // get component types from the children - for (unsigned i = 0, nchild = t.getNumChildren(); i < nchild; i++) + for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++) { - toProcess.push_back(t[i]); + toProcess.push_back(curr[i]); } } } while (!toProcess.empty()); diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index f99c8a2da..479d2127f 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -86,6 +86,11 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn) { return false; } + else if (pattern.getNumChildren() == 0) + { + // fail if the type parameter or type constructors are different + return pattern == tn; + } for (size_t j = 0, nchild = pattern.getNumChildren(); j < nchild; j++) { if (!doMatching(pattern[j], tn[j])) diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index ac371efeb..19434fa33 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -68,6 +68,15 @@ header = "options/datatypes_options.h" help = "when applicable, blast splitting lemmas for all variables at once" [[option]] + name = "dtNestedRec" + category = "regular" + long = "dt-nested-rec" + type = "bool" + default = "false" + read_only = true + help = "allow nested recursion in datatype definitions" + +[[option]] name = "dtSharedSelectors" category = "regular" long = "dt-share-sel" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9c8e9e2fa..6e5b028a7 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -561,6 +561,28 @@ void TheoryDatatypes::finishInit() { Node TheoryDatatypes::expandDefinition(Node n) { NodeManager* nm = NodeManager::currentNM(); + // must ensure the type is well founded and has no nested recursion if + // the option dtNestedRec is not set to true. + TypeNode tn = n.getType(); + if (tn.isDatatype()) + { + const DType& dt = tn.getDType(); + if (!dt.isWellFounded()) + { + std::stringstream ss; + ss << "Cannot handle non-well-founded datatype " << dt.getName(); + throw LogicException(ss.str()); + } + if (!options::dtNestedRec()) + { + if (dt.hasNestedRecursion()) + { + std::stringstream ss; + ss << "Cannot handle nested-recursive datatype " << dt.getName(); + throw LogicException(ss.str()); + } + } + } switch (n.getKind()) { case kind::APPLY_SELECTOR: |