python api unit tests for Op (#6785)

Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.

The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.

For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ada34e75de10c6b72a8ab6ce4aeb675e1fb3f19d..99e471b0a6f4cd29c41701aac2af32292f7b1d5b 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -122,6 +122,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort getSort() except +
         bint isNull() except +
         bint isIndexed() except +
+        size_t getNumIndices() except +
         T getIndices[T]() except +
         string toString() except +
 

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 7f01cb8a11e985a68c4e7ebaa44729d9a87671f6..d31fdc126a8abbe4758a8aec73633643202fd977 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -345,10 +345,13 @@ cdef class Op:
     def isNull(self):
         return self.cop.isNull()
 
+    def getNumIndices(self):
+        return self.cop.getNumIndices()
+
     def getIndices(self):
         indices = None
         try:
-            indices = self.cop.getIndices[string]()
+            indices = self.cop.getIndices[string]().decode()
         except:
             pass
 

diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index cefc16a07c25ded50e2b3bd545381236836c2b69..5b681ca36614958a9f547d6f919557048ae9b9f4 100644 (file)
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -33,4 +33,5 @@ cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
 cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py)
 cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
 cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py)
+cvc5_add_python_api_test(pytest_op unit/api/test_op.py)
 cvc5_add_python_api_test(pytest_result unit/api/test_result.py)

diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py
new file mode 100644 (file)
index 0000000..07a57a5
--- /dev/null
+++ b/test/python/unit/api/test_op.py
@@ -0,0 +1,178 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# 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.
+# #############################################################################
+#
+# Unit tests for op API.
+#
+# Obtained by translating test/unit/api/op_black.cpp
+##
+
+import pytest
+import pycvc5
+from pycvc5 import kinds
+from pycvc5 import Sort
+from pycvc5 import Op
+
+
+@pytest.fixture
+def solver():
+    return pycvc5.Solver()
+
+
+def test_get_kind(solver):
+    x = solver.mkOp(kinds.BVExtract, 31, 1)
+    x.getKind()
+
+
+def test_is_null(solver):
+    x = Op(solver)
+    assert x.isNull()
+    x = solver.mkOp(kinds.BVExtract, 31, 1)
+    assert not x.isNull()
+
+
+def test_op_from_kind(solver):
+    solver.mkOp(kinds.Plus)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.BVExtract)
+
+
+def test_get_num_indices(solver):
+    plus = solver.mkOp(kinds.Plus)
+    divisible = solver.mkOp(kinds.Divisible, 4)
+    bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5)
+    bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6)
+    bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7)
+    bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8)
+    bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9)
+    int_to_bitvector = solver.mkOp(kinds.IntToBV, 10)
+    iand = solver.mkOp(kinds.Iand, 3)
+    floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11)
+    floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13)
+    floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25)
+    floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25)
+    floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25)
+    floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4,
+                                                       25)
+    floatingpoint_to_fp_unsigned_bitvector = solver.mkOp(
+        kinds.FPToFpUnsignedBV, 4, 25)
+    floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25)
+    regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3)
+
+    assert 0 == plus.getNumIndices()
+    assert 1 == divisible.getNumIndices()
+    assert 1 == bitvector_repeat.getNumIndices()
+    assert 1 == bitvector_zero_extend.getNumIndices()
+    assert 1 == bitvector_sign_extend.getNumIndices()
+    assert 1 == bitvector_rotate_left.getNumIndices()
+    assert 1 == bitvector_rotate_right.getNumIndices()
+    assert 1 == int_to_bitvector.getNumIndices()
+    assert 1 == iand.getNumIndices()
+    assert 1 == floatingpoint_to_ubv.getNumIndices()
+    assert 1 == floatingopint_to_sbv.getNumIndices()
+    assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices()
+    assert 2 == floatingpoint_to_fp_real.getNumIndices()
+    assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_generic.getNumIndices()
+    assert 2 == regexp_loop.getNumIndices()
+
+
+def test_get_indices_string(solver):
+    x = Op(solver)
+    with pytest.raises(RuntimeError):
+        x.getIndices()
+
+    divisible_ot = solver.mkOp(kinds.Divisible, 4)
+    assert divisible_ot.isIndexed()
+    divisible_idx = divisible_ot.getIndices()
+    assert divisible_idx == "4"
+
+
+def test_get_indices_uint(solver):
+    bitvector_repeat_ot = solver.mkOp(kinds.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(kinds.BVZeroExtend, 6)
+    bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices()
+    assert bitvector_zero_extend_idx == 6
+
+    bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7)
+    bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices()
+    assert bitvector_sign_extend_idx == 7
+
+    bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8)
+    bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices()
+    assert bitvector_rotate_left_idx == 8
+
+    bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9)
+    bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices()
+    assert bitvector_rotate_right_idx == 9
+
+    int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10)
+    int_to_bitvector_idx = int_to_bitvector_ot.getIndices()
+    assert int_to_bitvector_idx == 10
+
+    floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11)
+    floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices()
+    assert floatingpoint_to_ubv_idx == 11
+
+    floatingpoint_to_sbv_ot = solver.mkOp(kinds.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(kinds.BVExtract, 4, 0)
+    assert bitvector_extract_ot.isIndexed()
+    bitvector_extract_indices = bitvector_extract_ot.getIndices()
+    assert bitvector_extract_indices == (4, 0)
+
+    floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp(
+        kinds.FPToFpIeeeBV, 4, 25)
+    floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices(
+    )
+    assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25)
+
+    floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25)
+    floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices(
+    )
+    assert floatingpoint_to_fp_floatingpoint_indices == (4, 25)
+
+    floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25)
+    floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices()
+    assert floatingpoint_to_fp_real_indices == (4, 25)
+
+    floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp(
+        kinds.FPToFpSignedBV, 4, 25)
+    floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices(
+    )
+    assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25)
+
+    floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp(
+        kinds.FPToFpUnsignedBV, 4, 25)
+    floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices(
+    )
+    assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25)
+
+    floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25)
+    floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices(
+    )
+    assert floatingpoint_to_fp_generic_indices == (4, 25)
+
+
+def test_op_scoping_to_string(solver):
+    bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5)
+    op_repr = str(bitvector_repeat_ot)
+    assert str(bitvector_repeat_ot) == op_repr