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