logic_form/
litvvec.rs

1use crate::{Lit, LitVec};
2use std::{
3    ops::{Deref, DerefMut},
4    slice, vec,
5};
6
7#[derive(Debug, Clone, Default)]
8pub struct LitVvec {
9    vec: Vec<LitVec>,
10}
11
12impl LitVvec {
13    #[inline]
14    pub fn new() -> Self {
15        Self::default()
16    }
17
18    #[inline]
19    pub fn cnf_and(n: Lit, lits: &[Lit]) -> Self {
20        let mut vec = Vec::new();
21        let mut cls = LitVec::from([n]);
22        for l in lits.iter() {
23            vec.push(LitVec::from([!n, *l]));
24            cls.push(!*l);
25        }
26        vec.push(cls);
27        Self { vec }
28    }
29
30    #[inline]
31    pub fn cnf_or(n: Lit, lits: &[Lit]) -> Self {
32        let mut vec = Vec::new();
33        let mut cls = LitVec::from([!n]);
34        for l in lits.iter() {
35            vec.push(LitVec::from([n, !*l]));
36            cls.push(*l);
37        }
38        vec.push(cls);
39        Self { vec }
40    }
41
42    #[inline]
43    pub fn cnf_assign(n: Lit, s: Lit) -> Self {
44        Self {
45            vec: vec![LitVec::from([n, !s]), LitVec::from([!n, s])],
46        }
47    }
48
49    #[inline]
50    pub fn cnf_xor(n: Lit, x: Lit, y: Lit) -> Self {
51        Self {
52            vec: vec![
53                LitVec::from([!x, y, n]),
54                LitVec::from([x, !y, n]),
55                LitVec::from([x, y, !n]),
56                LitVec::from([!x, !y, !n]),
57            ],
58        }
59    }
60
61    #[inline]
62    pub fn cnf_xnor(n: Lit, x: Lit, y: Lit) -> Self {
63        Self {
64            vec: vec![
65                LitVec::from([!x, y, !n]),
66                LitVec::from([x, !y, !n]),
67                LitVec::from([x, y, n]),
68                LitVec::from([!x, !y, n]),
69            ],
70        }
71    }
72
73    #[inline]
74    pub fn cnf_ite(n: Lit, c: Lit, t: Lit, e: Lit) -> Self {
75        Self {
76            vec: vec![
77                LitVec::from([t, !c, !n]),
78                LitVec::from([!t, !c, n]),
79                LitVec::from([e, c, !n]),
80                LitVec::from([!e, c, n]),
81            ],
82        }
83    }
84
85    pub fn subsume_simplify(&mut self) {
86        self.sort_by_key(|l| l.len());
87        for c in self.iter_mut() {
88            c.sort();
89        }
90        let mut i = 0;
91        while i < self.len() {
92            if self[i].is_empty() {
93                i += 1;
94                continue;
95            }
96            let mut update = false;
97            for j in 0..self.len() {
98                if i == j {
99                    continue;
100                }
101                if self[j].is_empty() {
102                    continue;
103                }
104                let (res, diff) = self[i].ordered_subsume_execpt_one(&self[j]);
105                if res {
106                    self[j] = Default::default();
107                    continue;
108                } else if let Some(diff) = diff {
109                    if self[i].len() == self[j].len() {
110                        update = true;
111                        self[i].retain(|l| *l != diff);
112                        self[j] = Default::default();
113                    } else {
114                        self[j].retain(|l| *l != !diff);
115                    }
116                }
117            }
118            if !update {
119                i += 1;
120            }
121        }
122        self.retain(|l| !l.is_empty());
123    }
124}
125
126impl Deref for LitVvec {
127    type Target = Vec<LitVec>;
128
129    #[inline]
130    fn deref(&self) -> &Self::Target {
131        &self.vec
132    }
133}
134
135impl DerefMut for LitVvec {
136    #[inline]
137    fn deref_mut(&mut self) -> &mut Self::Target {
138        &mut self.vec
139    }
140}
141
142impl IntoIterator for LitVvec {
143    type Item = LitVec;
144    type IntoIter = vec::IntoIter<LitVec>;
145
146    #[inline]
147    fn into_iter(self) -> Self::IntoIter {
148        self.vec.into_iter()
149    }
150}
151
152impl<'a> IntoIterator for &'a LitVvec {
153    type Item = &'a LitVec;
154    type IntoIter = slice::Iter<'a, LitVec>;
155
156    #[inline]
157    fn into_iter(self) -> Self::IntoIter {
158        self.vec.iter()
159    }
160}
161
162impl FromIterator<LitVec> for LitVvec {
163    #[inline]
164    fn from_iter<T: IntoIterator<Item = LitVec>>(iter: T) -> Self {
165        Self {
166            vec: Vec::from_iter(iter),
167        }
168    }
169}
logic_form/litvvec.rs

logic_form/
litvvec.rs
