From 4ecb61aeaa29984eb23cd62e9491bd3fa447b0f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Jul 2022 11:12:12 -0700 Subject: [PATCH] neatify Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 3c50076daf2..b8946ebf698 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1330,30 +1330,19 @@ namespace dd { auto merge = [&](unsigned_vector& lo_vars, unsigned_vector& hi_vars) { unsigned ir = 0, jr = 0; for (unsigned i = 0, j = 0; i < lo_vars.size() || j < hi_vars.size(); ) { - if (i == lo_vars.size()) { + if (i == lo_vars.size()) hi_vars[jr++] = hi_vars[j++]; - continue; - } - if (j == hi_vars.size()) { + else if (j == hi_vars.size()) lo_vars[ir++] = lo_vars[i++]; - continue; - } - if (lo_vars[i] == hi_vars[j]) { + else if (lo_vars[i] == hi_vars[j]) { lo_and_hi.push_back(lo_vars[i]); ++i; ++j; - continue; } - unsigned lvl_lo = m.m_var2level[lo_vars[i]]; - unsigned lvl_hi = m.m_var2level[hi_vars[j]]; - if (lvl_lo > lvl_hi) { + else if (m.m_var2level[lo_vars[i]] > m.m_var2level[hi_vars[j]]) hi_vars[jr++] = hi_vars[j++]; - continue; - } - else { + else lo_vars[ir++] = lo_vars[i++]; - continue; - } } lo_vars.shrink(ir); hi_vars.shrink(jr);