From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 21 Sep 2010 23:25:11 +0000 (+0000)
Subject: Rm'ing automatic type check in NodeBuilder for vars/constants
X-Git-Tag: cvc5-1.0.0~8854
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50f5d9673b5e387137fbe4d2624825644b4fb22d;p=cvc5.git

Rm'ing automatic type check in NodeBuilder for vars/constants
---

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index ff696dca9..2f10668c7 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -661,6 +661,18 @@ private:
   expr::NodeValue* constructNV();
   expr::NodeValue* constructNV() const;
 
+  inline void debugCheckType(const TNode n) const {
+    // force an immediate type check, if we are in debug mode
+    // and the current node isn't a variable or constant
+    if( IS_DEBUG_BUILD ) {
+      kind::MetaKind mk = n.getMetaKind();
+      if( mk != kind::metakind::VARIABLE 
+          && mk != kind::metakind::CONSTANT ) {
+        d_nm->getType(n,true);
+      }
+    }
+  }
+
 public:
 
   /** Construct the Node out of the node builder */
@@ -830,40 +842,28 @@ TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const {
 template <unsigned nchild_thresh>
 Node NodeBuilder<nchild_thresh>::constructNode() {
   Node n = Node(constructNV());
-  if( IS_DEBUG_BUILD ) {
-    // force an immediate type check
-    d_nm->getType(n,true);
-  }
+  debugCheckType(n);
   return n;
 }
 
 template <unsigned nchild_thresh>
 Node NodeBuilder<nchild_thresh>::constructNode() const {
   Node n = Node(constructNV());
-  if( IS_DEBUG_BUILD ) {
-    // force an immediate type check
-    d_nm->getType(n,true);
-  }
+  debugCheckType(n);
   return n;
 }
 
 template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
   Node *np = new Node(constructNV());
-  if( IS_DEBUG_BUILD ) {
-    // force an immediate type check
-    d_nm->getType(*np,true);
-  }
+  debugCheckType(*np);
   return np;
 }
 
 template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
   Node *np = new Node(constructNV());
-  if( IS_DEBUG_BUILD ) {
-    // force an immediate type check
-    d_nm->getType(*np,true);
-  }
+  debugCheckType(*np);
   return np;
 }