Added zero_extend function. Renamed bvdiv to bvudiv as per specification. Fixed off...

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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index bfb350c38e80e088f26a90c1cc4c73cd152fe715..1a3db0bc2698ca4758007adafd4e5a84ab7e9b24 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -666,6 +666,7 @@ namespace BEEV {
       os << endl;
       break;
     case BVSX:
+    case BVZX: 
       os << kind << "(";
       c[0].PL_Print1(os,indentation,letize);
       os << ",";
@@ -1197,10 +1198,19 @@ namespace BEEV {
       case BVSX:
        //in BVSX(n[0],len), the length of the BVSX term must be
        //greater than the length of n[0]
-       if(n[0].GetValueWidth() >= n.GetValueWidth()) {
+       if(n[0].GetValueWidth() > n.GetValueWidth()) {
          FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n);
        } 
        break;
+
+      case BVZX:
+       //in BVZX(n[0],len), the length of the BVZX term must be
+       //greater than the length of n[0]
+       if(n[0].GetValueWidth() > n.GetValueWidth()) {
+         FatalError("BVTypeCheck: BVZX(t,bvzx_len) : length of 't' must be <= bvzx_len\n",n);
+       }
+       break;
+
       default:
        for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++)
          if(BITVECTOR_TYPE != it->GetType()) {

diff --git a/AST/ASTKind.kinds b/AST/ASTKind.kinds
index b649de1448a4e052e68095cf61db64672961a1da..985ee6224c912c987605dbaaa63c05b2f11f1146 100644 (file)
--- a/AST/ASTKind.kinds
+++ b/AST/ASTKind.kinds
@@ -32,6 +32,7 @@ SBVDIV                2       2       Term
 SBVREM         2       2       Term
 SBVMOD         2       2       Term
 BVSX           1       1       Term
+BVZX           1       1       Term
 BOOLVEC         0       -       Term
 
 # Formula OR term, depending on context

diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp
index f87fa46f0ea690ee4c849cb6e040ef04837944f2..7ebf2de2fecbe565e12f9497c85877649dc72818 100644 (file)
--- a/AST/BitBlast.cpp
+++ b/AST/BitBlast.cpp
@@ -156,6 +156,48 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
       break;
     }
   }
+
+ case BVZX: {
+    // Fill the high-order bits with as many zeroes as needed.
+    // Arg 0 is expression to be sign extended.
+    const ASTNode& arg = term[0];
+    unsigned long result_width = term.GetValueWidth();
+    unsigned long arg_width = arg.GetValueWidth();
+
+      //FIXME Uses a temporary const ASTNode reference
+      const ASTNode& bbarg = BBTerm(arg);
+      ASTVec tmp_res(result_width);
+
+      //FIXME Should these be gotten from result?
+      ASTVec::const_iterator bb_it = bbarg.begin();
+      ASTVec::iterator res_it = tmp_res.begin();
+      ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part
+      ASTVec::iterator res_end = tmp_res.end();
+      // copy LSBs directly from bbvec
+      for( ; res_it < res_ext; (res_it++, bb_it++)) {
+       *res_it = *bb_it;
+      }
+      // repeat zero to fill up rest of result.
+      for( ; res_it < res_end; (res_it++)) {
+               *res_it = ASTFalse;
+      }
+      
+      // Temporary debugging code
+      //         cout << "Zero extending:" << endl 
+      //               << "  Vec ";
+      //    lpvec( bbarg.GetChildren() );
+      //     cout << "  Extended to ";
+      //          cout << result;
+      //   cout << endl;
+      
+      result = CreateNode(BOOLVEC, tmp_res);
+
+      break;
+    }
+
+
+
+
   case BVEXTRACT: {
     // bitblast the child, then extract the relevant bits.
     // Note: This could be optimized by not bitblasting the bits

diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp
index 77ba5b7e7c9b371f1443d107240956d7731ac808..b2700eeeed78c323541c5bba6935a3a41f3a82bb 100644 (file)
--- a/bitvec/consteval.cpp
+++ b/bitvec/consteval.cpp
@@ -80,6 +80,22 @@ namespace BEEV {
       }
       break;
     }
+
+    case BVZX: {
+      output = CONSTANTBV::BitVector_Create(inputwidth,true);
+      unsigned t0_width = t[0].GetValueWidth();
+      if(inputwidth == t0_width) {
+        CONSTANTBV::BitVector_Copy(output, tmp0);
+        OutputNode = CreateBVConst(output, outputwidth);
+      }
+      else {
+        CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, t0_width);
+        OutputNode = CreateBVConst(output, outputwidth);
+      }
+      break;
+    }
+
+
     case BVAND: {
       output = CONSTANTBV::BitVector_Create(inputwidth,true);
       CONSTANTBV::Set_Intersection(output,tmp0,tmp1);

diff --git a/parser/smtlib.lex b/parser/smtlib.lex
index e39bc47f1323e3ef8a27c850fb6f41d4d95dd633..7070686e5cba2951723a7817e6cc8d6cfcd227fd 100644 (file)
--- a/parser/smtlib.lex
+++ b/parser/smtlib.lex
@@ -183,7 +183,7 @@ bit{DIGIT}+     {
 "bvsub"         { return BVSUB_TOK;}
 "bvnot"         { return BVNOT_TOK;}
 "bvmul"         { return BVMULT_TOK;}
-"bvdiv"         { return BVDIV_TOK;}
+"bvudiv"         { return BVDIV_TOK;}
 "bvsdiv"        { return SBVDIV_TOK;}
 "bvurem"        { return BVMOD_TOK;} 
 "bvsrem"        { return SBVREM_TOK;}
@@ -215,6 +215,7 @@ bit{DIGIT}+     {
 "bvsle"         { return BVSLE_TOK;}
 "bvsge"         { return BVSGE_TOK;}
 
+"zero_extend"   { return BVZX_TOK;}
 "sign_extend"   { return BVSX_TOK;} 
 "boolextract"   { return BOOLEXTRACT_TOK;}
 "boolbv"        { return BOOL_TO_BV_TOK;}

diff --git a/parser/smtlib.y b/parser/smtlib.y
index d462299f53f3a2c36607dbbf951e9706aa39acf6..52215ecf5f7360c14cc037444d01e803739e8596 100644 (file)
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -194,6 +194,7 @@
 %token BVSLE_TOK
 %token BVSGE_TOK
 %token BVSX_TOK 
+%token BVZX_TOK
 %token BOOLEXTRACT_TOK
 %token BOOL_TO_BV_TOK
 %token BVEXTRACT_TOK
@@ -1108,6 +1109,17 @@ an_nonbvconst_term:
       $$ = n;
       delete $5;
     }
+| BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
+    {
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5);
+      unsigned w = $5->GetValueWidth() + $3;
+      BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w);
+      BEEV::ASTNode *n =  new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVZX,w,*$5,width));
+      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+      $$ = n;
+      delete $5;
+    }
+
 ;
   
 sort_symb:

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index 72c8700d1045026a46fb89b68365ff57d3da155b..fc715f6b8b97236003f042968649269d00213c4d 100644 (file)
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -1403,6 +1403,14 @@ namespace BEEV {
       }
       break;
     }
+
+   case BVZX:
+      {
+       output = CreateTerm(BVZX,inputValueWidth,SimplifyTerm(inputterm[0]),inputterm[1]);
+      }
+       break;
+
+
     case BVSX:{
       //a0 is the expr which is being sign extended
       ASTNode a0 = SimplifyTerm(inputterm[0]);