From 529f116be084470af275715d7691143ee04c038e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Nov 2022 22:29:59 -0800 Subject: [PATCH] disable new code until pre-condition gets fixed Signed-off-by: Nikolaj Bjorner --- src/ast/static_features.cpp | 6 + src/ast/static_features.h | 4 +- src/math/simplex/model_based_opt.cpp | 9 +- src/smt/params/smt_params.cpp | 228 +++++++++++++++++++++++++++ src/smt/params/smt_params.h | 44 ++++++ src/smt/smt_setup.cpp | 198 +++-------------------- 6 files changed, 311 insertions(+), 178 deletions(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index ad289cf5e..c5dedb16b 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -665,3 +665,9 @@ void static_features::display(std::ostream & out) const { void static_features::get_feature_vector(vector & result) { } + +bool static_features::is_dense() const { + return + (m_num_uninterpreted_constants < 1000) && + (m_num_arith_eqs + m_num_arith_ineqs) > m_num_uninterpreted_constants * 9; +} diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 92e0331fb..59c6154ef 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -188,7 +188,9 @@ struct static_features { void get_feature_vector(vector & result); bool has_uf() const; unsigned num_theories() const; - unsigned num_non_uf_theories() const; + unsigned num_non_uf_theories() const; + + bool is_dense() const; }; diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 919e07b16..8df04327d 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -1462,11 +1462,14 @@ namespace opt { rational w_value = w == UINT_MAX ? offset : m_var2value[w]; -#if 1 - // V := (a * z_value - w_value) div rMod +#if 0 + // V := (a * z_value + w_value) div rMod // V*rMod <= a*z + w < (V+1)*rMod // v = a*z + w - V*rMod - SASSERT(a * z_value - w_value >= 0); + SASSERT(a > 0); + SASSERT(z_value >= 0); + SASSERT(w_value >= 0); + SASSERT(a * z_value + w_value >= 0); rational V = div(a * z_value + w_value, rMod); vector mod_coeffs; SASSERT(V >= 0); diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8143bc31b..2636d29f3 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -188,3 +188,231 @@ void smt_params::validate_string_solver(symbol const& s) const { return; throw default_exception("Invalid string solver value. Legal values are z3str3, seq, empty, auto, none"); } + +void smt_params::setup_QF_UF() { + m_relevancy_lvl = 0; + m_nnf_cnf = false; + m_restart_strategy = RS_LUBY; + m_phase_selection = PS_CACHING_CONSERVATIVE2; + m_random_initial_activity = IA_RANDOM; +} + +void smt_params::setup_QF_RDL() { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_RDL(static_features & st) { + +} + +void smt_params::setup_QF_IDL() { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_arith_small_lemma_size = 30; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_IDL(static_features & st) { + +} + +void smt_params::setup_QF_LRA() { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_eliminate_term_ite = true; + m_nnf_cnf = false; + m_phase_selection = PS_THEORY; +} + +void smt_params::setup_QF_LRA(static_features const& st) { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_eliminate_term_ite = true; + m_nnf_cnf = false; + if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) { + m_relevancy_lvl = 2; + m_relevancy_lemma = false; + } + m_phase_selection = PS_THEORY; + if (!st.m_cnf) { + m_restart_strategy = RS_GEOMETRIC; + m_arith_stronger_lemmas = false; + m_restart_adaptive = false; + } + m_arith_small_lemma_size = 32; +} + +void smt_params::setup_QF_LIA() { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_LIA(static_features const& st) { + m_relevancy_lvl = 0; + m_arith_eq2ineq = true; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_nnf_cnf = false; + if (st.m_max_ite_tree_depth > 50) { + m_arith_eq2ineq = false; + m_pull_cheap_ite = true; + m_arith_propagate_eqs = true; + m_relevancy_lvl = 2; + m_relevancy_lemma = false; + } + else if (st.m_num_clauses == st.m_num_units) { + m_arith_gcd_test = false; + m_arith_branch_cut_ratio = 4; + m_relevancy_lvl = 2; + m_arith_eq2ineq = true; + m_eliminate_term_ite = true; + } + else { + m_eliminate_term_ite = true; + m_restart_adaptive = false; + m_restart_strategy = RS_GEOMETRIC; + m_restart_factor = 1.5; + } + if (st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses && st.m_cnf && st.m_arith_k_sum > rational(100000)) { + m_arith_bound_prop = bound_prop_mode::BP_NONE; + m_arith_stronger_lemmas = false; + } +} + +void smt_params::setup_QF_UFLIA() { + m_relevancy_lvl = 0; + m_arith_reflect = false; + m_nnf_cnf = false; + m_arith_propagation_threshold = 1000; +} + + +void smt_params::setup_QF_UFLRA() { + m_relevancy_lvl = 0; + m_arith_reflect = false; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_BV() { + m_relevancy_lvl = 0; + m_arith_reflect = false; + m_bv_cc = false; + m_bb_ext_gates = true; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_AUFBV() { + m_array_mode = AR_SIMPLE; + m_relevancy_lvl = 0; + m_bv_cc = false; + m_bb_ext_gates = true; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_AX() { + m_array_mode = AR_SIMPLE; + m_nnf_cnf = false; +} + +void smt_params::setup_QF_AX(static_features const& st) { + m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE; + m_nnf_cnf = false; + if (st.m_num_clauses == st.m_num_units) { + m_relevancy_lvl = 0; + m_phase_selection = PS_ALWAYS_FALSE; + } + else + m_relevancy_lvl = 2; +} + +void smt_params::setup_QF_AUFLIA() { + m_array_mode = AR_SIMPLE; + m_nnf_cnf = false; + m_relevancy_lvl = 2; + m_restart_strategy = RS_GEOMETRIC; + m_restart_factor = 1.5; + m_phase_selection = PS_CACHING_CONSERVATIVE2; +} + +void smt_params::setup_QF_AUFLIA(static_features const& st) { + m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE; + if (st.m_has_real) + throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic)."); + m_nnf_cnf = false; + if (st.m_num_clauses == st.m_num_units) { + TRACE("QF_AUFLIA", tout << "using relevancy: 0\n";); + m_relevancy_lvl = 0; + m_phase_selection = PS_ALWAYS_FALSE; + } + else { + m_relevancy_lvl = 0; // it was 2, for some reason 2 doesn't work anymore TODO: investigate + m_restart_strategy = RS_GEOMETRIC; + m_restart_factor = 1.5; + m_phase_selection = PS_CACHING_CONSERVATIVE2; + m_random_initial_activity = IA_ZERO; + } +} + +void smt_params::setup_AUFLIA(bool simple_array) { + m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; + m_pi_use_database = true; + m_phase_selection = PS_ALWAYS_FALSE; + m_restart_strategy = RS_GEOMETRIC; + m_restart_factor = 1.5; + m_eliminate_bounds = true; + m_qi_quick_checker = MC_UNSAT; + m_qi_lazy_threshold = 20; + m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-) + + // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general) + // It destroys the existing patterns. + // m_macro_finder = true; + + if (m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; +} + +void smt_params::setup_AUFLIA(static_features const & st) { + m_qi_eager_threshold = st.m_num_quantifiers_with_patterns == 0 ? 5 : 7; +} + +void smt_params::setup_AUFLIRA(bool simple_array) { + m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; + m_phase_selection = PS_ALWAYS_FALSE; + m_eliminate_bounds = true; + m_qi_quick_checker = MC_UNSAT; + m_qi_eager_threshold = 5; + // Added for MBQI release + m_qi_lazy_threshold = 20; + // + m_macro_finder = true; + if (m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; + m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP + m_array_lazy_ieq = true; + m_array_lazy_ieq_delay = 4; + // + m_mbqi = true; // enabling MBQI by default :-) + // +} + +void smt_params::setup_LRA() { + m_relevancy_lvl = 0; + m_arith_reflect = false; + m_arith_propagate_eqs = false; + m_eliminate_term_ite = true; +} + diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 73f556eb8..96e8c9ceb 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -18,6 +18,7 @@ Revision History: --*/ #pragma once +#include "ast/static_features.h" #include "smt/params/dyn_ack_params.h" #include "smt/params/qi_params.h" #include "smt/params/theory_arith_params.h" @@ -254,6 +255,49 @@ struct smt_params : public preprocessor_params, void display(std::ostream & out) const; void validate_string_solver(symbol const& s) const; + + void setup_QF_UF(); + + void setup_QF_RDL(); + + void setup_QF_RDL(static_features & st); + + void setup_QF_IDL(); + + void setup_QF_IDL(static_features & st); + + void setup_QF_LRA(); + + void setup_QF_LRA(static_features const& st); + + void setup_QF_LIA(); + + void setup_QF_LIA(static_features const& st); + + void setup_QF_UFLIA(); + + void setup_QF_UFLRA(); + + void setup_QF_BV(); + + void setup_QF_AUFBV(); + + void setup_QF_AX(); + + void setup_QF_AX(static_features const& st); + + void setup_QF_AUFLIA(); + + void setup_QF_AUFLIA(static_features const& st); + + void setup_AUFLIA(bool simple_array); + + void setup_AUFLIA(static_features const & st); + + void setup_AUFLIRA(bool simple_array); + + void setup_LRA(); + }; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 2d131c6ab..ef5f5493c 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -212,11 +212,7 @@ namespace smt { } void setup::setup_QF_UF() { - m_params.m_relevancy_lvl = 0; - m_params.m_nnf_cnf = false; - m_params.m_restart_strategy = RS_LUBY; - m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; - m_params.m_random_initial_activity = IA_RANDOM; + m_params.setup_QF_UF(); } void setup::setup_QF_DT() { @@ -240,20 +236,10 @@ namespace smt { } void setup::setup_QF_RDL() { - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_nnf_cnf = false; + m_params.setup_QF_RDL(); setup_mi_arith(); } - static bool is_dense(static_features const & st) { - return - st.m_num_uninterpreted_constants < 1000 && - (st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9; - } - static bool is_in_diff_logic(static_features const & st) { return st.m_num_arith_eqs == st.m_num_diff_eqs && @@ -285,7 +271,7 @@ namespace smt { m_params.m_arith_reflect = false; m_params.m_arith_propagate_eqs = false; m_params.m_nnf_cnf = false; - if (is_dense(st)) { + if (st.is_dense()) { m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_adaptive = false; m_params.m_phase_selection = PS_CACHING; @@ -327,12 +313,7 @@ namespace smt { void setup::setup_QF_IDL() { TRACE("setup", tout << "setup_QF_IDL()\n";); - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_arith_small_lemma_size = 30; - m_params.m_nnf_cnf = false; + m_params.setup_QF_IDL(); setup_lra_arith(); } @@ -353,11 +334,11 @@ namespace smt { m_params.m_nnf_cnf = false; if (st.m_num_uninterpreted_constants > 5000) m_params.m_relevancy_lvl = 2; - else if (st.m_cnf && !is_dense(st)) + else if (st.m_cnf && !st.is_dense()) m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; else m_params.m_phase_selection = PS_CACHING; - if (is_dense(st) && st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses) { + if (st.is_dense() && st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses) { m_params.m_restart_adaptive = false; m_params.m_restart_strategy = RS_GEOMETRIC; } @@ -373,7 +354,7 @@ namespace smt { if (m_manager.proofs_enabled()) { m_context.register_plugin(alloc(smt::theory_mi_arith, m_context)); } - else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { + else if (!m_params.m_arith_auto_config_simplex && st.is_dense()) { TRACE("setup", tout << "using dense diff logic...\n";); m_params.m_phase_selection = PS_CACHING_CONSERVATIVE; if (st.arith_k_sum_is_small()) @@ -418,7 +399,7 @@ namespace smt { if (st.m_num_uninterpreted_functions == 0) { m_params.m_arith_eq2ineq = true; m_params.m_arith_propagate_eqs = false; - if (is_dense(st)) { + if (st.is_dense()) { m_params.m_arith_small_lemma_size = 128; m_params.m_lemma_gc_half = true; m_params.m_restart_strategy = RS_GEOMETRIC; @@ -449,35 +430,13 @@ namespace smt { void setup::setup_QF_LRA() { TRACE("setup", tout << "setup_QF_LRA()\n";); - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_eliminate_term_ite = true; - m_params.m_nnf_cnf = false; - m_params.m_phase_selection = PS_THEORY; + m_params.setup_QF_LRA(); setup_lra_arith(); } void setup::setup_QF_LRA(static_features const & st) { check_no_uninterpreted_functions(st, "QF_LRA"); - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_eliminate_term_ite = true; - m_params.m_nnf_cnf = false; - if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) { - m_params.m_relevancy_lvl = 2; - m_params.m_relevancy_lemma = false; - } - m_params.m_phase_selection = PS_THEORY; - if (!st.m_cnf) { - m_params.m_restart_strategy = RS_GEOMETRIC; - m_params.m_arith_stronger_lemmas = false; - m_params.m_restart_adaptive = false; - } - m_params.m_arith_small_lemma_size = 32; + m_params.setup_QF_LRA(st); setup_lra_arith(); } @@ -487,56 +446,20 @@ namespace smt { void setup::setup_QF_LIA() { TRACE("setup", tout << "setup_QF_LIA(st)\n";); - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_nnf_cnf = false; + m_params.setup_QF_LIA(); setup_lra_arith(); } void setup::setup_QF_LIA(static_features const & st) { check_no_uninterpreted_functions(st, "QF_LIA"); TRACE("setup", tout << "QF_LIA setup\n";); - - m_params.m_relevancy_lvl = 0; - m_params.m_arith_eq2ineq = true; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_nnf_cnf = false; - if (st.m_max_ite_tree_depth > 50) { - m_params.m_arith_eq2ineq = false; - m_params.m_pull_cheap_ite = true; - m_params.m_arith_propagate_eqs = true; - m_params.m_relevancy_lvl = 2; - m_params.m_relevancy_lemma = false; - } - else if (st.m_num_clauses == st.m_num_units) { - m_params.m_arith_gcd_test = false; - m_params.m_arith_branch_cut_ratio = 4; - m_params.m_relevancy_lvl = 2; - m_params.m_arith_eq2ineq = true; - m_params.m_eliminate_term_ite = true; - } - else { - m_params.m_eliminate_term_ite = true; - m_params.m_restart_adaptive = false; - m_params.m_restart_strategy = RS_GEOMETRIC; - m_params.m_restart_factor = 1.5; - } - if (st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses && st.m_cnf && st.m_arith_k_sum > rational(100000)) { - m_params.m_arith_bound_prop = bound_prop_mode::BP_NONE; - m_params.m_arith_stronger_lemmas = false; - } + m_params.setup_QF_LIA(st); setup_lra_arith(); } void setup::setup_QF_UFLIA() { - m_params.m_relevancy_lvl = 0; - m_params.m_arith_reflect = false; - m_params.m_nnf_cnf = false; - m_params.m_arith_propagation_threshold = 1000; setup_lra_arith(); + m_params.setup_QF_UFLIA(); } void setup::setup_QF_UFLIA(static_features & st) { @@ -548,103 +471,49 @@ namespace smt { } void setup::setup_QF_UFLRA() { - m_params.m_relevancy_lvl = 0; - m_params.m_arith_reflect = false; - m_params.m_nnf_cnf = false; + m_params.setup_QF_UFLRA(); setup_lra_arith(); } void setup::setup_QF_BV() { TRACE("setup", tout << "qf-bv\n";); - m_params.m_relevancy_lvl = 0; - m_params.m_arith_reflect = false; - m_params.m_bv_cc = false; - m_params.m_bb_ext_gates = true; - m_params.m_nnf_cnf = false; + m_params.setup_QF_BV(); m_context.register_plugin(alloc(smt::theory_bv, m_context)); } void setup::setup_QF_AUFBV() { - m_params.m_array_mode = AR_SIMPLE; - m_params.m_relevancy_lvl = 0; - m_params.m_bv_cc = false; - m_params.m_bb_ext_gates = true; - m_params.m_nnf_cnf = false; + m_params.setup_QF_AUFBV(); m_context.register_plugin(alloc(smt::theory_bv, m_context)); setup_arrays(); } void setup::setup_QF_AX() { TRACE("setup", tout << "QF_AX\n";); - m_params.m_array_mode = AR_SIMPLE; - m_params.m_nnf_cnf = false; + m_params.setup_QF_AX(); setup_arrays(); } void setup::setup_QF_AX(static_features const & st) { - m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE; - m_params.m_nnf_cnf = false; - if (st.m_num_clauses == st.m_num_units) { - m_params.m_relevancy_lvl = 0; - m_params.m_phase_selection = PS_ALWAYS_FALSE; - } - else { - m_params.m_relevancy_lvl = 2; - } + m_params.setup_QF_AX(st); setup_arrays(); } void setup::setup_QF_AUFLIA() { TRACE("QF_AUFLIA", tout << "no static features\n";); - m_params.m_array_mode = AR_SIMPLE; - m_params.m_nnf_cnf = false; - m_params.m_relevancy_lvl = 2; - m_params.m_restart_strategy = RS_GEOMETRIC; - m_params.m_restart_factor = 1.5; - m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; + m_params.setup_QF_AUFLIA(); setup_i_arith(); setup_arrays(); } void setup::setup_QF_AUFLIA(static_features const & st) { - m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE; - if (st.m_has_real) - throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic)."); - m_params.m_nnf_cnf = false; - if (st.m_num_clauses == st.m_num_units) { - TRACE("QF_AUFLIA", tout << "using relevancy: 0\n";); - m_params.m_relevancy_lvl = 0; - m_params.m_phase_selection = PS_ALWAYS_FALSE; - } - else { - m_params.m_relevancy_lvl = 0; // it was 2, for some reason 2 doesn't work anymore TODO: investigate - m_params.m_restart_strategy = RS_GEOMETRIC; - m_params.m_restart_factor = 1.5; - m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; - m_params.m_random_initial_activity = IA_ZERO; - } + m_params.setup_QF_AUFLIA(st); setup_i_arith(); setup_arrays(); } void setup::setup_AUFLIA(bool simple_array) { TRACE("setup", tout << "AUFLIA\n";); - m_params.m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; - m_params.m_pi_use_database = true; - m_params.m_phase_selection = PS_ALWAYS_FALSE; - m_params.m_restart_strategy = RS_GEOMETRIC; - m_params.m_restart_factor = 1.5; - m_params.m_eliminate_bounds = true; - m_params.m_qi_quick_checker = MC_UNSAT; - m_params.m_qi_lazy_threshold = 20; - m_params.m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-) - - // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general) - // It destroys the existing patterns. - // m_params.m_macro_finder = true; - - if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) - m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; + m_params.setup_AUFLIA(simple_array); TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); m_context.register_plugin(alloc(smt::theory_i_arith, m_context)); setup_arrays(); @@ -653,29 +522,13 @@ namespace smt { void setup::setup_AUFLIA(static_features const & st) { if (st.m_has_real) throw default_exception("Benchmark has real variables but it is marked as AUFLIA (arrays, uninterpreted functions and linear integer arithmetic)."); - m_params.m_qi_eager_threshold = st.m_num_quantifiers_with_patterns == 0 ? 5 : 7; + m_params.setup_AUFLIA(st); setup_AUFLIA(); } void setup::setup_AUFLIRA(bool simple_array) { TRACE("setup", tout << "AUFLIRA\n";); - m_params.m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; - m_params.m_phase_selection = PS_ALWAYS_FALSE; - m_params.m_eliminate_bounds = true; - m_params.m_qi_quick_checker = MC_UNSAT; - m_params.m_qi_eager_threshold = 5; - // Added for MBQI release - m_params.m_qi_lazy_threshold = 20; - // - m_params.m_macro_finder = true; - if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) - m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; - m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP - m_params.m_array_lazy_ieq = true; - m_params.m_array_lazy_ieq_delay = 4; - // - m_params.m_mbqi = true; // enabling MBQI by default :-) - // + m_params.setup_AUFLIRA(simple_array); setup_mi_arith(); setup_arrays(); } @@ -697,10 +550,7 @@ namespace smt { } void setup::setup_LRA() { - m_params.m_relevancy_lvl = 0; - m_params.m_arith_reflect = false; - m_params.m_arith_propagate_eqs = false; - m_params.m_eliminate_term_ite = true; + m_params.setup_LRA(); setup_mi_arith(); }