From 79fefe5fb3c8518355a2f57f29ca8285075e0e2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2020 14:30:34 -0700 Subject: [PATCH] local Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_solver.cpp | 6 ++++++ src/math/lp/nla_solver.h | 3 ++- src/smt/theory_lra.cpp | 37 +++++++++++++++++++++---------------- 3 files changed, 29 insertions(+), 17 deletions(-) diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 4833ceb98..766b43b0c 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -58,4 +58,10 @@ bool solver::influences_nl_var(lpvar j) const { solver::~solver() { dealloc(m_core); } + +std::ostream& solver::display(std::ostream& out) const { + m_core->print_monics(out); + return out; +} + } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index cefce8c81..855a2e84d 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -38,12 +38,13 @@ public: solver(lp::lar_solver& s); ~solver(); - inline core * get_core() { return m_core; } + core& get_core() { return *m_core; } void push(); void pop(unsigned scopes); bool need_check(); lbool check(vector&); bool is_monic_var(lpvar) const; bool influences_nl_var(lpvar) const; + std::ostream& display(std::ostream& out) const; }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f8f448236..3c56127eb 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -450,21 +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->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(); } } @@ -1396,7 +1395,7 @@ public: th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); 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_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()))); }; if_trace_stream _ts(m, log); @@ -3743,6 +3742,12 @@ public: lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); } } + if (m_nla) { + m_nla->display(out); + } + if (m_nra) { + m_nra->display(out); + } unsigned nv = th.get_num_vars(); for (unsigned v = 0; v < nv; ++v) { if (!ctx().is_relevant(get_enode(v))) out << "irr: ";