Expand description
Rust native FFI for the IPASIR interface for incremental SAT solvers.
Visit the IPASIR manual here.
Modules§
- ffi
- IPASIR FFI solver and C bindings.
Structs§
- Clause
- A clause from the IPASIR solver.
- Invalid
LitVal - Encountered when trying to create a literal with an invalid value.
- Lit
- A literal of the IPASIR implementing solver.
- LitIter
- Iterator over the literals of a clause.
- Solver
Error - An error encountered at some solver calls.
- Var
- A variable of the IPASIR implementing solver.
Enums§
- LitValue
- The assignment of a literal.
- Response
Error - An error encountered when using an FII IPASIR solver that returned an invalid response value.
- Sign
- The polarity of a literal.
- Solve
Control - Tells the solver to either stop solving process or continue.
- Solve
Response - Possible responses from a call to
ipasir_solve. - Solver
Error Kind - A kind of a SAT solver error.
Traits§
- Ipasir
Solver - The IPASIR interface a SAT solver has to implement to be conforming.
Type Aliases§
- Result
- Type alias that has a
SolverErroras error variant.