CVC5_API_TRY_CATCH_END;
}
+std::vector<Sort> Sort::getInstantiatedParameters() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_CHECK(d_type->isInstantiated())
+ << "Expected instantiated parametric sort";
+ //////// all checks before this line
+ return typeNodeVectorToSorts(d_solver, d_type->getInstantiatedParamTypes());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_TRY_CATCH_END;
}
-/* Uninterpreted sort -------------------------------------------------- */
-
-std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
- //////// all checks before this line
-
- /* This method is not implemented in the NodeManager, since whether a
- * uninterpreted sort is parameterized is irrelevant for solving. */
- std::vector<TypeNode> params;
- for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++)
- {
- params.push_back((*d_type)[i]);
- }
- return typeNodeVectorToSorts(d_solver, params);
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
/* Sort constructor sort ----------------------------------------------- */
size_t Sort::getUninterpretedSortConstructorArity() const
/* Datatype sort ------------------------------------------------------- */
-std::vector<Sort> Sort::getDatatypeParamSorts() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(d_type->isParametricDatatype())
- << "Not a parametric datatype sort.";
- //////// all checks before this line
- return typeNodeVectorToSorts(d_solver, d_type->getDType().getParameters());
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
size_t Sort::getDatatypeArity() const
{
CVC5_API_TRY_CATCH_BEGIN;
* Instantiate a parameterized datatype sort or uninterpreted sort
* constructor sort.
*
- * Create sorts parameter with Solver::mkParamSort().
+ * Create sort parameters with Solver::mkParamSort().
*
* @warning This method is experimental and may change in future versions.
*
* @param params the list of sort parameters to instantiate with
+ * @return the instantiated sort
*/
Sort instantiate(const std::vector<Sort>& params) const;
+ /**
+ * Get the sorts used to instantiate the sort parameters of a parametric
+ * sort (parametric datatype or uninterpreted sort constructor sort,
+ * see Sort::instantiate(const std::vector<Sort>& const)).
+ *
+ * @return the sorts used to instantiate the sort parameters of a
+ * parametric sort
+ */
+ std::vector<Sort> getInstantiatedParameters() const;
+
/**
* Substitution of Sorts.
*
*/
bool isUninterpretedSortParameterized() const;
- /**
- * @return the parameter sorts of an uninterpreted sort
- */
- std::vector<Sort> getUninterpretedSortParamSorts() const;
-
/* Sort constructor sort ----------------------------------------------- */
/**
/* Datatype sort ------------------------------------------------------- */
- /**
- *
- * Return the parameters of a parametric datatype sort. If this sort is a
- * non-instantiated parametric datatype, this returns the parameter sorts of
- * the underlying datatype. If this sort is an instantiated parametric
- * datatype, then this returns the sort parameters that were used to
- * construct the sort via Sort::instantiate().
- *
- * @return the parameter sorts of a parametric datatype sort.
- */
- std::vector<Sort> getDatatypeParamSorts() const;
-
/**
* @return the arity of a datatype sort
*/
* @apiNote This method is experimental and may change in future versions.
*
* @param params the list of sort parameters to instantiate with
+ * @return the instantiated sort
*/
public Sort instantiate(List<Sort> params)
{
private native long instantiate(long pointer, long[] paramsPointers);
+ /**
+ * Get the sorts used to instantiate the sort parameters of a parametric
+ * sort (parametric datatype or uninterpreted sort constructor sort,
+ * see Sort.instantiate()).
+ *
+ * @return the sorts used to instantiate the sort parameters of a
+ * parametric sort
+ */
+ public Sort[] getInstantiatedParameters()
+ {
+ long[] pointers = getInstantiatedParameters(pointer);
+ return Utils.getSorts(solver, pointers);
+ }
+
+ private native long[] getInstantiatedParameters(long pointer);
+
/**
* Substitution of Sorts.
*
private native long getSequenceElementSort(long pointer);
- /* Uninterpreted sort -------------------------------------------------- */
-
- /**
- * @return the parameter sorts of an uninterpreted sort
- */
- public Sort[] getUninterpretedSortParamSorts()
- {
- long[] pointers = getUninterpretedSortParamSorts(pointer);
- return Utils.getSorts(solver, pointers);
- }
-
- private native long[] getUninterpretedSortParamSorts(long pointer);
-
/* Sort constructor sort ----------------------------------------------- */
/**
/* Datatype sort ------------------------------------------------------- */
- /**
- * Return the parameters of a parametric datatype sort. If this sort is a
- * non-instantiated parametric datatype, this returns the parameter sorts of
- * the underlying datatype. If this sort is an instantiated parametric
- * datatype, then this returns the sort parameters that were used to
- * construct the sort via Sort.instantiate().
- *
- * @return the parameter sorts of a datatype sort
- */
- public Sort[] getDatatypeParamSorts()
- {
- long[] pointers = getDatatypeParamSorts(pointer);
- return Utils.getSorts(solver, pointers);
- }
-
- private native long[] getDatatypeParamSorts(long pointer);
-
/**
* @return the arity of a datatype sort
*/
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
}
+/*
+ * Class: io_github_cvc5_api_Sort
+ * Method: getInstantiatedParameters
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL
+Java_io_github_cvc5_api_Sort_getInstantiatedParameters(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ std::vector<Sort> sorts = current->getInstantiatedParameters();
+ std::vector<jlong> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
+ }
+ jlongArray ret = env->NewLongArray(sorts.size());
+ env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
/*
* Class: io_github_cvc5_api_Sort
* Method: getDatatype
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
-/*
- * Class: io_github_cvc5_api_Sort
- * Method: getUninterpretedSortParamSorts
- * Signature: (J)[J
- */
-JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env,
- jobject,
- jlong pointer)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Sort* current = reinterpret_cast<Sort*>(pointer);
- std::vector<Sort> sorts = current->getUninterpretedSortParamSorts();
- std::vector<jlong> sortPointers(sorts.size());
- for (size_t i = 0; i < sorts.size(); i++)
- {
- sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
- }
- jlongArray ret = env->NewLongArray(sorts.size());
- env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
- return ret;
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
/*
* Class: io_github_cvc5_api_Sort
* Method: getUninterpretedSortConstructorArity
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
-/*
- * Class: io_github_cvc5_api_Sort
- * Method: getDatatypeParamSorts
- * Signature: (J)[J
- */
-JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Sort_getDatatypeParamSorts(
- JNIEnv* env, jobject, jlong pointer)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Sort* current = reinterpret_cast<Sort*>(pointer);
- std::vector<Sort> sorts = current->getDatatypeParamSorts();
- std::vector<jlong> sortPointers(sorts.size());
- for (size_t i = 0; i < sorts.size(); i++)
- {
- sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
- }
- jlongArray ret = env->NewLongArray(sorts.size());
- env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
- return ret;
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
/*
* Class: io_github_cvc5_api_Sort
* Method: getDatatypeArity
bint isInstantiated() except +
Datatype getDatatype() except +
Sort instantiate(const vector[Sort]& params) except +
+ vector[Sort] getInstantiatedParameters() except +
Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
size_t getConstructorArity() except +
vector[Sort] getConstructorDomainSorts() except +
Sort getSetElementSort() except +
Sort getBagElementSort() except +
Sort getSequenceElementSort() except +
- vector[Sort] getUninterpretedSortParamSorts() except +
size_t getUninterpretedSortConstructorArity() except +
uint32_t getBitVectorSize() except +
uint32_t getFloatingPointExponentSize() except +
uint32_t getFloatingPointSignificandSize() except +
- vector[Sort] getDatatypeParamSorts() except +
size_t getDatatypeArity() except +
size_t getTupleLength() except +
vector[Sort] getTupleSorts() except +
versions.
:param params: the list of sort parameters to instantiate with
+ :return: the instantiated sort
"""
cdef Sort sort = Sort(self.solver)
cdef vector[c_Sort] v
sort.csort = self.csort.instantiate(v)
return sort
+ def getInstantiatedParameters(self):
+ """
+ Get the sorts used to instantiate the sort parameters of a
+ parametric sort (parametric datatype or uninterpreted sort
+ constructor sort, see Sort.instantiate()).
+
+ :return the sorts used to instantiate the sort parameters of a
+ parametric sort
+ """
+ instantiated_sorts = []
+ for s in self.csort.getInstantiatedParameters():
+ sort = Sort(self.solver)
+ sort.csort = s
+ instantiated_sorts.append(sort)
+ return instantiated_sorts
+
def substitute(self, sort_or_list_1, sort_or_list_2):
"""
Substitution of Sorts.
sort.csort = self.csort.getSequenceElementSort()
return sort
- def getUninterpretedSortParamSorts(self):
- """
- :return: the parameter sorts of an uninterpreted sort
- """
- param_sorts = []
- for s in self.csort.getUninterpretedSortParamSorts():
- sort = Sort(self.solver)
- sort.csort = s
- param_sorts.append(sort)
- return param_sorts
-
def getUninterpretedSortConstructorArity(self):
"""
:return: the arity of a sort constructor sort
"""
return self.csort.getFloatingPointSignificandSize()
- def getDatatypeParamSorts(self):
- """
- Return the parameters of a parametric datatype sort. If this sort
- is a non-instantiated parametric datatype, this returns the
- parameter sorts of the underlying datatype. If this sort is an
- instantiated parametric datatype, then this returns the sort
- parameters that were used to construct the sort via
- :py:meth:`instantiate()`.
-
- :return: the parameter sorts of a parametric datatype sort
- """
- param_sorts = []
- for s in self.csort.getDatatypeParamSorts():
- sort = Sort(self.solver)
- sort.csort = s
- param_sorts.append(sort)
- return param_sorts
-
def getDatatypeArity(self):
"""
:return: the arity of a datatype sort
{
Assert(isInstantiated());
vector<TypeNode> params;
- for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i)
+ for (uint32_t i = isInstantiatedDatatype() ? 1 : 0, i_end = getNumChildren();
+ i < i_end;
+ ++i)
{
params.push_back((*this)[i]);
}
{
// instantiate parametric datatype, check should not fail
Sort paramDtypeSort = create_param_datatype_sort();
- ASSERT_NO_THROW(
- paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
+ ASSERT_NO_THROW(paramDtypeSort.instantiate({d_solver.getIntegerSort()}));
// instantiate non-parametric datatype sort, check should fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
- ASSERT_THROW(
- dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
- CVC5ApiException);
+ ASSERT_THROW(dtypeSort.instantiate({d_solver.getIntegerSort()}),
+ CVC5ApiException);
// instantiate uninterpreted sort constructor
Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
- ASSERT_NO_THROW(
- sortConsSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
+ ASSERT_NO_THROW(sortConsSort.instantiate({d_solver.getIntegerSort()}));
}
TEST_F(TestApiBlackSort, isInstantiated)
Sort paramDtypeSort = create_param_datatype_sort();
ASSERT_FALSE(paramDtypeSort.isInstantiated());
Sort instParamDtypeSort =
- paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+ paramDtypeSort.instantiate({d_solver.getIntegerSort()});
ASSERT_TRUE(instParamDtypeSort.isInstantiated());
Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
ASSERT_FALSE(sortConsSort.isInstantiated());
- Sort instSortConsSort =
- sortConsSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+ Sort instSortConsSort = sortConsSort.instantiate({d_solver.getIntegerSort()});
ASSERT_TRUE(instSortConsSort.isInstantiated());
ASSERT_FALSE(d_solver.getIntegerSort().isInstantiated());
ASSERT_FALSE(d_solver.mkBitVectorSort(32).isInstantiated());
}
+TEST_F(TestApiBlackSort, getInstantiatedParameters)
+{
+ Sort intSort = d_solver.getIntegerSort();
+ Sort realSort = d_solver.getRealSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ std::vector<Sort> instSorts;
+
+ // parametric datatype instantiation
+ Sort p1 = d_solver.mkParamSort("p1");
+ Sort p2 = d_solver.mkParamSort("p2");
+ DatatypeDecl pspec = d_solver.mkDatatypeDecl("pdtype", {p1, p2});
+ DatatypeConstructorDecl pcons1 = d_solver.mkDatatypeConstructorDecl("cons1");
+ DatatypeConstructorDecl pcons2 = d_solver.mkDatatypeConstructorDecl("cons2");
+ DatatypeConstructorDecl pnil = d_solver.mkDatatypeConstructorDecl("nil");
+ pcons1.addSelector("sel", p1);
+ pcons2.addSelector("sel", p2);
+ pspec.addConstructor(pcons1);
+ pspec.addConstructor(pcons2);
+ pspec.addConstructor(pnil);
+ Sort paramDtypeSort = d_solver.mkDatatypeSort(pspec);
+
+ ASSERT_THROW(paramDtypeSort.getInstantiatedParameters(), CVC5ApiException);
+
+ Sort instParamDtypeSort = paramDtypeSort.instantiate({realSort, boolSort});
+
+ instSorts = instParamDtypeSort.getInstantiatedParameters();
+ ASSERT_EQ(instSorts[0], realSort);
+ ASSERT_EQ(instSorts[1], boolSort);
+
+ // uninterpreted sort constructor sort instantiation
+ Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4);
+ ASSERT_THROW(sortConsSort.getInstantiatedParameters(), CVC5ApiException);
+
+ Sort instSortConsSort =
+ sortConsSort.instantiate({boolSort, intSort, bvSort, realSort});
+
+ instSorts = instSortConsSort.getInstantiatedParameters();
+ ASSERT_EQ(instSorts[0], boolSort);
+ ASSERT_EQ(instSorts[1], intSort);
+ ASSERT_EQ(instSorts[2], bvSort);
+ ASSERT_EQ(instSorts[3], realSort);
+
+ ASSERT_THROW(intSort.getInstantiatedParameters(), CVC5ApiException);
+ ASSERT_THROW(bvSort.getInstantiatedParameters(), CVC5ApiException);
+}
+
TEST_F(TestApiBlackSort, getFunctionArity)
{
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException);
}
-TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
-{
- Sort uSort = d_solver.mkUninterpretedSort("u");
- ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
- Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
- Sort siSort = sSort.instantiate({uSort, uSort});
- ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
- Sort bvSort = d_solver.mkBitVectorSort(32);
- ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC5ApiException);
-}
-
TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
{
Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException);
}
-TEST_F(TestApiBlackSort, getDatatypeParamSorts)
-{
- // create parametric datatype, check should not fail
- Sort sort = d_solver.mkParamSort("T");
- DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl paramCons =
- d_solver.mkDatatypeConstructorDecl("cons");
- DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
- paramCons.addSelector("head", sort);
- paramDtypeSpec.addConstructor(paramCons);
- paramDtypeSpec.addConstructor(paramNil);
- Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
- ASSERT_NO_THROW(paramDtypeSort.getDatatypeParamSorts());
- // create non-parametric datatype sort, check should fail
- DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
- cons.addSelector("head", d_solver.getIntegerSort());
- dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
- dtypeSpec.addConstructor(nil);
- Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
- ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC5ApiException);
-}
-
TEST_F(TestApiBlackSort, getDatatypeArity)
{
// create datatype sort, check should not fail
assertFalse(d_solver.mkBitVectorSort(32).isInstantiated());
}
+ @Test void getInstantiatedParameters() throws CVC5ApiException
+ {
+ Sort intSort = d_solver.getIntegerSort();
+ Sort realSort = d_solver.getRealSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort[] instSorts;
+
+ // parametric datatype instantiation
+ Sort p1 = d_solver.mkParamSort("p1");
+ Sort p2 = d_solver.mkParamSort("p2");
+ DatatypeDecl pspec = d_solver.mkDatatypeDecl("pdtype", new Sort[] {p1, p2});
+ DatatypeConstructorDecl pcons1 = d_solver.mkDatatypeConstructorDecl("cons1");
+ DatatypeConstructorDecl pcons2 = d_solver.mkDatatypeConstructorDecl("cons2");
+ DatatypeConstructorDecl pnil = d_solver.mkDatatypeConstructorDecl("nil");
+ pcons1.addSelector("sel", p1);
+ pcons2.addSelector("sel", p2);
+ pspec.addConstructor(pcons1);
+ pspec.addConstructor(pcons2);
+ pspec.addConstructor(pnil);
+ Sort paramDtypeSort = d_solver.mkDatatypeSort(pspec);
+
+ assertThrows(CVC5ApiException.class, () -> paramDtypeSort.getInstantiatedParameters());
+
+ Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {realSort, boolSort});
+
+ instSorts = instParamDtypeSort.getInstantiatedParameters();
+ assertEquals(instSorts[0], realSort);
+ assertEquals(instSorts[1], boolSort);
+
+ // uninterpreted sort constructor sort instantiation
+ Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4);
+ assertThrows(CVC5ApiException.class, () -> sortConsSort.getInstantiatedParameters());
+
+ Sort instSortConsSort =
+ sortConsSort.instantiate(new Sort[] {boolSort, intSort, bvSort, realSort});
+
+ instSorts = instSortConsSort.getInstantiatedParameters();
+ assertEquals(instSorts[0], boolSort);
+ assertEquals(instSorts[1], intSort);
+ assertEquals(instSorts[2], bvSort);
+ assertEquals(instSorts[3], realSort);
+
+ assertThrows(CVC5ApiException.class, () -> intSort.getInstantiatedParameters());
+ assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters());
+ }
+
@Test void getFunctionArity() throws CVC5ApiException
{
Sort funSort =
assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol());
}
- @Test void getUninterpretedSortParamSorts() throws CVC5ApiException
- {
- Sort uSort = d_solver.mkUninterpretedSort("u");
- assertDoesNotThrow(() -> uSort.getUninterpretedSortParamSorts());
- Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
- Sort siSort = sSort.instantiate(new Sort[] {uSort, uSort});
- assertEquals(siSort.getUninterpretedSortParamSorts().length, 2);
- Sort bvSort = d_solver.mkBitVectorSort(32);
- assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortParamSorts());
- }
-
@Test void getUninterpretedSortConstructorName() throws CVC5ApiException
{
Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize());
}
- @Test void getDatatypeParamSorts() throws CVC5ApiException
- {
- // create parametric datatype, check should not fail
- Sort sort = d_solver.mkParamSort("T");
- DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl paramCons = d_solver.mkDatatypeConstructorDecl("cons");
- DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
- paramCons.addSelector("head", sort);
- paramDtypeSpec.addConstructor(paramCons);
- paramDtypeSpec.addConstructor(paramNil);
- Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
- assertDoesNotThrow(() -> paramDtypeSort.getDatatypeParamSorts());
- // create non-parametric datatype sort, check should fail
- DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
- cons.addSelector("head", d_solver.getIntegerSort());
- dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
- dtypeSpec.addConstructor(nil);
- Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
- assertThrows(CVC5ApiException.class, () -> dtypeSort.getDatatypeParamSorts());
- }
-
@Test void getDatatypeArity() throws CVC5ApiException
{
// create datatype sort, check should not fail
assert not solver.getIntegerSort().isInstantiated()
assert not solver.mkBitVectorSort(32).isInstantiated()
+def test_get_instantiated_parameters(solver):
+ intSort = solver.getIntegerSort()
+ realSort = solver.getRealSort()
+ boolSort = solver.getBooleanSort()
+ bvSort = solver.mkBitVectorSort(8)
+
+ # parametric datatype instantiation
+ p1 = solver.mkParamSort("p1")
+ p2 = solver.mkParamSort("p2")
+ pspec = solver.mkDatatypeDecl("pdtype", [p1, p2])
+ pcons1 = solver.mkDatatypeConstructorDecl("cons1")
+ pcons2 = solver.mkDatatypeConstructorDecl("cons2")
+ pnil = solver.mkDatatypeConstructorDecl("nil")
+ pcons1.addSelector("sel", p1)
+ pcons2.addSelector("sel", p2)
+ pspec.addConstructor(pcons1)
+ pspec.addConstructor(pcons2)
+ pspec.addConstructor(pnil)
+ paramDtypeSort = solver.mkDatatypeSort(pspec)
+
+ with pytest.raises(RuntimeError):
+ paramDtypeSort.getInstantiatedParameters()
+
+ instParamDtypeSort = \
+ paramDtypeSort.instantiate([realSort, boolSort]);
+
+ instSorts = instParamDtypeSort.getInstantiatedParameters();
+ assert instSorts[0] == realSort
+ assert instSorts[1] == boolSort
+
+ # uninterpreted sort constructor sort instantiation
+ sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4)
+ with pytest.raises(RuntimeError):
+ sortConsSort.getInstantiatedParameters()
+
+ instSortConsSort = sortConsSort.instantiate(
+ [boolSort, intSort, bvSort, realSort]);
+
+ instSorts = instSortConsSort.getInstantiatedParameters()
+ assert instSorts[0] == boolSort
+ assert instSorts[1] == intSort
+ assert instSorts[2] == bvSort
+ assert instSorts[3] == realSort
+
+ with pytest.raises(RuntimeError):
+ intSort.getInstantiatedParameters()
+ with pytest.raises(RuntimeError):
+ bvSort.getInstantiatedParameters()
+
def test_get_function_arity(solver):
funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
solver.getIntegerSort())
bvSort.getSymbol()
-def test_get_uninterpreted_sort_paramsorts(solver):
- uSort = solver.mkUninterpretedSort("u")
- uSort.getUninterpretedSortParamSorts()
- sSort = solver.mkUninterpretedSortConstructorSort("s", 2)
- siSort = sSort.instantiate([uSort, uSort])
- assert len(siSort.getUninterpretedSortParamSorts()) == 2
- bvSort = solver.mkBitVectorSort(32)
- with pytest.raises(RuntimeError):
- bvSort.getUninterpretedSortParamSorts()
-
-
def test_get_uninterpreted_sort_constructor_name(solver):
sSort = solver.mkUninterpretedSortConstructorSort("s", 2)
sSort.getSymbol()
setSort.getFloatingPointSignificandSize()
-def test_get_datatype_paramsorts(solver):
- # create parametric datatype, check should not fail
- sort = solver.mkParamSort("T")
- paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
- paramCons = solver.mkDatatypeConstructorDecl("cons")
- paramNil = solver.mkDatatypeConstructorDecl("nil")
- paramCons.addSelector("head", sort)
- paramDtypeSpec.addConstructor(paramCons)
- paramDtypeSpec.addConstructor(paramNil)
- paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
- paramDtypeSort.getDatatypeParamSorts()
- # create non-parametric datatype sort, check should fail
- dtypeSpec = solver.mkDatatypeDecl("list")
- cons = solver.mkDatatypeConstructorDecl("cons")
- cons.addSelector("head", solver.getIntegerSort())
- dtypeSpec.addConstructor(cons)
- nil = solver.mkDatatypeConstructorDecl("nil")
- dtypeSpec.addConstructor(nil)
- dtypeSort = solver.mkDatatypeSort(dtypeSpec)
- with pytest.raises(RuntimeError):
- dtypeSort.getDatatypeParamSorts()
-
-
def test_get_datatype_arity(solver):
# create datatype sort, check should not fail
dtypeSpec = solver.mkDatatypeDecl("list")
projects / cvc5.git / commitdiff