1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
//! Crate `validator` implements a model checker. use crate::{ assign::{AssignIF, PropagateIF}, cdb::ClauseDBIF, solver::Solver, types::{Lit, MaybeInconsistent, SolverError}, }; /// API for SAT validator like [`inject_assignment`](`crate::solver::ValidateIF::inject_assignment`), [`validate`](`crate::solver::ValidateIF::validate`) and so on. pub trait ValidateIF { /// load a assignment set into solver. /// /// # Errors /// /// if solver becomes inconsistent. fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent; /// return `true` is the loaded assignment set is satisfiable (a model of a problem). fn validate(&self) -> Option<Vec<i32>>; } impl ValidateIF for Solver { /// 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(())); ///``` /// fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent { if vec.is_empty() { return Err(SolverError::Inconsistent); } for i in vec { self.asg.assign_at_root_level(Lit::from(*i))?; } Ok(()) } /// 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); ///``` /// fn validate(&self) -> Option<Vec<i32>> { self.cdb .validate(self.asg.assign_ref(), true) .map(|cid| Vec::<i32>::from(&self.cdb[cid])) } }