diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h index a816ba518..d70a49d20 100644 --- a/src/ast/sls/sls_arith_base.h +++ b/src/ast/sls/sls_arith_base.h @@ -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) diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index 48ab3cb96..ae04142c7 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -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 dj = [&](std::ostream& out, void* j) { out << "lit " << to_literal(reinterpret_cast(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 args; - m_stack.reset(); for (auto t : ctx.subterms()) { args.reset(); if (is_app(t)) diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h index a9e5032d2..71b0aabe2 100644 --- a/src/ast/sls/sls_euf_plugin.h +++ b/src/ast/sls/sls_euf_plugin.h @@ -40,10 +40,6 @@ namespace sls { }; hashtable m_values; - - - bool m_incremental = false; - unsigned m_incremental_mode = 0; stats m_stats; scoped_ptr m_g; @@ -52,14 +48,8 @@ namespace sls { scoped_ptr 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)(l.index() << 4)); }; @@ -88,8 +78,6 @@ namespace sls { void collect_statistics(statistics& st) const override; void reset_statistics() override; - - scoped_ptr& egraph() { return m_g; } }; diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index b13376004..854366609 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -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') diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index a475a551f..f9234f75d 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -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) { diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index 65b4aef07..f58510522 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -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;