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 7bf23c21fe425ce2f4e85d279968ddcd07d35f42..97dedeadfe5b2a6feabc3f57f31f56cda9951e42 100644 (file)
--- 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;