From: Christopher L. Conway 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::constructTypeNode() const { template Node NodeBuilder::constructNode() { Node n = Node(constructNV()); - if( IS_DEBUG_BUILD ) { - // force an immediate type check - d_nm->getType(n,true); - } + debugCheckType(n); return n; } template Node NodeBuilder::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 Node* NodeBuilder::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 Node* NodeBuilder::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; }