From 4b72e517b7b37affe410390b242fc6d56032e855 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Nov 2024 20:13:02 -0800 Subject: [PATCH] SLS: log clause , allow more frequent export of SLS state to SMT --- src/ast/sls/sls_arith_base.cpp | 40 +++++++++++++++++----------------- src/ast/sls/sls_euf_plugin.cpp | 10 +++++++++ src/ast/sls/sls_euf_plugin.h | 1 + src/ast/sls/sls_smt_plugin.cpp | 2 +- 4 files changed, 32 insertions(+), 21 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 8e68781ccba..0ede505196b 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -123,38 +123,37 @@ namespace sls { // distance to true template num_t arith_base::dtt(bool sign, num_t const& args, ineq const& ineq) const { - num_t zero{ 0 }; switch (ineq.m_op) { case ineq_kind::LE: if (sign) { if (args + ineq.m_coeff <= 0) return -ineq.m_coeff - args + 1; - return zero; + return num_t(0); } if (args + ineq.m_coeff <= 0) - return zero; + return num_t(0); return args + ineq.m_coeff; case ineq_kind::EQ: if (sign) { if (args + ineq.m_coeff == 0) return num_t(1); - return zero; + return num_t(0); } if (args + ineq.m_coeff == 0) - return zero; + return num_t(0); return num_t(1); case ineq_kind::LT: if (sign) { if (args + ineq.m_coeff < 0) return -ineq.m_coeff - args; - return zero; + return num_t(0); } if (args + ineq.m_coeff < 0) - return zero; + return num_t(0); return args + ineq.m_coeff + 1; default: UNREACHABLE(); - return zero; + return num_t(0); } } @@ -863,36 +862,36 @@ namespace sls { template typename arith_base::var_t arith_base::mk_op(arith_op_kind k, expr* e, expr* x, expr* y) { auto v = mk_var(e); - auto w = mk_term(x); + auto vx = mk_term(x); + auto vy = mk_term(y); unsigned idx = m_ops.size(); num_t val; switch (k) { case arith_op_kind::OP_MOD: - val = value(v) == 0 ? num_t(0) : mod(value(w), value(v)); + val = value(vy) == 0 ? num_t(0) : mod(value(v), value(vy)); break; case arith_op_kind::OP_REM: - if (value(v) == 0) + if (value(vy) == 0) val = 0; else { - val = value(w); - val %= value(v); + val = value(vx); + val %= value(vy); } break; case arith_op_kind::OP_IDIV: - val = value(v) == 0 ? num_t(0): div(value(w), value(v)); + val = value(vy) == 0 ? num_t(0): div(value(vx), value(vy)); break; case arith_op_kind::OP_DIV: - val = value(v) == 0? num_t(0) : value(w) / value(v); + val = value(vy) == 0? num_t(0) : value(vx) / value(vy); break; case arith_op_kind::OP_ABS: - val = abs(value(w)); + val = abs(value(vx)); break; default: NOT_IMPLEMENTED_YET(); break; } - verbose_stream() << "mk-op " << mk_bounded_pp(e, m) << "\n"; - m_ops.push_back({v, k, v, w}); + m_ops.push_back({v, k, vx, vy}); m_vars[v].m_def_idx = idx; m_vars[v].m_op = k; m_vars[v].set_value(val); @@ -1606,7 +1605,7 @@ namespace sls { bool arith_base::repair_idiv(op_def const& od) { auto v1 = value(od.m_arg1); auto v2 = value(od.m_arg2); - IF_VERBOSE(0, verbose_stream() << "todo repair div"); + IF_VERBOSE(0, verbose_stream() << "TODO repair div"); // bail return update(od.m_var, v2 == 0 ? num_t(0) : div(v1, v2)); } @@ -1615,7 +1614,7 @@ namespace sls { bool arith_base::repair_div(op_def const& od) { auto v1 = value(od.m_arg1); auto v2 = value(od.m_arg2); - IF_VERBOSE(0, verbose_stream() << "todo repair /"); + IF_VERBOSE(0, verbose_stream() << "TODO repair /"); // bail return update(od.m_var, v2 == 0 ? num_t(0) : v1 / v2); } @@ -2112,6 +2111,7 @@ namespace sls { auto const& vi = m_vars[v]; if (vi.m_def_idx == UINT_MAX) return true; + verbose_stream() << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"; TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); switch (vi.m_op) { case arith_op_kind::LAST_ARITH_OP: diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index ae04142c7be..fa00cf4db72 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -114,10 +114,19 @@ namespace sls { } // flip the last literal on the replay stack IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n"); + log_clause(lits); ctx.add_clause(lits); return flit; } + void euf_plugin::log_clause(sat::literal_vector const& lits) { + IF_VERBOSE(3, verbose_stream() << "block " << lits << "\n"; + for (auto lit : lits) + verbose_stream() << (lit.sign() ? "~" : "") << mk_bounded_pp(ctx.atom(lit.var()), m) << "\n"; + verbose_stream() << "\n"; + ); + } + void euf_plugin::propagate_literal(sat::literal lit) { SASSERT(ctx.is_true(lit)); auto e = ctx.atom(lit.var()); @@ -154,6 +163,7 @@ namespace sls { ++m_stats.m_num_conflicts; if (flit != sat::null_literal) ctx.flip(flit.var()); + log_clause(lits); }; if (lit.sign() && m.is_eq(e, x, y)) diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h index 71b0aabe27a..2c465e66f8e 100644 --- a/src/ast/sls/sls_euf_plugin.h +++ b/src/ast/sls/sls_euf_plugin.h @@ -56,6 +56,7 @@ namespace sls { sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); }; void validate_model(); + void log_clause(sat::literal_vector const& lits); public: euf_plugin(context& c); diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index 4e8d2f0bbcc..3d0d3e101d6 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -293,7 +293,7 @@ namespace sls { } void smt_plugin::export_from_sls() { - if (unsat().size() >= m_min_unsat_size) + if (unsat().size() > m_min_unsat_size) return; m_min_unsat_size = unsat().size(); export_phase_from_sls();