From 57152430f9161e7a6f0fcf5598ef375c61bd1c93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jul 2023 18:05:17 -0700 Subject: [PATCH] working on multiple intervals Signed-off-by: Nikolaj Bjorner --- src/math/dd/pdd_interval.h | 40 ++++++++++---- src/math/interval/dep_intervals.h | 20 +++++++ src/math/lp/nla_core.cpp | 20 +++---- src/math/lp/nla_grobner.cpp | 9 +++- src/math/lp/nla_grobner.h | 2 + src/math/lp/nla_intervals.cpp | 86 +++++++++++++++---------------- src/math/lp/nla_intervals.h | 6 +++ src/sat/smt/arith_solver.cpp | 7 ++- src/smt/theory_lra.cpp | 5 +- 9 files changed, 125 insertions(+), 70 deletions(-) diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index abe49cc15..69fc8b0d2 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -21,6 +21,7 @@ Revision History: #include "math/dd/dd_pdd.h" #include "math/interval/dep_intervals.h" +#include "util/scoped_ptr_vector.h" namespace dd { typedef dep_intervals::interval interval; @@ -29,7 +30,7 @@ typedef dep_intervals::with_deps_t w_dep; class pdd_interval { dep_intervals& m_dep_intervals; std::function m_var2interval; - std::function&)> m_var2intervals; + std::function&)> m_var2intervals; // retrieve intervals after distributing multiplication over addition. template @@ -66,8 +67,8 @@ public: std::function& var2interval() { return m_var2interval; } // setter const std::function& var2interval() const { return m_var2interval; } // getter - std::function&)>& var2intervals() { return m_var2intervals; } // setter - const std::function&)>& var2intervals() const { return m_var2intervals; } // getter + std::function&)>& var2intervals() { return m_var2intervals; } // setter + const std::function&)>& var2intervals() const { return m_var2intervals; } // getter template void get_interval(pdd const& p, scoped_dep_interval& ret) { @@ -96,7 +97,6 @@ public: get_interval_distributed(p, i, ret); } - // // produce an explanation for a range using weaker bounds. // @@ -121,17 +121,37 @@ public: m_dep_intervals.mul(hi, a, hi_interval); m_dep_intervals.sub(bound, hi_interval, lo_bound); explain(p.lo(), lo_bound, lo_interval); - m_dep_intervals.add(lo_interval, hi_interval, ret); } - else { + else { + // lo_B + coeff*v : bounds + // v in (bounds - l_B) / coeff + get_interval(p.lo(), lo_interval); m_dep_intervals.sub(bound, lo_interval, hi_bound); m_dep_intervals.div(hi_bound, p.hi().val().to_mpq(), hi_bound); - vector as; - m_var2intervals(p.var(), true, as); - // use hi_bound to adjust for variable bound. + scoped_ptr_vector var_intervals; + scoped_dep_interval var_interval(m()); + m_var2intervals(p.var(), true, var_intervals); + for (auto* vip : var_intervals) { + auto & vi = *vip; + if (!m_dep_intervals.lower_is_inf(vi) && !m_dep_intervals.lower_is_inf(hi_bound) && rational(m_dep_intervals.lower(vi)) > m_dep_intervals.lower(hi_bound)) { + if (m_dep_intervals.lower_is_inf(var_interval) || m_dep_intervals.lower(vi) > m_dep_intervals.lower(var_interval)) { + m_dep_intervals.set_lower(var_interval, m_dep_intervals.lower(vi)); + m_dep_intervals.set_lower_dep(var_interval, m_dep_intervals.lower_dep(vi)); + } + } + if (!m_dep_intervals.upper_is_inf(vi) && !m_dep_intervals.upper_is_inf(hi_bound) && m_dep_intervals.upper(hi_bound) > m_dep_intervals.upper(vi)) { + if (m_dep_intervals.upper_is_inf(var_interval) || m_dep_intervals.upper(var_interval) > m_dep_intervals.upper(vi)) { + m_dep_intervals.set_upper(var_interval, m_dep_intervals.upper(vi)); + m_dep_intervals.set_upper_dep(var_interval, m_dep_intervals.upper_dep(vi)); + } + } + } + m_dep_intervals.mul(var_interval, p.hi().val().to_mpq(), hi_interval); + m_dep_intervals.sub(bound, hi_interval, lo_bound); + explain(p.lo(), lo_bound, lo_interval); } - + m_dep_intervals.add(lo_interval, hi_interval, ret); } }; } diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index e5523e09f..7863f1947 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -80,6 +80,8 @@ private: 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; } + u_dependency* upper_dep(interval const & a) { return a.m_upper_dep; } + u_dependency* lower_dep(interval const & a) { return a.m_lower_dep; } 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; } @@ -196,6 +198,7 @@ public: 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 sub(const interval& a, const interval& b, interval& c) { m_imanager.sub(a, b, c); } + void mul(const interval& a, const mpq& b, interval& c) { m_imanager.mul(b, a, c); } void div(const interval& a, const mpq& b, interval& c) { m_imanager.div(a, b, c); } template @@ -296,6 +299,18 @@ public: div(a, b, c); } } + + template + void mul(const interval& a, const mpq& b, interval& c) { + if (wd == with_deps) { + interval_deps_combine_rule comb_rule; + mul(b, a, c, comb_rule); + combine_deps(a, comb_rule, c); + } + else { + mul(b, a, c); + } + } template void copy_upper_bound(const interval& a, interval& i) const { @@ -359,6 +374,10 @@ public: mpq const& lower(interval const& a) const { return m_config.lower(a); } mpq const& upper(interval const& a) const { return m_config.upper(a); } + u_dependency* upper_dep(interval const & a) { return m_config.upper_dep(a); } + u_dependency* lower_dep(interval const & a) { return m_config.lower_dep(a); } + + bool is_empty(interval const& a) const; void set_interval_for_scalar(interval&, const rational&); template @@ -441,6 +460,7 @@ private: void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } void sub(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.sub(a, b, c, deps); } void div(const interval& a, const mpq& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.div(a, b, c, deps); } + void mul(const interval& a, const mpq& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(b, a, c, deps); } void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { m_config.add_deps(a, b, deps, i); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index ee85bf7c7..b6c404b13 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1535,7 +1535,7 @@ void core::add_bounds() { //m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n"; if (var_is_free(j)) m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); -#if 0 +#if 1 else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added)) m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j))); else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added)) @@ -1574,13 +1574,10 @@ lbool core::check(vector& lits, vector& l_vec) { bool run_bounded_nlsat = should_run_bounded_nlsat(); bool run_bounds = params().arith_nl_branching(); - - if (l_vec.empty() && !done()) - m_monomial_bounds(); - - auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); }; - + + if (no_effect()) + m_monomial_bounds(); { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; @@ -1595,15 +1592,14 @@ lbool core::check(vector& lits, vector& l_vec) { if (!l_vec.empty() || !lits.empty()) return l_false; } - - - if (l_vec.empty() && !done()) + + if (no_effect()) m_basics.basic_lemma(true); - if (l_vec.empty() && !done()) + if (no_effect()) m_basics.basic_lemma(false); - if (l_vec.empty() && !done()) + if (no_effect()) m_divisions.check(); if (!conflict_found() && !done() && run_bounded_nlsat) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index f293770b9..e4c3aea98 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -274,8 +274,14 @@ namespace nla { if (di.upper(i) >= mx) return false; + eval.var2intervals() = [this](lpvar j, bool deps, scoped_ptr_vector& intervals) { + verbose_stream() << "get-intervals\n"; + // var2intervals(j, deps, intervals); + }; // TODO - relax bound dependencies to weakest that admit within interval -mx, mx. - eval.get_interval(lo, i_wd); + eval.explain(lo, i, i_wd); + + // eval.get_interval(lo, i_wd); lp::lar_term lo_t; rational k(0); @@ -311,6 +317,7 @@ namespace nla { return true; } + void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) { lp::explanation ex; u_dependency_manager dm; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index a1c877fb4..6556ab347 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -48,6 +48,8 @@ namespace nla { void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq); + void var2intervals(lpvar j, bool deps, vector& intervals); + // setup void configure(); void set_level2var(); diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 66ab571fb..298d57c41 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -62,7 +62,8 @@ std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream& if (!expl.empty()) { m_core->print_explanation(e, out); expl.clear(); - } else { + } + else { out << "\nno constraints\n"; } } @@ -135,7 +136,8 @@ lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational for (const nex* c : *e) { if (c->is_scalar()) { b += c->to_scalar().value(); - } else { + } + else { add_linear_to_vector(c, v); if (v.empty()) continue; @@ -153,7 +155,8 @@ lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational for (auto& p : v) { t.add_monomial(p.first, p.second); } - } else { + } + else { for (unsigned k = 0; k < v.size(); k++) { auto& p = v[k]; if (k != a_index) @@ -212,26 +215,23 @@ u_dependency *intervals::mk_dep(lp::constraint_index ci) { u_dependency *intervals::mk_dep(const lp::explanation& expl) { u_dependency * r = nullptr; - for (auto p : expl) { - if (r == nullptr) { - r = m_dep_intervals.mk_leaf(p.ci()); - } else { - r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci())); - } - } + for (auto p : expl) + r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci())); return r; } std::ostream& intervals::display(std::ostream& out, const interval& i) const { if (m_dep_intervals.lower_is_inf(i)) { out << "(-oo"; - } else { + } + else { out << (m_dep_intervals.lower_is_open(i)? "(":"[") << rational(m_dep_intervals.lower(i)); } out << ","; if (m_dep_intervals.upper_is_inf(i)) { out << "oo)"; - } else { + } + else { out << rational(m_dep_intervals.upper(i)) << (m_dep_intervals.upper_is_open(i)? ")":"]"); } svector expl; @@ -247,7 +247,7 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { } template -void intervals::set_var_interval(lpvar v, interval& b) { +void intervals::set_var_interval1(lpvar v, interval& b) { TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";); lp::constraint_index ci; rational val; @@ -274,17 +274,29 @@ void intervals::set_var_interval(lpvar v, interval& b) { m_dep_intervals.set_upper_is_inf(b, true); if (wd == e_with_deps::with_deps) b.m_upper_dep = nullptr; } +} +template +bool intervals::set_var_interval2(lpvar v, scoped_dep_interval& b) { if (ls().column_corresponds_to_term(v)) { auto const& lt = ls().column_index_to_term(v); - scoped_dep_interval ti(m_dep_intervals), r(m_dep_intervals); - if (interval_from_lar_term(lt, ti)) { - m_dep_intervals.intersect(b, ti, r); - m_dep_intervals.set(b, r); - } + return interval_from_lar_term(lt, b); + } + return false; +} + +template +void intervals::set_var_interval(lpvar v, interval& b) { + set_var_interval1(v, b); + scoped_dep_interval ti(m_dep_intervals), r(m_dep_intervals); + if (set_var_interval2(v, ti)) { + m_dep_intervals.intersect(b, ti, r); + m_dep_intervals.set(b, r); } } + + template bool intervals::interval_from_lar_term(lp::lar_term const& t, scoped_dep_interval& i) { m_dep_intervals.set_value(i, rational::zero()); @@ -363,21 +375,14 @@ bool intervals::interval_of_sum_no_term(const nex_sum& e, scoped_dep_interval & // return true iff a.upper < b.lower, or a.upper == b.lower and one of these bounds is open bool intervals::conflict_u_l(const interval& a, const interval& b) const { - if (a.m_upper_inf) { + if (a.m_upper_inf) return false; - } - if (b.m_lower_inf) { + if (b.m_lower_inf) return false; - } - - if (m_dep_intervals.num_manager().lt(a.m_upper, b.m_lower)) { + if (m_dep_intervals.num_manager().lt(a.m_upper, b.m_lower)) return true; - } - - if (m_dep_intervals.num_manager().gt(a.m_upper, b.m_lower)) { - return false; - } - + if (m_dep_intervals.num_manager().gt(a.m_upper, b.m_lower)) + return false; return a.m_upper_open || b.m_upper_open; } @@ -468,31 +473,24 @@ template bool intervals::interval_of_expr(const nex* e, unsigned p, scoped_dep_interval& a, const std::function& f) { switch (e->type()) { case expr_type::SCALAR: - { - m_dep_intervals.set_interval_for_scalar(a, power(to_scalar(e)->value(), p)); - } + m_dep_intervals.set_interval_for_scalar(a, power(to_scalar(e)->value(), p)); break; - case expr_type::SUM: { + case expr_type::SUM: if (!interval_of_sum(e->to_sum(), a, f)) return false; - if (p != 1) { + if (p != 1) to_power(a, p); - } break; - } - case expr_type::MUL: { + case expr_type::MUL: if (!interval_of_mul(e->to_mul(), a, f)) return false; - if (p != 1) { + if (p != 1) to_power(a, p); - } break; - } case expr_type::VAR: set_var_interval(e->to_var().var(), a); - if (p != 1) { + if (p != 1) to_power(a, p); - } break; default: TRACE("nla_intervals_details", tout << e->type() << "\n";); @@ -507,5 +505,7 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } + } // end of nla namespace + diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index d39f1c8d8..7455f676d 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -52,6 +52,12 @@ public: template void set_var_interval(lpvar v, interval& b); + template + void set_var_interval1(lpvar v, interval& b); + + template + bool set_var_interval2(lpvar v, scoped_dep_interval& b); + template bool interval_from_term(const nex& e, scoped_dep_interval& i); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 24cfd4b46..9b42b2c07 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1420,8 +1420,11 @@ namespace arith { } void solver::assume_literals() { - for (auto const& ineq : m_nla_literals) - s().set_phase(mk_ineq_literal(ineq)); + for (auto const& ineq : m_nla_literals) { + auto lit = mk_ineq_literal(ineq); + ctx.mark_relevant(lit); + s().set_phase(lit); + } } sat::literal solver::mk_ineq_literal(nla::ineq const& ineq) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index db12e852a..110adc039 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2575,17 +2575,18 @@ public: void assume_literal(nla::ineq const& i) { auto lit = mk_literal(i); + ctx().mark_as_relevant(lit); ctx().set_true_first_flag(lit.var()); } final_check_status check_nla_continue() { m_a1 = nullptr; m_a2 = nullptr; lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector); - for (const nla::ineq& i : m_nla_literals) - return (assume_literal(i), FC_CONTINUE); switch (r) { case l_false: + for (const nla::ineq& i : m_nla_literals) + assume_literal(i); for (const nla::lemma & l : m_nla_lemma_vector) false_case_of_check_nla(l); return FC_CONTINUE;