Forcing a type check on Node construction in debug mode (Fixes: #188)

NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5fcbad3a2d1df9f653c3c7545ba46497bd3b71c5..343f060e920c394baee0e74bedc1bcb01a5055b8 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -77,7 +77,11 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
@@ -88,8 +92,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
-                                             child2.getNode()));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+                                               child1.getNode(),
+                                               child2.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+                                e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -101,7 +111,15 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode()));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+                                               child1.getNode(), 
+                                               child2.getNode(), 
+                                               child3.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+                                e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -113,9 +131,16 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
-                                          child2.getNode(), child3.getNode(),
-                                          child4.getNode()));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+                                               child1.getNode(),
+                                               child2.getNode(), 
+                                               child3.getNode(),
+                                               child4.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+                                e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -128,9 +153,17 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
-                                          child2.getNode(), child3.getNode(),
-                                          child5.getNode()));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+                                               child1.getNode(),
+                                               child2.getNode(), 
+                                               child3.getNode(),
+                                               child4.getNode(),
+                                               child5.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+                                e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
@@ -150,7 +183,12 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+  try {
+    return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+                                e.getMessage());
+  }
 }
 
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
@@ -171,7 +209,11 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+  try {
+    return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+  }
 }
 
 /** Make a function type from domain to range. */

diff --git a/src/expr/node.h b/src/expr/node.h
index 4b1a0e5bec7c4bee8160390f55d50e1cf06a6240..222185e8ce86377fa45bc41e18ce7e96071d1292 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -34,6 +34,7 @@
 #include "expr/metakind.h"
 #include "expr/expr.h"
 #include "util/Assert.h"
+#include "util/configuration.h"
 #include "util/output.h"
 
 namespace CVC4 {

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7a53cabfc261f9381ff9de987390062f253c6186..b7c7f871e8ff59107142f5c5695c8843256370a8 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -242,6 +242,12 @@ class NodeManager {
   // bool containsDecision(TNode); // is "atomic"
   // bool properlyContainsDecision(TNode); // all children are atomic
 
+  template <unsigned nchild_thresh>
+  Node doMkNode(NodeBuilder<nchild_thresh>&);
+
+  template <unsigned nchild_thresh>
+  Node* doMkNodePtr(NodeBuilder<nchild_thresh>&);
+
 public:
 
   NodeManager(context::Context* ctxt);
@@ -779,61 +785,91 @@ inline TypeNode NodeManager::mkSort(const std::string& name) {
   return type;
 }
 
+template <unsigned nchild_thresh>
+inline Node NodeManager::doMkNode(NodeBuilder<nchild_thresh>& nb) {
+  Node n = nb.constructNode();
+  if( Configuration::isDebugBuild() ) {
+    // force an immediate type check
+    getType(n,true);
+  }
+  return n;
+}
+
+template <unsigned nchild_thresh>
+inline Node* NodeManager::doMkNodePtr(NodeBuilder<nchild_thresh>& nb) {
+  Node* np = nb.constructNodePtr();
+  if( Configuration::isDebugBuild() ) {
+    // force an immediate type check
+    getType(*np,true);
+  }
+  return np;
+}
+
+
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
-  return NodeBuilder<1>(this, kind) << child1;
+  NodeBuilder<1> nb(this, kind);
+  nb << child1;
+  return doMkNode(nb);
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
   NodeBuilder<1> nb(this, kind);
   nb << child1;
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
-  return NodeBuilder<2>(this, kind) << child1 << child2;
+  NodeBuilder<2> nb(this, kind);
+  nb << child1 << child2;
+  return doMkNode(nb);
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
   NodeBuilder<2> nb(this, kind);
   nb << child1 << child2;
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
-  return NodeBuilder<3>(this, kind) << child1 << child2 << child3;
+  NodeBuilder<3> nb(this, kind);
+  nb << child1 << child2 << child3;
+  return doMkNode(nb);
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
   NodeBuilder<3> nb(this, kind);
   nb << child1 << child2 << child3;
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  return NodeBuilder<4>(this, kind) << child1 << child2 << child3 << child4;
+  NodeBuilder<4> nb(this, kind);
+  nb << child1 << child2 << child3 << child4;
+  return doMkNode(nb);
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
   NodeBuilder<4> nb(this, kind);
   nb << child1 << child2 << child3 << child4;
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  return NodeBuilder<5>(this, kind) << child1 << child2 << child3 << child4
-                                   << child5;
+  NodeBuilder<5> nb(this, kind);
+  nb << child1 << child2 << child3 << child4 << child5;
+  return doMkNode(nb);
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
   NodeBuilder<5> nb(this, kind);
   nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 // N-ary version
@@ -841,14 +877,18 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(Kind kind,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  return NodeBuilder<>(this, kind).append(children);
+  NodeBuilder<> nb(this, kind);
+  nb.append(children);
+  return doMkNode(nb);
 }
 
 template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(Kind kind,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  return NodeBuilder<>(this, kind).append(children).constructNodePtr();
+  NodeBuilder<> nb(this, kind);
+  nb.append(children);
+  return doMkNodePtr(nb);
 }
 
 // N-ary version for operators
@@ -860,7 +900,7 @@ inline Node NodeManager::mkNode(TNode opNode,
   NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
   nb << opNode;
   nb.append(children);
-  return nb;
+  return doMkNode(nb);
 }
 
 template <bool ref_count>
@@ -870,7 +910,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode,
   NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
   nb << opNode;
   nb.append(children);
-  return nb.constructNodePtr();
+  return doMkNodePtr(nb);
 }
 
 

diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 6b38abaab9381cb0db28ce82616f47c9d2f9cb9e..3532b8aa7fea33a822ff59b311245c63a78fae35 100644 (file)
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -59,12 +59,12 @@ CvcInput::~CvcInput() {
 }
 
 Command* CvcInput::parseCommand()
-  throw (ParserException, AssertionException) {
+  throw (ParserException, TypeCheckingException, AssertionException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
 Expr CvcInput::parseExpr()
-  throw (ParserException, AssertionException) {
+  throw (ParserException, TypeCheckingException, AssertionException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 

diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 6a37680e8b7d627a728949a8d0a259175f490193..cce935c0b20ad791cbb522860b4c409634f564e0 100644 (file)
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -71,14 +71,16 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() throw(ParserException, AssertionException);
+  Command* parseCommand() 
+    throw(ParserException, TypeCheckingException, AssertionException);
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() throw(ParserException, AssertionException);
+  Expr parseExpr() 
+    throw(ParserException, TypeCheckingException, AssertionException);
 
 private:
 

diff --git a/src/parser/input.h b/src/parser/input.h
index 62015ba51a478b4e6134abd6d7275d3a00593466..1a90a41917ace501408dc60018a63dfa73d66329 100644 (file)
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -155,7 +155,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Command* parseCommand()
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException, AssertionException) = 0;
 
   /**
    * Throws a <code>ParserException</code> with the given message.
@@ -171,7 +171,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Expr parseExpr()
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException, AssertionException) = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2bad12e2ce09f55a822381f5059731adf21a97b7..f73e268a30c45763dfd5e49a494b9b4dd597b437 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -234,6 +234,11 @@ Command* Parser::nextCommand() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -252,6 +257,11 @@ Expr Parser::nextExpression() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextExpression() => " << result << std::endl;

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 33e4c942f32db0bc503c4e2071d949eefd32a2fc..354bf02bd6c4cf7f0f157ce92633556d044b34c6 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -25,6 +25,8 @@
 #include "expr/type_node.h"
 #include "expr/expr.h"
 
+#include <sstream>
+
 namespace CVC4 {
 namespace theory {
 namespace builtin {
@@ -39,7 +41,11 @@ class EqualityTypeRule {
       TypeNode rhsType = n[1].getType(check);
 
       if ( lhsType != rhsType ) {
-        throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+        std::stringstream ss;
+        ss << "Types do not match in equation ";
+        ss << "[" << lhsType << "<>" << rhsType << "]";
+        
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
       if ( lhsType == booleanType ) {

diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index 16c812086da80b390bf8134b8d9fe1f78b75b84d..6d712d43d5d3502493579091d1232554b49c070f 100644 (file)
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -1,7 +1,7 @@
 % EXPECT: VALID
 % Simple test for right precedence of = and NOT.
 
-A, B: BOOLEAN;
+A, B: INT;
 
 QUERY (NOT A = B) <=> (NOT (A = B));
 % EXIT: 20

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 4849e55cb54a34a1aa6c4dae8607160ffb276bb8..e000e618eaef1243c99d3cd00b5071934fd03526 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -37,8 +37,8 @@ private:
 
   Expr* a_bool;
   Expr* b_bool;
-  Expr* c_bool_mult;
-  Expr* mult_op;
+  Expr* c_bool_and;
+  Expr* and_op;
   Expr* plus_op;
   Type* fun_type;
   Expr* fun_op;
@@ -58,8 +58,8 @@ public:
 
       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));
+      c_bool_and = new Expr(d_em->mkExpr(AND, *a_bool, *b_bool));
+      and_op = new Expr(d_em->mkConst(AND));
       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));
@@ -88,8 +88,8 @@ public:
       delete fun_type;
       delete fun_op;
       delete plus_op;
-      delete mult_op;
-      delete c_bool_mult;
+      delete and_op;
+      delete c_bool_and;
       delete b_bool;
       delete a_bool;
 
@@ -122,7 +122,7 @@ public:
     TS_ASSERT(!(e < e2));
     TS_ASSERT(e.isNull());
     TS_ASSERT(e2.isNull());
-    Expr f = d_em->mkExpr(PLUS, *a_bool, *b_bool);
+    Expr f = d_em->mkExpr(OR, *a_bool, *b_bool);
     Expr f2 = f;
     TS_ASSERT(!f.isNull());
     TS_ASSERT(!f2.isNull());
@@ -130,12 +130,12 @@ public:
     TS_ASSERT(f2 == f);
     TS_ASSERT(!(f2 < f));
     TS_ASSERT(!(f < f2));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
+    TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
   }
 
   void testAssignment() {
     /* Expr& operator=(const Expr& e); */
-    Expr e = d_em->mkExpr(PLUS, *a_bool, *b_bool);
+    Expr e = d_em->mkExpr(OR, *a_bool, *b_bool);
     Expr f;
     TS_ASSERT(f.isNull());
     f = e;
@@ -144,7 +144,7 @@ public:
     TS_ASSERT(f == e);
     TS_ASSERT(!(f < e));
     TS_ASSERT(!(e < f));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
+    TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
   }
 
   void testEquality() {
@@ -167,43 +167,43 @@ public:
 
     TS_ASSERT(*null < *a_bool);
     TS_ASSERT(*null < *b_bool);
-    TS_ASSERT(*null < *c_bool_mult);
+    TS_ASSERT(*null < *c_bool_and);
     TS_ASSERT(*null < *d_apply_fun_bool);
     TS_ASSERT(*null < *plus_op);
-    TS_ASSERT(*null < *mult_op);
+    TS_ASSERT(*null < *and_op);
     TS_ASSERT(*null < *i1);
     TS_ASSERT(*null < *i2);
     TS_ASSERT(*null < *r1);
     TS_ASSERT(*null < *r2);
 
     TS_ASSERT(*a_bool < *b_bool);
-    TS_ASSERT(*a_bool < *c_bool_mult);
+    TS_ASSERT(*a_bool < *c_bool_and);
     TS_ASSERT(*a_bool < *d_apply_fun_bool);
     TS_ASSERT(!(*b_bool < *a_bool));
-    TS_ASSERT(!(*c_bool_mult < *a_bool));
+    TS_ASSERT(!(*c_bool_and < *a_bool));
     TS_ASSERT(!(*d_apply_fun_bool < *a_bool));
 
-    TS_ASSERT(*b_bool < *c_bool_mult);
+    TS_ASSERT(*b_bool < *c_bool_and);
     TS_ASSERT(*b_bool < *d_apply_fun_bool);
-    TS_ASSERT(!(*c_bool_mult < *b_bool));
+    TS_ASSERT(!(*c_bool_and < *b_bool));
     TS_ASSERT(!(*d_apply_fun_bool < *b_bool));
 
-    TS_ASSERT(*c_bool_mult < *d_apply_fun_bool);
-    TS_ASSERT(!(*d_apply_fun_bool < *c_bool_mult));
+    TS_ASSERT(*c_bool_and < *d_apply_fun_bool);
+    TS_ASSERT(!(*d_apply_fun_bool < *c_bool_and));
 
-    TS_ASSERT(*mult_op < *c_bool_mult);
-    TS_ASSERT(*mult_op < *d_apply_fun_bool);
+    TS_ASSERT(*and_op < *c_bool_and);
+    TS_ASSERT(*and_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(!(*c_bool_and < *and_op));
+    TS_ASSERT(!(*d_apply_fun_bool < *and_op));
     TS_ASSERT(!(*d_apply_fun_bool < *plus_op));
 
     TS_ASSERT(!(*null < *null));
     TS_ASSERT(!(*a_bool < *a_bool));
     TS_ASSERT(!(*b_bool < *b_bool));
-    TS_ASSERT(!(*c_bool_mult < *c_bool_mult));
+    TS_ASSERT(!(*c_bool_and < *c_bool_and));
     TS_ASSERT(!(*plus_op < *plus_op));
-    TS_ASSERT(!(*mult_op < *mult_op));
+    TS_ASSERT(!(*and_op < *and_op));
     TS_ASSERT(!(*d_apply_fun_bool < *d_apply_fun_bool));
   }
 
@@ -212,8 +212,8 @@ public:
 
     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(c_bool_and->getKind() == AND);
+    TS_ASSERT(and_op->getKind() == BUILTIN);
     TS_ASSERT(plus_op->getKind() == BUILTIN);
     TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF);
     TS_ASSERT(null->getKind() == NULL_EXPR);
@@ -229,8 +229,8 @@ public:
 
     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(c_bool_and->getNumChildren() == 2);
+    TS_ASSERT(and_op->getNumChildren() == 0);
     TS_ASSERT(plus_op->getNumChildren() == 0);
     TS_ASSERT(d_apply_fun_bool->getNumChildren() == 1);
     TS_ASSERT(null->getNumChildren() == 0);
@@ -247,17 +247,17 @@ public:
 
     TS_ASSERT(!a_bool->hasOperator());
     TS_ASSERT(!b_bool->hasOperator());
-    TS_ASSERT(c_bool_mult->hasOperator());
-    TS_ASSERT(!mult_op->hasOperator());
+    TS_ASSERT(c_bool_and->hasOperator());
+    TS_ASSERT(!and_op->hasOperator());
     TS_ASSERT(!plus_op->hasOperator());
     TS_ASSERT(d_apply_fun_bool->hasOperator());
     TS_ASSERT(!null->hasOperator());
 
     TS_ASSERT_THROWS(a_bool->getOperator(), IllegalArgumentException);
     TS_ASSERT_THROWS(b_bool->getOperator(), IllegalArgumentException);
-    TS_ASSERT(c_bool_mult->getOperator() == *mult_op);
+    TS_ASSERT(c_bool_and->getOperator() == *and_op);
     TS_ASSERT_THROWS(plus_op->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(mult_op->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(and_op->getOperator(), IllegalArgumentException);
     TS_ASSERT(d_apply_fun_bool->getOperator() == *fun_op);
     TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException);
   }
@@ -269,9 +269,10 @@ public:
     TS_ASSERT(a_bool->getType(true) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(false) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(true) == d_em->booleanType());
-    TS_ASSERT_THROWS(c_bool_mult->getType(true), TypeCheckingException);
+    TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true), 
+                     TypeCheckingException);
 // These need better support for operators
-//    TS_ASSERT(mult_op->getType().isNull());
+//    TS_ASSERT(and_op->getType().isNull());
 //    TS_ASSERT(plus_op->getType().isNull());
     TS_ASSERT(d_apply_fun_bool->getType() == d_em->booleanType());
     TS_ASSERT(i1->getType().isInteger());
@@ -285,8 +286,8 @@ public:
 
     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(c_bool_and->toString() == "(AND a b)");
+    TS_ASSERT(and_op->toString() == "(BUILTIN AND)");
     TS_ASSERT(plus_op->toString() == "(BUILTIN PLUS)");
     TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)");
     TS_ASSERT(null->toString() == "null");
@@ -304,8 +305,8 @@ public:
     stringstream si1, si2, sr1, sr2;
     a_bool->toStream(sa);
     b_bool->toStream(sb);
-    c_bool_mult->toStream(sc);
-    mult_op->toStream(smult);
+    c_bool_and->toStream(sc);
+    and_op->toStream(smult);
     plus_op->toStream(splus);
     d_apply_fun_bool->toStream(sd);
     null->toStream(snull);
@@ -317,8 +318,8 @@ public:
 
     TS_ASSERT(sa.str() == "a");
     TS_ASSERT(sb.str() == "b");
-    TS_ASSERT(sc.str() == "(MULT a b)");
-    TS_ASSERT(smult.str() == "(BUILTIN MULT)");
+    TS_ASSERT(sc.str() == "(AND a b)");
+    TS_ASSERT(smult.str() == "(BUILTIN AND)");
     TS_ASSERT(splus.str() == "(BUILTIN PLUS)");
     TS_ASSERT(sd.str() == "(APPLY_UF f a)");
     TS_ASSERT(snull.str() == "null");
@@ -334,8 +335,8 @@ public:
 
     TS_ASSERT(!a_bool->isNull());
     TS_ASSERT(!b_bool->isNull());
-    TS_ASSERT(!c_bool_mult->isNull());
-    TS_ASSERT(!mult_op->isNull());
+    TS_ASSERT(!c_bool_and->isNull());
+    TS_ASSERT(!and_op->isNull());
     TS_ASSERT(!plus_op->isNull());
     TS_ASSERT(!d_apply_fun_bool->isNull());
     TS_ASSERT(null->isNull());
@@ -346,8 +347,8 @@ public:
 
     TS_ASSERT(!a_bool->isConst());
     TS_ASSERT(!b_bool->isConst());
-    TS_ASSERT(!c_bool_mult->isConst());
-    TS_ASSERT(mult_op->isConst());
+    TS_ASSERT(!c_bool_and->isConst());
+    TS_ASSERT(and_op->isConst());
     TS_ASSERT(plus_op->isConst());
     TS_ASSERT(!d_apply_fun_bool->isConst());
     TS_ASSERT(!null->isConst());
@@ -359,9 +360,9 @@ public:
 
     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_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT(and_op->getConst<Kind>() == AND);
+    TS_ASSERT_THROWS(and_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);
@@ -383,8 +384,8 @@ public:
 
     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(c_bool_and->getExprManager() == d_em);
+    TS_ASSERT(and_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);

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index c7983258356b1d1cf5cc4c12ef33dd256b15e2ca..f1bb7c25195deb3cd94cebf85f58b146f7d50cdd 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -40,6 +40,7 @@ private:
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
   TypeNode *d_booleanType;
+  TypeNode *d_realType;
 
 public:
 
@@ -48,6 +49,7 @@ public:
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
+    d_realType = new TypeNode(d_nodeManager->realType());
   }
 
   void tearDown() {
@@ -265,8 +267,9 @@ public:
   void testEqNode() {
     /* Node eqNode(const Node& right) const; */
 
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
+    TypeNode t = d_nodeManager->mkSort();
+    Node left = d_nodeManager->mkVar(t);
+    Node right = d_nodeManager->mkVar(t);
     Node eq = left.eqNode(right);
 
     TS_ASSERT(EQUAL == eq.getKind());
@@ -326,7 +329,7 @@ public:
     Node a = d_nodeManager->mkVar(*d_booleanType);
     Node b = d_nodeManager->mkVar(*d_booleanType);
 
-    Node cnd = d_nodeManager->mkNode(PLUS, a, b);
+    Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
     Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
     Node ite = cnd.iteNode(thenBranch, elseBranch);
@@ -395,10 +398,13 @@ public:
     n = d_nodeManager->mkNode(IFF, a, b);
     TS_ASSERT(IFF == n.getKind());
 
-    n = d_nodeManager->mkNode(PLUS, a, b);
+    Node x = d_nodeManager->mkVar(*d_realType);
+    Node y = d_nodeManager->mkVar(*d_realType);
+
+    n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
 
-    n = d_nodeManager->mkNode(UMINUS, a);
+    n = d_nodeManager->mkNode(UMINUS, x);
     TS_ASSERT(UMINUS == n.getKind());
   }
 
@@ -408,7 +414,7 @@ public:
     TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
-    Node a = d_nodeManager->mkVar(booleanType);
+    Node a = d_nodeManager->mkVar(sort);
     Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 
     TS_ASSERT( fa.hasOperator() );

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 7f315f0926b9fcd5aba4ac89dfeb48c0a257723c..e3883b8241d63baeffb0c54e7fa88a8b72af4180 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -29,6 +29,7 @@
 #include "expr/kind.h"
 #include "context/context.h"
 #include "util/Assert.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -42,6 +43,7 @@ private:
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
   TypeNode* d_booleanType;
+  TypeNode* d_realType;
 
 public:
 
@@ -52,6 +54,7 @@ public:
 
     specKind = PLUS;
     d_booleanType = new TypeNode(d_nm->booleanType());
+    d_realType = new TypeNode(d_nm->realType());
   }
 
   void tearDown() {
@@ -484,7 +487,13 @@ public:
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
-    Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z);
+
+    Node r = d_nm->mkVar(*d_realType);
+    Node s = d_nm->mkVar(*d_realType);
+    Node t = d_nm->mkVar(*d_realType);
+
+    Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0),
+                          d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t));
     Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
 
 #ifdef CVC4_ASSERTIONS
@@ -606,43 +615,45 @@ public:
 
   void testConvenienceBuilders() {
     Node a = d_nm->mkVar(*d_booleanType);
+
     Node b = d_nm->mkVar(*d_booleanType);
     Node c = d_nm->mkVar(*d_booleanType);
-    Node d = d_nm->mkVar(*d_booleanType);
-    Node e = d_nm->mkVar(*d_booleanType);
-    Node f = d_nm->mkVar(*d_booleanType);
+
+    Node d = d_nm->mkVar(*d_realType);
+    Node e = d_nm->mkVar(*d_realType);
+    Node f = d_nm->mkVar(*d_realType);
 
     Node m = a && b;
-    Node n = (a && b) || c;
-    Node o = d + e - b;
-    Node p = (a && o) || c;
+    TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
 
-    Node x = d + e + o - m;
-    Node y = f - a - c + e;
+    Node n = (a && b) || c;
+    TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
 
-    Node q = a && b && c;
+    Node p = (a && m) || n;
+    TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, m), n));
 
-    Node r = (e && d && b && a) || (x && y) || f || (q && a);
+    Node w = d + e - f;
+    TS_ASSERT_EQUALS(w, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f)));
 
-    TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
-    TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
-    TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b)));
-    TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c));
+    Node x = d + e + w - f;
+    TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, w, d_nm->mkNode(UMINUS, f)));
 
-    TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m)));
+    Node y = f - x - e + w;
     TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS,
                                      f,
-                                     d_nm->mkNode(UMINUS, a),
-                                     d_nm->mkNode(UMINUS, c),
-                                     e));
+                                     d_nm->mkNode(UMINUS, x),
+                                     d_nm->mkNode(UMINUS, e),
+                                     w));
 
+    Node q = a && b && c;
     TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c));
 
+    Node r = (c && b && a) || (m && n) || p || (a && p);
     TS_ASSERT_EQUALS(r, d_nm->mkNode(OR,
-                                     d_nm->mkNode(AND, e, d, b, a),
-                                     d_nm->mkNode(AND, x, y),
-                                     f,
-                                     d_nm->mkNode(AND, q, a)));
+                                     d_nm->mkNode(AND, c, b, a),
+                                     d_nm->mkNode(AND, m, n),
+                                     p,
+                                     d_nm->mkNode(AND, a, p)));
 
     TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c));
     TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c)));
@@ -653,28 +664,28 @@ public:
     TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c));
     TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c)));
 
-    TS_ASSERT_EQUALS(Node((a + b) + c), d_nm->mkNode(PLUS, a, b, c));
-    TS_ASSERT_EQUALS(Node(a + (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, c)));
-    TS_ASSERT_EQUALS(Node((a - b) - c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a - (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))));
-    TS_ASSERT_EQUALS(Node((a * b) * c), d_nm->mkNode(MULT, a, b, c));
-    TS_ASSERT_EQUALS(Node(a * (b * c)), d_nm->mkNode(MULT, a, d_nm->mkNode(MULT, b, c)));
-    TS_ASSERT_EQUALS(Node((a + b) - c), d_nm->mkNode(PLUS, a, b, d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a + (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
-    TS_ASSERT_EQUALS(Node((a - b) + c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), c));
-    TS_ASSERT_EQUALS(Node(a - (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, c))));
-    TS_ASSERT_EQUALS(Node((a + b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, b), c));
-    TS_ASSERT_EQUALS(Node(a + (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(MULT, b, c)));
-    TS_ASSERT_EQUALS(Node((a - b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b)), c));
-    TS_ASSERT_EQUALS(Node(a - (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, b, c))));
-    TS_ASSERT_EQUALS(Node((a * b) + c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), c));
-    TS_ASSERT_EQUALS(Node(a * (b + c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, c)));
-    TS_ASSERT_EQUALS(Node((a * b) - c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a * (b - c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
-
-    TS_ASSERT_EQUALS(Node(-a), d_nm->mkNode(UMINUS, a));
-    TS_ASSERT_EQUALS(Node(- a - b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), d_nm->mkNode(UMINUS, b)));
-    TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b));
-    TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b));
+    TS_ASSERT_EQUALS(Node((d + e) + f), d_nm->mkNode(PLUS, d, e, f));
+    TS_ASSERT_EQUALS(Node(d + (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, f)));
+    TS_ASSERT_EQUALS(Node((d - e) - f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d - (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))));
+    TS_ASSERT_EQUALS(Node((d * e) * f), d_nm->mkNode(MULT, d, e, f));
+    TS_ASSERT_EQUALS(Node(d * (e * f)), d_nm->mkNode(MULT, d, d_nm->mkNode(MULT, e, f)));
+    TS_ASSERT_EQUALS(Node((d + e) - f), d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d + (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))));
+    TS_ASSERT_EQUALS(Node((d - e) + f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), f));
+    TS_ASSERT_EQUALS(Node(d - (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, f))));
+    TS_ASSERT_EQUALS(Node((d + e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, e), f));
+    TS_ASSERT_EQUALS(Node(d + (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(MULT, e, f)));
+    TS_ASSERT_EQUALS(Node((d - e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e)), f));
+    TS_ASSERT_EQUALS(Node(d - (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, e, f))));
+    TS_ASSERT_EQUALS(Node((d * e) + f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), f));
+    TS_ASSERT_EQUALS(Node(d * (e + f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, f)));
+    TS_ASSERT_EQUALS(Node((d * e) - f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d * (e - f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))));
+
+    TS_ASSERT_EQUALS(Node(-d), d_nm->mkNode(UMINUS, d));
+    TS_ASSERT_EQUALS(Node(- d - e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), d_nm->mkNode(UMINUS, e)));
+    TS_ASSERT_EQUALS(Node(- d + e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), e));
+    TS_ASSERT_EQUALS(Node(- d * e), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, d), e));
   }
 };

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1f986732c059b55be80851e23b4d1ecc701ce8ad..0e0835327c9da3f8587c20263ef38b6340d06aee 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -191,7 +191,7 @@ public:
     tryGoodInput("CHECKSAT FALSE;");
     tryGoodInput("a, b : BOOLEAN;");
     tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
-    tryGoodInput("T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;");
+    tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
     tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
     tryGoodInput("%% nothing but a comment");
     tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 570fa74a40f539f649c074d5fc0a58675a915360..8132cc2627f1be78576fc69b05fc59d42c01f4f8 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -261,10 +261,12 @@ public:
   }
 
   void testRewriterComplicated() {
+    try {
     Node x = d_nm->mkVar("x", d_nm->integerType());
     Node y = d_nm->mkVar("y", d_nm->realType());
-    Node z1 = d_nm->mkVar("z1", d_nm->mkSort("U"));
-    Node z2 = d_nm->mkVar("z2", d_nm->mkSort("U"));
+    TypeNode u = d_nm->mkSort("U");
+    Node z1 = d_nm->mkVar("z1", u);
+    Node z2 = d_nm->mkVar("z2", u);
     Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(),
                                                    d_nm->integerType()));
     Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(),
@@ -279,10 +281,8 @@ public:
     Node gy = d_nm->mkNode(APPLY_UF, g, y);
     Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2);
     Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2);
-    Node ffxeqgy = d_nm->mkNode(EQUAL,
-                                ffx,
-                                gy);
-    Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2, ffx);
+    Node ffxeqgy = d_nm->mkNode(EQUAL, ffx, gy);
+    Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2);
     Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1);
     Node or1 = d_nm->mkNode(OR, and1, ffxeqf1);
     // make the expression:
@@ -350,5 +350,9 @@ public:
     TS_ASSERT(FakeTheory::nothingMoreExpected());
 
     TS_ASSERT_EQUALS(nOut, nExpected);
+    } catch( TypeCheckingExceptionPrivate& e ) {
+      cerr << "Type error: " << e.getMessage() << ": " << e.getNode();
+      throw;
+    }
   }
 };

diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index 8e72c428f885cc839a30b67fb49f419c746283d7..f273de30f8a4e85567b4d76a8019782d12b66de1 100644 (file)
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -74,7 +74,8 @@ public:
   }
 
   void testPushPopSimple() {
-    Node x = d_nm->mkVar(*d_booleanType);
+    TypeNode t = d_nm->mkSort();
+    Node x = d_nm->mkVar(t);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();