mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
fde8808a40
commit
46107022f7
|
@ -2225,6 +2225,7 @@ namespace sat {
|
|||
bool solver::should_restart() const {
|
||||
if (m_conflicts_since_restart <= m_restart_threshold) return false;
|
||||
if (scope_lvl() < 2 + search_lvl()) return false;
|
||||
if (m_case_split_queue.empty()) return false;
|
||||
if (m_config.m_restart != RS_EMA) return true;
|
||||
return
|
||||
m_fast_glue_avg + search_lvl() <= scope_lvl() &&
|
||||
|
@ -2315,9 +2316,9 @@ namespace sat {
|
|||
}
|
||||
|
||||
unsigned solver::restart_level(bool to_base) {
|
||||
if (to_base || scope_lvl() == search_lvl()) {
|
||||
return scope_lvl() - search_lvl();
|
||||
}
|
||||
SASSERT(!m_case_split_queue.empty());
|
||||
if (to_base || scope_lvl() == search_lvl())
|
||||
return scope_lvl() - search_lvl();
|
||||
else {
|
||||
bool_var next = m_case_split_queue.min_var();
|
||||
|
||||
|
|
Loading…
Reference in a new issue