mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
add sequential option for SLS, fixes to import/export methods SLS<->SMT
This commit is contained in:
Nikolaj Bjorner
parent
6a9d5910cb
commit
8e3b9f6686
16 changed files with 224 additions and 63 deletions
|
|
@ -50,6 +50,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
|
|||
m_threads_cube_frequency = p.threads_cube_frequency();
|
||||
m_core_validate = p.core_validate();
|
||||
m_sls_enable = p.sls_enable();
|
||||
m_sls_parallel = p.sls_parallel();
|
||||
m_logic = _p.get_sym("logic", m_logic);
|
||||
m_string_solver = p.string_solver();
|
||||
m_up_persist_clauses = p.up_persist_clauses();
|
||||
|
|
|
|||
|
|
@ -115,6 +115,7 @@ struct smt_params : public preprocessor_params,
|
|||
bool m_clause_proof = false;
|
||||
symbol m_proof_log;
|
||||
bool m_sls_enable = false;
|
||||
bool m_sls_parallel = true;
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
|
|||
|
|
@ -137,6 +137,7 @@ def_module_params(module_name='smt',
|
|||
('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'),
|
||||
('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'),
|
||||
('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'),
|
||||
('sls.parallel', BOOL, True, 'use sls co-processor in parallel or sequential with SMT engine'),
|
||||
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
|
||||
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
|
||||
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
|
||||
|
|
|
|||
|
|
@ -1193,9 +1193,9 @@ namespace smt {
|
|||
void rescale_bool_var_activity();
|
||||
|
||||
public:
|
||||
void inc_bvar_activity(bool_var v) {
|
||||
void inc_bvar_activity(bool_var v, double inc = 1.0) {
|
||||
double & act = m_activity[v];
|
||||
act += m_bvar_inc;
|
||||
act += m_bvar_inc * inc;
|
||||
if (act > ACTIVITY_LIMIT)
|
||||
rescale_bool_var_activity();
|
||||
m_case_split_queue->activity_increased_eh(v);
|
||||
|
|
|
|||
|
|
@ -1494,6 +1494,11 @@ bool theory_seq::internalize_term(app* term) {
|
|||
bool_var bv = ctx.mk_bool_var(term);
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
ctx.mark_as_relevant(bv);
|
||||
#if 1
|
||||
// experiment
|
||||
if (m_util.str.is_contains(term))
|
||||
init_length_limit_for_contains(term);
|
||||
#endif
|
||||
}
|
||||
|
||||
enode* e = nullptr;
|
||||
|
|
@ -1533,6 +1538,20 @@ void theory_seq::add_length(expr* l) {
|
|||
m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
|
||||
}
|
||||
|
||||
|
||||
void theory_seq::init_length_limit_for_contains(expr* c) {
|
||||
if (ctx.is_searching())
|
||||
return;
|
||||
expr* x, *y;
|
||||
VERIFY(m_util.str.is_contains(c, x, y));
|
||||
unsigned min_y = m_util.str.min_length(y);
|
||||
if (min_y > 0) {
|
||||
unsigned old_min_y = 0;
|
||||
m_length_limit_map.find(x, old_min_y);
|
||||
add_length_limit(x, old_min_y + min_y, false);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
Add length limit restrictions to sequence s.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -562,6 +562,7 @@ namespace smt {
|
|||
void enforce_length_coherence(enode* n1, enode* n2);
|
||||
|
||||
void add_length_limit(expr* s, unsigned k, bool is_searching);
|
||||
void init_length_limit_for_contains(expr* c);
|
||||
|
||||
// model-check the functions that convert integers to strings and the other way.
|
||||
void add_int_string(expr* e);
|
||||
|
|
|
|||
|
|
@ -37,13 +37,12 @@ namespace smt {
|
|||
return ctx.get_params();
|
||||
}
|
||||
|
||||
void theory_sls::initialize_value(expr* t, expr* v) {
|
||||
//ctx.user_propagate_initialize_value(t, v);
|
||||
void theory_sls::set_value(expr* t, expr* v) {
|
||||
ctx.user_propagate_initialize_value(t, v);
|
||||
}
|
||||
|
||||
void theory_sls::force_phase(sat::literal lit) {
|
||||
//
|
||||
// ctx.force_phase(lit);
|
||||
ctx.force_phase(lit);
|
||||
}
|
||||
|
||||
void theory_sls::set_has_new_best_phase(bool b) {
|
||||
|
|
@ -51,7 +50,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool theory_sls::get_best_phase(sat::bool_var v) {
|
||||
return false;
|
||||
return ctx.get_assignment(v) == l_true;
|
||||
}
|
||||
|
||||
expr* theory_sls::bool_var2expr(sat::bool_var v) {
|
||||
|
|
@ -61,6 +60,15 @@ namespace smt {
|
|||
void theory_sls::set_finished() {
|
||||
ctx.set_sls_completed();
|
||||
}
|
||||
|
||||
bool theory_sls::get_value(expr* v, expr_ref& value) {
|
||||
auto* n = ctx.get_enode(v);
|
||||
return n && ctx.get_value(n, value);
|
||||
}
|
||||
|
||||
void theory_sls::inc_activity(sat::bool_var v, double inc) {
|
||||
ctx.inc_bvar_activity(v, inc);
|
||||
}
|
||||
|
||||
unsigned theory_sls::get_num_bool_vars() const {
|
||||
return ctx.get_num_bool_vars();
|
||||
|
|
@ -85,7 +93,7 @@ namespace smt {
|
|||
m_smt_plugin->check(fmls, clauses);
|
||||
return;
|
||||
}
|
||||
if (!m_smt_plugin)
|
||||
if (!m_smt_plugin || !m_parallel_mode)
|
||||
return;
|
||||
if (!m_smt_plugin->completed())
|
||||
return;
|
||||
|
|
@ -103,18 +111,20 @@ namespace smt {
|
|||
for (; m_trail_lim < lits.size() && ctx.get_assign_level(lits[m_trail_lim]) == scope_lvl; ++m_trail_lim)
|
||||
m_smt_plugin->add_unit(lits[m_trail_lim]);
|
||||
}
|
||||
|
||||
++m_difference_score; // blindly assume we backtrack over initial clauses.
|
||||
#if 0
|
||||
if (ctx.has_new_best_phase())
|
||||
m_smt_plugin->import_phase_from_smt();
|
||||
|
||||
#endif
|
||||
|
||||
// m_smt_plugin->import_from_sls();
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_sls::init() {
|
||||
if (m_smt_plugin)
|
||||
finalize();
|
||||
smt_params p(ctx.get_fparams());
|
||||
m_parallel_mode = p.m_sls_parallel;
|
||||
m_smt_plugin = alloc(sls::smt_plugin, *this);
|
||||
m_checking = false;
|
||||
}
|
||||
|
|
@ -123,11 +133,52 @@ namespace smt {
|
|||
st.copy(m_st);
|
||||
}
|
||||
|
||||
void theory_sls::display(std::ostream& out) const {
|
||||
out << "theory-sls\n";
|
||||
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;
|
||||
bounded_run(m_restart_ls_steps);
|
||||
m_smt_plugin->sls_activity_to_smt();
|
||||
}
|
||||
m_difference_score = 0;
|
||||
m_difference_score_threshold = 1;
|
||||
}
|
||||
|
||||
void theory_sls::bounded_run(unsigned num_steps) {
|
||||
m_smt_plugin->bounded_run(num_steps);
|
||||
if (m_smt_plugin->result() == l_true) {
|
||||
m_smt_plugin->finalize(m_model, m_st);
|
||||
m_smt_plugin = nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
final_check_status theory_sls::final_check_eh() {
|
||||
if (m_parallel_mode || !m_smt_plugin)
|
||||
return FC_DONE;
|
||||
if (m_difference_score < m_difference_score_threshold + 100)
|
||||
return FC_DONE;
|
||||
|
||||
++m_difference_score_threshold;
|
||||
m_difference_score = 0;
|
||||
++m_num_guided_sls;
|
||||
|
||||
m_smt_plugin->smt_phase_to_sls();
|
||||
m_smt_plugin->smt_values_to_sls();
|
||||
bounded_run(m_final_check_ls_steps);
|
||||
dec_final_check_ls_steps();
|
||||
m_smt_plugin->sls_phase_to_smt();
|
||||
m_smt_plugin->sls_values_to_smt();
|
||||
if (m_num_guided_sls % 20 == 0)
|
||||
m_smt_plugin->sls_activity_to_smt();
|
||||
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
void theory_sls::display(std::ostream& out) const {
|
||||
out << "theory-sls\n";
|
||||
}
|
||||
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
|
|
@ -54,9 +54,30 @@ namespace smt {
|
|||
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_restart_sls_count = 0;
|
||||
unsigned m_difference_score = 0;
|
||||
unsigned m_difference_score_threshold = 0;
|
||||
unsigned m_num_guided_sls = 0;
|
||||
unsigned m_restart_ls_steps = 100000;
|
||||
unsigned m_restart_ls_steps_inc = 10000;
|
||||
unsigned m_restart_ls_steps_max = 300000;
|
||||
unsigned m_final_check_ls_steps = 30000;
|
||||
unsigned m_final_check_ls_steps_dec = 10000;
|
||||
unsigned m_final_check_ls_steps_min = 10000;
|
||||
::statistics m_st;
|
||||
|
||||
void finalize();
|
||||
void bounded_run(unsigned num_steps);
|
||||
void inc_restart_ls_steps() {
|
||||
if (m_restart_ls_steps < m_restart_ls_steps_max)
|
||||
m_restart_ls_steps += m_restart_ls_steps_inc;
|
||||
}
|
||||
void dec_final_check_ls_steps() {
|
||||
if (m_final_check_ls_steps > m_final_check_ls_steps_min)
|
||||
m_final_check_ls_steps -= m_final_check_ls_steps_dec;
|
||||
}
|
||||
|
||||
public:
|
||||
theory_sls(context& ctx);
|
||||
|
|
@ -75,17 +96,22 @@ namespace smt {
|
|||
bool internalize_term(app* term) override { return false; }
|
||||
void new_eq_eh(theory_var v1, theory_var v2) override {}
|
||||
void new_diseq_eh(theory_var v1, theory_var v2) override {}
|
||||
void restart_eh() override;
|
||||
final_check_status final_check_eh() override;
|
||||
|
||||
// sls::smt_context interface
|
||||
ast_manager& get_manager() override { return m; }
|
||||
params_ref get_params() override;
|
||||
void initialize_value(expr* t, expr* v) override;
|
||||
void set_value(expr* t, expr* v) override;
|
||||
void force_phase(sat::literal lit) override;
|
||||
void set_has_new_best_phase(bool b) override;
|
||||
bool get_best_phase(sat::bool_var v) override;
|
||||
expr* bool_var2expr(sat::bool_var v) override;
|
||||
void set_finished() override;
|
||||
unsigned get_num_bool_vars() const override;
|
||||
void inc_activity(sat::bool_var v, double inc) override;
|
||||
bool parallel_mode() const { return m_parallel_mode; }
|
||||
bool get_value(expr* v, expr_ref& value) override;
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue