Struct IpasirSolver

pub struct IpasirSolver<'term, 'learn> { /* private fields */ }

Type for an IPASIR solver.

Trait Implementations

impl Default for IpasirSolver<'_, '_>

fn default() -> Self

Returns the “default value” for a type.

impl Drop for IpasirSolver<'_, '_>

fn drop(&mut self)

Executes the destructor for this type.

impl<'a, C> Extend<&'a C> for IpasirSolver<'_, '_>

where C: AsRef<Cl> + ?Sized,

fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

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

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

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

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Clause> for IpasirSolver<'_, '_>

fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

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

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

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

Reserves capacity in a collection for the given number of additional elements.

impl<'learn> Learn<'learn> for IpasirSolver<'_, 'learn>

fn attach_learner<CB>(&mut self, cb: CB, max_len: usize)

where CB: FnMut(Clause) + 'learn,

Sets a learner callback that gets passed clauses up to a certain length learned by the solver.

The callback goes out of scope with the solver, afterwards captured variables become accessible.

Examples

Count number of learned clauses up to length 10.

use rustsat::solvers::{Solve, SolverResult, Learn};
use rustsat_ipasir::IpasirSolver;

let mut cnt = 0;

{
    let mut solver = IpasirSolver::default();
    // Load instance

    solver.attach_learner(|_| cnt += 1, 10);

    solver.solve().unwrap();
}

// cnt variable can be accessed from here on

fn detach_learner(&mut self)

Detaches the learner

impl Solve for IpasirSolver<'_, '_>

fn signature(&self) -> &'static str

Gets a signature of the solver implementation

fn solve(&mut self) -> Result<SolverResult>

Solves the internal CNF formula without any assumptions.

fn lit_val(&self, lit: Lit) -> Result<TernaryVal>

Gets an assignment of a variable in the solver.

fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>

where C: AsRef<Cl> + ?Sized,

Adds a clause to the solver by reference. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn reserve(&mut self, _max_var: Var) -> Result<(), Error>

Reserves memory in the solver until a maximum variables, if the solver supports it

fn solution(&self, high_var: Var) -> Result<Assignment, Error>

Gets a solution found by the solver up to a specified highest variable.

fn full_solution(&self) -> Result<Assignment, Error>

where Self: SolveStats,

Gets a solution found by the solver up to the highest variable known to the solver.

fn var_val(&self, var: Var) -> Result<TernaryVal, Error>

Same as Solve::lit_val, but for variables.

fn add_clause(&mut self, clause: Clause) -> Result<(), Error>

Adds a clause to the solver. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn add_unit(&mut self, lit: Lit) -> Result<(), Error>

Like Solve::add_clause but for unit clauses (clauses with one literal).

fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<(), Error>

Like Solve::add_clause but for clauses with two literals.

fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<(), Error>

Like Solve::add_clause but for clauses with three literals.

fn add_cnf(&mut self, cnf: Cnf) -> Result<(), Error>

Adds all clauses from a Cnf instance.

fn add_cnf_ref(&mut self, cnf: &Cnf) -> Result<(), Error>

Adds all clauses from a Cnf instance by reference.

impl SolveIncremental for IpasirSolver<'_, '_>

fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult>

Solves the internal CNF formula under assumptions.

fn core(&mut self) -> Result<Vec<Lit>>

Gets a core found by an unsatisfiable query. A core is a clause entailed by the formula that contains only inverted literals of the assumptions.

impl SolveStats for IpasirSolver<'_, '_>

fn stats(&self) -> SolverStats

Gets the available statistics from the solver

fn n_sat_solves(&self) -> usize

Gets the number of satisfiable queries executed.

fn n_unsat_solves(&self) -> usize

Gets the number of unsatisfiable queries executed.

fn n_terminated(&self) -> usize

Gets the number of queries that were prematurely terminated.

fn n_solves(&self) -> usize

Gets the total number of queries executed.

fn n_clauses(&self) -> usize

Gets the number of clauses in the solver.

fn max_var(&self) -> Option<Var>

Gets the variable with the highest index in the solver, if any. If all variables below have been used, the index of this variable +1 is the number of variables in the solver.

fn n_vars(&self) -> usize

Get number of variables. Note: this is only correct if all variables are used in order!

fn avg_clause_len(&self) -> f32

Gets the average length of all clauses in the solver.

fn cpu_solve_time(&self) -> Duration

Gets the total CPU time spent solving.

impl<'term> Terminate<'term> for IpasirSolver<'term, '_>

fn attach_terminator<CB>(&mut self, cb: CB)

where CB: FnMut() -> ControlSignal + 'term,

Sets a terminator callback that is regularly called during solving.

Examples

Terminate solver after 10 callback calls.

use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
use rustsat_ipasir::IpasirSolver;

let mut solver = IpasirSolver::default();

// Load instance

let mut cnt = 1;
solver.attach_terminator(move || {
    if cnt > 10 {
        ControlSignal::Terminate
    } else {
        cnt += 1;
        ControlSignal::Continue
    }
});

let ret = solver.solve().unwrap();

// Assuming an instance is actually loaded and runs long enough
// assert_eq!(ret, SolverResult::Interrupted);

fn detach_terminator(&mut self)

Detaches the terminator

impl Send for IpasirSolver<'_, '_>