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

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index 64d458f9f3d81830057d9349b0f1fa48b5fd8c90..ede5925a812dea983129f02ae657be6e5856a9d3 100644 (file)
--- 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).