mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
make linear search the default for theory_str
This commit is contained in:
parent
83230f944a
commit
a5180edc76
|
@ -74,7 +74,7 @@ def_module_params(module_name='smt',
|
|||
('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
|
||||
('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
|
||||
('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
|
||||
('str.use_binary_search', BOOL, True, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
|
||||
('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
|
||||
('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
|
||||
('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
|
||||
('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
|
||||
|
|
Loading…
Reference in a new issue