Mercurial > hg > Gears > GearsAgda

comparison src/llrb/verifier/verify_put_cs.c @ 99:ca55f4be5f0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Create verifier directory
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 02 Feb 2016 16:02:55 +0900
parents
children 3d7ecced7e14
comparison
equal deleted inserted replaced
98:d400948dbbab 99:ca55f4be5f0f
1 /* Verification of LLRB-Tree height in put operations.
2 * LLRB-Tree allows (max-height) <= 2*(min-height).
3 */
4
5 #include <stdlib.h>
6 #include <stdio.h>
7 #include <time.h>
8 #include "../llrbContext.h"
9
10 void verify_tree_height(struct Node*);
11
12 __code meta(struct Context* context, enum Code next) {
13 if (next == Put) {
14 verify_tree_height(context->data[Tree]->tree.root);
15 }
16 goto (context->code[next])(context);
17 }
18
19 __code start_code(struct Context* context, enum Code next) {
20 unsigned int seed = (unsigned int)time(NULL);
21
22 printf("--- srand(%u)\n", seed);
23 goto meta(context, next);
24 }
25
26 __code exit_code(struct Context* context) {
27 free(context->code);
28 free(context->data);
29 free(context->heapStart);
30 goto exit(0);
31 }
32
33 unsigned int min_height(struct Node* node, unsigned int height) {
34 if ((node->left == NULL) && (node->right == NULL)) return height;
35 if (node->left == NULL) return min_height(node->right, height+1);
36 if (node->right == NULL) return min_height(node->left, height+1);
37
38 unsigned int left_min = min_height(node->left, height+1);
39 unsigned int right_min = min_height(node->right, height+1);
40
41 if (left_min < right_min) {
42 return left_min;
43 } else {
44 return right_min;
45 }
46 }
47
48 unsigned int max_height(struct Node* node, unsigned int height) {
49 if ((node->left == NULL) && (node->right == NULL)) return height;
50 if (node->left == NULL) return max_height(node->right, height+1);
51 if (node->right == NULL) return max_height(node->left, height+1);
52
53 unsigned int left_max = max_height(node->left, height+1);
54 unsigned int right_max = max_height(node->right, height+1);
55
56 if (left_max > right_max) {
57 return left_max;
58 } else {
59 return right_max;
60 }
61 }
62
63 void verify_tree_height(struct Node* root) {
64 if (root == NULL) return;
65
66 unsigned int min_h = min_height(root, 1);
67 unsigned int max_h = max_height(root, 1);
68
69 if (max_h >= 2*min_h) {
70 printf("llrb-condition violated.\n");
71 printf("\tmin-height %u", min_h);
72 printf("\tmax-height %u", max_h);
73 exit(EXIT_FAILURE);
74 }
75 }