mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

throttle costly flips by reset and random

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-02 20:39:41 -08:00
parent 70f7feabc8
commit e9c656701d
5 changed files with 54 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -95,7 +95,7 @@ namespace sls {
for (unsigned i = 0; i < sz; ++i)
add_updates(vars[(start + i) % sz]);
CTRACE("bv", !m_best_expr, tout << "no guided move\n";);
return apply_update(m_last_atom, m_best_expr, m_best_value, "increasing move");
return apply_update(m_last_atom, m_best_expr, m_best_value, move_type::guided_t);
}
/**
@ -117,7 +117,8 @@ namespace sls {
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
v.get_variant(m_v_updated, m_ev.m_rand);
return apply_update(nullptr, e, m_v_updated, "random update");
++m_stats.random_flip_count;
return apply_update(m_last_atom, e, m_v_updated, move_type::random_t);
}
/**
@ -153,7 +154,7 @@ namespace sls {
v.sub1(m_v_updated);
break;
}
return apply_update(nullptr, e, m_v_updated, "random move");
return apply_update(m_last_atom, e, m_v_updated, move_type::move_t);
}
/**
@ -243,7 +244,7 @@ namespace sls {
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
m_v_updated.set_zero();
apply_update(nullptr, e, m_v_updated, "reset");
apply_update(nullptr, e, m_v_updated, move_type::reset_t);
}
}
}
@ -517,7 +518,18 @@ namespace sls {
* The update is committed.
*/
bool bv_lookahead::apply_update(expr* p, expr* t, bvect const& new_value, char const* reason) {
std::ostream& operator<<(std::ostream& out, bv_lookahead::move_type t) {
switch (t) {
case bv_lookahead::move_type::guided_t: return out << "guided";
case bv_lookahead::move_type::random_t: return out << "random";
case bv_lookahead::move_type::move_t: return out << "move";
case bv_lookahead::move_type::reset_t: return out << "reset";
default:
return out;
}
}
bool bv_lookahead::apply_update(expr* p, expr* t, bvect const& new_value, move_type mt) {
if (!t || m.is_bool(t) || !wval(t).can_set(new_value))
return false;
@ -553,27 +565,32 @@ namespace sls {
continue;
if (ctx.is_true(v) == v1)
continue;
if (!p || e == p)
if (e == p)
continue;
TRACE("bv", tout << "updated truth value " << v << ": " << mk_bounded_pp(e, m) << "\n";);
#if 0
unsigned num_unsat = ctx.unsat().size();
#if 0
TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";);
auto r = ctx.reward(v);
auto lit = sat::literal(v, !ctx.is_true(v));
bool is_bv_lit = is_bv_literal(lit);
verbose_stream() << "flip " << is_bv_literal(lit) << " " << mk_bounded_pp(e, m) << " " << lit << " " << r << " num unsat " << ctx.unsat().size() << "\n";
ctx.flip(v);
sat::bool_var_set rotated;
unsigned budget = 100;
bool rot = ctx.try_rotate(v, rotated, budget);
verbose_stream() << "try-rotate " << rot << " " << rotated.size() << "\n";
verbose_stream() << "flip " << ((!p || e == p) ? "top " : "not top ") << is_bv_literal(lit) << " " << mk_bounded_pp(e, m) << " " << lit << " " << r << " num unsat " << num_unsat << " -> " << ctx.unsat().size() << "\n";
verbose_stream() << "new unsat " << ctx.unsat().size() << "\n";
if (num_unsat < ctx.unsat().size()) {
verbose_stream() << "flip back\n";
ctx.flip(v);
}
#endif
#if 1
if (allow_costly_flips(mt))
ctx.flip(v);
#endif
}
m_ev.set_bool_value(to_app(e), v1);
}
@ -589,12 +606,20 @@ namespace sls {
}
m_in_update_stack.reset();
m_ev.clear_bool_values();
TRACE("bv", tout << reason << " " << mk_bounded_pp(t, m)
TRACE("bv", tout << mt << " " << mk_bounded_pp(t, m)
<< " := " << new_value
<< " score " << m_top_score << "\n";);
return true;
}
bool bv_lookahead::allow_costly_flips(move_type mt) {
if (mt == move_type::reset_t)
return true;
if (mt != move_type::random_t)
return false;
return m_stats.random_flip_count % 100 == 0;
}
void bv_lookahead::insert_update(expr* e) {
TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n");

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

@ -53,6 +53,7 @@ namespace sls {
unsigned m_moves = 0;
unsigned m_restarts = 0;
unsigned m_num_propagations = 0;
unsigned random_flip_count = 0;
};
struct bool_info {
@ -109,10 +110,15 @@ namespace sls {
void set_touched(app* e, unsigned t) { get_bool_info(e).touched = t; }
void inc_touched(app* e) { ++get_bool_info(e).touched; }
enum class move_type { random_t, guided_t, move_t, reset_t };
friend std::ostream& operator<<(std::ostream& out, move_type mt);
bool allow_costly_flips(move_type mt);
void try_set(expr* u, bvect const& new_value);
void try_flip(expr* u);
void add_updates(expr* u);
bool apply_update(expr* p, expr* t, bvect const& new_value, char const* reason);
bool apply_update(expr* p, expr* t, bvect const& new_value, move_type mt);
bool apply_random_move(ptr_vector<expr> const& vars);
bool apply_guided_move(ptr_vector<expr> const& vars);
bool apply_random_update(ptr_vector<expr> const& vars);

2
src/ast/sls/sls_context.h
View file

@ -69,6 +69,7 @@ namespace sls {
virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
virtual void flip(sat::bool_var v) = 0;
virtual bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) = 0;
virtual double reward(sat::bool_var v) = 0;
virtual double get_weigth(unsigned clause_idx) = 0;
virtual bool is_true(sat::literal lit) = 0;
@ -175,6 +176,7 @@ namespace sls {
void add_clause(expr* f);
void add_clause(sat::literal_vector const& lits);
void flip(sat::bool_var v) { s.flip(v); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) { return s.reward(v); }
indexed_uint_set const& unsat() const { return s.unsat(); }
unsigned rand() { return m_rand(); }

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

@ -148,6 +148,9 @@ namespace sls {
void flip(sat::bool_var v) override {
m_ddfw->flip(v);
}
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override {
return m_ddfw->try_rotate(v, rotated, budget);
}
double reward(sat::bool_var v) override { return m_ddfw->reward(v); }
double get_weigth(unsigned clause_idx) override { return m_ddfw->get_clause_info(clause_idx).m_weight; }
bool is_true(sat::literal lit) override {

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

@ -85,6 +85,7 @@ namespace sls {
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.flip(v); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.try_rotate(v, rotated, budget); }
double reward(sat::bool_var v) override { return m_ddfw.reward(v); }
double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }
bool is_true(sat::literal lit) override { return m_ddfw.get_value(lit.var()) != lit.sign(); }