mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-04 01:15:15 +00:00
Code Activity

throttle lemmas in nla_solver untested

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-25 17:27:53 -07:00 • committed by Lev Nachmanson
parent 46319156b8
commit 5caa7f1a29
9 changed files with 156 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/math/lp/nla_monotone_lemmas.cpp
View file

@ -7,10 +7,30 @@
--*/
#include "math/lp/nla_basics_lemmas.h"
#include "math/lp/nla_core.h"
#include "util/trail.h"
namespace nla {
monotone::monotone(core * c) : common(c) {}
bool monotone::throttle_monotone(const monic& m, bool is_lt, const std::string& debug_location) {
// Check if throttling is enabled
if (!c().params().arith_nl_thrl())
return false;
// Create the key for this specific monotonicity_lemma invocation
monotone_key key(m.var(), is_lt);
// Check if this combination has already been processed
if (m_processed_monotone.contains(key)) {
TRACE(nla_solver, tout << "throttled monotonicity_lemma at " << debug_location << "\n";);
return true;
}
// Mark this combination as processed and add to trail for backtracking
m_processed_monotone.insert(key);
c().trail().push(insert_map(m_processed_monotone, key));
return false;
}
void monotone::monotonicity_lemma() {
unsigned shift = random();
@ -29,7 +49,13 @@ void monotone::monotonicity_lemma(monic const& m) {
return;
const rational prod_val = abs(c().product_value(m));
const rational m_val = abs(var_val(m));
if (m_val < prod_val)
bool is_lt = m_val < prod_val;
// Check if this specific combination should be throttled
if (throttle_monotone(m, is_lt, __FUNCTION__))
return;
if (is_lt)
monotonicity_lemma_lt(m);
else if (m_val > prod_val)
monotonicity_lemma_gt(m);