1
use std::fmt;
2

            
3
use crate::IncomingTransitions;
4
use super::IndexedPartition;
5
use super::Partition;
6

            
7
/// A partition that explicitly stores a list of blocks and their indexing into
8
/// the list of elements.
9
#[derive(Debug)]
10
pub struct BlockPartition {
11
    elements: Vec<usize>,
12
    blocks: Vec<Block>,
13

            
14
    // These are only used to provide O(1) marking of elemets.
15
    /// Stores the block index for each element.
16
    element_to_block: Vec<usize>,
17

            
18
    /// Stores the offset within the block for every element.
19
    element_offset: Vec<usize>,
20
}
21

            
22
impl BlockPartition {
23
    /// Create an initial partition where all the states are in a single block
24
    /// 0. And all the elements in the block are marked.
25
59
    pub fn new(num_of_elements: usize) -> BlockPartition {
26
59
        debug_assert!(num_of_elements > 0, "Cannot partition the empty set");
27

            
28
59
        let blocks = vec![Block::new(0, num_of_elements)];
29
59
        let elements = (0..num_of_elements).collect();
30
59
        let element_to_block = vec![0; num_of_elements];
31
59
        let element_to_block_offset = (0..num_of_elements).collect();
32
59

            
33
59
        BlockPartition {
34
59
            elements,
35
59
            element_to_block,
36
59
            element_offset: element_to_block_offset,
37
59
            blocks,
38
59
        }
39
59
    }
40

            
41
    /// Partition the elements of the given block into multiple new blocks based
42
    /// on the given partitioner; which returns a number for each marked
43
    /// element. Elements with the same number belong to the same block, and the
44
    /// returned numbers should be dense.
45
    ///
46
    /// Returns an iterator over the new block indices, where the first element
47
    /// is the index of the block that was partitioned. And that block is the
48
    /// largest block.
49
156704
    pub fn partition_marked_with<F>(
50
156704
        &mut self,
51
156704
        block_index: usize,
52
156704
        builder: &mut BlockPartitionBuilder,
53
156704
        mut partitioner: F,
54
156704
    ) -> impl Iterator<Item = usize>
55
156704
    where
56
156704
        F: FnMut(usize, &BlockPartition) -> usize,
57
156704
    {
58
156704
        let block = self.blocks[block_index];
59
156704
        debug_assert!(
60
156704
            block.has_marked(),
61
            "Cannot partition marked elements of a block without marked elements"
62
        );
63

            
64
156704
        if block.len() == 1 {
65
            // Block only has one element, so trivially partitioned.
66
151772
            self.blocks[block_index].unmark_all();
67
151772
            return (block_index..=block_index).chain(0..0);
68
4932
        }
69
4932

            
70
4932
        // Keeps track of the block index for every element in this block by index.
71
4932
        builder.index_to_block.clear();
72
4932
        builder.block_sizes.clear();
73
4932
        builder.old_elements.clear();
74
4932

            
75
4932
        builder.index_to_block.resize(block.len_marked(), 0);
76
4932

            
77
4932
        // O(n log n) Loop through the marked elements in order (to maintain topological sorting)
78
4932
        builder.old_elements.extend(block.iter_marked(&self.elements));
79
4932
        builder.old_elements.sort_unstable();
80

            
81
        // O(n) Loop over marked elements to determine the number of the new block each element is in.
82
464086
        for (element_index, &element) in builder.old_elements.iter().enumerate() {
83
464086
            let number = partitioner(element, self);
84
464086

            
85
464086
            builder.index_to_block[element_index] = number;
86
464086
            if number + 1 > builder.block_sizes.len() {
87
161636
                builder.block_sizes.resize(number + 1, 0);
88
302456
            }
89

            
90
464086
            builder.block_sizes[number] += 1;
91
        }
92

            
93
        // Convert block sizes into block offsets.
94
4932
        let end_of_blocks = self.blocks.len();
95
4932
        let new_block_index = if block.has_unmarked() {
96
1454
            self.blocks.len()
97
        } else {
98
3478
            self.blocks.len() - 1
99
        };
100

            
101
161636
        let _ = builder.block_sizes.iter_mut().fold(0usize, |current, size| {
102
161636
            debug_assert!(*size > 0, "Partition is not dense, there are empty blocks");
103

            
104
161636
            let current = if current == 0 {
105
4932
                if block.has_unmarked() {
106
                    // Adapt the offsets of the current block to only include the unmarked elements.
107
1454
                    self.blocks[block_index] = Block::new_unmarked(block.begin, block.marked_split);
108
1454

            
109
1454
                    // Introduce a new block for the zero block.
110
1454
                    self.blocks
111
1454
                        .push(Block::new_unmarked(block.marked_split, block.marked_split + *size));
112
1454
                    block.marked_split
113
                } else {
114
                    // Use this as the zero block.
115
3478
                self.blocks[block_index] = Block::new_unmarked(block.begin, block.begin + *size);
116
3478
                block.begin
117
                }
118
            } else {
119
                // Introduce a new block for every other non-empty block.
120
156704
                self.blocks.push(Block::new_unmarked(current, current + *size));
121
156704
                current
122
            };
123

            
124
161636
            let offset = current + *size;
125
161636
            *size = current;
126
161636
            offset
127
161636
        });
128
4932
        let block_offsets = &mut builder.block_sizes;
129

            
130
464086
        for (index, offset_block_index) in builder.index_to_block.iter().enumerate() {
131
            // Swap the element to the correct position.
132
464086
            let element = builder.old_elements[index];
133
464086
            self.elements[block_offsets[*offset_block_index]] = builder.old_elements[index];
134
464086
            self.element_offset[element] = block_offsets[*offset_block_index];
135
464086
            self.element_to_block[element] = if *offset_block_index == 0 && !block.has_unmarked() {
136
141795
                block_index
137
            } else {
138
322291
                new_block_index + *offset_block_index
139
            };
140

            
141
            // Update the offset for this block.
142
464086
            block_offsets[*offset_block_index] += 1;
143
        }
144

            
145
        // Swap the first block and the maximum sized block.
146
4932
        let max_block_index =  (block_index..=block_index).chain(end_of_blocks..self.blocks.len())
147
163090
            .max_by_key(|block_index| self.block(*block_index).len())
148
4932
            .unwrap();
149
4932
        self.swap_blocks(block_index, max_block_index);
150
4932

            
151
4932
        self.assert_consistent();
152
4932

            
153
4932
        (block_index..=block_index).chain(end_of_blocks..self.blocks.len())
154
156704
    }
155

            
156
    /// Split the given block into two separate block based on the splitter
157
    /// predicate.
158
3
    pub fn split_marked(&mut self, block_index: usize, mut splitter: impl FnMut(usize) -> bool) {
159
3
        let mut updated_block = self.blocks[block_index];
160
3
        let mut new_block: Option<Block> = None;
161
3

            
162
3
        // Loop over all elements, we use a while loop since the index stays the
163
3
        // same when a swap takes place.
164
3
        let mut element_index = updated_block.marked_split;
165
23
        while element_index < updated_block.end {
166
20
            let element = self.elements[element_index];
167
20
            if splitter(element) {
168
10
                match &mut new_block {
169
3
                    None => {
170
3
                        new_block = Some(Block::new_unmarked(updated_block.end - 1, updated_block.end));
171
3

            
172
3
                        // Swap the current element to the last place
173
3
                        self.swap_elements(element_index, updated_block.end - 1);
174
3
                        updated_block.end -= 1;
175
3
                    }
176
7
                    Some(new_block_index) => {
177
7
                        // Swap the current element to the beginning of the new block.
178
7
                        new_block_index.begin -= 1;
179
7
                        updated_block.end -= 1;
180
7

            
181
7
                        self.swap_elements(element_index, new_block_index.begin);
182
7
                    }
183
                }
184
10
            } else {
185
10
                // If no swap takes place consider the next index.
186
10
                element_index += 1;
187
10
            }
188
        }
189

            
190
3
        if let Some(new_block) = new_block {
191
3
            if (updated_block.end - updated_block.begin) != 0 {
192
                // A new block was introduced, so we need to update the current
193
                // block. Unless the current block is empty in which case
194
                // nothing changes.
195
2
                updated_block.unmark_all();
196
2
                self.blocks[block_index] = updated_block;
197
2

            
198
2
                // Introduce a new block for the split, containing only the new element.
199
2
                self.blocks.push(new_block);
200

            
201
                // Update the elements for the new block
202
7
                for element in new_block.iter(&self.elements) {
203
7
                    self.element_to_block[element] = self.blocks.len() - 1;
204
7
                }
205
1
            }
206
        }
207

            
208
3
        println!("{self:?}");
209
3
        self.assert_consistent();
210
3
    }
211

            
212
    /// Makes the marked elements closed under the silent closure of incoming
213
    /// tau-transitions within the current block.
214
76892
    pub fn mark_backward_closure(
215
76892
        &mut self,
216
76892
        block_index: usize,
217
76892
        incoming_transitions: &IncomingTransitions,
218
76892
    ) {
219
76892
        let block = self.blocks[block_index];
220
76892
        let mut it = block.end - 1;
221

            
222
        // First compute backwards silent transitive closure.
223
372640
        while it >= self.blocks[block_index].marked_split {
224
295809
            for (_label, s) in incoming_transitions.incoming_silent_transitions(self.elements[it]) {
225
186370
                if self.block_number(*s) == block_index {
226
181162
                    self.mark_element(*s);
227
181162
                }
228
            }
229

            
230
295809
            if it == 0 {
231
61
                break;
232
295748
            }
233
295748

            
234
295748
            it -= 1;
235
        }
236
76892
    }
237

            
238
    /// Swaps the given blocks given by the indices.
239
4932
    pub fn swap_blocks(&mut self, left_index: usize, right_index: usize) {
240
4932
        if left_index == right_index {
241
            // Nothing to do.
242
3733
            return;
243
1199
        }
244
1199

            
245
1199
        self.blocks.swap(left_index, right_index);
246

            
247
38805
        for element in self.block(left_index).iter(&self.elements) {
248
38805
            self.element_to_block[element] = left_index;
249
38805
        }
250

            
251
15036
        for element in self.block(right_index).iter(&self.elements) {
252
15036
            self.element_to_block[element] = right_index;
253
15036
        }
254

            
255
1199
        self.assert_consistent();
256
4932
    }
257

            
258
    /// Marks the given element, such that it is returned by iter_marked.
259
646268
    pub fn mark_element(&mut self, element: usize) {
260
646268
        let block_index = self.element_to_block[element];
261
646268
        let offset = self.element_offset[element];
262
646268
        let marked_split = self.blocks[block_index].marked_split;
263
646268

            
264
646268
        if offset < marked_split {
265
333360
            // Element was not already marked.
266
333360
            self.swap_elements(offset, marked_split - 1);
267
333360
            self.blocks[block_index].marked_split -= 1;
268
333360
        }
269

            
270
646268
        self.blocks[block_index].assert_consistent();
271
646268
    }
272

            
273
    /// Returns true iff the given element has already been marked.
274
182545
    pub fn is_element_marked(&self, element: usize) -> bool {
275
182545
        let block_index = self.element_to_block[element];
276
182545
        let offset = self.element_offset[element];
277
182545
        let marked_split = self.blocks[block_index].marked_split;
278
182545

            
279
182545
        offset >= marked_split
280
182545
    }
281

            
282
    /// Return a reference to the given block.
283
787284
    pub fn block(&self, block_index: usize) -> &Block {
284
787284
        &self.blocks[block_index]
285
787284
    }
286

            
287
    /// Returns the number of blocks in the partition.
288
313433
    pub fn num_of_blocks(&self) -> usize {
289
313433
        self.blocks.len()
290
313433
    }
291

            
292
    /// Returns an iterator over the elements of a given block.
293
158158
    pub fn iter_block(&self, block_index: usize) -> BlockIter<'_> {
294
158158
        BlockIter {
295
158158
            elements: &self.elements,
296
158158
            index: self.blocks[block_index].begin,
297
158158
            end: self.blocks[block_index].end,
298
158158
        }
299
158158
    }
300

            
301
    /// Swaps the elements at the given indices and updates the element_to_block
302
333370
    fn swap_elements(&mut self, left_index: usize, right_index: usize) {
303
333370
        self.elements.swap(left_index, right_index);
304
333370
        self.element_offset[self.elements[left_index]] = left_index;
305
333370
        self.element_offset[self.elements[right_index]] = right_index;
306
333370
    }
307

            
308
    /// Returns true iff the invariants of a partition hold
309
6134
    fn assert_consistent(&self) -> bool {
310
6134
        if cfg!(debug_assertions) {
311
6134
            let mut marked = vec![false; self.elements.len()];
312

            
313
1915958
            for block in &self.blocks {
314
33446057
                for element in block.iter(&self.elements) {
315
33446057
                    debug_assert!(
316
33446057
                        !marked[element],
317
                        "Partition {self}, element {element} belongs to multiple blocks"
318
                    );
319
33446057
                    marked[element] = true;
320
                }
321

            
322
1909824
                block.assert_consistent();
323
            }
324

            
325
            // Check that every element belongs to a block.
326
6134
            debug_assert!(
327
6134
                !marked.contains(&false),
328
                "Partition {self} contains elements that do not belong to a block"
329
            );
330

            
331
            // Check that it belongs to the block indicated by element_to_block
332
33446057
            for (current_element, block_index) in self.element_to_block.iter().enumerate() {
333
33446057
                debug_assert!(self.blocks[*block_index]
334
33446057
                    .iter(&self.elements)
335
3386110435
                    .any(|element| element == current_element),
336
                    "Partition {self:?}, element {current_element} does not belong to block {block_index} as indicated by element_to_block");
337

            
338
33446057
                let index = self.element_offset[current_element];
339
33446057
                debug_assert_eq!(
340
33446057
                    self.elements[index], current_element,
341
                    "Partition {self:?}, element {current_element} does not have the correct offset in the block"
342
                );
343
            }
344
        }
345

            
346
6134
        true
347
6134
    }
348
}
349

            
350
#[derive(Default)]
351
pub struct BlockPartitionBuilder {
352
    // Keeps track of the block index for every element in this block by index.
353
    index_to_block: Vec<usize>,
354

            
355
    /// Keeps track of the size of each block.
356
    block_sizes: Vec<usize>,
357

            
358
    /// Stores the old elements to perform the swaps safely.
359
    old_elements: Vec<usize>,
360
}
361

            
362
impl From<BlockPartition> for IndexedPartition {
363
29
    fn from(partition: BlockPartition) -> Self {
364
29
        let num_of_blocks = partition.num_of_blocks();
365
29
        IndexedPartition::with_partition(partition.element_to_block, num_of_blocks)
366
29
    }
367
}
368

            
369
impl Partition for BlockPartition {
370
3956331502
    fn block_number(&self, element: usize) -> usize {
371
3956331502
        self.element_to_block[element]
372
3956331502
    }
373

            
374
57
    fn num_of_blocks(&self) -> usize {
375
57
        self.blocks.len()
376
57
    }
377

            
378
316422
    fn len(&self) -> usize {
379
316422
        self.elements.len()
380
316422
    }
381
}
382

            
383
impl PartialEq<IndexedPartition> for BlockPartition {
384
57
    fn eq(&self, other: &IndexedPartition) -> bool {
385
57
        self.equal(other)
386
57
    }
387
}
388

            
389
impl fmt::Display for BlockPartition {
390
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
391
        write!(f, "{{")?;
392

            
393
        let mut first_block = true;
394
        for block in &self.blocks {
395
            if !first_block {
396
                write!(f, ", ")?;
397
            }
398
            write!(f, "{{")?;
399

            
400
            let mut first = true;
401
            for element in block.iter_unmarked(&self.elements) {
402
                if !first {
403
                    write!(f, ", ")?;
404
                }
405
                write!(f, "{}", element)?;
406
                first = false;
407
            }
408

            
409
            for element in block.iter_marked(&self.elements) {
410
                if !first {
411
                    write!(f, ", ")?;
412
                }
413
                write!(f, "{}*", element)?;
414
                first = false;
415
            }
416

            
417
            write!(f, "}}")?;
418
            first_block = false;
419
        }
420

            
421
        write!(f, "}}")
422
    }
423
}
424

            
425
/// A block stores a subset of the elements in a partition. It uses start,
426
/// middle and end to indicate a range start..end of elements in the partition.
427
/// The middle is used such that marked_split..end are the marked elements. This
428
/// is useful to be able to split off new blocks cheaply.
429
///
430
/// Invariant: start <= middle <= end && start < end.
431
#[derive(Clone, Copy, Debug)]
432
pub struct Block {
433
    begin: usize,
434
    marked_split: usize,
435
    end: usize,
436
}
437

            
438
impl Block {
439
    /// Creates a new block where every element is marked.
440
59
    pub fn new(begin: usize, end: usize) -> Block {
441
59
        debug_assert!(begin < end, "The range of this block is incorrect");
442

            
443
59
        Block {
444
59
            begin,
445
59
            marked_split: begin,
446
59
            end,
447
59
        }
448
59
    }
449

            
450
163093
    pub fn new_unmarked(begin: usize, end: usize) -> Block {
451
163093
        debug_assert!(begin < end, "The range {begin} to {end} of this block is incorrect");
452

            
453
163093
        Block {
454
163093
            begin,
455
163093
            marked_split: end,
456
163093
            end,
457
163093
        }
458
163093
    }
459

            
460
    /// Returns an iterator over the elements in this block.
461
35358281
    pub fn iter<'a>(&self, elements: &'a Vec<usize>) -> BlockIter<'a> {
462
35358281
        BlockIter {
463
35358281
            elements,
464
35358281
            index: self.begin,
465
35358281
            end: self.end,
466
35358281
        }
467
35358281
    }
468

            
469
    /// Returns an iterator over the marked elements in this block.
470
4932
    pub fn iter_marked<'a>(&self, elements: &'a Vec<usize>) -> BlockIter<'a> {
471
4932
        BlockIter {
472
4932
            elements,
473
4932
            index: self.marked_split,
474
4932
            end: self.end,
475
4932
        }
476
4932
    }
477

            
478
    pub fn iter_unmarked<'a>(&self, elements: &'a Vec<usize>) -> BlockIter<'a> {
479
        BlockIter {
480
            elements,
481
            index: self.begin,
482
            end: self.marked_split,
483
        }
484
    }
485

            
486
    /// Returns true iff the block has marked elements.
487
778500
    pub fn has_marked(&self) -> bool {
488
778500
        self.assert_consistent();
489
778500

            
490
778500
        self.marked_split < self.end
491
778500
    }
492

            
493
    /// Returns true iff the block has unmarked elements.
494
176991
    pub fn has_unmarked(&self) -> bool {
495
176991
        self.assert_consistent();
496
176991

            
497
176991
        self.begin < self.marked_split
498
176991
    }
499

            
500
    /// Returns the number of elements in the block.
501
319794
    pub fn len(&self) -> usize {
502
319794
        self.assert_consistent();
503
319794

            
504
319794
        self.end - self.begin
505
319794
    }
506

            
507
    /// Returns true iff the block is empty.
508
    pub fn is_empty(&self) -> bool {
509
        self.assert_consistent();
510

            
511
        self.begin == self.end
512
    }
513

            
514
    /// Returns the number of marked elements in the block.
515
4932
    pub fn len_marked(&self) -> usize {
516
4932
        self.assert_consistent();
517
4932

            
518
4932
        self.end - self.marked_split
519
4932
    }
520

            
521
    /// Unmark all elements in the block.
522
151774
    fn unmark_all(&mut self) {
523
151774
        self.marked_split = self.end;
524
151774
    }
525

            
526
    /// Returns true iff the block is consistent.
527
3836309
    fn assert_consistent(self) {
528
3836309
        debug_assert!(self.begin < self.end, "The range of block {self:?} is incorrect",);
529

            
530
3836309
        debug_assert!(
531
3836309
            self.begin <= self.marked_split,
532
            "The marked_split lies before the beginning of the block {self:?}"
533
        );
534

            
535
3836309
        debug_assert!(
536
3836309
            self.marked_split <= self.end,
537
            "The marked_split lies after the beginning of the block {self:?}"
538
        );
539
3836309
    }
540
}
541

            
542
pub struct BlockIter<'a> {
543
    elements: &'a Vec<usize>,
544
    index: usize,
545
    end: usize,
546
}
547

            
548
impl Iterator for BlockIter<'_> {
549
    type Item = usize;
550

            
551
3422448272
    fn next(&mut self) -> Option<Self::Item> {
552
3422448272
        if self.index < self.end {
553
3420372958
            let element = self.elements[self.index];
554
3420372958
            self.index += 1;
555
3420372958
            Some(element)
556
        } else {
557
2075314
            None
558
        }
559
3422448272
    }
560
}
561

            
562
#[cfg(test)]
563
mod tests {
564
    use super::*;
565

            
566
    use test_log::test;
567

            
568
1
    #[test]
569
    fn test_block_partition_split() {
570
        let mut partition = BlockPartition::new(10);
571

            
572
10
        partition.split_marked(0, |element| element < 3);
573

            
574
        // The new block only has elements that satisfy the predicate.
575
        for element in partition.iter_block(1) {
576
            assert!(element < 3);
577
        }
578

            
579
        for element in partition.iter_block(0) {
580
            assert!(element >= 3);
581
        }
582

            
583
        for i in 0..10 {
584
            partition.mark_element(i);
585
        }
586

            
587
7
        partition.split_marked(0, |element| element < 7);
588
        for element in partition.iter_block(2) {
589
            assert!(element >= 3 && element < 7);
590
        }
591

            
592
        for element in partition.iter_block(0) {
593
            assert!(element >= 7);
594
        }
595

            
596
        // Test the case where all elements belong to the split block.
597
3
        partition.split_marked(1, |element| element < 7);
598
    }
599

            
600
1
    #[test]
601
    fn test_block_partition_partitioning() {
602
        // Test the partitioning function for a random assignment of elements
603
        let mut partition = BlockPartition::new(10);
604
        let mut builder = BlockPartitionBuilder::default();
605

            
606
10
        let _ = partition.partition_marked_with(0, &mut builder, |element, _| match element {
607
10
            0..=1 => 0,
608
8
            2..=6 => 1,
609
3
            _ => 2,
610
10
        });
611

            
612
        partition.mark_element(7);
613
        partition.mark_element(8);
614
2
        let _ = partition.partition_marked_with(2, &mut builder, |element, _| match element {
615
1
            7 => 0,
616
1
            8 => 1,
617
            _ => 2,
618
2
        });
619
    }
620
}