From 54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Wed, 1 May 2013 13:22:29 -0400
Subject: [PATCH] added back BitwiseEq rule

---
 src/smt/smt_engine.cpp                                 |  7 +++++++
 src/theory/bv/theory_bv.cpp                            | 10 +++++-----
 .../bv/theory_bv_rewrite_rules_operator_elimination.h  |  1 -
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bc89e8d44..78f6e3dae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1822,11 +1822,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   hash_set<TNode, TNodeHashFunction> s;
+  Trace("debugging") << "NonClausal simplify pre-preprocess\n"; 
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Node assertion = d_assertionsToPreprocess[i];
     Node assertionNew = d_topLevelSubstitutions.apply(assertion);
+    Trace("debugging") << "assertion = " << assertion << endl;
+    Trace("debugging") << "assertionNew = " << assertionNew << endl; 
     if (assertion != assertionNew) {
       assertion = Rewriter::rewrite(assertionNew);
+      Trace("debugging") << "rewrite(assertion) = " << assertion << endl; 
     }
     Assert(Rewriter::rewrite(assertion) == assertion);
     for (;;) {
@@ -1835,8 +1839,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         break;
       }
       ++d_smt.d_stats->d_numConstantProps;
+      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
       assertion = Rewriter::rewrite(assertionNew);
+      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
     }
+    Trace("debugging") << "\n"; 
     s.insert(assertion);
     d_assertionsToCheck.push_back(assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b2f91e070..6f450d08e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -284,12 +284,12 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
-  // if (RewriteRule<BitwiseEq>::applies(t)) {
-  //   Node result = RewriteRule<BitwiseEq>::run<false>(t);
-  //   return Rewriter::rewrite(result);
-  // }
+  if (RewriteRule<BitwiseEq>::applies(t)) {
+	Node result = RewriteRule<BitwiseEq>::run<false>(t);
+    return Rewriter::rewrite(result);
+  }
 
-  if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) {
+  if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
     return utils::mkAnd(equalities); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index a63721de1..626116453 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -85,7 +85,6 @@ Node RewriteRule<SgeEliminate>::apply(TNode node) {
   return result;
 }
 
-
 template <>
 bool RewriteRule<SltEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLT); 
-- 
2.30.2