Improvement. Pull bvsx through multiplication, signed division and plus.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 9a5411a0b166a39d9855e43c7c971419ea4dc6a7..bb9b620e1812e966f8d24845329b32b967635c37 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1676,6 +1676,42 @@ namespace BEEV
     return (it->second == n);
   }
 
+ // If both of the children are sign extended. Makes this node sign extended too.
+  ASTNode Simplifier::pullUpBVSX(ASTNode output)
+  {
+    assert(output.GetChildren().size() ==2);
+    assert(output[0].GetKind() == BVSX);
+    assert(output[1].GetKind() == BVSX);
+    const Kind k = output.GetKind();
+
+    assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
+    const int inputValueWidth = output.GetValueWidth();
+
+    int lengthA = output.GetChildren()[0][0].GetValueWidth();
+    int lengthB = output.GetChildren()[1][0].GetValueWidth();
+    int maxLength;
+    if (BVMULT == output.GetKind())
+      maxLength = lengthA + lengthB;
+    else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
+      maxLength = std::max(lengthA,lengthB)+1;
+    else
+      FatalError("Unexpected.");
+    if (maxLength < output.GetValueWidth())
+      {
+        ASTNode newA =  nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[0], _bm->CreateBVConst(32,maxLength-1), _bm->CreateZeroConst(32));
+        newA = SimplifyTerm(newA);
+        ASTNode newB =  nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[1], _bm->CreateBVConst(32,maxLength-1), _bm->CreateZeroConst(32));
+        newB = SimplifyTerm(newB);
+
+        ASTNode mult = nf->CreateTerm(output.GetKind(), maxLength, newA,newB);
+        output = nf->CreateTerm(BVSX, inputValueWidth, mult, _bm->CreateBVConst(32,inputValueWidth));
+        cerr << k;
+      }
+    return output;
+  }
+
+
+
   //This function simplifies terms based on their kind
   ASTNode 
   Simplifier::SimplifyTerm(const ASTNode& actualInputterm, 
@@ -1976,7 +2012,11 @@ namespace BEEV
                 }
             }
 
-          if (BVMULT == output.GetKind())
+          if ((BVMULT == output.GetKind() || BVPLUS == output.GetKind()) && output.GetChildren().size() == 2 && output.GetChildren()[0].GetKind() == BVSX && output.GetChildren()[1].GetKind() == BVSX )
+            {
+              output = pullUpBVSX(output);
+            }
+          else if (BVMULT == output.GetKind())
             {
               output = makeTower(BVMULT,output.GetChildren());
             }
@@ -2893,13 +2933,15 @@ namespace BEEV
         }
       case SBVDIV:
         {
+          output = inputterm;
           if (inputterm[0] == inputterm[1])
           {
             output = _bm->CreateOneConst(inputValueWidth);
             break;
           }
+          if (SBVDIV == output.GetKind() && output.GetChildren().size() == 2 && output.GetChildren()[0].GetKind() == BVSX && output.GetChildren()[1].GetKind() == BVSX )
+            output = pullUpBVSX(output);
 
-          output = inputterm;
           break;
         }
       case WRITE:

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index a53837d518f450ef8e2e5a1c9b9df37ea661f279..1f5611a602bb4e1b5b9ba973aa3918c3a6f0728e 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -58,6 +58,8 @@ namespace BEEV
 
     ASTNode makeTower(const Kind k , const ASTVec& children);
 
+    ASTNode pullUpBVSX(const ASTNode output);
+
   public:
 
     /****************************************************************