e000e618eaef1243c99d3cd00b5071934fd03526
1 /********************* */
2 /*! \file expr_public.h
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Public black-box testing of CVC4::Expr.
16 ** Public black-box testing of CVC4::Expr.
19 #include <cxxtest/TestSuite.h>
24 #include "expr/expr_manager.h"
25 #include "expr/expr.h"
26 #include "util/Assert.h"
27 #include "util/exception.h"
30 using namespace CVC4::kind
;
33 class ExprPublic
: public CxxTest::TestSuite
{
45 Expr
* d_apply_fun_bool
;
57 d_em
= new ExprManager
;
59 a_bool
= new Expr(d_em
->mkVar("a",d_em
->booleanType()));
60 b_bool
= new Expr(d_em
->mkVar("b", d_em
->booleanType()));
61 c_bool_and
= new Expr(d_em
->mkExpr(AND
, *a_bool
, *b_bool
));
62 and_op
= new Expr(d_em
->mkConst(AND
));
63 plus_op
= new Expr(d_em
->mkConst(PLUS
));
64 fun_type
= new Type(d_em
->mkFunctionType(d_em
->booleanType(), d_em
->booleanType()));
65 fun_op
= new Expr(d_em
->mkVar("f", *fun_type
));
66 d_apply_fun_bool
= new Expr(d_em
->mkExpr(APPLY_UF
, *fun_op
, *a_bool
));
69 i1
= new Expr(d_em
->mkConst(Integer("0")));
70 i2
= new Expr(d_em
->mkConst(Integer(23)));
71 r1
= new Expr(d_em
->mkConst(Rational(1, 5)));
72 r2
= new Expr(d_em
->mkConst(Rational("0")));
73 } catch(Exception e
) {
74 cerr
<< "Exception during setUp():" << endl
<< e
;
87 delete d_apply_fun_bool
;
97 } catch(Exception e
) {
98 cerr
<< "Exception during tearDown():" << endl
<< e
;
103 void testDefaultCtor() {
106 TS_ASSERT(e
.isNull());
110 TS_ASSERT(!a_bool
->isNull());
111 TS_ASSERT(!b_bool
->isNull());
115 TS_ASSERT(e
.isNull());
117 /* Expr(const Expr& e) */
121 TS_ASSERT(!(e2
< e
));
122 TS_ASSERT(!(e
< e2
));
123 TS_ASSERT(e
.isNull());
124 TS_ASSERT(e2
.isNull());
125 Expr f
= d_em
->mkExpr(OR
, *a_bool
, *b_bool
);
127 TS_ASSERT(!f
.isNull());
128 TS_ASSERT(!f2
.isNull());
131 TS_ASSERT(!(f2
< f
));
132 TS_ASSERT(!(f
< f2
));
133 TS_ASSERT(f
== d_em
->mkExpr(OR
, *a_bool
, *b_bool
));
136 void testAssignment() {
137 /* Expr& operator=(const Expr& e); */
138 Expr e
= d_em
->mkExpr(OR
, *a_bool
, *b_bool
);
140 TS_ASSERT(f
.isNull());
142 TS_ASSERT(!f
.isNull());
147 TS_ASSERT(f
== d_em
->mkExpr(OR
, *a_bool
, *b_bool
));
150 void testEquality() {
151 /* bool operator==(const Expr& e) const; */
152 /* bool operator!=(const Expr& e) const; */
154 TS_ASSERT(*a_bool
== *a_bool
);
155 TS_ASSERT(*b_bool
== *b_bool
);
156 TS_ASSERT(!(*a_bool
!= *a_bool
));
157 TS_ASSERT(!(*b_bool
!= *b_bool
));
159 TS_ASSERT(*a_bool
!= *b_bool
);
160 TS_ASSERT(*b_bool
!= *a_bool
);
161 TS_ASSERT(!(*a_bool
== *b_bool
));
162 TS_ASSERT(!(*b_bool
== *a_bool
));
165 void testComparison() {
166 /* bool operator<(const Expr& e) const; */
168 TS_ASSERT(*null
< *a_bool
);
169 TS_ASSERT(*null
< *b_bool
);
170 TS_ASSERT(*null
< *c_bool_and
);
171 TS_ASSERT(*null
< *d_apply_fun_bool
);
172 TS_ASSERT(*null
< *plus_op
);
173 TS_ASSERT(*null
< *and_op
);
174 TS_ASSERT(*null
< *i1
);
175 TS_ASSERT(*null
< *i2
);
176 TS_ASSERT(*null
< *r1
);
177 TS_ASSERT(*null
< *r2
);
179 TS_ASSERT(*a_bool
< *b_bool
);
180 TS_ASSERT(*a_bool
< *c_bool_and
);
181 TS_ASSERT(*a_bool
< *d_apply_fun_bool
);
182 TS_ASSERT(!(*b_bool
< *a_bool
));
183 TS_ASSERT(!(*c_bool_and
< *a_bool
));
184 TS_ASSERT(!(*d_apply_fun_bool
< *a_bool
));
186 TS_ASSERT(*b_bool
< *c_bool_and
);
187 TS_ASSERT(*b_bool
< *d_apply_fun_bool
);
188 TS_ASSERT(!(*c_bool_and
< *b_bool
));
189 TS_ASSERT(!(*d_apply_fun_bool
< *b_bool
));
191 TS_ASSERT(*c_bool_and
< *d_apply_fun_bool
);
192 TS_ASSERT(!(*d_apply_fun_bool
< *c_bool_and
));
194 TS_ASSERT(*and_op
< *c_bool_and
);
195 TS_ASSERT(*and_op
< *d_apply_fun_bool
);
196 TS_ASSERT(*plus_op
< *d_apply_fun_bool
);
197 TS_ASSERT(!(*c_bool_and
< *and_op
));
198 TS_ASSERT(!(*d_apply_fun_bool
< *and_op
));
199 TS_ASSERT(!(*d_apply_fun_bool
< *plus_op
));
201 TS_ASSERT(!(*null
< *null
));
202 TS_ASSERT(!(*a_bool
< *a_bool
));
203 TS_ASSERT(!(*b_bool
< *b_bool
));
204 TS_ASSERT(!(*c_bool_and
< *c_bool_and
));
205 TS_ASSERT(!(*plus_op
< *plus_op
));
206 TS_ASSERT(!(*and_op
< *and_op
));
207 TS_ASSERT(!(*d_apply_fun_bool
< *d_apply_fun_bool
));
211 /* Kind getKind() const; */
213 TS_ASSERT(a_bool
->getKind() == VARIABLE
);
214 TS_ASSERT(b_bool
->getKind() == VARIABLE
);
215 TS_ASSERT(c_bool_and
->getKind() == AND
);
216 TS_ASSERT(and_op
->getKind() == BUILTIN
);
217 TS_ASSERT(plus_op
->getKind() == BUILTIN
);
218 TS_ASSERT(d_apply_fun_bool
->getKind() == APPLY_UF
);
219 TS_ASSERT(null
->getKind() == NULL_EXPR
);
221 TS_ASSERT(i1
->getKind() == CONST_INTEGER
);
222 TS_ASSERT(i2
->getKind() == CONST_INTEGER
);
223 TS_ASSERT(r1
->getKind() == CONST_RATIONAL
);
224 TS_ASSERT(r2
->getKind() == CONST_RATIONAL
);
227 void testGetNumChildren() {
228 /* size_t getNumChildren() const; */
230 TS_ASSERT(a_bool
->getNumChildren() == 0);
231 TS_ASSERT(b_bool
->getNumChildren() == 0);
232 TS_ASSERT(c_bool_and
->getNumChildren() == 2);
233 TS_ASSERT(and_op
->getNumChildren() == 0);
234 TS_ASSERT(plus_op
->getNumChildren() == 0);
235 TS_ASSERT(d_apply_fun_bool
->getNumChildren() == 1);
236 TS_ASSERT(null
->getNumChildren() == 0);
238 TS_ASSERT(i1
->getNumChildren() == 0);
239 TS_ASSERT(i2
->getNumChildren() == 0);
240 TS_ASSERT(r1
->getNumChildren() == 0);
241 TS_ASSERT(r2
->getNumChildren() == 0);
244 void testOperatorFunctions() {
245 /* bool hasOperator() const; */
246 /* Expr getOperator() const; */
248 TS_ASSERT(!a_bool
->hasOperator());
249 TS_ASSERT(!b_bool
->hasOperator());
250 TS_ASSERT(c_bool_and
->hasOperator());
251 TS_ASSERT(!and_op
->hasOperator());
252 TS_ASSERT(!plus_op
->hasOperator());
253 TS_ASSERT(d_apply_fun_bool
->hasOperator());
254 TS_ASSERT(!null
->hasOperator());
256 TS_ASSERT_THROWS(a_bool
->getOperator(), IllegalArgumentException
);
257 TS_ASSERT_THROWS(b_bool
->getOperator(), IllegalArgumentException
);
258 TS_ASSERT(c_bool_and
->getOperator() == *and_op
);
259 TS_ASSERT_THROWS(plus_op
->getOperator(), IllegalArgumentException
);
260 TS_ASSERT_THROWS(and_op
->getOperator(), IllegalArgumentException
);
261 TS_ASSERT(d_apply_fun_bool
->getOperator() == *fun_op
);
262 TS_ASSERT_THROWS(null
->getOperator(), IllegalArgumentException
);
266 /* Type getType(); */
268 TS_ASSERT(a_bool
->getType(false) == d_em
->booleanType());
269 TS_ASSERT(a_bool
->getType(true) == d_em
->booleanType());
270 TS_ASSERT(b_bool
->getType(false) == d_em
->booleanType());
271 TS_ASSERT(b_bool
->getType(true) == d_em
->booleanType());
272 TS_ASSERT_THROWS(d_em
->mkExpr(MULT
,*a_bool
,*b_bool
).getType(true),
273 TypeCheckingException
);
274 // These need better support for operators
275 // TS_ASSERT(and_op->getType().isNull());
276 // TS_ASSERT(plus_op->getType().isNull());
277 TS_ASSERT(d_apply_fun_bool
->getType() == d_em
->booleanType());
278 TS_ASSERT(i1
->getType().isInteger());
279 TS_ASSERT(i2
->getType().isInteger());
280 TS_ASSERT(r1
->getType().isReal());
281 TS_ASSERT(r2
->getType().isReal());
284 void testToString() {
285 /* std::string toString() const; */
287 TS_ASSERT(a_bool
->toString() == "a");
288 TS_ASSERT(b_bool
->toString() == "b");
289 TS_ASSERT(c_bool_and
->toString() == "(AND a b)");
290 TS_ASSERT(and_op
->toString() == "(BUILTIN AND)");
291 TS_ASSERT(plus_op
->toString() == "(BUILTIN PLUS)");
292 TS_ASSERT(d_apply_fun_bool
->toString() == "(APPLY_UF f a)");
293 TS_ASSERT(null
->toString() == "null");
295 TS_ASSERT(i1
->toString() == "(CONST_INTEGER 0)");
296 TS_ASSERT(i2
->toString() == "(CONST_INTEGER 23)");
297 TS_ASSERT(r1
->toString() == "(CONST_RATIONAL 1/5)");
298 TS_ASSERT(r2
->toString() == "(CONST_RATIONAL 0)");
301 void testToStream() {
302 /* void toStream(std::ostream& out) const; */
304 stringstream sa
, sb
, sc
, smult
, splus
, sd
, snull
;
305 stringstream si1
, si2
, sr1
, sr2
;
306 a_bool
->toStream(sa
);
307 b_bool
->toStream(sb
);
308 c_bool_and
->toStream(sc
);
309 and_op
->toStream(smult
);
310 plus_op
->toStream(splus
);
311 d_apply_fun_bool
->toStream(sd
);
312 null
->toStream(snull
);
319 TS_ASSERT(sa
.str() == "a");
320 TS_ASSERT(sb
.str() == "b");
321 TS_ASSERT(sc
.str() == "(AND a b)");
322 TS_ASSERT(smult
.str() == "(BUILTIN AND)");
323 TS_ASSERT(splus
.str() == "(BUILTIN PLUS)");
324 TS_ASSERT(sd
.str() == "(APPLY_UF f a)");
325 TS_ASSERT(snull
.str() == "null");
327 TS_ASSERT(si1
.str() == "(CONST_INTEGER 0)");
328 TS_ASSERT(si2
.str() == "(CONST_INTEGER 23)");
329 TS_ASSERT(sr1
.str() == "(CONST_RATIONAL 1/5)");
330 TS_ASSERT(sr2
.str() == "(CONST_RATIONAL 0)");
334 /* bool isNull() const; */
336 TS_ASSERT(!a_bool
->isNull());
337 TS_ASSERT(!b_bool
->isNull());
338 TS_ASSERT(!c_bool_and
->isNull());
339 TS_ASSERT(!and_op
->isNull());
340 TS_ASSERT(!plus_op
->isNull());
341 TS_ASSERT(!d_apply_fun_bool
->isNull());
342 TS_ASSERT(null
->isNull());
346 /* bool isConst() const; */
348 TS_ASSERT(!a_bool
->isConst());
349 TS_ASSERT(!b_bool
->isConst());
350 TS_ASSERT(!c_bool_and
->isConst());
351 TS_ASSERT(and_op
->isConst());
352 TS_ASSERT(plus_op
->isConst());
353 TS_ASSERT(!d_apply_fun_bool
->isConst());
354 TS_ASSERT(!null
->isConst());
357 void testGetConst() {
358 /* template <class T>
359 const T& getConst() const; */
361 TS_ASSERT_THROWS(a_bool
->getConst
<Kind
>(), IllegalArgumentException
);
362 TS_ASSERT_THROWS(b_bool
->getConst
<Kind
>(), IllegalArgumentException
);
363 TS_ASSERT_THROWS(c_bool_and
->getConst
<Kind
>(), IllegalArgumentException
);
364 TS_ASSERT(and_op
->getConst
<Kind
>() == AND
);
365 TS_ASSERT_THROWS(and_op
->getConst
<Integer
>(), IllegalArgumentException
);
366 TS_ASSERT(plus_op
->getConst
<Kind
>() == PLUS
);
367 TS_ASSERT_THROWS(plus_op
->getConst
<Rational
>(), IllegalArgumentException
);
368 TS_ASSERT_THROWS(d_apply_fun_bool
->getConst
<Kind
>(), IllegalArgumentException
);
369 TS_ASSERT_THROWS(null
->getConst
<Kind
>(), IllegalArgumentException
);
371 TS_ASSERT(i1
->getConst
<Integer
>() == 0);
372 TS_ASSERT(i2
->getConst
<Integer
>() == 23);
373 TS_ASSERT(r1
->getConst
<Rational
>() == Rational(1, 5));
374 TS_ASSERT(r2
->getConst
<Rational
>() == Rational("0"));
376 TS_ASSERT_THROWS(i1
->getConst
<Kind
>(), IllegalArgumentException
);
377 TS_ASSERT_THROWS(i2
->getConst
<Kind
>(), IllegalArgumentException
);
378 TS_ASSERT_THROWS(r1
->getConst
<Kind
>(), IllegalArgumentException
);
379 TS_ASSERT_THROWS(r2
->getConst
<Kind
>(), IllegalArgumentException
);
382 void testGetExprManager() {
383 /* ExprManager* getExprManager() const; */
385 TS_ASSERT(a_bool
->getExprManager() == d_em
);
386 TS_ASSERT(b_bool
->getExprManager() == d_em
);
387 TS_ASSERT(c_bool_and
->getExprManager() == d_em
);
388 TS_ASSERT(and_op
->getExprManager() == d_em
);
389 TS_ASSERT(plus_op
->getExprManager() == d_em
);
390 TS_ASSERT(d_apply_fun_bool
->getExprManager() == d_em
);
391 TS_ASSERT(null
->getExprManager() == NULL
);
393 TS_ASSERT(i1
->getExprManager() == d_em
);
394 TS_ASSERT(i2
->getExprManager() == d_em
);
395 TS_ASSERT(r1
->getExprManager() == d_em
);
396 TS_ASSERT(r2
->getExprManager() == d_em
);