Add Op.java to the java API (#6387)

This commit adds Op.java OpTest.java and cvc5_Op.cpp to the java api.

diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java
new file mode 100644 (file)
index 0000000..98915c1
--- /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 (file)
index 0000000..5c2a006
--- /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<Op*>(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<Op*>(pointer1);
+  Op* op2 = reinterpret_cast<Op*>(pointer2);
+  // We compare the actual operators, not their pointers.
+  return static_cast<jboolean>(*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<Op*>(pointer);
+  return static_cast<jboolean>(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<Op*>(pointer);
+  return static_cast<jboolean>(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<Op*>(pointer);
+  return static_cast<jboolean>(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<Op*>(pointer);
+  return static_cast<jint>(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<Op*>(pointer);
+  size_t size = current->getNumIndices();
+  std::vector<jint> indices(size);
+  if (size == 1)
+  {
+    uint32_t index = current->getIndices<uint32_t>();
+    indices[0] = index;
+  }
+
+  if (size == 2)
+  {
+    std::pair<uint32_t, uint32_t> pair =
+        current->getIndices<std::pair<uint32_t, uint32_t>>();
+    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<Op*>(pointer);
+  size_t size = current->getNumIndices();
+  std::vector<jstring> indices(size);
+  if (size == 1)
+  {
+    std::string cIndex = current->getIndices<std::string>();
+    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<Op*>(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 (file)
index 0000000..afe728b
--- /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<std::pair<uint32_t, uint32_t>>() 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);
+  }
+}