// codesnip-guard: HornSatisfiability
#[cfg_attr(any(),rustfmt::skip)]pub use self::horn_satisfiability::HornSatisfiability;#[cfg_attr(any(),rustfmt::skip)]mod horn_satisfiability{#[doc=" Horn Satisfiability"]#[doc=""]#[doc=" $\\wedge(\\wedge_i v_{p_i}\\rightarrow v_q = f)$"]pub struct HornSatisfiability{literals:Vec<Option<bool>>,clauses:Vec<(usize,usize,bool)>,idx:Vec<Vec<usize>>,satisfiable:bool,stack:Vec<usize>}impl HornSatisfiability{pub fn new(size:usize)->Self{Self{literals:vec![None;size],clauses:vec![],idx:vec![vec![];size],satisfiable:true,stack:vec![]}}pub fn add_clause(&mut self,p:impl IntoIterator<Item=usize>,q:usize,f:bool){let mut count=0;let id=self.clauses.len();for p_i in p.into_iter(){if self.literals[p_i]!=Some(true){self.idx[p_i].push(id);count+=1;}}self.clauses.push((count,q,f));if count==0{self.stack.push(id);self.resolve();}}pub fn is_satisfiable(&self)->bool{self.satisfiable}pub fn solve(&self)->Option<Vec<bool>>{if!self.satisfiable{return None;}Some(self.literals.iter().map(|&x|x.unwrap_or(false)).collect())}fn resolve(&mut self){while let Some(id)=self.stack.pop(){let(_count,q,f)=self.clauses[id];self.satisfiable&=self.literals[q]!=Some(!f);self.literals[q]=Some(f);if f{while let Some(i)=self.idx[q].pop(){let(ref mut count,_,_)=self.clauses[i];*count-=1;if*count==0{self.stack.push(i);}}}}}}}