mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

move nla stats to nla_core

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-15 12:58:34 -07:00
parent 82fd2a062d
commit 01279582ff
5 changed files with 34 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/nla_core.cpp
View file

@ -1474,10 +1474,18 @@ lbool core::check(vector<lemma>& 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<unsigned>(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

12
src/math/lp/nla_core.h
View file

@ -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<emonics> 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 {

4
src/math/lp/nla_solver.cpp
View file

@ -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);
}
}

1
src/math/lp/nla_solver.h
View file

@ -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);
};
}

11
src/smt/theory_lra.cpp
View file

@ -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<unsigned>(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);