1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 permutation.h
7
8 Abstract:
9
10 Simple abstraction for managing permutations.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-06-10.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21 #include<iostream>
22 #include "util/vector.h"
23
24 class permutation {
25 unsigned_vector m_p;
26 unsigned_vector m_inv_p;
27 public:
28 permutation(unsigned size = 0);
29 void reset(unsigned size = 0);
30
operator()31 unsigned operator()(unsigned i) const { return m_p[i]; }
inv(unsigned i_prime)32 unsigned inv(unsigned i_prime) const { return m_inv_p[i_prime]; }
33
34 void swap(unsigned i, unsigned j);
35 void move_after(unsigned i, unsigned j);
36
37 void display(std::ostream & out) const;
38 bool check_invariant() const;
39 };
40
41 inline std::ostream & operator<<(std::ostream & out, permutation const & p) {
42 p.display(out);
43 return out;
44 }
45
46 /**
47 \brief Apply permutation p to data.
48 The algorithm does not use any extra memory.
49
50 Requirement: swap(T, T) must be available.
51
52 This version will perform destructive updates to p.
53 Use apply_permutation if p must not be preserved
54 */
55 template<typename T>
apply_permutation_core(unsigned sz,T * data,unsigned * p)56 void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
57 int * p1 = reinterpret_cast<int*>(p);
58 for (int i = 0; i < static_cast<int>(sz); i++) {
59 if (p1[i] < 0)
60 continue; // already processed
61 int j = i;
62 while (true) {
63 SASSERT(j >= 0);
64 int p_j = p1[j];
65 SASSERT(p_j >= 0);
66 SASSERT(p_j < static_cast<int>(sz));
67 p1[j] = - p1[j] - 1; // mark as done
68 if (p_j == i)
69 break; // cycle starting at i is done
70 swap(data[j], data[p_j]);
71 j = p_j;
72 }
73 }
74 }
75
76 /**
77 \brief Apply permutation p to data.
78 The algorithm does not use any extra memory.
79
80 Requirement: swap(T, T) must be available.
81 */
82 template<typename T>
apply_permutation(unsigned sz,T * data,unsigned const * p)83 void apply_permutation(unsigned sz, T * data, unsigned const * p) {
84 apply_permutation_core(sz, data, const_cast<unsigned*>(p));
85 // restore p
86 int * p1 = reinterpret_cast<int*>(const_cast<unsigned*>(p));
87 for (unsigned i = 0; i < sz; i++) {
88 p1[i] = - p1[i] - 1;
89 }
90 }
91
92