From 9fb86a4d4fea06470cb83d17f70f20d868095a49 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jan 2024 11:09:06 -0800 Subject: [PATCH] fixing fixed-bits viable --- src/sat/smt/polysat/fixed_bits.cpp | 7 +++++-- src/sat/smt/polysat/forbidden_intervals.cpp | 5 +++++ src/sat/smt/polysat/forbidden_intervals.h | 2 ++ src/sat/smt/polysat/types.h | 2 +- src/sat/smt/polysat/viable.cpp | 11 +---------- src/sat/smt/polysat_egraph.cpp | 12 ++++-------- 6 files changed, 18 insertions(+), 21 deletions(-) diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp index 282e1fe28..761c0fabd 100644 --- a/src/sat/smt/polysat/fixed_bits.cpp +++ b/src/sat/smt/polysat/fixed_bits.cpp @@ -34,10 +34,12 @@ namespace polysat { bool fixed_bits::check(rational const& val, fi_record& fi) { unsigned sz = c.size(m_var); rational bw = rational::power_of_two(sz); + // verbose_stream() << "check for fixed bits v" << m_var << "[" << sz << "] := " << val << "\n"; for (auto const& s : m_fixed_slices) { rational sbw = rational::power_of_two(s.length); // slice is properly contained in bit-vector variable - if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset + 1), sbw)) { + // verbose_stream() << " slice " << s.value << "[" << s.length << "]@" << s.offset << "\n"; + if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) { SASSERT(s.offset + s.length <= sz); rational hi_val = s.value; rational lo_val = mod(s.value + 1, sbw); @@ -46,6 +48,7 @@ namespace polysat { fi.reset(); fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); fi.deps.push_back(dependency({ m_var, s })); + fi.bit_width = s.length; fi.coeff = 1; return false; @@ -59,7 +62,7 @@ namespace polysat { pdd hi = c.value(hi_val, sz); fi.reset(); fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); - fi.deps.push_back(dependency({ m_var, s })); + fi.deps.push_back(dependency({ m_var, s })); fi.bit_width = sz; fi.coeff = 1; return false; diff --git a/src/sat/smt/polysat/forbidden_intervals.cpp b/src/sat/smt/polysat/forbidden_intervals.cpp index 890fb7147..3b573548c 100644 --- a/src/sat/smt/polysat/forbidden_intervals.cpp +++ b/src/sat/smt/polysat/forbidden_intervals.cpp @@ -21,6 +21,11 @@ Author: namespace polysat { + std::ostream& operator<<(std::ostream& out, fi_record const& fi) { + out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " << fi.src << fi.side_cond << fi.deps << ")"; + return out; + } + /** * * \param[in] c Original constraint diff --git a/src/sat/smt/polysat/forbidden_intervals.h b/src/sat/smt/polysat/forbidden_intervals.h index 362b03455..1845c09bd 100644 --- a/src/sat/smt/polysat/forbidden_intervals.h +++ b/src/sat/smt/polysat/forbidden_intervals.h @@ -49,6 +49,8 @@ namespace polysat { }; }; + std::ostream& operator<<(std::ostream& out, fi_record const& fi); + class forbidden_intervals { void push_eq(bool is_trivial, pdd const& p, vector& side_cond); diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 8d605cf41..5258fd31b 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -47,7 +47,7 @@ namespace polysat { pvar v; fixed_claim() = default; fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(value, offset, length), v(v) {} - fixed_claim(pvar, fixed_slice const& s) : fixed_slice(s), v(v) {} + fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), v(v) {} }; struct offset_slice { diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 459f6f5e3..de2b9f8a4 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -92,7 +92,6 @@ namespace polysat { m_conflict = false; m_propagation = false; - // verbose_stream() << "find viable v" << v << " starting with " << lo << "\n"; for (unsigned rounds = 0; rounds < 10; ) { @@ -361,9 +360,6 @@ namespace polysat { } bool viable::check_fixed_bits(pvar v, rational const& val) { - // disable fixed bits for now - return true; - auto e = alloc_entry(v, constraint_id::null()); if (m_fixed_bits.check(val, *e)) { m_alloc.push_back(e); @@ -371,6 +367,7 @@ namespace polysat { } else { intersect(v, e); + TRACE("bv", tout << "fixed " << *e << "\n"); return false; } } @@ -391,11 +388,6 @@ namespace polysat { m_diseq_lin[v] = m_diseq_lin[v]->next(); do { - // IF_LOGGING( - // verbose_stream() << "refine-disequal-lin for v" << v << " in src: "; - // for (const auto& src : e->src) - // verbose_stream() << lit_pp(s, src) << "\n"; - // ); // We compute an interval if the concrete value 'val' violates the constraint: // p*val + q > r*val + s if e->src.is_positive() @@ -806,7 +798,6 @@ namespace polysat { bool viable::intersect(pvar v, entry* ne) { SASSERT(!c.is_assigned(v)); - SASSERT(!ne->src.empty()); entry*& entries = m_units[v].ensure_layer(ne->bit_width).entries; entry* e = entries; if (e && e->interval.is_full()) { diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 5038f1293..fa0f27d1a 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -94,26 +94,22 @@ namespace polysat { // walk the e-graph to retrieve fixed overlaps void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) { - std::function consume_slice = [&](euf::enode* n, unsigned offset) { - // verbose_stream() << "sub-slice " << ctx.bpp(n) << " " << offset << "\n"; + n = n->get_root(); if (!n->interpreted()) return true; - auto w = n->get_root()->get_th_var(get_id()); + auto w = n->get_th_var(get_id()); if (w == euf::null_theory_var) return true; - auto const& p = m_var2pdd[w]; - if (!p.is_var()) - return true; unsigned length = bv.get_bv_size(n->get_expr()); rational value; VERIFY(bv.is_numeral(n->get_expr(), value)); out.push_back({ fixed_slice(value, offset, length) }); return false; }; - theory_var v = m_pddvar2var[pv]; - // verbose_stream() << "Get fixed_bits " << ctx.bpp(var2enode(v)) << "\n"; + theory_var v = m_pddvar2var[pv]; m_bv_plugin->sub_slices(var2enode(v), consume_slice); + m_bv_plugin->super_slices(var2enode(v), consume_slice); } void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function& consume_eq) {