Trait splr::traits::ValidatorIF

pub trait ValidatorIF {
    fn inject_assigmnent(&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_assigmnent(&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).

Loading content...

Implementors

impl ValidatorIF for Solver

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

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

returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment.

Loading content...