GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/solver_black.cpp Lines: 1533 1545 99.2 %
Date: 2021-03-23 Branches: 6010 16756 35.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mudathir Mohamed, Ying Sheng
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 Solver class of the  C++ API.
13
 **
14
 ** Black box testing of the Solver class of the  C++ API.
15
 **/
16
17
#include "base/configuration.h"
18
#include "test_api.h"
19
20
namespace CVC4 {
21
22
using namespace api;
23
24
namespace test {
25
26
524
class TestApiBlackSolver : public TestApi
27
{
28
};
29
30
140
TEST_F(TestApiBlackSolver, recoverableException)
31
{
32
2
  d_solver.setOption("produce-models", "true");
33
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
34
2
  d_solver.assertFormula(x.eqTerm(x).notTerm());
35
4
  ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException);
36
}
37
38
140
TEST_F(TestApiBlackSolver, supportsFloatingPoint)
39
{
40
2
  if (d_solver.supportsFloatingPoint())
41
  {
42
2
    ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
43
  }
44
  else
45
  {
46
    ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
47
                 CVC4ApiException);
48
  }
49
}
50
51
140
TEST_F(TestApiBlackSolver, getBooleanSort)
52
{
53
2
  ASSERT_NO_THROW(d_solver.getBooleanSort());
54
}
55
56
140
TEST_F(TestApiBlackSolver, getIntegerSort)
57
{
58
2
  ASSERT_NO_THROW(d_solver.getIntegerSort());
59
}
60
61
140
TEST_F(TestApiBlackSolver, getNullSort)
62
{
63
2
  ASSERT_NO_THROW(d_solver.getNullSort());
64
}
65
66
140
TEST_F(TestApiBlackSolver, getRealSort)
67
{
68
2
  ASSERT_NO_THROW(d_solver.getRealSort());
69
}
70
71
140
TEST_F(TestApiBlackSolver, getRegExpSort)
72
{
73
2
  ASSERT_NO_THROW(d_solver.getRegExpSort());
74
}
75
76
140
TEST_F(TestApiBlackSolver, getStringSort)
77
{
78
2
  ASSERT_NO_THROW(d_solver.getStringSort());
79
}
80
81
140
TEST_F(TestApiBlackSolver, getRoundingModeSort)
82
{
83
2
  if (d_solver.supportsFloatingPoint())
84
  {
85
2
    ASSERT_NO_THROW(d_solver.getRoundingModeSort());
86
  }
87
  else
88
  {
89
    ASSERT_THROW(d_solver.getRoundingModeSort(), CVC4ApiException);
90
  }
91
}
92
93
140
TEST_F(TestApiBlackSolver, mkArraySort)
94
{
95
4
  Sort boolSort = d_solver.getBooleanSort();
96
4
  Sort intSort = d_solver.getIntegerSort();
97
4
  Sort realSort = d_solver.getRealSort();
98
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
99
2
  ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, boolSort));
100
2
  ASSERT_NO_THROW(d_solver.mkArraySort(intSort, intSort));
101
2
  ASSERT_NO_THROW(d_solver.mkArraySort(realSort, realSort));
102
2
  ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, bvSort));
103
2
  ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort));
104
2
  ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort));
105
106
2
  if (d_solver.supportsFloatingPoint())
107
  {
108
4
    Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
109
2
    ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
110
2
    ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
111
  }
112
113
4
  Solver slv;
114
4
  ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException);
115
}
116
117
140
TEST_F(TestApiBlackSolver, mkBitVectorSort)
118
{
119
2
  ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
120
4
  ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException);
121
}
122
123
140
TEST_F(TestApiBlackSolver, mkFloatingPointSort)
124
{
125
2
  if (d_solver.supportsFloatingPoint())
126
  {
127
2
    ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
128
4
    ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException);
129
4
    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException);
130
  }
131
  else
132
  {
133
    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC4ApiException);
134
  }
135
}
136
137
140
TEST_F(TestApiBlackSolver, mkDatatypeSort)
138
{
139
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
140
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
141
2
  cons.addSelector("head", d_solver.getIntegerSort());
142
2
  dtypeSpec.addConstructor(cons);
143
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
144
2
  dtypeSpec.addConstructor(nil);
145
2
  ASSERT_NO_THROW(d_solver.mkDatatypeSort(dtypeSpec));
146
147
4
  Solver slv;
148
4
  ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException);
149
150
4
  DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
151
4
  ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException);
152
}
153
154
140
TEST_F(TestApiBlackSolver, mkDatatypeSorts)
155
{
156
4
  Solver slv;
157
158
4
  DatatypeDecl dtypeSpec1 = d_solver.mkDatatypeDecl("list1");
159
4
  DatatypeConstructorDecl cons1 = d_solver.mkDatatypeConstructorDecl("cons1");
160
2
  cons1.addSelector("head1", d_solver.getIntegerSort());
161
2
  dtypeSpec1.addConstructor(cons1);
162
4
  DatatypeConstructorDecl nil1 = d_solver.mkDatatypeConstructorDecl("nil1");
163
2
  dtypeSpec1.addConstructor(nil1);
164
4
  DatatypeDecl dtypeSpec2 = d_solver.mkDatatypeDecl("list2");
165
4
  DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons2");
166
2
  cons2.addSelector("head2", d_solver.getIntegerSort());
167
2
  dtypeSpec2.addConstructor(cons2);
168
4
  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
169
2
  dtypeSpec2.addConstructor(nil2);
170
4
  std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
171
2
  ASSERT_NO_THROW(d_solver.mkDatatypeSorts(decls));
172
173
4
  ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC4ApiException);
174
175
4
  DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
176
4
  std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
177
4
  ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC4ApiException);
178
179
  /* with unresolved sorts */
180
4
  Sort unresList = d_solver.mkUninterpretedSort("ulist");
181
4
  std::set<Sort> unresSorts = {unresList};
182
4
  DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
183
4
  DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
184
2
  ucons.addSelector("car", unresList);
185
2
  ucons.addSelector("cdr", unresList);
186
2
  ulist.addConstructor(ucons);
187
4
  DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
188
2
  ulist.addConstructor(unil);
189
4
  std::vector<DatatypeDecl> udecls = {ulist};
190
2
  ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts));
191
192
4
  ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException);
193
194
  /* Note: More tests are in datatype_api_black. */
195
}
196
197
140
TEST_F(TestApiBlackSolver, mkFunctionSort)
198
{
199
2
  ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
200
                                          d_solver.getIntegerSort()));
201
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
202
8
                                         d_solver.getIntegerSort());
203
  // function arguments are allowed
204
2
  ASSERT_NO_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
205
  // non-first-class arguments are not allowed
206
4
  Sort reSort = d_solver.getRegExpSort();
207
4
  ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()),
208
2
               CVC4ApiException);
209
4
  ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
210
2
               CVC4ApiException);
211
2
  ASSERT_NO_THROW(d_solver.mkFunctionSort(
212
      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
213
      d_solver.getIntegerSort()));
214
4
  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
215
8
                                          d_solver.getIntegerSort());
216
  // function arguments are allowed
217
2
  ASSERT_NO_THROW(
218
      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
219
                              d_solver.getIntegerSort()));
220
4
  ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
221
                                        d_solver.mkUninterpretedSort("u")},
222
                                       funSort2),
223
2
               CVC4ApiException);
224
225
4
  Solver slv;
226
4
  ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
227
                                  d_solver.getIntegerSort()),
228
2
               CVC4ApiException);
229
4
  ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
230
                                  d_solver.getIntegerSort()),
231
2
               CVC4ApiException);
232
  std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
233
                              slv.getIntegerSort(),
234
4
                              d_solver.getIntegerSort()};
235
4
  std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
236
2
  ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
237
4
  ASSERT_THROW(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
238
2
               CVC4ApiException);
239
4
  ASSERT_THROW(slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()),
240
2
               CVC4ApiException);
241
}
242
243
140
TEST_F(TestApiBlackSolver, mkParamSort)
244
{
245
2
  ASSERT_NO_THROW(d_solver.mkParamSort("T"));
246
2
  ASSERT_NO_THROW(d_solver.mkParamSort(""));
247
}
248
249
140
TEST_F(TestApiBlackSolver, mkPredicateSort)
250
{
251
2
  ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
252
4
  ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
253
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
254
8
                                         d_solver.getIntegerSort());
255
  // functions as arguments are allowed
256
2
  ASSERT_NO_THROW(
257
      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}));
258
259
4
  Solver slv;
260
4
  ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}),
261
2
               CVC4ApiException);
262
}
263
264
140
TEST_F(TestApiBlackSolver, mkRecordSort)
265
{
266
  std::vector<std::pair<std::string, Sort>> fields = {
267
4
      std::make_pair("b", d_solver.getBooleanSort()),
268
4
      std::make_pair("bv", d_solver.mkBitVectorSort(8)),
269
6
      std::make_pair("i", d_solver.getIntegerSort())};
270
4
  std::vector<std::pair<std::string, Sort>> empty;
271
2
  ASSERT_NO_THROW(d_solver.mkRecordSort(fields));
272
2
  ASSERT_NO_THROW(d_solver.mkRecordSort(empty));
273
4
  Sort recSort = d_solver.mkRecordSort(fields);
274
2
  ASSERT_NO_THROW(recSort.getDatatype());
275
276
4
  Solver slv;
277
4
  ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException);
278
}
279
280
140
TEST_F(TestApiBlackSolver, mkSetSort)
281
{
282
2
  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getBooleanSort()));
283
2
  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
284
2
  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
285
4
  Solver slv;
286
4
  ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
287
}
288
289
140
TEST_F(TestApiBlackSolver, mkBagSort)
290
{
291
2
  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getBooleanSort()));
292
2
  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
293
2
  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
294
4
  Solver slv;
295
4
  ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
296
}
297
298
140
TEST_F(TestApiBlackSolver, mkSequenceSort)
299
{
300
2
  ASSERT_NO_THROW(d_solver.mkSequenceSort(d_solver.getBooleanSort()));
301
2
  ASSERT_NO_THROW(d_solver.mkSequenceSort(
302
      d_solver.mkSequenceSort(d_solver.getIntegerSort())));
303
4
  Solver slv;
304
4
  ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException);
305
}
306
307
140
TEST_F(TestApiBlackSolver, mkUninterpretedSort)
308
{
309
2
  ASSERT_NO_THROW(d_solver.mkUninterpretedSort("u"));
310
2
  ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
311
}
312
313
140
TEST_F(TestApiBlackSolver, mkSortConstructorSort)
314
{
315
2
  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
316
2
  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
317
4
  ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException);
318
}
319
320
140
TEST_F(TestApiBlackSolver, mkTupleSort)
321
{
322
2
  ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
323
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
324
8
                                         d_solver.getIntegerSort());
325
4
  ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
326
2
               CVC4ApiException);
327
328
4
  Solver slv;
329
4
  ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException);
330
}
331
332
140
TEST_F(TestApiBlackSolver, mkBitVector)
333
{
334
2
  uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
335
2
  uint64_t val2 = 2;
336
2
  ASSERT_NO_THROW(d_solver.mkBitVector(size1, val1));
337
2
  ASSERT_NO_THROW(d_solver.mkBitVector(size2, val2));
338
2
  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 2));
339
2
  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 10));
340
2
  ASSERT_NO_THROW(d_solver.mkBitVector("1234", 10));
341
2
  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 16));
342
2
  ASSERT_NO_THROW(d_solver.mkBitVector("a09f", 16));
343
2
  ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10));
344
4
  ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC4ApiException);
345
4
  ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC4ApiException);
346
4
  ASSERT_THROW(d_solver.mkBitVector("", 2), CVC4ApiException);
347
4
  ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC4ApiException);
348
4
  ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException);
349
4
  ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException);
350
4
  ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException);
351
2
  ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
352
2
  ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
353
2
  ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
354
2
  ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
355
2
  ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10),
356
2
            d_solver.mkBitVector(8, "FF", 16));
357
}
358
359
140
TEST_F(TestApiBlackSolver, mkVar)
360
{
361
4
  Sort boolSort = d_solver.getBooleanSort();
362
4
  Sort intSort = d_solver.getIntegerSort();
363
4
  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
364
2
  ASSERT_NO_THROW(d_solver.mkVar(boolSort));
365
2
  ASSERT_NO_THROW(d_solver.mkVar(funSort));
366
2
  ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
367
2
  ASSERT_NO_THROW(d_solver.mkVar(funSort, ""));
368
4
  ASSERT_THROW(d_solver.mkVar(Sort()), CVC4ApiException);
369
4
  ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC4ApiException);
370
4
  Solver slv;
371
4
  ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException);
372
}
373
374
140
TEST_F(TestApiBlackSolver, mkBoolean)
375
{
376
2
  ASSERT_NO_THROW(d_solver.mkBoolean(true));
377
2
  ASSERT_NO_THROW(d_solver.mkBoolean(false));
378
}
379
380
140
TEST_F(TestApiBlackSolver, mkRoundingMode)
381
{
382
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
383
  {
384
2
    ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
385
  }
386
  else
387
  {
388
    ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
389
                 CVC4ApiException);
390
  }
391
}
392
393
140
TEST_F(TestApiBlackSolver, mkUninterpretedConst)
394
{
395
2
  ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
396
4
  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException);
397
4
  Solver slv;
398
4
  ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1),
399
2
               CVC4ApiException);
400
}
401
402
140
TEST_F(TestApiBlackSolver, mkAbstractValue)
403
{
404
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
405
4
  ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException);
406
4
  ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC4ApiException);
407
4
  ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC4ApiException);
408
4
  ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC4ApiException);
409
4
  ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC4ApiException);
410
411
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1));
412
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1));
413
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1));
414
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1));
415
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1));
416
2
  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1));
417
4
  ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException);
418
}
419
420
140
TEST_F(TestApiBlackSolver, mkFloatingPoint)
421
{
422
4
  Term t1 = d_solver.mkBitVector(8);
423
4
  Term t2 = d_solver.mkBitVector(4);
424
4
  Term t3 = d_solver.mkInteger(2);
425
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
426
  {
427
2
    ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
428
  }
429
  else
430
  {
431
    ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException);
432
  }
433
4
  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException);
434
4
  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException);
435
4
  ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException);
436
4
  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
437
4
  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
438
439
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
440
  {
441
4
    Solver slv;
442
4
    ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException);
443
  }
444
}
445
446
140
TEST_F(TestApiBlackSolver, mkEmptySet)
447
{
448
4
  Solver slv;
449
4
  Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
450
2
  ASSERT_NO_THROW(d_solver.mkEmptySet(Sort()));
451
2
  ASSERT_NO_THROW(d_solver.mkEmptySet(s));
452
4
  ASSERT_THROW(d_solver.mkEmptySet(d_solver.getBooleanSort()),
453
2
               CVC4ApiException);
454
4
  ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException);
455
}
456
457
140
TEST_F(TestApiBlackSolver, mkEmptyBag)
458
{
459
4
  Solver slv;
460
4
  Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
461
2
  ASSERT_NO_THROW(d_solver.mkEmptyBag(Sort()));
462
2
  ASSERT_NO_THROW(d_solver.mkEmptyBag(s));
463
4
  ASSERT_THROW(d_solver.mkEmptyBag(d_solver.getBooleanSort()),
464
2
               CVC4ApiException);
465
4
  ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException);
466
}
467
468
140
TEST_F(TestApiBlackSolver, mkEmptySequence)
469
{
470
4
  Solver slv;
471
4
  Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
472
2
  ASSERT_NO_THROW(d_solver.mkEmptySequence(s));
473
2
  ASSERT_NO_THROW(d_solver.mkEmptySequence(d_solver.getBooleanSort()));
474
4
  ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException);
475
}
476
477
140
TEST_F(TestApiBlackSolver, mkFalse)
478
{
479
2
  ASSERT_NO_THROW(d_solver.mkFalse());
480
2
  ASSERT_NO_THROW(d_solver.mkFalse());
481
}
482
483
140
TEST_F(TestApiBlackSolver, mkNaN)
484
{
485
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
486
  {
487
2
    ASSERT_NO_THROW(d_solver.mkNaN(3, 5));
488
  }
489
  else
490
  {
491
    ASSERT_THROW(d_solver.mkNaN(3, 5), CVC4ApiException);
492
  }
493
}
494
495
140
TEST_F(TestApiBlackSolver, mkNegZero)
496
{
497
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
498
  {
499
2
    ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
500
  }
501
  else
502
  {
503
    ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC4ApiException);
504
  }
505
}
506
507
140
TEST_F(TestApiBlackSolver, mkNegInf)
508
{
509
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
510
  {
511
2
    ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
512
  }
513
  else
514
  {
515
    ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC4ApiException);
516
  }
517
}
518
519
140
TEST_F(TestApiBlackSolver, mkPosInf)
520
{
521
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
522
  {
523
2
    ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
524
  }
525
  else
526
  {
527
    ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC4ApiException);
528
  }
529
}
530
531
140
TEST_F(TestApiBlackSolver, mkPosZero)
532
{
533
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
534
  {
535
2
    ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
536
  }
537
  else
538
  {
539
    ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC4ApiException);
540
  }
541
}
542
543
140
TEST_F(TestApiBlackSolver, mkOp)
544
{
545
  // mkOp(Kind kind, Kind k)
546
4
  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException);
547
548
  // mkOp(Kind kind, const std::string& arg)
549
2
  ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf"));
550
2
  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
551
4
  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException);
552
553
  // mkOp(Kind kind, uint32_t arg)
554
2
  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, 1));
555
2
  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1));
556
2
  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
557
4
  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException);
558
559
  // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
560
2
  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
561
4
  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
562
563
  // mkOp(Kind kind, std::vector<uint32_t> args)
564
4
  std::vector<uint32_t> args = {1, 2, 2};
565
2
  ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, args));
566
}
567
568
140
TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
569
570
140
TEST_F(TestApiBlackSolver, mkInteger)
571
{
572
2
  ASSERT_NO_THROW(d_solver.mkInteger("123"));
573
4
  ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException);
574
4
  ASSERT_THROW(d_solver.mkInteger("1/23"), CVC4ApiException);
575
4
  ASSERT_THROW(d_solver.mkInteger("12/3"), CVC4ApiException);
576
4
  ASSERT_THROW(d_solver.mkInteger(".2"), CVC4ApiException);
577
4
  ASSERT_THROW(d_solver.mkInteger("2."), CVC4ApiException);
578
4
  ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException);
579
4
  ASSERT_THROW(d_solver.mkInteger("asdf"), CVC4ApiException);
580
4
  ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC4ApiException);
581
4
  ASSERT_THROW(d_solver.mkInteger("."), CVC4ApiException);
582
4
  ASSERT_THROW(d_solver.mkInteger("/"), CVC4ApiException);
583
4
  ASSERT_THROW(d_solver.mkInteger("2/"), CVC4ApiException);
584
4
  ASSERT_THROW(d_solver.mkInteger("/2"), CVC4ApiException);
585
586
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
587
4
  ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC4ApiException);
588
4
  ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC4ApiException);
589
4
  ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC4ApiException);
590
4
  ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC4ApiException);
591
4
  ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC4ApiException);
592
4
  ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC4ApiException);
593
4
  ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC4ApiException);
594
4
  ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC4ApiException);
595
4
  ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC4ApiException);
596
4
  ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC4ApiException);
597
4
  ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC4ApiException);
598
4
  ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC4ApiException);
599
600
2
  int32_t val1 = 1;
601
2
  int64_t val2 = -1;
602
2
  uint32_t val3 = 1;
603
2
  uint64_t val4 = -1;
604
2
  ASSERT_NO_THROW(d_solver.mkInteger(val1));
605
2
  ASSERT_NO_THROW(d_solver.mkInteger(val2));
606
2
  ASSERT_NO_THROW(d_solver.mkInteger(val3));
607
2
  ASSERT_NO_THROW(d_solver.mkInteger(val4));
608
2
  ASSERT_NO_THROW(d_solver.mkInteger(val4));
609
}
610
611
140
TEST_F(TestApiBlackSolver, mkReal)
612
{
613
2
  ASSERT_NO_THROW(d_solver.mkReal("123"));
614
2
  ASSERT_NO_THROW(d_solver.mkReal("1.23"));
615
2
  ASSERT_NO_THROW(d_solver.mkReal("1/23"));
616
2
  ASSERT_NO_THROW(d_solver.mkReal("12/3"));
617
2
  ASSERT_NO_THROW(d_solver.mkReal(".2"));
618
2
  ASSERT_NO_THROW(d_solver.mkReal("2."));
619
4
  ASSERT_THROW(d_solver.mkReal(""), CVC4ApiException);
620
4
  ASSERT_THROW(d_solver.mkReal("asdf"), CVC4ApiException);
621
4
  ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC4ApiException);
622
4
  ASSERT_THROW(d_solver.mkReal("."), CVC4ApiException);
623
4
  ASSERT_THROW(d_solver.mkReal("/"), CVC4ApiException);
624
4
  ASSERT_THROW(d_solver.mkReal("2/"), CVC4ApiException);
625
4
  ASSERT_THROW(d_solver.mkReal("/2"), CVC4ApiException);
626
627
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
628
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("1.23")));
629
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("1/23")));
630
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("12/3")));
631
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string(".2")));
632
2
  ASSERT_NO_THROW(d_solver.mkReal(std::string("2.")));
633
4
  ASSERT_THROW(d_solver.mkReal(std::string("")), CVC4ApiException);
634
4
  ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC4ApiException);
635
4
  ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException);
636
4
  ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC4ApiException);
637
4
  ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC4ApiException);
638
4
  ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC4ApiException);
639
4
  ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC4ApiException);
640
641
2
  int32_t val1 = 1;
642
2
  int64_t val2 = -1;
643
2
  uint32_t val3 = 1;
644
2
  uint64_t val4 = -1;
645
2
  ASSERT_NO_THROW(d_solver.mkReal(val1));
646
2
  ASSERT_NO_THROW(d_solver.mkReal(val2));
647
2
  ASSERT_NO_THROW(d_solver.mkReal(val3));
648
2
  ASSERT_NO_THROW(d_solver.mkReal(val4));
649
2
  ASSERT_NO_THROW(d_solver.mkReal(val4));
650
2
  ASSERT_NO_THROW(d_solver.mkReal(val1, val1));
651
2
  ASSERT_NO_THROW(d_solver.mkReal(val2, val2));
652
2
  ASSERT_NO_THROW(d_solver.mkReal(val3, val3));
653
2
  ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
654
}
655
656
140
TEST_F(TestApiBlackSolver, mkRegexpEmpty)
657
{
658
4
  Sort strSort = d_solver.getStringSort();
659
4
  Term s = d_solver.mkConst(strSort, "s");
660
2
  ASSERT_NO_THROW(
661
      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
662
}
663
664
140
TEST_F(TestApiBlackSolver, mkRegexpSigma)
665
{
666
4
  Sort strSort = d_solver.getStringSort();
667
4
  Term s = d_solver.mkConst(strSort, "s");
668
2
  ASSERT_NO_THROW(
669
      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
670
}
671
672
140
TEST_F(TestApiBlackSolver, mkSepNil)
673
{
674
2
  ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
675
4
  ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException);
676
4
  Solver slv;
677
4
  ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException);
678
}
679
680
140
TEST_F(TestApiBlackSolver, mkString)
681
{
682
2
  ASSERT_NO_THROW(d_solver.mkString(""));
683
2
  ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
684
2
  ASSERT_EQ(d_solver.mkString("asdf\\nasdf").toString(),
685
2
            "\"asdf\\u{5c}nasdf\"");
686
2
  ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
687
2
            "\"asdf\\u{5c}nasdf\"");
688
}
689
690
140
TEST_F(TestApiBlackSolver, mkChar)
691
{
692
2
  ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
693
2
  ASSERT_NO_THROW(d_solver.mkChar("aA"));
694
4
  ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException);
695
4
  ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException);
696
4
  ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException);
697
2
  ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
698
}
699
700
140
TEST_F(TestApiBlackSolver, mkTerm)
701
{
702
4
  Sort bv32 = d_solver.mkBitVectorSort(32);
703
4
  Term a = d_solver.mkConst(bv32, "a");
704
4
  Term b = d_solver.mkConst(bv32, "b");
705
4
  std::vector<Term> v1 = {a, b};
706
4
  std::vector<Term> v2 = {a, Term()};
707
4
  std::vector<Term> v3 = {a, d_solver.mkTrue()};
708
4
  std::vector<Term> v4 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
709
4
  std::vector<Term> v5 = {d_solver.mkInteger(1), Term()};
710
4
  std::vector<Term> v6 = {};
711
4
  Solver slv;
712
713
  // mkTerm(Kind kind) const
714
2
  ASSERT_NO_THROW(d_solver.mkTerm(PI));
715
2
  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY));
716
2
  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA));
717
4
  ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException);
718
719
  // mkTerm(Kind kind, Term child) const
720
2
  ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue()));
721
4
  ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC4ApiException);
722
4
  ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC4ApiException);
723
4
  ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC4ApiException);
724
725
  // mkTerm(Kind kind, Term child1, Term child2) const
726
2
  ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, a, b));
727
4
  ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException);
728
4
  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException);
729
4
  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC4ApiException);
730
4
  ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC4ApiException);
731
732
  // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
733
2
  ASSERT_NO_THROW(d_solver.mkTerm(
734
      ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
735
4
  ASSERT_THROW(
736
      d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()),
737
2
      CVC4ApiException);
738
4
  ASSERT_THROW(
739
      d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()),
740
2
      CVC4ApiException);
741
4
  ASSERT_THROW(
742
      d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()),
743
2
      CVC4ApiException);
744
4
  ASSERT_THROW(d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b),
745
2
               CVC4ApiException);
746
4
  ASSERT_THROW(
747
      slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()),
748
2
      CVC4ApiException);
749
750
  // mkTerm(Kind kind, const std::vector<Term>& children) const
751
2
  ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, v1));
752
4
  ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC4ApiException);
753
4
  ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC4ApiException);
754
4
  ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException);
755
}
756
757
140
TEST_F(TestApiBlackSolver, mkTermFromOp)
758
{
759
4
  Sort bv32 = d_solver.mkBitVectorSort(32);
760
4
  Term a = d_solver.mkConst(bv32, "a");
761
4
  Term b = d_solver.mkConst(bv32, "b");
762
4
  std::vector<Term> v1 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
763
4
  std::vector<Term> v2 = {d_solver.mkInteger(1), Term()};
764
4
  std::vector<Term> v3 = {};
765
4
  std::vector<Term> v4 = {d_solver.mkInteger(5)};
766
4
  Solver slv;
767
768
  // simple operator terms
769
4
  Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
770
4
  Op opterm2 = d_solver.mkOp(DIVISIBLE, 1);
771
772
  // list datatype
773
4
  Sort sort = d_solver.mkParamSort("T");
774
4
  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
775
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
776
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
777
2
  cons.addSelector("head", sort);
778
2
  cons.addSelectorSelf("tail");
779
2
  listDecl.addConstructor(cons);
780
2
  listDecl.addConstructor(nil);
781
4
  Sort listSort = d_solver.mkDatatypeSort(listDecl);
782
  Sort intListSort =
783
4
      listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
784
4
  Term c = d_solver.mkConst(intListSort, "c");
785
4
  Datatype list = listSort.getDatatype();
786
787
  // list datatype constructor and selector operator terms
788
4
  Term consTerm1 = list.getConstructorTerm("cons");
789
4
  Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
790
4
  Term nilTerm1 = list.getConstructorTerm("nil");
791
4
  Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
792
4
  Term headTerm1 = list["cons"].getSelectorTerm("head");
793
4
  Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
794
4
  Term tailTerm1 = list["cons"].getSelectorTerm("tail");
795
4
  Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
796
797
  // mkTerm(Op op, Term term) const
798
2
  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
799
2
  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
800
4
  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC4ApiException);
801
4
  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC4ApiException);
802
4
  ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC4ApiException);
803
4
  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
804
4
  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC4ApiException);
805
4
  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
806
4
  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException);
807
808
  // mkTerm(Op op, Term child) const
809
2
  ASSERT_NO_THROW(d_solver.mkTerm(opterm1, a));
810
2
  ASSERT_NO_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
811
2
  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
812
2
  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
813
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC4ApiException);
814
4
  ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC4ApiException);
815
4
  ASSERT_THROW(
816
      d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)),
817
2
      CVC4ApiException);
818
4
  ASSERT_THROW(slv.mkTerm(opterm1, a), CVC4ApiException);
819
820
  // mkTerm(Op op, Term child1, Term child2) const
821
2
  ASSERT_NO_THROW(
822
      d_solver.mkTerm(APPLY_CONSTRUCTOR,
823
                      consTerm1,
824
                      d_solver.mkInteger(0),
825
                      d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
826
4
  ASSERT_THROW(
827
      d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)),
828
2
      CVC4ApiException);
829
4
  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC4ApiException);
830
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1), Term()),
831
2
               CVC4ApiException);
832
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, Term(), d_solver.mkInteger(1)),
833
2
               CVC4ApiException);
834
4
  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR,
835
                          consTerm1,
836
                          d_solver.mkInteger(0),
837
                          d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
838
2
               CVC4ApiException);
839
840
  // mkTerm(Op op, Term child1, Term child2, Term child3) const
841
4
  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException);
842
4
  ASSERT_THROW(
843
      d_solver.mkTerm(
844
          opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), Term()),
845
2
      CVC4ApiException);
846
847
  // mkTerm(Op op, const std::vector<Term>& children) const
848
2
  ASSERT_NO_THROW(d_solver.mkTerm(opterm2, v4));
849
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC4ApiException);
850
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC4ApiException);
851
4
  ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC4ApiException);
852
4
  ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException);
853
}
854
855
140
TEST_F(TestApiBlackSolver, mkTrue)
856
{
857
2
  ASSERT_NO_THROW(d_solver.mkTrue());
858
2
  ASSERT_NO_THROW(d_solver.mkTrue());
859
}
860
861
140
TEST_F(TestApiBlackSolver, mkTuple)
862
{
863
2
  ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
864
                                   {d_solver.mkBitVector("101", 2)}));
865
2
  ASSERT_NO_THROW(
866
      d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}));
867
868
4
  ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}),
869
2
               CVC4ApiException);
870
4
  ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)},
871
                                {d_solver.mkBitVector("101", 2)}),
872
2
               CVC4ApiException);
873
4
  ASSERT_THROW(
874
      d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}),
875
2
      CVC4ApiException);
876
4
  Solver slv;
877
4
  ASSERT_THROW(
878
      slv.mkTuple({d_solver.mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
879
2
      CVC4ApiException);
880
4
  ASSERT_THROW(
881
      slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver.mkBitVector("101", 2)}),
882
2
      CVC4ApiException);
883
}
884
885
140
TEST_F(TestApiBlackSolver, mkUniverseSet)
886
{
887
2
  ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
888
4
  ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException);
889
4
  Solver slv;
890
4
  ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException);
891
}
892
893
140
TEST_F(TestApiBlackSolver, mkConst)
894
{
895
4
  Sort boolSort = d_solver.getBooleanSort();
896
4
  Sort intSort = d_solver.getIntegerSort();
897
4
  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
898
2
  ASSERT_NO_THROW(d_solver.mkConst(boolSort));
899
2
  ASSERT_NO_THROW(d_solver.mkConst(funSort));
900
2
  ASSERT_NO_THROW(d_solver.mkConst(boolSort, std::string("b")));
901
2
  ASSERT_NO_THROW(d_solver.mkConst(intSort, std::string("i")));
902
2
  ASSERT_NO_THROW(d_solver.mkConst(funSort, "f"));
903
2
  ASSERT_NO_THROW(d_solver.mkConst(funSort, ""));
904
4
  ASSERT_THROW(d_solver.mkConst(Sort()), CVC4ApiException);
905
4
  ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC4ApiException);
906
907
4
  Solver slv;
908
4
  ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException);
909
}
910
911
140
TEST_F(TestApiBlackSolver, mkConstArray)
912
{
913
4
  Sort intSort = d_solver.getIntegerSort();
914
4
  Sort arrSort = d_solver.mkArraySort(intSort, intSort);
915
4
  Term zero = d_solver.mkInteger(0);
916
4
  Term constArr = d_solver.mkConstArray(arrSort, zero);
917
918
2
  ASSERT_NO_THROW(d_solver.mkConstArray(arrSort, zero));
919
4
  ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC4ApiException);
920
4
  ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC4ApiException);
921
4
  ASSERT_THROW(d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)),
922
2
               CVC4ApiException);
923
4
  ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC4ApiException);
924
4
  Solver slv;
925
4
  Term zero2 = slv.mkInteger(0);
926
4
  Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
927
4
  ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC4ApiException);
928
4
  ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException);
929
}
930
931
140
TEST_F(TestApiBlackSolver, declareDatatype)
932
{
933
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
934
4
  std::vector<DatatypeConstructorDecl> ctors1 = {nil};
935
2
  ASSERT_NO_THROW(d_solver.declareDatatype(std::string("a"), ctors1));
936
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
937
4
  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
938
4
  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
939
2
  ASSERT_NO_THROW(d_solver.declareDatatype(std::string("b"), ctors2));
940
4
  DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
941
4
  DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
942
4
  std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
943
2
  ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3));
944
4
  std::vector<DatatypeConstructorDecl> ctors4;
945
4
  ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4),
946
2
               CVC4ApiException);
947
4
  ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4),
948
2
               CVC4ApiException);
949
4
  Solver slv;
950
4
  ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException);
951
}
952
953
140
TEST_F(TestApiBlackSolver, declareFun)
954
{
955
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
956
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
957
8
                                         d_solver.getIntegerSort());
958
2
  ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
959
2
  ASSERT_NO_THROW(
960
      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
961
4
  ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException);
962
  // functions as arguments is allowed
963
2
  ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort));
964
4
  ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
965
2
               CVC4ApiException);
966
4
  Solver slv;
967
4
  ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException);
968
}
969
970
140
TEST_F(TestApiBlackSolver, declareSort)
971
{
972
2
  ASSERT_NO_THROW(d_solver.declareSort("s", 0));
973
2
  ASSERT_NO_THROW(d_solver.declareSort("s", 2));
974
2
  ASSERT_NO_THROW(d_solver.declareSort("", 2));
975
}
976
977
140
TEST_F(TestApiBlackSolver, defineSort)
978
{
979
4
  Sort sortVar0 = d_solver.mkParamSort("T0");
980
4
  Sort sortVar1 = d_solver.mkParamSort("T1");
981
4
  Sort intSort = d_solver.getIntegerSort();
982
4
  Sort realSort = d_solver.getRealSort();
983
4
  Sort arraySort0 = d_solver.mkArraySort(sortVar0, sortVar0);
984
4
  Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
985
  // Now create instantiations of the defined sorts
986
2
  ASSERT_NO_THROW(arraySort0.substitute(sortVar0, intSort));
987
2
  ASSERT_NO_THROW(
988
      arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
989
}
990
991
140
TEST_F(TestApiBlackSolver, defineFun)
992
{
993
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
994
4
  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
995
4
  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
996
8
                                          d_solver.getIntegerSort());
997
4
  Term b1 = d_solver.mkVar(bvSort, "b1");
998
4
  Term b11 = d_solver.mkVar(bvSort, "b1");
999
4
  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
1000
4
  Term b3 = d_solver.mkVar(funSort2, "b3");
1001
4
  Term v1 = d_solver.mkConst(bvSort, "v1");
1002
4
  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
1003
4
  Term v3 = d_solver.mkConst(funSort2, "v3");
1004
4
  Term f1 = d_solver.mkConst(funSort1, "f1");
1005
4
  Term f2 = d_solver.mkConst(funSort2, "f2");
1006
4
  Term f3 = d_solver.mkConst(bvSort, "f3");
1007
2
  ASSERT_NO_THROW(d_solver.defineFun("f", {}, bvSort, v1));
1008
2
  ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
1009
2
  ASSERT_NO_THROW(d_solver.defineFun(f1, {b1, b11}, v1));
1010
4
  ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1),
1011
2
               CVC4ApiException);
1012
4
  ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException);
1013
4
  ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3),
1014
2
               CVC4ApiException);
1015
  // b3 has function sort, which is allowed as an argument
1016
2
  ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1));
1017
4
  ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException);
1018
4
  ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException);
1019
4
  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException);
1020
4
  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException);
1021
4
  ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException);
1022
4
  ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException);
1023
1024
4
  Solver slv;
1025
4
  Sort bvSort2 = slv.mkBitVectorSort(32);
1026
4
  Term v12 = slv.mkConst(bvSort2, "v1");
1027
4
  Term b12 = slv.mkVar(bvSort2, "b1");
1028
4
  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
1029
4
  ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException);
1030
4
  ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException);
1031
4
  ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC4ApiException);
1032
4
  ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC4ApiException);
1033
4
  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC4ApiException);
1034
4
  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException);
1035
}
1036
1037
140
TEST_F(TestApiBlackSolver, defineFunGlobal)
1038
{
1039
4
  Sort bSort = d_solver.getBooleanSort();
1040
4
  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
1041
1042
4
  Term bTrue = d_solver.mkBoolean(true);
1043
  // (define-fun f () Bool true)
1044
4
  Term f = d_solver.defineFun("f", {}, bSort, bTrue, true);
1045
4
  Term b = d_solver.mkVar(bSort, "b");
1046
4
  Term gSym = d_solver.mkConst(fSort, "g");
1047
  // (define-fun g (b Bool) Bool b)
1048
4
  Term g = d_solver.defineFun(gSym, {b}, b, true);
1049
1050
  // (assert (or (not f) (not (g true))))
1051
4
  d_solver.assertFormula(d_solver.mkTerm(
1052
4
      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
1053
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1054
2
  d_solver.resetAssertions();
1055
  // (assert (or (not f) (not (g true))))
1056
4
  d_solver.assertFormula(d_solver.mkTerm(
1057
4
      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
1058
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1059
}
1060
1061
140
TEST_F(TestApiBlackSolver, defineFunRec)
1062
{
1063
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
1064
4
  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
1065
4
  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
1066
8
                                          d_solver.getIntegerSort());
1067
4
  Term b1 = d_solver.mkVar(bvSort, "b1");
1068
4
  Term b11 = d_solver.mkVar(bvSort, "b1");
1069
4
  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
1070
4
  Term b3 = d_solver.mkVar(funSort2, "b3");
1071
4
  Term v1 = d_solver.mkConst(bvSort, "v1");
1072
4
  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
1073
4
  Term v3 = d_solver.mkConst(funSort2, "v3");
1074
4
  Term f1 = d_solver.mkConst(funSort1, "f1");
1075
4
  Term f2 = d_solver.mkConst(funSort2, "f2");
1076
4
  Term f3 = d_solver.mkConst(bvSort, "f3");
1077
2
  ASSERT_NO_THROW(d_solver.defineFunRec("f", {}, bvSort, v1));
1078
2
  ASSERT_NO_THROW(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
1079
2
  ASSERT_NO_THROW(d_solver.defineFunRec(f1, {b1, b11}, v1));
1080
4
  ASSERT_THROW(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
1081
2
               CVC4ApiException);
1082
4
  ASSERT_THROW(d_solver.defineFunRec("ff", {b1, v2}, bvSort, v1),
1083
2
               CVC4ApiException);
1084
4
  ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
1085
2
               CVC4ApiException);
1086
  // b3 has function sort, which is allowed as an argument
1087
2
  ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1));
1088
4
  ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException);
1089
4
  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException);
1090
4
  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException);
1091
4
  ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException);
1092
4
  ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException);
1093
1094
4
  Solver slv;
1095
4
  Sort bvSort2 = slv.mkBitVectorSort(32);
1096
4
  Term v12 = slv.mkConst(bvSort2, "v1");
1097
4
  Term b12 = slv.mkVar(bvSort2, "b1");
1098
4
  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
1099
2
  ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12));
1100
2
  ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
1101
4
  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException);
1102
4
  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException);
1103
4
  ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
1104
2
               CVC4ApiException);
1105
4
  ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
1106
2
               CVC4ApiException);
1107
4
  ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
1108
2
               CVC4ApiException);
1109
4
  ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
1110
2
               CVC4ApiException);
1111
}
1112
1113
140
TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
1114
{
1115
2
  d_solver.setLogic("QF_BV");
1116
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
1117
4
  Sort funSort = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
1118
4
  Term b = d_solver.mkVar(bvSort, "b");
1119
4
  Term v = d_solver.mkConst(bvSort, "v");
1120
4
  Term f = d_solver.mkConst(funSort, "f");
1121
4
  ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC4ApiException);
1122
4
  ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException);
1123
}
1124
1125
140
TEST_F(TestApiBlackSolver, defineFunRecGlobal)
1126
{
1127
4
  Sort bSort = d_solver.getBooleanSort();
1128
4
  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
1129
1130
2
  d_solver.push();
1131
4
  Term bTrue = d_solver.mkBoolean(true);
1132
  // (define-fun f () Bool true)
1133
4
  Term f = d_solver.defineFunRec("f", {}, bSort, bTrue, true);
1134
4
  Term b = d_solver.mkVar(bSort, "b");
1135
4
  Term gSym = d_solver.mkConst(fSort, "g");
1136
  // (define-fun g (b Bool) Bool b)
1137
4
  Term g = d_solver.defineFunRec(gSym, {b}, b, true);
1138
1139
  // (assert (or (not f) (not (g true))))
1140
4
  d_solver.assertFormula(d_solver.mkTerm(
1141
4
      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
1142
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1143
2
  d_solver.pop();
1144
  // (assert (or (not f) (not (g true))))
1145
4
  d_solver.assertFormula(d_solver.mkTerm(
1146
4
      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
1147
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1148
}
1149
1150
140
TEST_F(TestApiBlackSolver, defineFunsRec)
1151
{
1152
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1153
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
1154
4
  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
1155
4
  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
1156
4
  Term b1 = d_solver.mkVar(bvSort, "b1");
1157
4
  Term b11 = d_solver.mkVar(bvSort, "b1");
1158
4
  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
1159
4
  Term b3 = d_solver.mkVar(funSort2, "b3");
1160
4
  Term b4 = d_solver.mkVar(uSort, "b4");
1161
4
  Term v1 = d_solver.mkConst(bvSort, "v1");
1162
4
  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
1163
4
  Term v3 = d_solver.mkConst(funSort2, "v3");
1164
4
  Term v4 = d_solver.mkConst(uSort, "v4");
1165
4
  Term f1 = d_solver.mkConst(funSort1, "f1");
1166
4
  Term f2 = d_solver.mkConst(funSort2, "f2");
1167
4
  Term f3 = d_solver.mkConst(bvSort, "f3");
1168
2
  ASSERT_NO_THROW(
1169
      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
1170
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
1171
2
               CVC4ApiException);
1172
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
1173
2
               CVC4ApiException);
1174
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
1175
2
               CVC4ApiException);
1176
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
1177
2
               CVC4ApiException);
1178
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
1179
2
               CVC4ApiException);
1180
1181
4
  Solver slv;
1182
4
  Sort uSort2 = slv.mkUninterpretedSort("u");
1183
4
  Sort bvSort2 = slv.mkBitVectorSort(32);
1184
4
  Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
1185
4
  Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
1186
4
  Term b12 = slv.mkVar(bvSort2, "b1");
1187
4
  Term b112 = slv.mkVar(bvSort2, "b1");
1188
4
  Term b42 = slv.mkVar(uSort2, "b4");
1189
4
  Term v12 = slv.mkConst(bvSort2, "v1");
1190
4
  Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
1191
4
  Term f12 = slv.mkConst(funSort12, "f1");
1192
4
  Term f22 = slv.mkConst(funSort22, "f2");
1193
2
  ASSERT_NO_THROW(
1194
      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
1195
4
  ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
1196
2
               CVC4ApiException);
1197
4
  ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
1198
2
               CVC4ApiException);
1199
4
  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
1200
2
               CVC4ApiException);
1201
4
  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
1202
2
               CVC4ApiException);
1203
4
  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
1204
2
               CVC4ApiException);
1205
4
  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
1206
2
               CVC4ApiException);
1207
4
  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
1208
2
               CVC4ApiException);
1209
}
1210
1211
140
TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
1212
{
1213
2
  d_solver.setLogic("QF_BV");
1214
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1215
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
1216
4
  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
1217
4
  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
1218
4
  Term b = d_solver.mkVar(bvSort, "b");
1219
4
  Term u = d_solver.mkVar(uSort, "u");
1220
4
  Term v1 = d_solver.mkConst(bvSort, "v1");
1221
4
  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
1222
4
  Term f1 = d_solver.mkConst(funSort1, "f1");
1223
4
  Term f2 = d_solver.mkConst(funSort2, "f2");
1224
4
  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
1225
2
               CVC4ApiException);
1226
}
1227
1228
140
TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
1229
{
1230
4
  Sort bSort = d_solver.getBooleanSort();
1231
4
  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
1232
1233
2
  d_solver.push();
1234
4
  Term bTrue = d_solver.mkBoolean(true);
1235
4
  Term b = d_solver.mkVar(bSort, "b");
1236
4
  Term gSym = d_solver.mkConst(fSort, "g");
1237
  // (define-funs-rec ((g ((b Bool)) Bool)) (b))
1238
2
  d_solver.defineFunsRec({gSym}, {{b}}, {b}, true);
1239
1240
  // (assert (not (g true)))
1241
2
  d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
1242
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1243
2
  d_solver.pop();
1244
  // (assert (not (g true)))
1245
2
  d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
1246
2
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1247
}
1248
1249
140
TEST_F(TestApiBlackSolver, uFIteration)
1250
{
1251
4
  Sort intSort = d_solver.getIntegerSort();
1252
4
  Sort funSort = d_solver.mkFunctionSort({intSort, intSort}, intSort);
1253
4
  Term x = d_solver.mkConst(intSort, "x");
1254
4
  Term y = d_solver.mkConst(intSort, "y");
1255
4
  Term f = d_solver.mkConst(funSort, "f");
1256
4
  Term fxy = d_solver.mkTerm(APPLY_UF, f, x, y);
1257
1258
  // Expecting the uninterpreted function to be one of the children
1259
8
  Term expected_children[3] = {f, x, y};
1260
2
  uint32_t idx = 0;
1261
8
  for (auto c : fxy)
1262
  {
1263
6
    ASSERT_LT(idx, 3);
1264
6
    ASSERT_EQ(c, expected_children[idx]);
1265
6
    idx++;
1266
  }
1267
}
1268
1269
140
TEST_F(TestApiBlackSolver, getInfo)
1270
{
1271
2
  ASSERT_NO_THROW(d_solver.getInfo("name"));
1272
4
  ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException);
1273
}
1274
1275
140
TEST_F(TestApiBlackSolver, getInterpolant)
1276
{
1277
2
  d_solver.setLogic("QF_LIA");
1278
2
  d_solver.setOption("produce-interpols", "default");
1279
2
  d_solver.setOption("incremental", "false");
1280
1281
4
  Sort intSort = d_solver.getIntegerSort();
1282
4
  Term zero = d_solver.mkInteger(0);
1283
4
  Term x = d_solver.mkConst(intSort, "x");
1284
4
  Term y = d_solver.mkConst(intSort, "y");
1285
4
  Term z = d_solver.mkConst(intSort, "z");
1286
1287
  // Assumptions for interpolation: x + y > 0 /\ x < 0
1288
4
  d_solver.assertFormula(
1289
4
      d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
1290
2
  d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
1291
  // Conjecture for interpolation: y + z > 0 \/ z < 0
1292
  Term conj =
1293
      d_solver.mkTerm(OR,
1294
4
                      d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero),
1295
8
                      d_solver.mkTerm(LT, z, zero));
1296
4
  Term output;
1297
  // Call the interpolation api, while the resulting interpolant is the output
1298
2
  d_solver.getInterpolant(conj, output);
1299
1300
  // We expect the resulting output to be a boolean formula
1301
2
  ASSERT_TRUE(output.getSort().isBoolean());
1302
}
1303
1304
140
TEST_F(TestApiBlackSolver, getOp)
1305
{
1306
4
  Sort bv32 = d_solver.mkBitVectorSort(32);
1307
4
  Term a = d_solver.mkConst(bv32, "a");
1308
4
  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
1309
4
  Term exta = d_solver.mkTerm(ext, a);
1310
1311
2
  ASSERT_FALSE(a.hasOp());
1312
4
  ASSERT_THROW(a.getOp(), CVC4ApiException);
1313
2
  ASSERT_TRUE(exta.hasOp());
1314
2
  ASSERT_EQ(exta.getOp(), ext);
1315
1316
  // Test Datatypes -- more complicated
1317
4
  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
1318
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
1319
2
  cons.addSelector("head", d_solver.getIntegerSort());
1320
2
  cons.addSelectorSelf("tail");
1321
2
  consListSpec.addConstructor(cons);
1322
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
1323
2
  consListSpec.addConstructor(nil);
1324
4
  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
1325
4
  Datatype consList = consListSort.getDatatype();
1326
1327
4
  Term consTerm = consList.getConstructorTerm("cons");
1328
4
  Term nilTerm = consList.getConstructorTerm("nil");
1329
4
  Term headTerm = consList["cons"].getSelectorTerm("head");
1330
1331
4
  Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
1332
  Term listcons1 = d_solver.mkTerm(
1333
4
      APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
1334
4
  Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
1335
1336
2
  ASSERT_TRUE(listnil.hasOp());
1337
2
  ASSERT_TRUE(listcons1.hasOp());
1338
2
  ASSERT_TRUE(listhead.hasOp());
1339
}
1340
1341
140
TEST_F(TestApiBlackSolver, getOption)
1342
{
1343
2
  ASSERT_NO_THROW(d_solver.getOption("incremental"));
1344
4
  ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException);
1345
}
1346
1347
140
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
1348
{
1349
#if IS_PROOFS_BUILD
1350
  d_solver.setOption("incremental", "false");
1351
  d_solver.checkSatAssuming(d_solver.mkFalse());
1352
  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
1353
#endif
1354
2
}
1355
1356
140
TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
1357
{
1358
#if IS_PROOFS_BUILD
1359
  d_solver.setOption("incremental", "true");
1360
  d_solver.setOption("produce-unsat-assumptions", "false");
1361
  d_solver.checkSatAssuming(d_solver.mkFalse());
1362
  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
1363
#endif
1364
2
}
1365
1366
140
TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
1367
{
1368
#if IS_PROOFS_BUILD
1369
  d_solver.setOption("incremental", "true");
1370
  d_solver.setOption("produce-unsat-assumptions", "true");
1371
  d_solver.checkSatAssuming(d_solver.mkFalse());
1372
  ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
1373
  d_solver.checkSatAssuming(d_solver.mkTrue());
1374
  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
1375
#endif
1376
2
}
1377
1378
140
TEST_F(TestApiBlackSolver, getUnsatCore1)
1379
{
1380
#if IS_PROOFS_BUILD
1381
  d_solver.setOption("incremental", "false");
1382
  d_solver.assertFormula(d_solver.mkFalse());
1383
  d_solver.checkSat();
1384
  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
1385
#endif
1386
2
}
1387
1388
140
TEST_F(TestApiBlackSolver, getUnsatCore2)
1389
{
1390
#if IS_PROOFS_BUILD
1391
  d_solver.setOption("incremental", "false");
1392
  d_solver.setOption("produce-unsat-cores", "false");
1393
  d_solver.assertFormula(d_solver.mkFalse());
1394
  d_solver.checkSat();
1395
  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
1396
#endif
1397
2
}
1398
1399
140
TEST_F(TestApiBlackSolver, getUnsatCore3)
1400
{
1401
#if IS_PROOFS_BUILD
1402
  d_solver.setOption("incremental", "true");
1403
  d_solver.setOption("produce-unsat-cores", "true");
1404
1405
  Sort uSort = d_solver.mkUninterpretedSort("u");
1406
  Sort intSort = d_solver.getIntegerSort();
1407
  Sort boolSort = d_solver.getBooleanSort();
1408
  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
1409
  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
1410
  std::vector<Term> unsat_core;
1411
1412
  Term x = d_solver.mkConst(uSort, "x");
1413
  Term y = d_solver.mkConst(uSort, "y");
1414
  Term f = d_solver.mkConst(uToIntSort, "f");
1415
  Term p = d_solver.mkConst(intPredSort, "p");
1416
  Term zero = d_solver.mkInteger(0);
1417
  Term one = d_solver.mkInteger(1);
1418
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
1419
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
1420
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
1421
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
1422
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
1423
  d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x));
1424
  d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y));
1425
  d_solver.assertFormula(d_solver.mkTerm(GT, sum, one));
1426
  d_solver.assertFormula(p_0);
1427
  d_solver.assertFormula(p_f_y.notTerm());
1428
  ASSERT_TRUE(d_solver.checkSat().isUnsat());
1429
1430
  ASSERT_NO_THROW(unsat_core = d_solver.getUnsatCore());
1431
1432
  d_solver.resetAssertions();
1433
  for (const auto& t : unsat_core)
1434
  {
1435
    d_solver.assertFormula(t);
1436
  }
1437
  Result res = d_solver.checkSat();
1438
  ASSERT_TRUE(res.isUnsat());
1439
#endif
1440
2
}
1441
1442
140
TEST_F(TestApiBlackSolver, getValue1)
1443
{
1444
2
  d_solver.setOption("produce-models", "false");
1445
4
  Term t = d_solver.mkTrue();
1446
2
  d_solver.assertFormula(t);
1447
2
  d_solver.checkSat();
1448
4
  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
1449
}
1450
1451
140
TEST_F(TestApiBlackSolver, getValue2)
1452
{
1453
2
  d_solver.setOption("produce-models", "true");
1454
4
  Term t = d_solver.mkFalse();
1455
2
  d_solver.assertFormula(t);
1456
2
  d_solver.checkSat();
1457
4
  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
1458
}
1459
1460
140
TEST_F(TestApiBlackSolver, getValue3)
1461
{
1462
2
  d_solver.setOption("produce-models", "true");
1463
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1464
4
  Sort intSort = d_solver.getIntegerSort();
1465
4
  Sort boolSort = d_solver.getBooleanSort();
1466
4
  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
1467
4
  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
1468
4
  std::vector<Term> unsat_core;
1469
1470
4
  Term x = d_solver.mkConst(uSort, "x");
1471
4
  Term y = d_solver.mkConst(uSort, "y");
1472
4
  Term z = d_solver.mkConst(uSort, "z");
1473
4
  Term f = d_solver.mkConst(uToIntSort, "f");
1474
4
  Term p = d_solver.mkConst(intPredSort, "p");
1475
4
  Term zero = d_solver.mkInteger(0);
1476
4
  Term one = d_solver.mkInteger(1);
1477
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
1478
4
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
1479
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
1480
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
1481
4
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
1482
1483
2
  d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_x));
1484
2
  d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_y));
1485
2
  d_solver.assertFormula(d_solver.mkTerm(LEQ, sum, one));
1486
2
  d_solver.assertFormula(p_0.notTerm());
1487
2
  d_solver.assertFormula(p_f_y);
1488
2
  ASSERT_TRUE(d_solver.checkSat().isSat());
1489
2
  ASSERT_NO_THROW(d_solver.getValue(x));
1490
2
  ASSERT_NO_THROW(d_solver.getValue(y));
1491
2
  ASSERT_NO_THROW(d_solver.getValue(z));
1492
2
  ASSERT_NO_THROW(d_solver.getValue(sum));
1493
2
  ASSERT_NO_THROW(d_solver.getValue(p_f_y));
1494
1495
4
  Solver slv;
1496
4
  ASSERT_THROW(slv.getValue(x), CVC4ApiException);
1497
}
1498
1499
140
TEST_F(TestApiBlackSolver, getQuantifierElimination)
1500
{
1501
4
  Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
1502
  Term forall =
1503
      d_solver.mkTerm(FORALL,
1504
4
                      d_solver.mkTerm(BOUND_VAR_LIST, x),
1505
8
                      d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
1506
4
  ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC4ApiException);
1507
4
  ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)),
1508
2
               CVC4ApiException);
1509
2
  ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
1510
}
1511
1512
140
TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
1513
{
1514
4
  Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
1515
  Term forall =
1516
      d_solver.mkTerm(FORALL,
1517
4
                      d_solver.mkTerm(BOUND_VAR_LIST, x),
1518
8
                      d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
1519
4
  ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()),
1520
2
               CVC4ApiException);
1521
4
  ASSERT_THROW(
1522
      d_solver.getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
1523
2
      CVC4ApiException);
1524
2
  ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
1525
}
1526
1527
140
TEST_F(TestApiBlackSolver, declareSeparationHeap)
1528
{
1529
2
  d_solver.setLogic("ALL_SUPPORTED");
1530
4
  Sort integer = d_solver.getIntegerSort();
1531
2
  ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer));
1532
  // cannot declare separation logic heap more than once
1533
4
  ASSERT_THROW(d_solver.declareSeparationHeap(integer, integer),
1534
2
               CVC4ApiException);
1535
}
1536
1537
namespace {
1538
/**
1539
 * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
1540
 * some simple separation logic constraints.
1541
 */
1542
8
void checkSimpleSeparationConstraints(Solver* solver)
1543
{
1544
16
  Sort integer = solver->getIntegerSort();
1545
  // declare the separation heap
1546
8
  solver->declareSeparationHeap(integer, integer);
1547
16
  Term x = solver->mkConst(integer, "x");
1548
16
  Term p = solver->mkConst(integer, "p");
1549
16
  Term heap = solver->mkTerm(CVC4::api::Kind::SEP_PTO, p, x);
1550
8
  solver->assertFormula(heap);
1551
16
  Term nil = solver->mkSepNil(integer);
1552
8
  solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
1553
8
  solver->checkSat();
1554
8
}
1555
}  // namespace
1556
1557
140
TEST_F(TestApiBlackSolver, getSeparationHeapTerm1)
1558
{
1559
2
  d_solver.setLogic("QF_BV");
1560
2
  d_solver.setOption("incremental", "false");
1561
2
  d_solver.setOption("produce-models", "true");
1562
4
  Term t = d_solver.mkTrue();
1563
2
  d_solver.assertFormula(t);
1564
4
  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
1565
}
1566
1567
140
TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
1568
{
1569
2
  d_solver.setLogic("ALL_SUPPORTED");
1570
2
  d_solver.setOption("incremental", "false");
1571
2
  d_solver.setOption("produce-models", "false");
1572
2
  checkSimpleSeparationConstraints(&d_solver);
1573
4
  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
1574
}
1575
1576
140
TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
1577
{
1578
2
  d_solver.setLogic("ALL_SUPPORTED");
1579
2
  d_solver.setOption("incremental", "false");
1580
2
  d_solver.setOption("produce-models", "true");
1581
4
  Term t = d_solver.mkFalse();
1582
2
  d_solver.assertFormula(t);
1583
2
  d_solver.checkSat();
1584
4
  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
1585
}
1586
1587
140
TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
1588
{
1589
2
  d_solver.setLogic("ALL_SUPPORTED");
1590
2
  d_solver.setOption("incremental", "false");
1591
2
  d_solver.setOption("produce-models", "true");
1592
4
  Term t = d_solver.mkTrue();
1593
2
  d_solver.assertFormula(t);
1594
2
  d_solver.checkSat();
1595
4
  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
1596
}
1597
1598
140
TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
1599
{
1600
2
  d_solver.setLogic("ALL_SUPPORTED");
1601
2
  d_solver.setOption("incremental", "false");
1602
2
  d_solver.setOption("produce-models", "true");
1603
2
  checkSimpleSeparationConstraints(&d_solver);
1604
2
  ASSERT_NO_THROW(d_solver.getSeparationHeap());
1605
}
1606
1607
140
TEST_F(TestApiBlackSolver, getSeparationNilTerm1)
1608
{
1609
2
  d_solver.setLogic("QF_BV");
1610
2
  d_solver.setOption("incremental", "false");
1611
2
  d_solver.setOption("produce-models", "true");
1612
4
  Term t = d_solver.mkTrue();
1613
2
  d_solver.assertFormula(t);
1614
4
  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
1615
}
1616
1617
140
TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
1618
{
1619
2
  d_solver.setLogic("ALL_SUPPORTED");
1620
2
  d_solver.setOption("incremental", "false");
1621
2
  d_solver.setOption("produce-models", "false");
1622
2
  checkSimpleSeparationConstraints(&d_solver);
1623
4
  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
1624
}
1625
1626
140
TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
1627
{
1628
2
  d_solver.setLogic("ALL_SUPPORTED");
1629
2
  d_solver.setOption("incremental", "false");
1630
2
  d_solver.setOption("produce-models", "true");
1631
4
  Term t = d_solver.mkFalse();
1632
2
  d_solver.assertFormula(t);
1633
2
  d_solver.checkSat();
1634
4
  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
1635
}
1636
1637
140
TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
1638
{
1639
2
  d_solver.setLogic("ALL_SUPPORTED");
1640
2
  d_solver.setOption("incremental", "false");
1641
2
  d_solver.setOption("produce-models", "true");
1642
4
  Term t = d_solver.mkTrue();
1643
2
  d_solver.assertFormula(t);
1644
2
  d_solver.checkSat();
1645
4
  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
1646
}
1647
1648
140
TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
1649
{
1650
2
  d_solver.setLogic("ALL_SUPPORTED");
1651
2
  d_solver.setOption("incremental", "false");
1652
2
  d_solver.setOption("produce-models", "true");
1653
2
  checkSimpleSeparationConstraints(&d_solver);
1654
2
  ASSERT_NO_THROW(d_solver.getSeparationNilTerm());
1655
}
1656
1657
140
TEST_F(TestApiBlackSolver, push1)
1658
{
1659
2
  d_solver.setOption("incremental", "true");
1660
2
  ASSERT_NO_THROW(d_solver.push(1));
1661
4
  ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC4ApiException);
1662
4
  ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException);
1663
}
1664
1665
140
TEST_F(TestApiBlackSolver, push2)
1666
{
1667
2
  d_solver.setOption("incremental", "false");
1668
4
  ASSERT_THROW(d_solver.push(1), CVC4ApiException);
1669
}
1670
1671
140
TEST_F(TestApiBlackSolver, pop1)
1672
{
1673
2
  d_solver.setOption("incremental", "false");
1674
4
  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
1675
}
1676
1677
140
TEST_F(TestApiBlackSolver, pop2)
1678
{
1679
2
  d_solver.setOption("incremental", "true");
1680
4
  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
1681
}
1682
1683
140
TEST_F(TestApiBlackSolver, pop3)
1684
{
1685
2
  d_solver.setOption("incremental", "true");
1686
2
  ASSERT_NO_THROW(d_solver.push(1));
1687
2
  ASSERT_NO_THROW(d_solver.pop(1));
1688
4
  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
1689
}
1690
1691
140
TEST_F(TestApiBlackSolver, blockModel1)
1692
{
1693
2
  d_solver.setOption("produce-models", "true");
1694
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1695
2
  d_solver.assertFormula(x.eqTerm(x));
1696
2
  d_solver.checkSat();
1697
4
  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
1698
}
1699
1700
140
TEST_F(TestApiBlackSolver, blockModel2)
1701
{
1702
2
  d_solver.setOption("block-models", "literals");
1703
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1704
2
  d_solver.assertFormula(x.eqTerm(x));
1705
2
  d_solver.checkSat();
1706
4
  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
1707
}
1708
1709
140
TEST_F(TestApiBlackSolver, blockModel3)
1710
{
1711
2
  d_solver.setOption("produce-models", "true");
1712
2
  d_solver.setOption("block-models", "literals");
1713
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1714
2
  d_solver.assertFormula(x.eqTerm(x));
1715
4
  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
1716
}
1717
1718
140
TEST_F(TestApiBlackSolver, blockModel4)
1719
{
1720
2
  d_solver.setOption("produce-models", "true");
1721
2
  d_solver.setOption("block-models", "literals");
1722
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1723
2
  d_solver.assertFormula(x.eqTerm(x));
1724
2
  d_solver.checkSat();
1725
2
  ASSERT_NO_THROW(d_solver.blockModel());
1726
}
1727
1728
140
TEST_F(TestApiBlackSolver, blockModelValues1)
1729
{
1730
2
  d_solver.setOption("produce-models", "true");
1731
2
  d_solver.setOption("block-models", "literals");
1732
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1733
2
  d_solver.assertFormula(x.eqTerm(x));
1734
2
  d_solver.checkSat();
1735
4
  ASSERT_THROW(d_solver.blockModelValues({}), CVC4ApiException);
1736
4
  ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC4ApiException);
1737
4
  ASSERT_THROW(d_solver.blockModelValues({Solver().mkBoolean(false)}),
1738
2
               CVC4ApiException);
1739
}
1740
1741
140
TEST_F(TestApiBlackSolver, blockModelValues2)
1742
{
1743
2
  d_solver.setOption("produce-models", "true");
1744
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1745
2
  d_solver.assertFormula(x.eqTerm(x));
1746
2
  d_solver.checkSat();
1747
4
  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
1748
}
1749
1750
140
TEST_F(TestApiBlackSolver, blockModelValues3)
1751
{
1752
2
  d_solver.setOption("block-models", "literals");
1753
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1754
2
  d_solver.assertFormula(x.eqTerm(x));
1755
2
  d_solver.checkSat();
1756
4
  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
1757
}
1758
1759
140
TEST_F(TestApiBlackSolver, blockModelValues4)
1760
{
1761
2
  d_solver.setOption("produce-models", "true");
1762
2
  d_solver.setOption("block-models", "literals");
1763
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1764
2
  d_solver.assertFormula(x.eqTerm(x));
1765
4
  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
1766
}
1767
1768
140
TEST_F(TestApiBlackSolver, blockModelValues5)
1769
{
1770
2
  d_solver.setOption("produce-models", "true");
1771
2
  d_solver.setOption("block-models", "literals");
1772
4
  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
1773
2
  d_solver.assertFormula(x.eqTerm(x));
1774
2
  d_solver.checkSat();
1775
2
  ASSERT_NO_THROW(d_solver.blockModelValues({x}));
1776
}
1777
1778
140
TEST_F(TestApiBlackSolver, setInfo)
1779
{
1780
4
  ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException);
1781
4
  ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException);
1782
4
  ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC4ApiException);
1783
1784
2
  ASSERT_NO_THROW(d_solver.setInfo("source", "asdf"));
1785
2
  ASSERT_NO_THROW(d_solver.setInfo("category", "asdf"));
1786
2
  ASSERT_NO_THROW(d_solver.setInfo("difficulty", "asdf"));
1787
2
  ASSERT_NO_THROW(d_solver.setInfo("filename", "asdf"));
1788
2
  ASSERT_NO_THROW(d_solver.setInfo("license", "asdf"));
1789
2
  ASSERT_NO_THROW(d_solver.setInfo("name", "asdf"));
1790
2
  ASSERT_NO_THROW(d_solver.setInfo("notes", "asdf"));
1791
1792
2
  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2"));
1793
2
  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.0"));
1794
2
  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.5"));
1795
2
  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.6"));
1796
4
  ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC4ApiException);
1797
1798
2
  ASSERT_NO_THROW(d_solver.setInfo("status", "sat"));
1799
2
  ASSERT_NO_THROW(d_solver.setInfo("status", "unsat"));
1800
2
  ASSERT_NO_THROW(d_solver.setInfo("status", "unknown"));
1801
4
  ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException);
1802
}
1803
1804
140
TEST_F(TestApiBlackSolver, simplify)
1805
{
1806
4
  ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException);
1807
1808
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
1809
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1810
4
  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
1811
4
  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
1812
4
  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
1813
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
1814
2
  cons.addSelector("head", d_solver.getIntegerSort());
1815
2
  cons.addSelectorSelf("tail");
1816
2
  consListSpec.addConstructor(cons);
1817
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
1818
2
  consListSpec.addConstructor(nil);
1819
4
  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
1820
1821
4
  Term x = d_solver.mkConst(bvSort, "x");
1822
2
  ASSERT_NO_THROW(d_solver.simplify(x));
1823
4
  Term a = d_solver.mkConst(bvSort, "a");
1824
2
  ASSERT_NO_THROW(d_solver.simplify(a));
1825
4
  Term b = d_solver.mkConst(bvSort, "b");
1826
2
  ASSERT_NO_THROW(d_solver.simplify(b));
1827
4
  Term x_eq_x = d_solver.mkTerm(EQUAL, x, x);
1828
2
  ASSERT_NO_THROW(d_solver.simplify(x_eq_x));
1829
2
  ASSERT_NE(d_solver.mkTrue(), x_eq_x);
1830
2
  ASSERT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
1831
4
  Term x_eq_b = d_solver.mkTerm(EQUAL, x, b);
1832
2
  ASSERT_NO_THROW(d_solver.simplify(x_eq_b));
1833
2
  ASSERT_NE(d_solver.mkTrue(), x_eq_b);
1834
2
  ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
1835
4
  Solver slv;
1836
4
  ASSERT_THROW(slv.simplify(x), CVC4ApiException);
1837
1838
4
  Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
1839
2
  ASSERT_NO_THROW(d_solver.simplify(i1));
1840
4
  Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23"));
1841
2
  ASSERT_NO_THROW(d_solver.simplify(i2));
1842
2
  ASSERT_NE(i1, i2);
1843
2
  ASSERT_NE(i1, d_solver.simplify(i2));
1844
4
  Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
1845
2
  ASSERT_NO_THROW(d_solver.simplify(i3));
1846
2
  ASSERT_NE(i1, i3);
1847
2
  ASSERT_EQ(i1, d_solver.simplify(i3));
1848
1849
4
  Datatype consList = consListSort.getDatatype();
1850
  Term dt1 = d_solver.mkTerm(
1851
      APPLY_CONSTRUCTOR,
1852
4
      consList.getConstructorTerm("cons"),
1853
4
      d_solver.mkInteger(0),
1854
8
      d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
1855
2
  ASSERT_NO_THROW(d_solver.simplify(dt1));
1856
  Term dt2 = d_solver.mkTerm(
1857
4
      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
1858
2
  ASSERT_NO_THROW(d_solver.simplify(dt2));
1859
1860
4
  Term b1 = d_solver.mkVar(bvSort, "b1");
1861
2
  ASSERT_NO_THROW(d_solver.simplify(b1));
1862
4
  Term b2 = d_solver.mkVar(bvSort, "b1");
1863
2
  ASSERT_NO_THROW(d_solver.simplify(b2));
1864
4
  Term b3 = d_solver.mkVar(uSort, "b3");
1865
2
  ASSERT_NO_THROW(d_solver.simplify(b3));
1866
4
  Term v1 = d_solver.mkConst(bvSort, "v1");
1867
2
  ASSERT_NO_THROW(d_solver.simplify(v1));
1868
4
  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
1869
2
  ASSERT_NO_THROW(d_solver.simplify(v2));
1870
4
  Term f1 = d_solver.mkConst(funSort1, "f1");
1871
2
  ASSERT_NO_THROW(d_solver.simplify(f1));
1872
4
  Term f2 = d_solver.mkConst(funSort2, "f2");
1873
2
  ASSERT_NO_THROW(d_solver.simplify(f2));
1874
2
  d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
1875
2
  ASSERT_NO_THROW(d_solver.simplify(f1));
1876
2
  ASSERT_NO_THROW(d_solver.simplify(f2));
1877
}
1878
1879
140
TEST_F(TestApiBlackSolver, assertFormula)
1880
{
1881
2
  ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
1882
4
  ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException);
1883
4
  Solver slv;
1884
4
  ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException);
1885
}
1886
1887
140
TEST_F(TestApiBlackSolver, checkEntailed)
1888
{
1889
2
  d_solver.setOption("incremental", "false");
1890
2
  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
1891
4
  ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
1892
4
  Solver slv;
1893
4
  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
1894
}
1895
1896
140
TEST_F(TestApiBlackSolver, checkEntailed1)
1897
{
1898
4
  Sort boolSort = d_solver.getBooleanSort();
1899
4
  Term x = d_solver.mkConst(boolSort, "x");
1900
4
  Term y = d_solver.mkConst(boolSort, "y");
1901
4
  Term z = d_solver.mkTerm(AND, x, y);
1902
2
  d_solver.setOption("incremental", "true");
1903
2
  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
1904
4
  ASSERT_THROW(d_solver.checkEntailed(Term()), CVC4ApiException);
1905
2
  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
1906
2
  ASSERT_NO_THROW(d_solver.checkEntailed(z));
1907
4
  Solver slv;
1908
4
  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
1909
}
1910
1911
140
TEST_F(TestApiBlackSolver, checkEntailed2)
1912
{
1913
2
  d_solver.setOption("incremental", "true");
1914
1915
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1916
4
  Sort intSort = d_solver.getIntegerSort();
1917
4
  Sort boolSort = d_solver.getBooleanSort();
1918
4
  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
1919
4
  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
1920
1921
4
  Term n = Term();
1922
  // Constants
1923
4
  Term x = d_solver.mkConst(uSort, "x");
1924
4
  Term y = d_solver.mkConst(uSort, "y");
1925
  // Functions
1926
4
  Term f = d_solver.mkConst(uToIntSort, "f");
1927
4
  Term p = d_solver.mkConst(intPredSort, "p");
1928
  // Values
1929
4
  Term zero = d_solver.mkInteger(0);
1930
4
  Term one = d_solver.mkInteger(1);
1931
  // Terms
1932
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
1933
4
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
1934
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
1935
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
1936
4
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
1937
  // Assertions
1938
  Term assertions =
1939
      d_solver.mkTerm(AND,
1940
6
                      std::vector<Term>{
1941
                          d_solver.mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
1942
                          d_solver.mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
1943
                          d_solver.mkTerm(LEQ, sum, one),   // f(x) + f(y) <= 1
1944
                          p_0.notTerm(),                    // not p(0)
1945
                          p_f_y                             // p(f(y))
1946
16
                      });
1947
1948
2
  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
1949
2
  d_solver.assertFormula(assertions);
1950
2
  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y)));
1951
2
  ASSERT_NO_THROW(d_solver.checkEntailed(
1952
      {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
1953
4
  ASSERT_THROW(d_solver.checkEntailed(n), CVC4ApiException);
1954
4
  ASSERT_THROW(d_solver.checkEntailed({n, d_solver.mkTerm(DISTINCT, x, y)}),
1955
2
               CVC4ApiException);
1956
4
  Solver slv;
1957
4
  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
1958
}
1959
1960
140
TEST_F(TestApiBlackSolver, checkSat)
1961
{
1962
2
  d_solver.setOption("incremental", "false");
1963
2
  ASSERT_NO_THROW(d_solver.checkSat());
1964
4
  ASSERT_THROW(d_solver.checkSat(), CVC4ApiException);
1965
}
1966
1967
140
TEST_F(TestApiBlackSolver, checkSatAssuming)
1968
{
1969
2
  d_solver.setOption("incremental", "false");
1970
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
1971
4
  ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
1972
4
  Solver slv;
1973
4
  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
1974
}
1975
1976
140
TEST_F(TestApiBlackSolver, checkSatAssuming1)
1977
{
1978
4
  Sort boolSort = d_solver.getBooleanSort();
1979
4
  Term x = d_solver.mkConst(boolSort, "x");
1980
4
  Term y = d_solver.mkConst(boolSort, "y");
1981
4
  Term z = d_solver.mkTerm(AND, x, y);
1982
2
  d_solver.setOption("incremental", "true");
1983
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
1984
4
  ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC4ApiException);
1985
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
1986
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(z));
1987
4
  Solver slv;
1988
4
  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
1989
}
1990
1991
140
TEST_F(TestApiBlackSolver, checkSatAssuming2)
1992
{
1993
2
  d_solver.setOption("incremental", "true");
1994
1995
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
1996
4
  Sort intSort = d_solver.getIntegerSort();
1997
4
  Sort boolSort = d_solver.getBooleanSort();
1998
4
  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
1999
4
  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
2000
2001
4
  Term n = Term();
2002
  // Constants
2003
4
  Term x = d_solver.mkConst(uSort, "x");
2004
4
  Term y = d_solver.mkConst(uSort, "y");
2005
  // Functions
2006
4
  Term f = d_solver.mkConst(uToIntSort, "f");
2007
4
  Term p = d_solver.mkConst(intPredSort, "p");
2008
  // Values
2009
4
  Term zero = d_solver.mkInteger(0);
2010
4
  Term one = d_solver.mkInteger(1);
2011
  // Terms
2012
4
  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
2013
4
  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
2014
4
  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
2015
4
  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
2016
4
  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
2017
  // Assertions
2018
  Term assertions =
2019
      d_solver.mkTerm(AND,
2020
6
                      std::vector<Term>{
2021
                          d_solver.mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
2022
                          d_solver.mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
2023
                          d_solver.mkTerm(LEQ, sum, one),   // f(x) + f(y) <= 1
2024
                          p_0.notTerm(),                    // not p(0)
2025
                          p_f_y                             // p(f(y))
2026
16
                      });
2027
2028
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
2029
2
  d_solver.assertFormula(assertions);
2030
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y)));
2031
2
  ASSERT_NO_THROW(d_solver.checkSatAssuming(
2032
      {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
2033
4
  ASSERT_THROW(d_solver.checkSatAssuming(n), CVC4ApiException);
2034
4
  ASSERT_THROW(d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, x, y)}),
2035
2
               CVC4ApiException);
2036
4
  Solver slv;
2037
4
  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
2038
}
2039
2040
140
TEST_F(TestApiBlackSolver, setLogic)
2041
{
2042
2
  ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
2043
4
  ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException);
2044
2
  d_solver.assertFormula(d_solver.mkTrue());
2045
4
  ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException);
2046
}
2047
2048
140
TEST_F(TestApiBlackSolver, setOption)
2049
{
2050
2
  ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
2051
4
  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException);
2052
2
  d_solver.assertFormula(d_solver.mkTrue());
2053
4
  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "minisat"),
2054
2
               CVC4ApiException);
2055
}
2056
2057
140
TEST_F(TestApiBlackSolver, resetAssertions)
2058
{
2059
2
  d_solver.setOption("incremental", "true");
2060
2061
4
  Sort bvSort = d_solver.mkBitVectorSort(4);
2062
4
  Term one = d_solver.mkBitVector(4, 1);
2063
4
  Term x = d_solver.mkConst(bvSort, "x");
2064
4
  Term ule = d_solver.mkTerm(BITVECTOR_ULE, x, one);
2065
4
  Term srem = d_solver.mkTerm(BITVECTOR_SREM, one, x);
2066
2
  d_solver.push(4);
2067
4
  Term slt = d_solver.mkTerm(BITVECTOR_SLT, srem, one);
2068
2
  d_solver.resetAssertions();
2069
2
  d_solver.checkSatAssuming({slt, ule});
2070
2
}
2071
2072
140
TEST_F(TestApiBlackSolver, mkSygusVar)
2073
{
2074
4
  Sort boolSort = d_solver.getBooleanSort();
2075
4
  Sort intSort = d_solver.getIntegerSort();
2076
4
  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
2077
2078
2
  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort));
2079
2
  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort));
2080
2
  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort, std::string("b")));
2081
2
  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort, ""));
2082
4
  ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC4ApiException);
2083
4
  ASSERT_THROW(d_solver.mkSygusVar(d_solver.getNullSort(), "a"),
2084
2
               CVC4ApiException);
2085
4
  Solver slv;
2086
4
  ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException);
2087
}
2088
2089
140
TEST_F(TestApiBlackSolver, mkSygusGrammar)
2090
{
2091
4
  Term nullTerm;
2092
4
  Term boolTerm = d_solver.mkBoolean(true);
2093
4
  Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
2094
4
  Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
2095
2096
2
  ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar}));
2097
2
  ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar}));
2098
4
  ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC4ApiException);
2099
4
  ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC4ApiException);
2100
4
  ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC4ApiException);
2101
4
  ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC4ApiException);
2102
4
  Solver slv;
2103
4
  Term boolVar2 = slv.mkVar(slv.getBooleanSort());
2104
4
  Term intVar2 = slv.mkVar(slv.getIntegerSort());
2105
2
  ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2}));
2106
4
  ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException);
2107
4
  ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException);
2108
}
2109
2110
140
TEST_F(TestApiBlackSolver, synthFun)
2111
{
2112
4
  Sort null = d_solver.getNullSort();
2113
4
  Sort boolean = d_solver.getBooleanSort();
2114
4
  Sort integer = d_solver.getIntegerSort();
2115
2116
4
  Term nullTerm;
2117
4
  Term x = d_solver.mkVar(boolean);
2118
2119
4
  Term start1 = d_solver.mkVar(boolean);
2120
4
  Term start2 = d_solver.mkVar(integer);
2121
2122
4
  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
2123
2
  g1.addRule(start1, d_solver.mkBoolean(false));
2124
2125
4
  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
2126
2
  g2.addRule(start2, d_solver.mkInteger(0));
2127
2128
2
  ASSERT_NO_THROW(d_solver.synthFun("", {}, boolean));
2129
2
  ASSERT_NO_THROW(d_solver.synthFun("f1", {x}, boolean));
2130
2
  ASSERT_NO_THROW(d_solver.synthFun("f2", {x}, boolean, g1));
2131
2132
4
  ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC4ApiException);
2133
4
  ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC4ApiException);
2134
4
  ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC4ApiException);
2135
4
  Solver slv;
2136
4
  Term x2 = slv.mkVar(slv.getBooleanSort());
2137
2
  ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
2138
4
  ASSERT_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()),
2139
2
               CVC4ApiException);
2140
4
  ASSERT_THROW(slv.synthFun("f1", {x}, d_solver.getBooleanSort()),
2141
2
               CVC4ApiException);
2142
}
2143
2144
140
TEST_F(TestApiBlackSolver, synthInv)
2145
{
2146
4
  Sort boolean = d_solver.getBooleanSort();
2147
4
  Sort integer = d_solver.getIntegerSort();
2148
2149
4
  Term nullTerm;
2150
4
  Term x = d_solver.mkVar(boolean);
2151
2152
4
  Term start1 = d_solver.mkVar(boolean);
2153
4
  Term start2 = d_solver.mkVar(integer);
2154
2155
4
  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
2156
2
  g1.addRule(start1, d_solver.mkBoolean(false));
2157
2158
4
  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
2159
2
  g2.addRule(start2, d_solver.mkInteger(0));
2160
2161
2
  ASSERT_NO_THROW(d_solver.synthInv("", {}));
2162
2
  ASSERT_NO_THROW(d_solver.synthInv("i1", {x}));
2163
2
  ASSERT_NO_THROW(d_solver.synthInv("i2", {x}, g1));
2164
2165
4
  ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC4ApiException);
2166
4
  ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException);
2167
}
2168
2169
140
TEST_F(TestApiBlackSolver, addSygusConstraint)
2170
{
2171
4
  Term nullTerm;
2172
4
  Term boolTerm = d_solver.mkBoolean(true);
2173
4
  Term intTerm = d_solver.mkInteger(1);
2174
2175
2
  ASSERT_NO_THROW(d_solver.addSygusConstraint(boolTerm));
2176
4
  ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC4ApiException);
2177
4
  ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC4ApiException);
2178
2179
4
  Solver slv;
2180
4
  ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException);
2181
}
2182
2183
140
TEST_F(TestApiBlackSolver, addSygusInvConstraint)
2184
{
2185
4
  Sort boolean = d_solver.getBooleanSort();
2186
4
  Sort real = d_solver.getRealSort();
2187
2188
4
  Term nullTerm;
2189
4
  Term intTerm = d_solver.mkInteger(1);
2190
2191
4
  Term inv = d_solver.declareFun("inv", {real}, boolean);
2192
4
  Term pre = d_solver.declareFun("pre", {real}, boolean);
2193
4
  Term trans = d_solver.declareFun("trans", {real, real}, boolean);
2194
4
  Term post = d_solver.declareFun("post", {real}, boolean);
2195
2196
4
  Term inv1 = d_solver.declareFun("inv1", {real}, real);
2197
2198
4
  Term trans1 = d_solver.declareFun("trans1", {boolean, real}, boolean);
2199
4
  Term trans2 = d_solver.declareFun("trans2", {real, boolean}, boolean);
2200
4
  Term trans3 = d_solver.declareFun("trans3", {real, real}, real);
2201
2202
2
  ASSERT_NO_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, post));
2203
2204
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(nullTerm, pre, trans, post),
2205
2
               CVC4ApiException);
2206
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, nullTerm, trans, post),
2207
2
               CVC4ApiException);
2208
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, nullTerm, post),
2209
2
               CVC4ApiException);
2210
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm),
2211
2
               CVC4ApiException);
2212
2213
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(intTerm, pre, trans, post),
2214
2
               CVC4ApiException);
2215
2216
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv1, pre, trans, post),
2217
2
               CVC4ApiException);
2218
2219
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, trans, trans, post),
2220
2
               CVC4ApiException);
2221
2222
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, intTerm, post),
2223
2
               CVC4ApiException);
2224
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, pre, post),
2225
2
               CVC4ApiException);
2226
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans1, post),
2227
2
               CVC4ApiException);
2228
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans2, post),
2229
2
               CVC4ApiException);
2230
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans3, post),
2231
2
               CVC4ApiException);
2232
2233
4
  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans),
2234
2
               CVC4ApiException);
2235
4
  Solver slv;
2236
4
  Sort boolean2 = slv.getBooleanSort();
2237
4
  Sort real2 = slv.getRealSort();
2238
4
  Term inv22 = slv.declareFun("inv", {real2}, boolean2);
2239
4
  Term pre22 = slv.declareFun("pre", {real2}, boolean2);
2240
4
  Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
2241
4
  Term post22 = slv.declareFun("post", {real2}, boolean2);
2242
2
  ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
2243
4
  ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
2244
2
               CVC4ApiException);
2245
4
  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
2246
2
               CVC4ApiException);
2247
4
  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
2248
2
               CVC4ApiException);
2249
4
  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
2250
2
               CVC4ApiException);
2251
}
2252
2253
140
TEST_F(TestApiBlackSolver, getSynthSolution)
2254
{
2255
2
  d_solver.setOption("lang", "sygus2");
2256
2
  d_solver.setOption("incremental", "false");
2257
2258
4
  Term nullTerm;
2259
4
  Term x = d_solver.mkBoolean(false);
2260
4
  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
2261
2262
4
  ASSERT_THROW(d_solver.getSynthSolution(f), CVC4ApiException);
2263
2264
2
  d_solver.checkSynth();
2265
2266
2
  ASSERT_NO_THROW(d_solver.getSynthSolution(f));
2267
2
  ASSERT_NO_THROW(d_solver.getSynthSolution(f));
2268
2269
4
  ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC4ApiException);
2270
4
  ASSERT_THROW(d_solver.getSynthSolution(x), CVC4ApiException);
2271
2272
4
  Solver slv;
2273
4
  ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException);
2274
}
2275
2276
140
TEST_F(TestApiBlackSolver, getSynthSolutions)
2277
{
2278
2
  d_solver.setOption("lang", "sygus2");
2279
2
  d_solver.setOption("incremental", "false");
2280
2281
4
  Term nullTerm;
2282
4
  Term x = d_solver.mkBoolean(false);
2283
4
  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
2284
2285
4
  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
2286
4
  ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC4ApiException);
2287
2288
2
  d_solver.checkSynth();
2289
2290
2
  ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
2291
2
  ASSERT_NO_THROW(d_solver.getSynthSolutions({f, f}));
2292
2293
4
  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
2294
4
  ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC4ApiException);
2295
4
  ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC4ApiException);
2296
2297
4
  Solver slv;
2298
4
  ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException);
2299
}
2300
2301
140
TEST_F(TestApiBlackSolver, tupleProject)
2302
{
2303
  std::vector<Sort> sorts = {d_solver.getBooleanSort(),
2304
                             d_solver.getIntegerSort(),
2305
                             d_solver.getStringSort(),
2306
4
                             d_solver.mkSetSort(d_solver.getStringSort())};
2307
  std::vector<Term> elements = {
2308
      d_solver.mkBoolean(true),
2309
      d_solver.mkInteger(3),
2310
      d_solver.mkString("C"),
2311
4
      d_solver.mkTerm(SINGLETON, d_solver.mkString("Z"))};
2312
2313
4
  Term tuple = d_solver.mkTuple(sorts, elements);
2314
2315
4
  std::vector<uint32_t> indices1 = {};
2316
4
  std::vector<uint32_t> indices2 = {0};
2317
4
  std::vector<uint32_t> indices3 = {0, 1};
2318
4
  std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
2319
4
  std::vector<uint32_t> indices5 = {4};
2320
4
  std::vector<uint32_t> indices6 = {0, 4};
2321
2322
2
  ASSERT_NO_THROW(
2323
      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple));
2324
2
  ASSERT_NO_THROW(
2325
      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple));
2326
2
  ASSERT_NO_THROW(
2327
      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple));
2328
2
  ASSERT_NO_THROW(
2329
      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple));
2330
2331
4
  ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple),
2332
2
               CVC4ApiException);
2333
4
  ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple),
2334
2
               CVC4ApiException);
2335
2336
4
  std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
2337
2338
4
  Op op = d_solver.mkOp(TUPLE_PROJECT, indices);
2339
4
  Term projection = d_solver.mkTerm(op, tuple);
2340
2341
4
  Datatype datatype = tuple.getSort().getDatatype();
2342
4
  DatatypeConstructor constructor = datatype[0];
2343
2344
14
  for (size_t i = 0; i < indices.size(); i++)
2345
  {
2346
24
    Term selectorTerm = constructor[indices[i]].getSelectorTerm();
2347
24
    Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple);
2348
24
    Term simplifiedTerm = d_solver.simplify(selectedTerm);
2349
12
    ASSERT_EQ(elements[indices[i]], simplifiedTerm);
2350
  }
2351
2352
2
  ASSERT_EQ(
2353
      "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton "
2354
      "\"Z\")))",
2355
2
      projection.toString());
2356
}
2357
2358
}  // namespace test
2359
396
}  // namespace CVC4