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 b1dda28e6699608fe2df1f212d0dc06b32a39131..48fe2a01be7d8fe4e5b5aacae7b4fb7e69fac598 100644 (file)
--- 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;
 }