cop/lean/
matrix.rs

1use super::Contrapositive;
2use crate::fof::Cnf;
3use crate::{Clause, Lit};
4
5/// A matrix of clauses.
6pub type Matrix<L> = crate::Matrix<Clause<L>>;
7
8impl<L: Eq> From<Cnf<L>> for Matrix<L> {
9    fn from(fm: Cnf<L>) -> Self {
10        match fm {
11            Cnf::Conj(fms) => fms
12                .into_iter()
13                .flat_map(|fm| Self::from(fm).into_iter())
14                .collect(),
15            Cnf::Disj(disj) => core::iter::once(Clause::from(disj)).collect(),
16        }
17    }
18}
19
20impl<P, C, V: Clone + Ord> Matrix<Lit<P, C, V>> {
21    /// Decompose a matrix into contrapositives.
22    pub fn contrapositives(&self) -> impl Iterator<Item = Contrapositive<Lit<P, C, V>, V>> {
23        self.into_iter().flat_map(|cl| {
24            let max_var = cl.vars().max();
25            cl.contrapositives().map(move |contra| Contrapositive {
26                contra,
27                vars: max_var.cloned(),
28            })
29        })
30    }
31}
cop/lean/matrix.rs

cop/lean/
matrix.rs
