From 919f687df6266a8cf52ecef1e9d0839c7c89ac2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Mar 2020 01:38:29 -0700 Subject: [PATCH] expose settings, not all of core Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 2 +- src/math/lp/nla_core.h | 1 - src/math/lp/nla_settings.h | 5 ++++- src/math/lp/nla_solver.h | 2 +- src/smt/theory_lra.cpp | 28 ++++++++++++++-------------- 5 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 71b5f6f7a..41d8d1dba 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1386,7 +1386,7 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const void core::run_grobner() { - unsigned& quota = m_grobner_quota; + unsigned& quota = m_nla_settings.grobner_quota(); if (quota == 1) { return; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 633518be5..4acb40f21 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -95,7 +95,6 @@ private: mutable lp::int_set m_active_var_set; lp::int_set m_rows; public: - unsigned m_grobner_quota; reslimit m_reslim; diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 418c23599..0baab2d38 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -38,6 +38,7 @@ class nla_settings { unsigned m_grobner_expr_degree_growth; unsigned m_grobner_max_simplified; unsigned m_grobner_number_of_conflicts_to_report; + unsigned m_grobner_quota; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -47,7 +48,8 @@ public: m_horner_subs_fixed(2), m_run_grobner(true), m_grobner_row_length_limit(50), - m_grobner_subs_fixed(false) + m_grobner_subs_fixed(false), + m_grobner_quota(0) {} unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;} unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;} @@ -90,6 +92,7 @@ public: 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; } }; } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 855a2e84d..cad590dde 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -38,7 +38,7 @@ public: solver(lp::lar_solver& s); ~solver(); - core& get_core() { return *m_core; } + nla_settings& settings() { return m_core->m_nla_settings; } void push(); void pop(unsigned scopes); bool need_check(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e7e8a0a4b..ecfeabd4a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -450,20 +450,20 @@ class theory_lra::imp { m_nla->push(); } smt_params_helper prms(ctx().get_params()); - m_nla->get_core().m_nla_settings.run_order() = prms.arith_nl_order(); - m_nla->get_core().m_nla_settings.run_tangents() = prms.arith_nl_tangents(); - m_nla->get_core().m_nla_settings.run_horner() = prms.arith_nl_horner(); - m_nla->get_core().m_nla_settings.horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); - m_nla->get_core().m_nla_settings.horner_frequency() = prms.arith_nl_horner_frequency(); - m_nla->get_core().m_nla_settings.horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); - m_nla->get_core().m_nla_settings.run_grobner() = prms.arith_nl_grobner(); - m_nla->get_core().m_nla_settings.grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); - m_nla->get_core().m_nla_settings.grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); - m_nla->get_core().m_nla_settings.grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); - m_nla->get_core().m_nla_settings.grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); - m_nla->get_core().m_nla_settings.grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); - m_nla->get_core().m_nla_settings.grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); - m_nla->get_core().m_grobner_quota = prms.arith_nl_gr_q(); + 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().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(); } }