Changed bitvector theory rewriter so that equalities always get rewritten to

equalities or true or false

1 files changed, 11 insertions, 0 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;