mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add sat option for doing a global simplification before the bounded search and the main CDCL search loop. The option is also used for the sat-preprocess tacitc (#4514)
Co-authored-by: rainoftime <rainoftime@gmail.com>
This commit is contained in:
parent
41430cd128
commit
55cd1e996c
|
@ -85,6 +85,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
m_burst_search = p.burst_search();
|
||||
m_enable_pre_simplify = p.enable_pre_simplify();
|
||||
|
||||
m_max_conflicts = p.max_conflicts();
|
||||
m_num_threads = p.threads();
|
||||
|
|
|
@ -108,6 +108,7 @@ namespace sat {
|
|||
double m_random_freq;
|
||||
unsigned m_random_seed;
|
||||
unsigned m_burst_search;
|
||||
bool m_enable_pre_simplify;
|
||||
unsigned m_max_conflicts;
|
||||
unsigned m_num_threads;
|
||||
bool m_ddfw_search;
|
||||
|
|
|
@ -27,6 +27,7 @@ def_module_params('sat',
|
|||
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
|
||||
('random_seed', UINT, 0, 'random seed'),
|
||||
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
|
||||
('enable_pre_simplify', BOOL, False, 'enable pre simplifications before the bounded search'),
|
||||
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
|
||||
('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
|
||||
('gc.initial', UINT, 20000, 'learned clauses garbage collection frequency'),
|
||||
|
|
|
@ -1222,6 +1222,16 @@ namespace sat {
|
|||
do_gc();
|
||||
}
|
||||
|
||||
if (m_config.m_enable_pre_simplify) {
|
||||
do_simplify();
|
||||
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;
|
||||
}
|
||||
|
||||
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
|
||||
m_restart_threshold = m_config.m_burst_search;
|
||||
lbool r = bounded_search();
|
||||
|
|
|
@ -229,6 +229,7 @@ tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref p_aux;
|
||||
p_aux.set_uint("max_conflicts", 0);
|
||||
p_aux.set_bool("enable_pre_simplify", true);
|
||||
tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux));
|
||||
t->updt_params(p);
|
||||
return t;
|
||||
|
|
Loading…
Reference in a new issue