mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

toggle default for bv2int decision procedure support to avoid confusing users. Issue #301

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-10 15:09:52 -05:00
parent 746689904d
commit 315dc80eb0
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -33,7 +33,7 @@ def_module_params(module_name='smt',
('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'), ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'), ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'), ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),

2
src/smt/params/theory_bv_params.h
View file

@ -39,7 +39,7 @@ struct theory_bv_params {
m_bv_lazy_le(false), m_bv_lazy_le(false),
m_bv_cc(false), m_bv_cc(false),
m_bv_blast_max_size(INT_MAX), m_bv_blast_max_size(INT_MAX),
m_bv_enable_int2bv2int(false) { m_bv_enable_int2bv2int(true) {
updt_params(p); updt_params(p);
} }