Rewrite rule changes. Left shift by a constant now rewrites to multiplication (rather...

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 476a961aa08463cf09c0c2a26dc4fe5329901a31..c288adc84fa17c9dcf43713d35a83425f723c5de 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -930,6 +930,9 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
             result = bm.CreateZeroConst(width);
           else if (children[1].isConstant())
             result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing);
+          else if(children[0].isConstant() && children[0] == bm.CreateOneConst(width) && width > 1)
+            result = NodeFactory::CreateTerm(BEEV::ITE,width, NodeFactory::CreateNode(BEEV::EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width));
+
         }
        break;
 
@@ -955,6 +958,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                           result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing);
                         else if (children[1].GetKind() == BEEV::BVUMINUS && children[0] == children[1][0])
                           result = NodeFactory::CreateTerm(BEEV::BVSRSHIFT,width, children[0], children[1][0]);
+                        else if(children[0].isConstant() && !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(), width-1))
+                          result = NodeFactory::CreateTerm(BEEV::BVRIGHTSHIFT,width, children[0], children[1]);
                }
         break;
 
@@ -1237,7 +1242,6 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
             result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
           break;
 
-
        case BEEV::BVDIV:
          if (children[1].isConstant() && children[1] == bm.CreateOneConst(width))
            result = children[0];
@@ -1245,6 +1249,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
              result =  bm.CreateOneConst(width);
           else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0] == children[1])
              result =  bm.CreateOneConst(width);
+          else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
+             result = NodeFactory::CreateTerm(BEEV::ITE,width, NodeFactory::CreateNode(BEEV::EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width));
 
          break;
 
@@ -1253,8 +1259,10 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
             result = children[0];
           else if (children[0] == children[1] && bm.UserFlags.division_by_zero_returns_one_flag)
             result =   bm.CreateOneConst(width);
+          else if (children[1].GetKind() == BEEV::BVUMINUS && children[0] == children[1][0] && bm.UserFlags.division_by_zero_returns_one_flag)
+              result = NodeFactory::CreateTerm(BEEV::SBVDIV,width, children[1], children[0]);
           else
-            result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
+           result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
           break;
 
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 3e507b7bed6454e0de799a0151ca70f839e448c1..8d518a9b173734fefeac1555c57a45ebf1bba27a 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1754,7 +1754,7 @@ namespace BEEV
   }
 
 
-  // If the rhs of a left or right shift is known. Then replace it with a concat / extract.
+  // If the rhs of a left or right shift is known.
   ASTNode Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf)
   {
     const ASTNode a =children[0];
@@ -1787,17 +1787,16 @@ namespace BEEV
         {
           if (k == BVLEFTSHIFT)
             {
-              ASTNode zero = bm.CreateZeroConst(shift);
-              ASTNode hi = bm.CreateBVConst(32, width - shift -1);
-              ASTNode low = bm.CreateZeroConst(32);
-              ASTNode extract =
-                nf->CreateTerm(BVEXTRACT, width - shift,
-                                a, hi, low);
-              BVTypeCheck(extract);
+              CBV cbv =  CONSTANTBV::BitVector_Create(width,true);
+              CONSTANTBV::BitVector_Bit_On(cbv,shift);
+              ASTNode c = bm.CreateBVConst(cbv,width);
+
               output =
-                nf->CreateTerm(BVCONCAT, width,
-                                extract, zero);
+                nf->CreateTerm(BVMULT, width,
+                                a, c);
               BVTypeCheck(output);
+              //cout << output;
+              //cout << a << b << endl;
             }
           else if (k == BVRIGHTSHIFT)
             {
@@ -1819,8 +1818,6 @@ namespace BEEV
   return output;
 }
 
-
-
   //This function simplifies terms based on their kind
   ASTNode 
   Simplifier::SimplifyTerm(const ASTNode& actualInputterm, 
@@ -2236,7 +2233,24 @@ namespace BEEV
                 output = nf->CreateTerm(BVSUB, inputValueWidth, a0[1], a0[0]);
                 break;
               }
-            case ITE:
+              case BVAND:
+            if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0])
+              {
+                output = nf->CreateTerm(BVOR, inputValueWidth, a0[0], a0[1]);
+              }
+            break;
+            case BVOR:
+            if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0])
+              {
+                output = nf->CreateTerm(BVAND, inputValueWidth, a0[0], a0[1]);
+              }
+            break;
+          case BVLEFTSHIFT:
+            if (a0[0].GetKind() == BVCONST)
+              output = nf->CreateTerm(BVLEFTSHIFT, inputValueWidth, nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]),
+                  a0[1]);
+            break;
+          case ITE:
               {
                 //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2))
                 ASTNode c = a0[0];