ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
radix.hpp
Go to the documentation of this file.
1#ifndef _radix_hpp_INCLUDED
2#define _radix_hpp_INCLUDED
3
4#include "global.h"
5
6#include <cassert>
7#include <cstring>
8#include <iterator>
9#include <vector>
10
12
13namespace CaDiCaL {
14
15using namespace std;
16
17// This provides an implementation of a generic radix sort algorithm. The
18// reason for having it is that for certain benchmarks and certain parts of
19// CaDiCaL where sorting is used, the standard sorting algorithm 'sort'
20// turned out to be a hot-spot. Up to 30% of the total running time was for
21// instance used for some benchmarks in sorting variables during bumping
22// to make sure to bump them in 'enqueued' order.
23//
24// Further, in most cases, where we need to sort something, sorting is
25// actually performed on positive numbers (such as the 'enqueued' time stamp
26// during bumping), which allows to use radix sort or variants. At least
27// starting with medium sized arrays to be sorted (say above 1000 elements,
28// but see discussion on 'MSORT' below), radix sort can be way faster.
29//
30// Finally it is stable, which is actually preferred most of the time too.
31//
32// This template algorithm 'rsort' takes as first template parameter the
33// iterator class similar to the standard 'sort' algorithm template, but
34// then as second parameter a function class (similar to the second 'less
35// than' parameter of 'sort') which can obtain a 'rank' from each element,
36// on which they are compared. The 'rank' should be able to turn an element
37// into a number. The type of these ranks is determined automatically but
38// should be 'unsigned'.
39
41 typedef size_t Type;
42 Type operator() (void *ptr) { return (size_t) ptr; }
43};
44
45template <class I, class Rank> void rsort (I first, I last, Rank rank) {
46 typedef typename iterator_traits<I>::value_type T;
47 typedef typename Rank::Type R;
48
49 CADICAL_assert (first <= last);
50 const size_t n = last - first;
51 if (n <= 1)
52 return;
53
54 const size_t l = 8; // Radix 8, thus byte-wise.
55 const size_t w = (1 << l); // So many buckets.
56
57 const unsigned mask = w - 1; // Fast mod 'w'.
58
59// Uncomment the following define for large values of 'w' in order to keep
60// the large bucket array 'count' on the heap instead of the stack.
61//
62// #define CADICAL_RADIX_BUCKETS_ON_THE_HEAP
63//
64#ifdef CADICAL_RADIX_BUCKETS_ON_THE_HEAP
65 size_t *count = new size_t[w]; // Put buckets on the heap.
66#else
67 size_t count[w]; // Put buckets on the stack.
68#endif
69
70 I a = first, b = last, c = a;
71 bool initialized = false;
72 std::vector<T> v;
73
74 R upper = 0, lower = ~upper;
75 R shifted = mask;
76 bool bounded = false;
77
78 R masked_lower = 0, masked_upper = mask;
79
80 for (size_t i = 0; i < 8 * sizeof (rank (*first));
81 i += l, shifted <<= l) {
82
83 if (bounded && (lower & shifted) == (upper & shifted))
84 continue;
85
86 memset (count + masked_lower, 0,
87 (masked_upper - masked_lower + 1) * sizeof *count);
88
89 const I end = c + n;
90 bool sorted = true;
91 R last = 0;
92
93 for (I p = c; p != end; p++) {
94 const auto r = rank (*p);
95 if (!bounded)
96 lower &= r, upper |= r;
97 const auto s = r >> i;
98 const auto m = s & mask;
99 if (sorted && last > m)
100 sorted = false;
101 else
102 last = m;
103 count[m]++;
104 }
105
106 masked_lower = (lower >> i) & mask;
107 masked_upper = (upper >> i) & mask;
108
109 if (!bounded) {
110 bounded = true;
111 if ((lower & shifted) == (upper & shifted))
112 continue;
113 }
114
115 if (sorted)
116 continue;
117
118 size_t pos = 0;
119 for (R j = masked_lower; j <= masked_upper; j++) {
120 const size_t delta = count[j];
121 count[j] = pos;
122 pos += delta;
123 }
124
125 if (!initialized) {
126 CADICAL_assert (&*c == &*a); // MS VC++
127 v.resize (n);
128 b = v.begin ();
129 initialized = true;
130 }
131
132 I d = (&*c == &*a) ? b : a; // MS VC++
133
134 for (I p = c; p != end; p++) {
135 const auto r = rank (*p);
136 const auto s = r >> i;
137 const auto m = s & mask;
138 d[count[m]++] = *p;
139 }
140 c = d;
141 }
142
143 if (c == b) {
144 for (size_t i = 0; i < n; i++)
145 a[i] = b[i];
146 }
147
148#ifdef CADICAL_RADIX_BUCKETS_ON_THE_HEAP
149 delete[] count;
150#endif
151
152#ifndef CADICAL_NDEBUG
153 for (I p = first; p + 1 != last; p++)
154 CADICAL_assert (rank (p[0]) <= rank (p[1]));
155#endif
156}
157
158// It turns out that for small number of elements (like '100') and in
159// particular for large value ranges the standard sorting function is
160// considerably faster than our radix sort (like 2.5x). This negative effect
161// vanishes at around 800 elements (sorting integers) and thus we provide a
162// function 'MSORT' which selects between standard sort and radix sort based
163// on the number of elements. However we failed to put this into proper C++
164// style template code and thus have to use a macro instead. We also do not
165// use it everywhere instead of 'rsort' since it requires a fourth
166// parameter, which is awkward, particular in those situation where we
167// expect large arrays to be sorted anyhow (such as during sorting the
168// clauses in an arena or the probes during probing). The first argument
169// is the limit up to which we use the standard sort. Above the limit we
170// use radix sort. As usual we do not want to hard code it here (default
171// is '800') in order to make fuzzing and delta debugging more effective.
172
173#define MSORT(LIMIT, FIRST, LAST, RANK, LESS) \
174 do { \
175 const size_t N = LAST - FIRST; \
176 if (N <= (size_t) (LIMIT)) \
177 sort (FIRST, LAST, LESS); \
178 else \
179 rsort (FIRST, LAST, RANK); \
180 } while (0)
181
182} // namespace CaDiCaL
183
185
186#endif
#define ABC_NAMESPACE_CXX_HEADER_START
#define ABC_NAMESPACE_CXX_HEADER_END
#define CADICAL_assert(ignore)
Definition global.h:14
bool pos
Definition globals.c:30
Cube * p
Definition exorList.c:222
void rsort(I first, I last, Rank rank)
Definition radix.hpp:45
Type operator()(void *ptr)
Definition radix.hpp:42
char * memset()
unsigned rank
Definition vector.c:142