Function ipasir_sys::ipasir_val

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

Get the truth value of the given literal in the found satisfying assignment. Return 'lit' if True, '-lit' if False; 'ipasir_val(lit)' may return '0' if the found assignment is satisfying for both valuations of lit. Each solution that agrees with all non-zero values of ipasir_val() is a model of the formula.

This function can only be used if ipasir_solve has returned 10 and no 'ipasir_add' nor 'ipasir_assume' has been called since then, i.e., the state of the solver is SAT.

Required state: SAT State after: SAT