mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

remove broken optimization (leads to undesired explanations)

Browse source
This commit is contained in:
Jakob Rath 2023-10-24 10:23:51 +02:00
parent 45bd052b3e
commit ebeb1296fd
1 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/polysat/slicing.cpp
View file

@ -98,9 +98,16 @@ namespace polysat {
if (d.is_null()) if (d.is_null())
out << "null"; out << "null";
else if (d.is_value()) { else if (d.is_value()) {
out << "value(v" << get_dep_var(d) << " on slice " << get_dep_slice(d)->get_id(); pvar x = get_dep_var(d);
if (get_dep_lit(d) != sat::null_literal) enode* n = get_dep_slice(d);
out << " by literal " << get_dep_lit(d); sat::literal lit = get_dep_lit(d);
out << "value(v" << x << " on slice ";
if (n)
out << n->get_id();
else
out << "<null>";
if (lit != sat::null_literal)
out << " by literal " << lit;
out << ")"; out << ")";
} }
else if (d.is_lit()) else if (d.is_lit())
@ -923,17 +930,8 @@ namespace polysat {
} }
bool slicing::egraph_merge(enode* s1, enode* s2, dep_t dep) { bool slicing::egraph_merge(enode* s1, enode* s2, dep_t dep) {
LOG("egraph_merge: " << slice_pp(*this, s1) << " and " << slice_pp(*this, s2)); LOG("egraph_merge: " << slice_pp(*this, s1) << " and " << slice_pp(*this, s2) << " by " << dep_pp(*this, dep));
SASSERT_EQ(width(s1), width(s2)); SASSERT_EQ(width(s1), width(s2));
enode* v1 = get_value_node(s1);
enode* v2 = get_value_node(s2);
if (v1 && v2 && get_value(v1) == get_value(v2)) {
// optimization: if s1, s2 are already equivalent to the same value,
// then they could have been merged already and we do not need to record 'dep'.
// merge the value slices instead.
m_egraph.merge(v1, v2, dep_t().encode());
return !is_conflict();
}
if (dep.is_value()) { if (dep.is_value()) {
if (is_value(s1)) if (is_value(s1))
std::swap(s1, s2); std::swap(s1, s2);