GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/datatype_api_black.cpp Lines: 376 376 100.0 %
Date: 2021-03-22 Branches: 1009 2992 33.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file datatype_api_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz, Andres Noetzli
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 datatype classes of the C++ API.
13
 **
14
 ** Black box testing of the datatype classes of the C++ API.
15
 **/
16
17
#include "test_api.h"
18
19
namespace CVC4 {
20
21
using namespace api;
22
23
namespace test {
24
25
28
class TestApiBlackDatatype : public TestApi
26
{
27
};
28
29
16
TEST_F(TestApiBlackDatatype, mkDatatypeSort)
30
{
31
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
32
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
33
2
  cons.addSelector("head", d_solver.getIntegerSort());
34
2
  dtypeSpec.addConstructor(cons);
35
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
36
2
  dtypeSpec.addConstructor(nil);
37
4
  Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
38
4
  Datatype d = listSort.getDatatype();
39
4
  DatatypeConstructor consConstr = d[0];
40
4
  DatatypeConstructor nilConstr = d[1];
41
4
  ASSERT_THROW(d[2], CVC4ApiException);
42
2
  ASSERT_NO_THROW(consConstr.getConstructorTerm());
43
2
  ASSERT_NO_THROW(nilConstr.getConstructorTerm());
44
}
45
46
16
TEST_F(TestApiBlackDatatype, mkDatatypeSorts)
47
{
48
  /* Create two mutual datatypes corresponding to this definition
49
   * block:
50
   *
51
   *   DATATYPE
52
   *     tree = node(left: tree, right: tree) | leaf(data: list),
53
   *     list = cons(car: tree, cdr: list) | nil
54
   *   END;
55
   */
56
  // Make unresolved types as placeholders
57
4
  std::set<Sort> unresTypes;
58
4
  Sort unresTree = d_solver.mkUninterpretedSort("tree");
59
4
  Sort unresList = d_solver.mkUninterpretedSort("list");
60
2
  unresTypes.insert(unresTree);
61
2
  unresTypes.insert(unresList);
62
63
4
  DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
64
4
  DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
65
2
  node.addSelector("left", unresTree);
66
2
  node.addSelector("right", unresTree);
67
2
  tree.addConstructor(node);
68
69
4
  DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
70
2
  leaf.addSelector("data", unresList);
71
2
  tree.addConstructor(leaf);
72
73
4
  DatatypeDecl list = d_solver.mkDatatypeDecl("list");
74
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
75
2
  cons.addSelector("car", unresTree);
76
2
  cons.addSelector("cdr", unresTree);
77
2
  list.addConstructor(cons);
78
79
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
80
2
  list.addConstructor(nil);
81
82
4
  std::vector<DatatypeDecl> dtdecls;
83
2
  dtdecls.push_back(tree);
84
2
  dtdecls.push_back(list);
85
4
  std::vector<Sort> dtsorts;
86
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
87
2
  ASSERT_EQ(dtsorts.size(), dtdecls.size());
88
6
  for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
89
  {
90
4
    ASSERT_TRUE(dtsorts[i].isDatatype());
91
4
    ASSERT_FALSE(dtsorts[i].getDatatype().isFinite());
92
4
    ASSERT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
93
  }
94
  // verify the resolution was correct
95
4
  Datatype dtTree = dtsorts[0].getDatatype();
96
4
  DatatypeConstructor dtcTreeNode = dtTree[0];
97
2
  ASSERT_EQ(dtcTreeNode.getName(), "node");
98
4
  DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
99
2
  ASSERT_EQ(dtsTreeNodeLeft.getName(), "left");
100
  // argument type should have resolved to be recursive
101
2
  ASSERT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
102
2
  ASSERT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
103
104
  // fails due to empty datatype
105
4
  std::vector<DatatypeDecl> dtdeclsBad;
106
4
  DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
107
2
  dtdeclsBad.push_back(emptyD);
108
4
  ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
109
}
110
111
16
TEST_F(TestApiBlackDatatype, datatypeStructs)
112
{
113
4
  Sort intSort = d_solver.getIntegerSort();
114
4
  Sort boolSort = d_solver.getBooleanSort();
115
116
  // create datatype sort to test
117
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
118
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
119
2
  cons.addSelector("head", intSort);
120
2
  cons.addSelectorSelf("tail");
121
4
  Sort nullSort;
122
4
  ASSERT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
123
2
  dtypeSpec.addConstructor(cons);
124
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
125
2
  dtypeSpec.addConstructor(nil);
126
4
  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
127
4
  Datatype dt = dtypeSort.getDatatype();
128
2
  ASSERT_FALSE(dt.isCodatatype());
129
2
  ASSERT_FALSE(dt.isTuple());
130
2
  ASSERT_FALSE(dt.isRecord());
131
2
  ASSERT_FALSE(dt.isFinite());
132
2
  ASSERT_TRUE(dt.isWellFounded());
133
  // get constructor
134
4
  DatatypeConstructor dcons = dt[0];
135
4
  Term consTerm = dcons.getConstructorTerm();
136
2
  ASSERT_EQ(dcons.getNumSelectors(), 2);
137
138
  // create datatype sort to test
139
4
  DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
140
4
  DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A");
141
2
  dtypeSpecEnum.addConstructor(ca);
142
4
  DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B");
143
2
  dtypeSpecEnum.addConstructor(cb);
144
4
  DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C");
145
2
  dtypeSpecEnum.addConstructor(cc);
146
4
  Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
147
4
  Datatype dtEnum = dtypeSortEnum.getDatatype();
148
2
  ASSERT_FALSE(dtEnum.isTuple());
149
2
  ASSERT_TRUE(dtEnum.isFinite());
150
151
  // create codatatype
152
4
  DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
153
  DatatypeConstructorDecl consStream =
154
4
      d_solver.mkDatatypeConstructorDecl("cons");
155
2
  consStream.addSelector("head", intSort);
156
2
  consStream.addSelectorSelf("tail");
157
2
  dtypeSpecStream.addConstructor(consStream);
158
4
  Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
159
4
  Datatype dtStream = dtypeSortStream.getDatatype();
160
2
  ASSERT_TRUE(dtStream.isCodatatype());
161
2
  ASSERT_FALSE(dtStream.isFinite());
162
  // codatatypes may be well-founded
163
2
  ASSERT_TRUE(dtStream.isWellFounded());
164
165
  // create tuple
166
4
  Sort tupSort = d_solver.mkTupleSort({boolSort});
167
4
  Datatype dtTuple = tupSort.getDatatype();
168
2
  ASSERT_TRUE(dtTuple.isTuple());
169
2
  ASSERT_FALSE(dtTuple.isRecord());
170
2
  ASSERT_TRUE(dtTuple.isFinite());
171
2
  ASSERT_TRUE(dtTuple.isWellFounded());
172
173
  // create record
174
  std::vector<std::pair<std::string, Sort>> fields = {
175
4
      std::make_pair("b", boolSort), std::make_pair("i", intSort)};
176
4
  Sort recSort = d_solver.mkRecordSort(fields);
177
2
  ASSERT_TRUE(recSort.isDatatype());
178
4
  Datatype dtRecord = recSort.getDatatype();
179
2
  ASSERT_FALSE(dtRecord.isTuple());
180
2
  ASSERT_TRUE(dtRecord.isRecord());
181
2
  ASSERT_FALSE(dtRecord.isFinite());
182
2
  ASSERT_TRUE(dtRecord.isWellFounded());
183
}
184
185
16
TEST_F(TestApiBlackDatatype, datatypeNames)
186
{
187
4
  Sort intSort = d_solver.getIntegerSort();
188
189
  // create datatype sort to test
190
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
191
2
  ASSERT_NO_THROW(dtypeSpec.getName());
192
2
  ASSERT_EQ(dtypeSpec.getName(), std::string("list"));
193
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
194
2
  cons.addSelector("head", intSort);
195
2
  cons.addSelectorSelf("tail");
196
2
  dtypeSpec.addConstructor(cons);
197
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
198
2
  dtypeSpec.addConstructor(nil);
199
4
  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
200
4
  Datatype dt = dtypeSort.getDatatype();
201
2
  ASSERT_EQ(dt.getName(), std::string("list"));
202
2
  ASSERT_NO_THROW(dt.getConstructor("nil"));
203
2
  ASSERT_NO_THROW(dt["cons"]);
204
4
  ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
205
4
  ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
206
207
4
  DatatypeConstructor dcons = dt[0];
208
2
  ASSERT_EQ(dcons.getName(), std::string("cons"));
209
2
  ASSERT_NO_THROW(dcons.getSelector("head"));
210
2
  ASSERT_NO_THROW(dcons["tail"]);
211
4
  ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
212
213
  // get selector
214
4
  DatatypeSelector dselTail = dcons[1];
215
2
  ASSERT_EQ(dselTail.getName(), std::string("tail"));
216
2
  ASSERT_EQ(dselTail.getRangeSort(), dtypeSort);
217
218
  // possible to construct null datatype declarations if not using solver
219
4
  ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
220
}
221
222
16
TEST_F(TestApiBlackDatatype, parametricDatatype)
223
{
224
4
  std::vector<Sort> v;
225
4
  Sort t1 = d_solver.mkParamSort("T1");
226
4
  Sort t2 = d_solver.mkParamSort("T2");
227
2
  v.push_back(t1);
228
2
  v.push_back(t2);
229
4
  DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v);
230
231
  DatatypeConstructorDecl mkpair =
232
4
      d_solver.mkDatatypeConstructorDecl("mk-pair");
233
2
  mkpair.addSelector("first", t1);
234
2
  mkpair.addSelector("second", t2);
235
2
  pairSpec.addConstructor(mkpair);
236
237
4
  Sort pairType = d_solver.mkDatatypeSort(pairSpec);
238
239
2
  ASSERT_TRUE(pairType.getDatatype().isParametric());
240
241
2
  v.clear();
242
2
  v.push_back(d_solver.getIntegerSort());
243
2
  v.push_back(d_solver.getIntegerSort());
244
4
  Sort pairIntInt = pairType.instantiate(v);
245
2
  v.clear();
246
2
  v.push_back(d_solver.getRealSort());
247
2
  v.push_back(d_solver.getRealSort());
248
4
  Sort pairRealReal = pairType.instantiate(v);
249
2
  v.clear();
250
2
  v.push_back(d_solver.getRealSort());
251
2
  v.push_back(d_solver.getIntegerSort());
252
4
  Sort pairRealInt = pairType.instantiate(v);
253
2
  v.clear();
254
2
  v.push_back(d_solver.getIntegerSort());
255
2
  v.push_back(d_solver.getRealSort());
256
4
  Sort pairIntReal = pairType.instantiate(v);
257
258
2
  ASSERT_NE(pairIntInt, pairRealReal);
259
2
  ASSERT_NE(pairIntReal, pairRealReal);
260
2
  ASSERT_NE(pairRealInt, pairRealReal);
261
2
  ASSERT_NE(pairIntInt, pairIntReal);
262
2
  ASSERT_NE(pairIntInt, pairRealInt);
263
2
  ASSERT_NE(pairIntReal, pairRealInt);
264
265
2
  ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal));
266
2
  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal));
267
2
  ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal));
268
2
  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal));
269
2
  ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt));
270
2
  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt));
271
2
  ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt));
272
2
  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt));
273
2
  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal));
274
2
  ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal));
275
2
  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal));
276
2
  ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal));
277
2
  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt));
278
2
  ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt));
279
2
  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt));
280
2
  ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt));
281
282
2
  ASSERT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
283
2
  ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
284
2
  ASSERT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
285
2
  ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
286
2
  ASSERT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
287
2
  ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
288
2
  ASSERT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
289
2
  ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
290
2
  ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
291
2
  ASSERT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
292
2
  ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
293
2
  ASSERT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
294
2
  ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
295
2
  ASSERT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
296
2
  ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
297
2
  ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
298
}
299
300
16
TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
301
{
302
  /* Create mutual datatypes corresponding to this definition block:
303
   *
304
   *   DATATYPE
305
   *     wlist = leaf(data: list),
306
   *     list = cons(car: wlist, cdr: list) | nil,
307
   *     ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list))
308
   *   END;
309
   */
310
  // Make unresolved types as placeholders
311
4
  std::set<Sort> unresTypes;
312
4
  Sort unresWList = d_solver.mkUninterpretedSort("wlist");
313
4
  Sort unresList = d_solver.mkUninterpretedSort("list");
314
4
  Sort unresNs = d_solver.mkUninterpretedSort("ns");
315
2
  unresTypes.insert(unresWList);
316
2
  unresTypes.insert(unresList);
317
2
  unresTypes.insert(unresNs);
318
319
4
  DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist");
320
4
  DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
321
2
  leaf.addSelector("data", unresList);
322
2
  wlist.addConstructor(leaf);
323
324
4
  DatatypeDecl list = d_solver.mkDatatypeDecl("list");
325
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
326
2
  cons.addSelector("car", unresWList);
327
2
  cons.addSelector("cdr", unresList);
328
2
  list.addConstructor(cons);
329
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
330
2
  list.addConstructor(nil);
331
332
4
  DatatypeDecl ns = d_solver.mkDatatypeDecl("ns");
333
4
  DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem");
334
2
  elem.addSelector("ndata", d_solver.mkSetSort(unresWList));
335
2
  ns.addConstructor(elem);
336
  DatatypeConstructorDecl elemArray =
337
4
      d_solver.mkDatatypeConstructorDecl("elemArray");
338
2
  elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList));
339
2
  ns.addConstructor(elemArray);
340
341
4
  std::vector<DatatypeDecl> dtdecls;
342
2
  dtdecls.push_back(wlist);
343
2
  dtdecls.push_back(list);
344
2
  dtdecls.push_back(ns);
345
  // this is well-founded and has no nested recursion
346
4
  std::vector<Sort> dtsorts;
347
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
348
2
  ASSERT_EQ(dtsorts.size(), 3);
349
2
  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
350
2
  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
351
2
  ASSERT_TRUE(dtsorts[2].getDatatype().isWellFounded());
352
2
  ASSERT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
353
2
  ASSERT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
354
2
  ASSERT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
355
356
  /* Create mutual datatypes corresponding to this definition block:
357
   *   DATATYPE
358
   *     ns2 = elem2(ndata: array(int,ns2)) | nil2
359
   *   END;
360
   */
361
2
  unresTypes.clear();
362
4
  Sort unresNs2 = d_solver.mkUninterpretedSort("ns2");
363
2
  unresTypes.insert(unresNs2);
364
365
4
  DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2");
366
4
  DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2");
367
2
  elem2.addSelector("ndata",
368
4
                    d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2));
369
2
  ns2.addConstructor(elem2);
370
4
  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
371
2
  ns2.addConstructor(nil2);
372
373
2
  dtdecls.clear();
374
2
  dtdecls.push_back(ns2);
375
376
2
  dtsorts.clear();
377
  // this is not well-founded due to non-simple recursion
378
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
379
2
  ASSERT_EQ(dtsorts.size(), 1);
380
2
  ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
381
2
  ASSERT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
382
2
            dtsorts[0]);
383
2
  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
384
2
  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
385
386
  /* Create mutual datatypes corresponding to this definition block:
387
   *   DATATYPE
388
   *     list3 = cons3(car: ns3, cdr: list3) | nil3,
389
   *     ns3 = elem3(ndata: set(list3))
390
   *   END;
391
   */
392
2
  unresTypes.clear();
393
4
  Sort unresNs3 = d_solver.mkUninterpretedSort("ns3");
394
2
  unresTypes.insert(unresNs3);
395
4
  Sort unresList3 = d_solver.mkUninterpretedSort("list3");
396
2
  unresTypes.insert(unresList3);
397
398
4
  DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3");
399
4
  DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3");
400
2
  cons3.addSelector("car", unresNs3);
401
2
  cons3.addSelector("cdr", unresList3);
402
2
  list3.addConstructor(cons3);
403
4
  DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3");
404
2
  list3.addConstructor(nil3);
405
406
4
  DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3");
407
4
  DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3");
408
2
  elem3.addSelector("ndata", d_solver.mkSetSort(unresList3));
409
2
  ns3.addConstructor(elem3);
410
411
2
  dtdecls.clear();
412
2
  dtdecls.push_back(list3);
413
2
  dtdecls.push_back(ns3);
414
415
2
  dtsorts.clear();
416
  // both are well-founded and have nested recursion
417
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
418
2
  ASSERT_EQ(dtsorts.size(), 2);
419
2
  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
420
2
  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
421
2
  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
422
2
  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
423
424
  /* Create mutual datatypes corresponding to this definition block:
425
   *   DATATYPE
426
   *     list4 = cons(car: set(ns4), cdr: list4) | nil,
427
   *     ns4 = elem(ndata: list4)
428
   *   END;
429
   */
430
2
  unresTypes.clear();
431
4
  Sort unresNs4 = d_solver.mkUninterpretedSort("ns4");
432
2
  unresTypes.insert(unresNs4);
433
4
  Sort unresList4 = d_solver.mkUninterpretedSort("list4");
434
2
  unresTypes.insert(unresList4);
435
436
4
  DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4");
437
4
  DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4");
438
2
  cons4.addSelector("car", d_solver.mkSetSort(unresNs4));
439
2
  cons4.addSelector("cdr", unresList4);
440
2
  list4.addConstructor(cons4);
441
4
  DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4");
442
2
  list4.addConstructor(nil4);
443
444
4
  DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4");
445
4
  DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3");
446
2
  elem4.addSelector("ndata", unresList4);
447
2
  ns4.addConstructor(elem4);
448
449
2
  dtdecls.clear();
450
2
  dtdecls.push_back(list4);
451
2
  dtdecls.push_back(ns4);
452
453
2
  dtsorts.clear();
454
  // both are well-founded and have nested recursion
455
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
456
2
  ASSERT_EQ(dtsorts.size(), 2);
457
2
  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
458
2
  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
459
2
  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
460
2
  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
461
462
  /* Create mutual datatypes corresponding to this definition block:
463
   *   DATATYPE
464
   *     list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
465
   *   END;
466
   */
467
2
  unresTypes.clear();
468
4
  Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1);
469
2
  unresTypes.insert(unresList5);
470
471
4
  std::vector<Sort> v;
472
4
  Sort x = d_solver.mkParamSort("X");
473
2
  v.push_back(x);
474
4
  DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v);
475
476
4
  std::vector<Sort> args;
477
2
  args.push_back(x);
478
4
  Sort urListX = unresList5.instantiate(args);
479
2
  args[0] = urListX;
480
4
  Sort urListListX = unresList5.instantiate(args);
481
482
4
  DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5");
483
2
  cons5.addSelector("car", x);
484
2
  cons5.addSelector("cdr", urListListX);
485
2
  list5.addConstructor(cons5);
486
4
  DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5");
487
2
  list5.addConstructor(nil5);
488
489
2
  dtdecls.clear();
490
2
  dtdecls.push_back(list5);
491
492
  // well-founded and has nested recursion
493
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
494
2
  ASSERT_EQ(dtsorts.size(), 1);
495
2
  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
496
2
  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
497
}
498
499
16
TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
500
{
501
  /* Create mutual datatypes corresponding to this definition block:
502
   *   DATATYPE
503
   *     plist[X] = pcons(car: X, cdr: plist[X]) | pnil
504
   *   END;
505
   */
506
  // Make unresolved types as placeholders
507
4
  std::set<Sort> unresTypes;
508
4
  Sort unresList = d_solver.mkSortConstructorSort("plist", 1);
509
2
  unresTypes.insert(unresList);
510
511
4
  std::vector<Sort> v;
512
4
  Sort x = d_solver.mkParamSort("X");
513
2
  v.push_back(x);
514
4
  DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v);
515
516
4
  std::vector<Sort> args;
517
2
  args.push_back(x);
518
4
  Sort urListX = unresList.instantiate(args);
519
520
4
  DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons");
521
2
  pcons.addSelector("car", x);
522
2
  pcons.addSelector("cdr", urListX);
523
2
  plist.addConstructor(pcons);
524
4
  DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil");
525
2
  plist.addConstructor(nil5);
526
527
4
  std::vector<DatatypeDecl> dtdecls;
528
2
  dtdecls.push_back(plist);
529
530
4
  std::vector<Sort> dtsorts;
531
  // make the datatype sorts
532
2
  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
533
2
  ASSERT_EQ(dtsorts.size(), 1);
534
4
  Datatype d = dtsorts[0].getDatatype();
535
4
  DatatypeConstructor nilc = d[0];
536
537
4
  Sort isort = d_solver.getIntegerSort();
538
4
  std::vector<Sort> iargs;
539
2
  iargs.push_back(isort);
540
4
  Sort listInt = dtsorts[0].instantiate(iargs);
541
542
4
  Term testConsTerm;
543
  // get the specialized constructor term for list[Int]
544
2
  ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
545
2
  ASSERT_NE(testConsTerm, nilc.getConstructorTerm());
546
  // error to get the specialized constructor term for Int
547
4
  ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
548
}
549
}  // namespace test
550
24
}  // namespace CVC4