solver_register_on_clause method

void solver_register_on_clause(
  1. Z3_context c,
  2. Z3_solver s,
  3. Pointer<Void> user_context,
  4. Pointer<Z3_on_clause_eh> on_clause_eh,
)

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

Implementation

void solver_register_on_clause(
  Z3_context c,
  Z3_solver s,
  ffi.Pointer<ffi.Void> user_context,
  ffi.Pointer<Z3_on_clause_eh> on_clause_eh,
) {
  return _solver_register_on_clause(
    c,
    s,
    user_context,
    on_clause_eh,
  );
}