Trait splr::solver::ValidateIF

pub trait ValidateIF {
    fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent;
    fn validate(&self) -> Option<Vec<i32>>;
}

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

Required methods

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

load a assignment set into solver.

Errors

if solver becomes inconsistent.

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

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

Implementors

impl ValidateIF for Solver