mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
remove incremental mode from EUF, include statistics about restart vs propagation calls to sls
This commit is contained in:
Nikolaj Bjorner
parent
c7ea4964f2
commit
84447b7031
6 changed files with 17 additions and 123 deletions
|
|
@ -102,9 +102,9 @@ namespace sls {
|
|||
if (-m_range < n && n < m_range)
|
||||
return true;
|
||||
bool result = false;
|
||||
if (m_lo && !m_hi)
|
||||
if (m_lo)
|
||||
result = n < m_lo->value + m_range;
|
||||
else if (!m_lo && m_hi)
|
||||
if (!result && m_hi)
|
||||
result = n > m_hi->value - m_range;
|
||||
#if 0
|
||||
if (!result)
|
||||
|
|
|
|||
|
|
@ -38,21 +38,16 @@ namespace sls {
|
|||
euf_plugin::~euf_plugin() {}
|
||||
|
||||
void euf_plugin::initialize() {
|
||||
sls_params sp(ctx.get_params());
|
||||
m_incremental_mode = sp.euf_incremental();
|
||||
m_incremental = 1 == m_incremental_mode;
|
||||
IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental_mode << "\n");
|
||||
}
|
||||
|
||||
void euf_plugin::start_propagation() {
|
||||
if (m_incremental_mode == 2)
|
||||
m_incremental = !m_incremental;
|
||||
|
||||
m_g = alloc(euf::egraph, m);
|
||||
std::function<void(std::ostream&, void*)> dj = [&](std::ostream& out, void* j) {
|
||||
out << "lit " << to_literal(reinterpret_cast<size_t*>(j));
|
||||
};
|
||||
m_g->set_display_justification(dj);
|
||||
init_egraph(*m_g, !m_incremental);
|
||||
init_egraph(*m_g, true);
|
||||
}
|
||||
|
||||
void euf_plugin::register_term(expr* e) {
|
||||
|
|
@ -84,11 +79,6 @@ namespace sls {
|
|||
return true;
|
||||
}
|
||||
|
||||
void euf_plugin::propagate_literal_incremental(sat::literal lit) {
|
||||
m_replay_stack.push_back(lit);
|
||||
replay();
|
||||
}
|
||||
|
||||
sat::literal euf_plugin::resolve_conflict() {
|
||||
auto& g = *m_g;
|
||||
SASSERT(g.inconsistent());
|
||||
|
|
@ -128,92 +118,7 @@ namespace sls {
|
|||
return flit;
|
||||
}
|
||||
|
||||
void euf_plugin::resolve() {
|
||||
auto& g = *m_g;
|
||||
if (!g.inconsistent())
|
||||
return;
|
||||
|
||||
auto flit = resolve_conflict();
|
||||
sat::literal slit;
|
||||
if (flit == sat::null_literal)
|
||||
return;
|
||||
do {
|
||||
slit = m_stack.back();
|
||||
g.pop(1);
|
||||
m_replay_stack.push_back(slit);
|
||||
m_stack.pop_back();
|
||||
}
|
||||
while (slit != flit);
|
||||
ctx.flip(flit.var());
|
||||
m_replay_stack.back().neg();
|
||||
|
||||
}
|
||||
|
||||
void euf_plugin::replay() {
|
||||
while (!m_replay_stack.empty()) {
|
||||
auto l = m_replay_stack.back();
|
||||
m_replay_stack.pop_back();
|
||||
propagate_literal_incremental_step(l);
|
||||
if (m_g->inconsistent())
|
||||
resolve();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void euf_plugin::propagate_literal_incremental_step(sat::literal lit) {
|
||||
SASSERT(ctx.is_true(lit));
|
||||
auto e = ctx.atom(lit.var());
|
||||
expr* x, * y;
|
||||
auto& g = *m_g;
|
||||
|
||||
if (!e)
|
||||
return;
|
||||
|
||||
TRACE("euf", tout << "propagate " << lit << "\n");
|
||||
m_stack.push_back(lit);
|
||||
g.push();
|
||||
if (m.is_eq(e, x, y)) {
|
||||
if (lit.sign())
|
||||
g.new_diseq(g.find(e), to_ptr(lit));
|
||||
else
|
||||
g.merge(g.find(x), g.find(y), to_ptr(lit));
|
||||
g.merge(g.find(e), g.find(m.mk_bool_val(!lit.sign())), to_ptr(lit));
|
||||
}
|
||||
else if (!lit.sign() && m.is_distinct(e)) {
|
||||
auto n = to_app(e)->get_num_args();
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
expr* a = to_app(e)->get_arg(i);
|
||||
for (unsigned j = i + 1; j < n; ++j) {
|
||||
auto b = to_app(e)->get_arg(j);
|
||||
expr_ref eq(m.mk_eq(a, b), m);
|
||||
auto c = g.find(eq);
|
||||
if (!c) {
|
||||
euf::enode* args[2] = { g.find(a), g.find(b) };
|
||||
c = g.mk(eq, 0, 2, args);
|
||||
}
|
||||
g.new_diseq(c, to_ptr(lit));
|
||||
g.merge(c, g.find(m.mk_false()), to_ptr(lit));
|
||||
}
|
||||
}
|
||||
}
|
||||
// else if (m.is_bool(e) && is_app(e) && to_app(e)->get_family_id() == basic_family_id)
|
||||
// ;
|
||||
else {
|
||||
auto a = g.find(e);
|
||||
auto b = g.find(m.mk_bool_val(!lit.sign()));
|
||||
g.merge(a, b, to_ptr(lit));
|
||||
}
|
||||
g.propagate();
|
||||
}
|
||||
|
||||
void euf_plugin::propagate_literal(sat::literal lit) {
|
||||
if (m_incremental)
|
||||
propagate_literal_incremental(lit);
|
||||
else
|
||||
propagate_literal_non_incremental(lit);
|
||||
}
|
||||
|
||||
void euf_plugin::propagate_literal_non_incremental(sat::literal lit) {
|
||||
SASSERT(ctx.is_true(lit));
|
||||
auto e = ctx.atom(lit.var());
|
||||
expr* x, * y;
|
||||
|
|
@ -272,7 +177,6 @@ namespace sls {
|
|||
|
||||
void euf_plugin::init_egraph(euf::egraph& g, bool merge_eqs) {
|
||||
ptr_vector<euf::enode> args;
|
||||
m_stack.reset();
|
||||
for (auto t : ctx.subterms()) {
|
||||
args.reset();
|
||||
if (is_app(t))
|
||||
|
|
|
|||
|
|
@ -40,10 +40,6 @@ namespace sls {
|
|||
};
|
||||
hashtable<app*, value_hash, value_eq> m_values;
|
||||
|
||||
|
||||
|
||||
bool m_incremental = false;
|
||||
unsigned m_incremental_mode = 0;
|
||||
stats m_stats;
|
||||
|
||||
scoped_ptr<euf::egraph> m_g;
|
||||
|
|
@ -52,14 +48,8 @@ namespace sls {
|
|||
scoped_ptr<expr_ref_vector> m_pinned;
|
||||
|
||||
void init_egraph(euf::egraph& g, bool merge_eqs);
|
||||
sat::literal_vector m_stack, m_replay_stack;
|
||||
void propagate_literal_incremental(sat::literal lit);
|
||||
void propagate_literal_incremental_step(sat::literal lit);
|
||||
void resolve();
|
||||
sat::literal resolve_conflict();
|
||||
void replay();
|
||||
|
||||
void propagate_literal_non_incremental(sat::literal lit);
|
||||
bool is_user_sort(sort* s) { return s->get_family_id() == user_sort_family_id; }
|
||||
|
||||
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
|
||||
|
|
@ -88,8 +78,6 @@ namespace sls {
|
|||
void collect_statistics(statistics& st) const override;
|
||||
void reset_statistics() override;
|
||||
|
||||
|
||||
|
||||
scoped_ptr<euf::egraph>& egraph() { return m_g; }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,6 @@ def_module_params('sls',
|
|||
('early_prune', BOOL, 1, 'use early pruning for score prediction'),
|
||||
('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
|
||||
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
|
||||
('euf_incremental', UINT, 0, '0 non-incremental, 1 incremental, 2 alternating EUF resolver'),
|
||||
('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
|
||||
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
|
||||
('random_seed', UINT, 0, 'random seed')
|
||||
|
|
|
|||
|
|
@ -164,7 +164,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_sls::run_guided_sls() {
|
||||
++m_num_guided_sls;
|
||||
++m_stats.m_num_guided_sls;
|
||||
m_smt_plugin->smt_phase_to_sls();
|
||||
m_smt_plugin->smt_units_to_sls();
|
||||
m_smt_plugin->smt_values_to_sls();
|
||||
|
|
@ -173,7 +173,7 @@ namespace smt {
|
|||
if (m_smt_plugin) {
|
||||
m_smt_plugin->sls_phase_to_smt();
|
||||
m_smt_plugin->sls_values_to_smt();
|
||||
if (m_num_guided_sls % 20 == 0)
|
||||
if (m_stats.m_num_guided_sls % 20 == 0)
|
||||
m_smt_plugin->sls_activity_to_smt();
|
||||
}
|
||||
}
|
||||
|
|
@ -192,21 +192,22 @@ namespace smt {
|
|||
m_smt_plugin->collect_statistics(st);
|
||||
else
|
||||
st.copy(m_st);
|
||||
st.update("sls-num-guided-search", m_stats.m_num_guided_sls);
|
||||
st.update("sls-num-restart-search", m_stats.m_num_restart_sls);
|
||||
}
|
||||
|
||||
void theory_sls::restart_eh() {
|
||||
if (m_parallel_mode || !m_smt_plugin)
|
||||
return;
|
||||
|
||||
if (ctx.m_stats.m_num_restarts >= m_threshold + 5) {
|
||||
m_threshold *= 2;
|
||||
if (ctx.m_stats.m_num_restarts >= m_restart_gap + 5) {
|
||||
m_restart_gap *= 2;
|
||||
m_smt_plugin->smt_units_to_sls();
|
||||
++m_stats.m_num_restart_sls;
|
||||
bounded_run(m_restart_ls_steps);
|
||||
if (m_smt_plugin)
|
||||
m_smt_plugin->sls_activity_to_smt();
|
||||
}
|
||||
m_difference_score = 0;
|
||||
m_difference_score_threshold = 1;
|
||||
}
|
||||
|
||||
void theory_sls::bounded_run(unsigned num_steps) {
|
||||
|
|
|
|||
|
|
@ -50,15 +50,17 @@ namespace smt {
|
|||
namespace smt {
|
||||
|
||||
class theory_sls : public theory, public sls::smt_context {
|
||||
struct stats {
|
||||
unsigned m_num_guided_sls = 0;
|
||||
unsigned m_num_restart_sls = 0;
|
||||
};
|
||||
stats m_stats;
|
||||
model_ref m_model;
|
||||
sls::smt_plugin* m_smt_plugin = nullptr;
|
||||
unsigned m_trail_lim = 0;
|
||||
bool m_checking = false;
|
||||
bool m_parallel_mode = true;
|
||||
unsigned m_threshold = 1;
|
||||
unsigned m_difference_score = 0;
|
||||
unsigned m_difference_score_threshold = 0;
|
||||
unsigned m_num_guided_sls = 0;
|
||||
unsigned m_restart_gap = 1;
|
||||
unsigned m_restart_ls_steps = 100000;
|
||||
unsigned m_restart_ls_steps_inc = 10000;
|
||||
unsigned m_restart_ls_steps_max = 300000;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue