ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sort.h
Go to the documentation of this file.
1#ifndef _sort_h_INCLUDED
2#define _sort_h_INCLUDED
3
4#include "utilities.h"
5
6#include "global.h"
8
9#define GREATER_SWAP(TYPE, P, Q, LESS) \
10 do { \
11 if (LESS (Q, P)) \
12 SWAP (TYPE, P, Q); \
13 } while (0)
14
15#define SORTER (solver->sorter)
16
17#define PARTITION(TYPE, L, R, A, LESS) \
18 do { \
19 const size_t L_PARTITION = (L); \
20 I_QUICK_SORT = L_PARTITION - 1; \
21\
22 size_t J_PARTITION = (R); \
23\
24 TYPE PIVOT_PARTITION = A[J_PARTITION]; \
25\
26 for (;;) { \
27 while (LESS (A[++I_QUICK_SORT], PIVOT_PARTITION)) \
28 ; \
29 while (LESS (PIVOT_PARTITION, A[--J_PARTITION])) \
30 if (J_PARTITION == L_PARTITION) \
31 break; \
32\
33 if (I_QUICK_SORT >= J_PARTITION) \
34 break; \
35\
36 SWAP (TYPE, A[I_QUICK_SORT], A[J_PARTITION]); \
37 } \
38\
39 SWAP (TYPE, A[I_QUICK_SORT], A[R]); \
40 } while (0)
41
42#define QUICK_SORT_LIMIT 10
43
44#define QUICK_SORT(TYPE, N, A, LESS) \
45 do { \
46 KISSAT_assert (N); \
47 KISSAT_assert (EMPTY_STACK (SORTER)); \
48\
49 size_t L_QUICK_SORT = 0; \
50 size_t R_QUICK_SORT = N - 1; \
51\
52 if (R_QUICK_SORT - L_QUICK_SORT <= QUICK_SORT_LIMIT) \
53 break; \
54\
55 for (;;) { \
56 const size_t M = L_QUICK_SORT + (R_QUICK_SORT - L_QUICK_SORT) / 2; \
57\
58 SWAP (TYPE, A[M], A[R_QUICK_SORT - 1]); \
59\
60 GREATER_SWAP (TYPE, A[L_QUICK_SORT], A[R_QUICK_SORT - 1], LESS); \
61 GREATER_SWAP (TYPE, A[L_QUICK_SORT], A[R_QUICK_SORT], LESS); \
62 GREATER_SWAP (TYPE, A[R_QUICK_SORT - 1], A[R_QUICK_SORT], LESS); \
63\
64 size_t I_QUICK_SORT; \
65\
66 PARTITION (TYPE, L_QUICK_SORT + 1, R_QUICK_SORT - 1, A, LESS); \
67 KISSAT_assert (L_QUICK_SORT < I_QUICK_SORT); \
68 KISSAT_assert (I_QUICK_SORT <= R_QUICK_SORT); \
69\
70 size_t LL_QUICK_SORT; \
71 size_t RR_QUICK_SORT; \
72\
73 if (I_QUICK_SORT - L_QUICK_SORT < R_QUICK_SORT - I_QUICK_SORT) { \
74 LL_QUICK_SORT = I_QUICK_SORT + 1; \
75 RR_QUICK_SORT = R_QUICK_SORT; \
76 R_QUICK_SORT = I_QUICK_SORT - 1; \
77 } else { \
78 LL_QUICK_SORT = L_QUICK_SORT; \
79 RR_QUICK_SORT = I_QUICK_SORT - 1; \
80 L_QUICK_SORT = I_QUICK_SORT + 1; \
81 } \
82 if (R_QUICK_SORT - L_QUICK_SORT > QUICK_SORT_LIMIT) { \
83 KISSAT_assert (RR_QUICK_SORT - LL_QUICK_SORT > QUICK_SORT_LIMIT); \
84 PUSH_STACK (SORTER, LL_QUICK_SORT); \
85 PUSH_STACK (SORTER, RR_QUICK_SORT); \
86 } else if (RR_QUICK_SORT - LL_QUICK_SORT > QUICK_SORT_LIMIT) { \
87 L_QUICK_SORT = LL_QUICK_SORT; \
88 R_QUICK_SORT = RR_QUICK_SORT; \
89 } else if (!EMPTY_STACK (SORTER)) { \
90 R_QUICK_SORT = POP_STACK (SORTER); \
91 L_QUICK_SORT = POP_STACK (SORTER); \
92 } else \
93 break; \
94 } \
95 } while (0)
96
97#define INSERTION_SORT(TYPE, N, A, LESS) \
98 do { \
99 size_t L_INSERTION_SORT = 0; \
100 size_t R_INSERTION_SORT = N - 1; \
101\
102 for (size_t I_INSERTION_SORT = R_INSERTION_SORT; \
103 I_INSERTION_SORT > L_INSERTION_SORT; I_INSERTION_SORT--) \
104 GREATER_SWAP (TYPE, A[I_INSERTION_SORT - 1], A[I_INSERTION_SORT], \
105 LESS); \
106\
107 for (size_t I_INSERTION_SORT = L_INSERTION_SORT + 2; \
108 I_INSERTION_SORT <= R_INSERTION_SORT; I_INSERTION_SORT++) { \
109 TYPE PIVOT_INSERTION_SORT = A[I_INSERTION_SORT]; \
110\
111 size_t J_INSERTION_SORT = I_INSERTION_SORT; \
112\
113 while (LESS (PIVOT_INSERTION_SORT, A[J_INSERTION_SORT - 1])) { \
114 A[J_INSERTION_SORT] = A[J_INSERTION_SORT - 1]; \
115 J_INSERTION_SORT--; \
116 } \
117\
118 A[J_INSERTION_SORT] = PIVOT_INSERTION_SORT; \
119 } \
120 } while (0)
121
122#ifdef KISSAT_NDEBUG
123#define CHECK_SORTED(...) \
124 do { \
125 } while (0)
126#else
127#define CHECK_SORTED(N, A, LESS) \
128 do { \
129 for (size_t I_CHECK_SORTED = 0; I_CHECK_SORTED < N - 1; \
130 I_CHECK_SORTED++) \
131 KISSAT_assert (!LESS (A[I_CHECK_SORTED + 1], A[I_CHECK_SORTED])); \
132 } while (0)
133#endif
134
135#define SORT(TYPE, N, A, LESS) \
136 do { \
137 const size_t N_SORT = (N); \
138 if (!N_SORT) \
139 break; \
140 START (sort); \
141 TYPE *A_SORT = (A); \
142 QUICK_SORT (TYPE, N_SORT, A_SORT, LESS); \
143 INSERTION_SORT (TYPE, N_SORT, A_SORT, LESS); \
144 CHECK_SORTED (N_SORT, A_SORT, LESS); \
145 STOP (sort); \
146 } while (0)
147
148#define SORT_STACK(TYPE, S, LESS) \
149 do { \
150 const size_t N_SORT_STACK = SIZE_STACK (S); \
151 if (N_SORT_STACK <= 1) \
152 break; \
153 TYPE *A_SORT_STACK = BEGIN_STACK (S); \
154 SORT (TYPE, N_SORT_STACK, A_SORT_STACK, LESS); \
155 } while (0)
156
158
159#endif
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.