Adds a simplification rule to replace BVANDS with zeroes at the front with a CONCAT.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 838c0f7550969dfddf65b56f9d149ac95134304e..100fef064e8f3f0a2753718441f9ed6333e15af6 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -469,6 +469,7 @@ namespace BEEV
     return output;
   } //end of SimplifyAtomicFormula()
 
+
   // number of constant bits in the most significant places.
   int mostSignificantConstants(const ASTNode& n)
   {
@@ -524,6 +525,18 @@ namespace BEEV
        return false;
     }
 
+    int numberOfLeadingZeroes(const ASTNode& n)
+    {
+         int c = mostSignificantConstants( n);
+         if (c<=0)
+                 return 0;
+
+         for (int i =0; i < c;i++)
+                 if (getConstantBit(n,i)!=0)
+                         return i;
+         return c;
+    }
+
 
     bool unsignedGreaterThan(const ASTNode& n1, const ASTNode& n2)
     {
@@ -2392,6 +2405,32 @@ namespace BEEV
                                                        zero);
                                        assert(BVTypeCheck(output));
                                }
+
+
+                               // If the leading bits are zero. Replace it by a concat with zero.
+                               int i;
+                               if (output.GetKind() == BVAND && output.Degree() ==2 && ((i=numberOfLeadingZeroes(output[0])) > 0) )
+                               {
+                                       // i contains the number of leading zeroes.
+                                               output = nf->CreateTerm(BVCONCAT,
+                                                               output.GetValueWidth(),
+                                                               _bm->CreateZeroConst(i),
+                                                               nf->CreateTerm(BVAND, output.GetValueWidth() - i,
+                                                               nf->CreateTerm(BVEXTRACT,
+                                                                               output.GetValueWidth() - i,
+                                                                               output[0],
+                                                                               _bm->CreateBVConst(32,output.GetValueWidth() - i-1),
+                                                                               _bm->CreateBVConst(32,0)
+                                                                               ),
+                                                               nf->CreateTerm(BVEXTRACT,
+                                                                               output.GetValueWidth() - i,
+                                                                               output[1],
+                                                                               _bm->CreateBVConst(32,output.GetValueWidth() - i-1),
+                                                                               _bm->CreateBVConst(32,0)
+                                                                               ))
+                                                               );
+                                               assert(BVTypeCheck(output));
+                               }
                        }
           break;
         }