1use {super::AssignStack, crate::types::*, std::fmt};
5
6#[cfg(feature = "trail_saving")]
7use super::TrailSavingIF;
8
9#[derive(Clone, Debug, Default)]
15pub struct VarIdHeap {
16 heap: Vec<u32>,
18 idxs: Vec<u32>,
21}
22
23impl fmt::Display for VarIdHeap {
24 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
25 write!(
26 f,
27 " - seek pointer - nth -> var: {:?}\n - var -> nth: {:?}",
28 self.heap, self.idxs,
29 )
30 }
31}
32
33impl VarIdHeap {
34 pub fn new(n: usize) -> Self {
35 let mut heap = Vec::with_capacity(n + 1);
36 let mut idxs = Vec::with_capacity(n + 1);
37 heap.push(0);
38 idxs.push(n as u32);
39 for i in 1..=n {
40 heap.push(i as u32);
41 idxs.push(i as u32);
42 }
43 idxs[0] = n as u32;
44 VarIdHeap { heap, idxs }
45 }
46}
47
48pub trait VarHeapIF {
50 fn clear_heap(&mut self);
51 fn expand_heap(&mut self);
52 fn insert_heap(&mut self, vi: VarId);
53 fn update_heap(&mut self, v: VarId);
54 fn get_heap_root(&mut self) -> VarId;
55 fn percolate_up(&mut self, start: u32);
56 fn percolate_down(&mut self, start: u32);
57 fn remove_from_heap(&mut self, vs: VarId);
58}
59
60impl VarHeapIF for AssignStack {
61 fn clear_heap(&mut self) {
62 self.var_order.clear();
63 }
64 fn expand_heap(&mut self) {
65 let id = self.var_order.heap.len() as u32;
67 self.var_order.heap.push(id);
68 self.var_order.idxs.push(id);
69 }
70 fn update_heap(&mut self, v: VarId) {
71 debug_assert!(v != 0, "Invalid VarId");
72 let start = self.var_order.idxs[v];
73 if self.var_order.contains(v) {
74 self.percolate_up(start);
75 }
76 }
77 fn insert_heap(&mut self, vi: VarId) {
78 let i = self.var_order.insert(vi);
79 self.percolate_up(i as u32);
80 }
81 fn get_heap_root(&mut self) -> VarId {
82 #[cfg(feature = "trail_saving")]
83 if self.var_order.is_empty() {
84 self.clear_saved_trail();
85 }
86 let vs = self.var_order.get_root();
87 if 1 < self.var_order.len() {
88 self.percolate_down(1);
89 }
90 vs
91 }
92 fn percolate_up(&mut self, start: u32) {
93 let mut q = start;
94 let vq = self.var_order.heap[q as usize];
95 debug_assert!(0 < vq, "size of heap is too small");
96 let aq = self.activity(vq as usize);
97 loop {
98 let p = q / 2;
99 if p == 0 {
100 self.var_order.heap[q as usize] = vq;
101 debug_assert!(vq != 0, "Invalid index in percolate_up");
102 self.var_order.idxs[vq as usize] = q;
103 return;
104 } else {
105 let vp = self.var_order.heap[p as usize];
106 let ap = self.activity(vp as usize);
107 if ap < aq {
108 self.var_order.heap[q as usize] = vp;
110 debug_assert!(vq != 0, "Invalid index in percolate_up");
111 self.var_order.idxs[vp as usize] = q;
112 q = p;
113 } else {
114 self.var_order.heap[q as usize] = vq;
115 debug_assert!(vq != 0, "Invalid index in percolate_up");
116 self.var_order.idxs[vq as usize] = q;
117 return;
118 }
119 }
120 }
121 }
122 fn percolate_down(&mut self, start: u32) {
123 let n = self.var_order.len();
124 let mut i = start;
125 let vi = self.var_order.heap[i as usize];
126 let ai = self.activity(vi as usize);
127 loop {
128 let l = 2 * i; if l < n as u32 {
130 let vl = self.var_order.heap[l as usize];
131 let al = self.activity(vl as usize);
132 let r = l + 1; let (target, vc, ac) = if r < (n as u32)
134 && al < self.activity(self.var_order.heap[r as usize] as usize)
135 {
136 let vr = self.var_order.heap[r as usize];
137 (r, vr, self.activity(vr as usize))
138 } else {
139 (l, vl, al)
140 };
141 if ai < ac {
142 self.var_order.heap[i as usize] = vc;
143 self.var_order.idxs[vc as usize] = i;
144 i = target;
145 } else {
146 self.var_order.heap[i as usize] = vi;
147 debug_assert!(vi != 0, "invalid index");
148 self.var_order.idxs[vi as usize] = i;
149 return;
150 }
151 } else {
152 self.var_order.heap[i as usize] = vi;
153 debug_assert!(vi != 0, "invalid index");
154 self.var_order.idxs[vi as usize] = i;
155 return;
156 }
157 }
158 }
159 fn remove_from_heap(&mut self, vi: VarId) {
160 if let Some(i) = self.var_order.remove(vi) {
161 self.percolate_down(i as u32);
162 }
163 }
164}
165
166trait VarOrderIF {
167 fn clear(&mut self);
168 fn contains(&self, v: VarId) -> bool;
169 fn get_root(&mut self) -> VarId;
170 fn len(&self) -> usize;
171 fn insert(&mut self, vi: VarId) -> usize;
172 fn is_empty(&self) -> bool;
173 fn remove(&mut self, vi: VarId) -> Option<usize>;
174}
175
176impl VarOrderIF for VarIdHeap {
177 fn clear(&mut self) {
178 for i in 0..self.idxs.len() {
179 self.idxs[i] = i as u32;
180 self.heap[i] = i as u32;
181 }
182 }
183 fn contains(&self, v: VarId) -> bool {
184 self.idxs[v] <= self.idxs[0]
185 }
186 fn get_root(&mut self) -> VarId {
187 let s: usize = 1;
188 let vs = self.heap[s];
189 let n = self.idxs[0];
190 let vn = self.heap[n as usize];
191 debug_assert!(vn != 0, "Invalid VarId for heap: vn {vn}, n {n}");
192 debug_assert!(vs != 0, "Invalid VarId for heap: vs {vs}, n {n}");
193 self.heap.swap(n as usize, s);
194 self.idxs.swap(vn as usize, vs as usize);
195 self.idxs[0] -= 1;
196 vs as VarId
197 }
198 fn len(&self) -> usize {
199 self.idxs[0] as usize
200 }
201 #[allow(clippy::unnecessary_cast)]
202 fn insert(&mut self, vi: VarId) -> usize {
203 if self.contains(vi) {
204 return self.idxs[vi as usize] as usize;
205 }
206 let i = self.idxs[vi];
207 let n = self.idxs[0] + 1;
208 let vn = self.heap[n as usize];
209 self.heap.swap(i as usize, n as usize);
210 self.idxs.swap(vi, vn as usize);
211 self.idxs[0] = n;
212 n as usize
213 }
214 fn is_empty(&self) -> bool {
215 self.idxs[0] == 0
216 }
217 fn remove(&mut self, vi: VarId) -> Option<usize> {
218 let i = self.idxs[vi];
219 let n = self.idxs[0];
220 debug_assert_ne!(i, 0);
221 if n < i {
222 return None;
223 }
224 let vn = self.heap[n as usize];
225 self.heap.swap(n as usize, i as usize);
226 self.idxs.swap(vn as usize, vi);
227 self.idxs[0] -= 1;
228 if 1 < self.idxs[0] {
229 return Some(i as usize);
230 }
231 None
232 }
233}
234
235impl VarIdHeap {
236 #[allow(dead_code)]
237 fn peek(&self) -> VarId {
238 self.heap[1] as VarId
239 }
240 #[allow(dead_code)]
241 fn check(&self, s: &str) {
242 let h = &mut self.heap.clone()[1..];
243 let d = &mut self.idxs.clone()[1..];
244 h.sort_unstable();
245 d.sort_unstable();
246 for i in 0..h.len() {
247 if h[i] != i as u32 + 1 {
248 panic!("heap {} {} {:?}", i, h[i], h);
249 }
250 if d[i] != i as u32 + 1 {
251 panic!("idxs {} {} {:?}", i, d[i], d);
252 }
253 }
254 println!(" - pass var_order test at {s}");
255 }
256}