mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 04:31:24 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2024-02-26 10:40:37 +01:00
parent 3eb42cdf4b
commit b561795214
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -227,7 +227,6 @@ namespace polysat {
lhs *= x; lhs *= x;
SASSERT(lhs.leading_coefficient().is_power_of_two()); SASSERT(lhs.leading_coefficient().is_power_of_two());
} }
TRACE("bv_verbose", tout << "simplified " << lhs << " <= " << rhs << "\n");
} // simplify_impl } // simplify_impl
} }
@ -262,6 +261,7 @@ namespace polysat {
if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) { if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) {
ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs); ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs);
ule_pp const new_ule(to_lbool(is_positive), lhs, rhs); ule_pp const new_ule(to_lbool(is_positive), lhs, rhs);
TRACE("bv", tout << "original: " << old_ule << "\nsimplified: " << new_ule << "\n");
// always-false and always-true constraints should be rewritten to 0 != 0 and 0 == 0, respectively. // always-false and always-true constraints should be rewritten to 0 != 0 and 0 == 0, respectively.
if (is_always_false(old_is_positive, old_lhs, old_rhs)) { if (is_always_false(old_is_positive, old_lhs, old_rhs)) {
SASSERT(!is_positive); SASSERT(!is_positive);

9
src/sat/smt/polysat/viable.cpp
View file

@ -648,11 +648,17 @@ namespace polysat {
verbose_stream() << "\n\n\n\n\n\nNon-viable assignment for v" << m_var << " size " << c.size(m_var) << "\n"; verbose_stream() << "\n\n\n\n\n\nNon-viable assignment for v" << m_var << " size " << c.size(m_var) << "\n";
display_one(verbose_stream() << "entry: ", e) << "\n"; display_one(verbose_stream() << "entry: ", e) << "\n";
verbose_stream() << "value " << value << "\n"; verbose_stream() << "value " << value << "\n";
m_fixed_bits.display(verbose_stream() << "fixed: ") << "\n";
fixed_slice_extra_vector fixed; fixed_slice_extra_vector fixed;
offset_slice_extra_vector subslices; offset_slice_extra_vector subslices;
c.s.get_fixed_sub_slices(m_var, fixed, subslices); // TODO: move into m_fixed bits? c.s.get_fixed_sub_slices(m_var, fixed, subslices); // TODO: move into m_fixed bits?
// this case occurs if e-graph merges e.g. nodes "x - 2" and "3";
// polysat will see assignment "x = 5" but no fixed bits
if (subslices.empty())
return null_dependency;
unsigned max_level = 0; unsigned max_level = 0;
for (auto const& slice : subslices) for (auto const& slice : subslices)
max_level = std::max(max_level, slice.level); max_level = std::max(max_level, slice.level);
@ -681,6 +687,9 @@ namespace polysat {
unsigned w_level = slice.level; // level where value of w was fixed unsigned w_level = slice.level; // level where value of w was fixed
if (w == m_var) if (w == m_var)
return null_dependency; return null_dependency;
if (w == e->var)
return null_dependency;
// verbose_stream() << "v" << m_var << " size " << c.size(m_var) << ", v" << w << " size " << c.size(w) << " offset " << offset << " level " << w_level << "\n"; // verbose_stream() << "v" << m_var << " size " << c.size(m_var) << ", v" << w << " size " << c.size(w) << " offset " << offset << " level " << w_level << "\n";
// Let: // Let: