From 161250d98e943b73e4a308a323bf3a28b8f429a0 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 25 Mar 2011 11:55:20 +0000 Subject: [PATCH] Improvement. Better unsigned interval propagation of BVRIGHTSHIFT. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1237 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/EstablishIntervals.h | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h index 64d458f..ede5925 100644 --- a/src/simplifier/EstablishIntervals.h +++ b/src/simplifier/EstablishIntervals.h @@ -29,13 +29,13 @@ namespace BEEV void print() { - if (size_(minV) <= sizeof(unsigned int)) + if (size_(minV) == 1) cerr << *(minV) << " " << *maxV << endl; - else + else { unsigned char * a = CONSTANTBV::BitVector_to_Dec(minV); unsigned char * b = CONSTANTBV::BitVector_to_Dec(maxV); - cerr << *a << " " << *b << endl; + cerr << a << " " << b << endl; free(a); free(b); } @@ -465,6 +465,7 @@ namespace BEEV break; //case BVLEFTSHIFT: // case BVAND: + //case BVSRSHIFT: { // Todo two cases. // 1) The maximum shift of the maximum value doesn't overflow, and, @@ -472,10 +473,15 @@ namespace BEEV } case BVRIGHTSHIFT: - if (knownC0 && knownC1) + if (knownC0 || knownC1) { result = freshUnsignedInterval(width); + if (children[0] == NULL) + children[0] = freshUnsignedInterval(width); + if (children[1] == NULL) + children[1] = freshUnsignedInterval(width); + // The maximum result is the maximum >> (minimum shift). if (CONSTANTBV::Set_Max(children[1]->minV) > 1 + log2(width) || *(children[1]->minV) > width) { @@ -487,7 +493,9 @@ namespace BEEV 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); + { + CONSTANTBV::BitVector_shift_right(result->maxV,0); + } } // The minimum result is the minimum >> (maximum shift). -- 2.47.3