From 0ad2b54404de8e733766e5f4dbee68ada5f2921d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Nov 2022 13:08:31 -0800 Subject: [PATCH] fingers starting on xor_gaussian.cpp Signed-off-by: Nikolaj Bjorner --- src/sat/smt/xor_gaussian.cpp | 51 ++++++++++++++++++------------------ 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index 7d608f176..bf7d214e0 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/src/sat/smt/xor_gaussian.cpp @@ -66,33 +66,34 @@ void PackedRow::get_reason( PackedRow& tmp_col2, literal prop) { tmp_col2.set_and(*this, cols_vals); - for (int i = 0; i < size; i++) - if (mp[i]) { - int64_t tmp = mp[i]; - unsigned long at; - at = scan_fwd_64b(tmp); - int extra = 0; - while (at != 0) { - unsigned col = extra + at - 1 + i * 64; - SASSERT(operator[](col) == 1); - const unsigned var = col_to_var[col]; - if (var == prop.var()) { - tmp_clause.push_back(prop); - std::swap(tmp_clause[0], tmp_clause.back()); - } - else { - bool val_bool = tmp_col2[col]; // NSB: double check if z3 use of sign is compatible - tmp_clause.push_back(sat::literal(var, val_bool)); - } - - extra += at; - if (extra == 64) - break; - - tmp >>= at; - at = scan_fwd_64b(tmp); + for (int i = 0; i < size; i++) { + if (!mp[i]) + continue; + int64_t tmp = mp[i]; + unsigned long at; + at = scan_fwd_64b(tmp); + int extra = 0; + while (at != 0) { + unsigned col = extra + at - 1 + i * 64; + SASSERT(operator[](col) == 1); + const unsigned var = col_to_var[col]; + if (var == prop.var()) { + tmp_clause.push_back(prop); + std::swap(tmp_clause[0], tmp_clause.back()); } + else { + bool val_bool = tmp_col2[col]; // NSB: double check if z3 use of sign is compatible + tmp_clause.push_back(sat::literal(var, val_bool)); + } + + extra += at; + if (extra == 64) + break; + + tmp >>= at; + at = scan_fwd_64b(tmp); } + } } gret PackedRow::propGause(