mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 07:06:28 +00:00
Merge ab523fce54 into c67bb140dc
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
108f302716
20 changed files with 2051 additions and 390 deletions
|
|
@ -28,7 +28,6 @@ z3_add_component(params
|
|||
seq_rewriter_params.pyg
|
||||
sls_params.pyg
|
||||
smt_params_helper.pyg
|
||||
smt_parallel_params.pyg
|
||||
solver_params.pyg
|
||||
tactic_params.pyg
|
||||
EXTRA_REGISTER_MODULE_HEADERS
|
||||
|
|
|
|||
|
|
@ -1,12 +0,0 @@
|
|||
def_module_params('smt_parallel',
|
||||
export=True,
|
||||
description='Experimental parameters for parallel solving',
|
||||
params=(
|
||||
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
|
||||
('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
|
||||
('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
|
||||
('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
|
||||
('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'),
|
||||
('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'),
|
||||
('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'),
|
||||
))
|
||||
|
|
@ -132,6 +132,8 @@ namespace sat {
|
|||
m_best_phase.reset();
|
||||
m_phase.reset();
|
||||
m_prev_phase.reset();
|
||||
m_phase_birthdate.reset();
|
||||
m_best_phase_birthdate.reset();
|
||||
m_assigned_since_gc.reset();
|
||||
m_last_conflict.reset();
|
||||
m_last_propagation.reset();
|
||||
|
|
@ -161,6 +163,8 @@ namespace sat {
|
|||
m_phase[v] = src.m_phase[v];
|
||||
m_best_phase[v] = src.m_best_phase[v];
|
||||
m_prev_phase[v] = src.m_prev_phase[v];
|
||||
m_phase_birthdate[v] = src.m_phase_birthdate[v];
|
||||
m_best_phase_birthdate[v] = src.m_best_phase_birthdate[v];
|
||||
|
||||
// inherit activity:
|
||||
m_activity[v] = src.m_activity[v];
|
||||
|
|
@ -267,6 +271,8 @@ namespace sat {
|
|||
m_phase[v] = false;
|
||||
m_best_phase[v] = false;
|
||||
m_prev_phase[v] = false;
|
||||
m_phase_birthdate[v] = 0;
|
||||
m_best_phase_birthdate[v] = 0;
|
||||
m_assigned_since_gc[v] = false;
|
||||
m_last_conflict[v] = 0;
|
||||
m_last_propagation[v] = 0;
|
||||
|
|
@ -308,6 +314,8 @@ namespace sat {
|
|||
m_phase.push_back(false);
|
||||
m_best_phase.push_back(false);
|
||||
m_prev_phase.push_back(false);
|
||||
m_phase_birthdate.push_back(0);
|
||||
m_best_phase_birthdate.push_back(0);
|
||||
m_assigned_since_gc.push_back(false);
|
||||
m_last_conflict.push_back(0);
|
||||
m_last_propagation.push_back(0);
|
||||
|
|
@ -645,6 +653,26 @@ namespace sat {
|
|||
return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size();
|
||||
}
|
||||
|
||||
void solver::set_phase(literal l) {
|
||||
if (l.var() >= num_vars())
|
||||
return;
|
||||
bool value = !l.sign();
|
||||
set_phase(l.var(), value);
|
||||
set_best_phase(l.var(), value);
|
||||
}
|
||||
|
||||
void solver::set_phase(bool_var v, bool value) {
|
||||
if (m_phase[v] != value)
|
||||
m_phase_birthdate[v] = m_stats.m_conflicts;
|
||||
m_phase[v] = value;
|
||||
}
|
||||
|
||||
void solver::set_best_phase(bool_var v, bool value) {
|
||||
if (m_best_phase[v] != value)
|
||||
m_best_phase_birthdate[v] = m_stats.m_conflicts;
|
||||
m_best_phase[v] = value;
|
||||
}
|
||||
|
||||
struct solver::cmp_activity {
|
||||
solver& s;
|
||||
cmp_activity(solver& s):s(s) {}
|
||||
|
|
@ -896,7 +924,7 @@ namespace sat {
|
|||
m_assignment[(~l).index()] = l_false;
|
||||
bool_var v = l.var();
|
||||
m_justification[v] = j;
|
||||
m_phase[v] = !l.sign();
|
||||
set_phase(v, !l.sign());
|
||||
m_assigned_since_gc[v] = true;
|
||||
m_trail.push_back(l);
|
||||
|
||||
|
|
@ -904,17 +932,17 @@ namespace sat {
|
|||
case BH_VSIDS:
|
||||
break;
|
||||
case BH_CHB:
|
||||
m_last_propagation[v] = m_stats.m_conflict;
|
||||
m_last_propagation[v] = m_stats.m_conflicts;
|
||||
break;
|
||||
}
|
||||
|
||||
if (m_config.m_anti_exploration) {
|
||||
uint64_t age = m_stats.m_conflict - m_canceled[v];
|
||||
uint64_t age = m_stats.m_conflicts - m_canceled[v];
|
||||
if (age > 0) {
|
||||
double decay = pow(0.95, static_cast<double>(age));
|
||||
set_activity(v, static_cast<unsigned>(m_activity[v] * decay));
|
||||
// NB. MapleSAT does not update canceled.
|
||||
m_canceled[v] = m_stats.m_conflict;
|
||||
m_canceled[v] = m_stats.m_conflicts;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1378,8 +1406,10 @@ namespace sat {
|
|||
lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr);
|
||||
auto const& mdl = m_local_search->get_model();
|
||||
if (mdl.size() == m_best_phase.size()) {
|
||||
for (unsigned i = 0; i < m_best_phase.size(); ++i)
|
||||
m_best_phase[i] = l_true == mdl[i];
|
||||
for (unsigned i = 0; i < m_best_phase.size(); ++i) {
|
||||
bool is_true = l_true == mdl[i];
|
||||
set_best_phase(i, is_true);
|
||||
}
|
||||
|
||||
if (r == l_true) {
|
||||
m_conflicts_since_restart = 0;
|
||||
|
|
@ -1671,12 +1701,12 @@ namespace sat {
|
|||
while (!m_case_split_queue.empty()) {
|
||||
if (m_config.m_anti_exploration) {
|
||||
next = m_case_split_queue.min_var();
|
||||
auto age = m_stats.m_conflict - m_canceled[next];
|
||||
auto age = m_stats.m_conflicts - m_canceled[next];
|
||||
while (age > 0) {
|
||||
set_activity(next, static_cast<unsigned>(m_activity[next] * pow(0.95, static_cast<double>(age))));
|
||||
m_canceled[next] = m_stats.m_conflict;
|
||||
m_canceled[next] = m_stats.m_conflicts;
|
||||
next = m_case_split_queue.min_var();
|
||||
age = m_stats.m_conflict - m_canceled[next];
|
||||
age = m_stats.m_conflicts - m_canceled[next];
|
||||
}
|
||||
}
|
||||
next = m_case_split_queue.next_var();
|
||||
|
|
@ -1714,6 +1744,32 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
uint64_t solver::get_preferred_phase_birthdate(bool_var v) const {
|
||||
bool use_best =
|
||||
m_config.m_phase == PS_FROZEN ||
|
||||
((m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH) && m_search_state == s_sat);
|
||||
return use_best ? m_best_phase_birthdate[v] : m_phase_birthdate[v];
|
||||
}
|
||||
|
||||
void solver::get_backbone_candidates(literal_vector& lits, unsigned max_num) {
|
||||
struct candidate {
|
||||
literal lit;
|
||||
uint64_t age;
|
||||
};
|
||||
svector<candidate> cands;
|
||||
uint64_t now = m_stats.m_conflicts;
|
||||
for (bool_var v = 0; v < num_vars(); ++v) {
|
||||
if (value(v) != l_undef || was_eliminated(v))
|
||||
continue;
|
||||
bool is_pos = guess(v);
|
||||
cands.push_back({ literal(v, !is_pos), now - get_preferred_phase_birthdate(v) });
|
||||
}
|
||||
std::stable_sort(cands.begin(), cands.end(),
|
||||
[](candidate const& a, candidate const& b) { return a.age > b.age; });
|
||||
for (unsigned i = 0; i < cands.size() && i < max_num; ++i)
|
||||
lits.push_back(cands[i].lit);
|
||||
}
|
||||
|
||||
bool solver::decide() {
|
||||
bool_var next;
|
||||
lbool phase = l_undef;
|
||||
|
|
@ -2145,8 +2201,9 @@ namespace sat {
|
|||
for (bool_var v = 0; v < num; ++v) {
|
||||
if (!was_eliminated(v)) {
|
||||
m_model[v] = value(v);
|
||||
m_phase[v] = value(v) == l_true;
|
||||
m_best_phase[v] = value(v) == l_true;
|
||||
bool is_true = value(v) == l_true;
|
||||
set_phase(v, is_true);
|
||||
set_best_phase(v, is_true);
|
||||
}
|
||||
}
|
||||
TRACE(sat_mc_bug, m_mc.display(tout););
|
||||
|
|
@ -2274,7 +2331,7 @@ namespace sat {
|
|||
m_restart_logs++;
|
||||
|
||||
std::stringstream strm;
|
||||
strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " "
|
||||
strm << "(sat.stats " << std::setw(6) << m_stats.m_conflicts << " "
|
||||
<< std::setw(6) << m_stats.m_decision << " "
|
||||
<< std::setw(4) << m_stats.m_restart
|
||||
<< mk_stat(*this)
|
||||
|
|
@ -2432,7 +2489,7 @@ namespace sat {
|
|||
m_conflicts_since_init++;
|
||||
m_conflicts_since_restart++;
|
||||
m_conflicts_since_gc++;
|
||||
m_stats.m_conflict++;
|
||||
m_stats.m_conflicts++;
|
||||
if (m_step_size > m_config.m_step_size_min)
|
||||
m_step_size -= m_config.m_step_size_dec;
|
||||
|
||||
|
|
@ -2564,7 +2621,7 @@ namespace sat {
|
|||
tout << "missed " << lit << "@" << lvl(lit) << "\n";);
|
||||
CTRACE(sat, idx == 0, display(tout););
|
||||
if (idx == 0)
|
||||
IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflict << "\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflicts << "\n");
|
||||
VERIFY(idx > 0);
|
||||
idx--;
|
||||
}
|
||||
|
|
@ -2874,7 +2931,7 @@ namespace sat {
|
|||
inc_activity(var);
|
||||
break;
|
||||
case BH_CHB:
|
||||
m_last_conflict[var] = m_stats.m_conflict;
|
||||
m_last_conflict[var] = m_stats.m_conflicts;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
|
@ -2915,14 +2972,15 @@ namespace sat {
|
|||
for (unsigned i = head; i < sz; ++i) {
|
||||
bool_var v = m_trail[i].var();
|
||||
TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";);
|
||||
m_phase[v] = m_rand() % 2 == 0;
|
||||
bool value = m_rand() % 2 == 0;
|
||||
set_phase(v, value);
|
||||
}
|
||||
if (is_sat_phase() && head >= m_best_phase_size) {
|
||||
m_best_phase_size = head;
|
||||
IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n");
|
||||
for (unsigned i = 0; i < head; ++i) {
|
||||
bool_var v = m_trail[i].var();
|
||||
m_best_phase[v] = m_phase[v];
|
||||
set_best_phase(v, m_phase[v]);
|
||||
}
|
||||
set_has_new_best_phase(true);
|
||||
}
|
||||
|
|
@ -2971,23 +3029,30 @@ namespace sat {
|
|||
void solver::do_rephase() {
|
||||
switch (m_config.m_phase) {
|
||||
case PS_ALWAYS_TRUE:
|
||||
for (auto& p : m_phase) p = true;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, true);
|
||||
break;
|
||||
case PS_ALWAYS_FALSE:
|
||||
for (auto& p : m_phase) p = false;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, false);
|
||||
break;
|
||||
case PS_FROZEN:
|
||||
break;
|
||||
case PS_BASIC_CACHING:
|
||||
switch (m_rephase.count % 4) {
|
||||
case 0:
|
||||
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i) {
|
||||
bool value = (m_rand() % 2) == 0;
|
||||
set_phase(i, value);
|
||||
}
|
||||
break;
|
||||
case 1:
|
||||
for (auto& p : m_phase) p = false;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, false);
|
||||
break;
|
||||
case 2:
|
||||
for (auto& p : m_phase) p = !p;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, !m_phase[i]);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
|
@ -2995,18 +3060,21 @@ namespace sat {
|
|||
break;
|
||||
case PS_SAT_CACHING:
|
||||
if (m_search_state == s_sat)
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
m_phase[i] = m_best_phase[i];
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, m_best_phase[i]);
|
||||
break;
|
||||
case PS_RANDOM:
|
||||
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i) {
|
||||
bool value = (m_rand() % 2) == 0;
|
||||
set_phase(i, value);
|
||||
}
|
||||
break;
|
||||
case PS_LOCAL_SEARCH:
|
||||
if (m_search_state == s_sat) {
|
||||
if (m_rand() % 2 == 0)
|
||||
bounded_local_search();
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
m_phase[i] = m_best_phase[i];
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i)
|
||||
set_phase(i, m_best_phase[i]);
|
||||
}
|
||||
|
||||
break;
|
||||
|
|
@ -3601,6 +3669,8 @@ namespace sat {
|
|||
m_phase.shrink(v);
|
||||
m_best_phase.shrink(v);
|
||||
m_prev_phase.shrink(v);
|
||||
m_phase_birthdate.shrink(v);
|
||||
m_best_phase_birthdate.shrink(v);
|
||||
m_assigned_since_gc.shrink(v);
|
||||
m_simplifier.reset_todos();
|
||||
}
|
||||
|
|
@ -3644,7 +3714,7 @@ namespace sat {
|
|||
SASSERT(value(v) == l_undef);
|
||||
m_case_split_queue.unassign_var_eh(v);
|
||||
if (m_config.m_anti_exploration) {
|
||||
m_canceled[v] = m_stats.m_conflict;
|
||||
m_canceled[v] = m_stats.m_conflicts;
|
||||
}
|
||||
}
|
||||
m_trail.shrink(old_sz);
|
||||
|
|
@ -3812,7 +3882,7 @@ namespace sat {
|
|||
double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
|
||||
for (unsigned i = qhead; i < m_trail.size(); ++i) {
|
||||
auto v = m_trail[i].var();
|
||||
auto d = m_stats.m_conflict - m_last_conflict[v] + 1;
|
||||
auto d = m_stats.m_conflicts - m_last_conflict[v] + 1;
|
||||
if (d == 0) d = 1;
|
||||
auto reward = multiplier / d;
|
||||
auto activity = m_activity[v];
|
||||
|
|
@ -4745,7 +4815,7 @@ namespace sat {
|
|||
st.update("sat mk var", m_mk_var);
|
||||
st.update("sat gc clause", m_gc_clause);
|
||||
st.update("sat del clause", m_del_clause);
|
||||
st.update("sat conflicts", m_conflict);
|
||||
st.update("sat conflicts", m_conflicts);
|
||||
st.update("sat decisions", m_decision);
|
||||
st.update("sat propagations 2ary", m_bin_propagate);
|
||||
st.update("sat propagations 3ary", m_ter_propagate);
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ namespace sat {
|
|||
unsigned m_mk_bin_clause;
|
||||
unsigned m_mk_ter_clause;
|
||||
unsigned m_mk_clause;
|
||||
unsigned m_conflict;
|
||||
unsigned m_conflicts;
|
||||
unsigned m_propagate;
|
||||
unsigned m_bin_propagate;
|
||||
unsigned m_ter_propagate;
|
||||
|
|
@ -148,6 +148,8 @@ namespace sat {
|
|||
bool_vector m_phase;
|
||||
bool_vector m_best_phase;
|
||||
bool_vector m_prev_phase;
|
||||
svector<uint64_t> m_phase_birthdate;
|
||||
svector<uint64_t> m_best_phase_birthdate;
|
||||
bool m_new_best_phase = false;
|
||||
svector<char> m_assigned_since_gc;
|
||||
search_state m_search_state;
|
||||
|
|
@ -373,12 +375,19 @@ namespace sat {
|
|||
bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
|
||||
void set_eliminated(bool_var v, bool f) override;
|
||||
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
|
||||
void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); }
|
||||
void set_phase(literal l) override;
|
||||
void set_phase(bool_var v, bool value);
|
||||
void set_best_phase(bool_var v, bool value);
|
||||
bool get_phase(bool_var b) { return m_phase.get(b, false); }
|
||||
bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); }
|
||||
uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }
|
||||
uint64_t get_best_phase_birthdate(bool_var b) const { return m_best_phase_birthdate.get(b, 0); }
|
||||
uint64_t get_preferred_phase_birthdate(bool_var b) const;
|
||||
void set_has_new_best_phase(bool b) { m_new_best_phase = b; }
|
||||
bool has_new_best_phase() const { return m_new_best_phase; }
|
||||
void move_to_front(bool_var b);
|
||||
unsigned get_activity(bool_var v) const { return m_activity[v]; }
|
||||
void get_backbone_candidates(literal_vector& lits, unsigned max_num);
|
||||
unsigned scope_lvl() const { return m_scope_lvl; }
|
||||
unsigned search_lvl() const { return m_search_lvl; }
|
||||
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
|
||||
|
|
|
|||
|
|
@ -405,6 +405,46 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
unsigned get_assign_level(expr* e) const override {
|
||||
m.is_not(e, e);
|
||||
sat::bool_var bv = m_map.to_bool_var(e);
|
||||
return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv);
|
||||
}
|
||||
|
||||
bool is_relevant(expr* e) const override {
|
||||
m.is_not(e, e);
|
||||
sat::bool_var bv = m_map.to_bool_var(e);
|
||||
if (bv == sat::null_bool_var)
|
||||
return true;
|
||||
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
|
||||
return !ext || ext->is_relevant(bv);
|
||||
}
|
||||
|
||||
unsigned get_num_bool_vars() const override {
|
||||
return m_solver.num_vars();
|
||||
}
|
||||
|
||||
sat::bool_var get_bool_var(expr* e) const override {
|
||||
m.is_not(e, e);
|
||||
return m_map.to_bool_var(e);
|
||||
}
|
||||
|
||||
expr* bool_var2expr(sat::bool_var v) const override {
|
||||
return v < m_solver.num_vars() ? m_map.bool_var2expr(v) : nullptr;
|
||||
}
|
||||
|
||||
lbool get_assignment(sat::bool_var v) const override {
|
||||
return v < m_solver.num_vars() ? m_solver.value(v) : l_undef;
|
||||
}
|
||||
|
||||
double get_activity(sat::bool_var v) const override {
|
||||
return v < m_solver.num_vars() ? static_cast<double>(m_solver.get_activity(v)) : 0.0;
|
||||
}
|
||||
|
||||
bool was_eliminated(sat::bool_var v) const override {
|
||||
return v < m_solver.num_vars() && m_solver.was_eliminated(v);
|
||||
}
|
||||
|
||||
expr_ref_vector get_trail(unsigned max_level) override {
|
||||
expr_ref_vector result(m);
|
||||
unsigned sz = m_solver.trail_size();
|
||||
|
|
@ -451,8 +491,46 @@ public:
|
|||
vars.push_back(kv.m_value);
|
||||
}
|
||||
sat::literal_vector lits;
|
||||
lbool result = m_solver.cube(vars, lits, backtrack_level);
|
||||
expr_ref_vector fmls(m);
|
||||
parallel_params pp(m_params);
|
||||
if (!pp.cube_lookahead()) {
|
||||
sat::bool_var_vector candidates;
|
||||
unsigned search_lvl = m_solver.search_lvl();
|
||||
for (sat::bool_var v : vars) {
|
||||
if (was_eliminated(v))
|
||||
continue;
|
||||
if (get_assignment(v) != l_undef && m_solver.lvl(v) <= search_lvl)
|
||||
continue;
|
||||
candidates.push_back(v);
|
||||
}
|
||||
std::sort(candidates.begin(), candidates.end(), [&](sat::bool_var a, sat::bool_var b) {
|
||||
return get_activity(a) > get_activity(b);
|
||||
});
|
||||
// shuffle sub-sequences with equal activity
|
||||
unsigned i = 0;
|
||||
while (i < candidates.size()) {
|
||||
unsigned j = i + 1;
|
||||
double act = get_activity(candidates[i]);
|
||||
while (j < candidates.size() && get_activity(candidates[j]) == act)
|
||||
++j;
|
||||
if (j - i > 1)
|
||||
shuffle(j - i, candidates.data() + i, m_solver.rand());
|
||||
i = j;
|
||||
}
|
||||
if (candidates.empty())
|
||||
return expr_ref_vector(m);
|
||||
vs.reset();
|
||||
for (sat::bool_var v : candidates) {
|
||||
expr* e = bool_var2expr(v);
|
||||
if (e) {
|
||||
if (fmls.size() < backtrack_level)
|
||||
fmls.push_back(e);
|
||||
vs.push_back(e);
|
||||
}
|
||||
}
|
||||
return fmls;
|
||||
}
|
||||
lbool result = m_solver.cube(vars, lits, backtrack_level);
|
||||
expr_ref_vector lit2expr(m);
|
||||
lit2expr.resize(m_solver.num_vars() * 2);
|
||||
m_map.mk_inv(lit2expr);
|
||||
|
|
@ -482,6 +560,27 @@ public:
|
|||
return fmls;
|
||||
}
|
||||
|
||||
void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
|
||||
if (!is_internalized()) {
|
||||
lbool r = internalize_formulas();
|
||||
if (r != l_true)
|
||||
return;
|
||||
}
|
||||
convert_internalized();
|
||||
sat::literal_vector lits;
|
||||
m_solver.get_backbone_candidates(lits, max_num);
|
||||
expr_ref_vector lit2expr(m);
|
||||
lit2expr.resize(m_solver.num_vars() * 2);
|
||||
m_map.mk_inv(lit2expr);
|
||||
uint64_t now = m_solver.get_stats().m_conflicts;
|
||||
for (sat::literal lit : lits) {
|
||||
expr* e = lit2expr.get(lit.index());
|
||||
if (!e)
|
||||
continue;
|
||||
candidates.push_back(scored_literal(m, e, static_cast<double>(now - m_solver.get_phase_birthdate(lit.var()))));
|
||||
}
|
||||
}
|
||||
|
||||
expr* congruence_next(expr* e) override { return e; }
|
||||
expr* congruence_root(expr* e) override { return e; }
|
||||
expr_ref congruence_explain(expr* a, expr* b) override { return expr_ref(m.mk_eq(a, b), m); }
|
||||
|
|
|
|||
|
|
@ -49,6 +49,13 @@ sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
|
|||
return m_mapping[idx].m_value;
|
||||
}
|
||||
|
||||
expr* atom2bool_var::bool_var2expr(sat::bool_var v) const {
|
||||
for (auto const& kv : m_mapping)
|
||||
if (kv.m_value == v)
|
||||
return kv.m_key;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
struct collect_boolean_interface_proc {
|
||||
struct visitor {
|
||||
obj_hashtable<expr> & m_r;
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@ public:
|
|||
atom2bool_var(ast_manager & m):expr2var(m) {}
|
||||
void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); }
|
||||
sat::bool_var to_bool_var(expr * n) const;
|
||||
expr* bool_var2expr(sat::bool_var v) const;
|
||||
void mk_inv(expr_ref_vector & lit2expr) const;
|
||||
void mk_var_inv(expr_ref_vector & var2expr) const;
|
||||
// return true if the mapping contains uninterpreted atoms.
|
||||
|
|
|
|||
|
|
@ -155,7 +155,7 @@ namespace bv {
|
|||
void ackerman::propagate() {
|
||||
auto* n = m_queue;
|
||||
vv* k = nullptr;
|
||||
unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.get_config().m_dack_factor);
|
||||
unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflicts * s.get_config().m_dack_factor);
|
||||
num_prop = std::min(num_prop, m_table.size());
|
||||
for (unsigned i = 0; i < num_prop; ++i, n = k) {
|
||||
k = n->next();
|
||||
|
|
|
|||
|
|
@ -171,7 +171,7 @@ namespace euf {
|
|||
SASSERT(ctx.s().at_base_lvl());
|
||||
auto* n = m_queue;
|
||||
inference* k = nullptr;
|
||||
unsigned num_prop = static_cast<unsigned>(ctx.s().get_stats().m_conflict * ctx.m_config.m_dack_factor);
|
||||
unsigned num_prop = static_cast<unsigned>(ctx.s().get_stats().m_conflicts * ctx.m_config.m_dack_factor);
|
||||
num_prop = std::min(num_prop, m_table.size());
|
||||
for (unsigned i = 0; i < num_prop; ++i, n = k) {
|
||||
k = n->next();
|
||||
|
|
|
|||
|
|
@ -118,6 +118,10 @@ namespace smt {
|
|||
if (!m_setup.already_configured()) {
|
||||
m_fparams.updt_params(p);
|
||||
}
|
||||
else {
|
||||
// selected parameters are safe to update after initialization
|
||||
m_fparams.m_max_conflicts = p.get_uint("max_conflicts", m_fparams.m_max_conflicts);
|
||||
}
|
||||
for (auto th : m_theory_set)
|
||||
if (th)
|
||||
th->updt_params();
|
||||
|
|
@ -3652,6 +3656,13 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::setup_for_parallel() {
|
||||
// Native SMT parallel configures the parent context before cloning workers.
|
||||
// context::copy then configures/internalizes each worker copy while
|
||||
// preprocessing is still enabled.
|
||||
setup_context(m_fparams.m_auto_config);
|
||||
}
|
||||
|
||||
config_mode context::get_config_mode(bool use_static_features) const {
|
||||
if (!m_fparams.m_auto_config)
|
||||
return CFG_BASIC;
|
||||
|
|
@ -4672,7 +4683,6 @@ namespace smt {
|
|||
theory_id th_id = l->get_id();
|
||||
|
||||
for (enode * parent : enode::parents(n)) {
|
||||
auto p = parent->get_expr();
|
||||
family_id fid = parent->get_family_id();
|
||||
if (fid != th_id && fid != m.get_basic_family_id()) {
|
||||
if (is_beta_redex(parent, n))
|
||||
|
|
|
|||
|
|
@ -64,6 +64,7 @@ namespace smt {
|
|||
|
||||
class model_generator;
|
||||
class context;
|
||||
class kernel;
|
||||
|
||||
struct oom_exception : public z3_error {
|
||||
oom_exception() : z3_error(ERR_MEMOUT) {}
|
||||
|
|
@ -85,6 +86,7 @@ namespace smt {
|
|||
friend class model_generator;
|
||||
friend class lookahead;
|
||||
friend class parallel;
|
||||
friend class kernel;
|
||||
public:
|
||||
statistics m_stats;
|
||||
|
||||
|
|
@ -292,6 +294,10 @@ namespace smt {
|
|||
return m_fparams;
|
||||
}
|
||||
|
||||
smt_params const& get_fparams() const {
|
||||
return m_fparams;
|
||||
}
|
||||
|
||||
params_ref const & get_params() {
|
||||
return m_params;
|
||||
}
|
||||
|
|
@ -452,6 +458,8 @@ namespace smt {
|
|||
svector<double> const & get_activity_vector() const { return m_activity; }
|
||||
|
||||
double get_activity(bool_var v) const { return m_activity[v]; }
|
||||
unsigned get_num_assignments() const { return m_stats.m_num_assignments; }
|
||||
unsigned get_birthdate(bool_var v) const { return m_birthdate[v]; }
|
||||
|
||||
void set_activity(bool_var v, double act) { m_activity[v] = act; }
|
||||
|
||||
|
|
@ -538,6 +546,8 @@ namespace smt {
|
|||
return m_scope_lvl == m_search_lvl;
|
||||
}
|
||||
|
||||
void pop_to_search_level() { pop_to_search_lvl(); }
|
||||
|
||||
bool tracking_assumptions() const {
|
||||
return !m_assumptions.empty() && m_search_lvl > m_base_lvl;
|
||||
}
|
||||
|
|
@ -1697,6 +1707,8 @@ namespace smt {
|
|||
|
||||
lbool setup_and_check(bool reset_cancel = true);
|
||||
|
||||
void setup_for_parallel();
|
||||
|
||||
void reduce_assertions();
|
||||
|
||||
bool resource_limits_exceeded();
|
||||
|
|
@ -1913,5 +1925,3 @@ namespace smt {
|
|||
std::ostream& operator<<(std::ostream& out, enode_pp const& p);
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -280,10 +280,22 @@ namespace smt {
|
|||
smt_params_helper::collect_param_descrs(d);
|
||||
}
|
||||
|
||||
void kernel::pop_to_base_level() {
|
||||
m_imp->m_kernel.pop_to_base_lvl();
|
||||
}
|
||||
|
||||
void kernel::set_preprocess(bool f) {
|
||||
m_imp->m_kernel.get_fparams().m_preprocess = f;
|
||||
}
|
||||
|
||||
context & kernel::get_context() {
|
||||
return m_imp->m_kernel;
|
||||
}
|
||||
|
||||
context const& kernel::get_context() const {
|
||||
return m_imp->m_kernel;
|
||||
}
|
||||
|
||||
void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
|
||||
m_imp->m_kernel.get_levels(vars, depth);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -300,6 +300,10 @@ namespace smt {
|
|||
*/
|
||||
static void collect_param_descrs(param_descrs & d);
|
||||
|
||||
void pop_to_base_level();
|
||||
|
||||
void set_preprocess(bool f);
|
||||
|
||||
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause);
|
||||
|
||||
/**
|
||||
|
|
@ -340,6 +344,6 @@ namespace smt {
|
|||
\warning This method should not be used in new code.
|
||||
*/
|
||||
context & get_context();
|
||||
context const& get_context() const;
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ Author:
|
|||
#include "smt/smt_parallel.h"
|
||||
#include "smt/smt_lookahead.h"
|
||||
#include "solver/solver_preprocess.h"
|
||||
#include "params/smt_parallel_params.hpp"
|
||||
#include "solver/parallel_params.hpp"
|
||||
|
||||
#include <cmath>
|
||||
#include <mutex>
|
||||
|
|
@ -78,8 +78,11 @@ namespace smt {
|
|||
|
||||
lbool res = l_undef;
|
||||
try {
|
||||
if (!m.inc())
|
||||
if (!m.inc()) {
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
return;
|
||||
}
|
||||
res = m_sls->check();
|
||||
} catch (z3_exception &ex) {
|
||||
// Cancellation is normal in portfolio mode
|
||||
|
|
@ -180,8 +183,9 @@ namespace smt {
|
|||
for (expr* lit : bb_candidate_lits) {
|
||||
if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch))
|
||||
break;
|
||||
if (!m.inc() || canceled())
|
||||
if (!m.inc() || canceled())
|
||||
break;
|
||||
|
||||
|
||||
expr* atom = lit;
|
||||
m.is_not(lit, atom);
|
||||
|
|
@ -218,11 +222,14 @@ namespace smt {
|
|||
}
|
||||
|
||||
if (!m.inc())
|
||||
return;
|
||||
break;
|
||||
if (!canceled())
|
||||
b.cancel_current_backbone_batch();
|
||||
bb_candidates.reset();
|
||||
}
|
||||
if (!m.inc())
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
}
|
||||
|
||||
lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) {
|
||||
|
|
@ -390,8 +397,11 @@ namespace smt {
|
|||
|
||||
while (true) {
|
||||
|
||||
if (!m.inc())
|
||||
if (!m.inc()) {
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
return;
|
||||
}
|
||||
if (canceled())
|
||||
break;
|
||||
|
||||
|
|
@ -515,6 +525,9 @@ namespace smt {
|
|||
|
||||
bb_curr_batch_candidates.reset();
|
||||
}
|
||||
if (!m.inc())
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
}
|
||||
|
||||
void parallel::backbones_worker::cancel() {
|
||||
|
|
@ -550,7 +563,7 @@ namespace smt {
|
|||
if (m_ablate_backtracking) {
|
||||
// Ablation: for each target, pass the entire path from root to that node
|
||||
for (auto const& target : targets) {
|
||||
if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch))
|
||||
if (m_search_tree.is_lease_canceled(target.leased_node))
|
||||
continue;
|
||||
|
||||
// Reconstruct the full path from root to this target node
|
||||
|
|
@ -626,7 +639,7 @@ namespace smt {
|
|||
ctx->set_logic(p.ctx.m_setup.get_logic());
|
||||
context::copy(p.ctx, *ctx, true);
|
||||
ctx->pop_to_base_lvl();
|
||||
ctx->get_fparams().m_preprocess = false;
|
||||
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
|
||||
}
|
||||
|
||||
void parallel::core_minimizer_worker::cancel() {
|
||||
|
|
@ -742,6 +755,8 @@ namespace smt {
|
|||
if (minimized.size() < original_size)
|
||||
b.publish_minimized_core(m_l2g, asms, source, original_size, minimized);
|
||||
}
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
}
|
||||
|
||||
void parallel::worker::run() {
|
||||
|
|
@ -763,21 +778,29 @@ namespace smt {
|
|||
if (m_config.m_global_backbones) {
|
||||
bb_candidates local_candidates = find_backbone_candidates();
|
||||
b.collect_backbone_candidates(m_l2g, local_candidates);
|
||||
if (!m.inc())
|
||||
return;
|
||||
if (!m.inc()) {
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
lbool r = check_cube(cube);
|
||||
|
||||
if (b.lease_canceled(lease)) {
|
||||
bool cancel_signaled = false;
|
||||
if (b.release_canceled_lease(id, lease, cancel_signaled)) {
|
||||
LOG_WORKER(1, " abandoning canceled lease\n");
|
||||
lease = {};
|
||||
m.limit().dec_cancel();
|
||||
if (cancel_signaled)
|
||||
m.limit().dec_cancel();
|
||||
continue;
|
||||
}
|
||||
|
||||
if (!m.inc())
|
||||
return;
|
||||
if (!m.inc()) {
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
break;
|
||||
}
|
||||
|
||||
switch (r) {
|
||||
case l_undef: {
|
||||
|
|
@ -836,6 +859,11 @@ namespace smt {
|
|||
if (m_config.m_share_units)
|
||||
share_units();
|
||||
}
|
||||
if (!m.inc()) {
|
||||
b.set_canceled();
|
||||
// b.notify_cv_waiters;
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms)
|
||||
|
|
@ -854,10 +882,10 @@ namespace smt {
|
|||
m_num_initial_atoms = ctx->get_num_bool_vars();
|
||||
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
|
||||
|
||||
smt_parallel_params pp(p.ctx.m_params);
|
||||
m_config.m_inprocessing = pp.inprocessing();
|
||||
m_config.m_global_backbones = pp.num_global_bb_batch_threads() > 0 || pp.num_global_bb_fl_threads() > 0;
|
||||
m_config.m_local_backbones = pp.local_backbones();
|
||||
parallel_params pp(p.ctx.get_params());
|
||||
m_config.m_inprocessing = false;
|
||||
m_config.m_global_backbones = pp.num_bb_threads() > 0;
|
||||
m_config.m_local_backbones = false;
|
||||
m_config.m_core_minimize = pp.core_minimize();
|
||||
m_config.m_ablate_backtracking = pp.ablate_backtracking();
|
||||
|
||||
|
|
@ -887,9 +915,8 @@ namespace smt {
|
|||
ctx->pop_to_base_lvl();
|
||||
m_shared_units_prefix = ctx->assigned_literals().size();
|
||||
m_num_initial_atoms = ctx->get_num_bool_vars();
|
||||
|
||||
smt_parallel_params pp(p.ctx.m_params);
|
||||
m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0;
|
||||
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
|
||||
m_use_failed_literal_test = false; // true failed literal mode, false for Janota chunking algorithm
|
||||
}
|
||||
|
||||
parallel::bb_candidates parallel::worker::find_backbone_candidates(unsigned k) {
|
||||
|
|
@ -1124,7 +1151,7 @@ namespace smt {
|
|||
|
||||
// only cancel workers that currently hold a lease, whose lease is canceled,
|
||||
// and haven't already been signaled (prevents multiple inc_cancel() for same lease)
|
||||
if (lease.leased_node && !lease.cancel_signaled && m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) {
|
||||
if (lease.leased_node && !lease.cancel_signaled && m_search_tree.is_lease_canceled(lease.leased_node)) {
|
||||
p.m_workers[worker_id]->cancel_lease();
|
||||
m_worker_leases[worker_id].cancel_signaled = true;
|
||||
}
|
||||
|
|
@ -1179,14 +1206,13 @@ namespace smt {
|
|||
|
||||
unsigned best_idx = select_best_core_min_job_unlocked();
|
||||
m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1);
|
||||
core_min_job* job = m_core_min_jobs.detach_back();
|
||||
scoped_ptr<core_min_job> job = m_core_min_jobs.detach_back();
|
||||
m_core_min_jobs.pop_back();
|
||||
SASSERT(job);
|
||||
source = job->source;
|
||||
core.reset();
|
||||
for (expr* c : job->core)
|
||||
core.push_back(g2l(c));
|
||||
dealloc(job);
|
||||
return source != nullptr;
|
||||
}
|
||||
|
||||
|
|
@ -1277,7 +1303,7 @@ namespace smt {
|
|||
if (!g_core.empty()) {
|
||||
collect_matching_targets_unlocked(source, g_core[0].get(), g_core, targets);
|
||||
for (auto const& target : targets) {
|
||||
if (!m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch))
|
||||
if (!m_search_tree.is_lease_canceled(target.leased_node))
|
||||
m_search_tree.backtrack(target.leased_node, g_core);
|
||||
}
|
||||
}
|
||||
|
|
@ -1331,7 +1357,7 @@ namespace smt {
|
|||
for (node* t : matches) {
|
||||
if (!t || t == source)
|
||||
continue;
|
||||
if (m_search_tree.is_lease_canceled(t, t->get_cancel_epoch()))
|
||||
if (m_search_tree.is_lease_canceled(t))
|
||||
continue;
|
||||
|
||||
// When source is provided, keep only external matches. Nodes in the
|
||||
|
|
@ -1358,7 +1384,7 @@ namespace smt {
|
|||
if (!is_highest_ancestor)
|
||||
continue;
|
||||
|
||||
targets.push_back({ t, t->get_cancel_epoch() });
|
||||
targets.push_back({ t });
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1374,7 +1400,7 @@ namespace smt {
|
|||
SASSERT(lease != nullptr || targets != nullptr);
|
||||
bool did_backtrack = false;
|
||||
|
||||
if (lease && !m_search_tree.is_lease_canceled(lease->leased_node, lease->cancel_epoch)) {
|
||||
if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) {
|
||||
// we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
|
||||
// i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
|
||||
did_backtrack = true;
|
||||
|
|
@ -1384,7 +1410,7 @@ namespace smt {
|
|||
}
|
||||
if (targets) {
|
||||
for (auto const& target : *targets) {
|
||||
if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch))
|
||||
if (m_search_tree.is_lease_canceled(target.leased_node))
|
||||
continue;
|
||||
|
||||
did_backtrack = true;
|
||||
|
|
@ -1416,13 +1442,13 @@ namespace smt {
|
|||
if (m_state != state::is_running)
|
||||
return;
|
||||
|
||||
if (m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch))
|
||||
if (m_search_tree.is_lease_canceled(lease.leased_node))
|
||||
return;
|
||||
|
||||
expr_ref lit(m), nlit(m);
|
||||
lit = l2g(atom);
|
||||
nlit = mk_not(m, lit);
|
||||
bool did_split = m_search_tree.try_split(lease.leased_node, lease.cancel_epoch, lit, nlit, effort);
|
||||
bool did_split = m_search_tree.try_split(lease.leased_node, lit, nlit, effort);
|
||||
|
||||
release_lease_unlocked(worker_id, lease.leased_node);
|
||||
|
||||
|
|
@ -1438,9 +1464,22 @@ namespace smt {
|
|||
release_lease_unlocked(worker_id, lease.leased_node);
|
||||
}
|
||||
|
||||
bool parallel::batch_manager::lease_canceled(node_lease const &lease) {
|
||||
bool parallel::batch_manager::release_canceled_lease(unsigned worker_id, node_lease const &lease, bool& cancel_signaled) {
|
||||
std::scoped_lock lock(mux);
|
||||
return m_state == state::is_running && m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch);
|
||||
cancel_signaled = false;
|
||||
if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size())
|
||||
return false;
|
||||
|
||||
auto& stored = m_worker_leases[worker_id];
|
||||
if (stored.leased_node != lease.leased_node)
|
||||
return false;
|
||||
|
||||
if (!m_search_tree.is_lease_canceled(stored.leased_node))
|
||||
return false;
|
||||
|
||||
cancel_signaled = stored.cancel_signaled;
|
||||
release_lease_unlocked(worker_id, stored.leased_node);
|
||||
return true;
|
||||
}
|
||||
|
||||
void parallel::batch_manager::collect_clause(ast_translation &l2g, unsigned source_worker_id, expr *clause) {
|
||||
|
|
@ -1683,6 +1722,19 @@ namespace smt {
|
|||
cancel_background_threads();
|
||||
}
|
||||
|
||||
void parallel::batch_manager::set_canceled() {
|
||||
std::scoped_lock lock(mux);
|
||||
if (m_state != state::is_running)
|
||||
return;
|
||||
cancel_background_threads();
|
||||
}
|
||||
|
||||
// void parallel::batch_manager::notify_cv_waiters {
|
||||
// std::scoped_lock lock(mux);
|
||||
// m_bb_cv.notify_all();
|
||||
// m_core_min_cv.notify_all();
|
||||
// }
|
||||
|
||||
void parallel::batch_manager::set_exception(unsigned error_code) {
|
||||
std::scoped_lock lock(mux);
|
||||
IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n");
|
||||
|
|
@ -1745,7 +1797,6 @@ namespace smt {
|
|||
IF_VERBOSE(2, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";);
|
||||
|
||||
lease.leased_node = t;
|
||||
lease.cancel_epoch = t->get_cancel_epoch();
|
||||
if (id >= m_worker_leases.size())
|
||||
m_worker_leases.resize(id + 1);
|
||||
m_worker_leases[id] = lease;
|
||||
|
|
@ -1779,7 +1830,7 @@ namespace smt {
|
|||
m_worker_leases.reset();
|
||||
m_worker_leases.resize(p.m_workers.size());
|
||||
|
||||
smt_parallel_params pp(p.ctx.m_params);
|
||||
parallel_params pp(p.ctx.get_params());
|
||||
m_ablate_backtracking = pp.ablate_backtracking();
|
||||
}
|
||||
|
||||
|
|
@ -1794,18 +1845,18 @@ namespace smt {
|
|||
}
|
||||
|
||||
lbool parallel::operator()(expr_ref_vector const &asms) {
|
||||
smt_parallel_params pp(ctx.m_params);
|
||||
unsigned num_global_bb_batch_threads = pp.num_global_bb_batch_threads();
|
||||
params_ref const& params = ctx.get_params();
|
||||
parallel_params pp(params);
|
||||
unsigned num_global_bb_batch_threads = pp.num_bb_threads();
|
||||
if (num_global_bb_batch_threads > 2)
|
||||
throw default_exception("smt_parallel.num_global_bb_batch_threads must be 0, 1, or 2");
|
||||
throw default_exception("parallel.num_bb_threads must be 0, 1, or 2");
|
||||
unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads);
|
||||
unsigned num_sls_threads = (pp.sls() ? 1 : 0);
|
||||
unsigned num_core_min_threads = (pp.core_minimize() ? 1 : 0);
|
||||
unsigned num_global_bb_fl_threads = pp.num_global_bb_fl_threads();
|
||||
if (num_global_bb_fl_threads > 2)
|
||||
throw default_exception("smt_parallel.num_global_bb_fl_threads must be 0, 1, or 2");
|
||||
if (num_global_bb_fl_threads > 0 && num_global_bb_batch_threads > 0)
|
||||
throw default_exception("smt_parallel.num_global_bb_fl_threads and smt_parallel.num_global_bb_batch_threads cannot both be enabled");
|
||||
unsigned num_sls_threads = 0;
|
||||
bool core_minimize = pp.core_minimize();
|
||||
if (pp.ablate_backtracking())
|
||||
core_minimize = false;
|
||||
unsigned num_core_min_threads = (core_minimize ? 1 : 0);
|
||||
unsigned num_global_bb_fl_threads = 0;
|
||||
unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads;
|
||||
unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads;
|
||||
|
||||
|
|
@ -1841,7 +1892,7 @@ namespace smt {
|
|||
m_sls_worker = alloc(sls_worker, *this);
|
||||
sl.push_child(&(m_sls_worker->limit()));
|
||||
}
|
||||
if (pp.core_minimize()) {
|
||||
if (num_core_min_threads == 1) {
|
||||
m_core_minimizer_worker = alloc(core_minimizer_worker, *this, asms);
|
||||
sl.push_child(&(m_core_minimizer_worker->limit()));
|
||||
}
|
||||
|
|
@ -1857,17 +1908,31 @@ namespace smt {
|
|||
|
||||
m_batch_manager.initialize(num_global_bb_threads);
|
||||
|
||||
auto safe_run = [&](auto* w) {
|
||||
try {
|
||||
w->run();
|
||||
}
|
||||
catch (z3_error& err) {
|
||||
if (!w->limit().is_canceled())
|
||||
m_batch_manager.set_exception(err.error_code());
|
||||
}
|
||||
catch (z3_exception& ex) {
|
||||
if (!w->limit().is_canceled() && !is_cancellation_exception(ex.what()))
|
||||
m_batch_manager.set_exception(ex.what());
|
||||
}
|
||||
};
|
||||
|
||||
// Launch threads
|
||||
vector<std::thread> threads(total_threads);
|
||||
unsigned thread_idx = 0;
|
||||
for (auto* w : m_workers)
|
||||
threads[thread_idx++] = std::thread([&, w]() { w->run(); });
|
||||
threads[thread_idx++] = std::thread([&, w]() { safe_run(w); });
|
||||
if (m_sls_worker)
|
||||
threads[thread_idx++] = std::thread([&]() { m_sls_worker->run(); });
|
||||
threads[thread_idx++] = std::thread([&]() { safe_run(m_sls_worker.get()); });
|
||||
if (m_core_minimizer_worker)
|
||||
threads[thread_idx++] = std::thread([&]() { m_core_minimizer_worker->run(); });
|
||||
threads[thread_idx++] = std::thread([&]() { safe_run(m_core_minimizer_worker.get()); });
|
||||
for (auto* w : m_global_backbones_workers)
|
||||
threads[thread_idx++] = std::thread([&, w]() { w->run(); });
|
||||
threads[thread_idx++] = std::thread([&, w]() { safe_run(w); });
|
||||
|
||||
|
||||
// Wait for all threads to finish
|
||||
|
|
|
|||
|
|
@ -32,6 +32,13 @@ namespace smt {
|
|||
struct cube_config {
|
||||
using literal = expr_ref;
|
||||
static bool literal_is_null(expr_ref const& l) { return l == nullptr; }
|
||||
static bool same_atom(expr_ref const& a, expr_ref const& b) {
|
||||
expr* atom_a = a.get();
|
||||
expr* atom_b = b.get();
|
||||
a.get_manager().is_not(atom_a, atom_a);
|
||||
b.get_manager().is_not(atom_b, atom_b);
|
||||
return atom_a == atom_b;
|
||||
}
|
||||
static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { return out << mk_bounded_pp(l, l.get_manager()); }
|
||||
};
|
||||
|
||||
|
|
@ -57,12 +64,6 @@ namespace smt {
|
|||
struct node_lease {
|
||||
node* leased_node = nullptr;
|
||||
|
||||
// Cancellation generation counter for this node/subtree.
|
||||
// Incremented when the node is closed; used to signal that all
|
||||
// workers holding leases on this node (or its descendants)
|
||||
// must abandon work immediately.
|
||||
unsigned cancel_epoch = 0;
|
||||
|
||||
// Guards against multiple inc_cancel() calls for the same lease.
|
||||
// Set when cancel_lease() is signaled; cleared when a new lease is assigned.
|
||||
bool cancel_signaled = false;
|
||||
|
|
@ -189,6 +190,8 @@ namespace smt {
|
|||
void set_sat(ast_translation& l2g, model& m);
|
||||
void set_exception(std::string const& msg);
|
||||
void set_exception(unsigned error_code);
|
||||
void set_canceled();
|
||||
void notify_cv_waiters();
|
||||
void collect_statistics(::statistics& st) const;
|
||||
|
||||
void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates);
|
||||
|
|
@ -218,7 +221,7 @@ namespace smt {
|
|||
unsigned original_core_size, expr_ref_vector const& minimized_core);
|
||||
void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort);
|
||||
void release_lease(unsigned worker_id, node_lease const& lease);
|
||||
bool lease_canceled(node_lease const& lease);
|
||||
bool release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled);
|
||||
|
||||
void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause);
|
||||
expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
|
||||
|
|
|
|||
|
|
@ -22,12 +22,16 @@ Notes:
|
|||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/func_decl_dependencies.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include "smt/smt_kernel.h"
|
||||
#include "params/smt_params.h"
|
||||
#include "params/smt_params_helper.hpp"
|
||||
#include "solver/solver_na2as.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
#include "solver/mus.h"
|
||||
|
||||
#include <algorithm>
|
||||
|
||||
namespace {
|
||||
|
||||
class smt_solver : public solver_na2as {
|
||||
|
|
@ -61,6 +65,7 @@ namespace {
|
|||
smt_params m_smt_params;
|
||||
smt::kernel m_context;
|
||||
cuber* m_cuber;
|
||||
random_gen m_rand;
|
||||
symbol m_logic;
|
||||
bool m_minimizing_core;
|
||||
bool m_core_extend_patterns;
|
||||
|
|
@ -84,16 +89,19 @@ namespace {
|
|||
updt_params(p);
|
||||
}
|
||||
|
||||
solver * translate(ast_manager & m, params_ref const & p) override {
|
||||
ast_translation translator(get_manager(), m);
|
||||
solver * translate(ast_manager & target, params_ref const & p) override {
|
||||
ast_translation translator(get_manager(), target);
|
||||
params_ref init;
|
||||
init.copy(get_params());
|
||||
init.copy(p);
|
||||
|
||||
smt_solver * result = alloc(smt_solver, m, p, m_logic);
|
||||
smt_solver* result = alloc(smt_solver, target, init, m_logic);
|
||||
smt::kernel::copy(m_context, result->m_context, true);
|
||||
|
||||
if (mc0())
|
||||
if (mc0())
|
||||
result->set_model_converter(mc0()->translate(translator));
|
||||
|
||||
for (auto & [k, v] : m_name2assertion) {
|
||||
for (auto& [k, v] : m_name2assertion) {
|
||||
expr* val = translator(k);
|
||||
expr* key = translator(v);
|
||||
result->assert_expr(val, key);
|
||||
|
|
@ -212,6 +220,88 @@ namespace {
|
|||
return m_context.get_trail(max_level);
|
||||
}
|
||||
|
||||
expr_ref_vector get_assigned_literals() override {
|
||||
expr_ref_vector result(m);
|
||||
auto const& ctx = m_context.get_context();
|
||||
for (auto lit : ctx.assigned_literals()) {
|
||||
expr* atom = ctx.bool_var2expr(lit.var());
|
||||
if (!atom)
|
||||
continue;
|
||||
result.push_back(lit.sign() ? m.mk_not(atom) : atom);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
unsigned get_assign_level(expr* e) const override {
|
||||
auto const& ctx = m_context.get_context();
|
||||
get_manager().is_not(e, e);
|
||||
if (!ctx.b_internalized(e))
|
||||
return UINT_MAX;
|
||||
return ctx.get_assign_level(ctx.get_bool_var(e));
|
||||
}
|
||||
|
||||
bool is_relevant(expr* e) const override {
|
||||
auto const& ctx = m_context.get_context();
|
||||
get_manager().is_not(e, e);
|
||||
return ctx.b_internalized(e) && ctx.is_relevant(e);
|
||||
}
|
||||
|
||||
unsigned get_num_bool_vars() const override {
|
||||
return m_context.get_context().get_num_bool_vars();
|
||||
}
|
||||
|
||||
sat::bool_var get_bool_var(expr* e) const override {
|
||||
auto const& ctx = m_context.get_context();
|
||||
get_manager().is_not(e, e);
|
||||
return ctx.b_internalized(e) ? ctx.get_bool_var(e) : sat::null_bool_var;
|
||||
}
|
||||
|
||||
void pop_to_base_level() override {
|
||||
m_context.pop_to_base_level();
|
||||
}
|
||||
|
||||
void setup_for_parallel() override {
|
||||
m_context.get_context().setup_for_parallel();
|
||||
}
|
||||
|
||||
void set_preprocess(bool f) override {
|
||||
m_context.set_preprocess(f);
|
||||
}
|
||||
|
||||
void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
|
||||
ast_manager& m = get_manager();
|
||||
auto& ctx = m_context.get_context();
|
||||
unsigned curr_time = ctx.get_num_assignments();
|
||||
vector<solver::scored_literal> all;
|
||||
|
||||
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
|
||||
if (ctx.get_assignment(v) != l_undef && ctx.get_assign_level(v) == ctx.get_base_level())
|
||||
continue;
|
||||
|
||||
expr* candidate = ctx.bool_var2expr(v);
|
||||
if (!candidate)
|
||||
continue;
|
||||
|
||||
auto const& d = ctx.get_bdata(v);
|
||||
if (d.m_phase_available && !d.m_phase)
|
||||
candidate = m.mk_not(candidate);
|
||||
|
||||
double age = static_cast<double>(curr_time - ctx.get_birthdate(v));
|
||||
all.push_back(solver::scored_literal(m, candidate, age));
|
||||
}
|
||||
|
||||
std::stable_sort(
|
||||
all.begin(),
|
||||
all.end(),
|
||||
[](solver::scored_literal const& a, solver::scored_literal const& b) {
|
||||
return a.score > b.score;
|
||||
});
|
||||
|
||||
unsigned n = std::min<unsigned>(max_num, all.size());
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
candidates.push_back(all[i]);
|
||||
}
|
||||
|
||||
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
|
||||
m_context.register_on_clause(ctx, on_clause);
|
||||
}
|
||||
|
|
@ -347,6 +437,53 @@ namespace {
|
|||
|
||||
expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override {
|
||||
ast_manager& m = get_manager();
|
||||
parallel_params pp(get_params());
|
||||
if (!pp.cube_lookahead()) {
|
||||
auto& ctx = m_context.get_context();
|
||||
expr_mark selected_vars;
|
||||
for (expr* v : vars)
|
||||
selected_vars.mark(v);
|
||||
struct candidate {
|
||||
expr* e;
|
||||
double score;
|
||||
};
|
||||
vector<candidate> candidates;
|
||||
|
||||
ctx.pop_to_search_level();
|
||||
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
|
||||
if (ctx.get_assignment(v) != l_undef)
|
||||
continue;
|
||||
expr* e = ctx.bool_var2expr(v);
|
||||
if (!e)
|
||||
continue;
|
||||
if (!vars.empty() && !selected_vars.is_marked(e))
|
||||
continue;
|
||||
candidates.push_back({ e, ctx.get_activity(v) });
|
||||
}
|
||||
|
||||
std::stable_sort(candidates.begin(), candidates.end(),
|
||||
[](candidate const& a, candidate const& b) {
|
||||
return a.score > b.score;
|
||||
});
|
||||
for (unsigned i = 0, j = 0; i < candidates.size(); i = j) {
|
||||
j = i + 1;
|
||||
while (j < candidates.size() && candidates[i].score == candidates[j].score)
|
||||
++j;
|
||||
if (j > i + 1)
|
||||
shuffle(j - i, candidates.data() + i, m_rand);
|
||||
}
|
||||
|
||||
vars.reset();
|
||||
expr_ref_vector lits(m);
|
||||
for (auto const &c : candidates) {
|
||||
vars.push_back(c.e);
|
||||
if (lits.size() < cutoff)
|
||||
lits.push_back(c.e);
|
||||
}
|
||||
|
||||
return lits;
|
||||
}
|
||||
|
||||
if (!m_cuber) {
|
||||
m_cuber = alloc(cuber, *this);
|
||||
// force propagation
|
||||
|
|
@ -537,4 +674,3 @@ public:
|
|||
solver_factory * mk_smt_solver_factory() {
|
||||
return alloc(smt_solver_factory);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,10 @@ def_module_params('parallel',
|
|||
('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'),
|
||||
('enable2', BOOL, False, 'enable (experimental) parallel solver by default on selected tactics (for QF_BV)'),
|
||||
('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
|
||||
('num_bb_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'),
|
||||
('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'),
|
||||
('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'),
|
||||
('cube.lookahead', BOOL, False, 'use lookahead cubing in the parallel solver; when false, use VSIDS activity to select one split literal'),
|
||||
('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'),
|
||||
('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
|
||||
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
#include "solver/check_sat_result.h"
|
||||
#include "solver/progress_callback.h"
|
||||
#include "util/params.h"
|
||||
#include "util/sat_literal.h"
|
||||
|
||||
class solver;
|
||||
class model_converter;
|
||||
|
|
@ -58,6 +59,13 @@ class solver : public check_sat_result, public user_propagator::core {
|
|||
params_ref m_params;
|
||||
symbol m_cancel_backup_file;
|
||||
public:
|
||||
struct scored_literal {
|
||||
expr_ref lit;
|
||||
double score = 0.0;
|
||||
scored_literal(ast_manager& m, expr* e, double s): lit(e, m), score(s) {}
|
||||
scored_literal(expr_ref const& e, double s): lit(e), score(s) {}
|
||||
};
|
||||
|
||||
solver(ast_manager& m): check_sat_result(m) {}
|
||||
|
||||
/**
|
||||
|
|
@ -298,9 +306,26 @@ public:
|
|||
expr_ref_vector get_non_units();
|
||||
|
||||
virtual expr_ref_vector get_trail(unsigned max_level) = 0; // { return expr_ref_vector(get_manager()); }
|
||||
virtual expr_ref_vector get_assigned_literals() { return get_trail(UINT_MAX); }
|
||||
virtual unsigned get_assign_level(expr* e) const { return UINT_MAX; }
|
||||
virtual bool is_relevant(expr* e) const { return true; }
|
||||
virtual unsigned get_num_bool_vars() const { return UINT_MAX; }
|
||||
virtual sat::bool_var get_bool_var(expr* e) const { return sat::null_bool_var; }
|
||||
virtual expr* bool_var2expr(sat::bool_var) const { return nullptr; }
|
||||
virtual lbool get_assignment(sat::bool_var) const { return l_undef; }
|
||||
virtual double get_activity(sat::bool_var) const { return 0.0; }
|
||||
virtual bool was_eliminated(sat::bool_var) const { return false; }
|
||||
|
||||
virtual void pop_to_base_level() {}
|
||||
|
||||
virtual void setup_for_parallel() {}
|
||||
|
||||
virtual void set_preprocess(bool) {}
|
||||
|
||||
virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;
|
||||
|
||||
virtual void get_backbone_candidates(vector<scored_literal>&, unsigned) {}
|
||||
|
||||
class scoped_push {
|
||||
solver& s;
|
||||
bool m_nopop;
|
||||
|
|
|
|||
|
|
@ -50,7 +50,6 @@ namespace search_tree {
|
|||
unsigned m_effort_spent = 0;
|
||||
unsigned m_round_max_effort = 0;
|
||||
unsigned m_active_workers = 0;
|
||||
unsigned m_cancel_epoch = 0;
|
||||
|
||||
public:
|
||||
node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {}
|
||||
|
|
@ -68,9 +67,17 @@ namespace search_tree {
|
|||
literal const &get_literal() const {
|
||||
return m_literal;
|
||||
}
|
||||
bool path_contains_atom(literal const& l) const {
|
||||
for (node const* n = this; n; n = n->parent())
|
||||
if (!Config::literal_is_null(n->get_literal()) && Config::same_atom(n->get_literal(), l))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
void split(literal const &a, literal const &b) {
|
||||
SASSERT(!Config::literal_is_null(a));
|
||||
SASSERT(!Config::literal_is_null(b));
|
||||
VERIFY(!path_contains_atom(a));
|
||||
VERIFY(!path_contains_atom(b));
|
||||
if (m_status != status::active)
|
||||
return;
|
||||
SASSERT(!m_left);
|
||||
|
|
@ -148,12 +155,6 @@ namespace search_tree {
|
|||
m_round_max_effort = effort;
|
||||
m_effort_spent += m_round_max_effort;
|
||||
}
|
||||
unsigned get_cancel_epoch() const {
|
||||
return m_cancel_epoch;
|
||||
}
|
||||
void inc_cancel_epoch() {
|
||||
++m_cancel_epoch;
|
||||
}
|
||||
};
|
||||
|
||||
template <typename Config> class tree {
|
||||
|
|
@ -340,7 +341,6 @@ namespace search_tree {
|
|||
void close(node<Config> *n, vector<literal> const &C) {
|
||||
if (!n || n->get_status() == status::closed)
|
||||
return;
|
||||
n->inc_cancel_epoch();
|
||||
n->set_status(status::closed);
|
||||
n->set_core(C);
|
||||
close(n->left(), C);
|
||||
|
|
@ -444,8 +444,8 @@ namespace search_tree {
|
|||
|
||||
// On timeout, either expand the current leaf or reopen the node for a
|
||||
// later revisit, depending on the tree-expansion heuristic.
|
||||
bool try_split(node<Config> *n, unsigned cancel_epoch, literal const &a, literal const &b, unsigned effort) {
|
||||
if (is_lease_canceled(n, cancel_epoch))
|
||||
bool try_split(node<Config> *n, literal const &a, literal const &b, unsigned effort) {
|
||||
if (is_lease_canceled(n))
|
||||
return false;
|
||||
|
||||
// Record at most one effort contribution per concurrent round on this node.
|
||||
|
|
@ -544,8 +544,8 @@ namespace search_tree {
|
|||
n->dec_active_workers();
|
||||
}
|
||||
|
||||
bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {
|
||||
return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch;
|
||||
bool is_lease_canceled(node<Config>* n) const {
|
||||
return !n || n->get_status() == status::closed;
|
||||
}
|
||||
|
||||
vector<literal> const &get_core_from_root() const {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue