From: lianah <lianahady@gmail.com>
Date: Wed, 1 May 2013 17:22:29 +0000 (-0400)
Subject: added back BitwiseEq rule
X-Git-Tag: cvc5-1.0.0~7292
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a;p=cvc5.git

added back BitwiseEq rule
---

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);