Sort u = slv.mkUninterpretedSort("u");
Sort integer = slv.getIntegerSort();
Sort boolean = slv.getBooleanSort();
- Sort uToInt = slv.mkFunctionSort(u, integer);
- Sort intPred = slv.mkFunctionSort(integer, boolean);
+ Sort uToInt = slv.mkFunctionSort({u}, integer);
+ Sort intPred = slv.mkFunctionSort({integer}, boolean);
// Variables
Term x = slv.mkConst(u, "x");
Sort integer = slv.getIntegerSort();
Sort boolean = slv.getBooleanSort();
- Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
+ Sort integerPredicate = slv.mkFunctionSort({integer}, boolean);
Term p = slv.mkConst(integerPredicate, "P");
Term x = slv.mkVar(integer, "x");
CVC5_API_TRY_CATCH_END;
}
-Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain);
- CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain);
- //////// all checks before this line
- return Sort(
- this, getNodeManager()->mkFunctionType(*domain.d_type, *codomain.d_type));
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
const Sort& codomain) const
{
const std::vector<DatatypeDecl>& dtypedecls,
const std::set<Sort>& unresolvedSorts) const;
- /**
- * Create function sort.
- * @param domain the sort of the function argument
- * @param codomain the sort of the function return value
- * @return the function sort
- */
- Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const;
-
/**
* Create function sort.
* @param sorts the sort of the function arguments
*/
public Sort mkFunctionSort(Sort domain, Sort codomain)
{
- long sortPointer = mkFunctionSort(pointer, domain.getPointer(), codomain.getPointer());
- return new Sort(this, sortPointer);
+ return mkFunctionSort(new Sort[] {domain}, codomain);
}
- private native long mkFunctionSort(long pointer, long domainPointer, long codomainPointer);
-
/**
* Create function sort.
* @param sorts the sort of the function arguments
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
}
-/*
- * Class: io_github_cvc5_Solver
- * Method: mkFunctionSort
- * Signature: (JJJ)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkFunctionSort__JJJ(JNIEnv* env,
- jobject,
- jlong pointer,
- jlong domainPointer,
- jlong codomainPointer)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- Sort* domain = reinterpret_cast<Sort*>(domainPointer);
- Sort* codomain = reinterpret_cast<Sort*>(codomainPointer);
- Sort* sortPointer = new Sort(solver->mkFunctionSort(*domain, *codomain));
- return reinterpret_cast<jlong>(sortPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
/*
* Class: io_github_cvc5_Solver
* Method: mkFunctionSort
* Signature: (J[JJ)J
*/
JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env,
- jobject,
- jlong pointer,
- jlongArray sortPointers,
- jlong codomainPointer)
+Java_io_github_cvc5_Solver_mkFunctionSort(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlongArray sortPointers,
+ jlong codomainPointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Solver* solver = reinterpret_cast<Solver*>(pointer);
Sort mkDatatypeSort(DatatypeDecl dtypedecl) except +
vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls,
const set[Sort]& unresolvedSorts) except +
- Sort mkFunctionSort(Sort domain, Sort codomain) except +
Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except +
Sort mkParamSort() except +
Sort mkParamSort(const string& symbol) except +
cdef Sort sort = Sort(self)
# populate a vector with dereferenced c_Sorts
cdef vector[c_Sort] v
-
if isinstance(sorts, Sort):
- sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
- codomain.csort)
- elif isinstance(sorts, list):
+ v.push_back((<Sort?>sorts).csort)
+ else:
for s in sorts:
v.push_back((<Sort?>s).csort)
- sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
- codomain.csort)
+ sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
+ codomain.csort)
return sort
def mkParamSort(self, str symbolname = None):
if (d_rtu_op.isNull()) {
cvc5::Sort t;
// Conversion from rational to unsorted
- t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
+ t = d_solver->mkFunctionSort({d_solver->getRealSort()}, d_unsorted);
d_rtu_op = d_solver->mkConst(t, "$$rtu");
preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
// Conversion from unsorted to rational
- t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
+ t = d_solver->mkFunctionSort({d_unsorted}, d_solver->getRealSort());
d_utr_op = d_solver->mkConst(t, "$$utr");
preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
}
TEST_F(TestApiBlackSolver, mkFunctionSort)
{
- ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ ASSERT_NO_THROW(d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort()));
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
// function arguments are allowed
- ASSERT_NO_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
+ ASSERT_NO_THROW(
+ d_solver.mkFunctionSort({funSort}, d_solver.getIntegerSort()));
// non-first-class arguments are not allowed
Sort reSort = d_solver.getRegExpSort();
- ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()),
+ ASSERT_THROW(d_solver.mkFunctionSort({reSort}, d_solver.getIntegerSort()),
CVC5ApiException);
- ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
+ ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort()}, funSort),
CVC5ApiException);
ASSERT_NO_THROW(d_solver.mkFunctionSort(
{d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
d_solver.getIntegerSort()));
- Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
// function arguments are allowed
ASSERT_NO_THROW(
CVC5ApiException);
Solver slv;
- ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ ASSERT_THROW(slv.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort()),
CVC5ApiException);
- ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+ ASSERT_THROW(slv.mkFunctionSort({slv.mkUninterpretedSort("u")},
d_solver.getIntegerSort()),
CVC5ApiException);
std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
{
ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
ASSERT_THROW(d_solver.mkPredicateSort({}), CVC5ApiException);
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
// functions as arguments are allowed
ASSERT_NO_THROW(
TEST_F(TestApiBlackSolver, mkTupleSort)
{
ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
CVC5ApiException);
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
- Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
ASSERT_NO_THROW(d_solver.mkVar(boolSort));
ASSERT_NO_THROW(d_solver.mkVar(funSort));
ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
- Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
ASSERT_NO_THROW(d_solver.mkConst(boolSort));
ASSERT_NO_THROW(d_solver.mkConst(funSort));
ASSERT_NO_THROW(d_solver.mkConst(boolSort, std::string("b")));
TEST_F(TestApiBlackSolver, declareFun)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
ASSERT_NO_THROW(
TEST_F(TestApiBlackSolver, defineFun)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
Term b1 = d_solver.mkVar(bvSort, "b1");
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
- Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
Term b1 = d_solver.mkVar(bvSort, "b1");
Term b11 = d_solver.mkVar(bvSort, "b1");
TEST_F(TestApiBlackSolver, defineFunRecGlobal)
{
Sort bSort = d_solver.getBooleanSort();
- Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+ Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
d_solver.push();
Term bTrue = d_solver.mkBoolean(true);
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
- Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+ Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
Term b1 = d_solver.mkVar(bvSort, "b1");
Term b11 = d_solver.mkVar(bvSort, "b1");
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
Sort uSort2 = slv.mkUninterpretedSort("u");
Sort bvSort2 = slv.mkBitVectorSort(32);
Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
- Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
+ Sort funSort22 = slv.mkFunctionSort({uSort2}, slv.getIntegerSort());
Term b12 = slv.mkVar(bvSort2, "b1");
Term b112 = slv.mkVar(bvSort2, "b1");
Term b42 = slv.mkVar(uSort2, "b4");
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
- Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+ Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
Term b = d_solver.mkVar(bvSort, "b");
Term u = d_solver.mkVar(uSort, "u");
Term v1 = d_solver.mkConst(bvSort, "v1");
TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
{
Sort bSort = d_solver.getBooleanSort();
- Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+ Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
d_solver.push();
Term bTrue = d_solver.mkBoolean(true);
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
- Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+ Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
std::vector<Term> uc;
Term x = d_solver.mkConst(uSort, "x");
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
- Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+ Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
std::vector<Term> unsat_core;
Term x = d_solver.mkConst(uSort, "x");
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
- Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+ Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
- Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+ Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
Term n = Term();
// Constants
d_solver.setOption("sygus", "true");
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
- Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
ASSERT_NO_THROW(d_solver.declareSygusVar("", boolSort));
ASSERT_NO_THROW(d_solver.declareSygusVar("", funSort));
TEST_F(TestApiBlackSolver, issue7000)
{
Sort s1 = d_solver.getIntegerSort();
- Sort s2 = d_solver.mkFunctionSort(s1, s1);
+ Sort s2 = d_solver.mkFunctionSort({s1}, s1);
Sort s3 = d_solver.getRealSort();
Term t4 = d_solver.mkPi();
Term t7 = d_solver.mkConst(s3, "_x5");
TEST_F(TestApiBlackSort, isFunction)
{
- Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(),
+ Sort fun_sort = d_solver.mkFunctionSort({d_solver.getRealSort()},
d_solver.getIntegerSort());
ASSERT_TRUE(fun_sort.isFunction());
ASSERT_NO_THROW(Sort().isFunction());
TEST_F(TestApiBlackSort, getFunctionArity)
{
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort(),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
ASSERT_NO_THROW(funSort.getFunctionArity());
Sort bvSort = d_solver.mkBitVectorSort(32);
TEST_F(TestApiBlackSort, getFunctionDomainSorts)
{
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
ASSERT_NO_THROW(funSort.getFunctionDomainSorts());
Sort bvSort = d_solver.mkBitVectorSort(32);
TEST_F(TestApiBlackSort, getFunctionCodomainSort)
{
- Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
d_solver.getIntegerSort());
ASSERT_NO_THROW(funSort.getFunctionCodomainSort());
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({uSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term n;
ASSERT_THROW(n.getKind(), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term n;
ASSERT_THROW(n.getSort(), CVC5ApiException);
Sort intsort = d_solver.getIntegerSort();
Sort bvsort = d_solver.mkBitVectorSort(8);
Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
- Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+ Sort funsort = d_solver.mkFunctionSort({intsort}, bvsort);
Term x = d_solver.mkConst(intsort, "x");
Term a = d_solver.mkConst(arrsort, "a");
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
ASSERT_THROW(Term().notTerm(), CVC5ApiException);
Term b = d_solver.mkTrue();
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().andTerm(b), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().orTerm(b), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().xorTerm(b), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().eqTerm(b), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().impTerm(b), CVC5ApiException);
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
- Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
- Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+ Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
Term b = d_solver.mkTrue();
ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException);
// apply term f(2)
Sort intSort = d_solver.getIntegerSort();
- Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+ Sort fsort = d_solver.mkFunctionSort({intSort}, intSort);
Term f = d_solver.mkConst(fsort, "f");
Term t2 = d_solver.mkTerm(APPLY_UF, {f, two});
// due to our higher-order view of terms, we treat f as a child of APPLY_UF
Sort intsort = d_solver.getIntegerSort();
Sort bvsort = d_solver.mkBitVectorSort(8);
Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
- Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+ Sort funsort = d_solver.mkFunctionSort({intsort}, bvsort);
Term x = d_solver.mkConst(intsort, "x");
Term a = d_solver.mkConst(arrsort, "a");
cvc5::Sort u = parser.mkSort("u");
cvc5::Sort v = parser.mkSort("v");
/* f : t->u; g: u->v; h: v->t; */
- parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u));
- parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v));
- parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t));
+ parser.bindVar("f", d_solver.get()->mkFunctionSort({t}, u));
+ parser.bindVar("g", d_solver.get()->mkFunctionSort({u}, v));
+ parser.bindVar("h", d_solver.get()->mkFunctionSort({v}, t));
/* x:t; y:u; z:v; */
parser.bindVar("x", t);
parser.bindVar("y", u);