Experimental. Push bvand and bvor through concats.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 52f999749cfb5da6f864b4bdc42ed0a74c24879e..77d7b1b17d432b414d7f3683d466838fa3992ad3 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2451,6 +2451,15 @@ namespace BEEV
       case BVAND:
       case BVOR:
         {
+          // turn BVAND(CONCAT CONCAT) into concat(BVAND() BVAND()). i.e. push ops through concat.
+          if (inputterm.Degree() ==2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT && inputterm[0][0].GetValueWidth() ==inputterm[1][0].GetValueWidth() )
+          {
+                output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(),
+                    nf->CreateTerm(k,inputterm[0][0].GetValueWidth(), inputterm[0][0],inputterm[1][0]),
+                    nf->CreateTerm(k,inputterm[0][1].GetValueWidth(),inputterm[0][1],inputterm[1][1]));
+                break;
+          }
+
           ASTNode max = _bm->CreateMaxConst(inputValueWidth);
           ASTNode zero = _bm->CreateZeroConst(inputValueWidth);
 
@@ -2755,6 +2764,18 @@ namespace BEEV
                          output = _bm->CreateZeroConst(inputterm.GetValueWidth());
                          break;
                  }
+                 if (inputterm.Degree() ==2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT && inputterm[0][0].GetValueWidth() ==inputterm[1][0].GetValueWidth() )
+                 {
+                       output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(),
+                           nf->CreateTerm(k,inputterm[0][0].GetValueWidth(), inputterm[0][0],inputterm[1][0]),
+                           nf->CreateTerm(k,inputterm[0][1].GetValueWidth(),inputterm[0][1],inputterm[1][1]));
+                       break;
+                 }
+                 if (inputterm.Degree() ==2 && inputterm[0] == _bm->CreateZeroConst(inputterm.GetValueWidth()))
+                   {
+                     output = inputterm[1];
+                     break;
+                   }
          }
          //run on.
       case BVXNOR:

diff --git a/unit_test/eq.smt2 b/unit_test/eq.smt2
new file mode 100644 (file)
index 0000000..5ade2bd
--- /dev/null
+++ b/unit_test/eq.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+(declare-fun v3 () (_ BitVec 2))
+
+
+(assert  
+       (=      
+               (bvor (concat v0 (_ bv0 2))  (concat (_ bv0 2) v1) )
+               (bvxor (concat v2 (_ bv0 2))  (concat (_ bv0 2) v3) )
+       )
+)
+
+
+
+(check-sat)
+(exit)
+