diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-29 20:02:38 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-29 20:02:38 -0800 |
commit | dc2f9914f49076d56cdb18e14971df67fbe567bb (patch) | |
tree | a82f640d60e27525a3094efaaae110b542ffccc9 /src/theory/quantifiers/bv_inverter.cpp | |
parent | 2d147b72e1339f4c281caf7786dfa9b4d79ed21c (diff) |
Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)
We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 174 |
1 files changed, 139 insertions, 35 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 9fe645a9a..cce56ab01 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -111,7 +111,7 @@ static bool isInvertible(Kind k, unsigned index) || k == BITVECTOR_PLUS || k == BITVECTOR_SUB || k == BITVECTOR_MULT - || (k == BITVECTOR_UREM_TOTAL && index == 1) + || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND || k == BITVECTOR_OR @@ -363,11 +363,10 @@ static Node getScBvUrem(bool pol, Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert(litk != EQUAL || pol == false || idx == 1); - + Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT); NodeManager* nm = NodeManager::currentNM(); - Node scl, scr; + Node scl; unsigned w = bv::utils::getSize(s); Assert (w == bv::utils::getSize(t)); Node z = bv::utils::mkZero(w); @@ -376,37 +375,46 @@ static Node getScBvUrem(bool pol, { if (idx == 0) { - Assert (pol == false); - /* x % s != t - * with side condition: - * s != 1 || t != 0 */ - scl = nm->mkNode(OR, - s.eqNode(bv::utils::mkOne(w)).notNode(), - t.eqNode(z).notNode()); - scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + if (pol) + { + /* x % s = t + * with side condition (synthesized): + * (not (bvult (bvnot (bvneg s)) t)) + * <-> + * ~(-s) >= t*/ + Node neg = nm->mkNode(BITVECTOR_NEG, s); + scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); + } + else + { + /* x % s != t + * with side condition: + * s != 1 || t != 0 */ + scl = nm->mkNode(OR, + s.eqNode(bv::utils::mkOne(w)).notNode(), + t.eqNode(z).notNode()); + } } else { if (pol) { /* s % x = t - * with side condition: + * with side condition (synthesized): + * (bvuge (bvand (bvsub (bvadd t t) s) s) t) + * <-> + * (t + t - s) & s >= t + * + * is equivalent to: * s = t * || * ( s > t * && s-t > t * && (t = 0 || t != s-1) ) */ - - Node a1 = nm->mkNode(BITVECTOR_UGT, s, t); - Node a2 = nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t); - Node a3 = nm->mkNode(OR, - t.eqNode(z), - t.eqNode(bv::utils::mkDec(s)).notNode()); - - scl = nm->mkNode(OR, - t.eqNode(s), - nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3))); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node sub = nm->mkNode(BITVECTOR_SUB, add, s); + Node a = nm->mkNode(BITVECTOR_AND, sub, s); + scl = nm->mkNode(BITVECTOR_UGE, a, t); } else { @@ -414,16 +422,119 @@ static Node getScBvUrem(bool pol, * with side condition: * s != 0 || t != 0 */ scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t); } } } - else + else if (litk == BITVECTOR_ULT) { - return Node::null(); + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with side condition: + * (distinct t z) + * where z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* x % s >= t + * with side condition (synthesized): + * (bvuge (bvnot (bvneg s)) t) */ + Node neg = nm->mkNode(BITVECTOR_NEG, s); + scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); + } + } + else + { + if (pol) + { + /* s % x < t + * with side condition: + * (distinct t z) + * where z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* s % x < t + * with side condition (combination of = and >): + * (or + * (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized + * (bvult t s)) ; ugt, synthesized */ + Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node sub = nm->mkNode(BITVECTOR_SUB, add, s); + Node a = nm->mkNode(BITVECTOR_AND, sub, s); + Node sceq = nm->mkNode(BITVECTOR_UGE, a, t); + Node scugt = nm->mkNode(BITVECTOR_ULT, t, s); + scl = nm->mkNode(OR, sceq, scugt); + } + } + } + else /* litk == BITVECTOR_SLT */ + { + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with side condition (synthesized): + * (bvslt (bvnot t) (bvor (bvneg s) (bvneg t))) */ + Node o1 = nm->mkNode(BITVECTOR_NEG, s); + Node o2 = nm->mkNode(BITVECTOR_NEG, t); + Node o = nm->mkNode(BITVECTOR_OR, o1, o2); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, t), o); + } + else + { + /* x % s >= t + * with side condition (synthesized): + * (or (bvslt t s) (bvsge z s)) + * where z = 0 with getSize(z) = w */ + Node s1 = nm->mkNode(BITVECTOR_SLT, t, s); + Node s2 = nm->mkNode(BITVECTOR_SGE, z, s); + scl = nm->mkNode(OR, s1, s2); + } + } + else + { + if (pol) + { + /* s % x < t + * with side condition (synthesized): + * (or (bvslt s t) (bvslt z t)) + * where z = 0 with getSize(z) = w */ + Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t); + Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t); + scl = nm->mkNode(OR, slt1, slt2); + } + else + { + /* s % x < t + * with side condition: + * (and + * (=> (= s z) (bvsle t z)) + * (=> (bvsgt s z) (bvsge s t)) + * (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t))) + * where z = 0 with getSize(z) = w */ + Node i1 = nm->mkNode(IMPLIES, + s.eqNode(z), nm->mkNode(BITVECTOR_SLE, t, z)); + Node i2 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, s, t)); + Node i3 = nm->mkNode(IMPLIES, + nm->mkNode(AND, + nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, t, z)), + nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t)); + scl = nm->mkNode(AND, i1, i2, i3); + return Node::null(); + } + } } - Node sc = nm->mkNode(IMPLIES, scl, scr); + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } @@ -1141,13 +1252,6 @@ Node BvInverter::solveBvLit(Node sv, break; case BITVECTOR_UREM_TOTAL: - if (index == 0) - { - /* x % s = t is rewritten to x - x / y * y */ - Trace("bv-invert") << "bv-invert : Unsupported for index " - << index << ", from " << sv_t << std::endl; - return Node::null(); - } sc = getScBvUrem( pol, litk, k, index, getSolveVariable(solve_tn), s, t); break; |