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

use super::clause::{Clause, VClause};
use super::Matrix;
use crate::{Lit, LitMat, Signed};

impl<P: Clone, C: Clone, V: Clone> Matrix<Lit<Signed<P>, C, V>, V> {
    /// A matrix is positive if some of its elements are positive.
    pub fn positive(&self) -> Self {
        self.iter().filter_map(|cl| cl.positive()).collect()
    }
}

impl<P: Clone, C: Clone, V: Clone> Clause<Lit<Signed<P>, C, V>, Matrix<Lit<Signed<P>, C, V>, V>> {
    /// A clause is positive if all its elements are positive.
    pub fn positive(&self) -> Option<Self> {
        self.iter().map(|lm| lm.positive()).collect()
    }
}

impl<P: Clone, C: Clone, V: Clone> VClause<Lit<Signed<P>, C, V>, V> {
    /// A clause is positive if all its elements are positive.
    pub fn positive(&self) -> Option<Self> {
        self.1.positive().map(|cl| Self(self.0.clone(), cl))
    }
}

impl<P: Clone, C: Clone, V: Clone> LitMat<Lit<Signed<P>, C, V>, Matrix<Lit<Signed<P>, C, V>, V>> {
    /// A litmat is positive if it is a negative literal or if it is a non-empty positive matrix.
    pub fn positive(&self) -> Option<Self> {
        match self {
            LitMat::Lit(l) => l.head().is_sign_negative().then(|| LitMat::Lit(l.clone())),
            LitMat::Mat(m) => Some(m.positive())
                .filter(|m| !m.is_empty())
                .map(LitMat::Mat),
        }
    }
}