Improvement. Simplifying EQ a little better.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 87b6b450c0f5df06fea36d32338e2f0126d42c43..7cb493ef2937ce8fad375f2f368c5fc91a403ab2 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -956,6 +956,17 @@ namespace BEEV
                        return ASTFalse;
        }
 
+    // The above loop has determined that the leading bits are the same.
+    if (constStart > 0)
+      {
+        int newWidth = in1.GetValueWidth() - constStart;
+        ASTNode zero = _bm->CreateZeroConst(32);
+
+        ASTNode lhs =  nf->CreateTerm(BVEXTRACT,newWidth, in1,_bm->CreateBVConst(32,newWidth-1) ,zero);
+        ASTNode rhs =  nf->CreateTerm(BVEXTRACT,newWidth, in2,_bm->CreateBVConst(32,newWidth-1) ,zero);
+        return nf->CreateNode(EQ, lhs,rhs);
+      }
+
     // If both the children are concats split them apart.
     // nb. This doesn't cover the case when the children are organised differently:
     // (concat (concat A B) C) == (concat A (concat B C))
@@ -964,6 +975,20 @@ namespace BEEV
       return nf->CreateNode(AND, nf->CreateNode(EQ, in1[0], in2[0]), nf->CreateNode(EQ, in1[1], in2[1]));
     }
 
+    // If the rhs is a concat, and the lhs is a constant. Split.
+    if (k1== BVCONST && k2 == BVCONCAT)
+    {
+        int width = in1.GetValueWidth();
+        int bottomW = in2[1].GetValueWidth();
+        ASTNode zero = _bm->CreateZeroConst(32);
+
+        // split the constant.
+        ASTNode top =  nf->CreateTerm(BVEXTRACT,bottomW, in1,_bm->CreateBVConst(32,width-1) ,_bm->CreateBVConst(32,bottomW));
+        ASTNode bottom =  nf->CreateTerm(BVEXTRACT,width-bottomW, in1,_bm->CreateBVConst(32,bottomW-1) ,zero);
+
+        return nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1]));
+    }
+
 
     //last resort is to CreateNode
     return nf->CreateNode(EQ, in1, in2);