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