From a8f867f1458571b5098ca2cca1bc5ec1cf3c8814 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Jun 2023 18:41:27 -0700 Subject: [PATCH] consolidate settings Signed-off-by: Nikolaj Bjorner --- src/math/lp/horner.cpp | 4 ++-- src/math/lp/nla_common.cpp | 8 ++++---- src/math/lp/nla_core.cpp | 19 ++++++++++++------- src/math/lp/nla_core.h | 10 +++++++--- src/math/lp/nla_grobner.cpp | 24 ++++++++++++------------ src/math/lp/nla_order_lemmas.cpp | 2 +- src/math/lp/nla_settings.h | 28 ---------------------------- src/math/lp/nla_solver.cpp | 4 ++-- src/math/lp/nla_solver.h | 2 +- src/math/lp/nla_tangent_lemmas.cpp | 2 +- src/sat/smt/arith_internalize.cpp | 20 +------------------- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/theory_lra.cpp | 20 +------------------- 13 files changed, 45 insertions(+), 100 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 4d4ac4975..4971b912a 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().params().arith_nl_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().params().arith_nl_horner()) { TRACE("nla_solver", tout << "not generating horner lemmas\n";); return false; } diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 45898c613..00f2ff4ee 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().params().arith_nl_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().params().arith_nl_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 == 1 && c().var_is_fixed(k)) { + if (c().params().arith_nl_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().params().arith_nl_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 afee267c8..fa2f7afd6 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -21,7 +21,7 @@ namespace nla { typedef lp::lar_term term; -core::core(lp::lar_solver& s, reslimit & lim) : +core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_evars(), m_lar_solver(s), m_reslim(lim), @@ -36,6 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_horner(this), m_grobner(this), m_emons(m_evars), + m_params(p), m_use_nra_model(false), m_nra(s, m_nra_lim, *this) { @@ -1504,8 +1505,11 @@ void core::check_bounded_divisions(vector& l_vec) { bool core::can_add_bound(unsigned j, u_map& bounds) { unsigned count = 1; - if (bounds.find(j, count)) + if (bounds.find(j, count)) { + if (count >= 2) + return false; ++count; + } bounds.insert(j, count); struct decrement : public trail { u_map& bounds; @@ -1519,7 +1523,7 @@ bool core::can_add_bound(unsigned j, u_map& bounds) { } }; trail().push(decrement(bounds, j)); - return count < 3; + return true; } void core::add_bounds() { @@ -1566,6 +1570,7 @@ lbool core::check(vector& lits, vector& l_vec) { bool run_grobner = need_run_grobner(); bool run_horner = need_run_horner(); bool run_bounded_nlsat = should_run_bounded_nlsat(); + bool run_bounds = true; //m_nla_settings.branch_nl; @@ -1579,7 +1584,7 @@ lbool core::check(vector& lits, vector& l_vec) { { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; std::function check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); }; - std::function check3 = [&]() { if (no_effect()) add_bounds(); }; + std::function check3 = [&]() { if (no_effect() && run_bounds) add_bounds(); }; std::pair> checks[] = { {1, check1}, @@ -1615,11 +1620,11 @@ lbool core::check(vector& lits, 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() && params().arith_nl_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() && params().arith_nl_nra() && ret == l_undef) { ret = m_nra.check(); m_stats.m_nra_calls++; } @@ -1639,7 +1644,7 @@ lbool core::check(vector& lits, vector& l_vec) { } bool core::should_run_bounded_nlsat() { - if (!m_nla_settings.run_nra) + if (!params().arith_nl_nra()) return false; if (m_nlsat_delay > m_nlsat_fails) ++m_nlsat_fails; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 800701308..a7fadf8e3 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -28,6 +28,7 @@ #include "math/lp/monomial_bounds.h" #include "math/lp/nla_intervals.h" #include "nlsat/nlsat_solver.h" +#include "smt/params/smt_params_helper.hpp" namespace nra { class solver; @@ -103,6 +104,7 @@ class core { mutable lp::u_set m_active_var_set; reslimit m_nra_lim; + smt_params_helper m_params; bool m_use_nra_model = false; nra::solver m_nra; @@ -118,7 +120,7 @@ class core { public: // constructor - core(lp::lar_solver& s, reslimit&); + core(lp::lar_solver& s, params_ref const& p, reslimit&); void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); @@ -173,13 +175,15 @@ public: lpvar var(const factor& f) const { return f.var(); } + smt_params_helper const & params() const { return m_params; } + // 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 params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_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 params().arith_nl_grobner(); // && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0; } void set_active_vars_weights(nex_creator&); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 2fae62426..f293770b9 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -25,7 +25,7 @@ namespace nla { m_pdd_manager(m_core.m_lar_solver.number_of_vars()), m_solver(m_core.m_reslim, m_pdd_manager), m_lar_solver(m_core.m_lar_solver), - m_quota(m_core.m_nla_settings.grobner_quota*2) + m_quota(m_core.params().arith_nl_gr_q()*2) {} lp::lp_settings& grobner::lp_settings() { @@ -34,9 +34,9 @@ namespace nla { void grobner::operator()() { if (m_quota == 0) { - m_quota = 2*c().m_nla_settings.grobner_quota; + m_quota = 2*c().params().arith_nl_gr_q(); } - if (m_quota <= c().m_nla_settings.grobner_quota) { + if (m_quota <= c().params().arith_nl_gr_q()) { ++m_quota; return; } @@ -360,11 +360,11 @@ namespace nla { struct dd::solver::config cfg; cfg.m_max_steps = m_solver.equations().size(); - cfg.m_max_simplified = c().m_nla_settings.grobner_max_simplified; - cfg.m_eqs_growth = c().m_nla_settings.grobner_eqs_growth; - cfg.m_expr_size_growth = c().m_nla_settings.grobner_expr_size_growth; - cfg.m_expr_degree_growth = c().m_nla_settings.grobner_expr_degree_growth; - cfg.m_number_of_conflicts_to_report = c().m_nla_settings.grobner_number_of_conflicts_to_report; + cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified(); + cfg.m_eqs_growth = c().params().arith_nl_grobner_eqs_growth(); + cfg.m_expr_size_growth = c().params().arith_nl_grobner_expr_size_growth(); + cfg.m_expr_degree_growth = c().params().arith_nl_grobner_expr_degree_growth(); + cfg.m_number_of_conflicts_to_report = c().params().arith_nl_grobner_cnfl_to_report(); m_solver.set(cfg); m_solver.adjust_cfg(); m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. @@ -470,9 +470,9 @@ namespace nla { CTRACE("grobner", m_lar_solver.column_is_free(k) && k != j, tout << "skip " << k << "\n"); if (false && m_lar_solver.column_is_free(k) && k != j) continue; - CTRACE("grobner", matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit, + CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit(), tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); - if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit) + if (matrix.m_rows[row].size() > c().params().arith_nl_horner_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); @@ -495,12 +495,12 @@ namespace nla { while (!vars.empty()) { j = vars.back(); vars.pop_back(); - if (c().m_nla_settings.grobner_subs_fixed > 0 && c().var_is_fixed_to_zero(j)) { + if (c().params().arith_nl_grobner_subs_fixed() > 0 && c().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; } - if (c().m_nla_settings.grobner_subs_fixed == 1 && c().var_is_fixed(j)) + if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j)) r *= val_of_fixed_var_with_deps(j, dep); else if (!c().is_monic_var(j)) r *= m_pdd_manager.mk_var(j); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 94ddc4d9b..5f5f24ac4 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().params().arith_nl_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 ec11ea5b2..5c1120a40 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -10,37 +10,9 @@ Author: #pragma once namespace nla { 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; - - - // 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; - - - // nra fields - bool run_nra = false; - // expensive patching bool expensive_patching = false; - nla_settings() {} - }; } diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 9b3f3a762..cab673e07 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -57,8 +57,8 @@ namespace nla { m_core->pop(n); } - solver::solver(lp::lar_solver& s, reslimit& limit): - m_core(alloc(core, s, limit)) { + solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit): + m_core(alloc(core, s, p, limit)) { } bool solver::influences_nl_var(lpvar j) const { diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 09d8191ce..d97e13ae1 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -25,7 +25,7 @@ namespace nla { core* m_core; public: - solver(lp::lar_solver& s, reslimit& limit); + solver(lp::lar_solver& s, params_ref const& p, reslimit& limit); ~solver(); void add_monic(lpvar v, unsigned sz, lpvar const* vs); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 299d8031f..87328e0ec 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().params().arith_nl_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 60ca9651a..4227e66a4 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -61,29 +61,11 @@ namespace arith { void solver::ensure_nla() { if (!m_nla) { - m_nla = alloc(nla::solver, *m_solver.get(), m.limit()); + m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit()); for (auto const& _s : m_scopes) { (void)_s; 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; } } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4b4a453c8..66736bd3f 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -59,7 +59,7 @@ def_module_params(module_name='smt', ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), - ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), + ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'), ('arith.nl.order', BOOL, True, 'run order lemmas'), ('arith.nl.expp', BOOL, False, 'expensive patching'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c822b7caf..db12e852a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -267,7 +267,7 @@ class theory_lra::imp { void ensure_nla() { if (!m_nla) { - m_nla = alloc(nla::solver, *m_solver.get(), m.limit()); + m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit()); for (auto const& _s : m_scopes) { (void)_s; m_nla->push(); @@ -277,24 +277,6 @@ class theory_lra::imp { return ctx().is_relevant(th.get_enode(u)); }; m_nla->set_relevant(is_relevant); - 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; } }