mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 19:32:04 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-18 13:59:45 -08:00
parent 469f618742
commit 98bfbc2d62
2 changed files with 6 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/dd_pdd.cpp
View file

@ -441,7 +441,7 @@ namespace dd {
pdd_manager::PDD pdd_manager::make_node(unsigned lvl, PDD l, PDD h) { pdd_manager::PDD pdd_manager::make_node(unsigned lvl, PDD l, PDD h) {
m_is_new_node = false; m_is_new_node = false;
if (is_zero(h)) return l; if (is_zero(h)) return l;
SASSERT(is_val(l) || level(l) <= lvl); SASSERT(is_val(l) || level(l) < lvl);
SASSERT(is_val(h) || level(h) <= lvl); SASSERT(is_val(h) || level(h) <= lvl);
pdd_node n(lvl, l, h, tree_size(l) + tree_size(h) + 1); pdd_node n(lvl, l, h, tree_size(l) + tree_size(h) + 1);
return insert_node(n); return insert_node(n);
@ -706,7 +706,7 @@ namespace dd {
PDD lo = n.m_lo; PDD lo = n.m_lo;
PDD hi = n.m_hi; PDD hi = n.m_hi;
if (hi == 0) continue; // it is a value if (hi == 0) continue; // it is a value
ok &= is_val(lo) || level(lo) <= lvl; ok &= is_val(lo) || level(lo) < lvl;
ok &= is_val(hi) || level(hi) <= lvl; ok &= is_val(hi) || level(hi) <= lvl;
ok &= is_val(lo) || !m_nodes[lo].is_internal(); ok &= is_val(lo) || !m_nodes[lo].is_internal();
ok &= is_val(hi) || !m_nodes[hi].is_internal(); ok &= is_val(hi) || !m_nodes[hi].is_internal();

13
src/math/grobner/pdd_grobner.cpp
View file

@ -72,16 +72,12 @@ namespace dd {
grobner::equation* grobner::pick_next() { grobner::equation* grobner::pick_next() {
equation* eq = nullptr; equation* eq = nullptr;
ptr_buffer<equation> to_delete;
for (auto* curr : m_to_simplify) { for (auto* curr : m_to_simplify) {
if (!eq|| is_simpler(*curr, *eq)) { if (!eq || is_simpler(*curr, *eq)) {
eq = curr; eq = curr;
} }
} }
for (auto* e : to_delete) if (eq) m_to_simplify.erase(eq);
del_equation(e);
if (eq)
m_to_simplify.erase(eq);
return eq; return eq;
} }
@ -174,10 +170,9 @@ namespace dd {
if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return; if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return;
m_stats.m_superposed++; m_stats.m_superposed++;
if (r.is_zero()) return; if (r.is_zero()) return;
unsigned idx = m_equations.size(); equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size());
equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), idx);
update_stats_max_degree_and_size(*eq); update_stats_max_degree_and_size(*eq);
if (r.is_val()) set_conflict(); check_conflict(*eq);
m_to_simplify.insert(eq); m_to_simplify.insert(eq);
} }