added variable right shift to the CVC parser

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

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 2bf9ad9743aa48260695ff01968452b99bc29e0f..aad561c7c23fc932f4d176966a5795f24f3b4578 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -919,7 +919,7 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
   $$ = n;
   delete $1;
 }
-|      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK 
+|      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK
 {
   ASTNode len = ParserBM->CreateZeroConst($3);
   unsigned int w = $1->GetValueWidth();
@@ -934,20 +934,77 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
     ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, w,len, extract));
     BVTypeCheck(*n);
     $$ = n;
-  } 
+  }
   else
-    $$ = new ASTNode(ParserBM->CreateZeroConst(w));                      
+    $$ = new ASTNode(ParserBM->CreateZeroConst(w));
 
   delete $1;
 }
-/* |      Expr BVRIGHTSHIFT_TOK Expr */
-/* { */
-/*   //$1 is being shifted by variable shift amount $3 */
-/*   // */
+|      Expr BVRIGHTSHIFT_TOK Expr
+{
+  // VARIABLE RIGHT SHIFT
+  //
+  // $1 (THEEXPR) is being shifted
+  //
+  // $3 is the variable shift amount
+  ASTNode inputExpr = *$1;
+  ASTNode varShiftAmt = *$3;
 
-/*   delete $1; */
-/*   delete $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));
+  BVTypeCheck(*ret);
+  //cout << *ret;
+
+  $$ = ret;
+  delete $1;
+  delete $3;
+}
 |      BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' 
 {
   ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, $3, *$5));

diff --git a/tests/sample-tests/variable-rightshift-invalid.cvc b/tests/sample-tests/variable-rightshift-invalid.cvc
new file mode 100644 (file)
index 0000000..3df311b
--- /dev/null
+++ b/tests/sample-tests/variable-rightshift-invalid.cvc
@@ -0,0 +1,10 @@
+%% Regression level = 3
+%% Result = InValid
+%% Language = presentation
+
+X, Y : BITVECTOR(2);
+
+ASSERT X = 0bin11;
+ASSERT X >> Y = 0bin01;
+
+QUERY FALSE;
\ No newline at end of file

diff --git a/tests/sample-tests/variable-rightshift-valid.cvc b/tests/sample-tests/variable-rightshift-valid.cvc
new file mode 100644 (file)
index 0000000..dc90949
--- /dev/null
+++ b/tests/sample-tests/variable-rightshift-valid.cvc
@@ -0,0 +1,10 @@
+%% Regression level = 3
+%% Result = Valid
+%% Language = presentation
+
+X, Y : BITVECTOR(2);
+
+ASSERT X = 0bin11;
+ASSERT X >> Y = 0bin10;
+
+QUERY FALSE;
\ No newline at end of file