1 /********************* */
2 /*! \file type_enumerator_white.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andres Noetzli, Clark Barrett
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 "smt/smt_engine.h"
29 #include "smt/smt_engine_scope.h"
30 #include "theory/type_enumerator.h"
33 using namespace CVC4::smt
;
34 using namespace CVC4::theory
;
35 using namespace CVC4::kind
;
39 class TypeEnumeratorWhite
: public CxxTest::TestSuite
{
43 d_em
= new ExprManager();
44 d_smt
= new SmtEngine(d_em
);
45 d_nm
= NodeManager::fromExprManager(d_em
);
46 d_scope
= new SmtScope(d_smt
);
47 d_smt
->finalOptionsAreSet();
50 void tearDown() override
58 TypeEnumerator
te(d_nm
->booleanType());
59 TS_ASSERT( ! te
.isFinished() );
60 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(false));
61 TS_ASSERT( ! te
.isFinished() );
62 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(true));
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() );
68 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
&);
69 TS_ASSERT( te
.isFinished() );
73 TypeNode sort
= d_nm
->mkSort("T");
74 TypeNode sort2
= d_nm
->mkSort("U");
75 TypeEnumerator
te(sort
);
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(d_em
, "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(d_em
, "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(d_em
, "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
236 d_nm
->mkArrayType(d_nm
->integerType(), d_nm
->integerType());
238 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(0))));
240 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(1))));
242 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(2))));
244 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(3))));
246 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(4))));
248 d_nm
->mkConst(ArrayStoreAll(arrayType
, d_nm
->mkConst(Rational(10))));
250 Node zero
= d_nm
->mkConst(Rational(0));
251 Node one
= d_nm
->mkConst(Rational(1));
252 Node two
= d_nm
->mkConst(Rational(2));
253 Node three
= d_nm
->mkConst(Rational(3));
254 Node four
= d_nm
->mkConst(Rational(4));
255 Node five
= d_nm
->mkConst(Rational(5));
256 Node eleven
= d_nm
->mkConst(Rational(11));
258 // FIXME: the arrays enumerator isn't currently a fair enumerator,
259 // so these will fail; disable them for now
260 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
261 //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
262 //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() );
263 //TS_ASSERT( elts.find( threes ) != elts.end() );
264 //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() );
268 TypeEnumerator
te(d_nm
->mkBitVectorType(3));
269 TS_ASSERT_EQUALS(*te
, d_nm
->mkConst(BitVector(3u, 0u)));
270 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 1u)));
271 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 2u)));
272 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 3u)));
273 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 4u)));
274 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 5u)));
275 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 6u)));
276 TS_ASSERT_EQUALS(*++te
, d_nm
->mkConst(BitVector(3u, 7u)));
277 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
&);
278 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
&);
279 TS_ASSERT_THROWS(*++te
, NoMoreValuesException
&);
287 };/* class TypeEnumeratorWhite */