mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

enable SAT solver by default for MaxSAT constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-02 17:09:01 -07:00
parent 26c53d055a
commit bd162588b2
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_params.pyg
View file

@ -8,7 +8,7 @@ def_module_params('opt',
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('print_model', BOOL, False, 'display model for satisfiable constraints'), ('print_model', BOOL, False, 'display model for satisfiable constraints'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('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)'),