From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 9 Mar 2010 13:39:26 +0000 (+0000)
Subject: Bugfix. Rightshift in CVC was broken. Thanks to Elnatan Reisner for the patch.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8787f3d86719d7684d2ae747ecb9d82a157eb515;p=francis%2Fstp.git

Bugfix. Rightshift in CVC was broken. Thanks to Elnatan Reisner for the patch.



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

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 7bf23c2..97dedea 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -1011,57 +1011,8 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
   // $1 (THEEXPR) is being shifted
   //
   // $3 is the variable shift amount
-  ASTNode inputExpr = *$1;
-  ASTNode varShiftAmt = *$3;
-
-  unsigned int exprWidth = $1->GetValueWidth();
-  unsigned int shiftAmtWidth = $3->GetValueWidth();
-  ASTNode exprWidthNode = ParserBM->CreateBVConst(shiftAmtWidth, exprWidth);
-  
-  ASTNode cond, thenExpr, elseExpr;
-  unsigned int count = 0;
-  ASTNode hi = ParserBM->CreateBVConst(32,exprWidth-1);
-  while(count < exprWidth)
-    {
-      if(0 == count)
-	{
-	  // if count is zero then the appropriate rightshift expression is
-	  // THEEXPR itself
-	  elseExpr = inputExpr;
-	}
-      else
-	{
-	  // 1 <= count < exprWidth
-	  //
-	  // Construct appropriate conditional
-	  ASTNode countNode = ParserBM->CreateBVConst(shiftAmtWidth, count);
-	  cond = ParserBM->CreateNode(EQ, countNode, varShiftAmt);
-
-	  //Construct the rightshift expression padding @ Expr[hi:low]
-	  ASTNode low =
-	    ParserBM->CreateBVConst(32,count);
-	  ASTNode extract =
-	    ParserBM->CreateTerm(BVEXTRACT,exprWidth-count,inputExpr,hi,low);
-	  ASTNode padding =
-	    ParserBM->CreateZeroConst(count);
-	  thenExpr =
-	    ParserBM->CreateTerm(BVCONCAT, exprWidth, padding, extract);
-	  ASTNode ite =
-	    ParserBM->CreateTerm(ITE, exprWidth, cond, thenExpr, elseExpr);
-	  BVTypeCheck(ite);
-	  elseExpr = ite;
-	}
-      count++;
-    } //End of while loop
-
-  // if shiftamount is greater than or equal to exprwidth, then
-  // output is zero.
-  cond = ParserBM->CreateNode(BVGE, varShiftAmt, exprWidthNode);
-  thenExpr = ParserBM->CreateZeroConst(exprWidth);
-  ASTNode * ret =
-    new ASTNode(ParserBM->CreateTerm(ITE,
-				     exprWidth,
-				     cond, thenExpr, elseExpr));
+  unsigned int width = $1->GetValueWidth();
+  ASTNode * ret = new ASTNode(ParserBM->CreateTerm(BVRIGHTSHIFT, width, *$1, *$3));
   BVTypeCheck(*ret);
   //cout << *ret;