diff options
| author | lianah <lianahady@gmail.com> | 2013-04-30 13:42:50 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-30 13:42:50 -0400 |
| commit | 7a088fea6ba227437106091558ce656bbe8f29b8 (patch) | |
| tree | 9cb566c0bdd35b3ab3f10503afbdffaef8b6ef23 /src/theory/bv/theory_bv.cpp | |
| parent | c2cf8201afa6b44a5d3103cf8938eccb69cec590 (diff) | |
added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bd7d4c70b..91226f032 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -129,16 +129,22 @@ void TheoryBV::checkForLemma(TNode fact) { TNode urem = fact[0]; TNode result = fact[1]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { TNode urem = fact[1]; TNode result = fact[0]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } } |