Add Term.java to the Java API (#6330)

This commit adds `Term.java`, `TermTest.java`, and `cvc5_Term.cpp` to the Java API. 

4 files changed, 1884 insertions, 1 deletions

diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 53ea46f46..d1e818f30 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -91,7 +91,9 @@ message(STATUS "JAVA_INCLUDE_PATH    : ${JAVA_INCLUDE_PATH}")
 message(STATUS "JAVA_INCLUDE_PATH2   : ${JAVA_INCLUDE_PATH2}")
 message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}")
 
-add_library(cvc5jni SHARED jni/cvc5_Solver.cpp)
+add_library(cvc5jni SHARED
+  jni/cvc5_Solver.cpp
+)
 add_dependencies(cvc5jni generate-jni-headers)
 
 target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS})
diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java
new file mode 100644
index 000000000..276c288d1
--- /dev/null
+++ b/src/api/java/cvc5/Term.java
@@ -0,0 +1,442 @@
+/******************************************************************************
+ * 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.Iterator;
+import java.util.List;
+import java.util.NoSuchElementException;
+
+public class Term
+    extends AbstractPointer implements Comparable<Term>, Iterable<Term> {
+  // region construction and destruction
+  Term(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
+
+  /**
+   * Syntactic equality operator.
+   * Return true if both terms are syntactically identical.
+   * Both terms must belong to the same solver object.
+   *
+   * @param t the term to compare to for equality
+   * @return true if the terms are equal
+   */
+  @Override
+  public boolean equals(Object t) {
+    if (this == t)
+      return true;
+    if (t == null || getClass() != t.getClass())
+      return false;
+    Term term = (Term) t;
+    if (this.pointer == term.pointer) {
+      return true;
+    }
+    return equals(pointer, term.getPointer());
+  }
+
+  private native boolean equals(long pointer1, long pointer2);
+
+  /**
+   * Comparison for ordering on terms.
+   *
+   * @param t the term to compare to
+   * @return a negative integer, zero, or a positive integer as this term
+   * is less than, equal to, or greater than the specified term.
+   */
+  @Override
+  public int compareTo(Term t) {
+    return this.compareTo(pointer, t.getPointer());
+  }
+
+  private native int compareTo(long pointer1, long pointer2);
+
+  /**
+   * @return the number of children of this term
+   */
+  public int getNumChildren() {
+    return getNumChildren(pointer);
+  }
+
+  private native int getNumChildren(long pointer);
+
+  /**
+   * Get the child term at a given index.
+   *
+   * @param index the index of the child term to return
+   * @return the child term with the given index
+   */
+  public Term getChild(int index) throws CVC5ApiException {
+    Utils.validateUnsigned(index, "index");
+    long termPointer = getChild(pointer, index);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getChild(long pointer, int index);
+
+  /**
+   * @return the id of this term
+   */
+  public long getId() {
+    return getId(pointer);
+  }
+
+  private native long getId(long pointer);
+
+  /**
+   * @return the kind of this term
+   */
+  public Kind getKind() throws CVC5ApiException {
+    int value = getKind(pointer);
+    return Kind.fromInt(value);
+  }
+
+  private native int getKind(long pointer);
+
+  /**
+   * @return the sort of this term
+   */
+  public Sort getSort() {
+    long sortPointer = getSort(pointer);
+    return new Sort(solver, sortPointer);
+  }
+
+  private native long getSort(long pointer);
+
+  /**
+   * @return the result of replacing 'term' by 'replacement' in this term
+   */
+  public Term substitute(Term term, Term replacement) {
+    long termPointer =
+        substitute(pointer, term.getPointer(), replacement.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long substitute(
+      long pointer, long termPointer, long replacementPointer);
+
+  /**
+   * @return the result of simultaneously replacing 'terms' by 'replacements'
+   * in this term
+   */
+  public Term substitute(List<Term> terms, List<Term> replacements) {
+    return substitute(
+        terms.toArray(new Term[0]), replacements.toArray(new Term[0]));
+  }
+
+  /**
+   * @return the result of simultaneously replacing 'terms' by 'replacements'
+   * in this term
+   */
+  public Term substitute(Term[] terms, Term[] replacements) {
+    long[] termPointers = new long[terms.length];
+    for (int i = 0; i < termPointers.length; i++) {
+      termPointers[i] = terms[i].getPointer();
+    }
+    long[] replacementPointers = new long[replacements.length];
+    for (int i = 0; i < replacements.length; i++) {
+      replacementPointers[i] = replacements[i].getPointer();
+    }
+
+    long termPointer = substitute(pointer, termPointers, replacementPointers);
+    return new Term(solver, termPointer);
+  }
+
+  private native long substitute(
+      long pointer, long[] termPointers, long[] replacementPointers);
+
+  /**
+   * @return true iff this term has an operator
+   */
+  public boolean hasOp() {
+    return hasOp(pointer);
+  }
+
+  private native boolean hasOp(long pointer);
+
+  /**
+   * @return the Op used to create this term
+   * Note: This is safe to call when hasOp() returns true.
+   */
+  public Op getOp() {
+    long opPointer = getOp(pointer);
+    return new Op(solver, opPointer);
+  }
+
+  private native long getOp(long pointer);
+
+  /**
+   * @return true if this Term is a null term
+   */
+  public boolean isNull() {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * Return the base (element stored at all indices) of a constant array
+   * throws an exception if the kind is not CONST_ARRAY
+   *
+   * @return the base value
+   */
+  public Term getConstArrayBase() {
+    long termPointer = getConstArrayBase(pointer);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getConstArrayBase(long pointer);
+
+  /**
+   * Return the elements of a constant sequence
+   * throws an exception if the kind is not CONST_SEQUENCE
+   *
+   * @return the elements of the constant sequence.
+   */
+  public Term[] getConstSequenceElements() {
+    long[] termPointers = getConstSequenceElements(pointer);
+    Term[] terms = new Term[termPointers.length];
+    for (int i = 0; i < termPointers.length; i++) {
+      terms[i] = new Term(solver, termPointers[i]);
+    }
+
+    return terms;
+  }
+
+  private native long[] getConstSequenceElements(long pointer);
+
+  /**
+   * Boolean negation.
+   *
+   * @return the Boolean negation of this term
+   */
+  public Term notTerm() {
+    long termPointer = notTerm(pointer);
+    return new Term(solver, termPointer);
+  }
+
+  private native long notTerm(long pointer);
+
+  /**
+   * Boolean and.
+   *
+   * @param t a Boolean term
+   * @return the conjunction of this term and the given term
+   */
+  public Term andTerm(Term t) {
+    long termPointer = andTerm(pointer, t.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long andTerm(long pointer, long termPointer);
+
+  /**
+   * Boolean or.
+   *
+   * @param t a Boolean term
+   * @return the disjunction of this term and the given term
+   */
+  public Term orTerm(Term t) {
+    long termPointer = orTerm(pointer, t.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long orTerm(long pointer, long termPointer);
+
+  /**
+   * Boolean exclusive or.
+   *
+   * @param t a Boolean term
+   * @return the exclusive disjunction of this term and the given term
+   */
+  public Term xorTerm(Term t) {
+    long termPointer = xorTerm(pointer, t.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long xorTerm(long pointer, long termPointer);
+
+  /**
+   * Equality.
+   *
+   * @param t a Boolean term
+   * @return the Boolean equivalence of this term and the given term
+   */
+  public Term eqTerm(Term t) {
+    long termPointer = eqTerm(pointer, t.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long eqTerm(long pointer, long termPointer);
+
+  /**
+   * Boolean implication.
+   *
+   * @param t a Boolean term
+   * @return the implication of this term and the given term
+   */
+  public Term impTerm(Term t) {
+    long termPointer = impTerm(pointer, t.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long impTerm(long pointer, long termPointer);
+
+  /**
+   * If-then-else with this term as the Boolean condition.
+   *
+   * @param thenTerm the 'then' term
+   * @param elseTerm the 'else' term
+   * @return the if-then-else term with this term as the Boolean condition
+   */
+  public Term iteTerm(Term thenTerm, Term elseTerm) {
+    long termPointer =
+        iteTerm(pointer, thenTerm.getPointer(), elseTerm.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long iteTerm(long pointer, long thenPointer, long elsePointer);
+
+  /**
+   * @return a string representation of this term
+   */
+  protected native String toString(long pointer);
+
+  /**
+   * @return true if the term is an integer that fits within a Java integer.
+   */
+  public boolean isInt() {
+    return isInt(pointer);
+  }
+
+  private native boolean isInt(long pointer);
+
+  /**
+   * @return the stored integer as an int.
+   * Note: Asserts isInt().
+   */
+  public int getInt() {
+    return getInt(pointer);
+  }
+
+  private native int getInt(long pointer);
+
+  /**
+   * @return true if the term is an integer that fits within a Java long.
+   */
+  public boolean isLong() {
+    return isLong(pointer);
+  }
+
+  private native boolean isLong(long pointer);
+
+  /**
+   * @return the stored integer as a long.
+   * Note: Asserts isLong().
+   */
+  public long getLong() {
+    return getLong(pointer);
+  }
+
+  private native long getLong(long pointer);
+
+  /**
+   * @return true if the term is an integer.
+   */
+  public boolean isInteger() {
+    return isInteger(pointer);
+  }
+
+  private native boolean isInteger(long pointer);
+
+  /**
+   * @return the stored integer in (decimal) string representation.
+   * Note: Asserts isInteger().
+   */
+  public String getInteger() {
+    return getInteger(pointer);
+  }
+
+  private native String getInteger(long pointer);
+
+  /**
+   * @return true if the term is a string constant.
+   */
+  public boolean isString() {
+    return isString(pointer);
+  }
+
+  private native boolean isString(long pointer);
+
+  /**
+   * @return the stored string constant.
+   * <p>
+   * Note: This method is not to be confused with toString() which returns the
+   * term in some string representation, whatever data it may hold.
+   * Asserts isString().
+   */
+  public String getString() {
+    return getString(pointer);
+  }
+
+  private native String getString(long pointer);
+
+  public class ConstIterator implements Iterator<Term> {
+    private int currentIndex;
+    private int size;
+
+    public ConstIterator() {
+      currentIndex = -1;
+      size = getNumChildren();
+    }
+
+    @Override
+    public boolean hasNext() {
+      return currentIndex < size - 1;
+    }
+
+    @Override
+    public Term next() {
+      if (currentIndex >= size - 1) {
+        throw new NoSuchElementException();
+      }
+      currentIndex++;
+      try {
+        return getChild(currentIndex);
+      } catch (CVC5ApiException e) {
+        e.printStackTrace();
+        throw new RuntimeException(e.getMessage());
+      }
+    }
+  }
+
+  @Override
+  public Iterator<Term> iterator() {
+    return new ConstIterator();
+  }
+}
diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp
new file mode 100644
index 000000000..6c4d00ff3
--- /dev/null
+++ b/src/api/java/jni/cvc5_Term.cpp
@@ -0,0 +1,587 @@
+/******************************************************************************
+ * 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_Term.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Term
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Term_deletePointer(JNIEnv* env,
+                                                    jclass,
+                                                    jlong pointer)
+{
+  delete reinterpret_cast<Term*>(pointer);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    equals
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_equals(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer1,
+                                                 jlong pointer2)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* term1 = reinterpret_cast<Term*>(pointer1);
+  Term* term2 = reinterpret_cast<Term*>(pointer2);
+  // We compare the actual terms, not their pointers.
+  return static_cast<jboolean>(*term1 == *term2);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    compareTo
+ * Signature: (JJ)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Term_compareTo(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer1,
+                                                jlong pointer2)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* term1 = reinterpret_cast<Term*>(pointer1);
+  Term* term2 = reinterpret_cast<Term*>(pointer2);
+  if (*term1 < *term2)
+  {
+    return static_cast<jint>(-1);
+  }
+  if (*term1 == *term2)
+  {
+    return 0;
+  }
+  return static_cast<jint>(1);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getNumChildren
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Term_getNumChildren(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jint>(current->getNumChildren());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getChild
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getChild(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer,
+                                                jint index)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* ret = new Term((*current)[static_cast<size_t>(index)]);
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getId
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getId(JNIEnv* env,
+                                             jobject,
+                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jlong>(current->getId());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getKind
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Term_getKind(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jint>(current->getKind());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getSort(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Sort* ret = new Sort(current->getSort());
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    substitute
+ * Signature: (JJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_substitute__JJJ(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer,
+                                                       jlong termPointer,
+                                                       jlong replacementPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* replacement = reinterpret_cast<Term*>(replacementPointer);
+  Term* ret = new Term(current->substitute(*term, *replacement));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    substitute
+ * Signature: (J[J[J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_Term_substitute__J_3J_3J(JNIEnv* env,
+                                   jobject,
+                                   jlong pointer,
+                                   jlongArray termPointers,
+                                   jlongArray replacementPointers)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  jsize termsSize = env->GetArrayLength(termPointers);
+  jsize replacementsSize = env->GetArrayLength(replacementPointers);
+  jlong* termElements = env->GetLongArrayElements(termPointers, nullptr);
+  jlong* replacementElements =
+      env->GetLongArrayElements(replacementPointers, nullptr);
+
+  std::vector<Term> terms(termsSize);
+  std::vector<Term> replacements(replacementsSize);
+
+  for (jsize i = 0; i < termsSize; i++)
+  {
+    Term* term = (Term*)termElements[i];
+    terms[i] = *term;
+  }
+  env->ReleaseLongArrayElements(termPointers, termElements, 0);
+
+  for (jsize i = 0; i < replacementsSize; i++)
+  {
+    Term* term = (Term*)replacementElements[i];
+    replacements[i] = *term;
+  }
+  env->ReleaseLongArrayElements(replacementPointers, replacementElements, 0);
+
+  Term* ret = new Term(current->substitute(terms, replacements));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    hasOp
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_hasOp(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->hasOp());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getOp
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getOp(JNIEnv* env,
+                                             jobject,
+                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Op* ret = new Op(current->getOp());
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isNull());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getConstArrayBase
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* ret = new Term(current->getConstArrayBase());
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getConstSequenceElements
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL
+Java_cvc5_Term_getConstSequenceElements(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::vector<Term> terms = current->getSequenceValue();
+  std::vector<long> termPointers(terms.size());
+  for (size_t i = 0; i < terms.size(); i++)
+  {
+    termPointers[i] = reinterpret_cast<long>(new Term(terms[i]));
+  }
+
+  jlongArray ret = env->NewLongArray(terms.size());
+  env->SetLongArrayRegion(ret, 0, terms.size(), termPointers.data());
+
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    notTerm
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_notTerm(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* ret = new Term(current->notTerm());
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    andTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_andTerm(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer,
+                                               jlong termPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* ret = new Term(current->andTerm(*term));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    orTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_orTerm(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer,
+                                              jlong termPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* ret = new Term(current->orTerm(*term));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    xorTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_xorTerm(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer,
+                                               jlong termPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* ret = new Term(current->xorTerm(*term));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    eqTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_eqTerm(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer,
+                                              jlong termPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* ret = new Term(current->eqTerm(*term));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    impTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_impTerm(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer,
+                                               jlong termPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* term = reinterpret_cast<Term*>(termPointer);
+  Term* ret = new Term(current->impTerm(*term));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    iteTerm
+ * Signature: (JJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_iteTerm(
+    JNIEnv* env, jobject, jlong pointer, jlong thenPointer, jlong elsePointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term* thenTerm = reinterpret_cast<Term*>(thenPointer);
+  Term* elseTerm = reinterpret_cast<Term*>(elsePointer);
+  Term* ret = new Term(current->iteTerm(*thenTerm, *elseTerm));
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isInt
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInt(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isInt32Value());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getInt
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Term_getInt(JNIEnv* env,
+                                             jobject,
+                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jint>(current->getInt32Value());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isLong
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isLong(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isInt64Value());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getLong
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getLong(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jlong>(current->getInt64Value());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isInteger
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInteger(JNIEnv* env,
+                                                    jobject,
+                                                    jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isIntegerValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getInteger
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getInteger(JNIEnv* env,
+                                                    jobject,
+                                                    jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return env->NewStringUTF(current->getIntegerValue().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isString
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isString(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isStringValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getString(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::wstring termString = current->getStringValue();
+
+  size_t length = termString.length();
+  jchar* unicode = new jchar[length];
+  const wchar_t* s = termString.c_str();
+  for (size_t i = 0; i < length; i++)
+  {
+    unicode[i] = s[i];
+  }
+  jstring ret = env->NewString(unicode, length);
+  delete[] unicode;
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    iterator
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Term_iterator(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  Term::const_iterator* retPointer = new Term::const_iterator(current->begin());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java
new file mode 100644
index 000000000..d5491e0e7
--- /dev/null
+++ b/test/unit/api/java/cvc5/TermTest.java
@@ -0,0 +1,852 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Makai Mann, Andrew Reynolds, 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 Term class.
+ */
+
+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 TermTest {
+  private Solver d_solver;
+
+  @BeforeEach
+  void setUp() {
+    d_solver = new Solver();
+  }
+
+  @Test
+  void eq() {
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(uSort, "x");
+    Term y = d_solver.mkVar(uSort, "y");
+    Term z = d_solver.getNullTerm();
+
+    assertTrue(x == x);
+    assertFalse(x != x);
+    assertFalse(x == y);
+    assertTrue(x != y);
+    assertFalse((x == z));
+    assertTrue(x != z);
+  }
+
+  @Test
+  void getId() {
+    Term n = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> n.getId());
+    Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
+    assertDoesNotThrow(() -> x.getId());
+    Term y = x;
+    assertEquals(x.getId(), y.getId());
+
+    Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
+    assertNotEquals(x.getId(), z.getId());
+  }
+
+  @Test
+  void getKind() throws CVC5ApiException {
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term n = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> n.getKind());
+    Term x = d_solver.mkVar(uSort, "x");
+    assertDoesNotThrow(() -> x.getKind());
+    Term y = d_solver.mkVar(uSort, "y");
+    assertDoesNotThrow(() -> y.getKind());
+
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertDoesNotThrow(() -> f.getKind());
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertDoesNotThrow(() -> p.getKind());
+
+    Term zero = d_solver.mkInteger(0);
+    assertDoesNotThrow(() -> zero.getKind());
+
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertDoesNotThrow(() -> f_x.getKind());
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    assertDoesNotThrow(() -> f_y.getKind());
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    assertDoesNotThrow(() -> sum.getKind());
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.getKind());
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+    assertDoesNotThrow(() -> p_f_y.getKind());
+
+    // Sequence kinds do not exist internally, test that the API properly
+    // converts them back.
+    Sort seqSort = d_solver.mkSequenceSort(intSort);
+    Term s = d_solver.mkConst(seqSort, "s");
+    Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
+    assertEquals(ss.getKind(), SEQ_CONCAT);
+  }
+
+  @Test
+  void getSort() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term n = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> n.getSort());
+    Term x = d_solver.mkVar(bvSort, "x");
+    assertDoesNotThrow(() -> x.getSort());
+    assertEquals(x.getSort(), bvSort);
+    Term y = d_solver.mkVar(bvSort, "y");
+    assertDoesNotThrow(() -> y.getSort());
+    assertEquals(y.getSort(), bvSort);
+
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertDoesNotThrow(() -> f.getSort());
+    assertEquals(f.getSort(), funSort1);
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertDoesNotThrow(() -> p.getSort());
+    assertEquals(p.getSort(), funSort2);
+
+    Term zero = d_solver.mkInteger(0);
+    assertDoesNotThrow(() -> zero.getSort());
+    assertEquals(zero.getSort(), intSort);
+
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertDoesNotThrow(() -> f_x.getSort());
+    assertEquals(f_x.getSort(), intSort);
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    assertDoesNotThrow(() -> f_y.getSort());
+    assertEquals(f_y.getSort(), intSort);
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    assertDoesNotThrow(() -> sum.getSort());
+    assertEquals(sum.getSort(), intSort);
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.getSort());
+    assertEquals(p_0.getSort(), boolSort);
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+    assertDoesNotThrow(() -> p_f_y.getSort());
+    assertEquals(p_f_y.getSort(), boolSort);
+  }
+
+  @Test
+  void getOp() throws CVC5ApiException {
+    Sort intsort = d_solver.getIntegerSort();
+    Sort bvsort = d_solver.mkBitVectorSort(8);
+    Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
+    Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+
+    Term x = d_solver.mkConst(intsort, "x");
+    Term a = d_solver.mkConst(arrsort, "a");
+    Term b = d_solver.mkConst(bvsort, "b");
+
+    assertFalse(x.hasOp());
+    assertThrows(CVC5ApiException.class, () -> x.getOp());
+
+    Term ab = d_solver.mkTerm(SELECT, a, b);
+    Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+    Term extb = d_solver.mkTerm(ext, b);
+
+    assertTrue(ab.hasOp());
+    assertFalse(ab.getOp().isIndexed());
+    // can compare directly to a Kind (will invoke Op constructor)
+    assertTrue(extb.hasOp());
+    assertTrue(extb.getOp().isIndexed());
+    assertEquals(extb.getOp(), ext);
+
+    Term f = d_solver.mkConst(funsort, "f");
+    Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+    assertFalse(f.hasOp());
+    assertThrows(CVC5ApiException.class, () -> f.getOp());
+    assertTrue(fx.hasOp());
+    List<Term> children = new ArrayList();
+
+    Iterator<Term> iterator = fx.iterator();
+    for (Term t : fx) {
+      children.add(t);
+    }
+
+    // testing rebuild from op and children
+    assertEquals(fx, d_solver.mkTerm(fx.getOp(), children));
+
+    // Test Datatypes Ops
+    Sort sort = d_solver.mkParamSort("T");
+    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    cons.addSelector("head", sort);
+    cons.addSelectorSelf("tail");
+    listDecl.addConstructor(cons);
+    listDecl.addConstructor(nil);
+    Sort listSort = d_solver.mkDatatypeSort(listDecl);
+    Sort intListSort =
+        listSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
+    Term c = d_solver.mkConst(intListSort, "c");
+    Datatype list = listSort.getDatatype();
+    // list datatype constructor and selector operator terms
+    Term consOpTerm = list.getConstructorTerm("cons");
+    Term nilOpTerm = list.getConstructorTerm("nil");
+  }
+
+  @Test
+  void isNull() throws CVC5ApiException {
+    Term x = d_solver.getNullTerm();
+    assertTrue(x.isNull());
+    x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
+    assertFalse(x.isNull());
+  }
+
+  @Test
+  void notTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().notTerm());
+    Term b = d_solver.mkTrue();
+    assertDoesNotThrow(() -> b.notTerm());
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.notTerm());
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.notTerm());
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.notTerm());
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.notTerm());
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.notTerm());
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.notTerm());
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.notTerm());
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.notTerm());
+  }
+
+  @Test
+  void andTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().andTerm(b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.andTerm(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.andTerm(b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> x.andTerm(x));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f.andTerm(f));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p.andTerm(p));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> zero.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> zero.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> zero.andTerm(p));
+    assertThrows(CVC5ApiException.class, () -> zero.andTerm(zero));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(p));
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f_x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(p));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> sum.andTerm(sum));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_0.andTerm(sum));
+    assertDoesNotThrow(() -> p_0.andTerm(p_0));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(sum));
+    assertDoesNotThrow(() -> p_f_x.andTerm(p_0));
+    assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x));
+  }
+
+  @Test
+  void orTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().orTerm(b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.orTerm(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.orTerm(b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> x.orTerm(x));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f.orTerm(f));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p.orTerm(p));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> zero.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> zero.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> zero.orTerm(p));
+    assertThrows(CVC5ApiException.class, () -> zero.orTerm(zero));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(p));
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f_x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(p));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> sum.orTerm(sum));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_0.orTerm(sum));
+    assertDoesNotThrow(() -> p_0.orTerm(p_0));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(sum));
+    assertDoesNotThrow(() -> p_f_x.orTerm(p_0));
+    assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x));
+  }
+
+  @Test
+  void xorTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().xorTerm(b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.xorTerm(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.xorTerm(b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> x.xorTerm(x));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f.xorTerm(f));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p.xorTerm(p));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> zero.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> zero.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> zero.xorTerm(p));
+    assertThrows(CVC5ApiException.class, () -> zero.xorTerm(zero));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(p));
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f_x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(p));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> sum.xorTerm(sum));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(sum));
+    assertDoesNotThrow(() -> p_0.xorTerm(p_0));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(sum));
+    assertDoesNotThrow(() -> p_f_x.xorTerm(p_0));
+    assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x));
+  }
+
+  @Test
+  void eqTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().eqTerm(b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.eqTerm(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.eqTerm(b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.eqTerm(b));
+    assertDoesNotThrow(() -> x.eqTerm(x));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f.eqTerm(x));
+    assertDoesNotThrow(() -> f.eqTerm(f));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p.eqTerm(f));
+    assertDoesNotThrow(() -> p.eqTerm(p));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> zero.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> zero.eqTerm(f));
+    assertThrows(CVC5ApiException.class, () -> zero.eqTerm(p));
+    assertDoesNotThrow(() -> zero.eqTerm(zero));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(f));
+    assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(p));
+    assertDoesNotThrow(() -> f_x.eqTerm(zero));
+    assertDoesNotThrow(() -> f_x.eqTerm(f_x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> sum.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> sum.eqTerm(f));
+    assertThrows(CVC5ApiException.class, () -> sum.eqTerm(p));
+    assertDoesNotThrow(() -> sum.eqTerm(zero));
+    assertDoesNotThrow(() -> sum.eqTerm(f_x));
+    assertDoesNotThrow(() -> sum.eqTerm(sum));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(sum));
+    assertDoesNotThrow(() -> p_0.eqTerm(p_0));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(sum));
+    assertDoesNotThrow(() -> p_f_x.eqTerm(p_0));
+    assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x));
+  }
+
+  @Test
+  void impTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().impTerm(b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.impTerm(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.impTerm(b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertThrows(CVC5ApiException.class, () -> x.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> x.impTerm(x));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f.impTerm(f));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p.impTerm(p));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> zero.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> zero.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> zero.impTerm(p));
+    assertThrows(CVC5ApiException.class, () -> zero.impTerm(zero));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(p));
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f_x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(p));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> sum.impTerm(sum));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_0.impTerm(sum));
+    assertDoesNotThrow(() -> p_0.impTerm(p_0));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(p));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(zero));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f_x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(sum));
+    assertDoesNotThrow(() -> p_f_x.impTerm(p_0));
+    assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x));
+  }
+
+  @Test
+  void iteTerm() throws CVC5ApiException {
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+    Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term b = d_solver.mkTrue();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getNullTerm().iteTerm(b, b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.iteTerm(d_solver.getNullTerm(), b));
+    assertThrows(
+        CVC5ApiException.class, () -> b.iteTerm(b, d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> b.iteTerm(b, b));
+    Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+    assertDoesNotThrow(() -> b.iteTerm(x, x));
+    assertDoesNotThrow(() -> b.iteTerm(b, b));
+    assertThrows(CVC5ApiException.class, () -> b.iteTerm(x, b));
+    assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, x));
+    assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, b));
+    Term f = d_solver.mkVar(funSort1, "f");
+    assertThrows(CVC5ApiException.class, () -> f.iteTerm(b, b));
+    assertThrows(CVC5ApiException.class, () -> x.iteTerm(b, x));
+    Term p = d_solver.mkVar(funSort2, "p");
+    assertThrows(CVC5ApiException.class, () -> p.iteTerm(b, b));
+    assertThrows(CVC5ApiException.class, () -> p.iteTerm(x, b));
+    Term zero = d_solver.mkInteger(0);
+    assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, x));
+    assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, b));
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b));
+    assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x));
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+    assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x));
+    assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x));
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    assertDoesNotThrow(() -> p_0.iteTerm(b, b));
+    assertDoesNotThrow(() -> p_0.iteTerm(x, x));
+    assertThrows(CVC5ApiException.class, () -> p_0.iteTerm(x, b));
+    Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+    assertDoesNotThrow(() -> p_f_x.iteTerm(b, b));
+    assertDoesNotThrow(() -> p_f_x.iteTerm(x, x));
+    assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b));
+  }
+
+  @Test
+  void termAssignment() {
+    Term t1 = d_solver.mkInteger(1);
+    Term t2 = t1;
+    t2 = d_solver.mkInteger(2);
+    assertEquals(t1, d_solver.mkInteger(1));
+  }
+
+  @Test
+  void termCompare() {
+    Term t1 = d_solver.mkInteger(1);
+    Term t2 =
+        d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+    Term t3 =
+        d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+    assertTrue(t2.compareTo(t3) >= 0);
+    assertTrue(t2.compareTo(t3) <= 0);
+    assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0));
+    assertTrue(
+        (t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0));
+  }
+
+  @Test
+  void termChildren() throws CVC5ApiException {
+    // simple term 2+3
+    Term two = d_solver.mkInteger(2);
+    Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
+    assertEquals(t1.getChild(0), two);
+    assertEquals(t1.getNumChildren(), 2);
+    Term tnull = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> tnull.getNumChildren());
+
+    // apply term f(2)
+    Sort intSort = d_solver.getIntegerSort();
+    Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+    Term f = d_solver.mkConst(fsort, "f");
+    Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
+    // due to our higher-order view of terms, we treat f as a child of APPLY_UF
+    assertEquals(t2.getNumChildren(), 2);
+    assertEquals(t2.getChild(0), f);
+    assertEquals(t2.getChild(1), two);
+    assertThrows(CVC5ApiException.class, () -> tnull.getChild(0));
+  }
+
+  @Test
+  void getInteger() throws CVC5ApiException {
+    Term int1 = d_solver.mkInteger("-18446744073709551616");
+    Term int2 = d_solver.mkInteger("-18446744073709551615");
+    Term int3 = d_solver.mkInteger("-4294967296");
+    Term int4 = d_solver.mkInteger("-4294967295");
+    Term int5 = d_solver.mkInteger("-10");
+    Term int6 = d_solver.mkInteger("0");
+    Term int7 = d_solver.mkInteger("10");
+    Term int8 = d_solver.mkInteger("4294967295");
+    Term int9 = d_solver.mkInteger("4294967296");
+    Term int10 = d_solver.mkInteger("18446744073709551615");
+    Term int11 = d_solver.mkInteger("18446744073709551616");
+    Term int12 = d_solver.mkInteger("-0");
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(""));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-1-"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0.0"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-0.1"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("012"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0000"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-01"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-00"));
+
+    assertTrue(!int1.isInt() && !int1.isLong() && int1.isInteger());
+    assertEquals(int1.getInteger(), "-18446744073709551616");
+    assertTrue(!int2.isInt() && !int2.isLong() && int2.isInteger());
+    assertEquals(int2.getInteger(), "-18446744073709551615");
+    assertTrue(!int3.isInt() && int3.isLong() && int3.isInteger());
+    assertEquals(int3.getLong(), -4294967296L);
+    assertEquals(int3.getInteger(), "-4294967296");
+    assertTrue(!int4.isInt() && int4.isLong() && int4.isInteger());
+    assertEquals(int4.getLong(), -4294967295L);
+    assertEquals(int4.getInteger(), "-4294967295");
+    assertTrue(int5.isInt() && int5.isLong() && int5.isInteger());
+    assertEquals(int5.getInt(), -10);
+    assertEquals(int5.getLong(), -10);
+    assertEquals(int5.getInteger(), "-10");
+    assertTrue(int6.isInt() && int6.isLong() && int6.isInteger());
+    assertEquals(int6.getInt(), 0);
+    assertEquals(int6.getLong(), 0);
+    assertEquals(int6.getInteger(), "0");
+    assertTrue(int7.isInt() && int7.isLong() && int7.isInteger());
+    assertEquals(int7.getInt(), 10);
+    assertEquals(int7.getLong(), 10);
+    assertEquals(int7.getInteger(), "10");
+    assertTrue(!int8.isInt() && int8.isLong() && int8.isInteger());
+    assertEquals(Integer.toUnsignedLong(int8.getInt()), 4294967295L);
+    assertEquals(int8.getLong(), 4294967295L);
+    assertEquals(int8.getInteger(), "4294967295");
+    assertTrue(!int9.isInt() && int9.isLong() && int9.isInteger());
+    assertEquals(int9.getLong(), 4294967296L);
+    assertEquals(int9.getInteger(), "4294967296");
+    assertTrue(!int10.isInt() && !int10.isLong() && int10.isInteger());
+
+    assertEquals(Long.compareUnsigned(int10.getLong(),
+                     new BigInteger("18446744073709551615").longValue()),
+        0);
+    assertEquals(int10.getInteger(), "18446744073709551615");
+    assertTrue(!int11.isInt() && !int11.isLong() && int11.isInteger());
+    assertEquals(int11.getInteger(), "18446744073709551616");
+  }
+
+  @Test
+  void getString() {
+    Term s1 = d_solver.mkString("abcde");
+    assertTrue(s1.isString());
+    assertEquals(s1.getString(), "abcde");
+  }
+
+  @Test
+  void substitute() {
+    Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+    Term one = d_solver.mkInteger(1);
+    Term ttrue = d_solver.mkTrue();
+    Term xpx = d_solver.mkTerm(PLUS, x, x);
+    Term onepone = d_solver.mkTerm(PLUS, one, one);
+
+    assertEquals(xpx.substitute(x, one), onepone);
+    assertEquals(onepone.substitute(one, x), xpx);
+    // incorrect due to type
+    assertThrows(CVC5ApiException.class, () -> xpx.substitute(one, ttrue));
+
+    // simultaneous substitution
+    Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
+    Term xpy = d_solver.mkTerm(PLUS, x, y);
+    Term xpone = d_solver.mkTerm(PLUS, y, one);
+    List<Term> es = new ArrayList<>();
+    List<Term> rs = new ArrayList<>();
+    es.add(x);
+    rs.add(y);
+    es.add(y);
+    rs.add(one);
+    assertEquals(xpy.substitute(es, rs), xpone);
+
+    // incorrect substitution due to arity
+    rs.remove(rs.size() - 1);
+    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+
+    // incorrect substitution due to types
+    rs.add(ttrue);
+    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+
+    // null cannot substitute
+    Term tnull = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> tnull.substitute(one, x));
+    assertThrows(CVC5ApiException.class, () -> xpx.substitute(tnull, x));
+    assertThrows(CVC5ApiException.class, () -> xpx.substitute(x, tnull));
+    rs.remove(rs.size() - 1);
+    rs.add(tnull);
+    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+    es.clear();
+    rs.clear();
+    es.add(x);
+    rs.add(y);
+    assertThrows(CVC5ApiException.class, () -> tnull.substitute(es, rs));
+    es.add(tnull);
+    rs.add(one);
+    assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs));
+  }
+
+  @Test
+  void constArray() throws CVC5ApiException {
+    Sort intsort = d_solver.getIntegerSort();
+    Sort arrsort = d_solver.mkArraySort(intsort, intsort);
+    Term a = d_solver.mkConst(arrsort, "a");
+    Term one = d_solver.mkInteger(1);
+    Term constarr = d_solver.mkConstArray(arrsort, one);
+
+    assertEquals(constarr.getKind(), CONST_ARRAY);
+    assertEquals(constarr.getConstArrayBase(), one);
+    assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase());
+
+    arrsort =
+        d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+    Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
+    Term stores = d_solver.mkTerm(
+        STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+    stores =
+        d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+    stores =
+        d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
+  }
+
+  @Test
+  void constSequenceElements() throws CVC5ApiException {
+    Sort realsort = d_solver.getRealSort();
+    Sort seqsort = d_solver.mkSequenceSort(realsort);
+    Term s = d_solver.mkEmptySequence(seqsort);
+
+    assertEquals(s.getKind(), CONST_SEQUENCE);
+    // empty sequence has zero elements
+    List<Term> cs = Arrays.asList(s.getConstSequenceElements());
+    assertTrue(cs.isEmpty());
+
+    // A seq.unit app is not a constant sequence (regardless of whether it is
+    // applied to a constant).
+    Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
+    assertThrows(CVC5ApiException.class, () -> su.getConstSequenceElements());
+  }
+
+  @Test
+  void termScopedToString() {
+    Sort intsort = d_solver.getIntegerSort();
+    Term x = d_solver.mkConst(intsort, "x");
+    assertEquals(x.toString(), "x");
+    Solver solver2;
+    assertEquals(x.toString(), "x");
+  }
+}