mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

add statistics on horner's heuristic

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-09 15:10:24 -07:00
parent 22e2ad6824
commit 5435942228
3 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/horner.cpp
View file

@ -72,6 +72,7 @@ bool horner::lemmas_on_expr(nex& e) {
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";); TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
conflict = m_intervals.check_interval_for_conflict_on_zero(i); conflict = m_intervals.check_interval_for_conflict_on_zero(i);
c().lp_settings().st().m_cross_nested_forms++;
m_intervals.reset(); // clean the memory allocated by the interval bound dependencies m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
return conflict; return conflict;
}, },
@ -94,7 +95,7 @@ void horner::horner_lemmas() {
TRACE("nla_solver", tout << "not generating horner lemmas\n";); TRACE("nla_solver", tout << "not generating horner lemmas\n";);
return; return;
} }
c().lp_settings().st().m_horner_calls++;
const auto& matrix = c().m_lar_solver.A_r(); const auto& matrix = c().m_lar_solver.A_r();
// choose only rows that depend on m_to_refine variables // choose only rows that depend on m_to_refine variables
std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
@ -112,9 +113,11 @@ void horner::horner_lemmas() {
unsigned sz = rows.size(); unsigned sz = rows.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
unsigned row_index = rows[(i + r) % sz]; unsigned row_index = rows[(i + r) % sz];
if (lemmas_on_row(matrix.m_rows[row_index])) if (lemmas_on_row(matrix.m_rows[row_index])) {
c().lp_settings().st().m_horner_conflicts++;
break; break;
} }
}
} }
typedef nla_expr<rational> nex; typedef nla_expr<rational> nex;

3
src/math/lp/lp_settings.h
View file

@ -107,6 +107,9 @@ struct stats {
unsigned m_hnf_cutter_calls; unsigned m_hnf_cutter_calls;
unsigned m_hnf_cuts; unsigned m_hnf_cuts;
unsigned m_nla_calls; unsigned m_nla_calls;
unsigned m_horner_calls;
unsigned m_horner_conflicts;
unsigned m_cross_nested_forms;
stats() { reset(); } stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
}; };

3
src/smt/theory_lra.cpp
View file

@ -3784,6 +3784,9 @@ public:
st.update("arith-patches", lp().settings().st().m_patches); st.update("arith-patches", lp().settings().st().m_patches);
st.update("arith-patches-success", lp().settings().st().m_patches_success); st.update("arith-patches-success", lp().settings().st().m_patches_success);
st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls); st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls);
st.update("horner-calls", lp().settings().st().m_horner_calls);
st.update("horner-conflicts", lp().settings().st().m_horner_conflicts);
st.update("horner-cross-nested-forms", lp().settings().st().m_cross_nested_forms);
st.update("nla-explanations", m_stats.m_nla_explanations); st.update("nla-explanations", m_stats.m_nla_explanations);
st.update("nla-lemmas", m_stats.m_nla_lemmas); st.update("nla-lemmas", m_stats.m_nla_lemmas);
} }