GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/term_black.cpp Lines: 699 699 100.0 %
Date: 2021-03-22 Branches: 2924 9160 31.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Makai Mann, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of the Term class.
13
 **/
14
15
#include "test_api.h"
16
17
namespace CVC4 {
18
19
using namespace api;
20
21
namespace test {
22
23
88
class TestApiBlackTerm : public TestApi
24
{
25
};
26
27
31
TEST_F(TestApiBlackTerm, eq)
28
{
29
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
30
4
  Term x = d_solver.mkVar(uSort, "x");
31
4
  Term y = d_solver.mkVar(uSort, "y");
32
4
  Term z;
33
34
2
  ASSERT_TRUE(x == x);
35
2
  ASSERT_FALSE(x != x);
36
2
  ASSERT_FALSE(x == y);
37
2
  ASSERT_TRUE(x != y);
38
2
  ASSERT_FALSE((x == z));
39
2
  ASSERT_TRUE(x != z);
40
}
41
42
31
TEST_F(TestApiBlackTerm, getId)
43
{
44
4
  Term n;
45
4
  ASSERT_THROW(n.getId(), CVC4ApiException);
46
4
  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
47
2
  ASSERT_NO_THROW(x.getId());
48
4
  Term y = x;
49
2
  ASSERT_EQ(x.getId(), y.getId());
50
51
4
  Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
52
2
  ASSERT_NE(x.getId(), z.getId());
53
}
54
55
31
TEST_F(TestApiBlackTerm, getKind)
56
{
57
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
58
4
  Sort intSort = d_solver.getIntegerSort();
59
4
  Sort boolSort = d_solver.getBooleanSort();
60
4
  Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
61
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
62
63
4
  Term n;
64
4
  ASSERT_THROW(n.getKind(), CVC4ApiException);
65
4
  Term x = d_solver.mkVar(uSort, "x");
66
2
  ASSERT_NO_THROW(x.getKind());
67
4
  Term y = d_solver.mkVar(uSort, "y");
68
2
  ASSERT_NO_THROW(y.getKind());
69
70
4
  Term f = d_solver.mkVar(funSort1, "f");
71
2
  ASSERT_NO_THROW(f.getKind());
72
4
  Term p = d_solver.mkVar(funSort2, "p");
73
2
  ASSERT_NO_THROW(p.getKind());
74
75
4
  Term zero = d_solver.mkInteger(0);
76
2
  ASSERT_NO_THROW(zero.getKind());
77
78
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
79
2
  ASSERT_NO_THROW(f_x.getKind());
80
4
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
81
2
  ASSERT_NO_THROW(f_y.getKind());
82
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
83
2
  ASSERT_NO_THROW(sum.getKind());
84
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
85
2
  ASSERT_NO_THROW(p_0.getKind());
86
4
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
87
2
  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
4
  Sort seqSort = d_solver.mkSequenceSort(intSort);
92
4
  Term s = d_solver.mkConst(seqSort, "s");
93
4
  Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
94
2
  ASSERT_EQ(ss.getKind(), SEQ_CONCAT);
95
}
96
97
31
TEST_F(TestApiBlackTerm, getSort)
98
{
99
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
100
4
  Sort intSort = d_solver.getIntegerSort();
101
4
  Sort boolSort = d_solver.getBooleanSort();
102
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
103
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
104
105
4
  Term n;
106
4
  ASSERT_THROW(n.getSort(), CVC4ApiException);
107
4
  Term x = d_solver.mkVar(bvSort, "x");
108
2
  ASSERT_NO_THROW(x.getSort());
109
2
  ASSERT_EQ(x.getSort(), bvSort);
110
4
  Term y = d_solver.mkVar(bvSort, "y");
111
2
  ASSERT_NO_THROW(y.getSort());
112
2
  ASSERT_EQ(y.getSort(), bvSort);
113
114
4
  Term f = d_solver.mkVar(funSort1, "f");
115
2
  ASSERT_NO_THROW(f.getSort());
116
2
  ASSERT_EQ(f.getSort(), funSort1);
117
4
  Term p = d_solver.mkVar(funSort2, "p");
118
2
  ASSERT_NO_THROW(p.getSort());
119
2
  ASSERT_EQ(p.getSort(), funSort2);
120
121
4
  Term zero = d_solver.mkInteger(0);
122
2
  ASSERT_NO_THROW(zero.getSort());
123
2
  ASSERT_EQ(zero.getSort(), intSort);
124
125
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
126
2
  ASSERT_NO_THROW(f_x.getSort());
127
2
  ASSERT_EQ(f_x.getSort(), intSort);
128
4
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
129
2
  ASSERT_NO_THROW(f_y.getSort());
130
2
  ASSERT_EQ(f_y.getSort(), intSort);
131
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
132
2
  ASSERT_NO_THROW(sum.getSort());
133
2
  ASSERT_EQ(sum.getSort(), intSort);
134
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
135
2
  ASSERT_NO_THROW(p_0.getSort());
136
2
  ASSERT_EQ(p_0.getSort(), boolSort);
137
4
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
138
2
  ASSERT_NO_THROW(p_f_y.getSort());
139
2
  ASSERT_EQ(p_f_y.getSort(), boolSort);
140
}
141
142
31
TEST_F(TestApiBlackTerm, getOp)
143
{
144
4
  Sort intsort = d_solver.getIntegerSort();
145
4
  Sort bvsort = d_solver.mkBitVectorSort(8);
146
4
  Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
147
4
  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
148
149
4
  Term x = d_solver.mkConst(intsort, "x");
150
4
  Term a = d_solver.mkConst(arrsort, "a");
151
4
  Term b = d_solver.mkConst(bvsort, "b");
152
153
2
  ASSERT_FALSE(x.hasOp());
154
4
  ASSERT_THROW(x.getOp(), CVC4ApiException);
155
156
4
  Term ab = d_solver.mkTerm(SELECT, a, b);
157
4
  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
158
4
  Term extb = d_solver.mkTerm(ext, b);
159
160
2
  ASSERT_TRUE(ab.hasOp());
161
2
  ASSERT_FALSE(ab.getOp().isIndexed());
162
  // can compare directly to a Kind (will invoke Op constructor)
163
2
  ASSERT_TRUE(extb.hasOp());
164
2
  ASSERT_TRUE(extb.getOp().isIndexed());
165
2
  ASSERT_EQ(extb.getOp(), ext);
166
167
4
  Term f = d_solver.mkConst(funsort, "f");
168
4
  Term fx = d_solver.mkTerm(APPLY_UF, f, x);
169
170
2
  ASSERT_FALSE(f.hasOp());
171
4
  ASSERT_THROW(f.getOp(), CVC4ApiException);
172
2
  ASSERT_TRUE(fx.hasOp());
173
4
  std::vector<Term> children(fx.begin(), fx.end());
174
  // testing rebuild from op and children
175
2
  ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
176
177
  // Test Datatypes Ops
178
4
  Sort sort = d_solver.mkParamSort("T");
179
4
  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
180
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
181
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
182
2
  cons.addSelector("head", sort);
183
2
  cons.addSelectorSelf("tail");
184
2
  listDecl.addConstructor(cons);
185
2
  listDecl.addConstructor(nil);
186
4
  Sort listSort = d_solver.mkDatatypeSort(listDecl);
187
  Sort intListSort =
188
4
      listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
189
4
  Term c = d_solver.mkConst(intListSort, "c");
190
4
  Datatype list = listSort.getDatatype();
191
  // list datatype constructor and selector operator terms
192
4
  Term consOpTerm = list.getConstructorTerm("cons");
193
4
  Term nilOpTerm = list.getConstructorTerm("nil");
194
4
  Term headOpTerm = list["cons"].getSelectorTerm("head");
195
4
  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
196
197
4
  Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
198
  Term consTerm = d_solver.mkTerm(
199
4
      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
200
4
  Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
201
4
  Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
202
203
2
  ASSERT_TRUE(nilTerm.hasOp());
204
2
  ASSERT_TRUE(consTerm.hasOp());
205
2
  ASSERT_TRUE(headTerm.hasOp());
206
2
  ASSERT_TRUE(tailTerm.hasOp());
207
208
  // Test rebuilding
209
2
  children.clear();
210
2
  children.insert(children.begin(), headTerm.begin(), headTerm.end());
211
2
  ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
212
}
213
214
31
TEST_F(TestApiBlackTerm, isNull)
215
{
216
4
  Term x;
217
2
  ASSERT_TRUE(x.isNull());
218
2
  x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
219
2
  ASSERT_FALSE(x.isNull());
220
}
221
222
31
TEST_F(TestApiBlackTerm, notTerm)
223
{
224
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
225
4
  Sort intSort = d_solver.getIntegerSort();
226
4
  Sort boolSort = d_solver.getBooleanSort();
227
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
228
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
229
230
4
  ASSERT_THROW(Term().notTerm(), CVC4ApiException);
231
4
  Term b = d_solver.mkTrue();
232
2
  ASSERT_NO_THROW(b.notTerm());
233
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
234
4
  ASSERT_THROW(x.notTerm(), CVC4ApiException);
235
4
  Term f = d_solver.mkVar(funSort1, "f");
236
4
  ASSERT_THROW(f.notTerm(), CVC4ApiException);
237
4
  Term p = d_solver.mkVar(funSort2, "p");
238
4
  ASSERT_THROW(p.notTerm(), CVC4ApiException);
239
4
  Term zero = d_solver.mkInteger(0);
240
4
  ASSERT_THROW(zero.notTerm(), CVC4ApiException);
241
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
242
4
  ASSERT_THROW(f_x.notTerm(), CVC4ApiException);
243
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
244
4
  ASSERT_THROW(sum.notTerm(), CVC4ApiException);
245
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
246
2
  ASSERT_NO_THROW(p_0.notTerm());
247
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
248
2
  ASSERT_NO_THROW(p_f_x.notTerm());
249
}
250
251
31
TEST_F(TestApiBlackTerm, andTerm)
252
{
253
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
254
4
  Sort intSort = d_solver.getIntegerSort();
255
4
  Sort boolSort = d_solver.getBooleanSort();
256
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
257
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
258
259
4
  Term b = d_solver.mkTrue();
260
4
  ASSERT_THROW(Term().andTerm(b), CVC4ApiException);
261
4
  ASSERT_THROW(b.andTerm(Term()), CVC4ApiException);
262
2
  ASSERT_NO_THROW(b.andTerm(b));
263
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
264
4
  ASSERT_THROW(x.andTerm(b), CVC4ApiException);
265
4
  ASSERT_THROW(x.andTerm(x), CVC4ApiException);
266
4
  Term f = d_solver.mkVar(funSort1, "f");
267
4
  ASSERT_THROW(f.andTerm(b), CVC4ApiException);
268
4
  ASSERT_THROW(f.andTerm(x), CVC4ApiException);
269
4
  ASSERT_THROW(f.andTerm(f), CVC4ApiException);
270
4
  Term p = d_solver.mkVar(funSort2, "p");
271
4
  ASSERT_THROW(p.andTerm(b), CVC4ApiException);
272
4
  ASSERT_THROW(p.andTerm(x), CVC4ApiException);
273
4
  ASSERT_THROW(p.andTerm(f), CVC4ApiException);
274
4
  ASSERT_THROW(p.andTerm(p), CVC4ApiException);
275
4
  Term zero = d_solver.mkInteger(0);
276
4
  ASSERT_THROW(zero.andTerm(b), CVC4ApiException);
277
4
  ASSERT_THROW(zero.andTerm(x), CVC4ApiException);
278
4
  ASSERT_THROW(zero.andTerm(f), CVC4ApiException);
279
4
  ASSERT_THROW(zero.andTerm(p), CVC4ApiException);
280
4
  ASSERT_THROW(zero.andTerm(zero), CVC4ApiException);
281
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
282
4
  ASSERT_THROW(f_x.andTerm(b), CVC4ApiException);
283
4
  ASSERT_THROW(f_x.andTerm(x), CVC4ApiException);
284
4
  ASSERT_THROW(f_x.andTerm(f), CVC4ApiException);
285
4
  ASSERT_THROW(f_x.andTerm(p), CVC4ApiException);
286
4
  ASSERT_THROW(f_x.andTerm(zero), CVC4ApiException);
287
4
  ASSERT_THROW(f_x.andTerm(f_x), CVC4ApiException);
288
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
289
4
  ASSERT_THROW(sum.andTerm(b), CVC4ApiException);
290
4
  ASSERT_THROW(sum.andTerm(x), CVC4ApiException);
291
4
  ASSERT_THROW(sum.andTerm(f), CVC4ApiException);
292
4
  ASSERT_THROW(sum.andTerm(p), CVC4ApiException);
293
4
  ASSERT_THROW(sum.andTerm(zero), CVC4ApiException);
294
4
  ASSERT_THROW(sum.andTerm(f_x), CVC4ApiException);
295
4
  ASSERT_THROW(sum.andTerm(sum), CVC4ApiException);
296
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
297
2
  ASSERT_NO_THROW(p_0.andTerm(b));
298
4
  ASSERT_THROW(p_0.andTerm(x), CVC4ApiException);
299
4
  ASSERT_THROW(p_0.andTerm(f), CVC4ApiException);
300
4
  ASSERT_THROW(p_0.andTerm(p), CVC4ApiException);
301
4
  ASSERT_THROW(p_0.andTerm(zero), CVC4ApiException);
302
4
  ASSERT_THROW(p_0.andTerm(f_x), CVC4ApiException);
303
4
  ASSERT_THROW(p_0.andTerm(sum), CVC4ApiException);
304
2
  ASSERT_NO_THROW(p_0.andTerm(p_0));
305
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
306
2
  ASSERT_NO_THROW(p_f_x.andTerm(b));
307
4
  ASSERT_THROW(p_f_x.andTerm(x), CVC4ApiException);
308
4
  ASSERT_THROW(p_f_x.andTerm(f), CVC4ApiException);
309
4
  ASSERT_THROW(p_f_x.andTerm(p), CVC4ApiException);
310
4
  ASSERT_THROW(p_f_x.andTerm(zero), CVC4ApiException);
311
4
  ASSERT_THROW(p_f_x.andTerm(f_x), CVC4ApiException);
312
4
  ASSERT_THROW(p_f_x.andTerm(sum), CVC4ApiException);
313
2
  ASSERT_NO_THROW(p_f_x.andTerm(p_0));
314
2
  ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
315
}
316
317
31
TEST_F(TestApiBlackTerm, orTerm)
318
{
319
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
320
4
  Sort intSort = d_solver.getIntegerSort();
321
4
  Sort boolSort = d_solver.getBooleanSort();
322
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
323
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
324
325
4
  Term b = d_solver.mkTrue();
326
4
  ASSERT_THROW(Term().orTerm(b), CVC4ApiException);
327
4
  ASSERT_THROW(b.orTerm(Term()), CVC4ApiException);
328
2
  ASSERT_NO_THROW(b.orTerm(b));
329
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
330
4
  ASSERT_THROW(x.orTerm(b), CVC4ApiException);
331
4
  ASSERT_THROW(x.orTerm(x), CVC4ApiException);
332
4
  Term f = d_solver.mkVar(funSort1, "f");
333
4
  ASSERT_THROW(f.orTerm(b), CVC4ApiException);
334
4
  ASSERT_THROW(f.orTerm(x), CVC4ApiException);
335
4
  ASSERT_THROW(f.orTerm(f), CVC4ApiException);
336
4
  Term p = d_solver.mkVar(funSort2, "p");
337
4
  ASSERT_THROW(p.orTerm(b), CVC4ApiException);
338
4
  ASSERT_THROW(p.orTerm(x), CVC4ApiException);
339
4
  ASSERT_THROW(p.orTerm(f), CVC4ApiException);
340
4
  ASSERT_THROW(p.orTerm(p), CVC4ApiException);
341
4
  Term zero = d_solver.mkInteger(0);
342
4
  ASSERT_THROW(zero.orTerm(b), CVC4ApiException);
343
4
  ASSERT_THROW(zero.orTerm(x), CVC4ApiException);
344
4
  ASSERT_THROW(zero.orTerm(f), CVC4ApiException);
345
4
  ASSERT_THROW(zero.orTerm(p), CVC4ApiException);
346
4
  ASSERT_THROW(zero.orTerm(zero), CVC4ApiException);
347
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
348
4
  ASSERT_THROW(f_x.orTerm(b), CVC4ApiException);
349
4
  ASSERT_THROW(f_x.orTerm(x), CVC4ApiException);
350
4
  ASSERT_THROW(f_x.orTerm(f), CVC4ApiException);
351
4
  ASSERT_THROW(f_x.orTerm(p), CVC4ApiException);
352
4
  ASSERT_THROW(f_x.orTerm(zero), CVC4ApiException);
353
4
  ASSERT_THROW(f_x.orTerm(f_x), CVC4ApiException);
354
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
355
4
  ASSERT_THROW(sum.orTerm(b), CVC4ApiException);
356
4
  ASSERT_THROW(sum.orTerm(x), CVC4ApiException);
357
4
  ASSERT_THROW(sum.orTerm(f), CVC4ApiException);
358
4
  ASSERT_THROW(sum.orTerm(p), CVC4ApiException);
359
4
  ASSERT_THROW(sum.orTerm(zero), CVC4ApiException);
360
4
  ASSERT_THROW(sum.orTerm(f_x), CVC4ApiException);
361
4
  ASSERT_THROW(sum.orTerm(sum), CVC4ApiException);
362
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
363
2
  ASSERT_NO_THROW(p_0.orTerm(b));
364
4
  ASSERT_THROW(p_0.orTerm(x), CVC4ApiException);
365
4
  ASSERT_THROW(p_0.orTerm(f), CVC4ApiException);
366
4
  ASSERT_THROW(p_0.orTerm(p), CVC4ApiException);
367
4
  ASSERT_THROW(p_0.orTerm(zero), CVC4ApiException);
368
4
  ASSERT_THROW(p_0.orTerm(f_x), CVC4ApiException);
369
4
  ASSERT_THROW(p_0.orTerm(sum), CVC4ApiException);
370
2
  ASSERT_NO_THROW(p_0.orTerm(p_0));
371
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
372
2
  ASSERT_NO_THROW(p_f_x.orTerm(b));
373
4
  ASSERT_THROW(p_f_x.orTerm(x), CVC4ApiException);
374
4
  ASSERT_THROW(p_f_x.orTerm(f), CVC4ApiException);
375
4
  ASSERT_THROW(p_f_x.orTerm(p), CVC4ApiException);
376
4
  ASSERT_THROW(p_f_x.orTerm(zero), CVC4ApiException);
377
4
  ASSERT_THROW(p_f_x.orTerm(f_x), CVC4ApiException);
378
4
  ASSERT_THROW(p_f_x.orTerm(sum), CVC4ApiException);
379
2
  ASSERT_NO_THROW(p_f_x.orTerm(p_0));
380
2
  ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
381
}
382
383
31
TEST_F(TestApiBlackTerm, xorTerm)
384
{
385
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
386
4
  Sort intSort = d_solver.getIntegerSort();
387
4
  Sort boolSort = d_solver.getBooleanSort();
388
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
389
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
390
391
4
  Term b = d_solver.mkTrue();
392
4
  ASSERT_THROW(Term().xorTerm(b), CVC4ApiException);
393
4
  ASSERT_THROW(b.xorTerm(Term()), CVC4ApiException);
394
2
  ASSERT_NO_THROW(b.xorTerm(b));
395
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
396
4
  ASSERT_THROW(x.xorTerm(b), CVC4ApiException);
397
4
  ASSERT_THROW(x.xorTerm(x), CVC4ApiException);
398
4
  Term f = d_solver.mkVar(funSort1, "f");
399
4
  ASSERT_THROW(f.xorTerm(b), CVC4ApiException);
400
4
  ASSERT_THROW(f.xorTerm(x), CVC4ApiException);
401
4
  ASSERT_THROW(f.xorTerm(f), CVC4ApiException);
402
4
  Term p = d_solver.mkVar(funSort2, "p");
403
4
  ASSERT_THROW(p.xorTerm(b), CVC4ApiException);
404
4
  ASSERT_THROW(p.xorTerm(x), CVC4ApiException);
405
4
  ASSERT_THROW(p.xorTerm(f), CVC4ApiException);
406
4
  ASSERT_THROW(p.xorTerm(p), CVC4ApiException);
407
4
  Term zero = d_solver.mkInteger(0);
408
4
  ASSERT_THROW(zero.xorTerm(b), CVC4ApiException);
409
4
  ASSERT_THROW(zero.xorTerm(x), CVC4ApiException);
410
4
  ASSERT_THROW(zero.xorTerm(f), CVC4ApiException);
411
4
  ASSERT_THROW(zero.xorTerm(p), CVC4ApiException);
412
4
  ASSERT_THROW(zero.xorTerm(zero), CVC4ApiException);
413
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
414
4
  ASSERT_THROW(f_x.xorTerm(b), CVC4ApiException);
415
4
  ASSERT_THROW(f_x.xorTerm(x), CVC4ApiException);
416
4
  ASSERT_THROW(f_x.xorTerm(f), CVC4ApiException);
417
4
  ASSERT_THROW(f_x.xorTerm(p), CVC4ApiException);
418
4
  ASSERT_THROW(f_x.xorTerm(zero), CVC4ApiException);
419
4
  ASSERT_THROW(f_x.xorTerm(f_x), CVC4ApiException);
420
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
421
4
  ASSERT_THROW(sum.xorTerm(b), CVC4ApiException);
422
4
  ASSERT_THROW(sum.xorTerm(x), CVC4ApiException);
423
4
  ASSERT_THROW(sum.xorTerm(f), CVC4ApiException);
424
4
  ASSERT_THROW(sum.xorTerm(p), CVC4ApiException);
425
4
  ASSERT_THROW(sum.xorTerm(zero), CVC4ApiException);
426
4
  ASSERT_THROW(sum.xorTerm(f_x), CVC4ApiException);
427
4
  ASSERT_THROW(sum.xorTerm(sum), CVC4ApiException);
428
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
429
2
  ASSERT_NO_THROW(p_0.xorTerm(b));
430
4
  ASSERT_THROW(p_0.xorTerm(x), CVC4ApiException);
431
4
  ASSERT_THROW(p_0.xorTerm(f), CVC4ApiException);
432
4
  ASSERT_THROW(p_0.xorTerm(p), CVC4ApiException);
433
4
  ASSERT_THROW(p_0.xorTerm(zero), CVC4ApiException);
434
4
  ASSERT_THROW(p_0.xorTerm(f_x), CVC4ApiException);
435
4
  ASSERT_THROW(p_0.xorTerm(sum), CVC4ApiException);
436
2
  ASSERT_NO_THROW(p_0.xorTerm(p_0));
437
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
438
2
  ASSERT_NO_THROW(p_f_x.xorTerm(b));
439
4
  ASSERT_THROW(p_f_x.xorTerm(x), CVC4ApiException);
440
4
  ASSERT_THROW(p_f_x.xorTerm(f), CVC4ApiException);
441
4
  ASSERT_THROW(p_f_x.xorTerm(p), CVC4ApiException);
442
4
  ASSERT_THROW(p_f_x.xorTerm(zero), CVC4ApiException);
443
4
  ASSERT_THROW(p_f_x.xorTerm(f_x), CVC4ApiException);
444
4
  ASSERT_THROW(p_f_x.xorTerm(sum), CVC4ApiException);
445
2
  ASSERT_NO_THROW(p_f_x.xorTerm(p_0));
446
2
  ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
447
}
448
449
31
TEST_F(TestApiBlackTerm, eqTerm)
450
{
451
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
452
4
  Sort intSort = d_solver.getIntegerSort();
453
4
  Sort boolSort = d_solver.getBooleanSort();
454
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
455
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
456
457
4
  Term b = d_solver.mkTrue();
458
4
  ASSERT_THROW(Term().eqTerm(b), CVC4ApiException);
459
4
  ASSERT_THROW(b.eqTerm(Term()), CVC4ApiException);
460
2
  ASSERT_NO_THROW(b.eqTerm(b));
461
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
462
4
  ASSERT_THROW(x.eqTerm(b), CVC4ApiException);
463
2
  ASSERT_NO_THROW(x.eqTerm(x));
464
4
  Term f = d_solver.mkVar(funSort1, "f");
465
4
  ASSERT_THROW(f.eqTerm(b), CVC4ApiException);
466
4
  ASSERT_THROW(f.eqTerm(x), CVC4ApiException);
467
2
  ASSERT_NO_THROW(f.eqTerm(f));
468
4
  Term p = d_solver.mkVar(funSort2, "p");
469
4
  ASSERT_THROW(p.eqTerm(b), CVC4ApiException);
470
4
  ASSERT_THROW(p.eqTerm(x), CVC4ApiException);
471
4
  ASSERT_THROW(p.eqTerm(f), CVC4ApiException);
472
2
  ASSERT_NO_THROW(p.eqTerm(p));
473
4
  Term zero = d_solver.mkInteger(0);
474
4
  ASSERT_THROW(zero.eqTerm(b), CVC4ApiException);
475
4
  ASSERT_THROW(zero.eqTerm(x), CVC4ApiException);
476
4
  ASSERT_THROW(zero.eqTerm(f), CVC4ApiException);
477
4
  ASSERT_THROW(zero.eqTerm(p), CVC4ApiException);
478
2
  ASSERT_NO_THROW(zero.eqTerm(zero));
479
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
480
4
  ASSERT_THROW(f_x.eqTerm(b), CVC4ApiException);
481
4
  ASSERT_THROW(f_x.eqTerm(x), CVC4ApiException);
482
4
  ASSERT_THROW(f_x.eqTerm(f), CVC4ApiException);
483
4
  ASSERT_THROW(f_x.eqTerm(p), CVC4ApiException);
484
2
  ASSERT_NO_THROW(f_x.eqTerm(zero));
485
2
  ASSERT_NO_THROW(f_x.eqTerm(f_x));
486
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
487
4
  ASSERT_THROW(sum.eqTerm(b), CVC4ApiException);
488
4
  ASSERT_THROW(sum.eqTerm(x), CVC4ApiException);
489
4
  ASSERT_THROW(sum.eqTerm(f), CVC4ApiException);
490
4
  ASSERT_THROW(sum.eqTerm(p), CVC4ApiException);
491
2
  ASSERT_NO_THROW(sum.eqTerm(zero));
492
2
  ASSERT_NO_THROW(sum.eqTerm(f_x));
493
2
  ASSERT_NO_THROW(sum.eqTerm(sum));
494
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
495
2
  ASSERT_NO_THROW(p_0.eqTerm(b));
496
4
  ASSERT_THROW(p_0.eqTerm(x), CVC4ApiException);
497
4
  ASSERT_THROW(p_0.eqTerm(f), CVC4ApiException);
498
4
  ASSERT_THROW(p_0.eqTerm(p), CVC4ApiException);
499
4
  ASSERT_THROW(p_0.eqTerm(zero), CVC4ApiException);
500
4
  ASSERT_THROW(p_0.eqTerm(f_x), CVC4ApiException);
501
4
  ASSERT_THROW(p_0.eqTerm(sum), CVC4ApiException);
502
2
  ASSERT_NO_THROW(p_0.eqTerm(p_0));
503
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
504
2
  ASSERT_NO_THROW(p_f_x.eqTerm(b));
505
4
  ASSERT_THROW(p_f_x.eqTerm(x), CVC4ApiException);
506
4
  ASSERT_THROW(p_f_x.eqTerm(f), CVC4ApiException);
507
4
  ASSERT_THROW(p_f_x.eqTerm(p), CVC4ApiException);
508
4
  ASSERT_THROW(p_f_x.eqTerm(zero), CVC4ApiException);
509
4
  ASSERT_THROW(p_f_x.eqTerm(f_x), CVC4ApiException);
510
4
  ASSERT_THROW(p_f_x.eqTerm(sum), CVC4ApiException);
511
2
  ASSERT_NO_THROW(p_f_x.eqTerm(p_0));
512
2
  ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
513
}
514
515
31
TEST_F(TestApiBlackTerm, impTerm)
516
{
517
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
518
4
  Sort intSort = d_solver.getIntegerSort();
519
4
  Sort boolSort = d_solver.getBooleanSort();
520
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
521
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
522
523
4
  Term b = d_solver.mkTrue();
524
4
  ASSERT_THROW(Term().impTerm(b), CVC4ApiException);
525
4
  ASSERT_THROW(b.impTerm(Term()), CVC4ApiException);
526
2
  ASSERT_NO_THROW(b.impTerm(b));
527
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
528
4
  ASSERT_THROW(x.impTerm(b), CVC4ApiException);
529
4
  ASSERT_THROW(x.impTerm(x), CVC4ApiException);
530
4
  Term f = d_solver.mkVar(funSort1, "f");
531
4
  ASSERT_THROW(f.impTerm(b), CVC4ApiException);
532
4
  ASSERT_THROW(f.impTerm(x), CVC4ApiException);
533
4
  ASSERT_THROW(f.impTerm(f), CVC4ApiException);
534
4
  Term p = d_solver.mkVar(funSort2, "p");
535
4
  ASSERT_THROW(p.impTerm(b), CVC4ApiException);
536
4
  ASSERT_THROW(p.impTerm(x), CVC4ApiException);
537
4
  ASSERT_THROW(p.impTerm(f), CVC4ApiException);
538
4
  ASSERT_THROW(p.impTerm(p), CVC4ApiException);
539
4
  Term zero = d_solver.mkInteger(0);
540
4
  ASSERT_THROW(zero.impTerm(b), CVC4ApiException);
541
4
  ASSERT_THROW(zero.impTerm(x), CVC4ApiException);
542
4
  ASSERT_THROW(zero.impTerm(f), CVC4ApiException);
543
4
  ASSERT_THROW(zero.impTerm(p), CVC4ApiException);
544
4
  ASSERT_THROW(zero.impTerm(zero), CVC4ApiException);
545
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
546
4
  ASSERT_THROW(f_x.impTerm(b), CVC4ApiException);
547
4
  ASSERT_THROW(f_x.impTerm(x), CVC4ApiException);
548
4
  ASSERT_THROW(f_x.impTerm(f), CVC4ApiException);
549
4
  ASSERT_THROW(f_x.impTerm(p), CVC4ApiException);
550
4
  ASSERT_THROW(f_x.impTerm(zero), CVC4ApiException);
551
4
  ASSERT_THROW(f_x.impTerm(f_x), CVC4ApiException);
552
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
553
4
  ASSERT_THROW(sum.impTerm(b), CVC4ApiException);
554
4
  ASSERT_THROW(sum.impTerm(x), CVC4ApiException);
555
4
  ASSERT_THROW(sum.impTerm(f), CVC4ApiException);
556
4
  ASSERT_THROW(sum.impTerm(p), CVC4ApiException);
557
4
  ASSERT_THROW(sum.impTerm(zero), CVC4ApiException);
558
4
  ASSERT_THROW(sum.impTerm(f_x), CVC4ApiException);
559
4
  ASSERT_THROW(sum.impTerm(sum), CVC4ApiException);
560
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
561
2
  ASSERT_NO_THROW(p_0.impTerm(b));
562
4
  ASSERT_THROW(p_0.impTerm(x), CVC4ApiException);
563
4
  ASSERT_THROW(p_0.impTerm(f), CVC4ApiException);
564
4
  ASSERT_THROW(p_0.impTerm(p), CVC4ApiException);
565
4
  ASSERT_THROW(p_0.impTerm(zero), CVC4ApiException);
566
4
  ASSERT_THROW(p_0.impTerm(f_x), CVC4ApiException);
567
4
  ASSERT_THROW(p_0.impTerm(sum), CVC4ApiException);
568
2
  ASSERT_NO_THROW(p_0.impTerm(p_0));
569
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
570
2
  ASSERT_NO_THROW(p_f_x.impTerm(b));
571
4
  ASSERT_THROW(p_f_x.impTerm(x), CVC4ApiException);
572
4
  ASSERT_THROW(p_f_x.impTerm(f), CVC4ApiException);
573
4
  ASSERT_THROW(p_f_x.impTerm(p), CVC4ApiException);
574
4
  ASSERT_THROW(p_f_x.impTerm(zero), CVC4ApiException);
575
4
  ASSERT_THROW(p_f_x.impTerm(f_x), CVC4ApiException);
576
4
  ASSERT_THROW(p_f_x.impTerm(sum), CVC4ApiException);
577
2
  ASSERT_NO_THROW(p_f_x.impTerm(p_0));
578
2
  ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
579
}
580
581
31
TEST_F(TestApiBlackTerm, iteTerm)
582
{
583
4
  Sort bvSort = d_solver.mkBitVectorSort(8);
584
4
  Sort intSort = d_solver.getIntegerSort();
585
4
  Sort boolSort = d_solver.getBooleanSort();
586
4
  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
587
4
  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
588
589
4
  Term b = d_solver.mkTrue();
590
4
  ASSERT_THROW(Term().iteTerm(b, b), CVC4ApiException);
591
4
  ASSERT_THROW(b.iteTerm(Term(), b), CVC4ApiException);
592
4
  ASSERT_THROW(b.iteTerm(b, Term()), CVC4ApiException);
593
2
  ASSERT_NO_THROW(b.iteTerm(b, b));
594
4
  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
595
2
  ASSERT_NO_THROW(b.iteTerm(x, x));
596
2
  ASSERT_NO_THROW(b.iteTerm(b, b));
597
4
  ASSERT_THROW(b.iteTerm(x, b), CVC4ApiException);
598
4
  ASSERT_THROW(x.iteTerm(x, x), CVC4ApiException);
599
4
  ASSERT_THROW(x.iteTerm(x, b), CVC4ApiException);
600
4
  Term f = d_solver.mkVar(funSort1, "f");
601
4
  ASSERT_THROW(f.iteTerm(b, b), CVC4ApiException);
602
4
  ASSERT_THROW(x.iteTerm(b, x), CVC4ApiException);
603
4
  Term p = d_solver.mkVar(funSort2, "p");
604
4
  ASSERT_THROW(p.iteTerm(b, b), CVC4ApiException);
605
4
  ASSERT_THROW(p.iteTerm(x, b), CVC4ApiException);
606
4
  Term zero = d_solver.mkInteger(0);
607
4
  ASSERT_THROW(zero.iteTerm(x, x), CVC4ApiException);
608
4
  ASSERT_THROW(zero.iteTerm(x, b), CVC4ApiException);
609
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
610
4
  ASSERT_THROW(f_x.iteTerm(b, b), CVC4ApiException);
611
4
  ASSERT_THROW(f_x.iteTerm(b, x), CVC4ApiException);
612
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
613
4
  ASSERT_THROW(sum.iteTerm(x, x), CVC4ApiException);
614
4
  ASSERT_THROW(sum.iteTerm(b, x), CVC4ApiException);
615
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
616
2
  ASSERT_NO_THROW(p_0.iteTerm(b, b));
617
2
  ASSERT_NO_THROW(p_0.iteTerm(x, x));
618
4
  ASSERT_THROW(p_0.iteTerm(x, b), CVC4ApiException);
619
4
  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
620
2
  ASSERT_NO_THROW(p_f_x.iteTerm(b, b));
621
2
  ASSERT_NO_THROW(p_f_x.iteTerm(x, x));
622
4
  ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException);
623
}
624
625
31
TEST_F(TestApiBlackTerm, termAssignment)
626
{
627
4
  Term t1 = d_solver.mkInteger(1);
628
4
  Term t2 = t1;
629
2
  t2 = d_solver.mkInteger(2);
630
2
  ASSERT_EQ(t1, d_solver.mkInteger(1));
631
}
632
633
31
TEST_F(TestApiBlackTerm, termCompare)
634
{
635
4
  Term t1 = d_solver.mkInteger(1);
636
4
  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
637
4
  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
638
2
  ASSERT_TRUE(t2 >= t3);
639
2
  ASSERT_TRUE(t2 <= t3);
640
2
  ASSERT_TRUE((t1 > t2) != (t1 < t2));
641
2
  ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2));
642
}
643
644
31
TEST_F(TestApiBlackTerm, termChildren)
645
{
646
  // simple term 2+3
647
4
  Term two = d_solver.mkInteger(2);
648
4
  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
649
2
  ASSERT_EQ(t1[0], two);
650
2
  ASSERT_EQ(t1.getNumChildren(), 2);
651
4
  Term tnull;
652
4
  ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException);
653
654
  // apply term f(2)
655
4
  Sort intSort = d_solver.getIntegerSort();
656
4
  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
657
4
  Term f = d_solver.mkConst(fsort, "f");
658
4
  Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
659
  // due to our higher-order view of terms, we treat f as a child of APPLY_UF
660
2
  ASSERT_EQ(t2.getNumChildren(), 2);
661
2
  ASSERT_EQ(t2[0], f);
662
2
  ASSERT_EQ(t2[1], two);
663
4
  ASSERT_THROW(tnull[0], CVC4ApiException);
664
}
665
666
31
TEST_F(TestApiBlackTerm, getInteger)
667
{
668
4
  Term int1 = d_solver.mkInteger("-18446744073709551616");
669
4
  Term int2 = d_solver.mkInteger("-18446744073709551615");
670
4
  Term int3 = d_solver.mkInteger("-4294967296");
671
4
  Term int4 = d_solver.mkInteger("-4294967295");
672
4
  Term int5 = d_solver.mkInteger("-10");
673
4
  Term int6 = d_solver.mkInteger("0");
674
4
  Term int7 = d_solver.mkInteger("10");
675
4
  Term int8 = d_solver.mkInteger("4294967295");
676
4
  Term int9 = d_solver.mkInteger("4294967296");
677
4
  Term int10 = d_solver.mkInteger("18446744073709551615");
678
4
  Term int11 = d_solver.mkInteger("18446744073709551616");
679
4
  Term int12 = d_solver.mkInteger("-0");
680
681
4
  ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException);
682
4
  ASSERT_THROW(d_solver.mkInteger("-"), CVC4ApiException);
683
4
  ASSERT_THROW(d_solver.mkInteger("-1-"), CVC4ApiException);
684
4
  ASSERT_THROW(d_solver.mkInteger("0.0"), CVC4ApiException);
685
4
  ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC4ApiException);
686
4
  ASSERT_THROW(d_solver.mkInteger("012"), CVC4ApiException);
687
4
  ASSERT_THROW(d_solver.mkInteger("0000"), CVC4ApiException);
688
4
  ASSERT_THROW(d_solver.mkInteger("-01"), CVC4ApiException);
689
4
  ASSERT_THROW(d_solver.mkInteger("-00"), CVC4ApiException);
690
691
2
  ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
692
2
              && !int1.isUInt64() && int1.isInteger());
693
2
  ASSERT_EQ(int1.getInteger(), "-18446744073709551616");
694
2
  ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
695
2
              && !int2.isUInt64() && int2.isInteger());
696
2
  ASSERT_EQ(int2.getInteger(), "-18446744073709551615");
697
2
  ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
698
2
              && !int3.isUInt64() && int3.isInteger());
699
2
  ASSERT_EQ(int3.getInt64(), -4294967296);
700
2
  ASSERT_EQ(int3.getInteger(), "-4294967296");
701
2
  ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
702
2
              && !int4.isUInt64() && int4.isInteger());
703
2
  ASSERT_EQ(int4.getInt64(), -4294967295);
704
2
  ASSERT_EQ(int4.getInteger(), "-4294967295");
705
2
  ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
706
2
              && !int5.isUInt64() && int5.isInteger());
707
2
  ASSERT_EQ(int5.getInt32(), -10);
708
2
  ASSERT_EQ(int5.getInt64(), -10);
709
2
  ASSERT_EQ(int5.getInteger(), "-10");
710
2
  ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
711
2
              && int6.isUInt64() && int6.isInteger());
712
2
  ASSERT_EQ(int6.getInt32(), 0);
713
2
  ASSERT_EQ(int6.getUInt32(), 0);
714
2
  ASSERT_EQ(int6.getInt64(), 0);
715
2
  ASSERT_EQ(int6.getUInt64(), 0);
716
2
  ASSERT_EQ(int6.getInteger(), "0");
717
2
  ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
718
2
              && int7.isUInt64() && int7.isInteger());
719
2
  ASSERT_EQ(int7.getInt32(), 10);
720
2
  ASSERT_EQ(int7.getUInt32(), 10);
721
2
  ASSERT_EQ(int7.getInt64(), 10);
722
2
  ASSERT_EQ(int7.getUInt64(), 10);
723
2
  ASSERT_EQ(int7.getInteger(), "10");
724
2
  ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
725
2
              && int8.isUInt64() && int8.isInteger());
726
2
  ASSERT_EQ(int8.getUInt32(), 4294967295);
727
2
  ASSERT_EQ(int8.getInt64(), 4294967295);
728
2
  ASSERT_EQ(int8.getUInt64(), 4294967295);
729
2
  ASSERT_EQ(int8.getInteger(), "4294967295");
730
2
  ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
731
2
              && int9.isUInt64() && int9.isInteger());
732
2
  ASSERT_EQ(int9.getInt64(), 4294967296);
733
2
  ASSERT_EQ(int9.getUInt64(), 4294967296);
734
2
  ASSERT_EQ(int9.getInteger(), "4294967296");
735
2
  ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
736
2
              && int10.isUInt64() && int10.isInteger());
737
2
  ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull);
738
2
  ASSERT_EQ(int10.getInteger(), "18446744073709551615");
739
2
  ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
740
2
              && !int11.isUInt64() && int11.isInteger());
741
2
  ASSERT_EQ(int11.getInteger(), "18446744073709551616");
742
}
743
744
31
TEST_F(TestApiBlackTerm, getString)
745
{
746
4
  Term s1 = d_solver.mkString("abcde");
747
2
  ASSERT_TRUE(s1.isString());
748
2
  ASSERT_EQ(s1.getString(), L"abcde");
749
}
750
751
31
TEST_F(TestApiBlackTerm, substitute)
752
{
753
4
  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
754
4
  Term one = d_solver.mkInteger(1);
755
4
  Term ttrue = d_solver.mkTrue();
756
4
  Term xpx = d_solver.mkTerm(PLUS, x, x);
757
4
  Term onepone = d_solver.mkTerm(PLUS, one, one);
758
759
2
  ASSERT_EQ(xpx.substitute(x, one), onepone);
760
2
  ASSERT_EQ(onepone.substitute(one, x), xpx);
761
  // incorrect due to type
762
4
  ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException);
763
764
  // simultaneous substitution
765
4
  Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
766
4
  Term xpy = d_solver.mkTerm(PLUS, x, y);
767
4
  Term xpone = d_solver.mkTerm(PLUS, y, one);
768
4
  std::vector<Term> es;
769
4
  std::vector<Term> rs;
770
2
  es.push_back(x);
771
2
  rs.push_back(y);
772
2
  es.push_back(y);
773
2
  rs.push_back(one);
774
2
  ASSERT_EQ(xpy.substitute(es, rs), xpone);
775
776
  // incorrect substitution due to arity
777
2
  rs.pop_back();
778
4
  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
779
780
  // incorrect substitution due to types
781
2
  rs.push_back(ttrue);
782
4
  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
783
784
  // null cannot substitute
785
4
  Term tnull;
786
4
  ASSERT_THROW(tnull.substitute(one, x), CVC4ApiException);
787
4
  ASSERT_THROW(xpx.substitute(tnull, x), CVC4ApiException);
788
4
  ASSERT_THROW(xpx.substitute(x, tnull), CVC4ApiException);
789
2
  rs.pop_back();
790
2
  rs.push_back(tnull);
791
4
  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
792
2
  es.clear();
793
2
  rs.clear();
794
2
  es.push_back(x);
795
2
  rs.push_back(y);
796
4
  ASSERT_THROW(tnull.substitute(es, rs), CVC4ApiException);
797
2
  es.push_back(tnull);
798
2
  rs.push_back(one);
799
4
  ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException);
800
}
801
802
31
TEST_F(TestApiBlackTerm, constArray)
803
{
804
4
  Sort intsort = d_solver.getIntegerSort();
805
4
  Sort arrsort = d_solver.mkArraySort(intsort, intsort);
806
4
  Term a = d_solver.mkConst(arrsort, "a");
807
4
  Term one = d_solver.mkInteger(1);
808
4
  Term constarr = d_solver.mkConstArray(arrsort, one);
809
810
2
  ASSERT_EQ(constarr.getKind(), CONST_ARRAY);
811
2
  ASSERT_EQ(constarr.getConstArrayBase(), one);
812
4
  ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException);
813
814
2
  arrsort =
815
4
      d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
816
4
  Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
817
  Term stores = d_solver.mkTerm(
818
4
      STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
819
2
  stores =
820
4
      d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
821
2
  stores =
822
4
      d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
823
}
824
825
31
TEST_F(TestApiBlackTerm, constSequenceElements)
826
{
827
4
  Sort realsort = d_solver.getRealSort();
828
4
  Sort seqsort = d_solver.mkSequenceSort(realsort);
829
4
  Term s = d_solver.mkEmptySequence(seqsort);
830
831
2
  ASSERT_EQ(s.getKind(), CONST_SEQUENCE);
832
  // empty sequence has zero elements
833
4
  std::vector<Term> cs = s.getConstSequenceElements();
834
2
  ASSERT_TRUE(cs.empty());
835
836
  // A seq.unit app is not a constant sequence (regardless of whether it is
837
  // applied to a constant).
838
4
  Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
839
4
  ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException);
840
}
841
842
31
TEST_F(TestApiBlackTerm, termScopedToString)
843
{
844
4
  Sort intsort = d_solver.getIntegerSort();
845
4
  Term x = d_solver.mkConst(intsort, "x");
846
2
  ASSERT_EQ(x.toString(), "x");
847
4
  Solver solver2;
848
2
  ASSERT_EQ(x.toString(), "x");
849
}
850
}  // namespace test
851
69
}  // namespace CVC4