Crate ipasir_loading

Ipasir-loading: load and use an IPASIR SAT library

Ipasir-loading is designed to load shared libraries of IPASIR compatible SAT solvers. IPASIR is implemented by several SAT solvers, allowing them to be used in an easy and standardized way. See the SAT competition 2020 webpage for more information about IPASIR.

Example of use

// load the IPASIR library
let loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();

// create a solver from the library and populate it
let mut solver = loader.new_solver().unwrap();
solver.ipasir_add(-1).unwrap();
solver.ipasir_add(-2).unwrap();
solver.ipasir_add(0).unwrap();
solver.ipasir_add(1).unwrap();
solver.ipasir_add(2).unwrap();
solver.ipasir_add(0).unwrap();

// check satisfiability and get back the model
assert!(solver.ipasir_solve().unwrap().unwrap());
let model = vec![solver.ipasir_val(1).unwrap(), solver.ipasir_val(2).unwrap()];
let expected_1 = vec![Some(true), Some(false)];
let expected_2 = vec![Some(false), Some(true)];
assert!(model == expected_1 || model == expected_2);

License

Ipasir-loading is developed at CRIL (Univ. Artois & CNRS). It is distributed under the terms of the GNU GPLv3 license.

Structs

IpasirSolver

A SAT solver conforming to the IPASIR specification.

IpasirSolverLoader

A structure used to load a shared library and build new SAT solvers from it.

IpasirSolverWrapper

A wrapper around IpasirSolver.