logic_form/dagcnf/
mod.rs

1mod occur;
2pub mod simplify;
3pub mod simulate;
4
5use crate::{Lit, LitVec, LitVvec, Var, VarMap};
6use giputils::hash::{GHashMap, GHashSet};
7use std::{
8    iter::{Flatten, Zip, once},
9    ops::{Index, RangeInclusive},
10    slice,
11};
12
13#[derive(Debug, Clone)]
14pub struct DagCnf {
15    max_var: Var,
16    cnf: VarMap<LitVvec>,
17    pub dep: VarMap<Vec<Var>>,
18}
19
20impl DagCnf {
21    #[inline]
22    pub fn new() -> Self {
23        Self::default()
24    }
25
26    #[inline]
27    pub fn new_var(&mut self) -> Var {
28        self.max_var += 1;
29        self.dep.reserve(self.max_var);
30        self.cnf.reserve(self.max_var);
31        self.max_var
32    }
33
34    #[inline]
35    pub fn new_var_to(&mut self, n: Var) {
36        while self.max_var < n {
37            self.new_var();
38        }
39    }
40
41    #[inline]
42    pub fn max_var(&self) -> Var {
43        self.max_var
44    }
45
46    #[inline]
47    #[allow(clippy::len_without_is_empty)]
48    pub fn len(&self) -> usize {
49        self.clause().count()
50    }
51
52    #[inline]
53    pub fn clause(&self) -> Flatten<slice::Iter<'_, LitVvec>> {
54        self.cnf.iter().flatten()
55    }
56
57    #[inline]
58    pub fn iter(&self) -> Zip<RangeInclusive<Var>, std::slice::Iter<'_, LitVvec>> {
59        (Var::CONST..=self.max_var).zip(self.cnf.iter())
60    }
61
62    #[inline]
63    pub fn add_rel(&mut self, n: Var, rel: &[LitVec]) {
64        self.new_var_to(n);
65        if n.is_constant() {
66            return;
67        }
68        assert!(self.dep[n].is_empty() && self.cnf[n].is_empty());
69        for mut r in rel.iter().cloned() {
70            r.sort();
71            assert!(r.last().var() == n);
72            self.cnf[n].push(r);
73        }
74        self.dep[n] = deps(n, &self.cnf[n]);
75    }
76
77    #[inline]
78    pub fn del_rel(&mut self, n: Var) {
79        self.dep[n].clear();
80        self.cnf[n].clear();
81    }
82
83    #[inline]
84    pub fn has_rel(&self, n: Var) -> bool {
85        !n.is_constant() && !self.cnf[n].is_empty()
86    }
87
88    #[inline]
89    pub fn new_and(&mut self, ands: impl IntoIterator<Item = Lit>) -> Lit {
90        let ands: Vec<_> = ands.into_iter().collect();
91        if ands.is_empty() {
92            Lit::constant(true)
93        } else if ands.len() == 1 {
94            ands[0]
95        } else {
96            let n = self.new_var().lit();
97            self.add_rel(n.var(), &LitVvec::cnf_and(n, &ands));
98            n
99        }
100    }
101
102    #[inline]
103    pub fn new_or(&mut self, ors: impl IntoIterator<Item = Lit>) -> Lit {
104        let ors: Vec<_> = ors.into_iter().collect();
105        if ors.is_empty() {
106            Lit::constant(false)
107        } else if ors.len() == 1 {
108            ors[0]
109        } else {
110            let n = self.new_var().lit();
111            self.add_rel(n.var(), &LitVvec::cnf_or(n, &ors));
112            n
113        }
114    }
115
116    #[inline]
117    pub fn new_xor(&mut self, x: Lit, y: Lit) -> Lit {
118        let n = self.new_var().lit();
119        self.add_rel(n.var(), &LitVvec::cnf_xor(n, x, y));
120        n
121    }
122
123    #[inline]
124    pub fn new_xnor(&mut self, x: Lit, y: Lit) -> Lit {
125        let n = self.new_var().lit();
126        self.add_rel(n.var(), &LitVvec::cnf_xnor(n, x, y));
127        n
128    }
129
130    #[inline]
131    pub fn new_imply(&mut self, x: Lit, y: Lit) -> Lit {
132        let n = self.new_var().lit();
133        self.add_rel(n.var(), &LitVvec::cnf_or(n, &[!x, y]));
134        n
135    }
136
137    #[inline]
138    pub fn new_ite(&mut self, c: Lit, t: Lit, e: Lit) -> Lit {
139        let n = self.new_var().lit();
140        self.add_rel(n.var(), &LitVvec::cnf_ite(n, c, t, e));
141        n
142    }
143
144    pub fn fanins(&self, var: impl Iterator<Item = Var>) -> GHashSet<Var> {
145        let mut marked = GHashSet::new();
146        let mut queue = vec![];
147        for v in var {
148            marked.insert(v);
149            queue.push(v);
150        }
151        while let Some(v) = queue.pop() {
152            for d in self.dep[v].iter() {
153                if !marked.contains(d) {
154                    marked.insert(*d);
155                    queue.push(*d);
156                }
157            }
158        }
159        marked
160    }
161
162    pub fn fanouts(&self, var: impl Iterator<Item = Var>) -> GHashSet<Var> {
163        let mut marked = GHashSet::from_iter(var);
164        for v in Var::CONST..=self.max_var {
165            if self.dep[v].iter().any(|d| marked.contains(d)) {
166                marked.insert(v);
167            }
168        }
169        marked
170    }
171
172    pub fn root(&self) -> GHashSet<Var> {
173        let mut root = GHashSet::from_iter(
174            (Var::new(0)..=self.max_var()).filter(|v| !self.dep[*v].is_empty()),
175        );
176        for d in self.dep.iter() {
177            for d in d.iter() {
178                root.remove(d);
179            }
180        }
181        root
182    }
183
184    pub fn pol_filter(&mut self, pol: impl IntoIterator<Item = Lit>) {
185        for p in pol {
186            self.cnf[p.var()].retain(|cls| cls.last() != !p);
187            self.dep[p.var()] = deps(p.var(), &self.cnf[p.var()]);
188        }
189    }
190
191    pub fn rearrange(&mut self, additional: impl Iterator<Item = Var>) -> GHashMap<Var, Var> {
192        let mut domain = GHashSet::from_iter(additional.chain(once(Var::CONST)));
193        for cls in self.clause() {
194            for l in cls.iter() {
195                domain.insert(l.var());
196            }
197        }
198        let mut domain = Vec::from_iter(domain);
199        domain.sort();
200        let mut domain_map = GHashMap::new();
201        let mut res = DagCnf::new();
202        for (i, d) in domain.iter().enumerate() {
203            let v = Var::new(i);
204            res.new_var_to(v);
205            domain_map.insert(*d, v);
206        }
207        let map_lit = |l: &Lit| l.map_var(|v| domain_map[&v]);
208        for (d, v) in domain_map.iter() {
209            if d.is_constant() {
210                continue;
211            }
212            let mut new_cls = Vec::new();
213            for cls in self.cnf[*d].iter() {
214                new_cls.push(cls.iter().map(map_lit).collect());
215            }
216            res.add_rel(*v, &new_cls);
217        }
218        *self = res;
219        domain_map
220    }
221
222    pub fn map(&self, map: impl Fn(Var) -> Var) -> Self {
223        assert!(map(Var::CONST) == Var::CONST);
224        let mut res = DagCnf::new();
225        for (v, rel) in self.iter() {
226            let new_cls: Vec<_> = rel.iter().map(|cls| cls.map(|l| l.map_var(&map))).collect();
227            res.add_rel(map(v), &new_cls);
228        }
229        res
230    }
231}
232
233impl Default for DagCnf {
234    fn default() -> Self {
235        let max_var = Var::CONST;
236        let mut cnf: VarMap<LitVvec> = VarMap::new_with(max_var);
237        cnf[max_var].push(LitVec::from(Lit::constant(true)));
238        Self {
239            max_var,
240            cnf,
241            dep: VarMap::new_with(max_var),
242        }
243    }
244}
245
246impl Index<Var> for DagCnf {
247    type Output = [LitVec];
248
249    #[inline]
250    fn index(&self, index: Var) -> &Self::Output {
251        &self.cnf[index]
252    }
253}
254
255#[inline]
256fn deps(n: Var, cnf: &[LitVec]) -> Vec<Var> {
257    let mut dep = GHashSet::new();
258    for cls in cnf.iter() {
259        for l in cls.iter() {
260            dep.insert(l.var());
261        }
262    }
263    dep.remove(&n);
264    dep.into_iter().collect()
265}