1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Makai Mann, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Black box testing of the Term class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "test_api.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
|
20 |
|
using namespace api; |
21 |
|
|
22 |
|
namespace test { |
23 |
|
|
24 |
128 |
class TestApiBlackTerm : public TestApi |
25 |
|
{ |
26 |
|
}; |
27 |
|
|
28 |
41 |
TEST_F(TestApiBlackTerm, eq) |
29 |
|
{ |
30 |
4 |
Sort uSort = d_solver.mkUninterpretedSort("u"); |
31 |
4 |
Term x = d_solver.mkVar(uSort, "x"); |
32 |
4 |
Term y = d_solver.mkVar(uSort, "y"); |
33 |
4 |
Term z; |
34 |
|
|
35 |
2 |
ASSERT_TRUE(x == x); |
36 |
2 |
ASSERT_FALSE(x != x); |
37 |
2 |
ASSERT_FALSE(x == y); |
38 |
2 |
ASSERT_TRUE(x != y); |
39 |
2 |
ASSERT_FALSE((x == z)); |
40 |
2 |
ASSERT_TRUE(x != z); |
41 |
|
} |
42 |
|
|
43 |
41 |
TEST_F(TestApiBlackTerm, getId) |
44 |
|
{ |
45 |
4 |
Term n; |
46 |
4 |
ASSERT_THROW(n.getId(), CVC5ApiException); |
47 |
4 |
Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); |
48 |
2 |
ASSERT_NO_THROW(x.getId()); |
49 |
4 |
Term y = x; |
50 |
2 |
ASSERT_EQ(x.getId(), y.getId()); |
51 |
|
|
52 |
4 |
Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z"); |
53 |
2 |
ASSERT_NE(x.getId(), z.getId()); |
54 |
|
} |
55 |
|
|
56 |
41 |
TEST_F(TestApiBlackTerm, getKind) |
57 |
|
{ |
58 |
4 |
Sort uSort = d_solver.mkUninterpretedSort("u"); |
59 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
60 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
61 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort); |
62 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
63 |
|
|
64 |
4 |
Term n; |
65 |
4 |
ASSERT_THROW(n.getKind(), CVC5ApiException); |
66 |
4 |
Term x = d_solver.mkVar(uSort, "x"); |
67 |
2 |
ASSERT_NO_THROW(x.getKind()); |
68 |
4 |
Term y = d_solver.mkVar(uSort, "y"); |
69 |
2 |
ASSERT_NO_THROW(y.getKind()); |
70 |
|
|
71 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
72 |
2 |
ASSERT_NO_THROW(f.getKind()); |
73 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
74 |
2 |
ASSERT_NO_THROW(p.getKind()); |
75 |
|
|
76 |
4 |
Term zero = d_solver.mkInteger(0); |
77 |
2 |
ASSERT_NO_THROW(zero.getKind()); |
78 |
|
|
79 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
80 |
2 |
ASSERT_NO_THROW(f_x.getKind()); |
81 |
4 |
Term f_y = d_solver.mkTerm(APPLY_UF, f, y); |
82 |
2 |
ASSERT_NO_THROW(f_y.getKind()); |
83 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_y); |
84 |
2 |
ASSERT_NO_THROW(sum.getKind()); |
85 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
86 |
2 |
ASSERT_NO_THROW(p_0.getKind()); |
87 |
4 |
Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); |
88 |
2 |
ASSERT_NO_THROW(p_f_y.getKind()); |
89 |
|
|
90 |
|
// Sequence kinds do not exist internally, test that the API properly |
91 |
|
// converts them back. |
92 |
4 |
Sort seqSort = d_solver.mkSequenceSort(intSort); |
93 |
4 |
Term s = d_solver.mkConst(seqSort, "s"); |
94 |
4 |
Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); |
95 |
2 |
ASSERT_EQ(ss.getKind(), SEQ_CONCAT); |
96 |
|
} |
97 |
|
|
98 |
41 |
TEST_F(TestApiBlackTerm, getSort) |
99 |
|
{ |
100 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
101 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
102 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
103 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
104 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
105 |
|
|
106 |
4 |
Term n; |
107 |
4 |
ASSERT_THROW(n.getSort(), CVC5ApiException); |
108 |
4 |
Term x = d_solver.mkVar(bvSort, "x"); |
109 |
2 |
ASSERT_NO_THROW(x.getSort()); |
110 |
2 |
ASSERT_EQ(x.getSort(), bvSort); |
111 |
4 |
Term y = d_solver.mkVar(bvSort, "y"); |
112 |
2 |
ASSERT_NO_THROW(y.getSort()); |
113 |
2 |
ASSERT_EQ(y.getSort(), bvSort); |
114 |
|
|
115 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
116 |
2 |
ASSERT_NO_THROW(f.getSort()); |
117 |
2 |
ASSERT_EQ(f.getSort(), funSort1); |
118 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
119 |
2 |
ASSERT_NO_THROW(p.getSort()); |
120 |
2 |
ASSERT_EQ(p.getSort(), funSort2); |
121 |
|
|
122 |
4 |
Term zero = d_solver.mkInteger(0); |
123 |
2 |
ASSERT_NO_THROW(zero.getSort()); |
124 |
2 |
ASSERT_EQ(zero.getSort(), intSort); |
125 |
|
|
126 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
127 |
2 |
ASSERT_NO_THROW(f_x.getSort()); |
128 |
2 |
ASSERT_EQ(f_x.getSort(), intSort); |
129 |
4 |
Term f_y = d_solver.mkTerm(APPLY_UF, f, y); |
130 |
2 |
ASSERT_NO_THROW(f_y.getSort()); |
131 |
2 |
ASSERT_EQ(f_y.getSort(), intSort); |
132 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_y); |
133 |
2 |
ASSERT_NO_THROW(sum.getSort()); |
134 |
2 |
ASSERT_EQ(sum.getSort(), intSort); |
135 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
136 |
2 |
ASSERT_NO_THROW(p_0.getSort()); |
137 |
2 |
ASSERT_EQ(p_0.getSort(), boolSort); |
138 |
4 |
Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); |
139 |
2 |
ASSERT_NO_THROW(p_f_y.getSort()); |
140 |
2 |
ASSERT_EQ(p_f_y.getSort(), boolSort); |
141 |
|
} |
142 |
|
|
143 |
41 |
TEST_F(TestApiBlackTerm, getOp) |
144 |
|
{ |
145 |
4 |
Sort intsort = d_solver.getIntegerSort(); |
146 |
4 |
Sort bvsort = d_solver.mkBitVectorSort(8); |
147 |
4 |
Sort arrsort = d_solver.mkArraySort(bvsort, intsort); |
148 |
4 |
Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); |
149 |
|
|
150 |
4 |
Term x = d_solver.mkConst(intsort, "x"); |
151 |
4 |
Term a = d_solver.mkConst(arrsort, "a"); |
152 |
4 |
Term b = d_solver.mkConst(bvsort, "b"); |
153 |
|
|
154 |
2 |
ASSERT_FALSE(x.hasOp()); |
155 |
4 |
ASSERT_THROW(x.getOp(), CVC5ApiException); |
156 |
|
|
157 |
4 |
Term ab = d_solver.mkTerm(SELECT, a, b); |
158 |
4 |
Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); |
159 |
4 |
Term extb = d_solver.mkTerm(ext, b); |
160 |
|
|
161 |
2 |
ASSERT_TRUE(ab.hasOp()); |
162 |
2 |
ASSERT_FALSE(ab.getOp().isIndexed()); |
163 |
|
// can compare directly to a Kind (will invoke Op constructor) |
164 |
2 |
ASSERT_TRUE(extb.hasOp()); |
165 |
2 |
ASSERT_TRUE(extb.getOp().isIndexed()); |
166 |
2 |
ASSERT_EQ(extb.getOp(), ext); |
167 |
|
|
168 |
4 |
Term f = d_solver.mkConst(funsort, "f"); |
169 |
4 |
Term fx = d_solver.mkTerm(APPLY_UF, f, x); |
170 |
|
|
171 |
2 |
ASSERT_FALSE(f.hasOp()); |
172 |
4 |
ASSERT_THROW(f.getOp(), CVC5ApiException); |
173 |
2 |
ASSERT_TRUE(fx.hasOp()); |
174 |
4 |
std::vector<Term> children(fx.begin(), fx.end()); |
175 |
|
// testing rebuild from op and children |
176 |
2 |
ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children)); |
177 |
|
|
178 |
|
// Test Datatypes Ops |
179 |
4 |
Sort sort = d_solver.mkParamSort("T"); |
180 |
4 |
DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); |
181 |
4 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
182 |
4 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
183 |
2 |
cons.addSelector("head", sort); |
184 |
2 |
cons.addSelectorSelf("tail"); |
185 |
2 |
listDecl.addConstructor(cons); |
186 |
2 |
listDecl.addConstructor(nil); |
187 |
4 |
Sort listSort = d_solver.mkDatatypeSort(listDecl); |
188 |
|
Sort intListSort = |
189 |
4 |
listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}); |
190 |
4 |
Term c = d_solver.mkConst(intListSort, "c"); |
191 |
4 |
Datatype list = listSort.getDatatype(); |
192 |
|
// list datatype constructor and selector operator terms |
193 |
4 |
Term consOpTerm = list.getConstructorTerm("cons"); |
194 |
4 |
Term nilOpTerm = list.getConstructorTerm("nil"); |
195 |
4 |
Term headOpTerm = list["cons"].getSelectorTerm("head"); |
196 |
4 |
Term tailOpTerm = list["cons"].getSelectorTerm("tail"); |
197 |
|
|
198 |
4 |
Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); |
199 |
|
Term consTerm = d_solver.mkTerm( |
200 |
4 |
APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); |
201 |
4 |
Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); |
202 |
4 |
Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); |
203 |
|
|
204 |
2 |
ASSERT_TRUE(nilTerm.hasOp()); |
205 |
2 |
ASSERT_TRUE(consTerm.hasOp()); |
206 |
2 |
ASSERT_TRUE(headTerm.hasOp()); |
207 |
2 |
ASSERT_TRUE(tailTerm.hasOp()); |
208 |
|
|
209 |
|
// Test rebuilding |
210 |
2 |
children.clear(); |
211 |
2 |
children.insert(children.begin(), headTerm.begin(), headTerm.end()); |
212 |
2 |
ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); |
213 |
|
} |
214 |
|
|
215 |
41 |
TEST_F(TestApiBlackTerm, isNull) |
216 |
|
{ |
217 |
4 |
Term x; |
218 |
2 |
ASSERT_TRUE(x.isNull()); |
219 |
2 |
x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x"); |
220 |
2 |
ASSERT_FALSE(x.isNull()); |
221 |
|
} |
222 |
|
|
223 |
41 |
TEST_F(TestApiBlackTerm, notTerm) |
224 |
|
{ |
225 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
226 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
227 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
228 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
229 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
230 |
|
|
231 |
4 |
ASSERT_THROW(Term().notTerm(), CVC5ApiException); |
232 |
4 |
Term b = d_solver.mkTrue(); |
233 |
2 |
ASSERT_NO_THROW(b.notTerm()); |
234 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
235 |
4 |
ASSERT_THROW(x.notTerm(), CVC5ApiException); |
236 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
237 |
4 |
ASSERT_THROW(f.notTerm(), CVC5ApiException); |
238 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
239 |
4 |
ASSERT_THROW(p.notTerm(), CVC5ApiException); |
240 |
4 |
Term zero = d_solver.mkInteger(0); |
241 |
4 |
ASSERT_THROW(zero.notTerm(), CVC5ApiException); |
242 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
243 |
4 |
ASSERT_THROW(f_x.notTerm(), CVC5ApiException); |
244 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
245 |
4 |
ASSERT_THROW(sum.notTerm(), CVC5ApiException); |
246 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
247 |
2 |
ASSERT_NO_THROW(p_0.notTerm()); |
248 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
249 |
2 |
ASSERT_NO_THROW(p_f_x.notTerm()); |
250 |
|
} |
251 |
|
|
252 |
41 |
TEST_F(TestApiBlackTerm, andTerm) |
253 |
|
{ |
254 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
255 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
256 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
257 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
258 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
259 |
|
|
260 |
4 |
Term b = d_solver.mkTrue(); |
261 |
4 |
ASSERT_THROW(Term().andTerm(b), CVC5ApiException); |
262 |
4 |
ASSERT_THROW(b.andTerm(Term()), CVC5ApiException); |
263 |
2 |
ASSERT_NO_THROW(b.andTerm(b)); |
264 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
265 |
4 |
ASSERT_THROW(x.andTerm(b), CVC5ApiException); |
266 |
4 |
ASSERT_THROW(x.andTerm(x), CVC5ApiException); |
267 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
268 |
4 |
ASSERT_THROW(f.andTerm(b), CVC5ApiException); |
269 |
4 |
ASSERT_THROW(f.andTerm(x), CVC5ApiException); |
270 |
4 |
ASSERT_THROW(f.andTerm(f), CVC5ApiException); |
271 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
272 |
4 |
ASSERT_THROW(p.andTerm(b), CVC5ApiException); |
273 |
4 |
ASSERT_THROW(p.andTerm(x), CVC5ApiException); |
274 |
4 |
ASSERT_THROW(p.andTerm(f), CVC5ApiException); |
275 |
4 |
ASSERT_THROW(p.andTerm(p), CVC5ApiException); |
276 |
4 |
Term zero = d_solver.mkInteger(0); |
277 |
4 |
ASSERT_THROW(zero.andTerm(b), CVC5ApiException); |
278 |
4 |
ASSERT_THROW(zero.andTerm(x), CVC5ApiException); |
279 |
4 |
ASSERT_THROW(zero.andTerm(f), CVC5ApiException); |
280 |
4 |
ASSERT_THROW(zero.andTerm(p), CVC5ApiException); |
281 |
4 |
ASSERT_THROW(zero.andTerm(zero), CVC5ApiException); |
282 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
283 |
4 |
ASSERT_THROW(f_x.andTerm(b), CVC5ApiException); |
284 |
4 |
ASSERT_THROW(f_x.andTerm(x), CVC5ApiException); |
285 |
4 |
ASSERT_THROW(f_x.andTerm(f), CVC5ApiException); |
286 |
4 |
ASSERT_THROW(f_x.andTerm(p), CVC5ApiException); |
287 |
4 |
ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException); |
288 |
4 |
ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException); |
289 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
290 |
4 |
ASSERT_THROW(sum.andTerm(b), CVC5ApiException); |
291 |
4 |
ASSERT_THROW(sum.andTerm(x), CVC5ApiException); |
292 |
4 |
ASSERT_THROW(sum.andTerm(f), CVC5ApiException); |
293 |
4 |
ASSERT_THROW(sum.andTerm(p), CVC5ApiException); |
294 |
4 |
ASSERT_THROW(sum.andTerm(zero), CVC5ApiException); |
295 |
4 |
ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException); |
296 |
4 |
ASSERT_THROW(sum.andTerm(sum), CVC5ApiException); |
297 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
298 |
2 |
ASSERT_NO_THROW(p_0.andTerm(b)); |
299 |
4 |
ASSERT_THROW(p_0.andTerm(x), CVC5ApiException); |
300 |
4 |
ASSERT_THROW(p_0.andTerm(f), CVC5ApiException); |
301 |
4 |
ASSERT_THROW(p_0.andTerm(p), CVC5ApiException); |
302 |
4 |
ASSERT_THROW(p_0.andTerm(zero), CVC5ApiException); |
303 |
4 |
ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException); |
304 |
4 |
ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException); |
305 |
2 |
ASSERT_NO_THROW(p_0.andTerm(p_0)); |
306 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
307 |
2 |
ASSERT_NO_THROW(p_f_x.andTerm(b)); |
308 |
4 |
ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException); |
309 |
4 |
ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException); |
310 |
4 |
ASSERT_THROW(p_f_x.andTerm(p), CVC5ApiException); |
311 |
4 |
ASSERT_THROW(p_f_x.andTerm(zero), CVC5ApiException); |
312 |
4 |
ASSERT_THROW(p_f_x.andTerm(f_x), CVC5ApiException); |
313 |
4 |
ASSERT_THROW(p_f_x.andTerm(sum), CVC5ApiException); |
314 |
2 |
ASSERT_NO_THROW(p_f_x.andTerm(p_0)); |
315 |
2 |
ASSERT_NO_THROW(p_f_x.andTerm(p_f_x)); |
316 |
|
} |
317 |
|
|
318 |
41 |
TEST_F(TestApiBlackTerm, orTerm) |
319 |
|
{ |
320 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
321 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
322 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
323 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
324 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
325 |
|
|
326 |
4 |
Term b = d_solver.mkTrue(); |
327 |
4 |
ASSERT_THROW(Term().orTerm(b), CVC5ApiException); |
328 |
4 |
ASSERT_THROW(b.orTerm(Term()), CVC5ApiException); |
329 |
2 |
ASSERT_NO_THROW(b.orTerm(b)); |
330 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
331 |
4 |
ASSERT_THROW(x.orTerm(b), CVC5ApiException); |
332 |
4 |
ASSERT_THROW(x.orTerm(x), CVC5ApiException); |
333 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
334 |
4 |
ASSERT_THROW(f.orTerm(b), CVC5ApiException); |
335 |
4 |
ASSERT_THROW(f.orTerm(x), CVC5ApiException); |
336 |
4 |
ASSERT_THROW(f.orTerm(f), CVC5ApiException); |
337 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
338 |
4 |
ASSERT_THROW(p.orTerm(b), CVC5ApiException); |
339 |
4 |
ASSERT_THROW(p.orTerm(x), CVC5ApiException); |
340 |
4 |
ASSERT_THROW(p.orTerm(f), CVC5ApiException); |
341 |
4 |
ASSERT_THROW(p.orTerm(p), CVC5ApiException); |
342 |
4 |
Term zero = d_solver.mkInteger(0); |
343 |
4 |
ASSERT_THROW(zero.orTerm(b), CVC5ApiException); |
344 |
4 |
ASSERT_THROW(zero.orTerm(x), CVC5ApiException); |
345 |
4 |
ASSERT_THROW(zero.orTerm(f), CVC5ApiException); |
346 |
4 |
ASSERT_THROW(zero.orTerm(p), CVC5ApiException); |
347 |
4 |
ASSERT_THROW(zero.orTerm(zero), CVC5ApiException); |
348 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
349 |
4 |
ASSERT_THROW(f_x.orTerm(b), CVC5ApiException); |
350 |
4 |
ASSERT_THROW(f_x.orTerm(x), CVC5ApiException); |
351 |
4 |
ASSERT_THROW(f_x.orTerm(f), CVC5ApiException); |
352 |
4 |
ASSERT_THROW(f_x.orTerm(p), CVC5ApiException); |
353 |
4 |
ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException); |
354 |
4 |
ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException); |
355 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
356 |
4 |
ASSERT_THROW(sum.orTerm(b), CVC5ApiException); |
357 |
4 |
ASSERT_THROW(sum.orTerm(x), CVC5ApiException); |
358 |
4 |
ASSERT_THROW(sum.orTerm(f), CVC5ApiException); |
359 |
4 |
ASSERT_THROW(sum.orTerm(p), CVC5ApiException); |
360 |
4 |
ASSERT_THROW(sum.orTerm(zero), CVC5ApiException); |
361 |
4 |
ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException); |
362 |
4 |
ASSERT_THROW(sum.orTerm(sum), CVC5ApiException); |
363 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
364 |
2 |
ASSERT_NO_THROW(p_0.orTerm(b)); |
365 |
4 |
ASSERT_THROW(p_0.orTerm(x), CVC5ApiException); |
366 |
4 |
ASSERT_THROW(p_0.orTerm(f), CVC5ApiException); |
367 |
4 |
ASSERT_THROW(p_0.orTerm(p), CVC5ApiException); |
368 |
4 |
ASSERT_THROW(p_0.orTerm(zero), CVC5ApiException); |
369 |
4 |
ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException); |
370 |
4 |
ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException); |
371 |
2 |
ASSERT_NO_THROW(p_0.orTerm(p_0)); |
372 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
373 |
2 |
ASSERT_NO_THROW(p_f_x.orTerm(b)); |
374 |
4 |
ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException); |
375 |
4 |
ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException); |
376 |
4 |
ASSERT_THROW(p_f_x.orTerm(p), CVC5ApiException); |
377 |
4 |
ASSERT_THROW(p_f_x.orTerm(zero), CVC5ApiException); |
378 |
4 |
ASSERT_THROW(p_f_x.orTerm(f_x), CVC5ApiException); |
379 |
4 |
ASSERT_THROW(p_f_x.orTerm(sum), CVC5ApiException); |
380 |
2 |
ASSERT_NO_THROW(p_f_x.orTerm(p_0)); |
381 |
2 |
ASSERT_NO_THROW(p_f_x.orTerm(p_f_x)); |
382 |
|
} |
383 |
|
|
384 |
41 |
TEST_F(TestApiBlackTerm, xorTerm) |
385 |
|
{ |
386 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
387 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
388 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
389 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
390 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
391 |
|
|
392 |
4 |
Term b = d_solver.mkTrue(); |
393 |
4 |
ASSERT_THROW(Term().xorTerm(b), CVC5ApiException); |
394 |
4 |
ASSERT_THROW(b.xorTerm(Term()), CVC5ApiException); |
395 |
2 |
ASSERT_NO_THROW(b.xorTerm(b)); |
396 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
397 |
4 |
ASSERT_THROW(x.xorTerm(b), CVC5ApiException); |
398 |
4 |
ASSERT_THROW(x.xorTerm(x), CVC5ApiException); |
399 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
400 |
4 |
ASSERT_THROW(f.xorTerm(b), CVC5ApiException); |
401 |
4 |
ASSERT_THROW(f.xorTerm(x), CVC5ApiException); |
402 |
4 |
ASSERT_THROW(f.xorTerm(f), CVC5ApiException); |
403 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
404 |
4 |
ASSERT_THROW(p.xorTerm(b), CVC5ApiException); |
405 |
4 |
ASSERT_THROW(p.xorTerm(x), CVC5ApiException); |
406 |
4 |
ASSERT_THROW(p.xorTerm(f), CVC5ApiException); |
407 |
4 |
ASSERT_THROW(p.xorTerm(p), CVC5ApiException); |
408 |
4 |
Term zero = d_solver.mkInteger(0); |
409 |
4 |
ASSERT_THROW(zero.xorTerm(b), CVC5ApiException); |
410 |
4 |
ASSERT_THROW(zero.xorTerm(x), CVC5ApiException); |
411 |
4 |
ASSERT_THROW(zero.xorTerm(f), CVC5ApiException); |
412 |
4 |
ASSERT_THROW(zero.xorTerm(p), CVC5ApiException); |
413 |
4 |
ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException); |
414 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
415 |
4 |
ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException); |
416 |
4 |
ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException); |
417 |
4 |
ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException); |
418 |
4 |
ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException); |
419 |
4 |
ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException); |
420 |
4 |
ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException); |
421 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
422 |
4 |
ASSERT_THROW(sum.xorTerm(b), CVC5ApiException); |
423 |
4 |
ASSERT_THROW(sum.xorTerm(x), CVC5ApiException); |
424 |
4 |
ASSERT_THROW(sum.xorTerm(f), CVC5ApiException); |
425 |
4 |
ASSERT_THROW(sum.xorTerm(p), CVC5ApiException); |
426 |
4 |
ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException); |
427 |
4 |
ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException); |
428 |
4 |
ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException); |
429 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
430 |
2 |
ASSERT_NO_THROW(p_0.xorTerm(b)); |
431 |
4 |
ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException); |
432 |
4 |
ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException); |
433 |
4 |
ASSERT_THROW(p_0.xorTerm(p), CVC5ApiException); |
434 |
4 |
ASSERT_THROW(p_0.xorTerm(zero), CVC5ApiException); |
435 |
4 |
ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException); |
436 |
4 |
ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException); |
437 |
2 |
ASSERT_NO_THROW(p_0.xorTerm(p_0)); |
438 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
439 |
2 |
ASSERT_NO_THROW(p_f_x.xorTerm(b)); |
440 |
4 |
ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException); |
441 |
4 |
ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException); |
442 |
4 |
ASSERT_THROW(p_f_x.xorTerm(p), CVC5ApiException); |
443 |
4 |
ASSERT_THROW(p_f_x.xorTerm(zero), CVC5ApiException); |
444 |
4 |
ASSERT_THROW(p_f_x.xorTerm(f_x), CVC5ApiException); |
445 |
4 |
ASSERT_THROW(p_f_x.xorTerm(sum), CVC5ApiException); |
446 |
2 |
ASSERT_NO_THROW(p_f_x.xorTerm(p_0)); |
447 |
2 |
ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x)); |
448 |
|
} |
449 |
|
|
450 |
41 |
TEST_F(TestApiBlackTerm, eqTerm) |
451 |
|
{ |
452 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
453 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
454 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
455 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
456 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
457 |
|
|
458 |
4 |
Term b = d_solver.mkTrue(); |
459 |
4 |
ASSERT_THROW(Term().eqTerm(b), CVC5ApiException); |
460 |
4 |
ASSERT_THROW(b.eqTerm(Term()), CVC5ApiException); |
461 |
2 |
ASSERT_NO_THROW(b.eqTerm(b)); |
462 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
463 |
4 |
ASSERT_THROW(x.eqTerm(b), CVC5ApiException); |
464 |
2 |
ASSERT_NO_THROW(x.eqTerm(x)); |
465 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
466 |
4 |
ASSERT_THROW(f.eqTerm(b), CVC5ApiException); |
467 |
4 |
ASSERT_THROW(f.eqTerm(x), CVC5ApiException); |
468 |
2 |
ASSERT_NO_THROW(f.eqTerm(f)); |
469 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
470 |
4 |
ASSERT_THROW(p.eqTerm(b), CVC5ApiException); |
471 |
4 |
ASSERT_THROW(p.eqTerm(x), CVC5ApiException); |
472 |
4 |
ASSERT_THROW(p.eqTerm(f), CVC5ApiException); |
473 |
2 |
ASSERT_NO_THROW(p.eqTerm(p)); |
474 |
4 |
Term zero = d_solver.mkInteger(0); |
475 |
4 |
ASSERT_THROW(zero.eqTerm(b), CVC5ApiException); |
476 |
4 |
ASSERT_THROW(zero.eqTerm(x), CVC5ApiException); |
477 |
4 |
ASSERT_THROW(zero.eqTerm(f), CVC5ApiException); |
478 |
4 |
ASSERT_THROW(zero.eqTerm(p), CVC5ApiException); |
479 |
2 |
ASSERT_NO_THROW(zero.eqTerm(zero)); |
480 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
481 |
4 |
ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException); |
482 |
4 |
ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException); |
483 |
4 |
ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException); |
484 |
4 |
ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException); |
485 |
2 |
ASSERT_NO_THROW(f_x.eqTerm(zero)); |
486 |
2 |
ASSERT_NO_THROW(f_x.eqTerm(f_x)); |
487 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
488 |
4 |
ASSERT_THROW(sum.eqTerm(b), CVC5ApiException); |
489 |
4 |
ASSERT_THROW(sum.eqTerm(x), CVC5ApiException); |
490 |
4 |
ASSERT_THROW(sum.eqTerm(f), CVC5ApiException); |
491 |
4 |
ASSERT_THROW(sum.eqTerm(p), CVC5ApiException); |
492 |
2 |
ASSERT_NO_THROW(sum.eqTerm(zero)); |
493 |
2 |
ASSERT_NO_THROW(sum.eqTerm(f_x)); |
494 |
2 |
ASSERT_NO_THROW(sum.eqTerm(sum)); |
495 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
496 |
2 |
ASSERT_NO_THROW(p_0.eqTerm(b)); |
497 |
4 |
ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException); |
498 |
4 |
ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException); |
499 |
4 |
ASSERT_THROW(p_0.eqTerm(p), CVC5ApiException); |
500 |
4 |
ASSERT_THROW(p_0.eqTerm(zero), CVC5ApiException); |
501 |
4 |
ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException); |
502 |
4 |
ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException); |
503 |
2 |
ASSERT_NO_THROW(p_0.eqTerm(p_0)); |
504 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
505 |
2 |
ASSERT_NO_THROW(p_f_x.eqTerm(b)); |
506 |
4 |
ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException); |
507 |
4 |
ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException); |
508 |
4 |
ASSERT_THROW(p_f_x.eqTerm(p), CVC5ApiException); |
509 |
4 |
ASSERT_THROW(p_f_x.eqTerm(zero), CVC5ApiException); |
510 |
4 |
ASSERT_THROW(p_f_x.eqTerm(f_x), CVC5ApiException); |
511 |
4 |
ASSERT_THROW(p_f_x.eqTerm(sum), CVC5ApiException); |
512 |
2 |
ASSERT_NO_THROW(p_f_x.eqTerm(p_0)); |
513 |
2 |
ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x)); |
514 |
|
} |
515 |
|
|
516 |
41 |
TEST_F(TestApiBlackTerm, impTerm) |
517 |
|
{ |
518 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
519 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
520 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
521 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
522 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
523 |
|
|
524 |
4 |
Term b = d_solver.mkTrue(); |
525 |
4 |
ASSERT_THROW(Term().impTerm(b), CVC5ApiException); |
526 |
4 |
ASSERT_THROW(b.impTerm(Term()), CVC5ApiException); |
527 |
2 |
ASSERT_NO_THROW(b.impTerm(b)); |
528 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
529 |
4 |
ASSERT_THROW(x.impTerm(b), CVC5ApiException); |
530 |
4 |
ASSERT_THROW(x.impTerm(x), CVC5ApiException); |
531 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
532 |
4 |
ASSERT_THROW(f.impTerm(b), CVC5ApiException); |
533 |
4 |
ASSERT_THROW(f.impTerm(x), CVC5ApiException); |
534 |
4 |
ASSERT_THROW(f.impTerm(f), CVC5ApiException); |
535 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
536 |
4 |
ASSERT_THROW(p.impTerm(b), CVC5ApiException); |
537 |
4 |
ASSERT_THROW(p.impTerm(x), CVC5ApiException); |
538 |
4 |
ASSERT_THROW(p.impTerm(f), CVC5ApiException); |
539 |
4 |
ASSERT_THROW(p.impTerm(p), CVC5ApiException); |
540 |
4 |
Term zero = d_solver.mkInteger(0); |
541 |
4 |
ASSERT_THROW(zero.impTerm(b), CVC5ApiException); |
542 |
4 |
ASSERT_THROW(zero.impTerm(x), CVC5ApiException); |
543 |
4 |
ASSERT_THROW(zero.impTerm(f), CVC5ApiException); |
544 |
4 |
ASSERT_THROW(zero.impTerm(p), CVC5ApiException); |
545 |
4 |
ASSERT_THROW(zero.impTerm(zero), CVC5ApiException); |
546 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
547 |
4 |
ASSERT_THROW(f_x.impTerm(b), CVC5ApiException); |
548 |
4 |
ASSERT_THROW(f_x.impTerm(x), CVC5ApiException); |
549 |
4 |
ASSERT_THROW(f_x.impTerm(f), CVC5ApiException); |
550 |
4 |
ASSERT_THROW(f_x.impTerm(p), CVC5ApiException); |
551 |
4 |
ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException); |
552 |
4 |
ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException); |
553 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
554 |
4 |
ASSERT_THROW(sum.impTerm(b), CVC5ApiException); |
555 |
4 |
ASSERT_THROW(sum.impTerm(x), CVC5ApiException); |
556 |
4 |
ASSERT_THROW(sum.impTerm(f), CVC5ApiException); |
557 |
4 |
ASSERT_THROW(sum.impTerm(p), CVC5ApiException); |
558 |
4 |
ASSERT_THROW(sum.impTerm(zero), CVC5ApiException); |
559 |
4 |
ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException); |
560 |
4 |
ASSERT_THROW(sum.impTerm(sum), CVC5ApiException); |
561 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
562 |
2 |
ASSERT_NO_THROW(p_0.impTerm(b)); |
563 |
4 |
ASSERT_THROW(p_0.impTerm(x), CVC5ApiException); |
564 |
4 |
ASSERT_THROW(p_0.impTerm(f), CVC5ApiException); |
565 |
4 |
ASSERT_THROW(p_0.impTerm(p), CVC5ApiException); |
566 |
4 |
ASSERT_THROW(p_0.impTerm(zero), CVC5ApiException); |
567 |
4 |
ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException); |
568 |
4 |
ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException); |
569 |
2 |
ASSERT_NO_THROW(p_0.impTerm(p_0)); |
570 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
571 |
2 |
ASSERT_NO_THROW(p_f_x.impTerm(b)); |
572 |
4 |
ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException); |
573 |
4 |
ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException); |
574 |
4 |
ASSERT_THROW(p_f_x.impTerm(p), CVC5ApiException); |
575 |
4 |
ASSERT_THROW(p_f_x.impTerm(zero), CVC5ApiException); |
576 |
4 |
ASSERT_THROW(p_f_x.impTerm(f_x), CVC5ApiException); |
577 |
4 |
ASSERT_THROW(p_f_x.impTerm(sum), CVC5ApiException); |
578 |
2 |
ASSERT_NO_THROW(p_f_x.impTerm(p_0)); |
579 |
2 |
ASSERT_NO_THROW(p_f_x.impTerm(p_f_x)); |
580 |
|
} |
581 |
|
|
582 |
41 |
TEST_F(TestApiBlackTerm, iteTerm) |
583 |
|
{ |
584 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(8); |
585 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
586 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
587 |
4 |
Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); |
588 |
4 |
Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); |
589 |
|
|
590 |
4 |
Term b = d_solver.mkTrue(); |
591 |
4 |
ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException); |
592 |
4 |
ASSERT_THROW(b.iteTerm(Term(), b), CVC5ApiException); |
593 |
4 |
ASSERT_THROW(b.iteTerm(b, Term()), CVC5ApiException); |
594 |
2 |
ASSERT_NO_THROW(b.iteTerm(b, b)); |
595 |
4 |
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); |
596 |
2 |
ASSERT_NO_THROW(b.iteTerm(x, x)); |
597 |
2 |
ASSERT_NO_THROW(b.iteTerm(b, b)); |
598 |
4 |
ASSERT_THROW(b.iteTerm(x, b), CVC5ApiException); |
599 |
4 |
ASSERT_THROW(x.iteTerm(x, x), CVC5ApiException); |
600 |
4 |
ASSERT_THROW(x.iteTerm(x, b), CVC5ApiException); |
601 |
4 |
Term f = d_solver.mkVar(funSort1, "f"); |
602 |
4 |
ASSERT_THROW(f.iteTerm(b, b), CVC5ApiException); |
603 |
4 |
ASSERT_THROW(x.iteTerm(b, x), CVC5ApiException); |
604 |
4 |
Term p = d_solver.mkVar(funSort2, "p"); |
605 |
4 |
ASSERT_THROW(p.iteTerm(b, b), CVC5ApiException); |
606 |
4 |
ASSERT_THROW(p.iteTerm(x, b), CVC5ApiException); |
607 |
4 |
Term zero = d_solver.mkInteger(0); |
608 |
4 |
ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException); |
609 |
4 |
ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException); |
610 |
4 |
Term f_x = d_solver.mkTerm(APPLY_UF, f, x); |
611 |
4 |
ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException); |
612 |
4 |
ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException); |
613 |
4 |
Term sum = d_solver.mkTerm(PLUS, f_x, f_x); |
614 |
4 |
ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException); |
615 |
4 |
ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException); |
616 |
4 |
Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); |
617 |
2 |
ASSERT_NO_THROW(p_0.iteTerm(b, b)); |
618 |
2 |
ASSERT_NO_THROW(p_0.iteTerm(x, x)); |
619 |
4 |
ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException); |
620 |
4 |
Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); |
621 |
2 |
ASSERT_NO_THROW(p_f_x.iteTerm(b, b)); |
622 |
2 |
ASSERT_NO_THROW(p_f_x.iteTerm(x, x)); |
623 |
4 |
ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException); |
624 |
|
} |
625 |
|
|
626 |
41 |
TEST_F(TestApiBlackTerm, termAssignment) |
627 |
|
{ |
628 |
4 |
Term t1 = d_solver.mkInteger(1); |
629 |
4 |
Term t2 = t1; |
630 |
2 |
t2 = d_solver.mkInteger(2); |
631 |
2 |
ASSERT_EQ(t1, d_solver.mkInteger(1)); |
632 |
|
} |
633 |
|
|
634 |
41 |
TEST_F(TestApiBlackTerm, termCompare) |
635 |
|
{ |
636 |
4 |
Term t1 = d_solver.mkInteger(1); |
637 |
4 |
Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); |
638 |
4 |
Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); |
639 |
2 |
ASSERT_TRUE(t2 >= t3); |
640 |
2 |
ASSERT_TRUE(t2 <= t3); |
641 |
2 |
ASSERT_TRUE((t1 > t2) != (t1 < t2)); |
642 |
2 |
ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2)); |
643 |
|
} |
644 |
|
|
645 |
41 |
TEST_F(TestApiBlackTerm, termChildren) |
646 |
|
{ |
647 |
|
// simple term 2+3 |
648 |
4 |
Term two = d_solver.mkInteger(2); |
649 |
4 |
Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); |
650 |
2 |
ASSERT_EQ(t1[0], two); |
651 |
2 |
ASSERT_EQ(t1.getNumChildren(), 2); |
652 |
4 |
Term tnull; |
653 |
4 |
ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException); |
654 |
|
|
655 |
|
// apply term f(2) |
656 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
657 |
4 |
Sort fsort = d_solver.mkFunctionSort(intSort, intSort); |
658 |
4 |
Term f = d_solver.mkConst(fsort, "f"); |
659 |
4 |
Term t2 = d_solver.mkTerm(APPLY_UF, f, two); |
660 |
|
// due to our higher-order view of terms, we treat f as a child of APPLY_UF |
661 |
2 |
ASSERT_EQ(t2.getNumChildren(), 2); |
662 |
2 |
ASSERT_EQ(t2[0], f); |
663 |
2 |
ASSERT_EQ(t2[1], two); |
664 |
4 |
ASSERT_THROW(tnull[0], CVC5ApiException); |
665 |
|
} |
666 |
|
|
667 |
41 |
TEST_F(TestApiBlackTerm, getInteger) |
668 |
|
{ |
669 |
4 |
Term int1 = d_solver.mkInteger("-18446744073709551616"); |
670 |
4 |
Term int2 = d_solver.mkInteger("-18446744073709551615"); |
671 |
4 |
Term int3 = d_solver.mkInteger("-4294967296"); |
672 |
4 |
Term int4 = d_solver.mkInteger("-4294967295"); |
673 |
4 |
Term int5 = d_solver.mkInteger("-10"); |
674 |
4 |
Term int6 = d_solver.mkInteger("0"); |
675 |
4 |
Term int7 = d_solver.mkInteger("10"); |
676 |
4 |
Term int8 = d_solver.mkInteger("4294967295"); |
677 |
4 |
Term int9 = d_solver.mkInteger("4294967296"); |
678 |
4 |
Term int10 = d_solver.mkInteger("18446744073709551615"); |
679 |
4 |
Term int11 = d_solver.mkInteger("18446744073709551616"); |
680 |
4 |
Term int12 = d_solver.mkInteger("-0"); |
681 |
|
|
682 |
4 |
ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException); |
683 |
4 |
ASSERT_THROW(d_solver.mkInteger("-"), CVC5ApiException); |
684 |
4 |
ASSERT_THROW(d_solver.mkInteger("-1-"), CVC5ApiException); |
685 |
4 |
ASSERT_THROW(d_solver.mkInteger("0.0"), CVC5ApiException); |
686 |
4 |
ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC5ApiException); |
687 |
4 |
ASSERT_THROW(d_solver.mkInteger("012"), CVC5ApiException); |
688 |
4 |
ASSERT_THROW(d_solver.mkInteger("0000"), CVC5ApiException); |
689 |
4 |
ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException); |
690 |
4 |
ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException); |
691 |
|
|
692 |
2 |
ASSERT_TRUE(!int1.isInt32Value() && !int1.isUInt32Value() |
693 |
|
&& !int1.isInt64Value() && !int1.isUInt64Value() |
694 |
2 |
&& int1.isIntegerValue()); |
695 |
2 |
ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616"); |
696 |
2 |
ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value() |
697 |
|
&& !int2.isInt64Value() && !int2.isUInt64Value() |
698 |
2 |
&& int2.isIntegerValue()); |
699 |
2 |
ASSERT_EQ(int2.getIntegerValue(), "-18446744073709551615"); |
700 |
2 |
ASSERT_TRUE(!int3.isInt32Value() && !int3.isUInt32Value() |
701 |
|
&& int3.isInt64Value() && !int3.isUInt64Value() |
702 |
2 |
&& int3.isIntegerValue()); |
703 |
2 |
ASSERT_EQ(int3.getInt64Value(), -4294967296); |
704 |
2 |
ASSERT_EQ(int3.getIntegerValue(), "-4294967296"); |
705 |
2 |
ASSERT_TRUE(!int4.isInt32Value() && !int4.isUInt32Value() |
706 |
|
&& int4.isInt64Value() && !int4.isUInt64Value() |
707 |
2 |
&& int4.isIntegerValue()); |
708 |
2 |
ASSERT_EQ(int4.getInt64Value(), -4294967295); |
709 |
2 |
ASSERT_EQ(int4.getIntegerValue(), "-4294967295"); |
710 |
2 |
ASSERT_TRUE(int5.isInt32Value() && !int5.isUInt32Value() |
711 |
|
&& int5.isInt64Value() && !int5.isUInt64Value() |
712 |
2 |
&& int5.isIntegerValue()); |
713 |
2 |
ASSERT_EQ(int5.getInt32Value(), -10); |
714 |
2 |
ASSERT_EQ(int5.getInt64Value(), -10); |
715 |
2 |
ASSERT_EQ(int5.getIntegerValue(), "-10"); |
716 |
2 |
ASSERT_TRUE(int6.isInt32Value() && int6.isUInt32Value() && int6.isInt64Value() |
717 |
2 |
&& int6.isUInt64Value() && int6.isIntegerValue()); |
718 |
2 |
ASSERT_EQ(int6.getInt32Value(), 0); |
719 |
2 |
ASSERT_EQ(int6.getUInt32Value(), 0); |
720 |
2 |
ASSERT_EQ(int6.getInt64Value(), 0); |
721 |
2 |
ASSERT_EQ(int6.getUInt64Value(), 0); |
722 |
2 |
ASSERT_EQ(int6.getIntegerValue(), "0"); |
723 |
2 |
ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value() |
724 |
2 |
&& int7.isUInt64Value() && int7.isIntegerValue()); |
725 |
2 |
ASSERT_EQ(int7.getInt32Value(), 10); |
726 |
2 |
ASSERT_EQ(int7.getUInt32Value(), 10); |
727 |
2 |
ASSERT_EQ(int7.getInt64Value(), 10); |
728 |
2 |
ASSERT_EQ(int7.getUInt64Value(), 10); |
729 |
2 |
ASSERT_EQ(int7.getIntegerValue(), "10"); |
730 |
2 |
ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value() |
731 |
|
&& int8.isInt64Value() && int8.isUInt64Value() |
732 |
2 |
&& int8.isIntegerValue()); |
733 |
2 |
ASSERT_EQ(int8.getUInt32Value(), 4294967295); |
734 |
2 |
ASSERT_EQ(int8.getInt64Value(), 4294967295); |
735 |
2 |
ASSERT_EQ(int8.getUInt64Value(), 4294967295); |
736 |
2 |
ASSERT_EQ(int8.getIntegerValue(), "4294967295"); |
737 |
2 |
ASSERT_TRUE(!int9.isInt32Value() && !int9.isUInt32Value() |
738 |
|
&& int9.isInt64Value() && int9.isUInt64Value() |
739 |
2 |
&& int9.isIntegerValue()); |
740 |
2 |
ASSERT_EQ(int9.getInt64Value(), 4294967296); |
741 |
2 |
ASSERT_EQ(int9.getUInt64Value(), 4294967296); |
742 |
2 |
ASSERT_EQ(int9.getIntegerValue(), "4294967296"); |
743 |
2 |
ASSERT_TRUE(!int10.isInt32Value() && !int10.isUInt32Value() |
744 |
|
&& !int10.isInt64Value() && int10.isUInt64Value() |
745 |
2 |
&& int10.isIntegerValue()); |
746 |
2 |
ASSERT_EQ(int10.getUInt64Value(), 18446744073709551615ull); |
747 |
2 |
ASSERT_EQ(int10.getIntegerValue(), "18446744073709551615"); |
748 |
2 |
ASSERT_TRUE(!int11.isInt32Value() && !int11.isUInt32Value() |
749 |
|
&& !int11.isInt64Value() && !int11.isUInt64Value() |
750 |
2 |
&& int11.isIntegerValue()); |
751 |
2 |
ASSERT_EQ(int11.getIntegerValue(), "18446744073709551616"); |
752 |
|
} |
753 |
|
|
754 |
41 |
TEST_F(TestApiBlackTerm, getString) |
755 |
|
{ |
756 |
4 |
Term s1 = d_solver.mkString("abcde"); |
757 |
2 |
ASSERT_TRUE(s1.isStringValue()); |
758 |
2 |
ASSERT_EQ(s1.getStringValue(), L"abcde"); |
759 |
|
} |
760 |
|
|
761 |
41 |
TEST_F(TestApiBlackTerm, getReal) |
762 |
|
{ |
763 |
4 |
Term real1 = d_solver.mkReal("0"); |
764 |
4 |
Term real2 = d_solver.mkReal(".0"); |
765 |
4 |
Term real3 = d_solver.mkReal("-17"); |
766 |
4 |
Term real4 = d_solver.mkReal("-3/5"); |
767 |
4 |
Term real5 = d_solver.mkReal("12.7"); |
768 |
4 |
Term real6 = d_solver.mkReal("1/4294967297"); |
769 |
4 |
Term real7 = d_solver.mkReal("4294967297"); |
770 |
4 |
Term real8 = d_solver.mkReal("1/18446744073709551617"); |
771 |
4 |
Term real9 = d_solver.mkReal("18446744073709551617"); |
772 |
4 |
Term real10 = d_solver.mkReal("2343.2343"); |
773 |
|
|
774 |
2 |
ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value() |
775 |
2 |
&& real1.isReal32Value()); |
776 |
2 |
ASSERT_TRUE(real2.isRealValue() && real2.isReal64Value() |
777 |
2 |
&& real2.isReal32Value()); |
778 |
2 |
ASSERT_TRUE(real3.isRealValue() && real3.isReal64Value() |
779 |
2 |
&& real3.isReal32Value()); |
780 |
2 |
ASSERT_TRUE(real4.isRealValue() && real4.isReal64Value() |
781 |
2 |
&& real4.isReal32Value()); |
782 |
2 |
ASSERT_TRUE(real5.isRealValue() && real5.isReal64Value() |
783 |
2 |
&& real5.isReal32Value()); |
784 |
2 |
ASSERT_TRUE(real6.isRealValue() && real6.isReal64Value()); |
785 |
2 |
ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value()); |
786 |
2 |
ASSERT_TRUE(real8.isRealValue()); |
787 |
2 |
ASSERT_TRUE(real9.isRealValue()); |
788 |
2 |
ASSERT_TRUE(real10.isRealValue()); |
789 |
|
|
790 |
2 |
ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real1.getReal32Value()); |
791 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real1.getReal64Value()); |
792 |
2 |
ASSERT_EQ("0.0", real1.getRealValue()); |
793 |
|
|
794 |
2 |
ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real2.getReal32Value()); |
795 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real2.getReal64Value()); |
796 |
2 |
ASSERT_EQ("0.0", real2.getRealValue()); |
797 |
|
|
798 |
2 |
ASSERT_EQ((std::pair<int32_t, uint32_t>(-17, 1)), real3.getReal32Value()); |
799 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(-17, 1)), real3.getReal64Value()); |
800 |
2 |
ASSERT_EQ("-17.0", real3.getRealValue()); |
801 |
|
|
802 |
2 |
ASSERT_EQ((std::pair<int32_t, uint32_t>(-3, 5)), real4.getReal32Value()); |
803 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(-3, 5)), real4.getReal64Value()); |
804 |
2 |
ASSERT_EQ("-3/5", real4.getRealValue()); |
805 |
|
|
806 |
2 |
ASSERT_EQ((std::pair<int32_t, uint32_t>(127, 10)), real5.getReal32Value()); |
807 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value()); |
808 |
2 |
ASSERT_EQ("127/10", real5.getRealValue()); |
809 |
|
|
810 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value()); |
811 |
2 |
ASSERT_EQ("1/4294967297", real6.getRealValue()); |
812 |
|
|
813 |
2 |
ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value()); |
814 |
2 |
ASSERT_EQ("4294967297.0", real7.getRealValue()); |
815 |
|
|
816 |
2 |
ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); |
817 |
|
|
818 |
2 |
ASSERT_EQ("18446744073709551617.0", real9.getRealValue()); |
819 |
|
|
820 |
2 |
ASSERT_EQ("23432343/10000", real10.getRealValue()); |
821 |
|
} |
822 |
|
|
823 |
41 |
TEST_F(TestApiBlackTerm, getConstArrayBase) |
824 |
|
{ |
825 |
4 |
Sort intsort = d_solver.getIntegerSort(); |
826 |
4 |
Sort arrsort = d_solver.mkArraySort(intsort, intsort); |
827 |
4 |
Term one = d_solver.mkInteger(1); |
828 |
4 |
Term constarr = d_solver.mkConstArray(arrsort, one); |
829 |
|
|
830 |
2 |
ASSERT_TRUE(constarr.isConstArray()); |
831 |
2 |
ASSERT_EQ(one, constarr.getConstArrayBase()); |
832 |
|
} |
833 |
|
|
834 |
41 |
TEST_F(TestApiBlackTerm, getBoolean) |
835 |
|
{ |
836 |
4 |
Term b1 = d_solver.mkBoolean(true); |
837 |
4 |
Term b2 = d_solver.mkBoolean(false); |
838 |
|
|
839 |
2 |
ASSERT_TRUE(b1.isBooleanValue()); |
840 |
2 |
ASSERT_TRUE(b2.isBooleanValue()); |
841 |
2 |
ASSERT_TRUE(b1.getBooleanValue()); |
842 |
2 |
ASSERT_FALSE(b2.getBooleanValue()); |
843 |
|
} |
844 |
|
|
845 |
41 |
TEST_F(TestApiBlackTerm, getBitVector) |
846 |
|
{ |
847 |
4 |
Term b1 = d_solver.mkBitVector(8, 15); |
848 |
4 |
Term b2 = d_solver.mkBitVector("00001111", 2); |
849 |
4 |
Term b3 = d_solver.mkBitVector("15", 10); |
850 |
4 |
Term b4 = d_solver.mkBitVector("0f", 16); |
851 |
4 |
Term b5 = d_solver.mkBitVector(8, "00001111", 2); |
852 |
4 |
Term b6 = d_solver.mkBitVector(8, "15", 10); |
853 |
4 |
Term b7 = d_solver.mkBitVector(8, "0f", 16); |
854 |
|
|
855 |
2 |
ASSERT_TRUE(b1.isBitVectorValue()); |
856 |
2 |
ASSERT_TRUE(b2.isBitVectorValue()); |
857 |
2 |
ASSERT_TRUE(b3.isBitVectorValue()); |
858 |
2 |
ASSERT_TRUE(b4.isBitVectorValue()); |
859 |
2 |
ASSERT_TRUE(b5.isBitVectorValue()); |
860 |
2 |
ASSERT_TRUE(b6.isBitVectorValue()); |
861 |
2 |
ASSERT_TRUE(b7.isBitVectorValue()); |
862 |
|
|
863 |
2 |
ASSERT_EQ("00001111", b1.getBitVectorValue(2)); |
864 |
2 |
ASSERT_EQ("15", b1.getBitVectorValue(10)); |
865 |
2 |
ASSERT_EQ("f", b1.getBitVectorValue(16)); |
866 |
2 |
ASSERT_EQ("00001111", b2.getBitVectorValue(2)); |
867 |
2 |
ASSERT_EQ("15", b2.getBitVectorValue(10)); |
868 |
2 |
ASSERT_EQ("f", b2.getBitVectorValue(16)); |
869 |
2 |
ASSERT_EQ("1111", b3.getBitVectorValue(2)); |
870 |
2 |
ASSERT_EQ("15", b3.getBitVectorValue(10)); |
871 |
2 |
ASSERT_EQ("f", b3.getBitVectorValue(16)); |
872 |
2 |
ASSERT_EQ("00001111", b4.getBitVectorValue(2)); |
873 |
2 |
ASSERT_EQ("15", b4.getBitVectorValue(10)); |
874 |
2 |
ASSERT_EQ("f", b4.getBitVectorValue(16)); |
875 |
2 |
ASSERT_EQ("00001111", b5.getBitVectorValue(2)); |
876 |
2 |
ASSERT_EQ("15", b5.getBitVectorValue(10)); |
877 |
2 |
ASSERT_EQ("f", b5.getBitVectorValue(16)); |
878 |
2 |
ASSERT_EQ("00001111", b6.getBitVectorValue(2)); |
879 |
2 |
ASSERT_EQ("15", b6.getBitVectorValue(10)); |
880 |
2 |
ASSERT_EQ("f", b6.getBitVectorValue(16)); |
881 |
2 |
ASSERT_EQ("00001111", b7.getBitVectorValue(2)); |
882 |
2 |
ASSERT_EQ("15", b7.getBitVectorValue(10)); |
883 |
2 |
ASSERT_EQ("f", b7.getBitVectorValue(16)); |
884 |
|
} |
885 |
|
|
886 |
41 |
TEST_F(TestApiBlackTerm, getAbstractValue) |
887 |
|
{ |
888 |
4 |
Term v1 = d_solver.mkAbstractValue(1); |
889 |
4 |
Term v2 = d_solver.mkAbstractValue("15"); |
890 |
4 |
Term v3 = d_solver.mkAbstractValue("18446744073709551617"); |
891 |
|
|
892 |
2 |
ASSERT_TRUE(v1.isAbstractValue()); |
893 |
2 |
ASSERT_TRUE(v2.isAbstractValue()); |
894 |
2 |
ASSERT_TRUE(v3.isAbstractValue()); |
895 |
2 |
ASSERT_EQ("1", v1.getAbstractValue()); |
896 |
2 |
ASSERT_EQ("15", v2.getAbstractValue()); |
897 |
2 |
ASSERT_EQ("18446744073709551617", v3.getAbstractValue()); |
898 |
|
} |
899 |
|
|
900 |
41 |
TEST_F(TestApiBlackTerm, getTuple) |
901 |
|
{ |
902 |
4 |
Sort s1 = d_solver.getIntegerSort(); |
903 |
4 |
Sort s2 = d_solver.getRealSort(); |
904 |
4 |
Sort s3 = d_solver.getStringSort(); |
905 |
|
|
906 |
4 |
Term t1 = d_solver.mkInteger(15); |
907 |
4 |
Term t2 = d_solver.mkReal(17, 25); |
908 |
4 |
Term t3 = d_solver.mkString("abc"); |
909 |
|
|
910 |
4 |
Term tup = d_solver.mkTuple({s1, s2, s3}, {t1, t2, t3}); |
911 |
|
|
912 |
2 |
ASSERT_TRUE(tup.isTupleValue()); |
913 |
2 |
ASSERT_EQ(std::vector<Term>({t1, t2, t3}), tup.getTupleValue()); |
914 |
|
} |
915 |
|
|
916 |
41 |
TEST_F(TestApiBlackTerm, getFloatingPoint) |
917 |
|
{ |
918 |
4 |
Term bvval = d_solver.mkBitVector("0000110000000011"); |
919 |
4 |
Term fp = d_solver.mkFloatingPoint(5, 11, bvval); |
920 |
|
|
921 |
2 |
ASSERT_TRUE(fp.isFloatingPointValue()); |
922 |
2 |
ASSERT_FALSE(fp.isFloatingPointPosZero()); |
923 |
2 |
ASSERT_FALSE(fp.isFloatingPointNegZero()); |
924 |
2 |
ASSERT_FALSE(fp.isFloatingPointPosInf()); |
925 |
2 |
ASSERT_FALSE(fp.isFloatingPointNegInf()); |
926 |
2 |
ASSERT_FALSE(fp.isFloatingPointNaN()); |
927 |
2 |
ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue()); |
928 |
|
|
929 |
2 |
ASSERT_TRUE(d_solver.mkPosZero(5, 11).isFloatingPointPosZero()); |
930 |
2 |
ASSERT_TRUE(d_solver.mkNegZero(5, 11).isFloatingPointNegZero()); |
931 |
2 |
ASSERT_TRUE(d_solver.mkPosInf(5, 11).isFloatingPointPosInf()); |
932 |
2 |
ASSERT_TRUE(d_solver.mkNegInf(5, 11).isFloatingPointNegInf()); |
933 |
2 |
ASSERT_TRUE(d_solver.mkNaN(5, 11).isFloatingPointNaN()); |
934 |
|
} |
935 |
|
|
936 |
41 |
TEST_F(TestApiBlackTerm, getSet) |
937 |
|
{ |
938 |
4 |
Sort s = d_solver.mkSetSort(d_solver.getIntegerSort()); |
939 |
|
|
940 |
4 |
Term i1 = d_solver.mkInteger(5); |
941 |
4 |
Term i2 = d_solver.mkInteger(7); |
942 |
|
|
943 |
4 |
Term s1 = d_solver.mkEmptySet(s); |
944 |
4 |
Term s2 = d_solver.mkTerm(Kind::SINGLETON, i1); |
945 |
4 |
Term s3 = d_solver.mkTerm(Kind::SINGLETON, i1); |
946 |
4 |
Term s4 = d_solver.mkTerm(Kind::SINGLETON, i2); |
947 |
|
Term s5 = |
948 |
4 |
d_solver.mkTerm(Kind::UNION, s2, d_solver.mkTerm(Kind::UNION, s3, s4)); |
949 |
|
|
950 |
2 |
ASSERT_TRUE(s1.isSetValue()); |
951 |
2 |
ASSERT_TRUE(s2.isSetValue()); |
952 |
2 |
ASSERT_TRUE(s3.isSetValue()); |
953 |
2 |
ASSERT_TRUE(s4.isSetValue()); |
954 |
2 |
ASSERT_FALSE(s5.isSetValue()); |
955 |
2 |
s5 = d_solver.simplify(s5); |
956 |
2 |
ASSERT_TRUE(s5.isSetValue()); |
957 |
|
|
958 |
2 |
ASSERT_EQ(std::set<Term>({}), s1.getSetValue()); |
959 |
2 |
ASSERT_EQ(std::set<Term>({i1}), s2.getSetValue()); |
960 |
2 |
ASSERT_EQ(std::set<Term>({i1}), s3.getSetValue()); |
961 |
2 |
ASSERT_EQ(std::set<Term>({i2}), s4.getSetValue()); |
962 |
2 |
ASSERT_EQ(std::set<Term>({i1, i2}), s5.getSetValue()); |
963 |
|
} |
964 |
|
|
965 |
41 |
TEST_F(TestApiBlackTerm, getSequence) |
966 |
|
{ |
967 |
4 |
Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort()); |
968 |
|
|
969 |
4 |
Term i1 = d_solver.mkInteger(5); |
970 |
4 |
Term i2 = d_solver.mkInteger(7); |
971 |
|
|
972 |
4 |
Term s1 = d_solver.mkEmptySequence(s); |
973 |
4 |
Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); |
974 |
4 |
Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); |
975 |
4 |
Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, i2); |
976 |
|
Term s5 = d_solver.mkTerm( |
977 |
4 |
Kind::SEQ_CONCAT, s2, d_solver.mkTerm(Kind::SEQ_CONCAT, s3, s4)); |
978 |
|
|
979 |
2 |
ASSERT_TRUE(s1.isSequenceValue()); |
980 |
2 |
ASSERT_TRUE(!s2.isSequenceValue()); |
981 |
2 |
ASSERT_TRUE(!s3.isSequenceValue()); |
982 |
2 |
ASSERT_TRUE(!s4.isSequenceValue()); |
983 |
2 |
ASSERT_TRUE(!s5.isSequenceValue()); |
984 |
|
|
985 |
2 |
s2 = d_solver.simplify(s2); |
986 |
2 |
s3 = d_solver.simplify(s3); |
987 |
2 |
s4 = d_solver.simplify(s4); |
988 |
2 |
s5 = d_solver.simplify(s5); |
989 |
|
|
990 |
2 |
ASSERT_EQ(std::vector<Term>({}), s1.getSequenceValue()); |
991 |
2 |
ASSERT_EQ(std::vector<Term>({i1}), s2.getSequenceValue()); |
992 |
2 |
ASSERT_EQ(std::vector<Term>({i1}), s3.getSequenceValue()); |
993 |
2 |
ASSERT_EQ(std::vector<Term>({i2}), s4.getSequenceValue()); |
994 |
2 |
ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue()); |
995 |
|
} |
996 |
|
|
997 |
41 |
TEST_F(TestApiBlackTerm, getUninterpretedConst) |
998 |
|
{ |
999 |
4 |
Sort s = d_solver.mkUninterpretedSort("test"); |
1000 |
4 |
Term t1 = d_solver.mkUninterpretedConst(s, 3); |
1001 |
4 |
Term t2 = d_solver.mkUninterpretedConst(s, 5); |
1002 |
|
|
1003 |
2 |
ASSERT_TRUE(t1.isUninterpretedValue()); |
1004 |
2 |
ASSERT_TRUE(t2.isUninterpretedValue()); |
1005 |
|
|
1006 |
2 |
ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue()); |
1007 |
2 |
ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue()); |
1008 |
|
} |
1009 |
|
|
1010 |
41 |
TEST_F(TestApiBlackTerm, substitute) |
1011 |
|
{ |
1012 |
4 |
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); |
1013 |
4 |
Term one = d_solver.mkInteger(1); |
1014 |
4 |
Term ttrue = d_solver.mkTrue(); |
1015 |
4 |
Term xpx = d_solver.mkTerm(PLUS, x, x); |
1016 |
4 |
Term onepone = d_solver.mkTerm(PLUS, one, one); |
1017 |
|
|
1018 |
2 |
ASSERT_EQ(xpx.substitute(x, one), onepone); |
1019 |
2 |
ASSERT_EQ(onepone.substitute(one, x), xpx); |
1020 |
|
// incorrect due to type |
1021 |
4 |
ASSERT_THROW(xpx.substitute(one, ttrue), CVC5ApiException); |
1022 |
|
|
1023 |
|
// simultaneous substitution |
1024 |
4 |
Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); |
1025 |
4 |
Term xpy = d_solver.mkTerm(PLUS, x, y); |
1026 |
4 |
Term xpone = d_solver.mkTerm(PLUS, y, one); |
1027 |
4 |
std::vector<Term> es; |
1028 |
4 |
std::vector<Term> rs; |
1029 |
2 |
es.push_back(x); |
1030 |
2 |
rs.push_back(y); |
1031 |
2 |
es.push_back(y); |
1032 |
2 |
rs.push_back(one); |
1033 |
2 |
ASSERT_EQ(xpy.substitute(es, rs), xpone); |
1034 |
|
|
1035 |
|
// incorrect substitution due to arity |
1036 |
2 |
rs.pop_back(); |
1037 |
4 |
ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); |
1038 |
|
|
1039 |
|
// incorrect substitution due to types |
1040 |
2 |
rs.push_back(ttrue); |
1041 |
4 |
ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); |
1042 |
|
|
1043 |
|
// null cannot substitute |
1044 |
4 |
Term tnull; |
1045 |
4 |
ASSERT_THROW(tnull.substitute(one, x), CVC5ApiException); |
1046 |
4 |
ASSERT_THROW(xpx.substitute(tnull, x), CVC5ApiException); |
1047 |
4 |
ASSERT_THROW(xpx.substitute(x, tnull), CVC5ApiException); |
1048 |
2 |
rs.pop_back(); |
1049 |
2 |
rs.push_back(tnull); |
1050 |
4 |
ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); |
1051 |
2 |
es.clear(); |
1052 |
2 |
rs.clear(); |
1053 |
2 |
es.push_back(x); |
1054 |
2 |
rs.push_back(y); |
1055 |
4 |
ASSERT_THROW(tnull.substitute(es, rs), CVC5ApiException); |
1056 |
2 |
es.push_back(tnull); |
1057 |
2 |
rs.push_back(one); |
1058 |
4 |
ASSERT_THROW(xpx.substitute(es, rs), CVC5ApiException); |
1059 |
|
} |
1060 |
|
|
1061 |
41 |
TEST_F(TestApiBlackTerm, constArray) |
1062 |
|
{ |
1063 |
4 |
Sort intsort = d_solver.getIntegerSort(); |
1064 |
4 |
Sort arrsort = d_solver.mkArraySort(intsort, intsort); |
1065 |
4 |
Term a = d_solver.mkConst(arrsort, "a"); |
1066 |
4 |
Term one = d_solver.mkInteger(1); |
1067 |
4 |
Term constarr = d_solver.mkConstArray(arrsort, one); |
1068 |
|
|
1069 |
2 |
ASSERT_EQ(constarr.getKind(), CONST_ARRAY); |
1070 |
2 |
ASSERT_EQ(constarr.getConstArrayBase(), one); |
1071 |
4 |
ASSERT_THROW(a.getConstArrayBase(), CVC5ApiException); |
1072 |
|
|
1073 |
2 |
arrsort = |
1074 |
4 |
d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); |
1075 |
4 |
Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0)); |
1076 |
|
Term stores = d_solver.mkTerm( |
1077 |
4 |
STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2)); |
1078 |
2 |
stores = |
1079 |
4 |
d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3)); |
1080 |
2 |
stores = |
1081 |
4 |
d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); |
1082 |
|
} |
1083 |
|
|
1084 |
41 |
TEST_F(TestApiBlackTerm, getSequenceValue) |
1085 |
|
{ |
1086 |
4 |
Sort realsort = d_solver.getRealSort(); |
1087 |
4 |
Sort seqsort = d_solver.mkSequenceSort(realsort); |
1088 |
4 |
Term s = d_solver.mkEmptySequence(seqsort); |
1089 |
|
|
1090 |
2 |
ASSERT_EQ(s.getKind(), CONST_SEQUENCE); |
1091 |
|
// empty sequence has zero elements |
1092 |
4 |
std::vector<Term> cs = s.getSequenceValue(); |
1093 |
2 |
ASSERT_TRUE(cs.empty()); |
1094 |
|
|
1095 |
|
// A seq.unit app is not a constant sequence (regardless of whether it is |
1096 |
|
// applied to a constant). |
1097 |
4 |
Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); |
1098 |
4 |
ASSERT_THROW(su.getSequenceValue(), CVC5ApiException); |
1099 |
|
} |
1100 |
|
|
1101 |
41 |
TEST_F(TestApiBlackTerm, termScopedToString) |
1102 |
|
{ |
1103 |
4 |
Sort intsort = d_solver.getIntegerSort(); |
1104 |
4 |
Term x = d_solver.mkConst(intsort, "x"); |
1105 |
2 |
ASSERT_EQ(x.toString(), "x"); |
1106 |
4 |
Solver solver2; |
1107 |
2 |
ASSERT_EQ(x.toString(), "x"); |
1108 |
|
} |
1109 |
|
} // namespace test |
1110 |
99 |
} // namespace cvc5 |