From 6103c9d718b83b231a89e172501a54d1b08c26aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Dec 2023 11:29:42 -0800 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 67 +++++++++++++++++++++++++++------- src/ast/euf/euf_bv_plugin.h | 13 ++++++- src/ast/euf/euf_egraph.cpp | 6 +++ src/sat/smt/polysat/core.cpp | 10 ++++- src/sat/smt/polysat/core.h | 2 +- src/sat/smt/polysat/types.h | 4 +- src/sat/smt/polysat/viable.cpp | 23 +++++++++++- src/sat/smt/polysat/viable.h | 3 ++ src/sat/smt/polysat_solver.cpp | 17 ++++++++- 9 files changed, 124 insertions(+), 21 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 89b5ade16..bb595b386 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -103,7 +103,7 @@ namespace euf { return mk(e, 0, nullptr); } - void bv_plugin::merge_eh(enode* x, enode* y) { + void bv_plugin::propagate_merge(enode* x, enode* y) { if (!bv.is_bv(x->get_expr())) return; @@ -128,6 +128,35 @@ namespace euf { propagate_extract(n); } + void bv_plugin::register_node(enode* n) { + m_queue.push_back(n); + m_trail.push_back(new (get_region()) push_back_vector(m_queue)); + push_plugin_undo(bv.get_family_id()); + } + + void bv_plugin::merge_eh(enode* n1, enode* n2) { + m_queue.push_back(enode_pair(n1, n2)); + m_trail.push_back(new (get_region()) push_back_vector(m_queue)); + push_plugin_undo(bv.get_family_id()); + } + + void bv_plugin::propagate() { + if (m_qhead == m_queue.size()) + return; + m_trail.push_back(new (get_region()) value_trail(m_qhead)); + push_plugin_undo(bv.get_family_id()); + for (; m_qhead < m_queue.size(); ++m_qhead) { + if (std::holds_alternative(m_queue[m_qhead])) { + auto n = *std::get_if(&m_queue[m_qhead]); + propagate_register_node(n); + } + else { + auto [a, b] = *std::get_if(&m_queue[m_qhead]); + propagate_merge(a, b); + } + } + } + // enforce concat(v1, v2) = v2*2^|v1| + v1 void bv_plugin::propagate_values(enode* x) { if (!is_value(x)) @@ -203,21 +232,32 @@ namespace euf { } } - void bv_plugin::push_undo_split(enode* n) { - m_undo_split.push_back(n); + class bv_plugin::undo_split : public trail { + bv_plugin& p; + enode* n; + public: + undo_split(bv_plugin& p, enode* n): p(p), n(n) {} + void undo() override { + auto& i = p.info(n); + i.value = nullptr; + i.lo = nullptr; + i.hi = nullptr; + i.cut = null_cut; + } + }; + + void bv_plugin::push_undo_split(enode* n) { + m_trail.push_back(new (get_region()) undo_split(*this, n)); push_plugin_undo(bv.get_family_id()); } void bv_plugin::undo() { - enode* n = m_undo_split.back(); - m_undo_split.pop_back(); - auto& i = info(n); - i.lo = nullptr; - i.hi = nullptr; - i.cut = null_cut; + m_trail.back()->undo(); + m_trail.pop_back(); } + - void bv_plugin::register_node(enode* n) { + void bv_plugin::propagate_register_node(enode* n) { TRACE("bv", tout << "register " << g.bpp(n) << "\n"); auto& i = info(n); i.value = n; @@ -236,6 +276,7 @@ namespace euf { push_merge(mk_extract(arg, 0, w - 1), arg); ensure_slice(arg, lo, hi); } + TRACE("bv", tout << "done register " << g.bpp(n) << "\n"); } // @@ -487,10 +528,10 @@ namespace euf { } std::ostream& bv_plugin::display(std::ostream& out) const { - out << "bv\n"; + out << "bv\n"; for (auto const& i : m_info) - if (i.lo) - out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n"; + if (i.lo) + out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n"; return out; } } diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h index 199aed4e7..f09697f39 100644 --- a/src/ast/euf/euf_bv_plugin.h +++ b/src/ast/euf/euf_bv_plugin.h @@ -19,6 +19,7 @@ Author: #pragma once +#include "util/trail.h" #include "ast/bv_decl_plugin.h" #include "ast/euf/euf_plugin.h" @@ -81,8 +82,16 @@ namespace euf { svector> m_jtodo; void clear_offsets(); - enode_vector m_undo_split; + + ptr_vector m_trail; + + class undo_split; void push_undo_split(enode* n); + + vector> m_queue; + unsigned m_qhead = 0; + void propagate_register_node(enode* n); + void propagate_merge(enode* a, enode* b); public: bv_plugin(egraph& g); @@ -97,7 +106,7 @@ namespace euf { void diseq_eh(enode* eq) override {} - void propagate() override {} + void propagate() override; void undo() override; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index c32a81739..6f6b6a7e8 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -107,7 +107,10 @@ namespace euf { void egraph::update_children(enode* n) { for (enode* child : enode_args(n)) child->get_root()->add_parent(n); + for (enode* child : enode_args(n)) + SASSERT(child->get_root()->m_parents.back() == n); m_updates.push_back(update_record(n, update_record::update_children())); + TRACE("euf", tout << "update children " << bpp(n) << "\n"; display(tout)); } enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) { @@ -441,7 +444,10 @@ namespace euf { p.r1->set_relevant(false); break; case update_record::tag_t::is_update_children: + TRACE("euf", tout << "reverse update children " << bpp(p.r1) << "\n"; display(tout)); for (unsigned i = 0; i < p.r1->num_args(); ++i) { + CTRACE("euf", (p.r1->m_args[i]->get_root()->m_parents.back() != p.r1), + display(tout << bpp(p.r1->m_args[i]) << " " << bpp(p.r1->m_args[i]->get_root()) << " ");); SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1); p.r1->m_args[i]->get_root()->m_parents.pop_back(); } diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 83fffd812..04f0ae857 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -320,7 +320,8 @@ namespace polysat { if (!is_assigned(v0) || is_assigned(v1)) continue; // detect unitary, add to viable, detect conflict? - m_viable.add_unitary(v1, idx); + if (value != l_undef) + m_viable.add_unitary(v1, idx); } SASSERT(m_watch[v].size() == sz && "size of watch list was not changed"); m_watch[v].shrink(j); @@ -347,16 +348,20 @@ namespace polysat { } dependency core::get_dependency(constraint_id idx) const { + if (idx.is_null()) + return null_dependency; auto [sc, d, value] = m_constraint_index[idx.id]; return d; } +#if 0 dependency_vector core::get_dependencies(constraint_id_vector const& ids) const { dependency_vector result; for (auto id : ids) result.push_back(get_dependency(id)); return result; } +#endif void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) { lbool eval_value = eval(sc); @@ -442,8 +447,9 @@ namespace polysat { out << "polysat:\n"; for (auto const& [sc, d, value] : m_constraint_index) out << sc << " " << d << " := " << value << "\n"; - for (unsigned i = 0; i < m_vars.size(); ++i) + for (unsigned i = 0; i < m_vars.size(); ++i) { out << m_vars[i] << " := " << m_values[i] << " " << get_dependency(m_justification[i]) << "\n"; + } m_var_queue.display(out << "vars ") << "\n"; return out; } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index dc67b0ddc..7c8466b92 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -155,7 +155,7 @@ namespace polysat { dependency_vector const& unsat_core() const { return m_unsat_core; } constraint_id_vector const& assigned_constraints() const { return m_prop_queue; } dependency get_dependency(constraint_id idx) const; - dependency_vector get_dependencies(constraint_id_vector const& ids) const; + // dependency_vector get_dependencies(constraint_id_vector const& ids) const; lbool eval(constraint_id id); dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps); } lbool eval(signed_constraint const& sc); diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 9acb96901..255231453 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -110,7 +110,9 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) { - return out << "v" << js.v << "[" << js.offset << "[ @"; + if (js.offset == 0) + return out << "v" << js.v; + return out << "v" << js.v << " at offset " << js.offset; } using fixed_bits_vector = svector; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index a0eb4c2e4..1578dc443 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -84,6 +84,7 @@ namespace polysat { } find_t viable::find_viable(pvar v, rational& lo) { + display(verbose_stream() << "find viable for v" << v << "\n"); rational hi; switch (find_viable(v, lo, hi)) { case l_true: @@ -99,7 +100,6 @@ namespace polysat { m_overlaps.reset(); c.get_bitvector_suffixes(v, m_overlaps); std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); }); - LOG("Overlaps with v" << v << ":" << m_overlaps); } lbool viable::find_viable(pvar v, rational& val1, rational& val2) { @@ -217,6 +217,8 @@ namespace polysat { } // TODO check if admitted: layer.entries = e; m_explain.push_back(e); + if (e->interval.is_full()) + return l_false; auto hi = e->interval.hi_val(); if (hi < val1) { if (is_zero) @@ -868,6 +870,25 @@ namespace polysat { return out; } + std::ostream& viable::display(std::ostream& out) const { + for (unsigned v = 0; v < m_units.size(); ++v) { + bool first = true; + for (auto const& layer : m_units[v].get_layers()) { + if (!layer.entries) + continue; + if (first) + out << "v" << v << ": "; + first = false; + if (layer.bit_width != c.size(v)) + out << "width[" << layer.bit_width << "] "; + display_all(out, v, layer.entries, " "); + } + if (!first) + out << "\n"; + } + return out; + } + /* * Lower bounds are strictly ascending. * Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction). diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index f1ae50c2c..54681c7a5 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -158,6 +158,9 @@ namespace polysat { */ void ensure_var(pvar v); + + std::ostream& display(std::ostream& out) const; + }; } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 4d10039e7..599fadd87 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -40,7 +40,8 @@ namespace polysat { m_intblast(ctx), m_lemma(ctx.get_manager()) { - // ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph())); + m_bv_plugin = alloc(euf::bv_plugin, ctx.get_egraph()); + ctx.get_egraph().add_plugin(m_bv_plugin); } unsigned solver::get_bv_size(euf::enode* n) { @@ -120,6 +121,20 @@ namespace polysat { auto lit = sat::literal(bv, s().value(bv) == l_false); core.push_back(lit); } + else if (d.is_fixed_claim()) { + auto const& o = d.fixed(); + std::function consume = [&](auto* a, auto* b) { + eqs.push_back({ a, b }); + }; + explain_fixed(o.v, o.lo, o.hi, o.value, consume); + } + else if (d.is_offset_claim()) { + auto const& offs = d.offset(); + std::function consume = [&](auto* a, auto* b) { + eqs.push_back({ a, b }); + }; + explain_slice(offs.v, offs.w, offs.offset, consume); + } else { auto const [v1, v2] = d.eq(); euf::enode* const n1 = var2enode(v1);