Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
projects / cvc5.git / commitdiff