[][src]Function ipasir_sys::ipasir_set_learn

pub unsafe extern "C" fn ipasir_set_learn(
    solver: *mut c_void,
    data: *mut c_void,
    max_length: c_int,
    learn: Option<unsafe extern "C" fn(data: *mut c_void, clause: *mut c_int)>
)

Set a callback function used to extract learned clauses up to a given length from the solver. The solver will call this function for each learned clause that satisfies the maximum length (literal count) condition. The ipasir_set_learn function can be called in any state of the solver, the state remains unchanged after the call. The callback function is of the form "void learn(void * data, int * clause)"

  • the solver calls the callback function with the parameter "data" having the value passed in the ipasir_set_learn function (2nd parameter).
  • the argument "clause" is a pointer to a null terminated integer array containing the learned clause. the solver can change the data at the memory location that "clause" points to after the function call.

Required state: INPUT or SAT or UNSAT State after: INPUT or SAT or UNSAT