mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

update smt_setup and default parameters to only use new solver consveratively

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-01 12:52:50 -07:00
parent 5a2a8d7d5c
commit 593a6e5139
3 changed files with 17 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ def_module_params(module_name='smt',
('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, True, '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, 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', 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.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'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

27
src/smt/smt_setup.cpp
View file

@ -332,7 +332,7 @@ namespace smt {
m_params.m_arith_propagate_eqs = false; m_params.m_arith_propagate_eqs = false;
m_params.m_arith_small_lemma_size = 30; m_params.m_arith_small_lemma_size = 30;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
setup_i_arith(); setup_lra_arith();
} }
void setup::setup_QF_IDL(static_features & st) { 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_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5; m_params.m_restart_factor = 1.5;
m_params.m_restart_adaptive = false; m_params.m_restart_adaptive = false;
setup_i_arith(); setup_lra_arith();
} }
void setup::setup_QF_UFIDL(static_features & st) { void setup::setup_QF_UFIDL(static_features & st) {
@ -454,7 +454,7 @@ namespace smt {
m_params.m_arith_propagate_eqs = false; m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true; m_params.m_eliminate_term_ite = true;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
setup_r_arith(); setup_lra_arith();
} }
void setup::setup_QF_LRA(static_features const & st) { void setup::setup_QF_LRA(static_features const & st) {
@ -479,7 +479,7 @@ namespace smt {
m_params.m_restart_adaptive = false; m_params.m_restart_adaptive = false;
} }
m_params.m_arith_small_lemma_size = 32; m_params.m_arith_small_lemma_size = 32;
setup_r_arith(); setup_lra_arith();
} }
void setup::setup_QF_LIRA(static_features const& st) { 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_reflect = false;
m_params.m_arith_propagate_eqs = false; m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
setup_i_arith(); setup_lra_arith();
} }
void setup::setup_QF_LIA(static_features const & st) { 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_bound_prop = BP_NONE;
m_params.m_arith_stronger_lemmas = false; m_params.m_arith_stronger_lemmas = false;
} }
setup_i_arith(); setup_lra_arith();
} }
void setup::setup_QF_UFLIA() { void setup::setup_QF_UFLIA() {
@ -542,7 +542,7 @@ namespace smt {
m_params.m_arith_reflect = false; m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
m_params.m_arith_propagation_threshold = 1000; m_params.m_arith_propagation_threshold = 1000;
setup_i_arith(); setup_lra_arith();
} }
void setup::setup_QF_UFLIA(static_features & st) { void setup::setup_QF_UFLIA(static_features & st) {
@ -555,7 +555,7 @@ namespace smt {
m_params.m_relevancy_lvl = 0; m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false; m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
setup_r_arith(); setup_lra_arith();
} }
void setup::setup_QF_BV() { void setup::setup_QF_BV() {
@ -744,11 +744,11 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
} }
else { 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)); 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)); m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));
break; break;
case AS_NEW_ARITH: case AS_NEW_ARITH:
setup_r_arith(); setup_lra_arith();
break; break;
default: default:
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
@ -827,8 +827,11 @@ namespace smt {
else else
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break; break;
case AS_NEW_ARITH:
setup_lra_arith();
break;
default: default:
setup_i_arith(); m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break; break;
} }
} }

2
src/smt/smt_setup.h
View file

@ -101,7 +101,7 @@ namespace smt {
void setup_card(); void setup_card();
void setup_i_arith(); void setup_i_arith();
void setup_mi_arith(); void setup_mi_arith();
void setup_r_arith(); void setup_lra_arith();
void setup_fpa(); void setup_fpa();
void setup_str(); void setup_str();