From 3f6ecfb3b6dae2c3e4dde7c658d4b6366a769359 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 14 Jun 2019 17:32:07 -0700 Subject: [PATCH] generate lemmas from nla_intervals Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 84 +++++++--- src/math/lp/explanation.h | 4 +- src/math/lp/lar_solver.cpp | 21 +++ src/math/lp/lar_solver.h | 6 + src/math/lp/lp_bound_propagator.cpp | 133 +-------------- src/math/lp/lp_bound_propagator.h | 21 +-- src/math/lp/nla_basics_lemmas.cpp | 14 +- src/math/lp/nla_core.cpp | 3 +- src/math/lp/nla_core.h | 4 +- src/math/lp/nla_intervals.cpp | 130 +++++++-------- src/math/lp/nla_intervals.h | 249 ++++++++++++++-------------- src/math/lp/nla_solver.cpp | 24 +-- src/math/lp/nla_solver.h | 7 - 13 files changed, 292 insertions(+), 408 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 73fcd1212..8682232a7 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -30,7 +30,7 @@ namespace lp { template // C plays a role of a container class bound_analyzer_on_row { const C& m_row; - lp_bound_propagator & m_bp; + lp_bound_propagator & m_bp; unsigned m_row_or_term_index; int m_column_of_u; // index of an unlimited from above monoid // -1 means that such a value is not found, -2 means that at least two of such monoids were found @@ -55,8 +55,9 @@ public : m_rs(rs) {} + + unsigned j; void analyze() { - TRACE("lp_bound_prop", print_linear_combination_of_column_indices_only(m_row, tout); tout << " = " << m_rs << "\n";); for (const auto & c : m_row) { if ((m_column_of_l == -2) && (m_column_of_u == -2)) break; @@ -79,53 +80,86 @@ public : } bool upper_bound_is_available(unsigned j) const { - return m_bp.upper_bound_is_available(j); + switch (m_bp.get_column_type(j)) + { + case column_type::fixed: + case column_type::boxed: + case column_type::upper_bound: + return true; + default: + return false; + } } bool lower_bound_is_available(unsigned j) const { - return m_bp.lower_bound_is_available(j); + switch (m_bp.get_column_type(j)) + { + case column_type::fixed: + case column_type::boxed: + case column_type::lower_bound: + return true; + default: + return false; + } } - impq ub(unsigned j) const { + const impq & ub(unsigned j) const { lp_assert(upper_bound_is_available(j)); return m_bp.get_upper_bound(j); } - impq lb(unsigned j) const { + const impq & lb(unsigned j) const { lp_assert(lower_bound_is_available(j)); return m_bp.get_lower_bound(j); } - mpq u_strict(unsigned j, bool & strict) const { - const impq u = ub(j); - strict = !is_zero(u.y); - return u.x; - } - mpq l_strict(unsigned j, bool & strict) const { - const impq l = lb(j); - strict = !is_zero(l.y); - return l.x; - } - - mpq monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const { - return a_is_pos? u_strict(j, strict) : l_strict(j, strict); + const mpq & monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const { + if (a_is_pos) { + strict = !is_zero(ub(j).y); + return ub(j).x; + } + strict = !is_zero(lb(j).y); + return lb(j).x; } mpq monoid_max(const mpq & a, unsigned j) const { - return a * (is_pos(a) ? ub(j).x : lb(j).x); + if (is_pos(a)) { + return a * ub(j).x; + } + return a * lb(j).x; } mpq monoid_max(const mpq & a, unsigned j, bool & strict) const { - return a * (is_pos(a)? u_strict(j, strict) : l_strict(j, strict)); + if (is_pos(a)) { + strict = !is_zero(ub(j).y); + return a * ub(j).x; + } + strict = !is_zero(lb(j).y); + return a * lb(j).x; } - mpq monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { - return a_is_pos? l_strict(j, strict) : u_strict(j, strict); + const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { + if (!a_is_pos) { + strict = !is_zero(ub(j).y); + return ub(j).x; + } + strict = !is_zero(lb(j).y); + return lb(j).x; } mpq monoid_min(const mpq & a, unsigned j, bool& strict) const { - return a * (is_neg(a)? u_strict(j, strict) : l_strict(j, strict)); + if (is_neg(a)) { + strict = !is_zero(ub(j).y); + return a * ub(j).x; + } + + strict = !is_zero(lb(j).y); + return a * lb(j).x; } mpq monoid_min(const mpq & a, unsigned j) const { - return a * (is_neg(a)? ub(j).x : lb(j).x ); + if (is_neg(a)) { + return a * ub(j).x; + } + + return a * lb(j).x; } diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index b2558818e..62b21aa0d 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -37,8 +37,10 @@ public: m_explanation.push_back(std::make_pair(one_of_type(), j)); } + void add(const explanation& e) { for (auto j: e.m_set_of_ci) add(j); } - + template + void add_expl(const T& e) { for (auto j: e) add(j); } void add(unsigned ci) { push_justification(ci); } void add(const std::pair& j) { push_justification(j.second, j.first); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 4294e34cc..a7ce4ebb5 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -224,6 +224,27 @@ void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagat } +void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) { + unsigned i = ib.m_row_or_term_index; + int bound_sign = ib.m_is_lower_bound? 1: -1; + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; + unsigned bound_j = ib.m_j; + if (is_term(bound_j)) { + bound_j = m_var_register.external_to_local(bound_j); + } + for (auto const& r : A_r().m_rows[i]) { + unsigned j = r.var(); + if (j == bound_j) continue; + mpq const& a = r.get_val(); + int a_sign = is_pos(a)? 1: -1; + int sign = j_sign * a_sign; + const ul_pair & ul = m_columns_to_ul_pairs[j]; + auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); + lp_assert(is_valid(witness)); + bp.consume(a, witness); + } + // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); +} bool lar_solver::term_is_used_as_row(unsigned term) const { lp_assert(is_term(term)); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 2f20c625c..74516db64 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -315,6 +315,10 @@ public: void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset); + + void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp); + + bool term_is_used_as_row(unsigned term) const; void propagate_bounds_on_terms(lp_bound_propagator & bp); @@ -392,6 +396,8 @@ public: bool use_tableau_costs() const; + void detect_rows_of_column_with_bound_change(unsigned j); + void adjust_x_of_column(unsigned j); bool row_is_correct(unsigned i) const; diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp index 729d060e1..eed77b1f6 100644 --- a/src/math/lp/lp_bound_propagator.cpp +++ b/src/math/lp/lp_bound_propagator.cpp @@ -3,86 +3,19 @@ Author: Lev Nachmanson */ #include "math/lp/lar_solver.h" -#include "math/lp/nla_solver.h" namespace lp { - -lp_bound_propagator::lp_bound_propagator(lar_solver & ls, nla::solver* nla): - m_lar_solver(ls), m_nla_solver(nla) {} - +lp_bound_propagator::lp_bound_propagator(lar_solver & ls): + m_lar_solver(ls) {} column_type lp_bound_propagator::get_column_type(unsigned j) const { return m_lar_solver.m_mpq_lar_core_solver.m_column_types()[j]; } - -bool lp_bound_propagator::lower_bound_is_available(unsigned j) const { - if (lower_bound_is_available_for_column(j)) - return true; - if (!m_nla_solver->is_monomial_var(j)) - return false; - return m_nla_solver->monomial_has_lower_bound(j); +const impq & lp_bound_propagator::get_lower_bound(unsigned j) const { + return m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]; } - -bool lp_bound_propagator::upper_bound_is_available_for_column(unsigned j) const { - switch (get_column_type(j)) { - case column_type::fixed: - case column_type::boxed: - case column_type::upper_bound: - return true; - default: - return false; - } +const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { + return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; } - -bool lp_bound_propagator::lower_bound_is_available_for_column(unsigned j) const { - switch (get_column_type(j)) { - case column_type::fixed: - case column_type::boxed: - case column_type::lower_bound: - return true; - default: - return false; - } -} - -bool lp_bound_propagator::upper_bound_is_available(unsigned j) const { - if (upper_bound_is_available_for_column(j)) - return true; - if (!m_nla_solver->is_monomial_var(j)) - return false; - return m_nla_solver->monomial_has_upper_bound(j); -} -bool lp_bound_propagator::nl_monomial_upper_bound_is_available(unsigned j) const { - return m_nla_solver && m_nla_solver->is_monomial_var(j) - && - m_nla_solver->monomial_has_upper_bound(j); -} -bool lp_bound_propagator::nl_monomial_lower_bound_is_available(unsigned j) const { - return m_nla_solver && m_nla_solver->is_monomial_var(j) - && - m_nla_solver->monomial_has_lower_bound(j); -} - -impq lp_bound_propagator::get_lower_bound(unsigned j) const { - lp_assert(lower_bound_is_available(j)); - if (lower_bound_is_available_for_column(j)) { - const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]; - return nl_monomial_lower_bound_is_available(j)? - std::max(l, m_nla_solver->get_lower_bound(j)) : l; - } - return m_nla_solver->get_lower_bound(j); -} - -impq lp_bound_propagator::get_upper_bound(unsigned j) const { - lp_assert(upper_bound_is_available(j)); - if (upper_bound_is_available_for_column(j)) { - const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; - return nl_monomial_upper_bound_is_available(j)? - std::min(l, m_nla_solver->get_upper_bound(j)) : l; - } - return m_nla_solver->get_upper_bound(j); -} - void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { - CTRACE("nla_solver", m_nla_solver && m_nla_solver->is_monomial_var(j), tout << "mon_var = " << j << "\n"; ); j = m_lar_solver.adjust_column_index_to_term_index(j); lconstraint_kind kind = is_low? GE : LE; @@ -118,58 +51,4 @@ void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool co } } } -bool lp_bound_propagator::nl_monomial_upper_bound_should_be_taken(unsigned j) const { - return (!upper_bound_is_available_for_column(j)) || ( - nl_monomial_upper_bound_is_available(j) && m_nla_solver->get_upper_bound(j) < m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]); } - -bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const { - lp_assert(lower_bound_is_available(j)); - return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]); -} - -void lp_bound_propagator::explain_implied_bound(implied_bound & ib) { - unsigned i = ib.m_row_or_term_index; - int bound_sign = ib.m_is_lower_bound? 1: -1; - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; - unsigned bound_j = ib.m_j; - if (m_lar_solver.is_term(bound_j)) { - bound_j = m_lar_solver.m_var_register.external_to_local(bound_j); - } - for (auto const& r : m_lar_solver.A_r().m_rows[i]) { - unsigned j = r.var(); - if (j == bound_j) continue; - mpq const& a = r.get_val(); - int a_sign = is_pos(a)? 1: -1; - int sign = j_sign * a_sign; - if (sign > 0) { - if (nl_monomial_upper_bound_should_be_taken(j)) { - TRACE("nla_intervals", tout << "using the monomial upper bound\n";); - svector expl; - m_nla_solver->get_explanation_of_upper_bound_for_monomial(j, expl); - for (auto c : expl) - consume(a, c); - } else { - const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j]; - auto witness = ul.upper_bound_witness(); - lp_assert(is_valid(witness)); - consume(a, witness); - } - } else { - if (nl_monomial_lower_bound_should_be_taken(j)) { - TRACE("nla_intervals", tout << "using the monomial lower bound\n";); - svector expl; - m_nla_solver->get_explanation_of_lower_bound_for_monomial(j, expl); - for (auto c : expl) - consume(a, c); - - } else { - const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j]; - auto witness = ul.lower_bound_witness(); - lp_assert(is_valid(witness)); - consume(a, witness); - } - } - } -} -} // end of namespace lp diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 7a9c84292..4537ac1f3 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -4,39 +4,24 @@ */ #pragma once #include "math/lp/lp_settings.h" -namespace nla { -// forward definition -class solver; -} namespace lp { class lar_solver; class lp_bound_propagator { std::unordered_map m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_upper_bounds; lar_solver & m_lar_solver; - nla::solver * m_nla_solver; public: vector m_ibounds; public: - lp_bound_propagator(lar_solver & ls, nla::solver * nla); + lp_bound_propagator(lar_solver & ls); column_type get_column_type(unsigned) const; - - bool lower_bound_is_available_for_column(unsigned) const; - bool upper_bound_is_available_for_column(unsigned) const; - bool lower_bound_is_available(unsigned) const; - bool upper_bound_is_available(unsigned) const; - impq get_lower_bound(unsigned) const; - impq get_upper_bound(unsigned) const; + const impq & get_lower_bound(unsigned) const; + const impq & get_upper_bound(unsigned) const; void try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict); virtual bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) {return true;} unsigned number_of_found_bounds() const { return m_ibounds.size(); } - void explain_implied_bound(implied_bound & ib); virtual void consume(mpq const& v, lp::constraint_index j) = 0; - bool nl_monomial_upper_bound_is_available(unsigned) const; - bool nl_monomial_lower_bound_is_available(unsigned) const; - bool nl_monomial_lower_bound_should_be_taken(unsigned) const; - bool nl_monomial_upper_bound_should_be_taken(unsigned) const; }; } diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 8abd3fcbf..d74f7eade 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -251,15 +251,15 @@ bool basics::basic_lemma(bool derived) { if (basic_sign_lemma(derived)) return true; if (derived) - return false; - const auto& rm_ref = c().m_to_refine; - TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout);); + return c().m_intervals.get_lemmas(); + const auto& mon_inds_to_ref = c().m_to_refine; + TRACE("nla_solver", tout << "mon_inds_to_ref = "; print_vector(mon_inds_to_ref, tout);); unsigned start = c().random(); - unsigned sz = rm_ref.size(); + unsigned sz = mon_inds_to_ref.size(); for (unsigned j = 0; j < sz; ++j) { - lpvar v = rm_ref[(j + start) % rm_ref.size()]; - const monomial& r = c().m_emons[v]; - SASSERT (!c().check_monomial(c().m_emons[v])); + lpvar v = mon_inds_to_ref[(j + start) % mon_inds_to_ref.size()]; + const monomial& r = c().emons()[v]; + SASSERT (!c().check_monomial(c().emons()[v])); basic_lemma_for_mon(r, derived); } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 940823cf5..e00599f80 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -21,10 +21,11 @@ Revision History: #include "math/lp/factorization_factory_imp.h" namespace nla { -core::core(lp::lar_solver& s) : +core::core(lp::lar_solver& s, reslimit & lim) : m_evars(), m_lar_solver(s), m_tangents(this), + m_intervals(this, lim), m_basics(this), m_order(this), m_monotone(this), diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fe6ec0236..827141dde 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -27,6 +27,7 @@ #include "math/lp/nla_monotone_lemmas.h" #include "math/lp/emonomials.h" #include "math/lp/nla_settings.h" +#include "math/lp/nla_intervals.h" namespace nla { template @@ -82,6 +83,7 @@ public: vector * m_lemma_vec; svector m_to_refine; tangents m_tangents; + intervals m_intervals; basics m_basics; order m_order; monotone m_monotone; @@ -91,7 +93,7 @@ public: emonomials& emons() { return m_emons; } const emonomials& emons() const { return m_emons; } // constructor - core(lp::lar_solver& s); + core(lp::lar_solver& s, reslimit &); bool compare_holds(const rational& ls, llc cmp, const rational& rs) const; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index f9b55be27..150770bb6 100755 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -1,90 +1,76 @@ #include "math/lp/nla_core.h" #include "math/interval/interval_def.h" #include "math/lp/nla_intervals.h" + namespace nla { -bool intervals::check() { - // m_region.reset(); - // for (auto const& m : m_core->emons()) { - // if (!check(m)) { - // return false; - // } - // } - // for (auto const& t : ls().terms()) { - // if (!check(*t)) { - // return false; - // } - // } - return true; +bool intervals::get_lemmas() { + m_region.reset(); + bool ret = false; + for (auto const& k : c().m_to_refine) { + if (get_lemma(c().emons()[k])) { + ret = true; + } + if (c().done()) + break; + } + return ret; } // create a product of interval signs together with the depencies intervals::interval intervals::mul_signs_with_deps(const svector& vars) const { interval a, b, c; m_imanager.set(a, mpq(1)); for (lpvar v : vars) { - set_var_interval_signs_with_deps(v, b); - interval_deps deps; - m_imanager.mul(a, b, c, deps); - m_imanager.set(a, c); - m_config.add_deps(a, b, deps, a); - if (m_imanager.is_zero(a)) - return a; + set_var_interval_signs_with_deps(v, b); + interval_deps deps; + m_imanager.mul(a, b, c, deps); + m_imanager.set(a, c); + m_config.add_deps(a, b, deps, a); + if (m_imanager.is_zero(a)) + return a; } - return a; - + return a; } -// bool intervals::check(monomial const& m) { -// interval a, b, c, d; -// m_imanager.set(a, mpq(1)); -// set_var_interval(m.var(), d); -// if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) { -// return true; -// } -// for (lpvar v : m.vars()) { -// // TBD allow for division to get range of a -// // m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c -// if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) { -// return true; -// } -// // TBD: deal with powers v^n interval instead of multiplying v*v .. * v -// set_var_interval(v, b); -// interval_deps deps; -// m_imanager.mul(a, b, c, deps); -// m_imanager.set(a, c); -// m_config.add_deps(a, b, deps, a); -// } -// if (m_imanager.before(a, d)) { -// svector cs; -// m_dep_manager.linearize(a.m_upper_dep, cs); -// m_dep_manager.linearize(d.m_lower_dep, cs); -// for (auto ci : cs) { -// (void)ci; -// SASSERT(false); -// //expl.push_justification(ci); -// } -// // TBD conflict -// return false; -// } -// if (m_imanager.before(d, a)) { -// svector cs; -// m_dep_manager.linearize(a.m_lower_dep, cs); -// m_dep_manager.linearize(d.m_upper_dep, cs); -// for (auto ci : cs) { -// (void)ci; -// SASSERT(false); //expl.push_justification(ci); -// } -// // TBD conflict -// return false; -// } -// // could also perform bounds propagation: -// // a has tighter lower/upper bound than m.var(), -// // -> transfer bound to m.var() -// // all but one variable has bound -// // -> transfer bound to that variable using division -// return true; -// } +bool intervals::get_lemma(monomial const& m) { + interval b, c, d; + interval a = mul(m.vars()); + lp::impq v(val(m.var())); + if (!m_imanager.lower_is_inf(a)) { + lp::impq lb(rational(a.m_lower)); + if (m_config.lower_is_open(a)) + lb.y = 1; + if (v < lb) { + interval signs_a = mul_signs_with_deps(m.vars()); + add_empty_lemma(); + svector expl; + m_dep_manager.linearize(signs_a.m_lower_dep, expl); + _().current_expl().add_expl(expl); + llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE; + mk_ineq(m.var(), cmp, lb.x); + TRACE("nla_solver", _().print_lemma(tout); ); + return true; + } + } + if (!m_imanager.upper_is_inf(a)) { + lp::impq ub(rational(a.m_upper)); + if (m_config.upper_is_open(a)) + ub.y = 1; + if (v > ub) { + interval signs_a = mul_signs_with_deps(m.vars()); + add_empty_lemma(); + svector expl; + m_dep_manager.linearize(signs_a.m_upper_dep, expl); + _().current_expl().add_expl(expl); + llc cmp = m_config.lower_is_open(a)? llc::LT: llc::LE; + mk_ineq(m.var(), cmp, ub.x); + TRACE("nla_solver", _().print_lemma(tout); ); + return true; + } + } + return false; +} void intervals::set_var_interval(lpvar v, interval& b) const { lp::constraint_index ci; rational val; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index a4a33241d..6c5e64548 100755 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -26,40 +26,39 @@ namespace nla { - class core; +class core; - class intervals { - core * m_core; - class ci_value_manager { - public: - void inc_ref(lp::constraint_index const & v) { - } +class intervals : common { + class ci_value_manager { + public: + void inc_ref(lp::constraint_index const & v) { + } - void dec_ref(lp::constraint_index const & v) { - } - }; + void dec_ref(lp::constraint_index const & v) { + } + }; - struct ci_dependency_config { - typedef ci_value_manager value_manager; - typedef small_object_allocator allocator; - static const bool ref_count = false; - typedef lp::constraint_index value; - }; + struct ci_dependency_config { + typedef ci_value_manager value_manager; + typedef small_object_allocator allocator; + static const bool ref_count = false; + typedef lp::constraint_index value; + }; - typedef dependency_manager ci_dependency_manager; + typedef dependency_manager ci_dependency_manager; - typedef ci_dependency_manager::dependency ci_dependency; + typedef ci_dependency_manager::dependency ci_dependency; - class im_config { - unsynch_mpq_manager& m_manager; - ci_dependency_manager& m_dep_manager; + class im_config { + unsynch_mpq_manager& m_manager; + ci_dependency_manager& m_dep_manager; - public: - typedef unsynch_mpq_manager numeral_manager; + public: + typedef unsynch_mpq_manager numeral_manager; - // Every configuration object must provide an interval type. - // The actual fields are irrelevant, the interval manager - // accesses interval data using the following API. + // Every configuration object must provide an interval type. + // The actual fields are irrelevant, the interval manager + // accesses interval data using the following API. struct interval { interval(): @@ -78,107 +77,105 @@ namespace nla { }; - void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { - ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); - ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); - i.m_lower_dep = lo; - i.m_upper_dep = hi; + void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { + ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); + ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); + i.m_lower_dep = lo; + i.m_upper_dep = hi; + } + + // Should be NOOPs for precise mpq types. + // For imprecise types (e.g., floats) it should set the rounding mode. + void round_to_minus_inf() {} + void round_to_plus_inf() {} + void set_rounding(bool to_plus_inf) {} + + // Getters + mpq const & lower(interval const & a) const { return a.m_lower; } + mpq const & upper(interval const & a) const { return a.m_upper; } + mpq & lower(interval & a) { return a.m_lower; } + mpq & upper(interval & a) { return a.m_upper; } + bool lower_is_open(interval const & a) const { return a.m_lower_open; } + bool upper_is_open(interval const & a) const { return a.m_upper_open; } + bool lower_is_inf(interval const & a) const { return a.m_lower_inf; } + bool upper_is_inf(interval const & a) const { return a.m_upper_inf; } + bool is_zero(interval const & a) const { + return unsynch_mpq_manager::is_zero(a.m_lower) + && unsynch_mpq_manager::is_zero(a.m_upper); } + + // Setters + void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); } + void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); } + void set_lower(interval & a, rational const & n) const { set_lower(a, n.to_mpq()); } + void set_upper(interval & a, rational const & n) const { set_upper(a, n.to_mpq()); } + void set_lower_is_open(interval & a, bool v) const { a.m_lower_open = v; } + void set_upper_is_open(interval & a, bool v) const { a.m_upper_open = v; } + void set_lower_is_inf(interval & a, bool v) const { a.m_lower_inf = v; } + void set_upper_is_inf(interval & a, bool v) const { a.m_upper_inf = v; } + + // Reference to numeral manager + numeral_manager & m() const { return m_manager; } + + im_config(numeral_manager & m, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {} + private: + ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const { + ci_dependency* dep = nullptr; + if (dep_in_lower1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_lower_dep); } - - // Should be NOOPs for precise mpq types. - // For imprecise types (e.g., floats) it should set the rounding mode. - void round_to_minus_inf() {} - void round_to_plus_inf() {} - void set_rounding(bool to_plus_inf) {} - - // Getters - mpq const & lower(interval const & a) const { return a.m_lower; } - mpq const & upper(interval const & a) const { return a.m_upper; } - mpq & lower(interval & a) { return a.m_lower; } - mpq & upper(interval & a) { return a.m_upper; } - bool lower_is_open(interval const & a) const { return a.m_lower_open; } - bool upper_is_open(interval const & a) const { return a.m_upper_open; } - bool lower_is_inf(interval const & a) const { return a.m_lower_inf; } - bool upper_is_inf(interval const & a) const { return a.m_upper_inf; } - bool is_zero(interval const & a) const { - return unsynch_mpq_manager::is_zero(a.m_lower) - && unsynch_mpq_manager::is_zero(a.m_upper); } - - // Setters - void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); } - void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); } - void set_lower(interval & a, rational const & n) const { set_lower(a, n.to_mpq()); } - void set_upper(interval & a, rational const & n) const { set_upper(a, n.to_mpq()); } - void set_lower_is_open(interval & a, bool v) const { a.m_lower_open = v; } - void set_upper_is_open(interval & a, bool v) const { a.m_upper_open = v; } - void set_lower_is_inf(interval & a, bool v) const { a.m_lower_inf = v; } - void set_upper_is_inf(interval & a, bool v) const { a.m_upper_inf = v; } - - // Reference to numeral manager - numeral_manager & m() const { return m_manager; } - - im_config(numeral_manager & m, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {} - private: - ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const { - ci_dependency* dep = nullptr; - if (dep_in_lower1(bd)) { - dep = m_dep_manager.mk_join(dep, a.m_lower_dep); - } - if (dep_in_lower2(bd)) { - dep = m_dep_manager.mk_join(dep, b.m_lower_dep); - } - if (dep_in_upper1(bd)) { - dep = m_dep_manager.mk_join(dep, a.m_upper_dep); - } - if (dep_in_upper2(bd)) { - dep = m_dep_manager.mk_join(dep, b.m_upper_dep); - } - return dep; + if (dep_in_lower2(bd)) { + dep = m_dep_manager.mk_join(dep, b.m_lower_dep); } - }; - - small_object_allocator m_alloc; - ci_value_manager m_val_manager; - unsynch_mpq_manager m_num_manager; - mutable ci_dependency_manager m_dep_manager; - im_config m_config; - mutable interval_manager m_imanager; - region m_region; - - typedef interval_manager::interval interval; - - bool check(monomial const& m); - - void set_var_interval(lpvar v, interval & b) const; - - void set_var_interval_signs(lpvar v, interval & b) const; - - void set_var_interval_signs_with_deps(lpvar v, interval & b) const; - - ci_dependency* mk_dep(lp::constraint_index ci) const; - - bool check(lp::lar_term const& t); - lp::lar_solver& ls(); - const lp::lar_solver& ls() const; - public: - intervals(core* c, reslimit& lim) : - m_core(c), - m_alloc("intervals"), - m_dep_manager(m_val_manager, m_alloc), - m_config(m_num_manager, m_dep_manager), - m_imanager(lim, im_config(m_num_manager, m_dep_manager)) - {} - bool check(); - bool monomial_has_lower_bound(lpvar j) const; - bool monomial_has_upper_bound(lpvar j) const; - bool product_has_upper_bound(int sign, const svector&) const; - lp::impq get_upper_bound_of_monomial(lpvar j) const; - lp::impq get_lower_bound_of_monomial(lpvar j) const; - interval mul(const svector&) const; - interval mul_signs(const svector&) const; - interval mul_signs_with_deps(const svector&) const; - void get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const; - void get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const; - std::ostream& print_explanations(const svector &, std::ostream&) const; + if (dep_in_upper1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_upper_dep); + } + if (dep_in_upper2(bd)) { + dep = m_dep_manager.mk_join(dep, b.m_upper_dep); + } + return dep; + } }; + + small_object_allocator m_alloc; + ci_value_manager m_val_manager; + unsynch_mpq_manager m_num_manager; + mutable ci_dependency_manager m_dep_manager; + im_config m_config; + mutable interval_manager m_imanager; + region m_region; + + typedef interval_manager::interval interval; + + void set_var_interval(lpvar v, interval & b) const; + + void set_var_interval_signs(lpvar v, interval & b) const; + + void set_var_interval_signs_with_deps(lpvar v, interval & b) const; + + ci_dependency* mk_dep(lp::constraint_index ci) const; + + lp::lar_solver& ls(); + const lp::lar_solver& ls() const; +public: + intervals(core* c, reslimit& lim) : + common(c), + m_alloc("intervals"), + m_dep_manager(m_val_manager, m_alloc), + m_config(m_num_manager, m_dep_manager), + m_imanager(lim, im_config(m_num_manager, m_dep_manager)) + {} + bool get_lemmas(); + bool get_lemma(monomial const& m); + bool monomial_has_lower_bound(lpvar j) const; + bool monomial_has_upper_bound(lpvar j) const; + bool product_has_upper_bound(int sign, const svector&) const; + lp::impq get_upper_bound_of_monomial(lpvar j) const; + lp::impq get_lower_bound_of_monomial(lpvar j) const; + interval mul(const svector&) const; + interval mul_signs(const svector&) const; + interval mul_signs_with_deps(const svector&) const; + void get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const; + void get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const; + std::ostream& print_explanations(const svector &, std::ostream&) const; +}; } // end of namespace nla diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 44f3a70dd..97afcfb24 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -54,32 +54,10 @@ void solver::pop(unsigned n) { } -solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit) { +solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)) { } solver::~solver() { dealloc(m_core); } -lp::impq solver::get_upper_bound(lpvar j) const { - SASSERT(is_monomial_var(j) && m_intervals.monomial_has_upper_bound(j)); - return m_intervals.get_upper_bound_of_monomial(j); -} - -lp::impq solver::get_lower_bound(lpvar j) const { - SASSERT(is_monomial_var(j) && m_intervals.monomial_has_lower_bound(j)); - return m_intervals.get_lower_bound_of_monomial(j); -} - -bool solver::monomial_has_lower_bound(lpvar j) const { - return m_intervals.monomial_has_lower_bound(j); -} -bool solver::monomial_has_upper_bound(lpvar j) const { - return m_intervals.monomial_has_upper_bound(j); -} -void solver::get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const { - m_intervals.get_explanation_of_upper_bound_for_monomial(j, expl); -} -void solver::get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const{ - m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl); -} } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 173ff4dfe..bf5d39671 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -34,7 +34,6 @@ namespace nla { class solver { core* m_core; reslimit m_res_limit; - intervals m_intervals; public: void add_monomial(lpvar v, unsigned sz, lpvar const* vs); @@ -47,11 +46,5 @@ public: lbool check(vector&); std::ostream& display(std::ostream& out); bool is_monomial_var(lpvar) const; - lp::impq get_lower_bound(lpvar j) const; - lp::impq get_upper_bound(lpvar j) const; - bool monomial_has_lower_bound(lpvar j) const; - bool monomial_has_upper_bound(lpvar j) const; - void get_explanation_of_upper_bound_for_monomial(lpvar j, svector&) const; - void get_explanation_of_lower_bound_for_monomial(lpvar j, svector&) const; }; }