/* x < t
* with side condition:
* (distinct t z)
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkZero(w));
Node scr = nm->mkNode(k, x, t);
sc = nm->mkNode(IMPLIES, scl, scr);
/* x > t
* with side condition:
* (distinct t ones)
- * where ones = ~0 with getSize(ones) = w */
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w));
Node scr = nm->mkNode(k, x, t);
sc = nm->mkNode(IMPLIES, scl, scr);
else
{
/* x <= t
- * true (no side condition) */
+ * true (no side condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
/* x < t
* with side condition:
* (distinct t min)
- * where min is the minimum signed value with getSize(min) = w */
+ * where
+ * min is the minimum signed value with getSize(min) = w */
Node min = bv::utils::mkConst(BitVector(w).setBit(w - 1));
Node scl = nm->mkNode(DISTINCT, min, t);
Node scr = nm->mkNode(k, x, t);
else
{
/* x >= t
- * true (no side condition) */
+ * true (no side condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
/* x > t
* with side condition:
* (distinct t max)
- * where max is the maximum signed value with getSize(max) = w */
+ * where
+ * max is the signed maximum value with getSize(max) = w */
BitVector bv = BitVector(w).setBit(w - 1);
Node max = bv::utils::mkConst(~bv);
Node scl = nm->mkNode(DISTINCT, t, max);
else
{
/* x <= t
- * true (no side condition) */
+ * true (no side condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
* (and
* (bvuge (bvand t (bvneg t)) (bvand s (bvneg s)))
* (distinct s z)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, o, t), t);
}
/* x * s != t
* with side condition:
* (or (distinct t z) (distinct s z))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode());
}
}
/* x * s < t
* with side condition (synthesized):
* (distinct t z)
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = nm->mkNode(DISTINCT, t, z);
}
{
/* x * s >= t
* with side condition (synthesized):
- * (not (bvult (bvor (bvneg s) s) t)) */
+ * (bvuge (bvor (bvneg s) s) t) */
Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
scl = nm->mkNode(BITVECTOR_UGE, o, t);
}
else
{
/* x * s <= t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* x * s >= t
* with side condition (synthesized):
- * (bvsge (bvand (bvor (bvneg s) s) max) t))
- * where max is the maximum signed value with getSize(max) = w */
+ * (bvsge (bvand (bvor (bvneg s) s) max) t)
+ * where
+ * max is the signed maximum value with getSize(max) = w */
BitVector bv = BitVector(w).setBit(w - 1);
Node max = bv::utils::mkConst(~bv);
Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
scl = nm->mkNode(BITVECTOR_SGE, a, t);
}
}
- else /* litk == BITVECTOR_SGT */
+ else /* litk == BITVECTOR_SGT */
{
if (pol)
{
/* x * s <= t
* with side condition (synthesized):
* (not (and (= s z) (bvslt t s)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = nm->mkNode(AND, s.eqNode(z), nm->mkNode(BITVECTOR_SLT, t, s));
scl = scl.notNode();
{
/* x % s = t
* with side condition (synthesized):
- * (not (bvult (bvnot (bvneg s)) t)) */
+ * (bvuge (bvnot (bvneg s)) t) */
Node neg = nm->mkNode(BITVECTOR_NEG, s);
scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
}
/* x % s != t
* with side condition:
* (or (distinct s (_ bv1 w)) (distinct t z))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = nm->mkNode(OR,
s.eqNode(bv::utils::mkOne(w)).notNode(),
* (and (bvugt s t)
* (bvugt (bvsub s t) t)
* (or (= t z) (distinct (bvsub s (_ bv1 w)) t))))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
Node a = nm->mkNode(BITVECTOR_AND, sub, s);
/* s % x != t
* with side condition:
* (or (distinct s z) (distinct t z))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
}
/* x % s < t
* with side condition:
* (distinct t z)
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = t.eqNode(z).notNode();
}
/* s % x < t
* with side condition:
* (distinct t z)
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = t.eqNode(z).notNode();
}
else
{
/* x % s <= t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
else
{
/* s % x <= t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
/* x % s >= t
* with side condition (synthesized):
* (or (bvslt t s) (bvsge z s))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
Node s1 = nm->mkNode(BITVECTOR_SLT, t, s);
Node s2 = nm->mkNode(BITVECTOR_SGE, z, s);
/* s % x < t
* with side condition (synthesized):
* (or (bvslt s t) (bvslt z t))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t);
Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t);
scl = nm->mkNode(OR, slt1, slt2);
* (and
* (=> (bvsge s z) (bvsge s t))
* (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node i1 = nm->mkNode(IMPLIES,
nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGE, s, t));
Node i2 = nm->mkNode(IMPLIES,
* (=> (bvsgt s z) (bvslt t (bvnot (bvneg s))))
* (=> (bvsle s z) (distinct t max)))
* (or (distinct t z) (distinct s (_ bv1 w))))
- * where z = 0 with getSize(z) = w
+ * where
+ * z = 0 with getSize(z) = w
* and max is the maximum signed value with getSize(max) = w */
BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
BitVector bv_max = BitVector(1).concat(bv_ones);
{
/* x % s <= t
* with side condition (synthesized):
- * (bvslt (bvnot z) (bvand (bvneg s) t))
- * where z = 0 with getSize(z) = w */
+ * (bvslt ones (bvand (bvneg s) t))
+ * where
+ * z = 0 with getSize(z) = w
+ * and ones = ~0 with getSize(ones) = w */
Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, s), t);
- scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, z), a);
+ scl = nm->mkNode(BITVECTOR_SLT, bv::utils::mkOnes(w), a);
}
}
else
{
if (pol)
{
- /* s % x >= t
+ /* s % x > t
* with side condition:
* (and
* (=> (bvsge s z) (bvsgt s t))
* (=> (bvslt s z)
* (bvsgt (bvlshr (bvsub s (_ bv1 w)) (_ bv1 w)) t)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
Node i1 = nm->mkNode(IMPLIES,
nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGT, s, t));
}
else
{
- /* s % x < t
+ /* s % x <= t
* with side condition (synthesized):
* (or (bvult t min) (bvsge t s))
- * where min is the minimum signed value with getSize(min) = w */
+ * where
+ * min is the minimum signed value with getSize(min) = w */
BitVector bv_min = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min);
Node o1 = nm->mkNode(BITVECTOR_ULT, t, min);
* (distinct s z)
* (not (umulo s t))))
*
- * where umulo(s, t) is true if s * t produces and overflow
+ * where
+ * umulo(s, t) is true if s * t produces and overflow
* and z = 0 with getSize(z) = w */
Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s);
/* x udiv s != t
* with side condition:
* (or (distinct s z) (distinct t ones))
- * where z = 0 with getSize(z) = w
+ * where
+ * z = 0 with getSize(z) = w
* and ones = ~0 with getSize(ones) = w */
Node ones = bv::utils::mkOnes(w);
scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(ones).notNode());
* (bvudiv s t)))
* (=> (= s (bvnot (_ bv0 8))) (distinct t (_ bv0 8)))))
*
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t);
scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, div), t);
}
else
{
/* s udiv x != t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
/* x udiv s < t
* with side condition (synthesized):
* (and (bvult z s) (bvult z t))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node u1 = nm->mkNode(BITVECTOR_ULT, z, s);
Node u2 = nm->mkNode(BITVECTOR_ULT, z, t);
scl = nm->mkNode(AND, u1, u2);
/* s udiv x < t
* with side condition (synthesized):
* (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, t), s);
Node u1 = nm->mkNode(BITVECTOR_ULT, z, nm->mkNode(BITVECTOR_NOT, a));
Node u2 = nm->mkNode(BITVECTOR_ULT, z, t);
else
{
/* s udiv x >= t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
/* x udiv s > t
* with side condition:
* (bvugt (bvudiv ones s) t)
- * where ones = ~0 with getSize(ones) = w */
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node ones = bv::utils::mkOnes(w);
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s);
scl = nm->mkNode(BITVECTOR_UGT, div, t);
{
/* x udiv s <= t
* with side condition (synthesized):
- * (not (bvult (bvor s t) (bvnot (bvneg s)))) */
+ * (bvuge (bvor s t) (bvnot (bvneg s))) */
Node u1 = nm->mkNode(BITVECTOR_OR, s, t);
Node u2 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s));
scl = nm->mkNode(BITVECTOR_UGE, u1, u2);
/* s udiv x > t
* with side condition (synthesized):
* (bvult t ones)
- * where ones = ~0 with getSize(ones) = w */
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node ones = bv::utils::mkOnes(w);
scl = nm->mkNode(BITVECTOR_ULT, t, ones);
}
/* s udiv x <= t
* with side condition (synthesized):
* (bvult z (bvor (bvnot s) t))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
scl = nm->mkNode(BITVECTOR_ULT,
z, nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NOT, s), t));
}
/* x udiv s < t
* with side condition:
* (=> (bvsle t z) (bvslt (bvudiv min s) t))
- * where z = 0 with getSize(z) = w
+ * where
+ * z = 0 with getSize(z) = w
* and min is the minimum signed value with getSize(min) = w */
BitVector bv_min = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min);
* (or
* (bvsge (bvudiv ones s) t)
* (bvsge (bvudiv max s) t))
- * where ones = ~0 with getSize(ones) = w
+ * where
+ * ones = ~0 with getSize(ones) = w
* and max is the maximum signed value with getSize(max) = w */
BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
BitVector bv_max = BitVector(1).concat(bv_ones);
/* s udiv x < t
* with side condition (synthesized):
* (or (bvslt s t) (bvsge t z))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node slt = nm->mkNode(BITVECTOR_SLT, s, t);
Node sge = nm->mkNode(BITVECTOR_SGE, t, z);
scl = nm->mkNode(OR, slt, sge);
* (and
* (=> (bvsge s z) (bvsge s t))
* (=> (bvslt s z) (bvsge (bvudiv s (_ bv2 w)) t)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL,
s, bv::utils::mkConst(w, 2));
Node i1 = nm->mkNode(IMPLIES,
}
}
}
- else /* litk == BITVECTOR_SGT */
+ else /* litk == BITVECTOR_SGT */
{
if (idx == 0)
{
* (or
* (bvsgt (bvudiv ones s) t)
* (bvsgt (bvudiv max s) t))
- * where ones = ~0 with getSize(ones) = w
+ * where
+ * ones = ~0 with getSize(ones) = w
* and max is the maximum signed value with getSize(max) = w */
BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
BitVector bv_max = BitVector(1).concat(bv_ones);
* (or
* (= (bvudiv (bvmul s t) s) t) ; eq, synthesized
* (=> (bvsle t z) (bvslt (bvudiv min s) t))) ; slt
- * where z = 0 with getSize(z) = w
+ * where
+ * z = 0 with getSize(z) = w
* and min is the minimum signed value with getSize(min) = w */
Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s);
* (and
* (=> (bvsge s z) (bvsgt s t))
* (=> (bvslt s z) (bvsgt (bvudiv s (_ bv2 w)) t)))
- * where z = 0 with getSize(z) = w */
+ * where
+ * z = 0 with getSize(z) = w */
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL,
s, bv::utils::mkConst(w, 2));
Node i1 = nm->mkNode(IMPLIES,
* (not (and (bvslt t (bvnot #x0)) (bvslt t s)))
* <->
* (or (bvsge t ones) (bvsge t s))
- * where ones = ~0 with getSize(ones) = w */
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node ones = bv::utils::mkOnes(w);
Node sge1 = nm->mkNode(BITVECTOR_SGE, t, ones);
Node sge2 = nm->mkNode(BITVECTOR_SGE, t, s);
|| litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
NodeManager* nm = NodeManager::currentNM();
+ unsigned w = bv::utils::getSize(s);
+ Assert (w == bv::utils::getSize(t));
Node scl;
if (litk == EQUAL)
/* x & s = t
* x | s = t
* with side condition:
- * t & s = t
- * t | s = t */
+ * (= (bvand t s) t)
+ * (= (bvor t s) t) */
scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
}
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 */
+ * (or (distinct s z) (distinct t z))
+ * where
+ * z = 0 with getSize(z) = w */
Node z = bv::utils::mkZero(w);
scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
}
{
/* x | s = t
* with side condition:
- * s != ~0 || t != ~0 */
+ * (or (distinct s ones) (distinct t ones))
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node n = bv::utils::mkOnes(w);
scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode());
}
{
/* x & s < t
* with side condition (synthesized):
- * t != 0 */
- Node z = bv::utils::mkZero(bv::utils::getSize(t));
+ * (distinct t z)
+ * where
+ * z = 0 with getSize(z) = 0 */
+ Node z = bv::utils::mkZero(w);
scl = t.eqNode(z).notNode();
}
else
{
/* x | s < t
* with side condition (synthesized):
- * (bvult s t) */
+ * (bvult s t) */
scl = nm->mkNode(BITVECTOR_ULT, s, t);
}
}
- else /* litk == BITVECTOR_SLT */
+ else
{
if (k == BITVECTOR_AND)
{
/* x & s >= t
* with side condition (synthesized):
- * (not (bvult s t)) */
+ * (bvuge s t) */
scl = nm->mkNode(BITVECTOR_UGE, s, t);
}
else
{
/* x | s >= t
* with side condition (synthesized):
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
}
+ else if (litk == BITVECTOR_UGT)
+ {
+ if (pol)
+ {
+ if (k == BITVECTOR_AND)
+ {
+ /* x & s > t
+ * with side condition (synthesized):
+ * (bvult t s) */
+ scl = nm->mkNode(BITVECTOR_ULT, t, s);
+ }
+ else
+ {
+ /* x | s > t
+ * with side condition (synthesized):
+ * (bvult t ones)
+ * where
+ * ones = ~0 with getSize(ones) = w */
+ scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w));
+ }
+ }
+ else
+ {
+ if (k == BITVECTOR_AND)
+ {
+ /* x & s <= t
+ * with side condition (synthesized):
+ * true (no side condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ else
+ {
+ /* x | s <= t
+ * with side condition (synthesized):
+ * (bvuge t s) */
+ scl = nm->mkNode(BITVECTOR_UGE, t, s);
+ }
+ }
+ }
else if (litk == BITVECTOR_SLT)
{
if (pol)
{
/* x & s < t
* with side condition (synthesized):
- * (bvslt (bvand (bvnot (bvneg t)) s) t) */
+ * (bvslt (bvand (bvnot (bvneg t)) s) t) */
Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t));
scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, nnt, s), t);
}
{
/* x | s < t
* with side condition (synthesized):
- * (bvslt (bvor (bvnot (bvsub s t)) s) t) */
+ * (bvslt (bvor (bvnot (bvsub s t)) s) t) */
Node st = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_SUB, s, t));
scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_OR, st, s), t);
}
* with side condition (case = combined with synthesized bvsgt):
* (or
* (= (bvand s t) t)
- * (bvslt t (bvand (bvsub t s) s))
- * ) */
+ * (bvslt t (bvand (bvsub t s) s))) */
Node sc_sgt = nm->mkNode(
BITVECTOR_SLT,
t,
{
/* x | s >= t
* with side condition (synthesized):
- * (not (bvslt s (bvand s t))) */
+ * (bvsge s (bvand s t)) */
scl = nm->mkNode(BITVECTOR_SGE, s, nm->mkNode(BITVECTOR_AND, s, t));
}
}
}
else
{
- return Node::null();
+ Assert(litk == BITVECTOR_SGT);
+ if (pol)
+ {
+ /* x & s > t
+ * x | s > t
+ * with side condition (synthesized):
+ * (bvslt t (bvand s max))
+ * (bvslt t (bvor s max))
+ * where
+ * max is the signed maximum value with getSize(max) = w */
+ BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
+ BitVector bv_max_val = BitVector(1).concat(bv_ones);
+ Node max = bv::utils::mkConst(bv_max_val);
+ scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(k, s, max));
+ }
+ else
+ {
+ if (k == BITVECTOR_AND)
+ {
+ /* x & s <= t
+ * with side condition (synthesized):
+ * (bvuge s (bvand t min))
+ * where
+ * min is the signed minimum value with getSize(min) = w */
+ BitVector bv_min_val = BitVector(w).setBit(w - 1);
+ Node min = bv::utils::mkConst(bv_min_val);
+ scl = nm->mkNode(BITVECTOR_UGE, s, nm->mkNode(BITVECTOR_AND, t, min));
+ }
+ else
+ {
+ /* x | s <= t
+ * with side condition (synthesized):
+ * (bvsge t (bvor s min))
+ * where
+ * min is the signed minimum value with getSize(min) = w */
+ BitVector bv_min_val = BitVector(w).setBit(w - 1);
+ Node min = bv::utils::mkConst(bv_min_val);
+ scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_OR, s, min));
+ }
+ }
}
Node scr = nm->mkNode(litk, nm->mkNode(k, x, s), t);
Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode());
* 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)
+ * (or
+ * (= s z)
+ * (and
+ * (bvult s w)
+ * (= ((_ extract 2*w-1 w) (bvshl (concat z t) (concat z s))) z))
+ * (and (bvuge s w) (= t z)))
* with w = getSize(t) = getSize(s)
* and z = 0 with getSize(z) = w */
Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t);
{
/* x >> s != t
* with side condition:
- * t != 0 || s < w
- * with
- * w = getSize(s) = getSize(t)
- */
+ * (or (distinct t z) (bvult s w))
+ * where
+ * z = 0 with getSize(z) = w
+ * and w = getSize(s) = getSize(t) */
scl = nm->mkNode(OR,
t.eqNode(z).notNode(),
nm->mkNode(BITVECTOR_ULT, s, ww));
{
/* 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
+ * (or
+ * (= t z)
+ * (= s t)
+ * (and
+ * (= ((_ extract w-1-i 0) t) ((_ extract w-1 i) s))
+ * (= ((_ extract w-1 w-i) t) z_i)))
+ * for 0 < i < w
* where
* w = getSize(s) = getSize(t)
- */
+ * and z_i = 0 with getSize(z_i) = i */
NodeBuilder<> nb(nm, OR);
nb << nm->mkNode(EQUAL, t, s);
for (unsigned i = 1; i < w; ++i)
{
/* s >> x != t
* with side condition:
- * s != 0 || t != 0 */
+ * (or (distinct s z) (distinct t z))
+ * where
+ * z = 0 with getSize(z) = w */
scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
}
}
{
/* x >> s < t
* with side condition (synthesized):
- * (not (= z t)) */
+ * (distinct t z)
+ * where
+ * z = 0 with getSize(z) = w */
scl = t.eqNode(z).notNode();
}
else
{
/* x >> s >= t
* with side condition (synthesized):
- * (= (bvlshr (bvshl t s) s) t) */
+ * (= (bvlshr (bvshl t s) s) t) */
Node ts = nm->mkNode(BITVECTOR_SHL, t, s);
scl = nm->mkNode(BITVECTOR_LSHR, ts, s).eqNode(t);
}
}
- else /* litk == BITVECTOR_SLT */
+ else
{
if (pol)
{
/* s >> x < t
* with side condition (synthesized):
- * (not (= z t)) */
+ * (distinct t z)
+ * where
+ * z = 0 with getSize(z) = w */
scl = t.eqNode(z).notNode();
}
else
{
/* s >> x >= t
* with side condition (synthesized):
- * (bvuge s t) */
+ * (bvuge s t) */
scl = nm->mkNode(BITVECTOR_UGE, s, t);
}
}
{
/* x >> s > t
* with side condition (synthesized):
- * (bvult t (bvlshr (bvnot s) s)) */
+ * (bvult t (bvlshr (bvnot s) s)) */
Node lshr = nm->mkNode(BITVECTOR_LSHR, nm->mkNode(BITVECTOR_NOT, s), s);
scl = nm->mkNode(BITVECTOR_ULT, t, lshr);
}
{
/* x >> s <= t
* with side condition:
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* s >> x > t
* with side condition (synthesized):
- * (bvult t s)
- */
+ * (bvult t s) */
scl = nm->mkNode(BITVECTOR_ULT, t, s);
}
else
{
/* s >> x <= t
* with side condition:
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* x >> s < t
* with side condition (synthesized):
- * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */
+ * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */
Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t));
Node lshr = nm->mkNode(BITVECTOR_LSHR, nnt, s);
scl = nm->mkNode(BITVECTOR_SLT, lshr, t);
/* x >> s >= t
* with side condition:
* (=> (not (= s z)) (bvsge (bvlshr ones s) t))
- * where ones = ~0 with getSize(ones) = w */
+ * where
+ * z = 0 with getSize(z) = w
+ * and ones = ~0 with getSize(ones) = w */
Node ones = bv::utils::mkOnes(w);
Node lshr = nm->mkNode(BITVECTOR_LSHR, ones, s);
Node nz = s.eqNode(z).notNode();
{
/* s >> x < t
* with side condition (synthesized):
- * (or (bvslt s t) (bvslt z t)) */
+ * (or (bvslt s t) (bvslt z t))
+ * where
+ * z = 0 with getSize(z) = w */
Node st = nm->mkNode(BITVECTOR_SLT, s, t);
Node zt = nm->mkNode(BITVECTOR_SLT, z, t);
scl = st.orNode(zt);
/* s >> x >= t
* with side condition:
* (and
- * (=> (bvslt s z) (bvsge (bvlshr s one) t))
- * (=> (bvsge s z) (bvsge s t))
- * ) */
+ * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))
+ * (=> (bvsge s z) (bvsge s t)))
+ * where
+ * z = 0 with getSize(z) = w */
Node one = bv::utils::mkConst(w, 1);
Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one);
{
/* x >> s <= t
* with side condition (synthesized):
- * (bvsge t (bvlshr t s)) */
+ * (bvsge t (bvlshr t s)) */
scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_LSHR, t, s));
}
}
/* s >> x > t
* with side condition:
* (and
- * (=> (bvslt s z) (bvsgt (bvlshr s one)) t))
- * (=> (bvsge s z) (bvsgt s t))) */
+ * (=> (bvslt s z) (bvsgt (bvlshr s one) t))
+ * (=> (bvsge s z) (bvsgt s t)))
+ * where
+ * z = 0 and getSize(z) = w */
Node one = bv::utils::mkOne(w);
Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one);
{
/* 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 */
-
+ * (or
+ * (= s z)
+ * (and
+ * (bvult s w)
+ * (or
+ * (= ((_ extract 2*w-1 w-1) (bvshl (concat z t) (concat z s))) z)
+ * (= ((_ extract 2*w-1 w-1)
+ * (bvshl (concat ones t) (concat z s))) ones)))
+ * (and (bvuge s w) (or (= t z) (= t ones))))
+ * where
+ * z = 0 with getSize(z) = w
+ * and ones = ~0 with getSize(ones) = w
+ * and w = getSize(t) = getSize(s) */
Node zz = bv::utils::mkZero(w+1);
Node nn = bv::utils::mkOnes(w+1);
Node ww = bv::utils::mkConst(w, w);
else
{
/* x >> s != t
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
- else /* litk == BITVECTOR_SLT */
+ else
{
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)))
+ * (or
+ * (and (= ((_ extract w-1 w-1) s) (_ bv0 1)) (= t z))
+ * (and (= ((_ extract w-1 w-1) s) (_ bv0 1)) (= t ones))
+ * (= s t)
+ * (and
+ * (= ((_ extract w-1-i 0) t) ((_ extract w-1 i) s))
+ * (or
+ * (and
+ * (= ((_ extract w-1 w-1) s) (_ bv0 1))
+ * (= ((_ extract w-1 w-i) t) (_ bv0 i)))
+ * (and
+ * (= ((_ extract w-1 w-1) s) (_ bv1 1))
+ * (= ((_ extract w-1 w-i) t) ones_i)))))
* for 0 < i < w
* where
- * w = getSize(s) = getSize(t)
- */
+ * z = 0 and getSize(z) = w
+ * and ones = ~0 and getSize(ones) = w
+ * and ones_i = ~0 and getSize(ones_i) = i
+ * and 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(
* with side condition:
* (and
* (or (not (= t z)) (not (= s z)))
- * (or (not (= t (bvnot z)) (not (= s (bvnot z))))))
- */
+ * (or (not (= t ones)) (not (= s ones))))
+ * where
+ * z = 0 with getSize(z) = w
+ * and ones = ~0 with getSize(ones) = w */
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()));
{
/* x >> s < t
* with side condition (synthesized):
- * (not (= t z)) */
+ * (distinct t z)
+ * where
+ * z = 0 with getSize(z) = w */
scl = t.eqNode(z).notNode();
}
else
{
/* x >> s >= t
* with side condition (synthesized):
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* s >> x < t
* with side condition (synthesized):
- * (and (not (and (not (bvult s t)) (bvslt s z))) (not (= t z))) */
+ * (and (not (and (bvuge s t) (bvslt s z))) (not (= t z)))
+ * where
+ * z = 0 with getSize(z) = w */
Node st = nm->mkNode(BITVECTOR_UGE, s, t);
Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
Node tz = t.eqNode(z).notNode();
}
else
{
- /* s >> x < t
+ /* s >> x >= t
* with side condition (synthesized):
- * (not (and (bvult s (bvnot s)) (bvult s t))) */
+ * (not (and (bvult s (bvnot s)) (bvult s t))) */
Node ss = nm->mkNode(BITVECTOR_ULT, s, nm->mkNode(BITVECTOR_NOT, s));
Node st = nm->mkNode(BITVECTOR_ULT, s, t);
scl = ss.andNode(st).notNode();
{
/* x >> s > t
* with side condition (synthesized):
- * (bvult t (bvnot #x0))
- */
+ * (bvult t ones)
+ * where
+ * ones = ~0 with getSize(ones) = w */
scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w));
}
else
{
/* x >> s <= t
* with side condition (synthesized):
- * true (no side condition)
- */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* s >> x > t
* with side condition (synthesized):
- * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s))
- */
+ * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s)) */
Node lshr = nm->mkNode(BITVECTOR_LSHR, s, nm->mkNode(BITVECTOR_NOT, t));
Node ts = nm->mkNode(BITVECTOR_ULT, t, s);
Node slt = nm->mkNode(BITVECTOR_SLT, s, lshr);
* with side condition:
* (bvsge (bvlshr max s) t)
* where
- * max is the signed maximum value with getSize(max) = w */
+ * max is the signed maximum value with getSize(max) = w */
BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
BitVector bv_max_val = BitVector(1).concat(bv_ones);
Node max = bv::utils::mkConst(bv_max_val);
{
/* s >> x < t
* with side condition (synthesized):
- * (or (bvslt s t) (bvslt z t)) */
+ * (or (bvslt s t) (bvslt z t))
+ * where
+ * z = 0 and getSize(z) = w */
Node st = nm->mkNode(BITVECTOR_SLT, s, t);
Node zt = nm->mkNode(BITVECTOR_SLT, z, t);
scl = st.orNode(zt);
{
/* s >> x >= t
* with side condition (synthesized):
- * (not (and (bvult t (bvnot t)) (bvslt s t))) */
+ * (not (and (bvult t (bvnot t)) (bvslt s t))) */
Node tt = nm->mkNode(BITVECTOR_ULT, t, nm->mkNode(BITVECTOR_NOT, t));
Node st = nm->mkNode(BITVECTOR_SLT, s, t);
scl = tt.andNode(st).notNode();
* with side condition (synthesized):
* (bvsge t (bvnot (bvlshr max s)))
* where
- * max is the signed maximum value with getSize(max) = w */
+ * max is the signed maximum value with getSize(max) = w */
scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, lshr));
}
}
{
/* s >> x <= t
* with side condition (synthesized):
- * (not (and (bvslt t z) (bvslt t s)))
* (or (bvsge t z) (bvsge t s))
- */
+ * where
+ * z = 0 and getSize(z) = w */
Node tz = nm->mkNode(BITVECTOR_SGE, t, z);
Node ts = nm->mkNode(BITVECTOR_SGE, t, s);
scl = tz.orNode(ts);
* 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)
+ * (or
+ * (= s z)
+ * (and
+ * (bvult s w)
+ * (= ((_ extract w-1 0) (bvlshr (concat t z) (concat z s))) z))
+ * (and (bvuge s w) (= t z)))
*
* where
- * w = getSize(s) = getSize(t) = getSize (z) && z = 0
- */
+ * w = getSize(s) = getSize(t) = getSize(z) and z = 0 */
Node shr = nm->mkNode(BITVECTOR_LSHR,
bv::utils::mkConcat(t, z),
bv::utils::mkConcat(z, s));
{
/* x << s != t
* with side condition:
- * t != 0 || s < w
+ * (or (distinct t z) (bvult s w))
* with
* w = getSize(s) = getSize(t)
- */
+ * and z = 0 with getSize(z) = w */
scl = nm->mkNode(OR,
t.eqNode(z).notNode(),
nm->mkNode(BITVECTOR_ULT, s, ww));
{
/* 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
+ * (or
+ * (= t z)
+ * (= s z)
+ * (and
+ * (= ((_ extract w-1 i) t) ((_ extract w-1-i 0)))
+ * (= ((_ extract i-1 0) t) z_i)))
+ * for 0 < i < w
* where
* w = getSize(s) = getSize(t)
- */
+ * and z = 0 with getSize(z) = w
+ * and z_i = 0 with getSize(z_i) = i */
NodeBuilder<> nb(nm, OR);
nb << nm->mkNode(EQUAL, t, s);
for (unsigned i = 1; i < w; ++i)
{
/* s << x != t
* with side condition:
- * s != 0 || t != 0 */
+ * (or (distinct s z) (distinct t z))
+ * where
+ * z = 0 with getSize(z) = w */
scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
}
}
{
/* x << s < t
* with side condition (synthesized):
- * (not (= t z)) */
+ * (not (= t z)) */
scl = t.eqNode(z).notNode();
}
else
{
/* x << s >= t
* with side condition (synthesized):
- * (bvuge (bvshl ones s) t) */
+ * (bvuge (bvshl ones s) t) */
Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s);
scl = nm->mkNode(BITVECTOR_UGE, shl, t);
}
{
/* s << x < t
* with side condition (synthesized):
- * (not (= t z)) */
+ * (not (= t z)) */
scl = t.eqNode(z).notNode();
}
else
/* s << x >= t
* with side condition:
* (or (bvuge (bvshl s i) t) ...)
- * for i in 0..w-1 */
+ * for i in 0..w-1 */
scl = naiveShlSc1(BITVECTOR_UGE, s, t);
}
}
{
/* x << s > t
* with side condition (synthesized):
- * (bvult t (bvshl ones s)) */
+ * (bvult t (bvshl ones s))
+ * where
+ * ones = ~0 with getSize(ones) = w */
Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s);
scl = nm->mkNode(BITVECTOR_ULT, t, shl);
}
{
/* x << s <= t
* with side condition:
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
/* s << x > t
* with side condition:
* (or (bvugt (bvshl s i) t) ...)
- * for i in 0..w-1 */
+ * for i in 0..w-1 */
scl = naiveShlSc1(BITVECTOR_UGT, s, t);
}
else
{
/* s << x <= t
* with side condition:
- * true (no side condition) */
+ * true (no side condition) */
scl = nm->mkConst<bool>(true);
}
}
{
/* x << s < t
* with side condition (synthesized):
- * (bvslt (bvshl (bvlshr min_val s) s) t)
+ * (bvslt (bvshl (bvlshr min s) s) t)
* where
- * min_val is the signed minimum value */
+ * min is the signed minimum value with getSize(min) = w */
BitVector bv_min_val = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min_val);
Node lshr = nm->mkNode(BITVECTOR_LSHR, min, s);
{
/* x << s >= t
* with side condition (synthesized):
- * (bvsge (bvand (bvshl max_val s) max_val) t)
+ * (bvsge (bvand (bvshl max s) max) t)
* where
- * max_val is the signed maximum value */
+ * max is the signed maximum value with getSize(max) = w */
BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
BitVector bv_max_val = BitVector(1).concat(bv_ones);
Node max = bv::utils::mkConst(bv_max_val);
{
/* s << x < t
* with side condition (synthesized):
- * (bvult (bvshl min_val s) (bvadd t min_val))
+ * (bvult (bvshl min s) (bvadd t min))
* where
- * min_val is the signed minimum value */
+ * min is the signed minimum value with getSize(min) = w */
BitVector bv_min_val = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min_val);
Node shl = nm->mkNode(BITVECTOR_SHL, min, s);
/* s << x >= t
* with side condition:
* (or (bvsge (bvshl s i) t) ...)
- * for i in 0..w-1 */
+ * for i in 0..w-1 */
scl = naiveShlSc1(BITVECTOR_SGE, s, t);
}
}
{
/* x << s > t
* with side condition (synthesized):
- * (bvslt t (bvand (bvshl max_val s) max_val))
+ * (bvslt t (bvand (bvshl max s) max))
* where
- * max_val is the signed maximum value */
+ * max is the signed maximum value with getSize(max) = w */
BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
BitVector bv_max_val = BitVector(1).concat(bv_ones);
Node max = bv::utils::mkConst(bv_max_val);
{
/* x << s <= t
* with side condition (synthesized):
- * (bvult (bvlshr t (bvlshr t s)) min_val)
+ * (bvult (bvlshr t (bvlshr t s)) min)
* where
- * min_val is the signed minimum value */
+ * min is the signed minimum value with getSize(min) = w */
BitVector bv_min_val = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min_val);
Node ts = nm->mkNode(BITVECTOR_LSHR, t, s);
/* s << x > t
* with side condition:
* (or (bvsgt (bvshl s i) t) ...)
- * for i in 0..w-1 */
+ * for i in 0..w-1 */
scl = naiveShlSc1(BITVECTOR_SGT, s, t);
}
else
{
/* s << x <= t
* with side condition (synthesized):
- * (bvult (bvlshr t s) min_val)
+ * (bvult (bvlshr t s) min)
* where
- * min_val is the signed minimum value */
+ * min is the signed minimum value with getSize(min) = w */
BitVector bv_min_val = BitVector(w).setBit(w - 1);
Node min = bv::utils::mkConst(bv_min_val);
scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, s), min);
/* x = t[upper:lower]
* where
* upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
- * lower = getSize(sv_t[i]) for i > index
- */
+ * lower = getSize(sv_t[i]) for i > index */
unsigned upper, lower;
upper = bv::utils::getSize(t) - 1;
lower = 0;
<< " for bit-vector term " << sv_t << std::endl;
return Node::null();
}
- Assert (litk != EQUAL || !sc.isNull());
- /* No specific handling for litk and operator k, generate generic
- * side condition. */
- if (sc.isNull())
- {
- solve_tn = sv_t.getType();
- if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
- {
- sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t);
- }
- else
- {
- Assert (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT);
- sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t);
- }
- }
+ Assert(!sc.isNull());
/* 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.,
projects / cvc5.git / commitdiff