pub struct Solver<Cb: Callbacks> { /* private fields */ }
Expand description
The main solver structure
A Solver
object contains the whole state of the SAT solver, including
a clause allocator, literals, clauses, and statistics.
It is parametrized by Callbacks
Implementations
sourceimpl<Cb: Callbacks> Solver<Cb>
impl<Cb: Callbacks> Solver<Cb>
sourcepub fn new(opts: SolverOpts, cb: Cb) -> Self
pub fn new(opts: SolverOpts, cb: Cb) -> Self
Create a new solver with the given options
pub fn num_learnts(&self) -> u32
pub fn dimacs_model(&self) -> SolverPrintDimacs<'_, Cb>
pub fn dimacs_proof(&self) -> SolverPrintDimacs<'_, Cb>
sourcepub fn interrupt_async(&self)
pub fn interrupt_async(&self)
Interrupt search asynchronously
Trait Implementations
sourceimpl<Cb: Callbacks> SolverInterface for Solver<Cb>
impl<Cb: Callbacks> SolverInterface for Solver<Cb>
sourcefn new_var(&mut self, upol: lbool, dvar: bool) -> Var
fn new_var(&mut self, upol: lbool, dvar: bool) -> Var
Creates a new SAT variable in the solver. If ‘decision’ is cleared, variable will not be
used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). Read more
sourcefn new_var_default(&mut self) -> Var
fn new_var_default(&mut self) -> Var
Create a new variable with the default polarity
sourcefn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool
fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool
sourcefn solve_limited(&mut self, assumps: &[Lit]) -> lbool
fn solve_limited(&mut self, assumps: &[Lit]) -> lbool
Search for a model that respects a given set of assumptions (With resource constraints).
sourcefn simplify(&mut self) -> bool
fn simplify(&mut self) -> bool
Simplify the clause database according to the current top-level assigment. Currently, the only
thing done here is the removal of satisfied clauses, but more things can be put here. Read more
fn is_ok(&self) -> bool
fn num_vars(&self) -> u32
fn num_clauses(&self) -> u32
fn num_conflicts(&self) -> u32
sourcefn value_lvl_0(&self, lit: Lit) -> lbool
fn value_lvl_0(&self, lit: Lit) -> lbool
Value of this literal if it’s assigned at level 0, or
UNDEF
otherwisesourcefn print_stats(&self)
fn print_stats(&self)
Print some current statistics to standard output.
sourcefn unsat_core(&self) -> &[Lit]
fn unsat_core(&self) -> &[Lit]
Return unsat core (as a subset of assumptions). Read more
sourcefn unsat_core_contains_lit(&self, lit: Lit) -> bool
fn unsat_core_contains_lit(&self, lit: Lit) -> bool
Does this literal occur in the unsat-core? Read more
sourcefn unsat_core_contains_var(&self, v: Var) -> bool
fn unsat_core_contains_var(&self, v: Var) -> bool
Does this variable occur in the unsat-core? Read more
sourcefn proved_at_lvl_0(&self) -> &[Lit]
fn proved_at_lvl_0(&self) -> &[Lit]
Obtain the slice of literals that are proved at level 0. Read more
Auto Trait Implementations
impl<Cb> RefUnwindSafe for Solver<Cb>where
Cb: RefUnwindSafe,
impl<Cb> Send for Solver<Cb>where
Cb: Send,
impl<Cb> Sync for Solver<Cb>where
Cb: Sync,
impl<Cb> Unpin for Solver<Cb>where
Cb: Unpin,
impl<Cb> UnwindSafe for Solver<Cb>where
Cb: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more