1 /********************* */
2 /*! \file type_enumerator_white.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** \brief White box testing of CVC4::theory::TypeEnumerator
14 ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends
15 ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
18 #include <cxxtest/TestSuite.h>
20 #include <unordered_set>
22 #include "expr/array_store_all.h"
23 #include "expr/expr_manager.h"
24 #include "expr/kind.h"
25 #include "expr/node_manager.h"
26 #include "expr/type_node.h"
27 #include "options/language.h"
28 #include "theory/type_enumerator.h"
31 using namespace CVC4::theory
;
32 using namespace CVC4::kind
;
36 class TypeEnumeratorWhite
: public CxxTest::TestSuite
{
39 NodeManagerScope
* d_scope
;
44 d_em
= new ExprManager();
45 d_nm
= NodeManager::fromExprManager(d_em
);
46 d_scope
= new NodeManagerScope(d_nm
);
49 void tearDown() override
56 TypeEnumerator
te(d_nm
->booleanType());
57 TS_ASSERT( ! te
.isFinished() );
58 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(false));
59 TS_ASSERT( ! te
.isFinished() );
60 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(true));
61 TS_ASSERT( ! te
.isFinished() );
62 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
63 TS_ASSERT( te
.isFinished() );
64 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
65 TS_ASSERT( te
.isFinished() );
66 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
67 TS_ASSERT( te
.isFinished() );
71 TypeNode sortn
= d_nm
->mkSort("T");
72 Type sort
= sortn
.toType();
73 TypeNode sortn2
= d_nm
->mkSort("U");
74 Type sort2
= sortn2
.toType();
75 TypeEnumerator
te(sortn
);
76 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, 0)));
77 for(size_t i
= 1; i
< 100; ++i
) {
78 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
)));
79 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort2
, i
)));
80 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
)));
81 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
+ 2)));
86 TypeEnumerator
te(d_nm
->integerType());
87 TS_ASSERT( ! te
.isFinished() );
88 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(0)));
89 for(int i
= 1; i
<= 100; ++i
) {
90 TS_ASSERT( ! te
.isFinished() );
91 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(i
)));
92 TS_ASSERT( ! te
.isFinished() );
93 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-i
)));
95 TS_ASSERT( ! te
.isFinished() );
97 te
= TypeEnumerator(d_nm
->realType());
98 TS_ASSERT( ! te
.isFinished() );
99 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(0, 1)));
100 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 1)));
101 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 1)));
102 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 1)));
103 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 1)));
104 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 2)));
105 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 2)));
106 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 1)));
107 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 1)));
108 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 3)));
109 TS_ASSERT( ! te
.isFinished() );
110 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 3)));
111 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(4, 1)));
112 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-4, 1)));
113 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 2)));
114 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 2)));
115 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 3)));
116 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 3)));
117 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 4)));
118 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 4)));
119 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 1)));
120 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 1)));
121 TS_ASSERT( ! te
.isFinished() );
122 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 5)));
123 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 5)));
124 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(6, 1)));
125 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-6, 1)));
126 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 2)));
127 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 2)));
128 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(4, 3)));
129 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-4, 3)));
130 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 4)));
131 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 4)));
132 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 5)));
133 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 5)));
134 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 6)));
135 TS_ASSERT( ! te
.isFinished() );
136 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 6)));
137 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(7, 1)));
138 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-7, 1)));
139 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 3)));
140 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 3)));
141 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 5)));
142 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 5)));
143 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 7)));
144 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 7)));
145 TS_ASSERT( ! te
.isFinished() );
148 void testDatatypesFinite() {
149 Datatype
dt("Colors");
150 dt
.addConstructor(DatatypeConstructor("red"));
151 dt
.addConstructor(DatatypeConstructor("orange"));
152 dt
.addConstructor(DatatypeConstructor("yellow"));
153 dt
.addConstructor(DatatypeConstructor("green"));
154 dt
.addConstructor(DatatypeConstructor("blue"));
155 dt
.addConstructor(DatatypeConstructor("violet"));
156 TypeNode datatype
= TypeNode::fromType(d_em
->mkDatatypeType(dt
));
157 TypeEnumerator
te(datatype
);
158 TS_ASSERT_EQUALS(*te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("red")));
159 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("orange")));
160 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("yellow")));
161 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("green")));
162 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("blue")));
163 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("violet")));
164 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
165 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
166 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
169 void testDatatypesInfinite1() {
170 Datatype
colors("Colors");
171 colors
.addConstructor(DatatypeConstructor("red"));
172 colors
.addConstructor(DatatypeConstructor("orange"));
173 colors
.addConstructor(DatatypeConstructor("yellow"));
174 colors
.addConstructor(DatatypeConstructor("green"));
175 colors
.addConstructor(DatatypeConstructor("blue"));
176 colors
.addConstructor(DatatypeConstructor("violet"));
177 TypeNode colorsType
= TypeNode::fromType(d_em
->mkDatatypeType(colors
));
178 Datatype
listColors("ListColors");
179 DatatypeConstructor
consC("cons");
180 consC
.addArg("car", colorsType
.toType());
181 consC
.addArg("cdr", DatatypeSelfType());
182 listColors
.addConstructor(consC
);
183 listColors
.addConstructor(DatatypeConstructor("nil"));
184 TypeNode listColorsType
= TypeNode::fromType(d_em
->mkDatatypeType(listColors
));
186 TypeEnumerator
te(listColorsType
);
187 TS_ASSERT( ! te
.isFinished() );
188 Node cons
= Node::fromExpr(DatatypeType(listColorsType
.toType()).getDatatype().getConstructor("cons"));
189 Node nil
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(listColorsType
.toType()).getDatatype().getConstructor("nil"));
190 Node red
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("red"));
191 Node orange
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("orange"));
192 Node yellow
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("yellow"));
193 TS_ASSERT_EQUALS(*te
, nil
);
194 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
));
195 TS_ASSERT( ! te
.isFinished() );
196 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
197 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
)));
198 TS_ASSERT( ! te
.isFinished() );
199 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
, nil
));
200 TS_ASSERT( ! te
.isFinished() );
201 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
202 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
203 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
))));
204 TS_ASSERT( ! te
.isFinished() );
205 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
,
206 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
)));
207 TS_ASSERT( ! te
.isFinished() );
208 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, yellow
, nil
));
209 TS_ASSERT( ! te
.isFinished() );
210 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
211 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
, nil
)));
212 TS_ASSERT( ! te
.isFinished() );
215 void NOTYETtestDatatypesInfinite2() {
217 //TypeEnumerator te(datatype);
218 //TS_ASSERT( ! te.isFinished() );
219 TS_FAIL("unimplemented");
222 void testArraysInfinite() {
223 TypeEnumerator
te(d_nm
->mkArrayType(d_nm
->integerType(), d_nm
->integerType()));
224 unordered_set
<Node
, NodeHashFunction
> elts
;
225 for(size_t i
= 0; i
< 1000; ++i
) {
226 TS_ASSERT( ! te
.isFinished() );
228 // ensure no duplicates
229 TS_ASSERT( elts
.find(elt
) == elts
.end() );
232 TS_ASSERT( ! te
.isFinished() );
234 // ensure that certain items were found
235 ArrayType
arrayType(d_em
->mkArrayType(d_em
->integerType(), d_em
->integerType()));
236 Node zeroes
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(0))));
237 Node ones
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(1))));
238 Node twos
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(2))));
239 Node threes
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(3))));
240 Node fours
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(4))));
241 Node tens
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(10))));
243 Node zero
= d_nm
->mkConst(Rational(0));
244 Node one
= d_nm
->mkConst(Rational(1));
245 Node two
= d_nm
->mkConst(Rational(2));
246 Node three
= d_nm
->mkConst(Rational(3));
247 Node four
= d_nm
->mkConst(Rational(4));
248 Node five
= d_nm
->mkConst(Rational(5));
249 Node eleven
= d_nm
->mkConst(Rational(11));
251 // FIXME: the arrays enumerator isn't currently a fair enumerator,
252 // so these will fail; disable them for now
253 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
254 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
255 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, fours, eleven, two), two, one), zero, two) ) != elts.end() );
256 //TS_ASSERT( elts.find( threes ) != elts.end() );
257 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() );
261 TypeEnumerator
te(d_nm
->mkBitVectorType(3));
262 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(BitVector(3u, 0u)));
263 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 1u)));
264 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 2u)));
265 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 3u)));
266 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 4u)));
267 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 5u)));
268 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 6u)));
269 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 7u)));
270 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
271 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
272 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
275 };/* class TypeEnumeratorWhite */