From cdcfbeb6d88a1b0274228e14842df1c5ae2b6314 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Sep 2021 16:01:59 -0700 Subject: [PATCH] #5532 remove "reflect" parameter from exposed options. It should be internal only. --- src/sat/smt/arith_solver.cpp | 5 +- src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_arith_params.cpp | 1 - src/smt/params/theory_arith_params.h | 138 +++++++++---------------- 4 files changed, 48 insertions(+), 97 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 6ceea42f2..2f9c44cc8 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -605,8 +605,7 @@ namespace arith { else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, *m_a1); if (a.is_int(o) && !m_nla->am().is_int(an)) - value = a.mk_numeral(rational::zero(), a.is_int(o)); - else + value = a.mk_numeral(rational::zero(), a.is_int(o)); value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); } else if (v != euf::null_theory_var) { @@ -617,7 +616,7 @@ namespace arith { r = floor(r); value = a.mk_numeral(r, o->get_sort()); } - else if (a.is_arith_expr(o)) { + else if (a.is_arith_expr(o) && reflect(o)) { expr_ref_vector args(m); for (auto* arg : *to_app(o)) { if (m.is_value(arg)) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f0a715e96..20839ea8a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -74,7 +74,6 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), - ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 6906c5940..deec4e4da 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -35,7 +35,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_dump_lemmas = p.arith_dump_lemmas(); - m_arith_reflect = p.arith_reflect(); m_arith_eager_eq_axioms = p.arith_eager_eq_axioms(); m_arith_auto_config_simplex = p.arith_auto_config_simplex(); diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 623f91fd0..d45a902db 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -51,110 +51,64 @@ enum class arith_pivot_strategy { inline std::ostream& operator<<(std::ostream& out, arith_pivot_strategy st) { return out << (int)st; } struct theory_arith_params { - bool m_arith_eq2ineq; - bool m_arith_process_all_eqs; - arith_solver_id m_arith_mode; - bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config - unsigned m_arith_blands_rule_threshold; - bool m_arith_propagate_eqs; - bound_prop_mode m_arith_bound_prop; - bool m_arith_stronger_lemmas; - bool m_arith_skip_rows_with_big_coeffs; - unsigned m_arith_max_lemma_size; - unsigned m_arith_small_lemma_size; - bool m_arith_reflect; - bool m_arith_ignore_int; - unsigned m_arith_lazy_pivoting_lvl; - unsigned m_arith_random_seed; - bool m_arith_random_initial_value; - int m_arith_random_lower; - int m_arith_random_upper; - bool m_arith_adaptive; - double m_arith_adaptive_assertion_threshold; - double m_arith_adaptive_propagation_threshold; - bool m_arith_dump_lemmas; - bool m_arith_eager_eq_axioms; - unsigned m_arith_branch_cut_ratio; - bool m_arith_int_eq_branching; - bool m_arith_enum_const_mod; + bool m_arith_eq2ineq = false; + bool m_arith_process_all_eqs = false; + arith_solver_id m_arith_mode = arith_solver_id::AS_NEW_ARITH; + bool m_arith_auto_config_simplex = false; //!< force simplex solver in auto_config + unsigned m_arith_blands_rule_threshold = 1000; + bool m_arith_propagate_eqs = true; + bound_prop_mode m_arith_bound_prop = bound_prop_mode::BP_REFINE; + bool m_arith_stronger_lemmas = true; + bool m_arith_skip_rows_with_big_coeffs = true; + unsigned m_arith_max_lemma_size = 128; + unsigned m_arith_small_lemma_size = 16; + bool m_arith_reflect = true; + bool m_arith_ignore_int = false; + unsigned m_arith_lazy_pivoting_lvl = 0; + unsigned m_arith_random_seed = 0; + bool m_arith_random_initial_value = false; + int m_arith_random_lower = -1000; + int m_arith_random_upper = 1000; + bool m_arith_adaptive = false; + double m_arith_adaptive_assertion_threshold = 0.2; + double m_arith_adaptive_propagation_threshold = 0.4; + bool m_arith_dump_lemmas = false; + bool m_arith_eager_eq_axioms = true; + unsigned m_arith_branch_cut_ratio = 2; + bool m_arith_int_eq_branching = false; + bool m_arith_enum_const_mod = false; - bool m_arith_gcd_test; - bool m_arith_eager_gcd; - bool m_arith_adaptive_gcd; - unsigned m_arith_propagation_threshold; + bool m_arith_gcd_test = true; + bool m_arith_eager_gcd = false; + bool m_arith_adaptive_gcd = false; + unsigned m_arith_propagation_threshold = UINT_MAX; - arith_pivot_strategy m_arith_pivot_strategy; + arith_pivot_strategy m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_SMALLEST; // used in diff-logic - bool m_arith_add_binary_bounds; - arith_prop_strategy m_arith_propagation_strategy; + bool m_arith_add_binary_bounds = false; + arith_prop_strategy m_arith_propagation_strategy = arith_prop_strategy::ARITH_PROP_PROPORTIONAL; // used arith_eq_adapter - bool m_arith_eq_bounds; - bool m_arith_lazy_adapter; + bool m_arith_eq_bounds = false; + bool m_arith_lazy_adapter = false; // performance debugging flags - bool m_arith_fixnum; - bool m_arith_int_only; + bool m_arith_fixnum = false; + bool m_arith_int_only = false; // non linear support - bool m_nl_arith; - bool m_nl_arith_gb; - unsigned m_nl_arith_gb_threshold; - bool m_nl_arith_gb_eqs; - bool m_nl_arith_gb_perturbate; - unsigned m_nl_arith_max_degree; - bool m_nl_arith_branching; - unsigned m_nl_arith_rounds; + bool m_nl_arith = true; + bool m_nl_arith_gb = true; + unsigned m_nl_arith_gb_threshold = 512; + bool m_nl_arith_gb_eqs = false; + bool m_nl_arith_gb_perturbate = true; + unsigned m_nl_arith_max_degree = 6; + bool m_nl_arith_branching = true; + unsigned m_nl_arith_rounds = 1024; - - theory_arith_params(params_ref const & p = params_ref()): - m_arith_eq2ineq(false), - m_arith_process_all_eqs(false), - m_arith_mode(arith_solver_id::AS_NEW_ARITH), - m_arith_auto_config_simplex(false), - m_arith_blands_rule_threshold(1000), - m_arith_propagate_eqs(true), - m_arith_bound_prop(bound_prop_mode::BP_REFINE), - m_arith_stronger_lemmas(true), - m_arith_skip_rows_with_big_coeffs(true), - m_arith_max_lemma_size(128), - m_arith_small_lemma_size(16), - m_arith_reflect(true), - m_arith_ignore_int(false), - m_arith_lazy_pivoting_lvl(0), - m_arith_random_seed(0), - m_arith_random_initial_value(false), - m_arith_random_lower(-1000), - m_arith_random_upper(1000), - m_arith_adaptive(false), - m_arith_adaptive_assertion_threshold(0.2), - m_arith_adaptive_propagation_threshold(0.4), - m_arith_dump_lemmas(false), - m_arith_eager_eq_axioms(true), - m_arith_branch_cut_ratio(2), - m_arith_int_eq_branching(false), - m_arith_enum_const_mod(false), - m_arith_gcd_test(true), - m_arith_eager_gcd(false), - m_arith_adaptive_gcd(false), - m_arith_propagation_threshold(UINT_MAX), - m_arith_pivot_strategy(arith_pivot_strategy::ARITH_PIVOT_SMALLEST), - m_arith_add_binary_bounds(false), - m_arith_propagation_strategy(arith_prop_strategy::ARITH_PROP_PROPORTIONAL), - m_arith_eq_bounds(false), - m_arith_lazy_adapter(false), - m_arith_fixnum(false), - m_arith_int_only(false), - m_nl_arith(true), - m_nl_arith_gb(true), - m_nl_arith_gb_threshold(512), - m_nl_arith_gb_eqs(false), - m_nl_arith_gb_perturbate(true), - m_nl_arith_max_degree(6), - m_nl_arith_branching(true), - m_nl_arith_rounds(1024) { + theory_arith_params(params_ref const & p = params_ref()) { updt_params(p); }