mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 04:39:00 +00:00
Code Activity

categorize lp stats

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-29 17:05:59 -07:00
parent 06de5f422c
commit 91b4873b79
2 changed files with 34 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -103,7 +103,6 @@ struct statistics {
unsigned m_make_feasible = 0;
unsigned m_total_iterations = 0;
unsigned m_iters_with_no_cost_growing = 0;
unsigned m_num_factorizations = 0;
unsigned m_num_of_implied_bounds = 0;
unsigned m_need_to_solve_inf = 0;
unsigned m_max_cols = 0;
@ -137,44 +136,47 @@ struct statistics {
unsigned m_bounds_tightening_conflicts = 0;
unsigned m_bounds_tightenings = 0;
unsigned m_nla_throttled_lemmas = 0;
unsigned m_nla_bounds_lemmas = 0;
unsigned m_nla_bounds_propagations = 0;
::statistics m_st = {};
void reset() {
*this = statistics{};
}
void collect_statistics(::statistics& st) const {
st.update("arith-factorizations", m_num_factorizations);
st.update("arith-make-feasible", m_make_feasible);
st.update("arith-max-columns", m_max_cols);
st.update("arith-max-rows", m_max_rows);
st.update("arith-gcd-calls", m_gcd_calls);
st.update("arith-gcd-conflict", m_gcd_conflicts);
st.update("arith-cube-calls", m_cube_calls);
st.update("arith-cube-success", m_cube_success);
st.update("arith-patches", m_patches);
st.update("arith-patches-success", m_patches_success);
st.update("arith-hnf-calls", m_hnf_cutter_calls);
st.update("arith-hnf-cuts", m_hnf_cuts);
st.update("arith-gomory-cuts", m_gomory_cuts);
st.update("arith-horner-calls", m_horner_calls);
st.update("arith-horner-conflicts", m_horner_conflicts);
st.update("arith-horner-cross-nested-forms", m_cross_nested_forms);
st.update("arith-grobner-calls", m_grobner_calls);
st.update("arith-grobner-conflicts", m_grobner_conflicts);
st.update("arith-offset-eqs", m_offset_eqs);
st.update("arith-fixed-eqs", m_fixed_eqs);
st.update("arith-lp-make-feasible", m_make_feasible);
st.update("arith-lp-max-columns", m_max_cols);
st.update("arith-lp-max-rows", m_max_rows);
st.update("arith-lp-offset-eqs", m_offset_eqs);
st.update("arith-lp-fixed-eqs", m_fixed_eqs);
st.update("arith-lia-patches", m_patches);
st.update("arith-lia-patches-success", m_patches_success);
st.update("arith-lia-gcd-calls", m_gcd_calls);
st.update("arith-lia-gcd-conflict", m_gcd_conflicts);
st.update("arith-lia-cube-calls", m_cube_calls);
st.update("arith-lia-cube-success", m_cube_success);
st.update("arith-lia-hermite-calls", m_hnf_cutter_calls);
st.update("arith-lia-hermite-cuts", m_hnf_cuts);
st.update("arith-lia-gomory-cuts", m_gomory_cuts);
st.update("arith-lia-diophantine-calls", m_dio_calls);
st.update("arith-lia-diophantine-tighten-conflicts", m_dio_tighten_conflicts);
st.update("arith-lia-diophantine-rewrite-conflicts", m_dio_rewrite_conflicts);
st.update("arith-lia-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
st.update("arith-lia-bounds-tightenings", m_bounds_tightenings);
st.update("arith-nla-horner-calls", m_horner_calls);
st.update("arith-nla-horner-conflicts", m_horner_conflicts);
st.update("arith-nla-horner-cross-nested-forms", m_cross_nested_forms);
st.update("arith-nla-grobner-calls", m_grobner_calls);
st.update("arith-nla-grobner-conflicts", m_grobner_conflicts);
st.update("arith-nla-add-bounds", m_nla_add_bounds);
st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds);
st.update("arith-nla-propagate-eq", m_nla_propagate_eq);
st.update("arith-nla-lemmas", m_nla_lemmas);
st.update("arith-nra-calls", m_nra_calls);
st.update("arith-bounds-improvements", m_nla_bounds_improvements);
st.update("arith-dio-calls", m_dio_calls);
st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts);
st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
st.update("arith-bounds-tightenings", m_bounds_tightenings);
st.update("arith-nla-nra-calls", m_nra_calls);
st.update("arith-nla-bounds-improvements", m_nla_bounds_improvements);
st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas);
st.update("arith-nla-bounds-lemmas", m_nla_bounds_lemmas);
st.update("artih-nla-bounds-propagations", m_nla_bounds_propagations);
st.copy(m_st);
}
};

5
src/math/lp/monomial_bounds.cpp
View file

@ -378,6 +378,7 @@ namespace nla {
bool monomial_bounds::add_lemma() {
if (c().lra.get_status() != lp::lp_status::INFEASIBLE)
return false;
c().lp_settings().stats().m_nla_bounds_lemmas++;
lp::explanation exp;
c().lra.get_infeasibility_explanation(exp);
lemma_builder lemma(c(), "propagate fixed - infeasible lra");
@ -422,6 +423,7 @@ namespace nla {
TRACE(nla_solver, tout << "propagate fixed " << m << " = 0, fixed_to_zero = " << fixed_to_zero << "\n";);
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep);
c().lp_settings().stats().m_nla_bounds_propagations++;
// propagate fixed equality
auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), rational(0), exp);
@ -431,7 +433,7 @@ namespace nla {
auto* dep = explain_fixed(m, k);
TRACE(nla_solver, tout << "propagate fixed " << m << " = " << k << "\n";);
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
c().lp_settings().stats().m_nla_bounds_propagations++;
// propagate fixed equality
auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), k, exp);
@ -448,6 +450,7 @@ namespace nla {
if (k == 1) {
lp::explanation exp = get_explanation(dep);
c().lp_settings().stats().m_nla_bounds_propagations++;
c().add_equality(m.var(), w, exp);
}
}