Struct Solver

pub struct Solver<Cb: Callbacks> { /* private fields */ }

RustSAT wrapper for a batsat::Solver Solver from BatSat

Implementations

impl<Cb: Callbacks> Solver<Cb>

pub fn batsat_ref(&self) -> &Solver<Cb>

Gets a reference to the internal BasicSolver

pub fn batsat_mut(&mut self) -> &mut Solver<Cb>

Gets a mutable reference to the internal BasicSolver

Trait Implementations

impl<Cb: Default + Callbacks> Default for Solver<Cb>

fn default() -> Solver<Cb>

Returns the “default value” for a type.

impl<'a, C, Cb> Extend<&'a C> for Solver<Cb>

where C: AsRef<Cl> + ?Sized, Cb: Callbacks,

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<Cb: Callbacks> Extend<Clause> for Solver<Cb>

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<Cb: Callbacks> Solve for Solver<Cb>

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<Cb: Callbacks> SolveIncremental for Solver<Cb>

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<Cb: Callbacks> SolveStats for Solver<Cb>

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_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 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.

fn n_solves(&self) -> usize

Gets the total number of queries executed.

fn n_vars(&self) -> usize

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