mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

add a parameter for debugging throttling

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-20 12:32:02 -07:00
parent e66113d4c7
commit 71289d8c48
3 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_order_lemmas.cpp
View file

@ -96,6 +96,10 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int
} }
bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // todo - remove debug location! bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // todo - remove debug location!
// Check if throttling is enabled
if (!c().params().arith_nl_trl())
return false;
// Check if this monic has already been processed using its variable ID // Check if this monic has already been processed using its variable ID
if (m_processed_monics.contains(ac.var())) { if (m_processed_monics.contains(ac.var())) {
TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";); TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";);

4
src/math/lp/nla_tangent_lemmas.cpp
View file

@ -200,6 +200,10 @@ void tangents::tangent_lemma() {
} }
bool tangents::throttle_plane(unsigned var, bool below, std::string const & debug_location) { bool tangents::throttle_plane(unsigned var, bool below, std::string const & debug_location) {
// Check if throttling is enabled
if (!c().params().arith_nl_trl())
return false;
tangent_key key(var, below); tangent_key key(var, below);
// Check if this (var, below) pair has already been processed // Check if this (var, below) pair has already been processed

1
src/params/smt_params_helper.pyg
View file

@ -65,6 +65,7 @@ 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.trl', BOOL, True, 'throttle repeated lemmas'),
('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'),