From 91b9d78cd3ff4d1cb7768438972534d2c22cf513 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Dec 2023 17:36:42 -0800 Subject: [PATCH] bugfixes Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 59 ++++++++++++++++------------- src/ast/euf/euf_bv_plugin.h | 4 +- src/ast/euf/euf_plugin.cpp | 1 + src/sat/smt/intblast_solver.cpp | 19 ++++++---- src/sat/smt/polysat/constraints.cpp | 5 ++- src/sat/smt/polysat/core.cpp | 8 ++-- src/sat/smt/polysat_model.cpp | 33 +++++++++++----- src/sat/smt/polysat_solver.cpp | 3 +- 8 files changed, 81 insertions(+), 51 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index e6be6e45b..97cb8d52e 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -74,13 +74,10 @@ then t1 = t2 iff t1 ~ t2 in the E-graph. TODO: Is saturation for (7) overkill for the purpose of canonization? -TODO: revisit re-entrancy during register_node. It can be called when creating internal extract terms. -Instead of allowing re-entrancy we can accumulate nodes that are registered during recursive calls -and have the main call perform recursive slicing. - --*/ +#include "ast/ast_pp.h" #include "ast/euf/euf_bv_plugin.h" #include "ast/euf/euf_egraph.h" @@ -91,11 +88,11 @@ namespace euf { bv(g.get_manager()) {} - enode* bv_plugin::mk_value_concat(enode* a, enode* b) { - auto v1 = get_value(a); - auto v2 = get_value(b); - auto v3 = v1 + v2 * power(rational(2), width(a)); - return mk_value(v3, width(a) + width(b)); + enode* bv_plugin::mk_value_concat(enode* hi, enode* lo) { + auto v1 = get_value(hi); + auto v2 = get_value(lo); + auto v3 = v2 + v1 * rational::power_of_two(width(lo)); + return mk_value(v3, width(lo) + width(lo)); } enode* bv_plugin::mk_value(rational const& v, unsigned sz) { @@ -157,7 +154,7 @@ namespace euf { } } - // enforce concat(v1, v2) = v2*2^|v1| + v1 + // enforce concat(v1, v2) = v1*2^|v2| + v2 void bv_plugin::propagate_values(enode* x) { if (!is_value(x)) return; @@ -171,9 +168,9 @@ namespace euf { if (is_concat(sib, a, b)) { if (!is_value(a) || !is_value(b)) { auto val = get_value(x); - auto v1 = mod2k(val, width(a)); - auto v2 = machine_div2k(val, width(a)); - push_merge(mk_concat(mk_value(v1, width(a)), mk_value(v2, width(b))), x->get_interpreted()); + auto val_a = machine_div2k(val, width(b)); + auto val_b = mod2k(val, width(b)); + push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); } } } @@ -205,18 +202,18 @@ namespace euf { if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r) return; // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications - push_merge(mk_concat(mk_extract(arg, lo, mid), mk_extract(arg, mid + 1, hi)), mk_extract(arg, lo, hi)); + push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi)); }; - auto propagate_left = [&](enode* b) { - TRACE("bv", tout << "propagate-left " << g.bpp(b) << "\n"); + auto propagate_above = [&](enode* b) { + TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n"); for (enode* sib : enode_class(b)) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2) ensure_concat(lo1, hi1, hi2); }; - auto propagate_right = [&](enode* a) { - TRACE("bv", tout << "propagate-right " << g.bpp(a) << "\n"); + auto propagate_below = [&](enode* a) { + TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n"); for (enode* sib : enode_class(a)) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1) ensure_concat(lo2, hi2, hi1); @@ -225,9 +222,9 @@ namespace euf { for (enode* p : enode_parents(n)) { if (is_concat(p, a, b)) { if (a->get_root() == n_r) - propagate_left(b); + propagate_below(b); if (b->get_root() == n_r) - propagate_right(a); + propagate_above(a); } } } @@ -263,9 +260,9 @@ namespace euf { i.value = n; enode* a, * b; if (is_concat(n, a, b)) { - i.lo = a; - i.hi = b; - i.cut = width(a); + i.hi = a; + i.lo = b; + i.cut = width(b); push_undo_split(n); } unsigned lo, hi; @@ -328,12 +325,20 @@ namespace euf { hi += lo1; n = n->get_arg(0); } + if (n->interpreted()) { + auto v = get_value(n); + if (lo > 0) + v = div(v, rational::power_of_two(lo)); + if (hi + 1 != width(n)) + v = mod(v, rational::power_of_two(hi + 1)); + return mk(bv.mk_numeral(v, hi - lo + 1), 0, nullptr); + } return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n); } - enode* bv_plugin::mk_concat(enode* lo, enode* hi) { - enode* args[2] = { lo, hi }; - return mk(bv.mk_concat(lo->get_expr(), hi->get_expr()), 2, args); + enode* bv_plugin::mk_concat(enode* hi, enode* lo) { + enode* args[2] = { hi, lo }; + return mk(bv.mk_concat(hi->get_expr(), lo->get_expr()), 2, args); } void bv_plugin::merge(enode_vector& xs, enode_vector& ys, justification dep) { @@ -390,7 +395,7 @@ namespace euf { i.lo = lo; i.cut = cut; push_undo_split(n); - push_merge(mk_concat(lo, hi), n); + push_merge(mk_concat(hi, lo), n); } void bv_plugin::sub_slices(enode* n, std::function& consumer) { diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h index f09697f39..b2253e816 100644 --- a/src/ast/euf/euf_bv_plugin.h +++ b/src/ast/euf/euf_bv_plugin.h @@ -53,8 +53,8 @@ namespace euf { unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); } enode* mk_extract(enode* n, unsigned lo, unsigned hi); - enode* mk_concat(enode* lo, enode* hi); - enode* mk_value_concat(enode* lo, enode* hi); + enode* mk_concat(enode* hi, enode* lo); + enode* mk_value_concat(enode* hi, enode* lo); enode* mk_value(rational const& v, unsigned sz); unsigned width(enode* n) { return bv.get_bv_size(n->get_expr()); } bool is_value(enode* n) { return n->get_root()->interpreted(); } diff --git a/src/ast/euf/euf_plugin.cpp b/src/ast/euf/euf_plugin.cpp index 57c1849fd..9551b7948 100644 --- a/src/ast/euf/euf_plugin.cpp +++ b/src/ast/euf/euf_plugin.cpp @@ -26,6 +26,7 @@ namespace euf { } void plugin::push_merge(enode* a, enode* b, justification j) { + TRACE("euf", tout << "push-merge " << g.bpp(a) << " == " << g.bpp(b) << " " << j << "\n"); g.push_merge(a, b, j); } diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index bc0457509..f3fee6ce2 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -220,7 +220,8 @@ namespace intblast { m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); } - IF_VERBOSE(10, verbose_stream() << "check\n"; + IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n"); + IF_VERBOSE(3, verbose_stream() << "check\n"; m_solver->display(verbose_stream()); verbose_stream() << es << "\n"); @@ -230,14 +231,18 @@ namespace intblast { IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); if (r == l_true) { - model_ref mdl; - m_solver->get_model(mdl); - verbose_stream() << original_es << "\n"; - verbose_stream() << *mdl << "\n"; - verbose_stream() << es << "\n"; - m_solver->display(verbose_stream()); + IF_VERBOSE(0, + model_ref mdl; + m_solver->get_model(mdl); + verbose_stream() << original_es << "\n"; + verbose_stream() << *mdl << "\n"; + verbose_stream() << es << "\n"; + m_solver->display(verbose_stream());); + SASSERT(false); } + m_solver = nullptr; + return r; } diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index e7a204295..5bf8df60b 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -75,7 +75,10 @@ namespace polysat { if (!l.hi().is_one()) return false; v = l.var(); - val = -l.lo().val(); + if (l.lo().val() == 0) + val = 0; + else + val = l.manager().max_value() + 1 - l.lo().val(); return true; } diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 6b6dc1acf..ada63336d 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -172,8 +172,10 @@ namespace polysat { s.set_conflict(m_viable.explain(), "viable-conflict"); return sat::check_result::CR_CONTINUE; case find_t::singleton: { - TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << "\n"); - auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain(), "viable-propagate"); + auto p = var2pdd(m_var).mk_var(m_var); + auto sc = m_constraints.eq(p, m_value); + TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << " " << sc << "\n"); + auto d = s.propagate(sc, m_viable.explain(), "viable-propagate"); propagate_assignment(m_var, m_value, d); return sat::check_result::CR_CONTINUE; } @@ -297,8 +299,6 @@ namespace polysat { return; v = w; } - if (v != null_var) - verbose_stream() << "propagate activation " << v << " " << sc << " " << dep << "\n"; if (v != null_var && !m_viable.add_unitary(v, idx.id)) s.set_conflict(m_viable.explain(), "viable-conflict"); } diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp index 3883b334d..8d1c40c37 100644 --- a/src/sat/smt/polysat_model.cpp +++ b/src/sat/smt/polysat_model.cpp @@ -23,16 +23,29 @@ Author: namespace polysat { - void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { - auto p = expr2pdd(n->get_expr()); - rational val; - if (!m_core.try_eval(p, val)) { - ctx.s().display(verbose_stream()); - verbose_stream() << ctx.bpp(n) << " := " << p << "\n"; - UNREACHABLE(); + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr_ref value(m); + if (n->interpreted()) + value = n->get_expr(); + else if (n->get_decl() && n->get_decl()->get_family_id() == bv.get_family_id()) { + bv_rewriter rw(m); + expr_ref_vector args(m); + for (auto arg : euf::enode_args(n)) + args.push_back(values.get(arg->get_root_id())); + rw.mk_app(n->get_decl(), args.size(), args.data(), value); } - VERIFY(m_core.try_eval(p, val)); - values.set(n->get_root_id(), bv.mk_numeral(val, get_bv_size(n))); + else { + auto p = expr2pdd(n->get_expr()); + rational val; + if (!m_core.try_eval(p, val)) { + ctx.s().display(verbose_stream()); + verbose_stream() << ctx.bpp(n) << " := " << p << "\n"; + UNREACHABLE(); + } + VERIFY(m_core.try_eval(p, val)); + value = bv.mk_numeral(val, get_bv_size(n)); + } + values.set(n->get_root_id(), value); } bool solver::add_dep(euf::enode* n, top_sort& dep) { @@ -87,12 +100,14 @@ namespace polysat { auto r = m_intblast.check_propagation(lit, core, eqs); VERIFY (r != l_true); } + void solver::validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) { if (!ctx.get_config().m_core_validate) return; auto r = m_intblast.check_core(core, eqs); VERIFY (r != l_true); } + void solver::validate_axiom(sat::literal_vector const& clause) { if (!ctx.get_config().m_core_validate) return; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index f66e90ed3..d51eb4b75 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -114,6 +114,7 @@ namespace polysat { hint = mk_proof_hint(hint_info); auto ex = euf::th_explain::conflict(*this, lits, eqs, hint); TRACE("bv", ex->display(tout << "conflict: ") << "\n"; s().display(tout)); + validate_conflict(lits, eqs); ctx.set_conflict(ex); } @@ -217,7 +218,7 @@ namespace polysat { auto d = dependency(eq.var()); auto id = eq_constraint(p, q, d); TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n"); - m_core.assign_eh(id, false, s().lvl(eq)); + m_core.assign_eh(id, true, s().lvl(eq)); } // Core uses the propagate callback to add unit propagations to the trail.