pub struct IpasirSolver { /* private fields */ }Expand description
A SAT solver conforming to the IPASIR specification.
All of the functions below, except the callback functions, are just safe interfaces to the IPASIR functions of the same name. For the two functions where the behavior differs from the specification, this is indicated in the function documentation.
When the IpasirSolver is dropped, the underlying data is automatically released by calling the ipasir_release function from the loaded library.
Note that an error encountered in this function can lead to a panic.
// 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);Implementations§
Source§impl IpasirSolver
impl IpasirSolver
Sourcepub fn ipasir_add(&mut self, lit: i32) -> Result<()>
pub fn ipasir_add(&mut self, lit: i32) -> Result<()>
Add the given literal into the currently added clause or finalize the clause with a 0.
§Errors
This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.
Sourcepub fn ipasir_solve(&mut self) -> Result<Option<bool>>
pub fn ipasir_solve(&mut self) -> Result<Option<bool>>
Solve the formula with specified clauses under the specified assumptions.
The solver returns an Option containing true (resp. false) if the formula is satisfiable,
or None if the search was stopped before deciding the satisfiability.
§Errors
This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.
Sourcepub fn ipasir_val(&mut self, lit: i32) -> Result<Option<bool>>
pub fn ipasir_val(&mut self, lit: i32) -> Result<Option<bool>>
Get the truth value of the given literal in the found satisfying assignment.
This function must not be called if the formula changed since the last time ipasir_solve found a model.
This function returns an Option containing true (resp. false) if the variable was set to true (resp. false) in the last satisfying assignment.
In case the solver detected both polarities of the literal would lead to a model, None may be returned.
§Errors
This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.
Sourcepub fn ipasir_assume(&mut self, lit: i32) -> Result<()>
pub fn ipasir_assume(&mut self, lit: i32) -> Result<()>
Add an assumption for the next SAT search (the next call of ipasir_solve).
After calling ipasir_solve all the previously added assumptions are cleared.
§Errors
This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.
Sourcepub fn ipasir_failed(&mut self, lit: i32) -> Result<bool>
pub fn ipasir_failed(&mut self, lit: i32) -> Result<bool>
Check if the given assumption literal was used to prove the unsatisfiability of the formula under the assumptions used for the last SAT search.
This function must not be called if the formula changed since the last time ipasir_solve proved the unsatisfiability of the formula.
Return true if so, false otherwise.
§Errors
This function returns an error if the library does not include the corresponding IPASIR function, or if an error occurs when calling it.
Sourcepub fn ipasir_set_terminate(
&mut self,
callback: Box<dyn Fn() -> bool>,
) -> Result<()>
pub fn ipasir_set_terminate( &mut self, callback: Box<dyn Fn() -> bool>, ) -> Result<()>
Add a callback function used to indicate a termination requirement to the solver.
The IpasirSolverLoader that created this solver must have enabled such callbacks with enable_set_terminate.
The solver will periodically call the callback function and check its return value during the search.
If the function returns true, the solver should terminate.
Contrary to the IPASIR specification, more than one callback function can be set in this way.
§Errors
This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.
Sourcepub fn ipasir_set_learn(&mut self, callback: Box<dyn Fn(&[i32])>) -> Result<()>
pub fn ipasir_set_learn(&mut self, callback: Box<dyn Fn(&[i32])>) -> Result<()>
Add a callback function to be called when a clause is learned by the solver.
The IpasirSolverLoader that created this solver must have enabled such callbacks with enable_set_learn.
Contrary to the IPASIR specification, more than one callback function can be set in this way.
The maximum length of the clauses passed to the callbacks is defined when enabling the callbacks in IpasirSolverLoader.
§Errors
This function will return an error if the correct type of callback function has not been enabled prior to the creation of the solver.