Add missing functions in Term.java (#7297)

This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.

11 files changed, 751 insertions, 182 deletions

diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 12601f397..95831f33d 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -67,6 +67,7 @@ set(JAVA_FILES
   ${CMAKE_CURRENT_LIST_DIR}/cvc5/Stat.java
   ${CMAKE_CURRENT_LIST_DIR}/cvc5/Statistics.java
   ${CMAKE_CURRENT_LIST_DIR}/cvc5/Term.java
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/Triplet.java
   ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java
   ${JAVA_KIND_FILE}
 )
diff --git a/src/api/java/cvc5/AbstractPointer.java b/src/api/java/cvc5/AbstractPointer.java
index f6cdff8ad..8006b67be 100644
--- a/src/api/java/cvc5/AbstractPointer.java
+++ b/src/api/java/cvc5/AbstractPointer.java
@@ -25,6 +25,11 @@ abstract class AbstractPointer implements IPointer
     return pointer;
   }
 
+  public Solver getSolver()
+  {
+    return solver;
+  }
+
   @Override public String toString()
   {
     return toString(pointer);
diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java
index 6819946b6..bf908aff2 100644
--- a/src/api/java/cvc5/Op.java
+++ b/src/api/java/cvc5/Op.java
@@ -58,7 +58,7 @@ public class Op extends AbstractPointer
   /**
    * @return the kind of this operator
    */
-  Kind getKind()
+  public Kind getKind()
   {
     try
     {
diff --git a/src/api/java/cvc5/Pair.java b/src/api/java/cvc5/Pair.java
index 19cd3e797..84c9d8efe 100644
--- a/src/api/java/cvc5/Pair.java
+++ b/src/api/java/cvc5/Pair.java
@@ -34,8 +34,6 @@ public class Pair<K, V>
 
     Pair<K, V> p = (Pair<K, V>) pair;
 
-    if (!first.equals(p.first))
-      return false;
-    return second.equals(p.second);
+    return first.equals(p.first) && second.equals(p.second);
   }
 }
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index d295113b0..b0bee500c 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -2467,10 +2467,17 @@ public class Solver implements IPointer
   private native long[] getSynthSolutions(long pointer, long[] termPointers);
 
   /**
-   * Print solution for synthesis conjecture to the given output stream.
-   * @param out the output stream
+   * Returns a snapshot of the current state of the statistic values of this
+   * solver. The returned object is completely decoupled from the solver and
+   * will not change when the solver is used again.
    */
-  // TODO: void printSynthSolution(std::ostream& out)
+  public Statistics getStatistics()
+  {
+    long statisticsPointer = getStatistics(pointer);
+    return new Statistics(this, statisticsPointer);
+  }
+
+  private native long getStatistics(long pointer);
 
   /**
    * @return null term
diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java
index a935e453f..e2c719098 100644
--- a/src/api/java/cvc5/Term.java
+++ b/src/api/java/cvc5/Term.java
@@ -16,10 +16,12 @@
 package cvc5;
 
 import java.math.BigInteger;
+import java.util.Arrays;
+import java.util.HashSet;
 import java.util.Iterator;
 import java.util.List;
 import java.util.NoSuchElementException;
-import java.math.BigInteger;
+import java.util.Set;
 
 public class Term extends AbstractPointer implements Comparable<Term>, Iterable<Term>
 {
@@ -214,40 +216,6 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
   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
@@ -346,119 +314,337 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
   private native long iteTerm(long pointer, long thenPointer, long elsePointer);
 
   /**
-   * @return a string representation of this term
+   * @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.
+   * @return true if the term is an integer value.
    */
-  public boolean isInt()
+  public boolean isIntegerValue()
   {
-    return isInt(pointer);
+    return isIntegerValue(pointer);
   }
 
-  private native boolean isInt(long pointer);
+  private native boolean isIntegerValue(long pointer);
 
   /**
-   * @return the stored integer as an int.
-   * Note: Asserts isInt().
+   * Asserts isIntegerValue().
+   * @return the integer represented by this term.
    */
-  public int getInt()
+  public BigInteger getIntegerValue()
   {
-    return getInt(pointer);
+    return new BigInteger(getIntegerValue(pointer));
   }
 
-  private native int getInt(long pointer);
+  private native String getIntegerValue(long pointer);
 
   /**
-   * @return true if the term is an integer that fits within a Java long.
+   * @return true if the term is a string constant.
    */
-  public boolean isLong()
+  public boolean isStringValue()
   {
-    return isLong(pointer);
+    return isStringValue(pointer);
   }
 
-  private native boolean isLong(long pointer);
+  private native boolean isStringValue(long pointer);
 
   /**
-   * @return the stored integer as a long.
-   * Note: Asserts isLong().
+   * @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 long getLong()
+  public String getStringValue()
   {
-    return getLong(pointer);
+    return getStringValue(pointer);
   }
 
-  private native long getLong(long pointer);
+  private native String getStringValue(long pointer);
 
   /**
-   * @return true if the term is an integer.
+   * @return true if the term is a rational value.
    */
-  public boolean isInteger()
+  public boolean isRealValue()
   {
-    return isInteger(pointer);
+    return isRealValue(pointer);
   }
 
-  private native boolean isInteger(long pointer);
+  private native boolean isRealValue(long pointer);
 
   /**
-   * @return the stored integer in (decimal) string representation.
-   * Note: Asserts isInteger().
+   * Asserts isRealValue().
+   * @return the representation of a rational value as a pair of its numerator
+   * and denominator.
    */
-  public String getInteger()
+  public Pair<BigInteger, BigInteger> getRealValue()
   {
-    return getInteger(pointer);
+    String rational = getRealValue(pointer);
+    return Utils.getRational(rational);
   }
 
-  private native String getInteger(long pointer);
+  private native String getRealValue(long pointer);
 
   /**
-   * @return true if the term is a string constant.
+   * @return true if the term is a constant array.
    */
-  public boolean isString()
+  public boolean isConstArray()
   {
-    return isString(pointer);
+    return isConstArray(pointer);
   }
 
-  private native boolean isString(long pointer);
+  private native boolean isConstArray(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().
+   * Asserts isConstArray().
+   * @return the base (element stored at all indices) of a constant array
    */
-  public String getString()
+  public Term getConstArrayBase()
   {
-    return getString(pointer);
+    long termPointer = getConstArrayBase(pointer);
+    return new Term(solver, termPointer);
   }
 
-  private native String getString(long pointer);
+  private native long getConstArrayBase(long pointer);
 
   /**
-   * @return true if the term is a rational value.
+   * @return true if the term is a Boolean value.
    */
-  public boolean isRealValue()
+  public boolean isBooleanValue()
   {
-    return isRealValue(pointer);
+    return isBooleanValue(pointer);
   }
 
-  private native boolean isRealValue(long pointer);
+  private native boolean isBooleanValue(long pointer);
+  /**
+   * Asserts isBooleanValue().
+   * @return the representation of a Boolean value as a native Boolean value.
+   */
+  public boolean getBooleanValue()
+  {
+    return getBooleanValue(pointer);
+  }
+
+  private native boolean getBooleanValue(long pointer);
 
   /**
-   * Asserts isRealValue().
-   * @return the representation of a rational value as a pair of its numerator
-   * and denominator.
+   * @return true if the term is a bit-vector value.
    */
-  public Pair<BigInteger, BigInteger> getRealValue()
+  public boolean isBitVectorValue()
   {
-    String rational = getRealValue(pointer);
-    return Utils.getRational(rational);
+    return isBitVectorValue(pointer);
   }
 
-  private native String getRealValue(long pointer);
+  private native boolean isBitVectorValue(long pointer);
+
+  /**
+   * Asserts isBitVectorValue().
+   * @return the representation of a bit-vector value in bit string representation.
+   */
+  public String getBitVectorValue() throws CVC5ApiException
+  {
+    return getBitVectorValue(2);
+  }
+
+  /**
+   * Asserts isBitVectorValue().
+   * @return the representation of a bit-vector value in string representation.
+   * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
+   * string).
+   */
+  public String getBitVectorValue(int base) throws CVC5ApiException
+  {
+    Utils.validateUnsigned(base, "base");
+    return getBitVectorValue(pointer, base);
+  }
+
+  private native String getBitVectorValue(long pointer, int base);
+
+  /**
+   * @return true if the term is an abstract value.
+   */
+  public boolean isAbstractValue()
+  {
+    return isAbstractValue(pointer);
+  }
+
+  private native boolean isAbstractValue(long pointer);
+
+  /**
+   * Asserts isAbstractValue().
+   * @return the representation of an abstract value as a string.
+   */
+  public String getAbstractValue()
+  {
+    return getAbstractValue(pointer);
+  }
+
+  private native String getAbstractValue(long pointer);
+
+  /**
+   * @return true if the term is a tuple value.
+   */
+  public boolean isTupleValue()
+  {
+    return isTupleValue(pointer);
+  }
+
+  private native boolean isTupleValue(long pointer);
+
+  /**
+   * Asserts isTupleValue().
+   * @return the representation of a tuple value as a vector of terms.
+   */
+  public Term[] getTupleValue()
+  {
+    long[] termPointers = getTupleValue(pointer);
+    return Utils.getTerms(solver, termPointers);
+  }
+
+  private native long[] getTupleValue(long pointer);
+
+  /**
+   * @return true if the term is the floating-point value for positive zero.
+   */
+  public boolean isFloatingPointPosZero()
+  {
+    return isFloatingPointPosZero(pointer);
+  }
+
+  private native boolean isFloatingPointPosZero(long pointer);
+  /**
+   * @return true if the term is the floating-point value for negative zero.
+   */
+  public boolean isFloatingPointNegZero()
+  {
+    return isFloatingPointNegZero(pointer);
+  }
+
+  private native boolean isFloatingPointNegZero(long pointer);
+  /**
+   * @return true if the term is the floating-point value for positive
+   * infinity.
+   */
+  public boolean isFloatingPointPosInf()
+  {
+    return isFloatingPointPosInf(pointer);
+  }
+
+  private native boolean isFloatingPointPosInf(long pointer);
+  /**
+   * @return true if the term is the floating-point value for negative
+   * infinity.
+   */
+  public boolean isFloatingPointNegInf()
+  {
+    return isFloatingPointNegInf(pointer);
+  }
+
+  private native boolean isFloatingPointNegInf(long pointer);
+  /**
+   * @return true if the term is the floating-point value for not a number.
+   */
+  public boolean isFloatingPointNaN()
+  {
+    return isFloatingPointNaN(pointer);
+  }
+
+  private native boolean isFloatingPointNaN(long pointer);
+  /**
+   * @return true if the term is a floating-point value.
+   */
+  public boolean isFloatingPointValue()
+  {
+    return isFloatingPointValue(pointer);
+  }
+
+  private native boolean isFloatingPointValue(long pointer);
+  /**
+   * Asserts isFloatingPointValue().
+   * @return the representation of a floating-point value as a tuple of the
+   * exponent width, the significand width and a bit-vector value.
+   */
+  public Triplet<Long, Long, Term> getFloatingPointValue()
+  {
+    Triplet<Long, Long, Long> triplet = getFloatingPointValue(pointer);
+    return new Triplet(triplet.first, triplet.second, new Term(solver, triplet.third));
+  }
+
+  private native Triplet<Long, Long, Long> getFloatingPointValue(long pointer);
+
+  /**
+   * @return true if the term is a set value.
+   */
+  public boolean isSetValue()
+  {
+    return isSetValue(pointer);
+  }
+
+  private native boolean isSetValue(long pointer);
+  /**
+   * Asserts isSetValue().
+   * @return the representation of a set value as a set of terms.
+   */
+  public Set<Term> getSetValue()
+  {
+    long[] termPointers = getSetValue(pointer);
+    Term[] terms = Utils.getTerms(solver, termPointers);
+    return new HashSet<Term>(Arrays.asList(terms));
+  }
+
+  private native long[] getSetValue(long pointer);
+
+  /**
+   * @return true if the term is a sequence value.
+   */
+  public boolean isSequenceValue()
+  {
+    return isSequenceValue(pointer);
+  }
+
+  private native boolean isSequenceValue(long pointer);
+
+  /**
+   * Asserts isSequenceValue().
+   * Note that it is usually necessary for sequences to call
+   * `Solver::simplify()` to turn a sequence that is constructed by, e.g.,
+   * concatenation of unit sequences, into a sequence value.
+   * @return the representation of a sequence value as a vector of terms.
+   */
+  public Term[] getSequenceValue()
+  {
+    long[] termPointers = getSequenceValue(pointer);
+    return Utils.getTerms(solver, termPointers);
+  }
+
+  private native long[] getSequenceValue(long pointer);
+
+  /**
+   * @return true if the term is a value from an uninterpreted sort.
+   */
+  public boolean isUninterpretedValue()
+  {
+    return isUninterpretedValue(pointer);
+  }
+
+  private native boolean isUninterpretedValue(long pointer);
+
+  /**
+  boolean @return()
+   * Asserts isUninterpretedValue().
+   * @return the representation of an uninterpreted value as a pair of its
+  sort and its
+   * index.
+   */
+  public Pair<Sort, Integer> getUninterpretedValue()
+  {
+    Pair<Long, Integer> pair = getUninterpretedValue(pointer);
+    Sort sort = new Sort(solver, pair.first);
+    return new Pair<Sort, Integer>(sort, pair.second);
+  }
+
+  private native Pair<Long, Integer> getUninterpretedValue(long pointer);
 
   public class ConstIterator implements Iterator<Term>
   {
diff --git a/src/api/java/cvc5/Triplet.java b/src/api/java/cvc5/Triplet.java
new file mode 100644
index 000000000..0ba75e7fb
--- /dev/null
+++ b/src/api/java/cvc5/Triplet.java
@@ -0,0 +1,41 @@
+/******************************************************************************
+ * 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.
+ */
+
+package cvc5;
+
+public class Triplet<A, B, C>
+{
+  public A first;
+  public B second;
+  public C third;
+  public Triplet(A first, B second, C third)
+  {
+    this.first = first;
+    this.second = second;
+    this.third = third;
+  }
+
+  @Override public boolean equals(Object object)
+  {
+    if (this == object)
+      return true;
+    if (object == null || getClass() != object.getClass())
+      return false;
+
+    Triplet<A, B, C> triplet = (Triplet<A, B, C>) object;
+    return this.first.equals(triplet.first) && this.second.equals(triplet.second)
+        && this.third.equals(triplet.third);
+  }
+}
diff --git a/src/api/java/cvc5/Utils.java b/src/api/java/cvc5/Utils.java
index 077b77168..ce8632c88 100644
--- a/src/api/java/cvc5/Utils.java
+++ b/src/api/java/cvc5/Utils.java
@@ -155,6 +155,14 @@ public class Utils
   }
 
   /**
+     Convert a pair of BigIntegers to a rational string a/b
+   */
+  public static String getRational(Pair<BigInteger, BigInteger> pair)
+  {
+    return pair.first.toString() + "/" + pair.second.toString();
+  }
+
+  /**
    * Get the string version of define-fun command.
    * @param f the function to print
    * @param params the function parameters
diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h
index fc4399fed..7b550ef28 100644
--- a/src/api/java/jni/cvc5JavaApi.h
+++ b/src/api/java/jni/cvc5JavaApi.h
@@ -73,7 +73,7 @@ std::vector<T> getObjectsFromPointers(JNIEnv* env, jlongArray jPointers)
  * @return jni array of pointers
  */
 template <class T>
-jlongArray getPointersFromObjects(JNIEnv* env, std::vector<T> objects)
+jlongArray getPointersFromObjects(JNIEnv* env, const std::vector<T>& objects)
 {
   std::vector<jlong> pointers(objects.size());
   for (size_t i = 0; i < objects.size(); i++)
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index 9bcecd07f..c28ea412f 100644
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -2521,6 +2521,22 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getSynthSolutions(
 
 /*
  * Class:     cvc5_Solver
+ * Method:    getStatistics
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStatistics(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Statistics* retPointer = new Statistics(solver->getStatistics());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Solver
  * Method:    getNullTerm
  * Signature: (J)J
  */
diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp
index 0de1b5673..325a9c744 100644
--- a/src/api/java/jni/cvc5_Term.cpp
+++ b/src/api/java/jni/cvc5_Term.cpp
@@ -263,42 +263,33 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env,
 
 /*
  * Class:     cvc5_Term
- * Method:    getConstArrayBase
- * Signature: (J)J
+ * Method:    isConstArray
+ * Signature: (J)Z
  */
-JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env,
-                                                         jobject,
-                                                         jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isConstArray(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);
+  return static_cast<jboolean>(current->isConstArray());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getConstSequenceElements
- * Signature: (J)[J
+ * Method:    getConstArrayBase
+ * Signature: (J)J
  */
-JNIEXPORT jlongArray JNICALL
-Java_cvc5_Term_getConstSequenceElements(JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(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);
+  Term* ret = new Term(current->getConstArrayBase());
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
@@ -441,164 +432,480 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env,
 
 /*
  * Class:     cvc5_Term
- * Method:    isInt
+ * Method:    isIntegerValue
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInt(JNIEnv* env,
-                                                jobject,
-                                                jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isIntegerValue(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isInt32Value());
+  return static_cast<jboolean>(current->isIntegerValue());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getInt
- * Signature: (J)I
+ * Method:    getIntegerValue
+ * Signature: (J)Ljava/lang/String;
  */
-JNIEXPORT jint JNICALL Java_cvc5_Term_getInt(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer)
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getIntegerValue(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);
+  std::string value = current->getIntegerValue();
+  jstring ret = env->NewStringUTF(value.c_str());
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    isLong
+ * Method:    isStringValue
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isLong(JNIEnv* env,
-                                                 jobject,
-                                                 jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isStringValue(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isInt64Value());
+  return static_cast<jboolean>(current->isStringValue());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getLong
- * Signature: (J)J
+ * Method:    getStringValue
+ * Signature: (J)Ljava/lang/String;
  */
-JNIEXPORT jlong JNICALL Java_cvc5_Term_getLong(JNIEnv* env,
-                                               jobject,
-                                               jlong pointer)
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getStringValue(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);
+  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:    isInteger
+ * Method:    isRealValue
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInteger(JNIEnv* env,
-                                                    jobject,
-                                                    jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isIntegerValue());
+  return static_cast<jboolean>(current->isRealValue());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getInteger
+ * Method:    getRealValue
  * Signature: (J)Ljava/lang/String;
  */
-JNIEXPORT jstring JNICALL Java_cvc5_Term_getInteger(JNIEnv* env,
-                                                    jobject,
-                                                    jlong pointer)
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::string realValue = current->getRealValue();
+  return env->NewStringUTF(realValue.c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isBooleanValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBooleanValue(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isBooleanValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getBooleanValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_getBooleanValue(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->getBooleanValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isBitVectorValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBitVectorValue(JNIEnv* env,
+                                                           jobject,
+                                                           jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return env->NewStringUTF(current->getIntegerValue().c_str());
+  return static_cast<jboolean>(current->isBitVectorValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getBitVectorValue
+ * Signature: (JI)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getBitVectorValue(JNIEnv* env,
+                                                           jobject,
+                                                           jlong pointer,
+                                                           jint base)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::string ret =
+      current->getBitVectorValue(static_cast<std::uint32_t>(base));
+  return env->NewStringUTF(ret.c_str());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    isString
+ * Method:    isAbstractValue
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isString(JNIEnv* env,
-                                                   jobject,
-                                                   jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isAbstractValue(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isStringValue());
+  return static_cast<jboolean>(current->isAbstractValue());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getString
+ * Method:    getAbstractValue
  * Signature: (J)Ljava/lang/String;
  */
-JNIEXPORT jstring JNICALL Java_cvc5_Term_getString(JNIEnv* env,
-                                                   jobject,
-                                                   jlong pointer)
+JNIEXPORT jstring JNICALL Java_cvc5_Term_getAbstractValue(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  std::wstring termString = current->getStringValue();
+  std::string ret = current->getAbstractValue();
+  return env->NewStringUTF(ret.c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
 
-  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++)
+/*
+ * Class:     cvc5_Term
+ * Method:    isTupleValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isTupleValue(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isTupleValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getTupleValue
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getTupleValue(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::vector<Term> terms = current->getTupleValue();
+  jlongArray ret = getPointersFromObjects<Term>(env, terms);
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointPosZero
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosZero(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointPosZero());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointNegZero
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegZero(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointNegZero());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointPosInf
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosInf(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointPosInf());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointNegInf
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegInf(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointNegInf());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointNaN
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNaN(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointNaN());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isFloatingPointValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointValue(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFloatingPointValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getFloatingPointValue
+ * Signature: (J)Lcvc5/Triplet;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_Term_getFloatingPointValue(
+    JNIEnv* env, jobject thisObject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  auto [exponent, significand, term] = current->getFloatingPointValue();
+  Term* termPointer = new Term(term);
+
+  // Long longObject = new Long(pointer)
+  jclass longClass = env->FindClass("Ljava/lang/Long;");
+  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+  jobject e = env->NewObject(longClass, longConstructor, exponent);
+  jobject s = env->NewObject(longClass, longConstructor, significand);
+  jobject t = env->NewObject(longClass, longConstructor, termPointer);
+
+  // Triplet triplet = new Triplet<Long, Long, Long>(e, s, t);
+  jclass tripletClass = env->FindClass("Lcvc5/Triplet;");
+  jmethodID tripletConstructor = env->GetMethodID(
+      tripletClass,
+      "<init>",
+      "(Ljava/lang/Object;Ljava/lang/Object;Ljava/lang/Object;)V");
+  jobject triplet = env->NewObject(tripletClass, tripletConstructor, e, s, t);
+
+  return triplet;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isSetValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSetValue(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isSetValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getSetValue
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSetValue(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::set<Term> terms = current->getSetValue();
+  std::vector<jlong> pointers(terms.size());
+  int i = 0;
+  for (const Term& t : terms)
   {
-    unicode[i] = s[i];
+    pointers[i] = reinterpret_cast<jlong>(new Term(t));
+    i++;
   }
-  jstring ret = env->NewString(unicode, length);
-  delete[] unicode;
+  jlongArray ret = env->NewLongArray(pointers.size());
+  env->SetLongArrayRegion(ret, 0, pointers.size(), pointers.data());
   return ret;
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    isRealValue
+ * Method:    isSequenceValue
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env,
-                                                      jobject,
-                                                      jlong pointer)
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSequenceValue(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isRealValue());
+  return static_cast<jboolean>(current->isSequenceValue());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
 /*
  * Class:     cvc5_Term
- * Method:    getRealValue
- * Signature: (J)Ljava/lang/String;
+ * Method:    getSequenceValue
+ * Signature: (J)[J
  */
-JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env,
-                                                      jobject,
-                                                      jlong pointer)
+JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* current = reinterpret_cast<Term*>(pointer);
-  std::string realValue = current->getRealValue();
-  return env->NewStringUTF(realValue.c_str());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+  std::vector<Term> terms = current->getSequenceValue();
+  jlongArray ret = getPointersFromObjects<Term>(env, terms);
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    isUninterpretedValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isUninterpretedValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Term
+ * Method:    getUninterpretedValue
+ * Signature: (J)Lcvc5/Pair;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
+
+  Sort* sort = new Sort(value.first);
+  jlong sortPointer = reinterpret_cast<jlong>(sort);
+
+  // Long longObject = new Long(pointer)
+  jclass longClass = env->FindClass("Ljava/lang/Long;");
+  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+  jobject longObject = env->NewObject(longClass, longConstructor, sortPointer);
+
+  // Integer integerObject = new Integer(pair.second)
+  jclass integerClass = env->FindClass("Ljava/lang/Integer;");
+  jmethodID integerConstructor =
+      env->GetMethodID(integerClass, "<init>", "(I)V");
+  jobject integerObject = env->NewObject(
+      integerClass, integerConstructor, static_cast<jint>(value.second));
+
+  // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
+  jclass pairClass = env->FindClass("Lcvc5/Pair;");
+  jmethodID pairConstructor = env->GetMethodID(
+      pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
+  jobject pair =
+      env->NewObject(pairClass, pairConstructor, longObject, integerObject);
+
+  return pair;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
 /*