diff options
author | lianah <lianahady@gmail.com> | 2014-06-14 13:48:55 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-14 13:50:56 -0400 |
commit | 1f705d9a92b6a8a01b8a567ff9d5b44177ecb2f0 (patch) | |
tree | a77421b607ea4fdfbecc3a29d2ea53279ab6cc64 /src/theory/bv/theory_bv.cpp | |
parent | 348e37e437aa4a153b7f0444731322519fef962f (diff) |
added bv inequality rewrite
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f6092031c..441577c9e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -548,6 +548,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { + Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; if (RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); @@ -556,6 +557,9 @@ Node TheoryBV::ppRewrite(TNode t) std::vector<Node> equalities; Slicer::splitEqualities(t, equalities); res = utils::mkAnd(equalities); + } else if (RewriteRule<UltPlusOne>::applies(t)) { + Node result = RewriteRule<UltPlusOne>::run<false>(t); + res = Rewriter::rewrite(result); } // if(t.getKind() == kind::EQUAL && @@ -593,6 +597,7 @@ Node TheoryBV::ppRewrite(TNode t) if (options::bvAbstraction() && t.getType().isBoolean()) { d_abstractionModule->addInputAtom(res); } + Debug("bv-pp-rewrite") << "to " << res << "\n"; return res; } |