solver_propagate_final method

void solver_propagate_final(Z3_context c, Z3_solver s, Pointer<Z3_final_eh> final_eh)

\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 \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.

def_API('Z3_solver_propagate_final', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_final_eh)))

Implementation

void solver_propagate_final(
  Z3_context c,
  Z3_solver s,
  ffi.Pointer<Z3_final_eh> final_eh,
) {
  return _solver_propagate_final(
    c,
    s,
    final_eh,
  );
}