Add Sort.java to the java API (#6382)

This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.

3 files changed, 2503 insertions, 0 deletions

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<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);
+}
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<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);
+}
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<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);
+  }
+}