3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Fix a couple of typos.

This commit is contained in:
Bruce Mitchener 2018-11-28 14:58:04 +07:00
parent eea9b79035
commit 090f14e7bc

View file

@ -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'),