diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index a7209306a..81d631e4e 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -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) { diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg new file mode 100644 index 000000000..8940c64a6 --- /dev/null +++ b/src/sat/sat_asymm_branch_params.pyg @@ -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'))) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index e30569d89..cc0f97ff0 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -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); } }; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg new file mode 100644 index 000000000..71579b86a --- /dev/null +++ b/src/sat/sat_params.pyg @@ -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'))) diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index f2598119f..29f3f006f 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -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); } }; diff --git a/src/sat/sat_scc_params.pyg b/src/sat/sat_scc_params.pyg new file mode 100644 index 000000000..b88de4de8 --- /dev/null +++ b/src/sat/sat_scc_params.pyg @@ -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'),)) + diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 8a1713647..623c73758 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -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) { diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg new file mode 100644 index 000000000..6165e7e62 --- /dev/null +++ b/src/sat/sat_simplifier_params.pyg @@ -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)')))