From 991bef531131336549eccd2446243204f4733c20 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 7 Oct 2021 06:29:28 -0500 Subject: Add missing functions in Term.java (#7297) This adds recent API functions that were added to terms. It also uses BigInteger now for integer terms. --- src/api/java/CMakeLists.txt | 1 + src/api/java/cvc5/AbstractPointer.java | 5 + src/api/java/cvc5/Op.java | 2 +- src/api/java/cvc5/Pair.java | 4 +- src/api/java/cvc5/Solver.java | 13 +- src/api/java/cvc5/Term.java | 358 ++++++++++++++++++------ src/api/java/cvc5/Triplet.java | 41 +++ src/api/java/cvc5/Utils.java | 8 + src/api/java/jni/cvc5JavaApi.h | 2 +- src/api/java/jni/cvc5_Solver.cpp | 16 ++ src/api/java/jni/cvc5_Term.cpp | 483 +++++++++++++++++++++++++++------ 11 files changed, 751 insertions(+), 182 deletions(-) create mode 100644 src/api/java/cvc5/Triplet.java (limited to 'src/api/java') diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 12601f397..95831f33d 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -67,6 +67,7 @@ set(JAVA_FILES ${CMAKE_CURRENT_LIST_DIR}/cvc5/Stat.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/Statistics.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/Term.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Triplet.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java ${JAVA_KIND_FILE} ) diff --git a/src/api/java/cvc5/AbstractPointer.java b/src/api/java/cvc5/AbstractPointer.java index f6cdff8ad..8006b67be 100644 --- a/src/api/java/cvc5/AbstractPointer.java +++ b/src/api/java/cvc5/AbstractPointer.java @@ -25,6 +25,11 @@ abstract class AbstractPointer implements IPointer return pointer; } + public Solver getSolver() + { + return solver; + } + @Override public String toString() { return toString(pointer); diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java index 6819946b6..bf908aff2 100644 --- a/src/api/java/cvc5/Op.java +++ b/src/api/java/cvc5/Op.java @@ -58,7 +58,7 @@ public class Op extends AbstractPointer /** * @return the kind of this operator */ - Kind getKind() + public Kind getKind() { try { diff --git a/src/api/java/cvc5/Pair.java b/src/api/java/cvc5/Pair.java index 19cd3e797..84c9d8efe 100644 --- a/src/api/java/cvc5/Pair.java +++ b/src/api/java/cvc5/Pair.java @@ -34,8 +34,6 @@ public class Pair Pair p = (Pair) pair; - if (!first.equals(p.first)) - return false; - return second.equals(p.second); + return first.equals(p.first) && second.equals(p.second); } } diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java index d295113b0..b0bee500c 100644 --- a/src/api/java/cvc5/Solver.java +++ b/src/api/java/cvc5/Solver.java @@ -2467,10 +2467,17 @@ public class Solver implements IPointer private native long[] getSynthSolutions(long pointer, long[] termPointers); /** - * Print solution for synthesis conjecture to the given output stream. - * @param out the output stream + * Returns a snapshot of the current state of the statistic values of this + * solver. The returned object is completely decoupled from the solver and + * will not change when the solver is used again. */ - // TODO: void printSynthSolution(std::ostream& out) + public Statistics getStatistics() + { + long statisticsPointer = getStatistics(pointer); + return new Statistics(this, statisticsPointer); + } + + private native long getStatistics(long pointer); /** * @return null term diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java index a935e453f..e2c719098 100644 --- a/src/api/java/cvc5/Term.java +++ b/src/api/java/cvc5/Term.java @@ -16,10 +16,12 @@ package cvc5; import java.math.BigInteger; +import java.util.Arrays; +import java.util.HashSet; import java.util.Iterator; import java.util.List; import java.util.NoSuchElementException; -import java.math.BigInteger; +import java.util.Set; public class Term extends AbstractPointer implements Comparable, Iterable { @@ -213,40 +215,6 @@ public class Term extends AbstractPointer implements Comparable, Iterable< private native boolean isNull(long pointer); - /** - * Return the base (element stored at all indices) of a constant array - * throws an exception if the kind is not CONST_ARRAY - * - * @return the base value - */ - public Term getConstArrayBase() - { - long termPointer = getConstArrayBase(pointer); - return new Term(solver, termPointer); - } - - private native long getConstArrayBase(long pointer); - - /** - * Return the elements of a constant sequence - * throws an exception if the kind is not CONST_SEQUENCE - * - * @return the elements of the constant sequence. - */ - public Term[] getConstSequenceElements() - { - long[] termPointers = getConstSequenceElements(pointer); - Term[] terms = new Term[termPointers.length]; - for (int i = 0; i < termPointers.length; i++) - { - terms[i] = new Term(solver, termPointers[i]); - } - - return terms; - } - - private native long[] getConstSequenceElements(long pointer); - /** * Boolean negation. * @@ -346,119 +314,337 @@ public class Term extends AbstractPointer implements Comparable, Iterable< private native long iteTerm(long pointer, long thenPointer, long elsePointer); /** - * @return a string representation of this term + * @return a string representation of this term. */ protected native String toString(long pointer); /** - * @return true if the term is an integer that fits within a Java integer. + * @return true if the term is an integer value. */ - public boolean isInt() + public boolean isIntegerValue() { - return isInt(pointer); + return isIntegerValue(pointer); } - private native boolean isInt(long pointer); + private native boolean isIntegerValue(long pointer); /** - * @return the stored integer as an int. - * Note: Asserts isInt(). + * Asserts isIntegerValue(). + * @return the integer represented by this term. */ - public int getInt() + public BigInteger getIntegerValue() { - return getInt(pointer); + return new BigInteger(getIntegerValue(pointer)); } - private native int getInt(long pointer); + private native String getIntegerValue(long pointer); /** - * @return true if the term is an integer that fits within a Java long. + * @return true if the term is a string constant. */ - public boolean isLong() + public boolean isStringValue() { - return isLong(pointer); + return isStringValue(pointer); } - private native boolean isLong(long pointer); + private native boolean isStringValue(long pointer); /** - * @return the stored integer as a long. - * Note: Asserts isLong(). + * @return the stored string constant. + *

+ * Note: This method is not to be confused with toString() which returns the + * term in some string representation, whatever data it may hold. + * Asserts isString(). */ - public long getLong() + public String getStringValue() { - return getLong(pointer); + return getStringValue(pointer); } - private native long getLong(long pointer); + private native String getStringValue(long pointer); /** - * @return true if the term is an integer. + * @return true if the term is a rational value. */ - public boolean isInteger() + public boolean isRealValue() { - return isInteger(pointer); + return isRealValue(pointer); } - private native boolean isInteger(long pointer); + private native boolean isRealValue(long pointer); /** - * @return the stored integer in (decimal) string representation. - * Note: Asserts isInteger(). + * Asserts isRealValue(). + * @return the representation of a rational value as a pair of its numerator + * and denominator. */ - public String getInteger() + public Pair getRealValue() { - return getInteger(pointer); + String rational = getRealValue(pointer); + return Utils.getRational(rational); } - private native String getInteger(long pointer); + private native String getRealValue(long pointer); /** - * @return true if the term is a string constant. + * @return true if the term is a constant array. */ - public boolean isString() + public boolean isConstArray() { - return isString(pointer); + return isConstArray(pointer); } - private native boolean isString(long pointer); + private native boolean isConstArray(long pointer); /** - * @return the stored string constant. - *

- * Note: This method is not to be confused with toString() which returns the - * term in some string representation, whatever data it may hold. - * Asserts isString(). + * Asserts isConstArray(). + * @return the base (element stored at all indices) of a constant array */ - public String getString() + public Term getConstArrayBase() { - return getString(pointer); + long termPointer = getConstArrayBase(pointer); + return new Term(solver, termPointer); } - private native String getString(long pointer); + private native long getConstArrayBase(long pointer); /** - * @return true if the term is a rational value. + * @return true if the term is a Boolean value. */ - public boolean isRealValue() + public boolean isBooleanValue() { - return isRealValue(pointer); + return isBooleanValue(pointer); } - private native boolean isRealValue(long pointer); + private native boolean isBooleanValue(long pointer); + /** + * Asserts isBooleanValue(). + * @return the representation of a Boolean value as a native Boolean value. + */ + public boolean getBooleanValue() + { + return getBooleanValue(pointer); + } + + private native boolean getBooleanValue(long pointer); /** - * Asserts isRealValue(). - * @return the representation of a rational value as a pair of its numerator - * and denominator. + * @return true if the term is a bit-vector value. */ - public Pair getRealValue() + public boolean isBitVectorValue() { - String rational = getRealValue(pointer); - return Utils.getRational(rational); + return isBitVectorValue(pointer); } - private native String getRealValue(long pointer); + private native boolean isBitVectorValue(long pointer); + + /** + * Asserts isBitVectorValue(). + * @return the representation of a bit-vector value in bit string representation. + */ + public String getBitVectorValue() throws CVC5ApiException + { + return getBitVectorValue(2); + } + + /** + * Asserts isBitVectorValue(). + * @return the representation of a bit-vector value in string representation. + * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal + * string). + */ + public String getBitVectorValue(int base) throws CVC5ApiException + { + Utils.validateUnsigned(base, "base"); + return getBitVectorValue(pointer, base); + } + + private native String getBitVectorValue(long pointer, int base); + + /** + * @return true if the term is an abstract value. + */ + public boolean isAbstractValue() + { + return isAbstractValue(pointer); + } + + private native boolean isAbstractValue(long pointer); + + /** + * Asserts isAbstractValue(). + * @return the representation of an abstract value as a string. + */ + public String getAbstractValue() + { + return getAbstractValue(pointer); + } + + private native String getAbstractValue(long pointer); + + /** + * @return true if the term is a tuple value. + */ + public boolean isTupleValue() + { + return isTupleValue(pointer); + } + + private native boolean isTupleValue(long pointer); + + /** + * Asserts isTupleValue(). + * @return the representation of a tuple value as a vector of terms. + */ + public Term[] getTupleValue() + { + long[] termPointers = getTupleValue(pointer); + return Utils.getTerms(solver, termPointers); + } + + private native long[] getTupleValue(long pointer); + + /** + * @return true if the term is the floating-point value for positive zero. + */ + public boolean isFloatingPointPosZero() + { + return isFloatingPointPosZero(pointer); + } + + private native boolean isFloatingPointPosZero(long pointer); + /** + * @return true if the term is the floating-point value for negative zero. + */ + public boolean isFloatingPointNegZero() + { + return isFloatingPointNegZero(pointer); + } + + private native boolean isFloatingPointNegZero(long pointer); + /** + * @return true if the term is the floating-point value for positive + * infinity. + */ + public boolean isFloatingPointPosInf() + { + return isFloatingPointPosInf(pointer); + } + + private native boolean isFloatingPointPosInf(long pointer); + /** + * @return true if the term is the floating-point value for negative + * infinity. + */ + public boolean isFloatingPointNegInf() + { + return isFloatingPointNegInf(pointer); + } + + private native boolean isFloatingPointNegInf(long pointer); + /** + * @return true if the term is the floating-point value for not a number. + */ + public boolean isFloatingPointNaN() + { + return isFloatingPointNaN(pointer); + } + + private native boolean isFloatingPointNaN(long pointer); + /** + * @return true if the term is a floating-point value. + */ + public boolean isFloatingPointValue() + { + return isFloatingPointValue(pointer); + } + + private native boolean isFloatingPointValue(long pointer); + /** + * Asserts isFloatingPointValue(). + * @return the representation of a floating-point value as a tuple of the + * exponent width, the significand width and a bit-vector value. + */ + public Triplet getFloatingPointValue() + { + Triplet triplet = getFloatingPointValue(pointer); + return new Triplet(triplet.first, triplet.second, new Term(solver, triplet.third)); + } + + private native Triplet getFloatingPointValue(long pointer); + + /** + * @return true if the term is a set value. + */ + public boolean isSetValue() + { + return isSetValue(pointer); + } + + private native boolean isSetValue(long pointer); + /** + * Asserts isSetValue(). + * @return the representation of a set value as a set of terms. + */ + public Set getSetValue() + { + long[] termPointers = getSetValue(pointer); + Term[] terms = Utils.getTerms(solver, termPointers); + return new HashSet(Arrays.asList(terms)); + } + + private native long[] getSetValue(long pointer); + + /** + * @return true if the term is a sequence value. + */ + public boolean isSequenceValue() + { + return isSequenceValue(pointer); + } + + private native boolean isSequenceValue(long pointer); + + /** + * Asserts isSequenceValue(). + * Note that it is usually necessary for sequences to call + * `Solver::simplify()` to turn a sequence that is constructed by, e.g., + * concatenation of unit sequences, into a sequence value. + * @return the representation of a sequence value as a vector of terms. + */ + public Term[] getSequenceValue() + { + long[] termPointers = getSequenceValue(pointer); + return Utils.getTerms(solver, termPointers); + } + + private native long[] getSequenceValue(long pointer); + + /** + * @return true if the term is a value from an uninterpreted sort. + */ + public boolean isUninterpretedValue() + { + return isUninterpretedValue(pointer); + } + + private native boolean isUninterpretedValue(long pointer); + + /** + boolean @return() + * Asserts isUninterpretedValue(). + * @return the representation of an uninterpreted value as a pair of its + sort and its + * index. + */ + public Pair getUninterpretedValue() + { + Pair pair = getUninterpretedValue(pointer); + Sort sort = new Sort(solver, pair.first); + return new Pair(sort, pair.second); + } + + private native Pair getUninterpretedValue(long pointer); public class ConstIterator implements Iterator { diff --git a/src/api/java/cvc5/Triplet.java b/src/api/java/cvc5/Triplet.java new file mode 100644 index 000000000..0ba75e7fb --- /dev/null +++ b/src/api/java/cvc5/Triplet.java @@ -0,0 +1,41 @@ +/****************************************************************************** + * 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. + */ + +package cvc5; + +public class Triplet +{ + public A first; + public B second; + public C third; + public Triplet(A first, B second, C third) + { + this.first = first; + this.second = second; + this.third = third; + } + + @Override public boolean equals(Object object) + { + if (this == object) + return true; + if (object == null || getClass() != object.getClass()) + return false; + + Triplet triplet = (Triplet) object; + return this.first.equals(triplet.first) && this.second.equals(triplet.second) + && this.third.equals(triplet.third); + } +} diff --git a/src/api/java/cvc5/Utils.java b/src/api/java/cvc5/Utils.java index 077b77168..ce8632c88 100644 --- a/src/api/java/cvc5/Utils.java +++ b/src/api/java/cvc5/Utils.java @@ -154,6 +154,14 @@ public class Utils return new Pair<>(new BigInteger(rational), new BigInteger("1")); } + /** + Convert a pair of BigIntegers to a rational string a/b + */ + public static String getRational(Pair pair) + { + return pair.first.toString() + "/" + pair.second.toString(); + } + /** * Get the string version of define-fun command. * @param f the function to print diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h index fc4399fed..7b550ef28 100644 --- a/src/api/java/jni/cvc5JavaApi.h +++ b/src/api/java/jni/cvc5JavaApi.h @@ -73,7 +73,7 @@ std::vector getObjectsFromPointers(JNIEnv* env, jlongArray jPointers) * @return jni array of pointers */ template -jlongArray getPointersFromObjects(JNIEnv* env, std::vector objects) +jlongArray getPointersFromObjects(JNIEnv* env, const std::vector& objects) { std::vector pointers(objects.size()); for (size_t i = 0; i < objects.size(); i++) diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index 9bcecd07f..c28ea412f 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -2519,6 +2519,22 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getSynthSolutions( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } +/* + * Class: cvc5_Solver + * Method: getStatistics + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStatistics(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + Statistics* retPointer = new Statistics(solver->getStatistics()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: cvc5_Solver * Method: getNullTerm diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp index 0de1b5673..325a9c744 100644 --- a/src/api/java/jni/cvc5_Term.cpp +++ b/src/api/java/jni/cvc5_Term.cpp @@ -263,42 +263,33 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env, /* * Class: cvc5_Term - * Method: getConstArrayBase - * Signature: (J)J + * Method: isConstArray + * Signature: (J)Z */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isConstArray(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - Term* ret = new Term(current->getConstArrayBase()); - return reinterpret_cast(ret); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); + return static_cast(current->isConstArray()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getConstSequenceElements - * Signature: (J)[J + * Method: getConstArrayBase + * Signature: (J)J */ -JNIEXPORT jlongArray JNICALL -Java_cvc5_Term_getConstSequenceElements(JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - std::vector terms = current->getSequenceValue(); - std::vector termPointers(terms.size()); - for (size_t i = 0; i < terms.size(); i++) - { - termPointers[i] = reinterpret_cast(new Term(terms[i])); - } - - jlongArray ret = env->NewLongArray(terms.size()); - env->SetLongArrayRegion(ret, 0, terms.size(), termPointers.data()); - - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); + Term* ret = new Term(current->getConstArrayBase()); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* @@ -441,164 +432,480 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env, /* * Class: cvc5_Term - * Method: isInt + * Method: isIntegerValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInt(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isIntegerValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isInt32Value()); + return static_cast(current->isIntegerValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getInt - * Signature: (J)I + * Method: getIntegerValue + * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jint JNICALL Java_cvc5_Term_getInt(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_cvc5_Term_getIntegerValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->getInt32Value()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); + std::string value = current->getIntegerValue(); + jstring ret = env->NewStringUTF(value.c_str()); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } /* * Class: cvc5_Term - * Method: isLong + * Method: isStringValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isLong(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isStringValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isInt64Value()); + return static_cast(current->isStringValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getLong - * Signature: (J)J + * Method: getStringValue + * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getLong(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_cvc5_Term_getStringValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->getInt64Value()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); + std::wstring termString = current->getStringValue(); + + size_t length = termString.length(); + jchar* unicode = new jchar[length]; + const wchar_t* s = termString.c_str(); + for (size_t i = 0; i < length; i++) + { + unicode[i] = s[i]; + } + jstring ret = env->NewString(unicode, length); + delete[] unicode; + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } /* * Class: cvc5_Term - * Method: isInteger + * Method: isRealValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInteger(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isIntegerValue()); + return static_cast(current->isRealValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getInteger + * Method: getRealValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getInteger(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + std::string realValue = current->getRealValue(); + return env->NewStringUTF(realValue.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: isBooleanValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBooleanValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isBooleanValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getBooleanValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_getBooleanValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getBooleanValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isBitVectorValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBitVectorValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return env->NewStringUTF(current->getIntegerValue().c_str()); + return static_cast(current->isBitVectorValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getBitVectorValue + * Signature: (JI)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Term_getBitVectorValue(JNIEnv* env, + jobject, + jlong pointer, + jint base) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + std::string ret = + current->getBitVectorValue(static_cast(base)); + return env->NewStringUTF(ret.c_str()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } /* * Class: cvc5_Term - * Method: isString + * Method: isAbstractValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isAbstractValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isStringValue()); + return static_cast(current->isAbstractValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getString + * Method: getAbstractValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_cvc5_Term_getAbstractValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - std::wstring termString = current->getStringValue(); + std::string ret = current->getAbstractValue(); + return env->NewStringUTF(ret.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} - size_t length = termString.length(); - jchar* unicode = new jchar[length]; - const wchar_t* s = termString.c_str(); - for (size_t i = 0; i < length; i++) +/* + * Class: cvc5_Term + * Method: isTupleValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isTupleValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isTupleValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getTupleValue + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getTupleValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + std::vector terms = current->getTupleValue(); + jlongArray ret = getPointersFromObjects(env, terms); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointPosZero + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosZero(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointPosZero()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointNegZero + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegZero(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointNegZero()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointPosInf + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosInf(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointPosInf()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointNegInf + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegInf(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointNegInf()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointNaN + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNaN(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointNaN()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: isFloatingPointValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isFloatingPointValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getFloatingPointValue + * Signature: (J)Lcvc5/Triplet; + */ +JNIEXPORT jobject JNICALL Java_cvc5_Term_getFloatingPointValue( + JNIEnv* env, jobject thisObject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + auto [exponent, significand, term] = current->getFloatingPointValue(); + Term* termPointer = new Term(term); + + // Long longObject = new Long(pointer) + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); + jobject e = env->NewObject(longClass, longConstructor, exponent); + jobject s = env->NewObject(longClass, longConstructor, significand); + jobject t = env->NewObject(longClass, longConstructor, termPointer); + + // Triplet triplet = new Triplet(e, s, t); + jclass tripletClass = env->FindClass("Lcvc5/Triplet;"); + jmethodID tripletConstructor = env->GetMethodID( + tripletClass, + "", + "(Ljava/lang/Object;Ljava/lang/Object;Ljava/lang/Object;)V"); + jobject triplet = env->NewObject(tripletClass, tripletConstructor, e, s, t); + + return triplet; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Term + * Method: isSetValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSetValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isSetValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getSetValue + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSetValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + std::set terms = current->getSetValue(); + std::vector pointers(terms.size()); + int i = 0; + for (const Term& t : terms) { - unicode[i] = s[i]; + pointers[i] = reinterpret_cast(new Term(t)); + i++; } - jstring ret = env->NewString(unicode, length); - delete[] unicode; + jlongArray ret = env->NewLongArray(pointers.size()); + env->SetLongArrayRegion(ret, 0, pointers.size(), pointers.data()); return ret; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } /* * Class: cvc5_Term - * Method: isRealValue + * Method: isSequenceValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSequenceValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isRealValue()); + return static_cast(current->isSequenceValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: cvc5_Term - * Method: getRealValue - * Signature: (J)Ljava/lang/String; + * Method: getSequenceValue + * Signature: (J)[J */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - std::string realValue = current->getRealValue(); - return env->NewStringUTF(realValue.c_str()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); + std::vector terms = current->getSequenceValue(); + jlongArray ret = getPointersFromObjects(env, terms); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Term + * Method: isUninterpretedValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isUninterpretedValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getUninterpretedValue + * Signature: (J)Lcvc5/Pair; + */ +JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + std::pair value = current->getUninterpretedValue(); + + Sort* sort = new Sort(value.first); + jlong sortPointer = reinterpret_cast(sort); + + // Long longObject = new Long(pointer) + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); + jobject longObject = env->NewObject(longClass, longConstructor, sortPointer); + + // Integer integerObject = new Integer(pair.second) + jclass integerClass = env->FindClass("Ljava/lang/Integer;"); + jmethodID integerConstructor = + env->GetMethodID(integerClass, "", "(I)V"); + jobject integerObject = env->NewObject( + integerClass, integerConstructor, static_cast(value.second)); + + // Pair pair = new Pair(jName, longObject) + jclass pairClass = env->FindClass("Lcvc5/Pair;"); + jmethodID pairConstructor = env->GetMethodID( + pairClass, "", "(Ljava/lang/Object;Ljava/lang/Object;)V"); + jobject pair = + env->NewObject(pairClass, pairConstructor, longObject, integerObject); + + return pair; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } /* -- cgit v1.2.3