logic_form/
litvec.rs

1use crate::{Lit, Var};
2use giputils::hash::GHashSet;
3use std::{
4    cmp::Ordering,
5    fmt::{self, Debug, Display},
6    ops::{Deref, DerefMut, Not},
7    slice,
8};
9
10#[derive(Clone, Hash, PartialEq, Eq)]
11pub struct LitVec {
12    lits: Vec<Lit>,
13}
14
15impl LitVec {
16    #[inline]
17    pub fn new() -> Self {
18        LitVec { lits: Vec::new() }
19    }
20
21    #[inline]
22    pub fn new_with(c: usize) -> Self {
23        LitVec {
24            lits: Vec::with_capacity(c),
25        }
26    }
27
28    #[inline]
29    pub fn last(&self) -> Lit {
30        #[cfg(debug_assertions)]
31        {
32            self.lits.last().copied().unwrap()
33        }
34        #[cfg(not(debug_assertions))]
35        unsafe {
36            self.lits.last().copied().unwrap_unchecked()
37        }
38    }
39
40    #[inline]
41    pub fn cls_simp(&mut self) {
42        self.sort();
43        self.dedup();
44        for i in 1..self.len() {
45            if self[i] == !self[i - 1] {
46                self.clear();
47                return;
48            }
49        }
50    }
51
52    #[inline]
53    pub fn subsume(&self, o: &[Lit]) -> bool {
54        if self.len() > o.len() {
55            return false;
56        }
57        'n: for x in self.iter() {
58            for y in o.iter() {
59                if x == y {
60                    continue 'n;
61                }
62            }
63            return false;
64        }
65        true
66    }
67
68    pub fn subsume_execpt_one(&self, o: &[Lit]) -> (bool, Option<Lit>) {
69        if self.len() > o.len() {
70            return (false, None);
71        }
72        let mut diff = None;
73        'n: for x in self.iter() {
74            for y in o.iter() {
75                if x == y {
76                    continue 'n;
77                }
78                if diff.is_none() && x.var() == y.var() {
79                    diff = Some(*x);
80                    continue 'n;
81                }
82            }
83            return (false, None);
84        }
85
86        (diff.is_none(), diff)
87    }
88
89    #[inline]
90    pub fn ordered_subsume(&self, cube: &LitVec) -> bool {
91        debug_assert!(self.is_sorted());
92        debug_assert!(cube.is_sorted());
93        if self.len() > cube.len() {
94            return false;
95        }
96        let mut j = 0;
97        for i in 0..self.len() {
98            while j < cube.len() && self[i].0 > cube[j].0 {
99                j += 1;
100            }
101            if j == cube.len() || self[i] != cube[j] {
102                return false;
103            }
104        }
105        true
106    }
107
108    #[inline]
109    pub fn ordered_subsume_execpt_one(&self, cube: &LitVec) -> (bool, Option<Lit>) {
110        debug_assert!(self.is_sorted());
111        debug_assert!(cube.is_sorted());
112        let mut diff = None;
113        if self.len() > cube.len() {
114            return (false, None);
115        }
116        let mut j = 0;
117        for i in 0..self.len() {
118            while j < cube.len() && self[i].var() > cube[j].var() {
119                j += 1;
120            }
121            if j == cube.len() {
122                return (false, None);
123            }
124            if self[i] != cube[j] {
125                if diff.is_none() && self[i].var() == cube[j].var() {
126                    diff = Some(self[i]);
127                } else {
128                    return (false, None);
129                }
130            }
131        }
132        (diff.is_none(), diff)
133    }
134
135    #[inline]
136    pub fn intersection(&self, cube: &LitVec) -> LitVec {
137        let x_lit_set = self.iter().collect::<GHashSet<&Lit>>();
138        let y_lit_set = cube.iter().collect::<GHashSet<&Lit>>();
139        Self {
140            lits: x_lit_set
141                .intersection(&y_lit_set)
142                .copied()
143                .copied()
144                .collect(),
145        }
146    }
147
148    #[inline]
149    pub fn ordered_intersection(&self, cube: &LitVec) -> LitVec {
150        debug_assert!(self.is_sorted());
151        debug_assert!(cube.is_sorted());
152        let mut res = LitVec::new();
153        let mut i = 0;
154        for l in self.iter() {
155            while i < cube.len() && cube[i] < *l {
156                i += 1;
157            }
158            if i == cube.len() {
159                break;
160            }
161            if *l == cube[i] {
162                res.push(*l);
163            }
164        }
165        res
166    }
167
168    #[inline]
169    pub fn resolvent(&self, other: &LitVec, v: Var) -> Option<LitVec> {
170        let (x, y) = if self.len() < other.len() {
171            (self, other)
172        } else {
173            (other, self)
174        };
175        let mut new = LitVec::new();
176        'n: for x in x.iter() {
177            if x.var() != v {
178                for y in y.iter() {
179                    if x.var() == y.var() {
180                        if *x == !*y {
181                            return None;
182                        } else {
183                            continue 'n;
184                        }
185                    }
186                }
187                new.push(*x);
188            }
189        }
190        new.extend(y.iter().filter(|l| l.var() != v).copied());
191        Some(new)
192    }
193
194    #[inline]
195    pub fn ordered_resolvent(&self, other: &LitVec, v: Var) -> Option<LitVec> {
196        debug_assert!(self.is_sorted());
197        debug_assert!(other.is_sorted());
198        let (x, y) = if self.len() < other.len() {
199            (self, other)
200        } else {
201            (other, self)
202        };
203        let mut new = LitVec::new_with(self.len() + other.len());
204        let (mut i, mut j) = (0, 0);
205        while i < x.len() {
206            if x[i].var() == v {
207                i += 1;
208                continue;
209            }
210            while j < y.len() && y[j].var() < x[i].var() {
211                j += 1;
212            }
213            if j < y.len() && x[i].var() == y[j].var() {
214                if x[i] == !y[j] {
215                    return None;
216                }
217            } else {
218                new.push(x[i]);
219            }
220            i += 1;
221        }
222        new.extend(y.iter().filter(|l| l.var() != v).copied());
223        Some(new)
224    }
225
226    #[inline]
227    pub fn map(&self, f: impl Fn(Lit) -> Lit) -> LitVec {
228        let mut new = LitVec::new_with(self.len());
229        for l in self.iter() {
230            new.push(f(*l));
231        }
232        new
233    }
234}
235
236impl Default for LitVec {
237    fn default() -> Self {
238        Self::new()
239    }
240}
241
242impl Deref for LitVec {
243    type Target = Vec<Lit>;
244
245    #[inline]
246    fn deref(&self) -> &Self::Target {
247        &self.lits
248    }
249}
250
251impl DerefMut for LitVec {
252    #[inline]
253    fn deref_mut(&mut self) -> &mut Self::Target {
254        &mut self.lits
255    }
256}
257
258impl PartialOrd for LitVec {
259    #[inline]
260    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
261        Some(self.cmp(other))
262    }
263}
264
265impl Ord for LitVec {
266    #[inline]
267    fn cmp(&self, other: &Self) -> Ordering {
268        debug_assert!(self.is_sorted());
269        debug_assert!(other.is_sorted());
270        let min_index = self.len().min(other.len());
271        for i in 0..min_index {
272            match self[i].0.cmp(&other[i].0) {
273                Ordering::Less => return Ordering::Less,
274                Ordering::Equal => {}
275                Ordering::Greater => return Ordering::Greater,
276            }
277        }
278        self.len().cmp(&other.len())
279    }
280}
281
282impl Not for LitVec {
283    type Output = LitVec;
284
285    #[inline]
286    fn not(self) -> Self::Output {
287        let lits = self.lits.iter().map(|lit| !*lit).collect();
288        LitVec { lits }
289    }
290}
291
292impl Not for &LitVec {
293    type Output = LitVec;
294
295    #[inline]
296    fn not(self) -> Self::Output {
297        let lits = self.lits.iter().map(|lit| !*lit).collect();
298        LitVec { lits }
299    }
300}
301
302impl<const N: usize> From<[Lit; N]> for LitVec {
303    #[inline]
304    fn from(s: [Lit; N]) -> Self {
305        Self { lits: Vec::from(s) }
306    }
307}
308
309impl From<Lit> for LitVec {
310    #[inline]
311    fn from(l: Lit) -> Self {
312        Self { lits: vec![l] }
313    }
314}
315
316impl From<&[Lit]> for LitVec {
317    #[inline]
318    fn from(s: &[Lit]) -> Self {
319        Self { lits: Vec::from(s) }
320    }
321}
322
323impl From<LitVec> for Vec<Lit> {
324    #[inline]
325    fn from(val: LitVec) -> Self {
326        val.lits
327    }
328}
329
330impl FromIterator<Lit> for LitVec {
331    #[inline]
332    fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self {
333        Self {
334            lits: Vec::from_iter(iter),
335        }
336    }
337}
338
339impl IntoIterator for LitVec {
340    type Item = Lit;
341    type IntoIter = std::vec::IntoIter<Lit>;
342
343    #[inline]
344    fn into_iter(self) -> Self::IntoIter {
345        self.lits.into_iter()
346    }
347}
348
349impl<'a> IntoIterator for &'a LitVec {
350    type Item = &'a Lit;
351    type IntoIter = slice::Iter<'a, Lit>;
352
353    #[inline]
354    fn into_iter(self) -> Self::IntoIter {
355        self.lits.iter()
356    }
357}
358
359impl AsRef<[Lit]> for LitVec {
360    #[inline]
361    fn as_ref(&self) -> &[Lit] {
362        self.as_slice()
363    }
364}
365
366impl Display for LitVec {
367    #[inline]
368    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
369        self.lits.fmt(f)
370    }
371}
372
373impl Debug for LitVec {
374    #[inline]
375    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
376        self.lits.fmt(f)
377    }
378}
logic_form/litvec.rs

logic_form/
litvec.rs
