Add extra simplifying rules.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 0fad7593b1109d06491994ff5da03aec10fe5b81..d7dd80396fadd3b98ccb6f592076591f5b33a93b 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -469,6 +469,25 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
         }
 
 
+        if (k1 == BEEV::BVCONST && k2 == BEEV::BVSX)
+          {
+              // Each of the bits in the extended part, and one into the un-extended part must be the same.
+              bool foundZero=false, foundOne=false;
+              const unsigned original_width = in2[0].GetValueWidth();
+              const unsigned new_width = in2.GetValueWidth();
+              for (int i = original_width-1; i < new_width;i++)
+                      if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i))
+                              foundOne=true;
+                      else
+                              foundZero=true;
+              if (foundZero && foundOne)
+                      return ASTFalse;
+              ASTNode lhs = NodeFactory::CreateTerm(BEEV::BVEXTRACT, original_width, in1, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32));
+              ASTNode rhs = NodeFactory::CreateTerm(BEEV::BVEXTRACT, original_width, in2, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32));
+              return NodeFactory::CreateNode(BEEV::EQ, lhs,rhs);
+          }
+
+
        //last resort is to CreateNode
        return hashing.CreateNode(BEEV::EQ, children);
 }
@@ -791,8 +810,7 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                {
                        if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
                                result = bm.CreateZeroConst(width);
-
-                       if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
+                       else if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
                                result = bm.CreateMaxConst(width);
                        else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
                                         result = children[0];
@@ -800,6 +818,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                              result = children[0];
                         else if (width == 1 && children[1].isConstant() && children[1] == bm.CreateOneConst(1))
                               result = children[0];
+                        else if (children[1].isConstant())
+                          result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing);
 
 
                }
@@ -831,6 +851,10 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                           if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
                                     result = children[1];
 
+                          if (children[1].GetKind() == BEEV::BVNEG && children[0] == children[1][0])
+                              result = bm.CreateMaxConst(width);
+                          if (children[0].GetKind() == BEEV::BVNEG && children[1] == children[0][0])
+                              result = bm.CreateMaxConst(width);
                          }
                  }
                  break;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index f0786cf4e4b1319fa152b8aae0f9f469db3c859f..b29a770c7db72030e7e3ede2187570771ca41b71 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1056,23 +1056,6 @@ namespace BEEV
         }
     }
 
-    if (k1 == BVCONST && k2 == BVSX)
-    {
-       // Each of the bits in the extended part, and one into the un-extended part must be the same.
-       bool foundZero=false, foundOne=false;
-       const unsigned original_width = in2[0].GetValueWidth();
-       const unsigned new_width = in2.GetValueWidth();
-       for (int i = original_width-1; i < new_width;i++)
-               if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i))
-                       foundOne=true;
-               else
-                       foundZero=true;
-       if (foundZero && foundOne)
-               return ASTFalse;
-       ASTNode lhs = nf->CreateTerm(BVEXTRACT, original_width, in1, _bm->CreateBVConst(32,original_width-1), _bm->CreateZeroConst(32));
-       ASTNode rhs = nf->CreateTerm(BVEXTRACT, original_width, in2, _bm->CreateBVConst(32,original_width-1), _bm->CreateZeroConst(32));
-       return nf->CreateNode(EQ, lhs,rhs);
-    }
 
     //last resort is to CreateNode
     return nf->CreateNode(EQ, in1, in2);
@@ -1746,6 +1729,28 @@ namespace BEEV
     return output;
   }
 
+  // If the shift is bigger than the bitwidth, replace by an extract.
+  ASTNode Simplifier::convertArithmeticKnownShiftAmount(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 == BVSRSHIFT);
+    const unsigned int shift = b.GetUnsignedConst();
+
+    if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width) || (shift >= width))
+      {
+        ASTNode top = bm.CreateBVConst(32,width-1);
+        return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width));
+      }
+
+    return ASTNode();
+  }
+
+
   // 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)
   {

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 8a337ac3982c09eab6eed408cddd043d765d55db..9002cff4c4b75e9bb1d4be397ed5a60ab9a78100 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -61,7 +61,7 @@ namespace BEEV
     ASTNode pullUpBVSX(const ASTNode output);
 
   public:
-
+    static ASTNode convertArithmeticKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf);
     static ASTNode convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf);