pub struct IpasirSolver<'term, 'learn> { /* private fields */ }
Expand description
Type for an IPASIR solver.
Trait Implementations§
source§impl Default for IpasirSolver<'_, '_>
impl Default for IpasirSolver<'_, '_>
source§impl Drop for IpasirSolver<'_, '_>
impl Drop for IpasirSolver<'_, '_>
source§impl<'a, C> Extend<&'a C> for IpasirSolver<'_, '_>
impl<'a, C> Extend<&'a C> for IpasirSolver<'_, '_>
source§fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T)
fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T)
Extends a collection with the contents of an iterator. Read more
source§fn extend_one(&mut self, item: A)
fn extend_one(&mut self, item: A)
🔬This is a nightly-only experimental API. (
extend_one
)Extends a collection with exactly one element.
source§fn extend_reserve(&mut self, additional: usize)
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. Read more
source§impl Extend<Clause> for IpasirSolver<'_, '_>
impl Extend<Clause> for IpasirSolver<'_, '_>
source§fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T)
fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T)
Extends a collection with the contents of an iterator. Read more
source§fn extend_one(&mut self, item: A)
fn extend_one(&mut self, item: A)
🔬This is a nightly-only experimental API. (
extend_one
)Extends a collection with exactly one element.
source§fn extend_reserve(&mut self, additional: usize)
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. Read more
source§impl<'learn> Learn<'learn> for IpasirSolver<'_, 'learn>
impl<'learn> Learn<'learn> for IpasirSolver<'_, 'learn>
source§fn attach_learner<CB>(&mut self, cb: CB, max_len: usize)
fn attach_learner<CB>(&mut self, cb: CB, max_len: usize)
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
source§fn detach_learner(&mut self)
fn detach_learner(&mut self)
Detaches the learner
source§impl Solve for IpasirSolver<'_, '_>
impl Solve for IpasirSolver<'_, '_>
source§fn solve(&mut self) -> Result<SolverResult>
fn solve(&mut self) -> Result<SolverResult>
Solves the internal CNF formula without any assumptions. Read more
source§fn lit_val(&self, lit: Lit) -> Result<TernaryVal>
fn lit_val(&self, lit: Lit) -> Result<TernaryVal>
Gets an assignment of a variable in the solver. Read more
source§fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>
fn add_clause_ref<C>(&mut self, clause: &C) -> Result<()>
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. Read more
source§fn reserve(&mut self, _max_var: Var) -> Result<(), Error>
fn reserve(&mut self, _max_var: Var) -> Result<(), Error>
Reserves memory in the solver until a maximum variables, if the solver
supports it Read more
source§fn solution(&self, high_var: Var) -> Result<Assignment, Error>
fn solution(&self, high_var: Var) -> Result<Assignment, Error>
Gets a solution found by the solver up to a specified highest variable. Read more
source§fn full_solution(&self) -> Result<Assignment, Error>where
Self: SolveStats,
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. Read more
source§fn var_val(&self, var: Var) -> Result<TernaryVal, Error>
fn var_val(&self, var: Var) -> Result<TernaryVal, Error>
Same as
Solve::lit_val
, but for variables. Read moresource§fn add_clause(&mut self, clause: Clause) -> Result<(), Error>
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. Read more
source§fn add_unit(&mut self, lit: Lit) -> Result<(), Error>
fn add_unit(&mut self, lit: Lit) -> Result<(), Error>
Like
Solve::add_clause
but for unit clauses (clauses with one literal). Read moresource§fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<(), Error>
fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<(), Error>
Like
Solve::add_clause
but for clauses with two literals. Read moresource§fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<(), Error>
fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<(), Error>
Like
Solve::add_clause
but for clauses with three literals. Read moresource§impl SolveIncremental for IpasirSolver<'_, '_>
impl SolveIncremental for IpasirSolver<'_, '_>
source§fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult>
fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult>
Solves the internal CNF formula under assumptions. Read more
source§impl SolveStats for IpasirSolver<'_, '_>
impl SolveStats for IpasirSolver<'_, '_>
source§fn stats(&self) -> SolverStats
fn stats(&self) -> SolverStats
Gets the available statistics from the solver
source§fn n_sat_solves(&self) -> usize
fn n_sat_solves(&self) -> usize
Gets the number of satisfiable queries executed.
source§fn n_unsat_solves(&self) -> usize
fn n_unsat_solves(&self) -> usize
Gets the number of unsatisfiable queries executed.
source§fn n_terminated(&self) -> usize
fn n_terminated(&self) -> usize
Gets the number of queries that were prematurely terminated.
source§fn max_var(&self) -> Option<Var>
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.
source§fn n_vars(&self) -> usize
fn n_vars(&self) -> usize
Get number of variables.
Note: this is only correct if all variables are used in order!
source§fn avg_clause_len(&self) -> f32
fn avg_clause_len(&self) -> f32
Gets the average length of all clauses in the solver.
source§fn cpu_solve_time(&self) -> Duration
fn cpu_solve_time(&self) -> Duration
Gets the total CPU time spent solving.
source§impl<'term> Terminate<'term> for IpasirSolver<'term, '_>
impl<'term> Terminate<'term> for IpasirSolver<'term, '_>
source§fn attach_terminator<CB>(&mut self, cb: CB)where
CB: FnMut() -> ControlSignal + '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);
source§fn detach_terminator(&mut self)
fn detach_terminator(&mut self)
Detaches the terminator
impl Send for IpasirSolver<'_, '_>
Auto Trait Implementations§
impl<'term, 'learn> Freeze for IpasirSolver<'term, 'learn>
impl<'term, 'learn> !RefUnwindSafe for IpasirSolver<'term, 'learn>
impl<'term, 'learn> !Sync for IpasirSolver<'term, 'learn>
impl<'term, 'learn> Unpin for IpasirSolver<'term, 'learn>
impl<'term, 'learn> !UnwindSafe for IpasirSolver<'term, 'learn>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
source§impl<S> CollectClauses for Swhere
S: Solve + SolveStats,
impl<S> CollectClauses for Swhere
S: Solve + SolveStats,
source§fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), OutOfMemory>where
T: IntoIterator<Item = Clause>,
fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), OutOfMemory>where
T: IntoIterator<Item = Clause>,
Extends the clause collector with an iterator of clauses Read more
source§fn add_clause(&mut self, cl: Clause) -> Result<(), OutOfMemory>
fn add_clause(&mut self, cl: Clause) -> Result<(), OutOfMemory>
Adds one clause to the collector Read more
source§impl<T> IntoEither for T
impl<T> IntoEither for T
source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moresource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more