diff --git a/scripts/update_api.py b/scripts/update_api.py index dc25f8df2..ad76b9be0 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1919,7 +1919,7 @@ _error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) _lib.Z3_set_error_handler.restype = None _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type] -Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.POINTER(ctypes.c_uint), ctypes.c_void_p) Z3_push_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) Z3_pop_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint) Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ae77cb4ea..953167fe9 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -984,14 +984,14 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); init_solver(c, s); - user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned n, expr* const* _literals) { + user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned nd, unsigned const* deps, unsigned n, expr* const* _literals) { Z3_ast_vector_ref * literals = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); mk_c(c)->save_object(literals); expr_ref pr(proof, mk_c(c)->m()); scoped_ast_vector _sc(literals); for (unsigned i = 0; i < n; ++i) literals->m_ast_vector.push_back(_literals[i]); - on_clause_eh(user_ctx, of_expr(pr.get()), of_ast_vector(literals)); + on_clause_eh(user_ctx, of_expr(pr.get()), nd, deps, of_ast_vector(literals)); }; to_solver_ref(s)->register_on_clause(user_context, _on_clause); auto& solver = *to_solver(s); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d1a856174..bac80b33e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11438,11 +11438,12 @@ def to_AstVectorObj(ptr,): # for UserPropagator we use a global dictionary, which isn't great code. _my_hacky_class = None -def on_clause_eh(ctx, p, clause): +def on_clause_eh(ctx, p, n, dep, clause): onc = _my_hacky_class p = _to_expr_ref(to_Ast(p), onc.ctx) clause = AstVector(to_AstVectorObj(clause), onc.ctx) - onc.on_clause(p, clause) + deps = [dep[i] for i in range(n)] + onc.on_clause(p, deps, clause) _on_clause_eh = Z3_on_clause_eh(on_clause_eh) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index a931bc523..36634b8a4 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1437,7 +1437,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_as Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb)); Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t)); Z3_DECLARE_CLOSURE(Z3_decide_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase)); -Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, Z3_ast_vector literals)); +Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals)); /** diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index e2a19446d..31d708733 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -126,7 +126,7 @@ public: if (m_empty) return; - if (hint && !is_rup(hint) && m_checker.check(hint)) { + if (hint && !is_rup(hint)) { auto clause1 = m_checker.clause(hint); if (clause1.size() != clause.size()) { mk_clause(clause1); @@ -239,8 +239,10 @@ public: class proof_cmds_imp : public proof_cmds { cmd_context& ctx; ast_manager& m; + arith_util m_arith; expr_ref_vector m_lits; app_ref m_proof_hint; + unsigned_vector m_deps; bool m_check = true; bool m_save = false; bool m_trim = false; @@ -266,11 +268,24 @@ class proof_cmds_imp : public proof_cmds { m_del = m.mk_app(symbol("del"), 0, nullptr, m.mk_proof_sort()); return m_del; } + + bool is_dep(expr* e) { + return m.is_proof(e) && symbol("deps") == to_app(e)->get_name(); + } + + void get_deps(expr* e) { + rational n; + bool is_int = false; + for (expr* arg : *to_app(e)) + if (m_arith.is_numeral(arg, n, is_int) && n.is_unsigned()) + m_deps.push_back(n.get_unsigned()); + } public: proof_cmds_imp(cmd_context& ctx): ctx(ctx), - m(ctx.m()), + m(ctx.m()), + m_arith(m), m_lits(m), m_proof_hint(m), m_assumption(m), @@ -280,7 +295,9 @@ public: void add_literal(expr* e) override { if (m.is_proof(e)) { - if (!m_proof_hint) + if (is_dep(e)) + get_deps(e); + else if (!m_proof_hint) m_proof_hint = to_app(e); } else if (!m.is_bool(e)) @@ -297,9 +314,10 @@ public: if (m_trim) trim().assume(m_lits); if (m_on_clause_eh) - m_on_clause_eh(m_on_clause_ctx, assumption(), m_lits.size(), m_lits.data()); + m_on_clause_eh(m_on_clause_ctx, assumption(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); + m_deps.reset(); } void end_infer() override { @@ -310,9 +328,10 @@ public: if (m_trim) trim().infer(m_lits, m_proof_hint); if (m_on_clause_eh) - m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_lits.size(), m_lits.data()); + m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); + m_deps.reset(); } void end_deleted() override { @@ -323,9 +342,10 @@ public: if (m_trim) trim().del(m_lits); if (m_on_clause_eh) - m_on_clause_eh(m_on_clause_ctx, del(), m_lits.size(), m_lits.data()); + m_on_clause_eh(m_on_clause_ctx, del(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); + m_deps.reset(); } void updt_params(params_ref const& p) override { diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index 56c4a1b7a..41f7ea7f7 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -266,7 +266,8 @@ namespace sat { m_clause.reset(); switch (j.get_kind()) { case justification::NONE: - m_clause.push_back(l); + if (l != null_literal) + m_clause.push_back(l); break; case justification::BINARY: m_clause.push_back(l); @@ -282,7 +283,7 @@ namespace sat { break; } std::sort(m_clause.begin(), m_clause.end()); - IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n"); + IF_VERBOSE(3, verbose_stream() << "add core {" << m_clause << "}\n"); auto& [clauses, id, in_core] = m_clauses.find(m_clause); in_core = true; insert_dep(id); @@ -337,7 +338,13 @@ namespace sat { } void proof_trim::assume(unsigned id, bool is_initial) { - std::sort(m_clause.begin(), m_clause.end()); + std::sort(m_clause.begin(), m_clause.end()); + unsigned j = 0; + sat::literal prev = null_literal; + for (unsigned i = 0; i < m_clause.size(); ++i) + if (m_clause[i] != prev) + prev = m_clause[j++] = m_clause[i]; + m_clause.shrink(j); if (unit_or_binary_occurs()) return; if (!m_conflict.empty() && m_clause.empty()) { diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index ac9e81311..e96ec91ab 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -312,7 +312,7 @@ namespace euf { for (unsigned i = 0; i < n; ++i) m_clause.push_back(literal2expr(lits[i])); auto hint = status2proof_hint(st); - m_on_clause(m_on_clause_ctx, hint, m_clause.size(), m_clause.data()); + m_on_clause(m_on_clause_ctx, hint, 0, nullptr, m_clause.size(), m_clause.data()); } void solver::on_proof(unsigned n, literal const* lits, sat::status st) { diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index 3bb2a1fdf..777961334 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -190,7 +190,7 @@ namespace smt { if (ctx.get_fparams().m_clause_proof) m_trail.push_back(info(st, v, p)); if (m_on_clause_eh) - m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data()); + m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data()); if (m_has_log) { init_pp_out(); auto& out = *m_pp_out; diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 40c0fa8fc..58904a12d 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -27,7 +27,7 @@ namespace user_propagator { typedef std::function pop_eh_t; typedef std::function created_eh_t; typedef std::function decide_eh_t; - typedef std::function on_clause_eh_t; + typedef std::function on_clause_eh_t; class plugin : public decl_plugin { public: