Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of the Op class.
11 : : */
12 : :
13 : : #include "test_api.h"
14 : :
15 : : namespace cvc5::internal {
16 : :
17 : : namespace test {
18 : :
19 : : class TestApiBlackOp : public TestApi
20 : : {
21 : : };
22 : :
23 : 4 : TEST_F(TestApiBlackOp, hash)
24 : : {
25 : : std::hash<Op> h;
26 [ - + ]: 1 : ASSERT_EQ(h(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1})),
27 [ + - ]: 1 : h(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1})));
28 [ - + ]: 1 : ASSERT_NE(h(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1})),
29 [ + - ]: 1 : h(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 2})));
30 : 1 : (void)std::hash<Op>{}(Op());
31 : : }
32 : :
33 : 4 : TEST_F(TestApiBlackOp, getKind)
34 : : {
35 : 1 : Op x = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1});
36 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getKind(), Kind::BITVECTOR_EXTRACT);
37 [ + - ]: 1 : }
38 : :
39 : 4 : TEST_F(TestApiBlackOp, isNull)
40 : : {
41 : 1 : Op x;
42 [ - + ][ + - ]: 1 : ASSERT_TRUE(x.isNull());
43 : 1 : Op y = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1});
44 [ - + ][ + - ]: 1 : ASSERT_FALSE(y.isNull());
45 [ - + ][ + - ]: 1 : ASSERT_NE(x, y);
46 [ + - ]: 1 : }
47 : :
48 : 4 : TEST_F(TestApiBlackOp, opFromKind)
49 : : {
50 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(d_tm.mkOp(Kind::ADD));
[ + - ][ - - ]
51 : 2 : ASSERT_THROW(d_tm.mkOp(Kind::BITVECTOR_EXTRACT), CVC5ApiException);
52 : : }
53 : :
54 : 4 : TEST_F(TestApiBlackOp, getNumIndices)
55 : : {
56 : : // Operators with 0 indices
57 : 1 : Op plus = d_tm.mkOp(Kind::ADD);
58 : :
59 [ - + ][ + - ]: 1 : ASSERT_EQ(0, plus.getNumIndices());
60 : :
61 : : // Operators with 1 index
62 : 1 : Op divisible = d_tm.mkOp(Kind::DIVISIBLE, {4});
63 : 1 : Op bvRepeat = d_tm.mkOp(Kind::BITVECTOR_REPEAT, {5});
64 : 1 : Op bvZeroExtend = d_tm.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {6});
65 : 1 : Op bvSignExtend = d_tm.mkOp(Kind::BITVECTOR_SIGN_EXTEND, {7});
66 : 1 : Op bvRotateLeft = d_tm.mkOp(Kind::BITVECTOR_ROTATE_LEFT, {8});
67 : 1 : Op bvRotateRight = d_tm.mkOp(Kind::BITVECTOR_ROTATE_RIGHT, {9});
68 : 1 : Op intToBv = d_tm.mkOp(Kind::INT_TO_BITVECTOR, {10});
69 : 1 : Op iand = d_tm.mkOp(Kind::IAND, {11});
70 : 1 : Op fpToUbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_UBV, {12});
71 : 1 : Op fpToSbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_SBV, {13});
72 : :
73 [ - + ][ + - ]: 1 : ASSERT_EQ(1, divisible.getNumIndices());
74 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvRepeat.getNumIndices());
75 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvZeroExtend.getNumIndices());
76 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvSignExtend.getNumIndices());
77 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvRotateLeft.getNumIndices());
78 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvRotateRight.getNumIndices());
79 [ - + ][ + - ]: 1 : ASSERT_EQ(1, intToBv.getNumIndices());
80 [ - + ][ + - ]: 1 : ASSERT_EQ(1, iand.getNumIndices());
81 [ - + ][ + - ]: 1 : ASSERT_EQ(1, fpToUbv.getNumIndices());
82 [ - + ][ + - ]: 1 : ASSERT_EQ(1, fpToSbv.getNumIndices());
83 : :
84 : : // Operators with 2 indices
85 : 1 : Op bvExtract = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {1, 0});
86 : 1 : Op toFpFromIeeeBv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, {3, 2});
87 : 1 : Op toFpFromFp = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_FP, {5, 4});
88 : 1 : Op toFpFromReal = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_REAL, {7, 6});
89 : 1 : Op toFpFromSbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_SBV, {9, 8});
90 : 1 : Op toFpFromUbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_UBV, {11, 10});
91 : 1 : Op regexpLoop = d_tm.mkOp(Kind::REGEXP_LOOP, {15, 14});
92 : :
93 [ - + ][ + - ]: 1 : ASSERT_EQ(2, bvExtract.getNumIndices());
94 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromIeeeBv.getNumIndices());
95 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromFp.getNumIndices());
96 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromReal.getNumIndices());
97 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromSbv.getNumIndices());
98 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromUbv.getNumIndices());
99 [ - + ][ + - ]: 1 : ASSERT_EQ(2, regexpLoop.getNumIndices());
100 : :
101 : : // Operators with n indices
102 : 1 : std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
103 : 1 : Op tupleProject = d_tm.mkOp(Kind::TUPLE_PROJECT, indices);
104 [ - + ][ + - ]: 1 : ASSERT_EQ(indices.size(), tupleProject.getNumIndices());
105 : :
106 : 1 : Op relationProject = d_tm.mkOp(Kind::RELATION_PROJECT, indices);
107 [ - + ][ + - ]: 1 : ASSERT_EQ(indices.size(), relationProject.getNumIndices());
108 : :
109 : 1 : Op tableProject = d_tm.mkOp(Kind::TABLE_PROJECT, indices);
110 [ - + ][ + - ]: 1 : ASSERT_EQ(indices.size(), tableProject.getNumIndices());
111 [ + - ]: 1 : }
112 : :
113 : 4 : TEST_F(TestApiBlackOp, subscriptOperator)
114 : : {
115 : : // Operators with 0 indices
116 : 1 : Op plus = d_tm.mkOp(Kind::ADD);
117 : :
118 : 1 : ASSERT_THROW(plus[0], CVC5ApiException);
119 : :
120 : : // Operators with 1 index
121 : 1 : Op divisible = d_tm.mkOp(Kind::DIVISIBLE, {4});
122 : 1 : Op bvRepeat = d_tm.mkOp(Kind::BITVECTOR_REPEAT, {5});
123 : 1 : Op bvZeroExtend = d_tm.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {6});
124 : 1 : Op bvSignExtend = d_tm.mkOp(Kind::BITVECTOR_SIGN_EXTEND, {7});
125 : 1 : Op bvRotateLeft = d_tm.mkOp(Kind::BITVECTOR_ROTATE_LEFT, {8});
126 : 1 : Op bvRotateRight = d_tm.mkOp(Kind::BITVECTOR_ROTATE_RIGHT, {9});
127 : 1 : Op intToBv = d_tm.mkOp(Kind::INT_TO_BITVECTOR, {10});
128 : 1 : Op iand = d_tm.mkOp(Kind::IAND, {11});
129 : 1 : Op fpToUbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_UBV, {12});
130 : 1 : Op fpToSbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_SBV, {13});
131 : 1 : Op regexpRepeat = d_tm.mkOp(Kind::REGEXP_REPEAT, {14});
132 : :
133 [ - + ][ + - ]: 1 : ASSERT_EQ(4, divisible[0].getUInt32Value());
134 [ - + ][ + - ]: 1 : ASSERT_EQ(5, bvRepeat[0].getUInt32Value());
135 [ - + ][ + - ]: 1 : ASSERT_EQ(6, bvZeroExtend[0].getUInt32Value());
136 [ - + ][ + - ]: 1 : ASSERT_EQ(7, bvSignExtend[0].getUInt32Value());
137 [ - + ][ + - ]: 1 : ASSERT_EQ(8, bvRotateLeft[0].getUInt32Value());
138 [ - + ][ + - ]: 1 : ASSERT_EQ(9, bvRotateRight[0].getUInt32Value());
139 [ - + ][ + - ]: 1 : ASSERT_EQ(10, intToBv[0].getUInt32Value());
140 [ - + ][ + - ]: 1 : ASSERT_EQ(11, iand[0].getUInt32Value());
141 [ - + ][ + - ]: 1 : ASSERT_EQ(12, fpToUbv[0].getUInt32Value());
142 [ - + ][ + - ]: 1 : ASSERT_EQ(13, fpToSbv[0].getUInt32Value());
143 [ - + ][ + - ]: 1 : ASSERT_EQ(14, regexpRepeat[0].getUInt32Value());
144 : :
145 : : // Operators with 2 indices
146 : 1 : Op bvExtract = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {1, 0});
147 : 1 : Op toFpFromIeeeBv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, {3, 2});
148 : 1 : Op toFpFromFp = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_FP, {5, 4});
149 : 1 : Op toFpFromReal = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_REAL, {7, 6});
150 : 1 : Op toFpFromSbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_SBV, {9, 8});
151 : 1 : Op toFpFromUbv = d_tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_UBV, {11, 10});
152 : 1 : Op regexpLoop = d_tm.mkOp(Kind::REGEXP_LOOP, {15, 14});
153 : :
154 [ - + ][ + - ]: 1 : ASSERT_EQ(1, bvExtract[0].getUInt32Value());
155 [ - + ][ + - ]: 1 : ASSERT_EQ(0, bvExtract[1].getUInt32Value());
156 [ - + ][ + - ]: 1 : ASSERT_EQ(3, toFpFromIeeeBv[0].getUInt32Value());
157 [ - + ][ + - ]: 1 : ASSERT_EQ(2, toFpFromIeeeBv[1].getUInt32Value());
158 [ - + ][ + - ]: 1 : ASSERT_EQ(5, toFpFromFp[0].getUInt32Value());
159 [ - + ][ + - ]: 1 : ASSERT_EQ(4, toFpFromFp[1].getUInt32Value());
160 [ - + ][ + - ]: 1 : ASSERT_EQ(7, toFpFromReal[0].getUInt32Value());
161 [ - + ][ + - ]: 1 : ASSERT_EQ(6, toFpFromReal[1].getUInt32Value());
162 [ - + ][ + - ]: 1 : ASSERT_EQ(9, toFpFromSbv[0].getUInt32Value());
163 [ - + ][ + - ]: 1 : ASSERT_EQ(8, toFpFromSbv[1].getUInt32Value());
164 [ - + ][ + - ]: 1 : ASSERT_EQ(11, toFpFromUbv[0].getUInt32Value());
165 [ - + ][ + - ]: 1 : ASSERT_EQ(10, toFpFromUbv[1].getUInt32Value());
166 [ - + ][ + - ]: 1 : ASSERT_EQ(15, regexpLoop[0].getUInt32Value());
167 [ - + ][ + - ]: 1 : ASSERT_EQ(14, regexpLoop[1].getUInt32Value());
168 : :
169 : : // Operators with n indices
170 : 1 : std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
171 : 1 : Op tupleProject = d_tm.mkOp(Kind::TUPLE_PROJECT, indices);
172 [ + + ]: 7 : for (size_t i = 0, size = tupleProject.getNumIndices(); i < size; i++)
173 : : {
174 [ - + ][ + - ]: 6 : ASSERT_EQ(indices[i], tupleProject[i].getUInt32Value());
175 : : }
176 [ + - ]: 1 : }
177 : :
178 : 4 : TEST_F(TestApiBlackOp, opScopingToString)
179 : : {
180 : 1 : Op bitvector_repeat_ot = d_tm.mkOp(Kind::BITVECTOR_REPEAT, {5});
181 : 1 : std::string op_repr = bitvector_repeat_ot.toString();
182 [ - + ][ + - ]: 2 : ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr);
183 : : {
184 : 1 : std::stringstream ss;
185 : 1 : ss << bitvector_repeat_ot;
186 [ - + ][ + - ]: 2 : ASSERT_EQ(ss.str(), op_repr);
187 [ + - ]: 1 : }
188 [ + - ][ + - ]: 1 : }
189 : : } // namespace test
190 : : } // namespace cvc5::internal
|
