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

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

3 files changed, 110 insertions, 27 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5fcbad3a2..343f060e9 100644
--- 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 4b1a0e5be..222185e8c 100644
--- 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 7a53cabfc..b7c7f871e 100644
--- 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);
 }