scuttle_core::algs

Trait Solve

Source 
pub trait Solve: KernelFunctions {
    // Required methods
    fn solve(&mut self, limits: Limits) -> MaybeTerminatedError;
    fn all_stats(
        &self,
    ) -> (Stats, Option<SolverStats>, Option<Vec<EncodingStats>>);
}
Expand description

Solving interface for each algorithm

Required Methods§

Source

fn solve(&mut self, limits: Limits) -> MaybeTerminatedError

Solves the instance under given limits. If not fully solved, returns an early termination reason.

Source

fn all_stats(&self) -> (Stats, Option<SolverStats>, Option<Vec<EncodingStats>>)

Gets all statistics from the solver

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§

Source§

impl<'learn, 'term, ProofW, OInit, BCG> Solve for BiOptSat<CaDiCaL<'term, 'learn>, GeneralizedTotalizer, Totalizer, ProofW, OInit, BCG>
where BCG: Fn(Assignment) -> Clause, ProofW: Write + 'static,

Source§

impl<'learn, 'term, ProofW, OInit, BCG> Solve for LowerBounding<CaDiCaL<'term, 'learn>, GeneralizedTotalizer, Totalizer, ProofW, OInit, BCG>
where BCG: Fn(Assignment) -> Clause, ProofW: Write + 'static,

Source§

impl<'learn, 'term, ProofW, OInit, BCG> Solve for PMinimal<CaDiCaL<'term, 'learn>, GeneralizedTotalizer, Totalizer, ProofW, OInit, BCG>
where BCG: Fn(Assignment) -> Clause, ProofW: Write + 'static,