From 9033e5379802ebe41d520ce80b0defb96a3be5dd Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 9 May 2011 03:57:25 +0000 Subject: [PATCH] Adds two extra simplfication rules. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1316 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 78 +++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index eefa74a..2310e73 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -1012,6 +1012,7 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, oneFound = true; else if (CONSTANTBV::BitVector_is_empty(children[i].GetBVConst())) zeroFound = true; + } } @@ -1043,6 +1044,61 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, { result = children[0]; } + + // If there is just one run of 1 bits, replace by an extract and a concat. + // i.e. 00011111111000000 & x , will be replaced by an extract of x just where + // there are one bits. This should + if (children.size() ==2 && (children[0].isConstant() || children[1].isConstant())) + { + ASTNode c0 = children[0]; + ASTNode c1 = children[1]; + if (c1.isConstant()) + { + ASTNode t = c0; + c0 = c1; + c1 = t; + } + + int start=-1; + int end=-1; + BEEV::CBV c = c0.GetBVConst(); + bool bad= false; + for (int i =0; i < width; i++) + { + if (CONSTANTBV::BitVector_bit_test(c,i)) + if (start == -1) + start = i; // first one bit. + else if (end != -1) + bad = true; + + if (!CONSTANTBV::BitVector_bit_test(c,i)) + if (start != -1 && end==-1) + end = i-1; // end of run. + } + if (start != -1 && end == -1) + end = width-1; + + if (!bad && start !=-1) + { + assert(end != -1); + + result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, end-start+1, c1, bm.CreateBVConst(32,end) , bm.CreateBVConst(32,start)); + + if (start > 0) + { + ASTNode z = bm.CreateZeroConst(start); + result = NodeFactory::CreateTerm(BEEV::BVCONCAT, end+1, result,z); + } + if (end < width-1) + { + ASTNode z = bm.CreateZeroConst(width-end-1); + result = NodeFactory::CreateTerm(BEEV::BVCONCAT, width, z,result); + } + } + } + + + break; case BEEV::BVSX: @@ -1072,6 +1128,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = NodeFactory::CreateTerm(BEEV::BVNEG, width, children[0][1]); else if (children[0].GetKind() == BEEV::BVNEG) result = NodeFactory::CreateTerm(BEEV::BVPLUS, width, children[0][0], bm.CreateOneConst(width)); + else if (children[0].GetKind() == BEEV::BVSX && children[0][0].GetValueWidth() ==1) + result = NodeFactory::CreateTerm(BEEV::BVCONCAT, width, bm.CreateZeroConst(width-1), children[0][0]); break; case BEEV::BVEXTRACT: @@ -1115,6 +1173,26 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = plusRules(children[0],children[1]); if (result.IsNull()) result = plusRules(children[1],children[0]); + +#if 0 + // This slowed down some of the smtcomp2007 problems x4 total runtime. + + // Put the unary minus on the node with the lowest variable number. + if (result.IsNull() && children[0].GetKind() == BEEV::BVUMINUS && !arithless(children[0][0], children[1])) + { + // Need to be swapped. + ASTNode r = NodeFactory::CreateTerm(BEEV::BVUMINUS, width, children[1]); + ASTNode p = NodeFactory::CreateTerm(BEEV::BVPLUS, width, r, children[0][0]); + result = NodeFactory::CreateTerm(BEEV::BVUMINUS, width, p); + } + else if (result.IsNull() && children[1].GetKind() == BEEV::BVUMINUS && arithless(children[0], children[1][0])) + { + // Need to be swapped. + ASTNode r = NodeFactory::CreateTerm(BEEV::BVUMINUS, width, children[0]); + ASTNode p = NodeFactory::CreateTerm(BEEV::BVPLUS, width, r, children[1][0]); + result = NodeFactory::CreateTerm(BEEV::BVUMINUS, width, p); + } +#endif } break; -- 2.47.3