Function ipasir_sys::ipasir_solve

pub unsafe extern "C" fn ipasir_solve(solver: *mut c_void) -> c_int

Solve the formula with specified clauses under the specified assumptions. If the formula is satisfiable the function returns 10 and the state of the solver is changed to SAT. If the formula is unsatisfiable the function returns 20 and the state of the solver is changed to UNSAT. If the search is interrupted (see ipasir_set_terminate) the function returns 0 and the state of the solver is changed to INPUT. This function can be called in any defined state of the solver. Note that the state of the solver during execution of 'ipasir_solve' is undefined.

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