mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Fix whitespace issues in *.pyg.
This commit is contained in:
Bruce Mitchener
Nikolaj Bjorner
parent
0734c5f3f3
commit
e2122c0d3d
|
|
@ -3,7 +3,7 @@ def_module_params('fp',
|
|||
export=True,
|
||||
params=(('engine', SYMBOL, 'auto-config',
|
||||
'Select: auto-config, datalog, bmc, spacer'),
|
||||
('datalog.default_table', SYMBOL, 'sparse',
|
||||
('datalog.default_table', SYMBOL, 'sparse',
|
||||
'default table implementation: sparse, hashtable, bitvector, interval'),
|
||||
('datalog.default_relation', SYMBOL, 'pentagon',
|
||||
'default relation implementation: external_relation, pentagon'),
|
||||
|
|
@ -87,7 +87,7 @@ def_module_params('fp',
|
|||
('print_aig', SYMBOL, '',
|
||||
'Dump clauses in AIG text format (AAG) to the given file name'),
|
||||
('print_statistics', BOOL, False, 'print statistics'),
|
||||
('tab.selection', SYMBOL, 'weight',
|
||||
('tab.selection', SYMBOL, 'weight',
|
||||
'selection method for tabular strategy: weight (default), first, var-use'),
|
||||
('xform.bit_blast', BOOL, False,
|
||||
'bit-blast bit-vectors'),
|
||||
|
|
@ -104,7 +104,7 @@ def_module_params('fp',
|
|||
('xform.unfold_rules', UINT, 0,
|
||||
"unfold rules statically using iterative squaring"),
|
||||
('xform.slice', BOOL, True, "simplify clause set using slicing"),
|
||||
('xform.karr', BOOL, False,
|
||||
('xform.karr', BOOL, False,
|
||||
"Add linear invariants to clauses using Karr's method"),
|
||||
('spacer.use_euf_gen', BOOL, False, 'Generalize lemmas and pobs using implied equalities'),
|
||||
('xform.transform_arrays', BOOL, False,
|
||||
|
|
@ -117,9 +117,9 @@ def_module_params('fp',
|
|||
"Gives the number of quantifiers per array"),
|
||||
('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing",
|
||||
"<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true"),
|
||||
('xform.quantify_arrays', BOOL, False,
|
||||
('xform.quantify_arrays', BOOL, False,
|
||||
"create quantified Horn clauses from clauses with arrays"),
|
||||
('xform.instantiate_quantifiers', BOOL, False,
|
||||
('xform.instantiate_quantifiers', BOOL, False,
|
||||
"instantiate quantified Horn clauses using E-matching heuristic"),
|
||||
('xform.coalesce_rules', BOOL, False, "coalesce rules"),
|
||||
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
|
||||
|
|
@ -131,7 +131,7 @@ def_module_params('fp',
|
|||
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
|
||||
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
|
||||
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
|
||||
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
|
||||
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
|
||||
('xform.elim_term_ite', BOOL, False, 'Eliminate term-ite expressions'),
|
||||
('xform.elim_term_ite.inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)'),
|
||||
('spacer.propagate', BOOL, True, 'Enable propagate/pushing phase'),
|
||||
|
|
|
|||
|
|
@ -1,25 +1,25 @@
|
|||
def_module_params('sat',
|
||||
def_module_params('sat',
|
||||
export=True,
|
||||
description='propositional SAT solver',
|
||||
params=(max_memory_param(),
|
||||
('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, basic_caching, random, caching'),
|
||||
('phase.sticky', BOOL, True, 'use sticky phase caching'),
|
||||
('phase.sticky', BOOL, True, 'use sticky phase caching'),
|
||||
('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'),
|
||||
('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'),
|
||||
('rephase.base', UINT, 1000, 'number of conflicts per rephase '),
|
||||
('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),
|
||||
('reorder.itau', DOUBLE, 4.0, 'inverse temperature for softmax'),
|
||||
('reorder.activity_scale', UINT, 100, 'scaling factor for activity update'),
|
||||
('rephase.base', UINT, 1000, 'number of conflicts per rephase '),
|
||||
('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),
|
||||
('reorder.itau', DOUBLE, 4.0, 'inverse temperature for softmax'),
|
||||
('reorder.activity_scale', UINT, 100, 'scaling factor for activity update'),
|
||||
('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
|
||||
('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
|
||||
('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),
|
||||
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
||||
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
||||
('restart.fast', BOOL, True, 'use fast restart approach only removing less active literals.'),
|
||||
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
|
||||
('restart.margin', DOUBLE, 1.1, 'margin between fast and slow restart factors. For ema'),
|
||||
('restart.emafastglue', DOUBLE, 3e-2, 'ema alpha factor for fast moving average'),
|
||||
('restart.emaslowglue', DOUBLE, 1e-5, 'ema alpha factor for slow moving average'),
|
||||
('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'),
|
||||
('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'),
|
||||
('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
|
||||
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
|
||||
('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
|
||||
|
|
@ -40,8 +40,8 @@ def_module_params('sat',
|
|||
('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'),
|
||||
('backtrack.scopes', UINT, 100, 'number of scopes to enable chronological backtracking'),
|
||||
('backtrack.conflicts', UINT, 4000, 'number of conflicts before enabling chronological backtracking'),
|
||||
('backtrack.scopes', UINT, 100, 'number of scopes to enable chronological backtracking'),
|
||||
('backtrack.conflicts', UINT, 4000, 'number of conflicts before enabling chronological backtracking'),
|
||||
('threads', UINT, 1, 'number of parallel threads to use'),
|
||||
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
|
||||
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
|
||||
|
|
@ -51,7 +51,7 @@ def_module_params('sat',
|
|||
('cardinality.solver', BOOL, True, 'use cardinality solver'),
|
||||
('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)'),
|
||||
('pb.min_arity', UINT, 9, 'minimal arity to compile pb/cardinality constraints to CNF'),
|
||||
('xor.solver', BOOL, False, 'use xor solver'),
|
||||
('xor.solver', BOOL, False, 'use xor solver'),
|
||||
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
|
||||
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
|
||||
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
|
||||
|
|
@ -60,19 +60,19 @@ def_module_params('sat',
|
|||
('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.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'),
|
||||
('local_search', BOOL, False, 'use local search instead of CDCL'),
|
||||
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
|
||||
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
|
||||
('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'),
|
||||
('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
|
||||
('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
|
||||
('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
|
||||
('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'),
|
||||
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
|
||||
# - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
|
||||
# - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
|
||||
# So if the value is 10, at most 1024 cubes will be generated of length 10.
|
||||
# - freevars: cutoff based on a variable fraction of lookahead.cube.freevars.
|
||||
# - freevars: cutoff based on a variable fraction of lookahead.cube.freevars.
|
||||
# Cut if the number of current unassigned variables drops below a fraction of number of initial variables.
|
||||
# - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp
|
||||
# Cut if the value of psat_heur exceeds psat.trigger
|
||||
|
|
@ -98,7 +98,7 @@ def_module_params('sat',
|
|||
# reward function used to determine which literal to cube on.
|
||||
# - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March.
|
||||
# - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018
|
||||
# The score of a literal lit is:
|
||||
# The score of a literal lit is:
|
||||
# Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1)
|
||||
# * Sum_{lit' in C | lit' != lit} lit_occs(~lit')
|
||||
# / | C |
|
||||
|
|
@ -106,7 +106,7 @@ def_module_params('sat',
|
|||
# - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1)
|
||||
# - unit: heule_schur + also counts number of unit clauses.
|
||||
# - march_cu: default reward function used in a version of March
|
||||
# Each reward function also comes with its own variant of "mix_diff", which
|
||||
# is the function for combining reward metrics for the positive and negative variant of a literal.
|
||||
# Each reward function also comes with its own variant of "mix_diff", which
|
||||
# is the function for combining reward metrics for the positive and negative variant of a literal.
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
def_module_params(module_name='sat',
|
||||
def_module_params(module_name='sat',
|
||||
class_name='sat_simplifier_params',
|
||||
export=True,
|
||||
params=(('bce', BOOL, False, 'eliminate blocked clauses'),
|
||||
|
|
@ -8,7 +8,7 @@ def_module_params(module_name='sat',
|
|||
('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'),
|
||||
('bce_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
|
||||
('bca', BOOL, False, 'blocked clause addition - add blocked binary clauses'),
|
||||
('bce_delay', UINT, 2, 'delay eliminate blocked clauses until simplification round'),
|
||||
('bce_delay', UINT, 2, 'delay eliminate blocked clauses until simplification round'),
|
||||
('retain_blocked_clauses', BOOL, True, 'retain blocked clauses as lemmas'),
|
||||
('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
|
||||
('override_incremental', BOOL, False, 'override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),
|
||||
|
|
@ -24,7 +24,7 @@ def_module_params(module_name='sat',
|
|||
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
|
||||
('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
|
||||
('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
|
||||
('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
|
||||
('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
|
||||
('probing', BOOL, True, 'apply failed literal detection during simplification'),
|
||||
('probing_limit', UINT, 5000000, 'limit to the number of probe calls'),
|
||||
('probing_cache', BOOL, True, 'add binary literals as lemmas'),
|
||||
|
|
|
|||
|
|
@ -7,10 +7,10 @@ def_module_params('parallel',
|
|||
('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
|
||||
('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'),
|
||||
('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
|
||||
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
|
||||
('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
|
||||
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
|
||||
('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
|
||||
('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multiplied by simplify.exp ^ depth'),
|
||||
('simplify.max_conflicts', UINT, UINT_MAX, 'maximal number of conflicts during simplifcation phase'),
|
||||
('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
|
||||
('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
|
||||
('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
|
||||
))
|
||||
|
|
|
|||
Loading…
Reference in a new issue