diff options
Diffstat (limited to 'src/expr/dtype.cpp')
| -rw-r--r-- | src/expr/dtype.cpp | 167 |
1 files changed, 153 insertions, 14 deletions
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) |