Struct rustsat_kissat::Kissat
source · pub struct Kissat<'term> { /* private fields */ }
Expand description
The Kissat solver type
Implementations§
source§impl Kissat<'_>
impl Kissat<'_>
sourcepub fn set_configuration(&mut self, config: Config) -> Result<()>
pub fn set_configuration(&mut self, config: Config) -> Result<()>
Sets a pre-defined configuration for Kissat’s internal options
sourcepub fn set_option(&mut self, name: &str, value: c_int) -> Result<()>
pub fn set_option(&mut self, name: &str, value: c_int) -> Result<()>
Sets the value of a Kissat option. For possible options, check Kissat with kissat --help
.
Requires state SolverState::Configuring
.
sourcepub fn get_option(&self, name: &str) -> Result<c_int>
pub fn get_option(&self, name: &str) -> Result<c_int>
Gets the value of a Kissat option. For possible options, check Kissat with kissat --help
.
sourcepub fn print_stats(&self)
pub fn print_stats(&self)
Prints the solver statistics from the Kissat backend
Trait Implementations§
source§impl<'a> Extend<&'a Clause> for Kissat<'_>
impl<'a> Extend<&'a Clause> for Kissat<'_>
source§fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T)
fn extend<T: IntoIterator<Item = &'a 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 Extend<Clause> for Kissat<'_>
impl Extend<Clause> for Kissat<'_>
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 Interrupt for Kissat<'_>
impl Interrupt for Kissat<'_>
§type Interrupter = Interrupter
type Interrupter = Interrupter
The interrupter of the solver
source§fn interrupter(&mut self) -> Self::Interrupter
fn interrupter(&mut self) -> Self::Interrupter
Gets a thread safe interrupter object that can be used to terminate the solver
source§impl Solve for Kissat<'_>
impl Solve for Kissat<'_>
source§fn reserve(&mut self, max_var: Var) -> Result<()>
fn reserve(&mut self, max_var: Var) -> Result<()>
Reserves memory in the solver until a maximum variables, if the solver
supports it
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(&mut self, clause: &Clause) -> Result<()>
fn add_clause_ref(&mut self, clause: &Clause) -> 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.
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.source§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).source§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.source§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.source§impl SolveStats for Kissat<'_>
impl SolveStats for Kissat<'_>
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 Kissat<'term>
impl<'term> Terminate<'term> for Kissat<'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_kissat::Kissat;
let mut solver = Kissat::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 Kissat<'_>
Auto Trait Implementations§
impl<'term> Freeze for Kissat<'term>
impl<'term> !RefUnwindSafe for Kissat<'term>
impl<'term> !Sync for Kissat<'term>
impl<'term> Unpin for Kissat<'term>
impl<'term> !UnwindSafe for Kissat<'term>
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