diff options
Diffstat (limited to 'src/api/java')
-rw-r--r-- | src/api/java/CMakeLists.txt | 7 | ||||
-rw-r--r-- | src/api/java/cvc5/CVC5ApiOptionException.java | 24 | ||||
-rw-r--r-- | src/api/java/cvc5/DatatypeSelector.java | 2 | ||||
-rw-r--r-- | src/api/java/cvc5/OptionInfo.java | 209 | ||||
-rw-r--r-- | src/api/java/cvc5/Solver.java | 133 | ||||
-rw-r--r-- | src/api/java/cvc5/Sort.java | 18 | ||||
-rw-r--r-- | src/api/java/jni/cvc5JavaApi.cpp | 52 | ||||
-rw-r--r-- | src/api/java/jni/cvc5JavaApi.h | 86 | ||||
-rw-r--r-- | src/api/java/jni/cvc5_OptionInfo.cpp | 351 | ||||
-rw-r--r-- | src/api/java/jni/cvc5_Solver.cpp | 159 | ||||
-rw-r--r-- | src/api/java/jni/cvc5_Sort.cpp | 28 |
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); } |