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.
# use ipasir_loading::IpasirSolverLoader;
// 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);
Ipasir-loading is developed at CRIL (Univ. Artois & CNRS). It is distributed under the terms of the GNU GPLv3 license.