From e9dad84b857c10c710605cc5294349737d4dcbfe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Feb 2022 03:35:32 +0200 Subject: [PATCH] update documentation comments --- src/api/z3_api.h | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0b0d286d1..c9bf68a67 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6672,6 +6672,13 @@ extern "C" { /** \brief register a user-properator with the solver. + + \param c - context. + \param s - solver object. + \param user_context - a context used to maintain state for callbacks. + \param push_eh - a callback invoked when scopes are pushed + \param pop_eh - a callback invoked when scopes are poped + \param fresh_eh - a solver may spawn new solvers internally. This callback is used to produce a fresh user_context to be associated with fresh solvers. */ void Z3_API Z3_solver_propagate_init( @@ -6694,11 +6701,15 @@ extern "C" { /** \brief register a callback on final check. This provides freedom to the propagator to delay actions or implement a branch-and bound solver. + The final check is invoked when all decision variables have been assigned by the solver. - The final_eh callback takes as argument the original user_context that was used - when calling \c Z3_solver_propagate_init, and it takes a callback context for propagations. - If may use the callback context to invoke the \c Z3_solver_propagate_consequence function. - If the callback context gets used, the solver continues. + The \c final_eh callback takes as argument the original user_context that was used + when calling \c Z3_solver_propagate_init, and it takes a callback context with the + opaque type \c Z3_solver_callback. + The callback context is passed as argument to invoke the \c Z3_solver_propagate_consequence function. + The callback context can only be accessed (for propagation and for dynamically registering expressions) within a callback. + If the callback context gets used for propagation or conflicts, those propagations take effect and + may trigger new decision variables to be set. */ void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);