Revert. The prior change to min/max has some problem I don't understand yet.

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

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