From ef0d4fb9384fd2a6995d29f8170be0dc430801dd Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 18 Mar 2011 00:16:20 +0000 Subject: [PATCH] Improvement. Add more operations to the unsigned interval analysis. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1216 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/EstablishIntervals.h | 210 +++++++++++++++++++++++++++- 1 file changed, 204 insertions(+), 6 deletions(-) diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h index 2a5a627..53117b9 100644 --- a/src/simplifier/EstablishIntervals.h +++ b/src/simplifier/EstablishIntervals.h @@ -22,17 +22,42 @@ namespace BEEV { minV = _min; maxV = _max; + assert(minV != NULL); + assert(maxV != NULL); + assert(size_(minV) == size_(maxV)); } void print() { - cerr << *(minV) << " " << *(maxV) << endl; + if (size_(minV) <= sizeof(unsigned int)) + 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() { return !CONSTANTBV::BitVector_Lexicompare(minV, maxV); } + + bool isComplete() + { + return (CONSTANTBV::BitVector_is_empty(minV) && CONSTANTBV::BitVector_is_full(maxV)); + } + + bool checkInvariant() + { + assert( CONSTANTBV::BitVector_Lexicompare(minV, maxV) <=0); + + // We use NULL to represent the complete domain. + assert( !isComplete()); + } }; vector toDeleteLater; @@ -40,6 +65,7 @@ namespace BEEV IntervalType * freshUnsignedInterval(int width) { + assert(width > 0); IntervalType *it = createInterval(makeCBV(width), makeCBV(width)); CONSTANTBV::BitVector_Fill(it->maxV); return it; @@ -289,6 +315,11 @@ namespace BEEV result = freshUnsignedInterval(n.GetValueWidth()); CONSTANTBV::BitVector_Copy(result->maxV , children[1]->maxV); CONSTANTBV::BitVector_decrement(result->maxV); + + // If the top is known, and it's maximum is less, use that. + if (knownC0 && CONSTANTBV::BitVector_Lexicompare(children[0]->maxV,result->maxV) < 0) + CONSTANTBV::BitVector_Copy(result->maxV , children[0]->maxV); + } } else if (BVSX == n.GetKind() && knownC0 && knownC1) @@ -316,6 +347,167 @@ namespace BEEV CONSTANTBV::BitVector_Bit_Off(result->maxV,i); } } + else if (BVNEG == n.GetKind() && knownC0) // NOT of the bitvector. + { + result = freshUnsignedInterval(width); + CONSTANTBV::BitVector_Copy(result->maxV, children[0]->minV); + CONSTANTBV::BitVector_Flip(result->maxV); + CONSTANTBV::BitVector_Copy(result->minV, children[0]->maxV); + CONSTANTBV::BitVector_Flip(result->minV); + } + else if (BVUMINUS == n.GetKind() && knownC0) + { + // Imagine it's {00, 01}, the unary minus of these is: {00,11}, + // i.e. it's everything. When there's a zero, (except for [0,0]), + // it will be everything. + + if (!CONSTANTBV::BitVector_is_empty(children[0]->minV)) + { + result = freshUnsignedInterval(width); + CONSTANTBV::BitVector_Copy(result->maxV, children[0]->minV); + CONSTANTBV::BitVector_Flip(result->maxV); + CONSTANTBV::BitVector_increment(result->maxV); + + CONSTANTBV::BitVector_Copy(result->minV, children[0]->maxV); + CONSTANTBV::BitVector_Flip(result->minV); + CONSTANTBV::BitVector_increment(result->minV); + } + } + else if (ITE == n.GetKind() && children[1] != NULL && children[2] != NULL) + { + // Both terms and propositions. + result = freshUnsignedInterval(width==0? 1: width); + CBV min, max; + if (CONSTANTBV::BitVector_Lexicompare(children[1]->minV, children[2]->minV) >0) + min = children[2]->minV; + else + min = children[1]->minV; + + if (CONSTANTBV::BitVector_Lexicompare(children[1]->maxV, children[2]->maxV) >0) + max = children[1]->maxV; + else + max = children[2]->maxV; + + CONSTANTBV::BitVector_Copy(result->minV, min); + CONSTANTBV::BitVector_Copy(result->maxV, max); + } + else if (BVMULT == n.GetKind() && knownC0 && knownC1) + { + // >=2 arity. + CBV min,max; + min = CONSTANTBV::BitVector_Create(2*width, true); + max = CONSTANTBV::BitVector_Create(2*width, true); + + // Make the result interval 1. + result = freshUnsignedInterval(width); + CONSTANTBV::BitVector_increment(result->minV); + CONSTANTBV::BitVector_Flip(result->maxV); + CONSTANTBV::BitVector_increment(result->maxV); + + bool bad= false; + for (int i =0; i < children.size(); i++) + { + if (children[i] == NULL) + { + bad = true; + break; + } + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Multiply(min, result->minV, children[i]->minV); + assert (0 == e); + + e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV); + assert (0 == e); + + if (CONSTANTBV::Set_Max(max) >= width) + bad = true; + + for (int j = width; j < 2 * width; j++) + { + if (CONSTANTBV::BitVector_bit_test(min, j)) + bad = true; + } + + CONSTANTBV::BitVector_Interval_Copy(result->minV, min, 0, 0, width); + CONSTANTBV::BitVector_Interval_Copy(result->maxV, max, 0, 0, width); + } + CONSTANTBV::BitVector_Destroy(min); + CONSTANTBV::BitVector_Destroy(max); + if (bad) + result = NULL; + } + else if (false && BVLEFTSHIFT == n.GetKind() && knownC0 && knownC1) + { + // Todo two cases. + // 1) The maximum shift of the maximum value doesn't overflow, and, + // 2) The minimum shift of the minimum value completely overflows (to zero). + } + else if (BVAND == n.GetKind()) + { + //int max=width; + //for (int i =0 ; i < children.size(); i++) + //{ + //if (children[i] != NULL) +// CONSTANTBV::Set_Max(children[1]->minV) + // } + } + else if (BVRIGHTSHIFT == n.GetKind() && knownC0 && knownC1) + { + result = freshUnsignedInterval(width); + + // The maximum result is the maximum >> (minimum shift). + if (CONSTANTBV::Set_Max(children[1]->minV) > 1 + log2(width) || *(children[1]->minV) > width) + { + // The maximum is zero. + CONSTANTBV::BitVector_Flip(result->maxV); + } + else + { + unsigned shift_amount = *(children[1]->minV); + CONSTANTBV::BitVector_Copy(result->maxV, children[0]->maxV); + while (shift_amount-- > 0) + CONSTANTBV::BitVector_shift_right(result->maxV,0); + } + + // The minimum result is the minimum >> (maximum shift). + if (CONSTANTBV::Set_Max(children[1]->maxV) > 1 + log2(width) || *(children[1]->maxV) > width) + { + // The mimimum is zero. (which it's set to by default.). + } + else + { + unsigned shift_amount = *(children[1]->maxV); + CONSTANTBV::BitVector_Copy(result->minV, children[0]->minV); + while (shift_amount-- > 0) + CONSTANTBV::BitVector_shift_right(result->minV,0); + } + } + else if (BVPLUS == n.GetKind() && knownC0 && knownC1) + { + // >=2 arity. + result = freshUnsignedInterval(width); + CONSTANTBV::BitVector_Flip(result->maxV); // make the max zero too. + + bool carry = false; + + for (int i =0; i < children.size(); i++) + { + if (children[i] == NULL) + { + carry = true; + break; + } + + CONSTANTBV::BitVector_add(result->maxV,result->maxV, children[i]->maxV, &carry); + if (carry) + break; + CONSTANTBV::BitVector_add(result->minV,result->minV, children[i]->minV, &carry); + if (carry) + break; + } + + if (carry) + result = NULL; + } else if (BVCONCAT == n.GetKind() && (knownC0 || knownC1)) { result = freshUnsignedInterval(n.GetValueWidth()); @@ -369,15 +561,21 @@ namespace BEEV if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND) { - cerr << n; - for (int i=0; i < n.Degree();i++) - children[i]->print(); + cerr << n; + for (int i=0; i < n.Degree();i++) + children[i]->print(); } } + if (result != NULL && result->isComplete()) + result = NULL; + + if (result != NULL) + result->checkInvariant(); + // result will often be null (which we take to mean the maximum range). - visited.insert(make_pair(n,result)); - return result; + visited.insert(make_pair(n,result)); + return result; } STPMgr& bm; -- 2.47.3