Implementation of rotate_left & rotate_right

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

diff --git a/parser/smtlib.lex b/parser/smtlib.lex
index c33682a6610d05d1ef1fda962eeda04d3182403f..9490bf098afcfc7f2342900f5b68ab47144b393c 100644 (file)
--- a/parser/smtlib.lex
+++ b/parser/smtlib.lex
@@ -215,6 +215,10 @@ bit{DIGIT}+     {
 
 "zero_extend"   { return BVZX_TOK;}
 "sign_extend"   { return BVSX_TOK;} 
+
+"rotate_left"   { return BVROTATE_LEFT_TOK;}
+"rotate_right"   { return BVROTATE_RIGHT_TOK;} 
+
 "boolextract"   { return BOOLEXTRACT_TOK;}
 "boolbv"        { return BOOL_TO_BV_TOK;}
 

diff --git a/parser/smtlib.y b/parser/smtlib.y
index d9309f4c8862a630e9a6ba4ce430be5fd3099f23..b1ed1510682333c989cc7f7f19906cd9ac57d740 100644 (file)
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -191,6 +191,8 @@
 %token BVSGE_TOK
 %token BVSX_TOK 
 %token BVZX_TOK
+%token BVROTATE_RIGHT_TOK
+%token BVROTATE_LEFT_TOK
 %token BOOLEXTRACT_TOK
 %token BOOL_TO_BV_TOK
 %token BVEXTRACT_TOK
@@ -1069,6 +1071,70 @@ an_nonbvconst_term:
       delete $2;
       delete $3;
     }
+  |  BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
+    {
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
+      
+      BEEV::ASTNode *n;
+      unsigned width = $5->GetValueWidth();
+      unsigned rotate = $3;
+      if (0 == rotate)
+      {
+       n = $5;
+      }
+      else if (rotate < width)
+      {
+       BEEV::ASTNode high = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-1);
+       BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0);
+       BEEV::ASTNode cut = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-rotate);
+       BEEV::ASTNode cutMinusOne = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-rotate-1);
+
+       BEEV::ASTNode top =  BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,rotate,*$5,high, cut);
+       BEEV::ASTNode bottom =  BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,width-rotate,*$5,cutMinusOne,zero);
+       n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,width,bottom,top));
+        delete $5;
+      }
+      else
+      {
+       yyerror("Rotate must be strictly less than the width.");
+      }
+      
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+      $$ = n;
+      
+    }
+    |  BVROTATE_RIGHT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
+    {
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
+      
+      BEEV::ASTNode *n;
+      unsigned width = $5->GetValueWidth();
+      unsigned rotate = $3;
+      if (0 == rotate)
+      {
+       n = $5;
+      }
+      else if (rotate < width)
+      {
+       BEEV::ASTNode high = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-1);
+       BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0);
+       BEEV::ASTNode cut = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,rotate); 
+       BEEV::ASTNode cutMinusOne = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,rotate-1);
+
+       BEEV::ASTNode bottom =  BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,rotate,*$5,cutMinusOne, zero);
+       BEEV::ASTNode top =  BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,width-rotate,*$5,high,cut);
+       n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,width,bottom,top));
+        delete $5;
+      }
+      else
+      {
+       yyerror("Rotate must be strictly less than the width.");
+      }
+      
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+      $$ = n;
+      
+    }
   |  BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
     {
       BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);