bug fixes for types, old unit tests for types work now

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index a1be2ece81f8981ec02b1314c5c0573887bdcdc1..876b400fea6844ff46de32c63a60f9777be628bf 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -38,6 +38,11 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
   return out;
 }
 
+TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
+: Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
+  {}
+
+
 TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message)
 : Exception(message), d_expr(new Expr(expr))
 {

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 914d479594172d38a184c28dff7af269020d3cbc..ceef80292b0e266bc3c3b7dcd8eb260a4a085da5 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -56,6 +56,9 @@ protected:
 
 public:
 
+  /** Copy constructor */
+  TypeCheckingException(const TypeCheckingException& t);
+
   /** Destructor */
   ~TypeCheckingException() throw ();
 

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 521e177d333449a1ea3f2a19691f7421bf795231..af333f9d31e12ca9f4c61755381bf15ba69f6f4f 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -118,7 +118,7 @@ Type::operator IntegerType() const throw (AssertionException) {
 /** Is this the real type? */
 bool Type::isReal() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isInteger();
+  return d_typeNode->isReal();
 }
 
 /** Cast to a real type */

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index e97af08ee952e65b60418b9c113748545790d0bd..b21ed0d6fa9e78acd063f7b07b1fce5763ed6d17 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -23,7 +23,7 @@ namespace arith {
 class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
@@ -32,7 +32,7 @@ public:
 class ArithOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TNode::iterator child_it = n.begin();
@@ -52,7 +52,7 @@ public:
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TypeNode lhsType = n[0].getType();

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 4cfc2f87f309117be8f1afdcd66a18f97af43c25..95d0f3bf6e17f547aad856db6a473f6c79eeb42d 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -22,7 +22,7 @@ namespace boolean {
 class BooleanTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode booleanType = nodeManager->booleanType();
     TNode::iterator child_it = n.begin();
     TNode::iterator child_it_end = n.end();
@@ -36,7 +36,8 @@ public:
 
 class IteTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode booleanType = nodeManager->booleanType();
     if (n[0].getType() != booleanType) {
       throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index c9a7c1f2c253f5cd8766ff92cb9305cbc1981e7e..9c245b67ab96e881cdfa9748fee9ab19d7966d3f 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -25,7 +25,7 @@ namespace bv {
 class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     return nodeManager->bitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -33,7 +33,7 @@ public:
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode lhs = n[0].getType();
     TypeNode rhs = n[1].getType();
     if (!lhs.isBitVector() || lhs != rhs) {
@@ -46,7 +46,7 @@ public:
 class BitVectorArithRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -65,7 +65,7 @@ public:
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
     TypeNode t = (*it).getType();
@@ -84,7 +84,7 @@ public:
 class BitVectorPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode lhsType = n[0].getType();
     if (!lhsType.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
@@ -100,7 +100,7 @@ public:
 class BitVectorExtractTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
@@ -119,7 +119,7 @@ public:
 class BitVectorConcatRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -137,7 +137,7 @@ public:
 class BitVectorRepeatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
@@ -150,7 +150,7 @@ public:
 class BitVectorExtendTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 8c05591d60a95d5474981b70fd3a6ab045dea07e..4028c302250003dc5a2e7a5162ee56e250bd4206 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -22,7 +22,7 @@ namespace uf {
 class UfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType();
     if (n.getNumChildren() != fType.getNumChildren() - 1) {

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index d483a86f4ec436e0634873b2ac430b7715b8d18b..1930e2bb183f6c0cd44ec2da9abce4e9e36ede1c 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -32,12 +32,14 @@ private:
 
   ExprManager* d_em;
 
-  Expr* a;
-  Expr* b;
-  Expr* c;
-  Expr* mult;
-  Expr* plus;
-  Expr* d;
+  Expr* a_bool;
+  Expr* b_bool;
+  Expr* c_bool_mult;
+  Expr* mult_op;
+  Expr* plus_op;
+  Type* fun_type;
+  Expr* fun_op;
+  Expr* d_apply_fun_bool;
   Expr* null;
 
   Expr* i1;
@@ -51,12 +53,14 @@ public:
     try {
       d_em = new ExprManager;
 
-      a = new Expr(d_em->mkVar("a",d_em->booleanType()));
-      b = new Expr(d_em->mkVar("b", d_em->booleanType()));
-      c = new Expr(d_em->mkExpr(MULT, *a, *b));
-      mult = new Expr(d_em->mkConst(MULT));
-      plus = new Expr(d_em->mkConst(PLUS));
-      d = new Expr(d_em->mkExpr(APPLY_UF, *plus, *b, *c));
+      a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
+      b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
+      c_bool_mult = new Expr(d_em->mkExpr(MULT, *a_bool, *b_bool));
+      mult_op = new Expr(d_em->mkConst(MULT));
+      plus_op = new Expr(d_em->mkConst(PLUS));
+      fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
+      fun_op = new Expr(d_em->mkVar("f", *fun_type));
+      d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
       null = new Expr;
 
       i1 = new Expr(d_em->mkConst(Integer("0")));
@@ -77,12 +81,14 @@ public:
       delete i1;
 
       delete null;
-      delete d;
-      delete plus;
-      delete mult;
-      delete c;
-      delete b;
-      delete a;
+      delete d_apply_fun_bool;
+      delete fun_type;
+      delete fun_op;
+      delete plus_op;
+      delete mult_op;
+      delete c_bool_mult;
+      delete b_bool;
+      delete a_bool;
 
       delete d_em;
     } catch(Exception e) {
@@ -98,8 +104,8 @@ public:
   }
 
   void testCtors() {
-    TS_ASSERT(!a->isNull());
-    TS_ASSERT(!b->isNull());
+    TS_ASSERT(!a_bool->isNull());
+    TS_ASSERT(!b_bool->isNull());
 
     /* Expr(); */
     Expr e;
@@ -113,7 +119,7 @@ public:
     TS_ASSERT(!(e < e2));
     TS_ASSERT(e.isNull());
     TS_ASSERT(e2.isNull());
-    Expr f = d_em->mkExpr(PLUS, *a, *b);
+    Expr f = d_em->mkExpr(PLUS, *a_bool, *b_bool);
     Expr f2 = f;
     TS_ASSERT(!f.isNull());
     TS_ASSERT(!f2.isNull());
@@ -121,12 +127,12 @@ public:
     TS_ASSERT(f2 == f);
     TS_ASSERT(!(f2 < f));
     TS_ASSERT(!(f < f2));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b));
+    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
   }
 
   void testAssignment() {
     /* Expr& operator=(const Expr& e); */
-    Expr e = d_em->mkExpr(PLUS, *a, *b);
+    Expr e = d_em->mkExpr(PLUS, *a_bool, *b_bool);
     Expr f;
     TS_ASSERT(f.isNull());
     f = e;
@@ -135,78 +141,78 @@ public:
     TS_ASSERT(f == e);
     TS_ASSERT(!(f < e));
     TS_ASSERT(!(e < f));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b));
+    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
   }
 
   void testEquality() {
     /* bool operator==(const Expr& e) const; */
     /* bool operator!=(const Expr& e) const; */
 
-    TS_ASSERT(*a == *a);
-    TS_ASSERT(*b == *b);
-    TS_ASSERT(!(*a != *a));
-    TS_ASSERT(!(*b != *b));
+    TS_ASSERT(*a_bool == *a_bool);
+    TS_ASSERT(*b_bool == *b_bool);
+    TS_ASSERT(!(*a_bool != *a_bool));
+    TS_ASSERT(!(*b_bool != *b_bool));
 
-    TS_ASSERT(*a != *b);
-    TS_ASSERT(*b != *a);
-    TS_ASSERT(!(*a == *b));
-    TS_ASSERT(!(*b == *a));
+    TS_ASSERT(*a_bool != *b_bool);
+    TS_ASSERT(*b_bool != *a_bool);
+    TS_ASSERT(!(*a_bool == *b_bool));
+    TS_ASSERT(!(*b_bool == *a_bool));
   }
 
   void testComparison() {
     /* bool operator<(const Expr& e) const; */
 
-    TS_ASSERT(*null < *a);
-    TS_ASSERT(*null < *b);
-    TS_ASSERT(*null < *c);
-    TS_ASSERT(*null < *d);
-    TS_ASSERT(*null < *plus);
-    TS_ASSERT(*null < *mult);
+    TS_ASSERT(*null < *a_bool);
+    TS_ASSERT(*null < *b_bool);
+    TS_ASSERT(*null < *c_bool_mult);
+    TS_ASSERT(*null < *d_apply_fun_bool);
+    TS_ASSERT(*null < *plus_op);
+    TS_ASSERT(*null < *mult_op);
     TS_ASSERT(*null < *i1);
     TS_ASSERT(*null < *i2);
     TS_ASSERT(*null < *r1);
     TS_ASSERT(*null < *r2);
 
-    TS_ASSERT(*a < *b);
-    TS_ASSERT(*a < *c);
-    TS_ASSERT(*a < *d);
-    TS_ASSERT(!(*b < *a));
-    TS_ASSERT(!(*c < *a));
-    TS_ASSERT(!(*d < *a));
+    TS_ASSERT(*a_bool < *b_bool);
+    TS_ASSERT(*a_bool < *c_bool_mult);
+    TS_ASSERT(*a_bool < *d_apply_fun_bool);
+    TS_ASSERT(!(*b_bool < *a_bool));
+    TS_ASSERT(!(*c_bool_mult < *a_bool));
+    TS_ASSERT(!(*d_apply_fun_bool < *a_bool));
 
-    TS_ASSERT(*b < *c);
-    TS_ASSERT(*b < *d);
-    TS_ASSERT(!(*c < *b));
-    TS_ASSERT(!(*d < *b));
+    TS_ASSERT(*b_bool < *c_bool_mult);
+    TS_ASSERT(*b_bool < *d_apply_fun_bool);
+    TS_ASSERT(!(*c_bool_mult < *b_bool));
+    TS_ASSERT(!(*d_apply_fun_bool < *b_bool));
 
-    TS_ASSERT(*c < *d);
-    TS_ASSERT(!(*d < *c));
+    TS_ASSERT(*c_bool_mult < *d_apply_fun_bool);
+    TS_ASSERT(!(*d_apply_fun_bool < *c_bool_mult));
 
-    TS_ASSERT(*mult < *c);
-    TS_ASSERT(*mult < *d);
-    TS_ASSERT(*plus < *d);
-    TS_ASSERT(!(*c < *mult));
-    TS_ASSERT(!(*d < *mult));
-    TS_ASSERT(!(*d < *plus));
+    TS_ASSERT(*mult_op < *c_bool_mult);
+    TS_ASSERT(*mult_op < *d_apply_fun_bool);
+    TS_ASSERT(*plus_op < *d_apply_fun_bool);
+    TS_ASSERT(!(*c_bool_mult < *mult_op));
+    TS_ASSERT(!(*d_apply_fun_bool < *mult_op));
+    TS_ASSERT(!(*d_apply_fun_bool < *plus_op));
 
     TS_ASSERT(!(*null < *null));
-    TS_ASSERT(!(*a < *a));
-    TS_ASSERT(!(*b < *b));
-    TS_ASSERT(!(*c < *c));
-    TS_ASSERT(!(*plus < *plus));
-    TS_ASSERT(!(*mult < *mult));
-    TS_ASSERT(!(*d < *d));
+    TS_ASSERT(!(*a_bool < *a_bool));
+    TS_ASSERT(!(*b_bool < *b_bool));
+    TS_ASSERT(!(*c_bool_mult < *c_bool_mult));
+    TS_ASSERT(!(*plus_op < *plus_op));
+    TS_ASSERT(!(*mult_op < *mult_op));
+    TS_ASSERT(!(*d_apply_fun_bool < *d_apply_fun_bool));
   }
 
   void testGetKind() {
     /* Kind getKind() const; */
 
-    TS_ASSERT(a->getKind() == VARIABLE);
-    TS_ASSERT(b->getKind() == VARIABLE);
-    TS_ASSERT(c->getKind() == MULT);
-    TS_ASSERT(mult->getKind() == BUILTIN);
-    TS_ASSERT(plus->getKind() == BUILTIN);
-    TS_ASSERT(d->getKind() == APPLY_UF);
+    TS_ASSERT(a_bool->getKind() == VARIABLE);
+    TS_ASSERT(b_bool->getKind() == VARIABLE);
+    TS_ASSERT(c_bool_mult->getKind() == MULT);
+    TS_ASSERT(mult_op->getKind() == BUILTIN);
+    TS_ASSERT(plus_op->getKind() == BUILTIN);
+    TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF);
     TS_ASSERT(null->getKind() == NULL_EXPR);
 
     TS_ASSERT(i1->getKind() == CONST_INTEGER);
@@ -218,12 +224,12 @@ public:
   void testGetNumChildren() {
     /* size_t getNumChildren() const; */
 
-    TS_ASSERT(a->getNumChildren() == 0);
-    TS_ASSERT(b->getNumChildren() == 0);
-    TS_ASSERT(c->getNumChildren() == 2);
-    TS_ASSERT(mult->getNumChildren() == 0);
-    TS_ASSERT(plus->getNumChildren() == 0);
-    TS_ASSERT(d->getNumChildren() == 2);
+    TS_ASSERT(a_bool->getNumChildren() == 0);
+    TS_ASSERT(b_bool->getNumChildren() == 0);
+    TS_ASSERT(c_bool_mult->getNumChildren() == 2);
+    TS_ASSERT(mult_op->getNumChildren() == 0);
+    TS_ASSERT(plus_op->getNumChildren() == 0);
+    TS_ASSERT(d_apply_fun_bool->getNumChildren() == 1);
     TS_ASSERT(null->getNumChildren() == 0);
 
     TS_ASSERT(i1->getNumChildren() == 0);
@@ -236,48 +242,48 @@ public:
     /* bool hasOperator() const; */
     /* Expr getOperator() const; */
 
-    TS_ASSERT(!a->hasOperator());
-    TS_ASSERT(!b->hasOperator());
-    TS_ASSERT(c->hasOperator());
-    TS_ASSERT(!mult->hasOperator());
-    TS_ASSERT(!plus->hasOperator());
-    TS_ASSERT(d->hasOperator());
+    TS_ASSERT(!a_bool->hasOperator());
+    TS_ASSERT(!b_bool->hasOperator());
+    TS_ASSERT(c_bool_mult->hasOperator());
+    TS_ASSERT(!mult_op->hasOperator());
+    TS_ASSERT(!plus_op->hasOperator());
+    TS_ASSERT(d_apply_fun_bool->hasOperator());
     TS_ASSERT(!null->hasOperator());
 
-    TS_ASSERT_THROWS(a->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b->getOperator(), IllegalArgumentException);
-    TS_ASSERT(c->getOperator() == *mult);
-    TS_ASSERT_THROWS(plus->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(mult->getOperator(), IllegalArgumentException);
-    TS_ASSERT(d->getOperator() == *plus);
+    TS_ASSERT_THROWS(a_bool->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(b_bool->getOperator(), IllegalArgumentException);
+    TS_ASSERT(c_bool_mult->getOperator() == *mult_op);
+    TS_ASSERT_THROWS(plus_op->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(mult_op->getOperator(), IllegalArgumentException);
+    TS_ASSERT(d_apply_fun_bool->getOperator() == *fun_op);
     TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException);
   }
 
   void testGetType() {
     /* Type getType(); */
 
-    TS_ASSERT(a->getType() == d_em->booleanType());
-    TS_ASSERT(b->getType() == d_em->booleanType());
-// TODO: Type-checking exceptions
-//    TS_ASSERT(c->getType().isNull());
-//    TS_ASSERT(mult->getType().isNull());
-//    TS_ASSERT(plus->getType().isNull());
-//    TS_ASSERT(d->getType().isNull());
-//    TS_ASSERT(i1->getType().isNull());
-//    TS_ASSERT(i2->getType().isNull());
-//    TS_ASSERT(r1->getType().isNull());
-//    TS_ASSERT(r2->getType().isNull());
+    TS_ASSERT(a_bool->getType() == d_em->booleanType());
+    TS_ASSERT(b_bool->getType() == d_em->booleanType());
+    TS_ASSERT_THROWS(c_bool_mult->getType(), TypeCheckingException);
+// These need better support for operators
+//    TS_ASSERT(mult_op->getType().isNull());
+//    TS_ASSERT(plus_op->getType().isNull());
+    TS_ASSERT(d_apply_fun_bool->getType() == d_em->booleanType());
+    TS_ASSERT(i1->getType().isInteger());
+    TS_ASSERT(i2->getType().isInteger());
+    TS_ASSERT(r1->getType().isReal());
+    TS_ASSERT(r2->getType().isReal());
   }
 
   void testToString() {
     /* std::string toString() const; */
 
-    TS_ASSERT(a->toString() == "a");
-    TS_ASSERT(b->toString() == "b");
-    TS_ASSERT(c->toString() == "(MULT a b)");
-    TS_ASSERT(mult->toString() == "(BUILTIN MULT)");
-    TS_ASSERT(plus->toString() == "(BUILTIN PLUS)");
-    TS_ASSERT(d->toString() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))");
+    TS_ASSERT(a_bool->toString() == "a");
+    TS_ASSERT(b_bool->toString() == "b");
+    TS_ASSERT(c_bool_mult->toString() == "(MULT a b)");
+    TS_ASSERT(mult_op->toString() == "(BUILTIN MULT)");
+    TS_ASSERT(plus_op->toString() == "(BUILTIN PLUS)");
+    TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)");
     TS_ASSERT(null->toString() == "null");
 
     TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)");
@@ -291,12 +297,12 @@ public:
 
     stringstream sa, sb, sc, smult, splus, sd, snull;
     stringstream si1, si2, sr1, sr2;
-    a->toStream(sa);
-    b->toStream(sb);
-    c->toStream(sc);
-    mult->toStream(smult);
-    plus->toStream(splus);
-    d->toStream(sd);
+    a_bool->toStream(sa);
+    b_bool->toStream(sb);
+    c_bool_mult->toStream(sc);
+    mult_op->toStream(smult);
+    plus_op->toStream(splus);
+    d_apply_fun_bool->toStream(sd);
     null->toStream(snull);
 
     i1->toStream(si1);
@@ -309,7 +315,7 @@ public:
     TS_ASSERT(sc.str() == "(MULT a b)");
     TS_ASSERT(smult.str() == "(BUILTIN MULT)");
     TS_ASSERT(splus.str() == "(BUILTIN PLUS)");
-    TS_ASSERT(sd.str() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))");
+    TS_ASSERT(sd.str() == "(APPLY_UF f a)");
     TS_ASSERT(snull.str() == "null");
 
     TS_ASSERT(si1.str() == "(CONST_INTEGER 0)");
@@ -321,36 +327,36 @@ public:
   void testIsNull() {
     /* bool isNull() const; */
 
-    TS_ASSERT(!a->isNull());
-    TS_ASSERT(!b->isNull());
-    TS_ASSERT(!c->isNull());
-    TS_ASSERT(!mult->isNull());
-    TS_ASSERT(!plus->isNull());
-    TS_ASSERT(!d->isNull());
+    TS_ASSERT(!a_bool->isNull());
+    TS_ASSERT(!b_bool->isNull());
+    TS_ASSERT(!c_bool_mult->isNull());
+    TS_ASSERT(!mult_op->isNull());
+    TS_ASSERT(!plus_op->isNull());
+    TS_ASSERT(!d_apply_fun_bool->isNull());
     TS_ASSERT(null->isNull());
   }
 
   void testIsConst() {
     /* bool isConst() const; */
 
-    TS_ASSERT(!a->isConst());
-    TS_ASSERT(!b->isConst());
-    TS_ASSERT(!c->isConst());
-    TS_ASSERT(mult->isConst());
-    TS_ASSERT(plus->isConst());
-    TS_ASSERT(!d->isConst());
+    TS_ASSERT(!a_bool->isConst());
+    TS_ASSERT(!b_bool->isConst());
+    TS_ASSERT(!c_bool_mult->isConst());
+    TS_ASSERT(mult_op->isConst());
+    TS_ASSERT(plus_op->isConst());
+    TS_ASSERT(!d_apply_fun_bool->isConst());
     TS_ASSERT(!null->isConst());
   }
 
   void testIsAtomic() {
     /* bool isAtomic() const; */
 
-    TS_ASSERT(a->isAtomic());
-    TS_ASSERT(b->isAtomic());
-    TS_ASSERT(c->isAtomic());
-    TS_ASSERT(mult->isAtomic());
-    TS_ASSERT(plus->isAtomic());
-    TS_ASSERT(d->isAtomic());
+    TS_ASSERT(a_bool->isAtomic());
+    TS_ASSERT(b_bool->isAtomic());
+    TS_ASSERT(c_bool_mult->isAtomic());
+    TS_ASSERT(mult_op->isAtomic());
+    TS_ASSERT(plus_op->isAtomic());
+    TS_ASSERT(d_apply_fun_bool->isAtomic());
 #ifdef CVC4_ASSERTIONS
     TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException);
 #endif /* CVC4_ASSERTIONS */
@@ -360,8 +366,8 @@ public:
     TS_ASSERT(r1->isAtomic());
     TS_ASSERT(r2->isAtomic());
 
-    Expr x = d_em->mkExpr(AND, *a, *b);
-    Expr y = d_em->mkExpr(ITE, *a, *b, *c);
+    Expr x = d_em->mkExpr(AND, *a_bool, *b_bool);
+    Expr y = d_em->mkExpr(ITE, *a_bool, *b_bool, *c_bool_mult);
     Expr z = d_em->mkExpr(IFF, x, y);
 
     TS_ASSERT(!x.isAtomic());
@@ -379,14 +385,14 @@ public:
     /* template <class T>
        const T& getConst() const; */
 
-    TS_ASSERT_THROWS(a->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(c->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT(mult->getConst<Kind>() == MULT);
-    TS_ASSERT_THROWS(mult->getConst<Integer>(), IllegalArgumentException);
-    TS_ASSERT(plus->getConst<Kind>() == PLUS);
-    TS_ASSERT_THROWS(plus->getConst<Rational>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(d->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(a_bool->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(c_bool_mult->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT(mult_op->getConst<Kind>() == MULT);
+    TS_ASSERT_THROWS(mult_op->getConst<Integer>(), IllegalArgumentException);
+    TS_ASSERT(plus_op->getConst<Kind>() == PLUS);
+    TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException);
 
     TS_ASSERT(i1->getConst<Integer>() == 0);
@@ -403,12 +409,12 @@ public:
   void testGetExprManager() {
     /* ExprManager* getExprManager() const; */
 
-    TS_ASSERT(a->getExprManager() == d_em);
-    TS_ASSERT(b->getExprManager() == d_em);
-    TS_ASSERT(c->getExprManager() == d_em);
-    TS_ASSERT(mult->getExprManager() == d_em);
-    TS_ASSERT(plus->getExprManager() == d_em);
-    TS_ASSERT(d->getExprManager() == d_em);
+    TS_ASSERT(a_bool->getExprManager() == d_em);
+    TS_ASSERT(b_bool->getExprManager() == d_em);
+    TS_ASSERT(c_bool_mult->getExprManager() == d_em);
+    TS_ASSERT(mult_op->getExprManager() == d_em);
+    TS_ASSERT(plus_op->getExprManager() == d_em);
+    TS_ASSERT(d_apply_fun_bool->getExprManager() == d_em);
     TS_ASSERT(null->getExprManager() == NULL);
 
     TS_ASSERT(i1->getExprManager() == d_em);