mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

throttle tangent plane lemmas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-20 07:25:56 -07:00
parent 740c6945c6
commit 521f6a6543
4 changed files with 69 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -8,6 +8,8 @@
--*/
#include "math/lp/nla_tangent_lemmas.h"
#include "math/lp/nla_core.h"
#include "util/trail.h"
#include <iostream>
namespace nla {
@ -70,6 +72,10 @@ private:
}
void generate_plane(const point & pl) {
// Throttle plane generation based on m_xy.var() and m_below
if (m_tang.throttle_plane(m_j, m_below, std::string(__FILE__) + "," + std::to_string(__LINE__)))
return;
new_lemma lemma(c(), "generate tangent plane");
c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x);
c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y);
@ -193,5 +199,20 @@ void tangents::tangent_lemma() {
}
}
bool tangents::throttle_plane(unsigned var, bool below, std::string const & debug_location) {
tangent_key key(var, below);
// Check if this (var, below) pair has already been processed
if (m_processed_planes.contains(key)) {
std::cout << "throttled plane at " << debug_location << " for var=" << var << ", below=" << below << "\n";
return true;
}
// Mark this (var, below) pair as processed and add to trail for backtracking
m_processed_planes.insert(key);
c().trail().push(insert_map(m_processed_planes, key));
return false;
}
}