From 2cb074ee47a5686587dbbcd048846dd302bfd140 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 27 Apr 2011 06:52:58 +0000 Subject: [PATCH] Extra simplification rules. In particular a simple signed interval analysis. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1286 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 15 +++ src/STPManager/STP.h | 2 +- src/simplifier/EstablishIntervals.h | 95 +++++++++++++++++-- 3 files changed, 101 insertions(+), 11 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index d7dd803..05efa15 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -109,6 +109,14 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) if (children[0] == smallestNumber) result = ASTFalse; } + + if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][1] == children[1][1]) + result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][0], children[1][0]); + + if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][0] == children[1][0]) + result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][1], children[1][1]); + + break; case BEEV::BVGT: @@ -119,6 +127,13 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) result = ASTFalse; if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) result = ASTFalse; + if (children[0].GetKind() == BEEV::BVRIGHTSHIFT && children[0][0] == children[1]) + result = ASTFalse; + if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][1] == children[1][1]) + result = NodeFactory::CreateNode(BEEV::BVGT, children[0][0], children[1][0]); + if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][0] == children[1][0]) + result = NodeFactory::CreateNode(BEEV::BVGT, children[0][1], children[1][1]); + break; case BEEV::BVGE: diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index da943de..2973d17 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -26,7 +26,7 @@ namespace BEEV { class STP { -private: +public: ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver); public: diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h index 747a375..590ebc3 100644 --- a/src/simplifier/EstablishIntervals.h +++ b/src/simplifier/EstablishIntervals.h @@ -29,16 +29,13 @@ namespace BEEV void print() { - if (size_(minV) == 1) - cerr << *(minV) << " " << *maxV << endl; - else - { + unsigned char * a = CONSTANTBV::BitVector_to_Dec(minV); unsigned char * b = CONSTANTBV::BitVector_to_Dec(maxV); cerr << a << " " << b << endl; free(a); free(b); - } + } bool isConstant() @@ -51,13 +48,28 @@ namespace BEEV return (CONSTANTBV::BitVector_is_empty(minV) && CONSTANTBV::BitVector_is_full(maxV)); } - bool checkInvariant() + bool checkUnsignedInvariant() { assert( CONSTANTBV::BitVector_Lexicompare(minV, maxV) <=0); // We use NULL to represent the complete domain. assert( !isComplete()); } + + // If the interval is interpreted as a clockwise interval. + bool crossesSignedUnsigned(int width) + { + bool minMSB = CONSTANTBV::BitVector_bit_test(minV, width- 1); + bool maxMSB = CONSTANTBV::BitVector_bit_test(maxV, width- 1); + + // If the min is zero, and the max is one, then it must cross. + if (!minMSB && maxMSB) + return true; + if (!(minMSB ^ maxMSB)) // bits are the same. + return CONSTANTBV::BitVector_Compare(minV, maxV) >0; + return false; + } + }; vector toDeleteLater; @@ -135,7 +147,8 @@ namespace BEEV { bm.GetRunTimes()->start(RunTimes::IntervalPropagation); map visited; - visit(top,visited); + map clockwise; + visit(top,visited, clockwise); ASTNodeMap fromTo; ASTNodeMap onePass; for (map::const_iterator it = visited.begin(); it != visited.end(); it++) @@ -304,7 +317,8 @@ namespace BEEV private: // A single pass through the problem replacing things that must be true of false. - IntervalType* visit(const ASTNode& n, map & visited) + // clockwise are intervals that go clockwise around the circle from low to high. + IntervalType* visit(const ASTNode& n, map & visited, map & clockwise) { map::iterator it; if ((it = visited.find(n)) != visited.end()) @@ -315,7 +329,7 @@ namespace BEEV children.reserve(number_children); for (int i=0; i < number_children;i++) { - children.push_back(visit(n[i],visited)); + children.push_back(visit(n[i],visited,clockwise)); } IntervalType * result = NULL; @@ -372,6 +386,48 @@ namespace BEEV if (CONSTANTBV::BitVector_Lexicompare(children[1]->minV,children[0]->maxV) >=0) result = createInterval(littleZero, littleZero); } + if (BVSGT == n.GetKind() && result ==NULL) + { + map::iterator clock_it; + clock_it = clockwise.find(n[0]); + IntervalType* clock0 = NULL; + IntervalType* clock1 = NULL; + if (clock_it != clockwise.end()) + clock0 = clock_it->second; + clock_it = clockwise.find(n[1]); + if (clock_it != clockwise.end()) + clock1 = clock_it->second; + + if (clock0 != NULL || clock1 !=NULL) + { + if (clock0 == NULL) + clock0 = children[0]; + if (clock1 == NULL) + clock1 = children[1]; + + if (clock0 != NULL && clock1 != NULL) + { +/* + clock0->print(); + clock1->print(); + cerr << clock0->crossesSignedUnsigned(n[0].GetValueWidth()) << endl; + cerr << clock1->crossesSignedUnsigned(n[0].GetValueWidth()) << endl; + cerr << n; +*/ + + // if the rhs doesn't cross +ve/-ve boundary, and the min > max + if (!clock0->crossesSignedUnsigned(n[0].GetValueWidth()) && !clock1->crossesSignedUnsigned(n[1].GetValueWidth())) + { + if (CONSTANTBV::BitVector_Compare(clock0->minV,clock1->maxV) >0) + result = createInterval(littleOne, littleOne); + + if (CONSTANTBV::BitVector_Compare(clock1->minV,clock0->maxV) >=0) + result = createInterval(littleZero, littleZero); + } + } + } + } + break; case BVGE: case BVSGE: @@ -454,7 +510,26 @@ namespace BEEV for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) CONSTANTBV::BitVector_Bit_Off(result->maxV,i); } + } else if (knownC1) + { + // Ignores what's already there for now.. + + IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth()); + for (int i=0; i < n[0].GetValueWidth()-1;i++) + { + CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i); + CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i); + } + + for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) + { + CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i); + CONSTANTBV::BitVector_Bit_On(circ_result->minV,i); + } + + clockwise.insert(make_pair(n, circ_result)); } + break; case BVNEG: if (knownC0) // NOT of the bitvector. @@ -696,7 +771,7 @@ namespace BEEV result = NULL; if (result != NULL) - result->checkInvariant(); + result->checkUnsignedInvariant(); // result will often be null (which we take to mean the maximum range). visited.insert(make_pair(n,result)); -- 2.47.3