mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
add restart.max parameter to control cancellation based on restart count
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2bd29548da
commit
aaf6e67ec8
|
@ -47,7 +47,6 @@ namespace opt {
|
|||
m_first(true),
|
||||
m_was_unknown(false) {
|
||||
m_params.updt_params(p);
|
||||
std::cout << "Case split strategy " << m_params.m_case_split_strategy << "\n";
|
||||
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
|
||||
m_params.m_relevancy_lvl = 0;
|
||||
}
|
||||
|
|
|
@ -26,6 +26,7 @@ namespace sat {
|
|||
m_always_true("always_true"),
|
||||
m_always_false("always_false"),
|
||||
m_caching("caching"),
|
||||
m_restart_max(0),
|
||||
m_random("random"),
|
||||
m_geometric("geometric"),
|
||||
m_luby("luby"),
|
||||
|
@ -66,7 +67,8 @@ namespace sat {
|
|||
|
||||
m_restart_initial = p.restart_initial();
|
||||
m_restart_factor = p.restart_factor();
|
||||
|
||||
m_restart_max = p.restart_max();
|
||||
|
||||
m_random_freq = p.random_freq();
|
||||
m_random_seed = p.random_seed();
|
||||
if (m_random_seed == 0)
|
||||
|
|
|
@ -52,6 +52,7 @@ namespace sat {
|
|||
restart_strategy m_restart;
|
||||
unsigned m_restart_initial;
|
||||
double m_restart_factor; // for geometric case
|
||||
unsigned m_restart_max;
|
||||
double m_random_freq;
|
||||
unsigned m_random_seed;
|
||||
unsigned m_burst_search;
|
||||
|
|
|
@ -7,6 +7,7 @@ def_module_params('sat',
|
|||
('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
|
||||
('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
|
||||
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
|
||||
('restart.max', UINT, 0, 'maximal number of restarts. Ignored if set to 0'),
|
||||
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
|
||||
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
|
||||
('random_seed', UINT, 0, 'random seed'),
|
||||
|
|
|
@ -744,7 +744,6 @@ namespace sat {
|
|||
simplify_problem();
|
||||
if (check_inconsistent()) return l_false;
|
||||
|
||||
|
||||
if (m_config.m_max_conflicts == 0) {
|
||||
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
|
||||
return l_undef;
|
||||
|
@ -766,6 +765,12 @@ namespace sat {
|
|||
simplify_problem();
|
||||
if (check_inconsistent()) return l_false;
|
||||
gc();
|
||||
|
||||
if (m_config.m_restart_max != 0 && m_config.m_restart_max <= m_restarts) {
|
||||
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
catch (abort_solver) {
|
||||
|
@ -1126,6 +1131,7 @@ namespace sat {
|
|||
m_restart_threshold = m_config.m_restart_initial;
|
||||
m_luby_idx = 1;
|
||||
m_gc_threshold = m_config.m_gc_initial;
|
||||
m_restarts = 0;
|
||||
m_min_d_tk = 1.0;
|
||||
m_stopwatch.reset();
|
||||
m_stopwatch.start();
|
||||
|
@ -1308,6 +1314,7 @@ namespace sat {
|
|||
|
||||
void solver::restart() {
|
||||
m_stats.m_restart++;
|
||||
m_restarts++;
|
||||
IF_VERBOSE(1,
|
||||
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
|
||||
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
|
||||
|
|
|
@ -293,6 +293,7 @@ namespace sat {
|
|||
|
||||
protected:
|
||||
unsigned m_conflicts;
|
||||
unsigned m_restarts;
|
||||
unsigned m_conflicts_since_restart;
|
||||
unsigned m_restart_threshold;
|
||||
unsigned m_luby_idx;
|
||||
|
|
Loading…
Reference in a new issue