Struct IpasirSolverLoader 

pub struct IpasirSolverLoader { /* private fields */ }

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

This structure takes as entry point a path to a shared library containing a SAT solver that conform to the IPASIR specification. An IpasirSolverLoader is built by passing this path to the from_path function. This object can be used to create new solvers with the new_solver function.

The IPASIR interface provides two functions that take a function pointer as parameter. To use them on solvers created by this object, these functions must be enabled by calling enable_set_terminate and enable_set_learn before creating the SAT solvers.

Example

let mut loader = IpasirSolverLoader::from_path("path/to/lib.so").unwrap();
loader.enable_set_terminate(true); // activate ipasir_set_terminate
loader.enable_set_learn(Some(8)); // activate ipasir_set_learn for clause of sizes at most 8
let sat_solver = loader.new_solver().unwrap(); // create the solver

Implementations

impl IpasirSolverLoader

pub fn from_path<P: AsRef<OsStr>>(path: P) -> Result<Self>

Builds a new IpasirSolverLoader given a path to a shared library containing a SAT solver that conform to the IPASIR specification.

Errors

This function returns an error if the library cannot be loaded, e.g. if the path does not point to a shared library.

pub fn ipasir_signature(&self) -> Result<String>

Returns a string describing the name and the version of the library solver.

Errors

This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.

pub fn new_solver(&self) -> Result<IpasirSolverWrapper>

Builds a new SAT solver from the shared library.

The returned solver can accept callback functions on termination or when learning a clause only if the appropriate activation functions (enable_set_terminate or enable_set_learn) have been called before calling this function.

Errors

This function returns an error if the library does not contain the ipasir_init function, or if an error occurs when calling it. In case some callback functions are enabled, this function will also return an error if the corresponding IPASIR callback function (ipasir_set_terminate or ipasir_set_learn) is missing from the library or if an error occurs when calling it.

pub fn enable_set_terminate(&mut self, v: bool)

Enables or disables the ipasir_set_terminate for the solvers created after the call to this function.

pub fn enable_set_learn(&mut self, bound: Option<i32>)

Enables or disables the ipasir_set_learn for the solvers created after the call to this function.

To enable the function, pass Some(n) where n is the maximum length of the learned clauses you are interested in. To disable the function, pass None.

Trait Implementations

impl AsRef<Library> for IpasirSolverLoader

fn as_ref(&self) -> &Library

Converts this type into a shared reference of the (usually inferred) input type.