mirror of
https://github.com/Z3Prover/z3
synced 2025-08-29 06:28:57 +00:00
26 lines
2.4 KiB
Text
26 lines
2.4 KiB
Text
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.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
|
('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'),
|
|
('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'),
|
|
('core.minimize', BOOL, False, 'minimize computed core'),
|
|
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
|
|
('parallel_threads', UINT, 1, 'number of parallel threads to use'),
|
|
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
|