mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

add stats for throttling

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-26 13:55:04 -07:00 • committed by Lev Nachmanson
parent 899677e626
commit 2b6c73af82
4 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,6 +136,7 @@ struct statistics {
unsigned m_dio_rewrite_conflicts = 0; unsigned m_dio_rewrite_conflicts = 0;
unsigned m_bounds_tightening_conflicts = 0; unsigned m_bounds_tightening_conflicts = 0;
unsigned m_bounds_tightenings = 0; unsigned m_bounds_tightenings = 0;
unsigned m_nla_throttled_lemmas = 0;
::statistics m_st = {}; ::statistics m_st = {};
void reset() { void reset() {
@ -173,6 +174,7 @@ struct statistics {
st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_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-tightening-conflicts", m_bounds_tightening_conflicts);
st.update("arith-bounds-tightenings", m_bounds_tightenings); st.update("arith-bounds-tightenings", m_bounds_tightenings);
st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas);
st.copy(m_st); st.copy(m_st);
} }
}; };

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

@ -39,7 +39,8 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_emons(m_evars), m_emons(m_evars),
m_use_nra_model(false), m_use_nra_model(false),
m_nra(s, m_nra_lim, *this), m_nra(s, m_nra_lim, *this),
m_throttle(lra.trail()) { m_throttle(lra.trail(),
lra.settings().stats()) {
m_nlsat_delay_bound = lp_settings().nlsat_delay(); m_nlsat_delay_bound = lp_settings().nlsat_delay();
m_throttle.set_enabled(m_params.arith_nl_thrl()); m_throttle.set_enabled(m_params.arith_nl_thrl());
lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {

1
src/math/lp/nla_throttle.cpp
View file

@ -76,6 +76,7 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpv
bool nla_throttle::insert_new_impl(const signature& sig) { bool nla_throttle::insert_new_impl(const signature& sig) {
if (m_seen.contains(sig)) { if (m_seen.contains(sig)) {
TRACE(nla_solver, tout << "throttled lemma generation\n";); TRACE(nla_solver, tout << "throttled lemma generation\n";);
m_stats.m_nla_throttled_lemmas++;
return true; // Already seen, throttle return true; // Already seen, throttle
} }

4
src/math/lp/nla_throttle.h
View file

@ -7,6 +7,7 @@
--*/ --*/
#pragma once #pragma once
#include "math/lp/nla_defs.h" #include "math/lp/nla_defs.h"
#include "math/lp/lp_settings.h"
#include "util/hashtable.h" #include "util/hashtable.h"
#include "util/trail.h" #include "util/trail.h"
#include <cstring> #include <cstring>
@ -47,10 +48,11 @@ private:
hashtable<signature, signature_hash, default_eq<signature>> m_seen; hashtable<signature, signature_hash, default_eq<signature>> m_seen;
trail_stack& m_trail; trail_stack& m_trail;
lp::statistics& m_stats;
bool m_enabled = true; bool m_enabled = true;
public: public:
nla_throttle(trail_stack& trail) : m_trail(trail) {} nla_throttle(trail_stack& trail, lp::statistics& stats) : m_trail(trail), m_stats(stats) {}
void set_enabled(bool enabled) { m_enabled = enabled; } void set_enabled(bool enabled) { m_enabled = enabled; }
bool enabled() const { return m_enabled; } bool enabled() const { return m_enabled; }