mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-17 16:52:15 +00:00
Code Activity

Update sat_params.pyg

Browse source 
spellcheck from https://github.com/microsoft/z3guide/pull/165
This commit is contained in:
Nikolaj Bjorner 2024-01-12 09:49:56 -08:00 • committed by GitHub
parent 59b18d4a14
commit 27171591d1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_params.pyg
View file

@ -64,7 +64,7 @@ def_module_params('sat',
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'), ('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'), ('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'), ('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),
('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hessitant restart backoff'), ('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hesitant restart backoff'),
('ddfw.reinit_base', UINT, 10000, 'increment basis for geometric backoff scheme of re-initialization of weights'), ('ddfw.reinit_base', UINT, 10000, 'increment basis for geometric backoff scheme of re-initialization of weights'),
('ddfw.threads', UINT, 0, 'number of ddfw threads to run in parallel with sat solver'), ('ddfw.threads', UINT, 0, 'number of ddfw threads to run in parallel with sat solver'),
('prob_search', BOOL, False, 'use probsat local search instead of CDCL'), ('prob_search', BOOL, False, 'use probsat local search instead of CDCL'),
@ -105,7 +105,7 @@ def_module_params('sat',
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead_scores', BOOL, False, 'extract lookahead scores. A utility that can only be used from the DIMACS front-end'), ('lookahead_scores', BOOL, False, 'extract lookahead scores. A utility that can only be used from the DIMACS front-end'),
('lookahead.double', BOOL, True, 'enable doubld lookahead'), ('lookahead.double', BOOL, True, 'enable double lookahead'),
('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),