From: Christopher L. Conway Date: Tue, 21 Sep 2010 16:36:42 +0000 (+0000) Subject: Moving automatic type check to NodeBuilder (Fixes: #199) X-Git-Tag: cvc5-1.0.0~8862 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b2b60003b225260904c0073cc952ed2f7169e11;p=cvc5.git Moving automatic type check to NodeBuilder (Fixes: #199) --- diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 422cb47a8..ff696dca9 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -829,22 +829,42 @@ TypeNode NodeBuilder::constructTypeNode() const { template Node NodeBuilder::constructNode() { - return Node(constructNV()); + Node n = Node(constructNV()); + if( IS_DEBUG_BUILD ) { + // force an immediate type check + d_nm->getType(n,true); + } + return n; } template Node NodeBuilder::constructNode() const { - return Node(constructNV()); + Node n = Node(constructNV()); + if( IS_DEBUG_BUILD ) { + // force an immediate type check + d_nm->getType(n,true); + } + return n; } template Node* NodeBuilder::constructNodePtr() { - return new Node(constructNV()); + Node *np = new Node(constructNV()); + if( IS_DEBUG_BUILD ) { + // force an immediate type check + d_nm->getType(*np,true); + } + return np; } template Node* NodeBuilder::constructNodePtr() const { - return new Node(constructNV()); + Node *np = new Node(constructNV()); + if( IS_DEBUG_BUILD ) { + // force an immediate type check + d_nm->getType(*np,true); + } + return np; } template diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5c6a05a03..ab727a627 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -243,12 +243,6 @@ class NodeManager { // bool containsDecision(TNode); // is "atomic" // bool properlyContainsDecision(TNode); // all children are atomic - template - Node doMkNode(NodeBuilder&); - - template - Node* doMkNodePtr(NodeBuilder&); - public: NodeManager(context::Context* ctxt); @@ -805,91 +799,70 @@ inline TypeNode NodeManager::mkSort(const std::string& name) { return type; } -template -inline Node NodeManager::doMkNode(NodeBuilder& nb) { - Node n = nb.constructNode(); - if( IS_DEBUG_BUILD ) { - // force an immediate type check - getType(n,true); - } - return n; -} - -template -inline Node* NodeManager::doMkNodePtr(NodeBuilder& nb) { - Node* np = nb.constructNodePtr(); - if( IS_DEBUG_BUILD ) { - // force an immediate type check - getType(*np,true); - } - return np; -} - - inline Node NodeManager::mkNode(Kind kind, TNode child1) { NodeBuilder<1> nb(this, kind); nb << child1; - return doMkNode(nb); + return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) { NodeBuilder<1> nb(this, kind); nb << child1; - return doMkNodePtr(nb); + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { NodeBuilder<2> nb(this, kind); nb << child1 << child2; - return doMkNode(nb); + return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) { NodeBuilder<2> nb(this, kind); nb << child1 << child2; - return doMkNodePtr(nb); + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { NodeBuilder<3> nb(this, kind); nb << child1 << child2 << child3; - return doMkNode(nb); + return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3) { NodeBuilder<3> nb(this, kind); nb << child1 << child2 << child3; - return doMkNodePtr(nb); + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { NodeBuilder<4> nb(this, kind); nb << child1 << child2 << child3 << child4; - return doMkNode(nb); + return nb.constructNode(); } 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 doMkNodePtr(nb); + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { NodeBuilder<5> nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; - return doMkNode(nb); + return nb.constructNode(); } 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 doMkNodePtr(nb); + return nb.constructNodePtr(); } // N-ary version @@ -899,7 +872,7 @@ inline Node NodeManager::mkNode(Kind kind, children) { NodeBuilder<> nb(this, kind); nb.append(children); - return doMkNode(nb); + return nb.constructNode(); } template @@ -908,7 +881,7 @@ inline Node* NodeManager::mkNodePtr(Kind kind, children) { NodeBuilder<> nb(this, kind); nb.append(children); - return doMkNodePtr(nb); + return nb.constructNodePtr(); } // N-ary version for operators @@ -919,7 +892,7 @@ inline Node NodeManager::mkNode(TNode opNode, NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind())); nb << opNode; nb.append(children); - return doMkNode(nb); + return nb.constructNode(); } template @@ -929,7 +902,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind())); nb << opNode; nb.append(children); - return doMkNodePtr(nb); + return nb.constructNodePtr(); }