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.
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(); }
*/
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
*/
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");
* 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
*
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
+#include "expr/type_matcher.h"
using namespace CVC4::kind;
d_sygusAllowConst(false),
d_sygusAllowAll(false),
d_card(CardinalityUnknown()),
- d_wellFounded(0)
+ d_wellFounded(0),
+ d_nestedRecursion(0)
{
}
d_sygusAllowConst(false),
d_sygusAllowAll(false),
d_card(CardinalityUnknown()),
- d_wellFounded(0)
+ d_wellFounded(0),
+ d_nestedRecursion(0)
{
}
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
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)
* 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
*
* 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)
* 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 */
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());
{
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]))
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"
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:
void testDatatypeStructs();
void testDatatypeNames();
+ void testParametricDatatype();
+
+ void testDatatypeSimplyRec();
+
private:
Solver d_solver;
};
// possible to construct null datatype declarations if not using solver
TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
}
+
+void DatatypeBlack::testParametricDatatype()
+{
+ std::vector<Sort> 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<Sort> 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<DatatypeDecl> dtdecls;
+ dtdecls.push_back(wlist);
+ dtdecls.push_back(list);
+ dtdecls.push_back(ns);
+ // this is well-founded and has no nested recursion
+ std::vector<Sort> 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<Sort> v;
+ Sort x = d_solver.mkParamSort("X");
+ v.push_back(x);
+ DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v);
+
+ std::vector<Sort> 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());
+}
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() {
projects / cvc5.git / commitdiff