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

take 1 on flip conditions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-31 11:44:38 -08:00
parent a511b8bcf0
commit b415b82625
7 changed files with 71 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/ast/sls/sls_basic_plugin.cpp
View file

@ -44,8 +44,17 @@ namespace sls {
void basic_plugin::register_term(expr* e) {
expr* c, * th, * el;
if (m.is_ite(e, c, th, el) && !m.is_bool(e)) {
ctx.add_clause(m.mk_or(mk_not(m, c), m.mk_eq(e, th)));
ctx.add_clause(m.mk_or(c, m.mk_eq(e, el)));
auto eq_th = expr_ref(m.mk_eq(e, th), m);
auto eq_el = expr_ref(m.mk_eq(e, el), m);
ctx.add_clause(m.mk_or(mk_not(m, c), eq_th));
ctx.add_clause(m.mk_or(c, eq_el));
#if 0
auto eq_th_el = expr_ref(m.mk_eq(th, el), m);
verbose_stream() << mk_bounded_pp(eq_th_el, m) << "\n";
ctx.add_clause(m.mk_or(eq_th_el, c, m.mk_not(eq_th)));
ctx.add_clause(m.mk_or(eq_th_el, m.mk_not(c), m.mk_not(eq_el)));
#endif
}
}
@ -178,8 +187,16 @@ namespace sls {
if (m.is_xor(e) && eval_xor(e) == ctx.get_value(e))
return true;
if (m.is_ite(e) && eval_ite(e) == ctx.get_value(e))
if (m.is_ite(e) && !m.is_bool(e)) {
if (eval_ite(e) == ctx.get_value(e))
return true;
if (try_repair(e, 1))
return true;
if (try_repair(e, 2))
return true;
ctx.flip(ctx.atom2bool_var(e->get_arg(0)));
return true;
}
if (m.is_distinct(e) && eval_distinct(e) == ctx.get_value(e))
return true;
unsigned n = e->get_num_args();

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

@ -1977,13 +1977,7 @@ namespace sls {
if (v.eval == v.bits())
return true;
for (unsigned i = 0; i < v.nw; ++i)
if (0 != (v.fixed(i) & (v.bits(i) ^ v.eval[i])))
return false;
if (!v.commit_eval_check_tabu())
return false;
v.commit_eval_ignore_tabu();
ctx.new_value_eh(e);
return true;
}

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

@ -38,6 +38,7 @@ namespace sls {
* before any other propagation with the main BV solver.
*/
void bv_lookahead::start_propagation() {
//verbose_stream() << "start_propagation " << m_stats.m_num_propagations << "\n";
if (m_stats.m_num_propagations++ % m_config.propagation_base == 0)
search();
}
@ -54,6 +55,8 @@ namespace sls {
updt_params(ctx.get_params());
rescore();
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
TRACE("bv", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
IF_VERBOSE(3, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
while (m.inc() && m_stats.m_moves < m_config.max_moves) {
m_stats.m_moves++;
@ -62,8 +65,8 @@ namespace sls {
// get candidate variables
auto& vars = get_candidate_uninterp();
if (vars.empty())
return;
if (vars.empty())
return;
// random walk
if (ctx.rand(2047) < m_config.wp && apply_random_move(vars))
@ -73,6 +76,9 @@ namespace sls {
if (apply_guided_move(vars))
continue;
if (apply_flip())
return;
// bail out if no progress, and try random update
if (apply_random_update(get_candidate_uninterp()))
recalibrate_weights();
@ -133,6 +139,17 @@ namespace sls {
return apply_update(e, m_v_updated, "random move");
}
bool bv_lookahead::apply_flip() {
if (!m_last_atom)
return false;
auto const& cond = m_ev.terms.condition_occurs(m_last_atom);
if (cond.empty())
return false;
expr* e = cond[ctx.rand(cond.size())];
ctx.flip(ctx.atom2bool_var(e));
return true;
}
/**
* Retrieve a candidate top-level predicate that is false, give preference to
* those with high score, but back off if they are frequently chosen.
@ -163,13 +180,15 @@ namespace sls {
if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0)
e = to_app(ctx.atom(lit.var()));
}
CTRACE("bv", !e, tout << "no candidate\n";
ctx.display(tout);
display_weights(tout););
CTRACE("bv", !e, ; display_weights(ctx.display(tout << "no candidate\n")););
m_last_atom = e;
if (!e)
return m_empty_vars;
auto const& vars = m_ev.terms.uninterp_occurs(e);
TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";

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

@ -39,7 +39,7 @@ namespace sls {
bool early_prune = true;
unsigned max_moves = 0;
unsigned max_moves_base = 800;
unsigned propagation_base = 10000;
unsigned propagation_base = 1000;
bool ucb = true;
double ucb_constant = 1.0;
double ucb_forget = 0.1;
@ -74,6 +74,7 @@ namespace sls {
double m_best_score = 0, m_top_score = 0;
bvect m_best_value;
expr* m_best_expr = nullptr;
expr* m_last_atom = nullptr;
ptr_vector<expr> m_empty_vars;
obj_map<expr, bool_info> m_bool_info;
expr_mark m_is_root;
@ -112,6 +113,7 @@ namespace sls {
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);
bool apply_flip();
ptr_vector<expr> const& get_candidate_uninterp();
void check_restart();

9
src/ast/sls/sls_bv_plugin.cpp
View file

@ -40,14 +40,7 @@ namespace sls {
}
bool bv_plugin::is_bv_predicate(expr* e) {
if (!e || !is_app(e))
return false;
auto a = to_app(e);
if (a->get_family_id() == bv.get_family_id())
return true;
if (m.is_eq(e) && bv.is_bv(a->get_arg(0)))
return true;
return false;
return m_terms.is_bv_predicate(e);
}
void bv_plugin::start_propagation() {

31
src/ast/sls/sls_bv_terms.cpp
View file

@ -114,6 +114,17 @@ namespace sls {
return r;
}
bool bv_terms::is_bv_predicate(expr* e) const {
if (!e || !is_app(e) || !m.is_bool(e))
return false;
auto a = to_app(e);
if (a->get_family_id() == bv.get_family_id())
return true;
if (m.is_eq(e) && bv.is_bv(a->get_arg(0)))
return true;
return false;
}
ptr_vector<expr> const& bv_terms::uninterp_occurs(expr* e) {
unsigned id = e->get_id();
m_uninterp_occurs.reserve(id + 1);
@ -133,21 +144,13 @@ namespace sls {
}
void bv_terms::register_uninterp(expr* e) {
if (!m.is_bool(e))
return;
expr* x, *y;
if (m.is_eq(e, x, y) && bv.is_bv(x))
;
else if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid())
;
else
if (!is_bv_predicate(e))
return;
m_uninterp_occurs.reserve(e->get_id() + 1);
m_condition_occurs.reserve(e->get_id() + 1);
auto& occs = m_uninterp_occurs[e->get_id()];
auto& cond_occs = m_condition_occurs[e->get_id()];
ptr_vector<expr> todo;
ptr_vector<expr> todo, cond_todo;
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
expr_mark marked;
expr* c, * th, * el;
@ -156,7 +159,13 @@ namespace sls {
if (marked.is_marked(e))
continue;
marked.mark(e);
if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid()) {
if (is_bv_predicate(e))
cond_occs.push_back(e);
else if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid()) {
for (expr* arg : *to_app(e))
todo.push_back(arg);
}
else if (m.is_bool(e) && to_app(e)->get_family_id() == basic_family_id) {
for (expr* arg : *to_app(e))
todo.push_back(arg);
}

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

@ -49,6 +49,8 @@ namespace sls {
void register_term(expr* e);
bool is_bv_predicate(expr* e) const;
expr_ref_vector& axioms() { return m_axioms; }
ptr_vector<expr> const& uninterp_occurs(expr* e);