1 ###############################################################################
2 # Top contributors (to current version):
3 # Aina Niemetz, Andres Noetzli, Yoni Zohar
5 # This file is part of the cvc5 project.
7 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 # in the top-level source directory and their institutional affiliations.
9 # All rights reserved. See the file COPYING in the top-level source
10 # directory for licensing information.
11 # #############################################################################
13 # Unit tests for op API.
15 # Obtained by translating test/unit/api/op_black.cpp
30 def test_hash(solver
):
31 hash(solver
.mkOp(Kind
.BITVECTOR_EXTRACT
, 31, 1))
33 def test_get_kind(solver
):
34 x
= solver
.mkOp(Kind
.BITVECTOR_EXTRACT
, 31, 1)
38 def test_is_null(solver
):
41 y
= solver
.mkOp(Kind
.BITVECTOR_EXTRACT
, 31, 1)
46 def test_op_from_kind(solver
):
48 with pytest
.raises(RuntimeError):
49 solver
.mkOp(Kind
.BITVECTOR_EXTRACT
)
52 def test_get_num_indices(solver
):
53 # Operators with 0 indices
54 plus
= solver
.mkOp(Kind
.ADD
)
56 assert 0 == plus
.getNumIndices()
58 # Operators with 1 index
59 divisible
= solver
.mkOp(Kind
.DIVISIBLE
, 4)
60 bitvector_repeat
= solver
.mkOp(Kind
.BITVECTOR_REPEAT
, 5)
61 bitvector_zero_extend
= solver
.mkOp(Kind
.BITVECTOR_ZERO_EXTEND
, 6)
62 bitvector_sign_extend
= solver
.mkOp(Kind
.BITVECTOR_SIGN_EXTEND
, 7)
63 bitvector_rotate_left
= solver
.mkOp(Kind
.BITVECTOR_ROTATE_LEFT
, 8)
64 bitvector_rotate_right
= solver
.mkOp(Kind
.BITVECTOR_ROTATE_RIGHT
, 9)
65 int_to_bitvector
= solver
.mkOp(Kind
.INT_TO_BITVECTOR
, 10)
66 iand
= solver
.mkOp(Kind
.IAND
, 3)
67 floatingpoint_to_ubv
= solver
.mkOp(Kind
.FLOATINGPOINT_TO_UBV
, 11)
68 floatingopint_to_sbv
= solver
.mkOp(Kind
.FLOATINGPOINT_TO_SBV
, 13)
70 assert 1 == divisible
.getNumIndices()
71 assert 1 == bitvector_repeat
.getNumIndices()
72 assert 1 == bitvector_zero_extend
.getNumIndices()
73 assert 1 == bitvector_sign_extend
.getNumIndices()
74 assert 1 == bitvector_rotate_left
.getNumIndices()
75 assert 1 == bitvector_rotate_right
.getNumIndices()
76 assert 1 == int_to_bitvector
.getNumIndices()
77 assert 1 == iand
.getNumIndices()
78 assert 1 == floatingpoint_to_ubv
.getNumIndices()
79 assert 1 == floatingopint_to_sbv
.getNumIndices()
81 # Operators with 2 indices
82 bitvector_extract
= solver
.mkOp(Kind
.BITVECTOR_EXTRACT
, 4, 25)
83 floatingpoint_to_fp_from_ieee_bv
= solver
.mkOp(
84 Kind
.FLOATINGPOINT_TO_FP_FROM_IEEE_BV
, 4, 25)
85 floatingpoint_to_fp_from_fp
= solver
.mkOp(
86 Kind
.FLOATINGPOINT_TO_FP_FROM_FP
, 4, 25)
87 floatingpoint_to_fp_from_real
= solver
.mkOp(
88 Kind
.FLOATINGPOINT_TO_FP_FROM_REAL
, 4, 25)
89 floatingpoint_to_fp_from_sbv
= solver
.mkOp(
90 Kind
.FLOATINGPOINT_TO_FP_FROM_SBV
, 4, 25)
91 floatingpoint_to_fp_from_ubv
= solver
.mkOp(
92 Kind
.FLOATINGPOINT_TO_FP_FROM_UBV
, 4, 25)
93 regexp_loop
= solver
.mkOp(Kind
.REGEXP_LOOP
, 2, 3)
95 assert 2 == bitvector_extract
.getNumIndices()
96 assert 2 == floatingpoint_to_fp_from_ieee_bv
.getNumIndices()
97 assert 2 == floatingpoint_to_fp_from_fp
.getNumIndices()
98 assert 2 == floatingpoint_to_fp_from_real
.getNumIndices()
99 assert 2 == floatingpoint_to_fp_from_sbv
.getNumIndices()
100 assert 2 == floatingpoint_to_fp_from_ubv
.getNumIndices()
101 assert 2 == regexp_loop
.getNumIndices()
103 # Operators with n indices
104 indices
= [0, 3, 2, 0, 1, 2]
105 tuple_project_op
= solver
.mkOp(Kind
.TUPLE_PROJECT
, *indices
)
106 assert len(indices
) == tuple_project_op
.getNumIndices()
109 def test_subscript_operator(solver
):
110 # Operators with 0 indices
111 plus
= solver
.mkOp(Kind
.ADD
)
113 with pytest
.raises(RuntimeError):
116 # Operators with 1 index
117 divisible
= solver
.mkOp(Kind
.DIVISIBLE
, 4)
118 bitvector_repeat
= solver
.mkOp(Kind
.BITVECTOR_REPEAT
, 5)
119 bitvector_zero_extend
= solver
.mkOp(Kind
.BITVECTOR_ZERO_EXTEND
, 6)
120 bitvector_sign_extend
= solver
.mkOp(Kind
.BITVECTOR_SIGN_EXTEND
, 7)
121 bitvector_rotate_left
= solver
.mkOp(Kind
.BITVECTOR_ROTATE_LEFT
, 8)
122 bitvector_rotate_right
= solver
.mkOp(Kind
.BITVECTOR_ROTATE_RIGHT
, 9)
123 int_to_bitvector
= solver
.mkOp(Kind
.INT_TO_BITVECTOR
, 10)
124 iand
= solver
.mkOp(Kind
.IAND
, 11)
125 floatingpoint_to_ubv
= solver
.mkOp(Kind
.FLOATINGPOINT_TO_UBV
, 12)
126 floatingopint_to_sbv
= solver
.mkOp(Kind
.FLOATINGPOINT_TO_SBV
, 13)
128 assert 4 == divisible
[0].getIntegerValue()
129 assert 5 == bitvector_repeat
[0].getIntegerValue()
130 assert 6 == bitvector_zero_extend
[0].getIntegerValue()
131 assert 7 == bitvector_sign_extend
[0].getIntegerValue()
132 assert 8 == bitvector_rotate_left
[0].getIntegerValue()
133 assert 9 == bitvector_rotate_right
[0].getIntegerValue()
134 assert 10 == int_to_bitvector
[0].getIntegerValue()
135 assert 11 == iand
[0].getIntegerValue()
136 assert 12 == floatingpoint_to_ubv
[0].getIntegerValue()
137 assert 13 == floatingopint_to_sbv
[0].getIntegerValue()
139 # Operators with 2 indices
140 bitvector_extract
= solver
.mkOp(Kind
.BITVECTOR_EXTRACT
, 1, 0)
141 floatingpoint_to_fp_from_ieee_bv
= solver
.mkOp(
142 Kind
.FLOATINGPOINT_TO_FP_FROM_IEEE_BV
, 3, 2)
143 floatingpoint_to_fp_from_fp
= solver
.mkOp(
144 Kind
.FLOATINGPOINT_TO_FP_FROM_FP
, 5, 4)
145 floatingpoint_to_fp_from_real
= solver
.mkOp(
146 Kind
.FLOATINGPOINT_TO_FP_FROM_REAL
, 7, 6)
147 floatingpoint_to_fp_from_sbv
= solver
.mkOp(
148 Kind
.FLOATINGPOINT_TO_FP_FROM_SBV
, 9, 8)
149 floatingpoint_to_fp_from_ubv
= solver
.mkOp(
150 Kind
.FLOATINGPOINT_TO_FP_FROM_UBV
, 11, 10)
151 regexp_loop
= solver
.mkOp(Kind
.REGEXP_LOOP
, 15, 14)
153 assert 1 == bitvector_extract
[0].getIntegerValue()
154 assert 0 == bitvector_extract
[1].getIntegerValue()
155 assert 3 == floatingpoint_to_fp_from_ieee_bv
[0].getIntegerValue()
156 assert 2 == floatingpoint_to_fp_from_ieee_bv
[1].getIntegerValue()
157 assert 5 == floatingpoint_to_fp_from_fp
[0].getIntegerValue()
158 assert 4 == floatingpoint_to_fp_from_fp
[1].getIntegerValue()
159 assert 7 == floatingpoint_to_fp_from_real
[0].getIntegerValue()
160 assert 6 == floatingpoint_to_fp_from_real
[1].getIntegerValue()
161 assert 9 == floatingpoint_to_fp_from_sbv
[0].getIntegerValue()
162 assert 8 == floatingpoint_to_fp_from_sbv
[1].getIntegerValue()
163 assert 11 == floatingpoint_to_fp_from_ubv
[0].getIntegerValue()
164 assert 10 == floatingpoint_to_fp_from_ubv
[1].getIntegerValue()
165 assert 15 == regexp_loop
[0].getIntegerValue()
166 assert 14 == regexp_loop
[1].getIntegerValue()
168 # Operators with n indices
169 indices
= [0, 3, 2, 0, 1, 2]
170 tuple_project_op
= solver
.mkOp(Kind
.TUPLE_PROJECT
, *indices
)
171 for i
in range(len(indices
)):
172 assert indices
[i
] == tuple_project_op
[i
].getIntegerValue()
175 def test_op_scoping_to_string(solver
):
176 bitvector_repeat_ot
= solver
.mkOp(Kind
.BITVECTOR_REPEAT
, 5)
177 op_repr
= str(bitvector_repeat_ot
)
178 assert str(bitvector_repeat_ot
) == op_repr