mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

add special handling of lshr, ashr

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-02 21:08:59 -07:00
parent 918ac2b176
commit 2ce202db75
5 changed files with 376 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/bv_sls.cpp
View file

@ -203,7 +203,7 @@ namespace bv {
if (res != l_undef)
break;
trace();
res = search2();
// res = search2();
if (res != l_undef)
break;
reinit_eval();

270
src/ast/sls/bv_sls_eval.cpp
View file

@ -84,10 +84,13 @@ namespace bv {
return false;
auto v = alloc_valuation(e);
m_values.set(e->get_id(), v);
if (bv.is_sign_ext(e)) {
unsigned p = e->get_parameter(0).get_int();
v->set_signed(p);
}
expr* x, * y;
rational val;
if (bv.is_sign_ext(e))
v->set_signed(e->get_parameter(0).get_int());
else if (bv.is_bv_ashr(e, x, y) && bv.is_numeral(y, val) &&
val.is_unsigned() && val.get_unsigned() <= bv.get_bv_size(e))
v->set_signed(val.get_unsigned());
return true;
}
@ -1349,6 +1352,13 @@ namespace bv {
}
bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (true) {
if (i == 0)
return try_repair_ashr0(e, a, b);
else
return try_repair_ashr1(e, a, b);
}
if (i == 0) {
unsigned sh = b.to_nat(b.bw);
if (sh == 0)
@ -1382,7 +1392,259 @@ namespace bv {
}
bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
#if 0
return try_repair_ashr(e, a, b, i);
#else
if (i == 0)
return try_repair_lshr0(e, a, b);
else
return try_repair_lshr1(e, a, b);
#endif
}
/**
* strong:
* - e = (e << b) >> b -> a := e << b, upper b bits set random
* weak:
* - e = 0 -> a := random
* - e > 0 -> a := random with msb(a) >= msb(e)
*/
bool sls_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) {
auto& t = m_tmp;
// t := e << b
// t := t >> b
t.set_shift_left(e, b.bits());
t.set_shift_right(t, b.bits());
bool use_strong = m_rand(10) != 0;
if (t == e && use_strong) {
t.set_shift_left(e, b.bits());
unsigned n = b.bits().to_nat(e.bw);
for (unsigned i = e.bw; i-- > e.bw - n;)
t.set(i, a.get_bit(i));
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t))
return true;
}
unsigned sh = b.to_nat(b.bw);
if (sh == 0 && a.try_set(e))
return true;
else if (sh >= b.bw)
return true;
else if (sh < b.bw && m_rand(20) != 0) {
// e = a >> sh
// a[bw-1:sh] = e[bw-sh-1:0]
// a[sh-1:0] = a[sh-1:0]
for (unsigned i = sh; i < a.bw; ++i)
t.set(i, e.get(i - sh));
for (unsigned i = 0; i < sh; ++i)
t.set(i, a.get_bit(i));
a.clear_overflow_bits(t);
if (a.try_set(t))
return true;
}
//bool r = try_repair_ashr(e, a, const_cast<bvval&>(b), 0);
//verbose_stream() << "repair lshr0 " << e << " b: " << b << " a: " << a << "\n";
//return r;
a.get_variant(t, m_rand);
unsigned msb = a.msb(e);
if (msb > a.msb(t)) {
unsigned num_flex = 0;
for (unsigned i = e.bw; i-- >= msb;)
if (!a.fixed.get(i))
++num_flex;
if (num_flex == 0)
return false;
unsigned n = m_rand(num_flex);
for (unsigned i = e.bw; i-- >= msb;) {
if (!a.fixed.get(i)) {
if (n == 0) {
t.set(i, true);
break;
}
else
n--;
}
}
}
return a.set_repair(random_bool(), t);
}
/**
* strong:
* - clz(a) <= clz(e), e = 0 or (a >> (clz(e) - clz(a)) = e
* - e = 0 and a = 0: b := random
* - e = 0 and a != 0: b := random, such that shift <= b
* - e != 0: b := shift
* where shift := clz(e) - clz(a)
*
* weak:
* - e = 0: b := random
* - e > 0: b := random >= clz(e)
*/
bool sls_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) {
auto& t = m_tmp;
auto clza = a.clz(a.bits());
auto clze = a.clz(e);
t.set_bw(a.bw);
// strong
if (m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) {
if (a.is_zero(e) && a.is_zero())
return true;
unsigned shift = clze - clza;
if (a.is_zero(e))
shift = m_rand(a.bw + 1 - shift) + shift;
b.set(t, shift);
if (b.try_set(t))
return true;
}
// no change
if (m_rand(10) != 0) {
if (a.is_zero(e))
return true;
if (b.bits() <= clze)
return true;
}
// weak
b.get_variant(t, m_rand);
if (a.is_zero(e))
return b.set_repair(random_bool(), t);
else {
for (unsigned i = 0; i < 4; ++i) {
for (unsigned i = a.bw; !(t <= clze) && i-- > 0; )
if (!b.fixed.get(i))
t.set(i, false);
if (t <= clze && b.set_repair(random_bool(), t))
return true;
b.get_variant(t, m_rand);
}
return false;
}
}
/**
* strong:
* b < |b| => (e << b) >>a b = e)
* b >= |b| => (e = ones || e = 0)
* - if b < |b|: a := e << b
* - if b >= |b|: a[bw-1] := e = ones
* weak:
*
*/
bool sls_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) {
auto& t = m_tmp;
t.set_bw(b.bw);
auto n = b.msb(b.bits());
bool use_strong = m_rand(20) != 0;
if (use_strong && n < b.bw) {
t.set_shift_left(e, b.bits());
bool sign = t.get(b.bw-1);
t.set_shift_right(t, b.bits());
if (sign) {
for (unsigned i = b.bw; i-- > b.bw - n; )
t.set(i, true);
}
use_strong &= t == e;
}
else {
use_strong &= a.is_zero(e) || a.is_ones(e);
}
if (use_strong) {
if (n < b.bw) {
t.set_shift_left(e, b.bits());
for (unsigned i = 0; i < n; ++i)
t.set(i, a.get_bit(i));
}
else {
for (unsigned i = 0; i < b.nw; ++i)
t[i] = a.bits()[i];
t.set(b.bw - 1, a.is_ones(e));
}
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t))
return true;
}
if (m_rand(10) != 0) {
if (n < b.bw) {
t.set_shift_left(e, b.bits());
for (unsigned i = 0; i < n; ++i)
t.set(i, random_bool());
}
else {
a.get_variant(t, m_rand);
t.set(b.bw - 1, a.is_ones(e));
}
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t))
return true;
}
a.get_variant(t, m_rand);
return a.set_repair(random_bool(), t);
}
/*
* strong:
* - clz(a) <= clz(e), e = 0 or (a >>a (clz(e) - clz(a)) = e
* - e = 0 and a = 0: b := random
* - e = 0 and a != 0: b := random, such that shift <= b
* - e != 0: b := shift
* where shift := clz(e) - clz(a)
*
* weak:
* - e = 0: b := random
* - e > 0: b := random >= clz(e)
*/
bool sls_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) {
auto& t = m_tmp;
auto clza = a.clz(a.bits());
auto clze = a.clz(e);
t.set_bw(a.bw);
// strong unsigned
if (!a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) {
if (a.is_zero(e) && a.is_zero())
return true;
unsigned shift = clze - clza;
if (a.is_zero(e))
shift = m_rand(a.bw + 1 - shift) + shift;
b.set(t, shift);
if (b.try_set(t))
return true;
}
// strong signed
if (a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza >= clze) {
t.set_shift_right(a.bits(), clza - clze);
for (unsigned i = a.bw; i-- > a.bw - clza + clze; )
t.set(i, true);
if (e == t) {
if (a.is_zero(e) && a.is_zero())
return true;
unsigned shift = clze - clza;
if (a.is_zero(e))
shift = m_rand(a.bw + 1 - shift) + shift;
b.set(t, shift);
if (b.try_set(t))
return true;
}
}
// weak
b.get_variant(t, m_rand);
return b.set_repair(random_bool(), t);
}
bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {

4
src/ast/sls/bv_sls_eval.h
View file

@ -93,6 +93,10 @@ namespace bv {
bool try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_ashr(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_lshr0(bvect const& e, bvval& a, bvval const& b);
bool try_repair_lshr1(bvect const& e, bvval const& a, bvval& b);
bool try_repair_ashr0(bvect const& e, bvval& a, bvval const& b);
bool try_repair_ashr1(bvect const& e, bvval const& a, bvval& b);
bool try_repair_bit2bool(bvval& a, unsigned idx);
bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i);

107
src/ast/sls/sls_valuation.cpp
View file

@ -56,6 +56,20 @@ namespace bv {
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0;
}
bool operator<=(digit_t a, bvect const& b) {
for (unsigned i = 1; i < b.nw; ++i)
if (0 != b[i])
return true;
return mpn_manager().compare(&a, 1, b.data(), 1) <= 0;
}
bool operator<=(bvect const& a, digit_t b) {
for (unsigned i = 1; i < a.nw; ++i)
if (0 != a[i])
return false;
return mpn_manager().compare(a.data(), 1, &b, 1) <= 0;
}
std::ostream& operator<<(std::ostream& out, bvect const& v) {
out << std::hex;
bool nz = false;
@ -83,6 +97,57 @@ namespace bv {
return r;
}
unsigned bvect::to_nat(unsigned max_n) const {
SASSERT(max_n < UINT_MAX / 2);
unsigned p = 1;
unsigned value = 0;
for (unsigned i = 0; i < bw; ++i) {
if (p >= max_n) {
for (unsigned j = i; j < bw; ++j)
if (get(j))
return max_n;
return value;
}
if (get(i))
value += p;
p <<= 1;
}
return value;
}
bvect& bvect::set_shift_right(bvect const& a, bvect const& b) {
SASSERT(a.bw == b.bw);
unsigned shift = b.to_nat(b.bw);
return set_shift_right(a, shift);
}
bvect& bvect::set_shift_right(bvect const& a, unsigned shift) {
set_bw(a.bw);
if (shift == 0)
a.copy_to(a.nw, *this);
else if (shift >= a.bw)
set_zero();
else
for (unsigned i = 0; i < bw; ++i)
set(i, i + shift < bw ? a.get(i + shift) : false);
return *this;
}
bvect& bvect::set_shift_left(bvect const& a, bvect const& b) {
set_bw(a.bw);
SASSERT(a.bw == b.bw);
unsigned shift = b.to_nat(b.bw);
if (shift == 0)
a.copy_to(a.nw, *this);
else if (shift >= a.bw)
set_zero();
else
for (unsigned i = bw; i-- > 0; )
set(i, i >= shift ? a.get(i - shift) : false);
return *this;
}
sls_valuation::sls_valuation(unsigned bw) {
set_bw(bw);
m_lo.set_bw(bw);
@ -411,6 +476,16 @@ namespace bv {
return bw;
}
unsigned sls_valuation::clz(bvect const& src) const {
SASSERT(!has_overflow(src));
unsigned i = bw;
for (; i-- > 0; )
if (!src.get(i))
return bw - 1 - i;
return bw;
}
void sls_valuation::set_value(bvect& bits, rational const& n) {
for (unsigned i = 0; i < bw; ++i)
bits.set(i, n.get_bit(i));
@ -438,11 +513,14 @@ namespace bv {
void sls_valuation::repair_sign_bits(bvect& dst) const {
if (m_signed_prefix == 0)
return;
bool sign = dst.get(bw - 1);
for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) {
bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1);
for (unsigned i = bw; i-- > bw - m_signed_prefix; ) {
if (dst.get(i) != sign) {
if (fixed.get(i)) {
for (unsigned i = bw; i-- >= bw - m_signed_prefix; )
unsigned j = bw - m_signed_prefix;
if (j > 0 && !fixed.get(j - 1))
dst.set(j - 1, !sign);
for (unsigned i = bw; i-- > bw - m_signed_prefix; )
if (!fixed.get(i))
dst.set(i, !sign);
return;
@ -466,24 +544,11 @@ namespace bv {
return in_range(new_bits);
}
unsigned sls_valuation::to_nat(unsigned max_n) {
unsigned sls_valuation::to_nat(unsigned max_n) const {
bvect const& d = m_bits;
SASSERT(!has_overflow(d));
SASSERT(max_n < UINT_MAX / 2);
unsigned p = 1;
unsigned value = 0;
for (unsigned i = 0; i < bw; ++i) {
if (p >= max_n) {
for (unsigned j = i; j < bw; ++j)
if (d.get(j))
return max_n;
return value;
}
if (d.get(i))
value += p;
p <<= 1;
}
return value;
return d.to_nat(max_n);
}
void sls_valuation::shift_right(bvect& out, unsigned shift) const {
@ -493,7 +558,9 @@ namespace bv {
SASSERT(well_formed());
}
void sls_valuation::add_range(rational l, rational h) {
void sls_valuation::add_range(rational l, rational h) {
//return;
l = mod(l, rational::power_of_two(bw));
h = mod(h, rational::power_of_two(bw));

20
src/ast/sls/sls_valuation.h
View file

@ -60,13 +60,27 @@ namespace bv {
return bw;
}
void set_zero() {
for (unsigned i = 0; i < nw; ++i)
(*this)[i] = 0;
}
bvect& set_shift_right(bvect const& a, bvect const& b);
bvect& set_shift_right(bvect const& a, unsigned shift);
bvect& set_shift_left(bvect const& a, bvect const& b);
rational get_value(unsigned nw) const;
unsigned to_nat(unsigned max_n) const;
friend bool operator==(bvect const& a, bvect const& b);
friend bool operator<(bvect const& a, bvect const& b);
friend bool operator>(bvect const& a, bvect const& b);
friend bool operator<=(bvect const& a, bvect const& b);
friend bool operator>=(bvect const& a, bvect const& b);
friend bool operator<=(digit_t a, bvect const& b);
friend bool operator<=(bvect const& a, digit_t b);
friend std::ostream& operator<<(std::ostream& out, bvect const& v);
private:
@ -198,6 +212,8 @@ namespace bv {
// most significant bit or bw if src = 0
unsigned msb(bvect const& src) const;
unsigned clz(bvect const& src) const;
bool is_power_of2(bvect const& src) const;
// retrieve largest number at or below (above) src which is feasible
@ -232,7 +248,7 @@ namespace bv {
clear_overflow_bits(eval);
}
void set_zero(bvect& out) const {
void set_zero(bvect& out) const {
for (unsigned i = 0; i < nw; ++i)
out[i] = 0;
}
@ -288,7 +304,7 @@ namespace bv {
dst[i] = src[i];
}
unsigned to_nat(unsigned max_n);
unsigned to_nat(unsigned max_n) const;
std::ostream& display(std::ostream& out) const {
out << m_bits;