From: mudathirmahgoub Date: Wed, 29 Sep 2021 00:30:24 +0000 (-0500) Subject: Add Sort.java to the java API (#6382) X-Git-Tag: cvc5-1.0.0~1165 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d84c92f254c722c0307267a866a5a3e8430bcd35;p=cvc5.git Add Sort.java to the java API (#6382) This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api. --- diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java new file mode 100644 index 000000000..a52a249f8 --- /dev/null +++ b/src/api/java/cvc5/Sort.java @@ -0,0 +1,803 @@ +/****************************************************************************** + * 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 +{ + // 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 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); +} diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp new file mode 100644 index 000000000..a2754f032 --- /dev/null +++ b/src/api/java/jni/cvc5_Sort.cpp @@ -0,0 +1,1098 @@ +/****************************************************************************** + * 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(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(pointer1)); + Sort sort2 = *(reinterpret_cast(pointer2)); + return static_cast((sort1 == sort2)); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer1); + Sort* sort2 = reinterpret_cast(pointer2); + if (*sort1 < *sort2) + { + return static_cast(-1); + } + if (*sort1 == *sort2) + { + return 0; + } + return static_cast(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(pointer); + return static_cast(current->isNull()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isBoolean()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isInteger()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isReal()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isString()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isRegExp()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isRoundingMode()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isBitVector()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isFloatingPoint()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isDatatype()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isParametricDatatype()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isConstructor()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isSelector()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isTester()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isUpdater()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isFunction()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isPredicate()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isTuple()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isRecord()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isArray()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isSet()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isBag()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isSequence()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isUninterpretedSort()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isSortConstructor()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isFirstClass()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isFunctionLike()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + Sort* sort = reinterpret_cast(sortPointer); + return static_cast(current->isSubsortOf(*sort)); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + Sort* sort = reinterpret_cast(sortPointer); + return static_cast(current->isComparableTo(*sort)); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + Datatype* retPointer = new Datatype(current->getDatatype()); + return reinterpret_cast(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(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 params; + for (jsize i = 0; i < size; i++) + { + Sort* sort = reinterpret_cast(buffer[i]); + params.push_back(*sort); + } + // free the buffer memory + delete[] buffer; + + Sort* retPointer = new Sort(current->instantiate(params)); + return reinterpret_cast(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(pointer); + Sort* sort = reinterpret_cast(sortPointer); + Sort* replacement = reinterpret_cast(replacementPointer); + Sort* retPointer = new Sort(current->substitute(*sort, *replacement)); + return reinterpret_cast(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(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 sorts; + for (jsize i = 0; i < sortsSize; i++) + { + Sort* sort = reinterpret_cast(sortsBuffer[i]); + sorts.push_back(*sort); + } + + std::vector replacements; + for (jsize i = 0; i < replacementsSize; i++) + { + Sort* sort = reinterpret_cast(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(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(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(pointer); + return static_cast(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(pointer); + std::vector sorts = current->getConstructorDomainSorts(); + std::vector 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(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(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(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(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(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(pointer); + return static_cast(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(pointer); + std::vector sorts = current->getFunctionDomainSorts(); + std::vector 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(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(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(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(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(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(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(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(pointer); + return static_cast(current->isUninterpretedSortParameterized()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + std::vector sorts = current->getUninterpretedSortParamSorts(); + std::vector 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(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(pointer); + return static_cast(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(pointer); + return static_cast(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(pointer); + return static_cast(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(pointer); + return static_cast(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(pointer); + std::vector sorts = current->getDatatypeParamSorts(); + std::vector 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(pointer); + return static_cast(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(pointer); + return static_cast(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(pointer); + std::vector sorts = current->getTupleSorts(); + std::vector 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); +} diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java new file mode 100644 index 000000000..a937e4dfc --- /dev/null +++ b/test/unit/api/java/cvc5/SortTest.java @@ -0,0 +1,602 @@ +/****************************************************************************** + * 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("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); + } +}