This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.
${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}
)
return pointer;
}
+ public Solver getSolver()
+ {
+ return solver;
+ }
+
@Override public String toString()
{
return toString(pointer);
/**
* @return the kind of this operator
*/
- Kind getKind()
+ public Kind getKind()
{
try
{
Pair<K, V> p = (Pair<K, V>) pair;
- if (!first.equals(p.first))
- return false;
- return second.equals(p.second);
+ return first.equals(p.first) && second.equals(p.second);
}
}
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
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<Term>, Iterable<Term>
{
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.
*
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.
+ * <p>
+ * 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<BigInteger, BigInteger> 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.
- * <p>
- * 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<BigInteger, BigInteger> 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<Long, Long, Term> getFloatingPointValue()
+ {
+ Triplet<Long, Long, Long> triplet = getFloatingPointValue(pointer);
+ return new Triplet(triplet.first, triplet.second, new Term(solver, triplet.third));
+ }
+
+ private native Triplet<Long, Long, Long> 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<Term> getSetValue()
+ {
+ long[] termPointers = getSetValue(pointer);
+ Term[] terms = Utils.getTerms(solver, termPointers);
+ return new HashSet<Term>(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<Sort, Integer> getUninterpretedValue()
+ {
+ Pair<Long, Integer> pair = getUninterpretedValue(pointer);
+ Sort sort = new Sort(solver, pair.first);
+ return new Pair<Sort, Integer>(sort, pair.second);
+ }
+
+ private native Pair<Long, Integer> getUninterpretedValue(long pointer);
public class ConstIterator implements Iterator<Term>
{
--- /dev/null
+/******************************************************************************
+ * 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<A, B, C>
+{
+ 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<A, B, C> triplet = (Triplet<A, B, C>) object;
+ return this.first.equals(triplet.first) && this.second.equals(triplet.second)
+ && this.third.equals(triplet.third);
+ }
+}
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<BigInteger, BigInteger> pair)
+ {
+ return pair.first.toString() + "/" + pair.second.toString();
+ }
+
/**
* Get the string version of define-fun command.
* @param f the function to print
* @return jni array of pointers
*/
template <class T>
-jlongArray getPointersFromObjects(JNIEnv* env, std::vector<T> objects)
+jlongArray getPointersFromObjects(JNIEnv* env, const std::vector<T>& objects)
{
std::vector<jlong> pointers(objects.size());
for (size_t i = 0; i < objects.size(); i++)
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<Solver*>(pointer);
+ Statistics* retPointer = new Statistics(solver->getStatistics());
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: cvc5_Solver
* Method: getNullTerm
/*
* 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<Term*>(pointer);
- Term* ret = new Term(current->getConstArrayBase());
- return reinterpret_cast<jlong>(ret);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+ return static_cast<jboolean>(current->isConstArray());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
- std::vector<Term> terms = current->getSequenceValue();
- std::vector<long> termPointers(terms.size());
- for (size_t i = 0; i < terms.size(); i++)
- {
- termPointers[i] = reinterpret_cast<long>(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<jlong>(ret);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
/*
/*
* 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<Term*>(pointer);
- return static_cast<jboolean>(current->isInt32Value());
+ return static_cast<jboolean>(current->isIntegerValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
- return static_cast<jint>(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<Term*>(pointer);
- return static_cast<jboolean>(current->isInt64Value());
+ return static_cast<jboolean>(current->isStringValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
- return static_cast<jlong>(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<Term*>(pointer);
- return static_cast<jboolean>(current->isIntegerValue());
+ return static_cast<jboolean>(current->isRealValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isBooleanValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->getBooleanValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
- return env->NewStringUTF(current->getIntegerValue().c_str());
+ return static_cast<jboolean>(current->isBitVectorValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ std::string ret =
+ current->getBitVectorValue(static_cast<std::uint32_t>(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<Term*>(pointer);
- return static_cast<jboolean>(current->isStringValue());
+ return static_cast<jboolean>(current->isAbstractValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isTupleValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ std::vector<Term> terms = current->getTupleValue();
+ jlongArray ret = getPointersFromObjects<Term>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointPosZero());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointNegZero());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointPosInf());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointNegInf());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointNaN());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isFloatingPointValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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, "<init>", "(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<Long, Long, Long>(e, s, t);
+ jclass tripletClass = env->FindClass("Lcvc5/Triplet;");
+ jmethodID tripletConstructor = env->GetMethodID(
+ tripletClass,
+ "<init>",
+ "(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isSetValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ std::set<Term> terms = current->getSetValue();
+ std::vector<jlong> pointers(terms.size());
+ int i = 0;
+ for (const Term& t : terms)
{
- unicode[i] = s[i];
+ pointers[i] = reinterpret_cast<jlong>(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<Term*>(pointer);
- return static_cast<jboolean>(current->isRealValue());
+ return static_cast<jboolean>(current->isSequenceValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
- std::string realValue = current->getRealValue();
- return env->NewStringUTF(realValue.c_str());
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+ std::vector<Term> terms = current->getSequenceValue();
+ jlongArray ret = getPointersFromObjects<Term>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isUninterpretedValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
+
+ Sort* sort = new Sort(value.first);
+ jlong sortPointer = reinterpret_cast<jlong>(sort);
+
+ // Long longObject = new Long(pointer)
+ jclass longClass = env->FindClass("Ljava/lang/Long;");
+ jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(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, "<init>", "(I)V");
+ jobject integerObject = env->NewObject(
+ integerClass, integerConstructor, static_cast<jint>(value.second));
+
+ // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
+ jclass pairClass = env->FindClass("Lcvc5/Pair;");
+ jmethodID pairConstructor = env->GetMethodID(
+ pairClass, "<init>", "(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);
}
/*
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;
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");
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<Long, Long, Term>(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<Term> B)
+ {
+ List<Term> a = Arrays.stream(A).sorted().collect(Collectors.toList());
+ List<Term> 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<Sort, Integer>(s, 3), t1.getUninterpretedValue());
+ assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue());
}
@Test void substitute()
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);
assertEquals(s.getKind(), CONST_SEQUENCE);
// empty sequence has zero elements
- List<Term> 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()
projects / cvc5.git / commitdiff