mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

remove the parameter for throttling nla lemmas

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-26 14:38:44 -07:00 • committed by Lev Nachmanson
parent 2b6c73af82
commit d717dae3ac
5 changed files with 1 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -42,7 +42,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_throttle(lra.trail(), m_throttle(lra.trail(),
lra.settings().stats()) { 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());
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) {
for (lpvar j : columns_with_changed_bounds) { for (lpvar j : columns_with_changed_bounds) {
if (is_monic_var(j)) if (is_monic_var(j))

1
src/math/lp/nla_core.h
View file

@ -436,7 +436,6 @@ public:
void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
void set_throttle_enabled(bool enabled) { m_throttle_enabled = enabled; m_throttle.set_enabled(enabled); }
bool throttle_enabled() const { return m_throttle_enabled; } bool throttle_enabled() const { return m_throttle_enabled; }
nla_throttle& throttle() { return m_throttle; } nla_throttle& throttle() { return m_throttle; }
const nla_throttle& throttle() const { return m_throttle; } const nla_throttle& throttle() const { return m_throttle; }

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

@ -11,7 +11,6 @@
namespace nla { namespace nla {
bool nla_throttle::insert_new(throttle_kind k, lpvar mvar, bool is_lt) { bool nla_throttle::insert_new(throttle_kind k, lpvar mvar, bool is_lt) {
if (!m_enabled) return false;
signature sig; signature sig;
sig.m_values[0] = static_cast<unsigned>(k); sig.m_values[0] = static_cast<unsigned>(k);
sig.m_values[1] = static_cast<unsigned>(mvar); sig.m_values[1] = static_cast<unsigned>(mvar);
@ -20,7 +19,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar mvar, bool is_lt) {
} }
bool nla_throttle::insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, int sign, int sy) { bool nla_throttle::insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, int sign, int sy) {
if (!m_enabled) return false;
signature sig; signature sig;
sig.m_values[0] = static_cast<unsigned>(k); sig.m_values[0] = static_cast<unsigned>(k);
sig.m_values[1] = static_cast<unsigned>(xy_var); sig.m_values[1] = static_cast<unsigned>(xy_var);
@ -33,7 +31,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, i
bool nla_throttle::insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rational& c_sign, lpvar c, bool nla_throttle::insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rational& c_sign, lpvar c,
lpvar bd_var, lpvar b_var, const rational& d_sign, lpvar d, llc ab_cmp) { lpvar bd_var, lpvar b_var, const rational& d_sign, lpvar d, llc ab_cmp) {
if (!m_enabled) return false;
signature sig; signature sig;
sig.m_values[0] = static_cast<unsigned>(k); sig.m_values[0] = static_cast<unsigned>(k);
sig.m_values[1] = static_cast<unsigned>(ac_var); sig.m_values[1] = static_cast<unsigned>(ac_var);
@ -50,7 +47,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rati
} }
bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below, int plane_type) { bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below, int plane_type) {
if (!m_enabled) return false;
signature sig; signature sig;
sig.m_values[0] = static_cast<unsigned>(k); sig.m_values[0] = static_cast<unsigned>(k);
sig.m_values[1] = static_cast<unsigned>(monic_var); sig.m_values[1] = static_cast<unsigned>(monic_var);
@ -62,7 +58,6 @@ bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpv
} }
bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below) { bool nla_throttle::insert_new(throttle_kind k, lpvar monic_var, lpvar x_var, lpvar y_var, bool below) {
if (!m_enabled) return false;
signature sig; signature sig;
sig.m_values[0] = static_cast<unsigned>(k); sig.m_values[0] = static_cast<unsigned>(k);
sig.m_values[1] = static_cast<unsigned>(monic_var); sig.m_values[1] = static_cast<unsigned>(monic_var);

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

@ -49,12 +49,10 @@ 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; lp::statistics& m_stats;
bool m_enabled = true;
public: public:
nla_throttle(trail_stack& trail, lp::statistics& stats) : m_trail(trail), m_stats(stats) {} nla_throttle(trail_stack& trail, lp::statistics& stats) : m_trail(trail), m_stats(stats) {}
void set_enabled(bool enabled) { m_enabled = enabled; }
bool enabled() const { return m_enabled; }
// Monotone lemma: mvar + is_lt // Monotone lemma: mvar + is_lt
bool insert_new(throttle_kind k, lpvar mvar, bool is_lt); bool insert_new(throttle_kind k, lpvar mvar, bool is_lt);

1
src/params/smt_params_helper.pyg
View file

@ -65,7 +65,6 @@ def_module_params(module_name='smt',
('arith.nl.order', BOOL, True, 'run order lemmas'), ('arith.nl.order', BOOL, True, 'run order lemmas'),
('arith.nl.expp', BOOL, False, 'expensive patching'), ('arith.nl.expp', BOOL, False, 'expensive patching'),
('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
('arith.nl.thrl', BOOL, True, 'throttle repeated lemmas - debug, remove later!!!'),
('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),