From 32442685864f069b18e9fd4d1a7b6624abf44b24 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Mar 2011 03:47:25 +0000 Subject: [PATCH] Improvement. The simplifying node factory now eliminates extract over extracts, as well as some extract over concats. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1244 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index d638808..d47bb7a 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -769,6 +769,41 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = children[0][0]; break; + case BEEV::BVEXTRACT: + if (width == children[0].GetValueWidth()) + result = children[0]; + else if (BEEV::BVEXTRACT == children[0].GetKind()) // reduce an extract over an extract. + { + const unsigned outerLow = children[2].GetUnsignedConst(); + const unsigned outerHigh = children[1].GetUnsignedConst(); + + const unsigned innerLow = children[0][2].GetUnsignedConst(); + const unsigned innerHigh = children[0][1].GetUnsignedConst(); + result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + + innerLow), bm.CreateBVConst(32, outerLow + innerLow)); + } + else if (BEEV::BVCONCAT == children[0].GetKind()) + { + // If the extract doesn't cross the concat, then remove the concat. + const ASTNode& a = children[0][0]; + const ASTNode& b = children[0][1]; + + const unsigned low = children[2].GetUnsignedConst(); + const unsigned high = children[1].GetUnsignedConst(); + + if (high < b.GetValueWidth()) // Extract entirely from the lower value (b). + { + result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, b, children[1], children[2]); + } + if (low >= b.GetValueWidth()) // Extract entirely from the upper value (a). + { + ASTNode i = bm.CreateBVConst(32, high - b.GetValueWidth()); + ASTNode j = bm.CreateBVConst(32, low - b.GetValueWidth()); + result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, a, i, j); + } + } + break; + case BEEV::BVPLUS: if (children.size() == 2) { -- 2.47.3