cop/lean/
clause.rs

1use crate::fof::Dnf;
2use crate::{Clause, Lit};
3use alloc::vec::Vec;
4
5impl<P, C, V> Clause<Lit<P, C, V>> {
6    /// All variables occurring in a clause.
7    pub fn vars(&self) -> impl Iterator<Item = &V> {
8        self.iter().flat_map(|lit| lit.vars())
9    }
10}
11
12impl<L: Eq> From<Dnf<L>> for Clause<L> {
13    fn from(fm: Dnf<L>) -> Self {
14        match fm {
15            Dnf::Disj(fms) => {
16                let fms = fms.into_iter().rev().map(Self::from);
17                fms.reduce(|acc, x| x.union(acc)).unwrap_or_default()
18            }
19            Dnf::Lit(lit) => Self(Vec::from([lit])),
20        }
21    }
22}
cop/lean/clause.rs

cop/lean/
clause.rs
