mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

User control over more arith options

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-24 11:40:25 -07:00
parent cfeee55d4f
commit b17be763d3
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -54,6 +54,8 @@ def_module_params(module_name='smt',
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
('arith.eager_eq_axioms', BOOL, True, 'eager equality axioms'),
('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
('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'),

3
src/smt/params/theory_arith_params.cpp
View file

@ -37,6 +37,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
arith_rewriter_params ap(_p);
m_arith_eq2ineq = ap.eq2ineq();
}