}
}
}
-
+
if (c.isNull())
{
NodeManager* nm = NodeManager::currentNM();
static Node dropChild(Node n, unsigned index)
{
unsigned nchildren = n.getNumChildren();
+ Assert(nchildren > 0);
Assert(index < nchildren);
+
+ if (nchildren < 2) return Node::null();
+
Kind k = n.getKind();
- Assert(k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_MULT
- || k == BITVECTOR_PLUS);
- NodeBuilder<> nb(NodeManager::currentNM(), k);
+ NodeBuilder<> nb(k);
for (unsigned i = 0; i < nchildren; ++i)
{
if (i == index) continue;
nb << n[i];
}
- return nb.constructNode();
+ Assert(nb.getNumChildren() > 0);
+ return nb.getNumChildren() == 1 ? nb[0] : nb.constructNode();
}
static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t)
if (pol == true)
{
/* x < t
- * with side condition:
+ * with invertibility condition:
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* x >= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
if (pol == true)
{
/* x > t
- * with side condition:
+ * with invertibility condition:
* (distinct t ones)
* where
* ones = ~0 with getSize(ones) = w */
else
{
/* x <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
if (pol == true)
{
/* x < t
- * with side condition:
+ * with invertibility condition:
* (distinct t min)
* where
* min is the minimum signed value with getSize(min) = w */
else
{
/* x >= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
if (pol == true)
{
/* x > t
- * with side condition:
+ * with invertibility condition:
* (distinct t max)
* where
* max is the signed maximum value with getSize(max) = w */
else
{
/* x <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
}
}
if (pol)
{
/* x * s = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvand (bvor (bvneg s) s) t) t)
*
* is equivalent to:
else
{
/* x * s != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct t z) (distinct s z))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x * s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* x * s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
if (pol)
{
/* x * s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t (bvor (bvneg s) s)) */
Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
scl = nm->mkNode(BITVECTOR_ULT, t, o);
else
{
/* x * s <= t
- * true (no side condition) */
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* x * s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt (bvand (bvnot (bvneg t)) (bvor (bvneg s) s)) t) */
Node a1 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t));
Node a2 = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
else
{
/* x * s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge (bvand (bvor (bvneg s) s) max) t)
* where
* max is the signed maximum value with getSize(max) = w */
scl = nm->mkNode(BITVECTOR_SGE, a, t);
}
}
- else /* litk == BITVECTOR_SGT */
+ else
{
+ Assert(litk == BITVECTOR_SGT);
if (pol)
{
/* x * s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt t (bvsub t (bvor (bvor s t) (bvneg s)))) */
Node o = nm->mkNode(BITVECTOR_OR,
nm->mkNode(BITVECTOR_OR, s, t), nm->mkNode(BITVECTOR_NEG, s));
else
{
/* x * s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (not (and (= s z) (bvslt t s)))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x % s = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge (bvnot (bvneg s)) t) */
Node neg = nm->mkNode(BITVECTOR_NEG, s);
scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
else
{
/* x % s != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s (_ bv1 w)) (distinct t z))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* s % x = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge (bvand (bvsub (bvadd t t) s) s) t)
*
* is equivalent to:
else
{
/* s % x != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s z) (distinct t z))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x % s < t
- * with side condition:
+ * with invertibility condition:
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* x % s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge (bvnot (bvneg s)) t) */
Node neg = nm->mkNode(BITVECTOR_NEG, s);
scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
if (pol)
{
/* s % x < t
- * with side condition:
+ * with invertibility condition:
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* s % x >= t
- * with side condition (combination of = and >):
+ * with invertibility condition (combination of = and >):
* (or
* (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized
* (bvult t s)) ; ugt, synthesized */
if (pol)
{
/* x % s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t (bvnot (bvneg s))) */
Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s));
scl = nm->mkNode(BITVECTOR_ULT, t, nt);
else
{
/* x % s <= t
- * true (no side condition) */
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s % x > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t s) */
scl = nm->mkNode(BITVECTOR_ULT, t, s);
}
else
{
/* s % x <= t
- * true (no side condition) */
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* x % s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt (bvnot t) (bvor (bvneg s) (bvneg t))) */
Node o1 = nm->mkNode(BITVECTOR_NEG, s);
Node o2 = nm->mkNode(BITVECTOR_NEG, t);
else
{
/* x % s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvslt t s) (bvsge z s))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* s % x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvslt s t) (bvslt z t))
* where
* z = 0 with getSize(z) = w */
else
{
/* s % x >= t
- * with side condition:
+ * with invertibility condition:
* (and
* (=> (bvsge s z) (bvsge s t))
* (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
}
}
}
- else /* litk == BITVECTOR_SGT */
+ else
{
+ Assert(litk == BITVECTOR_SGT);
if (idx == 0)
{
Node z = bv::utils::mkZero(w);
if (pol)
{
/* x % s > t
- * with side condition:
+ * with invertibility condition:
*
* (and
* (and
else
{
/* x % s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt ones (bvand (bvneg s) t))
* where
* z = 0 with getSize(z) = w
if (pol)
{
/* s % x > t
- * with side condition:
+ * with invertibility condition:
* (and
* (=> (bvsge s z) (bvsgt s t))
* (=> (bvslt s z)
else
{
/* s % x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvult t min) (bvsge t s))
* where
* min is the minimum signed value with getSize(min) = w */
if (pol)
{
/* x udiv s = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvudiv (bvmul s t) s) t)
*
* is equivalent to:
else
{
/* x udiv s != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s z) (distinct t ones))
* where
* z = 0 with getSize(z) = w
if (pol)
{
/* s udiv x = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvudiv s (bvudiv s t)) t)
*
* is equivalent to:
else
{
/* s udiv x != t
- * with side condition (w > 1):
- * true (no side condition)
+ * with invertibility condition (w > 1):
+ * true (no invertibility condition)
*
- * with side condition (w == 1):
+ * with invertibility condition (w == 1):
* (= (bvand s t) z)
*
* where
if (pol)
{
/* x udiv s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (and (bvult z s) (bvult z t))
* where
* z = 0 with getSize(z) = w */
else
{
/* x udiv s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvand (bvudiv (bvmul s t) t) s) s) */
Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, t);
if (pol)
{
/* s udiv x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t))
* where
* z = 0 with getSize(z) = w */
else
{
/* s udiv x >= t
- * true (no side condition) */
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* x udiv s > t
- * with side condition:
+ * with invertibility condition:
* (bvugt (bvudiv ones s) t)
* where
* ones = ~0 with getSize(ones) = w */
else
{
/* x udiv s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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));
if (pol)
{
/* s udiv x > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t ones)
* where
* ones = ~0 with getSize(ones) = w */
else
{
/* s udiv x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult z (bvor (bvnot s) t))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x udiv s < t
- * with side condition:
+ * with invertibility condition:
* (=> (bvsle t z) (bvslt (bvudiv min s) t))
* where
* z = 0 with getSize(z) = w
else
{
/* x udiv s >= t
- * with side condition:
+ * with invertibility condition:
* (or
* (bvsge (bvudiv ones s) t)
* (bvsge (bvudiv max s) t))
if (pol)
{
/* s udiv x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvslt s t) (bvsge t z))
* where
* z = 0 with getSize(z) = w */
else
{
/* s udiv x >= t
- * with side condition (w > 1):
+ * with invertibility condition (w > 1):
* (and
* (=> (bvsge s z) (bvsge s t))
* (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t)))
*
- * with side condition (w == 1):
+ * with invertibility condition (w == 1):
* (bvsge s t)
*
* where
}
}
}
- else /* litk == BITVECTOR_SGT */
+ else
{
+ Assert(litk == BITVECTOR_SGT);
if (idx == 0)
{
if (pol)
{
/* x udiv s > t
- * with side condition:
+ * with invertibility condition:
* (or
* (bvsgt (bvudiv ones s) t)
* (bvsgt (bvudiv max s) t))
else
{
/* x udiv s <= t
- * with side condition (combination of = and <):
+ * with invertibility condition (combination of = and <):
* (or
* (= (bvudiv (bvmul s t) s) t) ; eq, synthesized
* (=> (bvsle t z) (bvslt (bvudiv min s) t))) ; slt
if (pol)
{
/* s udiv x > t
- * with side condition (w > 1):
+ * with invertibility condition (w > 1):
* (and
* (=> (bvsge s z) (bvsgt s t))
* (=> (bvslt s z) (bvsgt (bvlshr s (_ bv1 w)) t)))
*
- * with side condition (w == 1):
+ * with invertibility condition (w == 1):
* (bvsgt s t)
*
* where
else
{
/* s udiv x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (not (and (bvslt t (bvnot #x0)) (bvslt t s)))
* <->
* (or (bvsge t ones) (bvsge t s))
{
/* x & s = t
* x | s = t
- * with side condition:
+ * with invertibility condition:
* (= (bvand t s) t)
* (= (bvor t s) t) */
scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
if (k == BITVECTOR_AND)
{
/* x & s = t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s z) (distinct t z))
* where
* z = 0 with getSize(z) = w */
else
{
/* x | s = t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s ones) (distinct t ones))
* where
* ones = ~0 with getSize(ones) = w */
if (k == BITVECTOR_AND)
{
/* x & s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (distinct t z)
* where
* z = 0 with getSize(z) = 0 */
else
{
/* x | s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult s t) */
scl = nm->mkNode(BITVECTOR_ULT, s, t);
}
if (k == BITVECTOR_AND)
{
/* x & s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge s t) */
scl = nm->mkNode(BITVECTOR_UGE, s, t);
}
else
{
/* x | s >= t
- * with side condition (synthesized):
- * true (no side condition) */
+ * with invertibility condition (synthesized):
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (k == BITVECTOR_AND)
{
/* x & s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t s) */
scl = nm->mkNode(BITVECTOR_ULT, t, s);
}
else
{
/* x | s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t ones)
* where
* ones = ~0 with getSize(ones) = w */
if (k == BITVECTOR_AND)
{
/* x & s <= t
- * with side condition (synthesized):
- * true (no side condition) */
+ * with invertibility condition (synthesized):
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
else
{
/* x | s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge t s) */
scl = nm->mkNode(BITVECTOR_UGE, t, s);
}
if (k == BITVECTOR_AND)
{
/* x & s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
else
{
/* x | s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
if (k == BITVECTOR_AND)
{
/* x & s >= t
- * with side condition (case = combined with synthesized bvsgt):
+ * with invertibility condition (case = combined with synthesized bvsgt):
* (or
* (= (bvand s t) t)
* (bvslt t (bvand (bvsub t s) s))) */
else
{
/* x | s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge s (bvand s t)) */
scl = nm->mkNode(BITVECTOR_SGE, s, nm->mkNode(BITVECTOR_AND, s, t));
}
{
/* x & s > t
* x | s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt t (bvand s max))
* (bvslt t (bvor s max))
* where
if (k == BITVECTOR_AND)
{
/* x & s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge s (bvand t min))
* where
* min is the signed minimum value with getSize(min) = w */
else
{
/* x | s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge t (bvor s min))
* where
* min is the signed minimum value with getSize(min) = w */
if (pol)
{
/* x >> s = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvlshr (bvshl t s) s) t) */
Node shl = nm->mkNode(BITVECTOR_SHL, t, s);
Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s);
else
{
/* x >> s != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct t z) (bvult s w))
* where
* z = 0 with getSize(z) = w
if (pol)
{
/* s >> x = t
- * with side condition:
+ * with invertibility condition:
* (or (= (bvlshr s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(EQUAL, BITVECTOR_LSHR, s, t);
else
{
/* s >> x != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s z) (distinct t z))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x >> s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* x >> s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvlshr (bvshl t s) s) t) */
Node ts = nm->mkNode(BITVECTOR_SHL, t, s);
scl = nm->mkNode(BITVECTOR_LSHR, ts, s).eqNode(t);
if (pol)
{
/* s >> x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* s >> x >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge s t) */
scl = nm->mkNode(BITVECTOR_UGE, s, t);
}
if (pol)
{
/* x >> s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
else
{
/* x >> s <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s >> x > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t s) */
scl = nm->mkNode(BITVECTOR_ULT, t, s);
}
else
{
/* s >> x <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* x >> s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
else
{
/* x >> s >= t
- * with side condition:
+ * with invertibility condition:
* (=> (not (= s z)) (bvsge (bvlshr ones s) t))
* where
* z = 0 with getSize(z) = w
if (pol)
{
/* s >> x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvslt s t) (bvslt z t))
* where
* z = 0 with getSize(z) = w */
else
{
/* s >> x >= t
- * with side condition:
+ * with invertibility condition:
* (and
* (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))
* (=> (bvsge s z) (bvsge s t)))
if (pol)
{
/* x >> s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt t (bvlshr (bvshl max s) s))
* where
* max is the signed maximum value with getSize(max) = w */
else
{
/* x >> s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge t (bvlshr t s)) */
scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_LSHR, t, s));
}
if (pol)
{
/* s >> x > t
- * with side condition:
+ * with invertibility condition:
* (and
* (=> (bvslt s z) (bvsgt (bvlshr s one) t))
* (=> (bvsge s z) (bvsgt s t)))
else
{
/* s >> x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvult t min) (bvsge t s))
* where
* min is the minimum signed value with getSize(min) = w */
if (pol)
{
/* x >> s = t
- * with side condition:
+ * with invertibility condition:
* (and
* (=> (bvult s w) (= (bvashr (bvshl t s) s) t))
* (=> (bvuge s w) (or (= t ones) (= t z)))
else
{
/* x >> s != t
- * true (no side condition) */
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s >> x = t
- * with side condition:
+ * with invertibility condition:
* (or (= (bvashr s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(EQUAL, BITVECTOR_ASHR, s, t);
else
{
/* s >> x != t
- * with side condition:
+ * with invertibility condition:
* (and
* (or (not (= t z)) (not (= s z)))
* (or (not (= t ones)) (not (= s ones))))
if (pol)
{
/* x >> s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (distinct t z)
* where
* z = 0 with getSize(z) = w */
else
{
/* x >> s >= t
- * with side condition (synthesized):
- * true (no side condition) */
+ * with invertibility condition (synthesized):
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s >> x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (and (not (and (bvuge s t) (bvslt s z))) (not (= t z)))
* where
* z = 0 with getSize(z) = w */
else
{
/* s >> x >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
if (pol)
{
/* x >> s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t ones)
* where
* ones = ~0 with getSize(ones) = w */
else
{
/* x >> s <= t
- * with side condition (synthesized):
- * true (no side condition) */
+ * with invertibility condition (synthesized):
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s >> x > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
else
{
/* s >> x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvult s min) (bvuge t s))
* where
* min is the minimum signed value with getSize(min) = w */
if (pol)
{
/* x >> s < t
- * with side condition:
+ * with invertibility condition:
* (bvslt (bvashr min s) t)
* where
* min is the minimum signed value with getSize(min) = w */
else
{
/* x >> s >= t
- * with side condition:
+ * with invertibility condition:
* (bvsge (bvlshr max s) t)
* where
* max is the signed maximum value with getSize(max) = w */
if (pol)
{
/* s >> x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvslt s t) (bvslt z t))
* where
* z = 0 and getSize(z) = w */
else
{
/* s >> x >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (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);
if (pol)
{
/* x >> s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt t (bvlshr max s)))
* where
* max is the signed maximum value with getSize(max) = w */
else
{
/* x >> s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge t (bvnot (bvlshr max s)))
* where
* max is the signed maximum value with getSize(max) = w */
if (pol)
{
/* s >> x > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (and (bvslt t (bvand s max)) (bvslt t (bvor s max)))
* where
* max is the signed maximum value with getSize(max) = w */
else
{
/* s >> x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (or (bvsge t z) (bvsge t s))
* where
* z = 0 and getSize(z) = w */
if (pol)
{
/* x << s = t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (= (bvshl (bvlshr t s) s) t) */
Node lshr = nm->mkNode(BITVECTOR_LSHR, t, s);
Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s);
else
{
/* x << s != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct t z) (bvult s w))
* with
* w = getSize(s) = getSize(t)
if (pol)
{
/* s << x = t
- * with side condition:
+ * with invertibility condition:
* (or (= (bvshl s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(EQUAL, BITVECTOR_SHL, s, t);
else
{
/* s << x != t
- * with side condition:
+ * with invertibility condition:
* (or (distinct s z) (distinct t z))
* where
* z = 0 with getSize(z) = w */
if (pol)
{
/* x << s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (not (= t z)) */
scl = t.eqNode(z).notNode();
}
else
{
/* x << s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvuge (bvshl ones s) t) */
Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s);
scl = nm->mkNode(BITVECTOR_UGE, shl, t);
if (pol)
{
/* s << x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (not (= t z)) */
scl = t.eqNode(z).notNode();
}
else
{
/* s << x >= t
- * with side condition:
+ * with invertibility condition:
* (or (bvuge (bvshl s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(BITVECTOR_UGE, BITVECTOR_SHL, s, t);
if (pol)
{
/* x << s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult t (bvshl ones s))
* where
* ones = ~0 with getSize(ones) = w */
else
{
/* x << s <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* s << x > t
- * with side condition:
+ * with invertibility condition:
* (or (bvugt (bvshl s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(BITVECTOR_UGT, BITVECTOR_SHL, s, t);
else
{
/* s << x <= t
- * with side condition:
- * true (no side condition) */
+ * with invertibility condition:
+ * true (no invertibility condition) */
scl = nm->mkConst<bool>(true);
}
}
if (pol)
{
/* x << s < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt (bvshl (bvlshr min s) s) t)
* where
* min is the signed minimum value with getSize(min) = w */
else
{
/* x << s >= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvsge (bvand (bvshl max s) max) t)
* where
* max is the signed maximum value with getSize(max) = w */
if (pol)
{
/* s << x < t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult (bvshl min s) (bvadd t min))
* where
* min is the signed minimum value with getSize(min) = w */
else
{
/* s << x >= t
- * with side condition:
+ * with invertibility condition:
* (or (bvsge (bvshl s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(BITVECTOR_SGE, BITVECTOR_SHL, s, t);
if (pol)
{
/* x << s > t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvslt t (bvand (bvshl max s) max))
* where
* max is the signed maximum value with getSize(max) = w */
else
{
/* x << s <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult (bvlshr t (bvlshr t s)) min)
* where
* min is the signed minimum value with getSize(min) = w */
if (pol)
{
/* s << x > t
- * with side condition:
+ * with invertibility condition:
* (or (bvsgt (bvshl s i) t) ...)
* for i in 0..w */
scl = defaultShiftSc(BITVECTOR_SGT, BITVECTOR_SHL, s, t);
else
{
/* s << x <= t
- * with side condition (synthesized):
+ * with invertibility condition (synthesized):
* (bvult (bvlshr t s) min)
* where
* min is the signed minimum value with getSize(min) = w */
return sc;
}
+static Node getScBvConcat(bool pol,
+ Kind litk,
+ unsigned idx,
+ Node x,
+ Node sv_t,
+ Node t)
+{
+ Assert(litk == EQUAL
+ || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT
+ || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
+
+ Kind k = sv_t.getKind();
+ Assert(k == BITVECTOR_CONCAT);
+ NodeManager* nm = NodeManager::currentNM();
+ unsigned nchildren = sv_t.getNumChildren();
+ unsigned w1 = 0, w2 = 0;
+ unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x);
+ NodeBuilder<> nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT);
+ Node s1, s2;
+ Node t1, t2, tx;
+ Node scl, scr;
+
+ if (idx != 0)
+ {
+ if (idx == 1)
+ {
+ s1 = sv_t[0];
+ }
+ else
+ {
+ for (unsigned i = 0; i < idx; ++i) { nbs1 << sv_t[i]; }
+ s1 = nbs1.constructNode();
+ }
+ w1 = bv::utils::getSize(s1);
+ t1 = bv::utils::mkExtract(t, w - 1, w - w1);
+ }
+
+ tx = bv::utils::mkExtract(t, w - w1 - 1 , w - w1 - wx);
+
+ if (idx != nchildren-1)
+ {
+ if (idx == nchildren-2)
+ {
+ s2 = sv_t[nchildren-1];
+ }
+ else
+ {
+ for (unsigned i = idx+1; i < nchildren; ++i) { nbs2 << sv_t[i]; }
+ s2 = nbs2.constructNode();
+ }
+ w2 = bv::utils::getSize(s2);
+ Assert(w2 == w - w1 - wx);
+ t2 = bv::utils::mkExtract(t, w2 - 1, 0);
+ }
+
+ Assert(!s1.isNull() || t1.isNull());
+ Assert(!s2.isNull() || t2.isNull());
+ Assert(!s1.isNull() || !s2.isNull());
+ Assert(s1.isNull() || w1 == bv::utils::getSize(t1));
+ Assert(s2.isNull() || w2 == bv::utils::getSize(t2));
+
+ if (litk == EQUAL)
+ {
+ if (s1.isNull())
+ {
+ if (pol)
+ {
+ /* x o s2 = t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (= s2 t2) */
+ scl = s2.eqNode(t2);
+ }
+ else
+ {
+ /* x o s2 != t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ else if (s2.isNull())
+ {
+ if (pol)
+ {
+ /* s1 o x = t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (= s1 t1) */
+ scl = s1.eqNode(t1);
+ }
+ else
+ {
+ /* s1 o x != t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ else
+ {
+ if (pol)
+ {
+ /* s1 o x o s2 = t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and (= s1 t1) (= s2 t2)) */
+ scl = nm->mkNode(AND, s1.eqNode(t1), s2.eqNode(t2));
+ }
+ else
+ {
+ /* s1 o x o s2 != t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ }
+ else if (litk == BITVECTOR_ULT)
+ {
+ if (s1.isNull())
+ {
+ if (pol)
+ {
+ /* x o s2 < t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx z) (bvult s2 t2))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(z), ult);
+ }
+ else
+ {
+ /* x o s2 >= t (interpret t as tx o t2)
+ * (=> (= tx ones) (bvuge s2 t2))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(n), uge);
+ }
+ }
+ else if (s2.isNull())
+ {
+ if (pol)
+ {
+ /* s1 o x < t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (and (bvule s1 t1) (=> (= s1 t1) (distinct tx z)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1);
+ Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode());
+ scl = nm->mkNode(AND, ule, imp);
+ }
+ else
+ {
+ /* s1 o x >= t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (bvuge s1 t1) */
+ scl = nm->mkNode(BITVECTOR_UGE, s1, t1);
+ }
+ }
+ else
+ {
+ if (pol)
+ {
+ /* s1 o x o s2 < t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvule s1 t1)
+ * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2));
+ scl = nm->mkNode(AND, ule, imp);
+ }
+ else
+ {
+ /* s1 o x o s2 >= t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvuge s1 t1)
+ * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2));
+ scl = nm->mkNode(AND, uge, imp);
+ }
+ }
+ }
+ else if (litk == BITVECTOR_UGT)
+ {
+ if (s1.isNull())
+ {
+ if (pol)
+ {
+ /* x o s2 > t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx ones) (bvugt s2 t2))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(n), ugt);
+ }
+ else
+ {
+ /* x o s2 <= t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx z) (bvule s2 t2))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(z), ule);
+ }
+ }
+ else if (s2.isNull())
+ {
+ if (pol)
+ {
+ /* s1 o x > t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (and (bvuge s1 t1) (=> (= s1 t1) (distinct tx ones)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1);
+ Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode());
+ scl = nm->mkNode(AND, uge, imp);
+ }
+ else
+ {
+ /* s1 o x <= t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (bvule s1 t1) */
+ scl = nm->mkNode(BITVECTOR_ULE, s1, t1);
+ }
+ }
+ else
+ {
+ if (pol)
+ {
+ /* s1 o x o s2 > t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvuge s1 t1)
+ * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2));
+ scl = nm->mkNode(AND, uge, imp);
+ }
+ else
+ {
+ /* s1 o x o s2 <= t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvule s1 t1)
+ * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2));
+ scl = nm->mkNode(AND, ule, imp);
+ }
+ }
+ }
+ else if (litk == BITVECTOR_SLT)
+ {
+ if (s1.isNull())
+ {
+ if (pol)
+ {
+ /* x o s2 < t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx min) (bvult s2 t2))
+ * where
+ * min is the signed minimum value with getSize(min) = wx */
+ Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(wx));
+ Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(min), ult);
+ }
+ else
+ {
+ /* x o s2 >= t (interpret t as tx o t2)
+ * (=> (= tx max) (bvuge s2 t2))
+ * where
+ * max is the signed maximum value with getSize(max) = wx */
+ Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(wx));
+ Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(max), uge);
+ }
+ }
+ else if (s2.isNull())
+ {
+ if (pol)
+ {
+ /* s1 o x < t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (and (bvsle s1 t1) (=> (= s1 t1) (distinct tx z)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1);
+ Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode());
+ scl = nm->mkNode(AND, sle, imp);
+ }
+ else
+ {
+ /* s1 o x >= t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (bvsge s1 t1) */
+ scl = nm->mkNode(BITVECTOR_SGE, s1, t1);
+ }
+ }
+ else
+ {
+ if (pol)
+ {
+ /* s1 o x o s2 < t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvsle s1 t1)
+ * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2));
+ scl = nm->mkNode(AND, sle, imp);
+ }
+ else
+ {
+ /* s1 o x o s2 >= t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvsge s1 t1)
+ * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2));
+ scl = nm->mkNode(AND, sge, imp);
+ }
+ }
+ }
+ else
+ {
+ Assert(litk == BITVECTOR_SGT);
+ if (s1.isNull())
+ {
+ if (pol)
+ {
+ /* x o s2 > t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx max) (bvugt s2 t2))
+ * where
+ * max is the signed maximum value with getSize(max) = wx */
+ Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(wx));
+ Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(max), ugt);
+ }
+ else
+ {
+ /* x o s2 <= t (interpret t as tx o t2)
+ * with invertibility condition:
+ * (=> (= tx min) (bvule s2 t2))
+ * where
+ * min is the signed minimum value with getSize(min) = wx */
+ Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(wx));
+ Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2);
+ scl = nm->mkNode(IMPLIES, tx.eqNode(min), ule);
+ }
+ }
+ else if (s2.isNull())
+ {
+ if (pol)
+ {
+ /* s1 o x > t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (and (bvsge s1 t1) (=> (= s1 t1) (distinct tx ones)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1);
+ Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode());
+ scl = nm->mkNode(AND, sge, imp);
+ }
+ else
+ {
+ /* s1 o x <= t (interpret t as t1 o tx)
+ * with invertibility condition:
+ * (bvsle s1 t1) */
+ scl = nm->mkNode(BITVECTOR_SLE, s1, t1);
+ }
+ }
+ else
+ {
+ if (pol)
+ {
+ /* s1 o x o s2 > t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvsge s1 t1)
+ * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2)))
+ * where
+ * ones = ~0 with getSize(ones) = wx */
+ Node n = bv::utils::mkOnes(wx);
+ Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2));
+ scl = nm->mkNode(AND, sge, imp);
+ }
+ else
+ {
+ /* s1 o x o s2 <= t (interpret t as t1 o tx o t2)
+ * with invertibility condition:
+ * (and
+ * (bvsle s1 t1)
+ * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2)))
+ * where
+ * z = 0 with getSize(z) = wx */
+ Node z = bv::utils::mkZero(wx);
+ Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1);
+ Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z));
+ Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2));
+ scl = nm->mkNode(AND, sle, imp);
+ }
+ }
+ }
+ scr = s1.isNull() ? x : bv::utils::mkConcat(s1, x);
+ if (!s2.isNull()) scr = bv::utils::mkConcat(scr, s2);
+ scr = nm->mkNode(litk, scr, t);
+ Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode());
+ Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+ return sc;
+}
+
+static Node getScBvSext(bool pol,
+ Kind litk,
+ unsigned idx,
+ Node x,
+ Node sv_t,
+ Node t)
+{
+ Assert(litk == EQUAL
+ || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT
+ || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node scl;
+ Assert(idx == 0);
+ (void) idx;
+ unsigned ws = bv::utils::getSignExtendAmount(sv_t);
+ unsigned w = bv::utils::getSize(t);
+
+ if (litk == EQUAL)
+ {
+ if (pol)
+ {
+ /* x sext ws = t
+ * with invertibility condition:
+ * (or (= ((_ extract u l) t) z)
+ * (= ((_ extract u l) t) ones))
+ * where
+ * u = w - 1
+ * l = w - 1 - ws
+ * z = 0 with getSize(z) = ws + 1
+ * ones = ~0 with getSize(ones) = ws + 1 */
+ Node ext = bv::utils::mkExtract(t, w - 1, w - 1 - ws);
+ Node z = bv::utils::mkZero(ws + 1);
+ Node n = bv::utils::mkOnes(ws + 1);
+ scl = nm->mkNode(OR, ext.eqNode(z), ext.eqNode(n));
+ }
+ else
+ {
+ /* x sext ws != t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ else if (litk == BITVECTOR_ULT)
+ {
+ if (pol)
+ {
+ /* x sext ws < t
+ * with invertibility condition:
+ * (distinct t z)
+ * where
+ * z = 0 with getSize(z) = w */
+ Node z = bv::utils::mkZero(w);
+ scl = t.eqNode(z).notNode();
+ }
+ else
+ {
+ /* x sext ws >= t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ else if (litk == BITVECTOR_UGT)
+ {
+ if (pol)
+ {
+ /* x sext ws > t
+ * with invertibility condition:
+ * (distinct t ones)
+ * where
+ * ones = ~0 with getSize(ones) = w */
+ Node n = bv::utils::mkOnes(w);
+ scl = t.eqNode(n).notNode();
+ }
+ else
+ {
+ /* x sext ws <= t
+ * true (no invertibility condition) */
+ scl = nm->mkConst<bool>(true);
+ }
+ }
+ else if (litk == BITVECTOR_SLT)
+ {
+ if (pol)
+ {
+ /* x sext ws < t
+ * with invertibility condition:
+ * (bvslt ((_ sign_extend ws) min) t)
+ * where
+ * min is the signed minimum value with getSize(min) = w - ws */
+ Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w - ws));
+ Node ext = bv::utils::mkSignExtend(min, ws);
+ scl = nm->mkNode(BITVECTOR_SLT, ext, t);
+ }
+ else
+ {
+ /* x sext ws >= t
+ * with invertibility condition (combination of sgt and eq):
+ *
+ * (or
+ * (or (= ((_ extract u l) t) z) ; eq
+ * (= ((_ extract u l) t) ones))
+ * (bvslt t ((_ zero_extend ws) max))) ; sgt
+ * where
+ * u = w - 1
+ * l = w - 1 - ws
+ * z = 0 with getSize(z) = ws + 1
+ * ones = ~0 with getSize(ones) = ws + 1
+ * max is the signed maximum value with getSize(max) = w - ws */
+ Node ext1 = bv::utils::mkExtract(t, w - 1, w - 1 - ws);
+ Node z = bv::utils::mkZero(ws + 1);
+ Node n = bv::utils::mkOnes(ws + 1);
+ Node o1 = nm->mkNode(OR, ext1.eqNode(z), ext1.eqNode(n));
+ Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+ Node ext2 = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
+ Node o2 = nm->mkNode(BITVECTOR_SLT, t, ext2);
+ scl = nm->mkNode(OR, o1, o2);
+ }
+ }
+ else
+ {
+ Assert(litk == BITVECTOR_SGT);
+ if (pol)
+ {
+ /* x sext ws > t
+ * with invertibility condition:
+ * (bvslt t ((_ zero_extend ws) max))
+ * where
+ * max is the signed maximum value with getSize(max) = w - ws */
+ Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+ Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
+ scl = nm->mkNode(BITVECTOR_SLT, t, ext);
+ }
+ else
+ {
+ /* x sext ws <= t
+ * with invertibility condition:
+ * (bvsge t (bvnot ((_ zero_extend ws) max)))
+ * where
+ * max is the signed maximum value with getSize(max) = w - ws */
+ Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+ Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
+ scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, ext));
+ }
+ }
+ Node scr = nm->mkNode(litk, bv::utils::mkSignExtend(x, ws), t);
+ Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode());
+ Trace("bv-invert") << "Add SC_" << BITVECTOR_SIGN_EXTEND << "(" << x
+ << "): " << sc << std::endl;
+ return sc;
+}
+
Node BvInverter::solveBvLit(Node sv,
Node lit,
std::vector<unsigned>& path,
Assert(!path.empty());
bool pol = true;
- unsigned index, nchildren;
+ unsigned index;
NodeManager* nm = NodeManager::currentNM();
Kind k, litk;
while (!path.empty())
{
+ unsigned nchildren = sv_t.getNumChildren();
+ Assert(nchildren > 0);
index = path.back();
- Assert(index < sv_t.getNumChildren());
+ Assert(index < nchildren);
path.pop_back();
k = sv_t.getKind();
- nchildren = sv_t.getNumChildren();
- if (k == BITVECTOR_NOT || k == BITVECTOR_NEG)
+ /* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND,
+ * BITVECTOR_OR, MULT, PLUS) are commutative (no case split
+ * based on index). */
+ Node s = dropChild(sv_t, index);
+ Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull()));
+ TypeNode solve_tn = sv_t[index].getType();
+ Node x = getSolveVariable(solve_tn);
+ Node sc;
+
+ if (litk == EQUAL && (k == BITVECTOR_NOT || k == BITVECTOR_NEG))
{
t = nm->mkNode(k, t);
}
+ else if (litk == EQUAL && k == BITVECTOR_PLUS)
+ {
+ t = nm->mkNode(BITVECTOR_SUB, t, s);
+ }
+ else if (litk == EQUAL && k == BITVECTOR_XOR)
+ {
+ t = nm->mkNode(BITVECTOR_XOR, t, s);
+ }
+ else if (k == BITVECTOR_MULT && s.isConst() && bv::utils::getBit(s, 0))
+ {
+ unsigned w = bv::utils::getSize(s);
+ Integer s_val = s.getConst<BitVector>().toInteger();
+ Integer mod_val = Integer(1).multiplyByPow2(w);
+ Trace("bv-invert-debug")
+ << "Compute inverse : " << s_val << " " << mod_val << std::endl;
+ Integer inv_val = s_val.modInverse(mod_val);
+ Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
+ Node inv = bv::utils::mkConst(w, inv_val);
+ t = nm->mkNode(BITVECTOR_MULT, inv, t);
+ }
+ else if (k == BITVECTOR_MULT)
+ {
+ sc = getScBvMult(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_SHL)
+ {
+ sc = getScBvShl(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_UREM_TOTAL)
+ {
+ sc = getScBvUrem(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_UDIV_TOTAL)
+ {
+ sc = getScBvUdiv(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_AND || k == BITVECTOR_OR)
+ {
+ sc = getScBvAndOr(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_LSHR)
+ {
+ sc = getScBvLshr(pol, litk, k, index, x, s, t);
+ }
+ else if (k == BITVECTOR_ASHR)
+ {
+ sc = getScBvAshr(pol, litk, k, index, x, s, t);
+ }
else if (k == BITVECTOR_CONCAT)
{
- /* 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 */
- unsigned upper, lower;
- upper = bv::utils::getSize(t) - 1;
- lower = 0;
- NodeBuilder<> nb(nm, BITVECTOR_CONCAT);
- for (unsigned i = 0; i < nchildren; i++)
- {
- if (i < index) { upper -= bv::utils::getSize(sv_t[i]); }
- else if (i > index) { lower += bv::utils::getSize(sv_t[i]); }
- }
- t = bv::utils::mkExtract(t, upper, lower);
+ sc = getScBvConcat(pol, litk, index, x, sv_t, t);
}
else if (k == BITVECTOR_SIGN_EXTEND)
{
- t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index]) - 1, 0);
+ sc = getScBvSext(pol, litk, index, x, sv_t, t);
}
- else if (k == BITVECTOR_EXTRACT || k == BITVECTOR_COMP)
+ else if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
{
- Trace("bv-invert") << "bv-invert : Unsupported for index " << index
- << ", from " << sv_t << std::endl;
- return Node::null();
+ sc = getScBvUltUgt(pol, litk, x, t);
+ }
+ else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT)
+ {
+ sc = getScBvSltSgt(pol, litk, x, t);
+ }
+ else if (pol == false)
+ {
+ Assert (litk == EQUAL);
+ sc = nm->mkNode(DISTINCT, x, t);
+ Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc
+ << std::endl;
}
else
{
- Assert(nchildren >= 2);
- Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index);
- Node t_new;
- /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS)
- * are commutative (no case split based on index). */
-
- // handle cases where the inversion has a unique solution
- if (k == BITVECTOR_PLUS)
- {
- t_new = nm->mkNode(BITVECTOR_SUB, t, s);
- }
- else if (k == BITVECTOR_XOR)
- {
- t_new = nm->mkNode(BITVECTOR_XOR, t, s);
- }
- else if (k == BITVECTOR_MULT && s.isConst() && bv::utils::getBit(s, 0))
- {
- unsigned w = bv::utils::getSize(s);
- Integer s_val = s.getConst<BitVector>().toInteger();
- Integer mod_val = Integer(1).multiplyByPow2(w);
- Trace("bv-invert-debug")
- << "Compute inverse : " << s_val << " " << mod_val << std::endl;
- Integer inv_val = s_val.modInverse(mod_val);
- Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
- Node inv = bv::utils::mkConst(w, inv_val);
- t_new = nm->mkNode(BITVECTOR_MULT, inv, t);
- }
-
- if (!t_new.isNull())
- {
- // In this case, s op x = t is equivalent to x = t_new
- t = t_new;
- }
- else
- {
- TypeNode solve_tn = sv_t[index].getType();
- Node sc;
+ Trace("bv-invert") << "bv-invert : Unknown kind " << k
+ << " for bit-vector term " << sv_t << std::endl;
+ return Node::null();
+ }
- switch (k)
- {
- 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:
- 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();
- }
- 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.,
- * from here on, the propagated literal is a positive equality. */
- litk = EQUAL;
- pol = true;
- /* t = fresh skolem constant */
- t = getInversionNode(sc, solve_tn, m);
- if (t.isNull())
- {
- return t;
- }
- }
+ if (!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.,
+ * from here on, the propagated literal is a positive equality. */
+ litk = EQUAL;
+ pol = true;
+ /* t = fresh skolem constant */
+ t = getInversionNode(sc, solve_tn, m);
+ if (t.isNull()) { return t; }
}
+
sv_t = sv_t[index];
}
+
+ /* Base case */
Assert(sv_t == sv);
+ TypeNode solve_tn = sv.getType();
+ Node x = getSolveVariable(solve_tn);
+ Node sc;
if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
{
- TypeNode solve_tn = sv_t.getType();
- Node sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t);
- t = getInversionNode(sc, solve_tn, m);
+ sc = getScBvUltUgt(pol, litk, x, t);
}
else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT)
{
- TypeNode solve_tn = sv_t.getType();
- Node sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t);
- t = getInversionNode(sc, solve_tn, m);
+ sc = getScBvSltSgt(pol, litk, x, t);
}
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);
+ sc = nm->mkNode(DISTINCT, x, t);
Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc
<< std::endl;
- t = getInversionNode(sc, solve_tn, m);
}
- return t;
+
+ return sc.isNull() ? t : getInversionNode(sc, solve_tn, m);
}
/*---------------------------------------------------------------------------*/
projects / cvc5.git / commitdiff