From 50654f1f4620bf58e132d44d3a22e48a17630922 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Sep 2023 08:52:09 +0900 Subject: [PATCH] add theory propagation to linear monomial propagation Signed-off-by: Nikolaj Bjorner --- src/math/lp/monomial_bounds.cpp | 20 +++++++++++++++++++- src/math/lp/monomial_bounds.h | 1 + src/math/lp/nla_core.cpp | 2 ++ src/math/lp/nla_core.h | 8 +++++++- src/math/lp/nla_solver.cpp | 9 +++++++++ src/math/lp/nla_solver.h | 2 ++ src/math/lp/nla_types.h | 14 ++++++++++++++ src/smt/smt_conflict_resolution.cpp | 1 + src/smt/theory_lra.cpp | 27 ++++++++++++++++++++++++++- 9 files changed, 81 insertions(+), 3 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 8e049f059..e3b14d1b7 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -10,6 +10,7 @@ #include "math/lp/monomial_bounds.h" #include "math/lp/nla_core.h" #include "math/lp/nla_intervals.h" +#include "math/lp/numeric_pair.h" namespace nla { @@ -281,9 +282,21 @@ namespace nla { propagate_nonfixed(m, k, w); } + lp::explanation monomial_bounds::get_explanation(u_dependency* dep) { + lp::explanation exp; + svector cs; + c().lra.dep_manager().linearize(dep, cs); + for (auto d : cs) + exp.add_pair(d, mpq(1)); + return exp; + } + void monomial_bounds::propagate_fixed(monic const& m, rational const& k) { auto* dep = explain_fixed(m, k); - c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); + c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); + // propagate fixed equality + auto exp = get_explanation(dep); + c().add_fixed_equality(m.var(), k, exp); } void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) { @@ -294,6 +307,11 @@ namespace nla { auto* dep = explain_fixed(m, k); term_index = c().lra.map_term_index_to_column_index(term_index); c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep); + + if (k == 1) { + lp::explanation exp = get_explanation(dep); + c().add_equality(m.var(), w, exp); + } } u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) { diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index ae05e2026..747aca9a2 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -28,6 +28,7 @@ namespace nla { void propagate_fixed(monic const& m, rational const& k); void propagate_nonfixed(monic const& m, rational const& k, lpvar w); u_dependency* explain_fixed(monic const& m, rational const& k); + lp::explanation get_explanation(u_dependency* dep); bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, dep_interval& product); void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const; bool is_free(lpvar v) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cf0be88fd..e65829ed7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -810,6 +810,8 @@ void core::print_stats(std::ostream& out) { void core::clear() { m_lemmas.clear(); m_literals.clear(); + m_fixed_equalities.clear(); + m_equalities.clear(); } void core::init_search() { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index ddf6d0687..17aa304ac 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -44,7 +44,6 @@ bool try_insert(const A& elem, B& collection) { return true; } - class core { friend struct common; friend class new_lemma; @@ -87,6 +86,8 @@ class core { std::function m_relevant; vector m_lemmas; vector m_literals; + vector m_equalities; + vector m_fixed_equalities; indexed_uint_set m_to_refine; tangents m_tangents; basics m_basics; @@ -430,6 +431,11 @@ public: void collect_statistics(::statistics&); vector const& lemmas() const { return m_lemmas; } vector const& literals() const { return m_literals; } + vector const& equalities() const { return m_equalities; } + vector const& fixed_equalities() const { return m_fixed_equalities; } + + void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } + void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } private: void restore_patched_values(); void constrain_nl_in_tableau(); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index dfbdca4e7..f4d09810e 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -108,4 +108,13 @@ namespace nla { vector const& solver::literals() const { return m_core->literals(); } + + vector const& solver::equalities() const { + return m_core->equalities(); + } + + vector const& solver::fixed_equalities() const { + return m_core->fixed_equalities(); + } + } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 32a3b668e..fec27c32b 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -49,5 +49,7 @@ namespace nla { void collect_statistics(::statistics & st); vector const& lemmas() const; vector const& literals() const; + vector const& fixed_equalities() const; + vector const& equalities() const; }; } diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index 8169266cc..3930a62a9 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -24,6 +24,20 @@ namespace nla { typedef lp::explanation expl_set; typedef lp::var_index lpvar; const lpvar null_lpvar = UINT_MAX; + + struct equality { + lp::lpvar i, j; + lp::explanation e; + equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {} + }; + + struct fixed_equality { + lp::lpvar v; + rational k; + lp::explanation e; + fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {} + }; + inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); } inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index d075c0652..2561fbb5a 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -601,6 +601,7 @@ namespace smt { finalize_resolve(conflict, not_l); + return true; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 14cb12890..1a64d4081 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2112,6 +2112,7 @@ public: bool propagate_core() { m_model_is_initialized = false; flush_bound_axioms(); + // disabled in master: propagate_nla(); if (!can_propagate_core()) return false; m_new_def = false; @@ -2144,7 +2145,6 @@ public: case l_true: propagate_basic_bounds(); propagate_bounds_with_lp_solver(); - // propagate_nla(); break; case l_undef: break; @@ -2156,9 +2156,34 @@ public: if (m_nla) { m_nla->propagate(); add_lemmas(); + add_equalities(); } } + void add_equalities() { + for (auto const& [v,k,e] : m_nla->fixed_equalities()) + add_equality(v, k, e); + for (auto const& [i,j,e] : m_nla->equalities()) + add_eq(i,j,e,false); + } + + void add_equality(lpvar j, rational const& k, lp::explanation const& exp) { + verbose_stream() << "equality " << j << " " << k << "\n"; + TRACE("arith", tout << "equality " << j << " " << k << "\n"); + theory_var v; + if (k == 1) + v = m_one_var; + else if (k == 0) + v = m_zero_var; + else if (!m_value2var.find(k, v)) + return; + theory_var w = lp().local_to_external(j); + if (w < 0) + return; + lpvar i = register_theory_var_in_lar_solver(v); + add_eq(i, j, exp, true); + } + void add_lemmas() { for (const nla::ineq& i : m_nla->literals()) assume_literal(i);