From b68af0c1e590c5fdd8543a5deaa99f90e4407a77 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jul 2022 07:38:51 -0700 Subject: [PATCH] working on reconciling perf for arithmetic solvers this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2. The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct. The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2. --- src/math/dd/dd_pdd.h | 6 +- src/math/dd/pdd_interval.h | 34 ++++- src/math/grobner/grobner.cpp | 32 ++--- src/math/grobner/grobner.h | 32 ++++- src/math/grobner/pdd_solver.cpp | 2 +- src/math/interval/dep_intervals.h | 1 - src/math/lp/horner.cpp | 4 +- src/math/lp/lar_solver.h | 8 +- src/math/lp/nla_common.cpp | 8 +- src/math/lp/nla_core.cpp | 202 ++++++++++++++++----------- src/math/lp/nla_core.h | 7 +- src/math/lp/nla_order_lemmas.cpp | 2 +- src/math/lp/nla_settings.h | 116 ++++----------- src/math/lp/nla_tangent_lemmas.cpp | 2 +- src/sat/smt/arith_internalize.cpp | 34 ++--- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/theory_arith_core.h | 2 +- src/smt/theory_arith_nl.h | 63 ++++----- src/smt/theory_lra.cpp | 82 +++++++---- 19 files changed, 357 insertions(+), 282 deletions(-) diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index d061bb0f7..78c447494 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -398,13 +398,17 @@ namespace dd { inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); } inline pdd operator-(int x, pdd const& b) { return rational(x) - b; } inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); } - + inline pdd operator-(pdd const& b, rational const& r) { return b + (-r); } + inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; } inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; } inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; } inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; } inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; } inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; } + inline pdd& operator+=(pdd & p, rational const& v) { p = p + v; return p; } + inline pdd& operator-=(pdd & p, rational const& v) { p = p - v; return p; } + inline pdd& operator*=(pdd & p, rational const& v) { p = p * v; return p; } std::ostream& operator<<(std::ostream& out, pdd const& b); diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index 55d2c9b21..d8e2b8db1 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -27,7 +27,33 @@ typedef dep_intervals::with_deps_t w_dep; class pdd_interval { dep_intervals& m_dep_intervals; std::function m_var2interval; - + + // retrieve intervals after distributing multiplication over addition. + template + void get_interval_distributed(pdd const& p, scoped_dep_interval& i, scoped_dep_interval& ret) { + bool deps = wd == w_dep::with_deps; + if (p.is_val()) { + if (deps) + m_dep_intervals.mul(p.val(), i, ret); + else + m_dep_intervals.mul(p.val(), i, ret); + return; + } + scoped_dep_interval hi(m()), lo(m()), t(m()), a(m()); + get_interval_distributed(p.lo(), i, lo); + m_var2interval(p.var(), deps, a); + if (deps) { + m_dep_intervals.mul(a, i, t); + get_interval_distributed(p.hi(), t, hi); + m_dep_intervals.add(hi, lo, ret); + } + else { + m_dep_intervals.mul(a, i, t); + get_interval_distributed(p.hi(), t, hi); + m_dep_intervals.add(hi, lo, ret); + } + } + public: pdd_interval(dep_intervals& d): m_dep_intervals(d) {} @@ -57,5 +83,11 @@ public: } } + template + void get_interval_distributed(pdd const& p, scoped_dep_interval& ret) { + scoped_dep_interval i(m()); + m_dep_intervals.set_interval_for_scalar(i, rational::one()); + get_interval_distributed(p, i, ret); + } }; } diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 264c2a08c..39a327891 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -132,7 +132,7 @@ void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const * } } -void grobner::display_monomial(std::ostream & out, monomial const & m) const { +void grobner::display_monomial(std::ostream & out, monomial const & m, std::function& display_var) const { if (!m.m_coeff.is_one() || m.m_vars.empty()) { out << m.m_coeff; if (!m.m_vars.empty()) @@ -165,7 +165,7 @@ void grobner::display_monomial(std::ostream & out, monomial const & m) const { } } -void grobner::display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const { +void grobner::display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials, std::function& display_var) const { bool first = true; for (unsigned i = 0; i < num_monomials; i++) { monomial const * m = monomials[i]; @@ -173,26 +173,26 @@ void grobner::display_monomials(std::ostream & out, unsigned num_monomials, mono first = false; else out << " + "; - display_monomial(out, *m); + display_monomial(out, *m, display_var); } } -void grobner::display_equation(std::ostream & out, equation const & eq) const { - display_monomials(out, eq.m_monomials.size(), eq.m_monomials.data()); +void grobner::display_equation(std::ostream & out, equation const & eq, std::function& display_var) const { + display_monomials(out, eq.m_monomials.size(), eq.m_monomials.data(), display_var); out << " = 0\n"; } -void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { - if (!v.empty()) { - out << header << "\n"; - for (equation const* eq : v) - display_equation(out, *eq); - } +void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header, std::function& display_var) const { + if (v.empty()) + return; + out << header << "\n"; + for (equation const* eq : v) + display_equation(out, *eq, display_var); } -void grobner::display(std::ostream & out) const { - display_equations(out, m_processed, "processed:"); - display_equations(out, m_to_process, "to process:"); +void grobner::display(std::ostream & out, std::function& display_var) const { + display_equations(out, m_processed, "processed:", display_var); + display_equations(out, m_to_process, "to process:", display_var); } void grobner::set_weight(expr * n, int weight) { @@ -528,7 +528,7 @@ bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vectorm_vars[i2]); TRACE("grobner", - tout << "monomail: "; display_monomial(tout, *m1); tout << " is a subset of "; + tout << "monomial: "; display_monomial(tout, *m1); tout << " is a subset of "; display_monomial(tout, *m2); tout << "\n"; tout << "rest: "; display_vars(tout, rest.size(), rest.data()); tout << "\n";); return true; @@ -552,7 +552,7 @@ bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector& display_var) const; - void display_equations(std::ostream & out, equation_set const & v, char const * header) const; + + void display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const { + std::function _fn = [&](std::ostream& out, expr* v) { display_var(out, v); }; + display_monomials(out, num_monomials, monomials, _fn); + } + + + void display_equations(std::ostream & out, equation_set const & v, char const * header, std::function& display_var) const; void del_equations(unsigned old_size); @@ -281,11 +288,26 @@ public: void pop_scope(unsigned num_scopes); - void display_equation(std::ostream & out, equation const & eq) const; + void display_equation(std::ostream & out, equation const & eq) const { + std::function _fn = [&](std::ostream& out, expr* v) { display_var(out, v); }; + display_equation(out, eq, _fn); + } - void display_monomial(std::ostream & out, monomial const & m) const; + void display_monomial(std::ostream & out, monomial const & m) const { + std::function _fn = [&](std::ostream& out, expr* v) { display_var(out, v); }; + display_monomial(out, m, _fn); + } + + void display_equation(std::ostream & out, equation const & eq, std::function& display_var) const; - void display(std::ostream & out) const; + void display_monomial(std::ostream & out, monomial const & m, std::function& display_var) const; + + void display(std::ostream & out) const { + std::function _fn = [&](std::ostream& out, expr* v) { display_var(out, v); }; + display(out, _fn); + } + + void display(std::ostream & out, std::function& display_var) const; }; diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 11c34e180..dd79b506b 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -11,9 +11,9 @@ --*/ +#include "util/uint_set.h" #include "math/grobner/pdd_solver.h" #include "math/grobner/pdd_simplifier.h" -#include "util/uint_set.h" #include diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index edc2da146..990816696 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -222,7 +222,6 @@ public: template void mul(const rational& r, const interval& a, interval& b) const { - if (r.is_zero()) return; m_imanager.mul(r.to_mpq(), a, b); if (wd == with_deps) { auto lower_dep = a.m_lower_dep; diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 82fb89b4e..4d4ac4975 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const { template bool horner::row_is_interesting(const T& row) const { TRACE("nla_solver_details", c().print_row(row, tout);); - if (row.size() > c().m_nla_settings.horner_row_length_limit()) { + if (row.size() > c().m_nla_settings.horner_row_length_limit) { TRACE("nla_solver_details", tout << "disregard\n";); return false; } @@ -98,7 +98,7 @@ bool horner::lemmas_on_row(const T& row) { } bool horner::horner_lemmas() { - if (!c().m_nla_settings.run_horner()) { + if (!c().m_nla_settings.run_horner) { TRACE("nla_solver", tout << "not generating horner lemmas\n";); return false; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 0c61bdcb2..f1cbd3370 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -275,9 +275,6 @@ class lar_solver : public column_namer { return m_column_buffer; } bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const; - inline unsigned get_base_column_in_row(unsigned row_index) const { - return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index); - } inline lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; } void catch_up_in_updating_int_solver(); var_index to_column(unsigned ext_j) const; @@ -357,6 +354,10 @@ public: } void set_value_for_nbasic_column(unsigned j, const impq& new_val); + inline unsigned get_base_column_in_row(unsigned row_index) const { + return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index); + } + // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); @@ -630,6 +631,7 @@ public: } void round_to_integer_solution(); inline const row_strip & get_row(unsigned i) const { return A_r().m_rows[i]; } + inline const row_strip & basic2row(unsigned i) const { return A_r().m_rows[row_of_basic_column(i)]; } inline const column_strip & get_column(unsigned i) const { return A_r().m_columns[i]; } bool row_is_correct(unsigned i) const; bool ax_is_correct() const; diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 8f635f391..45898c613 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -71,11 +71,11 @@ void common::add_deps_of_fixed(lpvar j, u_dependency*& dep) { // creates a nex expression for the coeff and var, nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_dependency*& dep) { SASSERT(!coeff.is_zero()); - if (c().m_nla_settings.horner_subs_fixed() == 1 && c().var_is_fixed(j)) { + if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(j)) { add_deps_of_fixed(j, dep); return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x); } - if (c().m_nla_settings.horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) { + if (c().m_nla_settings.horner_subs_fixed == 2 && c().var_is_fixed_to_zero(j)) { add_deps_of_fixed(j, dep); return cn.mk_scalar(rational(0)); } @@ -89,10 +89,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende mf *= coeff; u_dependency * initial_dep = dep; for (lpvar k : m.vars()) { - if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) { + if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(k)) { add_deps_of_fixed(k, dep); mf *= c().m_lar_solver.column_lower_bound(k).x; - } else if (c().m_nla_settings.horner_subs_fixed() == 2 && + } else if (c().m_nla_settings.horner_subs_fixed == 2 && c().var_is_fixed_to_zero(k)) { dep = initial_dep; add_deps_of_fixed(k, dep); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index d8d4930ce..e6eb8ad26 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -557,7 +557,7 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { } std::ostream & core::print_var(lpvar j, std::ostream & out) const { - if (m_emons.is_monic_var(j)) { + if (is_monic_var(j)) { print_monic(m_emons[j], out); } @@ -846,7 +846,7 @@ std::unordered_set core::collect_vars(const lemma& l) const { std::unordered_set vars; auto insert_j = [&](lpvar j) { vars.insert(j); - if (m_emons.is_monic_var(j)) { + if (is_monic_var(j)) { for (lpvar k : m_emons[j].vars()) vars.insert(k); } @@ -948,7 +948,7 @@ void core::maybe_add_a_factor(lpvar i, std::unordered_set& found_rm, vector & r) const { SASSERT(abs(val(i)) == abs(val(c))); - if (!m_emons.is_monic_var(i)) { + if (!is_monic_var(i)) { i = m_evars.find(i).var(); if (try_insert(i, found_vars)) { r.push_back(factor(i, factor_type::VAR)); @@ -1228,7 +1228,7 @@ bool core::var_breaks_correct_monic_as_factor(lpvar j, const monic& m) const { } bool core::var_breaks_correct_monic(lpvar j) const { - if (emons().is_monic_var(j) && !m_to_refine.contains(j)) { + if (is_monic_var(j) && !m_to_refine.contains(j)) { TRACE("nla_solver", tout << "j = " << j << ", m = "; print_monic(emons()[j], tout) << "\n";); return true; // changing the value of a correct monic } @@ -1333,7 +1333,7 @@ bool in_power(const svector& vs, unsigned l) { bool core::to_refine_is_correct() const { for (unsigned j = 0; j < m_lar_solver.number_of_vars(); j++) { - if (!emons().is_monic_var(j)) continue; + if (!is_monic_var(j)) continue; bool valid = check_monic(emons()[j]); if (valid == m_to_refine.contains(j)) { TRACE("nla_solver", tout << "inconstency in m_to_refine : "; @@ -1414,7 +1414,7 @@ void core::patch_monomials_on_to_refine() { void core::patch_monomials() { m_cautious_patching = true; patch_monomials_on_to_refine(); - if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching()) { + if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching) { return; } NOT_IMPLEMENTED_YET(); @@ -1530,11 +1530,11 @@ lbool core::check(vector& l_vec) { check_weighted(3, checks); unsigned num_calls = lp_settings().stats().m_nla_calls; - if (!conflict_found() && m_nla_settings.run_nra() && num_calls % 50 == 0 && num_calls > 500) + if (!conflict_found() && m_nla_settings.run_nra && num_calls % 50 == 0 && num_calls > 500) ret = bounded_nlsat(); } - if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) { + if (l_vec.empty() && !done() && m_nla_settings.run_nra && ret == l_undef) { ret = m_nra.check(); m_stats.m_nra_calls++; } @@ -1554,7 +1554,7 @@ lbool core::check(vector& l_vec) { } bool core::should_run_bounded_nlsat() { - if (!m_nla_settings.run_nra()) + if (!m_nla_settings.run_nra) return false; if (m_nlsat_delay > m_nlsat_fails) ++m_nlsat_fails; @@ -1619,8 +1619,13 @@ std::ostream& core::print_terms(std::ostream& out) const { } std::string core::var_str(lpvar j) const { - return is_monic_var(j)? - (product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_")) : (std::string("j") + lp::T_to_string(j)); + std::string result; + if (is_monic_var(j)) + result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_"); + else + result += std::string("j") + lp::T_to_string(j); + // result += ":w" + lp::T_to_string(get_var_weight(j)); + return result; } std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const { @@ -1632,7 +1637,7 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const void core::run_grobner() { - unsigned& quota = m_nla_settings.grobner_quota(); + unsigned& quota = m_nla_settings.grobner_quota; if (quota == 1) { return; } @@ -1645,13 +1650,14 @@ void core::run_grobner() { bool conflict = false; unsigned n = m_pdd_grobner.number_of_conflicts_to_report(); SASSERT(n > 0); - for (auto eq : m_pdd_grobner.equations()) { + for (auto eq : m_pdd_grobner.equations()) { if (check_pdd_eq(eq)) { conflict = true; if (--n == 0) break; } } + TRACE("grobner", m_pdd_grobner.display(tout)); if (conflict) { IF_VERBOSE(2, verbose_stream() << "grobner conflict\n"); return; @@ -1694,14 +1700,32 @@ void core::configure_grobner() { m_pdd_grobner.reset(); try { set_level2var_for_grobner(); - for (unsigned i : m_rows) { - add_row_to_grobner(m_lar_solver.A_r().m_rows[i]); + TRACE("grobner", + tout << "base vars: "; + for (lpvar j : active_var_set()) + if (m_lar_solver.is_base(j)) + tout << "j" << j << " "; + tout << "\n"); + for (lpvar j : active_var_set()) { + if (m_lar_solver.is_base(j)) + add_row_to_grobner(m_lar_solver.basic2row(j)); + + if (is_monic_var(j) && var_is_fixed(j)) { + u_dependency* dep = nullptr; + dd::pdd r = m_pdd_manager.mk_val(rational(1)); + for (lpvar k : emons()[j].vars()) + r *= pdd_expr(rational::one(), k, dep); + r -= val_of_fixed_var_with_deps(j, dep); + m_pdd_grobner.add(r, dep); + } } } catch (...) { IF_VERBOSE(2, verbose_stream() << "pdd throw\n"); return; } + TRACE("grobner", m_pdd_grobner.display(tout)); + #if 0 IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream())); dd::pdd_eval eval(m_pdd_manager); @@ -1717,11 +1741,11 @@ void core::configure_grobner() { struct dd::solver::config cfg; cfg.m_max_steps = m_pdd_grobner.equations().size(); - cfg.m_max_simplified = m_nla_settings.grobner_max_simplified(); - cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth(); - cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth(); - cfg.m_expr_degree_growth = m_nla_settings.grobner_expr_degree_growth(); - cfg.m_number_of_conflicts_to_report = m_nla_settings.grobner_number_of_conflicts_to_report(); + cfg.m_max_simplified = m_nla_settings.grobner_max_simplified; + cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth; + cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth; + cfg.m_expr_degree_growth = m_nla_settings.grobner_expr_degree_growth; + cfg.m_number_of_conflicts_to_report = m_nla_settings.grobner_number_of_conflicts_to_report; m_pdd_grobner.set(cfg); m_pdd_grobner.adjust_cfg(); m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. @@ -1762,49 +1786,66 @@ bool core::check_pdd_eq(const dd::solver::equation* e) { }; scoped_dep_interval i(di), i_wd(di); eval.get_interval(e->poly(), i); - if (!di.separated_from_zero(i)) + if (!di.separated_from_zero(i)) { + TRACE("grobner", m_pdd_grobner.display(tout << "not separated from 0 ", *e) << "\n"; + eval.get_interval_distributed(e->poly(), i); + tout << "separated from 0: " << di.separated_from_zero(i) << "\n"; + for (auto j : e->poly().free_vars()) { + scoped_dep_interval a(di); + m_intervals.set_var_interval(j, a); + m_intervals.display(tout << "j" << j << " ", a); tout << " "; + } + tout << "\n"); + return false; + } eval.get_interval(e->poly(), i_wd); std::function f = [this](const lp::explanation& e) { new_lemma lemma(*this, "pdd"); lemma &= e; }; if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) { + TRACE("grobner", m_pdd_grobner.display(tout << "conflict ", *e) << "\n"); lp_settings().stats().m_grobner_conflicts++; return true; } else { + TRACE("grobner", m_pdd_grobner.display(tout << "no conflict ", *e) << "\n"); return false; } } void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector & q) { - if (active_var_set_contains(j) || var_is_fixed(j)) return; - TRACE("grobner", tout << "j = " << j << ", " << pp(j);); - const auto& matrix = m_lar_solver.A_r(); + if (active_var_set_contains(j)) + return; insert_to_active_var_set(j); - for (auto & s : matrix.m_columns[j]) { - unsigned row = s.var(); - if (m_rows.contains(row)) continue; - if (matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit()) { - TRACE("grobner", tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); - continue; - } - m_rows.insert(row); - for (auto& rc : matrix.m_rows[row]) { - add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q); - } + if (is_monic_var(j)) { + const monic& m = emons()[j]; + for (auto fcn : factorization_factory_imp(m, *this)) + for (const factor& fc: fcn) + q.push_back(var(fc)); } - if (!is_monic_var(j)) + if (var_is_fixed(j)) return; + const auto& matrix = m_lar_solver.A_r(); + for (auto & s : matrix.m_columns[j]) { + unsigned row = s.var(); + if (m_rows.contains(row)) + continue; + m_rows.insert(row); + unsigned k = m_lar_solver.get_base_column_in_row(row); + if (m_lar_solver.column_is_free(k) && k != j) + continue; + CTRACE("grobner", matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit, + tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); + if (matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit) + continue; + for (auto& rc : matrix.m_rows[row]) + add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q); + } + - const monic& m = emons()[j]; - for (auto fcn : factorization_factory_imp(m, *this)) { - for (const factor& fc: fcn) { - q.push_back(var(fc)); - } - } } const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) { @@ -1816,41 +1857,36 @@ const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) { } dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) { - if (m_nla_settings.grobner_subs_fixed() == 1 && var_is_fixed(j)) { - return m_pdd_manager.mk_val(c * val_of_fixed_var_with_deps(j, dep)); - } - - if (m_nla_settings.grobner_subs_fixed() == 2 && var_is_fixed_to_zero(j)) { - return m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, dep)); - } - - if (!is_monic_var(j)) - return c * m_pdd_manager.mk_var(j); - - u_dependency* zero_dep = dep; - // j is a monic var dd::pdd r = m_pdd_manager.mk_val(c); - const monic& m = emons()[j]; - for (lpvar k : m.vars()) { - if (m_nla_settings.grobner_subs_fixed() && var_is_fixed(k)) { - r *= m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep)); - } else if (m_nla_settings.grobner_subs_fixed() == 2 && var_is_fixed_to_zero(k)) { - r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, zero_dep)); + sbuffer vars; + vars.push_back(j); + u_dependency* zero_dep = dep; + while (!vars.empty()) { + j = vars.back(); + vars.pop_back(); + if (m_nla_settings.grobner_subs_fixed > 0 && var_is_fixed_to_zero(j)) { + r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, zero_dep)); dep = zero_dep; return r; - } else { - r *= m_pdd_manager.mk_var(k); } + if (m_nla_settings.grobner_subs_fixed == 1 && var_is_fixed(j)) + r *= val_of_fixed_var_with_deps(j, dep); + else if (!is_monic_var(j)) + r *= m_pdd_manager.mk_var(j); + else + for (lpvar k : emons()[j].vars()) + vars.push_back(k); } return r; } void core::add_row_to_grobner(const vector> & row) { u_dependency *dep = nullptr; + rational val; dd::pdd sum = m_pdd_manager.mk_val(rational(0)); - for (const auto &p : row) { - sum += pdd_expr(p.coeff(), p.var(), dep); - } + for (const auto &p : row) + sum += pdd_expr(p.coeff(), p.var(), dep); + TRACE("grobner", print_row(row, tout) << " " << sum << "\n"); m_pdd_grobner.add(sum, dep); } @@ -1858,17 +1894,21 @@ void core::add_row_to_grobner(const vector> & row) { void core::find_nl_cluster() { prepare_rows_and_active_vars(); svector q; - for (lpvar j : m_to_refine) { - TRACE("grobner", print_monic(emons()[j], tout) << "\n";); + TRACE("grobner", for (lpvar j : m_to_refine) print_monic(emons()[j], tout) << "\n";); + + for (lpvar j : m_to_refine) q.push_back(j); - } while (!q.empty()) { lpvar j = q.back(); q.pop_back(); add_var_and_its_factors_to_q_and_collect_new_rows(j, q); } - TRACE("grobner", display_matrix_of_m_rows(tout);); + TRACE("grobner", tout << "vars in cluster: "; + for (lpvar j : active_var_set()) tout << "j" << j << " "; tout << "\n"; + display_matrix_of_m_rows(tout); + /*emons().display(tout << "emons\n");*/ + ); } void core::prepare_rows_and_active_vars() { @@ -1902,18 +1942,16 @@ std::unordered_set core::get_vars_of_expr_with_opening_terms(const nex *e void core::display_matrix_of_m_rows(std::ostream & out) const { const auto& matrix = m_lar_solver.A_r(); - out << m_rows.size() << " rows" <<"\n"; + out << m_rows.size() << " rows" << "\n"; out << "the matrix\n"; - for (const auto & r : matrix.m_rows) { + for (const auto & r : matrix.m_rows) print_row(r, out) << std::endl; - } } void core::set_active_vars_weights(nex_creator& nc) { nc.set_number_of_vars(m_lar_solver.column_count()); - for (lpvar j : active_var_set()) { + for (lpvar j : active_var_set()) nc.set_var_weight(j, get_var_weight(j)); - } } void core::set_level2var_for_grobner() { @@ -1944,6 +1982,11 @@ void core::set_level2var_for_grobner() { l2v[j] = sorted_vars[j]; m_pdd_manager.reset(l2v); + + TRACE("grobner", + for (auto v : sorted_vars) + tout << "j" << v << " w:" << weighted_vars[v] << " "; + tout << "\n"); } unsigned core::get_var_weight(lpvar j) const { @@ -1954,14 +1997,14 @@ unsigned core::get_var_weight(lpvar j) const { k = 0; break; case lp::column_type::boxed: - k = 2; + k = 3; break; case lp::column_type::lower_bound: case lp::column_type::upper_bound: - k = 4; + k = 6; break; case lp::column_type::free_column: - k = 6; + k = 9; break; default: UNREACHABLE(); @@ -1969,9 +2012,8 @@ unsigned core::get_var_weight(lpvar j) const { } if (is_monic_var(j)) { k++; - if (m_to_refine.contains(j)) { + if (m_to_refine.contains(j)) k++; - } } return k; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d0dc8d77d..e50075564 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -243,11 +243,11 @@ public: // returns true if the combination of the Horner's schema and Grobner Basis should be called bool need_run_horner() const { - return m_nla_settings.run_horner() && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; + return m_nla_settings.run_horner && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency == 0; } bool need_run_grobner() const { - return m_nla_settings.run_grobner() && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; + return m_nla_settings.run_grobner && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0; } void incremental_linearization(bool); @@ -456,8 +456,7 @@ public: for (auto p : row) { v.push_back(std::make_pair(p.coeff(), p.var())); } - return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, - out); + return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out); } void run_grobner(); void find_nl_cluster(); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index a7910601f..94ddc4d9b 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -19,7 +19,7 @@ typedef lp::lar_term term; // a > b && c > 0 => ac > bc void order::order_lemma() { TRACE("nla_solver", ); - if (!c().m_nla_settings.run_order()) { + if (!c().m_nla_settings.run_order) { TRACE("nla_solver", tout << "not generating order lemmas\n";); return; } diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 4045f4567..ec11ea5b2 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -9,94 +9,38 @@ Author: #pragma once namespace nla { -class nla_settings { - bool m_run_order; - bool m_run_tangents; - bool m_run_horner; - // how often to call the horner heuristic - unsigned m_horner_frequency; - unsigned m_horner_row_length_limit; - unsigned m_horner_subs_fixed; - // grobner fields - bool m_run_grobner; - unsigned m_grobner_row_length_limit; - unsigned m_grobner_subs_fixed; - unsigned m_grobner_eqs_growth; - unsigned m_grobner_tree_size_growth; - unsigned m_grobner_expr_size_growth; - unsigned m_grobner_expr_degree_growth; - unsigned m_grobner_max_simplified; - unsigned m_grobner_number_of_conflicts_to_report; - unsigned m_grobner_quota; - unsigned m_grobner_frequency; - bool m_run_nra; - // expensive patching - bool m_expensive_patching; -public: - nla_settings() : m_run_order(true), - m_run_tangents(true), - m_run_horner(true), - m_horner_frequency(4), - m_horner_row_length_limit(10), - m_horner_subs_fixed(2), - m_run_grobner(true), - m_grobner_row_length_limit(50), - m_grobner_subs_fixed(false), - m_grobner_quota(0), - m_grobner_frequency(4), - m_run_nra(false), - m_expensive_patching(false) - {} - unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;} - unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;} - bool run_order() const { return m_run_order; } - bool& run_order() { return m_run_order; } + struct nla_settings { + bool run_order = true; + bool run_tangents = true; + + // horner fields + bool run_horner = true; + unsigned horner_frequency = 4; + unsigned horner_row_length_limit = 10; + unsigned horner_subs_fixed = 2; - bool run_tangents() const { return m_run_tangents; } - bool& run_tangents() { return m_run_tangents; } + + // grobner fields + bool run_grobner = true; + unsigned grobner_row_length_limit = 50; + unsigned grobner_subs_fixed = 1; + unsigned grobner_eqs_growth = 10; + unsigned grobner_tree_size_growth = 2; + unsigned grobner_expr_size_growth = 2; + unsigned grobner_expr_degree_growth = 2; + unsigned grobner_max_simplified = 10000; + unsigned grobner_number_of_conflicts_to_report = 1; + unsigned grobner_quota = 0; + unsigned grobner_frequency = 4; - bool expensive_patching() const { return m_expensive_patching; } - bool& expensive_patching() { return m_expensive_patching; } - bool run_horner() const { return m_run_horner; } - bool& run_horner() { return m_run_horner; } - - unsigned horner_frequency() const { return m_horner_frequency; } - unsigned& horner_frequency() { return m_horner_frequency; } - unsigned horner_row_length_limit() const { return m_horner_row_length_limit; } - unsigned& horner_row_length_limit() { return m_horner_row_length_limit; } - unsigned horner_subs_fixed() const { return m_horner_subs_fixed; } - unsigned& horner_subs_fixed() { return m_horner_subs_fixed; } - - bool run_grobner() const { return m_run_grobner; } - bool& run_grobner() { return m_run_grobner; } - unsigned grobner_frequency() const { return m_grobner_frequency; } - unsigned& grobner_frequency() { return m_grobner_frequency; } - - bool run_nra() const { return m_run_nra; } - bool& run_nra() { return m_run_nra; } - - unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; } - unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; } - unsigned grobner_subs_fixed() const { return m_grobner_subs_fixed; } - unsigned& grobner_subs_fixed() { return m_grobner_subs_fixed; } - - unsigned grobner_tree_size_growth() const { return m_grobner_tree_size_growth; } - unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; } - - unsigned grobner_expr_size_growth() const { return m_grobner_expr_size_growth; } - unsigned & grobner_expr_size_growth() { return m_grobner_expr_size_growth; } - - unsigned grobner_expr_degree_growth() const { return m_grobner_expr_degree_growth; } - unsigned & grobner_expr_degree_growth() { return m_grobner_expr_degree_growth; } - - unsigned grobner_max_simplified() const { return m_grobner_max_simplified; } - unsigned & grobner_max_simplified() { return m_grobner_max_simplified; } - - unsigned grobner_number_of_conflicts_to_report() const { return m_grobner_number_of_conflicts_to_report; } - unsigned & grobner_number_of_conflicts_to_report() { return m_grobner_number_of_conflicts_to_report; } - - unsigned& grobner_quota() { return m_grobner_quota; } + // nra fields + bool run_nra = false; -}; + // expensive patching + bool expensive_patching = false; + + nla_settings() {} + + }; } diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index d01dc51ca..299d8031f 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -186,7 +186,7 @@ tangents::tangents(core * c) : common(c) {} void tangents::tangent_lemma() { factorization bf(nullptr); const monic* m = nullptr; - if (c().m_nla_settings.run_tangents() && c().find_bfc_to_refine(m, bf)) { + if (c().m_nla_settings.run_tangents && c().find_bfc_to_refine(m, bf)) { lpvar j = m->var(); tangent_imp tangent(point(val(bf[0]), val(bf[1])), c().val(j), *m, bf, *this); tangent(); diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 732cbfc6f..09352e147 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -69,23 +69,23 @@ namespace arith { m_nla->push(); } smt_params_helper prms(s().params()); - m_nla->settings().run_order() = prms.arith_nl_order(); - m_nla->settings().run_tangents() = prms.arith_nl_tangents(); - m_nla->settings().run_horner() = prms.arith_nl_horner(); - m_nla->settings().horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); - m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency(); - m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); - m_nla->settings().run_grobner() = prms.arith_nl_grobner(); - m_nla->settings().run_nra() = prms.arith_nl_nra(); - m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); - m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); - m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); - m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); - m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); - m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); - m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); - m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); - m_nla->settings().expensive_patching() = false; + m_nla->settings().run_order = prms.arith_nl_order(); + m_nla->settings().run_tangents = prms.arith_nl_tangents(); + m_nla->settings().run_horner = prms.arith_nl_horner(); + m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed(); + m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency(); + m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit(); + m_nla->settings().run_grobner = prms.arith_nl_grobner(); + m_nla->settings().run_nra = prms.arith_nl_nra(); + m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed(); + m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth(); + m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth(); + m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth(); + m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified(); + m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report(); + m_nla->settings().grobner_quota = prms.arith_nl_gr_q(); + m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency(); + m_nla->settings().expensive_patching = false; } } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 33b3e458f..2cf29ffa8 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -71,7 +71,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), - ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 808984521..1b2a7cc49 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -592,7 +592,7 @@ namespace smt { // (or (= y 0) (<= (* y (div x y)) x)) else if (!m_util.is_numeral(divisor)) { - expr_ref div_ge(m), div_le(m), ge(m), le(m); + expr_ref div_ge(m); div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero); s(div_ge); mk_axiom(eqz, div_ge, false); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 436dccc6a..3aa34cbc7 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -80,14 +80,12 @@ void theory_arith::mark_dependents(theory_var v, svector & vars if (is_fixed(v)) return; column & c = m_columns[v]; - typename svector::iterator it = c.begin_entries(); - typename svector::iterator end = c.end_entries(); - for (; it != end; ++it) { - if (it->is_dead() || already_visited_rows.contains(it->m_row_id)) + for (auto& ce : c) { + if (ce.is_dead() || already_visited_rows.contains(ce.m_row_id)) continue; - TRACE("non_linear_bug", tout << "visiting row: " << it->m_row_id << "\n";); - already_visited_rows.insert(it->m_row_id); - row & r = m_rows[it->m_row_id]; + TRACE("non_linear_bug", tout << "visiting row: " << ce.m_row_id << "\n";); + already_visited_rows.insert(ce.m_row_id); + row & r = m_rows[ce.m_row_id]; theory_var s = r.get_base_var(); // ignore quasi base vars... actually they should not be used if the problem is non linear... if (is_quasi_base(s)) @@ -97,14 +95,10 @@ void theory_arith::mark_dependents(theory_var v, svector & vars // was eliminated by substitution. if (s != null_theory_var && is_free(s) && s != v) continue; - typename vector::const_iterator it2 = r.begin_entries(); - typename vector::const_iterator end2 = r.end_entries(); - for (; it2 != end2; ++it2) { - if (!it2->is_dead() && !is_fixed(it2->m_var)) - mark_var(it2->m_var, vars, already_found); - if (!it2->is_dead() && is_fixed(it2->m_var)) { - TRACE("non_linear", tout << "skipped fixed\n";); - } + for (auto& re : r) { + if (!re.is_dead() && !is_fixed(re.m_var)) + mark_var(re.m_var, vars, already_found); + CTRACE("non_linear", !re.is_dead() && is_fixed(re.m_var), tout << "skipped fixed\n"); } } } @@ -119,6 +113,7 @@ void theory_arith::get_non_linear_cluster(svector & vars) { return; var_set already_found; row_set already_visited_rows; + for (theory_var v : m_nl_monomials) { expr * n = var2expr(v); if (ctx.is_relevant(n)) @@ -130,9 +125,9 @@ void theory_arith::get_non_linear_cluster(svector & vars) { TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";); mark_dependents(v, vars, already_found, already_visited_rows); } - TRACE("non_linear", tout << "variables in non linear cluster:\n"; - for (theory_var v : vars) tout << "v" << v << " "; - tout << "\n";); + TRACE("non_linear", tout << "variables in non linear cluster: "; + for (theory_var v : vars) tout << "v" << v << " "; tout << "\n"; + for (theory_var v : m_nl_monomials) tout << "non-linear v" << v << " " << mk_pp(var2expr(v), m) << "\n";); } @@ -1740,22 +1735,21 @@ grobner::monomial * theory_arith::mk_gb_monomial(rational const & _coeff, e */ template void theory_arith::add_row_to_gb(row const & r, grobner & gb) { - TRACE("non_linear", tout << "adding row to gb\n"; display_row(tout, r);); + TRACE("grobner", tout << "adding row to gb\n"; display_row(tout, r);); ptr_buffer monomials; v_dependency * dep = nullptr; m_tmp_var_set.reset(); - typename vector::const_iterator it = r.begin_entries(); - typename vector::const_iterator end = r.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead()) { - rational coeff = it->m_coeff.to_rational(); - expr * m = var2expr(it->m_var); - TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";); - grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set); - TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";); - if (new_m) - monomials.push_back(new_m); - } + for (auto& re : r) { + if (re.is_dead()) + continue; + rational coeff = re.m_coeff.to_rational(); + expr * m = var2expr(re.m_var); + grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set); + if (new_m) + monomials.push_back(new_m); + TRACE("grobner", + tout << "monomial: " << mk_pp(m, get_manager()) << "\n"; + tout << "new monomial: "; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";); } gb.assert_eq_0(monomials.size(), monomials.data(), dep); } @@ -2158,8 +2152,9 @@ bool theory_arith::get_gb_eqs_and_look_for_conflict(ptr_vector _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); }; for (grobner::equation* eq : eqs) - gb.display_equation(tout, *eq); + gb.display_equation(tout, *eq, _fn); ); for (grobner::equation* eq : eqs) { if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) { @@ -2259,7 +2254,9 @@ typename theory_arith::gb_result theory_arith::compute_grobner(svector ptr_vector eqs; do { - TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout);); + TRACE("grobner", tout << "before grobner:\n"; + std::function _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); }; + gb.display(tout, _fn)); compute_basis(gb, warn); update_statistics(gb); TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout);); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 67d9988ed..794a61e76 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -276,23 +276,23 @@ class theory_lra::imp { m_nla->push(); } smt_params_helper prms(ctx().get_params()); - m_nla->settings().run_order() = prms.arith_nl_order(); - m_nla->settings().run_tangents() = prms.arith_nl_tangents(); - m_nla->settings().run_horner() = prms.arith_nl_horner(); - m_nla->settings().horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); - m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency(); - m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); - m_nla->settings().run_grobner() = prms.arith_nl_grobner(); - m_nla->settings().run_nra() = prms.arith_nl_nra(); - m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); - m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); - m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); - m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); - m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); - m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); - m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); - m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); - m_nla->settings().expensive_patching() = false; + m_nla->settings().run_order = prms.arith_nl_order(); + m_nla->settings().run_tangents = prms.arith_nl_tangents(); + m_nla->settings().run_horner = prms.arith_nl_horner(); + m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed(); + m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency(); + m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit(); + m_nla->settings().run_grobner = prms.arith_nl_grobner(); + m_nla->settings().run_nra = prms.arith_nl_nra(); + m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed(); + m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth(); + m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth(); + m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth(); + m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified(); + m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report(); + m_nla->settings().grobner_quota = prms.arith_nl_gr_q(); + m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency(); + m_nla->settings().expensive_patching = false; } } @@ -1224,9 +1224,9 @@ public: return; } expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m); - + ctx().get_rewriter()(mod_r); expr_ref eq_r(th.mk_eq_atom(mod_r, p), m); - ctx().internalize(eq_r, false); + ctx().internalize(eq_r, false); literal eq = ctx().get_literal(eq_r); rational k(0); @@ -1256,6 +1256,38 @@ public: } else { + expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m); + expr_ref mone(a.mk_int(-1), m); + expr_ref modmq(a.mk_sub(mod, abs_q), m); + ctx().get_rewriter()(modmq); + literal eqz = mk_literal(m.mk_eq(q, zero)); + literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); + literal mod_lt_q = mk_literal(a.mk_le(modmq, mone)); + + // q = 0 or p = (p mod q) + q * (p div q) + // q = 0 or (p mod q) >= 0 + // q = 0 or (p mod q) < abs(q) + + mk_axiom(eqz, eq); + mk_axiom(eqz, mod_ge_0); + mk_axiom(eqz, mod_lt_q); + + if (a.is_zero(p)) { + mk_axiom(eqz, mk_literal(m.mk_eq(div, zero))); + mk_axiom(eqz, mk_literal(m.mk_eq(mod, zero))); + } + // (or (= y 0) (<= (* y (div x y)) x)) + else if (!a.is_numeral(q)) { + expr_ref div_ge(m); + div_ge = a.mk_ge(a.mk_sub(p, a.mk_mul(q, div)), zero); + ctx().get_rewriter()(div_ge); + mk_axiom(eqz, mk_literal(div_ge)); + TRACE("arith", tout << eqz << " " << div_ge << "\n"); + } + + +#if 0 + /*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero)); /*literal div_le_0 = */ mk_literal(a.mk_le(div, zero)); /*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero)); @@ -1266,7 +1298,7 @@ public: // q >= 0 or (p mod q) >= 0 // q <= 0 or (p mod q) >= 0 // q <= 0 or (p mod q) < q - // q >= 0 or (p mod q) < -q + // q >= 0 or (p mod q) < -q literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); literal q_le_0 = mk_literal(a.mk_le(q, zero)); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); @@ -1277,11 +1309,11 @@ public: mk_axiom(q_le_0, mod_ge_0); mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); - +#endif #if 0 // seem expensive - + mk_axiom(q_le_0, ~p_ge_0, div_ge_0); mk_axiom(q_le_0, ~p_le_0, div_le_0); mk_axiom(q_ge_0, ~p_ge_0, div_le_0); @@ -1293,19 +1325,21 @@ public: mk_axiom(q_ge_0, p_le_0, ~div_ge_0); #endif +#if 0 std::function log = [&,this]() { th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero))); th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); + }; + if_trace_stream _ts(m, log); +#endif #if 0 th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); #endif - }; - if_trace_stream _ts(m, log); } if (params().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) { unsigned _k = k.get_unsigned();