Remove BVZX. Bit vector zero extend is now replaced by a prepend with a zero bitvecto...

The simplification rules over concatentations are better than those that were over BVZX.

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

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index c6f9ad071e94d1e9b80f3e7a6a6cf0f5561a4a0e..ee5a4a2124253dfbedcb5463d112aa7a1a24f151 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -752,18 +752,6 @@ namespace BEEV
               FatalError("BVTypeCheck:BVSX must have two arguments. The second is the new width\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);
-              }
-            if ((v.size() != 2))
-              FatalError("BVTypeCheck:BVZX must have two arguments. The second is the new width\n", n);
-
-            break;
-
           default:
             for (ASTVec::const_iterator it = v.begin(), itend = v.end(); it != itend; it++)
               if (BITVECTOR_TYPE != it->GetType())

diff --git a/src/const-evaluator/consteval.cpp b/src/const-evaluator/consteval.cpp
index f0d026bc489c59f353be16aa8c8861de369786a2..8851bd61fc7ed3d412e287b86e653750320a8d35 100644 (file)
--- a/src/const-evaluator/consteval.cpp
+++ b/src/const-evaluator/consteval.cpp
@@ -94,23 +94,6 @@ 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 BVLEFTSHIFT:
                case BVRIGHTSHIFT:
                case BVSRSHIFT:
@@ -216,9 +199,10 @@ namespace BEEV
           OutputNode = CreateBVConst(output, outputwidth);
           break;
         }
-        //FIXME Only 2 inputs?
+
       case BVCONCAT:
         {
+          assert(2==t.Degree());
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
           unsigned t0_width = t[0].GetValueWidth();
           unsigned t1_width = t[1].GetValueWidth();

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index cd432f2c40f67c27247f697e7bced6b11918e397..0436df0df07eb4558b79c8cd09fbe591e744df4c 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -1152,14 +1152,19 @@ an_nonbvconst_term:
 | BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
     {
       GlobalBeevMgr->BVTypeCheck(*$5);
+      if (0 != $3)
+      {
       unsigned w = $5->GetValueWidth() + $3;
-      ASTNode width = GlobalBeevMgr->CreateBVConst(32,w);
-      ASTNode *n =  new ASTNode(GlobalBeevMgr->CreateTerm(BVZX,w,*$5,width));
+         ASTNode leading_zeroes = GlobalBeevMgr->CreateBVConst($3, 0);
+      ASTNode *n =  new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT,w,leading_zeroes,*$5));
       GlobalBeevMgr->BVTypeCheck(*n);
       $$ = n;
       delete $5;
     }
+      else
+       $$ = $5;
 
+    }
 ;
   
 sort_symb:

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7c4813985f5c294f458e47334b324b25d8fef79f..a3472ebaff80b5f62b298e41699f9f5327eb452e 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1940,16 +1940,6 @@ ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b)
           break;
         }
 
-      case BVZX:
-        {
-          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
-          if (a0.GetKind() == BVCONST)
-            output = BVConstEvaluator(CreateTerm(BVZX, inputValueWidth, a0, inputterm[1]));
-          else
-            output = CreateTerm(BVZX, inputValueWidth, a0, inputterm[1]);
-        }
-        break;
-
       case BVSX:
         {
           //a0 is the expr which is being sign extended

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index fd537c1a2afd0848ab24a9d7d845c8a251974fcc..e71867a6617d68b362483ddd627110f53841d40b 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -232,47 +232,6 @@ namespace BEEV
             }
         }
 
-      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.