added API to monitor clause inferences

See RELEASE_NOTES for more information
examples pending.

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

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

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, 

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):object(c) { init(Z3_mk_solver(c)); check_error(); }
-        solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }
+        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<void(expr const& proof, expr_vector const& clause)> 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<on_clause*>(_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 {
 

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

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;
+
+
+    /// <summary>
+    /// OnClause - clause inference callback
+    /// </summary>        
+    public class OnClause : IDisposable
+    {
+        /// <summary>
+        /// 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.
+        /// </summary>                
+        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);
+	}
+
+        /// <summary>
+        /// OnClause constructor
+        /// </summary>        
+        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);
+        }
+
+        /// <summary>
+        /// Release private memory.
+        /// </summary>            
+        ~OnClause()
+        {
+            Dispose();
+        }
+        
+        /// <summary>
+        /// Must be called. The object will not be garbage collected automatically even if the context is disposed
+        /// </summary>
+        public virtual void Dispose()
+        {
+            if (!gch.IsAllocated)
+                return;
+            gch.Free();
+        }
+    }
+}

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:
 

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.

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<sort> 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);

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<unsigned>(0), static_cast<expr**>(nullptr));

src/ast/ast_ll_pp.cpp

@@ -86,6 +86,7 @@ class ll_printer {
         default:
             display_child_ref(n);
         }
+
     }
 
     template<typename T>

src/sat/sat_solver.h

@@ -432,17 +432,17 @@ namespace sat {
         }
         
         void checkpoint() {
-            if (!m_checkpoint_enabled) return;
+            if (!m_checkpoint_enabled) 
-            if (limit_reached()) {
+                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; }

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,

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);
     }
 }

src/sat/smt/euf_proof.cpp

@@ -25,19 +25,25 @@ namespace euf {
         if (m_proof_initialized)
             return;
 
-        if (s().get_config().m_drat && 
+        if (m_on_clause)
-            (get_config().m_lemmas2console ||
+            s().set_drat(true);
-             s().get_config().m_smt_proof_check ||
+        
-             s().get_config().m_smt_proof.is_non_empty_string())) {
+        if (!s().get_config().m_drat)
+            return;
 
-            get_drat().add_theory(get_id(), symbol("euf"));
+        if (!get_config().m_lemmas2console &&
-            get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
+            !s().get_config().m_smt_proof_check &&
-            TRACE("euf", tout << "init-proof " << s().get_config().m_smt_proof << "\n");
+            !m_on_clause &&
-            if (s().get_config().m_smt_proof.is_non_empty_string())
+            !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);
+            return;
-            get_drat().set_clause_eh(*this);
+        
-            m_proof_initialized = true;
+        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<sort> 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)
+        return m.mk_app(th, args.size(), args.data(), proof);
-            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);
     }
 
     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) {

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,

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<euf::ackerman>     m_ackerman;
+        scoped_ptr<euf::ackerman>       m_ackerman;
-        user_solver::solver*          m_user_propagator = nullptr;
+        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,

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<sort> 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)
+        binding = m.mk_app(symbol("bind"), args.size(), args.data(), range);
-            sorts.push_back(arg->get_sort());
-        d = m.mk_func_decl(symbol("bind"), args.size(), sorts.data(), range);
-        binding = m.mk_app(d, args);
         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);
+        args.push_back(binding);        
-        for (expr* arg : args)
+        return m.mk_app(symbol("inst"), args.size(), args.data(), range);
-            sorts.push_back(arg->get_sort());
-        
-        d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range);
-        return m.mk_app(d, args);
     }
 
 }

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);

src/smt/smt_clause_proof.cpp

@@ -36,91 +36,113 @@ namespace smt {
         }
     }
 
-    proof* clause_proof::justification2proof(justification* j) {
+    proof* clause_proof::justification2proof(status st, justification* j) {
-        return (m.proofs_enabled() && j) ? j->mk_proof(ctx.get_cr()) : nullptr;
+        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) {  
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            justification* j = c.get_justification();
+            return;
-            proof_ref pr(justification2proof(j), m);
+        justification* j = c.get_justification();
-            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
+        auto st = kind2st(c.get_kind());
-            update(c, kind2st(c.get_kind()), pr);
+        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) {              
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            proof_ref pr(justification2proof(j), m);
+            return;
-            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
+        auto st = kind2st(k);
-            m_lits.reset();
+        proof_ref pr(justification2proof(st, j), m);
-            for (unsigned i = 0; i < n; ++i) {
+        CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-                m_lits.push_back(ctx.literal2expr(lits[i]));
+        m_lits.reset();
-            }
+        for (unsigned i = 0; i < n; ++i) 
-            update(kind2st(k), m_lits, pr);
+            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) {            
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            m_lits.reset();
+            return;
-            for (unsigned i = 0; i < new_size; ++i) {
+        m_lits.reset();
-                m_lits.push_back(ctx.literal2expr(c[i]));
+        for (unsigned i = 0; i < new_size; ++i) 
-            }
+            m_lits.push_back(ctx.literal2expr(c[i]));
-            update(status::lemma, m_lits, nullptr);
+        proof* p = justification2proof(status::lemma, nullptr);
-            for (unsigned i = new_size; i < c.get_num_literals(); ++i) {
+        update(status::lemma, m_lits, p);
-                m_lits.push_back(ctx.literal2expr(c[i]));
+        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);
+        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) {
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            m_lits.reset();
+            return;
-            m_lits.push_back(ctx.literal2expr(lit));
+        m_lits.reset();
-            proof* pr = justification2proof(j);
+        m_lits.push_back(ctx.literal2expr(lit));
-            update(kind2st(k), m_lits, pr);
+        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) {
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            m_lits.reset();
+            return;
-            m_lits.push_back(ctx.literal2expr(lit1));
+        m_lits.reset();
-            m_lits.push_back(ctx.literal2expr(lit2));
+        m_lits.push_back(ctx.literal2expr(lit1));
-            proof* pr = justification2proof(j);
+        m_lits.push_back(ctx.literal2expr(lit2));
-            m_trail.push_back(info(kind2st(k), m_lits, pr));
+        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");
+        if (ctx.get_fparams().m_clause_proof)
-        m_trail.push_back(info(st, v, p));
+            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) {
+        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
-            m_lits.reset();
+            return;
-            for (literal lit : c) {
+        m_lits.reset();
-                m_lits.push_back(ctx.literal2expr(lit));
+        for (literal lit : c) 
-            }
+            m_lits.push_back(ctx.literal2expr(lit));        
-            update(st, m_lits, p);
+        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);
     }
 

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;
+        context&        ctx;
-        ast_manager& m;
+        ast_manager&    m;
         expr_ref_vector m_lits;
-        vector<info> m_trail;
+        vector<info>    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);

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
          */

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) {

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);

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);
     }

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"
         */

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,

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(

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, 

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);

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,

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,

src/tactic/tactical.cpp

@@ -166,6 +166,10 @@ public:
         return translate_core<and_then_tactical>(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,

src/tactic/user_propagator_base.h

@@ -27,6 +27,7 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*, unsigned)>                  pop_eh_t;
     typedef std::function<void(void*, callback*, expr*)>                     created_eh_t;
     typedef std::function<void(void*, callback*, expr**, unsigned*, lbool*)> decide_eh_t;
+    typedef std::function<void(void*, expr*, unsigned, expr* const*)>        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");
+        }
+
        
     };