--- /dev/null
+/******************************************************************************
+ * 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<Term>, Iterable<Term> {
+ // 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<Term> terms, List<Term> 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.
+ * <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 String getString() {
+ return getString(pointer);
+ }
+
+ private native String getString(long pointer);
+
+ public class ConstIterator implements Iterator<Term> {
+ 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<Term> iterator() {
+ return new ConstIterator();
+ }
+}
--- /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.
+ */
+
+#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<Term*>(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<Term*>(pointer1);
+ Term* term2 = reinterpret_cast<Term*>(pointer2);
+ // We compare the actual terms, not their pointers.
+ return static_cast<jboolean>(*term1 == *term2);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer1);
+ Term* term2 = reinterpret_cast<Term*>(pointer2);
+ if (*term1 < *term2)
+ {
+ return static_cast<jint>(-1);
+ }
+ if (*term1 == *term2)
+ {
+ return 0;
+ }
+ return static_cast<jint>(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<Term*>(pointer);
+ return static_cast<jint>(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<Term*>(pointer);
+ Term* ret = new Term((*current)[static_cast<size_t>(index)]);
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ return static_cast<jlong>(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<Term*>(pointer);
+ return static_cast<jint>(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<Term*>(pointer);
+ Sort* ret = new Sort(current->getSort());
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* replacement = reinterpret_cast<Term*>(replacementPointer);
+ Term* ret = new Term(current->substitute(*term, *replacement));
+ return reinterpret_cast<jlong>(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<Term*>(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<Term> terms(termsSize);
+ std::vector<Term> 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<jlong>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->hasOp());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ Op* ret = new Op(current->getOp());
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isNull());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ Term* ret = new Term(current->getConstArrayBase());
+ return reinterpret_cast<jlong>(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<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);
+}
+
+/*
+ * 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<Term*>(pointer);
+ Term* ret = new Term(current->notTerm());
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* ret = new Term(current->andTerm(*term));
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* ret = new Term(current->orTerm(*term));
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* ret = new Term(current->xorTerm(*term));
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* ret = new Term(current->eqTerm(*term));
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* term = reinterpret_cast<Term*>(termPointer);
+ Term* ret = new Term(current->impTerm(*term));
+ return reinterpret_cast<jlong>(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<Term*>(pointer);
+ Term* thenTerm = reinterpret_cast<Term*>(thenPointer);
+ Term* elseTerm = reinterpret_cast<Term*>(elsePointer);
+ Term* ret = new Term(current->iteTerm(*thenTerm, *elseTerm));
+ return reinterpret_cast<jlong>(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<Term*>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isInt32Value());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jint>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isInt64Value());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(pointer);
+ return static_cast<jlong>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isIntegerValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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<Term*>(pointer);
+ return static_cast<jboolean>(current->isStringValue());
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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<Term*>(pointer);
+ Term::const_iterator* retPointer = new Term::const_iterator(current->begin());
+ return reinterpret_cast<jlong>(retPointer);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
--- /dev/null
+/******************************************************************************
+ * 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<Term> children = new ArrayList();
+
+ Iterator<Term> 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<Term> es = new ArrayList<>();
+ List<Term> 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<Term> 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");
+ }
+}
projects / cvc5.git / commitdiff