From f388f58a4ba44f31391a2b944c8af83c31e606a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2023 20:22:23 -0800 Subject: [PATCH] b-and, stats, reinsert variable to heap, debugging --- src/math/lp/lp_api.h | 4 ++++ src/sat/smt/arith_solver.cpp | 2 -- src/sat/smt/intblast_solver.cpp | 3 ++- src/sat/smt/intblast_solver.h | 2 +- src/sat/smt/polysat/core.cpp | 18 +++++++++++++-- src/sat/smt/polysat/core.h | 3 +++ src/sat/smt/polysat_internalize.cpp | 9 +++++++- src/sat/smt/polysat_model.cpp | 35 +++++++++++------------------ src/sat/smt/polysat_solver.cpp | 6 +++++ src/sat/smt/polysat_solver.h | 3 ++- 10 files changed, 55 insertions(+), 30 deletions(-) diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 021501ecd..50339e3ce 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -129,7 +129,11 @@ namespace lp_api { st.update("arith-gomory-cuts", m_gomory_cuts); st.update("arith-assume-eqs", m_assume_eqs); st.update("arith-branch", m_branch); +<<<<<<< HEAD st.update("arith-bv-axioms", m_bv_axioms); +======= + st.update("arith-band-axioms", m_band_axioms); +>>>>>>> c72780d9b (b-and, stats, reinsert variable to heap, debugging) } }; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 02849a8eb..078515184 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1212,8 +1212,6 @@ namespace arith { default: UNREACHABLE(); } - if (lia_check == l_true && !check_band_terms()) - lia_check = l_false; return lia_check; } diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 09241d42b..5c12d4061 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -257,6 +257,8 @@ namespace intblast { lbool r = m_solver->check_sat(es); + m_solver->collect_statistics(m_stats); + IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); if (r == l_false) { @@ -975,5 +977,4 @@ namespace intblast { st.copy(m_stats); } - } diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index d25f3e746..f4eb24b92 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -137,7 +137,7 @@ namespace intblast { sat::literal_vector const& unsat_core(); - rational get_value(expr* e) const; + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values); }; diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 8e779923d..a552bb9ab 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -119,7 +119,7 @@ namespace polysat { m_activity.pop_back(); m_justification.pop_back(); m_watch.pop_back(); - m_values.pop_back(); + m_values.pop_back(); m_var_queue.del_var_eh(v); } @@ -160,6 +160,7 @@ namespace polysat { s.add_eq_literal(m_var, m_value); return sat::check_result::CR_CONTINUE; case find_t::resource_out: + m_var_queue.unassign_var_eh(m_var); return sat::check_result::CR_GIVEUP; } UNREACHABLE(); @@ -342,8 +343,21 @@ namespace polysat { for (auto const& [sc, d, value] : m_constraint_index) out << sc << " " << d << " := " << value << "\n"; for (unsigned i = 0; i < m_vars.size(); ++i) - out << "p" << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; + out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; + m_var_queue.display(out << "vars ") << "\n"; return out; } + bool core::try_eval(pdd const& p, rational& r) { + auto q = subst(p); + if (!q.is_val()) + return false; + r = q.val(); + return true; + } + + void core::collect_statistics(statistics& st) const { + + } + } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index c6442a290..c3dddfece 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -104,6 +104,9 @@ namespace polysat { pdd value(rational const& v, unsigned sz); pdd subst(pdd const&); + bool try_eval(pdd const& p, rational& r); + + void collect_statistics(statistics& st) const; signed_constraint eq(pdd const& p) { return m_constraints.eq(p); } signed_constraint eq(pdd const& p, pdd const& q) { return m_constraints.eq(p - q); } diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 4496dc759..5e5647bd3 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -86,6 +86,7 @@ namespace polysat { case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break; case OP_BLSHR: internalize_lshr(a); break; case OP_BSHL: internalize_shl(a); break; + case OP_BASHR: internalize_ashr(a); break; case OP_BAND: internalize_band(a); break; case OP_BOR: internalize_bor(a); break; case OP_BXOR: internalize_bxor(a); break; @@ -148,7 +149,7 @@ namespace polysat { case OP_BSDIV_I: case OP_BSREM_I: case OP_BSMOD_I: - case OP_BASHR: + IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); NOT_IMPLEMENTED_YET(); return; @@ -254,6 +255,12 @@ namespace polysat { auto sc = m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n)); } + void solver::internalize_ashr(app* n) { + expr* x, * y; + VERIFY(bv.is_bv_ashr(n, x, y)); + auto sc = m_core.ashr(expr2pdd(x), expr2pdd(y), expr2pdd(n)); + } + void solver::internalize_shl(app* n) { expr* x, * y; VERIFY(bv.is_bv_shl(n, x, y)); diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp index 9a44e0abf..5bd8d4dc9 100644 --- a/src/sat/smt/polysat_model.cpp +++ b/src/sat/smt/polysat_model.cpp @@ -26,32 +26,18 @@ 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"); + m_intblast.add_value(n, mdl, values); return; } -#if 0 auto p = expr2pdd(n->get_expr()); rational val; - VERIFY(m_polysat.try_eval(p, val)); - values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n)); -#endif + 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)); + values.set(n->get_root_id(), bv.mk_numeral(val, get_bv_size(n))); } bool solver::add_dep(euf::enode* n, top_sort& dep) { @@ -78,6 +64,11 @@ namespace polysat { } + void solver::collect_statistics(statistics& st) const { + m_intblast.collect_statistics(st); + m_core.collect_statistics(st); + } + std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; } diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 43f156c7d..9f185b22d 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -184,6 +184,9 @@ namespace polysat { void solver::new_eq_eh(euf::th_eq const& eq) { auto v1 = eq.v1(), v2 = eq.v2(); + euf::enode* n = var2enode(v1); + if (!bv.is_bv(n->get_expr())) + return; pdd p = var2pdd(v1); pdd q = var2pdd(v2); auto sc = m_core.eq(p, q); @@ -197,6 +200,9 @@ namespace polysat { void solver::new_diseq_eh(euf::th_eq const& ne) { euf::theory_var v1 = ne.v1(), v2 = ne.v2(); + euf::enode* n = var2enode(v1); + if (!bv.is_bv(n->get_expr())) + return; pdd p = var2pdd(v1); pdd q = var2pdd(v2); auto sc = ~m_core.eq(p, q); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 7cf176b0c..f54bafb1c 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -121,6 +121,7 @@ namespace polysat { void internalize_bxnor(app* n); void internalize_band(app* n); void internalize_lshr(app* n); + void internalize_ashr(app* n); void internalize_shl(app* n); template void internalize_le(app* n); @@ -174,7 +175,7 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; 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 {} + void collect_statistics(statistics& st) const override; 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 {}