diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 18:32:42 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 18:32:42 +0000 |
commit | 706e3058a2a685a6849b2290f80167b74aded0be (patch) | |
tree | 407c4b40a8f74adfee045f1a6cf6c578fbd960cd | |
parent | 0659b7c7b50e49cbea1728f90f7ff04598f01eac (diff) |
Changed bitvector theory rewriter so that equalities always get rewritten to
equalities or true or false
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 11 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 11 |
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); } } |