From 593a6e51393373f18fb4fb5c909217ce196c0e4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 12:52:50 -0700 Subject: [PATCH] update smt_setup and default parameters to only use new solver consveratively Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_setup.cpp | 27 +++++++++++++++------------ src/smt/smt_setup.h | 2 +- 3 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c39b74722..3f4105c34 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -40,7 +40,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('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.solver', UINT, 6, '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 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), + ('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 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 8977ddb2a..ca3c01189 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -332,7 +332,7 @@ namespace smt { m_params.m_arith_propagate_eqs = false; m_params.m_arith_small_lemma_size = 30; m_params.m_nnf_cnf = false; - setup_i_arith(); + setup_lra_arith(); } void setup::setup_QF_IDL(static_features & st) { @@ -404,7 +404,7 @@ namespace smt { m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_factor = 1.5; m_params.m_restart_adaptive = false; - setup_i_arith(); + setup_lra_arith(); } void setup::setup_QF_UFIDL(static_features & st) { @@ -454,7 +454,7 @@ namespace smt { m_params.m_arith_propagate_eqs = false; m_params.m_eliminate_term_ite = true; m_params.m_nnf_cnf = false; - setup_r_arith(); + setup_lra_arith(); } void setup::setup_QF_LRA(static_features const & st) { @@ -479,7 +479,7 @@ namespace smt { m_params.m_restart_adaptive = false; } m_params.m_arith_small_lemma_size = 32; - setup_r_arith(); + setup_lra_arith(); } void setup::setup_QF_LIRA(static_features const& st) { @@ -493,7 +493,7 @@ namespace smt { m_params.m_arith_reflect = false; m_params.m_arith_propagate_eqs = false; m_params.m_nnf_cnf = false; - setup_i_arith(); + setup_lra_arith(); } void setup::setup_QF_LIA(static_features const & st) { @@ -534,7 +534,7 @@ namespace smt { m_params.m_arith_bound_prop = BP_NONE; m_params.m_arith_stronger_lemmas = false; } - setup_i_arith(); + setup_lra_arith(); } void setup::setup_QF_UFLIA() { @@ -542,7 +542,7 @@ namespace smt { m_params.m_arith_reflect = false; m_params.m_nnf_cnf = false; m_params.m_arith_propagation_threshold = 1000; - setup_i_arith(); + setup_lra_arith(); } void setup::setup_QF_UFLIA(static_features & st) { @@ -555,7 +555,7 @@ namespace smt { m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; m_params.m_nnf_cnf = false; - setup_r_arith(); + setup_lra_arith(); } void setup::setup_QF_BV() { @@ -744,11 +744,11 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); } else { - setup_r_arith(); + setup_lra_arith(); } } - void setup::setup_r_arith() { + void setup::setup_lra_arith() { m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } @@ -758,7 +758,7 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params)); break; case AS_NEW_ARITH: - setup_r_arith(); + setup_lra_arith(); break; default: m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); @@ -827,8 +827,11 @@ namespace smt { else m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); break; + case AS_NEW_ARITH: + setup_lra_arith(); + break; default: - setup_i_arith(); + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); break; } } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 924c2caec..ed0ab066d 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -101,7 +101,7 @@ namespace smt { void setup_card(); void setup_i_arith(); void setup_mi_arith(); - void setup_r_arith(); + void setup_lra_arith(); void setup_fpa(); void setup_str();