solver_propagate_init method

void solver_propagate_init(
  1. Z3_context c,
  2. Z3_solver s,
  3. Pointer<Void> user_context,
  4. Pointer<Z3_push_eh> push_eh,
  5. Pointer<Z3_pop_eh> pop_eh,
  6. Pointer<Z3_fresh_eh> fresh_eh,
)

\brief register a user-propagator 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 popped \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.

def_API('Z3_solver_propagate_init', VOID, (_in(CONTEXT), _in(SOLVER), _in(VOID_PTR), _fnptr(Z3_push_eh), _fnptr(Z3_pop_eh), _fnptr(Z3_fresh_eh)))

Implementation

void solver_propagate_init(
  Z3_context c,
  Z3_solver s,
  ffi.Pointer<ffi.Void> user_context,
  ffi.Pointer<Z3_push_eh> push_eh,
  ffi.Pointer<Z3_pop_eh> pop_eh,
  ffi.Pointer<Z3_fresh_eh> fresh_eh,
) {
  return _solver_propagate_init(
    c,
    s,
    user_context,
    push_eh,
    pop_eh,
    fresh_eh,
  );
}