Crate ipasir_sys

Functions

ipasir_add^⚠

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.

ipasir_assume^⚠

Add an assumption for the next SAT search (the next call of ipasir_solve). After calling ipasir_solve all the previously added assumptions are cleared.

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. Use the returned pointer as the first parameter in each of the following functions.

ipasir_release^⚠

Release the solver, i.e., all its resoruces and allocated memory (destructor). The solver pointer cannot be used for any purposes after this call.

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. 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)”

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. The ipasir_set_terminate function can be called in any state of the solver, the state remains unchanged after the call. The callback function is of the form “int terminate(void * data)”

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. 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.

ipasir_val^⚠

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.