Trait SolveIncremental

pub trait SolveIncremental: Solve {
    // Required methods
    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult>;
    fn core(&mut self) -> Result<Vec<Lit>>;
}

Trait for all SAT solvers in this library. Solvers outside of this library can also implement this trait to be able to use them with this library.

Required Methods

fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult>

Solves the internal CNF formula under assumptions.

Errors

A solver may return any error. One typical option might be crate::OutOfMemory.

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.

Errors

• If the solver is not in the unsatisfied state, returns StateError
• A specific implementation might return other errors

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