From 991bef531131336549eccd2446243204f4733c20 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 7 Oct 2021 06:29:28 -0500 Subject: [PATCH] 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 ++++++++++++++++++++----- test/unit/api/java/cvc5/TermTest.java | 311 ++++++++++++++-- 12 files changed, 1022 insertions(+), 222 deletions(-) create mode 100644 src/api/java/cvc5/Triplet.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); } /* diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java index 508e264e3..98f668006 100644 --- a/test/unit/api/java/cvc5/TermTest.java +++ b/test/unit/api/java/cvc5/TermTest.java @@ -21,8 +21,11 @@ import static org.junit.jupiter.api.Assertions.*; import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; +import java.util.HashSet; import java.util.Iterator; import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; @@ -663,7 +666,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> tnull.getChild(0)); } - @Test void getInteger() throws CVC5ApiException + @Test void getIntegerValue() throws CVC5ApiException { Term int1 = d_solver.mkInteger("-18446744073709551616"); Term int2 = d_solver.mkInteger("-18446744073709551615"); @@ -688,46 +691,274 @@ class TermTest assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-01")); assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-00")); - assertTrue(!int1.isInt() && !int1.isLong() && int1.isInteger()); - assertEquals(int1.getInteger(), "-18446744073709551616"); - assertTrue(!int2.isInt() && !int2.isLong() && int2.isInteger()); - assertEquals(int2.getInteger(), "-18446744073709551615"); - assertTrue(!int3.isInt() && int3.isLong() && int3.isInteger()); - assertEquals(int3.getLong(), -4294967296L); - assertEquals(int3.getInteger(), "-4294967296"); - assertTrue(!int4.isInt() && int4.isLong() && int4.isInteger()); - assertEquals(int4.getLong(), -4294967295L); - assertEquals(int4.getInteger(), "-4294967295"); - assertTrue(int5.isInt() && int5.isLong() && int5.isInteger()); - assertEquals(int5.getInt(), -10); - assertEquals(int5.getLong(), -10); - assertEquals(int5.getInteger(), "-10"); - assertTrue(int6.isInt() && int6.isLong() && int6.isInteger()); - assertEquals(int6.getInt(), 0); - assertEquals(int6.getLong(), 0); - assertEquals(int6.getInteger(), "0"); - assertTrue(int7.isInt() && int7.isLong() && int7.isInteger()); - assertEquals(int7.getInt(), 10); - assertEquals(int7.getLong(), 10); - assertEquals(int7.getInteger(), "10"); - assertTrue(!int8.isInt() && int8.isLong() && int8.isInteger()); - assertEquals(int8.getLong(), 4294967295L); - assertEquals(int8.getInteger(), "4294967295"); - assertTrue(!int9.isInt() && int9.isLong() && int9.isInteger()); - assertEquals(int9.getLong(), 4294967296L); - assertEquals(int9.getInteger(), "4294967296"); - assertTrue(!int10.isInt() && !int10.isLong() && int10.isInteger()); - - assertEquals(int10.getInteger(), "18446744073709551615"); - assertTrue(!int11.isInt() && !int11.isLong() && int11.isInteger()); - assertEquals(int11.getInteger(), "18446744073709551616"); + assertTrue(int1.isIntegerValue()); + assertEquals(int1.getIntegerValue().toString(), "-18446744073709551616"); + assertTrue(int2.isIntegerValue()); + assertEquals(int2.getIntegerValue().toString(), "-18446744073709551615"); + assertTrue(int3.isIntegerValue()); + assertEquals(int3.getIntegerValue().longValue(), -4294967296L); + assertEquals(int3.getIntegerValue().toString(), "-4294967296"); + assertTrue(int4.isIntegerValue()); + assertEquals(int4.getIntegerValue().longValue(), -4294967295L); + assertEquals(int4.getIntegerValue().toString(), "-4294967295"); + assertTrue(int5.isIntegerValue()); + assertEquals(int5.getIntegerValue().intValue(), -10); + assertEquals(int5.getIntegerValue().intValue(), -10); + assertEquals(int5.getIntegerValue().toString(), "-10"); + assertTrue(int6.isIntegerValue()); + assertEquals(int6.getIntegerValue().intValue(), 0); + assertEquals(int6.getIntegerValue().intValue(), 0); + assertEquals(int6.getIntegerValue().toString(), "0"); + assertTrue(int7.isIntegerValue()); + assertEquals(int7.getIntegerValue().intValue(), 10); + assertEquals(int7.getIntegerValue().intValue(), 10); + assertEquals(int7.getIntegerValue().toString(), "10"); + assertTrue(int8.isIntegerValue()); + assertEquals(int8.getIntegerValue().longValue(), 4294967295L); + assertEquals(int8.getIntegerValue().toString(), "4294967295"); + assertTrue(int9.isIntegerValue()); + assertEquals(int9.getIntegerValue().longValue(), 4294967296L); + assertEquals(int9.getIntegerValue().toString(), "4294967296"); + assertTrue(int10.isIntegerValue()); + + assertEquals(int10.getIntegerValue().toString(), "18446744073709551615"); + assertTrue(int11.isIntegerValue()); + assertEquals(int11.getIntegerValue().toString(), "18446744073709551616"); } @Test void getString() { Term s1 = d_solver.mkString("abcde"); - assertTrue(s1.isString()); - assertEquals(s1.getString(), "abcde"); + assertTrue(s1.isStringValue()); + assertEquals(s1.getStringValue(), "abcde"); + } + + @Test void getReal() throws CVC5ApiException + { + Term real1 = d_solver.mkReal("0"); + Term real2 = d_solver.mkReal(".0"); + Term real3 = d_solver.mkReal("-17"); + Term real4 = d_solver.mkReal("-3/5"); + Term real5 = d_solver.mkReal("12.7"); + Term real6 = d_solver.mkReal("1/4294967297"); + Term real7 = d_solver.mkReal("4294967297"); + Term real8 = d_solver.mkReal("1/18446744073709551617"); + Term real9 = d_solver.mkReal("18446744073709551617"); + Term real10 = d_solver.mkReal("2343.2343"); + + assertTrue(real1.isRealValue()); + assertTrue(real2.isRealValue()); + assertTrue(real3.isRealValue()); + assertTrue(real4.isRealValue()); + assertTrue(real5.isRealValue()); + assertTrue(real6.isRealValue()); + assertTrue(real7.isRealValue()); + assertTrue(real8.isRealValue()); + assertTrue(real9.isRealValue()); + assertTrue(real10.isRealValue()); + + assertEquals("0/1", Utils.getRational(real1.getRealValue())); + assertEquals("0/1", Utils.getRational(real2.getRealValue())); + assertEquals("-17/1", Utils.getRational(real3.getRealValue())); + assertEquals("-3/5", Utils.getRational(real4.getRealValue())); + assertEquals("127/10", Utils.getRational(real5.getRealValue())); + assertEquals("1/4294967297", Utils.getRational(real6.getRealValue())); + assertEquals("4294967297/1", Utils.getRational(real7.getRealValue())); + assertEquals("1/18446744073709551617", Utils.getRational(real8.getRealValue())); + assertEquals("18446744073709551617/1", Utils.getRational(real9.getRealValue())); + assertEquals("23432343/10000", Utils.getRational(real10.getRealValue())); + } + + @Test void getConstArrayBase() + { + Sort intsort = d_solver.getIntegerSort(); + Sort arrsort = d_solver.mkArraySort(intsort, intsort); + Term one = d_solver.mkInteger(1); + Term constarr = d_solver.mkConstArray(arrsort, one); + + assertTrue(constarr.isConstArray()); + assertEquals(one, constarr.getConstArrayBase()); + } + + @Test void getBoolean() + { + Term b1 = d_solver.mkBoolean(true); + Term b2 = d_solver.mkBoolean(false); + + assertTrue(b1.isBooleanValue()); + assertTrue(b2.isBooleanValue()); + assertTrue(b1.getBooleanValue()); + assertFalse(b2.getBooleanValue()); + } + + @Test void getBitVector() throws CVC5ApiException + { + Term b1 = d_solver.mkBitVector(8, 15); + Term b2 = d_solver.mkBitVector(8, "00001111", 2); + Term b3 = d_solver.mkBitVector(8, "15", 10); + Term b4 = d_solver.mkBitVector(8, "0f", 16); + Term b5 = d_solver.mkBitVector(9, "00001111", 2); + Term b6 = d_solver.mkBitVector(9, "15", 10); + Term b7 = d_solver.mkBitVector(9, "0f", 16); + + assertTrue(b1.isBitVectorValue()); + assertTrue(b2.isBitVectorValue()); + assertTrue(b3.isBitVectorValue()); + assertTrue(b4.isBitVectorValue()); + assertTrue(b5.isBitVectorValue()); + assertTrue(b6.isBitVectorValue()); + assertTrue(b7.isBitVectorValue()); + + assertEquals("00001111", b1.getBitVectorValue(2)); + assertEquals("15", b1.getBitVectorValue(10)); + assertEquals("f", b1.getBitVectorValue(16)); + assertEquals("00001111", b2.getBitVectorValue(2)); + assertEquals("15", b2.getBitVectorValue(10)); + assertEquals("f", b2.getBitVectorValue(16)); + assertEquals("00001111", b3.getBitVectorValue(2)); + assertEquals("15", b3.getBitVectorValue(10)); + assertEquals("f", b3.getBitVectorValue(16)); + assertEquals("00001111", b4.getBitVectorValue(2)); + assertEquals("15", b4.getBitVectorValue(10)); + assertEquals("f", b4.getBitVectorValue(16)); + assertEquals("000001111", b5.getBitVectorValue(2)); + assertEquals("15", b5.getBitVectorValue(10)); + assertEquals("f", b5.getBitVectorValue(16)); + assertEquals("000001111", b6.getBitVectorValue(2)); + assertEquals("15", b6.getBitVectorValue(10)); + assertEquals("f", b6.getBitVectorValue(16)); + assertEquals("000001111", b7.getBitVectorValue(2)); + assertEquals("15", b7.getBitVectorValue(10)); + assertEquals("f", b7.getBitVectorValue(16)); + } + + @Test void getAbstractValue() throws CVC5ApiException + { + Term v1 = d_solver.mkAbstractValue(1); + Term v2 = d_solver.mkAbstractValue("15"); + Term v3 = d_solver.mkAbstractValue("18446744073709551617"); + + assertTrue(v1.isAbstractValue()); + assertTrue(v2.isAbstractValue()); + assertTrue(v3.isAbstractValue()); + assertEquals("1", v1.getAbstractValue()); + assertEquals("15", v2.getAbstractValue()); + assertEquals("18446744073709551617", v3.getAbstractValue()); + } + + @Test void getTuple() + { + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.getRealSort(); + Sort s3 = d_solver.getStringSort(); + + Term t1 = d_solver.mkInteger(15); + Term t2 = d_solver.mkReal(17, 25); + Term t3 = d_solver.mkString("abc"); + + Term tup = d_solver.mkTuple(new Sort[] {s1, s2, s3}, new Term[] {t1, t2, t3}); + + assertTrue(tup.isTupleValue()); + assertEquals(Arrays.asList((new Term[] {t1, t2, t3})), Arrays.asList(tup.getTupleValue())); + } + + @Test void getFloatingPoint() throws CVC5ApiException + { + Term bvval = d_solver.mkBitVector(16, "0000110000000011", 2); + Term fp = d_solver.mkFloatingPoint(5, 11, bvval); + + assertTrue(fp.isFloatingPointValue()); + assertFalse(fp.isFloatingPointPosZero()); + assertFalse(fp.isFloatingPointNegZero()); + assertFalse(fp.isFloatingPointPosInf()); + assertFalse(fp.isFloatingPointNegInf()); + assertFalse(fp.isFloatingPointNaN()); + assertEquals(new Triplet(5L, 11L, bvval), fp.getFloatingPointValue()); + + assertTrue(d_solver.mkPosZero(5, 11).isFloatingPointPosZero()); + assertTrue(d_solver.mkNegZero(5, 11).isFloatingPointNegZero()); + assertTrue(d_solver.mkPosInf(5, 11).isFloatingPointPosInf()); + assertTrue(d_solver.mkNegInf(5, 11).isFloatingPointNegInf()); + assertTrue(d_solver.mkNaN(5, 11).isFloatingPointNaN()); + } + + @Test void getSet() + { + Sort s = d_solver.mkSetSort(d_solver.getIntegerSort()); + + Term i1 = d_solver.mkInteger(5); + Term i2 = d_solver.mkInteger(7); + + Term s1 = d_solver.mkEmptySet(s); + Term s2 = d_solver.mkTerm(Kind.SINGLETON, i1); + Term s3 = d_solver.mkTerm(Kind.SINGLETON, i1); + Term s4 = d_solver.mkTerm(Kind.SINGLETON, i2); + Term s5 = d_solver.mkTerm(Kind.UNION, s2, d_solver.mkTerm(Kind.UNION, s3, s4)); + + assertTrue(s1.isSetValue()); + assertTrue(s2.isSetValue()); + assertTrue(s3.isSetValue()); + assertTrue(s4.isSetValue()); + assertFalse(s5.isSetValue()); + s5 = d_solver.simplify(s5); + assertTrue(s5.isSetValue()); + + assertSetsEquality(new Term[] {}, s1.getSetValue()); + assertSetsEquality(new Term[] {i1}, s2.getSetValue()); + assertSetsEquality(new Term[] {i1}, s3.getSetValue()); + assertSetsEquality(new Term[] {i2}, s4.getSetValue()); + assertSetsEquality(new Term[] {i1, i2}, s5.getSetValue()); + } + + private void assertSetsEquality(Term[] A, Set B) + { + List a = Arrays.stream(A).sorted().collect(Collectors.toList()); + List b = B.stream().sorted().collect(Collectors.toList()); + assertEquals(a, b); + } + + @Test void getSequence() + { + Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort()); + + Term i1 = d_solver.mkInteger(5); + Term i2 = d_solver.mkInteger(7); + + Term s1 = d_solver.mkEmptySequence(s); + Term s2 = d_solver.mkTerm(Kind.SEQ_UNIT, i1); + Term s3 = d_solver.mkTerm(Kind.SEQ_UNIT, i1); + Term s4 = d_solver.mkTerm(Kind.SEQ_UNIT, i2); + Term s5 = d_solver.mkTerm(Kind.SEQ_CONCAT, s2, d_solver.mkTerm(Kind.SEQ_CONCAT, s3, s4)); + + assertTrue(s1.isSequenceValue()); + assertTrue(!s2.isSequenceValue()); + assertTrue(!s3.isSequenceValue()); + assertTrue(!s4.isSequenceValue()); + assertTrue(!s5.isSequenceValue()); + + s2 = d_solver.simplify(s2); + s3 = d_solver.simplify(s3); + s4 = d_solver.simplify(s4); + s5 = d_solver.simplify(s5); + + assertEquals(Arrays.asList(new Term[] {}), Arrays.asList(s1.getSequenceValue())); + assertEquals(Arrays.asList(new Term[] {i1}), Arrays.asList(s2.getSequenceValue())); + assertEquals(Arrays.asList(new Term[] {i1}), Arrays.asList(s3.getSequenceValue())); + assertEquals(Arrays.asList(new Term[] {i2}), Arrays.asList(s4.getSequenceValue())); + assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue())); + } + + @Test void getUninterpretedConst() throws CVC5ApiException + { + Sort s = d_solver.mkUninterpretedSort("test"); + Term t1 = d_solver.mkUninterpretedConst(s, 3); + Term t2 = d_solver.mkUninterpretedConst(s, 5); + + assertTrue(t1.isUninterpretedValue()); + assertTrue(t2.isUninterpretedValue()); + + assertEquals(new Pair(s, 3), t1.getUninterpretedValue()); + assertEquals(new Pair(s, 5), t2.getUninterpretedValue()); } @Test void substitute() @@ -800,7 +1031,7 @@ class TermTest stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); } - @Test void constSequenceElements() throws CVC5ApiException + @Test void getSequenceValue() throws CVC5ApiException { Sort realsort = d_solver.getRealSort(); Sort seqsort = d_solver.mkSequenceSort(realsort); @@ -808,13 +1039,13 @@ class TermTest assertEquals(s.getKind(), CONST_SEQUENCE); // empty sequence has zero elements - List cs = Arrays.asList(s.getConstSequenceElements()); - assertTrue(cs.isEmpty()); + Term[] cs = s.getSequenceValue(); + assertTrue(cs.length == 0); // A seq.unit app is not a constant sequence (regardless of whether it is // applied to a constant). Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); - assertThrows(CVC5ApiException.class, () -> su.getConstSequenceElements()); + assertThrows(CVC5ApiException.class, () -> su.getSequenceValue()); } @Test void termScopedToString() -- 2.30.2