mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

change opt.maxlen.enable default to true to prefer this over all other heuristics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-26 13:02:25 -08:00
parent 1297eeb817
commit d0b2f73c0c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_params.pyg
View file

@ -14,7 +14,7 @@ def_module_params('opt',
('elim_01', BOOL, True, 'eliminate 01 variables'), ('elim_01', BOOL, True, 'eliminate 01 variables'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
('maxlex.enable', BOOL, False, 'enable maxlex heuristic for lexicographic MaxSAT problems'), ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'), ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),