mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

first attempt at new explain_overlap

Browse source
This commit is contained in:
Jakob Rath 2024-05-14 16:22:57 +02:00
parent 764ccebcbf
commit 38745512c0
2 changed files with 69 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -672,7 +672,14 @@ if (counter == 17) {
SASSERT(first_it->e == last_it->e); SASSERT(first_it->e == last_it->e);
SASSERT(first_it != last_it); SASSERT(first_it != last_it);
#if 1 #if 1
explain_overlaps_v1(first_it, last_it, result); // the version discussed on whiteboard, no hole treatment needed
rational prefix(0);
for (explanation const* e = first_it; e != last_it; ++e) {
explanation const* after = e + 1;
explain_entry(e->e);
explain_overlap_v1(*e, *after, prefix, result);
}
#else #else
explain_overlaps_v2(first_it, last_it, result); explain_overlaps_v2(first_it, last_it, result);
#endif #endif
@ -707,7 +714,7 @@ if (counter == 17) {
} }
after = e; after = e;
explain_entry(e.e); explain_entry(e.e);
if (e.e == last.e) if (e.e == last.e)
break; break;
} }
@ -854,20 +861,9 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
return erased > 0; return erased > 0;
} }
void viable::explain_overlaps_v1(explanation const* first, explanation const* last, dependency_vector& deps) {
// version discussed on whiteboard, no hole stuff needed
SASSERT(first->e == last->e);
for (explanation const* e = first; e != last; ++e) {
explanation const* after = e + 1;
explain_overlap_v1(*e, *after, deps);
}
NOT_IMPLEMENTED_YET();
}
/* /*
* TODO: update explanation! (see appendix/notes)
*
* For two consecutive intervals * For two consecutive intervals
* *
* - 2^k x \not\in [lo, hi[ (entry 'e') * - 2^k x \not\in [lo, hi[ (entry 'e')
@ -924,8 +920,8 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
* - hi := v mod aw * - hi := v mod aw
* *
*/ */
void viable::explain_overlap_v1(explanation const& e, explanation const& after, dependency_vector& deps) { void viable::explain_overlap_v1(explanation const& e, explanation const& after, rational& prefix, dependency_vector& deps) {
#define DEBUG_EXPLAIN_OVERLAP 1 #define DEBUG_EXPLAIN_OVERLAP 0
unsigned const bw = c.size(e.e->var); unsigned const bw = c.size(e.e->var);
unsigned const ebw = e.e->bit_width; unsigned const ebw = e.e->bit_width;
unsigned const aw = c.size(after.e->var); unsigned const aw = c.size(after.e->var);
@ -939,6 +935,10 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
display_explain(verbose_stream() << " e ", e) << "\n"; display_explain(verbose_stream() << " e ", e) << "\n";
display_explain(verbose_stream() << " after ", after) << "\n"; display_explain(verbose_stream() << " after ", after) << "\n";
verbose_stream() << " bw " << bw << " ebw " << ebw << " aw " << aw << " abw " << abw << "\n"; verbose_stream() << " bw " << bw << " ebw " << ebw << " aw " << aw << " abw " << abw << "\n";
verbose_stream() << " t0: " << t << "\n";
verbose_stream() << " lo0: " << lo << "\n";
verbose_stream() << " hi0: " << hi << "\n";
verbose_stream() << " stored prefix: " << prefix << "\n";
#endif #endif
SASSERT(abw <= aw); SASSERT(abw <= aw);
@ -946,12 +946,43 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
SASSERT_EQ(mod2k(e.value, ebw), e.e->interval.hi_val()); SASSERT_EQ(mod2k(e.value, ebw), e.e->interval.hi_val());
SASSERT(r_interval::proper(after.e->interval.lo_val(), after.e->interval.hi_val()).contains(mod2k(e.value, abw))); SASSERT(r_interval::proper(after.e->interval.lo_val(), after.e->interval.hi_val()).contains(mod2k(e.value, abw)));
if (ebw < abw) { if (ebw > abw) {
// 'e' is the last entry of a hole. // effective bit-width reduces => store upper bits of value in prefix
// This case is handled in explain_hole_overlap. unsigned const store_sz = ebw - abw;
// return; // TODO: disabled for now rational const store_val = mod2k(machine_div2k(e.value, abw), store_sz);
prefix = prefix * rational::power_of_two(store_sz) + store_val;
verbose_stream() << " store_val = " << store_val << "\n";
verbose_stream() << " new stored prefix: " << prefix << "\n";
// for simplicity, we fix the evaluation of the stored upper bits
// (alternative would be to track sub-ranges of extracted symbolic bounds)
auto sc = cs.fixed(t, ebw - 1, abw, store_val);
verbose_stream() << " t[" << (ebw - 1) << ":" << abw << "] = " << store_val << "\n";
verbose_stream() << " fixed prefix constraint " << sc << "\n";
verbose_stream() << " eval " << sc.eval() << "\n";
verbose_stream() << " weval " << sc.weak_eval(c.get_assignment()) << "\n";
verbose_stream() << " seval " << sc.strong_eval(c.get_assignment()) << "\n";
VERIFY(!sc.is_always_false());
if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap prefix evaluation"));
}
verbose_stream() << "THIS IS IT\n"; rational restore_val;
if (ebw < abw) {
// restore bits from prefix
unsigned const restore_sz = abw - ebw;
/*rational const*/ restore_val = mod2k(prefix, restore_sz);
prefix = machine_div2k(prefix, restore_sz);
verbose_stream() << " restore_val = " << restore_val << "\n";
verbose_stream() << " new stored prefix: " << prefix << "\n";
// restore_val * rational::power_of_two(ebw) + t(?)
SASSERT(ebw < bw || aw != bw);
}
// if there is wrap-around, increment prefix
if (after.e->interval.lo_val() > after.e->interval.hi_val()) {
prefix++;
verbose_stream() << " incremented stored prefix: " << prefix << "\n";
} }
if (ebw < bw || aw != bw) { if (ebw < bw || aw != bw) {
@ -1003,28 +1034,29 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
verbose_stream() << "inconsistent overlap " << sc << " " << "\n"; verbose_stream() << "inconsistent overlap " << sc << " " << "\n";
} }
/*
if (ebw < abw) { if (ebw < abw) {
// NOTE: this doesn't work, because the projected interval may be empty if we just project 'after' instead of the hole's complement t = restore_val * rational::power_of_two(ebw) + t;
t *= rational::power_of_two(abw - ebw); verbose_stream() << " restored t: " << t << "\n";
lo *= rational::power_of_two(abw - ebw);
hi *= rational::power_of_two(abw - ebw);
} }
*/
if (abw < aw) if (abw < aw) {
t *= rational::power_of_two(aw - abw); t *= rational::power_of_two(aw - abw);
verbose_stream() << " shifted t: " << t << "\n";
}
auto sc = cs.ult(t - lo, hi - lo); auto sc = cs.ult(t - lo, hi - lo);
#if DEBUG_EXPLAIN_OVERLAP #if DEBUG_EXPLAIN_OVERLAP
// verbose_stream() << " lhs: " << t << " - (" << lo << ") == " << (t - lo) << "\n"; verbose_stream() << " t: " << t << "\n";
// verbose_stream() << " rhs: " << hi << " - (" << lo << ") == " << (hi - lo) << "\n"; verbose_stream() << " lo: " << lo << "\n";
// verbose_stream() << " ult: " << sc << "\n"; verbose_stream() << " hi: " << hi << "\n";
// verbose_stream() << " eval " << sc.eval() << "\n"; verbose_stream() << " lhs: " << t << " - (" << lo << ") == " << (t - lo) << "\n";
// verbose_stream() << " weval " << sc.weak_eval(c.get_assignment()) << "\n"; verbose_stream() << " rhs: " << hi << " - (" << lo << ") == " << (hi - lo) << "\n";
// verbose_stream() << " seval " << sc.strong_eval(c.get_assignment()) << "\n"; verbose_stream() << " ult: " << sc << "\n";
verbose_stream() << " eval " << sc.eval() << "\n";
verbose_stream() << " weval " << sc.weak_eval(c.get_assignment()) << "\n";
verbose_stream() << " seval " << sc.strong_eval(c.get_assignment()) << "\n";
#endif #endif
SASSERT(!sc.is_always_false()); VERIFY(!sc.is_always_false());
if (!sc.is_always_true()) if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap linking constraint")); deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap linking constraint"));
if (c.inconsistent()) { if (c.inconsistent()) {

3
src/sat/smt/polysat/viable.h
View file

@ -128,8 +128,7 @@ namespace polysat {
void update_value_to_high(rational& val, entry* e); void update_value_to_high(rational& val, entry* e);
bool is_conflict(); bool is_conflict();
void explain_overlaps_v1(explanation const* first, explanation const* last, dependency_vector& out_deps); void explain_overlap_v1(explanation const& e, explanation const& after, rational& prefix, dependency_vector& out_deps);
void explain_overlap_v1(explanation const& e, explanation const& after, dependency_vector& out_deps);
void explain_overlaps_v2(explanation const* first, explanation const* last, dependency_vector& out_deps); void explain_overlaps_v2(explanation const* first, explanation const* last, dependency_vector& out_deps);
void explain_overlap(explanation const& e, explanation const& after, dependency_vector& out_deps); void explain_overlap(explanation const& e, explanation const& after, dependency_vector& out_deps);
void explain_hole_overlap(explanation const& before, explanation const& e, explanation const& after, dependency_vector& out_deps); void explain_hole_overlap(explanation const& before, explanation const& e, explanation const& after, dependency_vector& out_deps);