From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 8 Sep 2021 08:25:23 +0000 (-0500)
Subject: Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, Dataty... 
X-Git-Tag: cvc5-1.0.0~1262
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44e45c450f5bf41f9fe6077437e9c3fc371868f6;p=cvc5.git

Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java (#6390)

Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files
---

diff --git a/src/api/java/cvc5/DatatypeConstructor.java b/src/api/java/cvc5/DatatypeConstructor.java
new file mode 100644
index 000000000..eb489456b
--- /dev/null
+++ b/src/api/java/cvc5/DatatypeConstructor.java
@@ -0,0 +1,162 @@
+/******************************************************************************
+ * 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 DatatypeConstructor extends AbstractPointer
+{
+  // region construction and destruction
+  DatatypeConstructor(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
+
+  /** @return the name of this Datatype constructor. */
+  String getName()
+  {
+    return getName(pointer);
+  }
+
+  private native String getName(long pointer);
+
+  /**
+   * Get the constructor operator of this datatype constructor.
+   * @return the constructor term
+   */
+  Term getConstructorTerm()
+  {
+    long termPointer = getConstructorTerm(pointer);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getConstructorTerm(long pointer);
+
+  /**
+   * Get the constructor operator of this datatype constructor whose return
+   * type is retSort. This method is intended to be used on constructors of
+   * parametric datatypes and can be seen as returning the constructor
+   * term that has been explicitly cast to the given sort.
+   *
+   * This method is required for constructors of parametric datatypes whose
+   * return type cannot be determined by type inference. For example, given:
+   *   (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+   * The type of nil terms need to be provided by the user. In SMT version 2.6,
+   * this is done via the syntax for qualified identifiers:
+   *   (as nil (List Int))
+   * This method is equivalent of applying the above, where this
+   * DatatypeConstructor is the one corresponding to nil, and retSort is
+   * (List Int).
+   *
+   * Furthermore note that the returned constructor term t is an operator,
+   * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
+   * (nullary) application of nil.
+   *
+   * @param retSort the desired return sort of the constructor
+   * @return the constructor term
+   */
+  Term getSpecializedConstructorTerm(Sort retSort)
+  {
+    long termPointer = getSpecializedConstructorTerm(pointer, retSort.getPointer());
+    return new Term(solver, termPointer);
+  }
+
+  private native long getSpecializedConstructorTerm(long pointer, long retSortPointer);
+
+  /**
+   * Get the tester operator of this datatype constructor.
+   * @return the tester operator
+   */
+  Term getTesterTerm()
+  {
+    long termPointer = getTesterTerm(pointer);
+    return new Term(solver, termPointer);
+  }
+  private native long getTesterTerm(long pointer);
+
+  /**
+   * @return the number of selectors (so far) of this Datatype constructor.
+   */
+  int getNumSelectors()
+  {
+    return getNumSelectors(pointer);
+  }
+  private native int getNumSelectors(long pointer);
+
+  /** @return the i^th DatatypeSelector. */
+  public DatatypeSelector getSelector(int index)
+  {
+    long selectorPointer = getSelector(pointer, index);
+    return new DatatypeSelector(solver, selectorPointer);
+  }
+  private native long getSelector(long pointer, int index);
+
+  /**
+   * Get the datatype selector with the given name.
+   * This is a linear search through the selectors, so in case of
+   * multiple, similarly-named selectors, the first is returned.
+   * @param name the name of the datatype selector
+   * @return the first 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);
+
+  /**
+   * Get the term representation of the datatype selector with the given name.
+   * This is a linear search through the arguments, so in case of multiple,
+   * similarly-named arguments, the selector for the first is returned.
+   * @param name the name of the datatype selector
+   * @return a term representing the datatype selector with the given name
+   */
+  Term getSelectorTerm(String name)
+  {
+    long termPointer = getSelectorTerm(pointer, name);
+    return new Term(solver, termPointer);
+  }
+  private native long getSelectorTerm(long pointer, String name);
+
+  /**
+   * @return true if this DatatypeConstructor is a null object
+   */
+  boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * @return a string representation of this datatype constructor
+   */
+  protected native String toString(long pointer);
+}
diff --git a/src/api/java/cvc5/DatatypeConstructorDecl.java b/src/api/java/cvc5/DatatypeConstructorDecl.java
new file mode 100644
index 000000000..8c1cfed7d
--- /dev/null
+++ b/src/api/java/cvc5/DatatypeConstructorDecl.java
@@ -0,0 +1,78 @@
+/******************************************************************************
+ * 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 DatatypeConstructorDecl extends AbstractPointer
+{
+  // region construction and destruction
+  DatatypeConstructorDecl(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
+
+  /**
+   * Add datatype selector declaration.
+   * @param name the name of the datatype selector declaration to add
+   * @param sort the range sort of the datatype selector declaration to add
+   */
+  public void addSelector(String name, Sort sort)
+  {
+    addSelector(pointer, name, sort.getPointer());
+  }
+
+  private native void addSelector(long pointer, String name, long sortPointer);
+
+  /**
+   * Add datatype selector declaration whose range type is the datatype itself.
+   * @param name the name of the datatype selector declaration to add
+   */
+  public void addSelectorSelf(String name)
+  {
+    addSelectorSelf(pointer, name);
+  }
+
+  private native void addSelectorSelf(long pointer, String name);
+
+  /**
+   * @return true if this DatatypeConstructorDecl is a null declaration.
+   */
+  public boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * @return a string representation of this datatype constructor declaration
+   */
+  protected native String toString(long pointer);
+}
diff --git a/src/api/java/cvc5/DatatypeDecl.java b/src/api/java/cvc5/DatatypeDecl.java
new file mode 100644
index 000000000..4be50f92f
--- /dev/null
+++ b/src/api/java/cvc5/DatatypeDecl.java
@@ -0,0 +1,89 @@
+/******************************************************************************
+ * 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 DatatypeDecl extends AbstractPointer
+{
+  // region construction and destruction
+  DatatypeDecl(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
+  /**
+   * Add datatype constructor declaration.
+   * @param ctor the datatype constructor declaration to add
+   */
+  public void addConstructor(DatatypeConstructorDecl ctor)
+  {
+    addConstructor(pointer, ctor.getPointer());
+  }
+
+  private native void addConstructor(long pointer, long declPointer);
+
+  /** Get the number of constructors (so far) for this Datatype declaration. */
+  int getNumConstructors()
+  {
+    return getNumConstructors(pointer);
+  }
+
+  private native int getNumConstructors(long pointer);
+
+  /** Is this Datatype declaration parametric? */
+  public boolean isParametric()
+  {
+    return isParametric(pointer);
+  }
+
+  private native boolean isParametric(long pointer);
+
+  /**
+   * @return true if this DatatypeDecl is a null object
+   */
+  public boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * @return a string representation of this datatype declaration
+   */
+  protected native String toString(long pointer);
+
+  /** @return the name of this datatype declaration. */
+  public String getName()
+  {
+    return getName(pointer);
+  }
+
+  private native String getName(long pointer);
+}
diff --git a/src/api/java/cvc5/DatatypeSelector.java b/src/api/java/cvc5/DatatypeSelector.java
new file mode 100644
index 000000000..b4e9fd6b6
--- /dev/null
+++ b/src/api/java/cvc5/DatatypeSelector.java
@@ -0,0 +1,96 @@
+/******************************************************************************
+ * 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 DatatypeSelector extends AbstractPointer
+{
+  // region construction and destruction
+  DatatypeSelector(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
+
+  /** @return the name of this Datatype selector. */
+  String getName()
+  {
+    return getName(pointer);
+  }
+
+  private native String getName(long pointer);
+
+  /**
+   * Get the selector operator of this datatype selector.
+   * @return the selector term
+   */
+  public Term getSelectorTerm()
+  {
+    long termPointer = getSelectorTerm(pointer);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getSelectorTerm(long pointer);
+
+  /**
+   * Get the upater operator of this datatype selector.
+   * @return the updater term
+   */
+  public Term getUpdaterTerm()
+  {
+    long termPointer = getUpdaterTerm(pointer);
+    return new Term(solver, termPointer);
+  }
+
+  private native long getUpdaterTerm(long pointer);
+
+  /** @return the range sort of this argument. */
+  Sort getRangeSort()
+  {
+    long sortPointer = getRangeSort(pointer);
+    return new Sort(solver, sortPointer);
+  }
+
+  private native long getRangeSort(long pointer);
+
+  /**
+   * @return true if this DatatypeSelector is a null object
+   */
+  public boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * @return a string representation of this datatype selector
+   */
+  protected native String toString(long pointer);
+}
diff --git a/src/api/java/jni/cvc5_DatatypeConstructor.cpp b/src/api/java/jni/cvc5_DatatypeConstructor.cpp
new file mode 100644
index 000000000..63aed366d
--- /dev/null
+++ b/src/api/java/jni/cvc5_DatatypeConstructor.cpp
@@ -0,0 +1,194 @@
+/******************************************************************************
+ * 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_DatatypeConstructor.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL
+Java_cvc5_DatatypeConstructor_deletePointer(JNIEnv*, jclass, jlong pointer)
+{
+  delete ((DatatypeConstructor*)pointer);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeConstructor_getName(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  return env->NewStringUTF(current->getName().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getConstructorTerm
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getConstructorTerm(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  Term* retPointer = new Term(current->getConstructorTerm());
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getSpecializedConstructorTerm
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_DatatypeConstructor_getSpecializedConstructorTerm(
+    JNIEnv* env, jobject, jlong pointer, jlong retSortPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  Sort* sort = (Sort*)retSortPointer;
+  Term* retPointer = new Term(current->getSpecializedConstructorTerm(*sort));
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getTesterTerm
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_DatatypeConstructor_getTesterTerm(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  Term* retPointer = new Term(current->getTesterTerm());
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getNumSelectors
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_DatatypeConstructor_getNumSelectors(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  return (jint)current->getNumSelectors();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getSelector
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelector__JI(
+    JNIEnv* env, jobject, jlong pointer, jint index)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  DatatypeSelector* retPointer =
+      new DatatypeSelector(current->operator[]((size_t)index));
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getSelector
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_DatatypeConstructor_getSelector__JLjava_lang_String_2(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer,
+                                                                jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  DatatypeSelector* retPointer =
+      new DatatypeSelector(current->operator[](cName));
+  env->ReleaseStringUTFChars(jName, s);
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    getSelectorTerm
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelectorTerm(
+    JNIEnv* env, jobject, jlong pointer, jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  Term* retPointer = new Term(current->getSelectorTerm(cName));
+  env->ReleaseStringUTFChars(jName, s);
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeConstructor_isNull(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructor
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeConstructor_toString(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp b/src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp
new file mode 100644
index 000000000..ce3c69585
--- /dev/null
+++ b/src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp
@@ -0,0 +1,95 @@
+/******************************************************************************
+ * 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_DatatypeConstructorDecl.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_DatatypeConstructorDecl
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL
+Java_cvc5_DatatypeConstructorDecl_deletePointer(JNIEnv*, jclass, jlong pointer)
+{
+  delete ((DatatypeConstructorDecl*)pointer);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructorDecl
+ * Method:    addSelector
+ * Signature: (JLjava/lang/String;J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelector(
+    JNIEnv* env, jobject, jlong pointer, jstring jName, jlong sortPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  Sort* sort = (Sort*)sortPointer;
+  current->addSelector(cName, *sort);
+  env->ReleaseStringUTFChars(jName, s);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructorDecl
+ * Method:    addSelectorSelf
+ * Signature: (JLjava/lang/String;)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelectorSelf(
+    JNIEnv* env, jobject, jlong pointer, jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  current->addSelectorSelf(cName);
+  env->ReleaseStringUTFChars(jName, s);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructorDecl
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL
+Java_cvc5_DatatypeConstructorDecl_isNull(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_DatatypeConstructorDecl
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL
+Java_cvc5_DatatypeConstructorDecl_toString(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/src/api/java/jni/cvc5_DatatypeDecl.cpp b/src/api/java/jni/cvc5_DatatypeDecl.cpp
new file mode 100644
index 000000000..b68c37842
--- /dev/null
+++ b/src/api/java/jni/cvc5_DatatypeDecl.cpp
@@ -0,0 +1,125 @@
+/******************************************************************************
+ * 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_DatatypeDecl.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_DatatypeDecl_deletePointer(JNIEnv*,
+                                                            jclass,
+                                                            jlong pointer)
+{
+  delete ((DatatypeDecl*)pointer);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    addConstructor
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_DatatypeDecl_addConstructor(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer,
+                                                             jlong declPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  DatatypeConstructorDecl* decl = (DatatypeConstructorDecl*)declPointer;
+  current->addConstructor(*decl);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    getNumConstructors
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_DatatypeDecl_getNumConstructors(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  return (jint)current->getNumConstructors();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    isParametric
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isParametric(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  return (jboolean)current->isParametric();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isNull(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeDecl_toString(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_DatatypeDecl
+ * Method:    getName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeDecl_getName(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeDecl* current = (DatatypeDecl*)pointer;
+  return env->NewStringUTF(current->getName().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/src/api/java/jni/cvc5_DatatypeSelector.cpp b/src/api/java/jni/cvc5_DatatypeSelector.cpp
new file mode 100644
index 000000000..fee0b33a4
--- /dev/null
+++ b/src/api/java/jni/cvc5_DatatypeSelector.cpp
@@ -0,0 +1,125 @@
+/******************************************************************************
+ * 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_DatatypeSelector.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_DatatypeSelector_deletePointer(JNIEnv*,
+                                                                jclass,
+                                                                jlong pointer)
+{
+  delete ((DatatypeSelector*)pointer);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    getName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeSelector_getName(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  return env->NewStringUTF(current->getName().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    getSelectorTerm
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_cvc5_DatatypeSelector_getSelectorTerm(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  Term* retPointer = new Term(current->getSelectorTerm());
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    getUpdaterTerm
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getUpdaterTerm(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  Term* retPointer = new Term(current->getUpdaterTerm());
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    getRangeSort
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getRangeSort(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  Sort* retPointer = new Sort(current->getRangeSort());
+  return (jlong)retPointer;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeSelector_isNull(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_DatatypeSelector
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_DatatypeSelector_toString(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  DatatypeSelector* current = (DatatypeSelector*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}