From 395a3042623d1bbd1cd15b3c5b11c52aff4b5270 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2020 21:34:54 -0700 Subject: [PATCH] add optional feature to bound search within ranges Signed-off-by: Nikolaj Bjorner --- 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 | 125 +++++++++++++++++++++++-- src/smt/theory_lra.h | 4 + 5 files changed, 129 insertions(+), 6 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c0d8548ca..81dec37eb 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -75,6 +75,7 @@ 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 5c0a7fe11..70285b681 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -38,6 +38,7 @@ 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(); @@ -78,6 +79,7 @@ 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(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 675cfce52..305b71177 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -82,6 +82,8 @@ 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 @@ -139,6 +141,7 @@ 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_SMALLEST), m_arith_add_binary_bounds(false), m_arith_propagation_strategy(ARITH_PROP_PROPORTIONAL), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4a5ba618b..9a7fd1598 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -932,7 +932,11 @@ public: m_solver(nullptr), m_resource_limit(*this), m_farkas("farkas"), - m_bp(*this) + m_bp(*this), + m_bounded_range_idx(0), + m_bounded_range_lit(null_literal), + m_bound_predicates(m), + m_bound_predicate(m) { } @@ -1769,7 +1773,13 @@ public: } // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) { - rational offset = k; + rational offset; + expr_ref t(m); + return mk_bound(term, k, lower_bound, offset, t); + } + + app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound, rational& offset, expr_ref& t) { + offset = k; u_map coeffs; term2coeffs(term, coeffs); bool is_int = true; @@ -1815,7 +1825,7 @@ public: // tout << "offset: " << offset << " gcd: " << g << "\n";); app_ref atom(m); - app_ref t = coeffs2app(coeffs, rational::zero(), is_int); + t = coeffs2app(coeffs, rational::zero(), is_int); if (lower_bound) { atom = a.mk_ge(t, a.mk_numeral(offset, is_int)); } @@ -2056,7 +2066,9 @@ public: app_ref b(m); bool u = m_lia->is_upper(); auto const & k = m_lia->get_offset(); - b = mk_bound(m_lia->get_term(), k, !u); + rational offset; + expr_ref t(m); + b = mk_bound(m_lia->get_term(), k, !u, offset, t); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_or(b, m.mk_not(b)); @@ -2071,6 +2083,7 @@ 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: { @@ -3874,6 +3887,100 @@ public: st.update("arith-assume-eqs", m_stats.m_assume_eqs); st.update("arith-branch", m_stats.m_branch); } + + /* + * Facility to put a small box around integer variables used in branch and bounds. + */ + + struct bound_info { + rational m_offset; + unsigned m_range; + bound_info() {} + bound_info(rational const& o, unsigned r):m_offset(o), m_range(r) {} + }; + unsigned m_bounded_range_idx; // current size of bounded range. + literal m_bounded_range_lit; // current bounded range literal + expr_ref_vector m_bound_predicates; // predicates used for bounds + expr_ref m_bound_predicate; + 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)); + 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); + 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; + VERIFY(m_term2bound_info.find(t, bi)); + 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_predicates.push_back(lo); + m_bound_predicates.push_back(hi); + IF_VERBOSE(10, verbose_stream() << "add " << lo << " " << hi << "\n"); + m_predicate2term.insert(lo, t); + m_predicate2term.insert(hi, t); + m_term2bound_info.insert(t, bi); + } + }; theory_lra::theory_lra(context& ctx): @@ -3888,8 +3995,7 @@ theory* theory_lra::mk_fresh(context* new_ctx) { } void theory_lra::init() { m_imp->init(); -} - +} bool theory_lra::internalize_atom(app * atom, bool gate_ctx) { return m_imp->internalize_atom(atom, gate_ctx); } @@ -3997,6 +4103,13 @@ 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); +} + } template class lp::lp_bound_propagator; template void lp::lar_solver::propagate_bounds_for_touched_rows(lp::lp_bound_propagator&); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 2522f0e79..128b3eb0d 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -95,6 +95,10 @@ namespace smt { void collect_statistics(::statistics & st) const 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;