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