mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

exposed sat params

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-02 16:38:33 -08:00
parent 773f82a44c
commit 0934cb06d8
8 changed files with 111 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/sat/sat_asymm_branch.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include"sat_asymm_branch.h"
#include"sat_asymm_branch_params.hpp"
#include"sat_solver.h"
#include"stopwatch.h"
#include"trace.h"
@ -193,18 +194,17 @@ namespace sat {
}
}
void asymm_branch::updt_params(params_ref const & p) {
m_asymm_branch = p.get_bool("asymm_branch", true);
m_asymm_branch_rounds = p.get_uint("asymm_branch_rounds", 32);
m_asymm_branch_limit = p.get_uint("asymm_branch_limit", 100000000);
void asymm_branch::updt_params(params_ref const & _p) {
sat_asymm_branch_params p(_p);
m_asymm_branch = p.asymm_branch();
m_asymm_branch_rounds = p.asymm_branch_rounds();
m_asymm_branch_limit = p.asymm_branch_limit();
if (m_asymm_branch_limit > INT_MAX)
m_asymm_branch_limit = INT_MAX;
}
void asymm_branch::collect_param_descrs(param_descrs & d) {
d.insert("asymm_branch", CPK_BOOL, "(default: true) asymmetric branching.");
d.insert("asymm_branch_rounds", CPK_UINT, "(default: 32) maximum number of rounds of asymmetric branching.");
d.insert("asymm_branch_limit", CPK_UINT, "approx. maximum number of literals visited during asymmetric branching.");
sat_asymm_branch_params::collect_param_descrs(d);
}
void asymm_branch::collect_statistics(statistics & st) {

6
src/sat/sat_asymm_branch_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params(module_name='sat',
class_name='sat_asymm_branch_params',
export=True,
params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
('asymm_branch.rounds', UINT, 32, 'maximum number of rounds of asymmetric branching'),
('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching')))

70
src/sat/sat_config.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include"sat_config.h"
#include"sat_types.h"
#include"sat_params.hpp"
namespace sat {
@ -36,10 +37,11 @@ namespace sat {
updt_params(p);
}
void config::updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
void config::updt_params(params_ref const & _p) {
sat_params p(_p);
m_max_memory = megabytes_to_bytes(p.max_memory());
symbol s = p.get_sym("restart", m_luby);
symbol s = p.restart();
if (s == m_luby)
m_restart = RS_LUBY;
else if (s == m_geometric)
@ -47,7 +49,7 @@ namespace sat {
else
throw sat_param_exception("invalid restart strategy");
s = p.get_sym("phase", m_caching);
s = p.phase();
if (s == m_always_false)
m_phase = PS_ALWAYS_FALSE;
else if (s == m_always_true)
@ -59,29 +61,31 @@ namespace sat {
else
throw sat_param_exception("invalid phase selection strategy");
m_phase_caching_on = p.get_uint("phase_caching_on", 400);
m_phase_caching_off = p.get_uint("phase_caching_off", 100);
m_phase_caching_on = p.phase_caching_on();
m_phase_caching_off = p.phase_caching_off();
m_restart_initial = p.get_uint("restart_initial", 100);
m_restart_factor = p.get_double("restart_factor", 1.5);
m_restart_initial = p.restart_initial();
m_restart_factor = p.restart_factor();
m_random_freq = p.get_double("random_freq", 0.01);
m_random_freq = p.random_freq();
m_burst_search = p.get_uint("burst_search", 100);
m_burst_search = p.burst_search();
m_max_conflicts = p.get_uint("max_conflicts", UINT_MAX);
m_max_conflicts = p.max_conflicts();
// These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);
m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5);
m_simplify_max = _p.get_uint("simplify_max", 500000);
// --------------------------------
m_simplify_mult1 = p.get_uint("simplify_mult1", 300);
m_simplify_mult2 = p.get_double("simplify_mult2", 1.5);
m_simplify_max = p.get_uint("simplify_max", 500000);
s = p.get_sym("gc_strategy", m_glue_psm);
s = p.gc();
if (s == m_dyn_psm) {
m_gc_strategy = GC_DYN_PSM;
m_gc_initial = p.get_uint("gc_initial", 500);
m_gc_increment = p.get_uint("gc_increment", 100);
m_gc_small_lbd = p.get_uint("gc_small_lbd", 3);
m_gc_k = p.get_uint("gc_k", 7);
m_gc_initial = p.gc_initial();
m_gc_increment = p.gc_increment();
m_gc_small_lbd = p.gc_small_lbd();
m_gc_k = p.gc_k();
if (m_gc_k > 255)
m_gc_k = 255;
}
@ -96,31 +100,15 @@ namespace sat {
m_gc_strategy = GC_PSM_GLUE;
else
throw sat_param_exception("invalid gc strategy");
m_gc_initial = p.get_uint("gc_initial", 20000);
m_gc_increment = p.get_uint("gc_increment", 500);
m_gc_initial = p.gc_initial();
m_gc_increment = p.gc_increment();
}
m_minimize_lemmas = p.get_bool("minimize_lemmas", true);
m_dyn_sub_res = p.get_bool("dyn_sub_res", true);
m_minimize_lemmas = p.minimize_lemmas();
m_dyn_sub_res = p.dyn_sub_res();
}
void config::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert("phase", CPK_SYMBOL, "(default: caching) phase selection strategy: always_false, always_true, caching, random.");
r.insert("phase_caching_on", CPK_UINT, "(default: 400)");
r.insert("phase_caching_off", CPK_UINT, "(default: 100)");
r.insert("restart", CPK_SYMBOL, "(default: luby) restart strategy: luby or geometric.");
r.insert("restart_initial", CPK_UINT, "(default: 100) initial restart (number of conflicts).");
r.insert("restart_factor", CPK_DOUBLE, "(default: 1.5) restart increment factor for geometric strategy.");
r.insert("random_freq", CPK_DOUBLE, "(default: 0.01) frequency of random case splits.");
r.insert("burst_search", CPK_UINT, "(default: 100) number of conflicts before first global simplification.");
r.insert("max_conflicts", CPK_UINT, "(default: inf) maximum number of conflicts.");
r.insert("gc_strategy", CPK_SYMBOL, "(default: glue_psm) garbage collection strategy: psm, glue, glue_psm, dyn_psm.");
r.insert("gc_initial", CPK_UINT, "(default: 20000) learned clauses garbage collection frequence.");
r.insert("gc_increment", CPK_UINT, "(default: 500) increment to the garbage collection threshold.");
r.insert("gc_small_lbd", CPK_UINT, "(default: 3) learned clauses with small LBD are never deleted (only used in dyn_psm).");
r.insert("gc_k", CPK_UINT, "(default: 7) learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm).");
r.insert("minimize_lemmas", CPK_BOOL, "(default: true) minimize learned clauses.");
r.insert("dyn_sub_res", CPK_BOOL, "(default: true) dynamic subsumption resolution for minimizing learned clauses.");
sat_params::collect_param_descrs(r);
}
};

20
src/sat/sat_params.pyg Normal file
View file

@ -0,0 +1,20 @@
def_module_params('sat',
export=True,
description='propositional SAT solver',
params=(max_memory_param(),
('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'),
('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
('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.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
('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 frequence'),
('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses')))

8
src/sat/sat_scc.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include"sat_elim_eqs.h"
#include"stopwatch.h"
#include"trace.h"
#include"sat_scc_params.hpp"
namespace sat {
@ -230,12 +231,13 @@ namespace sat {
m_num_elim = 0;
}
void scc::updt_params(params_ref const & p) {
m_scc = p.get_bool("scc", true);
void scc::updt_params(params_ref const & _p) {
sat_scc_params p(_p);
m_scc = p.scc();
}
void scc::collect_param_descrs(param_descrs & d) {
d.insert("scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components.");
sat_scc_params::collect_param_descrs(d);
}
};

5
src/sat/sat_scc_params.pyg Normal file
View file

@ -0,0 +1,5 @@
def_module_params(module_name='sat',
class_name='sat_scc_params',
export=True,
params=(('scc', BOOL, True, 'eliminate Boolean variables by computing strongly connected components'),))

56
src/sat/sat_simplifier.cpp
View file

@ -19,6 +19,7 @@ Revision History:
--*/
#include"sat_simplifier.h"
#include"sat_simplifier_params.hpp"
#include"sat_solver.h"
#include"stopwatch.h"
#include"trace.h"
@ -1430,45 +1431,28 @@ namespace sat {
m_new_cls.finalize();
}
void simplifier::updt_params(params_ref const & p) {
m_elim_blocked_clauses = p.get_bool("elim_blocked_clauses", false);
m_elim_blocked_clauses_at = p.get_uint("elim_blocked_clauses_at", 2);
m_blocked_clause_limit = p.get_uint("blocked_clause_limit", 100000000);
m_resolution = p.get_bool("resolution", true);
m_res_limit = p.get_uint("resolution_limit", 500000000);
m_res_occ_cutoff = p.get_uint("res_occ_cutoff", 10);
m_res_occ_cutoff1 = p.get_uint("res_occ_cutoff_range1", 8);
m_res_occ_cutoff2 = p.get_uint("res_occ_cutoff_range2", 5);
m_res_occ_cutoff3 = p.get_uint("res_occ_cutoff_range3", 3);
m_res_lit_cutoff1 = p.get_uint("res_lit_cutoff_range1", 700);
m_res_lit_cutoff2 = p.get_uint("res_lit_cutoff_range2", 400);
m_res_lit_cutoff3 = p.get_uint("res_lit_cutoff_range3", 300);
m_res_cls_cutoff1 = p.get_uint("res_cls_cutoff1", 100000);
m_res_cls_cutoff2 = p.get_uint("res_cls_cutoff2", 700000);
m_subsumption = p.get_bool("subsumption", true);
m_subsumption_limit = p.get_uint("subsumption_limit", 100000000);
void simplifier::updt_params(params_ref const & _p) {
sat_simplifier_params p(_p);
m_elim_blocked_clauses = p.elim_blocked_clauses();
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
m_blocked_clause_limit = p.blocked_clause_limit();
m_resolution = p.resolution();
m_res_limit = p.resolution_limit();
m_res_occ_cutoff = p.resolution_occ_cutoff();
m_res_occ_cutoff1 = p.resolution_occ_cutoff_range1();
m_res_occ_cutoff2 = p.resolution_occ_cutoff_range2();
m_res_occ_cutoff3 = p.resolution_occ_cutoff_range3();
m_res_lit_cutoff1 = p.resolution_lit_cutoff_range1();
m_res_lit_cutoff2 = p.resolution_lit_cutoff_range2();
m_res_lit_cutoff3 = p.resolution_lit_cutoff_range3();
m_res_cls_cutoff1 = p.resolution_cls_cutoff1();
m_res_cls_cutoff2 = p.resolution_cls_cutoff2();
m_subsumption = p.subsumption();
m_subsumption_limit = p.subsumption_limit();
}
void simplifier::collect_param_descrs(param_descrs & r) {
r.insert("elim_blocked_clauses", CPK_BOOL, "(default: false) eliminate blocked clauses.");
r.insert("elim_blocked_clauses_at", CPK_UINT, "(default: 2) eliminate blocked clauses only once at the given simplification round.");
r.insert("blocked_clause_limit", CPK_UINT, "(default: 100000000) maximum number of literals visited during blocked clause elimination.");
r.insert("resolution", CPK_BOOL, "(default: true) eliminate boolean variables using resolution.");
r.insert("resolution_limit", CPK_UINT, "(default: 500000000) approx. maximum number of literals visited during variable elimination.");
r.insert("res_occ_cutoff", CPK_UINT, "(default: 10) first cutoff (on number of positive/negative occurrences) for Boolean variable elimination.");
r.insert("res_occ_cutoff_range1", CPK_UINT, "(default: 8) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
r.insert("res_occ_cutoff_range2", CPK_UINT, "(default: 5) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
r.insert("res_occ_cutoff_range3", CPK_UINT, "(default: 3) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
r.insert("res_lit_cutoff_range1", CPK_UINT, "(default: 700) second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
r.insert("res_lit_cutoff_range2", CPK_UINT, "(default: 400) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
r.insert("res_lit_cutoff_range3", CPK_UINT, "(default: 300) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
r.insert("res_cls_cutoff1", CPK_UINT, "(default: 100000000) limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
r.insert("res_cls_cutoff2", CPK_UINT, "(default: 700000000) limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
r.insert("subsumption", CPK_BOOL, "(default: true) eliminate subsumed clauses.");
r.insert("subsumption_limit", CPK_UINT, "(default: 100000000) approx. maximum number of literals visited during subsumption (and subsumption resolution).");
sat_simplifier_params::collect_param_descrs(r);
}
void simplifier::collect_statistics(statistics & st) {

19
src/sat/sat_simplifier_params.pyg Normal file
View file

@ -0,0 +1,19 @@
def_module_params(module_name='sat',
class_name='sat_simplifier_params',
export=True,
params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
('resolution', BOOL, True, 'eliminate boolean variables using resolution'),
('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),
('resolution.occ_cutoff', UINT, 10, 'first cutoff (on number of positive/negative occurrences) for Boolean variable elimination'),
('resolution.occ_cutoff_range1', UINT, 8, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
('resolution.occ_cutoff_range2', UINT, 5, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
('resolution.occ_cutoff_range3', UINT, 3, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
('resolution.lit_cutoff_range1', UINT, 700, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
('resolution.lit_cutoff_range2', UINT, 400, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
('resolution.lit_cutoff_range3', UINT, 300, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))