This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes.
API Changes:
(1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors.
(2) adds to unit test examples that use this variant instead of using unresolved sorts.
(3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental.
Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet.
Followup PR will add to documentation on elaborate further on how to use the datatypes API.
CVC5_API_TRY_CATCH_END;
}
+void DatatypeConstructorDecl::addSelectorUnresolved(
+ const std::string& name, const std::string& unresDataypeName)
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ // make the unresolved sort with the given name
+ internal::TypeNode usort =
+ d_solver->getNodeManager()->mkUnresolvedDatatypeSort(unresDataypeName);
+ d_ctor->addArg(name, usort);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
bool DatatypeConstructorDecl::isNull() const
{
CVC5_API_TRY_CATCH_BEGIN;
}
std::vector<internal::DType> datatypes;
- std::set<internal::TypeNode> unresTypes;
datatypes.reserve(d_ntSyms.size());
<< " produced an empty rule list";
datatypes.push_back(*dtDecl.d_dtype);
- unresTypes.insert(*ntsToUnres[ntSym].d_type);
}
std::vector<internal::TypeNode> datatypeTypes =
return Term(this, res);
}
-std::vector<Sort> Solver::mkDatatypeSortsInternal(
- const std::vector<DatatypeDecl>& dtypedecls,
- const std::set<Sort>& unresolvedSorts) const
-{
- // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
- // double checks
- //////// all checks before this line
-
- std::vector<internal::DType> datatypes;
- for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
- {
- datatypes.push_back(dtypedecls[i].getDatatype());
- }
-
- std::vector<internal::TypeNode> dtypes =
- getNodeManager()->mkMutualDatatypeTypes(datatypes);
- std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes);
- return retTypes;
-}
-
Term Solver::synthFunHelper(const std::string& symbol,
const std::vector<Term>& boundVars,
const Sort& sort,
CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls);
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- return mkDatatypeSortsInternal(dtypedecls, {});
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-std::vector<Sort> Solver::mkDatatypeSorts(
- const std::vector<DatatypeDecl>& dtypedecls,
- const std::set<Sort>& unresolvedSorts) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls);
- CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts);
- //////// all checks before this line
- return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
+ std::vector<internal::DType> datatypes;
+ for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
+ {
+ datatypes.push_back(dtypedecls[i].getDatatype());
+ }
+ std::vector<internal::TypeNode> dtypes =
+ getNodeManager()->mkMutualDatatypeTypes(datatypes);
+ std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes);
+ return retTypes;
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
-
internal::TypeNode tn =
symbol ? getNodeManager()->mkSort(*symbol) : getNodeManager()->mkSort();
return Sort(this, tn);
CVC5_API_TRY_CATCH_END;
}
-Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const
+Sort Solver::mkUnresolvedDatatypeSort(const std::string& symbol,
+ size_t arity) const
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
*/
void addSelectorSelf(const std::string& name);
+ /**
+ * Add datatype selector declaration whose codomain sort is an unresolved
+ * datatype with the given name.
+ * @param name the name of the datatype selector declaration to add
+ * @param unresDataypeName the name of the unresolved datatype. The codomain
+ * of the selector will be the resolved datatype with
+ * the given name.
+ */
+ void addSelectorUnresolved(const std::string& name,
+ const std::string& unresDataypeName);
+
/**
* @return true if this DatatypeConstructorDecl is a null declaration.
*/
* with bound variables via purifySygusGTerm, and binding these variables
* via a lambda.
*
- * @note Create unresolved sorts with Solver::mkUnresolvedSort().
- *
* @param dt the non-terminal's datatype to which a constructor is added
* @param term the sygus operator of the constructor
* @param ntsToUnres mapping from non-terminals to their unresolved sorts
std::vector<Sort> mkDatatypeSorts(
const std::vector<DatatypeDecl>& dtypedecls) const;
- /**
- * Create a vector of datatype sorts using unresolved sorts. The names of
- * the datatype declarations in dtypedecls must be distinct.
- *
- * This method is called when the DatatypeDecl objects dtypedecls have been
- * built using "unresolved" sorts.
- *
- * We associate each sort in unresolvedSorts with exactly one datatype from
- * dtypedecls. In particular, it must have the same name as exactly one
- * datatype declaration in dtypedecls.
- *
- * When constructing datatypes, unresolved sorts are replaced by the datatype
- * sort constructed for the datatype declaration it is associated with.
- *
- * @note Create unresolved sorts with Solver::mkUnresolvedSort().
- *
- * @param dtypedecls the datatype declarations from which the sort is created
- * @param unresolvedSorts the list of unresolved sorts
- * @return the datatype sorts
- */
- std::vector<Sort> mkDatatypeSorts(
- const std::vector<DatatypeDecl>& dtypedecls,
- const std::set<Sort>& unresolvedSorts) const;
-
/**
* Create function sort.
* @param sorts the sort of the function arguments
const std::optional<std::string>& symbol = std::nullopt) const;
/**
- * Create an unresolved sort.
+ * Create an unresolved datatype sort.
*
* This is for creating yet unresolved sort placeholders for mutually
- * recursive datatypes.
+ * recursive parametric datatypes.
*
* @param symbol the symbol of the sort
* @param arity the number of sort parameters of the sort
* @return the unresolved sort
+ *
+ * @warning This method is experimental and may change in future versions.
*/
- Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const;
+ Sort mkUnresolvedDatatypeSort(const std::string& symbol,
+ size_t arity = 0) const;
/**
* Create an uninterpreted sort constructor sort.
*/
Term mkTermHelper(const Op& op, const std::vector<Term>& children) const;
- /**
- * Create a vector of datatype sorts, using unresolved sorts.
- * @param dtypedecls the datatype declarations from which the sort is created
- * @param unresolvedSorts the list of unresolved sorts
- * @return the datatype sorts
- */
- std::vector<Sort> mkDatatypeSortsInternal(
- const std::vector<DatatypeDecl>& dtypedecls,
- const std::set<Sort>& unresolvedSorts) const;
-
/**
* Synthesize n-ary function following specified syntactic constraints.
*
private native void addSelectorSelf(long pointer, String name);
+ /**
+ * Add datatype selector declaration whose codomain sort is an unresolved
+ * datatype with the given name.
+ * @param name the name of the datatype selector declaration to add
+ * @param unresDataypeName the name of the unresolved datatype. The codomain
+ * of the selector will be the resolved datatype with
+ * the given name.
+ */
+ public void addSelectorUnresolved(String name, String unresDataypeName)
+ {
+ addSelectorUnresolved(pointer, name, unresDataypeName);
+ }
+
+ private native void addSelectorUnresolved(long pointer, String name, String unresDataypeName);
+
/**
* @return true if this DatatypeConstructorDecl is a null declaration.
*/
private native long[] mkDatatypeSorts(long pointer, long[] declPointers) throws CVC5ApiException;
- /**
- * Create a vector of datatype sorts using unresolved sorts. The names of
- * the datatype declarations in dtypedecls must be distinct.
- *
- * This method is called when the DatatypeDecl objects dtypedecls have
- * been built using "unresolved" sorts.
- *
- * We associate each sort in unresolvedSorts with exacly one datatype from
- * dtypedecls. In particular, it must have the same name as exactly one
- * datatype declaration in dtypedecls.
- *
- * When constructing datatypes, unresolved sorts are replaced by the
- * datatype sort constructed for the datatype declaration it is associated
- * with.
- *
- * @api.note Create unresolved sorts with Solver::mkUnresolvedSort().
- *
- * @param dtypedecls the datatype declarations from which the sort is
- * created
- * @param unresolvedSorts the set of unresolved sorts
- * @return the datatype sorts
- * @throws CVC5ApiException
- */
- public List<Sort> mkDatatypeSorts(List<DatatypeDecl> dtypedecls, Set<Sort> unresolvedSorts)
- throws CVC5ApiException
- {
- Sort[] array = mkDatatypeSorts(
- dtypedecls.toArray(new DatatypeDecl[0]), unresolvedSorts.toArray(new Sort[0]));
- return Arrays.asList(array);
- }
-
- /**
- * Create a vector of datatype sorts using unresolved sorts. The names of
- * the datatype declarations in dtypedecls must be distinct.
- *
- * This method is called when the DatatypeDecl objects dtypedecls have
- * been built using "unresolved" sorts.
- *
- * We associate each sort in unresolvedSorts with exacly one datatype from
- * dtypedecls. In particular, it must have the same name as exactly one
- * datatype declaration in dtypedecls.
- *
- * When constructing datatypes, unresolved sorts are replaced by the
- * datatype sort constructed for the datatype declaration it is associated
- * with.
- *
- * @param dtypedecls the datatype declarations from which the sort is
- * created
- * @param unresolvedSorts the list of unresolved sorts
- * @return the datatype sorts
- */
- public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls, Sort[] unresolvedSorts)
- throws CVC5ApiException
- {
- long[] declPointers = Utils.getPointers(dtypedecls);
- long[] unresolvedPointers = Utils.getPointers(unresolvedSorts);
- long[] sortPointers = mkDatatypeSorts(pointer, declPointers, unresolvedPointers);
- Sort[] sorts = Utils.getSorts(this, sortPointers);
- return sorts;
- }
-
- private native long[] mkDatatypeSorts(
- long pointer, long[] declPointers, long[] unresolvedPointers) throws CVC5ApiException;
-
/**
* Create function sort.
* @param domain the sort of the fuction argument
private native long mkUninterpretedSort(long pointer);
/**
- * Create an unresolved sort.
+ * Create an unresolved datatype sort.
*
* This is for creating yet unresolved sort placeholders for mutually
- * recursive datatypes.
+ * recursive parametric datatypes.
*
* @param symbol the symbol of the sort
* @param arity the number of sort parameters of the sort
* @return the unresolved sort
* @throws CVC5ApiException
*/
- public Sort mkUnresolvedSort(String symbol, int arity) throws CVC5ApiException
+ public Sort mkUnresolvedDatatypeSort(String symbol, int arity) throws CVC5ApiException
{
Utils.validateUnsigned(arity, "arity");
- long sortPointer = mkUnresolvedSort(pointer, symbol, arity);
+ long sortPointer = mkUnresolvedDatatypeSort(pointer, symbol, arity);
return new Sort(this, sortPointer);
}
- private native long mkUnresolvedSort(long pointer, String symbol, int arity);
+ private native long mkUnresolvedDatatypeSort(long pointer, String symbol, int arity);
/**
- * Create an unresolved sort.
+ * Create an unresolved datatype sort.
*
* This is for creating yet unresolved sort placeholders for mutually
* recursive datatypes without sort parameters.
* @return the unresolved sort
* @throws CVC5ApiException
*/
- public Sort mkUnresolvedSort(String symbol) throws CVC5ApiException
+ public Sort mkUnresolvedDatatypeSort(String symbol) throws CVC5ApiException
{
- return mkUnresolvedSort(symbol, 0);
+ return mkUnresolvedDatatypeSort(symbol, 0);
}
/**
CVC5_JAVA_API_TRY_CATCH_BEGIN;
DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
const char* s = env->GetStringUTFChars(jName, nullptr);
- std::string cName(s);
- current->addSelectorSelf(cName);
+ std::string sName(s);
+ current->addSelectorSelf(sName);
+ env->ReleaseStringUTFChars(jName, s);
+ CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class: io_github_cvc5_DatatypeConstructorDecl
+ * Method: addSelectorUnresolved
+ * Signature: (JLjava/lang/String;Ljava/lang/String;)V
+ */
+JNIEXPORT void JNICALL
+Java_io_github_cvc5_DatatypeConstructorDecl_addSelectorUnresolved(
+ JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jstring jName,
+ jstring jUnresDataypeName)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
+ const char* s = env->GetStringUTFChars(jName, nullptr);
+ std::string sName(s);
+ const char* du = env->GetStringUTFChars(jUnresDataypeName, nullptr);
+ std::string duName(du);
+ current->addSelectorUnresolved(sName, duName);
+ env->ReleaseStringUTFChars(jUnresDataypeName, du);
env->ReleaseStringUTFChars(jName, s);
CVC5_JAVA_API_TRY_CATCH_END(env);
}
* Signature: (J[J)[J
*/
JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J(JNIEnv* env,
+Java_io_github_cvc5_Solver_mkDatatypeSorts(JNIEnv* env,
jobject,
jlong pointer,
jlongArray jDecls)
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
}
-/*
- * Class: io_github_cvc5_Solver
- * Method: mkDatatypeSorts
- * Signature: (J[J[J)[J
- */
-JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env,
- jobject,
- jlong pointer,
- jlongArray jDecls,
- jlongArray jUnresolved)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- std::vector<DatatypeDecl> decls =
- getObjectsFromPointers<DatatypeDecl>(env, jDecls);
- std::vector<Sort> cUnresolved =
- getObjectsFromPointers<Sort>(env, jUnresolved);
- std::set<Sort> unresolved(cUnresolved.begin(), cUnresolved.end());
- std::vector<Sort> sorts = solver->mkDatatypeSorts(decls, unresolved);
- jlongArray ret = getPointersFromObjects<Sort>(env, sorts);
- return ret;
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
/*
* Class: io_github_cvc5_Solver
* Method: mkFunctionSort
/*
* Class: io_github_cvc5_Solver
- * Method: mkUnresolvedSort
+ * Method: mkUnresolvedDatatypeSort
* Signature: (JLjava/lang/String;I)J
*/
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedSort(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedDatatypeSort(
JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Solver* solver = reinterpret_cast<Solver*>(pointer);
const char* s = env->GetStringUTFChars(jSymbol, nullptr);
std::string cSymbol(s);
- Sort* retPointer = new Sort(solver->mkUnresolvedSort(cSymbol, (size_t)arity));
+ Sort* retPointer =
+ new Sort(solver->mkUnresolvedDatatypeSort(cSymbol, (size_t)arity));
env->ReleaseStringUTFChars(jSymbol, s);
return reinterpret_cast<jlong>(retPointer);
cdef cppclass DatatypeConstructorDecl:
void addSelector(const string& name, Sort sort) except +
void addSelectorSelf(const string& name) except +
+ void addSelectorUnresolved(const string& name, const string& unresDatatypeName) except +
bint isNull() except +
string toString() except +
Sort mkBitVectorSort(uint32_t size) except +
Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except +
Sort mkDatatypeSort(DatatypeDecl dtypedecl) except +
- vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls,
- const set[Sort]& unresolvedSorts) except +
+ vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls) except +
Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except +
Sort mkParamSort() except +
Sort mkParamSort(const string& symbol) except +
Sort mkSequenceSort(Sort elemSort) except +
Sort mkUninterpretedSort() except +
Sort mkUninterpretedSort(const string& symbol) except +
- Sort mkUnresolvedSort(const string& symbol, size_t arity) except +
+ Sort mkUnresolvedDatatypeSort(const string& symbol, size_t arity) except +
Sort mkUninterpretedSortConstructorSort(size_t arity) except +
Sort mkUninterpretedSortConstructorSort(size_t arity, const string& symbol) except +
Sort mkTupleSort(const vector[Sort]& sorts) except +
"""
self.cddc.addSelectorSelf(name.encode())
+ def addSelectorUnresolved(self, str name, str unresDatatypeName):
+ """
+ Add datatype selector declaration whose codomain sort is an
+ unresolved datatype with the given name.
+
+ :param name: The name of the datatype selector declaration to add.
+ :param unresDataypeName: The name of the unresolved datatype. The
+ codomain of the selector will be the
+ resolved datatype with the given name.
+ """
+ self.cddc.addSelectorUnresolved(name.encode(), unresDatatypeName.encode())
+
def isNull(self):
"""
:return: True if this DatatypeConstructorDecl is a null object.
sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
return sort
- def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
+ def mkDatatypeSorts(self, list dtypedecls):
"""
Create a vector of datatype sorts using unresolved sorts. The names
of the datatype declarations in dtypedecls must be distinct.
- This method is called when the DatatypeDecl objects dtypedecls have
- been built using "unresolved" sorts.
-
- We associate each sort in unresolvedSorts with exacly one datatype
- from dtypedecls. In particular, it must have the same name as
- exactly one datatype declaration in dtypedecls.
-
When constructing datatypes, unresolved sorts are replaced by the
datatype sort constructed for the datatype declaration it is
associated with.
:param dtypedecls: The datatype declarations from which the sort is
created.
- :param unresolvedSorts: The list of unresolved sorts.
:return: The datatype sorts.
"""
- if unresolvedSorts == None:
- unresolvedSorts = set([])
- else:
- assert isinstance(unresolvedSorts, set)
-
sorts = []
cdef vector[c_DatatypeDecl] decls
for decl in dtypedecls:
decls.push_back((<DatatypeDecl?> decl).cdd)
- cdef c_set[c_Sort] usorts
- for usort in unresolvedSorts:
- usorts.insert((<Sort?> usort).csort)
-
csorts = self.csolver.mkDatatypeSorts(
- <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
+ <const vector[c_DatatypeDecl]&> decls)
for csort in csorts:
sort = Sort(self)
sort.csort = csort
sort.csort = self.csolver.mkUninterpretedSort(name.encode())
return sort
- def mkUnresolvedSort(self, str name, size_t arity = 0):
+ def mkUnresolvedDatatypeSort(self, str name, size_t arity = 0):
"""
- Create an unresolved sort.
+ Create an unresolved datatype sort.
This is for creating yet unresolved sort placeholders for mutually
recursive datatypes.
:return: The unresolved sort.
"""
cdef Sort sort = Sort(self)
- sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
+ sort.csort = self.csolver.mkUnresolvedDatatypeSort(name.encode(), arity)
return sort
def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None):
cvc5::Sort Parser::mkUnresolvedType(const std::string& name)
{
- cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name);
+ cvc5::Sort unresolved = d_solver->mkUnresolvedDatatypeSort(name);
defineType(name, unresolved);
return unresolved;
}
cvc5::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
size_t arity)
{
- cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name, arity);
+ cvc5::Sort unresolved = d_solver->mkUnresolvedDatatypeSort(name, arity);
defineType(name, vector<cvc5::Sort>(arity), unresolved);
return unresolved;
}
Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
cvc5::Sort unresolved =
- d_solver->mkUnresolvedSort(name, params.size());
+ d_solver->mkUnresolvedDatatypeSort(name, params.size());
defineType(name, params, unresolved);
cvc5::Sort t = getSort(name, params);
return unresolved;
* END;
*/
// Make unresolved types as placeholders
- std::set<Sort> unresTypes;
- Sort unresTree = d_solver.mkUnresolvedSort("tree");
- Sort unresList = d_solver.mkUnresolvedSort("list");
- unresTypes.insert(unresTree);
- unresTypes.insert(unresList);
+ Sort unresTree = d_solver.mkUnresolvedDatatypeSort("tree");
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("list");
DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
dtdecls.push_back(tree);
dtdecls.push_back(list);
std::vector<Sort> dtsorts;
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), dtdecls.size());
for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
{
ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC5ApiException);
}
+TEST_F(TestApiBlackDatatype, mkDatatypeSortsSelUnres)
+{
+ // Same as above, without unresolved sorts
+
+ DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
+ DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
+ node.addSelectorUnresolved("left", "tree");
+ node.addSelectorUnresolved("right", "tree");
+ tree.addConstructor(node);
+
+ DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
+ leaf.addSelectorUnresolved("data", "list");
+ tree.addConstructor(leaf);
+
+ DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ cons.addSelectorUnresolved("car", "tree");
+ cons.addSelectorUnresolved("cdr", "tree");
+ list.addConstructor(cons);
+
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+ list.addConstructor(nil);
+
+ std::vector<DatatypeDecl> dtdecls;
+ dtdecls.push_back(tree);
+ dtdecls.push_back(list);
+ std::vector<Sort> dtsorts;
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
+ ASSERT_EQ(dtsorts.size(), dtdecls.size());
+ for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+ {
+ ASSERT_TRUE(dtsorts[i].isDatatype());
+ ASSERT_FALSE(dtsorts[i].getDatatype().isFinite());
+ ASSERT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
+ }
+ // verify the resolution was correct
+ Datatype dtTree = dtsorts[0].getDatatype();
+ DatatypeConstructor dtcTreeNode = dtTree[0];
+ ASSERT_EQ(dtcTreeNode.getName(), "node");
+ DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
+ ASSERT_EQ(dtsTreeNodeLeft.getName(), "left");
+ // argument type should have resolved to be recursive
+ ASSERT_TRUE(dtsTreeNodeLeft.getCodomainSort().isDatatype());
+ ASSERT_EQ(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]);
+}
+
TEST_F(TestApiBlackDatatype, datatypeStructs)
{
Sort intSort = d_solver.getIntegerSort();
* END;
*/
// Make unresolved types as placeholders
- std::set<Sort> unresTypes;
- Sort unresWList = d_solver.mkUnresolvedSort("wlist");
- Sort unresList = d_solver.mkUnresolvedSort("list");
- Sort unresNs = d_solver.mkUnresolvedSort("ns");
- unresTypes.insert(unresWList);
- unresTypes.insert(unresList);
- unresTypes.insert(unresNs);
+ Sort unresWList = d_solver.mkUnresolvedDatatypeSort("wlist");
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("list");
+ Sort unresNs = d_solver.mkUnresolvedDatatypeSort("ns");
DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist");
DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
dtdecls.push_back(ns);
// this is well-founded and has no nested recursion
std::vector<Sort> dtsorts;
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 3);
ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
* ns2 = elem2(ndata: array(int,ns2)) | nil2
* END;
*/
- unresTypes.clear();
- Sort unresNs2 = d_solver.mkUnresolvedSort("ns2");
- unresTypes.insert(unresNs2);
+ Sort unresNs2 = d_solver.mkUnresolvedDatatypeSort("ns2");
DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2");
DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2");
dtsorts.clear();
// this is not well-founded due to non-simple recursion
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 1);
ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray());
ASSERT_EQ(
* ns3 = elem3(ndata: set(list3))
* END;
*/
- unresTypes.clear();
- Sort unresNs3 = d_solver.mkUnresolvedSort("ns3");
- unresTypes.insert(unresNs3);
- Sort unresList3 = d_solver.mkUnresolvedSort("list3");
- unresTypes.insert(unresList3);
+ Sort unresNs3 = d_solver.mkUnresolvedDatatypeSort("ns3");
+ Sort unresList3 = d_solver.mkUnresolvedDatatypeSort("list3");
DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3");
DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3");
dtsorts.clear();
// both are well-founded and have nested recursion
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 2);
ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
* ns4 = elem(ndata: list4)
* END;
*/
- unresTypes.clear();
- Sort unresNs4 = d_solver.mkUnresolvedSort("ns4");
- unresTypes.insert(unresNs4);
- Sort unresList4 = d_solver.mkUnresolvedSort("list4");
- unresTypes.insert(unresList4);
+ Sort unresNs4 = d_solver.mkUnresolvedDatatypeSort("ns4");
+ Sort unresList4 = d_solver.mkUnresolvedDatatypeSort("list4");
DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4");
DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4");
dtsorts.clear();
// both are well-founded and have nested recursion
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 2);
ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
* list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
* END;
*/
- unresTypes.clear();
Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort(1, "list5");
- unresTypes.insert(unresList5);
std::vector<Sort> v;
Sort x = d_solver.mkParamSort("X");
dtdecls.push_back(list5);
// well-founded and has nested recursion
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 1);
ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
}
* END;
*/
// Make unresolved types as placeholders
- std::set<Sort> unresTypes;
Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist");
- unresTypes.insert(unresList);
std::vector<Sort> v;
Sort x = d_solver.mkParamSort("X");
std::vector<Sort> dtsorts;
// make the datatype sorts
- ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+ ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls));
ASSERT_EQ(dtsorts.size(), 1);
Datatype d = dtsorts[0].getDatatype();
DatatypeConstructor nilc = d[0];
ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException);
/* with unresolved sorts */
- Sort unresList = d_solver.mkUnresolvedSort("ulist");
- std::set<Sort> unresSorts = {unresList};
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("ulist");
DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
ucons.addSelector("car", unresList);
DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
ulist.addConstructor(unil);
std::vector<DatatypeDecl> udecls = {ulist};
- ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts));
+ ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls));
- ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC5ApiException);
+ ASSERT_THROW(slv.mkDatatypeSorts(udecls), CVC5ApiException);
/* mutually recursive with unresolved parameterized sorts */
Sort p0 = d_solver.mkParamSort("p0");
Sort p1 = d_solver.mkParamSort("p1");
- Sort u0 = d_solver.mkUnresolvedSort("dt0", 1);
- Sort u1 = d_solver.mkUnresolvedSort("dt1", 1);
+ Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1);
+ Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1);
DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0);
DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1);
DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0");
ctordecl1.addSelector("s1", u0.instantiate({p1}));
dtdecl0.addConstructor(ctordecl0);
dtdecl1.addConstructor(ctordecl1);
- std::vector<Sort> dt_sorts =
- d_solver.mkDatatypeSorts({dtdecl0, dtdecl1}, {u0, u1});
+ std::vector<Sort> dt_sorts = d_solver.mkDatatypeSorts({dtdecl0, dtdecl1});
Sort isort1 = dt_sorts[1].instantiate({d_solver.getBooleanSort()});
Term t1 = d_solver.mkConst(isort1, "t");
Term t0 = d_solver.mkTerm(
ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
}
-TEST_F(TestApiBlackSolver, mkUnresolvedSort)
+TEST_F(TestApiBlackSolver, mkUnresolvedDatatypeSort)
{
- ASSERT_NO_THROW(d_solver.mkUnresolvedSort("u"));
- ASSERT_NO_THROW(d_solver.mkUnresolvedSort("u", 1));
- ASSERT_NO_THROW(d_solver.mkUnresolvedSort(""));
- ASSERT_NO_THROW(d_solver.mkUnresolvedSort("", 1));
+ ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u"));
+ ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u", 1));
+ ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort(""));
+ ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("", 1));
}
TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort)
* END;
*/
// Make unresolved types as placeholders
- Set<Sort> unresTypes = new HashSet<>();
- Sort unresTree = d_solver.mkUnresolvedSort("tree", 0);
- Sort unresList = d_solver.mkUnresolvedSort("list", 0);
- unresTypes.add(unresTree);
- unresTypes.add(unresList);
+ Sort unresTree = d_solver.mkUnresolvedDatatypeSort("tree", 0);
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("list", 0);
DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
dtdecls.add(tree);
dtdecls.add(list);
- AtomicReference<List<Sort>> atomic = new AtomicReference<>();
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
- List<Sort> dtsorts = atomic.get();
- assertEquals(dtsorts.size(), dtdecls.size());
+ AtomicReference<Sort[]> atomic = new AtomicReference<>();
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+ Sort[] dtsorts = atomic.get();
+ assertEquals(dtsorts.length, dtdecls.size());
for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
{
- assertTrue(dtsorts.get(i).isDatatype());
- assertFalse(dtsorts.get(i).getDatatype().isFinite());
- assertEquals(dtsorts.get(i).getDatatype().getName(), dtdecls.get(i).getName());
+ assertTrue(dtsorts[i].isDatatype());
+ assertFalse(dtsorts[i].getDatatype().isFinite());
+ assertEquals(dtsorts[i].getDatatype().getName(), dtdecls.get(i).getName());
}
// verify the resolution was correct
- Datatype dtTree = dtsorts.get(0).getDatatype();
+ Datatype dtTree = dtsorts[0].getDatatype();
DatatypeConstructor dtcTreeNode = dtTree.getConstructor(0);
assertEquals(dtcTreeNode.getName(), "node");
DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0);
assertEquals(dtsTreeNodeLeft.getName(), "left");
// argument type should have resolved to be recursive
assertTrue(dtsTreeNodeLeft.getCodomainSort().isDatatype());
- assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts.get(0));
+ assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]);
// fails due to empty datatype
List<DatatypeDecl> dtdeclsBad = new ArrayList<>();
assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(dtdeclsBad));
}
+ @Test
+ void mkDatatypeSortsSelUnres() throws CVC5ApiException
+ {
+ // Same as above, using unresolved selectors
+
+ DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
+ DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
+ node.addSelectorUnresolved("left", "tree");
+ node.addSelectorUnresolved("right", "tree");
+ tree.addConstructor(node);
+
+ DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
+ leaf.addSelectorUnresolved("data", "list");
+ tree.addConstructor(leaf);
+
+ DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ cons.addSelectorUnresolved("car", "tree");
+ cons.addSelectorUnresolved("cdr", "tree");
+ list.addConstructor(cons);
+
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+ list.addConstructor(nil);
+
+ List<DatatypeDecl> dtdecls = new ArrayList<>();
+ dtdecls.add(tree);
+ dtdecls.add(list);
+
+ AtomicReference<Sort[]> atomic = new AtomicReference<>();
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+ Sort[] dtsorts = atomic.get();
+ assertEquals(dtsorts.length, dtdecls.size());
+ for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+ {
+ assertTrue(dtsorts[i].isDatatype());
+ assertFalse(dtsorts[i].getDatatype().isFinite());
+ assertEquals(dtsorts[i].getDatatype().getName(), dtdecls.get(i).getName());
+ }
+ // verify the resolution was correct
+ Datatype dtTree = dtsorts[0].getDatatype();
+ DatatypeConstructor dtcTreeNode = dtTree.getConstructor(0);
+ assertEquals(dtcTreeNode.getName(), "node");
+ DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0);
+ assertEquals(dtsTreeNodeLeft.getName(), "left");
+ // argument type should have resolved to be recursive
+ assertTrue(dtsTreeNodeLeft.getCodomainSort().isDatatype());
+ assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]);
+ }
+
@Test
void datatypeStructs() throws CVC5ApiException
{
* END;
*/
// Make unresolved types as placeholders
- Set<Sort> unresTypes = new HashSet<>();
- Sort unresWList = d_solver.mkUnresolvedSort("wlist", 0);
- Sort unresList = d_solver.mkUnresolvedSort("list", 0);
- Sort unresNs = d_solver.mkUnresolvedSort("ns", 0);
- unresTypes.add(unresWList);
- unresTypes.add(unresList);
- unresTypes.add(unresNs);
+ Sort unresWList = d_solver.mkUnresolvedDatatypeSort("wlist", 0);
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("list", 0);
+ Sort unresNs = d_solver.mkUnresolvedDatatypeSort("ns", 0);
DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist");
DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
dtdecls.add(list);
dtdecls.add(ns);
// this is well-founded and has no nested recursion
- AtomicReference<List<Sort>> atomic = new AtomicReference<>();
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
- List<Sort> dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 3);
- assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
- assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
- assertTrue(dtsorts.get(2).getDatatype().isWellFounded());
+ AtomicReference<Sort[]> atomic = new AtomicReference<>();
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+ Sort[] dtsorts = atomic.get();
+ assertEquals(dtsorts.length, 3);
+ assertTrue(dtsorts[0].getDatatype().isWellFounded());
+ assertTrue(dtsorts[1].getDatatype().isWellFounded());
+ assertTrue(dtsorts[2].getDatatype().isWellFounded());
/* Create mutual datatypes corresponding to this definition block:
* DATATYPE
* ns2 = elem2(ndata: array(int,ns2)) | nil2
* END;
*/
- unresTypes.clear();
- Sort unresNs2 = d_solver.mkUnresolvedSort("ns2", 0);
- unresTypes.add(unresNs2);
+ Sort unresNs2 = d_solver.mkUnresolvedDatatypeSort("ns2", 0);
DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2");
DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2");
// dtsorts.clear();
// this is not well-founded due to non-simple recursion
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 1);
+ assertEquals(dtsorts.length, 1);
assertTrue(
- dtsorts.get(0).getDatatype().getConstructor(0).getSelector(0).getCodomainSort().isArray());
- assertEquals(dtsorts.get(0)
+ dtsorts[0].getDatatype().getConstructor(0).getSelector(0).getCodomainSort().isArray());
+ assertEquals(dtsorts[0]
.getDatatype()
.getConstructor(0)
.getSelector(0)
.getCodomainSort()
.getArrayElementSort(),
- dtsorts.get(0));
- assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+ dtsorts[0]);
+ assertTrue(dtsorts[0].getDatatype().isWellFounded());
/* Create mutual datatypes corresponding to this definition block:
* DATATYPE
* ns3 = elem3(ndata: set(list3))
* END;
*/
- unresTypes.clear();
- Sort unresNs3 = d_solver.mkUnresolvedSort("ns3", 0);
- unresTypes.add(unresNs3);
- Sort unresList3 = d_solver.mkUnresolvedSort("list3", 0);
- unresTypes.add(unresList3);
+ Sort unresNs3 = d_solver.mkUnresolvedDatatypeSort("ns3", 0);
+ Sort unresList3 = d_solver.mkUnresolvedDatatypeSort("list3", 0);
DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3");
DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3");
// dtsorts.clear();
// both are well-founded and have nested recursion
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 2);
- assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
- assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
+ assertEquals(dtsorts.length, 2);
+ assertTrue(dtsorts[0].getDatatype().isWellFounded());
+ assertTrue(dtsorts[1].getDatatype().isWellFounded());
/* Create mutual datatypes corresponding to this definition block:
* DATATYPE
* ns4 = elem(ndata: list4)
* END;
*/
- unresTypes.clear();
- Sort unresNs4 = d_solver.mkUnresolvedSort("ns4", 0);
- unresTypes.add(unresNs4);
- Sort unresList4 = d_solver.mkUnresolvedSort("list4", 0);
- unresTypes.add(unresList4);
+ Sort unresNs4 = d_solver.mkUnresolvedDatatypeSort("ns4", 0);
+ Sort unresList4 = d_solver.mkUnresolvedDatatypeSort("list4", 0);
DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4");
DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4");
// dtsorts.clear();
// both are well-founded and have nested recursion
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 2);
- assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
- assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
+ assertEquals(dtsorts.length, 2);
+ assertTrue(dtsorts[0].getDatatype().isWellFounded());
+ assertTrue(dtsorts[1].getDatatype().isWellFounded());
/* 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.mkUninterpretedSortConstructorSort(1, "list5");
- unresTypes.add(unresList5);
List<Sort> v = new ArrayList<>();
Sort x = d_solver.mkParamSort("X");
dtdecls.add(list5);
// well-founded and has nested recursion
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 1);
- assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+ assertEquals(dtsorts.length, 1);
+ assertTrue(dtsorts[0].getDatatype().isWellFounded());
}
@Test
* END;
*/
// Make unresolved types as placeholders
- Set<Sort> unresTypes = new HashSet<>();
Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist");
- unresTypes.add(unresList);
List<Sort> v = new ArrayList<>();
Sort x = d_solver.mkParamSort("X");
dtdecls.add(plist);
// make the datatype sorts
- AtomicReference<List<Sort>> atomic = new AtomicReference<>();
- assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
- List<Sort> dtsorts = atomic.get();
- assertEquals(dtsorts.size(), 1);
- Datatype d = dtsorts.get(0).getDatatype();
+ AtomicReference<Sort[]> atomic = new AtomicReference<>();
+ assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+ Sort[] dtsorts = atomic.get();
+ assertEquals(dtsorts.length, 1);
+ Datatype d = dtsorts[0].getDatatype();
DatatypeConstructor nilc = d.getConstructor(0);
Sort isort = d_solver.getIntegerSort();
List<Sort> iargs = new ArrayList<>();
iargs.add(isort);
- Sort listInt = dtsorts.get(0).instantiate(iargs);
+ Sort listInt = dtsorts[0].instantiate(iargs);
AtomicReference<Term> atomicTerm = new AtomicReference<>();
// get the specialized constructor term for list[Int]
assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(throwsDecls));
/* with unresolved sorts */
- Sort unresList = d_solver.mkUnresolvedSort("ulist", 1);
- Set<Sort> unresSorts = new HashSet<>();
- unresSorts.add(unresList);
+ Sort unresList = d_solver.mkUnresolvedDatatypeSort("ulist", 1);
DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
ucons.addSelector("car", unresList);
DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
ulist.addConstructor(unil);
DatatypeDecl[] udecls = new DatatypeDecl[] {ulist};
- assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+ assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls)));
- assertThrows(
- CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+ assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls)));
slv.close();
/* mutually recursive with unresolved parameterized sorts */
Sort p0 = d_solver.mkParamSort("p0");
Sort p1 = d_solver.mkParamSort("p1");
- Sort u0 = d_solver.mkUnresolvedSort("dt0", 1);
- Sort u1 = d_solver.mkUnresolvedSort("dt1", 1);
+ Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1);
+ Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1);
DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0);
DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1);
DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0");
ctordecl1.addSelector("s1", u0.instantiate(new Sort[] {p1}));
dtdecl0.addConstructor(ctordecl0);
dtdecl1.addConstructor(ctordecl1);
- Sort[] dt_sorts =
- d_solver.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1}, new Sort[] {u0, u1});
+ Sort[] dt_sorts = d_solver.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1});
Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()});
Term t1 = d_solver.mkConst(isort1, "t");
Term t0 = d_solver.mkTerm(APPLY_SELECTOR,
}
@Test
- void mkUnresolvedSort() throws CVC5ApiException
+ void mkUnresolvedDatatypeSort() throws CVC5ApiException
{
- assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u"));
- assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1));
- assertDoesNotThrow(() -> d_solver.mkUnresolvedSort(""));
- assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1));
+ assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u"));
+ assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u", 1));
+ assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort(""));
+ assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("", 1));
}
@Test
#
#Make unresolved types as placeholders
- unresTypes = set([])
- unresTree = solver.mkUnresolvedSort("tree")
- unresList = solver.mkUnresolvedSort("list")
- unresTypes.add(unresTree)
- unresTypes.add(unresList)
+ unresTree = solver.mkUnresolvedDatatypeSort("tree")
+ unresList = solver.mkUnresolvedDatatypeSort("list")
tree = solver.mkDatatypeDecl("tree")
node = solver.mkDatatypeConstructorDecl("node")
dtdecls.append(tree)
dtdecls.append(llist)
dtsorts = []
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == len(dtdecls)
for i in range(0, len(dtdecls)):
assert dtsorts[i].isDatatype()
solver.mkDatatypeSorts(dtdeclsBad)
+def test_mk_datatype_sorts_sel_unres(solver):
+ # Same as above, using unresolved selectors
+
+ tree = solver.mkDatatypeDecl("tree")
+ node = solver.mkDatatypeConstructorDecl("node")
+ node.addSelectorUnresolved("left", "tree")
+ node.addSelectorUnresolved("right", "tree")
+ tree.addConstructor(node)
+
+ leaf = solver.mkDatatypeConstructorDecl("leaf")
+ leaf.addSelectorUnresolved("data", "list")
+ tree.addConstructor(leaf)
+
+ llist = solver.mkDatatypeDecl("list")
+ cons = solver.mkDatatypeConstructorDecl("cons")
+ cons.addSelectorUnresolved("car", "tree")
+ cons.addSelectorUnresolved("cdr", "tree")
+ llist.addConstructor(cons)
+
+ nil = solver.mkDatatypeConstructorDecl("nil")
+ llist.addConstructor(nil)
+
+ dtdecls = []
+ dtdecls.append(tree)
+ dtdecls.append(llist)
+ dtsorts = []
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
+ assert len(dtsorts) == len(dtdecls)
+ for i in range(0, len(dtdecls)):
+ assert dtsorts[i].isDatatype()
+ assert not dtsorts[i].getDatatype().isFinite()
+ assert dtsorts[i].getDatatype().getName() == dtdecls[i].getName()
+ # verify the resolution was correct
+ dtTree = dtsorts[0].getDatatype()
+ dtcTreeNode = dtTree[0]
+ assert dtcTreeNode.getName() == "node"
+ dtsTreeNodeLeft = dtcTreeNode[0]
+ assert dtsTreeNodeLeft.getName() == "left"
+ # argument type should have resolved to be recursive
+ assert dtsTreeNodeLeft.getCodomainSort().isDatatype()
+ assert dtsTreeNodeLeft.getCodomainSort() == dtsorts[0]
+
def test_datatype_structs(solver):
intSort = solver.getIntegerSort()
boolSort = solver.getBooleanSort()
# END
# Make unresolved types as placeholders
- unresTypes = set([])
- unresWList = solver.mkUnresolvedSort("wlist")
- unresList = solver.mkUnresolvedSort("list")
- unresNs = solver.mkUnresolvedSort("ns")
- unresTypes.add(unresWList)
- unresTypes.add(unresList)
- unresTypes.add(unresNs)
+ unresWList = solver.mkUnresolvedDatatypeSort("wlist")
+ unresList = solver.mkUnresolvedDatatypeSort("list")
+ unresNs = solver.mkUnresolvedDatatypeSort("ns")
wlist = solver.mkDatatypeDecl("wlist")
leaf = solver.mkDatatypeConstructorDecl("leaf")
dtdecls = [wlist, llist, ns]
# this is well-founded and has no nested recursion
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 3
assert dtsorts[0].getDatatype().isWellFounded()
assert dtsorts[1].getDatatype().isWellFounded()
# ns2 = elem2(ndata: array(int,ns2)) | nil2
# END
- unresTypes.clear()
- unresNs2 = solver.mkUnresolvedSort("ns2")
- unresTypes.add(unresNs2)
+ unresNs2 = solver.mkUnresolvedDatatypeSort("ns2")
ns2 = solver.mkDatatypeDecl("ns2")
elem2 = solver.mkDatatypeConstructorDecl("elem2")
dtdecls.append(ns2)
# this is not well-founded due to non-simple recursion
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 1
assert dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray()
assert dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort() \
# ns3 = elem3(ndata: set(list3))
# END
- unresTypes.clear()
- unresNs3 = solver.mkUnresolvedSort("ns3")
- unresTypes.add(unresNs3)
- unresList3 = solver.mkUnresolvedSort("list3")
- unresTypes.add(unresList3)
+ unresNs3 = solver.mkUnresolvedDatatypeSort("ns3")
+ unresList3 = solver.mkUnresolvedDatatypeSort("list3")
list3 = solver.mkDatatypeDecl("list3")
cons3 = solver.mkDatatypeConstructorDecl("cons3")
dtdecls.append(ns3)
# both are well-founded and have nested recursion
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 2
assert dtsorts[0].getDatatype().isWellFounded()
assert dtsorts[1].getDatatype().isWellFounded()
# list4 = cons(car: set(ns4), cdr: list4) | nil,
# ns4 = elem(ndata: list4)
# END
- unresTypes.clear()
- unresNs4 = solver.mkUnresolvedSort("ns4")
- unresTypes.add(unresNs4)
- unresList4 = solver.mkUnresolvedSort("list4")
- unresTypes.add(unresList4)
+ unresNs4 = solver.mkUnresolvedDatatypeSort("ns4")
+ unresList4 = solver.mkUnresolvedDatatypeSort("list4")
list4 = solver.mkDatatypeDecl("list4")
cons4 = solver.mkDatatypeConstructorDecl("cons4")
dtdecls.append(ns4)
# both are well-founded and have nested recursion
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 2
assert dtsorts[0].getDatatype().isWellFounded()
assert dtsorts[1].getDatatype().isWellFounded()
# DATATYPE
# list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
# END
- unresTypes.clear()
unresList5 = solver.mkUninterpretedSortConstructorSort(1, "list5")
- unresTypes.add(unresList5)
v = []
x = solver.mkParamSort("X")
dtdecls.append(list5)
# well-founded and has nested recursion
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 1
assert dtsorts[0].getDatatype().isWellFounded()
# END
# Make unresolved types as placeholders
- unresTypes = set([])
unresList = solver.mkUninterpretedSortConstructorSort(1, "plist")
- unresTypes.add(unresList)
-
v = []
x = solver.mkParamSort("X")
v.append(x)
dtdecls = [plist]
# make the datatype sorts
- dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
+ dtsorts = solver.mkDatatypeSorts(dtdecls)
assert len(dtsorts) == 1
d = dtsorts[0].getDatatype()
nilc = d[0]
dtypeSpec2.addConstructor(nil2)
decls = [dtypeSpec1, dtypeSpec2]
- solver.mkDatatypeSorts(decls, set([]))
+ solver.mkDatatypeSorts(decls)
with pytest.raises(RuntimeError):
- slv.mkDatatypeSorts(decls, set([]))
+ slv.mkDatatypeSorts(decls)
throwsDtypeSpec = solver.mkDatatypeDecl("list")
throwsDecls = [throwsDtypeSpec]
with pytest.raises(RuntimeError):
- solver.mkDatatypeSorts(throwsDecls, set([]))
+ solver.mkDatatypeSorts(throwsDecls)
# with unresolved sorts
- unresList = solver.mkUnresolvedSort("ulist")
- unresSorts = set([unresList])
+ unresList = solver.mkUnresolvedDatatypeSort("ulist")
ulist = solver.mkDatatypeDecl("ulist")
ucons = solver.mkDatatypeConstructorDecl("ucons")
ucons.addSelector("car", unresList)
ulist.addConstructor(unil)
udecls = [ulist]
- solver.mkDatatypeSorts(udecls, unresSorts)
+ solver.mkDatatypeSorts(udecls)
with pytest.raises(RuntimeError):
- slv.mkDatatypeSorts(udecls, unresSorts)
+ slv.mkDatatypeSorts(udecls)
# mutually recursive with unresolved parameterized sorts
p0 = solver.mkParamSort("p0")
p1 = solver.mkParamSort("p1")
- u0 = solver.mkUnresolvedSort("dt0", 1)
- u1 = solver.mkUnresolvedSort("dt1", 1)
+ u0 = solver.mkUnresolvedDatatypeSort("dt0", 1)
+ u1 = solver.mkUnresolvedDatatypeSort("dt1", 1)
dtdecl0 = solver.mkDatatypeDecl("dt0", p0)
dtdecl1 = solver.mkDatatypeDecl("dt1", p1)
ctordecl0 = solver.mkDatatypeConstructorDecl("c0")
ctordecl1.addSelector("s1", u0.instantiate({p1}))
dtdecl0.addConstructor(ctordecl0)
dtdecl1.addConstructor(ctordecl1)
- dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1], {u0, u1})
+ dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1])
isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()})
t1 = solver.mkConst(isort1, "t")
t0 = solver.mkTerm(
def test_mk_unresolved_sort(solver):
- solver.mkUnresolvedSort("u")
- solver.mkUnresolvedSort("u", 1)
- solver.mkUnresolvedSort("")
- solver.mkUnresolvedSort("", 1)
+ solver.mkUnresolvedDatatypeSort("u")
+ solver.mkUnresolvedDatatypeSort("u", 1)
+ solver.mkUnresolvedDatatypeSort("")
+ solver.mkUnresolvedDatatypeSort("", 1)
def test_mk_sort_constructor_sort(solver):
projects / cvc5.git / commitdiff