From 80d5885363f12df98bfa46f76cc9594e56a25197 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 9 Sep 2021 22:28:48 -0500 Subject: [PATCH] Add Op.java to the java API (#6387) This commit adds Op.java OpTest.java and cvc5_Op.cpp to the java api. --- src/api/java/cvc5/Op.java | 125 +++++++++++++++++ src/api/java/jni/cvc5_Op.cpp | 200 ++++++++++++++++++++++++++++ test/unit/api/java/cvc5/OpTest.java | 172 ++++++++++++++++++++++++ 3 files changed, 497 insertions(+) create mode 100644 src/api/java/cvc5/Op.java create mode 100644 src/api/java/jni/cvc5_Op.cpp create mode 100644 test/unit/api/java/cvc5/OpTest.java diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java new file mode 100644 index 000000000..98915c1d1 --- /dev/null +++ b/src/api/java/cvc5/Op.java @@ -0,0 +1,125 @@ +/****************************************************************************** + * 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; + +public class Op extends AbstractPointer { + // region construction and destruction + Op(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 operators are syntactically identical. + * Both operators must belong to the same solver object. + * @param t the operator to compare to for equality + * @return true if the operators are equal + */ + @Override + public boolean equals(Object t) { + if (this == t) + return true; + if (t == null || getClass() != t.getClass()) + return false; + return equals(pointer, ((Op) t).getPointer()); + } + + private native boolean equals(long pointer1, long pointer2); + + /** + * @return the kind of this operator + */ + Kind getKind() { + try { + int value = getKind(pointer); + return Kind.fromInt(value); + } catch (CVC5ApiException e) { + e.printStackTrace(); + throw new RuntimeException(e.getMessage()); + } + } + + private native int getKind(long pointer); + + /** + * @return true if this operator is a null term + */ + public boolean isNull() { + return isNull(pointer); + } + + private native boolean isNull(long pointer); + + /** + * @return true iff this operator is indexed + */ + public boolean isIndexed() { + return isIndexed(pointer); + } + + private native boolean isIndexed(long pointer); + + /** + * @return the number of indices of this op + */ + public int getNumIndices() { + return getNumIndices(pointer); + } + + private native int getNumIndices(long pointer); + + /** + * Get the indices used to create this Op. + * Check the Op Kind with getKind() to determine which argument to use. + * + * @return the indices used to create this Op + */ + public int[] getIntegerIndices() { + return getIntegerIndices(pointer); + } + + private native int[] getIntegerIndices(long pointer); + + /** + * Get the indices used to create this Op. + * Check the Op Kind with getKind() to determine which argument to use. + * + * @return the indices used to create this Op + */ + public String[] getStringIndices() { + return getStringIndices(pointer); + } + + private native String[] getStringIndices(long pointer); + + /** + * @return a string representation of this operator + */ + protected native String toString(long pointer); +} diff --git a/src/api/java/jni/cvc5_Op.cpp b/src/api/java/jni/cvc5_Op.cpp new file mode 100644 index 000000000..5c2a00657 --- /dev/null +++ b/src/api/java/jni/cvc5_Op.cpp @@ -0,0 +1,200 @@ +/****************************************************************************** + * 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_Op.h" + +#include "api/cpp/cvc5.h" +#include "cvc5JavaApi.h" + +using namespace cvc5::api; + +/* + * Class: cvc5_Op + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Op_deletePointer(JNIEnv*, + jclass, + jlong pointer) +{ + delete reinterpret_cast(pointer); +} + +/* + * Class: cvc5_Op + * Method: equals + * Signature: (JJ)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Op_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* op1 = reinterpret_cast(pointer1); + Op* op2 = reinterpret_cast(pointer2); + // We compare the actual operators, not their pointers. + return static_cast(*op1 == *op2); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: cvc5_Op + * Method: getKind + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Op_getKind(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + return static_cast(current->getKind()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Op + * Method: isNull + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Op_isNull(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + return static_cast(current->isNull()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: cvc5_Op + * Method: isIndexed + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Op_isIndexed(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + return static_cast(current->isIndexed()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, false); +} + +/* + * Class: cvc5_Op + * Method: getNumIndices + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_cvc5_Op_getNumIndices(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + return static_cast(current->getNumIndices()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Op + * Method: getIntegerIndices + * Signature: (J)[I + */ +JNIEXPORT jintArray JNICALL Java_cvc5_Op_getIntegerIndices(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + size_t size = current->getNumIndices(); + std::vector indices(size); + if (size == 1) + { + uint32_t index = current->getIndices(); + indices[0] = index; + } + + if (size == 2) + { + std::pair pair = + current->getIndices>(); + indices[0] = pair.first; + indices[1] = pair.second; + } + + if (size > 2) + { + std::string message = "Unhandled case when number of indices > 2."; + throw CVC5ApiException(message); + } + + jintArray ret = env->NewIntArray((jsize)size); + env->SetIntArrayRegion(ret, 0, size, indices.data()); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Op + * Method: getStringIndices + * Signature: (J)[Ljava/lang/String; + */ +JNIEXPORT jobjectArray JNICALL Java_cvc5_Op_getStringIndices(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + size_t size = current->getNumIndices(); + std::vector indices(size); + if (size == 1) + { + std::string cIndex = current->getIndices(); + jstring jIndex = env->NewStringUTF(cIndex.c_str()); + indices[0] = jIndex; + } + + if (size > 1) // currently only one string is implemented in cvc5.cpp + { + std::string message = "Unhandled case when number of indices > 1."; + throw CVC5ApiException(message); + } + + // construct a java array of String + jclass stringClass = env->FindClass("Ljava/lang/String;"); + jobjectArray ret = env->NewObjectArray((jsize)size, stringClass, nullptr); + for (size_t i = 0; i < size; i++) + { + env->SetObjectArrayElement(ret, i, indices[i]); + } + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Op + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Op_toString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* current = reinterpret_cast(pointer); + return env->NewStringUTF(current->toString().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} diff --git a/test/unit/api/java/cvc5/OpTest.java b/test/unit/api/java/cvc5/OpTest.java new file mode 100644 index 000000000..afe728b88 --- /dev/null +++ b/test/unit/api/java/cvc5/OpTest.java @@ -0,0 +1,172 @@ +/****************************************************************************** + * Top contributors (to current version): + * Makai Mann, Aina Niemetz, 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 Op class. + */ + +package cvc5; + +import static cvc5.Kind.*; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Arrays; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class OpTest { + private Solver d_solver; + + @BeforeEach + void setUp() { + d_solver = new Solver(); + } + + @Test + void getKind() throws CVC5ApiException { + Op x; + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + assertDoesNotThrow(() -> x.getKind()); + } + + @Test + void isNull() throws CVC5ApiException { + Op x = d_solver.getNullOp(); + assertTrue(x.isNull()); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + assertFalse(x.isNull()); + } + + @Test + void opFromKind() { + assertDoesNotThrow(() -> d_solver.mkOp(PLUS)); + assertThrows( + CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT)); + } + + @Test + void getIndicesString() throws CVC5ApiException { + Op x = d_solver.getNullOp(); + assertThrows(CVC5ApiException.class, () -> x.getStringIndices()); + + Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); + assertTrue(divisible_ot.isIndexed()); + String divisible_idx = divisible_ot.getStringIndices()[0]; + assertEquals(divisible_idx, "4"); + } + + @Test + void getIndicesUint() throws CVC5ApiException { + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + assertTrue(bitvector_repeat_ot.isIndexed()); + int bitvector_repeat_idx = bitvector_repeat_ot.getIntegerIndices()[0]; + assertEquals(bitvector_repeat_idx, 5); + + // unlike bitvector_repeat_ot.getIndices>() in + // c++, this does not throw in Java + // assertThrows(CVC5ApiException.class, + // () -> bitvector_repeat_ot.getIntegerIndices()); + + Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); + int bitvector_zero_extend_idx = + bitvector_zero_extend_ot.getIntegerIndices()[0]; + assertEquals(bitvector_zero_extend_idx, 6); + + Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); + int bitvector_sign_extend_idx = + bitvector_sign_extend_ot.getIntegerIndices()[0]; + assertEquals(bitvector_sign_extend_idx, 7); + + Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); + int bitvector_rotate_left_idx = + bitvector_rotate_left_ot.getIntegerIndices()[0]; + assertEquals(bitvector_rotate_left_idx, 8); + + Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); + int bitvector_rotate_right_idx = + bitvector_rotate_right_ot.getIntegerIndices()[0]; + assertEquals(bitvector_rotate_right_idx, 9); + + Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10); + int int_to_bitvector_idx = int_to_bitvector_ot.getIntegerIndices()[0]; + assertEquals(int_to_bitvector_idx, 10); + + Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); + int floatingpoint_to_ubv_idx = + floatingpoint_to_ubv_ot.getIntegerIndices()[0]; + assertEquals(floatingpoint_to_ubv_idx, 11); + + Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); + int floatingpoint_to_sbv_idx = + floatingpoint_to_sbv_ot.getIntegerIndices()[0]; + assertEquals(floatingpoint_to_sbv_idx, 13); + } + + @Test + void getIndicesPairUint() throws CVC5ApiException { + Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + assertTrue(bitvector_extract_ot.isIndexed()); + int[] bitvector_extract_indices = bitvector_extract_ot.getIntegerIndices(); + assertArrayEquals(bitvector_extract_indices, new int[] {4, 0}); + + Op floatingpoint_to_fp_ieee_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); + int[] floatingpoint_to_fp_ieee_bitvector_indices = + floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices(); + assertArrayEquals( + floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25}); + + Op floatingpoint_to_fp_floatingpoint_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); + int[] floatingpoint_to_fp_floatingpoint_indices = + floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices(); + assertArrayEquals( + floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25}); + + Op floatingpoint_to_fp_real_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); + int[] floatingpoint_to_fp_real_indices = + floatingpoint_to_fp_real_ot.getIntegerIndices(); + assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25}); + + Op floatingpoint_to_fp_signed_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); + int[] floatingpoint_to_fp_signed_bitvector_indices = + floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices(); + assertArrayEquals( + floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25}); + + Op floatingpoint_to_fp_unsigned_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + int[] floatingpoint_to_fp_unsigned_bitvector_indices = + floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices(); + assertArrayEquals( + floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25}); + + Op floatingpoint_to_fp_generic_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); + int[] floatingpoint_to_fp_generic_indices = + floatingpoint_to_fp_generic_ot.getIntegerIndices(); + assertArrayEquals(floatingpoint_to_fp_generic_indices, new int[] {4, 25}); + assertThrows(CVC5ApiException.class, + () -> floatingpoint_to_fp_generic_ot.getStringIndices()); + } + + @Test + void opScopingToString() throws CVC5ApiException { + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + String op_repr = bitvector_repeat_ot.toString(); + + Solver solver2; + assertEquals(bitvector_repeat_ot.toString(), op_repr); + } +} -- 2.30.2