From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 24 Mar 2011 05:52:02 +0000 (+0000)
Subject: Slight speedup to the hashing node factory.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7efaa7f1995897684f03e4b3aa5b5a7f264e4105;p=francis%2Fstp.git

Slight speedup to the hashing node factory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1235 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/AST/NodeFactory/HashingNodeFactory.cpp b/src/AST/NodeFactory/HashingNodeFactory.cpp
index b1dda28..48fe2a0 100644
--- a/src/AST/NodeFactory/HashingNodeFactory.cpp
+++ b/src/AST/NodeFactory/HashingNodeFactory.cpp
@@ -13,12 +13,17 @@ HashingNodeFactory::~HashingNodeFactory()
 }
 
 // Get structurally hashed version of the node.
-BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind,	const BEEV::ASTVec & back_children)
+BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec & back_children)
 {
-	// create a new node.  Children will be modified.
-	ASTInterior *n_ptr = new ASTInterior(kind);
-
-	ASTVec children(back_children);
+       // We can't create NOT(NOT (..)) nodes because of how the numbering scheme we use works.
+       // So you can't trust the hashiing node factory even to return nodes of the same kind that
+       // you ask for.
+        if (kind == BEEV::NOT && back_children[0].GetKind() == BEEV::NOT)
+        {
+              return back_children[0][0];
+        }
+
+        ASTVec children(back_children);
 	// The Bitvector solver seems to expect constants on the RHS, variables on the LHS.
 	// We leave the order of equals children as we find them.
 	if (BEEV::isCommutative(kind) && kind != BEEV::AND)
@@ -26,17 +31,8 @@ BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind,	const BEEV::ASTVec
 		SortByArith(children);
 	}
 
-	// We can't create NOT(NOT (..)) nodes because of how the numbering scheme we use works.
-	// So you can't trust the hashiing node factory even to return nodes of the same kind that
-	// you ask for.
-	if (kind == BEEV::NOT && children[0].GetKind() == BEEV::NOT)
-	  {
-		delete n_ptr;
-		return children[0][0];
-	  }
-
-	// insert all of children at end of new_children.
-	ASTNode n(bm.CreateInteriorNode(kind, n_ptr, children));
+        ASTInterior *n_ptr = new ASTInterior(kind,children);
+	ASTNode n(bm.LookupOrCreateInterior(n_ptr));
 	return n;
 }