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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-19 15:32:53 +07:00
parent 991537836b
commit 4391c90960
9 changed files with 126 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -21,6 +21,7 @@ Author:
#include "ast/sls/bv_sls.h" #include "ast/sls/bv_sls.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "params/sls_params.hpp"
namespace bv { namespace bv {
@ -48,15 +49,17 @@ namespace bv {
void sls::reinit_eval() { void sls::reinit_eval() {
std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) { std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
auto should_keep = [&]() {
return m_rand() % 100 >= 95;
};
if (m.is_bool(e)) { if (m.is_bool(e)) {
if (m_eval.is_fixed0(e)) if (m_eval.is_fixed0(e) || should_keep())
return m_eval.bval0(e); return m_eval.bval0(e);
} }
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
auto& w = m_eval.wval0(e); auto& w = m_eval.wval0(e);
if (w.get(w.fixed, i)) if (w.get(w.fixed, i) || should_keep())
return w.get(w.bits, i); return w.get(w.bits, i);
} }
return m_rand() % 2 == 0; return m_rand() % 2 == 0;
}; };
@ -77,7 +80,7 @@ namespace bv {
unsigned index = m_rand(m_repair_down.size()); unsigned index = m_rand(m_repair_down.size());
e = m_terms.term(m_repair_down.elem_at(index)); e = m_terms.term(m_repair_down.elem_at(index));
} }
else if (m_repair_up.empty()) { else if (!m_repair_up.empty()) {
unsigned index = m_rand(m_repair_up.size()); unsigned index = m_rand(m_repair_up.size());
e = m_terms.term(m_repair_up.elem_at(index)); e = m_terms.term(m_repair_up.elem_at(index));
} }
@ -85,43 +88,51 @@ namespace bv {
} }
lbool sls::search() { lbool sls::search() {
// init and init_eval were invoked. // init and init_eval were invoked
unsigned& n = m_stats.m_moves; unsigned n = 0;
n = 0; for (; n++ < m_config.m_max_repairs && m.inc(); ) {
for (; n < m_config.m_max_repairs && m.inc(); ++n) { ++m_stats.m_moves;
auto [down, e] = next_to_repair(); auto [down, e] = next_to_repair();
if (!e) if (!e)
return l_true; return l_true;
IF_VERBOSE(20, verbose_stream() << (down ? "d " : "u ") << mk_bounded_pp(e, m, 1) << "\n"); IF_VERBOSE(20, verbose_stream() << (down ? "d #" : "u #")
<< e->get_id() << ": "
<< mk_bounded_pp(e, m, 1) << " ";
if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e);
verbose_stream() << "\n");
if (eval_is_correct(e)) { if (eval_is_correct(e)) {
if (down) if (down)
m_repair_down.remove(e->get_id()); m_repair_down.remove(e->get_id());
else else
m_repair_up.remove(e->get_id()); m_repair_up.remove(e->get_id());
} }
else if (down) { else if (down)
try_repair_down(e); try_repair_down(e);
}
else else
try_repair_up(e); try_repair_up(e);
} }
return l_undef; return l_undef;
} }
void sls::trace() {
IF_VERBOSE(2, verbose_stream()
<< "(bvsls :restarts " << m_stats.m_restarts
<< " :repair-down " << m_repair_down.size()
<< " :repair-up " << m_repair_up.size() << ")\n");
}
lbool sls::operator()() { lbool sls::operator()() {
lbool res = l_undef; lbool res = l_undef;
m_stats.reset();
m_stats.m_restarts = 0;
do { do {
if (!m.inc())
return l_undef;
res = search(); res = search();
if (res != l_undef) if (res != l_undef)
return res; break;
trace();
reinit_eval(); reinit_eval();
} }
while (m_stats.m_restarts++ < m_config.m_max_restarts); while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
return res; return res;
} }
@ -162,6 +173,8 @@ namespace bv {
} }
bool sls::eval_is_correct(app* e) { bool sls::eval_is_correct(app* e) {
if (!m_eval.can_eval1(e))
return false;
if (m.is_bool(e)) if (m.is_bool(e))
return m_eval.bval0(e) == m_eval.bval1(e); return m_eval.bval0(e) == m_eval.bval1(e);
if (bv.is_bv(e)) if (bv.is_bv(e))
@ -208,4 +221,9 @@ namespace bv {
terms.reset(); terms.reset();
return out; return out;
} }
void sls::updt_params(params_ref const& _p) {
sls_params p(_p);
m_config.m_max_restarts = p.max_restarts();
}
} }

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

@ -36,7 +36,7 @@ namespace bv {
struct config { struct config {
unsigned m_max_restarts = 1000; unsigned m_max_restarts = 1000;
unsigned m_max_repairs = 100000; unsigned m_max_repairs = 1000;
}; };
ast_manager& m; ast_manager& m;
@ -59,6 +59,7 @@ namespace bv {
lbool search(); lbool search();
void reinit_eval(); void reinit_eval();
void trace();
public: public:
sls(ast_manager& m); sls(ast_manager& m);
@ -85,7 +86,7 @@ namespace bv {
*/ */
lbool operator()(); lbool operator()();
void updt_params(params_ref const& p) {} void updt_params(params_ref const& p);
void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); } void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); }
void reset_statistics() { m_stats.reset(); } void reset_statistics() { m_stats.reset(); }

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

@ -171,15 +171,41 @@ namespace bv {
auto const& vb = wval0(b); auto const& vb = wval0(b);
return va.eq(vb); return va.eq(vb);
} }
UNREACHABLE(); return m.are_equal(a, b);
break;
} }
default: default:
UNREACHABLE(); UNREACHABLE();
break;
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
bool sls_eval::can_eval1(app* e) const {
expr* x, * y, * z;
if (m.is_eq(e, x, y))
return m.is_bool(x) || bv.is_bv(x);
if (m.is_ite(e, x, y, z))
return m.is_bool(y) || bv.is_bv(y);
if (e->get_family_id() == bv.get_fid()) {
switch (e->get_decl_kind()) {
case OP_BNEG_OVFL:
case OP_BSADD_OVFL:
case OP_BSDIV_OVFL:
case OP_BSMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
case OP_BSMUL_OVFL:
return false;
default:
return true;
}
}
if (e->get_family_id() == basic_family_id)
return true;
if (is_uninterp_const(e))
return m.is_bool(e) || bv.is_bv(e);
return false;
}
bool sls_eval::bval1_bv(app* e) const { bool sls_eval::bval1_bv(app* e) const {
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
@ -1182,8 +1208,8 @@ namespace bv {
if (i == 0) { if (i == 0) {
if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones()) if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones())
return false; return false;
if (b.is_zero()) if (b.is_zero())
return true; return false;
if (!e.is_ones()) { if (!e.is_ones()) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = ~a.fixed[i] | a.bits[i]; m_tmp[i] = ~a.fixed[i] | a.bits[i];
@ -1215,11 +1241,19 @@ namespace bv {
a.set_repair(true, m_tmp3); a.set_repair(true, m_tmp3);
} }
else { else {
if (e.is_one() && a.is_zero()) {
for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = random_bits();
a.clear_overflow_bits(m_tmp);
b.set_repair(true, m_tmp);
return true;
}
if (e.is_one()) { if (e.is_one()) {
b.set(m_tmp, a.bits); b.set(m_tmp, a.bits);
b.set_repair(true, m_tmp); b.set_repair(true, m_tmp);
return true; return true;
} }
// e * b + r = a // e * b + r = a
// b = (a - r) udiv e // b = (a - r) udiv e
// random version of r: // random version of r:

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

@ -134,6 +134,7 @@ namespace bv {
* Retrieve evaluation based on immediate children. * Retrieve evaluation based on immediate children.
*/ */
bool bval1(app* e) const; bool bval1(app* e) const;
bool can_eval1(app* e) const;
svector<digit_t>& wval1(app* e) const; svector<digit_t>& wval1(app* e) const;

5
src/ast/sls/bv_sls_fixed.cpp
View file

@ -11,6 +11,7 @@ Author:
--*/ --*/
#include "ast/ast_pp.h"
#include "ast/sls/bv_sls_fixed.h" #include "ast/sls/bv_sls_fixed.h"
#include "ast/sls/bv_sls_eval.h" #include "ast/sls/bv_sls_eval.h"
@ -137,12 +138,12 @@ namespace bv {
v.add_range(-b, a - b); v.add_range(-b, a - b);
} }
else if (!y) { else if (!y) {
if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 1) if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0)
return; return;
auto& v = wval0(x); auto& v = wval0(x);
if (!sign) if (!sign)
v.add_range(-a, b - a + 1); v.add_range(-a, b - a + 1);
else else
v.add_range(b - a + 1, -a); v.add_range(b - a + 1, -a);
} }
else if (x == y) { else if (x == y) {

7
src/ast/sls/sls_stats.h
View file

@ -35,13 +35,16 @@ namespace bv {
st.update("sls restarts", m_restarts); st.update("sls restarts", m_restarts);
st.update("sls full evals", m_full_evals); st.update("sls full evals", m_full_evals);
st.update("sls incr evals", m_incr_evals); st.update("sls incr evals", m_incr_evals);
st.update("sls incr evals/sec", m_incr_evals / seconds); if (seconds > 0 && m_incr_evals > 0)
st.update("sls incr evals/sec", m_incr_evals / seconds);
if (seconds > 0 && m_moves > 0)
st.update("sls moves/sec", m_moves / seconds);
st.update("sls FLIP moves", m_flips); st.update("sls FLIP moves", m_flips);
st.update("sls INC moves", m_incs); st.update("sls INC moves", m_incs);
st.update("sls DEC moves", m_decs); st.update("sls DEC moves", m_decs);
st.update("sls INV moves", m_invs); st.update("sls INV moves", m_invs);
st.update("sls moves", m_moves); st.update("sls moves", m_moves);
st.update("sls moves/sec", m_moves / seconds);
} }
}; };

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

@ -296,6 +296,7 @@ namespace bv {
h = mod(h, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw));
if (h == l) if (h == l)
return; return;
if (eq(lo, hi)) { if (eq(lo, hi)) {
set_value(lo, l); set_value(lo, l);
set_value(hi, h); set_value(hi, h);

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

@ -192,19 +192,26 @@ namespace bv {
std::ostream& display(std::ostream& out) const { std::ostream& display(std::ostream& out) const {
out << std::hex; out << std::hex;
for (unsigned i = 0; i < nw; ++i) auto print_bits = [&](svector<digit_t> const& v) {
out << bits[i]; bool nz = false;
for (unsigned i = nw; i-- > 0;)
if (nz)
out << std::setw(8) << std::setfill('0') << v[i];
else if (v[i] != 0)
out << v[i], nz = true;
if (!nz)
out << "0";
};
print_bits(bits);
out << " "; out << " ";
for (unsigned i = 0; i < nw; ++i) print_bits(fixed);
out << fixed[i];
if (!eq(lo, hi)) { if (!eq(lo, hi)) {
out << " ["; out << " [";
for (unsigned i = 0; i < nw; ++i) print_bits(lo);
out << lo[i];
out << ", "; out << ", ";
for (unsigned i = 0; i < nw; ++i) print_bits(hi);
out << hi[i];
out << "["; out << "[";
} }
out << std::dec; out << std::dec;

40
src/tactic/sls/sls_tactic.cpp
View file

@ -126,14 +126,15 @@ public:
class bv_sls_tactic : public tactic { class bv_sls_tactic : public tactic {
ast_manager& m; ast_manager& m;
params_ref m_params; params_ref m_params;
bv::sls* m_engine; bv::sls* m_sls;
statistics m_st;
public: public:
bv_sls_tactic(ast_manager& _m, params_ref const& p) : bv_sls_tactic(ast_manager& _m, params_ref const& p) :
m(_m), m(_m),
m_params(p) { m_params(p) {
m_engine = alloc(bv::sls, m); m_sls = alloc(bv::sls, m);
} }
tactic* translate(ast_manager& m) override { tactic* translate(ast_manager& m) override {
@ -141,14 +142,14 @@ public:
} }
~bv_sls_tactic() override { ~bv_sls_tactic() override {
dealloc(m_engine); dealloc(m_sls);
} }
char const* name() const override { return "bv-sls"; } char const* name() const override { return "bv-sls"; }
void updt_params(params_ref const& p) override { void updt_params(params_ref const& p) override {
m_params.append(p); m_params.append(p);
m_engine->updt_params(m_params); m_sls->updt_params(m_params);
} }
void collect_param_descrs(param_descrs& r) override { void collect_param_descrs(param_descrs& r) override {
@ -162,23 +163,24 @@ public:
} }
for (unsigned i = 0; i < g->size(); i++) for (unsigned i = 0; i < g->size(); i++)
m_engine->assert_expr(g->form(i)); m_sls->assert_expr(g->form(i));
m_engine->init(); m_sls->init();
std::function<bool(expr*, unsigned)> false_eval = [&](expr* e, unsigned idx) { std::function<bool(expr*, unsigned)> false_eval = [&](expr* e, unsigned idx) {
return false; return false;
}; };
m_engine->init_eval(false_eval); m_sls->init_eval(false_eval);
lbool res = m_engine->operator()(); lbool res = m_sls->operator()();
auto const& stats = m_engine->get_stats(); auto const& stats = m_sls->get_stats();
report_tactic_progress("Number of flips:", stats.m_moves); report_tactic_progress("Number of flips:", stats.m_moves);
IF_VERBOSE(0, verbose_stream() << res << "\n"); IF_VERBOSE(20, verbose_stream() << res << "\n");
IF_VERBOSE(0, m_engine->display(verbose_stream())); IF_VERBOSE(20, m_sls->display(verbose_stream()));
if (res == l_true) { m_st.reset();
m_sls->collect_statistics(m_st);
if (res == l_true) {
if (g->models_enabled()) { if (g->models_enabled()) {
model_ref mdl = m_engine->get_model(); model_ref mdl = m_sls->get_model();
mc = model2model_converter(mdl.get()); mc = model2model_converter(mdl.get());
TRACE("sls_model", mc->display(tout);); TRACE("sls_model", mc->display(tout););
} }
@ -204,17 +206,19 @@ public:
} }
void cleanup() override { void cleanup() override {
auto* d = alloc(bv::sls, m); auto* d = alloc(bv::sls, m);
std::swap(d, m_engine); std::swap(d, m_sls);
dealloc(d); dealloc(d);
} }
void collect_statistics(statistics& st) const override { void collect_statistics(statistics& st) const override {
m_engine->collect_statistics(st); st.copy(m_st);
} }
void reset_statistics() override { void reset_statistics() override {
m_engine->reset_statistics(); m_sls->reset_statistics();
m_st.reset();
} }
}; };