From c95f66e02a7ec6795d9b01a91440c89f70647bd3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 5 Aug 2019 17:28:39 -0700 Subject: [PATCH] toward fetching existing terms intervals from lar_solver Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 31 ++++++++++++++++++---------- src/math/lp/horner.h | 6 +++--- src/math/lp/lar_solver.cpp | 39 +++++++++++++++++++++++++++-------- src/math/lp/lar_solver.h | 3 +++ src/math/lp/nla_intervals.cpp | 2 +- src/math/lp/nla_intervals.h | 25 ++++++++++++++++++++-- 6 files changed, 80 insertions(+), 26 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 43400c8eb..6fa6e2f06 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -242,7 +242,7 @@ void horner::add_linear_to_vector(const nex& e, vector> v; @@ -281,12 +281,10 @@ lp::lar_term horner::expression_to_canonical_form(nex& e, rational& a, rational& return t; } -bool horner::find_term_expr(const nex& e, rational& a, const lp::lar_term* &t, rational& b) const { +lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const { nex n = e; - lp::lar_term can_t = expression_to_canonical_form(n, a, b); - TRACE("nla_horner_details", tout << "term = "; c().m_lar_solver.print_term(can_t, tout) << "\n";); - SASSERT(false); - return false; + lp::lar_term norm_t = expression_to_normalized_term(n, a, b); + return c().m_lar_solver.fetch_normalized_term_column(norm_t); } interv horner::interval_of_sum_no_terms(const nex& e) { @@ -326,10 +324,21 @@ interv horner::interval_of_sum_no_terms(const nex& e) { bool horner::interval_from_term(const nex& e, interv & i) const { rational a, b; nex n = e; - lp::lar_term canonical_t = expression_to_canonical_form(n, a, b); - // TRACE("nla_horner_details", - SASSERT(false); - return false; + lpvar j = find_term_column(n, a, b); + if (j + 1 == 0) + return false; + + set_var_interval(j, i); + interv bi; + m_intervals.mul(a, i, bi); + m_intervals.add(b, bi); + m_intervals.set(i, bi); + + TRACE("nla_horner", + c().m_lar_solver.print_column_info(j, tout) << "\n"; + tout << "a=" << a << ", b=" << b << "\n"; + tout << e << ", interval = "; m_intervals.display(tout, i);); + return true; } @@ -349,7 +358,7 @@ interv horner::interval_of_sum(const nex& e) { } // sets the dependencies also -void horner::set_var_interval(lpvar v, interv& b) { +void horner::set_var_interval(lpvar v, interv& b) const{ m_intervals.set_var_interval_with_deps(v, b); TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b);); } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 835cb2bcf..42d7ff5f8 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -46,13 +46,13 @@ public: intervals::interval interval_of_sum_no_terms(const nex&); intervals::interval interval_of_mul(const nex&); void set_interval_for_scalar(intervals::interval&, const rational&); - void set_var_interval(lpvar j, intervals::interval&); + void set_var_interval(lpvar j, intervals::interval&) const; bool lemmas_on_expr(nex &); template // T has an iterator of (coeff(), var()) bool row_has_monomial_to_refine(const T&) const; - bool find_term_expr(const nex& e, rational& a, const lp::lar_term * & t, rational& b) const; - static lp::lar_term expression_to_canonical_form(nex&, rational& a, rational & b); + lpvar find_term_column(const nex& e, rational& a, rational& b) const; + static lp::lar_term expression_to_normalized_term(nex&, rational& a, rational & b); static void add_linear_to_vector(const nex&, vector> &); static void add_mul_to_vector(const nex&, vector> &); bool is_tighter(const interv&, const interv&) const; diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 4c3ab8774..182bd3fb3 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -34,7 +34,7 @@ lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_terms_start_index(1000000), m_var_register(0), m_term_register(m_terms_start_index), - m_need_register_terms(true) // change to false + m_need_register_terms(false) {} void lar_solver::set_track_pivoted_rows(bool v) { @@ -387,9 +387,8 @@ void lar_solver::pop(unsigned k) { m_constraints.resize(m_constraint_count); m_term_count.pop(k); for (unsigned i = m_term_count; i < m_terms.size(); i++) { -#if Z3DEBUG_CHECK_UNIQUE_TERMS - m_set_of_terms.erase(m_terms[i]); -#endif + if (m_need_register_terms) + deregister_normalized_term(*m_terms[i]); delete m_terms[i]; } m_term_register.shrink(m_term_count); @@ -1822,6 +1821,8 @@ bool lar_solver::all_vars_are_registered(const vector> } var_index lar_solver::add_term(const vector> & coeffs, unsigned ext_i) { + TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); + m_term_register.add_var(ext_i); lp_assert(all_vars_are_registered(coeffs)); if (strategy_is_undecided()) @@ -1838,8 +1839,7 @@ var_index lar_solver::add_term(const vector> & coeffs, } lp_assert(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) { - lar_term normalized_t = t->get_normalized_by_min_var(); - m_normalized_terms_to_columns[normalized_t] = A_r().column_count() - 1; + register_normalized_term(*t, A_r().column_count() - 1); } return ret; } @@ -2371,14 +2371,35 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) { settings().set_hnf_cut_period(100000000); } } + +void lar_solver::register_normalized_term(const lar_term& t, lpvar j) { + lar_term normalized_t = t.get_normalized_by_min_var(); + TRACE("lar_solver_terms", tout << "t="; print_term_as_indices(t, tout); + tout << ", normalized_t="; print_term_as_indices(normalized_t, tout) << "\n";); + lp_assert(m_normalized_terms_to_columns.find(normalized_t) == m_normalized_terms_to_columns.end()); + m_normalized_terms_to_columns[normalized_t] = j; +} + +void lar_solver::deregister_normalized_term(const lar_term& t) { + lar_term normalized_t = t.get_normalized_by_min_var(); + lp_assert(m_normalized_terms_to_columns.find(normalized_t) != m_normalized_terms_to_columns.end()); + m_normalized_terms_to_columns.erase(normalized_t); +} + void lar_solver::register_existing_terms() { + TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";); for (unsigned k = 0; k < m_terms.size(); k++) { - lar_term * t = m_terms[k]; - lar_term normalized_t = t->get_normalized_by_min_var(); lpvar j = m_var_register.external_to_local(k + m_terms_start_index); - m_normalized_terms_to_columns[normalized_t] = j; + register_normalized_term(*m_terms[k], j); } } + +unsigned lar_solver::fetch_normalized_term_column(const lar_term& c) const { + auto it = m_normalized_terms_to_columns.find(c); + if (it != m_normalized_terms_to_columns.end()) + return it->second; + return -1; +} } // namespace lp diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 196c87c86..1782b02f8 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -644,5 +644,8 @@ public: void fix_Ax_b_on_rounded_row(unsigned); void collect_rounded_rows_to_fix(); void register_existing_terms(); + void register_normalized_term(const lar_term&, lpvar); + void deregister_normalized_term(const lar_term&); + lpvar fetch_normalized_term_column(const lar_term& t) const; }; } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 37f918ac0..debdeb55e 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -4,7 +4,7 @@ #include "util/mpq.h" namespace nla { -void intervals::set_var_interval_with_deps(lpvar v, interval& b) { +void intervals::set_var_interval_with_deps(lpvar v, interval& b) const { lp::constraint_index ci; rational val; bool is_strict; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 3b3a52d27..cbc5a35e8 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -171,10 +171,31 @@ public: void set_upper_is_open(interval & a, bool strict) { m_config.set_upper_is_open(a, strict); } void set_upper_is_inf(interval & a, bool inf) { m_config.set_upper_is_inf(a, inf); } bool is_zero(const interval& a) const { return m_config.is_zero(a); } + void mul(const rational& r, const interval& a, interval& b) const { + m_imanager.mul(r.to_mpq(), a, b); + if (r.is_pos()) { + b.m_lower_dep = a.m_lower_dep; + b.m_upper_dep = a.m_upper_dep; + } else { + SASSERT(r.is_neg()); + b.m_upper_dep = a.m_lower_dep; + b.m_lower_dep = a.m_upper_dep; + } + } + + void add(const rational& r, interval& a) const { + if (!a.m_lower_inf) { + m_config.set_lower(a, a.m_lower + r); + } + if (!a.m_upper_inf) { + m_config.set_upper(a, a.m_upper + r); + } + } + void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); } void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); } void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } - void set(interval& a, const interval& b) { + void set(interval& a, const interval& b) const { m_imanager.set(a, b); a.m_lower_dep = b.m_lower_dep; a.m_upper_dep = b.m_upper_dep; @@ -228,7 +249,7 @@ public: bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); } bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); } - void set_var_interval_with_deps(lpvar, interval &); + void set_var_interval_with_deps(lpvar, interval &) const; void set_zero_interval_deps_for_mult(interval&); bool is_inf(const interval& i) const { return m_config.is_inf(i); } bool check_interval_for_conflict_on_zero(const interval & i);