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

Merge pull request #1977 from waywardmonkeys/fix-typos

Fix a couple of typos.
This commit is contained in:
Nikolaj Bjorner 2018-11-28 09:04:35 -08:00 committed by GitHub
commit 649eb53ef9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

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