The constant evaluator can now evaluate shifts by amounts > MAX_INT. Prior, if an...

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

diff --git a/src/const-evaluator/consteval.cpp b/src/const-evaluator/consteval.cpp
index 294388e961ef81f85a6c4bcd3f7f8fa11e7a396c..f0d026bc489c59f353be16aa8c8861de369786a2 100644 (file)
--- a/src/const-evaluator/consteval.cpp
+++ b/src/const-evaluator/consteval.cpp
@@ -111,49 +111,59 @@ namespace BEEV
           break;
         }
 
-      case BVLEFTSHIFT:
-        {
-          output = CONSTANTBV::BitVector_Create(inputwidth, true);
-
-          // the shift is destructive, get a copy.
-          CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
-
-          // get the number of bits to shift it.
-          unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1]));
-
-          CONSTANTBV::BitVector_Move_Left(output, shift);
-          OutputNode = CreateBVConst(output, outputwidth);
-          break;
-        }
-      case BVRIGHTSHIFT:
-      case BVSRSHIFT:
-        {
-          bool msb = CONSTANTBV::BitVector_msb_(tmp0);
-
-          output = CONSTANTBV::BitVector_Create(inputwidth, true);
+        case BVLEFTSHIFT:
+               case BVRIGHTSHIFT:
+               case BVSRSHIFT:
+               {
+                       // load in the bitWidth.
+                       CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
+                               if ((inputwidth & (0x1 << i)) != 0)
+                                       CONSTANTBV::BitVector_Bit_On(width, i);
+
+                       output = CONSTANTBV::BitVector_Create(inputwidth, true);
+
+                       // Number of bits to shift it.
+                       ASTNode shiftNode = BVConstEvaluator(t[1]);
+
+                       bool msb = CONSTANTBV::BitVector_msb_(tmp0);
+
+                       // If this shift is greater than the bitWidth, make it zero.
+                       if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
+                       {
+                               if (k == BVSRSHIFT && msb)
+                                       CONSTANTBV::Set_Complement(output, output);
+                       }
+                       else
+                       {
+                               // the shift is destructive, get a copy.
+                               CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
+
+                               unsigned int shift = GetUnsignedConst(shiftNode);
+
+                               if (k == BVLEFTSHIFT)
+                                       CONSTANTBV::BitVector_Move_Left(output, shift);
+                               else
+                                       CONSTANTBV::BitVector_Move_Right(output, shift);
+
+                               if (k == BVSRSHIFT && msb)
+                               {
+                                       // signed shift, and the number was originally negative.
+                                       // Shift may be larger than the inputwidth.
+                                       for (unsigned int i = 0; i < min(shift, inputwidth); i++)
+                                       {
+                                               CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
+                                       }
+                                       assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative.
+                               }
+                       }
+
+                       OutputNode = CreateBVConst(output, outputwidth);
+
+                       CONSTANTBV::BitVector_Destroy(width);
+                       break;
+               }
 
-          // the shift is destructive, get a copy.
-          CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
-
-          // get the number of bits to shift it.
-          unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1]));
-
-          CONSTANTBV::BitVector_Move_Right(output, shift);
-
-          if (BVSRSHIFT == k && msb)
-            {
-              // signed shift, and the number was originally negative.
-              // Shift may be larger than the inputwidth.
-              for (unsigned int i = 0; i < min(shift, inputwidth); i++)
-                {
-                  CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
-                }
-              assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative.
-            }
-
-          OutputNode = CreateBVConst(output, outputwidth);
-          break;
-        }
 
       case BVAND:
         {