mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

Some code cleanup

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-05 07:42:22 +01:00
parent d2f3981d06
commit e4d3b4dcc5
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/sat/smt/xor_gaussian.cpp
View file

@ -64,12 +64,12 @@ void PackedRow::get_reason(
if (!mp[i]) if (!mp[i])
continue; continue;
int64_t tmp = mp[i]; int64_t tmp = mp[i];
unsigned long at; int at;
at = scan_fwd_64b(tmp); at = scan_fwd_64b(tmp);
int extra = 0; int extra = 0;
while (at != 0) { while (at != 0) {
unsigned col = extra + at - 1 + i * 64; unsigned col = extra + (at - 1) + i * 64;
SASSERT(operator[](col) == 1); SASSERT((*this)[col] == 1);
unsigned var = col_to_var[col]; unsigned var = col_to_var[col];
if (var == prop.var()) { if (var == prop.var()) {
tmp_clause.push_back(prop); tmp_clause.push_back(prop);
@ -108,7 +108,7 @@ gret PackedRow::propGause(
if (!tmp_col.mp[i]) if (!tmp_col.mp[i])
continue; continue;
int64_t tmp = tmp_col.mp[i]; int64_t tmp = tmp_col.mp[i];
unsigned long at; int at;
at = scan_fwd_64b(tmp); at = scan_fwd_64b(tmp);
int extra = 0; int extra = 0;
while (at != 0) { while (at != 0) {
@ -143,14 +143,17 @@ gret PackedRow::propGause(
return gret::confl; return gret::confl;
} }
for (int i = 0; i < size; i++) if (tmp_col.mp[i]) { for (int i = 0; i < size; i++) {
if (!tmp_col.mp[i])
continue;
int at = scan_fwd_64b(tmp_col.mp[i]); int at = scan_fwd_64b(tmp_col.mp[i]);
// found prop // found prop
unsigned col = at - 1 + i * 64; unsigned col = (at - 1) + i * 64;
SASSERT(tmp_col[col] == 1); SASSERT(tmp_col[col] == 1);
unsigned var = column_to_var[col]; unsigned var = column_to_var[col];
ret_lit_prop = literal(var, 1 == pop_t % 2); ret_lit_prop = literal(var,pop_t % 2);
return gret::prop; return gret::prop;
} }