# IPASIR interface for Rust

|       Docs        |       Crates.io      |
|:-----------------:|:--------------------:|
| [![docs][1]][2]   | [![crates][3]][4]    |

## What it is

IPASIR is a simple C interface to incremental SAT solvers.
(It stands for Reentrant Incremental Sat solver API, in reverse.)
This interface is supported by a few different solvers because it is used in the SAT competition's incremental track.
The IPASIR distribution, containing the interface and some sample solvers,
can be found at [this GitHub repository](https://github.com/biotomas/ipasir).
This IPASIR library is an attempt to semi-soundly allow Rust programs to interface with such SAT solver libraries.

## How the FFI is structured

For users of this FFI there are two distinct ways of usage.
Users can build their application on top of the `raw` module that offers direct but unsafe calls
into the C-API.
The recommended way to use this FFI is to use the `Solver` type that acts as safe wrapper around
the C-API.

Allocate a new solver instance with: `ipasir::Solver::init()`

## License

Licensed under either of

 * Apache license, Version 2.0, ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
 * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)

at your option.

### Dual licence: [![badge][license-mit-badge]](LICENSE-MIT) [![badge][license-apache-badge]](LICENSE-APACHE)

### Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted
for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any
additional terms or conditions.

[license-mit-badge]: https://img.shields.io/badge/license-MIT-blue.svg
[license-apache-badge]: https://img.shields.io/badge/license-APACHE-orange.svg

## Release Notes

### 0.3.1 - 12th April 2020

- Implement `Error` and `Display` for the error types of the crate.

### 0.3.0 - 10th April 2019

- Major API overhaul
- `ipasir::ffi::Solver` is now the FFI C targeting solver wrapper for Rust.
- `IpasirSolver` is the trait to be implemented by Rust IPASIR compatible solvers

### 0.2.0 - 25th April 2018

- Renamed `raw` module to `sys` to better fit with the rest of the ecosystem.
- `Lit::to_raw` is no longer publicly visible.
- Removed `LitOrEnd` and `EndOfClause`.
- Split `Solver::add` API into `Solver::add_lit` and `Solver::finalize_clause`.
- Add `Clause::len` and `Clause::get` methods.
- Add `Lit::new_unchecked` constructor.
- Add `Lit::sign` and `Sign` enum.
- Add `Lit::var` method.
- Make `SolveControl` now publicly visible. (Was accidentally private before.)

### 0.1.0 - 24th April 2018

- Initial Release

[1]: https://docs.rs/ipasir/badge.svg
[2]: https://docs.rs/ipasir/
[3]: https://img.shields.io/crates/v/ipasir.svg
[4]: https://crates.io/crates/ipasir/