1 /*
2  * This file is part of the Yices SMT Solver.
3  * Copyright (C) 2017 SRI International.
4  *
5  * Yices is free software: you can redistribute it and/or modify
6  * it under the terms of the GNU General Public License as published by
7  * the Free Software Foundation, either version 3 of the License, or
8  * (at your option) any later version.
9  *
10  * Yices is distributed in the hope that it will be useful,
11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13  * GNU General Public License for more details.
14  *
15  * You should have received a copy of the GNU General Public License
16  * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
17  */
18 
19 /*
20  * BASIC SORT FOR INTEGER ARRAYS
21  */
22 
23 #include "utils/int_array_sort.h"
24 #include "utils/prng.h"
25 
26 static void qsort_int_array(int32_t *a, uint32_t n);
27 
28 // insertion sort
isort_int_array(int32_t * a,uint32_t n)29 static void isort_int_array(int32_t *a, uint32_t n) {
30   uint32_t i, j;
31   int32_t x, y;
32 
33   for (i=1; i<n; i++) {
34     x = a[i];
35     j = 0;
36     while (a[j] < x) j ++;
37     while (j < i) {
38       y = a[j]; a[j] = x; x = y;
39       j ++;
40     }
41     a[j] = x;
42   }
43 }
44 
sort_array(int32_t * a,uint32_t n)45 static inline void sort_array(int32_t *a, uint32_t n) {
46   if (n < 10) {
47     isort_int_array(a, n);
48   } else {
49     qsort_int_array(a, n);
50   }
51 }
52 
53 // quick sort: requires n > 1
qsort_int_array(int32_t * a,uint32_t n)54 static void qsort_int_array(int32_t *a, uint32_t n) {
55   uint32_t i, j;
56   int32_t x, y;
57   uint32_t seed = PRNG_DEFAULT_SEED;
58 
59   // x = random pivot
60   i = random_uint(&seed, n);
61   x = a[i];
62 
63   // swap x and a[0]
64   a[i] = a[0];
65   a[0] = x;
66 
67   i = 0;
68   j = n;
69 
70   do { j--; } while (a[j] > x);
71   do { i++; } while (i <= j && a[i] < x);
72 
73   while (i < j) {
74     y = a[i]; a[i] = a[j]; a[j] = y;
75 
76     do { j--; } while (a[j] > x);
77     do { i++; } while (a[i] < x);
78   }
79 
80   // pivot goes into a[j]
81   a[0] = a[j];
82   a[j] = x;
83 
84   // sort a[0...j-1] and a[j+1 .. n-1]
85   sort_array(a, j);
86   j++;
87   sort_array(a + j, n - j);
88 }
89 
90 
91 /*
92  * External call
93  */
int_array_sort(int32_t * a,uint32_t n)94 void int_array_sort(int32_t *a, uint32_t n) {
95   sort_array(a, n);
96 }
97