From e2122c0d3d1302e3e71af083d2aada558e04b8e0 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 15 Aug 2019 13:20:23 +0700 Subject: [PATCH] Fix whitespace issues in *.pyg. --- src/muz/base/fp_params.pyg | 12 +++++------ src/sat/sat_params.pyg | 36 +++++++++++++++---------------- src/sat/sat_simplifier_params.pyg | 6 +++--- src/solver/parallel_params.pyg | 6 +++--- 4 files changed, 30 insertions(+), 30 deletions(-) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 71aaf188156..111a274de1f 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -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", "=> GetId(i) = i, => 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'), diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 1e72ceaa58e..3650cafd1fb 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -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. ) diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 60ca4a49b5e..93864ce2472 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -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'), diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index c238fca03ba..628d4242af6 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -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'), ))