[API] Support `Op::operator[]` in Java and Python (#8356)

This commit adds support for `Op::operator[]` in Java and Python and
updates all unit tests to be consistent.

diff --git a/src/api/java/io/github/cvc5/api/Op.java b/src/api/java/io/github/cvc5/api/Op.java
index 1263465e0550cf7afa31cf598dcbd3ee219d27a2..87d85c9630f58aeecc9a6b32e6764c303a11d63a 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Op.java
+++ b/src/api/java/io/github/cvc5/api/Op.java
@@ -99,6 +99,20 @@ public class Op extends AbstractPointer
 
   private native int getNumIndices(long pointer);
 
+  /**
+   * Get the index at position i.
+   * @param i the position of the index to return
+   * @return the index at position i
+   */
+  public Term get(int i) throws CVC5ApiException
+  {
+    Utils.validateUnsigned(i, "index");
+    long termPointer = get(pointer, i);
+    return new Term(solver, termPointer);
+  }
+
+  private native long get(long pointer, int i);
+
   /**
    * @return a string representation of this operator
    */

diff --git a/src/api/java/jni/op.cpp b/src/api/java/jni/op.cpp
index 83072e88c859dcb625a58ddfe8aad44d03b3d708..7ec481fc66ca8fab0284f62c70139e85f7cebf70 100644 (file)
--- a/src/api/java/jni/op.cpp
+++ b/src/api/java/jni/op.cpp
@@ -109,6 +109,22 @@ JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getNumIndices(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Op
+ * Method:    get
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Op_get(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer,
+                                                       jint i)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Op* current = reinterpret_cast<Op*>(pointer);
+  Term* ret = new Term((*current)[static_cast<size_t>(i)]);
+  return reinterpret_cast<jlong>(ret);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
 
 /*
  * Class:     io_github_cvc5_api_Op

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 0251790e75ba850050a9b785d3f05614d63420ae..7f0037d998a4b610b1e7c1be64d5c10fbc485cc1 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -129,6 +129,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isNull() except +
         bint isIndexed() except +
         size_t getNumIndices() except +
+        Term operator[](size_t i) except +
         string toString() except +
 
     cdef cppclass OpHashFunction:

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index e861473cc5d41c0b8667c636659e874fa2402170..f90cd5fa2a575e21984df8661e5184f2a40cb3d3 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -499,6 +499,17 @@ cdef class Op:
         """
         return self.cop.getNumIndices()
 
+    def __getitem__(self, i):
+        """
+            Get the index at position i.
+            :param i: the position of the index to return
+            :return: the index at position i
+        """
+        cdef Term term = Term(self.solver)
+        term.cterm = self.cop[i]
+        return term
+
+
 cdef class Grammar:
     """
         A Sygus Grammar.

diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp
index 8792b5df1c5d2a18481fa9b8bfae2e236daed196..0dfe9cdb5757a8d3989822a4d8548fed6fac3c01 100644 (file)
--- a/test/unit/api/cpp/op_black.cpp
+++ b/test/unit/api/cpp/op_black.cpp
@@ -48,98 +48,124 @@ TEST_F(TestApiBlackOp, opFromKind)
 
 TEST_F(TestApiBlackOp, getNumIndices)
 {
+  // Operators with 0 indices
   Op plus = d_solver.mkOp(ADD);
-  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
-  Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
-  Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
-  Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
-  Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
-  Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
-  Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 10);
-  Op iand = d_solver.mkOp(IAND, 3);
-  Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
-  Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
-  Op floatingpoint_to_fp_ieee_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25);
-  Op floatingpoint_to_fp_floatingpoint =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25);
-  Op floatingpoint_to_fp_real =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25);
-  Op floatingpoint_to_fp_signed_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25);
-  Op floatingpoint_to_fp_unsigned_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25);
-  Op floatingpoint_to_fp_generic =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
-  Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 2, 3);
 
   ASSERT_EQ(0, plus.getNumIndices());
+
+  // Operators with 1 index
+  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
+  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
+  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
+  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
+  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
+  Op iand = d_solver.mkOp(IAND, 11);
+  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
+  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+
   ASSERT_EQ(1, divisible.getNumIndices());
-  ASSERT_EQ(1, bitvector_repeat.getNumIndices());
-  ASSERT_EQ(1, bitvector_zero_extend.getNumIndices());
-  ASSERT_EQ(1, bitvector_sign_extend.getNumIndices());
-  ASSERT_EQ(1, bitvector_rotate_left.getNumIndices());
-  ASSERT_EQ(1, bitvector_rotate_right.getNumIndices());
-  ASSERT_EQ(1, int_to_bitvector.getNumIndices());
+  ASSERT_EQ(1, bvRepeat.getNumIndices());
+  ASSERT_EQ(1, bvZeroExtend.getNumIndices());
+  ASSERT_EQ(1, bvSignExtend.getNumIndices());
+  ASSERT_EQ(1, bvRotateLeft.getNumIndices());
+  ASSERT_EQ(1, bvRotateRight.getNumIndices());
+  ASSERT_EQ(1, intToBv.getNumIndices());
   ASSERT_EQ(1, iand.getNumIndices());
-  ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices());
-  ASSERT_EQ(1, floatingopint_to_sbv.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_ieee_bitvector.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_floatingpoint.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_real.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_signed_bitvector.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_unsigned_bitvector.getNumIndices());
-  ASSERT_EQ(2, floatingpoint_to_fp_generic.getNumIndices());
-  ASSERT_EQ(2, regexp_loop.getNumIndices());
+  ASSERT_EQ(1, fpToUbv.getNumIndices());
+  ASSERT_EQ(1, fpToSbv.getNumIndices());
+
+  // Operators with 2 indices
+  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
+  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
+  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
+  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
+  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
+  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
+  Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
+  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+
+  ASSERT_EQ(2, bvExtract.getNumIndices());
+  ASSERT_EQ(2, toFpFromIeeeBv.getNumIndices());
+  ASSERT_EQ(2, toFpFromFp.getNumIndices());
+  ASSERT_EQ(2, toFpFromReal.getNumIndices());
+  ASSERT_EQ(2, toFpFromSbv.getNumIndices());
+  ASSERT_EQ(2, toFpFromUbv.getNumIndices());
+  ASSERT_EQ(2, toFpGen.getNumIndices());
+  ASSERT_EQ(2, regexpLoop.getNumIndices());
+
+  // Operators with n indices
+  std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
+  Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
+  ASSERT_EQ(indices.size(), tupleProject.getNumIndices());
 }
 
 TEST_F(TestApiBlackOp, subscriptOperator)
 {
+  // Operators with 0 indices
   Op plus = d_solver.mkOp(ADD);
-  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
-  Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4);
-  Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4);
-  Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 4);
-  Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 4);
-  Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 4);
-  Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 4);
-  Op iand = d_solver.mkOp(IAND, 4);
-  Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 4);
-  Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 4);
-  Op floatingpoint_to_fp_ieee_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 5);
-  Op floatingpoint_to_fp_floatingpoint =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 5);
-  Op floatingpoint_to_fp_real =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 5);
-  Op floatingpoint_to_fp_signed_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 5);
-  Op floatingpoint_to_fp_unsigned_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 5);
-  Op floatingpoint_to_fp_generic =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 5);
-  Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 4, 5);
 
   ASSERT_THROW(plus[0], CVC5ApiException);
+
+  // Operators with 1 index
+  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
+  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
+  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
+  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
+  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
+  Op iand = d_solver.mkOp(IAND, 11);
+  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
+  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+
   ASSERT_EQ(4, divisible[0].getUInt32Value());
-  ASSERT_EQ(4, bitvector_repeat[0].getUInt32Value());
-  ASSERT_EQ(4, bitvector_zero_extend[0].getUInt32Value());
-  ASSERT_EQ(4, bitvector_sign_extend[0].getUInt32Value());
-  ASSERT_EQ(4, bitvector_rotate_left[0].getUInt32Value());
-  ASSERT_EQ(4, bitvector_rotate_right[0].getUInt32Value());
-  ASSERT_EQ(4, int_to_bitvector[0].getUInt32Value());
-  ASSERT_EQ(4, iand[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_ubv[0].getUInt32Value());
-  ASSERT_EQ(4, floatingopint_to_sbv[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_ieee_bitvector[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_floatingpoint[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_real[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_signed_bitvector[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_unsigned_bitvector[0].getUInt32Value());
-  ASSERT_EQ(4, floatingpoint_to_fp_generic[0].getUInt32Value());
-  ASSERT_EQ(4, regexp_loop[0].getUInt32Value());
-}
+  ASSERT_EQ(5, bvRepeat[0].getUInt32Value());
+  ASSERT_EQ(6, bvZeroExtend[0].getUInt32Value());
+  ASSERT_EQ(7, bvSignExtend[0].getUInt32Value());
+  ASSERT_EQ(8, bvRotateLeft[0].getUInt32Value());
+  ASSERT_EQ(9, bvRotateRight[0].getUInt32Value());
+  ASSERT_EQ(10, intToBv[0].getUInt32Value());
+  ASSERT_EQ(11, iand[0].getUInt32Value());
+  ASSERT_EQ(12, fpToUbv[0].getUInt32Value());
+  ASSERT_EQ(13, fpToSbv[0].getUInt32Value());
 
+  // Operators with 2 indices
+  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
+  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
+  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
+  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
+  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
+  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
+  Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
+  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+
+  ASSERT_EQ(1, bvExtract[0].getUInt32Value());
+  ASSERT_EQ(0, bvExtract[1].getUInt32Value());
+  ASSERT_EQ(3, toFpFromIeeeBv[0].getUInt32Value());
+  ASSERT_EQ(2, toFpFromIeeeBv[1].getUInt32Value());
+  ASSERT_EQ(5, toFpFromFp[0].getUInt32Value());
+  ASSERT_EQ(4, toFpFromFp[1].getUInt32Value());
+  ASSERT_EQ(7, toFpFromReal[0].getUInt32Value());
+  ASSERT_EQ(6, toFpFromReal[1].getUInt32Value());
+  ASSERT_EQ(9, toFpFromSbv[0].getUInt32Value());
+  ASSERT_EQ(8, toFpFromSbv[1].getUInt32Value());
+  ASSERT_EQ(11, toFpFromUbv[0].getUInt32Value());
+  ASSERT_EQ(10, toFpFromUbv[1].getUInt32Value());
+  ASSERT_EQ(13, toFpGen[0].getUInt32Value());
+  ASSERT_EQ(12, toFpGen[1].getUInt32Value());
+  ASSERT_EQ(15, regexpLoop[0].getUInt32Value());
+  ASSERT_EQ(14, regexpLoop[1].getUInt32Value());
+
+  // Operators with n indices
+  std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
+  Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
+  for (size_t i = 0, size = tupleProject.getNumIndices(); i < size; i++)
+  {
+    ASSERT_EQ(indices[i], tupleProject[i].getUInt32Value());
+  }
+}
 
 TEST_F(TestApiBlackOp, opScopingToString)
 {

diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index 17a7aee9a16225d5c6cc43a97329beea660cb06d..47793aa638560244091d65a1c660a946f5030cb1 100644 (file)
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -18,7 +18,10 @@ import static io.github.cvc5.api.Kind.*;
 import static org.junit.jupiter.api.Assertions.*;
 
 import io.github.cvc5.api.*;
+import java.math.BigInteger;
+import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.List;
 import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
@@ -58,6 +61,127 @@ class OpTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
   }
 
+  @Test void getNumIndices() throws CVC5ApiException
+  {
+    // Operators with 0 indices
+    Op plus = d_solver.mkOp(ADD);
+
+    assertEquals(0, plus.getNumIndices());
+
+    // Operators with 1 index
+    Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+    Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+    Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
+    Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
+    Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
+    Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
+    Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
+    Op iand = d_solver.mkOp(IAND, 11);
+    Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
+    Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+
+    assertEquals(1, divisible.getNumIndices());
+    assertEquals(1, bvRepeat.getNumIndices());
+    assertEquals(1, bvZeroExtend.getNumIndices());
+    assertEquals(1, bvSignExtend.getNumIndices());
+    assertEquals(1, bvRotateLeft.getNumIndices());
+    assertEquals(1, bvRotateRight.getNumIndices());
+    assertEquals(1, intToBv.getNumIndices());
+    assertEquals(1, iand.getNumIndices());
+    assertEquals(1, fpToUbv.getNumIndices());
+    assertEquals(1, fpToSbv.getNumIndices());
+
+    // Operators with 2 indices
+    Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
+    Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
+    Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
+    Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
+    Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
+    Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
+    Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
+    Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+
+    assertEquals(2, bvExtract.getNumIndices());
+    assertEquals(2, toFpFromIeeeBv.getNumIndices());
+    assertEquals(2, toFpFromFp.getNumIndices());
+    assertEquals(2, toFpFromReal.getNumIndices());
+    assertEquals(2, toFpFromSbv.getNumIndices());
+    assertEquals(2, toFpFromUbv.getNumIndices());
+    assertEquals(2, toFpGen.getNumIndices());
+    assertEquals(2, regexpLoop.getNumIndices());
+
+    // Operators with n indices
+    int[] indices = {0, 3, 2, 0, 1, 2};
+    Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
+    assertEquals(6, tupleProject.getNumIndices());
+  }
+
+  @Test void opSubscriptOperator() throws CVC5ApiException
+  {
+    // Operators with 0 indices
+    Op plus = d_solver.mkOp(ADD);
+
+    assertThrows(CVC5ApiException.class, () -> plus.get(0));
+
+    // Operators with 1 index
+    Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+    Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+    Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
+    Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
+    Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
+    Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
+    Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
+    Op iand = d_solver.mkOp(IAND, 11);
+    Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
+    Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+
+    assertEquals(4, divisible.get(0).getIntegerValue().intValue());
+    assertEquals(5, bvRepeat.get(0).getIntegerValue().intValue());
+    assertEquals(6, bvZeroExtend.get(0).getIntegerValue().intValue());
+    assertEquals(7, bvSignExtend.get(0).getIntegerValue().intValue());
+    assertEquals(8, bvRotateLeft.get(0).getIntegerValue().intValue());
+    assertEquals(9, bvRotateRight.get(0).getIntegerValue().intValue());
+    assertEquals(10, intToBv.get(0).getIntegerValue().intValue());
+    assertEquals(11, iand.get(0).getIntegerValue().intValue());
+    assertEquals(12, fpToUbv.get(0).getIntegerValue().intValue());
+    assertEquals(13, fpToSbv.get(0).getIntegerValue().intValue());
+
+    // Operators with 2 indices
+    Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
+    Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
+    Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
+    Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
+    Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
+    Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
+    Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
+    Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+
+    assertEquals(1, bvExtract.get(0).getIntegerValue().intValue());
+    assertEquals(0, bvExtract.get(1).getIntegerValue().intValue());
+    assertEquals(3, toFpFromIeeeBv.get(0).getIntegerValue().intValue());
+    assertEquals(2, toFpFromIeeeBv.get(1).getIntegerValue().intValue());
+    assertEquals(5, toFpFromFp.get(0).getIntegerValue().intValue());
+    assertEquals(4, toFpFromFp.get(1).getIntegerValue().intValue());
+    assertEquals(7, toFpFromReal.get(0).getIntegerValue().intValue());
+    assertEquals(6, toFpFromReal.get(1).getIntegerValue().intValue());
+    assertEquals(9, toFpFromSbv.get(0).getIntegerValue().intValue());
+    assertEquals(8, toFpFromSbv.get(1).getIntegerValue().intValue());
+    assertEquals(11, toFpFromUbv.get(0).getIntegerValue().intValue());
+    assertEquals(10, toFpFromUbv.get(1).getIntegerValue().intValue());
+    assertEquals(13, toFpGen.get(0).getIntegerValue().intValue());
+    assertEquals(12, toFpGen.get(1).getIntegerValue().intValue());
+    assertEquals(15, regexpLoop.get(0).getIntegerValue().intValue());
+    assertEquals(14, regexpLoop.get(1).getIntegerValue().intValue());
+
+    // Operators with n indices
+    int[] indices = {0, 3, 2, 0, 1, 2};
+    Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
+    for (int i = 0, size = tupleProject.getNumIndices(); i < size; i++)
+    {
+      assertEquals(
+          indices[i], tupleProject.get(i).getIntegerValue().intValue());
+    }
+  }
 
   @Test void opScopingToString() throws CVC5ApiException
   {

diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py
index 141c9d4e24d90061689035c5ffc240f0339d65d0..5a5d2ea865ea7406e27710a6662a3caaf5498aaa 100644 (file)
--- a/test/unit/api/python/test_op.py
+++ b/test/unit/api/python/test_op.py
@@ -46,7 +46,12 @@ def test_op_from_kind(solver):
 
 
 def test_get_num_indices(solver):
+    # Operators with 0 indices
     plus = solver.mkOp(Kind.Add)
+
+    assert 0 == plus.getNumIndices()
+
+    # Operators with 1 index
     divisible = solver.mkOp(Kind.Divisible, 4)
     bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5)
     bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6)
@@ -57,15 +62,7 @@ def test_get_num_indices(solver):
     iand = solver.mkOp(Kind.Iand, 3)
     floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11)
     floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13)
-    floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25)
-    floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 4, 25)
-    floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 4, 25)
-    floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 4, 25)
-    floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 4, 25)
-    floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25)
-    regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3)
 
-    assert 0 == plus.getNumIndices()
     assert 1 == divisible.getNumIndices()
     assert 1 == bitvector_repeat.getNumIndices()
     assert 1 == bitvector_zero_extend.getNumIndices()
@@ -76,6 +73,19 @@ def test_get_num_indices(solver):
     assert 1 == iand.getNumIndices()
     assert 1 == floatingpoint_to_ubv.getNumIndices()
     assert 1 == floatingopint_to_sbv.getNumIndices()
+
+    # Operators with 2 indices
+    bitvector_extract = solver.mkOp(Kind.BVExtract, 4, 25)
+    floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 4,
+                                                   25)
+    floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 4, 25)
+    floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 4, 25)
+    floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 4, 25)
+    floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 4, 25)
+    floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25)
+    regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3)
+
+    assert 2 == bitvector_extract.getNumIndices()
     assert 2 == floatingpoint_to_fp_from_ieee_bv.getNumIndices()
     assert 2 == floatingpoint_to_fp_from_fp.getNumIndices()
     assert 2 == floatingpoint_to_fp_from_real.getNumIndices()
@@ -84,92 +94,74 @@ def test_get_num_indices(solver):
     assert 2 == floatingpoint_to_fp_generic.getNumIndices()
     assert 2 == regexp_loop.getNumIndices()
 
-def test_op_indices_list(solver):
-    with_list = solver.mkOp(Kind.TupleProject, [4, 25])
-    assert 2 == with_list.getNumIndices()
+    # Operators with n indices
+    indices = [0, 3, 2, 0, 1, 2]
+    tuple_project_op = solver.mkOp(Kind.TupleProject, indices)
+    assert len(indices) == tuple_project_op.getNumIndices()
 
-def test_get_indices_string(solver):
-    x = Op(solver)
-    with pytest.raises(RuntimeError):
-        x.getIndices()
 
-    divisible_ot = solver.mkOp(Kind.Divisible, 4)
-    assert divisible_ot.isIndexed()
-    divisible_idx = divisible_ot.getIndices()
-    assert divisible_idx == "4"
+def test_subscript_operator(solver):
+    # Operators with 0 indices
+    plus = solver.mkOp(Kind.Add)
 
+    with pytest.raises(RuntimeError):
+        plus[0]
 
-def test_get_indices_uint(solver):
-    bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5)
-    assert bitvector_repeat_ot.isIndexed()
-    bitvector_repeat_idx = bitvector_repeat_ot.getIndices()
-    assert bitvector_repeat_idx == 5
-
-    bitvector_zero_extend_ot = solver.mkOp(Kind.BVZeroExtend, 6)
-    bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices()
-    assert bitvector_zero_extend_idx == 6
-
-    bitvector_sign_extend_ot = solver.mkOp(Kind.BVSignExtend, 7)
-    bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices()
-    assert bitvector_sign_extend_idx == 7
-
-    bitvector_rotate_left_ot = solver.mkOp(Kind.BVRotateLeft, 8)
-    bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices()
-    assert bitvector_rotate_left_idx == 8
-
-    bitvector_rotate_right_ot = solver.mkOp(Kind.BVRotateRight, 9)
-    bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices()
-    assert bitvector_rotate_right_idx == 9
-
-    int_to_bitvector_ot = solver.mkOp(Kind.IntToBV, 10)
-    int_to_bitvector_idx = int_to_bitvector_ot.getIndices()
-    assert int_to_bitvector_idx == 10
-
-    floatingpoint_to_ubv_ot = solver.mkOp(Kind.FPToUbv, 11)
-    floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices()
-    assert floatingpoint_to_ubv_idx == 11
-
-    floatingpoint_to_sbv_ot = solver.mkOp(Kind.FPToSbv, 13)
-    floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices()
-    assert floatingpoint_to_sbv_idx == 13
-
-
-def test_get_indices_pair_uint(solver):
-    bitvector_extract_ot = solver.mkOp(Kind.BVExtract, 4, 0)
-    assert bitvector_extract_ot.isIndexed()
-    bitvector_extract_indices = bitvector_extract_ot.getIndices()
-    assert bitvector_extract_indices == (4, 0)
-
-    floatingpoint_to_fp_from_ieee_bv_ot = \
-            solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25)
-    floatingpoint_to_fp_from_ieee_bv_indices = \
-            floatingpoint_to_fp_from_ieee_bv_ot.getIndices()
-    assert floatingpoint_to_fp_from_ieee_bv_indices == (4, 25)
-
-    floatingpoint_to_fp_from_fp_ot = solver.mkOp(Kind.FPToFpFromFp, 4, 25)
-    floatingpoint_to_fp_from_fp_indices = \
-            floatingpoint_to_fp_from_fp_ot.getIndices()
-    assert floatingpoint_to_fp_from_fp_indices == (4, 25)
-
-    floatingpoint_to_fp_from_real_ot = solver.mkOp(Kind.FPToFpFromReal, 4, 25)
-    floatingpoint_to_fp_from_real_indices = \
-            floatingpoint_to_fp_from_real_ot.getIndices()
-    assert floatingpoint_to_fp_from_real_indices == (4, 25)
-
-    floatingpoint_to_fp_from_sbv_ot = solver.mkOp(Kind.FPToFpFromSbv, 4, 25)
-    floatingpoint_to_fp_from_sbv_indices = \
-            floatingpoint_to_fp_from_sbv_ot.getIndices()
-    assert floatingpoint_to_fp_from_sbv_indices == (4, 25)
-
-    floatingpoint_to_fp_from_ubv_ot = solver.mkOp(Kind.FPToFpFromUbv, 4, 25)
-    floatingpoint_to_fp_from_ubv_indices = \
-            floatingpoint_to_fp_from_ubv_ot.getIndices()
-    assert floatingpoint_to_fp_from_ubv_indices == (4, 25)
-
-    floatingpoint_to_fp_generic_ot = solver.mkOp(Kind.FPToFpGeneric, 4, 25)
-    floatingpoint_to_fp_generic_indices = \
-            floatingpoint_to_fp_generic_ot.getIndices()
-    assert floatingpoint_to_fp_generic_indices == (4, 25)
+    # Operators with 1 index
+    divisible = solver.mkOp(Kind.Divisible, 4)
+    bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5)
+    bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6)
+    bitvector_sign_extend = solver.mkOp(Kind.BVSignExtend, 7)
+    bitvector_rotate_left = solver.mkOp(Kind.BVRotateLeft, 8)
+    bitvector_rotate_right = solver.mkOp(Kind.BVRotateRight, 9)
+    int_to_bitvector = solver.mkOp(Kind.IntToBV, 10)
+    iand = solver.mkOp(Kind.Iand, 11)
+    floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 12)
+    floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13)
+
+    assert 4 == divisible[0].getIntegerValue()
+    assert 5 == bitvector_repeat[0].getIntegerValue()
+    assert 6 == bitvector_zero_extend[0].getIntegerValue()
+    assert 7 == bitvector_sign_extend[0].getIntegerValue()
+    assert 8 == bitvector_rotate_left[0].getIntegerValue()
+    assert 9 == bitvector_rotate_right[0].getIntegerValue()
+    assert 10 == int_to_bitvector[0].getIntegerValue()
+    assert 11 == iand[0].getIntegerValue()
+    assert 12 == floatingpoint_to_ubv[0].getIntegerValue()
+    assert 13 == floatingopint_to_sbv[0].getIntegerValue()
+
+    # Operators with 2 indices
+    bitvector_extract = solver.mkOp(Kind.BVExtract, 1, 0)
+    floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 3, 2)
+    floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 5, 4)
+    floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 7, 6)
+    floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 9, 8)
+    floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 11, 10)
+    floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 13, 12)
+    regexp_loop = solver.mkOp(Kind.RegexpLoop, 15, 14)
+
+    assert 1 == bitvector_extract[0].getIntegerValue()
+    assert 0 == bitvector_extract[1].getIntegerValue()
+    assert 3 == floatingpoint_to_fp_from_ieee_bv[0].getIntegerValue()
+    assert 2 == floatingpoint_to_fp_from_ieee_bv[1].getIntegerValue()
+    assert 5 == floatingpoint_to_fp_from_fp[0].getIntegerValue()
+    assert 4 == floatingpoint_to_fp_from_fp[1].getIntegerValue()
+    assert 7 == floatingpoint_to_fp_from_real[0].getIntegerValue()
+    assert 6 == floatingpoint_to_fp_from_real[1].getIntegerValue()
+    assert 9 == floatingpoint_to_fp_from_sbv[0].getIntegerValue()
+    assert 8 == floatingpoint_to_fp_from_sbv[1].getIntegerValue()
+    assert 11 == floatingpoint_to_fp_from_ubv[0].getIntegerValue()
+    assert 10 == floatingpoint_to_fp_from_ubv[1].getIntegerValue()
+    assert 13 == floatingpoint_to_fp_generic[0].getIntegerValue()
+    assert 12 == floatingpoint_to_fp_generic[1].getIntegerValue()
+    assert 15 == regexp_loop[0].getIntegerValue()
+    assert 14 == regexp_loop[1].getIntegerValue()
+
+    # Operators with n indices
+    indices = [0, 3, 2, 0, 1, 2]
+    tuple_project_op = solver.mkOp(Kind.TupleProject, indices)
+    for i in range(len(indices)):
+        assert indices[i] == tuple_project_op[i].getIntegerValue()
 
 
 def test_op_scoping_to_string(solver):