mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update stats in check_pdd_eq()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
407c8a60db
commit
9ae9877353
|
@ -799,6 +799,7 @@ namespace dd {
|
|||
st.update("superposed", m_stats.m_superposed);
|
||||
st.update("degree", m_stats.m_max_expr_degree);
|
||||
st.update("size", m_stats.m_max_expr_size);
|
||||
st.update("conflicts", m_stats.m_conflicts);
|
||||
}
|
||||
|
||||
std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
|
||||
|
|
|
@ -37,6 +37,7 @@ public:
|
|||
unsigned m_max_expr_degree;
|
||||
unsigned m_superposed;
|
||||
unsigned m_compute_steps;
|
||||
unsigned m_conflicts;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
stats() { reset(); }
|
||||
};
|
||||
|
|
|
@ -1450,6 +1450,7 @@ void core::check_pdd_eq(const dd::grobner::equation* e) {
|
|||
current_expl().add(e);
|
||||
};
|
||||
di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f);
|
||||
m_pdd_grobner.get_stats().m_conflicts++;
|
||||
}
|
||||
|
||||
void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
|
||||
|
|
Loading…
Reference in a new issue