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

---
 src/theory/bv/theory_bv.cpp                   | 20 ++++++++++++
 src/theory/bv/theory_bv_rewrite_rules.h       |  5 ++-
 .../theory_bv_rewrite_rules_normalization.h   | 32 +++++++++++++++++++
 .../theory_bv_rewrite_rules_simplification.h  |  4 +++
 4 files changed, 60 insertions(+), 1 deletion(-)

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))) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 496e05c86..eadb63671 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -164,7 +164,8 @@ enum RewriteRuleId {
   BitwiseSlicing,
   // rules to simplify bitblasting
   BBPlusNeg,
-  UltPlusOne
+  UltPlusOne,
+  ConcatToMult
 };
 
 
@@ -291,6 +292,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ExtractSignExtend : out << "ExtractSignExtend"; return out;
   case MultDistrib: out << "MultDistrib"; return out;
   case UltPlusOne: out << "UltPlusOne"; return out;
+  case ConcatToMult: out << "ConcatToMult"; return out;
   default:
     Unreachable();
   }
@@ -513,6 +515,7 @@ struct AllRewriteRules {
   RewriteRule<IntToBVEliminate>  rule117;
   RewriteRule<MultDistrib> rule118;
   RewriteRule<UltPlusOne> rule119;
+  RewriteRule<ConcatToMult> rule120;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 0807b3d66..5cff67005 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -506,6 +506,38 @@ Node RewriteRule<MultDistrib>::apply(TNode node) {
   return utils::mkNode(sum.getKind(), children); 
 }
 
+template<> inline
+bool RewriteRule<ConcatToMult>::applies(TNode node) {
+  if (node.getKind() != kind::BITVECTOR_CONCAT) return false;
+  if (node.getNumChildren() != 2) return false;
+  if (node[0].getKind()!= kind::BITVECTOR_EXTRACT) return false;
+  if (!node[1].isConst()) return false;
+  TNode extract = node[0];
+  TNode c = node[1];
+  unsigned ammount = utils::getSize(c);
+  
+  if (utils::getSize(node) != utils::getSize(extract[0])) return false; 
+  if (c != utils::mkConst(ammount, 0)) return false;
+
+  unsigned low = utils::getExtractLow(extract);
+  if (low != 0) return false; 
+  unsigned high = utils::getExtractHigh(extract);
+  if (high + ammount + 1 != utils::getSize(node)) return false;
+  return true;
+}
+
+template<> inline
+Node RewriteRule<ConcatToMult>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << node << ")" << std::endl;
+  unsigned size = utils::getSize(node); 
+  Node factor = node[0][0];
+  Assert(utils::getSize(factor) == utils::getSize(node)); 
+  BitVector ammount = BitVector(size, utils::getSize(node[1]));
+  Node coef = utils::mkConst(BitVector(size, 1u).leftShift(ammount));
+  return utils::mkNode(kind::BITVECTOR_MULT, factor, coef); 
+}
+
+
 
 template<> inline
 bool RewriteRule<SolveEq>::applies(TNode node) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index a8a7d1127..71df1edca 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1169,6 +1169,10 @@ bool RewriteRule<UltPlusOne>::applies(TNode node) {
       y1[1].getKind() != kind::CONST_BITVECTOR)
     return false;
   
+  if (y1[0].getKind() == kind::CONST_BITVECTOR &&
+      y1[1].getKind() == kind::CONST_BITVECTOR)
+    return false;
+  
   if (y1.getNumChildren() != 2)
     return false; 
 
-- 
2.30.2