mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
enable value import in parallel mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e32f685f14
commit
4d33f442b9
|
@ -33,6 +33,7 @@ namespace sls {
|
|||
m_smt2sls_tr(m, m_sls),
|
||||
m_sls2sync_tr(m_sls, m_sync),
|
||||
m_sls2smt_tr(m_sls, m),
|
||||
m_sync2sls_tr(m_sync, m_sls),
|
||||
m_sync_uninterp(m_sync),
|
||||
m_sls_uninterp(m_sls),
|
||||
m_sync_values(m_sync),
|
||||
|
@ -47,7 +48,7 @@ namespace sls {
|
|||
void smt_plugin::check(expr_ref_vector const& fmls, vector <sat::literal_vector> const& clauses) {
|
||||
SASSERT(!m_ddfw);
|
||||
// set up state for local search theory_sls here
|
||||
|
||||
|
||||
m_result = l_undef;
|
||||
m_completed = false;
|
||||
m_units.reset();
|
||||
|
@ -225,6 +226,12 @@ namespace sls {
|
|||
m_has_new_sat_phase = false;
|
||||
updated = true;
|
||||
}
|
||||
if (m_has_new_smt_values) {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
export_values_to_sls();
|
||||
m_has_new_smt_values = false;
|
||||
updated = true;
|
||||
}
|
||||
return updated;
|
||||
}
|
||||
|
||||
|
@ -240,6 +247,18 @@ namespace sls {
|
|||
#endif
|
||||
}
|
||||
|
||||
void smt_plugin::export_values_to_sls() {
|
||||
IF_VERBOSE(2, verbose_stream() << "SMT -> SLS values\n");
|
||||
for (auto [var, value] : m_sync_var_values) {
|
||||
expr_ref var1(m_sls), value1(m_sls);
|
||||
var1 = m_sync2sls_tr(var.get());
|
||||
value1 = m_sync2sls_tr(value.get());
|
||||
if (!var1 || !value1)
|
||||
continue;
|
||||
m_context.set_value(var1, value1);
|
||||
}
|
||||
}
|
||||
|
||||
void smt_plugin::smt_phase_to_sls() {
|
||||
#if 0
|
||||
IF_VERBOSE(2, verbose_stream() << "SMT -> SLS phase\n");
|
||||
|
@ -254,6 +273,21 @@ namespace sls {
|
|||
}
|
||||
|
||||
void smt_plugin::smt_values_to_sls() {
|
||||
|
||||
if (ctx.parallel_mode()) {
|
||||
std::scoped_lock lock(m_mutex);
|
||||
m_sync_var_values.reset();
|
||||
for (auto const& [t, t_sync] : m_smt2sync_uninterp) {
|
||||
expr_ref val_t(m);
|
||||
if (!ctx.get_smt_value(t, val_t))
|
||||
continue;
|
||||
auto t_sls = expr_ref(m_smt2sls_tr(t), m_sls);
|
||||
auto val_sls = expr_ref(m_smt2sls_tr(val_t.get()), m_sls);
|
||||
m_sync_var_values.push_back({ t_sls, val_sls });
|
||||
}
|
||||
m_has_new_smt_values = true;
|
||||
return;
|
||||
}
|
||||
#if 0
|
||||
if (m_value_smt2sls_delay < m_value_smt2sls_delay_threshold) {
|
||||
m_value_smt2sls_delay++;
|
||||
|
@ -267,7 +301,7 @@ namespace sls {
|
|||
expr_ref val_t(m);
|
||||
if (!ctx.get_smt_value(t, val_t))
|
||||
continue;
|
||||
expr* t_sls = m_smt2sls_tr(t);
|
||||
auto t_sls = expr_ref(m_smt2sls_tr(t), m_sls);
|
||||
auto val_sls = expr_ref(m_smt2sls_tr(val_t.get()), m_sls);
|
||||
m_context.set_value(t_sls, val_sls);
|
||||
}
|
||||
|
|
|
@ -53,7 +53,7 @@ namespace sls {
|
|||
ast_manager& m;
|
||||
ast_manager m_sls;
|
||||
ast_manager m_sync;
|
||||
ast_translation m_smt2sync_tr, m_smt2sls_tr, m_sls2sync_tr, m_sls2smt_tr;
|
||||
ast_translation m_smt2sync_tr, m_smt2sls_tr, m_sls2sync_tr, m_sls2smt_tr, m_sync2sls_tr;
|
||||
expr_ref_vector m_sync_uninterp, m_sls_uninterp;
|
||||
expr_ref_vector m_sync_values;
|
||||
sat::ddfw* m_ddfw = nullptr;
|
||||
|
@ -73,11 +73,13 @@ namespace sls {
|
|||
unsigned m_min_unsat_size = UINT_MAX;
|
||||
obj_map<expr, expr*> m_sls2sync_uninterp; // hashtable from sls-uninterp to sync uninterp
|
||||
obj_map<expr, expr*> m_smt2sync_uninterp; // hashtable from external uninterp to sync uninterp
|
||||
vector<std::pair<expr_ref, expr_ref>> m_sync_var_values;
|
||||
std::atomic<bool> m_has_new_sls_values = false;
|
||||
uint_set m_shared_bool_vars, m_shared_terms;
|
||||
svector<bool> m_sat_phase;
|
||||
std::atomic<bool> m_has_new_sat_phase = false;
|
||||
std::atomic<bool> m_has_new_sls_phase = false;
|
||||
std::atomic<bool> m_has_new_smt_values = false;
|
||||
svector<bool> m_sls_phase;
|
||||
svector<double> m_rewards;
|
||||
svector<sat::bool_var> m_smt_bool_var2sls_bool_var, m_sls_bool_var2smt_bool_var;
|
||||
|
@ -91,6 +93,7 @@ namespace sls {
|
|||
|
||||
void import_phase_from_smt();
|
||||
void import_values_from_sls();
|
||||
void export_values_to_sls();
|
||||
void export_values_from_sls();
|
||||
void export_phase_from_sls();
|
||||
void import_activity_from_sls();
|
||||
|
|
|
@ -169,10 +169,14 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_sls::run_guided_sls() {
|
||||
m_smt_plugin->smt_values_to_sls();
|
||||
if (m_parallel_mode)
|
||||
return;
|
||||
|
||||
++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();
|
||||
|
||||
bounded_run(m_final_check_ls_steps);
|
||||
dec_final_check_ls_steps();
|
||||
if (m_smt_plugin) {
|
||||
|
@ -225,7 +229,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
final_check_status theory_sls::final_check_eh() {
|
||||
if (m_parallel_mode || !m_smt_plugin)
|
||||
if (!m_smt_plugin)
|
||||
return FC_DONE;
|
||||
++m_after_resolve_decide_count;
|
||||
if (m_after_resolve_decide_gap > m_after_resolve_decide_count)
|
||||
|
|
Loading…
Reference in a new issue