From 252a30e727e8c5cc290eea8d6deeba63f16ce4c2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 17 Aug 2023 18:44:27 -0700 Subject: [PATCH] use param_ref in nla_solver (#6862) * use param_ref in nla_solver Signed-off-by: Lev Nachmanson * add parameters Signed-off-by: Nikolaj Bjorner * add parameters Signed-off-by: Nikolaj Bjorner * replace nla_setting by command line parameters * delete nla_setting.h --------- Signed-off-by: Lev Nachmanson Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner --- package-lock.json | 27 ++-------------- src/math/lp/horner.cpp | 4 +-- src/math/lp/nla_common.cpp | 8 ++--- src/math/lp/nla_core.cpp | 11 ++++--- src/math/lp/nla_core.h | 15 ++++----- src/math/lp/nla_grobner.cpp | 36 ++++++++++++---------- src/math/lp/nla_grobner.h | 3 +- src/math/lp/nla_order_lemmas.cpp | 2 +- src/math/lp/nla_settings.h | 46 ---------------------------- src/math/lp/nla_solver.cpp | 7 ++--- src/math/lp/nla_solver.h | 4 +-- src/math/lp/nla_tangent_lemmas.cpp | 2 +- src/sat/smt/arith_internalize.cpp | 19 +----------- src/smt/params/smt_params_helper.pyg | 4 ++- src/smt/theory_lra.cpp | 19 +----------- src/test/lp/nla_solver_test.cpp | 24 +++++++-------- 16 files changed, 67 insertions(+), 164 deletions(-) delete mode 100644 src/math/lp/nla_settings.h diff --git a/package-lock.json b/package-lock.json index 4c22d5b85..ab471dfcd 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,27 +1,6 @@ { + "name": "z3", + "lockfileVersion": 3, "requires": true, - "lockfileVersion": 1, - "dependencies": { - "async-mutex": { - "version": "0.3.2", - "resolved": "https://registry.npmjs.org/async-mutex/-/async-mutex-0.3.2.tgz", - "integrity": "sha512-HuTK7E7MT7jZEh1P9GtRW9+aTWiDWWi9InbZ5hjxrnRa39KS4BW04+xLBhYNS2aXhHUIKZSw3gj4Pn1pj+qGAA==", - "requires": { - "tslib": "^2.3.1" - } - }, - "tslib": { - "version": "2.4.0", - "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.4.0.tgz", - "integrity": "sha512-d6xOpEDfsi2CZVlPQzGeux8XMwLT9hssAsaPYExaQMuYskwb+x1x7J371tWlbBdWHroy99KnVB6qIkUbs5X3UQ==" - }, - "z3-solver": { - "version": "4.9.0", - "resolved": "https://registry.npmjs.org/z3-solver/-/z3-solver-4.9.0.tgz", - "integrity": "sha512-clSV0uyHsfrO84pSbHxoqvmd5HgSG4CoSJG2f8U65hBVylbV6p/0svctQWee9W2fWo0IsxHYRjxz2Z85GT0LAA==", - "requires": { - "async-mutex": "^0.3.2" - } - } - } + "packages": {} } diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 51e2f533e..40f16d709 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 86ddb05b7..54f955760 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -21,10 +21,11 @@ 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), + m_params(p), m_tangents(this), m_basics(this), m_order(this), @@ -1428,7 +1429,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 || !params().arith_nl_expensive_patching()) { return; } NOT_IMPLEMENTED_YET(); @@ -1566,11 +1567,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() && 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++; } @@ -1590,7 +1591,7 @@ lbool core::check(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 9baa1b026..78f46bb41 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -22,12 +22,12 @@ #include "math/lp/nla_powers.h" #include "math/lp/nla_divisions.h" #include "math/lp/emonics.h" -#include "math/lp/nla_settings.h" #include "math/lp/nex.h" #include "math/lp/horner.h" #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; @@ -54,7 +54,6 @@ class core { friend struct tangents; friend class monotone; friend class powers; - friend struct nla_settings; friend class intervals; friend class horner; friend class solver; @@ -82,6 +81,7 @@ class core { lp::lar_solver& m_lar_solver; reslimit& m_reslim; + smt_params_helper m_params; std::function m_relevant; vector * m_lemma_vec; indexed_uint_set m_to_refine; @@ -93,8 +93,7 @@ class core { divisions m_divisions; intervals m_intervals; monomial_bounds m_monomial_bounds; - nla_settings m_nla_settings; - + horner m_horner; grobner m_grobner; emonics m_emons; @@ -113,7 +112,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); @@ -165,13 +164,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 % params().arith_nl_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 4c2f879cf..eefb07fac 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -24,8 +24,8 @@ namespace nla { common(c), 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_lar_solver(m_core.m_lar_solver), + m_quota(m_core.params().arith_nl_gr_q()) {} lp::lp_settings& grobner::lp_settings() { @@ -33,8 +33,10 @@ namespace nla { } void grobner::operator()() { - unsigned& quota = c().m_nla_settings.grobner_quota; - if (quota == 1) + if (m_quota == 0) + m_quota = c().params().arith_nl_gr_q(); + + if (m_quota == 1) return; lp_settings().stats().m_grobner_calls++; @@ -59,12 +61,14 @@ namespace nla { } - if (quota > 1) - quota--; + if (m_quota > 0) + --m_quota; - IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n"); + IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << m_quota << "\n"); IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream())); + + #if 0 // diagnostics: did we miss something vector eqs; @@ -239,11 +243,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. @@ -348,9 +352,9 @@ namespace nla { 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() > c().m_nla_settings.grobner_row_length_limit, + CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_grobner_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); @@ -373,12 +377,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_grobner.h b/src/math/lp/nla_grobner.h index ed3aa77db..f8e21d1a7 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -22,7 +22,8 @@ namespace nla { dd::pdd_manager m_pdd_manager; dd::solver m_solver; lp::lar_solver& m_lar_solver; - indexed_uint_set m_rows; + indexed_uint_set m_rows; + unsigned m_quota = 0; lp::lp_settings& lp_settings(); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 2cf5ac004..902e208fc 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 deleted file mode 100644 index ec11ea5b2..000000000 --- a/src/math/lp/nla_settings.h +++ /dev/null @@ -1,46 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Author: - - Lev Nachmanson (levnach) - ---*/ - -#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 bd0f1953c..0e6efd526 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -16,9 +16,6 @@ #include "math/polynomial/algebraic_numbers.h" namespace nla { - - nla_settings& solver::settings() { return m_core->m_nla_settings; } - void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) { m_core->add_monic(v, sz, vs); } @@ -57,8 +54,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 d04ff8e51..d61b0593b 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -13,7 +13,6 @@ Author: #include "util/params.h" #include "math/lp/lar_solver.h" #include "math/lp/monic.h" -#include "math/lp/nla_settings.h" #include "math/lp/nla_core.h" namespace nra { class solver; @@ -25,7 +24,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); @@ -34,7 +33,6 @@ namespace nla { void add_bounded_division(lpvar q, lpvar x, lpvar y); void check_bounded_divisions(vector&); void set_relevant(std::function& is_relevant); - nla_settings& settings(); void push(); void pop(unsigned scopes); bool need_check(); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 4ba9eeccc..56ebbfacc 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 65ed5ac42..9a4399b96 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -61,29 +61,12 @@ 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 2bb3d4197..f059dccb8 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -58,7 +58,8 @@ 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.expensive_patching', BOOL, False, 'use the expensive of monomials'), ('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'), @@ -67,6 +68,7 @@ def_module_params(module_name='smt', ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), ('arith.nl.horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), + ('arith.nl.grobner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'), ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'), ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 87de2d9e2..e134b13e2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -263,7 +263,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(); @@ -274,23 +274,6 @@ class theory_lra::imp { }; 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; } } diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 6e2e0336a..ce934e7ca 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -169,7 +169,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); nla.add_monic(lp_bde, v.size(), v.begin()); v.clear(); @@ -246,7 +246,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); nla.add_monic(lp_bde, v.size(), v.begin()); @@ -317,7 +317,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); create_abcde(nla, lp_a, @@ -379,7 +379,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial acd unsigned_vector vec; @@ -439,7 +439,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); create_abcde(nla, lp_a, @@ -514,7 +514,7 @@ void test_horner() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); vector v; v.push_back(a); v.push_back(b); nla.add_monic(lp_ab, v.size(), v.begin()); @@ -551,7 +551,7 @@ void test_basic_sign_lemma() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial bde vector vec; @@ -626,7 +626,7 @@ void test_order_lemma_params(bool var_equiv, int sign) { reslimit l; params_ref p; - solver nla(s,l); + solver nla(s,p,l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -757,7 +757,7 @@ void test_monotone_lemma() { reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -814,7 +814,7 @@ void test_tangent_lemma_rat() { s_set_column_value_test(s, lp_ab, v); reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -841,7 +841,7 @@ void test_tangent_lemma_reg() { s_set_column_value_test(s, lp_ab, rational(11)); reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -885,7 +885,7 @@ void test_tangent_lemma_equiv() { s_set_column_value_test(s, lp_a, - s.get_column_value(lp_k)); reslimit l; params_ref p; - solver nla(s, l); + solver nla(s, p, l); // create monomial ab vector vec; vec.push_back(lp_a);