From f214151669a5a0ec97df4cc21b66fdaa198001e1 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 20 Aug 2021 14:30:29 -0500 Subject: [PATCH] Add Term.java to the Java API (#6330) This commit adds `Term.java`, `TermTest.java`, and `cvc5_Term.cpp` to the Java API. --- src/api/java/CMakeLists.txt | 4 +- src/api/java/cvc5/Term.java | 442 +++++++++++++ src/api/java/jni/cvc5_Term.cpp | 587 ++++++++++++++++++ test/unit/api/java/cvc5/TermTest.java | 852 ++++++++++++++++++++++++++ 4 files changed, 1884 insertions(+), 1 deletion(-) create mode 100644 src/api/java/cvc5/Term.java create mode 100644 src/api/java/jni/cvc5_Term.cpp create mode 100644 test/unit/api/java/cvc5/TermTest.java diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 53ea46f46..d1e818f30 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -91,7 +91,9 @@ message(STATUS "JAVA_INCLUDE_PATH : ${JAVA_INCLUDE_PATH}") message(STATUS "JAVA_INCLUDE_PATH2 : ${JAVA_INCLUDE_PATH2}") message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}") -add_library(cvc5jni SHARED jni/cvc5_Solver.cpp) +add_library(cvc5jni SHARED + jni/cvc5_Solver.cpp +) add_dependencies(cvc5jni generate-jni-headers) target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS}) diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java new file mode 100644 index 000000000..276c288d1 --- /dev/null +++ b/src/api/java/cvc5/Term.java @@ -0,0 +1,442 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +import java.util.Iterator; +import java.util.List; +import java.util.NoSuchElementException; + +public class Term + extends AbstractPointer implements Comparable, Iterable { + // region construction and destruction + Term(Solver solver, long pointer) { + super(solver, pointer); + } + + protected static native void deletePointer(long pointer); + + public long getPointer() { + return pointer; + } + + @Override + public void finalize() { + deletePointer(pointer); + } + + // endregion + + /** + * Syntactic equality operator. + * Return true if both terms are syntactically identical. + * Both terms must belong to the same solver object. + * + * @param t the term to compare to for equality + * @return true if the terms are equal + */ + @Override + public boolean equals(Object t) { + if (this == t) + return true; + if (t == null || getClass() != t.getClass()) + return false; + Term term = (Term) t; + if (this.pointer == term.pointer) { + return true; + } + return equals(pointer, term.getPointer()); + } + + private native boolean equals(long pointer1, long pointer2); + + /** + * Comparison for ordering on terms. + * + * @param t the term to compare to + * @return a negative integer, zero, or a positive integer as this term + * is less than, equal to, or greater than the specified term. + */ + @Override + public int compareTo(Term t) { + return this.compareTo(pointer, t.getPointer()); + } + + private native int compareTo(long pointer1, long pointer2); + + /** + * @return the number of children of this term + */ + public int getNumChildren() { + return getNumChildren(pointer); + } + + private native int getNumChildren(long pointer); + + /** + * Get the child term at a given index. + * + * @param index the index of the child term to return + * @return the child term with the given index + */ + public Term getChild(int index) throws CVC5ApiException { + Utils.validateUnsigned(index, "index"); + long termPointer = getChild(pointer, index); + return new Term(solver, termPointer); + } + + private native long getChild(long pointer, int index); + + /** + * @return the id of this term + */ + public long getId() { + return getId(pointer); + } + + private native long getId(long pointer); + + /** + * @return the kind of this term + */ + public Kind getKind() throws CVC5ApiException { + int value = getKind(pointer); + return Kind.fromInt(value); + } + + private native int getKind(long pointer); + + /** + * @return the sort of this term + */ + public Sort getSort() { + long sortPointer = getSort(pointer); + return new Sort(solver, sortPointer); + } + + private native long getSort(long pointer); + + /** + * @return the result of replacing 'term' by 'replacement' in this term + */ + public Term substitute(Term term, Term replacement) { + long termPointer = + substitute(pointer, term.getPointer(), replacement.getPointer()); + return new Term(solver, termPointer); + } + + private native long substitute( + long pointer, long termPointer, long replacementPointer); + + /** + * @return the result of simultaneously replacing 'terms' by 'replacements' + * in this term + */ + public Term substitute(List terms, List replacements) { + return substitute( + terms.toArray(new Term[0]), replacements.toArray(new Term[0])); + } + + /** + * @return the result of simultaneously replacing 'terms' by 'replacements' + * in this term + */ + public Term substitute(Term[] terms, Term[] replacements) { + long[] termPointers = new long[terms.length]; + for (int i = 0; i < termPointers.length; i++) { + termPointers[i] = terms[i].getPointer(); + } + long[] replacementPointers = new long[replacements.length]; + for (int i = 0; i < replacements.length; i++) { + replacementPointers[i] = replacements[i].getPointer(); + } + + long termPointer = substitute(pointer, termPointers, replacementPointers); + return new Term(solver, termPointer); + } + + private native long substitute( + long pointer, long[] termPointers, long[] replacementPointers); + + /** + * @return true iff this term has an operator + */ + public boolean hasOp() { + return hasOp(pointer); + } + + private native boolean hasOp(long pointer); + + /** + * @return the Op used to create this term + * Note: This is safe to call when hasOp() returns true. + */ + public Op getOp() { + long opPointer = getOp(pointer); + return new Op(solver, opPointer); + } + + private native long getOp(long pointer); + + /** + * @return true if this Term is a null term + */ + public boolean isNull() { + return isNull(pointer); + } + + 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. + * + * @return the Boolean negation of this term + */ + public Term notTerm() { + long termPointer = notTerm(pointer); + return new Term(solver, termPointer); + } + + private native long notTerm(long pointer); + + /** + * Boolean and. + * + * @param t a Boolean term + * @return the conjunction of this term and the given term + */ + public Term andTerm(Term t) { + long termPointer = andTerm(pointer, t.getPointer()); + return new Term(solver, termPointer); + } + + private native long andTerm(long pointer, long termPointer); + + /** + * Boolean or. + * + * @param t a Boolean term + * @return the disjunction of this term and the given term + */ + public Term orTerm(Term t) { + long termPointer = orTerm(pointer, t.getPointer()); + return new Term(solver, termPointer); + } + + private native long orTerm(long pointer, long termPointer); + + /** + * Boolean exclusive or. + * + * @param t a Boolean term + * @return the exclusive disjunction of this term and the given term + */ + public Term xorTerm(Term t) { + long termPointer = xorTerm(pointer, t.getPointer()); + return new Term(solver, termPointer); + } + + private native long xorTerm(long pointer, long termPointer); + + /** + * Equality. + * + * @param t a Boolean term + * @return the Boolean equivalence of this term and the given term + */ + public Term eqTerm(Term t) { + long termPointer = eqTerm(pointer, t.getPointer()); + return new Term(solver, termPointer); + } + + private native long eqTerm(long pointer, long termPointer); + + /** + * Boolean implication. + * + * @param t a Boolean term + * @return the implication of this term and the given term + */ + public Term impTerm(Term t) { + long termPointer = impTerm(pointer, t.getPointer()); + return new Term(solver, termPointer); + } + + private native long impTerm(long pointer, long termPointer); + + /** + * If-then-else with this term as the Boolean condition. + * + * @param thenTerm the 'then' term + * @param elseTerm the 'else' term + * @return the if-then-else term with this term as the Boolean condition + */ + public Term iteTerm(Term thenTerm, Term elseTerm) { + long termPointer = + iteTerm(pointer, thenTerm.getPointer(), elseTerm.getPointer()); + return new Term(solver, termPointer); + } + + private native long iteTerm(long pointer, long thenPointer, long elsePointer); + + /** + * @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. + */ + public boolean isInt() { + return isInt(pointer); + } + + private native boolean isInt(long pointer); + + /** + * @return the stored integer as an int. + * Note: Asserts isInt(). + */ + public int getInt() { + return getInt(pointer); + } + + private native int getInt(long pointer); + + /** + * @return true if the term is an integer that fits within a Java long. + */ + public boolean isLong() { + return isLong(pointer); + } + + private native boolean isLong(long pointer); + + /** + * @return the stored integer as a long. + * Note: Asserts isLong(). + */ + public long getLong() { + return getLong(pointer); + } + + private native long getLong(long pointer); + + /** + * @return true if the term is an integer. + */ + public boolean isInteger() { + return isInteger(pointer); + } + + private native boolean isInteger(long pointer); + + /** + * @return the stored integer in (decimal) string representation. + * Note: Asserts isInteger(). + */ + public String getInteger() { + return getInteger(pointer); + } + + private native String getInteger(long pointer); + + /** + * @return true if the term is a string constant. + */ + public boolean isString() { + return isString(pointer); + } + + private native boolean isString(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(). + */ + public String getString() { + return getString(pointer); + } + + private native String getString(long pointer); + + public class ConstIterator implements Iterator { + private int currentIndex; + private int size; + + public ConstIterator() { + currentIndex = -1; + size = getNumChildren(); + } + + @Override + public boolean hasNext() { + return currentIndex < size - 1; + } + + @Override + public Term next() { + if (currentIndex >= size - 1) { + throw new NoSuchElementException(); + } + currentIndex++; + try { + return getChild(currentIndex); + } catch (CVC5ApiException e) { + e.printStackTrace(); + throw new RuntimeException(e.getMessage()); + } + } + } + + @Override + public Iterator iterator() { + return new ConstIterator(); + } +} diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp new file mode 100644 index 000000000..6c4d00ff3 --- /dev/null +++ b/src/api/java/jni/cvc5_Term.cpp @@ -0,0 +1,587 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#include "cvc5_Term.h" + +#include "api/cpp/cvc5.h" +#include "cvc5JavaApi.h" + +using namespace cvc5::api; + +/* + * Class: cvc5_Term + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Term_deletePointer(JNIEnv* env, + jclass, + jlong pointer) +{ + delete reinterpret_cast(pointer); +} + +/* + * Class: cvc5_Term + * Method: equals + * Signature: (JJ)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* term1 = reinterpret_cast(pointer1); + Term* term2 = reinterpret_cast(pointer2); + // We compare the actual terms, not their pointers. + return static_cast(*term1 == *term2); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: compareTo + * Signature: (JJ)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Term_compareTo(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* term1 = reinterpret_cast(pointer1); + Term* term2 = reinterpret_cast(pointer2); + if (*term1 < *term2) + { + return static_cast(-1); + } + if (*term1 == *term2) + { + return 0; + } + return static_cast(1); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: getNumChildren + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Term_getNumChildren(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getNumChildren()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: getChild + * Signature: (JI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getChild(JNIEnv* env, + jobject, + jlong pointer, + jint index) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* ret = new Term((*current)[static_cast(index)]); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: getId + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getId(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getId()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: getKind + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Term_getKind(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getKind()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: getSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Sort* ret = new Sort(current->getSort()); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: substitute + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_substitute__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer, + jlong replacementPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* replacement = reinterpret_cast(replacementPointer); + Term* ret = new Term(current->substitute(*term, *replacement)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: substitute + * Signature: (J[J[J)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Term_substitute__J_3J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray termPointers, + jlongArray replacementPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + jsize termsSize = env->GetArrayLength(termPointers); + jsize replacementsSize = env->GetArrayLength(replacementPointers); + jlong* termElements = env->GetLongArrayElements(termPointers, nullptr); + jlong* replacementElements = + env->GetLongArrayElements(replacementPointers, nullptr); + + std::vector terms(termsSize); + std::vector replacements(replacementsSize); + + for (jsize i = 0; i < termsSize; i++) + { + Term* term = (Term*)termElements[i]; + terms[i] = *term; + } + env->ReleaseLongArrayElements(termPointers, termElements, 0); + + for (jsize i = 0; i < replacementsSize; i++) + { + Term* term = (Term*)replacementElements[i]; + replacements[i] = *term; + } + env->ReleaseLongArrayElements(replacementPointers, replacementElements, 0); + + Term* ret = new Term(current->substitute(terms, replacements)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: hasOp + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_hasOp(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->hasOp()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getOp + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getOp(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Op* ret = new Op(current->getOp()); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: isNull + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isNull()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getConstArrayBase + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(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); +} + +/* + * Class: cvc5_Term + * Method: getConstSequenceElements + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL +Java_cvc5_Term_getConstSequenceElements(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); +} + +/* + * Class: cvc5_Term + * Method: notTerm + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_notTerm(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* ret = new Term(current->notTerm()); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: andTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_andTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* ret = new Term(current->andTerm(*term)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: orTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_orTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* ret = new Term(current->orTerm(*term)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: xorTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_xorTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* ret = new Term(current->xorTerm(*term)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: eqTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_eqTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* ret = new Term(current->eqTerm(*term)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: impTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_impTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* term = reinterpret_cast(termPointer); + Term* ret = new Term(current->impTerm(*term)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: iteTerm + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_iteTerm( + JNIEnv* env, jobject, jlong pointer, jlong thenPointer, jlong elsePointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term* thenTerm = reinterpret_cast(thenPointer); + Term* elseTerm = reinterpret_cast(elsePointer); + Term* ret = new Term(current->iteTerm(*thenTerm, *elseTerm)); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return env->NewStringUTF(current->toString().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Term + * Method: isInt + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInt(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isInt32Value()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getInt + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Term_getInt(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); +} + +/* + * Class: cvc5_Term + * Method: isLong + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isLong(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isInt64Value()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getLong + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_getLong(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); +} + +/* + * Class: cvc5_Term + * Method: isInteger + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isInteger(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isIntegerValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getInteger + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Term_getInteger(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return env->NewStringUTF(current->getIntegerValue().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Term + * Method: isString + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->isStringValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: cvc5_Term + * Method: getString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Term_getString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + 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: iterator + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Term_iterator(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + Term::const_iterator* retPointer = new Term::const_iterator(current->begin()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java new file mode 100644 index 000000000..d5491e0e7 --- /dev/null +++ b/test/unit/api/java/cvc5/TermTest.java @@ -0,0 +1,852 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Makai Mann, Andrew Reynolds, 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. + * **************************************************************************** + * + * Black box testing of the Term class. + */ + +package cvc5; + +import static cvc5.Kind.*; +import static org.junit.jupiter.api.Assertions.*; + +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Iterator; +import java.util.List; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class TermTest { + private Solver d_solver; + + @BeforeEach + void setUp() { + d_solver = new Solver(); + } + + @Test + void eq() { + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(uSort, "x"); + Term y = d_solver.mkVar(uSort, "y"); + Term z = d_solver.getNullTerm(); + + assertTrue(x == x); + assertFalse(x != x); + assertFalse(x == y); + assertTrue(x != y); + assertFalse((x == z)); + assertTrue(x != z); + } + + @Test + void getId() { + Term n = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> n.getId()); + Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); + assertDoesNotThrow(() -> x.getId()); + Term y = x; + assertEquals(x.getId(), y.getId()); + + Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z"); + assertNotEquals(x.getId(), z.getId()); + } + + @Test + void getKind() throws CVC5ApiException { + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term n = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> n.getKind()); + Term x = d_solver.mkVar(uSort, "x"); + assertDoesNotThrow(() -> x.getKind()); + Term y = d_solver.mkVar(uSort, "y"); + assertDoesNotThrow(() -> y.getKind()); + + Term f = d_solver.mkVar(funSort1, "f"); + assertDoesNotThrow(() -> f.getKind()); + Term p = d_solver.mkVar(funSort2, "p"); + assertDoesNotThrow(() -> p.getKind()); + + Term zero = d_solver.mkInteger(0); + assertDoesNotThrow(() -> zero.getKind()); + + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertDoesNotThrow(() -> f_x.getKind()); + Term f_y = d_solver.mkTerm(APPLY_UF, f, y); + assertDoesNotThrow(() -> f_y.getKind()); + Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + assertDoesNotThrow(() -> sum.getKind()); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.getKind()); + Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); + assertDoesNotThrow(() -> p_f_y.getKind()); + + // Sequence kinds do not exist internally, test that the API properly + // converts them back. + Sort seqSort = d_solver.mkSequenceSort(intSort); + Term s = d_solver.mkConst(seqSort, "s"); + Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); + assertEquals(ss.getKind(), SEQ_CONCAT); + } + + @Test + void getSort() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term n = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> n.getSort()); + Term x = d_solver.mkVar(bvSort, "x"); + assertDoesNotThrow(() -> x.getSort()); + assertEquals(x.getSort(), bvSort); + Term y = d_solver.mkVar(bvSort, "y"); + assertDoesNotThrow(() -> y.getSort()); + assertEquals(y.getSort(), bvSort); + + Term f = d_solver.mkVar(funSort1, "f"); + assertDoesNotThrow(() -> f.getSort()); + assertEquals(f.getSort(), funSort1); + Term p = d_solver.mkVar(funSort2, "p"); + assertDoesNotThrow(() -> p.getSort()); + assertEquals(p.getSort(), funSort2); + + Term zero = d_solver.mkInteger(0); + assertDoesNotThrow(() -> zero.getSort()); + assertEquals(zero.getSort(), intSort); + + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertDoesNotThrow(() -> f_x.getSort()); + assertEquals(f_x.getSort(), intSort); + Term f_y = d_solver.mkTerm(APPLY_UF, f, y); + assertDoesNotThrow(() -> f_y.getSort()); + assertEquals(f_y.getSort(), intSort); + Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + assertDoesNotThrow(() -> sum.getSort()); + assertEquals(sum.getSort(), intSort); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.getSort()); + assertEquals(p_0.getSort(), boolSort); + Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); + assertDoesNotThrow(() -> p_f_y.getSort()); + assertEquals(p_f_y.getSort(), boolSort); + } + + @Test + void getOp() throws CVC5ApiException { + Sort intsort = d_solver.getIntegerSort(); + Sort bvsort = d_solver.mkBitVectorSort(8); + Sort arrsort = d_solver.mkArraySort(bvsort, intsort); + Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); + + Term x = d_solver.mkConst(intsort, "x"); + Term a = d_solver.mkConst(arrsort, "a"); + Term b = d_solver.mkConst(bvsort, "b"); + + assertFalse(x.hasOp()); + assertThrows(CVC5ApiException.class, () -> x.getOp()); + + Term ab = d_solver.mkTerm(SELECT, a, b); + Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + Term extb = d_solver.mkTerm(ext, b); + + assertTrue(ab.hasOp()); + assertFalse(ab.getOp().isIndexed()); + // can compare directly to a Kind (will invoke Op constructor) + assertTrue(extb.hasOp()); + assertTrue(extb.getOp().isIndexed()); + assertEquals(extb.getOp(), ext); + + Term f = d_solver.mkConst(funsort, "f"); + Term fx = d_solver.mkTerm(APPLY_UF, f, x); + + assertFalse(f.hasOp()); + assertThrows(CVC5ApiException.class, () -> f.getOp()); + assertTrue(fx.hasOp()); + List children = new ArrayList(); + + Iterator iterator = fx.iterator(); + for (Term t : fx) { + children.add(t); + } + + // testing rebuild from op and children + assertEquals(fx, d_solver.mkTerm(fx.getOp(), children)); + + // Test Datatypes Ops + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + cons.addSelector("head", sort); + cons.addSelectorSelf("tail"); + listDecl.addConstructor(cons); + listDecl.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(listDecl); + Sort intListSort = + listSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); + Term c = d_solver.mkConst(intListSort, "c"); + Datatype list = listSort.getDatatype(); + // list datatype constructor and selector operator terms + Term consOpTerm = list.getConstructorTerm("cons"); + Term nilOpTerm = list.getConstructorTerm("nil"); + } + + @Test + void isNull() throws CVC5ApiException { + Term x = d_solver.getNullTerm(); + assertTrue(x.isNull()); + x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x"); + assertFalse(x.isNull()); + } + + @Test + void notTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().notTerm()); + Term b = d_solver.mkTrue(); + assertDoesNotThrow(() -> b.notTerm()); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.notTerm()); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.notTerm()); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.notTerm()); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.notTerm()); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.notTerm()); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.notTerm()); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.notTerm()); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.notTerm()); + } + + @Test + void andTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().andTerm(b)); + assertThrows( + CVC5ApiException.class, () -> b.andTerm(d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.andTerm(b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> x.andTerm(x)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> f.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> f.andTerm(f)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> p.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> p.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> p.andTerm(p)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> zero.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> zero.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> zero.andTerm(p)); + assertThrows(CVC5ApiException.class, () -> zero.andTerm(zero)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(p)); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(zero)); + assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f_x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(p)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(zero)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> sum.andTerm(sum)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_0.andTerm(sum)); + assertDoesNotThrow(() -> p_0.andTerm(p_0)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.andTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.andTerm(sum)); + assertDoesNotThrow(() -> p_f_x.andTerm(p_0)); + assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x)); + } + + @Test + void orTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().orTerm(b)); + assertThrows( + CVC5ApiException.class, () -> b.orTerm(d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.orTerm(b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> x.orTerm(x)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> f.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> f.orTerm(f)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> p.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> p.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> p.orTerm(p)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> zero.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> zero.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> zero.orTerm(p)); + assertThrows(CVC5ApiException.class, () -> zero.orTerm(zero)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(p)); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(zero)); + assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f_x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(p)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(zero)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> sum.orTerm(sum)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_0.orTerm(sum)); + assertDoesNotThrow(() -> p_0.orTerm(p_0)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.orTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.orTerm(sum)); + assertDoesNotThrow(() -> p_f_x.orTerm(p_0)); + assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x)); + } + + @Test + void xorTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().xorTerm(b)); + assertThrows( + CVC5ApiException.class, () -> b.xorTerm(d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.xorTerm(b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> x.xorTerm(x)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> f.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> f.xorTerm(f)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> p.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> p.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> p.xorTerm(p)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> zero.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> zero.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> zero.xorTerm(p)); + assertThrows(CVC5ApiException.class, () -> zero.xorTerm(zero)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(p)); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(zero)); + assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f_x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(p)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(zero)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> sum.xorTerm(sum)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_0.xorTerm(sum)); + assertDoesNotThrow(() -> p_0.xorTerm(p_0)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.xorTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.xorTerm(sum)); + assertDoesNotThrow(() -> p_f_x.xorTerm(p_0)); + assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x)); + } + + @Test + void eqTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().eqTerm(b)); + assertThrows( + CVC5ApiException.class, () -> b.eqTerm(d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.eqTerm(b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.eqTerm(b)); + assertDoesNotThrow(() -> x.eqTerm(x)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> f.eqTerm(x)); + assertDoesNotThrow(() -> f.eqTerm(f)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> p.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> p.eqTerm(f)); + assertDoesNotThrow(() -> p.eqTerm(p)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> zero.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> zero.eqTerm(f)); + assertThrows(CVC5ApiException.class, () -> zero.eqTerm(p)); + assertDoesNotThrow(() -> zero.eqTerm(zero)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(f)); + assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(p)); + assertDoesNotThrow(() -> f_x.eqTerm(zero)); + assertDoesNotThrow(() -> f_x.eqTerm(f_x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> sum.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> sum.eqTerm(f)); + assertThrows(CVC5ApiException.class, () -> sum.eqTerm(p)); + assertDoesNotThrow(() -> sum.eqTerm(zero)); + assertDoesNotThrow(() -> sum.eqTerm(f_x)); + assertDoesNotThrow(() -> sum.eqTerm(sum)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_0.eqTerm(sum)); + assertDoesNotThrow(() -> p_0.eqTerm(p_0)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.eqTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.eqTerm(sum)); + assertDoesNotThrow(() -> p_f_x.eqTerm(p_0)); + assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x)); + } + + @Test + void impTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().impTerm(b)); + assertThrows( + CVC5ApiException.class, () -> b.impTerm(d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.impTerm(b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertThrows(CVC5ApiException.class, () -> x.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> x.impTerm(x)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> f.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> f.impTerm(f)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> p.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> p.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> p.impTerm(p)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> zero.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> zero.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> zero.impTerm(p)); + assertThrows(CVC5ApiException.class, () -> zero.impTerm(zero)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(p)); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(zero)); + assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f_x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(p)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(zero)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> sum.impTerm(sum)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_0.impTerm(sum)); + assertDoesNotThrow(() -> p_0.impTerm(p_0)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.impTerm(b)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(p)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(zero)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(f_x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.impTerm(sum)); + assertDoesNotThrow(() -> p_f_x.impTerm(p_0)); + assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x)); + } + + @Test + void iteTerm() throws CVC5ApiException { + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); + Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + + Term b = d_solver.mkTrue(); + assertThrows( + CVC5ApiException.class, () -> d_solver.getNullTerm().iteTerm(b, b)); + assertThrows( + CVC5ApiException.class, () -> b.iteTerm(d_solver.getNullTerm(), b)); + assertThrows( + CVC5ApiException.class, () -> b.iteTerm(b, d_solver.getNullTerm())); + assertDoesNotThrow(() -> b.iteTerm(b, b)); + Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); + assertDoesNotThrow(() -> b.iteTerm(x, x)); + assertDoesNotThrow(() -> b.iteTerm(b, b)); + assertThrows(CVC5ApiException.class, () -> b.iteTerm(x, b)); + assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, x)); + assertThrows(CVC5ApiException.class, () -> x.iteTerm(x, b)); + Term f = d_solver.mkVar(funSort1, "f"); + assertThrows(CVC5ApiException.class, () -> f.iteTerm(b, b)); + assertThrows(CVC5ApiException.class, () -> x.iteTerm(b, x)); + Term p = d_solver.mkVar(funSort2, "p"); + assertThrows(CVC5ApiException.class, () -> p.iteTerm(b, b)); + assertThrows(CVC5ApiException.class, () -> p.iteTerm(x, b)); + Term zero = d_solver.mkInteger(0); + assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, x)); + assertThrows(CVC5ApiException.class, () -> zero.iteTerm(x, b)); + Term f_x = d_solver.mkTerm(APPLY_UF, f, x); + assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b)); + assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x)); + Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x)); + assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x)); + Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); + assertDoesNotThrow(() -> p_0.iteTerm(b, b)); + assertDoesNotThrow(() -> p_0.iteTerm(x, x)); + assertThrows(CVC5ApiException.class, () -> p_0.iteTerm(x, b)); + Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); + assertDoesNotThrow(() -> p_f_x.iteTerm(b, b)); + assertDoesNotThrow(() -> p_f_x.iteTerm(x, x)); + assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b)); + } + + @Test + void termAssignment() { + Term t1 = d_solver.mkInteger(1); + Term t2 = t1; + t2 = d_solver.mkInteger(2); + assertEquals(t1, d_solver.mkInteger(1)); + } + + @Test + void termCompare() { + Term t1 = d_solver.mkInteger(1); + Term t2 = + d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t3 = + d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); + assertTrue(t2.compareTo(t3) >= 0); + assertTrue(t2.compareTo(t3) <= 0); + assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0)); + assertTrue( + (t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0)); + } + + @Test + void termChildren() throws CVC5ApiException { + // simple term 2+3 + Term two = d_solver.mkInteger(2); + Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); + assertEquals(t1.getChild(0), two); + assertEquals(t1.getNumChildren(), 2); + Term tnull = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> tnull.getNumChildren()); + + // apply term f(2) + Sort intSort = d_solver.getIntegerSort(); + Sort fsort = d_solver.mkFunctionSort(intSort, intSort); + Term f = d_solver.mkConst(fsort, "f"); + Term t2 = d_solver.mkTerm(APPLY_UF, f, two); + // due to our higher-order view of terms, we treat f as a child of APPLY_UF + assertEquals(t2.getNumChildren(), 2); + assertEquals(t2.getChild(0), f); + assertEquals(t2.getChild(1), two); + assertThrows(CVC5ApiException.class, () -> tnull.getChild(0)); + } + + @Test + void getInteger() throws CVC5ApiException { + Term int1 = d_solver.mkInteger("-18446744073709551616"); + Term int2 = d_solver.mkInteger("-18446744073709551615"); + Term int3 = d_solver.mkInteger("-4294967296"); + Term int4 = d_solver.mkInteger("-4294967295"); + Term int5 = d_solver.mkInteger("-10"); + Term int6 = d_solver.mkInteger("0"); + Term int7 = d_solver.mkInteger("10"); + Term int8 = d_solver.mkInteger("4294967295"); + Term int9 = d_solver.mkInteger("4294967296"); + Term int10 = d_solver.mkInteger("18446744073709551615"); + Term int11 = d_solver.mkInteger("18446744073709551616"); + Term int12 = d_solver.mkInteger("-0"); + + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-1-")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0.0")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("-0.1")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("012")); + assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("0000")); + 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(Integer.toUnsignedLong(int8.getInt()), 4294967295L); + 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(Long.compareUnsigned(int10.getLong(), + new BigInteger("18446744073709551615").longValue()), + 0); + assertEquals(int10.getInteger(), "18446744073709551615"); + assertTrue(!int11.isInt() && !int11.isLong() && int11.isInteger()); + assertEquals(int11.getInteger(), "18446744073709551616"); + } + + @Test + void getString() { + Term s1 = d_solver.mkString("abcde"); + assertTrue(s1.isString()); + assertEquals(s1.getString(), "abcde"); + } + + @Test + void substitute() { + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + Term one = d_solver.mkInteger(1); + Term ttrue = d_solver.mkTrue(); + Term xpx = d_solver.mkTerm(PLUS, x, x); + Term onepone = d_solver.mkTerm(PLUS, one, one); + + assertEquals(xpx.substitute(x, one), onepone); + assertEquals(onepone.substitute(one, x), xpx); + // incorrect due to type + assertThrows(CVC5ApiException.class, () -> xpx.substitute(one, ttrue)); + + // simultaneous substitution + Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); + Term xpy = d_solver.mkTerm(PLUS, x, y); + Term xpone = d_solver.mkTerm(PLUS, y, one); + List es = new ArrayList<>(); + List rs = new ArrayList<>(); + es.add(x); + rs.add(y); + es.add(y); + rs.add(one); + assertEquals(xpy.substitute(es, rs), xpone); + + // incorrect substitution due to arity + rs.remove(rs.size() - 1); + assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs)); + + // incorrect substitution due to types + rs.add(ttrue); + assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs)); + + // null cannot substitute + Term tnull = d_solver.getNullTerm(); + assertThrows(CVC5ApiException.class, () -> tnull.substitute(one, x)); + assertThrows(CVC5ApiException.class, () -> xpx.substitute(tnull, x)); + assertThrows(CVC5ApiException.class, () -> xpx.substitute(x, tnull)); + rs.remove(rs.size() - 1); + rs.add(tnull); + assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs)); + es.clear(); + rs.clear(); + es.add(x); + rs.add(y); + assertThrows(CVC5ApiException.class, () -> tnull.substitute(es, rs)); + es.add(tnull); + rs.add(one); + assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs)); + } + + @Test + void constArray() throws CVC5ApiException { + Sort intsort = d_solver.getIntegerSort(); + Sort arrsort = d_solver.mkArraySort(intsort, intsort); + Term a = d_solver.mkConst(arrsort, "a"); + Term one = d_solver.mkInteger(1); + Term constarr = d_solver.mkConstArray(arrsort, one); + + assertEquals(constarr.getKind(), CONST_ARRAY); + assertEquals(constarr.getConstArrayBase(), one); + assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase()); + + arrsort = + d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); + Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0)); + Term stores = d_solver.mkTerm( + STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2)); + stores = + d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3)); + stores = + d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); + } + + @Test + void constSequenceElements() throws CVC5ApiException { + Sort realsort = d_solver.getRealSort(); + Sort seqsort = d_solver.mkSequenceSort(realsort); + Term s = d_solver.mkEmptySequence(seqsort); + + assertEquals(s.getKind(), CONST_SEQUENCE); + // empty sequence has zero elements + List cs = Arrays.asList(s.getConstSequenceElements()); + assertTrue(cs.isEmpty()); + + // 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()); + } + + @Test + void termScopedToString() { + Sort intsort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(intsort, "x"); + assertEquals(x.toString(), "x"); + Solver solver2; + assertEquals(x.toString(), "x"); + } +} -- 2.30.2