summaryrefslogtreecommitdiff
path: root/src/api/java
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/java')
-rw-r--r--src/api/java/CMakeLists.txt7
-rw-r--r--src/api/java/cvc5/CVC5ApiOptionException.java24
-rw-r--r--src/api/java/cvc5/DatatypeSelector.java2
-rw-r--r--src/api/java/cvc5/OptionInfo.java209
-rw-r--r--src/api/java/cvc5/Solver.java133
-rw-r--r--src/api/java/cvc5/Sort.java18
-rw-r--r--src/api/java/jni/cvc5JavaApi.cpp52
-rw-r--r--src/api/java/jni/cvc5JavaApi.h86
-rw-r--r--src/api/java/jni/cvc5_OptionInfo.cpp351
-rw-r--r--src/api/java/jni/cvc5_Solver.cpp159
-rw-r--r--src/api/java/jni/cvc5_Sort.cpp28
11 files changed, 1024 insertions, 45 deletions
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index d6759ba6e..df35390ea 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -50,6 +50,7 @@ include(UseJava)
set(JAVA_FILES
${CMAKE_CURRENT_LIST_DIR}/cvc5/AbstractPointer.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiException.java
+ ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiOptionException.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiRecoverableException.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/Datatype.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeConstructor.java
@@ -59,6 +60,7 @@ set(JAVA_FILES
${CMAKE_CURRENT_LIST_DIR}/cvc5/Grammar.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/IPointer.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/Op.java
+ ${CMAKE_CURRENT_LIST_DIR}/cvc5/OptionInfo.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/Pair.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/Result.java
${CMAKE_CURRENT_LIST_DIR}/cvc5/RoundingMode.java
@@ -115,12 +117,15 @@ add_library(cvc5jni SHARED
jni/cvc5_DatatypeSelector.cpp
jni/cvc5_Grammar.cpp
jni/cvc5_Op.cpp
+ jni/cvc5_OptionInfo.cpp
jni/cvc5_Result.cpp
jni/cvc5_Solver.cpp
jni/cvc5_Sort.cpp
jni/cvc5_Stat.cpp
jni/cvc5_Statistics.cpp
- jni/cvc5_Term.cpp)
+ jni/cvc5_Term.cpp
+ jni/cvc5JavaApi.cpp)
+
add_dependencies(cvc5jni generate-jni-headers)
target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS})
diff --git a/src/api/java/cvc5/CVC5ApiOptionException.java b/src/api/java/cvc5/CVC5ApiOptionException.java
new file mode 100644
index 000000000..e792091e1
--- /dev/null
+++ b/src/api/java/cvc5/CVC5ApiOptionException.java
@@ -0,0 +1,24 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer, 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 CVC5ApiOptionException extends CVC5ApiRecoverableException
+{
+ public CVC5ApiOptionException(String message)
+ {
+ super(message);
+ }
+}
diff --git a/src/api/java/cvc5/DatatypeSelector.java b/src/api/java/cvc5/DatatypeSelector.java
index 77136173e..014c35de0 100644
--- a/src/api/java/cvc5/DatatypeSelector.java
+++ b/src/api/java/cvc5/DatatypeSelector.java
@@ -69,7 +69,7 @@ public class DatatypeSelector extends AbstractPointer
private native long getUpdaterTerm(long pointer);
- /** @return the range sort of this argument. */
+ /** @return the range sort of this selector. */
Sort getRangeSort()
{
long sortPointer = getRangeSort(pointer);
diff --git a/src/api/java/cvc5/OptionInfo.java b/src/api/java/cvc5/OptionInfo.java
new file mode 100644
index 000000000..7690a1bc1
--- /dev/null
+++ b/src/api/java/cvc5/OptionInfo.java
@@ -0,0 +1,209 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer, 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;
+
+import java.math.BigInteger;
+
+/**
+ * Holds some description about a particular option, including its name, its
+ * aliases, whether the option was explicitly set by the user, and information
+ * concerning its value. The `valueInfo` member holds any of the following
+ * alternatives:
+ * - VoidInfo if the option holds no value (or the value has no native type)
+ * - ValueInfo if the option is of type boolean or String, holds the
+ * current value and the default value.
+ * - NumberInfo if the option is of type BigInteger or double, holds
+ * the current and default value, as well as the minimum and maximum.
+ * - ModeInfo if the option is a mode option, holds the current and default
+ * values, as well as a list of valid modes.
+ * Additionally, this class provides convenience functions to obtain the
+ * current value of an option in a type-safe manner using boolValue(),
+ * stringValue(), intValue(), and doubleValue(). They assert that
+ * the option has the respective type and return the current value.
+ */
+public class OptionInfo extends AbstractPointer
+{
+ // region construction and destruction
+ OptionInfo(Solver solver, long pointer)
+ {
+ super(solver, pointer);
+ this.name = getName(pointer);
+ this.aliases = getAliases(pointer);
+ this.setByUser = getSetByUser(pointer);
+ this.baseInfo = getBaseInfo(pointer);
+ }
+
+ protected static native void deletePointer(long pointer);
+
+ public long getPointer()
+ {
+ return pointer;
+ }
+
+ @Override public void finalize()
+ {
+ deletePointer(pointer);
+ }
+
+ /**
+ * @return a string representation of this optionInfo.
+ */
+ protected native String toString(long pointer);
+
+ // endregion
+
+ /** Abstract class for OptionInfo values */
+ abstract class BaseInfo
+ {
+ }
+
+ /** Has the current and the default value */
+ public abstract class ValueInfo<T> extends BaseInfo
+ {
+ private final T defaultValue;
+ private final T currentValue;
+ public ValueInfo(T defaultValue, T currentValue)
+ {
+ this.defaultValue = defaultValue;
+ this.currentValue = currentValue;
+ }
+ public T getDefaultValue()
+ {
+ return defaultValue;
+ }
+ public T getCurrentValue()
+ {
+ return currentValue;
+ }
+ }
+
+ public class ModeInfo extends ValueInfo<String>
+ {
+ private final String[] modes;
+
+ public ModeInfo(String defaultValue, String currentValue, String[] modes)
+ {
+ super(defaultValue, currentValue);
+ this.modes = modes;
+ }
+ public String[] getModes()
+ {
+ return modes;
+ }
+ }
+
+ /** Has no value information */
+ public class VoidInfo extends BaseInfo
+ {
+ }
+
+ /** Default value, current value, minimum and maximum of a numeric value */
+ public class NumberInfo<T> extends ValueInfo<T>
+ {
+ private final T minimum;
+ private final T maximum;
+ public NumberInfo(T defaultValue, T currentValue, T minimum, T maximum)
+ {
+ super(defaultValue, currentValue);
+ this.minimum = minimum;
+ this.maximum = maximum;
+ }
+ public T getMinimum()
+ {
+ return minimum;
+ }
+ public T getMaximum()
+ {
+ return maximum;
+ }
+ }
+
+ private native String getName(long pointer);
+
+ private native String[] getAliases(long pointer);
+
+ private native boolean getSetByUser(long pointer);
+
+ private native BaseInfo getBaseInfo(long pointer);
+
+ /** The option name */
+ private final String name;
+ public String getName()
+ {
+ return name;
+ }
+ /** The option name aliases */
+ private final String[] aliases;
+ public String[] getAliases()
+ {
+ return aliases;
+ }
+ /** Whether the option was explicitly set by the user */
+ private final boolean setByUser;
+ public boolean getSetByUser()
+ {
+ return setByUser;
+ }
+
+ /** The option variant information */
+ private final BaseInfo baseInfo;
+ public BaseInfo getBaseInfo()
+ {
+ return baseInfo;
+ }
+
+ /**
+ * Obtain the current value as a boolean. Asserts that valueInfo holds a boolean.
+ */
+ public boolean booleanValue()
+ {
+ return booleanValue(pointer);
+ }
+
+ private native boolean booleanValue(long pointer);
+
+ /**
+ * Obtain the current value as a string. Asserts that valueInfo holds a
+ * string.
+ */
+ public String stringValue()
+ {
+ return stringValue(pointer);
+ }
+
+ private native String stringValue(long pointer);
+
+ /**
+ * Obtain the current value as as int. Asserts that valueInfo holds an int.
+ */
+ public BigInteger intValue()
+ {
+ return intValue(pointer);
+ }
+
+ private native BigInteger intValue(long pointer);
+
+ /**
+ * Obtain the current value as a double. Asserts that valueInfo holds a
+ * double.
+ */
+ public double doubleValue()
+ {
+ return doubleValue(pointer);
+ }
+
+ private native double doubleValue(long pointer);
+};
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index b0bee500c..cc5797570 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -882,6 +882,18 @@ public class Solver implements IPointer
private native long mkEmptyBag(long pointer, long sortPointer);
/**
+ * Create a separation logic empty term.
+ * @return the separation logic empty term
+ */
+ public Term mkSepEmp()
+ {
+ long termPointer = mkSepEmp(pointer);
+ return new Term(this, termPointer);
+ }
+
+ private native long mkSepEmp(long pointer);
+
+ /**
* Create a separation logic nil term.
* @param sort the sort of the nil term
* @return the separation logic nil term
@@ -1794,6 +1806,31 @@ public class Solver implements IPointer
private native String getOption(long pointer, String option);
/**
+ * Get all option names that can be used with `setOption`, `getOption` and
+ * `getOptionInfo`.
+ * @return all option names
+ */
+ public String[] getOptionNames()
+ {
+ return getOptionNames(pointer);
+ }
+
+ private native String[] getOptionNames(long pointer);
+
+ /**
+ * Get some information about the given option. Check the `OptionInfo` class
+ * for more details on which information is available.
+ * @return information about the given option
+ */
+ public OptionInfo getOptionInfo(String option)
+ {
+ long optionPointer = getOptionInfo(pointer, option);
+ return new OptionInfo(this, optionPointer);
+ }
+
+ private native long getOptionInfo(long pointer, String option);
+
+ /**
* Get the set of unsat ("failed") assumptions.
* SMT-LIB:
* {@code
@@ -1828,7 +1865,47 @@ public class Solver implements IPointer
private native long[] getUnsatCore(long pointer);
/**
- * Get the value of the given term.
+ * Get a difficulty estimate for an asserted formula. This method is
+ * intended to be called immediately after any response to a checkSat.
+ *
+ * @return a map from (a subset of) the input assertions to a real value that
+ * is an estimate of how difficult each assertion was to solve. Unmentioned
+ * assertions can be assumed to have zero difficulty.
+ */
+ public Map<Term, Term> getDifficulty()
+ {
+ Map<Long, Long> map = getDifficulty(pointer);
+ Map<Term, Term> ret = new HashMap<>();
+ for (Map.Entry<Long, Long> entry : map.entrySet())
+ {
+ Term key = new Term(this, entry.getKey());
+ Term value = new Term(this, entry.getValue());
+ ret.put(key, value);
+ }
+ return ret;
+ }
+
+ private native Map<Long, Long> getDifficulty(long pointer);
+
+ /**
+ * Get the refutation proof
+ * SMT-LIB:
+ * {@code
+ * ( get-proof )
+ * }
+ * Requires to enable option 'produce-proofs'.
+ * @return a string representing the proof, according to the value of
+ * proof-format-mode.
+ */
+ public String getProof()
+ {
+ return getProof(pointer);
+ }
+
+ private native String getProof(long pointer);
+
+ /**
+ * Get the value of the given term in the current model.
* SMT-LIB:
* {@code
* ( get-value ( <term> ) )
@@ -1845,7 +1922,7 @@ public class Solver implements IPointer
private native long getValue(long pointer, long termPointer);
/**
- * Get the values of the given terms.
+ * Get the values of the given terms in the current model.
* SMT-LIB:
* {@code
* ( get-value ( <term>+ ) )
@@ -1863,6 +1940,22 @@ public class Solver implements IPointer
private native long[] getValue(long pointer, long[] termPointers);
/**
+ * Get the domain elements of uninterpreted sort s in the current model. The
+ * current model interprets s as the finite sort whose domain elements are
+ * given in the return value of this method.
+ *
+ * @param s The uninterpreted sort in question
+ * @return the domain elements of s in the current model
+ */
+ public Term[] getModelDomainElements(Sort s)
+ {
+ long[] pointers = getModelDomainElements(pointer, s.getPointer());
+ return Utils.getTerms(this, pointers);
+ }
+
+ private native long[] getModelDomainElements(long pointer, long sortPointer);
+
+ /**
* This returns false if the model value of free constant v was not essential
* for showing the satisfiability of the last call to checkSat using the
* current model. This method will only return false (for any v) if
@@ -2000,6 +2093,26 @@ public class Solver implements IPointer
private native long getSeparationNilTerm(long pointer);
/**
+ * Declare a symbolic pool of terms with the given initial value.
+ * SMT-LIB:
+ * {@code
+ * ( declare-pool <symbol> <sort> ( <term>* ) )
+ * }
+ * @param symbol The name of the pool
+ * @param sort The sort of the elements of the pool.
+ * @param initValue The initial value of the pool
+ */
+ public Term declarePool(String symbol, Sort sort, Term[] initValue)
+ {
+ long[] termPointers = Utils.getPointers(initValue);
+ long termPointer = declarePool(pointer, symbol, sort.getPointer(), termPointers);
+ return new Term(this, termPointer);
+ }
+
+ private native long declarePool(
+ long pointer, String symbol, long sortPointer, long[] termPointers);
+
+ /**
* Pop a level from the assertion stack.
* SMT-LIB:
* {@code
@@ -2398,6 +2511,22 @@ public class Solver implements IPointer
}
private native void addSygusConstraint(long pointer, long termPointer);
+
+ /**
+ * Add a forumla to the set of Sygus assumptions.
+ * SyGuS v2:
+ * {@code
+ * ( assume <term> )
+ * }
+ * @param term the formula to add as an assumption
+ */
+ public void addSygusAssume(Term term)
+ {
+ addSygusAssume(pointer, term.getPointer());
+ }
+
+ private native void addSygusAssume(long pointer, long termPointer);
+
/**
* Add a set of Sygus constraints to the current state that correspond to an
* invariant synthesis problem.
diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java
index f1f541e35..434c07424 100644
--- a/src/api/java/cvc5/Sort.java
+++ b/src/api/java/cvc5/Sort.java
@@ -725,34 +725,34 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
/**
* @return the bit-width of the bit-vector sort
*/
- public int getBVSize()
+ public int getBitVectorSize()
{
- return getBVSize(pointer);
+ return getBitVectorSize(pointer);
}
- private native int getBVSize(long pointer);
+ private native int getBitVectorSize(long pointer);
/* Floating-point sort ------------------------------------------------- */
/**
* @return the bit-width of the exponent of the floating-point sort
*/
- public int getFPExponentSize()
+ public int getFloatingPointExponentSize()
{
- return getFPExponentSize(pointer);
+ return getFloatingPointExponentSize(pointer);
}
- private native int getFPExponentSize(long pointer);
+ private native int getFloatingPointExponentSize(long pointer);
/**
* @return the width of the significand of the floating-point sort
*/
- public int getFPSignificandSize()
+ public int getFloatingPointSignificandSize()
{
- return getFPSignificandSize(pointer);
+ return getFloatingPointSignificandSize(pointer);
}
- private native int getFPSignificandSize(long pointer);
+ private native int getFloatingPointSignificandSize(long pointer);
/* Datatype sort ------------------------------------------------------- */
diff --git a/src/api/java/jni/cvc5JavaApi.cpp b/src/api/java/jni/cvc5JavaApi.cpp
new file mode 100644
index 000000000..378fa0948
--- /dev/null
+++ b/src/api/java/jni/cvc5JavaApi.cpp
@@ -0,0 +1,52 @@
+/******************************************************************************
+ * 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 "cvc5JavaApi.h"
+
+#include <string>
+#include <vector>
+
+jobjectArray getStringArrayFromStringVector(
+ JNIEnv* env, const std::vector<std::string>& cStrings)
+{
+ jclass stringClass = env->FindClass("java/lang/String");
+ jobjectArray ret =
+ env->NewObjectArray(cStrings.size(), stringClass, env->NewStringUTF(""));
+ for (size_t i = 0; i < cStrings.size(); i++)
+ {
+ jstring jString = env->NewStringUTF(cStrings[i].c_str());
+ env->SetObjectArrayElement(ret, i, jString);
+ }
+ return ret;
+}
+
+jobject getDoubleObject(JNIEnv* env, double cValue)
+{
+ jdouble jValue = static_cast<jdouble>(cValue);
+ jclass doubleClass = env->FindClass("java/lang/Double");
+ jmethodID methodId = env->GetMethodID(doubleClass, "<init>", "(D)V");
+ jobject ret = env->NewObject(doubleClass, methodId, jValue);
+ return ret;
+}
+
+jobject getBooleanObject(JNIEnv* env, bool cValue)
+{
+ jboolean jValue = static_cast<jboolean>(cValue);
+ jclass booleanClass = env->FindClass("Ljava/lang/Boolean;");
+ jmethodID booleanConstructor =
+ env->GetMethodID(booleanClass, "<init>", "(Z)V");
+ jobject ret = env->NewObject(booleanClass, booleanConstructor, jValue);
+ return ret;
+} \ No newline at end of file
diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h
index 7b550ef28..73f2fb396 100644
--- a/src/api/java/jni/cvc5JavaApi.h
+++ b/src/api/java/jni/cvc5JavaApi.h
@@ -13,31 +13,38 @@
* The cvc5 Java API.
*/
-#include <jni.h>
-
#ifndef CVC5__JAVA_API_H
#define CVC5__JAVA_API_H
+#include <jni.h>
+
+#include <string>
+#include <vector>
+
#define CVC5_JAVA_API_TRY_CATCH_BEGIN \
try \
{
-#define CVC5_JAVA_API_TRY_CATCH_END(env) \
- } \
- catch (const CVC5ApiRecoverableException& e) \
- { \
- jclass exceptionClass = \
- env->FindClass("cvc5/CVC5ApiRecoverableException"); \
- env->ThrowNew(exceptionClass, e.what()); \
- } \
- catch (const CVC5ApiException& e) \
- { \
- jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \
- env->ThrowNew(exceptionClass, e.what()); \
+#define CVC5_JAVA_API_TRY_CATCH_END(env) \
+ } \
+ catch (const CVC5ApiOptionException& e) \
+ { \
+ jclass exceptionClass = env->FindClass("cvc5/CVC5ApiOptionException"); \
+ env->ThrowNew(exceptionClass, e.what()); \
+ } \
+ catch (const CVC5ApiRecoverableException& e) \
+ { \
+ jclass exceptionClass = \
+ env->FindClass("cvc5/CVC5ApiRecoverableException"); \
+ env->ThrowNew(exceptionClass, e.what()); \
+ } \
+ catch (const CVC5ApiException& e) \
+ { \
+ jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \
+ env->ThrowNew(exceptionClass, e.what()); \
}
#define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \
CVC5_JAVA_API_TRY_CATCH_END(env) \
return returnValue;
-#endif // CVC5__JAVA_API_H
/**
* Convert pointers coming from Java to cvc5 objects
@@ -83,4 +90,51 @@ jlongArray getPointersFromObjects(JNIEnv* env, const std::vector<T>& objects)
jlongArray ret = env->NewLongArray(objects.size());
env->SetLongArrayRegion(ret, 0, objects.size(), pointers.data());
return ret;
-} \ No newline at end of file
+}
+
+/**
+ * Convert a cpp signed (unsigned) integer to an object of BigInteger class
+ * @tparam T cpp types (int64_t, uint64_t, int32_t, int32_t, etc)
+ * @param env jni environment
+ * @param value cpp integer value
+ * @return an object of java BigInteger
+ */
+template <class T>
+jobject getBigIntegerObject(JNIEnv* env, T value)
+{
+ std::string s = std::to_string(value);
+ jstring javaString = env->NewStringUTF(s.c_str());
+ jclass bigIntegerClass = env->FindClass("java/math/BigInteger");
+ jmethodID bigIntegerConstructor =
+ env->GetMethodID(bigIntegerClass, "<init>", "(Ljava/lang/String;)V");
+ jobject ret =
+ env->NewObject(bigIntegerClass, bigIntegerConstructor, javaString);
+ return ret;
+}
+
+/**
+ * Generate an array of java strings from a vector of cpp strings
+ * @param env jni environment
+ * @param cStrings a vector of strings
+ * @return an array of java strings
+ */
+jobjectArray getStringArrayFromStringVector(
+ JNIEnv* env, const std::vector<std::string>& cStrings);
+
+/**
+ * Generate a Double object from cpp double value
+ * @param env jni environment
+ * @param value
+ * @return a Double object
+ */
+jobject getDoubleObject(JNIEnv* env, double value);
+
+/**
+ * Generate a Boolean object from cpp bool value
+ * @param env jni environment
+ * @param value
+ * @return a Boolean object
+ */
+jobject getBooleanObject(JNIEnv* env, bool value);
+
+#endif // CVC5__JAVA_API_H \ No newline at end of file
diff --git a/src/api/java/jni/cvc5_OptionInfo.cpp b/src/api/java/jni/cvc5_OptionInfo.cpp
new file mode 100644
index 000000000..c4bcc2e04
--- /dev/null
+++ b/src/api/java/jni/cvc5_OptionInfo.cpp
@@ -0,0 +1,351 @@
+/******************************************************************************
+ * 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_OptionInfo.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_OptionInfo_deletePointer(JNIEnv*,
+ jclass,
+ jlong pointer)
+{
+ delete reinterpret_cast<OptionInfo*>(pointer);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_toString(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ std::stringstream ss;
+ ss << *current;
+ return env->NewStringUTF(ss.str().c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: getName
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_getName(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ return env->NewStringUTF(current->name.c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: getAliases
+ * Signature: (J)[Ljava/lang/String;
+ */
+JNIEXPORT jobjectArray JNICALL Java_cvc5_OptionInfo_getAliases(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ jobjectArray ret = getStringArrayFromStringVector(env, current->aliases);
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: getSetByUser
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_OptionInfo_getSetByUser(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ return static_cast<jboolean>(current->setByUser);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/**
+ * Convert OptionInfo::NumberInfo cpp object to OptionInfo.NumberInfo java
+ * object
+ * @tparam T cpp integer types int64_t, uint64_t, etc
+ * @param env jni environment
+ * @param optionInfo a java object for this OptionInfo
+ * @param numberInfoClass the java class for OptionInfo.NumberInfo
+ * @param methodId a constructor for OptionInfo.NumberInfo
+ * @param info the cpp OptionInfo::NumberInfo object
+ * @return a java object of class OptionInfo.NumberInfo<BigInteger>
+ */
+template <typename T>
+jobject getNumberInfoFromInteger(JNIEnv* env,
+ const _jobject* optionInfo,
+ jclass numberInfoClass,
+ jmethodID methodId,
+ const OptionInfo::NumberInfo<T>& info)
+{
+ jobject defaultValue = getBigIntegerObject<T>(env, info.defaultValue);
+ jobject currentValue = getBigIntegerObject<T>(env, info.currentValue);
+ jobject minimum = nullptr;
+ if (info.minimum)
+ {
+ minimum = getBigIntegerObject<T>(env, *info.minimum);
+ }
+ jobject maximum = nullptr;
+ if (info.maximum)
+ {
+ maximum = getBigIntegerObject<T>(env, *info.maximum);
+ }
+ jobject ret = env->NewObject(numberInfoClass,
+ methodId,
+ optionInfo,
+ defaultValue,
+ currentValue,
+ minimum,
+ maximum);
+
+ return ret;
+}
+
+template <typename T>
+jobject getNumberInfoFromInteger(JNIEnv* env,
+ const _jobject* optionInfo,
+ jclass numberInfoClass,
+ jmethodID methodId,
+ const OptionInfo::NumberInfo<int64_t>& info);
+
+template <typename T>
+jobject getNumberInfoFromInteger(JNIEnv* env,
+ const _jobject* optionInfo,
+ jclass numberInfoClass,
+ jmethodID methodId,
+ const OptionInfo::NumberInfo<uint64_t>& info);
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: getBaseInfo
+ * Signature: (J)Lcvc5/BaseInfo;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env,
+ jobject optionInfo,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ std::variant<OptionInfo::VoidInfo,
+ OptionInfo::ValueInfo<bool>,
+ OptionInfo::ValueInfo<std::string>,
+ OptionInfo::NumberInfo<int64_t>,
+ OptionInfo::NumberInfo<uint64_t>,
+ OptionInfo::NumberInfo<double>,
+ OptionInfo::ModeInfo>
+ v = current->valueInfo;
+
+ if (std::holds_alternative<OptionInfo::VoidInfo>(v))
+ {
+ jclass voidInfoClass = env->FindClass("cvc5/OptionInfo$VoidInfo");
+ jmethodID methodId =
+ env->GetMethodID(voidInfoClass, "<init>", "(Lcvc5/OptionInfo;)V");
+ jobject ret = env->NewObject(voidInfoClass, methodId, optionInfo);
+ return ret;
+ }
+
+ if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v)
+ || std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v))
+ {
+ jclass valueInfoClass = env->FindClass("cvc5/OptionInfo$ValueInfo");
+ jmethodID methodId = env->GetMethodID(
+ valueInfoClass,
+ "<init>",
+ "(Lcvc5/OptionInfo;Ljava/lang/Object;Ljava/lang/Object;)V");
+
+ if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v))
+ {
+ auto info = std::get<OptionInfo::ValueInfo<bool>>(v);
+ jobject currentValue = getBooleanObject(env, info.currentValue);
+ jobject defaultValue = getBooleanObject(env, info.defaultValue);
+ jobject ret = env->NewObject(
+ valueInfoClass, methodId, optionInfo, defaultValue, currentValue);
+ return ret;
+ }
+
+ if (std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v))
+ {
+ auto info = std::get<OptionInfo::ValueInfo<std::string>>(v);
+ jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str());
+ jstring currentValue = env->NewStringUTF(info.currentValue.c_str());
+ jobject ret = env->NewObject(
+ valueInfoClass, methodId, optionInfo, defaultValue, currentValue);
+ return ret;
+ }
+ }
+
+ if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v)
+ || std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v)
+ || std::holds_alternative<OptionInfo::NumberInfo<double>>(v))
+ {
+ jclass numberInfoClass = env->FindClass("cvc5/OptionInfo$NumberInfo");
+ jmethodID methodId =
+ env->GetMethodID(numberInfoClass,
+ "<init>",
+ "(Lcvc5/OptionInfo;Ljava/lang/Object;Ljava/lang/"
+ "Object;Ljava/lang/Object;Ljava/lang/Object;)V");
+
+ if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v))
+ {
+ auto info = std::get<OptionInfo::NumberInfo<int64_t>>(v);
+ return getNumberInfoFromInteger(
+ env, optionInfo, numberInfoClass, methodId, info);
+ }
+
+ if (std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v))
+ {
+ auto info = std::get<OptionInfo::NumberInfo<uint64_t>>(v);
+ return getNumberInfoFromInteger(
+ env, optionInfo, numberInfoClass, methodId, info);
+ }
+
+ if (std::holds_alternative<OptionInfo::NumberInfo<double>>(v))
+ {
+ auto info = std::get<OptionInfo::NumberInfo<double>>(v);
+ jobject defaultValue = getDoubleObject(env, info.defaultValue);
+ jobject currentValue = getDoubleObject(env, info.currentValue);
+ jobject minimum = nullptr;
+ if (info.minimum)
+ {
+ minimum = getDoubleObject(env, *info.minimum);
+ }
+ jobject maximum = nullptr;
+ if (info.maximum)
+ {
+ maximum = getDoubleObject(env, *info.maximum);
+ }
+ jobject ret = env->NewObject(numberInfoClass,
+ methodId,
+ optionInfo,
+ defaultValue,
+ currentValue,
+ minimum,
+ maximum);
+ return ret;
+ }
+ }
+
+ if (std::holds_alternative<OptionInfo::ModeInfo>(v))
+ {
+ jclass modeInfoClass = env->FindClass("cvc5/OptionInfo$ModeInfo");
+ jmethodID methodId =
+ env->GetMethodID(modeInfoClass,
+ "<init>",
+ "(Lcvc5/OptionInfo;Ljava/lang/String;Ljava/lang/"
+ "String;[Ljava/lang/String;)V");
+
+ auto info = std::get<OptionInfo::ModeInfo>(v);
+ jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str());
+ jstring currentValue = env->NewStringUTF(info.currentValue.c_str());
+ jobject stringArray = getStringArrayFromStringVector(env, info.modes);
+ jobject ret = env->NewObject(modeInfoClass,
+ methodId,
+ optionInfo,
+ defaultValue,
+ currentValue,
+ stringArray);
+ return ret;
+ }
+
+ return nullptr;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: booleanValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_OptionInfo_booleanValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ return static_cast<jboolean>(current->boolValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: stringValue
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_stringValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ std::string ret = current->stringValue();
+ return env->NewStringUTF(ret.c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: intValue
+ * Signature: (J)Ljava/math/BigInteger;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_intValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ std::int64_t value = current->intValue();
+ jobject ret = getBigIntegerObject<std::int64_t>(env, value);
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_OptionInfo
+ * Method: doubleValue
+ * Signature: (J)D
+ */
+JNIEXPORT jdouble JNICALL Java_cvc5_OptionInfo_doubleValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
+ double ret = current->doubleValue();
+ return static_cast<jdouble>(ret);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jdouble>(0.0));
+}
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index c28ea412f..cdbb48db0 100644
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -1061,6 +1061,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env,
/*
* Class: cvc5_Solver
+ * Method: mkSepEmp
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Term* retPointer = new Term(solver->mkSepEmp());
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Solver
* Method: mkSepNil
* Signature: (JJ)J
*/
@@ -1871,6 +1887,57 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getOption(JNIEnv* env,
/*
* Class: cvc5_Solver
+ * Method: getOptionNames
+ * Signature: (J)[Ljava/lang/String;
+ */
+JNIEXPORT jobjectArray JNICALL Java_cvc5_Solver_getOptionNames(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ std::vector<std::string> options = solver->getOptionNames();
+ jobjectArray ret = getStringArrayFromStringVector(env, options);
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Solver
+ * Method: getOptionInfo
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_getOptionInfo(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jstring jOption)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ std::string cOption(env->GetStringUTFChars(jOption, nullptr));
+ OptionInfo* ret = new OptionInfo(solver->getOptionInfo(cOption));
+ return reinterpret_cast<jlong>(ret);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Solver
+ * Method: getDriverOptions
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_getDriverOptions(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ DriverOptions* ret = new DriverOptions(solver->getDriverOptions());
+ return reinterpret_cast<jlong>(ret);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Solver
* Method: getUnsatAssumptions
* Signature: (J)[J
*/
@@ -1905,6 +1972,62 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatCore(JNIEnv* env,
/*
* Class: cvc5_Solver
+ * Method: getDifficulty
+ * Signature: (J)Ljava/util/Map;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_Solver_getDifficulty(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ std::map<Term, Term> map = solver->getDifficulty();
+ // HashMap hashMap = new HashMap();
+ jclass hashMapClass = env->FindClass("Ljava/util/HashMap;");
+ jmethodID constructor = env->GetMethodID(hashMapClass, "<init>", "()V");
+ jobject hashMap = env->NewObject(hashMapClass, constructor);
+ jmethodID putMethod = env->GetMethodID(
+ hashMapClass,
+ "put",
+ "(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;");
+
+ // Long longObject = new Long(statPointer)
+ jclass longClass = env->FindClass("Ljava/lang/Long;");
+ jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+
+ for (const auto& [k, v] : map)
+ {
+ // hashmap.put(key, value);
+ Term* termKey = new Term(k);
+ Term* termValue = new Term(v);
+ jobject key = env->NewObject(
+ longClass, longConstructor, reinterpret_cast<jlong>(termKey));
+ jobject value = env->NewObject(
+ longClass, longConstructor, reinterpret_cast<jlong>(termValue));
+ env->CallObjectMethod(hashMap, putMethod, key, value);
+ }
+ return hashMap;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Solver
+ * Method: getProof
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Solver_getProof(JNIEnv* env,
+ jobject,
+ jlong pointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ std::string proof = solver->getProof();
+ return env->NewStringUTF(proof.c_str());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class: cvc5_Solver
* Method: getValue
* Signature: (JJ)J
*/
@@ -1940,6 +2063,23 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getValue__J_3J(
/*
* Class: cvc5_Solver
+ * Method: getModelDomainElements
+ * Signature: (JJ)[J
+ */
+JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getModelDomainElements(
+ JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+ std::vector<Term> terms = solver->getModelDomainElements(*sort);
+ jlongArray ret = getPointersFromObjects<Term>(env, terms);
+ return ret;
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class: cvc5_Solver
* Method: isModelCoreSymbol
* Signature: (JJ)Z
*/
@@ -2446,6 +2586,23 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusConstraint(JNIEnv* env,
/*
* Class: cvc5_Solver
+ * Method: addSygusAssume
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusAssume(JNIEnv* env,
+ jobject,
+ jlong pointer,
+ jlong termPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ solver->addSygusAssume(*term);
+ CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
+/*
+ * Class: cvc5_Solver
* Method: addSygusInvConstraint
* Signature: (JJJJJ)V
*/
@@ -2591,4 +2748,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env,
DatatypeDecl* ret = new DatatypeDecl();
return reinterpret_cast<jlong>(ret);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-} \ No newline at end of file
+}
diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp
index a2754f032..36ba81249 100644
--- a/src/api/java/jni/cvc5_Sort.cpp
+++ b/src/api/java/jni/cvc5_Sort.cpp
@@ -978,46 +978,44 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env,
/*
* Class: cvc5_Sort
- * Method: getBVSize
+ * Method: getBitVectorSize
* Signature: (J)I
*/
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env,
- jobject,
- jlong pointer)
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env,
+ jobject,
+ jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Sort* current = reinterpret_cast<Sort*>(pointer);
- return static_cast<jint>(current->getBVSize());
+ return static_cast<jint>(current->getBitVectorSize());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
/*
* Class: cvc5_Sort
- * Method: getFPExponentSize
+ * Method: getFloatingPointExponentSize
* Signature: (J)I
*/
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env,
- jobject,
- jlong pointer)
+JNIEXPORT jint JNICALL
+Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Sort* current = reinterpret_cast<Sort*>(pointer);
- return static_cast<jint>(current->getFPExponentSize());
+ return static_cast<jint>(current->getFloatingPointExponentSize());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
/*
* Class: cvc5_Sort
- * Method: getFPSignificandSize
+ * Method: getFloatingPointSignificandSize
* Signature: (J)I
*/
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env,
- jobject,
- jlong pointer)
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize(
+ JNIEnv* env, jobject, jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Sort* current = reinterpret_cast<Sort*>(pointer);
- return static_cast<jint>(current->getFPSignificandSize());
+ return static_cast<jint>(current->getFloatingPointSignificandSize());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback