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}