From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 2 Feb 2012 12:28:24 +0000 (+0000)
Subject: A fixed version r1547. I missed a bound.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2dc3e4af1b05caa9471e4c5feca53bc6c3054e79;p=francis%2Fstp.git

A fixed version r1547. I missed a bound.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1549 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp
index 88604ca..6ee9d7b 100644
--- a/src/simplifier/constantBitP/FixedBits.cpp
+++ b/src/simplifier/constantBitP/FixedBits.cpp
@@ -362,43 +362,47 @@ namespace simplifier
       return true;
     }
 
-    // Gets the minimum and maximum unsigned values that are represented by the set "shift".
+    // Gets the minimum and maximum unsigned values that are held in the current
+    // set. It saturates to UINT_MAX.
     void
     FixedBits::getUnsignedMinMax(unsigned &minShift, unsigned &maxShift) const
     {
-      const FixedBits& shift = *this;
+      const int bitWidth = this->getWidth();
+      int unsignedBW = sizeof(unsigned)*8;
 
-      // Get the unsigned minimum and maximum of the shift.
-      BEEV::CBV minCBV = CONSTANTBV::BitVector_Create(shift.getWidth(), true);
-      BEEV::CBV maxCBV = CONSTANTBV::BitVector_Create(shift.getWidth(), true);
+      minShift = 0;
+      maxShift = 0;
 
-      setUnsignedMinMax(shift, minCBV, maxCBV);
+      bool bigMax = false;
+      bool bigMin = false;
 
-      BEEV::CBV maxValue = CONSTANTBV::BitVector_Create(shift.getWidth(), true);
-      for (unsigned i = 0; i < sizeof(unsigned) * 8; i++)
-        CONSTANTBV::BitVector_Bit_On(maxValue, i);
-
-      if (unsignedCompare(minCBV, maxValue) > 0)
-        {
-          minShift = UINT_MAX;
-        }
-      else
+      for (int i = unsignedBW; i < bitWidth; i++)
         {
-          minShift = cbvTOInt(minCBV);
-        }
+        if  ((*this)[i] == '1' || (*this)[i] == '*')
+          bigMax = true;
 
-      if (unsignedCompare(maxCBV, maxValue) > 0)
-        {
-          maxShift = UINT_MAX;
+         if ((*this)[i] == '1')
+          bigMin = true;
         }
-      else
+
+      for (int i = 0; i < std::min(unsignedBW,bitWidth); i++)
         {
-          maxShift = cbvTOInt(maxCBV);
+          if ((*this)[i] == '1')
+            {
+              minShift |= (1 <<i);
+              maxShift |= (1 <<i);
+            }
+          else if ((*this)[i] == '*')
+            {
+              maxShift |= (1 <<i);
+            }
         }
 
-      CONSTANTBV::BitVector_Destroy(maxValue);
-      CONSTANTBV::BitVector_Destroy(minCBV);
-      CONSTANTBV::BitVector_Destroy(maxCBV);
+      if (bigMax)
+        maxShift = UINT_MAX;
+
+      if (bigMin)
+        minShift = UINT_MAX;
     }
 
     bool