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)
<< " 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++)
}
else
{
+ /* x >= t
+ * no side condition */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
}
else
{
+ /* t >= x
+ * no side condition */
sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
}
}
}
else
{
+ /* x >= t
+ * no side condition */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
}
else
{
+ /* t >= x
+ * no side condition */
sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
}
}
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;
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;
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())
{
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;
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;
}
#include "util/result.h"
using namespace CVC4;
+using namespace CVC4::kind;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::smt;
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;
}
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()
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);
+ }
};
projects / cvc5.git / commitdiff