diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index d64c0eb6b..7f22643bb 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -449,6 +449,18 @@ namespace polysat { s.get_bitvector_sub_slices(v, out); } + pdd core::mk_zero_extend(unsigned sz, pdd const& p) { + if (p.is_val()) + return value(p.val(), p.manager().power_of_2() + sz); + throw default_exception("nyi zero_extend"); + } + + pdd core::mk_extract(unsigned hi, unsigned lo, pdd const& p) { + if (p.is_val()) + return value(p.val(), hi - lo + 1); + throw default_exception("nyi extract"); + } + bool core::inconsistent() const { return s.inconsistent(); } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index a64c34878..dcd0c852f 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -158,7 +158,8 @@ namespace polysat { void get_bitvector_suffixes(pvar v, offset_slices& out); void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice); void get_subslices(pvar v, offset_slices& out); - pdd mk_extract(unsigned hi, unsigned lo, pdd const& p) { throw default_exception("nyi extract"); } + pdd mk_zero_extend(unsigned sz, pdd const& p); + pdd mk_extract(unsigned hi, unsigned lo, pdd const& p); /* * Saturation diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index d134785bd..65d48a683 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -85,7 +85,6 @@ namespace polysat { find_t viable::find_viable(pvar v, rational& lo) { m_explain.reset(); - m_ineqs.reset(); m_var = v; m_num_bits = c.size(v); m_fixed_bits.reset(v); @@ -106,11 +105,10 @@ namespace polysat { continue; } - m_explain.push_back(n); - if (is_conflict()) - return find_t::empty; - update_value_to_high(lo, n); + m_explain.push_back({ n, lo }); + if (is_conflict()) + return find_t::empty; } return find_t::resource_out; @@ -457,12 +455,12 @@ namespace polysat { */ bool viable::is_conflict() { auto last = m_explain.back(); - unsigned bw = last->bit_width; + unsigned bw = last.e->bit_width; for (unsigned i = m_explain.size() - 1; i-- > 0; ) { auto e = m_explain[i]; - if (bw < e->bit_width) + if (bw < e.e->bit_width) return false; - if (last == e) + if (last.e == e.e) return true; } return false; @@ -478,20 +476,20 @@ namespace polysat { uint_set seen; auto last = m_explain.back(); auto after = last; - unsigned bw = c.size(last->var); + unsigned bw = c.size(last.e->var); for (unsigned i = m_explain.size() - 1; i-- > 0; ) { auto e = m_explain[i]; - auto index = e->constraint_index; + auto index = e.e->constraint_index; explain_overlap(e, after, result); - if (e == last) + if (e.e == last.e) break; after = e; if (seen.contains(index.id)) continue; seen.insert(index.id); - if (m_var != e->var) - result.push_back(offset_claim(m_var, { e->var, 0 })); - for (auto const& sc : e->side_cond) + if (m_var != e.e->var) + result.push_back(offset_claim(m_var, { e.e->var, 0 })); + for (auto const& sc : e.e->side_cond) result.push_back(c.propagate(sc, c.explain_eval(sc))); result.push_back(c.get_dependency(index)); } @@ -501,35 +499,65 @@ namespace polysat { return result; } - void viable::explain_overlap(entry* e, entry* after, dependency_vector& deps) { - auto bw = c.size(e->var); - auto bw_after = c.size(after->var); - auto t = e->interval.hi(); - auto lo = after->interval.lo(); - auto hi = after->interval.hi(); + /* + * For two consecutive intervals + * + * - 2^kx \not\in [lo, hi[, + * - 2^k'y \not\in [lo', hi'[ + * + * Where: + * - w is the width of x, w' the width of y + * - bw is the bit-width of x, bw' the bit-width of y + * - k = w - bwx, k' = w' - bw' + * + * We want to encode the constraint that (2^k' hi)[w'] in [lo', hi'[ + * + * Note that x in [lo, hi[ <=> x - lo < hi - lo + * If k' = 0, w' = w, there is nothing to do. + * If w' > w, then hi <- zero_extend(w' - w, hi) + * If w' < w, then hi <- hi[w' - 1:0] + * If k' > 0, then hi <- 2^k' hi + * + * TODO: So far we assume that hi is divisible by 2^k. + * + */ - SASSERT(after->bit_width <= bw_after); - SASSERT(e->bit_width <= bw); + void viable::explain_overlap(explanation const& e, explanation const& after, dependency_vector& deps) { + auto bw = c.size(e.e->var); + auto bw_after = c.size(after.e->var); + auto t = e.e->interval.hi(); + auto lo = after.e->interval.lo(); + auto hi = after.e->interval.hi(); - // if e/after use same bit-width, but different layer, then .. - // - if (bw < bw_after) { - SASSERT(after->bit_width == bw_after); - SASSERT(e->bit_width = bw); - verbose_stream() << t << " " << lo << " " << hi << "\n"; - auto s = c.mk_extract(bw - 1, 0, t); + verbose_stream() << e.e->interval << " then " << after.e->interval << "\n"; + + SASSERT(after.e->bit_width <= bw_after); + SASSERT(e.e->bit_width <= bw); + + if (bw_after > bw) { + auto eq = cs.eq(t, c.value(mod(e.value, rational::power_of_two(bw)), bw)); + if (!eq.is_always_true()) + deps.push_back(c.propagate(eq, c.explain_eval(eq))); t.reset(lo.manager()); - t = s; + t = c.value(e.value, bw_after); } - else if (bw > bw_after) { - throw default_exception("Nyi after"); -// auto s = c.mk_zero_extend(bw - bw_after, t); -// t.reset(lo.manager()); -// t = s; + + if (bw_after < bw) { + auto eq = cs.eq(t, c.value(e.value, bw)); + if (!eq.is_always_true()) + deps.push_back(c.propagate(eq, c.explain_eval(eq))); + t.reset(lo.manager()); + t = c.value(mod(e.value, rational::power_of_two(bw_after)), bw_after); } + + if (after.e->bit_width < bw_after) + t *= rational::power_of_two(bw_after - after.e->bit_width); + auto sc = cs.ult(t - lo, hi - lo); + verbose_stream() << "in interval: " << sc << "\n"; if (sc.is_always_true()) return; + SASSERT(!sc.is_always_false()); deps.push_back(c.propagate(sc, c.explain_eval(sc))); } @@ -647,8 +675,7 @@ namespace polysat { } if (ne->interval.is_full()) { m_explain.reset(); - m_ineqs.reset(); - m_explain.push_back(ne); + m_explain.push_back({ ne, rational::zero() }); m_fixed_bits.reset(); m_var = v; return false; diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index 010a069e7..4dc421301 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -86,15 +86,15 @@ namespace polysat { }; // short for t in [lo,hi[ - struct interval_member { - entry* prev, * next; + struct explanation { + entry* e; + rational value; }; ptr_vector m_alloc; vector m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order ptr_vector m_equal_lin; // entries that have non-unit multipliers, but are equal ptr_vector m_diseq_lin; // entries that have distinct non-zero multipliers - vector m_ineqs; // inequalities to justify that values are not viable. - ptr_vector m_explain; // entries that explain the current propagation or conflict + vector m_explain; // entries that explain the current propagation or conflict bool well_formed(entry* e); bool well_formed(layers const& ls); @@ -122,7 +122,7 @@ namespace polysat { void update_value_to_high(rational& val, entry* e); bool is_conflict(); - void explain_overlap(entry* e, entry* after, dependency_vector& deps); + void explain_overlap(explanation const& e, explanation const& after, dependency_vector& deps); lbool next_viable_layer(pvar w, layer& l, rational& val);