diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 617801127..386ac8b9a 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -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! + // 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 if (m_processed_monics.contains(ac.var())) { TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 9405a7ac7..81ae9c83e 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -200,6 +200,10 @@ void tangents::tangent_lemma() { } 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); // Check if this (var, below) pair has already been processed diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index c1eb0148a..c30ba85b8 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -65,6 +65,7 @@ def_module_params(module_name='smt', ('arith.nl.order', BOOL, True, 'run order lemmas'), ('arith.nl.expp', BOOL, False, 'expensive patching'), ('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_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),