diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-20 18:27:39 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-20 18:27:39 -0800 |
commit | f9149d3b3e785950a846fb195bf9fa9cb1a2d94a (patch) | |
tree | c69c90377a6c24abbc9c608a767507740abfd3b6 /src/theory/quantifiers/bv_inverter.cpp | |
parent | 13cc0e94ac8892fa1cefa53ff1c884d154894b58 (diff) |
Add explicit disequality handling when generating side condition for CBQI BV. (#1447)
This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 1072 |
1 files changed, 634 insertions, 438 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 0ac22a3e4..11d6ba85d 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -50,6 +50,8 @@ Node BvInverter::getSolveVariable(TypeNode tn) Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) { + TNode solve_var = getSolveVariable(tn); + // condition should be rewritten Node new_cond = Rewriter::rewrite(cond); if (new_cond != cond) @@ -58,11 +60,10 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) << " was rewritten to " << new_cond << std::endl; } + // optimization : if condition is ( x = solve_var ) should just return + // solve_var and not introduce a Skolem this can happen when we ask for + // the multiplicative inversion with bv1 Node c; - // optimization : if condition is ( x = v ) should just return v and not - // introduce a Skolem this can happen when we ask for the multiplicative - // inversion with bv1 - TNode solve_var = getSolveVariable(tn); if (new_cond.getKind() == EQUAL) { for (unsigned i = 0; i < 2; i++) @@ -225,6 +226,8 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t) } else { + /* x >= t + * no side condition */ sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } @@ -241,6 +244,8 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t) } else { + /* t >= x + * no side condition */ sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); } } @@ -270,6 +275,8 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t) } else { + /* x >= t + * no side condition */ sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } @@ -288,6 +295,8 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t) } else { + /* t >= x + * no side condition */ sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); } } @@ -295,392 +304,617 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t) return sc; } -static Node getScBvEq(bool pol, Kind k, unsigned idx, Node x, Node t) -{ - Assert(k == EQUAL); - Assert(pol == false); - - NodeManager* nm = NodeManager::currentNM(); - unsigned w = bv::utils::getSize(t); - - /* x != t - * <-> - * x < t || x > t (ULT) - * with side condition: - * t != 0 || t != ~0 */ - Node scl = nm->mkNode(OR, - nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)), - nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w))); - Node scr = nm->mkNode(DISTINCT, x, t); - Node sc = nm->mkNode(IMPLIES, scl, scr); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvMult(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvMult(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_MULT); + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); + Node scl, scr; + Node z = bv::utils::mkZero(bv::utils::getSize(s)); + + if (pol) + { + /* x * s = t + * with side condition: + * ctz(t) >= ctz(s) <-> x * s = t + * where + * ctz(t) >= ctz(s) -> t = 0 \/ ((t & -t) >= (s & -s) /\ s != 0) */ + Node t_uge_s = nm->mkNode(BITVECTOR_UGE, + nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), + nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); + scl = nm->mkNode(OR, + t.eqNode(z), + nm->mkNode(AND, t_uge_s, s.eqNode(z).notNode())); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + /* x * s != t + * with side condition: + * t != 0 || s != 0 */ + scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()); + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } - /* x * s = t - * with side condition: - * ctz(t) >= ctz(s) <-> x * s = t - * where - * ctz(t) >= ctz(s) -> t = 0 \/ ((t & -t) >= (s & -s) /\ s != 0) */ - Node zero = bv::utils::mkZero(bv::utils::getSize(s)); - Node t_uge_s = nm->mkNode(BITVECTOR_UGE, - nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), - nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); - Node scl = nm->mkNode(OR, - t.eqNode(zero), - nm->mkNode(AND, t_uge_s, s.eqNode(zero).notNode())); - Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvUrem(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvUrem(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert(idx == 1); + Assert(pol == false || idx == 1); + + if (litk != EQUAL) + { + return Node::null(); + } NodeManager* nm = NodeManager::currentNM(); + Node scl, scr; + unsigned w = bv::utils::getSize(s); + Assert (w == bv::utils::getSize(t)); + Node z = bv::utils::mkZero(w); - /* s % x = t - * with side condition: - * s = t - * || - * ( s > t - * && s-t > t - * && (t = 0 || t != s-1) ) */ - - Node a1 = // s > t - nm->mkNode(BITVECTOR_UGT, s, t); - Node a2 = // s-t > t - nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t); - Node a3 = // (t = 0 || t != s-1) - nm->mkNode(OR, - t.eqNode(bv::utils::mkZero(bv::utils::getSize(t))), - t.eqNode(bv::utils::mkDec(s)).notNode()); - - Node scl = nm->mkNode(OR, - t.eqNode(s), - nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3))); - Node scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, scr); + 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); + } + else + { + if (pol) + { + /* s % x = t + * with side condition: + * 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); + } + else + { + /* s % x != t + * 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); + } + } + Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvUdiv(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvUdiv(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_UDIV_TOTAL); + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); unsigned w = bv::utils::getSize(s); Assert (w == bv::utils::getSize(t)); - Node scl, scr; - Node zero = bv::utils::mkZero(w); + Node sc, scl, scr; + Node z = bv::utils::mkZero(w); + Node n = bv::utils::mkOnes(w); if (idx == 0) { - /* x udiv s = t - * with side condition: - * t = ~0 && (s = 0 || s = 1) - * || - * (t != ~0 && s != 0 && !umulo(s * t)) */ - Node o1 = nm->mkNode(AND, - t.eqNode(bv::utils::mkOnes(w)), - nm->mkNode(OR, - s.eqNode(bv::utils::mkZero(w)), - s.eqNode(bv::utils::mkOne(w)))); - Node o2 = nm->mkNode(AND, - t.eqNode(bv::utils::mkOnes(w)).notNode(), - s.eqNode(bv::utils::mkZero(w)).notNode(), - nm->mkNode(NOT, bv::utils::mkUmulo(s, t))); - - scl = nm->mkNode(OR, o1, o2); - scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + if (pol) + { + /* x udiv s = t + * with side condition: + * t = ~0 && (s = 0 || s = 1) + * || + * (t != ~0 && s != 0 && !umulo(s * t)) */ + Node one = bv::utils::mkOne(w); + Node o1 = nm->mkNode(AND, + t.eqNode(n), + nm->mkNode(OR, s.eqNode(z), s.eqNode(one))); + Node o2 = nm->mkNode(AND, + t.eqNode(n).notNode(), + s.eqNode(z).notNode(), + nm->mkNode(NOT, bv::utils::mkUmulo(s, t))); + + scl = nm->mkNode(OR, o1, o2); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + /* x udiv s != t + * with side condition: + * s != 0 || t != ~0 */ + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(n).notNode()); + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } + sc = nm->mkNode(IMPLIES, scl, scr); } else { - /* s udiv x = t - * with side condition: - * s = t - * || - * t = ~0 - * || - * (s >= t - * && (s % t = 0 || (s / (t+1) +1) <= s / t) - * && (s = ~0 => t != 0)) */ - - Node oo1 = nm->mkNode(EQUAL, - nm->mkNode(BITVECTOR_UREM_TOTAL, s, t), - bv::utils::mkZero(w)); - - Node ule1 = nm->mkNode(BITVECTOR_PLUS, - bv::utils::mkOne(w), - nm->mkNode(BITVECTOR_UDIV_TOTAL, - s, nm->mkNode(BITVECTOR_PLUS, t, bv::utils::mkOne(w)))); - Node ule2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t); - Node oo2 = nm->mkNode(BITVECTOR_ULE, ule1, ule2); - - Node a1 = nm->mkNode(BITVECTOR_UGE, s, t); - Node a2 = nm->mkNode(OR, oo1, oo2); - Node a3 = nm->mkNode(IMPLIES, - s.eqNode(bv::utils::mkOnes(w)), - t.eqNode(bv::utils::mkZero(w)).notNode()); - - Node o1 = s.eqNode(t); - Node o2 = t.eqNode(bv::utils::mkOnes(w)); - Node o3 = nm->mkNode(AND, a1, a2, a3); - - scl = nm->mkNode(OR, o1, o2, o3); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + if (pol) + { + /* s udiv x = t + * with side condition: + * s = t + * || + * t = ~0 + * || + * (s >= t + * && (s % t = 0 || (s / (t+1) +1) <= s / t) + * && (s = ~0 => t != 0)) */ + Node oo1 = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UREM_TOTAL, s, t), z); + Node udiv = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, bv::utils::mkInc(t)); + Node ule1 = bv::utils::mkInc(udiv); + Node ule2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t); + Node oo2 = nm->mkNode(BITVECTOR_ULE, ule1, ule2); + + Node a1 = nm->mkNode(BITVECTOR_UGE, s, t); + Node a2 = nm->mkNode(OR, oo1, oo2); + Node a3 = nm->mkNode(IMPLIES, s.eqNode(n), t.eqNode(z).notNode()); + + Node o1 = s.eqNode(t); + Node o2 = t.eqNode(n); + Node o3 = nm->mkNode(AND, a1, a2, a3); + + scl = nm->mkNode(OR, o1, o2, o3); + scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + sc = nm->mkNode(IMPLIES, scl, scr); + } + else + { + sc = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t); + } } - Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvAndOr(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvAndOr(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { + Assert (k == BITVECTOR_AND || k == BITVECTOR_OR); + + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); - /* with side condition: - * t & s = t - * t | s = t */ - Node scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); - Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + Node scl, scr; + + if (pol) + { + /* x & s = t + * x | s = t + * with side condition: + * t & s = t + * t | s = t */ + scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + unsigned w = bv::utils::getSize(s); + Assert (w == bv::utils::getSize(t)); + + if (k == BITVECTOR_AND) + { + /* x & s = t + * with side condition: + * s != 0 || t != 0 */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); + } + else + { + /* x | s = t + * with side condition: + * s != ~0 || t != ~0 */ + Node n = bv::utils::mkOnes(w); + scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode()); + } + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } + Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvLshr(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvLshr(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_LSHR); + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); Node scl, scr; unsigned w = bv::utils::getSize(s); Assert(w == bv::utils::getSize(t)); Node z = bv::utils::mkZero(w); - + if (idx == 0) { - /* x >> s = t - * with side condition: - * s = 0 || (s < w && clz(t) >=s) || (s >= w && t = 0) - * -> - * s = 0 || (s < w && ((z o t) << (z o s))[2w-1 : w] = z) || (s >= w && t = 0) - * with w = getSize(t) = getSize(s) - * and z = 0 with getSize(z) = w */ - Node ww = bv::utils::mkConst(w, w); - Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); - Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s); - Node shl = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); - Node ext = bv::utils::mkExtract(shl, 2*w-1, w); - - Node o1 = s.eqNode(z); - Node o2 = nm->mkNode(AND, nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z)); - Node o3 = nm->mkNode(AND, nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z)); - - scl = nm->mkNode(OR, o1, o2, o3); - scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + if (pol) + { + /* x >> s = t + * with side condition: + * s = 0 || (s < w && clz(t) >=s) || (s >= w && t = 0) + * -> + * s = 0 + * || (s < w && ((z o t) << (z o s))[2w-1 : w] = z) + * || (s >= w && t = 0) + * with w = getSize(t) = getSize(s) + * and z = 0 with getSize(z) = w */ + Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); + Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s); + Node shl = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); + Node ext = bv::utils::mkExtract(shl, 2*w-1, w); + + Node o1 = s.eqNode(z); + Node o2 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z)); + Node o3 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z)); + + scl = nm->mkNode(OR, o1, o2, o3); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + /* x >> s != t + * with side condition: + * t != 0 || s < w + * with + * w = getSize(s) = getSize(t) + */ + scl = nm->mkNode(OR, + t.eqNode(z).notNode(), + nm->mkNode(BITVECTOR_ULT, s, ww)); + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } } else { - /* s >> x = t - * with side condition: - * t = 0 - * || - * s = t - * || - * \/ (t[w-1-i:0] = s[w-1:i] && t[w-1:w-i] = 0) for 0 < i < w - * where - * w = getSize(s) = getSize(t) - */ - NodeBuilder<> nb(nm, OR); - nb << nm->mkNode(EQUAL, t, s); - for (unsigned i = 1; i < w; ++i) - { - nb << nm->mkNode(AND, - nm->mkNode(EQUAL, - bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i)), - nm->mkNode(EQUAL, - bv::utils::mkExtract(t, w-1, w-i), bv::utils::mkZero(i))); - } - nb << t.eqNode(z); - scl = nb.constructNode(); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + if (pol) + { + /* s >> x = t + * with side condition: + * t = 0 + * || + * s = t + * || + * \/ (t[w-1-i:0] = s[w-1:i] && t[w-1:w-i] = 0) for 0 < i < w + * where + * w = getSize(s) = getSize(t) + */ + NodeBuilder<> nb(nm, OR); + nb << nm->mkNode(EQUAL, t, s); + for (unsigned i = 1; i < w; ++i) + { + nb << nm->mkNode(AND, + nm->mkNode(EQUAL, + bv::utils::mkExtract(t, w - 1 - i, 0), + bv::utils::mkExtract(s, w - 1, i)), + nm->mkNode(EQUAL, + bv::utils::mkExtract(t, w - 1, w - i), + bv::utils::mkZero(i))); + } + nb << t.eqNode(z); + scl = nb.constructNode(); + scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + } + else + { + /* s >> x != t + * 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); + } } Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvAshr(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvAshr(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_ASHR); + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); Node scl, scr; unsigned w = bv::utils::getSize(s); Assert(w == bv::utils::getSize(t)); Node z = bv::utils::mkZero(w); Node n = bv::utils::mkOnes(w); - + if (idx == 0) { - /* x >> s = t - * with side condition: - * s = 0 - * || - * (s < w && (((z o t) << (z o s))[2w-1:w-1] = z - * || - * ((~z o t) << (z o s))[2w-1:w-1] = ~z)) - * || - * (s >= w && (t = 0 || t = ~0)) - * with w = getSize(t) = getSize(s) - * and z = 0 with getSize(z) = w */ - - Node zz = bv::utils::mkZero(w+1); - Node nn = bv::utils::mkOnes(w+1); - Node ww = bv::utils::mkConst(w, w); - - Node z_o_t = bv::utils::mkConcat(z, t); - Node z_o_s = bv::utils::mkConcat(z, s); - Node n_o_t = bv::utils::mkConcat(n, t); - - Node shlz = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); - Node shln = nm->mkNode(BITVECTOR_SHL, n_o_t, z_o_s); - Node extz = bv::utils::mkExtract(shlz, 2*w-1, w-1); - Node extn = bv::utils::mkExtract(shln, 2*w-1, w-1); - - Node o1 = s.eqNode(z); - Node o2 = nm->mkNode(AND, - nm->mkNode(BITVECTOR_ULT, s, ww), - nm->mkNode(OR, extz.eqNode(zz), extn.eqNode(nn))); - Node o3 = nm->mkNode(AND, - nm->mkNode(BITVECTOR_UGE, s, ww), - nm->mkNode(OR, t.eqNode(z), t.eqNode(n))); - - scl = nm->mkNode(OR, o1, o2, o3); - scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + if (pol) + { + /* x >> s = t + * with side condition: + * s = 0 + * || + * (s < w && (((z o t) << (z o s))[2w-1:w-1] = z + * || + * ((~z o t) << (z o s))[2w-1:w-1] = ~z)) + * || + * (s >= w && (t = 0 || t = ~0)) + * with w = getSize(t) = getSize(s) + * and z = 0 with getSize(z) = w */ + + Node zz = bv::utils::mkZero(w+1); + Node nn = bv::utils::mkOnes(w+1); + Node ww = bv::utils::mkConst(w, w); + + Node z_o_t = bv::utils::mkConcat(z, t); + Node z_o_s = bv::utils::mkConcat(z, s); + Node n_o_t = bv::utils::mkConcat(n, t); + + Node shlz = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); + Node shln = nm->mkNode(BITVECTOR_SHL, n_o_t, z_o_s); + Node extz = bv::utils::mkExtract(shlz, 2*w-1, w-1); + Node extn = bv::utils::mkExtract(shln, 2*w-1, w-1); + + Node o1 = s.eqNode(z); + Node o2 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_ULT, s, ww), + nm->mkNode(OR, extz.eqNode(zz), extn.eqNode(nn))); + Node o3 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_UGE, s, ww), + nm->mkNode(OR, t.eqNode(z), t.eqNode(n))); + + scl = nm->mkNode(OR, o1, o2, o3); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + /* x >> s != t + * no side condition */ + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } } else { - /* s >> x = t - * with side condition: - * (s[w-1:w-1] = 0 && t = 0) - * || - * (s[w-1:w-1] = 1 && t == ~0) - * || - * s = t - * || - * \/ (t[w-1-i:0] = s[w-1:i] - * && ((s[w-1:w-1] = 0 && t[w-1:w-i] = 0) - * || - * (s[w-1:w-1] = 1 && t[w-1:w-i] = ~0))) - * for 0 < i < w - * where - * w = getSize(s) = getSize(t) - */ - Node msbz = bv::utils::mkExtract(s, w-1, w-1).eqNode(bv::utils::mkZero(1)); - Node msbn = bv::utils::mkExtract(s, w-1, w-1).eqNode(bv::utils::mkOnes(1)); - NodeBuilder<> nb(nm, OR); - nb << nm->mkNode(EQUAL, t, s); - for (unsigned i = 1; i < w; ++i) + if (pol) { + /* s >> x = t + * with side condition: + * (s[w-1:w-1] = 0 && t = 0) + * || + * (s[w-1:w-1] = 1 && t == ~0) + * || + * s = t + * || + * \/ (t[w-1-i:0] = s[w-1:i] + * && ((s[w-1:w-1] = 0 && t[w-1:w-i] = 0) + * || + * (s[w-1:w-1] = 1 && t[w-1:w-i] = ~0))) + * for 0 < i < w + * where + * w = getSize(s) = getSize(t) + */ + Node msbz = bv::utils::mkExtract( + s, w-1, w-1).eqNode(bv::utils::mkZero(1)); + Node msbn = bv::utils::mkExtract( + s, w-1, w-1).eqNode(bv::utils::mkOnes(1)); + NodeBuilder<> nb(nm, OR); + nb << nm->mkNode(EQUAL, t, s); + for (unsigned i = 1; i < w; ++i) + { + Node ext = bv::utils::mkExtract(t, w-1, w-i); - Node ext = bv::utils::mkExtract(t, w-1, w-i); - - Node o1 = nm->mkNode(AND, msbz, ext.eqNode(bv::utils::mkZero(i))); - Node o2 = nm->mkNode(AND, msbn, ext.eqNode(bv::utils::mkOnes(i))); - Node o = nm->mkNode(OR, o1, o2); + Node o1 = nm->mkNode(AND, msbz, ext.eqNode(bv::utils::mkZero(i))); + Node o2 = nm->mkNode(AND, msbn, ext.eqNode(bv::utils::mkOnes(i))); + Node o = nm->mkNode(OR, o1, o2); - Node e = nm->mkNode(EQUAL, - bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i)); + Node e = nm->mkNode(EQUAL, + bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i)); - nb << nm->mkNode(AND, e, o); + nb << nm->mkNode(AND, e, o); + } + nb << nm->mkNode(AND, msbz, t.eqNode(z)); + nb << nm->mkNode(AND, msbn, t.eqNode(n)); + scl = nb.constructNode(); + scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + } + else + { + /* s >> x != t + * with side condition: + * (t != 0 || s != 0) && (t != ~0 || s != ~0) */ + scl = nm->mkNode(AND, + nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()), + nm->mkNode(OR, t.eqNode(n).notNode(), s.eqNode(n).notNode())); + scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t); } - nb << nm->mkNode(AND, msbz, t.eqNode(z)); - nb << nm->mkNode(AND, msbn, t.eqNode(n)); - scl = nb.constructNode(); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); } - Node sc = nm->mkNode(IMPLIES, scl, scr); + Node sc = scl.isNull() ? scr : nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvShl(Kind k, unsigned idx, Node x, Node s, Node t) +static Node getScBvShl(bool pol, + Kind litk, + Kind k, + unsigned idx, + Node x, + Node s, + Node t) { Assert(k == BITVECTOR_SHL); + if (litk != EQUAL) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); Node scl, scr; unsigned w = bv::utils::getSize(s); Assert(w == bv::utils::getSize(t)); - Node z = bv::utils::mkConst(w, 0u); + Node z = bv::utils::mkZero(w); if (idx == 0) { - /* x << s = t - * with side condition: - * (s = 0 || ctz(t) >= s) - * <-> - * (s = 0 || (s < w && ((t o z) >> (z o s))[w-1:0] = z) || (s >= w && t = 0) - * - * where - * w = getSize(s) = getSize(t) = getSize (z) && z = 0 - */ - Node ww = bv::utils::mkConst(w, w); - Node shr = nm->mkNode(BITVECTOR_LSHR, - bv::utils::mkConcat(t, z), - bv::utils::mkConcat(z, s)); - Node ext = bv::utils::mkExtract(shr, w - 1, 0); - - Node o1 = nm->mkNode(EQUAL, s, z); - Node o2 = nm->mkNode(AND, nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z)); - Node o3 = nm->mkNode(AND, nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z)); - - scl = nm->mkNode(OR, o1, o2, o3); - scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + if (pol) + { + /* x << s = t + * with side condition: + * (s = 0 || ctz(t) >= s) + * <-> + * s = 0 + * || + * (s < w && ((t o z) >> (z o s))[w-1:0] = z) + * || + * (s >= w && t = 0) + * + * where + * w = getSize(s) = getSize(t) = getSize (z) && z = 0 + */ + Node shr = nm->mkNode(BITVECTOR_LSHR, + bv::utils::mkConcat(t, z), + bv::utils::mkConcat(z, s)); + Node ext = bv::utils::mkExtract(shr, w - 1, 0); + + Node o1 = nm->mkNode(EQUAL, s, z); + Node o2 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z)); + Node o3 = nm->mkNode(AND, + nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z)); + + scl = nm->mkNode(OR, o1, o2, o3); + scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + } + else + { + /* x << s != t + * with side condition: + * t != 0 || s < w + * with + * w = getSize(s) = getSize(t) + */ + scl = nm->mkNode(OR, + t.eqNode(z).notNode(), + nm->mkNode(BITVECTOR_ULT, s, ww)); + scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + } } else { - /* s << x = t - * with side condition: - * t = 0 - * || - * s = t - * || - * \/ (t[w-1:i] = s[w-1-i:0] && t[i-1:0] = 0) for 0 < i < w - * where - * w = getSize(s) = getSize(t) - */ - NodeBuilder<> nb(nm, OR); - nb << nm->mkNode(EQUAL, t, s); - for (unsigned i = 1; i < w; ++i) - { - nb << nm->mkNode(AND, - nm->mkNode(EQUAL, - bv::utils::mkExtract(t, w-1, i), bv::utils::mkExtract(s, w-1-i, 0)), - nm->mkNode(EQUAL, - bv::utils::mkExtract(t, i-1, 0), bv::utils::mkZero(i))); - } - nb << t.eqNode(z); - scl = nb.constructNode(); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + if (pol) + { + /* s << x = t + * with side condition: + * t = 0 + * || + * s = t + * || + * \/ (t[w-1:i] = s[w-1-i:0] && t[i-1:0] = 0) for 0 < i < w + * where + * w = getSize(s) = getSize(t) + */ + NodeBuilder<> nb(nm, OR); + nb << nm->mkNode(EQUAL, t, s); + for (unsigned i = 1; i < w; ++i) + { + nb << nm->mkNode(AND, + nm->mkNode(EQUAL, + bv::utils::mkExtract(t, w-1, i), bv::utils::mkExtract(s, w-1-i, 0)), + nm->mkNode(EQUAL, + bv::utils::mkExtract(t, i-1, 0), bv::utils::mkZero(i))); + } + nb << t.eqNode(z); + scl = nb.constructNode(); + scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + } + else + { + /* s << x != t + * 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); + } } Node sc = nm->mkNode(IMPLIES, scl, scr); Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; @@ -690,28 +924,27 @@ static Node getScBvShl(Kind k, unsigned idx, Node x, Node s, Node t) Node BvInverter::solveBvLit(Node sv, Node lit, std::vector<unsigned>& path, - BvInverterQuery* m, - BvInverterStatus& status) + BvInverterQuery* m) { Assert(!path.empty()); bool pol = true; unsigned index, nchildren; NodeManager* nm = NodeManager::currentNM(); - Kind k; + Kind k, litk; Assert(!path.empty()); index = path.back(); Assert(index < lit.getNumChildren()); path.pop_back(); - k = lit.getKind(); - + litk = k = lit.getKind(); + /* Note: option --bool-to-bv is currently disabled when CBQI BV * is enabled. We currently do not support Boolean operators * that are interpreted as bit-vector operators of width 1. */ /* Boolean layer ----------------------------------------------- */ - + if (k == NOT) { pol = !pol; @@ -720,72 +953,16 @@ Node BvInverter::solveBvLit(Node sv, index = path.back(); Assert(index < lit.getNumChildren()); path.pop_back(); - k = lit.getKind(); + litk = k = lit.getKind(); } Assert(k == EQUAL || k == BITVECTOR_ULT - || k == BITVECTOR_SLT - || k == BITVECTOR_COMP); + || k == BITVECTOR_SLT); Node sv_t = lit[index]; Node t = lit[1-index]; - switch (k) - { - case BITVECTOR_ULT: - { - TypeNode solve_tn = sv_t.getType(); - Node sc = getScBvUlt(pol, k, index, getSolveVariable(solve_tn), t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - if (!path.empty()) - { - index = path.back(); - Assert(index < sv_t.getNumChildren()); - path.pop_back(); - sv_t = sv_t[index]; - k = sv_t.getKind(); - } - break; - } - - case BITVECTOR_SLT: - { - TypeNode solve_tn = sv_t.getType(); - Node sc = getScBvSlt(pol, k, index, getSolveVariable(solve_tn), t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - if (!path.empty()) - { - index = path.back(); - Assert(index < sv_t.getNumChildren()); - path.pop_back(); - sv_t = sv_t[index]; - k = sv_t.getKind(); - } - break; - } - - default: - Assert(k == EQUAL); - if (pol == false) - { - TypeNode solve_tn = sv_t.getType(); - Node sc = getScBvEq(pol, k, index, getSolveVariable(solve_tn), t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - if (!path.empty()) - { - index = path.back(); - Assert(index < sv_t.getNumChildren()); - path.pop_back(); - sv_t = sv_t[index]; - k = sv_t.getKind(); - } - } - } - /* Bit-vector layer -------------------------------------------- */ while (!path.empty()) @@ -822,7 +999,7 @@ Node BvInverter::solveBvLit(Node sv, { t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index]) - 1, 0); } - else if (k == BITVECTOR_EXTRACT) + else if (k == BITVECTOR_EXTRACT || k == BITVECTOR_COMP) { Trace("bv-invert") << "bv-invert : Unsupported for index " << index << ", from " << sv_t << std::endl; @@ -834,107 +1011,126 @@ Node BvInverter::solveBvLit(Node sv, Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index); /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS) * are commutative (no case split based on index). */ - switch (k) + if (k == BITVECTOR_PLUS) { - case BITVECTOR_COMP: - t = s; - break; - - case BITVECTOR_PLUS: - t = nm->mkNode(BITVECTOR_SUB, t, s); - break; - - case BITVECTOR_SUB: - t = nm->mkNode(BITVECTOR_PLUS, t, s); - break; + t = nm->mkNode(BITVECTOR_SUB, t, s); + } + else if (k == BITVECTOR_SUB) + { + t = nm->mkNode(BITVECTOR_PLUS, t, s); + } + else if (k == BITVECTOR_XOR) + { + t = nm->mkNode(BITVECTOR_XOR, t, s); + } + else + { + TypeNode solve_tn = sv_t[index].getType(); + Node sc; - case BITVECTOR_MULT: + switch (k) { - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvMult(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; + case BITVECTOR_MULT: + sc = getScBvMult( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + break; + + case BITVECTOR_SHL: + sc = getScBvShl( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + 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; + + case BITVECTOR_UDIV_TOTAL: + sc = getScBvUdiv( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + break; + + case BITVECTOR_AND: + case BITVECTOR_OR: + sc = getScBvAndOr( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + break; + + case BITVECTOR_LSHR: + sc = getScBvLshr( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + break; + + case BITVECTOR_ASHR: + sc = getScBvAshr( + pol, litk, k, index, getSolveVariable(solve_tn), s, t); + break; + + default: + Trace("bv-invert") << "bv-invert : Unknown kind " << k + << " for bit-vector term " << sv_t << std::endl; + return Node::null(); } - - case BITVECTOR_UREM_TOTAL: + Assert (litk != EQUAL || !sc.isNull()); + /* No specific handling for litk and operator k, generate generic + * side condition. */ + if (sc.isNull()) { - if (index == 0) + solve_tn = sv_t.getType(); + if (litk == BITVECTOR_ULT) { - /* 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 = getScBvUlt( + pol, litk, index, getSolveVariable(solve_tn), t); + } + else + { + Assert (litk == BITVECTOR_SLT); + sc = getScBvSlt( + pol, litk, index, getSolveVariable(solve_tn), t); } - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvUrem(k, index, getSolveVariable(solve_tn), s, t); - /* t = skv (fresh skolem constant) */ - t = getInversionNode(sc, solve_tn, m); - break; - } - - case BITVECTOR_UDIV_TOTAL: - { - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvUdiv(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; - } - - case BITVECTOR_AND: - case BITVECTOR_OR: - { - /* with side condition: - * t & s = t - * t | s = t */ - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvAndOr(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; - } - - case BITVECTOR_XOR: - t = nm->mkNode(BITVECTOR_XOR, t, s); - break; - - case BITVECTOR_LSHR: - { - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvLshr(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; - } - - case BITVECTOR_ASHR: - { - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvAshr(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; - } - - case BITVECTOR_SHL: - { - TypeNode solve_tn = sv_t[index].getType(); - Node sc = getScBvShl(k, index, getSolveVariable(solve_tn), s, t); - /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - break; } - - default: - Trace("bv-invert") << "bv-invert : Unknown kind " << k - << " for bit-vector term " << sv_t << std::endl; - return Node::null(); + /* We generate a choice term (choice x0. SC => x0 <k> s <litk> t) for + * x <k> s <litk> t. When traversing down, this choice term determines + * the value for x <k> s = (choice x0. SC => x0 <k> s <litk> t), i.e., + * from here on, the propagated literal is a positive equality. */ + litk = EQUAL; + pol = true; + /* t = fresh skolem constant */ + t = getInversionNode(sc, solve_tn, m); } } sv_t = sv_t[index]; } Assert(sv_t == sv); + if (litk == BITVECTOR_ULT) + { + TypeNode solve_tn = sv_t.getType(); + Node sc = getScBvUlt(pol, litk, index, getSolveVariable(solve_tn), t); + t = getInversionNode(sc, solve_tn, m); + } + else if (litk == BITVECTOR_SLT) + { + TypeNode solve_tn = sv_t.getType(); + Node sc = getScBvSlt(pol, litk, index, getSolveVariable(solve_tn), t); + t = getInversionNode(sc, solve_tn, m); + } + else if (pol == false) + { + Assert (litk == EQUAL); + TypeNode solve_tn = sv_t.getType(); + Node x = getSolveVariable(solve_tn); + Node sc = nm->mkNode(DISTINCT, x, t); + Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc + << std::endl; + t = getInversionNode(sc, solve_tn, m); + } return t; } |