mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

n/a

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-16 14:37:49 +07:00
parent ddf2d28350
commit 388b2f5eec
9 changed files with 274 additions and 202 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/bv_decl_plugin.cpp
View file

@ -942,3 +942,13 @@ app* bv_util::mk_int2bv(unsigned sz, expr* e) {
parameter p(sz);
return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e);
}
app* bv_util::mk_bv_rotate_left(expr* arg, unsigned n) {
parameter p(n);
return m_manager.mk_app(get_fid(), OP_ROTATE_LEFT, 1, &p, 1, &arg);
}
app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) {
parameter p(n);
return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg);
}

5
src/ast/bv_decl_plugin.h
View file

@ -546,6 +546,11 @@ public:
app * mk_bv2int(expr* e);
app * mk_int2bv(unsigned sz, expr* e);
app* mk_bv_rotate_left(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_LEFT, arg1, arg2); }
app* mk_bv_rotate_right(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_RIGHT, arg1, arg2); }
app* mk_bv_rotate_left(expr* arg, unsigned n);
app* mk_bv_rotate_right(expr* arg, unsigned n);
// TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return`
app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); }
app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }

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

@ -46,46 +46,53 @@ namespace bv {
m_eval.init_fixed(m_terms.assertions());
}
std::pair<bool, app*> sls::next_to_repair() {
app* e = nullptr;
if (!m_repair_down.empty()) {
unsigned index = m_rand(m_repair_down.size());
e = m_terms.term(m_repair_down.elem_at(index));
}
else if (m_repair_up.empty()) {
unsigned index = m_rand(m_repair_up.size());
e = m_terms.term(m_repair_up.elem_at(index));
}
return { !m_repair_down.empty(), e };
}
lbool sls::operator()() {
// init and init_eval were invoked.
unsigned& n = m_stats.m_moves;
n = 0;
for (; n < m_config.m_max_repairs && m.inc(); ++n) {
if (!m_repair_down.empty()) {
unsigned index = m_rand(m_repair_down.size());
unsigned expr_id = m_repair_down.elem_at(index);
auto e = m_terms.term(expr_id);
IF_VERBOSE(20, verbose_stream() << "d " << mk_bounded_pp(e, m, 1) << "\n");
if (eval_is_correct(e))
m_repair_down.remove(expr_id);
else
try_repair_down(e);
}
else if (!m_repair_up.empty()) {
unsigned index = m_rand(m_repair_up.size());
unsigned expr_id = m_repair_up.elem_at(index);
auto e = m_terms.term(expr_id);
IF_VERBOSE(20, verbose_stream() << "u " << mk_bounded_pp(e, m, 1) << "\n");
if (eval_is_correct(e))
m_repair_up.remove(expr_id);
else
try_repair_up(e);
}
else
auto [down, e] = next_to_repair();
if (!e)
return l_true;
IF_VERBOSE(20, verbose_stream() << (down?"d ":"u ") << mk_bounded_pp(e, m, 1) << "\n");
if (eval_is_correct(e)) {
if (down)
m_repair_down.remove(e->get_id());
else
m_repair_up.remove(e->get_id());
}
else if (down) {
try_repair_down(e);
}
else
try_repair_up(e);
}
return l_undef;
}
bool sls::try_repair_down(app* e) {
void sls::try_repair_down(app* e) {
unsigned n = e->get_num_args();
if (n == 0)
return false;
unsigned s = m_rand(n);
for (unsigned i = 0; i < n; ++i)
if (try_repair_down(e, (i + s) % n))
return true;
return false;
if (n > 0) {
unsigned s = m_rand(n);
for (unsigned i = 0; i < n; ++i)
if (try_repair_down(e, (i + s) % n))
return;
}
m_repair_down.remove(e->get_id());
m_repair_up.insert(e->get_id());
}
bool sls::try_repair_down(app* e, unsigned i) {
@ -99,17 +106,16 @@ namespace bv {
return was_repaired;
}
bool sls::try_repair_up(app* e) {
void sls::try_repair_up(app* e) {
m_repair_up.remove(e->get_id());
if (m_terms.is_assertion(e)) {
m_repair_down.insert(e->get_id());
return false;
}
m_eval.repair_up(e);
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
return true;
else {
m_eval.repair_up(e);
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
}
}
bool sls::eval_is_correct(app* e) {

5
src/ast/sls/bv_sls.h
View file

@ -49,10 +49,11 @@ namespace bv {
random_gen m_rand;
config m_config;
std::pair<bool, app*> next_to_repair();
bool eval_is_correct(app* e);
bool try_repair_down(app* e);
bool try_repair_up(app* e);
void try_repair_down(app* e);
void try_repair_up(app* e);
bool try_repair_down(app* e, unsigned i);

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

@ -343,16 +343,9 @@ namespace bv {
}
};
auto mk_rotate_left = [&](unsigned n) {
auto mk_rotate_left = [&](unsigned n) {
auto& a = wval0(e->get_arg(0));
if (n == 0 || a.bw == 1)
val.set(a.bits);
else {
for (unsigned i = a.bw - n; i < a.bw; ++i)
val.set(val.bits, i + n - a.bw, a.get(a.bits, i));
for (unsigned i = 0; i < a.bw - n; ++i)
val.set(val.bits, i + a.bw - n, a.get(a.bits, i));
}
VERIFY(try_repair_rotate_left(a, val, a.bw - n));
};
SASSERT(e->get_family_id() == bv.get_fid());
@ -853,6 +846,7 @@ namespace bv {
auto child = e->get_arg(i);
auto ev = bval0(e);
if (m.is_bool(child)) {
SASSERT(!is_fixed0(child));
auto bv = bval0(e->get_arg(1 - i));
m_eval[child->get_id()] = ev == bv;
return true;
@ -863,12 +857,21 @@ namespace bv {
if (ev)
return a.try_set(b.bits);
else {
// pick random bit to differ
for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = a.bits[i];
unsigned idx = m_rand(a.bw);
a.set(m_tmp, idx, !b.get(b.bits, idx));
return a.try_set(m_tmp);
// pick random bit to differ
a.get(m_tmp);
unsigned start = m_rand(a.bw);
for (unsigned idx = 0; idx < a.bw; ++idx) {
unsigned j = (idx + start) % a.bw;
if (!a.get(a.fixed, j)) {
a.set(m_tmp, idx, !b.get(b.bits, j));
bool r = a.try_set(m_tmp);
if (r)
return true;
a.set(m_tmp, j, b.get(b.bits, j));
}
}
// could be due to bounds?
return false;
}
}
return false;
@ -1107,9 +1110,9 @@ namespace bv {
return false;
}
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) {
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const {
// a := rotate_right(e, n)
n = (n % a.bw) - n;
n = (a.bw - n) % a.bw;
for (unsigned i = a.bw - n; i < a.bw; ++i)
a.set(m_tmp, i + n - a.bw, e.get(e.bits, i));
for (unsigned i = 0; i < a.bw - n; ++i)

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

@ -88,10 +88,9 @@ namespace bv {
bool try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n);
bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const;
bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i);
sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); }
void wval1(app* e, sls_valuation& val) const;

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

@ -33,26 +33,27 @@ namespace bv {
for (unsigned i = 0; i < nw; ++i)
lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0;
for (unsigned i = bw; i < 8 * sizeof(digit_t) * nw; ++i)
set(fixed, i, true);
set(fixed, i, false);
}
sls_valuation::~sls_valuation() {
}
bool sls_valuation::is_feasible() const {
return true;
mpn_manager m;
unsigned nb = (bw + 7) / 8;
auto c = m.compare(lo.data(), nb, hi.data(), nb);
bool sls_valuation::in_range(svector<digit_t> const& bits) const {
mpn_manager m;
auto c = m.compare(lo.data(), nw, hi.data(), nw);
// full range
if (c == 0)
return true;
// lo < hi: then lo <= bits & bits < hi
if (c < 0)
return
m.compare(lo.data(), nb, bits.data(), nb) <= 0 &&
m.compare(bits.data(), nb, hi.data(), nb) < 0;
return
m.compare(lo.data(), nb, bits.data(), nb) <= 0 ||
m.compare(bits.data(), nb, hi.data(), nb) < 0;
return
m.compare(lo.data(), nw, bits.data(), nw) <= 0 &&
m.compare(bits.data(), nw, hi.data(), nw) < 0;
// hi < lo: bits < hi or lo <= bits
return
m.compare(lo.data(), nw, bits.data(), nw) <= 0 ||
m.compare(bits.data(), nw, hi.data(), nw) < 0;
}
bool sls_valuation::eq(svector<digit_t> const& other) const {
@ -65,11 +66,34 @@ namespace bv {
return true;
}
bool sls_valuation::gt(svector<digit_t> const& a, svector<digit_t> const& b) const {
mpn_manager m;
return m.compare(a.data(), nw, b.data(), nw) > 0;
}
void sls_valuation::clear_overflow_bits(svector<digit_t>& bits) const {
for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
set(bits, i, false);
}
bool sls_valuation::get_below(svector<digit_t> const& src, svector<digit_t>& dst) {
for (unsigned i = 0; i < nw; ++i)
dst[i] = (src[i] & ~fixed[i]) | (fixed[i] & bits[i]);
for (unsigned i = 0; i < nw; ++i)
dst[i] = fixed[i] & bits[i];
if (gt(dst, src))
return false;
if (!in_range(dst)) {
// lo < hi:
// set dst to lo, except for fixed bits
//
if (gt(hi, lo)) {
}
}
return true;
}
void sls_valuation::set_value(svector<digit_t>& bits, rational const& n) {
for (unsigned i = 0; i < bw; ++i)
set(bits, i, n.get_bit(i));
@ -94,11 +118,16 @@ namespace bv {
set(bits, i, true);
}
bool sls_valuation::can_set(svector<digit_t> const& new_bits) const {
//
// new_bits != bits => ~fixed
// 0 = (new_bits ^ bits) & fixed
// also check that new_bits are in range
//
bool sls_valuation::can_set(svector<digit_t> const& new_bits) const {
for (unsigned i = 0; i < nw; ++i)
if (bits[i] != ((new_bits[i] & ~fixed[i]) | (bits[i] & fixed[i])))
return true;
return false;
if (0 != ((new_bits[i] ^ bits[i]) & fixed[i]))
return false;
return in_range(new_bits);
}
unsigned sls_valuation::to_nat(svector<digit_t> const& d, unsigned max_n) {
@ -124,10 +153,15 @@ namespace bv {
h = mod(h, rational::power_of_two(bw));
if (h == l)
return;
set_value(this->lo, l);
set_value(this->hi, h);
if (eq(lo, hi)) {
set_value(lo, l);
set_value(hi, h);
return;
}
// TODO: intersect with previous range, if any
set_value(lo, l);
set_value(hi, h);
}
}

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

@ -28,11 +28,10 @@ Author:
namespace bv {
struct sls_valuation {
unsigned bw; // bit-width
unsigned nw; // num words
svector<digit_t> lo, hi; // range assignment to bit-vector, as wrap-around interval
unsigned bw; // bit-width
unsigned nw; // num words
svector<digit_t> lo, hi; // range assignment to bit-vector, as wrap-around interval
svector<digit_t> bits, fixed; // bit assignment and don't care bit
bool is_feasible() const; // the current bit-evaluation is between lo and hi.
sls_valuation(unsigned bw);
~sls_valuation();
@ -44,17 +43,15 @@ namespace bv {
void add_range(rational lo, rational hi);
void set1(svector<digit_t>& bits);
void clear_overflow_bits(svector<digit_t>& bits) const;
bool in_range(svector<digit_t> const& bits) const;
bool can_set(svector<digit_t> const& bits) const;
bool eq(sls_valuation const& other) const { return eq(other.bits); }
bool eq(svector<digit_t> const& other) const;
bool gt(svector<digit_t> const& a, svector<digit_t> const& b) const {
return 0 > memcmp(a.data(), b.data(), num_bytes());
}
bool eq(svector<digit_t> const& other) const { return eq(other, bits); }
bool eq(svector<digit_t> const& a, svector<digit_t> const& b) const;
bool gt(svector<digit_t> const& a, svector<digit_t> const& b) const;
bool is_zero() const { return is_zero(bits); }
bool is_zero(svector<digit_t> const& a) const {
@ -79,6 +76,10 @@ namespace bv {
return i;
}
// retrieve number at or below src which is feasible
// with respect to fixed, lo, hi.
bool get_below(svector<digit_t> const& src, svector<digit_t>& dst);
bool try_set(svector<digit_t> const& src) {
if (!can_set(src))
return false;