Struct IpasirSolver 

pub struct IpasirSolver<'lib> { /* private fields */ }

Instance of a dynamically loaded IPASIR solver, created using a IpasirLibrary.

Implementations

impl IpasirSolver<'_>

pub fn signature(&self) -> &str

Wrapper for the ipasir_signature function.

Trait Implementations

impl Assumptions for IpasirSolver<'_>

fn solve_assuming<I: IntoIterator<Item = Lit>>( &mut self, assumptions: I, ) -> SolveResult<IpasirSol<'_>, IpasirFailed<'_>>

Solve the formula with specified clauses under the given assumptions.

impl ClauseDatabase for IpasirSolver<'_>

fn add_clause_from_slice(&mut self, clause: &[Lit]) -> Result<(), Unsatisfiable>

Add a clause to the ClauseDatabase. The database is allowed to return Unsatisfiable when the collection of clauses has been proven to be unsatisfiable. This is used as a signal to the encoder that any subsequent encoding effort can be abandoned.

fn new_var_range(&mut self, len: usize) -> VarRange

Method to be used to receive a new Boolean variable that can be used in the encoding of a problem or constraint.

impl Debug for IpasirSolver<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Drop for IpasirSolver<'_>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.

impl LearnCallback for IpasirSolver<'_>

fn set_learn_callback<F: FnMut(&mut dyn Iterator<Item = Lit>) + 'static>( &mut self, cb: Option<F>, )

Set a callback function used to extract learned clauses up to a given length from the solver.

impl Solver for IpasirSolver<'_>

fn solve(&mut self) -> SolveResult<IpasirSol<'_>, IpasirFailed<'_>>

Solve the formula with specified clauses.

impl TerminateCallback for IpasirSolver<'_>

fn set_terminate_callback<F: FnMut() -> TermSignal + 'static>( &mut self, cb: Option<F>, )

Set a callback function used to indicate a termination requirement to the solver.