diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index c03875f0b..06e6f6770 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -237,6 +237,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); diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index c7c93be07..d25f3e746 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -139,6 +139,7 @@ namespace intblast { rational get_value(expr* e) 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; }