Improvement. Convert left/right (NOT aritmetic), shifts by a known amount to a concat...

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index b4d36da112e6970c2a257aac778882a2ddbdbb73..3b56b9e06b736836709eb529219ad3737cf6df8e 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -638,33 +638,22 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 
        case BEEV::BVLEFTSHIFT:
        {
-                 if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
-                                result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && CONSTANTBV::Set_Max(children[1].GetBVConst()) > 1 + log2(width))
-                         result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && children[1].GetUnsignedConst() >=width)
-                         result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
-                                result = children[0];
-
-
+          if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
+            result = bm.CreateZeroConst(width);
+          else if (children[1].isConstant())
+            result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing);
        }
        break;
 
        case BEEV::BVRIGHTSHIFT:
-               {
-                       if (children[0] == children[1])
-                               result= bm.CreateZeroConst(width);
-                       if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
-                                result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && CONSTANTBV::Set_Max(children[1].GetBVConst()) > 1 + log2(width))
-                                 result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && children[1].GetUnsignedConst() >=width)
-                                 result = bm.CreateZeroConst(width);
-                 else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
-                                result = children[0];
-
-               }
+        {
+          if (children[0] == children[1])
+            result= bm.CreateZeroConst(width);
+          if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
+            result = bm.CreateZeroConst(width);
+          else if (children[1].isConstant())
+            result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing);
+        }
        break;
 
        case BEEV::BVSRSHIFT:

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 66fbdeda9e92d223be10a7467fa3aac35c02943d..ecc4c2230d9e355b612bdff20b541c580ddefba5 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1709,6 +1709,71 @@ namespace BEEV
     return output;
   }
 
+  // If the rhs of a left or right shift is known. Then replace it with a concat / extract.
+  ASTNode Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf)
+  {
+    const ASTNode a =children[0];
+    const ASTNode b =children[1];
+    const int width = children[0].GetValueWidth();
+    ASTNode output;
+
+    assert(b.isConstant());
+    assert(k == BVLEFTSHIFT || BVRIGHTSHIFT ==k);
+
+  if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
+    {
+      // Intended to remove shifts by very large amounts
+      // that don't fit into the unsigned.  at thhe start
+      // of the "else" branch.
+      output = bm.CreateZeroConst(width);
+    }
+  else
+    {
+      const unsigned int shift = b.GetUnsignedConst();
+      if (shift >= width)
+        {
+          output = bm.CreateZeroConst(width);
+        }
+      else if (shift == 0)
+        {
+          output = a; // unchanged.
+        }
+      else
+        {
+          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);
+              output =
+                nf->CreateTerm(BVCONCAT, width,
+                                extract, zero);
+              BVTypeCheck(output);
+            }
+          else if (k == BVRIGHTSHIFT)
+            {
+              ASTNode zero = bm.CreateZeroConst(shift);
+              ASTNode hi = bm.CreateBVConst(32, width -1);
+              ASTNode low = bm.CreateBVConst(32, shift);
+              ASTNode extract =
+                nf->CreateTerm(BVEXTRACT, width - shift,
+                                a, hi, low);
+              BVTypeCheck(extract);
+              output =
+                nf->CreateTerm(BVCONCAT, width, zero, extract);
+              BVTypeCheck(output);
+            }
+          else
+            FatalError("herasdf");
+        }
+    }
+  return output;
+}
+
 
 
   //This function simplifies terms based on their kind
@@ -2742,57 +2807,7 @@ namespace BEEV
           const unsigned int width = a.GetValueWidth();
           if (BVCONST == b.GetKind()) // known shift amount.
             {
-              if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
-                {
-                  // Intended to remove shifts by very large amounts
-                  // that don't fit into the unsigned.  at thhe start
-                  // of the "else" branch.
-                  output = _bm->CreateZeroConst(width);
-                }
-              else
-                {
-                  const unsigned int shift = b.GetUnsignedConst();
-                  if (shift >= width)
-                    {
-                      output = _bm->CreateZeroConst(width);
-                    }
-                  else if (shift == 0)
-                    {
-                      output = a; // unchanged.
-                    }
-                  else
-                    {
-                      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);
-                          output = 
-                            nf->CreateTerm(BVCONCAT, width,
-                                            extract, zero);
-                          BVTypeCheck(output);
-                        }
-                      else if (k == BVRIGHTSHIFT)
-                        {
-                          ASTNode zero = _bm->CreateZeroConst(shift);
-                          ASTNode hi = _bm->CreateBVConst(32, width -1);
-                          ASTNode low = _bm->CreateBVConst(32, shift);
-                          ASTNode extract = 
-                            nf->CreateTerm(BVEXTRACT, width - shift,
-                                            a, hi, low);
-                          BVTypeCheck(extract);
-                          output = 
-                            nf->CreateTerm(BVCONCAT, width, zero, extract);
-                          BVTypeCheck(output);
-                        }
-                      else
-                        FatalError("herasdf");
-                    }
-                }
+              output = convertKnownShiftAmount(k, inputterm.GetChildren(), *_bm, nf);
             }
           else if (a == _bm->CreateZeroConst(width))
           {

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 3aa9eb4896abe39c0bc6e54901e568d401785ff4..9c0343f74bf5b368e7800c52b1a786ba9da077a2 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -62,6 +62,9 @@ namespace BEEV
 
   public:
 
+    static ASTNode convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf);
+
+
     /****************************************************************
      * Public Member Functions                                      *
      ****************************************************************/