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

Re-enabled the smt.arith.greatest_error_pivot parameter.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-23 18:01:00 +01:00
parent 27f9dec926
commit 9912b2cd67
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/params/smt_params_helper.pyg
View file

@ -44,7 +44,8 @@ def_module_params(module_name='smt',
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),