This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+import java.util.List;
+
+public class Sort extends AbstractPointer implements Comparable<Sort>
+{
+ // region construction and destruction
+ Sort(Solver solver, long pointer)
+ {
+ super(solver, pointer);
+ }
+
+ protected static native void deletePointer(long pointer);
+
+ public long getPointer()
+ {
+ return pointer;
+ }
+
+ @Override
+ public void finalize()
+ {
+ deletePointer(pointer);
+ }
+
+ // endregion
+
+ /**
+ * Comparison for structural equality.
+ * @param s the sort to compare to
+ * @return true if the sorts are equal
+ */
+ @Override public boolean equals(Object s)
+ {
+ if (this == s)
+ return true;
+ if (s == null || getClass() != s.getClass())
+ return false;
+ Sort sort = (Sort) s;
+ if (this.pointer == sort.pointer)
+ {
+ return true;
+ }
+ return equals(pointer, sort.getPointer());
+ }
+
+ private native boolean equals(long pointer1, long pointer2);
+
+ /**
+ * Comparison for ordering on sorts.
+ *
+ * @param s the sort to compare to
+ * @return a negative integer, zero, or a positive integer as this sort
+ * is less than, equal to, or greater than the specified sort.
+ */
+ @Override public int compareTo(Sort s)
+ {
+ return this.compareTo(pointer, s.getPointer());
+ }
+
+ private native int compareTo(long pointer1, long pointer2);
+
+ /**
+ * @return true if this Sort is a null sort.
+ */
+ public boolean isNull()
+ {
+ return isNull(pointer);
+ }
+
+ private native boolean isNull(long pointer);
+
+ /**
+ * Is this a Boolean sort?
+ * @return true if the sort is a Boolean sort
+ */
+ public boolean isBoolean()
+ {
+ return isBoolean(pointer);
+ }
+
+ private native boolean isBoolean(long pointer);
+
+ /**
+ * Is this a integer sort?
+ * @return true if the sort is a integer sort
+ */
+ public boolean isInteger()
+ {
+ return isInteger(pointer);
+ }
+
+ private native boolean isInteger(long pointer);
+
+ /**
+ * Is this a real sort?
+ * @return true if the sort is a real sort
+ */
+ public boolean isReal()
+ {
+ return isReal(pointer);
+ }
+
+ private native boolean isReal(long pointer);
+
+ /**
+ * Is this a string sort?
+ * @return true if the sort is the string sort
+ */
+ public boolean isString()
+ {
+ return isString(pointer);
+ }
+
+ private native boolean isString(long pointer);
+
+ /**
+ * Is this a regexp sort?
+ * @return true if the sort is the regexp sort
+ */
+ public boolean isRegExp()
+ {
+ return isRegExp(pointer);
+ }
+
+ private native boolean isRegExp(long pointer);
+
+ /**
+ * Is this a rounding mode sort?
+ * @return true if the sort is the rounding mode sort
+ */
+ public boolean isRoundingMode()
+ {
+ return isRoundingMode(pointer);
+ }
+
+ private native boolean isRoundingMode(long pointer);
+
+ /**
+ * Is this a bit-vector sort?
+ * @return true if the sort is a bit-vector sort
+ */
+ public boolean isBitVector()
+ {
+ return isBitVector(pointer);
+ }
+
+ private native boolean isBitVector(long pointer);
+
+ /**
+ * Is this a floating-point sort?
+ * @return true if the sort is a floating-point sort
+ */
+ public boolean isFloatingPoint()
+ {
+ return isFloatingPoint(pointer);
+ }
+
+ private native boolean isFloatingPoint(long pointer);
+
+ /**
+ * Is this a datatype sort?
+ * @return true if the sort is a datatype sort
+ */
+ public boolean isDatatype()
+ {
+ return isDatatype(pointer);
+ }
+
+ private native boolean isDatatype(long pointer);
+
+ /**
+ * Is this a parametric datatype sort?
+ * @return true if the sort is a parametric datatype sort
+ */
+ public boolean isParametricDatatype()
+ {
+ return isParametricDatatype(pointer);
+ }
+
+ private native boolean isParametricDatatype(long pointer);
+
+ /**
+ * Is this a constructor sort?
+ * @return true if the sort is a constructor sort
+ */
+ public boolean isConstructor()
+ {
+ return isConstructor(pointer);
+ }
+
+ private native boolean isConstructor(long pointer);
+
+ /**
+ * Is this a selector sort?
+ * @return true if the sort is a selector sort
+ */
+ public boolean isSelector()
+ {
+ return isSelector(pointer);
+ }
+
+ private native boolean isSelector(long pointer);
+
+ /**
+ * Is this a tester sort?
+ * @return true if the sort is a tester sort
+ */
+ public boolean isTester()
+ {
+ return isTester(pointer);
+ }
+
+ private native boolean isTester(long pointer);
+
+ /**
+ * Is this a datatype updater sort?
+ * @return true if the sort is a datatype updater sort
+ */
+ public boolean isUpdater()
+ {
+ return isUpdater(pointer);
+ }
+
+ private native boolean isUpdater(long pointer);
+
+ /**
+ * Is this a function sort?
+ * @return true if the sort is a function sort
+ */
+ public boolean isFunction()
+ {
+ return isFunction(pointer);
+ }
+
+ private native boolean isFunction(long pointer);
+
+ /**
+ * Is this a predicate sort?
+ * That is, is this a function sort mapping to Boolean? All predicate
+ * sorts are also function sorts.
+ * @return true if the sort is a predicate sort
+ */
+ public boolean isPredicate()
+ {
+ return isPredicate(pointer);
+ }
+
+ private native boolean isPredicate(long pointer);
+
+ /**
+ * Is this a tuple sort?
+ * @return true if the sort is a tuple sort
+ */
+ public boolean isTuple()
+ {
+ return isTuple(pointer);
+ }
+
+ private native boolean isTuple(long pointer);
+
+ /**
+ * Is this a record sort?
+ * @return true if the sort is a record sort
+ */
+ public boolean isRecord()
+ {
+ return isRecord(pointer);
+ }
+
+ private native boolean isRecord(long pointer);
+
+ /**
+ * Is this an array sort?
+ * @return true if the sort is a array sort
+ */
+ public boolean isArray()
+ {
+ return isArray(pointer);
+ }
+
+ private native boolean isArray(long pointer);
+
+ /**
+ * Is this a Set sort?
+ * @return true if the sort is a Set sort
+ */
+ public boolean isSet()
+ {
+ return isSet(pointer);
+ }
+
+ private native boolean isSet(long pointer);
+
+ /**
+ * Is this a Bag sort?
+ * @return true if the sort is a Bag sort
+ */
+ public boolean isBag()
+ {
+ return isBag(pointer);
+ }
+
+ private native boolean isBag(long pointer);
+
+ /**
+ * Is this a Sequence sort?
+ * @return true if the sort is a Sequence sort
+ */
+ public boolean isSequence()
+ {
+ return isSequence(pointer);
+ }
+
+ private native boolean isSequence(long pointer);
+
+ /**
+ * Is this a sort kind?
+ * @return true if this is a sort kind
+ */
+ public boolean isUninterpretedSort()
+ {
+ return isUninterpretedSort(pointer);
+ }
+
+ private native boolean isUninterpretedSort(long pointer);
+
+ /**
+ * Is this a sort constructor kind?
+ * @return true if this is a sort constructor kind
+ */
+ public boolean isSortConstructor()
+ {
+ return isSortConstructor(pointer);
+ }
+
+ private native boolean isSortConstructor(long pointer);
+
+ /**
+ * Is this a first-class sort?
+ * First-class sorts are sorts for which:
+ * (1) we handle equalities between terms of that type, and
+ * (2) they are allowed to be parameters of parametric sorts (e.g. index or
+ * element sorts of arrays).
+ *
+ * Examples of sorts that are not first-class include sort constructor sorts
+ * and regular expression sorts.
+ *
+ * @return true if this is a first-class sort
+ */
+ public boolean isFirstClass()
+ {
+ return isFirstClass(pointer);
+ }
+
+ private native boolean isFirstClass(long pointer);
+
+ /**
+ * Is this a function-LIKE sort?
+ *
+ * Anything function-like except arrays (e.g., datatype selectors) is
+ * considered a function here. Function-like terms can not be the argument
+ * or return value for any term that is function-like.
+ * This is mainly to avoid higher order.
+ *
+ * Note that arrays are explicitly not considered function-like here.
+ *
+ * @return true if this is a function-like sort
+ */
+ public boolean isFunctionLike()
+ {
+ return isFunctionLike(pointer);
+ }
+
+ private native boolean isFunctionLike(long pointer);
+
+ /**
+ * Is this sort a subsort of the given sort?
+ * @return true if this sort is a subsort of s
+ */
+ public boolean isSubsortOf(Sort s)
+ {
+ return isSubsortOf(pointer, s.getPointer());
+ }
+
+ private native boolean isSubsortOf(long pointer, long sortPointer);
+
+ /**
+ * Is this sort comparable to the given sort (i.e., do they share
+ * a common ancestor in the subsort tree)?
+ * @return true if this sort is comparable to s
+ */
+ public boolean isComparableTo(Sort s)
+ {
+ return isComparableTo(pointer, s.getPointer());
+ }
+
+ private native boolean isComparableTo(long pointer, long sortPointer);
+
+ /**
+ * @return the underlying datatype of a datatype sort
+ */
+ public Datatype getDatatype()
+ {
+ long datatypePointer = getDatatype(pointer);
+ return new Datatype(solver, datatypePointer);
+ }
+
+ private native long getDatatype(long pointer);
+
+ /**
+ * Instantiate a parameterized datatype/sort sort.
+ * Create sorts parameter with Solver.mkParamSort().
+ * @param params the list of sort parameters to instantiate with
+ */
+ Sort instantiate(List<Sort> params)
+ {
+ return instantiate(params.toArray(new Sort[0]));
+ }
+
+ /**
+ * Instantiate a parameterized datatype/sort sort.
+ * Create sorts parameter with Solver.mkParamSort().
+ * @param params the list of sort parameters to instantiate with
+ */
+ Sort instantiate(Sort[] params)
+ {
+ long[] paramsPointers = Utils.getPointers(params);
+ long sortPointer = instantiate(pointer, paramsPointers);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long instantiate(long pointer, long[] paramsPointers);
+
+ /**
+ * Substitution of Sorts.
+ * @param sort the subsort to be substituted within this sort.
+ * @param replacement the sort replacing the substituted subsort.
+ */
+ public Sort substitute(Sort sort, Sort replacement)
+ {
+ long sortPointer = substitute(pointer, sort.getPointer(), replacement.getPointer());
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long substitute(long pointer, long sortPointer, long replacementPointer);
+
+ /**
+ * Simultaneous substitution of Sorts.
+ * @param sorts the subsorts to be substituted within this sort.
+ * @param replacements the sort replacing the substituted subsorts.
+ */
+ Sort substitute(Sort[] sorts, Sort[] replacements)
+ {
+ long[] sortPointers = Utils.getPointers(sorts);
+ long[] replacementPointers = Utils.getPointers(sorts);
+ long sortPointer = substitute(pointer, sortPointers, replacementPointers);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long substitute(long pointer, long[] sortPointers, long[] replacementPointers);
+
+ /**
+ * Output a string representation of this sort to a given stream.
+ * @param out the output stream
+ */
+ // TODO: do we need to support this?
+ // void toStream(std::ostream& out)
+
+ /**
+ * @return a string representation of this sort
+ */
+ protected native String toString(long pointer);
+
+ /* Constructor sort ------------------------------------------------------- */
+
+ /**
+ * @return the arity of a constructor sort
+ */
+ public int getConstructorArity()
+ {
+ return getConstructorArity(pointer);
+ }
+
+ private native int getConstructorArity(long pointer);
+
+ /**
+ * @return the domain sorts of a constructor sort
+ */
+ public Sort[] getConstructorDomainSorts()
+ {
+ long[] pointers = getConstructorDomainSorts(pointer);
+ return Utils.getSorts(solver, pointers);
+ }
+
+ private native long[] getConstructorDomainSorts(long pointer);
+
+ /**
+ * @return the codomain sort of a constructor sort
+ */
+ Sort getConstructorCodomainSort()
+ {
+ long sortPointer = getConstructorCodomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getConstructorCodomainSort(long pointer);
+
+ /* Selector sort ------------------------------------------------------- */
+
+ /**
+ * @return the domain sort of a selector sort
+ */
+ public Sort getSelectorDomainSort()
+ {
+ long sortPointer = getSelectorDomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getSelectorDomainSort(long pointer);
+
+ /**
+ * @return the codomain sort of a selector sort
+ */
+ public Sort getSelectorCodomainSort()
+ {
+ long sortPointer = getSelectorCodomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getSelectorCodomainSort(long pointer);
+
+ /* Tester sort ------------------------------------------------------- */
+
+ /**
+ * @return the domain sort of a tester sort
+ */
+ public Sort getTesterDomainSort()
+ {
+ long sortPointer = getTesterDomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getTesterDomainSort(long pointer);
+
+ /**
+ * @return the codomain sort of a tester sort, which is the Boolean sort
+ */
+ public Sort getTesterCodomainSort()
+ {
+ long sortPointer = getTesterCodomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getTesterCodomainSort(long pointer);
+
+ /* Function sort ------------------------------------------------------- */
+
+ /**
+ * @return the arity of a function sort
+ */
+ public int getFunctionArity()
+ {
+ return getFunctionArity(pointer);
+ }
+
+ private native int getFunctionArity(long pointer);
+
+ /**
+ * @return the domain sorts of a function sort
+ */
+ public Sort[] getFunctionDomainSorts()
+ {
+ long[] pointers = getFunctionDomainSorts(pointer);
+ return Utils.getSorts(solver, pointers);
+ }
+
+ private native long[] getFunctionDomainSorts(long pointer);
+
+ /**
+ * @return the codomain sort of a function sort
+ */
+ public Sort getFunctionCodomainSort()
+ {
+ long sortPointer = getFunctionCodomainSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getFunctionCodomainSort(long pointer);
+
+ /* Array sort ---------------------------------------------------------- */
+
+ /**
+ * @return the array index sort of an array sort
+ */
+ public Sort getArrayIndexSort()
+ {
+ long sortPointer = getArrayIndexSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getArrayIndexSort(long pointer);
+
+ /**
+ * @return the array element sort of an array element sort
+ */
+ public Sort getArrayElementSort()
+ {
+ long sortPointer = getArrayElementSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getArrayElementSort(long pointer);
+
+ /* Set sort ------------------------------------------------------------ */
+
+ /**
+ * @return the element sort of a set sort
+ */
+ public Sort getSetElementSort()
+ {
+ long sortPointer = getSetElementSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getSetElementSort(long pointer);
+
+ /* Bag sort ------------------------------------------------------------ */
+
+ /**
+ * @return the element sort of a bag sort
+ */
+ public Sort getBagElementSort()
+ {
+ long sortPointer = getBagElementSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getBagElementSort(long pointer);
+
+ /* Sequence sort ------------------------------------------------------- */
+
+ /**
+ * @return the element sort of a sequence sort
+ */
+ public Sort getSequenceElementSort()
+ {
+ long sortPointer = getSequenceElementSort(pointer);
+ return new Sort(solver, sortPointer);
+ }
+
+ private native long getSequenceElementSort(long pointer);
+
+ /* Uninterpreted sort -------------------------------------------------- */
+
+ /**
+ * @return the name of an uninterpreted sort
+ */
+ public String getUninterpretedSortName()
+ {
+ return getUninterpretedSortName(pointer);
+ }
+
+ private native String getUninterpretedSortName(long pointer);
+
+ /**
+ * @return true if an uninterpreted sort is parameterezied
+ */
+ public boolean isUninterpretedSortParameterized()
+ {
+ return isUninterpretedSortParameterized(pointer);
+ }
+
+ private native boolean isUninterpretedSortParameterized(long pointer);
+
+ /**
+ * @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 ----------------------------------------------- */
+
+ /**
+ * @return the name of a sort constructor sort
+ */
+ public String getSortConstructorName()
+ {
+ return getSortConstructorName(pointer);
+ }
+
+ private native String getSortConstructorName(long pointer);
+
+ /**
+ * @return the arity of a sort constructor sort
+ */
+ public int getSortConstructorArity()
+ {
+ return getSortConstructorArity(pointer);
+ }
+
+ private native int getSortConstructorArity(long pointer);
+
+ /* Bit-vector sort ----------------------------------------------------- */
+
+ /**
+ * @return the bit-width of the bit-vector sort
+ */
+ public int getBVSize()
+ {
+ return getBVSize(pointer);
+ }
+
+ private native int getBVSize(long pointer);
+
+ /* Floating-point sort ------------------------------------------------- */
+
+ /**
+ * @return the bit-width of the exponent of the floating-point sort
+ */
+ public int getFPExponentSize()
+ {
+ return getFPExponentSize(pointer);
+ }
+
+ private native int getFPExponentSize(long pointer);
+
+ /**
+ * @return the width of the significand of the floating-point sort
+ */
+ public int getFPSignificandSize()
+ {
+ return getFPSignificandSize(pointer);
+ }
+
+ private native int getFPSignificandSize(long pointer);
+
+ /* Datatype sort ------------------------------------------------------- */
+
+ /**
+ * @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
+ */
+ public int getDatatypeArity()
+ {
+ return getDatatypeArity(pointer);
+ }
+
+ private native int getDatatypeArity(long pointer);
+
+ /* Tuple sort ---------------------------------------------------------- */
+
+ /**
+ * @return the length of a tuple sort
+ */
+ public int getTupleLength()
+ {
+ return getTupleLength(pointer);
+ }
+
+ private native int getTupleLength(long pointer);
+
+ /**
+ * @return the element sorts of a tuple sort
+ */
+ public Sort[] getTupleSorts()
+ {
+ long[] pointers = getTupleSorts(pointer);
+ return Utils.getSorts(solver, pointers);
+ }
+
+ private native long[] getTupleSorts(long pointer);
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Sort.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class: cvc5_Sort
+ * Method: deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Sort_deletePointer(JNIEnv*,
+ jclass,
+ jlong pointer)
+{
+ delete reinterpret_cast<Sort*>(pointer);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: equals
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_equals(JNIEnv* env,
+ jobject,
+ jlong pointer1,
+ jlong pointer2)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort sort1 = *(reinterpret_cast<Sort*>(pointer1));
+ Sort sort2 = *(reinterpret_cast<Sort*>(pointer2));
+ return static_cast<jboolean>((sort1 == sort2));
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: compareTo
+ * Signature: (JJ)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_compareTo(JNIEnv* env,
+ jobject,
+ jlong pointer1,
+ jlong pointer2)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* sort1 = reinterpret_cast<Sort*>(pointer1);
+ Sort* sort2 = reinterpret_cast<Sort*>(pointer2);
+ if (*sort1 < *sort2)
+ {
+ return static_cast<jint>(-1);
+ }
+ if (*sort1 == *sort2)
+ {
+ return 0;
+ }
+ return static_cast<jint>(1);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isNull(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isNull());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isBoolean
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBoolean(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isBoolean());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isInteger
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isInteger(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isInteger());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isReal
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isReal(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isReal());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isString
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isString(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isString());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isRegExp
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRegExp(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isRegExp());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isRoundingMode
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRoundingMode(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isRoundingMode());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isBitVector
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBitVector(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isBitVector());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isFloatingPoint
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFloatingPoint(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPoint());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isDatatype
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isDatatype(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isDatatype());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isParametricDatatype
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isParametricDatatype(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isParametricDatatype());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isConstructor
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isConstructor(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isConstructor());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isSelector
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSelector(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isSelector());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isTester
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTester(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isTester());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isUpdater
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUpdater(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isUpdater());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isFunction
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunction(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isFunction());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isPredicate
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isPredicate(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isPredicate());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isTuple
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTuple(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isTuple());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isRecord
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRecord(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isRecord());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isArray
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isArray(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isArray());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isSet
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSet(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isSet());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isBag
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBag(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isBag());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isSequence
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSequence(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isSequence());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isUninterpretedSort
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isUninterpretedSort());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isSortConstructor
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSortConstructor(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isSortConstructor());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isFirstClass
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFirstClass(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isFirstClass());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isFunctionLike
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunctionLike(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isFunctionLike());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isSubsortOf
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSubsortOf(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlong sortPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+ return static_cast<jboolean>(current->isSubsortOf(*sort));
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isComparableTo
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isComparableTo(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlong sortPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+ return static_cast<jboolean>(current->isComparableTo(*sort));
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getDatatype
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getDatatype(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Datatype* retPointer = new Datatype(current->getDatatype());
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: instantiate
+ * Signature: (J[J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_instantiate(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlongArray paramsPointers)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ // get the size of params pointers
+ jsize size = env->GetArrayLength(paramsPointers);
+ // allocate buffer for the long array
+ jlong* buffer = new jlong[size];
+ // copy java array to the buffer
+ env->GetLongArrayRegion(paramsPointers, 0, size, buffer);
+ // copy the terms into a vector
+ std::vector<Sort> params;
+ for (jsize i = 0; i < size; i++)
+ {
+ Sort* sort = reinterpret_cast<Sort*>(buffer[i]);
+ params.push_back(*sort);
+ }
+ // free the buffer memory
+ delete[] buffer;
+
+ Sort* retPointer = new Sort(current->instantiate(params));
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: substitute
+ * Signature: (JJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_substitute__JJJ(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlong sortPointer,
+ jlong replacementPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+ Sort* replacement = reinterpret_cast<Sort*>(replacementPointer);
+ Sort* retPointer = new Sort(current->substitute(*sort, *replacement));
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: substitute
+ * Signature: (J[J[J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_Sort_substitute__J_3J_3J(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlongArray sortPointers,
+ jlongArray replacementPointers)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ // get the size of pointers
+ jsize sortsSize = env->GetArrayLength(sortPointers);
+ jsize replacementsSize = env->GetArrayLength(replacementPointers);
+ // allocate buffer for the long array
+ jlong* sortsBuffer = new jlong[sortsSize];
+ jlong* replacementsBuffer = new jlong[replacementsSize];
+ // copy java array to the buffer
+ env->GetLongArrayRegion(sortPointers, 0, sortsSize, sortsBuffer);
+ env->GetLongArrayRegion(
+ replacementPointers, 0, replacementsSize, replacementsBuffer);
+ // copy the terms into a vector
+ std::vector<Sort> sorts;
+ for (jsize i = 0; i < sortsSize; i++)
+ {
+ Sort* sort = reinterpret_cast<Sort*>(sortsBuffer[i]);
+ sorts.push_back(*sort);
+ }
+
+ std::vector<Sort> replacements;
+ for (jsize i = 0; i < replacementsSize; i++)
+ {
+ Sort* sort = reinterpret_cast<Sort*>(replacementsBuffer[i]);
+ replacements.push_back(*sort);
+ }
+
+ // free the buffer memory
+ delete[] sortsBuffer;
+ delete[] replacementsBuffer;
+
+ Sort* retPointer = new Sort(current->substitute(sorts, replacements));
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Sort_toString(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return env->NewStringUTF(current->toString().c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getConstructorArity
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getConstructorArity(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getConstructorArity());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getConstructorDomainSorts
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL
+Java_cvc5_Sort_getConstructorDomainSorts(JNIEnv* env, jobject, jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ std::vector<Sort> sorts = current->getConstructorDomainSorts();
+ std::vector<long> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = (long)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: cvc5_Sort
+ * Method: getConstructorCodomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getConstructorCodomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getConstructorCodomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getSelectorDomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorDomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getSelectorDomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getSelectorCodomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorCodomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getSelectorCodomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getTesterDomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterDomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getTesterDomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getTesterCodomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterCodomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getTesterCodomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getFunctionArity
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getFunctionArity(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getFunctionArity());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getFunctionDomainSorts
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL
+Java_cvc5_Sort_getFunctionDomainSorts(JNIEnv* env, jobject, jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ std::vector<Sort> sorts = current->getFunctionDomainSorts();
+ std::vector<long> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = (long)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: cvc5_Sort
+ * Method: getFunctionCodomainSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getFunctionCodomainSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getFunctionCodomainSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getArrayIndexSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayIndexSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getArrayIndexSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getArrayElementSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayElementSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getArrayElementSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getSetElementSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSetElementSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getSetElementSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getBagElementSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getBagElementSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getBagElementSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getSequenceElementSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSequenceElementSort(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ Sort* retPointer = new Sort(current->getSequenceElementSort());
+ return (jlong)retPointer;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getUninterpretedSortName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Sort_getUninterpretedSortName(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return env->NewStringUTF(current->getUninterpretedSortName().c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: isUninterpretedSortParameterized
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSortParameterized(
+ JNIEnv* env, jobject, jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jboolean>(current->isUninterpretedSortParameterized());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getUninterpretedSortParamSorts
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_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<long> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = (long)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: cvc5_Sort
+ * Method: getSortConstructorName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Sort_getSortConstructorName(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return env->NewStringUTF(current->getSortConstructorName().c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getSortConstructorArity
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getSortConstructorArity());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getBVSize
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getBVSize());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getFPExponentSize
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getFPExponentSize());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getFPSignificandSize
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getFPSignificandSize());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getDatatypeParamSorts
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_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<long> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = (long)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: cvc5_Sort
+ * Method: getDatatypeArity
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getDatatypeArity(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getDatatypeArity());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getTupleLength
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getTupleLength(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ return static_cast<jint>(current->getTupleLength());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Sort
+ * Method: getTupleSorts
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getTupleSorts(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Sort* current = reinterpret_cast<Sort*>(pointer);
+ std::vector<Sort> sorts = current->getTupleSorts();
+ std::vector<long> sortPointers(sorts.size());
+ for (size_t i = 0; i < sorts.size(); i++)
+ {
+ sortPointers[i] = (long)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);
+}
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Andrew Reynolds, Mathias Preiner, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the Java API functions.
+ */
+
+package cvc5;
+
+import static cvc5.Kind.*;
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Iterator;
+import java.util.List;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class SortTest
+{
+ private Solver d_solver;
+
+ @BeforeEach void setUp()
+ {
+ d_solver = new Solver();
+ }
+
+ Sort create_datatype_sort() throws CVC5ApiException
+ {
+ DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ cons.addSelector("head", d_solver.getIntegerSort());
+ cons.addSelectorSelf("tail");
+ dtypeSpec.addConstructor(cons);
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+ dtypeSpec.addConstructor(nil);
+ return d_solver.mkDatatypeSort(dtypeSpec);
+ }
+
+ Sort create_param_datatype_sort() throws CVC5ApiException
+ {
+ 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);
+ return d_solver.mkDatatypeSort(paramDtypeSpec);
+ }
+
+ @Test void operators_comparison()
+ {
+ assertDoesNotThrow(() -> d_solver.getIntegerSort() == d_solver.getNullSort());
+ assertDoesNotThrow(() -> d_solver.getIntegerSort() != d_solver.getNullSort());
+ assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort()));
+ }
+
+ @Test void isBoolean()
+ {
+ assertTrue(d_solver.getBooleanSort().isBoolean());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isBoolean());
+ }
+
+ @Test void isInteger()
+ {
+ assertTrue(d_solver.getIntegerSort().isInteger());
+ assertTrue(!d_solver.getRealSort().isInteger());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isInteger());
+ }
+
+ @Test void isReal()
+ {
+ assertTrue(d_solver.getRealSort().isReal());
+ assertTrue(!d_solver.getIntegerSort().isReal());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isReal());
+ }
+
+ @Test void isString()
+ {
+ assertTrue(d_solver.getStringSort().isString());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isString());
+ }
+
+ @Test void isRegExp()
+ {
+ assertTrue(d_solver.getRegExpSort().isRegExp());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isRegExp());
+ }
+
+ @Test void isRoundingMode() throws CVC5ApiException
+ {
+ if (d_solver.supportsFloatingPoint())
+ {
+ assertTrue(d_solver.getRoundingModeSort().isRoundingMode());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isRoundingMode());
+ }
+ }
+
+ @Test void isBitVector() throws CVC5ApiException
+ {
+ assertTrue(d_solver.mkBitVectorSort(8).isBitVector());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isBitVector());
+ }
+
+ @Test void isFloatingPoint() throws CVC5ApiException
+ {
+ if (d_solver.supportsFloatingPoint())
+ {
+ assertTrue(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isFloatingPoint());
+ }
+ }
+
+ @Test void isDatatype() throws CVC5ApiException
+ {
+ Sort dt_sort = create_datatype_sort();
+ assertTrue(dt_sort.isDatatype());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isDatatype());
+ }
+
+ @Test void isParametricDatatype() throws CVC5ApiException
+ {
+ Sort param_dt_sort = create_param_datatype_sort();
+ assertTrue(param_dt_sort.isParametricDatatype());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isParametricDatatype());
+ }
+
+ @Test void isConstructor() throws CVC5ApiException
+ {
+ Sort dt_sort = create_datatype_sort();
+ Datatype dt = dt_sort.getDatatype();
+ Sort cons_sort = dt.getConstructor(0).getConstructorTerm().getSort();
+ assertTrue(cons_sort.isConstructor());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isConstructor());
+ }
+
+ @Test void isSelector() throws CVC5ApiException
+ {
+ Sort dt_sort = create_datatype_sort();
+ Datatype dt = dt_sort.getDatatype();
+ Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort();
+ assertTrue(cons_sort.isSelector());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isSelector());
+ }
+
+ @Test void isTester() throws CVC5ApiException
+ {
+ Sort dt_sort = create_datatype_sort();
+ Datatype dt = dt_sort.getDatatype();
+ Sort cons_sort = dt.getConstructor(0).getTesterTerm().getSort();
+ assertTrue(cons_sort.isTester());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isTester());
+ }
+
+ @Test void isFunction()
+ {
+ Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort());
+ assertTrue(fun_sort.isFunction());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isFunction());
+ }
+
+ @Test void isPredicate()
+ {
+ Sort pred_sort = d_solver.mkPredicateSort(new Sort[] {d_solver.getRealSort()});
+ assertTrue(pred_sort.isPredicate());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isPredicate());
+ }
+
+ @Test void isTuple()
+ {
+ Sort tup_sort = d_solver.mkTupleSort(new Sort[] {d_solver.getRealSort()});
+ assertTrue(tup_sort.isTuple());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isTuple());
+ }
+
+ @Test void isRecord()
+ {
+ Sort rec_sort =
+ d_solver.mkRecordSort(new Pair[] {new Pair<String, Sort>("asdf", d_solver.getRealSort())});
+ assertTrue(rec_sort.isRecord());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isRecord());
+ }
+
+ @Test void isArray()
+ {
+ Sort arr_sort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getIntegerSort());
+ assertTrue(arr_sort.isArray());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isArray());
+ }
+
+ @Test void isSet()
+ {
+ Sort set_sort = d_solver.mkSetSort(d_solver.getRealSort());
+ assertTrue(set_sort.isSet());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isSet());
+ }
+
+ @Test void isBag()
+ {
+ Sort bag_sort = d_solver.mkBagSort(d_solver.getRealSort());
+ assertTrue(bag_sort.isBag());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isBag());
+ }
+
+ @Test void isSequence()
+ {
+ Sort seq_sort = d_solver.mkSequenceSort(d_solver.getRealSort());
+ assertTrue(seq_sort.isSequence());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isSequence());
+ }
+
+ @Test void isUninterpreted()
+ {
+ Sort un_sort = d_solver.mkUninterpretedSort("asdf");
+ assertTrue(un_sort.isUninterpretedSort());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSort());
+ }
+
+ @Test void isSortConstructor() throws CVC5ApiException
+ {
+ Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1);
+ assertTrue(sc_sort.isSortConstructor());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isSortConstructor());
+ }
+
+ @Test void isFirstClass()
+ {
+ Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort());
+ assertTrue(d_solver.getIntegerSort().isFirstClass());
+ assertTrue(fun_sort.isFirstClass());
+ Sort reSort = d_solver.getRegExpSort();
+ assertFalse(reSort.isFirstClass());
+ assertDoesNotThrow(() -> d_solver.getNullSort().isFirstClass());
+ }
+
+ @Test void isFunctionLike() throws CVC5ApiException
+ {
+ Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort());
+ assertFalse(d_solver.getIntegerSort().isFunctionLike());
+ assertTrue(fun_sort.isFunctionLike());
+
+ Sort dt_sort = create_datatype_sort();
+ Datatype dt = dt_sort.getDatatype();
+ Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort();
+ assertTrue(cons_sort.isFunctionLike());
+
+ assertDoesNotThrow(() -> d_solver.getNullSort().isFunctionLike());
+ }
+
+ @Test void isSubsortOf()
+ {
+ assertTrue(d_solver.getIntegerSort().isSubsortOf(d_solver.getIntegerSort()));
+ assertTrue(d_solver.getIntegerSort().isSubsortOf(d_solver.getRealSort()));
+ assertFalse(d_solver.getIntegerSort().isSubsortOf(d_solver.getBooleanSort()));
+ assertDoesNotThrow(() -> d_solver.getNullSort().isSubsortOf(d_solver.getNullSort()));
+ }
+
+ @Test void isComparableTo()
+ {
+ assertTrue(d_solver.getIntegerSort().isComparableTo(d_solver.getIntegerSort()));
+ assertTrue(d_solver.getIntegerSort().isComparableTo(d_solver.getRealSort()));
+ assertFalse(d_solver.getIntegerSort().isComparableTo(d_solver.getBooleanSort()));
+ assertDoesNotThrow(() -> d_solver.getNullSort().isComparableTo(d_solver.getNullSort()));
+ }
+
+ @Test void getDatatype() throws CVC5ApiException
+ {
+ Sort dtypeSort = create_datatype_sort();
+ assertDoesNotThrow(() -> dtypeSort.getDatatype());
+ // create bv sort, check should fail
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getDatatype());
+ }
+
+ @Test void datatypeSorts() throws CVC5ApiException
+ {
+ Sort intSort = d_solver.getIntegerSort();
+ Sort dtypeSort = create_datatype_sort();
+ Datatype dt = dtypeSort.getDatatype();
+ assertFalse(dtypeSort.isConstructor());
+ assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorCodomainSort());
+ assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorDomainSorts());
+ assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorArity());
+
+ // get constructor
+ DatatypeConstructor dcons = dt.getConstructor(0);
+ Term consTerm = dcons.getConstructorTerm();
+ Sort consSort = consTerm.getSort();
+ assertTrue(consSort.isConstructor());
+ assertFalse(consSort.isTester());
+ assertFalse(consSort.isSelector());
+ assertEquals(consSort.getConstructorArity(), 2);
+ Sort[] consDomSorts = consSort.getConstructorDomainSorts();
+ assertEquals(consDomSorts[0], intSort);
+ assertEquals(consDomSorts[1], dtypeSort);
+ assertEquals(consSort.getConstructorCodomainSort(), dtypeSort);
+
+ // get tester
+ Term isConsTerm = dcons.getTesterTerm();
+ assertTrue(isConsTerm.getSort().isTester());
+ assertEquals(isConsTerm.getSort().getTesterDomainSort(), dtypeSort);
+ Sort booleanSort = d_solver.getBooleanSort();
+ assertEquals(isConsTerm.getSort().getTesterCodomainSort(), booleanSort);
+ assertThrows(CVC5ApiException.class, () -> booleanSort.getTesterDomainSort());
+ assertThrows(CVC5ApiException.class, () -> booleanSort.getTesterCodomainSort());
+
+ // get selector
+ DatatypeSelector dselTail = dcons.getSelector(1);
+ Term tailTerm = dselTail.getSelectorTerm();
+ assertTrue(tailTerm.getSort().isSelector());
+ assertEquals(tailTerm.getSort().getSelectorDomainSort(), dtypeSort);
+ assertEquals(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort);
+ assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorDomainSort());
+ assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorCodomainSort());
+ }
+
+ @Test void instantiate() throws CVC5ApiException
+ {
+ // instantiate parametric datatype, check should not fail
+ Sort paramDtypeSort = create_param_datatype_sort();
+ assertDoesNotThrow(() -> paramDtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()}));
+ // instantiate 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.instantiate(new Sort[] {d_solver.getIntegerSort()}));
+ }
+
+ @Test void getFunctionArity() throws CVC5ApiException
+ {
+ Sort funSort =
+ d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+ assertDoesNotThrow(() -> funSort.getFunctionArity());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionArity());
+ }
+
+ @Test void getFunctionDomainSorts() throws CVC5ApiException
+ {
+ Sort funSort =
+ d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+ assertDoesNotThrow(() -> funSort.getFunctionDomainSorts());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionDomainSorts());
+ }
+
+ @Test void getFunctionCodomainSort() throws CVC5ApiException
+ {
+ Sort funSort =
+ d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+ assertDoesNotThrow(() -> funSort.getFunctionCodomainSort());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionCodomainSort());
+ }
+
+ @Test void getArrayIndexSort() throws CVC5ApiException
+ {
+ Sort elementSort = d_solver.mkBitVectorSort(32);
+ Sort indexSort = d_solver.mkBitVectorSort(32);
+ Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+ assertDoesNotThrow(() -> arraySort.getArrayIndexSort());
+ assertThrows(CVC5ApiException.class, () -> indexSort.getArrayIndexSort());
+ }
+
+ @Test void getArrayElementSort() throws CVC5ApiException
+ {
+ Sort elementSort = d_solver.mkBitVectorSort(32);
+ Sort indexSort = d_solver.mkBitVectorSort(32);
+ Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+ assertDoesNotThrow(() -> arraySort.getArrayElementSort());
+ assertThrows(CVC5ApiException.class, () -> indexSort.getArrayElementSort());
+ }
+
+ @Test void getSetElementSort() throws CVC5ApiException
+ {
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ assertDoesNotThrow(() -> setSort.getSetElementSort());
+ Sort elementSort = setSort.getSetElementSort();
+ assertEquals(elementSort, d_solver.getIntegerSort());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getSetElementSort());
+ }
+
+ @Test void getBagElementSort() throws CVC5ApiException
+ {
+ Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
+ assertDoesNotThrow(() -> bagSort.getBagElementSort());
+ Sort elementSort = bagSort.getBagElementSort();
+ assertEquals(elementSort, d_solver.getIntegerSort());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getBagElementSort());
+ }
+
+ @Test void getSequenceElementSort() throws CVC5ApiException
+ {
+ Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
+ assertTrue(seqSort.isSequence());
+ assertDoesNotThrow(() -> seqSort.getSequenceElementSort());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertFalse(bvSort.isSequence());
+ assertThrows(CVC5ApiException.class, () -> bvSort.getSequenceElementSort());
+ }
+
+ @Test void getUninterpretedSortName() throws CVC5ApiException
+ {
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ assertDoesNotThrow(() -> uSort.getUninterpretedSortName());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortName());
+ }
+
+ @Test void isUninterpretedSortParameterized() throws CVC5ApiException
+ {
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ assertFalse(uSort.isUninterpretedSortParameterized());
+ Sort sSort = d_solver.mkSortConstructorSort("s", 1);
+ Sort siSort = sSort.instantiate(new Sort[] {uSort});
+ assertTrue(siSort.isUninterpretedSortParameterized());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.isUninterpretedSortParameterized());
+ }
+
+ @Test void getUninterpretedSortParamSorts() throws CVC5ApiException
+ {
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ assertDoesNotThrow(() -> uSort.getUninterpretedSortParamSorts());
+ Sort sSort = d_solver.mkSortConstructorSort("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.mkSortConstructorSort("s", 2);
+ assertDoesNotThrow(() -> sSort.getSortConstructorName());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorName());
+ }
+
+ @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException
+ {
+ Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+ assertDoesNotThrow(() -> sSort.getSortConstructorArity());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity());
+ }
+
+ @Test void getBVSize() throws CVC5ApiException
+ {
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertDoesNotThrow(() -> bvSort.getBVSize());
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ assertThrows(CVC5ApiException.class, () -> setSort.getBVSize());
+ }
+
+ @Test void getFPExponentSize() throws CVC5ApiException
+ {
+ if (d_solver.supportsFloatingPoint())
+ {
+ Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+ assertDoesNotThrow(() -> fpSort.getFPExponentSize());
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize());
+ }
+ }
+
+ @Test void getFPSignificandSize() throws CVC5ApiException
+ {
+ if (d_solver.supportsFloatingPoint())
+ {
+ Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+ assertDoesNotThrow(() -> fpSort.getFPSignificandSize());
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize());
+ }
+ }
+
+ @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
+ 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);
+ assertDoesNotThrow(() -> dtypeSort.getDatatypeArity());
+ // create bv sort, check should fail
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getDatatypeArity());
+ }
+
+ @Test void getTupleLength() throws CVC5ApiException
+ {
+ Sort tupleSort =
+ d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+ assertDoesNotThrow(() -> tupleSort.getTupleLength());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getTupleLength());
+ }
+
+ @Test void getTupleSorts() throws CVC5ApiException
+ {
+ Sort tupleSort =
+ d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+ assertDoesNotThrow(() -> tupleSort.getTupleSorts());
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ assertThrows(CVC5ApiException.class, () -> bvSort.getTupleSorts());
+ }
+
+ @Test void sortCompare() throws CVC5ApiException
+ {
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort intSort = d_solver.getIntegerSort();
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ Sort bvSort2 = d_solver.mkBitVectorSort(32);
+ assertTrue(bvSort.compareTo(bvSort2) >= 0);
+ assertTrue(bvSort.compareTo(bvSort2) <= 0);
+ assertTrue(intSort.compareTo(boolSort) > 0 != intSort.compareTo(boolSort) < 0);
+ assertTrue((intSort.compareTo(bvSort) > 0 || intSort.equals(bvSort))
+ == (intSort.compareTo(bvSort) >= 0));
+ }
+
+ @Test void sortSubtyping()
+ {
+ Sort intSort = d_solver.getIntegerSort();
+ Sort realSort = d_solver.getRealSort();
+ assertTrue(intSort.isSubsortOf(realSort));
+ assertFalse(realSort.isSubsortOf(intSort));
+ assertTrue(intSort.isComparableTo(realSort));
+ assertTrue(realSort.isComparableTo(intSort));
+
+ Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
+ Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
+ assertFalse(arraySortII.isComparableTo(intSort));
+ // we do not support subtyping for arrays
+ assertFalse(arraySortII.isComparableTo(arraySortIR));
+
+ Sort setSortI = d_solver.mkSetSort(intSort);
+ Sort setSortR = d_solver.mkSetSort(realSort);
+ // we don't support subtyping for sets
+ assertFalse(setSortI.isComparableTo(setSortR));
+ assertFalse(setSortI.isSubsortOf(setSortR));
+ assertFalse(setSortR.isComparableTo(setSortI));
+ assertFalse(setSortR.isSubsortOf(setSortI));
+ }
+
+ @Test void sortScopedToString() throws CVC5ApiException
+ {
+ String name = "uninterp-sort";
+ Sort bvsort8 = d_solver.mkBitVectorSort(8);
+ Sort uninterp_sort = d_solver.mkUninterpretedSort(name);
+ assertEquals(bvsort8.toString(), "(_ BitVec 8)");
+ assertEquals(uninterp_sort.toString(), name);
+ Solver solver2;
+ assertEquals(bvsort8.toString(), "(_ BitVec 8)");
+ assertEquals(uninterp_sort.toString(), name);
+ }
+}
projects / cvc5.git / commitdiff