Function ipasir_sys::ipasir_add

pub unsafe extern "C" fn ipasir_add(solver: *mut c_void, lit_or_zero: c_int)

Add the given literal into the currently added clause or finalize the clause with a 0. Clauses added this way cannot be removed. The addition of removable clauses can be simulated using activation literals and assumptions.

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

Literals are encoded as (non-zero) integers as in the DIMACS formats. They have to be smaller or equal to INT_MAX and strictly larger than INT_MIN (to avoid negation overflow). This applies to all the literal arguments in API functions.