From 7efaa7f1995897684f03e4b3aa5b5a7f264e4105 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 24 Mar 2011 05:52:02 +0000 Subject: [PATCH] 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 --- src/AST/NodeFactory/HashingNodeFactory.cpp | 28 ++++++++++------------ 1 file changed, 12 insertions(+), 16 deletions(-) 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; } -- 2.47.3