In preparation for #8511.
This makes it so that unresolved sorts are automatically inferred when constructing datatypes at the NodeManager level. This is in preparation for simplifying the API.
Changes:
(1) NodeManager is cleaned so that unresolved types are automatically inferred and are not a part of its public interface. Internal code generating datatypes is simplified as a result.
(2) Adds necessary utilities to TypeNode and cleans an unused flag
(3) The parser is cleaned to not track unresolved sorts in an ad-hoc manner.
(4) The API is patched to use the simpler interface.
// make the unresolved type, used for referencing the final version of
// the ntsymbol's datatype
ntsToUnres[ntsymbol] =
- Sort(d_solver, d_solver->getNodeManager()->mkSort(ntsymbol.toString()));
+ Sort(d_solver,
+ d_solver->getNodeManager()->mkUnresolvedDatatypeSort(
+ ntsymbol.toString()));
}
std::vector<internal::DType> datatypes;
std::vector<internal::TypeNode> datatypeTypes =
d_solver->getNodeManager()->mkMutualDatatypeTypes(
datatypes,
- unresTypes,
internal::NodeManager::DATATYPE_FLAG_PLACEHOLDER);
// return is the first datatype
datatypes.push_back(dtypedecls[i].getDatatype());
}
- std::set<internal::TypeNode> utypes =
- Sort::sortSetToTypeNodes(unresolvedSorts);
std::vector<internal::TypeNode> dtypes =
- getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
+ getNodeManager()->mkMutualDatatypeTypes(datatypes);
std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes);
return retTypes;
}
//////// all checks before this line
internal::TypeNode tn =
- symbol ? getNodeManager()->mkSort(
- *symbol, internal::NodeManager::SORT_FLAG_PLACEHOLDER)
- : getNodeManager()->mkSort(
- internal::NodeManager::SORT_FLAG_PLACEHOLDER);
+ symbol ? getNodeManager()->mkSort(*symbol) : getNodeManager()->mkSort();
return Sort(this, tn);
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- if (arity)
- {
- return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity));
- }
- return Sort(this, getNodeManager()->mkSort(symbol));
+ return Sort(this, getNodeManager()->mkUnresolvedDatatypeSort(symbol, arity));
////////
CVC5_API_TRY_CATCH_END;
}
return item.getAttribute(DTypeConsIndexAttr());
}
+void DType::collectUnresolvedDatatypeTypes(std::set<TypeNode>& unresTypes) const
+{
+ // Scan the arguments of all constructors and collect their types. To be
+ // robust to datatypes with nested recursion, we collect the *component*
+ // types of all subfield types and store them in csfTypes. In other words, we
+ // search for unresolved datatypes that occur possibly as parameters to
+ // other parametric types.
+ std::unordered_set<TypeNode> csfTypes;
+ for (const std::shared_ptr<DTypeConstructor>& ctor : d_constructors)
+ {
+ for (size_t i = 0, nargs = ctor->getNumArgs(); i < nargs; i++)
+ {
+ Node sel = (*ctor)[i].d_selector;
+ if (sel.isNull())
+ {
+ // we currently permit null selector for representing self selectors,
+ // skip these.
+ continue;
+ }
+ // The selector has *not* been initialized to a variable of selector type,
+ // which is done during resolve. Instead, we get the raw type of sel
+ // and compute its component types.
+ expr::getComponentTypes(sel.getType(), csfTypes);
+ }
+ }
+ // Now, process each component type
+ for (const TypeNode& arg : csfTypes)
+ {
+ if (arg.isUnresolvedDatatype())
+ {
+ // it is an unresolved datatype
+ unresTypes.insert(arg);
+ }
+ else if (arg.isInstantiatedUninterpretedSort())
+ {
+ // it might be an instantiated sort constructor corresponding to a
+ // unresolved parametric datatype, in which case we extract its operator
+ TypeNode argc = arg.getUninterpretedSortConstructor();
+ if (argc.isUnresolvedDatatype())
+ {
+ unresTypes.insert(argc);
+ }
+ }
+ }
+}
+
bool DType::resolve(const std::map<std::string, TypeNode>& resolutions,
const std::vector<TypeNode>& placeholders,
const std::vector<TypeNode>& replacements,
void toStream(std::ostream& out) const;
private:
+ /**
+ * Collect unresolved datatype types. This is called by NodeManager when
+ * constructing datatypes from datatype declarations. This adds all
+ * unresolved datatype types to unresTypes, which are then considered
+ * when constructing the datatype (for details, see
+ * NodeManager::mkMutualDatatypeTypesInternal).
+ */
+ void collectUnresolvedDatatypeTypes(std::set<TypeNode>& unresTypes) const;
/**
* DTypes refer to themselves, recursively, and we have a
* chicken-and-egg problem. The TypeNode around the DType
Assert(name != "");
}
-void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
+void DTypeConstructor::addArg(std::string selectorName, TypeNode rangeType)
{
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the selector type away inside a var until resolution (when we can
// create the proper selector type)
Assert(!isResolved());
- Assert(!selectorType.isNull());
+ Assert(!rangeType.isNull());
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
Node sel = sm->mkDummySkolem("unresolved_" + selectorName,
- selectorType,
+ rangeType,
"is an unresolved selector type placeholder",
SkolemManager::SKOLEM_EXACT_NAME);
// can use null updater for now
* to this constructor. Selector names need not be unique;
* they are for convenience and pretty-printing only.
*/
- void addArg(std::string selectorName, TypeNode selectorType);
+ void addArg(std::string selectorName, TypeNode rangeType);
/**
* Add an argument, given a pointer to a selector object.
*/
return d_constructor;
}
-TypeNode DTypeSelector::getType() const { return d_selector.getType(); }
+TypeNode DTypeSelector::getType() const
+{
+ Assert(!d_selector.isNull());
+ return d_selector.getType();
+}
TypeNode DTypeSelector::getRangeType() const
{
struct SortArityTag { };
struct TypeTag { };
struct TypeCheckedTag { };
+ struct UnresolvedDatatypeTag
+ {
+ };
} // namespace attr
typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
+/** Attribute is true for unresolved datatype sorts */
+using UnresolvedDatatypeAttr =
+ expr::Attribute<expr::attr::UnresolvedDatatypeTag, bool>;
+
} // namespace expr
} // namespace cvc5::internal
const std::vector<DType>& datatypes, uint32_t flags)
{
std::set<TypeNode> unresolvedTypes;
- return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags);
+ // scan the list of datatypes to find unresolved datatypes
+ for (const DType& dt : datatypes)
+ {
+ dt.collectUnresolvedDatatypeTypes(unresolvedTypes);
+ }
+ return mkMutualDatatypeTypesInternal(datatypes, unresolvedTypes, flags);
}
-std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
+std::vector<TypeNode> NodeManager::mkMutualDatatypeTypesInternal(
const std::vector<DType>& datatypes,
const std::set<TypeNode>& unresolvedTypes,
uint32_t flags)
size_t NodeManager::poolSize() const { return d_nodeValuePool.size(); }
-TypeNode NodeManager::mkSort(uint32_t flags)
+TypeNode NodeManager::mkSort()
{
NodeBuilder nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder(this, kind::SORT_TAG);
return nb.constructTypeNode();
}
-TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags)
+TypeNode NodeManager::mkSort(const std::string& name)
{
NodeBuilder nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder(this, kind::SORT_TAG);
}
TypeNode NodeManager::mkSort(TypeNode constructor,
- const std::vector<TypeNode>& children,
- uint32_t flags)
+ const std::vector<TypeNode>& children)
{
Assert(constructor.getKind() == kind::SORT_TYPE
&& constructor.getNumChildren() == 0)
return type;
}
-TypeNode NodeManager::mkSortConstructor(const std::string& name,
- size_t arity,
- uint32_t flags)
+TypeNode NodeManager::mkSortConstructor(const std::string& name, size_t arity)
{
Assert(arity > 0);
NodeBuilder nb(this, kind::SORT_TYPE);
return type;
}
+TypeNode NodeManager::mkUnresolvedDatatypeSort(const std::string& name,
+ size_t arity)
+{
+ TypeNode usort = arity > 0 ? mkSortConstructor(name, arity) : mkSort(name);
+ // mark that it is an unresolved sort
+ setAttribute(usort, expr::UnresolvedDatatypeAttr(), true);
+ return usort;
+}
+
Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
{
Node n = NodeBuilder(this, kind::VARIABLE);
std::vector<TypeNode> mkMutualDatatypeTypes(
const std::vector<DType>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
- /**
- * Make a set of types representing the given datatypes, which may
- * be mutually recursive. unresolvedTypes is a set of SortTypes
- * that were used as placeholders in the Datatypes for the Datatypes
- * of the same name. This is just a more complicated version of the
- * above mkMutualDatatypeTypes() function, but is required to handle
- * complex types.
- *
- * For example, unresolvedTypes might contain the single sort "list"
- * (with that name reported from SortType::getName()). The
- * datatypes list might have the single datatype
- *
- * DATATYPE
- * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
- * END;
- *
- * To represent the Type of the array, the user had to create a
- * placeholder type (an uninterpreted sort) to stand for "list" in
- * the type of "car". It is this placeholder sort that should be
- * passed in unresolvedTypes. If the datatype was of the simpler
- * form:
- *
- * DATATYPE
- * list = cons(car:list, cdr:list) | nil;
- * END;
- *
- * then no complicated Type needs to be created, and the above,
- * simpler form of mkMutualDatatypeTypes() is enough.
- */
- std::vector<TypeNode> mkMutualDatatypeTypes(
- const std::vector<DType>& datatypes,
- const std::set<TypeNode>& unresolvedTypes,
- uint32_t flags = DATATYPE_FLAG_NONE);
-
/**
* Make a type representing a constructor with the given argument (subfield)
* types and return type range.
TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
/** Make a new (anonymous) sort of arity 0. */
- TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE);
+ TypeNode mkSort();
/** Make a new sort with the given name of arity 0. */
- TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE);
+ TypeNode mkSort(const std::string& name);
/** Make a new sort by parameterizing the given sort constructor. */
- TypeNode mkSort(TypeNode constructor,
- const std::vector<TypeNode>& children,
- uint32_t flags = SORT_FLAG_NONE);
+ TypeNode mkSort(TypeNode constructor, const std::vector<TypeNode>& children);
/** Make a new sort with the given name and arity. */
- TypeNode mkSortConstructor(const std::string& name,
- size_t arity,
- uint32_t flags = SORT_FLAG_NONE);
+ TypeNode mkSortConstructor(const std::string& name, size_t arity);
+
+ /** Make an unresolved datatype sort */
+ TypeNode mkUnresolvedDatatypeSort(const std::string& name, size_t arity = 0);
private:
+ /**
+ * Make a set of types representing the given datatypes, which may
+ * be mutually recursive. unresolvedTypes is a set of SortTypes
+ * that were used as placeholders in the Datatypes for the Datatypes
+ * of the same name. This is just a more complicated version of the
+ * above mkMutualDatatypeTypes() function, but is required to handle
+ * complex types.
+ *
+ * For example, unresolvedTypes might contain the single sort "list"
+ * (with that name reported from SortType::getName()). The
+ * datatypes list might have the single datatype
+ *
+ * DATATYPE
+ * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
+ * END;
+ *
+ * To represent the Type of the array, the user had to create a
+ * placeholder type (an uninterpreted sort) to stand for "list" in
+ * the type of "car". It is this placeholder sort that should be
+ * passed in unresolvedTypes. If the datatype was of the simpler
+ * form:
+ *
+ * DATATYPE
+ * list = cons(car:list, cdr:list) | nil;
+ * END;
+ *
+ * then no complicated Type needs to be created, and the above,
+ * simpler form of mkMutualDatatypeTypes() is enough.
+ */
+ std::vector<TypeNode> mkMutualDatatypeTypesInternal(
+ const std::vector<DType>& datatypes,
+ const std::set<TypeNode>& unresolvedTypes,
+ uint32_t flags = DATATYPE_FLAG_NONE);
+
typedef std::unordered_set<expr::NodeValue*,
expr::NodeValuePoolHashFunction,
expr::NodeValuePoolEq>
return getAttribute(expr::SortArityAttr());
}
+bool TypeNode::isUnresolvedDatatype() const
+{
+ return getAttribute(expr::UnresolvedDatatypeAttr());
+}
+
std::string TypeNode::getName() const
{
Assert(isUninterpretedSort() || isUninterpretedSortConstructor());
/** Get sort constructor arity. */
uint64_t getUninterpretedSortConstructorArity() const;
+ /** Is this an unresolved datatype? */
+ bool isUnresolvedDatatype() const;
+
/**
* Get name, for uninterpreted sorts and uninterpreted sort constructors.
*/
cvc5::Sort Parser::mkUnresolvedType(const std::string& name)
{
- cvc5::Sort unresolved = d_solver->mkUninterpretedSort(name);
+ cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name);
defineType(name, unresolved);
- d_unresolved.insert(unresolved);
return unresolved;
}
cvc5::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
size_t arity)
{
- cvc5::Sort unresolved =
- d_solver->mkUninterpretedSortConstructorSort(arity, name);
+ cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name, arity);
defineType(name, vector<cvc5::Sort>(arity), unresolved);
- d_unresolved.insert(unresolved);
return unresolved;
}
Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
cvc5::Sort unresolved =
- d_solver->mkUninterpretedSortConstructorSort(params.size(), name);
+ d_solver->mkUnresolvedSort(name, params.size());
defineType(name, params, unresolved);
cvc5::Sort t = getSort(name, params);
- d_unresolved.insert(unresolved);
return unresolved;
}
return mkUnresolvedTypeConstructor(name, arity);
}
-bool Parser::isUnresolvedType(const std::string& name) {
- if (!isDeclared(name, SYM_SORT)) {
- return false;
- }
- return d_unresolved.find(getSort(name)) != d_unresolved.end();
-}
-
std::vector<cvc5::Sort> Parser::bindMutualDatatypeTypes(
std::vector<cvc5::DatatypeDecl>& datatypes, bool doOverload)
{
try {
- std::vector<cvc5::Sort> types =
- d_solver->mkDatatypeSorts(datatypes, d_unresolved);
+ std::vector<cvc5::Sort> types = d_solver->mkDatatypeSorts(datatypes);
Assert(datatypes.size() == types.size());
}
}
- // These are no longer used, and the ExprManager would have
- // complained of a bad substitution if anything is left unresolved.
- // Clear out the set.
- d_unresolved.clear();
-
// throw exception if any datatype is not well-founded
for (unsigned i = 0; i < datatypes.size(); ++i) {
const cvc5::Datatype& dt = types[i].getDatatype();
/** The set of attributes already warned about. */
std::set<std::string> d_attributesWarnedAbout;
- /**
- * The current set of unresolved types. We can get by with this NOT
- * being on the scope, because we can only have one DATATYPE
- * definition going on at one time. This is a bit hackish; we
- * depend on mkMutualDatatypeTypes() to check everything and clear
- * this out.
- */
- std::set<cvc5::Sort> d_unresolved;
-
/**
* "Preemption commands": extra commands implied by subterms that
* should be issued before the currently-being-parsed command is
/** Get the associated input. */
Input* getInput() const { return d_input.get(); }
- /** Get unresolved sorts */
- inline std::set<cvc5::Sort>& getUnresolvedSorts() { return d_unresolved; }
-
/** Deletes and replaces the current parser input. */
void setInput(Input* input) {
d_input.reset(input);
*/
cvc5::Sort mkUnresolvedType(const std::string& name, size_t arity);
- /**
- * Returns true IFF name is an unresolved type.
- */
- bool isUnresolvedType(const std::string& name);
-
/**
* Creates and binds sorts of a list of mutually-recursive datatype
* declarations.
Trace("srs-input") << "Construct unresolved types..." << std::endl;
// each canonical subterm corresponds to a grammar type
- std::set<TypeNode> unres;
std::vector<SygusDatatype> sdts;
// make unresolved types for each canonical term
std::map<Node, TypeNode> cterm_to_utype;
std::stringstream ss;
ss << "T" << i;
std::string tname = ss.str();
- TypeNode tnu = nm->mkSort(tname, NodeManager::SORT_FLAG_PLACEHOLDER);
+ TypeNode tnu = nm->mkUnresolvedDatatypeSort(tname);
cterm_to_utype[ct] = tnu;
- unres.insert(tnu);
sdts.push_back(SygusDatatype(tname));
}
Trace("srs-input") << "...finished." << std::endl;
datatypes.push_back(sdts[i].getDatatype());
}
std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(
- datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Trace("srs-input") << "...finished." << std::endl;
- Assert(types.size() == unres.size());
+ Assert(types.size() == datatypes.size());
std::map<Node, TypeNode> subtermTypes;
for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
{
// must convert all constructors to version with variables in "vars"
std::vector<SygusDatatype> sdts;
- std::set<TypeNode> unres;
Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;
dtToProcess.push_back(sdt);
std::stringstream ssutn0;
ssutn0 << sdtd.getName() << "_s";
- TypeNode abdTNew =
- nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
- unres.insert(abdTNew);
+ TypeNode abdTNew = nm->mkUnresolvedDatatypeSort(ssutn0.str());
dtProcessed[sdt] = abdTNew;
// We must convert all symbols in the sygus datatype type sdt to
{
std::stringstream ssutn;
ssutn << argt.getDType().getName() << "_s";
- argtNew =
- nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
+ argtNew = nm->mkUnresolvedDatatypeSort(ssutn.str());
Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew
<< " for " << argt << std::endl;
- unres.insert(argtNew);
dtProcessed[argt] = argtNew;
dtNextToProcess.push_back(argt);
}
}
// make the datatype types
std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
- datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
TypeNode sdtS = datatypeTypes[0];
if (TraceIsOn("dtsygus-gen-debug"))
{
Node bvl;
std::string veName("_virtual_enum_grammar");
SygusDatatype sdt(veName);
- TypeNode u = nm->mkSort(veName, NodeManager::SORT_FLAG_PLACEHOLDER);
- std::set<TypeNode> unresolvedTypes;
- unresolvedTypes.insert(u);
+ TypeNode u = nm->mkUnresolvedDatatypeSort(veName);
std::vector<TypeNode> cargsEmpty;
Node cr = nm->mkConstInt(Rational(1));
sdt.addConstructor(cr, "1", cargsEmpty);
std::vector<DType> datatypes;
datatypes.push_back(sdt.getDatatype());
std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
- datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]);
d_tds->registerEnumerator(
d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
std::set<TypeNode>& unres)
{
- TypeNode unresolved = NodeManager::currentNM()->mkSort(
- name, NodeManager::SORT_FLAG_PLACEHOLDER);
+ TypeNode unresolved =
+ NodeManager::currentNM()->mkUnresolvedDatatypeSort(name);
unres.insert(unresolved);
return unresolved;
}
Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
Assert(!datatypes.empty());
std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
- datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Trace("sygus-grammar-def") << "...finished" << std::endl;
Assert(types.size() == datatypes.size());
return types[0];
}
std::vector<TypeNode> types =
NodeManager::currentNM()->mkMutualDatatypeTypes(
- datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Assert(types.size() == 1);
return types[0];
}
{
ss << "_" << std::to_string(op_pos[i]);
}
- d_unres_tn = NodeManager::currentNM()->mkSort(
- ss.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
+ d_unres_tn = NodeManager::currentNM()->mkUnresolvedDatatypeSort(ss.str());
Trace("sygus-grammar-normalize-trie")
<< "\tCreating type " << d_unres_tn << "\n";
unres_tn = d_unres_tn;
}
Assert(d_dt_all.size() == d_unres_t_all.size());
std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
- d_dt_all, d_unres_t_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ d_dt_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
Assert(types.size() == d_dt_all.size());
/* Clear accumulators */
d_dt_all.clear();
TEST_F(TestNodeBlackTypeCardinality, undefined_sorts)
{
- TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE);
+ TypeNode foo = d_nodeManager->mkSort("foo");
// We've currently assigned them a specific Beth number, which
// isn't really correct, but...
ASSERT_FALSE(foo.getCardinality().isFinite());
* list = cons(car: tree, cdr: list) | nil
* END;
*/
- std::set<TypeNode> unresolvedTypes;
- TypeNode unresList =
- d_nodeManager->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
- unresolvedTypes.insert(unresList);
- TypeNode unresTree =
- d_nodeManager->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
- unresolvedTypes.insert(unresTree);
+ TypeNode unresList = d_nodeManager->mkSort("list");
+ TypeNode unresTree = d_nodeManager->mkSort("tree");
DType tree("tree");
std::shared_ptr<DTypeConstructor> node =
std::vector<DType> dts;
dts.push_back(tree);
dts.push_back(list);
- std::vector<TypeNode> dtts =
- d_nodeManager->mkMutualDatatypeTypes(dts, unresolvedTypes);
+ std::vector<TypeNode> dtts = d_nodeManager->mkMutualDatatypeTypes(dts);
ASSERT_TRUE(dtts[0].getDType().isResolved());
ASSERT_TRUE(dtts[1].getDType().isResolved());
TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
{
- std::set<TypeNode> unresolvedTypes;
- TypeNode unresList =
- d_nodeManager->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
- unresolvedTypes.insert(unresList);
- TypeNode unresTree =
- d_nodeManager->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
- unresolvedTypes.insert(unresTree);
+ TypeNode unresList = d_nodeManager->mkSort("list");
+ TypeNode unresTree = d_nodeManager->mkSort("tree");
DType tree("tree");
std::shared_ptr<DTypeConstructor> node =
dts.push_back(tree);
dts.push_back(list);
// remake the types
- std::vector<TypeNode> dtts2 =
- d_nodeManager->mkMutualDatatypeTypes(dts, unresolvedTypes);
+ std::vector<TypeNode> dtts2 = d_nodeManager->mkMutualDatatypeTypes(dts);
ASSERT_FALSE(dtts2[0].getDType().isFinite());
ASSERT_TRUE(
projects / cvc5.git / commitdiff