mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

Removed debug output

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-17 15:42:14 +01:00
parent 3f8edb9aac
commit d976251390
2 changed files with 9 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/op_constraint.cpp
View file

@ -544,21 +544,12 @@ namespace polysat {
bool rb = rv.val().get_bit(i); bool rb = rv.val().get_bit(i);
if (rb == (pb && qb)) if (rb == (pb && qb))
continue; continue;
if (pb && qb && !rb) { if (pb && qb && !rb)
verbose_stream() << "Conflict propagation " << pv << " (" << p() << ") & " << qv << " (" << q() << ") = " << bitwise_and(pv.val(), qv.val()) << " (" << r() << ")\n";
verbose_stream() << "1 & 1 = 0 bit " << i << "\n";
s.add_clause(s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true)); s.add_clause(s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true));
} else if (!pb && rb)
else if (!pb && rb) {
verbose_stream() << "Conflict propagation " << pv << " (" << p() << ") & " << qv << " (" << q() << ") = " << bitwise_and(pv.val(), qv.val()) << " (" << r() << ")\n";
verbose_stream() << "0 & ? = 1 bit " << i << "\n";
s.add_clause(s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true)); s.add_clause(s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true));
} else if (!qb && rb)
else if (!qb && rb) {
verbose_stream() << "Conflict propagation " << pv << " (" << p() << ") & " << qv << " (" << q() << ") = " << bitwise_and(pv.val(), qv.val()) << " (" << r() << ")\n";
verbose_stream() << "? & 0 = 1 bit " << i << "\n";
s.add_clause(s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true)); s.add_clause(s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true));
}
else else
UNREACHABLE(); UNREACHABLE();
} }

16
src/math/polysat/viable.cpp
View file

@ -898,15 +898,11 @@ namespace {
vector<std::pair<entry*, trailing_bits>> postponed; vector<std::pair<entry*, trailing_bits>> postponed;
auto add_entry = [&builder](entry* e) { auto add_entry = [&builder](entry* e) {
for (const auto& sc : e->side_cond) { for (const auto& sc : e->side_cond)
builder.insert_eval(~sc); builder.insert_eval(~sc);
LOG("Side cond: " << sc);
}
SASSERT(e->src.size() == 1); SASSERT(e->src.size() == 1);
for (const auto& src : e->src) { for (const auto& src : e->src)
builder.insert_eval(~src); builder.insert_eval(~src);
LOG("Adding to core: " << e->src);
}
}; };
auto add_entry_list = [add_entry](const ptr_vector<entry>& list) { auto add_entry_list = [add_entry](const ptr_vector<entry>& list) {
@ -931,7 +927,7 @@ namespace {
fixed[bit.position] = bit.positive ? l_true : l_false; fixed[bit.position] = bit.positive ? l_true : l_false;
//verbose_stream() << "Setting bit " << bit.position << " to " << bit.positive << " because of " << e->src << "\n"; //verbose_stream() << "Setting bit " << bit.position << " to " << bit.positive << " because of " << e->src << "\n";
if (prev != l_undef && fixed[bit.position] != prev) { if (prev != l_undef && fixed[bit.position] != prev) {
verbose_stream() << "Bit conflicting " << e->src << " with " << justifications[bit.position][0]->src << "\n"; LOG("Bit conflicting " << e->src << " with " << justifications[bit.position][0]->src);
if (add_conflict) { if (add_conflict) {
add_entry_list(justifications[bit.position]); add_entry_list(justifications[bit.position]);
add_entry(e); add_entry(e);
@ -954,7 +950,7 @@ namespace {
//verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n"; //verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n";
if (prev != l_undef) { if (prev != l_undef) {
if (fixed[i] != prev) { if (fixed[i] != prev) {
verbose_stream() << "Positive parity conflicting " << e->src << " with " << justifications[i][0]->src << "\n"; LOG("Positive parity conflicting " << e->src << " with " << justifications[i][0]->src);
if (add_conflict) { if (add_conflict) {
add_entry_list(justifications[i]); add_entry_list(justifications[i]);
add_entry(e); add_entry(e);
@ -1013,7 +1009,7 @@ namespace {
if (i == neg.second.length) { if (i == neg.second.length) {
if (indet == 0) { if (indet == 0) {
// Already false // Already false
verbose_stream() << "Found conflict with constraint " << neg.first->src << "\n"; LOG("Found conflict with constraint " << neg.first->src);
if (add_conflict) { if (add_conflict) {
for (unsigned k = 0; k < neg.second.length; k++) for (unsigned k = 0; k < neg.second.length; k++)
add_entry_list(justifications[k]); add_entry_list(justifications[k]);
@ -1036,7 +1032,7 @@ namespace {
justification.push_back(neg.first); justification.push_back(neg.first);
fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true; fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true;
removed[j] = true; removed[j] = true;
//verbose_stream() << "Applying fast BCP on bit " << last_indet << " from constraint " << neg.first->src << "\n"; LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first->src);
changed = true; changed = true;
} }
} }