mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity

separate the lower and upper bound root functions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-17 13:26:23 -07:00
parent 7479b0296f
commit 881d74278d
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/levelwise.cpp
View file

@ -402,9 +402,6 @@ namespace nlsat {
std::sort(m_rel.m_rfunc.begin(), m_rel.m_rfunc.end(), [&](root_function const& a, root_function const& b){ std::sort(m_rel.m_rfunc.begin(), m_rel.m_rfunc.end(), [&](root_function const& a, root_function const& b){
return m_am.lt(a.val, b.val); return m_am.lt(a.val, b.val);
}); });
if (m_rel.m_rfunc.size() >= 2) {
enable_trace("lws");
}
TRACE(lws, TRACE(lws,
if (m_rel.empty()) tout << "E is empty\n"; if (m_rel.empty()) tout << "E is empty\n";
else { tout << "E:\n"; else { tout << "E:\n";
@ -433,6 +430,11 @@ namespace nlsat {
if (is_set(u)) if (is_set(u))
for (unsigned j = u + 1; j < m_rel.m_rfunc.size(); j++) for (unsigned j = u + 1; j < m_rel.m_rfunc.size(); j++)
m_rel.add_pair(u, j); m_rel.add_pair(u, j);
if (is_set(l) && is_set(u)) {
SASSERT(l + 1 == u);
m_rel.add_pair(l, u);
}
} }
void fill_relation_pairs() { void fill_relation_pairs() {