logic_form/
litordvec.rs

1use crate::{Lit, LitSet, LitVec};
2use ahash::AHasher;
3use std::hash::{Hash, Hasher};
4use std::slice;
5use std::{
6    cmp::Ordering,
7    fmt::{self, Display},
8    ops::{Deref, DerefMut},
9};
10
11#[derive(Debug, Default, Clone)]
12pub struct LitOrdVec {
13    cube: LitVec,
14    sign: u128,
15    hash: u64,
16}
17
18impl Deref for LitOrdVec {
19    type Target = LitVec;
20
21    #[inline]
22    fn deref(&self) -> &Self::Target {
23        &self.cube
24    }
25}
26
27impl DerefMut for LitOrdVec {
28    #[inline]
29    fn deref_mut(&mut self) -> &mut Self::Target {
30        &mut self.cube
31    }
32}
33
34impl PartialEq for LitOrdVec {
35    #[inline]
36    fn eq(&self, other: &Self) -> bool {
37        if self.hash != other.hash || self.sign != other.sign || self.len() != other.len() {
38            return false;
39        }
40        for i in 0..self.cube.len() {
41            if self[i] != other[i] {
42                return false;
43            }
44        }
45        true
46    }
47}
48
49impl Eq for LitOrdVec {}
50
51impl PartialOrd for LitOrdVec {
52    #[inline]
53    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
54        Some(self.cmp(other))
55    }
56}
57
58impl Ord for LitOrdVec {
59    #[inline]
60    fn cmp(&self, other: &Self) -> Ordering {
61        self.cube.cmp(&other.cube)
62    }
63}
64
65impl LitOrdVec {
66    #[inline]
67    pub fn new(mut cube: LitVec) -> Self {
68        cube.sort();
69        let mut sign = 0;
70        for l in cube.iter() {
71            sign |= 1 << (Into::<u32>::into(*l) % u128::BITS);
72        }
73        let mut hasher = AHasher::default();
74        cube.hash(&mut hasher);
75        Self {
76            cube,
77            sign,
78            hash: hasher.finish(),
79        }
80    }
81
82    #[inline]
83    pub fn cube(&self) -> &LitVec {
84        &self.cube
85    }
86
87    #[inline]
88    fn var_sign(&self) -> u128 {
89        ((self.sign >> 1) | self.sign) & 113427455640312821154458202477256070485_u128
90    }
91
92    #[inline]
93    pub fn subsume(&self, other: &LitOrdVec) -> bool {
94        if self.cube.len() > other.cube.len() {
95            return false;
96        }
97        if self.sign & other.sign != self.sign {
98            return false;
99        }
100        self.cube.ordered_subsume(&other.cube)
101    }
102
103    #[inline]
104    pub fn subsume_execpt_one(&self, other: &LitOrdVec) -> (bool, Option<Lit>) {
105        if self.cube.len() > other.cube.len() {
106            return (false, None);
107        }
108        let ss = self.var_sign();
109        if ss & other.var_sign() != ss {
110            return (false, None);
111        }
112        self.cube.ordered_subsume_execpt_one(&other.cube)
113    }
114
115    #[inline]
116    pub fn subsume_set(&self, other: &LitOrdVec, other_lits: &LitSet) -> bool {
117        if self.cube.len() > other.cube.len() {
118            return false;
119        }
120        if self.sign & other.sign != self.sign {
121            return false;
122        }
123        for l in self.iter() {
124            if !other_lits.has(*l) {
125                return false;
126            }
127        }
128        true
129    }
130}
131
132impl Hash for LitOrdVec {
133    #[inline]
134    fn hash<H: Hasher>(&self, state: &mut H) {
135        self.hash.hash(state);
136    }
137}
138
139impl Display for LitOrdVec {
140    #[inline]
141    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
142        Display::fmt(&self.cube, f)
143    }
144}
145
146pub fn lemmas_subsume_simplify(mut lemmas: Vec<LitOrdVec>) -> Vec<LitOrdVec> {
147    lemmas.sort_by_key(|l| l.len());
148    let mut i = 0;
149    while i < lemmas.len() {
150        if lemmas[i].is_empty() {
151            i += 1;
152            continue;
153        }
154        let mut update = false;
155        for j in i + 1..lemmas.len() {
156            if lemmas[j].is_empty() {
157                continue;
158            }
159            let (res, diff) = lemmas[i].subsume_execpt_one(&lemmas[j]);
160            if res {
161                lemmas[j] = Default::default();
162                continue;
163            } else if let Some(diff) = diff {
164                if lemmas[i].len() == lemmas[j].len() {
165                    update = true;
166                    let mut cube = lemmas[i].cube().clone();
167                    cube.retain(|l| *l != diff);
168                    lemmas[i] = LitOrdVec::new(cube);
169                    lemmas[j] = Default::default();
170                } else {
171                    let mut cube = lemmas[j].cube().clone();
172                    cube.retain(|l| *l != !diff);
173                    lemmas[j] = LitOrdVec::new(cube);
174                }
175            }
176        }
177        if !update {
178            i += 1;
179        }
180    }
181    lemmas.retain(|l| !l.is_empty());
182    lemmas
183}
184
185impl IntoIterator for LitOrdVec {
186    type Item = Lit;
187    type IntoIter = std::vec::IntoIter<Lit>;
188
189    #[inline]
190    fn into_iter(self) -> Self::IntoIter {
191        self.cube.clone().into_iter()
192    }
193}
194
195impl<'a> IntoIterator for &'a LitOrdVec {
196    type Item = &'a Lit;
197    type IntoIter = slice::Iter<'a, Lit>;
198
199    #[inline]
200    fn into_iter(self) -> Self::IntoIter {
201        self.cube.iter()
202    }
203}
logic_form/litordvec.rs

logic_form/
litordvec.rs
