From: Andrew Reynolds Date: Fri, 5 Jun 2020 22:57:25 +0000 (-0500) Subject: Datatypes with nested recursion are not handled in TheoryDatatypes unless option... X-Git-Tag: cvc5-1.0.0~3245 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8015e6dc858a3fd13234ec4acb22c80cb339ddc;p=cvc5.git Datatypes with nested recursion are not handled in TheoryDatatypes unless option is set (#3707) Towards experimental support for non-simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec). Builds a check for non-simple recursion in the DType class. If a term of a datatype type is registered to TheoryDatatypes for a datatype that has nested recursion, we throw a LogicException unless the option dtNestedRec is set to true. Also includes a bug discovered in the TypeMatcher utility and another in expr::getComponentTypes. It also adds a unit test using the new API for a simple parametric datatype example as well, not related to nested recursion, as this was previously missing. --- 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 @@ -1672,6 +1672,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 */ 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& 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 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 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& processing) const @@ -557,6 +565,137 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const return groundTerm; } +void DType::getAlienSubfieldTypes( + std::unordered_set& types, + std::map& processed, + bool isAlienPos) const +{ + std::map::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 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 types; + std::map 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& types, + std::map& 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 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 @@ -67,6 +67,15 @@ header = "options/datatypes_options.h" read_only = true 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" 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: diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index c9eaf103e..180db8f32 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -32,6 +32,10 @@ class DatatypeBlack : public CxxTest::TestSuite void testDatatypeStructs(); void testDatatypeNames(); + void testParametricDatatype(); + + void testDatatypeSimplyRec(); + private: Solver d_solver; }; @@ -233,3 +237,285 @@ void DatatypeBlack::testDatatypeNames() // possible to construct null datatype declarations if not using solver TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); } + +void DatatypeBlack::testParametricDatatype() +{ + std::vector v; + Sort t1 = d_solver.mkParamSort("T1"); + Sort t2 = d_solver.mkParamSort("T2"); + v.push_back(t1); + v.push_back(t2); + DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); + + DatatypeConstructorDecl mkpair = + d_solver.mkDatatypeConstructorDecl("mk-pair"); + mkpair.addSelector("first", t1); + mkpair.addSelector("second", t2); + pairSpec.addConstructor(mkpair); + + Sort pairType = d_solver.mkDatatypeSort(pairSpec); + + TS_ASSERT(pairType.getDatatype().isParametric()); + + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairIntInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getRealSort()); + Sort pairRealReal = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairRealInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getRealSort()); + Sort pairIntReal = pairType.instantiate(v); + + TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); + TS_ASSERT_DIFFERS(pairRealInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntInt, pairIntReal); + TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); + TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); + + TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); + TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); + TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); + TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); + + TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt)); + TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal)); + TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt)); + TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt)); +} + +void DatatypeBlack::testDatatypeSimplyRec() +{ + /* Create mutual datatypes corresponding to this definition block: + * + * DATATYPE + * wlist = leaf(data: list), + * list = cons(car: wlist, cdr: list) | nil, + * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresWList = d_solver.mkUninterpretedSort("wlist"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresNs = d_solver.mkUninterpretedSort("ns"); + unresTypes.insert(unresWList); + unresTypes.insert(unresList); + unresTypes.insert(unresNs); + + DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + wlist.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresWList); + cons.addSelector("cdr", unresList); + list.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); + DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); + elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); + ns.addConstructor(elem); + DatatypeConstructorDecl elemArray = + d_solver.mkDatatypeConstructorDecl("elemArray"); + elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); + ns.addConstructor(elemArray); + + std::vector dtdecls; + dtdecls.push_back(wlist); + dtdecls.push_back(list); + dtdecls.push_back(ns); + // this is well-founded and has no nested recursion + std::vector dtsorts; + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 3); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[2].getDatatype().isWellFounded()); + TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion()); + TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * ns2 = elem2(ndata: array(int,ns2)) | nil2 + * END; + */ + unresTypes.clear(); + Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + unresTypes.insert(unresNs2); + + DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); + DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); + elem2.addSelector("ndata", + d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); + ns2.addConstructor(elem2); + DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); + ns2.addConstructor(nil2); + + dtdecls.clear(); + dtdecls.push_back(ns2); + + dtsorts.clear(); + // this is not well-founded due to non-simple recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 1); + TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); + TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() + == dtsorts[0]); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list3 = cons3(car: ns3, cdr: list3) | nil3, + * ns3 = elem3(ndata: set(list3)) + * END; + */ + unresTypes.clear(); + Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + unresTypes.insert(unresNs3); + Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + unresTypes.insert(unresList3); + + DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); + DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); + cons3.addSelector("car", unresNs3); + cons3.addSelector("cdr", unresList3); + list3.addConstructor(cons3); + DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); + list3.addConstructor(nil3); + + DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); + DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); + ns3.addConstructor(elem3); + + dtdecls.clear(); + dtdecls.push_back(list3); + dtdecls.push_back(ns3); + + dtsorts.clear(); + // both are well-founded and have nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 2); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list4 = cons(car: set(ns4), cdr: list4) | nil, + * ns4 = elem(ndata: list4) + * END; + */ + unresTypes.clear(); + Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + unresTypes.insert(unresNs4); + Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + unresTypes.insert(unresList4); + + DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); + DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); + cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); + cons4.addSelector("cdr", unresList4); + list4.addConstructor(cons4); + DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); + list4.addConstructor(nil4); + + DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); + DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem4.addSelector("ndata", unresList4); + ns4.addConstructor(elem4); + + dtdecls.clear(); + dtdecls.push_back(list4); + dtdecls.push_back(ns4); + + dtsorts.clear(); + // both are well-founded and have nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 2); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + * END; + */ + unresTypes.clear(); + Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + unresTypes.insert(unresList5); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList5.instantiate(args); + args[0] = urListX; + Sort urListListX = unresList5.instantiate(args); + + DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); + cons5.addSelector("car", x); + cons5.addSelector("cdr", urListListX); + list5.addConstructor(cons5); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); + list5.addConstructor(nil5); + + dtdecls.clear(); + dtdecls.push_back(list5); + + // well-founded and has nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 1); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); +} diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index a829d9a8d..f1691edd4 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -254,7 +254,10 @@ public: tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;"); //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); - tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); + tryGoodInput( + "DATATYPE trex = Foo | Bar END; DATATYPE tree = " + "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list " + "OF tree,cdr:BITVECTOR(32)) END;"); } void testBadCvc4Inputs() {