test/unit/expr/expr_public.h

   1 /*********************                                                        */
   2 /*! \file expr_public.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Public black-box testing of CVC4::Expr.
  15  **
  16  ** Public black-box testing of CVC4::Expr.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20
  21 #include <sstream>
  22 #include <string>
  23
  24 #include "expr/expr_manager.h"
  25 #include "expr/expr.h"
  26 #include "util/Assert.h"
  27 #include "util/exception.h"
  28
  29 using namespace CVC4;
  30 using namespace CVC4::kind;
  31 using namespace std;
  32
  33 class ExprPublic : public CxxTest::TestSuite {
  34 private:
  35
  36   ExprManager* d_em;
  37
  38   Expr* a_bool;
  39   Expr* b_bool;
  40   Expr* c_bool_and;
  41   Expr* and_op;
  42   Expr* plus_op;
  43   Type* fun_type;
  44   Expr* fun_op;
  45   Expr* d_apply_fun_bool;
  46   Expr* null;
  47
  48   Expr* i1;
  49   Expr* i2;
  50   Expr* r1;
  51   Expr* r2;
  52
  53 public:
  54
  55   void setUp() {
  56     try {
  57       d_em = new ExprManager;
  58
  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));
  67       null = new Expr;
  68
  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;
  75       throw;
  76     }
  77   }
  78
  79   void tearDown() {
  80     try {
  81       delete r2;
  82       delete r1;
  83       delete i2;
  84       delete i1;
  85
  86       delete null;
  87       delete d_apply_fun_bool;
  88       delete fun_type;
  89       delete fun_op;
  90       delete plus_op;
  91       delete and_op;
  92       delete c_bool_and;
  93       delete b_bool;
  94       delete a_bool;
  95
  96       delete d_em;
  97     } catch(Exception e) {
  98       cerr << "Exception during tearDown():" << endl << e;
  99       throw;
 100     }
 101   }
 102
 103   void testDefaultCtor() {
 104     /* Expr(); */
 105     Expr e;
 106     TS_ASSERT(e.isNull());
 107   }
 108
 109   void testCtors() {
 110     TS_ASSERT(!a_bool->isNull());
 111     TS_ASSERT(!b_bool->isNull());
 112
 113     /* Expr(); */
 114     Expr e;
 115     TS_ASSERT(e.isNull());
 116
 117     /* Expr(const Expr& e) */
 118     Expr e2(e);
 119     TS_ASSERT(e == e2);
 120     TS_ASSERT(e2 == 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);
 126     Expr f2 = f;
 127     TS_ASSERT(!f.isNull());
 128     TS_ASSERT(!f2.isNull());
 129     TS_ASSERT(f == f2);
 130     TS_ASSERT(f2 == f);
 131     TS_ASSERT(!(f2 < f));
 132     TS_ASSERT(!(f < f2));
 133     TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
 134   }
 135
 136   void testAssignment() {
 137     /* Expr& operator=(const Expr& e); */
 138     Expr e = d_em->mkExpr(OR, *a_bool, *b_bool);
 139     Expr f;
 140     TS_ASSERT(f.isNull());
 141     f = e;
 142     TS_ASSERT(!f.isNull());
 143     TS_ASSERT(e == f);
 144     TS_ASSERT(f == e);
 145     TS_ASSERT(!(f < e));
 146     TS_ASSERT(!(e < f));
 147     TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
 148   }
 149
 150   void testEquality() {
 151     /* bool operator==(const Expr& e) const; */
 152     /* bool operator!=(const Expr& e) const; */
 153
 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));
 158
 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));
 163   }
 164
 165   void testComparison() {
 166     /* bool operator<(const Expr& e) const; */
 167
 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);
 178
 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));
 185
 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));
 190
 191     TS_ASSERT(*c_bool_and < *d_apply_fun_bool);
 192     TS_ASSERT(!(*d_apply_fun_bool < *c_bool_and));
 193
 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));
 200
 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));
 208   }
 209
 210   void testGetKind() {
 211     /* Kind getKind() const; */
 212
 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);
 220
 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);
 225   }
 226
 227   void testGetNumChildren() {
 228     /* size_t getNumChildren() const; */
 229
 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);
 237
 238     TS_ASSERT(i1->getNumChildren() == 0);
 239     TS_ASSERT(i2->getNumChildren() == 0);
 240     TS_ASSERT(r1->getNumChildren() == 0);
 241     TS_ASSERT(r2->getNumChildren() == 0);
 242   }
 243
 244   void testOperatorFunctions() {
 245     /* bool hasOperator() const; */
 246     /* Expr getOperator() const; */
 247
 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());
 255
 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);
 263   }
 264
 265   void testGetType() {
 266     /* Type getType(); */
 267
 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());
 282   }
 283
 284   void testToString() {
 285     /* std::string toString() const; */
 286
 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");
 294
 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)");
 299   }
 300
 301   void testToStream() {
 302     /* void toStream(std::ostream& out) const; */
 303
 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);
 313
 314     i1->toStream(si1);
 315     i2->toStream(si2);
 316     r1->toStream(sr1);
 317     r2->toStream(sr2);
 318
 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");
 326
 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)");
 331   }
 332
 333   void testIsNull() {
 334     /* bool isNull() const; */
 335
 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());
 343   }
 344
 345   void testIsConst() {
 346     /* bool isConst() const; */
 347
 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());
 355   }
 356
 357   void testGetConst() {
 358     /* template <class T>
 359        const T& getConst() const; */
 360
 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);
 370
 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"));
 375
 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);
 380   }
 381
 382   void testGetExprManager() {
 383     /* ExprManager* getExprManager() const; */
 384
 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);
 392
 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);
 397   }
 398 };