From 1c96a7d52f48b42891e5f40fa47e0b38c77a0b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2013 15:51:09 -0700 Subject: [PATCH] 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. Signed-off-by: Leonardo de Moura --- src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_bv_params.cpp | 1 + src/util/gparams.cpp | 1 + 3 files changed, 3 insertions(+) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 43dd1b586..21b5c6281 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -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.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'), ('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.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'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index c2a31c59d..d3f386ab4 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -22,4 +22,5 @@ Revision History: void theory_bv_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); m_bv_reflect = p.bv_reflect(); + m_bv_enable_int2bv2int = p.bv_enable_int2bv(); } diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 8b1fbe40e..3b2e8edc1 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -49,6 +49,7 @@ char const * g_params_renames[] = { "restart_factor", "smt.restart_factor", "arith_random_initial_value", "smt.arith.random_initial_value", "bv_reflect", "smt.bv.reflect", + "bv_enable_int2bv_propagation", "smt.bv.enable_int2bv", "qi_cost", "smt.qi.cost", "qi_eager_threshold", "smt.qi.eager_threshold", "nl_arith", "smt.arith.nl",