diff options
48 files changed, 1121 insertions, 675 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; } diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index a44d64904..ce2a58695 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -44,47 +44,22 @@ class BvInverterQuery virtual Node getBoundVariable(TypeNode tn) = 0; }; -// class for storing information about the solved status -class BvInverterStatus { - public: - BvInverterStatus() : d_status(0) {} - ~BvInverterStatus() {} - int d_status; -}; - // inverter class // TODO : move to theory/bv/ if generally useful? -class BvInverter { +class BvInverter +{ public: BvInverter() {} ~BvInverter() {} /** get dummy fresh variable of type tn, used as argument for sv */ Node getSolveVariable(TypeNode tn); - /** get inversion node - * - * This expects a condition cond where: - * (exists x. cond) - * is a BV tautology where x is getSolveVariable( tn ). - * - * It returns a term of the form: - * (choice y. cond { x -> y }) - * where y is a bound variable and x is getSolveVariable( tn ). - * - * In some cases, we may return a term t - * if cond implies an equality on the solve variable. - * For example, if cond is x = t where x is - * getSolveVariable( tn ), then we return t - * instead of introducing the choice function. - */ - Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); - /** Get path to pv in lit, replace that occurrence by sv and all others by * pvs. If return value R is non-null, then : lit.path = pv R.path = sv * R.path' = pvs for all lit.path' = pv, where path' != path */ - Node getPathToPv(Node lit, Node pv, Node sv, Node pvs, - std::vector<unsigned>& path); + Node getPathToPv( + Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path); /** solveBvLit * solve for sv in lit, where lit.path = sv @@ -93,16 +68,35 @@ class BvInverter { Node solveBvLit(Node sv, Node lit, std::vector<unsigned>& path, - BvInverterQuery* m, - BvInverterStatus& status); + BvInverterQuery* m); private: - /** dummy variables for each type */ + /** Dummy variables for each type */ std::map<TypeNode, Node> d_solve_var; - /** helper function for getPathToPv */ - Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path, + /** Helper function for getPathToPv */ + Node getPathToPv(Node lit, + Node pv, + Node sv, + std::vector<unsigned>& path, std::unordered_set<TNode, TNodeHashFunction>& visited); + + /** Helper function for getInv. + * + * This expects a condition cond where: + * (exists x. cond) + * is a BV tautology where x is getSolveVariable( tn ). + * + * It returns a term of the form: + * (choice y. cond { x -> y }) + * where y is a bound variable and x is getSolveVariable( tn ). + * + * In some cases, we may return a term t if cond implies an equality on + * the solve variable. For example, if cond is x = t where x is + * getSolveVariable(tn), then we return t instead of introducing the choice + * function. + */ + Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 55cc59c51..e4bc9adb8 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -965,7 +965,6 @@ void BvInstantiator::reset(CegInstantiator* ci, d_inst_id_counter = 0; d_var_to_inst_id.clear(); d_inst_id_to_term.clear(); - d_inst_id_to_status.clear(); d_inst_id_to_alit.clear(); d_var_to_curr_inst_id.clear(); d_alit_to_model_slack.clear(); @@ -979,31 +978,32 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Node alit, CegInstEffort effort) { - Assert( d_inverter!=NULL ); + Assert(d_inverter != NULL); // find path to pv - std::vector< unsigned > path; - Node sv = d_inverter->getSolveVariable( pv.getType() ); - Node pvs = ci->getModelValue( pv ); + std::vector<unsigned> path; + Node sv = d_inverter->getSolveVariable(pv.getType()); + Node pvs = ci->getModelValue(pv); Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl; - Node slit = d_inverter->getPathToPv( lit, pv, sv, pvs, path ); - if( !slit.isNull() ){ + Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path); + if (!slit.isNull()) + { CegInstantiatorBvInverterQuery m(ci); unsigned iid = d_inst_id_counter; Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl; - Node inst = - d_inverter->solveBvLit(sv, slit, path, &m, d_inst_id_to_status[iid]); - if( !inst.isNull() ){ + Node inst = d_inverter->solveBvLit(sv, slit, path, &m); + if (!inst.isNull()) + { inst = Rewriter::rewrite(inst); Trace("cegqi-bv") << "...solved form is " << inst << std::endl; // store information for id and increment - d_var_to_inst_id[pv].push_back( iid ); + d_var_to_inst_id[pv].push_back(iid); d_inst_id_to_term[iid] = inst; d_inst_id_to_alit[iid] = alit; d_inst_id_counter++; - }else{ + } + else + { Trace("cegqi-bv") << "...failed to solve." << std::endl; - // cleanup information if we failed to solve - d_inst_id_to_status.erase( iid ); } } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index c2864acc5..0648942e8 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -231,7 +231,6 @@ class BvInstantiator : public Instantiator { /** information about solved forms */ std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id; std::unordered_map< unsigned, Node > d_inst_id_to_term; - std::unordered_map< unsigned, BvInverterStatus > d_inst_id_to_status; std::unordered_map<unsigned, Node> d_inst_id_to_alit; // variable to current id we are processing std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index c59570651..bb43d6c1c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -90,25 +90,38 @@ TESTS = \ qbv-simp.smt2 \ psyco-001-bv.smt2 \ bug822.smt2 \ - qbv-test-invert-mul.smt2 \ + qbv-disequality3.smt2 \ + qbv-inequality2.smt2 \ + qbv-simple-2vars-vo.smt2 \ + qbv-test-invert-bvadd-neq.smt2 \ qbv-test-invert-bvand.smt2 \ - qbv-test-invert-bvcomp.smt2 \ - qbv-test-invert-bvor.smt2 \ - qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvand-neq.smt2 \ qbv-test-invert-bvashr-0.smt2 \ + qbv-test-invert-bvashr-0-neq.smt2 \ + qbv-test-invert-bvashr-1.smt2 \ + qbv-test-invert-bvashr-1-neq.smt2 \ + qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvlshr-0-neq.smt2 \ + qbv-test-invert-bvlshr-1.smt2 \ + qbv-test-invert-bvlshr-1-neq.smt2 \ + qbv-test-invert-bvmul.smt2 \ + qbv-test-invert-bvmul-neq.smt2 \ + qbv-test-invert-bvor.smt2 \ + qbv-test-invert-bvor-neq.smt2 \ + qbv-test-invert-bvshl-0.smt2 \ + qbv-test-invert-bvudiv-0.smt2 \ + qbv-test-invert-bvudiv-0-neq.smt2 \ + qbv-test-invert-bvudiv-1.smt2 \ + qbv-test-invert-bvudiv-1-neq.smt2 \ + qbv-test-invert-bvult-1.smt2 \ qbv-test-invert-bvurem-1.smt2 \ + qbv-test-invert-bvurem-1-neq.smt2 \ + qbv-test-invert-bvxor.smt2 \ + qbv-test-invert-bvxor-neq.smt2 \ qbv-test-invert-concat-0.smt2 \ qbv-test-invert-concat-1.smt2 \ - qbv-test-invert-disequality.smt2 \ - qbv-test-invert-shl.smt2 \ - qbv-test-invert-udiv-0.smt2 \ - qbv-test-invert-udiv-1.smt2 \ qbv-test-invert-sign-extend.smt2 \ - qbv-test-invert-bvxor.smt2 \ - qbv-simple-2vars-vo.smt2 \ qbv-test-urem-rewrite.smt2 \ - qbv-inequality2.smt2 \ - qbv-test-invert-bvult-1.smt2 \ intersection-example-onelane.proof-node22337.smt2 \ nested9_true-unreach-call.i_575.smt2 \ small-pipeline-fixpoint-3.smt2 \ @@ -127,6 +140,8 @@ TESTS = \ # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 +# disabled since bvcomp handling is currently disabled +# qbv-test-invert-bvcomp.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress0/quantifiers/qbv-disequality3.smt2 b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 new file mode 100644 index 000000000..d16157509 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul (bvadd x b) a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 index d53715a2d..1486e176d 100644 --- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 +++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 @@ -1,11 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) - -(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b)))) +(assert (forall ((x (_ BitVec 8))) (or (bvuge x (bvadd a b)) (bvule x b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 index d74a6cfea..3c4f93243 100644 --- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 +++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2 index 1f72d44e4..ec4626f52 100644 --- a/test/regress/regress0/quantifiers/qbv-simp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simp.smt2 @@ -1,9 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; EXPECT: unsat (set-logic BV) (set-info :status unsat) (assert (forall - ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32))) + ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8))) (or (and (= A B) (= C D)) (and (= A C) (= B D))))) - + (check-sat) - + diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 index b6ae95fec..c36322aac 100644 --- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,16 +1,16 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(declare-fun c () (_ BitVec 8)) -(assert (not (= a #x00000000))) +(assert (not (= a #x00))) -(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or -(not (= (bvmul x y) #x0000000A)) -(not (= (bvadd y a) #x00000010)) +(assert (forall ((x (_ BitVec 8)) (y (_ BitVec 8))) (or +(not (= (bvmul x y) #x0A)) +(not (= (bvadd y a) #x10)) ))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 new file mode 100644 index 000000000..216a98531 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvadd x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 new file mode 100644 index 000000000..ad3b9a9e5 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvand x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 index d611fcd68..8dd50b1be 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvand x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 index db7725896..30e7c2f8b 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 new file mode 100644 index 000000000..2835e5956 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 new file mode 100644 index 000000000..c3de64c4c --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 index e8f7c25db..3b55c0b9a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,11 +1,11 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) (declare-fun c () (_ BitVec 1)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x b))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvcomp x a) ((_ extract 7 7) (bvmul a b)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 index db7725896..1018ce72c 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 new file mode 100644 index 000000000..503bc9852 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvlshr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 new file mode 100644 index 000000000..08479d90e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 new file mode 100644 index 000000000..9dc9f98ac --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 new file mode 100644 index 000000000..f3dad679b --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvmul x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 new file mode 100644 index 000000000..74c2891cf --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvor x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 index 287da08c7..4145c68b1 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvor x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 new file mode 100644 index 000000000..e85ecc7de --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvshl x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 new file mode 100644 index 000000000..abef84da2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvshl x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 new file mode 100644 index 000000000..3748eca24 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 new file mode 100644 index 000000000..2cabb502e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 new file mode 100644 index 000000000..a0e1b62c2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 index bf69a8b4a..2690a0ac9 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 index 13c1bf10a..a1dca469a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) +(assert (forall ((x (_ BitVec 8))) (not (bvult a x)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 new file mode 100644 index 000000000..871df4827 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvurem a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 index f7fe54e3e..22bd306ee 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvurem a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 new file mode 100644 index 000000000..4f9c6edc3 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 index eec40a425..ef41eecdd 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 new file mode 100644 index 000000000..769854f6f --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 index f4e19fc52..7b66bd859 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 new file mode 100644 index 000000000..7dab5637e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 index 827e74605..13fb3e1c2 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 deleted file mode 100644 index 6ba782597..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 deleted file mode 100644 index 84e9fa7ce..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 deleted file mode 100644 index 97a0662eb..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (not (= (bvshl x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 index 21aa519ad..43019c4cb 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= ((_ sign_extend 8) x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 deleted file mode 100644 index becfc5315..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 16)) -(declare-fun b () (_ BitVec 16)) - -(assert (distinct a b (_ bv0 16))) -(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 index 6df69d80b..e57352b8f 100644 --- a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index ce01c17e4..5e1d404dc 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -23,6 +23,7 @@ #include "util/result.h" using namespace CVC4; +using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::smt; @@ -45,58 +46,63 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite unsigned idx, Node (*getsc)(bool, Kind, unsigned, Node, Node)) { - Assert(k == kind::BITVECTOR_ULT - || k == kind::BITVECTOR_SLT - || k == kind::EQUAL); - Assert(k != kind::EQUAL || pol == false); + Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL); + Assert(k != EQUAL || pol == false); Node sc = getsc(pol, k, idx, d_sk, d_t); Kind ksc = sc.getKind(); - TS_ASSERT((k == kind::BITVECTOR_ULT && pol == false) - || (k == kind::BITVECTOR_SLT && pol == false) - || ksc == kind::IMPLIES); - Node scl = ksc == kind::IMPLIES ? sc[0] : bv::utils::mkTrue(); + TS_ASSERT((k == BITVECTOR_ULT && pol == false) + || (k == BITVECTOR_SLT && pol == false) + || ksc == IMPLIES); + Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); if (!pol) { - k = k == kind::BITVECTOR_ULT - ? kind::BITVECTOR_UGE - : (k == kind::BITVECTOR_SLT ? kind::BITVECTOR_SGE : kind::DISTINCT); + k = k == BITVECTOR_ULT + ? BITVECTOR_UGE + : (k == BITVECTOR_SLT ? BITVECTOR_SGE : DISTINCT); } Node body = idx == 0 ? d_nm->mkNode(k, d_x, d_t) : d_nm->mkNode(k, d_t, d_x); - Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body); - Expr a = d_nm->mkNode(kind::DISTINCT, scl, scr).toExpr(); + Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body); + Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr(); Result res = d_smt->checkSat(a); TS_ASSERT(res.d_sat == Result::UNSAT); } - void runTest(Kind k, + void runTest(bool pol, + Kind litk, + Kind k, unsigned idx, - Node (*getsc)(Kind, unsigned, Node, Node, Node)) - { - Assert(k == kind::BITVECTOR_MULT - || k == kind::BITVECTOR_UREM_TOTAL - || k == kind::BITVECTOR_UDIV_TOTAL - || k == kind::BITVECTOR_AND - || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_LSHR - || k == kind::BITVECTOR_ASHR - || k == kind::BITVECTOR_SHL); - Assert(k != kind::BITVECTOR_UREM_TOTAL || idx == 1); - - Node sc = getsc(k, idx, d_sk, d_s, d_t); + Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node)) + { + Assert(k == BITVECTOR_MULT + || k == BITVECTOR_UREM_TOTAL + || k == BITVECTOR_UDIV_TOTAL + || k == BITVECTOR_AND + || k == BITVECTOR_OR + || k == BITVECTOR_LSHR + || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL); + Assert(k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1); + + Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); + TS_ASSERT (litk != EQUAL || sc != Node::null()); Kind ksc = sc.getKind(); - TS_ASSERT(ksc == kind::IMPLIES); + TS_ASSERT((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false) + || (k == BITVECTOR_ASHR && idx == 0 && pol == false) + || ksc == IMPLIES); + Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); Node body = idx == 0 - ? d_nm->mkNode(k, d_x, d_s).eqNode(d_t) - : d_nm->mkNode(k, d_s, d_x).eqNode(d_t); - Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body); - Expr a = d_nm->mkNode(kind::DISTINCT, sc[0], scr).toExpr(); + ? d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_x, d_s), d_t) + : d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_s, d_x), d_t); + Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body); + Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr(); Result res = d_smt->checkSat(a); if (res.d_sat == Result::SAT) { - std::cout << std::endl << "s " << d_smt->getValue(d_s.toExpr()) << std::endl; + std::cout << std::endl; + std::cout << "s " << d_smt->getValue(d_s.toExpr()) << std::endl; std::cout << "t " << d_smt->getValue(d_t.toExpr()) << std::endl; std::cout << "x " << d_smt->getValue(d_x.toExpr()) << std::endl; } @@ -119,7 +125,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite d_t = d_nm->mkVar("t", d_nm->mkBitVectorType(4)); d_sk = d_nm->mkSkolem("sk", d_t.getType()); d_x = d_nm->mkBoundVar(d_t.getType()); - d_bvarlist = d_nm->mkNode(kind::BOUND_VAR_LIST, { d_x }); + d_bvarlist = d_nm->mkNode(BOUND_VAR_LIST, { d_x }); } void tearDown() @@ -174,99 +180,163 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt); } - void testGetScBvEq0() + void testGetScBvMultEqTrue0() { - runTestPred(false, EQUAL, 0, getScBvEq); - TS_ASSERT_THROWS(runTestPred(true, EQUAL, 0, getScBvEq), - AssertionException); + runTest(true, EQUAL, BITVECTOR_MULT, 0, getScBvMult); } - void testGetScBvEq1() + void testGetScBvMultEqTrue1() { - runTestPred(false, EQUAL, 1, getScBvEq); - TS_ASSERT_THROWS(runTestPred(true, EQUAL, 1, getScBvEq), - AssertionException); + runTest(true, EQUAL, BITVECTOR_MULT, 1, getScBvMult); } - void testGetScBvMult0() + void testGetScBvMultEqFalse0() { - runTest(BITVECTOR_MULT, 0, getScBvMult); + runTest(false, EQUAL, BITVECTOR_MULT, 0, getScBvMult); } - void testGetScBvMult1() + void testGetScBvMultEqFalse1() { - runTest(BITVECTOR_MULT, 1, getScBvMult); + runTest(false, EQUAL, BITVECTOR_MULT, 1, getScBvMult); } - void testGetScBvUrem0() + void testGetScBvUremEqTrue0() { - TS_ASSERT_THROWS(runTest(BITVECTOR_UREM_TOTAL, 0, getScBvUrem), + TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem), AssertionException); } - void testGetScBvUrem1() + void testGetScBvUremEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + void testGetScBvUremEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + void testGetScBvUdivEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + void testGetScBvUdivFalse0() { - runTest(BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); } - void testGetScBvUdiv0() + void testGetScBvUdivFalse1() { - runTest(BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); } - void testGetScBvUdiv1() + void testGetScBvAndEqTrue0() { - runTest(BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + runTest(true, EQUAL, BITVECTOR_AND, 0, getScBvAndOr); } - void testGetScBvAnd0() + void testGetScBvAndEqTrue1() { - runTest(BITVECTOR_AND, 0, getScBvAndOr); + runTest(true, EQUAL, BITVECTOR_AND, 1, getScBvAndOr); } - void testGetScBvAnd1() + void testGetScBvAndEqFalse0() { - runTest(BITVECTOR_AND, 1, getScBvAndOr); + runTest(false, EQUAL, BITVECTOR_AND, 0, getScBvAndOr); } - void testGetScBvOr0() + void testGetScBvAndEqFalse1() { - runTest(BITVECTOR_OR, 0, getScBvAndOr); + runTest(false, EQUAL, BITVECTOR_AND, 1, getScBvAndOr); } - void testGetScBvOr1() + void testGetScBvOrEqTrue0() { - runTest(BITVECTOR_OR, 1, getScBvAndOr); + runTest(true, EQUAL, BITVECTOR_OR, 0, getScBvAndOr); } - void testGetScBvLshr0() + void testGetScBvOrEqTrue1() { - runTest(BITVECTOR_LSHR, 0, getScBvLshr); + runTest(true, EQUAL, BITVECTOR_OR, 1, getScBvAndOr); } - void testGetScBvLshr1() + void testGetScBvOrEqFalse0() { - runTest(BITVECTOR_LSHR, 1, getScBvLshr); + runTest(false, EQUAL, BITVECTOR_OR, 0, getScBvAndOr); } - void testGetScBvAshr0() + void testGetScBvOrEqFalse1() { - runTest(BITVECTOR_ASHR, 0, getScBvAshr); + runTest(false, EQUAL, BITVECTOR_OR, 1, getScBvAndOr); } - void testGetScBvAshr1() + void testGetScBvLshrEqTrue0() { - runTest(BITVECTOR_ASHR, 1, getScBvAshr); + runTest(true, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr); } - void testGetScBvShl0() + void testGetScBvLshrEqTrue1() { - runTest(BITVECTOR_SHL, 0, getScBvShl); + runTest(true, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr); } - void testGetScBvShl1() + void testGetScBvLshrEqFalse0() { - runTest(BITVECTOR_SHL, 1, getScBvShl); + runTest(false, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr); } + void testGetScBvLshrEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr); + } + + void testGetScBvAshrEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvAshrEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvShlEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_SHL, 1, getScBvShl); + } + + void testGetScBvShlEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_SHL, 1, getScBvShl); + } }; |