mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-04-03 15:51:09 -07:00
parent 67e9d74653
commit 1c96a7d52f
3 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,6 +29,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'),
('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'),

1
src/smt/params/theory_bv_params.cpp
View file

@ -22,4 +22,5 @@ Revision History:
void theory_bv_params::updt_params(params_ref const & _p) { void theory_bv_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p); smt_params_helper p(_p);
m_bv_reflect = p.bv_reflect(); m_bv_reflect = p.bv_reflect();
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
} }

1
src/util/gparams.cpp
View file

@ -49,6 +49,7 @@ char const * g_params_renames[] = {
"restart_factor", "smt.restart_factor", "restart_factor", "smt.restart_factor",
"arith_random_initial_value", "smt.arith.random_initial_value", "arith_random_initial_value", "smt.arith.random_initial_value",
"bv_reflect", "smt.bv.reflect", "bv_reflect", "smt.bv.reflect",
"bv_enable_int2bv_propagation", "smt.bv.enable_int2bv",
"qi_cost", "smt.qi.cost", "qi_cost", "smt.qi.cost",
"qi_eager_threshold", "smt.qi.eager_threshold", "qi_eager_threshold", "smt.qi.eager_threshold",
"nl_arith", "smt.arith.nl", "nl_arith", "smt.arith.nl",