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-2016 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 "expr/array_store_all.h"
21 #include "expr/expr_manager.h"
22 #include "expr/kind.h"
23 #include "expr/node_manager.h"
24 #include "expr/type_node.h"
25 #include "options/language.h"
26 #include "theory/type_enumerator.h"
29 using namespace CVC4::theory
;
30 using namespace CVC4::kind
;
34 class TypeEnumeratorWhite
: public CxxTest::TestSuite
{
37 NodeManagerScope
* d_scope
;
42 d_em
= new ExprManager();
43 d_nm
= NodeManager::fromExprManager(d_em
);
44 d_scope
= new NodeManagerScope(d_nm
);
53 TypeEnumerator
te(d_nm
->booleanType());
54 TS_ASSERT( ! te
.isFinished() );
55 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(false));
56 TS_ASSERT( ! te
.isFinished() );
57 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(true));
58 TS_ASSERT( ! te
.isFinished() );
59 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
60 TS_ASSERT( te
.isFinished() );
61 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
62 TS_ASSERT( te
.isFinished() );
63 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
64 TS_ASSERT( te
.isFinished() );
68 TypeNode sortn
= d_nm
->mkSort("T");
69 Type sort
= sortn
.toType();
70 TypeNode sortn2
= d_nm
->mkSort("U");
71 Type sort2
= sortn2
.toType();
72 TypeEnumerator
te(sortn
);
73 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, 0)));
74 for(size_t i
= 1; i
< 100; ++i
) {
75 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
)));
76 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort2
, i
)));
77 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
)));
78 TS_ASSERT_DIFFERS(*te
, d_nm
->mkConst(UninterpretedConstant(sort
, i
+ 2)));
83 TypeEnumerator
te(d_nm
->integerType());
84 TS_ASSERT( ! te
.isFinished() );
85 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(0)));
86 for(int i
= 1; i
<= 100; ++i
) {
87 TS_ASSERT( ! te
.isFinished() );
88 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(i
)));
89 TS_ASSERT( ! te
.isFinished() );
90 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-i
)));
92 TS_ASSERT( ! te
.isFinished() );
94 te
= TypeEnumerator(d_nm
->realType());
95 TS_ASSERT( ! te
.isFinished() );
96 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(0, 1)));
97 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 1)));
98 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 1)));
99 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 1)));
100 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 1)));
101 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 2)));
102 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 2)));
103 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 1)));
104 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 1)));
105 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 3)));
106 TS_ASSERT( ! te
.isFinished() );
107 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 3)));
108 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(4, 1)));
109 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-4, 1)));
110 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 2)));
111 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 2)));
112 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 3)));
113 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 3)));
114 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 4)));
115 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 4)));
116 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 1)));
117 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 1)));
118 TS_ASSERT( ! te
.isFinished() );
119 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 5)));
120 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 5)));
121 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(6, 1)));
122 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-6, 1)));
123 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 2)));
124 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 2)));
125 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(4, 3)));
126 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-4, 3)));
127 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 4)));
128 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 4)));
129 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(2, 5)));
130 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-2, 5)));
131 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 6)));
132 TS_ASSERT( ! te
.isFinished() );
133 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 6)));
134 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(7, 1)));
135 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-7, 1)));
136 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(5, 3)));
137 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-5, 3)));
138 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(3, 5)));
139 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-3, 5)));
140 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(1, 7)));
141 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(Rational(-1, 7)));
142 TS_ASSERT( ! te
.isFinished() );
144 // subrange bounded only below
145 te
= TypeEnumerator(d_nm
->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(0)), SubrangeBound())));
146 TS_ASSERT( ! te
.isFinished() );
147 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(0)));
148 for(int i
= 1; i
<= 100; ++i
) {
149 TS_ASSERT( ! (++te
).isFinished() );
150 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(i
)));
152 TS_ASSERT( ! te
.isFinished() );
154 // subrange bounded only above
155 te
= TypeEnumerator(d_nm
->mkSubrangeType(SubrangeBounds(SubrangeBound(), SubrangeBound(Integer(-5)))));
156 TS_ASSERT( ! te
.isFinished() );
157 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(-5)));
158 for(int i
= 1; i
<= 100; ++i
) {
159 TS_ASSERT( ! (++te
).isFinished() );
160 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(-5 - i
)));
162 TS_ASSERT( ! te
.isFinished() );
165 te
= TypeEnumerator(d_nm
->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(-10)), SubrangeBound(Integer(15)))));
166 TS_ASSERT( ! te
.isFinished() );
167 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(-10)));
168 for(int i
= -9; i
<= 15; ++i
) {
169 TS_ASSERT( ! (++te
).isFinished() );
170 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(Rational(i
)));
172 TS_ASSERT( (++te
).isFinished() );
173 TS_ASSERT_THROWS(*te
, NoMoreValuesException
);
175 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
178 void testDatatypesFinite() {
179 Datatype
dt("Colors");
180 dt
.addConstructor(DatatypeConstructor("red"));
181 dt
.addConstructor(DatatypeConstructor("orange"));
182 dt
.addConstructor(DatatypeConstructor("yellow"));
183 dt
.addConstructor(DatatypeConstructor("green"));
184 dt
.addConstructor(DatatypeConstructor("blue"));
185 dt
.addConstructor(DatatypeConstructor("violet"));
186 TypeNode datatype
= TypeNode::fromType(d_em
->mkDatatypeType(dt
));
187 TypeEnumerator
te(datatype
);
188 TS_ASSERT_EQUALS(*te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("red")));
189 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("orange")));
190 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("yellow")));
191 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("green")));
192 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("blue")));
193 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(datatype
.toType()).getDatatype().getConstructor("violet")));
194 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
195 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
196 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
199 void testDatatypesInfinite1() {
200 Datatype
colors("Colors");
201 colors
.addConstructor(DatatypeConstructor("red"));
202 colors
.addConstructor(DatatypeConstructor("orange"));
203 colors
.addConstructor(DatatypeConstructor("yellow"));
204 colors
.addConstructor(DatatypeConstructor("green"));
205 colors
.addConstructor(DatatypeConstructor("blue"));
206 colors
.addConstructor(DatatypeConstructor("violet"));
207 TypeNode colorsType
= TypeNode::fromType(d_em
->mkDatatypeType(colors
));
208 Datatype
listColors("ListColors");
209 DatatypeConstructor
consC("cons");
210 consC
.addArg("car", colorsType
.toType());
211 consC
.addArg("cdr", DatatypeSelfType());
212 listColors
.addConstructor(consC
);
213 listColors
.addConstructor(DatatypeConstructor("nil"));
214 TypeNode listColorsType
= TypeNode::fromType(d_em
->mkDatatypeType(listColors
));
216 TypeEnumerator
te(listColorsType
);
217 TS_ASSERT( ! te
.isFinished() );
218 Node cons
= Node::fromExpr(DatatypeType(listColorsType
.toType()).getDatatype().getConstructor("cons"));
219 Node nil
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(listColorsType
.toType()).getDatatype().getConstructor("nil"));
220 Node red
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("red"));
221 Node orange
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("orange"));
222 Node yellow
= d_nm
->mkNode(APPLY_CONSTRUCTOR
, DatatypeType(colorsType
.toType()).getDatatype().getConstructor("yellow"));
223 TS_ASSERT_EQUALS(*te
, nil
);
224 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
));
225 TS_ASSERT( ! te
.isFinished() );
226 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
227 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
)));
228 TS_ASSERT( ! te
.isFinished() );
229 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
, nil
));
230 TS_ASSERT( ! te
.isFinished() );
231 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
232 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
233 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
))));
234 TS_ASSERT( ! te
.isFinished() );
235 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
,
236 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
, nil
)));
237 TS_ASSERT( ! te
.isFinished() );
238 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, yellow
, nil
));
239 TS_ASSERT( ! te
.isFinished() );
240 TS_ASSERT_EQUALS(*++te
, d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, red
,
241 d_nm
->mkNode(APPLY_CONSTRUCTOR
, cons
, orange
, nil
)));
242 TS_ASSERT( ! te
.isFinished() );
245 void NOTYETtestDatatypesInfinite2() {
247 //TypeEnumerator te(datatype);
248 //TS_ASSERT( ! te.isFinished() );
249 TS_FAIL("unimplemented");
252 void testArraysInfinite() {
253 TypeEnumerator
te(d_nm
->mkArrayType(d_nm
->integerType(), d_nm
->integerType()));
254 hash_set
<Node
, NodeHashFunction
> elts
;
255 for(size_t i
= 0; i
< 1000; ++i
) {
256 TS_ASSERT( ! te
.isFinished() );
258 // ensure no duplicates
259 TS_ASSERT( elts
.find(elt
) == elts
.end() );
262 TS_ASSERT( ! te
.isFinished() );
264 // ensure that certain items were found
265 ArrayType
arrayType(d_em
->mkArrayType(d_em
->integerType(), d_em
->integerType()));
266 Node zeroes
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(0))));
267 Node ones
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(1))));
268 Node twos
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(2))));
269 Node threes
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(3))));
270 Node fours
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(4))));
271 Node tens
= d_nm
->mkConst(ArrayStoreAll(arrayType
, d_em
->mkConst(Rational(10))));
273 Node zero
= d_nm
->mkConst(Rational(0));
274 Node one
= d_nm
->mkConst(Rational(1));
275 Node two
= d_nm
->mkConst(Rational(2));
276 Node three
= d_nm
->mkConst(Rational(3));
277 Node four
= d_nm
->mkConst(Rational(4));
278 Node five
= d_nm
->mkConst(Rational(5));
279 Node eleven
= d_nm
->mkConst(Rational(11));
281 // FIXME: the arrays enumerator isn't currently a fair enumerator,
282 // so these will fail; disable them for now
283 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
284 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
285 //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() );
286 //TS_ASSERT( elts.find( threes ) != elts.end() );
287 //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() );
291 TypeEnumerator
te(d_nm
->mkBitVectorType(3));
292 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(BitVector(3u, 0u)));
293 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 1u)));
294 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 2u)));
295 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 3u)));
296 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 4u)));
297 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 5u)));
298 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 6u)));
299 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 7u)));
300 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
301 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
302 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
);
305 };/* class TypeEnumeratorWhite */