Enum SolverImpls

pub enum SolverImpls<C: SolverConfig = DynamicConfig> {
    Dpll(Box<Dpll<C>>),
    Cdcl(Box<Cdcl<C>>),
}

An enum representing different implementations of SAT solvers.

Variants

Dpll(Box<Dpll<C>>)

A DPLL-based SAT solver.

Cdcl(Box<Cdcl<C>>)

A CDCL-based SAT solver.

Trait Implementations

impl<C: Clone + SolverConfig> Clone for SolverImpls<C>

fn clone(&self) -> SolverImpls<C>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<C: Debug + SolverConfig> Debug for SolverImpls<C>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<C: SolverConfig> Solver<C> for SolverImpls<C>

fn new<L: Literal, S: LiteralStorage<L>>(cnf: Cnf<L, S>) -> Self

Creates a new instance of the solver, initialised with the given CNF formula.

fn from_parts<L: Literal, S: LiteralStorage<L>>( cnf: Cnf<L, S>, assignment: C::Assignment, manager: C::ClauseManager, propagator: C::Propagator, restarter: C::Restarter, selector: C::VariableSelector, ) -> Self

Creates a solver instance from its components.

fn solve(&mut self) -> Option<Solutions>

Attempts to solve the CNF formula provided at construction.

fn solutions(&self) -> Solutions

Returns the current satisfying assignment if one has been found.

fn stats(&self) -> SolutionStats

Returns statistics about the solver’s last execution of solve().

fn debug(&mut self)

Provides a way to debug the solver’s internal state. The exact output or behavior is implementation-defined.