[−][src]Trait splr::ValidateIF
API for SAT validator like inject_assignment
, validate
and so on.
Required methods
pub fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent
[src]
pub fn validate(&self) -> Option<Vec<i32>>
[src]
return true
is the loaded assignment set is satisfiable (a model of a problem).
Implementors
impl ValidateIF for Solver
[src]
pub fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent
[src]
inject an assignment set into solver.
An assignment set is represented by a list of i32
.
#Example
use crate::{splr::config::Config, splr::types::*}; use splr::solver::{Solver, ValidateIF}; let cnf = CNFDescription { num_of_variables: 4, ..CNFDescription::default() }; let mut s = Solver::instantiate(&Config::default(), &cnf); assert_eq!(s.inject_assignment(&[1i32, -2, 3]), Ok(()));
pub fn validate(&self) -> Option<Vec<i32>>
[src]
returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment.
#Example
use crate::{splr::config::Config, splr::types::*}; use splr::solver::{Solver, ValidateIF}; let cnf = CNFDescription { num_of_variables: 4, ..CNFDescription::default() }; let mut s = Solver::instantiate(&Config::default(), &cnf); s.inject_assignment(&[1i32, -2, 3]); assert_eq!(s.validate(), None);