1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Gereon Kremer, Mathias Preiner
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 * Black box testing of the Term class.
18 namespace cvc5::internal
{
22 class TestApiBlackTerm
: public TestApi
26 TEST_F(TestApiBlackTerm
, eq
)
28 Sort uSort
= d_solver
.mkUninterpretedSort("u");
29 Term x
= d_solver
.mkVar(uSort
, "x");
30 Term y
= d_solver
.mkVar(uSort
, "y");
37 ASSERT_FALSE((x
== z
));
41 TEST_F(TestApiBlackTerm
, getId
)
44 ASSERT_THROW(n
.getId(), CVC5ApiException
);
45 Term x
= d_solver
.mkVar(d_solver
.getIntegerSort(), "x");
46 ASSERT_NO_THROW(x
.getId());
48 ASSERT_EQ(x
.getId(), y
.getId());
50 Term z
= d_solver
.mkVar(d_solver
.getIntegerSort(), "z");
51 ASSERT_NE(x
.getId(), z
.getId());
54 TEST_F(TestApiBlackTerm
, getKind
)
56 Sort uSort
= d_solver
.mkUninterpretedSort("u");
57 Sort intSort
= d_solver
.getIntegerSort();
58 Sort boolSort
= d_solver
.getBooleanSort();
59 Sort funSort1
= d_solver
.mkFunctionSort({uSort
}, intSort
);
60 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
63 ASSERT_THROW(n
.getKind(), CVC5ApiException
);
64 Term x
= d_solver
.mkVar(uSort
, "x");
65 ASSERT_NO_THROW(x
.getKind());
66 Term y
= d_solver
.mkVar(uSort
, "y");
67 ASSERT_NO_THROW(y
.getKind());
69 Term f
= d_solver
.mkVar(funSort1
, "f");
70 ASSERT_NO_THROW(f
.getKind());
71 Term p
= d_solver
.mkVar(funSort2
, "p");
72 ASSERT_NO_THROW(p
.getKind());
74 Term zero
= d_solver
.mkInteger(0);
75 ASSERT_NO_THROW(zero
.getKind());
77 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
78 ASSERT_NO_THROW(f_x
.getKind());
79 Term f_y
= d_solver
.mkTerm(APPLY_UF
, {f
, y
});
80 ASSERT_NO_THROW(f_y
.getKind());
81 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_y
});
82 ASSERT_NO_THROW(sum
.getKind());
83 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
84 ASSERT_NO_THROW(p_0
.getKind());
85 Term p_f_y
= d_solver
.mkTerm(APPLY_UF
, {p
, f_y
});
86 ASSERT_NO_THROW(p_f_y
.getKind());
88 // Sequence kinds do not exist internally, test that the API properly
89 // converts them back.
90 Sort seqSort
= d_solver
.mkSequenceSort(intSort
);
91 Term s
= d_solver
.mkConst(seqSort
, "s");
92 Term ss
= d_solver
.mkTerm(SEQ_CONCAT
, {s
, s
});
93 ASSERT_EQ(ss
.getKind(), SEQ_CONCAT
);
96 TEST_F(TestApiBlackTerm
, getSort
)
98 Sort bvSort
= d_solver
.mkBitVectorSort(8);
99 Sort intSort
= d_solver
.getIntegerSort();
100 Sort boolSort
= d_solver
.getBooleanSort();
101 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
102 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
105 ASSERT_THROW(n
.getSort(), CVC5ApiException
);
106 Term x
= d_solver
.mkVar(bvSort
, "x");
107 ASSERT_NO_THROW(x
.getSort());
108 ASSERT_EQ(x
.getSort(), bvSort
);
109 Term y
= d_solver
.mkVar(bvSort
, "y");
110 ASSERT_NO_THROW(y
.getSort());
111 ASSERT_EQ(y
.getSort(), bvSort
);
113 Term f
= d_solver
.mkVar(funSort1
, "f");
114 ASSERT_NO_THROW(f
.getSort());
115 ASSERT_EQ(f
.getSort(), funSort1
);
116 Term p
= d_solver
.mkVar(funSort2
, "p");
117 ASSERT_NO_THROW(p
.getSort());
118 ASSERT_EQ(p
.getSort(), funSort2
);
120 Term zero
= d_solver
.mkInteger(0);
121 ASSERT_NO_THROW(zero
.getSort());
122 ASSERT_EQ(zero
.getSort(), intSort
);
124 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
125 ASSERT_NO_THROW(f_x
.getSort());
126 ASSERT_EQ(f_x
.getSort(), intSort
);
127 Term f_y
= d_solver
.mkTerm(APPLY_UF
, {f
, y
});
128 ASSERT_NO_THROW(f_y
.getSort());
129 ASSERT_EQ(f_y
.getSort(), intSort
);
130 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_y
});
131 ASSERT_NO_THROW(sum
.getSort());
132 ASSERT_EQ(sum
.getSort(), intSort
);
133 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
134 ASSERT_NO_THROW(p_0
.getSort());
135 ASSERT_EQ(p_0
.getSort(), boolSort
);
136 Term p_f_y
= d_solver
.mkTerm(APPLY_UF
, {p
, f_y
});
137 ASSERT_NO_THROW(p_f_y
.getSort());
138 ASSERT_EQ(p_f_y
.getSort(), boolSort
);
141 TEST_F(TestApiBlackTerm
, getOp
)
143 Sort intsort
= d_solver
.getIntegerSort();
144 Sort bvsort
= d_solver
.mkBitVectorSort(8);
145 Sort arrsort
= d_solver
.mkArraySort(bvsort
, intsort
);
146 Sort funsort
= d_solver
.mkFunctionSort({intsort
}, bvsort
);
148 Term x
= d_solver
.mkConst(intsort
, "x");
149 Term a
= d_solver
.mkConst(arrsort
, "a");
150 Term b
= d_solver
.mkConst(bvsort
, "b");
152 ASSERT_FALSE(x
.hasOp());
153 ASSERT_THROW(x
.getOp(), CVC5ApiException
);
155 Term ab
= d_solver
.mkTerm(SELECT
, {a
, b
});
156 Op ext
= d_solver
.mkOp(BITVECTOR_EXTRACT
, {4, 0});
157 Term extb
= d_solver
.mkTerm(ext
, {b
});
159 ASSERT_TRUE(ab
.hasOp());
160 ASSERT_FALSE(ab
.getOp().isIndexed());
161 // can compare directly to a Kind (will invoke Op constructor)
162 ASSERT_TRUE(extb
.hasOp());
163 ASSERT_TRUE(extb
.getOp().isIndexed());
164 ASSERT_EQ(extb
.getOp(), ext
);
166 Term f
= d_solver
.mkConst(funsort
, "f");
167 Term fx
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
169 ASSERT_FALSE(f
.hasOp());
170 ASSERT_THROW(f
.getOp(), CVC5ApiException
);
171 ASSERT_TRUE(fx
.hasOp());
172 std::vector
<Term
> children(fx
.begin(), fx
.end());
173 // testing rebuild from op and children
174 ASSERT_EQ(fx
, d_solver
.mkTerm(fx
.getOp(), children
));
176 // Test Datatypes Ops
177 Sort sort
= d_solver
.mkParamSort("T");
178 DatatypeDecl listDecl
= d_solver
.mkDatatypeDecl("paramlist", {sort
});
179 DatatypeConstructorDecl cons
= d_solver
.mkDatatypeConstructorDecl("cons");
180 DatatypeConstructorDecl nil
= d_solver
.mkDatatypeConstructorDecl("nil");
181 cons
.addSelector("head", sort
);
182 cons
.addSelectorSelf("tail");
183 listDecl
.addConstructor(cons
);
184 listDecl
.addConstructor(nil
);
185 Sort listSort
= d_solver
.mkDatatypeSort(listDecl
);
187 listSort
.instantiate(std::vector
<Sort
>{d_solver
.getIntegerSort()});
188 Term c
= d_solver
.mkConst(intListSort
, "c");
189 Datatype list
= listSort
.getDatatype();
190 // list datatype constructor and selector operator terms
191 Term consOpTerm
= list
.getConstructor("cons").getTerm();
192 Term nilOpTerm
= list
.getConstructor("nil").getTerm();
193 Term headOpTerm
= list
["cons"].getSelector("head").getTerm();
194 Term tailOpTerm
= list
["cons"].getSelector("tail").getTerm();
196 Term nilTerm
= d_solver
.mkTerm(APPLY_CONSTRUCTOR
, {nilOpTerm
});
197 Term consTerm
= d_solver
.mkTerm(APPLY_CONSTRUCTOR
,
198 {consOpTerm
, d_solver
.mkInteger(0), nilTerm
});
199 Term headTerm
= d_solver
.mkTerm(APPLY_SELECTOR
, {headOpTerm
, consTerm
});
200 Term tailTerm
= d_solver
.mkTerm(APPLY_SELECTOR
, {tailOpTerm
, consTerm
});
202 ASSERT_TRUE(nilTerm
.hasOp());
203 ASSERT_TRUE(consTerm
.hasOp());
204 ASSERT_TRUE(headTerm
.hasOp());
205 ASSERT_TRUE(tailTerm
.hasOp());
209 children
.insert(children
.begin(), headTerm
.begin(), headTerm
.end());
210 ASSERT_EQ(headTerm
, d_solver
.mkTerm(headTerm
.getOp(), children
));
213 TEST_F(TestApiBlackTerm
, hasGetSymbol
)
216 Term t
= d_solver
.mkBoolean(true);
217 Term c
= d_solver
.mkConst(d_solver
.getBooleanSort(), "|\\|");
219 ASSERT_THROW(n
.hasSymbol(), CVC5ApiException
);
220 ASSERT_FALSE(t
.hasSymbol());
221 ASSERT_TRUE(c
.hasSymbol());
223 ASSERT_THROW(n
.getSymbol(), CVC5ApiException
);
224 ASSERT_THROW(t
.getSymbol(), CVC5ApiException
);
225 ASSERT_EQ(c
.getSymbol(), "|\\|");
228 TEST_F(TestApiBlackTerm
, isNull
)
231 ASSERT_TRUE(x
.isNull());
232 x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(4), "x");
233 ASSERT_FALSE(x
.isNull());
236 TEST_F(TestApiBlackTerm
, notTerm
)
238 Sort bvSort
= d_solver
.mkBitVectorSort(8);
239 Sort intSort
= d_solver
.getIntegerSort();
240 Sort boolSort
= d_solver
.getBooleanSort();
241 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
242 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
244 ASSERT_THROW(Term().notTerm(), CVC5ApiException
);
245 Term b
= d_solver
.mkTrue();
246 ASSERT_NO_THROW(b
.notTerm());
247 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
248 ASSERT_THROW(x
.notTerm(), CVC5ApiException
);
249 Term f
= d_solver
.mkVar(funSort1
, "f");
250 ASSERT_THROW(f
.notTerm(), CVC5ApiException
);
251 Term p
= d_solver
.mkVar(funSort2
, "p");
252 ASSERT_THROW(p
.notTerm(), CVC5ApiException
);
253 Term zero
= d_solver
.mkInteger(0);
254 ASSERT_THROW(zero
.notTerm(), CVC5ApiException
);
255 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
256 ASSERT_THROW(f_x
.notTerm(), CVC5ApiException
);
257 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
258 ASSERT_THROW(sum
.notTerm(), CVC5ApiException
);
259 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
260 ASSERT_NO_THROW(p_0
.notTerm());
261 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
262 ASSERT_NO_THROW(p_f_x
.notTerm());
265 TEST_F(TestApiBlackTerm
, andTerm
)
267 Sort bvSort
= d_solver
.mkBitVectorSort(8);
268 Sort intSort
= d_solver
.getIntegerSort();
269 Sort boolSort
= d_solver
.getBooleanSort();
270 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
271 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
273 Term b
= d_solver
.mkTrue();
274 ASSERT_THROW(Term().andTerm(b
), CVC5ApiException
);
275 ASSERT_THROW(b
.andTerm(Term()), CVC5ApiException
);
276 ASSERT_NO_THROW(b
.andTerm(b
));
277 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
278 ASSERT_THROW(x
.andTerm(b
), CVC5ApiException
);
279 ASSERT_THROW(x
.andTerm(x
), CVC5ApiException
);
280 Term f
= d_solver
.mkVar(funSort1
, "f");
281 ASSERT_THROW(f
.andTerm(b
), CVC5ApiException
);
282 ASSERT_THROW(f
.andTerm(x
), CVC5ApiException
);
283 ASSERT_THROW(f
.andTerm(f
), CVC5ApiException
);
284 Term p
= d_solver
.mkVar(funSort2
, "p");
285 ASSERT_THROW(p
.andTerm(b
), CVC5ApiException
);
286 ASSERT_THROW(p
.andTerm(x
), CVC5ApiException
);
287 ASSERT_THROW(p
.andTerm(f
), CVC5ApiException
);
288 ASSERT_THROW(p
.andTerm(p
), CVC5ApiException
);
289 Term zero
= d_solver
.mkInteger(0);
290 ASSERT_THROW(zero
.andTerm(b
), CVC5ApiException
);
291 ASSERT_THROW(zero
.andTerm(x
), CVC5ApiException
);
292 ASSERT_THROW(zero
.andTerm(f
), CVC5ApiException
);
293 ASSERT_THROW(zero
.andTerm(p
), CVC5ApiException
);
294 ASSERT_THROW(zero
.andTerm(zero
), CVC5ApiException
);
295 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
296 ASSERT_THROW(f_x
.andTerm(b
), CVC5ApiException
);
297 ASSERT_THROW(f_x
.andTerm(x
), CVC5ApiException
);
298 ASSERT_THROW(f_x
.andTerm(f
), CVC5ApiException
);
299 ASSERT_THROW(f_x
.andTerm(p
), CVC5ApiException
);
300 ASSERT_THROW(f_x
.andTerm(zero
), CVC5ApiException
);
301 ASSERT_THROW(f_x
.andTerm(f_x
), CVC5ApiException
);
302 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
303 ASSERT_THROW(sum
.andTerm(b
), CVC5ApiException
);
304 ASSERT_THROW(sum
.andTerm(x
), CVC5ApiException
);
305 ASSERT_THROW(sum
.andTerm(f
), CVC5ApiException
);
306 ASSERT_THROW(sum
.andTerm(p
), CVC5ApiException
);
307 ASSERT_THROW(sum
.andTerm(zero
), CVC5ApiException
);
308 ASSERT_THROW(sum
.andTerm(f_x
), CVC5ApiException
);
309 ASSERT_THROW(sum
.andTerm(sum
), CVC5ApiException
);
310 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
311 ASSERT_NO_THROW(p_0
.andTerm(b
));
312 ASSERT_THROW(p_0
.andTerm(x
), CVC5ApiException
);
313 ASSERT_THROW(p_0
.andTerm(f
), CVC5ApiException
);
314 ASSERT_THROW(p_0
.andTerm(p
), CVC5ApiException
);
315 ASSERT_THROW(p_0
.andTerm(zero
), CVC5ApiException
);
316 ASSERT_THROW(p_0
.andTerm(f_x
), CVC5ApiException
);
317 ASSERT_THROW(p_0
.andTerm(sum
), CVC5ApiException
);
318 ASSERT_NO_THROW(p_0
.andTerm(p_0
));
319 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
320 ASSERT_NO_THROW(p_f_x
.andTerm(b
));
321 ASSERT_THROW(p_f_x
.andTerm(x
), CVC5ApiException
);
322 ASSERT_THROW(p_f_x
.andTerm(f
), CVC5ApiException
);
323 ASSERT_THROW(p_f_x
.andTerm(p
), CVC5ApiException
);
324 ASSERT_THROW(p_f_x
.andTerm(zero
), CVC5ApiException
);
325 ASSERT_THROW(p_f_x
.andTerm(f_x
), CVC5ApiException
);
326 ASSERT_THROW(p_f_x
.andTerm(sum
), CVC5ApiException
);
327 ASSERT_NO_THROW(p_f_x
.andTerm(p_0
));
328 ASSERT_NO_THROW(p_f_x
.andTerm(p_f_x
));
331 TEST_F(TestApiBlackTerm
, orTerm
)
333 Sort bvSort
= d_solver
.mkBitVectorSort(8);
334 Sort intSort
= d_solver
.getIntegerSort();
335 Sort boolSort
= d_solver
.getBooleanSort();
336 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
337 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
339 Term b
= d_solver
.mkTrue();
340 ASSERT_THROW(Term().orTerm(b
), CVC5ApiException
);
341 ASSERT_THROW(b
.orTerm(Term()), CVC5ApiException
);
342 ASSERT_NO_THROW(b
.orTerm(b
));
343 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
344 ASSERT_THROW(x
.orTerm(b
), CVC5ApiException
);
345 ASSERT_THROW(x
.orTerm(x
), CVC5ApiException
);
346 Term f
= d_solver
.mkVar(funSort1
, "f");
347 ASSERT_THROW(f
.orTerm(b
), CVC5ApiException
);
348 ASSERT_THROW(f
.orTerm(x
), CVC5ApiException
);
349 ASSERT_THROW(f
.orTerm(f
), CVC5ApiException
);
350 Term p
= d_solver
.mkVar(funSort2
, "p");
351 ASSERT_THROW(p
.orTerm(b
), CVC5ApiException
);
352 ASSERT_THROW(p
.orTerm(x
), CVC5ApiException
);
353 ASSERT_THROW(p
.orTerm(f
), CVC5ApiException
);
354 ASSERT_THROW(p
.orTerm(p
), CVC5ApiException
);
355 Term zero
= d_solver
.mkInteger(0);
356 ASSERT_THROW(zero
.orTerm(b
), CVC5ApiException
);
357 ASSERT_THROW(zero
.orTerm(x
), CVC5ApiException
);
358 ASSERT_THROW(zero
.orTerm(f
), CVC5ApiException
);
359 ASSERT_THROW(zero
.orTerm(p
), CVC5ApiException
);
360 ASSERT_THROW(zero
.orTerm(zero
), CVC5ApiException
);
361 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
362 ASSERT_THROW(f_x
.orTerm(b
), CVC5ApiException
);
363 ASSERT_THROW(f_x
.orTerm(x
), CVC5ApiException
);
364 ASSERT_THROW(f_x
.orTerm(f
), CVC5ApiException
);
365 ASSERT_THROW(f_x
.orTerm(p
), CVC5ApiException
);
366 ASSERT_THROW(f_x
.orTerm(zero
), CVC5ApiException
);
367 ASSERT_THROW(f_x
.orTerm(f_x
), CVC5ApiException
);
368 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
369 ASSERT_THROW(sum
.orTerm(b
), CVC5ApiException
);
370 ASSERT_THROW(sum
.orTerm(x
), CVC5ApiException
);
371 ASSERT_THROW(sum
.orTerm(f
), CVC5ApiException
);
372 ASSERT_THROW(sum
.orTerm(p
), CVC5ApiException
);
373 ASSERT_THROW(sum
.orTerm(zero
), CVC5ApiException
);
374 ASSERT_THROW(sum
.orTerm(f_x
), CVC5ApiException
);
375 ASSERT_THROW(sum
.orTerm(sum
), CVC5ApiException
);
376 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
377 ASSERT_NO_THROW(p_0
.orTerm(b
));
378 ASSERT_THROW(p_0
.orTerm(x
), CVC5ApiException
);
379 ASSERT_THROW(p_0
.orTerm(f
), CVC5ApiException
);
380 ASSERT_THROW(p_0
.orTerm(p
), CVC5ApiException
);
381 ASSERT_THROW(p_0
.orTerm(zero
), CVC5ApiException
);
382 ASSERT_THROW(p_0
.orTerm(f_x
), CVC5ApiException
);
383 ASSERT_THROW(p_0
.orTerm(sum
), CVC5ApiException
);
384 ASSERT_NO_THROW(p_0
.orTerm(p_0
));
385 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
386 ASSERT_NO_THROW(p_f_x
.orTerm(b
));
387 ASSERT_THROW(p_f_x
.orTerm(x
), CVC5ApiException
);
388 ASSERT_THROW(p_f_x
.orTerm(f
), CVC5ApiException
);
389 ASSERT_THROW(p_f_x
.orTerm(p
), CVC5ApiException
);
390 ASSERT_THROW(p_f_x
.orTerm(zero
), CVC5ApiException
);
391 ASSERT_THROW(p_f_x
.orTerm(f_x
), CVC5ApiException
);
392 ASSERT_THROW(p_f_x
.orTerm(sum
), CVC5ApiException
);
393 ASSERT_NO_THROW(p_f_x
.orTerm(p_0
));
394 ASSERT_NO_THROW(p_f_x
.orTerm(p_f_x
));
397 TEST_F(TestApiBlackTerm
, xorTerm
)
399 Sort bvSort
= d_solver
.mkBitVectorSort(8);
400 Sort intSort
= d_solver
.getIntegerSort();
401 Sort boolSort
= d_solver
.getBooleanSort();
402 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
403 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
405 Term b
= d_solver
.mkTrue();
406 ASSERT_THROW(Term().xorTerm(b
), CVC5ApiException
);
407 ASSERT_THROW(b
.xorTerm(Term()), CVC5ApiException
);
408 ASSERT_NO_THROW(b
.xorTerm(b
));
409 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
410 ASSERT_THROW(x
.xorTerm(b
), CVC5ApiException
);
411 ASSERT_THROW(x
.xorTerm(x
), CVC5ApiException
);
412 Term f
= d_solver
.mkVar(funSort1
, "f");
413 ASSERT_THROW(f
.xorTerm(b
), CVC5ApiException
);
414 ASSERT_THROW(f
.xorTerm(x
), CVC5ApiException
);
415 ASSERT_THROW(f
.xorTerm(f
), CVC5ApiException
);
416 Term p
= d_solver
.mkVar(funSort2
, "p");
417 ASSERT_THROW(p
.xorTerm(b
), CVC5ApiException
);
418 ASSERT_THROW(p
.xorTerm(x
), CVC5ApiException
);
419 ASSERT_THROW(p
.xorTerm(f
), CVC5ApiException
);
420 ASSERT_THROW(p
.xorTerm(p
), CVC5ApiException
);
421 Term zero
= d_solver
.mkInteger(0);
422 ASSERT_THROW(zero
.xorTerm(b
), CVC5ApiException
);
423 ASSERT_THROW(zero
.xorTerm(x
), CVC5ApiException
);
424 ASSERT_THROW(zero
.xorTerm(f
), CVC5ApiException
);
425 ASSERT_THROW(zero
.xorTerm(p
), CVC5ApiException
);
426 ASSERT_THROW(zero
.xorTerm(zero
), CVC5ApiException
);
427 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
428 ASSERT_THROW(f_x
.xorTerm(b
), CVC5ApiException
);
429 ASSERT_THROW(f_x
.xorTerm(x
), CVC5ApiException
);
430 ASSERT_THROW(f_x
.xorTerm(f
), CVC5ApiException
);
431 ASSERT_THROW(f_x
.xorTerm(p
), CVC5ApiException
);
432 ASSERT_THROW(f_x
.xorTerm(zero
), CVC5ApiException
);
433 ASSERT_THROW(f_x
.xorTerm(f_x
), CVC5ApiException
);
434 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
435 ASSERT_THROW(sum
.xorTerm(b
), CVC5ApiException
);
436 ASSERT_THROW(sum
.xorTerm(x
), CVC5ApiException
);
437 ASSERT_THROW(sum
.xorTerm(f
), CVC5ApiException
);
438 ASSERT_THROW(sum
.xorTerm(p
), CVC5ApiException
);
439 ASSERT_THROW(sum
.xorTerm(zero
), CVC5ApiException
);
440 ASSERT_THROW(sum
.xorTerm(f_x
), CVC5ApiException
);
441 ASSERT_THROW(sum
.xorTerm(sum
), CVC5ApiException
);
442 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
443 ASSERT_NO_THROW(p_0
.xorTerm(b
));
444 ASSERT_THROW(p_0
.xorTerm(x
), CVC5ApiException
);
445 ASSERT_THROW(p_0
.xorTerm(f
), CVC5ApiException
);
446 ASSERT_THROW(p_0
.xorTerm(p
), CVC5ApiException
);
447 ASSERT_THROW(p_0
.xorTerm(zero
), CVC5ApiException
);
448 ASSERT_THROW(p_0
.xorTerm(f_x
), CVC5ApiException
);
449 ASSERT_THROW(p_0
.xorTerm(sum
), CVC5ApiException
);
450 ASSERT_NO_THROW(p_0
.xorTerm(p_0
));
451 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
452 ASSERT_NO_THROW(p_f_x
.xorTerm(b
));
453 ASSERT_THROW(p_f_x
.xorTerm(x
), CVC5ApiException
);
454 ASSERT_THROW(p_f_x
.xorTerm(f
), CVC5ApiException
);
455 ASSERT_THROW(p_f_x
.xorTerm(p
), CVC5ApiException
);
456 ASSERT_THROW(p_f_x
.xorTerm(zero
), CVC5ApiException
);
457 ASSERT_THROW(p_f_x
.xorTerm(f_x
), CVC5ApiException
);
458 ASSERT_THROW(p_f_x
.xorTerm(sum
), CVC5ApiException
);
459 ASSERT_NO_THROW(p_f_x
.xorTerm(p_0
));
460 ASSERT_NO_THROW(p_f_x
.xorTerm(p_f_x
));
463 TEST_F(TestApiBlackTerm
, eqTerm
)
465 Sort bvSort
= d_solver
.mkBitVectorSort(8);
466 Sort intSort
= d_solver
.getIntegerSort();
467 Sort boolSort
= d_solver
.getBooleanSort();
468 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
469 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
471 Term b
= d_solver
.mkTrue();
472 ASSERT_THROW(Term().eqTerm(b
), CVC5ApiException
);
473 ASSERT_THROW(b
.eqTerm(Term()), CVC5ApiException
);
474 ASSERT_NO_THROW(b
.eqTerm(b
));
475 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
476 ASSERT_THROW(x
.eqTerm(b
), CVC5ApiException
);
477 ASSERT_NO_THROW(x
.eqTerm(x
));
478 Term f
= d_solver
.mkVar(funSort1
, "f");
479 ASSERT_THROW(f
.eqTerm(b
), CVC5ApiException
);
480 ASSERT_THROW(f
.eqTerm(x
), CVC5ApiException
);
481 ASSERT_NO_THROW(f
.eqTerm(f
));
482 Term p
= d_solver
.mkVar(funSort2
, "p");
483 ASSERT_THROW(p
.eqTerm(b
), CVC5ApiException
);
484 ASSERT_THROW(p
.eqTerm(x
), CVC5ApiException
);
485 ASSERT_THROW(p
.eqTerm(f
), CVC5ApiException
);
486 ASSERT_NO_THROW(p
.eqTerm(p
));
487 Term zero
= d_solver
.mkInteger(0);
488 ASSERT_THROW(zero
.eqTerm(b
), CVC5ApiException
);
489 ASSERT_THROW(zero
.eqTerm(x
), CVC5ApiException
);
490 ASSERT_THROW(zero
.eqTerm(f
), CVC5ApiException
);
491 ASSERT_THROW(zero
.eqTerm(p
), CVC5ApiException
);
492 ASSERT_NO_THROW(zero
.eqTerm(zero
));
493 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
494 ASSERT_THROW(f_x
.eqTerm(b
), CVC5ApiException
);
495 ASSERT_THROW(f_x
.eqTerm(x
), CVC5ApiException
);
496 ASSERT_THROW(f_x
.eqTerm(f
), CVC5ApiException
);
497 ASSERT_THROW(f_x
.eqTerm(p
), CVC5ApiException
);
498 ASSERT_NO_THROW(f_x
.eqTerm(zero
));
499 ASSERT_NO_THROW(f_x
.eqTerm(f_x
));
500 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
501 ASSERT_THROW(sum
.eqTerm(b
), CVC5ApiException
);
502 ASSERT_THROW(sum
.eqTerm(x
), CVC5ApiException
);
503 ASSERT_THROW(sum
.eqTerm(f
), CVC5ApiException
);
504 ASSERT_THROW(sum
.eqTerm(p
), CVC5ApiException
);
505 ASSERT_NO_THROW(sum
.eqTerm(zero
));
506 ASSERT_NO_THROW(sum
.eqTerm(f_x
));
507 ASSERT_NO_THROW(sum
.eqTerm(sum
));
508 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
509 ASSERT_NO_THROW(p_0
.eqTerm(b
));
510 ASSERT_THROW(p_0
.eqTerm(x
), CVC5ApiException
);
511 ASSERT_THROW(p_0
.eqTerm(f
), CVC5ApiException
);
512 ASSERT_THROW(p_0
.eqTerm(p
), CVC5ApiException
);
513 ASSERT_THROW(p_0
.eqTerm(zero
), CVC5ApiException
);
514 ASSERT_THROW(p_0
.eqTerm(f_x
), CVC5ApiException
);
515 ASSERT_THROW(p_0
.eqTerm(sum
), CVC5ApiException
);
516 ASSERT_NO_THROW(p_0
.eqTerm(p_0
));
517 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
518 ASSERT_NO_THROW(p_f_x
.eqTerm(b
));
519 ASSERT_THROW(p_f_x
.eqTerm(x
), CVC5ApiException
);
520 ASSERT_THROW(p_f_x
.eqTerm(f
), CVC5ApiException
);
521 ASSERT_THROW(p_f_x
.eqTerm(p
), CVC5ApiException
);
522 ASSERT_THROW(p_f_x
.eqTerm(zero
), CVC5ApiException
);
523 ASSERT_THROW(p_f_x
.eqTerm(f_x
), CVC5ApiException
);
524 ASSERT_THROW(p_f_x
.eqTerm(sum
), CVC5ApiException
);
525 ASSERT_NO_THROW(p_f_x
.eqTerm(p_0
));
526 ASSERT_NO_THROW(p_f_x
.eqTerm(p_f_x
));
529 TEST_F(TestApiBlackTerm
, impTerm
)
531 Sort bvSort
= d_solver
.mkBitVectorSort(8);
532 Sort intSort
= d_solver
.getIntegerSort();
533 Sort boolSort
= d_solver
.getBooleanSort();
534 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
535 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
537 Term b
= d_solver
.mkTrue();
538 ASSERT_THROW(Term().impTerm(b
), CVC5ApiException
);
539 ASSERT_THROW(b
.impTerm(Term()), CVC5ApiException
);
540 ASSERT_NO_THROW(b
.impTerm(b
));
541 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
542 ASSERT_THROW(x
.impTerm(b
), CVC5ApiException
);
543 ASSERT_THROW(x
.impTerm(x
), CVC5ApiException
);
544 Term f
= d_solver
.mkVar(funSort1
, "f");
545 ASSERT_THROW(f
.impTerm(b
), CVC5ApiException
);
546 ASSERT_THROW(f
.impTerm(x
), CVC5ApiException
);
547 ASSERT_THROW(f
.impTerm(f
), CVC5ApiException
);
548 Term p
= d_solver
.mkVar(funSort2
, "p");
549 ASSERT_THROW(p
.impTerm(b
), CVC5ApiException
);
550 ASSERT_THROW(p
.impTerm(x
), CVC5ApiException
);
551 ASSERT_THROW(p
.impTerm(f
), CVC5ApiException
);
552 ASSERT_THROW(p
.impTerm(p
), CVC5ApiException
);
553 Term zero
= d_solver
.mkInteger(0);
554 ASSERT_THROW(zero
.impTerm(b
), CVC5ApiException
);
555 ASSERT_THROW(zero
.impTerm(x
), CVC5ApiException
);
556 ASSERT_THROW(zero
.impTerm(f
), CVC5ApiException
);
557 ASSERT_THROW(zero
.impTerm(p
), CVC5ApiException
);
558 ASSERT_THROW(zero
.impTerm(zero
), CVC5ApiException
);
559 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
560 ASSERT_THROW(f_x
.impTerm(b
), CVC5ApiException
);
561 ASSERT_THROW(f_x
.impTerm(x
), CVC5ApiException
);
562 ASSERT_THROW(f_x
.impTerm(f
), CVC5ApiException
);
563 ASSERT_THROW(f_x
.impTerm(p
), CVC5ApiException
);
564 ASSERT_THROW(f_x
.impTerm(zero
), CVC5ApiException
);
565 ASSERT_THROW(f_x
.impTerm(f_x
), CVC5ApiException
);
566 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
567 ASSERT_THROW(sum
.impTerm(b
), CVC5ApiException
);
568 ASSERT_THROW(sum
.impTerm(x
), CVC5ApiException
);
569 ASSERT_THROW(sum
.impTerm(f
), CVC5ApiException
);
570 ASSERT_THROW(sum
.impTerm(p
), CVC5ApiException
);
571 ASSERT_THROW(sum
.impTerm(zero
), CVC5ApiException
);
572 ASSERT_THROW(sum
.impTerm(f_x
), CVC5ApiException
);
573 ASSERT_THROW(sum
.impTerm(sum
), CVC5ApiException
);
574 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
575 ASSERT_NO_THROW(p_0
.impTerm(b
));
576 ASSERT_THROW(p_0
.impTerm(x
), CVC5ApiException
);
577 ASSERT_THROW(p_0
.impTerm(f
), CVC5ApiException
);
578 ASSERT_THROW(p_0
.impTerm(p
), CVC5ApiException
);
579 ASSERT_THROW(p_0
.impTerm(zero
), CVC5ApiException
);
580 ASSERT_THROW(p_0
.impTerm(f_x
), CVC5ApiException
);
581 ASSERT_THROW(p_0
.impTerm(sum
), CVC5ApiException
);
582 ASSERT_NO_THROW(p_0
.impTerm(p_0
));
583 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
584 ASSERT_NO_THROW(p_f_x
.impTerm(b
));
585 ASSERT_THROW(p_f_x
.impTerm(x
), CVC5ApiException
);
586 ASSERT_THROW(p_f_x
.impTerm(f
), CVC5ApiException
);
587 ASSERT_THROW(p_f_x
.impTerm(p
), CVC5ApiException
);
588 ASSERT_THROW(p_f_x
.impTerm(zero
), CVC5ApiException
);
589 ASSERT_THROW(p_f_x
.impTerm(f_x
), CVC5ApiException
);
590 ASSERT_THROW(p_f_x
.impTerm(sum
), CVC5ApiException
);
591 ASSERT_NO_THROW(p_f_x
.impTerm(p_0
));
592 ASSERT_NO_THROW(p_f_x
.impTerm(p_f_x
));
595 TEST_F(TestApiBlackTerm
, iteTerm
)
597 Sort bvSort
= d_solver
.mkBitVectorSort(8);
598 Sort intSort
= d_solver
.getIntegerSort();
599 Sort boolSort
= d_solver
.getBooleanSort();
600 Sort funSort1
= d_solver
.mkFunctionSort({bvSort
}, intSort
);
601 Sort funSort2
= d_solver
.mkFunctionSort({intSort
}, boolSort
);
603 Term b
= d_solver
.mkTrue();
604 ASSERT_THROW(Term().iteTerm(b
, b
), CVC5ApiException
);
605 ASSERT_THROW(b
.iteTerm(Term(), b
), CVC5ApiException
);
606 ASSERT_THROW(b
.iteTerm(b
, Term()), CVC5ApiException
);
607 ASSERT_NO_THROW(b
.iteTerm(b
, b
));
608 Term x
= d_solver
.mkVar(d_solver
.mkBitVectorSort(8), "x");
609 ASSERT_NO_THROW(b
.iteTerm(x
, x
));
610 ASSERT_NO_THROW(b
.iteTerm(b
, b
));
611 ASSERT_THROW(b
.iteTerm(x
, b
), CVC5ApiException
);
612 ASSERT_THROW(x
.iteTerm(x
, x
), CVC5ApiException
);
613 ASSERT_THROW(x
.iteTerm(x
, b
), CVC5ApiException
);
614 Term f
= d_solver
.mkVar(funSort1
, "f");
615 ASSERT_THROW(f
.iteTerm(b
, b
), CVC5ApiException
);
616 ASSERT_THROW(x
.iteTerm(b
, x
), CVC5ApiException
);
617 Term p
= d_solver
.mkVar(funSort2
, "p");
618 ASSERT_THROW(p
.iteTerm(b
, b
), CVC5ApiException
);
619 ASSERT_THROW(p
.iteTerm(x
, b
), CVC5ApiException
);
620 Term zero
= d_solver
.mkInteger(0);
621 ASSERT_THROW(zero
.iteTerm(x
, x
), CVC5ApiException
);
622 ASSERT_THROW(zero
.iteTerm(x
, b
), CVC5ApiException
);
623 Term f_x
= d_solver
.mkTerm(APPLY_UF
, {f
, x
});
624 ASSERT_THROW(f_x
.iteTerm(b
, b
), CVC5ApiException
);
625 ASSERT_THROW(f_x
.iteTerm(b
, x
), CVC5ApiException
);
626 Term sum
= d_solver
.mkTerm(ADD
, {f_x
, f_x
});
627 ASSERT_THROW(sum
.iteTerm(x
, x
), CVC5ApiException
);
628 ASSERT_THROW(sum
.iteTerm(b
, x
), CVC5ApiException
);
629 Term p_0
= d_solver
.mkTerm(APPLY_UF
, {p
, zero
});
630 ASSERT_NO_THROW(p_0
.iteTerm(b
, b
));
631 ASSERT_NO_THROW(p_0
.iteTerm(x
, x
));
632 ASSERT_THROW(p_0
.iteTerm(x
, b
), CVC5ApiException
);
633 Term p_f_x
= d_solver
.mkTerm(APPLY_UF
, {p
, f_x
});
634 ASSERT_NO_THROW(p_f_x
.iteTerm(b
, b
));
635 ASSERT_NO_THROW(p_f_x
.iteTerm(x
, x
));
636 ASSERT_THROW(p_f_x
.iteTerm(x
, b
), CVC5ApiException
);
639 TEST_F(TestApiBlackTerm
, termAssignment
)
641 Term t1
= d_solver
.mkInteger(1);
643 t2
= d_solver
.mkInteger(2);
644 ASSERT_EQ(t1
, d_solver
.mkInteger(1));
647 TEST_F(TestApiBlackTerm
, termCompare
)
649 Term t1
= d_solver
.mkInteger(1);
651 d_solver
.mkTerm(ADD
, {d_solver
.mkInteger(2), d_solver
.mkInteger(2)});
653 d_solver
.mkTerm(ADD
, {d_solver
.mkInteger(2), d_solver
.mkInteger(2)});
654 ASSERT_TRUE(t2
>= t3
);
655 ASSERT_TRUE(t2
<= t3
);
656 ASSERT_TRUE((t1
> t2
) != (t1
< t2
));
657 ASSERT_TRUE((t1
> t2
|| t1
== t2
) == (t1
>= t2
));
660 TEST_F(TestApiBlackTerm
, termChildren
)
663 Term two
= d_solver
.mkInteger(2);
664 Term t1
= d_solver
.mkTerm(ADD
, {two
, d_solver
.mkInteger(3)});
665 ASSERT_EQ(t1
[0], two
);
666 ASSERT_EQ(t1
.getNumChildren(), 2);
668 ASSERT_THROW(tnull
.getNumChildren(), CVC5ApiException
);
671 Sort intSort
= d_solver
.getIntegerSort();
672 Sort fsort
= d_solver
.mkFunctionSort({intSort
}, intSort
);
673 Term f
= d_solver
.mkConst(fsort
, "f");
674 Term t2
= d_solver
.mkTerm(APPLY_UF
, {f
, two
});
675 // due to our higher-order view of terms, we treat f as a child of APPLY_UF
676 ASSERT_EQ(t2
.getNumChildren(), 2);
678 ASSERT_EQ(t2
[1], two
);
679 ASSERT_THROW(tnull
[0], CVC5ApiException
);
682 TEST_F(TestApiBlackTerm
, getInteger
)
684 Term int1
= d_solver
.mkInteger("-18446744073709551616");
685 Term int2
= d_solver
.mkInteger("-18446744073709551615");
686 Term int3
= d_solver
.mkInteger("-4294967296");
687 Term int4
= d_solver
.mkInteger("-4294967295");
688 Term int5
= d_solver
.mkInteger("-10");
689 Term int6
= d_solver
.mkInteger("0");
690 Term int7
= d_solver
.mkInteger("10");
691 Term int8
= d_solver
.mkInteger("4294967295");
692 Term int9
= d_solver
.mkInteger("4294967296");
693 Term int10
= d_solver
.mkInteger("18446744073709551615");
694 Term int11
= d_solver
.mkInteger("18446744073709551616");
695 Term int12
= d_solver
.mkInteger("-0");
697 ASSERT_THROW(d_solver
.mkInteger(""), CVC5ApiException
);
698 ASSERT_THROW(d_solver
.mkInteger("-"), CVC5ApiException
);
699 ASSERT_THROW(d_solver
.mkInteger("-1-"), CVC5ApiException
);
700 ASSERT_THROW(d_solver
.mkInteger("0.0"), CVC5ApiException
);
701 ASSERT_THROW(d_solver
.mkInteger("-0.1"), CVC5ApiException
);
702 ASSERT_THROW(d_solver
.mkInteger("012"), CVC5ApiException
);
703 ASSERT_THROW(d_solver
.mkInteger("0000"), CVC5ApiException
);
704 ASSERT_THROW(d_solver
.mkInteger("-01"), CVC5ApiException
);
705 ASSERT_THROW(d_solver
.mkInteger("-00"), CVC5ApiException
);
707 ASSERT_TRUE(!int1
.isInt32Value() && !int1
.isUInt32Value()
708 && !int1
.isInt64Value() && !int1
.isUInt64Value()
709 && int1
.isIntegerValue());
710 ASSERT_EQ(int1
.getIntegerValue(), "-18446744073709551616");
711 ASSERT_TRUE(int1
.getRealOrIntegerValueSign() == -1);
712 ASSERT_TRUE(!int2
.isInt32Value() && !int2
.isUInt32Value()
713 && !int2
.isInt64Value() && !int2
.isUInt64Value()
714 && int2
.isIntegerValue());
715 ASSERT_EQ(int2
.getIntegerValue(), "-18446744073709551615");
716 ASSERT_TRUE(!int3
.isInt32Value() && !int3
.isUInt32Value()
717 && int3
.isInt64Value() && !int3
.isUInt64Value()
718 && int3
.isIntegerValue());
719 ASSERT_EQ(int3
.getInt64Value(), -4294967296);
720 ASSERT_EQ(int3
.getIntegerValue(), "-4294967296");
721 ASSERT_TRUE(!int4
.isInt32Value() && !int4
.isUInt32Value()
722 && int4
.isInt64Value() && !int4
.isUInt64Value()
723 && int4
.isIntegerValue());
724 ASSERT_EQ(int4
.getInt64Value(), -4294967295);
725 ASSERT_EQ(int4
.getIntegerValue(), "-4294967295");
726 ASSERT_TRUE(int5
.isInt32Value() && !int5
.isUInt32Value()
727 && int5
.isInt64Value() && !int5
.isUInt64Value()
728 && int5
.isIntegerValue());
729 ASSERT_EQ(int5
.getInt32Value(), -10);
730 ASSERT_EQ(int5
.getInt64Value(), -10);
731 ASSERT_EQ(int5
.getIntegerValue(), "-10");
732 ASSERT_TRUE(int6
.isInt32Value() && int6
.isUInt32Value() && int6
.isInt64Value()
733 && int6
.isUInt64Value() && int6
.isIntegerValue());
734 ASSERT_EQ(int6
.getInt32Value(), 0);
735 ASSERT_EQ(int6
.getUInt32Value(), 0);
736 ASSERT_EQ(int6
.getInt64Value(), 0);
737 ASSERT_EQ(int6
.getUInt64Value(), 0);
738 ASSERT_EQ(int6
.getIntegerValue(), "0");
739 ASSERT_TRUE(int6
.getRealOrIntegerValueSign() == 0);
740 ASSERT_TRUE(int7
.isInt32Value() && int7
.isUInt32Value() && int7
.isInt64Value()
741 && int7
.isUInt64Value() && int7
.isIntegerValue());
742 ASSERT_EQ(int7
.getInt32Value(), 10);
743 ASSERT_EQ(int7
.getUInt32Value(), 10);
744 ASSERT_EQ(int7
.getInt64Value(), 10);
745 ASSERT_EQ(int7
.getUInt64Value(), 10);
746 ASSERT_EQ(int7
.getIntegerValue(), "10");
747 ASSERT_TRUE(int7
.getRealOrIntegerValueSign() == 1);
748 ASSERT_TRUE(!int8
.isInt32Value() && int8
.isUInt32Value()
749 && int8
.isInt64Value() && int8
.isUInt64Value()
750 && int8
.isIntegerValue());
751 ASSERT_EQ(int8
.getUInt32Value(), 4294967295);
752 ASSERT_EQ(int8
.getInt64Value(), 4294967295);
753 ASSERT_EQ(int8
.getUInt64Value(), 4294967295);
754 ASSERT_EQ(int8
.getIntegerValue(), "4294967295");
755 ASSERT_TRUE(!int9
.isInt32Value() && !int9
.isUInt32Value()
756 && int9
.isInt64Value() && int9
.isUInt64Value()
757 && int9
.isIntegerValue());
758 ASSERT_EQ(int9
.getInt64Value(), 4294967296);
759 ASSERT_EQ(int9
.getUInt64Value(), 4294967296);
760 ASSERT_EQ(int9
.getIntegerValue(), "4294967296");
761 ASSERT_TRUE(!int10
.isInt32Value() && !int10
.isUInt32Value()
762 && !int10
.isInt64Value() && int10
.isUInt64Value()
763 && int10
.isIntegerValue());
764 ASSERT_EQ(int10
.getUInt64Value(), 18446744073709551615ull);
765 ASSERT_EQ(int10
.getIntegerValue(), "18446744073709551615");
766 ASSERT_TRUE(!int11
.isInt32Value() && !int11
.isUInt32Value()
767 && !int11
.isInt64Value() && !int11
.isUInt64Value()
768 && int11
.isIntegerValue());
769 ASSERT_EQ(int11
.getIntegerValue(), "18446744073709551616");
772 TEST_F(TestApiBlackTerm
, getString
)
774 Term s1
= d_solver
.mkString("abcde");
775 ASSERT_TRUE(s1
.isStringValue());
776 ASSERT_EQ(s1
.getStringValue(), L
"abcde");
779 TEST_F(TestApiBlackTerm
, getReal
)
781 Term real1
= d_solver
.mkReal("0");
782 Term real2
= d_solver
.mkReal(".0");
783 Term real3
= d_solver
.mkReal("-17");
784 Term real4
= d_solver
.mkReal("-3/5");
785 Term real5
= d_solver
.mkReal("12.7");
786 Term real6
= d_solver
.mkReal("1/4294967297");
787 Term real7
= d_solver
.mkReal("4294967297");
788 Term real8
= d_solver
.mkReal("1/18446744073709551617");
789 Term real9
= d_solver
.mkReal("18446744073709551617");
790 Term real10
= d_solver
.mkReal("2343.2343");
792 ASSERT_TRUE(real1
.isRealValue() && real1
.isReal64Value()
793 && real1
.isReal32Value());
794 ASSERT_TRUE(real2
.isRealValue() && real2
.isReal64Value()
795 && real2
.isReal32Value());
796 ASSERT_TRUE(real3
.isRealValue() && real3
.isReal64Value()
797 && real3
.isReal32Value());
798 ASSERT_TRUE(real4
.isRealValue() && real4
.isReal64Value()
799 && real4
.isReal32Value());
800 ASSERT_TRUE(real5
.isRealValue() && real5
.isReal64Value()
801 && real5
.isReal32Value());
802 ASSERT_TRUE(real6
.isRealValue() && real6
.isReal64Value());
803 ASSERT_TRUE(real7
.isRealValue() && real7
.isReal64Value());
804 ASSERT_TRUE(real8
.isRealValue());
805 ASSERT_TRUE(real9
.isRealValue());
806 ASSERT_TRUE(real10
.isRealValue());
808 ASSERT_EQ((std::pair
<int32_t, uint32_t>(0, 1)), real1
.getReal32Value());
809 ASSERT_EQ((std::pair
<int64_t, uint64_t>(0, 1)), real1
.getReal64Value());
810 ASSERT_EQ("0/1", real1
.getRealValue());
812 ASSERT_EQ((std::pair
<int32_t, uint32_t>(0, 1)), real2
.getReal32Value());
813 ASSERT_EQ((std::pair
<int64_t, uint64_t>(0, 1)), real2
.getReal64Value());
814 ASSERT_EQ("0/1", real2
.getRealValue());
816 ASSERT_EQ((std::pair
<int32_t, uint32_t>(-17, 1)), real3
.getReal32Value());
817 ASSERT_EQ((std::pair
<int64_t, uint64_t>(-17, 1)), real3
.getReal64Value());
818 ASSERT_EQ("-17/1", real3
.getRealValue());
820 ASSERT_EQ((std::pair
<int32_t, uint32_t>(-3, 5)), real4
.getReal32Value());
821 ASSERT_EQ((std::pair
<int64_t, uint64_t>(-3, 5)), real4
.getReal64Value());
822 ASSERT_EQ("-3/5", real4
.getRealValue());
824 ASSERT_EQ((std::pair
<int32_t, uint32_t>(127, 10)), real5
.getReal32Value());
825 ASSERT_EQ((std::pair
<int64_t, uint64_t>(127, 10)), real5
.getReal64Value());
826 ASSERT_EQ("127/10", real5
.getRealValue());
828 ASSERT_EQ((std::pair
<int64_t, uint64_t>(1, 4294967297)),
829 real6
.getReal64Value());
830 ASSERT_EQ("1/4294967297", real6
.getRealValue());
832 ASSERT_EQ((std::pair
<int64_t, uint64_t>(4294967297, 1)),
833 real7
.getReal64Value());
834 ASSERT_EQ("4294967297/1", real7
.getRealValue());
836 ASSERT_EQ("1/18446744073709551617", real8
.getRealValue());
838 ASSERT_EQ("18446744073709551617/1", real9
.getRealValue());
840 ASSERT_EQ("23432343/10000", real10
.getRealValue());
843 TEST_F(TestApiBlackTerm
, getConstArrayBase
)
845 Sort intsort
= d_solver
.getIntegerSort();
846 Sort arrsort
= d_solver
.mkArraySort(intsort
, intsort
);
847 Term one
= d_solver
.mkInteger(1);
848 Term constarr
= d_solver
.mkConstArray(arrsort
, one
);
850 ASSERT_TRUE(constarr
.isConstArray());
851 ASSERT_EQ(one
, constarr
.getConstArrayBase());
854 TEST_F(TestApiBlackTerm
, getBoolean
)
856 Term b1
= d_solver
.mkBoolean(true);
857 Term b2
= d_solver
.mkBoolean(false);
859 ASSERT_TRUE(b1
.isBooleanValue());
860 ASSERT_TRUE(b2
.isBooleanValue());
861 ASSERT_TRUE(b1
.getBooleanValue());
862 ASSERT_FALSE(b2
.getBooleanValue());
865 TEST_F(TestApiBlackTerm
, getBitVector
)
867 Term b1
= d_solver
.mkBitVector(8, 15);
868 Term b2
= d_solver
.mkBitVector(8, "00001111", 2);
869 Term b3
= d_solver
.mkBitVector(8, "15", 10);
870 Term b4
= d_solver
.mkBitVector(8, "0f", 16);
871 Term b5
= d_solver
.mkBitVector(9, "00001111", 2);
872 Term b6
= d_solver
.mkBitVector(9, "15", 10);
873 Term b7
= d_solver
.mkBitVector(9, "0f", 16);
875 ASSERT_TRUE(b1
.isBitVectorValue());
876 ASSERT_TRUE(b2
.isBitVectorValue());
877 ASSERT_TRUE(b3
.isBitVectorValue());
878 ASSERT_TRUE(b4
.isBitVectorValue());
879 ASSERT_TRUE(b5
.isBitVectorValue());
880 ASSERT_TRUE(b6
.isBitVectorValue());
881 ASSERT_TRUE(b7
.isBitVectorValue());
883 ASSERT_EQ("00001111", b1
.getBitVectorValue(2));
884 ASSERT_EQ("15", b1
.getBitVectorValue(10));
885 ASSERT_EQ("f", b1
.getBitVectorValue(16));
886 ASSERT_EQ("00001111", b2
.getBitVectorValue(2));
887 ASSERT_EQ("15", b2
.getBitVectorValue(10));
888 ASSERT_EQ("f", b2
.getBitVectorValue(16));
889 ASSERT_EQ("00001111", b3
.getBitVectorValue(2));
890 ASSERT_EQ("15", b3
.getBitVectorValue(10));
891 ASSERT_EQ("f", b3
.getBitVectorValue(16));
892 ASSERT_EQ("00001111", b4
.getBitVectorValue(2));
893 ASSERT_EQ("15", b4
.getBitVectorValue(10));
894 ASSERT_EQ("f", b4
.getBitVectorValue(16));
895 ASSERT_EQ("000001111", b5
.getBitVectorValue(2));
896 ASSERT_EQ("15", b5
.getBitVectorValue(10));
897 ASSERT_EQ("f", b5
.getBitVectorValue(16));
898 ASSERT_EQ("000001111", b6
.getBitVectorValue(2));
899 ASSERT_EQ("15", b6
.getBitVectorValue(10));
900 ASSERT_EQ("f", b6
.getBitVectorValue(16));
901 ASSERT_EQ("000001111", b7
.getBitVectorValue(2));
902 ASSERT_EQ("15", b7
.getBitVectorValue(10));
903 ASSERT_EQ("f", b7
.getBitVectorValue(16));
906 TEST_F(TestApiBlackTerm
, getUninterpretedSortValue
)
908 d_solver
.setOption("produce-models", "true");
909 Sort uSort
= d_solver
.mkUninterpretedSort("u");
910 Term x
= d_solver
.mkConst(uSort
, "x");
911 Term y
= d_solver
.mkConst(uSort
, "y");
912 d_solver
.assertFormula(d_solver
.mkTerm(EQUAL
, {x
, y
}));
913 ASSERT_TRUE(d_solver
.checkSat().isSat());
914 Term vx
= d_solver
.getValue(x
);
915 Term vy
= d_solver
.getValue(y
);
916 ASSERT_TRUE(vx
.isUninterpretedSortValue());
917 ASSERT_TRUE(vy
.isUninterpretedSortValue());
918 ASSERT_EQ(vx
.getUninterpretedSortValue(), vy
.getUninterpretedSortValue());
921 TEST_F(TestApiBlackTerm
, isRoundingModeValue
)
923 ASSERT_FALSE(d_solver
.mkInteger(15).isRoundingModeValue());
924 ASSERT_TRUE(d_solver
.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
)
925 .isRoundingModeValue());
927 d_solver
.mkConst(d_solver
.getRoundingModeSort()).isRoundingModeValue());
930 TEST_F(TestApiBlackTerm
, getRoundingModeValue
)
932 ASSERT_THROW(d_solver
.mkInteger(15).getRoundingModeValue(), CVC5ApiException
);
933 ASSERT_EQ(d_solver
.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
)
934 .getRoundingModeValue(),
935 RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
);
936 ASSERT_EQ(d_solver
.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE
)
937 .getRoundingModeValue(),
938 RoundingMode::ROUND_TOWARD_POSITIVE
);
939 ASSERT_EQ(d_solver
.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE
)
940 .getRoundingModeValue(),
941 RoundingMode::ROUND_TOWARD_NEGATIVE
);
942 ASSERT_EQ(d_solver
.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO
)
943 .getRoundingModeValue(),
944 RoundingMode::ROUND_TOWARD_ZERO
);
945 ASSERT_EQ(d_solver
.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
)
946 .getRoundingModeValue(),
947 RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
);
950 TEST_F(TestApiBlackTerm
, getTuple
)
952 Sort s1
= d_solver
.getIntegerSort();
953 Sort s2
= d_solver
.getRealSort();
954 Sort s3
= d_solver
.getStringSort();
956 Term t1
= d_solver
.mkInteger(15);
957 Term t2
= d_solver
.mkReal(17, 25);
958 Term t3
= d_solver
.mkString("abc");
960 Term tup
= d_solver
.mkTuple({s1
, s2
, s3
}, {t1
, t2
, t3
});
962 ASSERT_TRUE(tup
.isTupleValue());
963 ASSERT_EQ(std::vector
<Term
>({t1
, t2
, t3
}), tup
.getTupleValue());
966 TEST_F(TestApiBlackTerm
, getFloatingPoint
)
968 Term bvval
= d_solver
.mkBitVector(16, "0000110000000011", 2);
969 Term fp
= d_solver
.mkFloatingPoint(5, 11, bvval
);
971 ASSERT_TRUE(fp
.isFloatingPointValue());
972 ASSERT_FALSE(fp
.isFloatingPointPosZero());
973 ASSERT_FALSE(fp
.isFloatingPointNegZero());
974 ASSERT_FALSE(fp
.isFloatingPointPosInf());
975 ASSERT_FALSE(fp
.isFloatingPointNegInf());
976 ASSERT_FALSE(fp
.isFloatingPointNaN());
977 ASSERT_EQ(std::make_tuple(5u, 11u, bvval
), fp
.getFloatingPointValue());
979 ASSERT_TRUE(d_solver
.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero());
980 ASSERT_TRUE(d_solver
.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero());
981 ASSERT_TRUE(d_solver
.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf());
982 ASSERT_TRUE(d_solver
.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf());
983 ASSERT_TRUE(d_solver
.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
986 TEST_F(TestApiBlackTerm
, getSet
)
988 Sort s
= d_solver
.mkSetSort(d_solver
.getIntegerSort());
990 Term i1
= d_solver
.mkInteger(5);
991 Term i2
= d_solver
.mkInteger(7);
993 Term s1
= d_solver
.mkEmptySet(s
);
994 Term s2
= d_solver
.mkTerm(Kind::SET_SINGLETON
, {i1
});
995 Term s3
= d_solver
.mkTerm(Kind::SET_SINGLETON
, {i1
});
996 Term s4
= d_solver
.mkTerm(Kind::SET_SINGLETON
, {i2
});
997 Term s5
= d_solver
.mkTerm(Kind::SET_UNION
,
998 {s2
, d_solver
.mkTerm(Kind::SET_UNION
, {s3
, s4
})});
1000 ASSERT_TRUE(s1
.isSetValue());
1001 ASSERT_TRUE(s2
.isSetValue());
1002 ASSERT_TRUE(s3
.isSetValue());
1003 ASSERT_TRUE(s4
.isSetValue());
1004 ASSERT_FALSE(s5
.isSetValue());
1005 s5
= d_solver
.simplify(s5
);
1006 ASSERT_TRUE(s5
.isSetValue());
1008 ASSERT_EQ(std::set
<Term
>({}), s1
.getSetValue());
1009 ASSERT_EQ(std::set
<Term
>({i1
}), s2
.getSetValue());
1010 ASSERT_EQ(std::set
<Term
>({i1
}), s3
.getSetValue());
1011 ASSERT_EQ(std::set
<Term
>({i2
}), s4
.getSetValue());
1012 ASSERT_EQ(std::set
<Term
>({i1
, i2
}), s5
.getSetValue());
1015 TEST_F(TestApiBlackTerm
, getSequence
)
1017 Sort s
= d_solver
.mkSequenceSort(d_solver
.getIntegerSort());
1019 Term i1
= d_solver
.mkInteger(5);
1020 Term i2
= d_solver
.mkInteger(7);
1022 Term s1
= d_solver
.mkEmptySequence(s
);
1023 Term s2
= d_solver
.mkTerm(Kind::SEQ_UNIT
, {i1
});
1024 Term s3
= d_solver
.mkTerm(Kind::SEQ_UNIT
, {i1
});
1025 Term s4
= d_solver
.mkTerm(Kind::SEQ_UNIT
, {i2
});
1026 Term s5
= d_solver
.mkTerm(Kind::SEQ_CONCAT
,
1027 {s2
, d_solver
.mkTerm(Kind::SEQ_CONCAT
, {s3
, s4
})});
1029 ASSERT_TRUE(s1
.isSequenceValue());
1030 ASSERT_TRUE(!s2
.isSequenceValue());
1031 ASSERT_TRUE(!s3
.isSequenceValue());
1032 ASSERT_TRUE(!s4
.isSequenceValue());
1033 ASSERT_TRUE(!s5
.isSequenceValue());
1035 s2
= d_solver
.simplify(s2
);
1036 s3
= d_solver
.simplify(s3
);
1037 s4
= d_solver
.simplify(s4
);
1038 s5
= d_solver
.simplify(s5
);
1040 ASSERT_EQ(std::vector
<Term
>({}), s1
.getSequenceValue());
1041 ASSERT_EQ(std::vector
<Term
>({i1
}), s2
.getSequenceValue());
1042 ASSERT_EQ(std::vector
<Term
>({i1
}), s3
.getSequenceValue());
1043 ASSERT_EQ(std::vector
<Term
>({i2
}), s4
.getSequenceValue());
1044 ASSERT_EQ(std::vector
<Term
>({i1
, i1
, i2
}), s5
.getSequenceValue());
1047 TEST_F(TestApiBlackTerm
, substitute
)
1049 Term x
= d_solver
.mkConst(d_solver
.getIntegerSort(), "x");
1050 Term one
= d_solver
.mkInteger(1);
1051 Term ttrue
= d_solver
.mkTrue();
1052 Term xpx
= d_solver
.mkTerm(ADD
, {x
, x
});
1053 Term onepone
= d_solver
.mkTerm(ADD
, {one
, one
});
1055 ASSERT_EQ(xpx
.substitute(x
, one
), onepone
);
1056 ASSERT_EQ(onepone
.substitute(one
, x
), xpx
);
1057 // incorrect due to type
1058 ASSERT_THROW(xpx
.substitute(one
, ttrue
), CVC5ApiException
);
1060 // simultaneous substitution
1061 Term y
= d_solver
.mkConst(d_solver
.getIntegerSort(), "y");
1062 Term xpy
= d_solver
.mkTerm(ADD
, {x
, y
});
1063 Term xpone
= d_solver
.mkTerm(ADD
, {y
, one
});
1064 std::vector
<Term
> es
;
1065 std::vector
<Term
> rs
;
1070 ASSERT_EQ(xpy
.substitute(es
, rs
), xpone
);
1072 // incorrect substitution due to arity
1074 ASSERT_THROW(xpy
.substitute(es
, rs
), CVC5ApiException
);
1076 // incorrect substitution due to types
1077 rs
.push_back(ttrue
);
1078 ASSERT_THROW(xpy
.substitute(es
, rs
), CVC5ApiException
);
1080 // null cannot substitute
1082 ASSERT_THROW(tnull
.substitute(one
, x
), CVC5ApiException
);
1083 ASSERT_THROW(xpx
.substitute(tnull
, x
), CVC5ApiException
);
1084 ASSERT_THROW(xpx
.substitute(x
, tnull
), CVC5ApiException
);
1086 rs
.push_back(tnull
);
1087 ASSERT_THROW(xpy
.substitute(es
, rs
), CVC5ApiException
);
1092 ASSERT_THROW(tnull
.substitute(es
, rs
), CVC5ApiException
);
1093 es
.push_back(tnull
);
1095 ASSERT_THROW(xpx
.substitute(es
, rs
), CVC5ApiException
);
1098 TEST_F(TestApiBlackTerm
, constArray
)
1100 Sort intsort
= d_solver
.getIntegerSort();
1101 Sort arrsort
= d_solver
.mkArraySort(intsort
, intsort
);
1102 Term a
= d_solver
.mkConst(arrsort
, "a");
1103 Term one
= d_solver
.mkInteger(1);
1104 Term constarr
= d_solver
.mkConstArray(arrsort
, one
);
1106 ASSERT_EQ(constarr
.getKind(), CONST_ARRAY
);
1107 ASSERT_EQ(constarr
.getConstArrayBase(), one
);
1108 ASSERT_THROW(a
.getConstArrayBase(), CVC5ApiException
);
1111 d_solver
.mkArraySort(d_solver
.getRealSort(), d_solver
.getRealSort());
1112 Term zero_array
= d_solver
.mkConstArray(arrsort
, d_solver
.mkReal(0));
1113 Term stores
= d_solver
.mkTerm(
1114 STORE
, {zero_array
, d_solver
.mkReal(1), d_solver
.mkReal(2)});
1116 d_solver
.mkTerm(STORE
, {stores
, d_solver
.mkReal(2), d_solver
.mkReal(3)});
1118 d_solver
.mkTerm(STORE
, {stores
, d_solver
.mkReal(4), d_solver
.mkReal(5)});
1121 TEST_F(TestApiBlackTerm
, getSequenceValue
)
1123 Sort realsort
= d_solver
.getRealSort();
1124 Sort seqsort
= d_solver
.mkSequenceSort(realsort
);
1125 Term s
= d_solver
.mkEmptySequence(seqsort
);
1127 ASSERT_EQ(s
.getKind(), CONST_SEQUENCE
);
1128 // empty sequence has zero elements
1129 std::vector
<Term
> cs
= s
.getSequenceValue();
1130 ASSERT_TRUE(cs
.empty());
1132 // A seq.unit app is not a constant sequence (regardless of whether it is
1133 // applied to a constant).
1134 Term su
= d_solver
.mkTerm(SEQ_UNIT
, {d_solver
.mkReal(1)});
1135 ASSERT_THROW(su
.getSequenceValue(), CVC5ApiException
);
1138 TEST_F(TestApiBlackTerm
, getCardinalityConstraint
)
1140 Sort su
= d_solver
.mkUninterpretedSort("u");
1141 Term t
= d_solver
.mkCardinalityConstraint(su
, 3);
1142 ASSERT_TRUE(t
.isCardinalityConstraint());
1143 std::pair
<Sort
, uint32_t> cc
= t
.getCardinalityConstraint();
1144 ASSERT_EQ(cc
.first
, su
);
1145 ASSERT_EQ(cc
.second
, 3);
1146 Term x
= d_solver
.mkConst(d_solver
.getIntegerSort(), "x");
1147 ASSERT_FALSE(x
.isCardinalityConstraint());
1148 ASSERT_THROW(x
.getCardinalityConstraint(), CVC5ApiException
);
1150 ASSERT_THROW(nullt
.isCardinalityConstraint(), CVC5ApiException
);
1153 TEST_F(TestApiBlackTerm
, termScopedToString
)
1155 Sort intsort
= d_solver
.getIntegerSort();
1156 Term x
= d_solver
.mkConst(intsort
, "x");
1157 ASSERT_EQ(x
.toString(), "x");
1159 ASSERT_EQ(x
.toString(), "x");
1162 TEST_F(TestApiBlackTerm
, toString
) { ASSERT_NO_THROW(Term().toString()); }
1164 } // namespace cvc5::internal