[−][src]Module ipasir::ffi::sys

The external IPASIR C API.

Prefer using the provided safe API instead.

Structs

Sealed FFI solver type.

ipasir_add ^⚠	Add the given literal into the currently added clause of finalize the clause with a 0 (zero).
ipasir_assume ^⚠	Add an assumption for the next SAT search (the next call to `ipasir_solve`).
ipasir_failed ^⚠	Check if the given assumption literal was used to prove the unsatisfiability of the formula under the assumptions used for the last SAT search. Return `1` if so, `0` otherwise.
ipasir_init ^⚠	Construct a new solver and return a pointer to it.
ipasir_release ^⚠	Release the solver, i.e., all its resources and allocated memory (runs destructors).
ipasir_set_learn ^⚠	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.
ipasir_set_terminate ^⚠	Set a callback function used to indicate a termination requirement to the solver. The solver will periodically call this function and check its return value during the search.
ipasir_signature ^⚠	Return the name and the version of the incremental SAT solving library.
ipasir_solve ^⚠	Solve the formula with specified clauses under the specified assumptions.
ipasir_val ^⚠	Get the truth value of the given literal in the found satisfying assignment.