From 01279582ff92b88746b7af13939c4767355b6f3b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 15 May 2020 12:58:34 -0700 Subject: [PATCH] move nla stats to nla_core Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 17 ++++++++++++++++- src/math/lp/nla_core.h | 12 ++++++++++++ src/math/lp/nla_solver.cpp | 4 ++++ src/math/lp/nla_solver.h | 1 + src/smt/theory_lra.cpp | 11 +---------- 5 files changed, 34 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 0a3da1a64..3120ee43e 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1474,10 +1474,18 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } - if (l_vec.empty() && !done() && m_nla_settings.run_nra()) + if (l_vec.empty() && !done() && m_nla_settings.run_nra()) { ret = m_nra.check(); + m_stats.m_nra_calls ++; + } + if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) ret = l_false; + + m_stats.m_nla_lemmas += l_vec.size(); + for (const auto& l : l_vec) + m_stats.m_nla_explanations += static_cast(l.expl().size()); + TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";); IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());}); @@ -1861,4 +1869,11 @@ bool core::influences_nl_var(lpvar j) const { return false; } +void core::collect_statistics(::statistics & st) { + st.update("arith-nla-explanations", m_stats.m_nla_explanations); + st.update("arith-nla-lemmas", m_stats.m_nla_lemmas); + st.update("arith-nra-calls", m_stats.m_nra_calls); +} + + } // end of nla diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fc303d8b1..9660b08a0 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -139,6 +139,17 @@ struct pp_factorization { }; class core { + struct stats { + unsigned m_nla_explanations; + unsigned m_nla_lemmas; + unsigned m_nra_calls; + unsigned m_assume_eqs; + stats() { reset(); } + void reset() { + memset(this, 0, sizeof(*this)); + } + }; + stats m_stats; friend class new_lemma; public: var_eqs m_evars; @@ -465,6 +476,7 @@ public: bool has_real(const monic& m) const; void set_use_nra_model(bool m) { m_use_nra_model = m; } bool use_nra_model() const { return m_use_nra_model; } + void collect_statistics(::statistics&); }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 21c092efb..0bd54a77e 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -68,4 +68,8 @@ nlsat::anum const& solver::am_value(lp::var_index v) const { return m_core->m_nra.value(v); } +void solver::collect_statistics(::statistics & st) { + m_core->collect_statistics(st); +} + } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 42231a4ee..0754a4970 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -39,5 +39,6 @@ public: core& get_core(); nlsat::anum_manager& am(); nlsat::anum const& am_value(lp::var_index v) const; + void collect_statistics(::statistics & st); }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bbb16723b..573514d2e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -123,9 +123,6 @@ struct stats { unsigned m_bound_propagations2; unsigned m_assert_diseq; unsigned m_gomory_cuts; - unsigned m_nla_explanations; - unsigned m_nla_lemmas; - unsigned m_nra_calls; unsigned m_assume_eqs; unsigned m_branch; stats() { reset(); } @@ -2128,7 +2125,6 @@ public: void false_case_of_check_nla(const nla::lemma & l) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); - m_stats.m_nla_explanations += static_cast(l.expl().size()); literal_vector core; for (auto const& ineq : m_lemma.ineqs()) { bool is_lower = true, pos = true, is_eq = false; @@ -2161,11 +2157,8 @@ public: lbool check_nla_continue() { m_a1 = nullptr; m_a2 = nullptr; lbool r = m_nla->check(m_nla_lemma_vector); - if (use_nra_model()) m_stats.m_nra_calls ++; - switch (r) { case l_false: { - m_stats.m_nla_lemmas += m_nla_lemma_vector.size(); for (const nla::lemma & l : m_nla_lemma_vector) { false_case_of_check_nla(l); } @@ -3856,9 +3849,7 @@ public: st.update("arith-horner-cross-nested-forms", lp().settings().stats().m_cross_nested_forms); st.update("arith-grobner-calls", lp().settings().stats().m_grobner_calls); st.update("arith-grobner-conflicts", lp().settings().stats().m_grobner_conflicts); - st.update("arith-nla-explanations", m_stats.m_nla_explanations); - st.update("arith-nla-lemmas", m_stats.m_nla_lemmas); - st.update("arith-nra-calls", m_stats.m_nra_calls); + if (m_nla) m_nla->collect_statistics(st); st.update("arith-gomory-cuts", m_stats.m_gomory_cuts); st.update("arith-assume-eqs", m_stats.m_assume_eqs); st.update("arith-branch", m_stats.m_branch);