mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 15:37:58 +00:00
Code Activity

Fixed build

Browse source
This commit is contained in:
CEisenhofer 2022-11-14 14:25:27 +01:00
parent 51ea347a4a
commit 1a5231fbf2
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/xor_solver.cpp
View file

@ -300,7 +300,7 @@ namespace xr {
xors[j++] = x; xors[j++] = x;
} }
else { else {
for (const auto& v : x.m_clash_vars) for (const bool_var& v : x.m_clash_vars)
m_removed_xorclauses_clash_vars.insert(v); m_removed_xorclauses_clash_vars.insert(v);
} }
} }
@ -317,14 +317,14 @@ namespace xr {
bool solver::clean_one_xor(xor_clause& x) { bool solver::clean_one_xor(xor_clause& x) {
unsigned j = 0; unsigned j = 0;
for (auto const& v : x.m_clash_vars) for (const bool_var & v : x.m_clash_vars)
if (s().value(v) == l_undef) if (s().value(v) == l_undef)
x.m_clash_vars[j++] = v; x.m_clash_vars[j++] = v;
x.m_clash_vars.shrink(j); x.m_clash_vars.shrink(j);
j = 0; j = 0;
for (auto const& v : x) { for (const bool_var& v : x) {
if (s().value(v) != l_undef) if (s().value(v) != l_undef)
x.m_rhs ^= s().value(v) == l_true; x.m_rhs ^= s().value(v) == l_true;
else else
@ -348,9 +348,9 @@ namespace xr {
return false; return false;
} }
case 2: { case 2: {
sat::literal_vector vec(x.size()); literal_vector vec(x.size());
for (const auto& v : x.m_vars) for (const auto& v : x.m_vars)
vec.push_back(sat::literal(v)); vec.push_back(literal(v));
add_xor_clause(vec, x.m_rhs, true); add_xor_clause(vec, x.m_rhs, true);
return false; return false;
} }
@ -590,7 +590,7 @@ namespace xr {
const auto& ws = s().get_wlist(i); const auto& ws = s().get_wlist(i);
for (const auto& w: ws) { for (const auto& w: ws) {
if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned()) { if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned()) {
sat::bool_var v = w.get_literal().var(); bool_var v = w.get_literal().var();
s().mark_visited(v); s().mark_visited(v);
} }
} }
@ -646,7 +646,7 @@ namespace xr {
} }
} }
SASSERT(at == 2); SASSERT(at == 2);
ws.resize(i2); ws.shrink(i2);
xor_clause& x0 = xors[indexes[0]]; xor_clause& x0 = xors[indexes[0]];
xor_clause& x1 = xors[indexes[1]]; xor_clause& x1 = xors[indexes[1]];
@ -704,7 +704,7 @@ namespace xr {
changed = true; changed = true;
xors.push_back(x_new); xors.push_back(x_new);
for (bool_var v2 : x_new) { for (bool_var v2 : x_new) {
sat::literal l(v2, false); literal l(v2, false);
watch_neg_literal(l, xors.size() - 1); watch_neg_literal(l, xors.size() - 1);
SASSERT(m_occ_cnt[l.var()] >= 1); SASSERT(m_occ_cnt[l.var()] >= 1);
if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) { if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) {