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

fix new (and unused) function for extracting min parity of a polynomial

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-08 07:13:31 -08:00
parent acbd60799d
commit 28fb67219e
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -178,16 +178,16 @@ namespace dd {
r++, v /= 2; r++, v /= 2;
return r; return r;
} }
init_mark();
PDD q = p; PDD q = p;
while (!is_val(q)) m_todo.push_back(hi(q));
while (!is_val(q)) {
q = lo(q); q = lo(q);
m_todo.push_back(hi(q));
}
unsigned p2 = val(q).trailing_zeros(); unsigned p2 = val(q).trailing_zeros();
init_mark(); init_mark();
if (p2 == 0) while (p2 != 0 && !m_todo.empty()) {
return 0;
init_mark();
m_todo.push_back(hi(p));
while (!m_todo.empty() && p2 != 0) {
PDD r = m_todo.back(); PDD r = m_todo.back();
m_todo.pop_back(); m_todo.pop_back();
if (is_marked(r)) if (is_marked(r))