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