diff options
author | lianah <lianahady@gmail.com> | 2013-05-01 13:22:29 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-01 13:22:29 -0400 |
commit | 54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a (patch) | |
tree | c523bcd8f43de72ac937057657a096265dc7ed9b /src/theory | |
parent | db93834744ae5e1c93404e6236e1b46348037770 (diff) |
added back BitwiseEq rule
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 1 |
2 files changed, 5 insertions, 6 deletions
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); |