From 9373e1b7f50016c5d71a009260a17b9defc4e5ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2023 10:00:11 -0800 Subject: [PATCH] intblast debugging --- src/ast/euf/euf_bv_plugin.cpp | 3 ++- src/sat/smt/intblast_solver.cpp | 36 ++++++++++++++++++++----- src/sat/smt/intblast_solver.h | 3 +++ src/sat/smt/polysat/core.h | 11 ++++---- src/sat/smt/polysat_internalize.cpp | 40 ++++++++++++++++++++++----- src/sat/smt/polysat_model.cpp | 42 ++++++++++++++++++++++++++++- src/sat/smt/polysat_solver.cpp | 2 +- src/sat/smt/polysat_solver.h | 6 ++++- 8 files changed, 121 insertions(+), 22 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 4766cba12..f640b3ed0 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -343,7 +343,8 @@ namespace euf { enode* hi = mk_extract(n, cut, w - 1); enode* lo = mk_extract(n, 0, cut - 1); auto& i = info(n); - SASSERT(i.value); + if (!i.value) + i.value = n; i.hi = hi; i.lo = lo; i.cut = cut; diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index c269fee9c..0a38597e2 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -82,6 +82,7 @@ namespace intblast { m_core.reset(); m_vars.reset(); m_trail.reset(); + m_new_funs.reset(); m_solver = mk_smt2_solver(m, s.params(), symbol::null); expr_ref_vector es(m); @@ -228,12 +229,19 @@ namespace intblast { } continue; } + + if (m.is_ite(e)) { + m_trail.push_back(m.mk_ite(args.get(0), args.get(1), args.get(2))); + translated.insert(e, m_trail.back()); + continue; + } if (ap->get_family_id() != bv.get_family_id()) { bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); }); bool has_bv_sort = bv.is_bv(e); func_decl* f = ap->get_decl(); if (has_bv_arg) { + verbose_stream() << mk_pp(ap, m) << "\n"; // need to update args with mod where they are bit-vectors. NOT_IMPLEMENTED_YET(); } @@ -245,14 +253,17 @@ namespace intblast { domain.push_back(bv.is_bv_sort(s) ? a.mk_int() : s); } sort* range = bv.is_bv(e) ? a.mk_int() : e->get_sort(); - f = m.mk_fresh_func_decl(ap->get_decl()->get_name(), symbol("bv"), domain.size(), domain.data(), range); + func_decl* g = nullptr; + if (!m_new_funs.find(f, g)) { + g = m.mk_fresh_func_decl(ap->get_decl()->get_name(), symbol("bv"), domain.size(), domain.data(), range); + m_new_funs.insert(f, g); + } + f = g; } m_trail.push_back(m.mk_app(f, args)); translated.insert(e, m_trail.back()); - verbose_stream() << "translate " << mk_pp(e, m) << " " << has_bv_sort << "\n"; - if (has_bv_sort) m_vars.insert(e, { m_trail.back(), bv_size() }); @@ -329,7 +340,7 @@ namespace intblast { unsigned sz = hi - lo + 1; expr* new_arg = args.get(0); if (lo > 0) - new_arg = a.mk_div(new_arg, a.mk_int(rational::power_of_two(lo))); + new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo))); m_trail.push_back(new_arg); break; } @@ -386,12 +397,19 @@ namespace intblast { default: verbose_stream() << mk_pp(e, m) << "\n"; NOT_IMPLEMENTED_YET(); - } - verbose_stream() << "insert " << mk_pp(e, m) << " -> " << mk_pp(m_trail.back(), m) << "\n"; + } translated.insert(e, m_trail.back()); } + + TRACE("bv", + for (unsigned i = 0; i < es.size(); ++i) + tout << mk_pp(es.get(i), m) << " -> " << mk_pp(translated[es.get(i)], m) << "\n"; + ); + for (unsigned i = 0; i < es.size(); ++i) es[i] = translated[es.get(i)]; + + } rational solver::get_value(expr* e) const { @@ -414,4 +432,10 @@ namespace intblast { return m_core; } + std::ostream& solver::display(std::ostream& out) const { + if (m_solver) + m_solver->display(out); + return out; + } + } diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index 1df46c300..33d024be5 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -45,6 +45,7 @@ namespace intblast { arith_util a; scoped_ptr<::solver> m_solver; obj_map m_vars; + obj_map m_new_funs; expr_ref_vector m_trail; sat::literal_vector m_core; @@ -62,6 +63,8 @@ namespace intblast { sat::literal_vector const& unsat_core(); rational get_value(expr* e) const; + + std::ostream& display(std::ostream& out) const; }; } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index b70e70d9b..e43633620 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -115,11 +115,12 @@ namespace polysat { signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } - pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); } - pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); } - pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); } - pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); } - pdd bnot(pdd a) { return -a - 1; } + void lshr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); } + void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); } + void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); } + void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); } + + pdd bnot(pdd p) { return -p - 1; } pvar add_var(unsigned sz); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 0afcf06d4..4eeec3da4 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -84,9 +84,9 @@ namespace polysat { case OP_BMUL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break; case OP_BADD: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break; case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break; - case OP_BLSHR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break; - case OP_BSHL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break; - case OP_BAND: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break; + case OP_BLSHR: internalize_lshr(a); break; + case OP_BSHL: internalize_shl(a); break; + case OP_BAND: internalize_band(a); break; case OP_BOR: internalize_bor(a); break; case OP_BXOR: internalize_bxor(a); break; case OP_BNAND: if_unary(m_core.bnot); internalize_bnand(a); break; @@ -230,6 +230,34 @@ namespace polysat { internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); }); } + void solver::internalize_band(app* n) { + if (n->get_num_args() == 2) { + expr* x, * y; + VERIFY(bv.is_bv_and(n, x, y)); + m_core.band(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + } + else { + expr_ref z(n->get_arg(0), m); + for (unsigned i = 1; i < n->get_num_args(); ++i) { + z = bv.mk_bv_and(z, n->get_arg(i)); + ctx.internalize(z); + } + internalize_set(n, expr2pdd(z)); + } + } + + void solver::internalize_lshr(app* n) { + expr* x, * y; + VERIFY(bv.is_bv_lshr(n, x, y)); + m_core.lshr(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + } + + void solver::internalize_shl(app* n) { + expr* x, * y; + VERIFY(bv.is_bv_shl(n, x, y)); + m_core.shl(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + } + void solver::internalize_urem_i(app* rem) { expr* x, *y; euf::enode* n = expr2enode(rem); @@ -389,14 +417,12 @@ namespace polysat { } void solver::internalize_extract(app* e) { - auto p = var2pdd(expr2enode(e)->get_th_var(get_id())); - internalize_set(e, p); + var2pdd(expr2enode(e)->get_th_var(get_id())); } void solver::internalize_concat(app* e) { SASSERT(bv.is_concat(e)); - auto p = var2pdd(expr2enode(e)->get_th_var(get_id())); - internalize_set(e, p); + var2pdd(expr2enode(e)->get_th_var(get_id())); } void solver::internalize_par_unary(app* e, std::function const& fn) { diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp index 383a3f692..9a44e0abf 100644 --- a/src/sat/smt/polysat_model.cpp +++ b/src/sat/smt/polysat_model.cpp @@ -18,11 +18,34 @@ Author: #include "params/bv_rewriter_params.hpp" #include "sat/smt/polysat_solver.h" #include "sat/smt/euf_solver.h" +#include "ast/rewriter/bv_rewriter.h" namespace polysat { void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + + if (m_use_intblast_model) { + expr_ref value(m); + if (n->interpreted()) + value = n->get_expr(); + else if (to_app(n->get_expr())->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(value); + } + else { + rational r = m_intblast.get_value(n->get_expr()); + verbose_stream() << ctx.bpp(n) << " := " << r << "\n"; + value = bv.mk_numeral(r, get_bv_size(n)); + } + values.set(n->get_root_id(), value); + TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); + return; + } #if 0 auto p = expr2pdd(n->get_expr()); rational val; @@ -31,9 +54,24 @@ namespace polysat { #endif } + bool solver::add_dep(euf::enode* n, top_sort& dep) { + if (!is_app(n->get_expr())) + return false; + app* e = to_app(n->get_expr()); + if (n->num_args() == 0) { + dep.insert(n, nullptr); + return true; + } + if (e->get_family_id() != bv.get_family_id()) + return false; + for (euf::enode* arg : euf::enode_args(n)) + dep.add(n, arg->get_root()); + return true; + } + bool solver::check_model(sat::model const& m) const { - return false; + return true; } void solver::finalize_model(model& mdl) { @@ -53,6 +91,8 @@ namespace polysat { for (unsigned v = 0; v < get_num_vars(); ++v) if (m_var2pdd_valid.get(v, false)) out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n"; + if (m_use_intblast_model) + m_intblast.display(out); return out; } } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index ad4beb561..43f156c7d 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -40,7 +40,7 @@ namespace polysat { m_intblast(ctx), m_lemma(ctx.get_manager()) { - ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph())); + // ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph())); } unsigned solver::get_bv_size(euf::enode* n) { diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index f3435f364..7cf176b0c 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -119,6 +119,9 @@ namespace polysat { void internalize_bnor(app* n); void internalize_bnand(app* n); void internalize_bxnor(app* n); + void internalize_band(app* n); + void internalize_lshr(app* n); + void internalize_shl(app* n); template void internalize_le(app* n); void internalize_zero_extend(app* n); @@ -172,7 +175,7 @@ namespace polysat { std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; void collect_statistics(statistics& st) const override {} - euf::th_solver* clone(euf::solver& ctx) override { throw default_exception("nyi"); } + euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx, get_id()); } extension* copy(sat::solver* s) override { throw default_exception("nyi"); } void find_mutexes(literal_vector& lits, vector & mutexes) override {} void gc() override {} @@ -190,6 +193,7 @@ namespace polysat { bool unit_propagate() override; void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + bool add_dep(euf::enode* n, top_sort& dep) override; bool extract_pb(std::function& card, std::function& pb) override { return false; }