1 |
|
/******************************************************************************************[Sort.h] |
2 |
|
Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson |
3 |
|
Copyright (c) 2007-2010, Niklas Sorensson |
4 |
|
|
5 |
|
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and |
6 |
|
associated documentation files (the "Software"), to deal in the Software without restriction, |
7 |
|
including without limitation the rights to use, copy, modify, merge, publish, distribute, |
8 |
|
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is |
9 |
|
furnished to do so, subject to the following conditions: |
10 |
|
|
11 |
|
The above copyright notice and this permission notice shall be included in all copies or |
12 |
|
substantial portions of the Software. |
13 |
|
|
14 |
|
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT |
15 |
|
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
16 |
|
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
17 |
|
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT |
18 |
|
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
19 |
|
**************************************************************************************************/ |
20 |
|
|
21 |
|
#ifndef Minisat_Sort_h |
22 |
|
#define Minisat_Sort_h |
23 |
|
|
24 |
|
#include "prop/minisat/mtl/Vec.h" |
25 |
|
|
26 |
|
//================================================================================================= |
27 |
|
// Some sorting algorithms for vec's |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace Minisat { |
31 |
|
|
32 |
|
template<class T> |
33 |
|
struct LessThan_default { |
34 |
26146004 |
bool operator () (T x, T y) { return x < y; } |
35 |
|
}; |
36 |
|
|
37 |
|
|
38 |
|
template <class T, class LessThan> |
39 |
7915739 |
void selectionSort(T* array, int size, LessThan lt) |
40 |
|
{ |
41 |
|
int i, j, best_i; |
42 |
|
T tmp; |
43 |
|
|
44 |
23475855 |
for (i = 0; i < size-1; i++){ |
45 |
15560116 |
best_i = i; |
46 |
56381291 |
for (j = i+1; j < size; j++){ |
47 |
40821175 |
if (lt(array[j], array[best_i])) |
48 |
8269183 |
best_i = j; |
49 |
|
} |
50 |
15560116 |
tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; |
51 |
|
} |
52 |
7915739 |
} |
53 |
|
template <class T> static inline void selectionSort(T* array, int size) { |
54 |
|
selectionSort(array, size, LessThan_default<T>()); } |
55 |
|
|
56 |
|
template <class T, class LessThan> |
57 |
8156868 |
void sort(T* array, int size, LessThan lt) |
58 |
|
{ |
59 |
8156868 |
if (size <= 15) |
60 |
7915739 |
selectionSort(array, size, lt); |
61 |
|
|
62 |
|
else{ |
63 |
241129 |
T pivot = array[size / 2]; |
64 |
|
T tmp; |
65 |
241129 |
int i = -1; |
66 |
241129 |
int j = size; |
67 |
|
|
68 |
1408945 |
for(;;){ |
69 |
5261257 |
do i++; while(lt(array[i], pivot)); |
70 |
4910174 |
do j--; while(lt(pivot, array[j])); |
71 |
|
|
72 |
1650074 |
if (i >= j) break; |
73 |
|
|
74 |
1408945 |
tmp = array[i]; array[i] = array[j]; array[j] = tmp; |
75 |
|
} |
76 |
|
|
77 |
241129 |
sort(array , i , lt); |
78 |
241129 |
sort(&array[i], size-i, lt); |
79 |
|
} |
80 |
8156868 |
} |
81 |
|
template <class T> static inline void sort(T* array, int size) { |
82 |
|
sort(array, size, LessThan_default<T>()); } |
83 |
|
|
84 |
|
|
85 |
|
//================================================================================================= |
86 |
|
// For 'vec's: |
87 |
|
|
88 |
|
|
89 |
7674610 |
template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { |
90 |
7674610 |
sort((T*)v, v.size(), lt); } |
91 |
3947488 |
template <class T> void sort(vec<T>& v) { |
92 |
3947488 |
sort(v, LessThan_default<T>()); } |
93 |
|
|
94 |
|
|
95 |
|
//================================================================================================= |
96 |
|
} |
97 |
|
} // namespace cvc5 |
98 |
|
|
99 |
|
#endif |