diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 3757aad2d..60ca4a49b 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -2,7 +2,7 @@ def_module_params(module_name='sat', class_name='sat_simplifier_params', export=True, params=(('bce', BOOL, False, 'eliminate blocked clauses'), - ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), + ('abce', BOOL, False, 'eliminate blocked clauses using asymmetric literals'), ('cce', BOOL, False, 'eliminate covered clauses'), ('ate', BOOL, True, 'asymmetric tautology elimination'), ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'), @@ -11,7 +11,7 @@ def_module_params(module_name='sat', ('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 incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'), + ('override_incremental', BOOL, False, 'override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'), ('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'),