mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

update documentation comments

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-06 03:35:32 +02:00
parent 9d655cc658
commit e9dad84b85
1 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/api/z3_api.h
View file

@ -6672,6 +6672,13 @@ extern "C" {
/** /**
\brief register a user-properator with the solver. \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( void Z3_API Z3_solver_propagate_init(
@ -6694,11 +6701,15 @@ extern "C" {
/** /**
\brief register a callback on final check. \brief register a callback on final check.
This provides freedom to the propagator to delay actions or implement a branch-and bound solver. 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 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 for propagations. when calling \c Z3_solver_propagate_init, and it takes a callback context with the
If may use the callback context to invoke the \c Z3_solver_propagate_consequence function. opaque type \c Z3_solver_callback.
If the callback context gets used, the solver continues. 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); void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);