From: Andres Noetzli Date: Tue, 22 Mar 2022 00:00:58 +0000 (-0700) Subject: [API] Support `Op::operator[]` in Java and Python (#8356) X-Git-Tag: cvc5-1.0.0~216 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e3f8ea19324685c25df378bd078a11bfcf639b77;p=cvc5.git [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 1263465e0..87d85c963 100644 --- 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 83072e88c..7ec481fc6 100644 --- 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(pointer); + Term* ret = new Term((*current)[static_cast(i)]); + return reinterpret_cast(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 0251790e7..7f0037d99 100644 --- 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 e861473cc..f90cd5fa2 100644 --- 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 8792b5df1..0dfe9cdb5 100644 --- 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 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 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 17a7aee9a..47793aa63 100644 --- 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 141c9d4e2..5a5d2ea86 100644 --- 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):