mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

instrument the tableau

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-25 12:11:07 -07:00
parent 09467ba677
commit 96cc58f67c
4 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/u_set.h
View file

@ -15,7 +15,7 @@ Author:
Revision History:
TBD use indexed_uint_set from src/util/uu_set.h,
TBD use indexed_uint_set from src/util/uint_set.h,
--*/
#pragma once

1
src/smt/theory_arith.h
View file

@ -49,6 +49,7 @@ namespace smt {
unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
unsigned m_nl_branching, m_nl_linear, m_nl_bounds, m_nl_cross_nested;
unsigned m_branch_infeasible_int, m_branch_infeasible_var;
unsigned m_tableau_max_rows, m_tableau_max_columns;
void reset() { memset(this, 0, sizeof(theory_arith_stats)); }
theory_arith_stats() { reset(); }

3
src/smt/theory_arith_core.h
View file

@ -258,6 +258,7 @@ namespace smt {
c_entry.m_row_id = r_id;
c_entry.m_row_idx = r_idx;
m_stats.m_tableau_max_columns = std::max(m_stats.m_tableau_max_columns, (unsigned)c_idx + 1);
}
/**
@ -832,6 +833,7 @@ namespace smt {
*/
template<typename Ext>
unsigned theory_arith<Ext>::mk_row() {
unsigned r;
if (m_dead_rows.empty()) {
r = m_rows.size();
@ -844,6 +846,7 @@ namespace smt {
m_in_to_check.assure_domain(r);
SASSERT(m_rows[r].size() == 0);
SASSERT(m_rows[r].num_entries() == 0);
m_stats.m_tableau_max_rows = std::max(m_stats.m_tableau_max_rows, m_rows.size());
return r;
}

2
src/smt/theory_arith_pp.h
View file

@ -48,6 +48,8 @@ namespace smt {
st.update("arith pseudo nonlinear", m_stats.m_nl_linear);
st.update("arith nonlinear bounds", m_stats.m_nl_bounds);
st.update("arith nonlinear horner", m_stats.m_nl_cross_nested);
st.update("arith tableau max rows", m_stats.m_tableau_max_rows);
st.update("arith tableau max columns", m_stats.m_tableau_max_columns);
m_arith_eq_adapter.collect_statistics(st);
}