mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fixed problems in the new parameter setting. Many thanks to Nuno Lopes for sending a benchmark that exposed the problem, a noticing the discrepancy between unstable and master branches.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e055e0b47c
commit
bd0366eef7
|
@ -5,7 +5,7 @@ def_module_params(class_name='pattern_inference_params_helper',
|
|||
params=(('max_multi_patterns', UINT, 0, 'when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern'),
|
||||
('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'),
|
||||
('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
|
||||
('use_database', BOOL, True, 'use pattern database'),
|
||||
('use_database', BOOL, False, 'use pattern database'),
|
||||
('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
|
||||
('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
|
||||
('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
|
||||
|
|
|
@ -7,7 +7,7 @@ def_module_params(module_name='smt',
|
|||
('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
|
||||
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
|
||||
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
|
||||
('phase_selection', UINT, 4, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
|
||||
('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
|
||||
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
|
||||
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
|
||||
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
|
||||
|
|
Loading…
Reference in a new issue