25#define RADIX_SORT(VTYPE, RTYPE, N, V, RANK) \
26 do { \
27 const size_t N_RADIX = (N); \
28 if (N_RADIX <= 1) \
29 break; \
30\
31 START (radix); \
32\
33 VTYPE *V_RADIX = (V); \
34\
35 const size_t LENGTH_RADIX = 8; \
36 const size_t WIDTH_RADIX = (1 << LENGTH_RADIX); \
37 const RTYPE MASK_RADIX = WIDTH_RADIX - 1; \
38\
39 size_t COUNT_RADIX[256]; \
40\
41 VTYPE *TMP_RADIX = 0; \
42 const size_t BYTES_TMP_RADIX = N_RADIX * sizeof (VTYPE); \
43\
44 VTYPE *A_RADIX = V_RADIX; \
45 VTYPE *B_RADIX = 0; \
46 VTYPE *C_RADIX = A_RADIX; \
47\
48 RTYPE MLOWER_RADIX = 0; \
49 RTYPE MUPPER_RADIX = MASK_RADIX; \
50\
51 bool BOUNDED_RADIX = false; \
52 RTYPE UPPER_RADIX = 0; \
53 RTYPE LOWER_RADIX = ~UPPER_RADIX; \
54 RTYPE SHIFT_RADIX = MASK_RADIX; \
55\
56 for (size_t I_RADIX = 0; I_RADIX < 8 * sizeof (RTYPE); \
57 I_RADIX += LENGTH_RADIX, SHIFT_RADIX <<= LENGTH_RADIX) { \
58 if (BOUNDED_RADIX && \
59 (LOWER_RADIX & SHIFT_RADIX) == (UPPER_RADIX & SHIFT_RADIX)) \
60 continue; \
61\
62 memset (COUNT_RADIX + MLOWER_RADIX, 0, \
63 (MUPPER_RADIX - MLOWER_RADIX + 1) * sizeof *COUNT_RADIX); \
64\
65 VTYPE *END_RADIX = C_RADIX + N_RADIX; \
66\
67 bool SORTED_RADIX = true; \
68 RTYPE LAST_RADIX = 0; \
69\
70 for (VTYPE *P_RADIX = C_RADIX; P_RADIX != END_RADIX; P_RADIX++) { \
71 RTYPE R_RADIX = RANK (*P_RADIX); \
72 if (!BOUNDED_RADIX) { \
73 LOWER_RADIX &= R_RADIX; \
74 UPPER_RADIX |= R_RADIX; \
75 } \
76 RTYPE S_RADIX = R_RADIX >> I_RADIX; \
77 RTYPE M_RADIX = S_RADIX & MASK_RADIX; \
78 if (SORTED_RADIX && LAST_RADIX > M_RADIX) \
79 SORTED_RADIX = false; \
80 else \
81 LAST_RADIX = M_RADIX; \
82 COUNT_RADIX[M_RADIX]++; \
83 } \
84\
85 MLOWER_RADIX = (LOWER_RADIX >> I_RADIX) & MASK_RADIX; \
86 MUPPER_RADIX = (UPPER_RADIX >> I_RADIX) & MASK_RADIX; \
87\
88 if (!BOUNDED_RADIX) { \
89 BOUNDED_RADIX = true; \
90 if ((LOWER_RADIX & SHIFT_RADIX) == (UPPER_RADIX & SHIFT_RADIX)) \
91 continue; \
92 } \
93\
94 if (SORTED_RADIX) \
95 continue; \
96\
97 size_t POS_RADIX = 0; \
98 for (size_t J_RADIX = MLOWER_RADIX; J_RADIX <= MUPPER_RADIX; \
99 J_RADIX++) { \
100 const size_t DELTA_RADIX = COUNT_RADIX[J_RADIX]; \
101 COUNT_RADIX[J_RADIX] = POS_RADIX; \
102 POS_RADIX += DELTA_RADIX; \
103 } \
104\
105 if (!TMP_RADIX) { \
106 KISSAT_assert (C_RADIX == A_RADIX); \
107 TMP_RADIX = (VTYPE*)kissat_malloc (solver, BYTES_TMP_RADIX); \
108 B_RADIX = TMP_RADIX; \
109 } \
110\
111 KISSAT_assert (B_RADIX == TMP_RADIX); \
112\
113 VTYPE *D_RADIX = (C_RADIX == A_RADIX) ? B_RADIX : A_RADIX; \
114\
115 for (VTYPE *P_RADIX = C_RADIX; P_RADIX != END_RADIX; P_RADIX++) { \
116 RTYPE R_RADIX = RANK (*P_RADIX); \
117 RTYPE S_RADIX = R_RADIX >> I_RADIX; \
118 RTYPE M_RADIX = S_RADIX & MASK_RADIX; \
119 const size_t POS_RADIX = COUNT_RADIX[M_RADIX]++; \
120 D_RADIX[POS_RADIX] = *P_RADIX; \
121 } \
122\
123 C_RADIX = D_RADIX; \
124 } \
125\
126 if (C_RADIX == B_RADIX) \
127 memcpy (A_RADIX, B_RADIX, N_RADIX * sizeof *A_RADIX); \
128\
129 if (TMP_RADIX) \
130 kissat_free (solver, TMP_RADIX, BYTES_TMP_RADIX); \
131\
132 CHECK_RANKED (N_RADIX, V_RADIX, RANK); \
133 STOP (radix); \
134 } while (0)
