From 44e45c450f5bf41f9fe6077437e9c3fc371868f6 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 8 Sep 2021 03:25:23 -0500 Subject: [PATCH] Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java (#6390) Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files --- src/api/java/cvc5/DatatypeConstructor.java | 162 +++++++++++++++ .../java/cvc5/DatatypeConstructorDecl.java | 78 +++++++ src/api/java/cvc5/DatatypeDecl.java | 89 ++++++++ src/api/java/cvc5/DatatypeSelector.java | 96 +++++++++ src/api/java/jni/cvc5_DatatypeConstructor.cpp | 194 ++++++++++++++++++ .../java/jni/cvc5_DatatypeConstructorDecl.cpp | 95 +++++++++ src/api/java/jni/cvc5_DatatypeDecl.cpp | 125 +++++++++++ src/api/java/jni/cvc5_DatatypeSelector.cpp | 125 +++++++++++ 8 files changed, 964 insertions(+) create mode 100644 src/api/java/cvc5/DatatypeConstructor.java create mode 100644 src/api/java/cvc5/DatatypeConstructorDecl.java create mode 100644 src/api/java/cvc5/DatatypeDecl.java create mode 100644 src/api/java/cvc5/DatatypeSelector.java create mode 100644 src/api/java/jni/cvc5_DatatypeConstructor.cpp create mode 100644 src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp create mode 100644 src/api/java/jni/cvc5_DatatypeDecl.cpp create mode 100644 src/api/java/jni/cvc5_DatatypeSelector.cpp 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); +} -- 2.30.2