diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index f2a1b0287..06901e062 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -16,7 +16,15 @@ namespace nla { monomial_bounds::monomial_bounds(core* c): common(c), - dep(c->m_intervals.get_dep_intervals()) {} + dep(c->m_intervals.get_dep_intervals()) { + + std::function fixed_eh = [&](lpvar v) { + c->trail().push(push_back_vector(m_fixed_var_trail)); + m_fixed_var_trail.push_back(v); + }; +// uncomment to enable: +// c->lra.m_fixed_var_eh = fixed_eh; + } void monomial_bounds::propagate() { for (lpvar v : c().m_to_refine) { @@ -24,6 +32,46 @@ namespace nla { if (add_lemma()) break; } + propagate_fixed_vars(); + } + + void monomial_bounds::propagate_fixed_vars() { + if (m_fixed_var_qhead == m_fixed_var_trail.size()) + return; + c().trail().push(value_trail(m_fixed_var_qhead)); + while (m_fixed_var_qhead < m_fixed_var_trail.size()) + propagate_fixed_var(m_fixed_var_trail[m_fixed_var_qhead++]); + } + + void monomial_bounds::propagate_fixed_var(lpvar v) { + SASSERT(c().var_is_fixed(v)); + TRACE("nla_solver", tout << "propagate fixed var: " << c().var_str(v) << "\n";); + for (auto const& m : c().emons().get_use_list(v)) + propagate_fixed_var(m, v); + } + + void monomial_bounds::propagate_fixed_var(monic const& m, lpvar v) { + unsigned num_free = 0; + lpvar free_var = null_lpvar; + for (auto w : m) + if (!c().var_is_fixed(w)) + ++num_free, free_var = w; + if (num_free != 1) + return; + u_dependency* d = nullptr; + auto& lra = c().lra; + lp::mpq coeff(1); + for (auto w : m) { + if (c().var_is_fixed(w)) { + d = lra.join_deps(d, lra.join_deps(lra.get_column_lower_bound_witness(w), lra.get_column_upper_bound_witness(w))); + coeff += lra.get_column_value(w).x; + } + } + vector> coeffs; + coeffs.push_back({coeff, free_var}); + coeffs.push_back({mpq(-1), v}); + lpvar j = lra.add_term(coeffs, UINT_MAX); + lra.update_column_type_and_bound(j, llc::EQ, mpq(0), d); } bool monomial_bounds::is_too_big(mpq const& q) const { diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index 19043e072..eb536a231 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -43,6 +43,13 @@ namespace nla { bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero); rational fixed_var_product(monic const& m, lpvar w); lpvar non_fixed_var(monic const& m); + + // fixed variable propagation + unsigned m_fixed_var_qhead = 0; + unsigned_vector m_fixed_var_trail; + void propagate_fixed_vars(); + void propagate_fixed_var(lpvar v); + void propagate_fixed_var(monic const& m, lpvar v); public: monomial_bounds(core* core); void propagate(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index eb1f8b436..ea591e8a5 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -100,11 +100,15 @@ class core { nra::solver m_nra; bool m_cautious_patching = true; lpvar m_patched_var = 0; - monic const* m_patched_monic = nullptr; + monic const* m_patched_monic = nullptr; + + void check_weighted(unsigned sz, std::pair>* checks); void add_bounds(); + + public: // constructor core(lp::lar_solver& s, params_ref const& p, reslimit&); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267805ada..3d1103c4e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -254,45 +254,6 @@ class theory_lra::imp { return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int); } - svector m_fixed_vars; - unsigned m_fixed_vars_head = 0; - - bool propagate_fixed_vars() { - if (m_fixed_vars_head == m_fixed_vars.size()) - return false; - ctx().push_trail(value_trail(m_fixed_vars_head)); - bool propagated = false; - while (m_fixed_vars_head < m_fixed_vars.size()) { - theory_var v = m_fixed_vars[m_fixed_vars_head++]; - enode* n = th.get_enode(v); - for (enode* p : n->get_parents()) { - expr* e = p->get_expr(); - expr* x, * y; - if (!a.is_mul(e, x, y)) - continue; - if (a.is_numeral(x) || a.is_numeral(y)) - continue; - if (x == n->get_expr()) - std::swap(x, y); - if (y != n->get_expr()) - continue; - - // comment out to enable propagation: - continue; - - expr_ref k(a.mk_numeral(get_value(v), a.is_int(y)), m); - literal eq1 = th.mk_eq(y, k, false); - literal eq2 = th.mk_eq(e, a.mk_mul(x, k), false); - ctx().mk_th_axiom(get_id(), ~eq1, eq2); - - // v2 could perform propagation directly - // v3 could consider multiplication of more than two variables. - // such as e := x * y * z. If both x, y become fixed we have e = z * value(x) * value(y) -// verbose_stream() << mk_bounded_pp(e, m) << " - " << mk_bounded_pp(n->get_expr(), m) << "\n"; - } - } - return propagated; - } void ensure_nla() { if (!m_nla) { m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit()); @@ -913,18 +874,6 @@ public: lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); - - std::function new_fixed = [&](lpvar v) { - theory_var u = lp().local_to_external(v); - if (u == null_theory_var) - return; - expr* var = th.get_expr(u); - if (a.is_numeral(var)) - return; - m_fixed_vars.push_back(u); - ctx().push_trail(push_back_vector(m_fixed_vars)); - }; - lp().m_fixed_var_eh = new_fixed; } void internalize_is_int(app * n) { @@ -2135,7 +2084,7 @@ public: } bool propagate() { - return process_atoms() && propagate_core() && propagate_fixed_vars(); + return process_atoms() && propagate_core(); } bool propagate_core() {