Trait splr::solver::ValidateIF

source ·
pub trait ValidateIF {
    // Required methods
    fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent;
    fn validate(&self) -> Option<Vec<i32>>;
}
Expand description

API for SAT validator like inject_assignment, validate and so on.

Required Methods§

source

fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent

load a assignment set into solver.

§Errors

if solver becomes inconsistent.

source

fn validate(&self) -> Option<Vec<i32>>

return true is the loaded assignment set is satisfiable (a model of a problem).

Implementors§