Changed bitvector theory rewriter so that equalities always get rewritten to

equalities or true or false

3 files changed, 13 insertions, 10 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 208ffba6c..811600ad4 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
 #include "theory/bv/bitblaster.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -189,6 +190,16 @@ 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);
+  }
+  return t;
+}
+
+
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
   Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index a2cf39049..247d66d89 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -65,6 +65,7 @@ public:
   std::string identify() const { return std::string("TheoryBV"); }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  Node ppRewrite(TNode atom);
 
 private:
 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 25cbae68c..c2a5780a3 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -516,8 +516,7 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
-        RewriteRule<ReflexivityEq>,
-        RewriteRule<BitwiseEq>
+        RewriteRule<ReflexivityEq>
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }
@@ -534,14 +533,6 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
         return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
       }
     }
-
-    if(RewriteRule<BitwiseEq>::applies(resultNode)) {
-      resultNode = RewriteRule<BitwiseEq>::run<false>(resultNode);
-      if (resultNode != node) {
-        return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
-      }
-    }
-
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }
 }