From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 27 Jul 2009 13:16:22 +0000 (+0000)
Subject: Implementation of rotate_left & rotate_right
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b86aa1296ed93bed4780399f2d567b9ebb09fb0c;p=francis%2Fstp.git

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 c33682a..9490bf0 100644
--- 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 d9309f4..b1ed151 100644
--- 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);