From 07dd1065dbcc7d1b076c5d2578fd74f808fa9c86 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Oct 2022 08:34:55 -0700 Subject: [PATCH] added API to monitor clause inferences See RELEASE_NOTES for more information examples pending. --- RELEASE_NOTES.md | 50 ++++++++++ scripts/update_api.py | 9 +- src/api/api_solver.cpp | 27 ++++++ src/api/c++/z3++.h | 27 +++++- src/api/dotnet/CMakeLists.txt | 1 + src/api/dotnet/OnClause.cs | 102 ++++++++++++++++++++ src/api/python/z3/z3.py | 52 ++++++++-- src/api/z3_api.h | 19 ++++ src/ast/ast.cpp | 8 ++ src/ast/ast.h | 2 + src/ast/ast_ll_pp.cpp | 1 + src/sat/sat_solver.h | 10 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 + src/sat/smt/bv_internalize.cpp | 2 +- src/sat/smt/euf_proof.cpp | 50 ++++++---- src/sat/smt/euf_solver.cpp | 8 ++ src/sat/smt/euf_solver.h | 12 ++- src/sat/smt/q_solver.cpp | 16 +-- src/smt/qi_queue.cpp | 10 ++ src/smt/smt_clause_proof.cpp | 134 +++++++++++++++----------- src/smt/smt_clause_proof.h | 18 +++- src/smt/smt_context.h | 6 ++ src/smt/smt_internalizer.cpp | 6 +- src/smt/smt_justification.cpp | 3 +- src/smt/smt_kernel.cpp | 4 + src/smt/smt_kernel.h | 2 + src/smt/smt_solver.cpp | 4 + src/smt/tactic/smt_tactic_core.cpp | 15 ++- src/solver/combined_solver.cpp | 6 +- src/solver/solver.h | 2 +- src/solver/tactic2solver.cpp | 4 + src/tactic/tactic.h | 4 + src/tactic/tactical.cpp | 4 + src/tactic/user_propagator_base.h | 5 + 34 files changed, 505 insertions(+), 122 deletions(-) create mode 100644 src/api/dotnet/OnClause.cs diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index b1fe88e06..0ec6c04b1 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,56 @@ Version 4.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. +Version 4.12.0 +============== +- add clause logging API. + - The purpose of logging API and self-checking is to enable an array of use cases. + - proof mining (what instantiations did Z3 use)? + - A refresh of the AxiomProfiler could use the logging API. The (brittle) trace feature should be deprecated. + - debugging + - a built-in self certifier implements a custom proof checker for the format used by the new solver (sat.euf=true). + - other potential options: + - integration into certified tool chains + - interpolation + - Z3_register_on_clause (also exposed over C++, Python and .Net) + - it applies to z3's main CDCL(T) core and a new CDCL(T) core (sat.euf=true). + - The added API function allows to register a callback for when clauses are inferred + More precisely, when clauses are assumed (as part of input), deleted, or deduced. + Clauses that are deduced by the CDCL SAT engine using standard inferences are marked as 'rup'. + Clauses that are deduced by theories are marked by default by 'smt', and when more detailed information + is available with proof hints or proof objects. Instantations are considered useful to track so they + are logged using terms of the form (inst (not (forall (x) body)) body[t/x] (bind t)), where + 'inst' is a name of a function that produces a proof term representing the instantiation. +- add options for proof logging, trimming, and checking for the new core. + - sat.smt.proof (symbol) add SMT proof to file (default: ) + - sat.smt.proof.check (bool) check SMT proof while it is created (default: false) + - it applies a custom self-validator. The self-validator comprises of several small checkers and represent a best-effort + validation mechanism. If there are no custom validators associated with inferences, or the custom validators fail to certify + inferences, the self-validator falls back to invoking z3 (SMT) solving on the lemma. + - euf - propagations and conflicts from congruence closure (theory of equality and uninterpreted functions) are checked + based on a proof format that tracks uses of congruence closure and equalities. It only performs union find operations. + - tseitin - clausification steps are checked for Boolean operators. + - farkas, bound, implies_eq - arithmetic inferences that can be justified using a combination of Farkas lemma and cuts are checked. + Note: the arithmetic solver may produce proof hints that the proof checker cannot check. It is mainly a limitation + of the arithmetic solver not pulling relevant information. Ensuring a tight coupling with proof hints and the validator + capabilites is open ended future work and good material for theses. + - bit-vector inferences - are treated as trusted (there is no validation, it always blindly succeeds) + - arrays, datatypes - there is no custom validation for other theories at present. Lemmas are validated using SMT. + - sat.smt.proof.check_rup (bool) apply forward RUP proof checking (default: true) + - this option can incur significant runtime overhead. Effective proof checking relies on first trimming + proofs into a format where dependencies are tracked and then checking relevant inferences. + Turn this option off if you just want to check theory inferences. +- add options to validate proofs offline. It applies to proofs saved when sat.smt.proof is set to a valid file name. + - solver.proof.check (bool) check proof logs (default: true) + - the option sat.smt.proof_check_rup can be used to control what is checked + - solver.proof.save (bool) save proof log into a proof object that can be extracted using (get-proof) (default: false) + - experimental: saves a proof log into a term + - solver.proof.trim (bool) trim the offline proof and print the trimmed proof to the console + - experimental: performs DRUP trimming to reduce the set of hypotheses and inferences relevant to derive the empty clause. +- JS support for Arrays, thanks to Walden Yan +- More portable memory allocation, thanks to Nuno Lopes (avoid custom handling to calculate memory usage) + + Version 4.11.2 ============== - add error handling to fromString method in JavaScript diff --git a/scripts/update_api.py b/scripts/update_api.py index 41a9face5..a9753ec23 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -339,6 +339,10 @@ def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handl _elems.Check(ctx) return ceh +def Z3_solver_register_on_clause(ctx, s, user_ctx, on_clause_eh, _elems = Elementaries(_lib.Z3_solver_register_on_clause)): + _elems.f(ctx, s, user_ctx, on_clause_eh) + _elems.Check(ctx) + def Z3_solver_propagate_init(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh, _elems = Elementaries(_lib.Z3_solver_propagate_init)): _elems.f(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh) _elems.Check(ctx) @@ -1315,7 +1319,8 @@ z3_ml_callbacks = frozenset([ 'Z3_solver_propagate_eq', 'Z3_solver_propagate_diseq', 'Z3_solver_propagate_created', - 'Z3_solver_propagate_decide' + 'Z3_solver_propagate_decide', + 'Z3_solver_register_on_clause' ]) def mk_ml(ml_src_dir, ml_output_dir): @@ -1844,6 +1849,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_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) @@ -1855,6 +1861,7 @@ Z3_eq_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_ Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +_lib.Z3_solver_register_on_clause.restype = None _lib.Z3_solver_propagate_init.restype = None _lib.Z3_solver_propagate_final.restype = None _lib.Z3_solver_propagate_fixed.restype = None diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 963a57666..ab285be06 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -907,6 +907,33 @@ extern "C" { ~api_context_obj() override { dealloc(c); } }; + struct scoped_ast_vector { + Z3_ast_vector_ref* v; + scoped_ast_vector(Z3_ast_vector_ref* v): v(v) { v->inc_ref(); } + ~scoped_ast_vector() { v->dec_ref(); } + }; + + void Z3_API Z3_solver_register_on_clause( + Z3_context c, + Z3_solver s, + void* user_context, + Z3_on_clause_eh on_clause_eh) { + 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) { + 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)); + }; + to_solver_ref(s)->register_on_clause(user_context, _on_clause); + Z3_CATCH; + } + void Z3_API Z3_solver_propagate_init( Z3_context c, Z3_solver s, diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0275a22e1..553e71287 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -158,7 +158,7 @@ namespace z3 { class context { private: friend class user_propagator_base; - bool m_enable_exceptions; + bool m_enable_exceptions = true; rounding_mode m_rounding_mode; Z3_context m_ctx = nullptr; void init(config & c) { @@ -2670,10 +2670,10 @@ namespace z3 { public: struct simple {}; struct translate {}; - solver(context & c):object(c) { init(Z3_mk_solver(c)); } - solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); } + solver(context & c):object(c) { init(Z3_mk_solver(c)); check_error(); } + solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); check_error(); } solver(context & c, Z3_solver s):object(c) { init(s); } - solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); } + solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); } solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); } solver(solver const & s):object(s) { init(s.m_solver); } ~solver() { Z3_solver_dec_ref(ctx(), m_solver); } @@ -4059,6 +4059,25 @@ namespace z3 { return expr(ctx(), r); } + typedef std::function on_clause_eh_t; + + class on_clause { + context& c; + on_clause_eh_t m_on_clause; + + static void _on_clause_eh(void* _ctx, Z3_ast _proof, Z3_ast_vector _literals) { + on_clause* ctx = static_cast(_ctx); + expr_vector lits(ctx->c, _literals); + expr proof(ctx->c, _proof); + ctx->m_on_clause(proof, lits); + } + public: + on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) { + m_on_clause = on_clause_eh; + Z3_solver_register_on_clause(c, s, this, _on_clause_eh); + c.check_error(); + } + }; class user_propagator_base { diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index b2ba590ce..a9344aa86 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -87,6 +87,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE NativeFuncInterp.cs NativeModel.cs NativeSolver.cs + OnClause.cs Optimize.cs ParamDescrs.cs Params.cs diff --git a/src/api/dotnet/OnClause.cs b/src/api/dotnet/OnClause.cs new file mode 100644 index 000000000..686318928 --- /dev/null +++ b/src/api/dotnet/OnClause.cs @@ -0,0 +1,102 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + OnClause.cs + +Abstract: + + Callback on clause inferences + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-19 + +Notes: + + +--*/ + +using System; +using System.Diagnostics; +using System.Linq; +using System.Collections.Generic; +using System.Runtime.InteropServices; + +namespace Microsoft.Z3 +{ + + using Z3_context = System.IntPtr; + using Z3_solver = System.IntPtr; + using voidp = System.IntPtr; + using Z3_ast = System.IntPtr; + using Z3_ast_vector = System.IntPtr; + + + /// + /// OnClause - clause inference callback + /// + public class OnClause : IDisposable + { + /// + /// Delegate type for when clauses are inferred. + /// An inference is a pair comprising of + /// - a proof (hint). A partial (or comprehensive) derivation justifying the inference. + /// - a clause (vector of literals) + /// The life-time of the proof hint and clause vector is limited to the scope of the callback. + /// should the callback want to store hints or clauses it will need to call Dup on the hints + /// and/or extract literals from the clause, respectively. + /// + public delegate void OnClauseEh(Expr proof_hint, ASTVector clause); + + + // access managed objects through a static array. + // thread safety is ignored for now. + GCHandle gch; + Solver solver; + Context ctx; + OnClauseEh on_clause; + + Native.Z3_on_clause_eh on_clause_eh; + + static void _on_clause(voidp ctx, Z3_ast _proof_hint, Z3_ast_vector _clause) + { + var onc = (OnClause)GCHandle.FromIntPtr(ctx).Target; + using var proof_hint = Expr.Create(onc.ctx, _proof_hint); + using var clause = new ASTVector(onc.ctx, _clause); + onc.on_clause(proof_hint, clause); + } + + /// + /// OnClause constructor + /// + public OnClause(Solver s, OnClauseEh onc) + { + gch = GCHandle.Alloc(this); + solver = s; + ctx = solver.Context; + on_clause = onc; + on_clause_eh = _on_clause; + Native.Z3_solver_register_on_clause(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), on_clause_eh); + } + + /// + /// Release private memory. + /// + ~OnClause() + { + Dispose(); + } + + /// + /// Must be called. The object will not be garbage collected automatically even if the context is disposed + /// + public virtual void Dispose() + { + if (!gch.IsAllocated) + return; + gch.Free(); + } + } +} diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index ca3bc6f53..bbe212453 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11301,6 +11301,45 @@ def TransitiveClosure(f): """ return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx) +def to_Ast(ptr,): + ast = Ast(ptr) + super(ctypes.c_void_p, ast).__init__(ptr) + return ast + +def to_ContextObj(ptr,): + ctx = ContextObj(ptr) + super(ctypes.c_void_p, ctx).__init__(ptr) + return ctx + +def to_AstVectorObj(ptr,): + v = AstVectorObj(ptr) + super(ctypes.c_void_p, v).__init__(ptr) + return v + +# NB. my-hacky-class only works for a single instance of OnClause +# it should be replaced with a proper correlation between OnClause +# and object references that can be passed over the FFI. +# for UserPropagator we use a global dictionary, which isn't great code. + +_my_hacky_class = None +def on_clause_eh(ctx, p, 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) + +_on_clause_eh = Z3_on_clause_eh(on_clause_eh) + +class OnClause: + def __init__(self, s, on_clause): + self.s = s + self.ctx = s.ctx + self.on_clause = on_clause + self.idx = 22 + global _my_hacky_class + _my_hacky_class = self + Z3_solver_register_on_clause(self.ctx.ref(), self.s.solver, self.idx, _on_clause_eh) + class PropClosures: def __init__(self): @@ -11358,11 +11397,6 @@ def user_prop_pop(ctx, cb, num_scopes): prop.cb = cb prop.pop(num_scopes) -def to_ContextObj(ptr,): - ctx = ContextObj(ptr) - super(ctypes.c_void_p, ctx).__init__(ptr) - return ctx - def user_prop_fresh(ctx, _new_ctx): _prop_closures.set_threaded() @@ -11377,10 +11411,6 @@ def user_prop_fresh(ctx, _new_ctx): _prop_closures.set(new_prop.id, new_prop) return new_prop.id -def to_Ast(ptr,): - ast = Ast(ptr) - super(ctypes.c_void_p, ast).__init__(ptr) - return ast def user_prop_fixed(ctx, cb, id, value): prop = _prop_closures.get(ctx) @@ -11442,6 +11472,7 @@ _user_prop_eq = Z3_eq_eh(user_prop_eq) _user_prop_diseq = Z3_eq_eh(user_prop_diseq) _user_prop_decide = Z3_decide_eh(user_prop_decide) + def PropagateFunction(name, *sig): """Create a function that gets tracked by user propagator. Every term headed by this function symbol is tracked. @@ -11462,7 +11493,8 @@ def PropagateFunction(name, *sig): dom[i] = sig[i].ast ctx = rng.ctx return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx) - + + class UserPropagateBase: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9955f91be..1100d60dd 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1433,6 +1433,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, Z3_lbool* phase)); +Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, Z3_ast_vector literals)); /** @@ -6877,6 +6878,24 @@ extern "C" { */ void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]); + /** + \brief register a callback to that retrieves assumed, inferred and deleted clauses during search. + + \param c - context. + \param s - solver object. + \param user_context - a context used to maintain state for callbacks. + \param on_clause_eh - a callback that is invoked by when a clause is + - asserted to the CDCL engine (corresponding to an input clause after pre-processing) + - inferred by CDCL(T) using either a SAT or theory conflict/propagation + - deleted by the CDCL(T) engine + + def_API('Z3_solver_register_on_clause', VOID, (_in(CONTEXT), _in(SOLVER), _in(VOID_PTR), _fnptr(Z3_on_clause_eh))) + */ + void Z3_API Z3_solver_register_on_clause( + Z3_context c, + Z3_solver s, + void* user_context, + Z3_on_clause_eh on_clause_eh); /** \brief register a user-properator with the solver. diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f9bdc3414..50b9e5a4d 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1969,6 +1969,14 @@ app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, return mk_app(fid, k, 0, nullptr, 3, args); } +app * ast_manager::mk_app(symbol const& name, unsigned n, expr* const* args, sort* range) { + ptr_buffer sorts; + for (unsigned i = 0; i < n; ++i) + sorts.push_back(args[i]->get_sort()); + return mk_app(mk_func_decl(name, n, sorts.data(), range), n, args); +} + + sort * ast_manager::mk_sort(symbol const & name, sort_info * info) { unsigned sz = sort::get_obj_size(); void * mem = allocate_node(sz); diff --git a/src/ast/ast.h b/src/ast/ast.h index 511c2cee0..ce9de96d4 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1883,6 +1883,8 @@ public: return mk_app(decl, 3, args); } + app * mk_app(symbol const& name, unsigned n, expr* const* args, sort* range); + app * mk_const(func_decl * decl) { SASSERT(decl->get_arity() == 0); return mk_app(decl, static_cast(0), static_cast(nullptr)); diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index 5de98c644..d04777eb7 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -86,6 +86,7 @@ class ll_printer { default: display_child_ref(n); } + } template diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 64ee209c9..2b341185f 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -432,17 +432,17 @@ namespace sat { } void checkpoint() { - if (!m_checkpoint_enabled) return; - if (limit_reached()) { + if (!m_checkpoint_enabled) + return; + if (limit_reached()) throw solver_exception(Z3_CANCELED_MSG); - } - if (memory_exceeded()) { + if (memory_exceeded()) throw solver_exception(Z3_MAX_MEMORY_MSG); - } } void set_par(parallel* p, unsigned id); bool canceled() { return !m_rlimit.inc(); } config const& get_config() const { return m_config; } + void set_drat(bool d) { m_config.m_drat = d; } drat& get_drat() { return m_drat; } drat* get_drat_ptr() { return &m_drat; } void set_incremental(bool b) { m_config.m_incremental = b; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5c1859258..6fb936435 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -661,6 +661,10 @@ public: return ext; } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + ensure_euf()->register_on_clause(ctx, on_clause); + } + void user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 4cc161829..cffd62acd 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -772,6 +772,6 @@ namespace bv { eqs.push_back(~eq); } TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";); - s().add_clause(eqs.size(), eqs.data(), sat::status::th(m_is_redundant, get_id())); + add_clause(eqs); } } diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index bfda8aad6..906e6e068 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -25,19 +25,25 @@ namespace euf { if (m_proof_initialized) return; - if (s().get_config().m_drat && - (get_config().m_lemmas2console || - s().get_config().m_smt_proof_check || - s().get_config().m_smt_proof.is_non_empty_string())) { + if (m_on_clause) + s().set_drat(true); + + if (!s().get_config().m_drat) + return; - get_drat().add_theory(get_id(), symbol("euf")); - get_drat().add_theory(m.get_basic_family_id(), symbol("bool")); - TRACE("euf", tout << "init-proof " << s().get_config().m_smt_proof << "\n"); - if (s().get_config().m_smt_proof.is_non_empty_string()) - m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out); - get_drat().set_clause_eh(*this); - m_proof_initialized = true; - } + if (!get_config().m_lemmas2console && + !s().get_config().m_smt_proof_check && + !m_on_clause && + !s().get_config().m_smt_proof.is_non_empty_string()) + return; + + get_drat().add_theory(get_id(), symbol("euf")); + get_drat().add_theory(m.get_basic_family_id(), symbol("bool")); + + if (s().get_config().m_smt_proof.is_non_empty_string()) + m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out); + get_drat().set_clause_eh(*this); + m_proof_initialized = true; } /** @@ -135,7 +141,6 @@ namespace euf { ast_manager& m = s.get_manager(); func_decl_ref cc(m), cc_comm(m); sort* proof = m.mk_proof_sort(); - ptr_buffer sorts; expr_ref_vector& args = s.m_expr_args; args.reset(); if (m_cc_head < m_cc_tail) { @@ -161,12 +166,8 @@ namespace euf { for (unsigned i = m_cc_head; i < m_cc_tail; ++i) { auto const& [a, b, ts, comm] = s.m_explain_cc[i]; args.push_back(cc_proof(comm, m.mk_eq(a, b))); - } - for (auto * arg : args) - sorts.push_back(arg->get_sort()); - - func_decl* f = m.mk_func_decl(th, sorts.size(), sorts.data(), proof); - return m.mk_app(f, args); + } + return m.mk_app(th, args.size(), args.data(), proof); } smt_proof_hint* solver::mk_smt_clause(symbol const& n, unsigned nl, literal const* lits) { @@ -304,6 +305,17 @@ namespace euf { on_lemma(n, lits, st); on_proof(n, lits, st); on_check(n, lits, st); + on_clause_eh(n, lits, st); + } + + void solver::on_clause_eh(unsigned n, literal const* lits, sat::status st) { + if (!m_on_clause) + return; + m_clause.reset(); + 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()); } void solver::on_proof(unsigned n, literal const* lits, sat::status st) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 128f6ecc9..df36501dd 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -1113,6 +1113,14 @@ namespace euf { return true; } + void solver::register_on_clause( + void* ctx, + user_propagator::on_clause_eh_t& on_clause) { + m_on_clause_ctx = ctx; + m_on_clause = on_clause; + init_proof(); + } + void solver::user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 9983a48dd..d4729dcfe 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -123,8 +123,10 @@ namespace euf { sat::lookahead* m_lookahead = nullptr; ast_manager* m_to_m; sat::sat_internalizer* m_to_si; - scoped_ptr m_ackerman; - user_solver::solver* m_user_propagator = nullptr; + scoped_ptr m_ackerman; + user_propagator::on_clause_eh_t m_on_clause; + void* m_on_clause_ctx = nullptr; + user_solver::solver* m_user_propagator = nullptr; th_solver* m_qsolver = nullptr; unsigned m_generation = 0; std::string m_reason_unknown; @@ -221,6 +223,7 @@ namespace euf { void on_lemma(unsigned n, literal const* lits, sat::status st); void on_proof(unsigned n, literal const* lits, sat::status st); void on_check(unsigned n, literal const* lits, sat::status st); + void on_clause_eh(unsigned n, literal const* lits, sat::status st); std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits); void display_assume(std::ostream& out, unsigned n, literal const* lits); void display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint); @@ -487,6 +490,11 @@ namespace euf { // diagnostics func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; } + // clause tracing + void register_on_clause( + void* ctx, + user_propagator::on_clause_eh_t& on_clause); + // user propagator void user_propagate_init( void* ctx, diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 7fd7be97e..a94008074 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -389,26 +389,16 @@ namespace q { expr* q_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); expr_ref_vector args(m); - ptr_buffer sorts; expr_ref binding(m); sort* range = m.mk_proof_sort(); - func_decl* d; for (unsigned i = 0; i < m_num_bindings; ++i) args.push_back(m_bindings[i]); - for (expr* arg : args) - sorts.push_back(arg->get_sort()); - d = m.mk_func_decl(symbol("bind"), args.size(), sorts.data(), range); - binding = m.mk_app(d, args); + binding = m.mk_app(symbol("bind"), args.size(), args.data(), range); args.reset(); - sorts.reset(); for (unsigned i = 0; i < m_num_literals; ++i) args.push_back(s.literal2expr(~m_literals[i])); - args.push_back(binding); - for (expr* arg : args) - sorts.push_back(arg->get_sort()); - - d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range); - return m.mk_app(d, args); + args.push_back(binding); + return m.mk_app(symbol("inst"), args.size(), args.data(), range); } } diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index f8fbe739e..a1402839d 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -304,6 +304,16 @@ namespace smt { } m_instances.push_back(pr1); } + else if (m_context.on_clause_active()) { + expr_ref_vector bindings_e(m), args(m); + for (unsigned i = 0; i < num_bindings; ++i) + bindings_e.push_back(bindings[i]->get_expr()); + args.push_back(m.mk_not(q)); + args.push_back(instance); + args.push_back(m.mk_app(symbol("bind"), num_bindings, bindings_e.data(), m.mk_proof_sort())); + pr1 = m.mk_app(symbol("inst"), args.size(), args.data(), m.mk_proof_sort()); + m_instances.push_back(pr1); + } TRACE("qi_queue", tout << mk_pp(lemma, m) << "\n#" << lemma->get_id() << ":=\n" << mk_ll_pp(lemma, m);); m_stats.m_num_instances++; unsigned gen = get_new_gen(q, generation, ent.m_cost); diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index 9722d95c0..a2bc381e4 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -36,91 +36,113 @@ namespace smt { } } - proof* clause_proof::justification2proof(justification* j) { - return (m.proofs_enabled() && j) ? j->mk_proof(ctx.get_cr()) : nullptr; + proof* clause_proof::justification2proof(status st, justification* j) { + proof* r = nullptr; + if (j) + r = j->mk_proof(ctx.get_cr()); + if (r) + return r; + if (!m_on_clause_active) + return nullptr; + switch (st) { + case status::assumption: + return m.mk_const("assumption", m.mk_proof_sort()); + case status::lemma: + return m.mk_const("rup", m.mk_proof_sort()); + case status::th_lemma: + case status::th_assumption: + return m.mk_const("smt", m.mk_proof_sort()); + case status::deleted: + return m.mk_const("del", m.mk_proof_sort()); + } + UNREACHABLE(); + return nullptr; } void clause_proof::add(clause& c) { - if (ctx.get_fparams().m_clause_proof) { - justification* j = c.get_justification(); - proof_ref pr(justification2proof(j), m); - CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";); - update(c, kind2st(c.get_kind()), pr); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + justification* j = c.get_justification(); + auto st = kind2st(c.get_kind()); + proof_ref pr(justification2proof(st, j), m); + CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";); + update(c, st, pr); } void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) { - if (ctx.get_fparams().m_clause_proof) { - proof_ref pr(justification2proof(j), m); - CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";); - m_lits.reset(); - for (unsigned i = 0; i < n; ++i) { - m_lits.push_back(ctx.literal2expr(lits[i])); - } - update(kind2st(k), m_lits, pr); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + auto st = kind2st(k); + proof_ref pr(justification2proof(st, j), m); + CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";); + m_lits.reset(); + for (unsigned i = 0; i < n; ++i) + m_lits.push_back(ctx.literal2expr(lits[i])); + update(st, m_lits, pr); } void clause_proof::shrink(clause& c, unsigned new_size) { - if (ctx.get_fparams().m_clause_proof) { - m_lits.reset(); - for (unsigned i = 0; i < new_size; ++i) { - m_lits.push_back(ctx.literal2expr(c[i])); - } - update(status::lemma, m_lits, nullptr); - for (unsigned i = new_size; i < c.get_num_literals(); ++i) { - m_lits.push_back(ctx.literal2expr(c[i])); - } - update(status::deleted, m_lits, nullptr); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + m_lits.reset(); + for (unsigned i = 0; i < new_size; ++i) + m_lits.push_back(ctx.literal2expr(c[i])); + proof* p = justification2proof(status::lemma, nullptr); + update(status::lemma, m_lits, p); + for (unsigned i = new_size; i < c.get_num_literals(); ++i) + m_lits.push_back(ctx.literal2expr(c[i])); + p = justification2proof(status::deleted, nullptr); + update(status::deleted, m_lits, p); } void clause_proof::add(literal lit, clause_kind k, justification* j) { - if (ctx.get_fparams().m_clause_proof) { - m_lits.reset(); - m_lits.push_back(ctx.literal2expr(lit)); - proof* pr = justification2proof(j); - update(kind2st(k), m_lits, pr); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + m_lits.reset(); + m_lits.push_back(ctx.literal2expr(lit)); + auto st = kind2st(k); + proof* pr = justification2proof(st, j); + update(st, m_lits, pr); } void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) { - if (ctx.get_fparams().m_clause_proof) { - m_lits.reset(); - m_lits.push_back(ctx.literal2expr(lit1)); - m_lits.push_back(ctx.literal2expr(lit2)); - proof* pr = justification2proof(j); - m_trail.push_back(info(kind2st(k), m_lits, pr)); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + m_lits.reset(); + m_lits.push_back(ctx.literal2expr(lit1)); + m_lits.push_back(ctx.literal2expr(lit2)); + auto st = kind2st(k); + proof* pr = justification2proof(st, j); + update(st, m_lits, pr); } void clause_proof::del(clause& c) { - update(c, status::deleted, nullptr); + update(c, status::deleted, justification2proof(status::deleted, nullptr)); } void clause_proof::update(status st, expr_ref_vector& v, proof* p) { TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";); - IF_VERBOSE(3, verbose_stream() << st << " " << v << "\n"); - m_trail.push_back(info(st, v, p)); + 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()); } void clause_proof::update(clause& c, status st, proof* p) { - if (ctx.get_fparams().m_clause_proof) { - m_lits.reset(); - for (literal lit : c) { - m_lits.push_back(ctx.literal2expr(lit)); - } - update(st, m_lits, p); - } + if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) + return; + m_lits.reset(); + for (literal lit : c) + m_lits.push_back(ctx.literal2expr(lit)); + update(st, m_lits, p); } proof_ref clause_proof::get_proof(bool inconsistent) { TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";); - if (!ctx.get_fparams().m_clause_proof) { + if (!ctx.get_fparams().m_clause_proof) return proof_ref(m); - } proof_ref_vector ps(m); for (auto& info : m_trail) { expr_ref fact = mk_or(info.m_clause); @@ -143,12 +165,10 @@ namespace smt { break; } } - if (inconsistent) { + if (inconsistent) ps.push_back(m.mk_false()); - } - else { + else ps.push_back(m.mk_const("clause-trail-end", m.mk_bool_sort())); - } return proof_ref(m.mk_clause_trail(ps.size(), ps.data()), m); } diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h index e78c9943c..f15d0ffe0 100644 --- a/src/smt/smt_clause_proof.h +++ b/src/smt/smt_clause_proof.h @@ -28,6 +28,7 @@ Revision History: #include "smt/smt_theory.h" #include "smt/smt_clause.h" +#include "tactic/user_propagator_base.h" namespace smt { class context; @@ -50,14 +51,17 @@ namespace smt { proof_ref m_proof; info(status st, expr_ref_vector& v, proof* p): m_status(st), m_clause(v), m_proof(p, m_clause.m()) {} }; - context& ctx; - ast_manager& m; + context& ctx; + ast_manager& m; expr_ref_vector m_lits; - vector m_trail; + vector m_trail; + bool m_on_clause_active = false; + user_propagator::on_clause_eh_t m_on_clause_eh; + void* m_on_clause_ctx = nullptr; void update(status st, expr_ref_vector& v, proof* p); void update(clause& c, status st, proof* p); status kind2st(clause_kind k); - proof* justification2proof(justification* j); + proof* justification2proof(status st, justification* j); public: clause_proof(context& ctx); void shrink(clause& c, unsigned new_size); @@ -67,6 +71,12 @@ namespace smt { void add(unsigned n, literal const* lits, clause_kind k, justification* j); void del(clause& c); proof_ref get_proof(bool inconsistent); + bool on_clause_active() const { return m_on_clause_active; } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) { + m_on_clause_eh = on_clause; + m_on_clause_ctx = ctx; + m_on_clause_active = !!m_on_clause_eh; + } }; std::ostream& operator<<(std::ostream& out, clause_proof::status st); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7ca2e1c63..4a5f64926 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1706,6 +1706,12 @@ namespace smt { void get_units(expr_ref_vector& result); + bool on_clause_active() const { return m_clause_proof.on_clause_active(); } + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) { + m_clause_proof.register_on_clause(ctx, on_clause); + } + /* * user-propagator */ diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index ac433c602..2483b2ca4 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1626,9 +1626,11 @@ namespace smt { } mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); } - else { + else if (pr && on_clause_active()) + // support logging of quantifier instantiations and other more detailed information + mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); + else mk_clause(num_lits, lits, nullptr); - } } void context::mk_root_clause(literal l1, literal l2, proof * pr) { diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 0124a1810..d2a8aa2e6 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -82,7 +82,8 @@ namespace smt { } proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) { - SASSERT(m_antecedent); + if (!m_antecedent) + return nullptr; ast_manager& m = cr.get_manager(); proof_ref_vector prs(m); proof * pr = cr.get_proof(m_antecedent); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 8f442596c..ae3338f52 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -260,6 +260,10 @@ namespace smt { m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } + void kernel::register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) { + m_imp->m_kernel.register_on_clause(ctx, on_clause); + } + void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_imp->m_kernel.user_propagate_register_fixed(fixed_eh); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 4fa840f5e..fa4a48406 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -290,6 +290,8 @@ namespace smt { */ static void collect_param_descrs(param_descrs & d); + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause); + /** \brief initialize a user-propagator "theory" */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 61c6de377..61c7fdda7 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -212,6 +212,10 @@ namespace { return m_context.get_trail(max_level); } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + m_context.register_on_clause(ctx, on_clause); + } + void user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index c45165d79..5527f12f5 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -323,7 +323,13 @@ public: user_propagator::eq_eh_t m_diseq_eh; user_propagator::created_eh_t m_created_eh; user_propagator::decide_eh_t m_decide_eh; - + void* m_on_clause_ctx = nullptr; + user_propagator::on_clause_eh_t m_on_clause_eh; + + void on_clause_delay_init() { + if (m_on_clause_eh) + m_ctx->register_on_clause(m_on_clause_ctx, m_on_clause_eh); + } void user_propagate_delay_init() { if (!m_user_ctx) @@ -349,6 +355,13 @@ public: m_diseq_eh = nullptr; m_created_eh = nullptr; m_decide_eh = nullptr; + m_on_clause_eh = nullptr; + m_on_clause_ctx = nullptr; + } + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + m_on_clause_ctx = ctx; + m_on_clause_eh = on_clause; } void user_propagate_init( diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 76e6138ab..7b1449637 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -344,7 +344,11 @@ public: else return m_solver2->get_labels(r); } - + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + switch_inc_mode(); + m_solver2->register_on_clause(ctx, on_clause); + } void user_propagate_init( void* ctx, diff --git a/src/solver/solver.h b/src/solver/solver.h index 8a4bec538..4ffdd5092 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -278,7 +278,7 @@ public: }; virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; - + protected: virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 6e34758e6..b65ffde57 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -84,6 +84,10 @@ public: void set_phase(phase* p) override { } void move_to_front(expr* e) override { } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + m_tactic->register_on_clause(ctx, on_clause); + } + void user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index d919f51ee..0f55ea0fe 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -76,6 +76,10 @@ public: static void checkpoint(ast_manager& m); + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + throw default_exception("tactic does not support clause logging"); + } + void user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 25f8365e3..0d1062d78 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -166,6 +166,10 @@ public: return translate_core(m); } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + m_t2->register_on_clause(ctx, on_clause); + } + void user_propagate_init( void* ctx, user_propagator::push_eh_t& push_eh, diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 18d71b514..68e55be75 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -27,6 +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; class plugin : public decl_plugin { public: @@ -94,6 +95,10 @@ namespace user_propagator { virtual void user_propagate_clear() { } + virtual void register_on_clause(void*, on_clause_eh_t& r) { + throw default_exception("clause logging is only supported on the SMT solver"); + } + };