From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 24 Sep 2010 00:32:30 +0000 (+0000)
Subject: Experimental. Push bvand and bvor through concats.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8a129a9a135a849f05aa96576673cc50eb435399;p=francis%2Fstp.git

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 52f9997..77d7b1b 100644
--- 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
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)
+