Add Datatype.java to the Java API (#6389)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 8 Sep 2021 08:33:16 +0000 (03:33 -0500)
committerGitHub <noreply@github.com>
Wed, 8 Sep 2021 08:33:16 +0000 (08:33 +0000)
This commit adds Datatype.java DatatypeTest.java and cvc5_Datatype.cpp to the java api.

src/api/java/cvc5/Datatype.java [new file with mode: 0644]
src/api/java/jni/cvc5_Datatype.cpp [new file with mode: 0644]
test/unit/api/java/cvc5/DatatypeTest.java [new file with mode: 0644]

diff --git a/src/api/java/cvc5/Datatype.java b/src/api/java/cvc5/Datatype.java
new file mode 100644 (file)
index 0000000..be1e476
--- /dev/null
@@ -0,0 +1,198 @@
+/******************************************************************************
+ * 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;
+
+public class Datatype extends AbstractPointer
+{
+  // region construction and destruction
+  Datatype(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
+
+  /**
+   * Get the datatype constructor at a given index.
+   * @param idx the index of the datatype constructor to return
+   * @return the datatype constructor with the given index
+   */
+  public DatatypeConstructor getConstructor(int idx)
+  {
+    long constructorPointer = getConstructor(pointer, idx);
+    return new DatatypeConstructor(solver, constructorPointer);
+  }
+
+  private native long getConstructor(long pointer, int index);
+
+  /**
+   * Get the datatype constructor with the given name.
+   * This is a linear search through the constructors, so in case of multiple,
+   * similarly-named constructors, the first is returned.
+   * @param name the name of the datatype constructor
+   * @return the datatype constructor with the given name
+   */
+  public DatatypeConstructor getConstructor(String name)
+  {
+    long constructorPointer = getConstructor(pointer, name);
+    return new DatatypeConstructor(solver, constructorPointer);
+  }
+
+  private native long getConstructor(long pointer, String name);
+
+  /**
+   * Get a term representing the datatype constructor with the given name.
+   * This is a linear search through the constructors, so in case of multiple,
+   * similarly-named constructors, the
+   * first is returned.
+   */
+  public Term getConstructorTerm(String name)
+  {
+    long termPointer = getConstructorTerm(pointer, name);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getConstructorTerm(long pointer, String name);
+
+  /**
+   * Get the datatype constructor with the given name.
+   * This is a linear search through the constructors and their selectors, so
+   * in case of multiple, similarly-named selectors, the first is returned.
+   * @param name the name of the datatype selector
+   * @return the datatype selector with the given name
+   */
+  public DatatypeSelector getSelector(String name)
+  {
+    long selectorPointer = getSelector(pointer, name);
+    return new DatatypeSelector(solver, selectorPointer);
+  }
+
+  private native long getSelector(long pointer, String name);
+
+  /** @return the name of this Datatype. */
+  public String getName()
+  {
+    return getName(pointer);
+  }
+
+  private native String getName(long pointer);
+
+  /** @return the number of constructors for this Datatype. */
+  public int getNumConstructors()
+  {
+    return getNumConstructors(pointer);
+  }
+
+  private native int getNumConstructors(long pointer);
+
+  /** @return true if this datatype is parametric */
+  public boolean isParametric()
+  {
+    return isParametric(pointer);
+  }
+
+  private native boolean isParametric(long pointer);
+
+  /** @return true if this datatype corresponds to a co-datatype */
+  public boolean isCodatatype()
+  {
+    return isCodatatype(pointer);
+  }
+
+  private native boolean isCodatatype(long pointer);
+
+  /** @return true if this datatype corresponds to a tuple */
+  public boolean isTuple()
+  {
+    return isTuple(pointer);
+  }
+
+  private native boolean isTuple(long pointer);
+
+  /** @return true if this datatype corresponds to a record */
+  public boolean isRecord()
+  {
+    return isRecord(pointer);
+  }
+
+  private native boolean isRecord(long pointer);
+
+  /** @return true if this datatype is finite */
+  public boolean isFinite()
+  {
+    return isFinite(pointer);
+  }
+
+  private native boolean isFinite(long pointer);
+
+  /**
+   * Is this datatype well-founded? If this datatype is not a codatatype,
+   * this returns false if there are no values of this datatype that are of
+   * finite size.
+   *
+   * @return true if this datatype is well-founded
+   */
+  public boolean isWellFounded()
+  {
+    return isWellFounded(pointer);
+  }
+
+  private native boolean isWellFounded(long pointer);
+
+  /**
+   * Does this datatype have nested recursion? This method returns false if a
+   * value of this datatype includes a subterm of its type that is nested
+   * beneath a non-datatype type constructor. For example, a datatype
+   * T containing a constructor having a selector with range type (Set T) has
+   * nested recursion.
+   *
+   * @return true if this datatype has nested recursion
+   */
+  public boolean hasNestedRecursion()
+  {
+    return hasNestedRecursion(pointer);
+  }
+
+  private native boolean hasNestedRecursion(long pointer);
+
+  /**
+   * @return true if this Datatype is a null object
+   */
+  public boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * @return a string representation of this datatype
+   */
+  protected native String toString(long pointer);
+}
diff --git a/src/api/java/jni/cvc5_Datatype.cpp b/src/api/java/jni/cvc5_Datatype.cpp
new file mode 100644 (file)
index 0000000..eb834da
--- /dev/null
@@ -0,0 +1,255 @@
+/******************************************************************************
+ * 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_Datatype.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Datatype_deletePointer(JNIEnv* env,
+                                                        jclass,
+                                                        jlong pointer)
+{
+  delete ((Datatype*)pointer);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    getConstructor
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JI(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jint idx)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  DatatypeConstructor* retPointer =
+      new DatatypeConstructor(current->operator[](idx));
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    getConstructor
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JLjava_lang_String_2(
+    JNIEnv* env, jobject, jlong pointer, jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  DatatypeConstructor* retPointer =
+      new DatatypeConstructor(current->operator[](cName));
+  env->ReleaseStringUTFChars(jName, s);
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    getConstructorTerm
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructorTerm(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  Term* retPointer = new Term(current->getConstructorTerm(cName));
+  env->ReleaseStringUTFChars(jName, s);
+  return ((jlong)retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    getName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Datatype_getName(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return env->NewStringUTF(current->getName().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    getNumConstructors
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Datatype_getNumConstructors(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jint)current->getNumConstructors();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isParametric
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isParametric(JNIEnv* env,
+                                                           jobject,
+                                                           jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isParametric();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isCodatatype
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isCodatatype(JNIEnv* env,
+                                                           jobject,
+                                                           jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isCodatatype();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isTuple
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isTuple(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isTuple();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isRecord
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isRecord(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isRecord();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isFinite
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isFinite(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isFinite();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isWellFounded
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isWellFounded(JNIEnv* env,
+                                                            jobject,
+                                                            jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isWellFounded();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    hasNestedRecursion
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_hasNestedRecursion(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->hasNestedRecursion();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isNull(JNIEnv* env,
+                                                     jobject,
+                                                     jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Datatype
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Datatype_toString(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Datatype* current = (Datatype*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/test/unit/api/java/cvc5/DatatypeTest.java b/test/unit/api/java/cvc5/DatatypeTest.java
new file mode 100644 (file)
index 0000000..2f57b6a
--- /dev/null
@@ -0,0 +1,566 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Aina Niemetz, Andres Noetzli, 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 datatype classes of the Java API.
+ */
+
+package cvc5;
+
+import static cvc5.Kind.*;
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.*;
+import java.util.concurrent.atomic.AtomicReference;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class DatatypeTest
+{
+  private Solver d_solver;
+
+  @BeforeEach void setUp()
+  {
+    d_solver = new Solver();
+  }
+
+  @Test void mkDatatypeSort() throws CVC5ApiException
+  {
+    DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", d_solver.getIntegerSort());
+    dtypeSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    dtypeSpec.addConstructor(nil);
+    Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
+    Datatype d = listSort.getDatatype();
+    DatatypeConstructor consConstr = d.getConstructor(0);
+    DatatypeConstructor nilConstr = d.getConstructor(1);
+    assertThrows(CVC5ApiException.class, () -> d.getConstructor(2));
+    assertDoesNotThrow(() -> consConstr.getConstructorTerm());
+    assertDoesNotThrow(() -> nilConstr.getConstructorTerm());
+  }
+
+  @Test void mkDatatypeSorts()
+  {
+    /* Create two mutual datatypes corresponding to this definition
+     * block:
+     *
+     *   DATATYPE
+     *     tree = node(left: tree, right: tree) | leaf(data: list),
+     *     list = cons(car: tree, cdr: list) | nil
+     *   END;
+     */
+    // Make unresolved types as placeholders
+    Set<Sort> unresTypes = new HashSet<>();
+    Sort unresTree = d_solver.mkUninterpretedSort("tree");
+    Sort unresList = d_solver.mkUninterpretedSort("list");
+    unresTypes.add(unresTree);
+    unresTypes.add(unresList);
+
+    DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
+    DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
+    node.addSelector("left", unresTree);
+    node.addSelector("right", unresTree);
+    tree.addConstructor(node);
+
+    DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
+    leaf.addSelector("data", unresList);
+    tree.addConstructor(leaf);
+
+    DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("car", unresTree);
+    cons.addSelector("cdr", unresTree);
+    list.addConstructor(cons);
+
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    list.addConstructor(nil);
+
+    List<DatatypeDecl> dtdecls = new ArrayList<>();
+    dtdecls.add(tree);
+    dtdecls.add(list);
+
+    AtomicReference<List<Sort>> atomic = new AtomicReference<>();
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    List<Sort> dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), dtdecls.size());
+    for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+    {
+      assertTrue(dtsorts.get(i).isDatatype());
+      assertFalse(dtsorts.get(i).getDatatype().isFinite());
+      assertEquals(dtsorts.get(i).getDatatype().getName(), dtdecls.get(i).getName());
+    }
+    // verify the resolution was correct
+    Datatype dtTree = dtsorts.get(0).getDatatype();
+    DatatypeConstructor dtcTreeNode = dtTree.getConstructor(0);
+    assertEquals(dtcTreeNode.getName(), "node");
+    DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0);
+    assertEquals(dtsTreeNodeLeft.getName(), "left");
+    // argument type should have resolved to be recursive
+    assertTrue(dtsTreeNodeLeft.getRangeSort().isDatatype());
+    assertEquals(dtsTreeNodeLeft.getRangeSort(), dtsorts.get(0));
+
+    // fails due to empty datatype
+    List<DatatypeDecl> dtdeclsBad = new ArrayList<>();
+    DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
+    dtdeclsBad.add(emptyD);
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(dtdeclsBad));
+  }
+
+  @Test void datatypeStructs() throws CVC5ApiException
+  {
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+
+    // create datatype sort to test
+    DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", intSort);
+    cons.addSelectorSelf("tail");
+    Sort nullSort = d_solver.getNullSort();
+    assertThrows(CVC5ApiException.class, () -> cons.addSelector("null", nullSort));
+    dtypeSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    dtypeSpec.addConstructor(nil);
+    Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+    Datatype dt = dtypeSort.getDatatype();
+    assertFalse(dt.isCodatatype());
+    assertFalse(dt.isTuple());
+    assertFalse(dt.isRecord());
+    assertFalse(dt.isFinite());
+    assertTrue(dt.isWellFounded());
+    // get constructor
+    DatatypeConstructor dcons = dt.getConstructor(0);
+    Term consTerm = dcons.getConstructorTerm();
+    assertEquals(dcons.getNumSelectors(), 2);
+
+    // create datatype sort to test
+    DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
+    DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A");
+    dtypeSpecEnum.addConstructor(ca);
+    DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B");
+    dtypeSpecEnum.addConstructor(cb);
+    DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C");
+    dtypeSpecEnum.addConstructor(cc);
+    Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
+    Datatype dtEnum = dtypeSortEnum.getDatatype();
+    assertFalse(dtEnum.isTuple());
+    assertTrue(dtEnum.isFinite());
+
+    // create codatatype
+    DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
+    DatatypeConstructorDecl consStream = d_solver.mkDatatypeConstructorDecl("cons");
+    consStream.addSelector("head", intSort);
+    consStream.addSelectorSelf("tail");
+    dtypeSpecStream.addConstructor(consStream);
+    Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
+    Datatype dtStream = dtypeSortStream.getDatatype();
+    assertTrue(dtStream.isCodatatype());
+    assertFalse(dtStream.isFinite());
+    // codatatypes may be well-founded
+    assertTrue(dtStream.isWellFounded());
+
+    // create tuple
+    Sort tupSort = d_solver.mkTupleSort(new Sort[] {boolSort});
+    Datatype dtTuple = tupSort.getDatatype();
+    assertTrue(dtTuple.isTuple());
+    assertFalse(dtTuple.isRecord());
+    assertTrue(dtTuple.isFinite());
+    assertTrue(dtTuple.isWellFounded());
+
+    // create record
+    Pair<String, Sort>[] fields = new Pair[] {new Pair<>("b", boolSort), new Pair<>("i", intSort)};
+    Sort recSort = d_solver.mkRecordSort(fields);
+    assertTrue(recSort.isDatatype());
+    Datatype dtRecord = recSort.getDatatype();
+    assertFalse(dtRecord.isTuple());
+    assertTrue(dtRecord.isRecord());
+    assertFalse(dtRecord.isFinite());
+    assertTrue(dtRecord.isWellFounded());
+  }
+
+  @Test void datatypeNames() throws CVC5ApiException
+  {
+    Sort intSort = d_solver.getIntegerSort();
+
+    // create datatype sort to test
+    DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+    assertDoesNotThrow(() -> dtypeSpec.getName());
+    assertEquals(dtypeSpec.getName(), "list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", intSort);
+    cons.addSelectorSelf("tail");
+    dtypeSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    dtypeSpec.addConstructor(nil);
+    Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+    Datatype dt = dtypeSort.getDatatype();
+    assertEquals(dt.getName(), "list");
+    assertDoesNotThrow(() -> dt.getConstructor("nil"));
+    assertDoesNotThrow(() -> dt.getConstructor("cons"));
+    assertThrows(CVC5ApiException.class, () -> dt.getConstructor("head"));
+    assertThrows(CVC5ApiException.class, () -> dt.getConstructor(""));
+
+    DatatypeConstructor dcons = dt.getConstructor(0);
+    assertEquals(dcons.getName(), "cons");
+    assertDoesNotThrow(() -> dcons.getSelector("head"));
+    assertDoesNotThrow(() -> dcons.getSelector("tail"));
+    assertThrows(CVC5ApiException.class, () -> dcons.getSelector("cons"));
+
+    // get selector
+    DatatypeSelector dselTail = dcons.getSelector(1);
+    assertEquals(dselTail.getName(), "tail");
+    assertEquals(dselTail.getRangeSort(), dtypeSort);
+
+    // possible to construct null datatype declarations if not using solver
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullDatatypeDecl().getName());
+  }
+
+  @Test void parametricDatatype() throws CVC5ApiException
+  {
+    List<Sort> v = new ArrayList<>();
+    Sort t1 = d_solver.mkParamSort("T1");
+    Sort t2 = d_solver.mkParamSort("T2");
+    v.add(t1);
+    v.add(t2);
+    DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v);
+
+    DatatypeConstructorDecl mkpair = d_solver.mkDatatypeConstructorDecl("mk-pair");
+    mkpair.addSelector("first", t1);
+    mkpair.addSelector("second", t2);
+    pairSpec.addConstructor(mkpair);
+
+    Sort pairType = d_solver.mkDatatypeSort(pairSpec);
+
+    assertTrue(pairType.getDatatype().isParametric());
+
+    v.clear();
+    v.add(d_solver.getIntegerSort());
+    v.add(d_solver.getIntegerSort());
+    Sort pairIntInt = pairType.instantiate(v);
+    v.clear();
+    v.add(d_solver.getRealSort());
+    v.add(d_solver.getRealSort());
+    Sort pairRealReal = pairType.instantiate(v);
+    v.clear();
+    v.add(d_solver.getRealSort());
+    v.add(d_solver.getIntegerSort());
+    Sort pairRealInt = pairType.instantiate(v);
+    v.clear();
+    v.add(d_solver.getIntegerSort());
+    v.add(d_solver.getRealSort());
+    Sort pairIntReal = pairType.instantiate(v);
+
+    assertNotEquals(pairIntInt, pairRealReal);
+    assertNotEquals(pairIntReal, pairRealReal);
+    assertNotEquals(pairRealInt, pairRealReal);
+    assertNotEquals(pairIntInt, pairIntReal);
+    assertNotEquals(pairIntInt, pairRealInt);
+    assertNotEquals(pairIntReal, pairRealInt);
+
+    assertTrue(pairRealReal.isComparableTo(pairRealReal));
+    assertFalse(pairIntReal.isComparableTo(pairRealReal));
+    assertFalse(pairRealInt.isComparableTo(pairRealReal));
+    assertFalse(pairIntInt.isComparableTo(pairRealReal));
+    assertFalse(pairRealReal.isComparableTo(pairRealInt));
+    assertFalse(pairIntReal.isComparableTo(pairRealInt));
+    assertTrue(pairRealInt.isComparableTo(pairRealInt));
+    assertFalse(pairIntInt.isComparableTo(pairRealInt));
+    assertFalse(pairRealReal.isComparableTo(pairIntReal));
+    assertTrue(pairIntReal.isComparableTo(pairIntReal));
+    assertFalse(pairRealInt.isComparableTo(pairIntReal));
+    assertFalse(pairIntInt.isComparableTo(pairIntReal));
+    assertFalse(pairRealReal.isComparableTo(pairIntInt));
+    assertFalse(pairIntReal.isComparableTo(pairIntInt));
+    assertFalse(pairRealInt.isComparableTo(pairIntInt));
+    assertTrue(pairIntInt.isComparableTo(pairIntInt));
+
+    assertTrue(pairRealReal.isSubsortOf(pairRealReal));
+    assertFalse(pairIntReal.isSubsortOf(pairRealReal));
+    assertFalse(pairRealInt.isSubsortOf(pairRealReal));
+    assertFalse(pairIntInt.isSubsortOf(pairRealReal));
+    assertFalse(pairRealReal.isSubsortOf(pairRealInt));
+    assertFalse(pairIntReal.isSubsortOf(pairRealInt));
+    assertTrue(pairRealInt.isSubsortOf(pairRealInt));
+    assertFalse(pairIntInt.isSubsortOf(pairRealInt));
+    assertFalse(pairRealReal.isSubsortOf(pairIntReal));
+    assertTrue(pairIntReal.isSubsortOf(pairIntReal));
+    assertFalse(pairRealInt.isSubsortOf(pairIntReal));
+    assertFalse(pairIntInt.isSubsortOf(pairIntReal));
+    assertFalse(pairRealReal.isSubsortOf(pairIntInt));
+    assertFalse(pairIntReal.isSubsortOf(pairIntInt));
+    assertFalse(pairRealInt.isSubsortOf(pairIntInt));
+    assertTrue(pairIntInt.isSubsortOf(pairIntInt));
+  }
+
+  @Test void datatypeSimplyRec() throws CVC5ApiException
+  {
+    /* Create mutual datatypes corresponding to this definition block:
+     *
+     *   DATATYPE
+     *     wlist = leaf(data: list),
+     *     list = cons(car: wlist, cdr: list) | nil,
+     *     ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list))
+     *   END;
+     */
+    // Make unresolved types as placeholders
+    Set<Sort> unresTypes = new HashSet<>();
+    Sort unresWList = d_solver.mkUninterpretedSort("wlist");
+    Sort unresList = d_solver.mkUninterpretedSort("list");
+    Sort unresNs = d_solver.mkUninterpretedSort("ns");
+    unresTypes.add(unresWList);
+    unresTypes.add(unresList);
+    unresTypes.add(unresNs);
+
+    DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist");
+    DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
+    leaf.addSelector("data", unresList);
+    wlist.addConstructor(leaf);
+
+    DatatypeDecl list = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("car", unresWList);
+    cons.addSelector("cdr", unresList);
+    list.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    list.addConstructor(nil);
+
+    DatatypeDecl ns = d_solver.mkDatatypeDecl("ns");
+    DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem");
+    elem.addSelector("ndata", d_solver.mkSetSort(unresWList));
+    ns.addConstructor(elem);
+    DatatypeConstructorDecl elemArray = d_solver.mkDatatypeConstructorDecl("elemArray");
+    elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList));
+    ns.addConstructor(elemArray);
+
+    List<DatatypeDecl> dtdecls = new ArrayList<>();
+    dtdecls.add(wlist);
+    dtdecls.add(list);
+    dtdecls.add(ns);
+    // this is well-founded and has no nested recursion
+    AtomicReference<List<Sort>> atomic = new AtomicReference<>();
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    List<Sort> dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 3);
+    assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(2).getDatatype().isWellFounded());
+    assertFalse(dtsorts.get(0).getDatatype().hasNestedRecursion());
+    assertFalse(dtsorts.get(1).getDatatype().hasNestedRecursion());
+    assertFalse(dtsorts.get(2).getDatatype().hasNestedRecursion());
+
+    /* Create mutual datatypes corresponding to this definition block:
+     *   DATATYPE
+     *     ns2 = elem2(ndata: array(int,ns2)) | nil2
+     *   END;
+     */
+    unresTypes.clear();
+    Sort unresNs2 = d_solver.mkUninterpretedSort("ns2");
+    unresTypes.add(unresNs2);
+
+    DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2");
+    DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2");
+    elem2.addSelector("ndata", d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2));
+    ns2.addConstructor(elem2);
+    DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
+    ns2.addConstructor(nil2);
+
+    dtdecls.clear();
+    dtdecls.add(ns2);
+
+    // dtsorts.clear();
+    // this is not well-founded due to non-simple recursion
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 1);
+    assertTrue(
+        dtsorts.get(0).getDatatype().getConstructor(0).getSelector(0).getRangeSort().isArray());
+    assertEquals(dtsorts.get(0)
+                     .getDatatype()
+                     .getConstructor(0)
+                     .getSelector(0)
+                     .getRangeSort()
+                     .getArrayElementSort(),
+        dtsorts.get(0));
+    assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
+
+    /* Create mutual datatypes corresponding to this definition block:
+     *   DATATYPE
+     *     list3 = cons3(car: ns3, cdr: list3) | nil3,
+     *     ns3 = elem3(ndata: set(list3))
+     *   END;
+     */
+    unresTypes.clear();
+    Sort unresNs3 = d_solver.mkUninterpretedSort("ns3");
+    unresTypes.add(unresNs3);
+    Sort unresList3 = d_solver.mkUninterpretedSort("list3");
+    unresTypes.add(unresList3);
+
+    DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3");
+    DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3");
+    cons3.addSelector("car", unresNs3);
+    cons3.addSelector("cdr", unresList3);
+    list3.addConstructor(cons3);
+    DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3");
+    list3.addConstructor(nil3);
+
+    DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3");
+    DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3");
+    elem3.addSelector("ndata", d_solver.mkSetSort(unresList3));
+    ns3.addConstructor(elem3);
+
+    dtdecls.clear();
+    dtdecls.add(list3);
+    dtdecls.add(ns3);
+
+    // dtsorts.clear();
+    // both are well-founded and have nested recursion
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 2);
+    assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
+    assertTrue(dtsorts.get(1).getDatatype().hasNestedRecursion());
+
+    /* Create mutual datatypes corresponding to this definition block:
+     *   DATATYPE
+     *     list4 = cons(car: set(ns4), cdr: list4) | nil,
+     *     ns4 = elem(ndata: list4)
+     *   END;
+     */
+    unresTypes.clear();
+    Sort unresNs4 = d_solver.mkUninterpretedSort("ns4");
+    unresTypes.add(unresNs4);
+    Sort unresList4 = d_solver.mkUninterpretedSort("list4");
+    unresTypes.add(unresList4);
+
+    DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4");
+    DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4");
+    cons4.addSelector("car", d_solver.mkSetSort(unresNs4));
+    cons4.addSelector("cdr", unresList4);
+    list4.addConstructor(cons4);
+    DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4");
+    list4.addConstructor(nil4);
+
+    DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4");
+    DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3");
+    elem4.addSelector("ndata", unresList4);
+    ns4.addConstructor(elem4);
+
+    dtdecls.clear();
+    dtdecls.add(list4);
+    dtdecls.add(ns4);
+
+    // dtsorts.clear();
+    // both are well-founded and have nested recursion
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 2);
+    assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
+    assertTrue(dtsorts.get(1).getDatatype().hasNestedRecursion());
+
+    /* Create mutual datatypes corresponding to this definition block:
+     *   DATATYPE
+     *     list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
+     *   END;
+     */
+    unresTypes.clear();
+    Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1);
+    unresTypes.add(unresList5);
+
+    List<Sort> v = new ArrayList<>();
+    Sort x = d_solver.mkParamSort("X");
+    v.add(x);
+    DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v);
+
+    List<Sort> args = new ArrayList<>();
+    args.add(x);
+    Sort urListX = unresList5.instantiate(args);
+    args.set(0, urListX);
+    Sort urListListX = unresList5.instantiate(args);
+
+    DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5");
+    cons5.addSelector("car", x);
+    cons5.addSelector("cdr", urListListX);
+    list5.addConstructor(cons5);
+    DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5");
+    list5.addConstructor(nil5);
+
+    dtdecls.clear();
+    dtdecls.add(list5);
+
+    // well-founded and has nested recursion
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 1);
+    assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
+    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
+  }
+
+  @Test void datatypeSpecializedCons() throws CVC5ApiException
+  {
+    /* Create mutual datatypes corresponding to this definition block:
+     *   DATATYPE
+     *     plist[X] = pcons(car: X, cdr: plist[X]) | pnil
+     *   END;
+     */
+    // Make unresolved types as placeholders
+    Set<Sort> unresTypes = new HashSet<>();
+    Sort unresList = d_solver.mkSortConstructorSort("plist", 1);
+    unresTypes.add(unresList);
+
+    List<Sort> v = new ArrayList<>();
+    Sort x = d_solver.mkParamSort("X");
+    v.add(x);
+    DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v);
+
+    List<Sort> args = new ArrayList<>();
+    args.add(x);
+    Sort urListX = unresList.instantiate(args);
+
+    DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons");
+    pcons.addSelector("car", x);
+    pcons.addSelector("cdr", urListX);
+    plist.addConstructor(pcons);
+    DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil");
+    plist.addConstructor(nil5);
+
+    List<DatatypeDecl> dtdecls = new ArrayList<>();
+    dtdecls.add(plist);
+
+    // make the datatype sorts
+    AtomicReference<List<Sort>> atomic = new AtomicReference<>();
+    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes)));
+    List<Sort> dtsorts = atomic.get();
+    assertEquals(dtsorts.size(), 1);
+    Datatype d = dtsorts.get(0).getDatatype();
+    DatatypeConstructor nilc = d.getConstructor(0);
+
+    Sort isort = d_solver.getIntegerSort();
+    List<Sort> iargs = new ArrayList<>();
+    iargs.add(isort);
+    Sort listInt = dtsorts.get(0).instantiate(iargs);
+
+    AtomicReference<Term> atomicTerm = new AtomicReference<>();
+    // get the specialized constructor term for list[Int]
+    assertDoesNotThrow(() -> atomicTerm.set(nilc.getSpecializedConstructorTerm(listInt)));
+    Term testConsTerm = atomicTerm.get();
+    assertNotEquals(testConsTerm, nilc.getConstructorTerm());
+    // error to get the specialized constructor term for Int
+    assertThrows(CVC5ApiException.class, () -> nilc.getSpecializedConstructorTerm(isort));
+  }
+}