From 47dbf8d8b3e04810f79fd3069eb15ee1b2fb176d Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 May 2018 11:42:40 -0700
Subject: Normalize negated bit-vector terms over equalities. (#2017)

---
 src/theory/bv/theory_bv.cpp                        |  4 ++
 src/theory/bv/theory_bv_rewrite_rules.h            |  6 +-
 .../bv/theory_bv_rewrite_rules_normalization.h     | 78 ++++++++++++++++++++++
 3 files changed, 87 insertions(+), 1 deletion(-)

(limited to 'src/theory/bv')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 107cb9672..638715ae4 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -767,6 +767,10 @@ Node TheoryBV::ppRewrite(TNode t)
   } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) {
     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
   }
+  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
+  {
+    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
+  }
 
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 1d2e7d9a3..c6fa42ab0 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -31,7 +31,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-enum RewriteRuleId {
+enum RewriteRuleId
+{
 
   /// core normalization rules
   EmptyRule,
@@ -175,6 +176,7 @@ enum RewriteRuleId {
   OrSimplify,
   XorSimplify,
   BitwiseSlicing,
+  NormalizeEqPlusNeg,
   // rules to simplify bitblasting
   BBPlusNeg,
   UltPlusOne,
@@ -321,6 +323,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ConcatToMult: out << "ConcatToMult"; return out;
   case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
   case MultSltMult: out << "MultSltMult"; return out;
+  case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out;
   default:
     Unreachable();
   }
@@ -548,6 +551,7 @@ struct AllRewriteRules {
   RewriteRule<SignExtendUltConst> rule126;
   RewriteRule<ZeroExtendUltConst> rule127;
   RewriteRule<MultSltMult> rule128;
+  RewriteRule<NormalizeEqPlusNeg> rule129;
 };
 
 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 c2f6620aa..a02bf305f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1451,6 +1451,84 @@ inline Node RewriteRule<BitwiseSlicing>::apply(TNode node)
   return result;
 }
 
+template <>
+inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node)
+{
+  return node.getKind() == kind::EQUAL
+         && (node[0].getKind() == kind::BITVECTOR_PLUS
+             || node[1].getKind() == kind::BITVECTOR_PLUS);
+}
+
+template <>
+inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
+                      << std::endl;
+
+  NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS);
+  NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS);
+  NodeManager *nm = NodeManager::currentNM();
+
+  if (node[0].getKind() == kind::BITVECTOR_PLUS)
+  {
+    for (const TNode &n : node[0])
+    {
+      if (n.getKind() == kind::BITVECTOR_NEG)
+        nb_rhs << n[0];
+      else
+        nb_lhs << n;
+    }
+  }
+  else
+  {
+    nb_lhs << node[0];
+  }
+
+  if (node[1].getKind() == kind::BITVECTOR_PLUS)
+  {
+    for (const TNode &n : node[1])
+    {
+      if (n.getKind() == kind::BITVECTOR_NEG)
+        nb_lhs << n[0];
+      else
+        nb_rhs << n;
+    }
+  }
+  else
+  {
+    nb_rhs << node[1];
+  }
+
+  Node zero = utils::mkZero(utils::getSize(node[0]));
+
+  Node lhs, rhs;
+  if (nb_lhs.getNumChildren() == 0)
+  {
+    lhs = zero;
+  }
+  else if (nb_lhs.getNumChildren() == 1)
+  {
+    lhs = nb_lhs[0];
+  }
+  else
+  {
+    lhs = nb_lhs.constructNode();
+  }
+  if (nb_rhs.getNumChildren() == 0)
+  {
+    rhs = zero;
+  }
+  else if (nb_rhs.getNumChildren() == 1)
+  {
+    rhs = nb_rhs[0];
+  }
+  else
+  {
+    rhs = nb_rhs.constructNode();
+  }
+  return nm->mkNode(node.getKind(), lhs, rhs);
+}
+
 // template<> inline
 // bool RewriteRule<>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_CONCAT);
-- 
cgit v1.2.3