Improvement. 10x better min and max value out of the sets of fixed bits.

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

diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp
index 88604ca99c70937f65fdae3a353e0190eb7e6bc4..f829762bd20ee4be3c879bc925ec2d9acd3bdbc0 100644 (file)
--- 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 < unsignedBW; 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