From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 15 Sep 2009 02:39:39 +0000 (+0000)
Subject: The constant evaluator can now evaluate shifts by amounts > MAX_INT. Prior, if an... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=07c33e43bbfb2c8e73a000d2d9e5f9a648aa5c98;p=francis%2Fstp.git

The constant evaluator can now evaluate shifts by amounts > MAX_INT. Prior, if an attempt was made to shift a value, by say, 2^100, it would fail because the shift amount was loaded into an integer.



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 294388e..f0d026b 100644
--- 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:
         {