From cd648c6f25a1d85abd9d677849de8af02de13d5b Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Sat, 14 Jun 2014 16:13:46 -0400
Subject: more bv rewrites

---
 src/theory/bv/theory_bv.cpp | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'src/theory/bv/theory_bv.cpp')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 441577c9e..04b8e9d6e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -562,6 +562,26 @@ Node TheoryBV::ppRewrite(TNode t)
     res = Rewriter::rewrite(result);
   }
 
+  if( res.getKind() == kind::EQUAL &&
+      ((res[0].getKind() == kind::BITVECTOR_PLUS &&
+        RewriteRule<ConcatToMult>::applies(res[1])) ||
+       res[1].getKind() == kind::BITVECTOR_PLUS &&
+       RewriteRule<ConcatToMult>::applies(res[0]))) {
+    Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
+      RewriteRule<ConcatToMult>::run<false>(res[0]) :
+      RewriteRule<ConcatToMult>::run<true>(res[1]);
+    Node factor = mult[0];
+    Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
+    Node new_eq =utils::mkNode(kind::EQUAL, sum, mult);
+    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
+    if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
+      res = Rewriter::rewrite(rewr_eq);
+    } else {
+      res = t;
+    }
+  }
+  
+
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == kind::BITVECTOR_PLUS))) {
-- 
cgit v1.2.3