From 12697767778532b237c03fe7415935b72c7ef1a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Nov 2020 11:46:19 -0800 Subject: [PATCH] remove experimental option. Fix #4806 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_solver.cpp | 23 +------ src/sat/smt/arith_solver.h | 2 - src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_arith_params.cpp | 2 - src/smt/params/theory_arith_params.h | 3 - src/smt/theory_lra.cpp | 85 +------------------------- src/smt/theory_lra.h | 4 -- 7 files changed, 2 insertions(+), 118 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index bb3336cd7..3f11d8388 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1056,7 +1056,6 @@ namespace arith { // SAT core assigns a value to lia_check = l_false; ++m_stats.m_branch; - add_variable_bound(t, offset); break; } case lp::lia_move::cut: { @@ -1167,27 +1166,6 @@ namespace arith { } } - void solver::add_variable_bound(expr* t, rational const& offset) { - if (!use_bounded_expansion()) - return; - if (m_bounded_range_lit == sat::null_literal) - return; - // if term is not already bounded, add a range and assert max_bound => range - bound_info bi(offset, init_range()); - if (m_term2bound_info.find(t, bi)) - return; - expr_ref hi(a.mk_le(t, a.mk_int(offset + bi.m_range)), m); - expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m); - add_clause(~m_bounded_range_lit, mk_literal(hi)); - add_clause(~m_bounded_range_lit, mk_literal(lo)); - m_bound_terms.push_back(lo); - m_bound_terms.push_back(hi); - m_bound_terms.push_back(t); - m_predicate2term.insert(lo, t); - m_predicate2term.insert(hi, t); - m_term2bound_info.insert(t, bi); - } - void solver::reset_evidence() { m_core.reset(); m_eqs.reset(); @@ -1204,6 +1182,7 @@ namespace arith { app_ref s(a.mk_numeral(offset, isint), m); return eq_internalize(t, s); } + // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false app_ref solver::mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) { rational offset; diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index cd66c00ad..507080c75 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -346,7 +346,6 @@ namespace arith { lbool make_feasible(); lbool check_lia(); lbool check_nla(); - void add_variable_bound(expr* t, rational const& offset); bool is_infeasible() const; nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const; @@ -375,7 +374,6 @@ namespace arith { obj_map m_term2bound_info; bool m_model_is_initialized{ false }; - bool use_bounded_expansion() const { return get_config().m_arith_bounded_expansion; } unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; } bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; } bool should_propagate() const { return bound_prop_mode::BP_NONE != propagation_mode(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 46f2cf175..227604b26 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -83,7 +83,6 @@ def_module_params(module_name='smt', ('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'), ('arith.rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info'), ('arith.min', BOOL, False, 'minimize cost'), - ('arith.bounded_expansion', BOOL, False, 'box variables used in branch and bound into bound assumptions'), ('arith.print_stats', BOOL, False, 'print statistic'), ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index ce9ff5fbc..6906c5940 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -38,7 +38,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { 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(); - m_arith_bounded_expansion = p.arith_bounded_expansion(); arith_rewriter_params ap(_p); m_arith_eq2ineq = ap.eq2ineq(); @@ -79,7 +78,6 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_arith_adaptive_gcd); DISPLAY_PARAM(m_arith_propagation_threshold); DISPLAY_PARAM(m_arith_pivot_strategy); - DISPLAY_PARAM(m_arith_bounded_expansion); DISPLAY_PARAM(m_arith_add_binary_bounds); DISPLAY_PARAM((unsigned)m_arith_propagation_strategy); DISPLAY_PARAM(m_arith_eq_bounds); diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 6abb75b10..623f91fd0 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -83,8 +83,6 @@ struct theory_arith_params { bool m_arith_adaptive_gcd; unsigned m_arith_propagation_threshold; - bool m_arith_bounded_expansion; - arith_pivot_strategy m_arith_pivot_strategy; // used in diff-logic @@ -142,7 +140,6 @@ struct theory_arith_params { m_arith_eager_gcd(false), m_arith_adaptive_gcd(false), m_arith_propagation_threshold(UINT_MAX), - m_arith_bounded_expansion(false), 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), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bf10cda82..3f99108c4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1926,7 +1926,6 @@ public: // SAT core assigns a value to lia_check = l_false; ++m_stats.m_branch; - add_variable_bound(t, offset); break; } case lp::lia_move::cut: { @@ -3733,86 +3732,9 @@ public: obj_map m_predicate2term; obj_map m_term2bound_info; - bool use_bounded_expansion() const { - return ctx().get_fparams().m_arith_bounded_expansion; - } - unsigned init_range() const { return 5; } unsigned max_range() const { return 20; } - void add_theory_assumptions(expr_ref_vector& assumptions) { - if (!use_bounded_expansion()) - return; - ctx().push_trail(value_trail(m_bounded_range_lit)); - if (!m_bound_predicate || !m_term2bound_info.empty()) - m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort()); - m_bounded_range_lit = mk_literal(m_bound_predicate); - // add max-unfolding literal - // add variable bounds - assumptions.push_back(m_bound_predicate); - for (auto const& kv : m_term2bound_info) { - bound_info const& bi = kv.m_value; - expr* t = kv.m_key; - expr_ref hi(a.mk_le(t, a.mk_int(bi.m_offset + bi.m_range)), m); - expr_ref lo(a.mk_ge(t, a.mk_int(bi.m_offset - bi.m_range)), m); - assumptions.push_back(lo); - assumptions.push_back(hi); - m_predicate2term.insert(lo, t); - m_predicate2term.insert(hi, t); - IF_VERBOSE(10, verbose_stream() << lo << "\n" << hi << "\n"); - } - } - - bool should_research(expr_ref_vector& unsat_core) { - if (!use_bounded_expansion()) - return false; - bool found = false; - expr* t = nullptr; - for (auto & e : unsat_core) { - if (e == m_bound_predicate) { - found = true; - for (auto & kv : m_term2bound_info) - if (kv.m_value.m_range == init_range()) - kv.m_value.m_range *= 2; - } - else if (m_predicate2term.find(e, t)) { - found = true; - bound_info bi; - if (!m_term2bound_info.find(t, bi)) { - TRACE("arith", tout << "bound information for term " << mk_pp(t, m) << " not found\n";); - } - else if (bi.m_range >= max_range()) { - m_term2bound_info.erase(t); - } - else { - bi.m_range *= 2; - m_term2bound_info.insert(t, bi); - } - } - } - return found; - } - - void add_variable_bound(expr* t, rational const& offset) { - if (!use_bounded_expansion()) - return; - if (m_bounded_range_lit == null_literal) - return; - // if term is not already bounded, add a range and assert max_bound => range - bound_info bi(offset, init_range()); - if (m_term2bound_info.find(t, bi)) - return; - expr_ref hi(a.mk_le(t, a.mk_int(offset + bi.m_range)), m); - expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m); - mk_axiom(~m_bounded_range_lit, mk_literal(hi)); - mk_axiom(~m_bounded_range_lit, mk_literal(lo)); - m_bound_terms.push_back(lo); - m_bound_terms.push_back(hi); - m_bound_terms.push_back(t); - m_predicate2term.insert(lo, t); - m_predicate2term.insert(hi, t); - m_term2bound_info.insert(t, bi); - } void setup() { m_bounded_range_lit = null_literal; @@ -3945,12 +3867,7 @@ theory_var theory_lra::add_objective(app* term) { expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) { return m_imp->mk_ge(fm, v, val); } -void theory_lra::add_theory_assumptions(expr_ref_vector& assumptions) { - m_imp->add_theory_assumptions(assumptions); -} -bool theory_lra::should_research(expr_ref_vector& unsat_core) { - return m_imp->should_research(unsat_core); -} + void theory_lra::setup() { m_imp->setup(); } diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 041a930ee..b7d271079 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -97,10 +97,6 @@ namespace smt { void setup() override; - void add_theory_assumptions(expr_ref_vector& assumptions) override; - - bool should_research(expr_ref_vector& unsat_core) override; - // optimization expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val); inf_eps value(theory_var) override;