Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
ipasir-sys
A Rust crate that contains FFI bindings for IPASIR-compatible SAT solvers.
This crate exposes the
minimal low-level C interface
to Rust. No more, no less. It does not try to provide safe wrappers or high
level abstractions. Those things can be built on top of this crate which is
inline with the *-sys
naming convention as discussed in
this article. Alternatively, you can use
the ipasir-rs crate which does provide
these things.
This crate will helpfully try to build Cadical if no solver is specified and has integration tests to verify the bindings work.
What is IPASIR?
IPASIR is a standard interface for incremental SAT solvers. It is the reverse acronym for Re-entrant Incremental Satisfiability Application Program Interface and was introduced at the 2015 annual SAT competition.
More explanation can be found in section 6.2 of this paper.
How to use this crate
There are two ways to use this crate:
- You can provide your own static library of a solver that implements IPASIR
- You can do nothing and the crate will try to build and link Cadical
The end result is the same. The IPASIR functions can be called by wrapping them in unsafe blocks:
use *;
For a more comprehensive example, see coloring_test.rs or refer to interface_test.rs.
Providing your own library
You can provide your own static library by setting the IPASIR
environment
variable at build time:
The crate will copy the library to its build directory and try to link against it. You must use an absolute path but the library's name does not matter. If your library has other dependencies, you can either pass additional flags to cargo or inline them into your static library.
Using the default solver
If the IPASIR
environment variable is not set, the crate will try to compile a
version of Cadical which is vendored as part of the crate. This compilation
depends on a relatively modern version of C++ and could fail if its standard
library cannot be found (libstdc++). At time of writing, the
clang version that ships with MacOS fails to compile
Cadical.
To fix this, there are two escape hatches that can be used to aid compilation:
- You can explicitly tell it which compiler to use by symlinking it to
/usr/local/bin/g++
- You can ensure libstdc++ is discoverable by symlinking it to
/usr/local/lib/libstdc++.a
You may also find the crate compiles but fails at runtime due to missing
linker symbols. This is likely the same problem and you should try re-compiling,
following the instructions above. It may be helpful to clone this crate and
build it on its own with cargo test
or refer to the
Travis CI build and
its configuration.
Compiling on MacOS
The GNU Compiler Collection is able to compile Cadical on MacOS. Based on the section above, here's how to fix it:
If this still fails, or if you're unable to compile the crate on linux, please open an issue.
Ideas for improvement
- Vendor more solvers and switch between them with a crate feature
- Improve operating system support (e.g. Windows)
- Add automated tests against different solvers and platforms
License
This crate has the MIT License but please check the license restrictions of the vendored software before using it.