mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

optimzie

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-06 15:36:20 -08:00
parent 6787d87623
commit e3e650a249
4 changed files with 42 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/sls_bv_eval.cpp
View file

@ -199,7 +199,7 @@ namespace sls {
return false; return false;
} }
void bv_eval::set_bool_value(expr* e, bool val) { void bv_eval::set_bool_value_log(expr* e, bool val) {
auto id = e->get_id(); auto id = e->get_id();
auto old_val = m_tmp_bool_values.get(id, l_undef); auto old_val = m_tmp_bool_values.get(id, l_undef);
m_tmp_bool_values.setx(id, to_lbool(val), l_undef); m_tmp_bool_values.setx(id, to_lbool(val), l_undef);
@ -207,6 +207,11 @@ namespace sls {
//TRACE("bv", tout << mk_bounded_pp(e, m) << " := " << val << " old: " << old_val << "\n"); //TRACE("bv", tout << mk_bounded_pp(e, m) << " := " << val << " old: " << old_val << "\n");
} }
void bv_eval::set_bool_value_no_log(expr* e, bool val) {
auto id = e->get_id();
m_tmp_bool_values.setx(id, to_lbool(val), l_undef);
}
bool bv_eval::get_bool_value(expr* e) const { bool bv_eval::get_bool_value(expr* e) const {
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
auto id = e->get_id(); auto id = e->get_id();

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

@ -193,7 +193,8 @@ namespace sls {
bool bval1(expr* e) const; bool bval1(expr* e) const;
unsigned bool_value_restore_point() const { return m_tmp_bool_value_updates.size(); } unsigned bool_value_restore_point() const { return m_tmp_bool_value_updates.size(); }
void set_bool_value(expr* e, bool val); void set_bool_value_log(expr* e, bool val);
void set_bool_value_no_log(expr* e, bool val);
void restore_bool_values(unsigned restore_point); void restore_bool_values(unsigned restore_point);
void commit_bool_values() { m_tmp_bool_value_updates.reset(); } void commit_bool_values() { m_tmp_bool_value_updates.reset(); }
bool get_bool_value(expr* e) const; bool get_bool_value(expr* e) const;

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

@ -97,7 +97,7 @@ namespace sls {
} }
else if (m.is_bool(t)) { else if (m.is_bool(t)) {
auto b = m_ev.bval1(t); auto b = m_ev.bval1(t);
m_ev.set_bool_value(t, b); m_ev.set_bool_value_no_log(t, b);
} }
} }
m_ev.commit_bool_values(); m_ev.commit_bool_values();
@ -472,7 +472,6 @@ namespace sls {
double bv_lookahead::lookahead_update(expr* t, bvect const& new_value) { double bv_lookahead::lookahead_update(expr* t, bvect const& new_value) {
SASSERT(bv.is_bv(t) || m.is_bool(t)); SASSERT(bv.is_bv(t) || m.is_bool(t));
SASSERT(is_uninterp(t)); SASSERT(is_uninterp(t));
SASSERT(m_restore.empty());
double score = m_top_score; double score = m_top_score;
unsigned restore_point = m_ev.bool_value_restore_point(); unsigned restore_point = m_ev.bool_value_restore_point();
@ -486,16 +485,16 @@ namespace sls {
insert_update(t); insert_update(t);
} }
else if (m.is_bool(t)) else if (m.is_bool(t))
m_ev.set_bool_value(t, !m_ev.get_bool_value(t)); m_ev.set_bool_value_no_log(t, !m_ev.get_bool_value(t));
// TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << "\n";); // TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << "\n";);
for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) { for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto a = m_update_stack[depth][i]; auto const& [a, is_bv] = m_update_stack[depth][i];
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " depth: " << depth << "\n";); TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " depth: " << depth << "\n";);
if (t != a) { if (t != a) {
if (bv.is_bv(a)) if (is_bv)
m_ev.eval(a); m_ev.eval(a);
insert_update(a); insert_update(a);
} }
@ -505,7 +504,6 @@ namespace sls {
} }
} }
} }
restore_lookahead();
m_ev.restore_bool_values(restore_point); m_ev.restore_bool_values(restore_point);
TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << " score: " << score << " " << m_best_score << "\n"); TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << " score: " << score << " " << m_best_score << "\n");
@ -514,15 +512,23 @@ namespace sls {
} }
void bv_lookahead::populate_update_stack(expr* t) { void bv_lookahead::populate_update_stack(expr* t) {
SASSERT(m_bv_restore.empty());
insert_update_stack(t); insert_update_stack(t);
m_min_depth = m_max_depth = get_depth(t); m_min_depth = m_max_depth = get_depth(t);
for (unsigned depth = m_max_depth; depth <= m_max_depth; ++depth) { for (unsigned depth = m_max_depth; depth <= m_max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto a = m_update_stack[depth][i]; auto [a, is_bv] = m_update_stack[depth][i];
for (auto p : ctx.parents(a)) { for (auto p : ctx.parents(a)) {
insert_update_stack(p); insert_update_stack(p);
m_max_depth = std::max(m_max_depth, get_depth(p)); m_max_depth = std::max(m_max_depth, get_depth(p));
} }
if (is_bv) {
wval(a).save_value();
SASSERT(!m_bv_restore.contains(a));
m_bv_restore.push_back(a);
}
else
m_bool_restore.push_back({ a, m_ev.get_bool_value(a) });
} }
} }
} }
@ -531,6 +537,14 @@ namespace sls {
for (unsigned i = m_min_depth; i <= m_max_depth; ++i) for (unsigned i = m_min_depth; i <= m_max_depth; ++i)
m_update_stack[i].reset(); m_update_stack[i].reset();
m_in_update_stack.reset(); m_in_update_stack.reset();
for (auto e : m_bv_restore) {
wval(e).restore_value();
TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
}
for (auto const& [e, b]: m_bool_restore)
m_ev.set_bool_value_no_log(e, b);
m_bv_restore.reset();
m_bool_restore.reset();
} }
void bv_lookahead::try_set(expr* u, bvect const& new_value) { void bv_lookahead::try_set(expr* u, bvect const& new_value) {
@ -646,7 +660,7 @@ namespace sls {
VERIFY(wval(t).commit_eval_check_tabu()); VERIFY(wval(t).commit_eval_check_tabu());
} }
else { else {
m_ev.set_bool_value(t, !m_ev.get_bool_value(t)); m_ev.set_bool_value_log(t, !m_ev.get_bool_value(t));
if (!m_config.use_top_level_assertions) { if (!m_config.use_top_level_assertions) {
auto v = ctx.atom2bool_var(t); auto v = ctx.atom2bool_var(t);
if (v != sat::null_bool_var) if (v != sat::null_bool_var)
@ -659,17 +673,17 @@ namespace sls {
unsigned restore_point = m_ev.bool_value_restore_point(); unsigned restore_point = m_ev.bool_value_restore_point();
for (unsigned depth = max_depth; depth <= max_depth; ++depth) { for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto e = m_update_stack[depth][i]; auto [e, is_bv] = m_update_stack[depth][i];
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(e, m) << "\n";); TRACE("bv_verbose", tout << "update " << mk_bounded_pp(e, m) << "\n";);
if (t == e) if (t == e)
; ;
else if (bv.is_bv(e)) { else if (is_bv) {
m_ev.eval(e); // updates wval(e).eval m_ev.eval(e); // updates wval(e).eval
wval(e).commit_eval_ignore_tabu(); wval(e).commit_eval_ignore_tabu();
} }
else if (m.is_bool(e)) { else {
SASSERT(is_bool(e));
auto v1 = m_ev.bval1(e); auto v1 = m_ev.bval1(e);
CTRACE("bv_verbose", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";); CTRACE("bv_verbose", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";);
@ -700,7 +714,7 @@ namespace sls {
} }
} }
} }
m_ev.set_bool_value(e, v1); m_ev.set_bool_value_log(e, v1);
} }
for (auto p : ctx.parents(e)) { for (auto p : ctx.parents(e)) {
@ -739,35 +753,25 @@ namespace sls {
TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n"); TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n");
if (bv.is_bv(e)) { if (bv.is_bv(e)) {
auto& v = wval(e); auto& v = wval(e);
v.save_value();
v.commit_eval_ignore_tabu(); v.commit_eval_ignore_tabu();
SASSERT(!m_restore.contains(e));
m_restore.push_back(e);
} }
else if (m.is_bool(e)) { else if (m.is_bool(e)) {
auto v1 = m_ev.bval1(to_app(e)); auto v1 = m_ev.bval1(to_app(e));
m_ev.set_bool_value(to_app(e), v1); m_ev.set_bool_value_no_log(to_app(e), v1);
} }
} }
void bv_lookahead::insert_update_stack(expr* e) { void bv_lookahead::insert_update_stack(expr* e) {
if (!bv.is_bv(e) && !m.is_bool(e))
return;
unsigned depth = get_depth(e); unsigned depth = get_depth(e);
m_update_stack.reserve(depth + 1); m_update_stack.reserve(depth + 1);
if (!m_in_update_stack.is_marked(e) && is_app(e)) { if (!m_in_update_stack.is_marked(e) && is_app(e)) {
m_in_update_stack.mark(e); m_in_update_stack.mark(e);
m_update_stack[depth].push_back(to_app(e)); m_update_stack[depth].push_back({ to_app(e), bv.is_bv(e) });
} }
} }
void bv_lookahead::restore_lookahead() {
for (auto e : m_restore) {
wval(e).restore_value();
TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
}
m_restore.reset();
}
sls::bv_valuation& bv_lookahead::wval(expr* e) const { sls::bv_valuation& bv_lookahead::wval(expr* e) const {
return m_ev.wval(e); return m_ev.wval(e);
} }

6
src/ast/sls/sls_bv_lookahead.h
View file

@ -73,8 +73,9 @@ namespace sls {
config m_config; config m_config;
stats m_stats; stats m_stats;
bvect m_v_saved, m_v_updated; bvect m_v_saved, m_v_updated;
ptr_vector<expr> m_restore; ptr_vector<expr> m_bv_restore;
vector<ptr_vector<app>> m_update_stack; svector<std::pair<expr*, bool>> m_bool_restore;
vector<vector<std::pair<app*, bool>>> m_update_stack;
expr_mark m_in_update_stack; expr_mark m_in_update_stack;
double m_best_score = 0, m_top_score = 0; double m_best_score = 0, m_top_score = 0;
bvect m_best_value; bvect m_best_value;
@ -95,7 +96,6 @@ namespace sls {
void clear_update_stack(); void clear_update_stack();
void insert_update_stack(expr* e); void insert_update_stack(expr* e);
void insert_update(expr* e); void insert_update(expr* e);
void restore_lookahead();
bool_info& get_bool_info(expr* e); bool_info& get_bool_info(expr* e);
double lookahead_update(expr* u, bvect const& new_value); double lookahead_update(expr* u, bvect const& new_value);