Mercurial > hg > Gears > GearsAgda
view src/llrb/verifier/verify_put_cs.c @ 99:ca55f4be5f0f
Create verifier directory
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 02 Feb 2016 16:02:55 +0900 |
parents | |
children | 3d7ecced7e14 |
line wrap: on
line source
/* Verification of LLRB-Tree height in put operations. * LLRB-Tree allows (max-height) <= 2*(min-height). */ #include <stdlib.h> #include <stdio.h> #include <time.h> #include "../llrbContext.h" void verify_tree_height(struct Node*); __code meta(struct Context* context, enum Code next) { if (next == Put) { verify_tree_height(context->data[Tree]->tree.root); } goto (context->code[next])(context); } __code start_code(struct Context* context, enum Code next) { unsigned int seed = (unsigned int)time(NULL); printf("--- srand(%u)\n", seed); goto meta(context, next); } __code exit_code(struct Context* context) { free(context->code); free(context->data); free(context->heapStart); goto exit(0); } unsigned int min_height(struct Node* node, unsigned int height) { if ((node->left == NULL) && (node->right == NULL)) return height; if (node->left == NULL) return min_height(node->right, height+1); if (node->right == NULL) return min_height(node->left, height+1); unsigned int left_min = min_height(node->left, height+1); unsigned int right_min = min_height(node->right, height+1); if (left_min < right_min) { return left_min; } else { return right_min; } } unsigned int max_height(struct Node* node, unsigned int height) { if ((node->left == NULL) && (node->right == NULL)) return height; if (node->left == NULL) return max_height(node->right, height+1); if (node->right == NULL) return max_height(node->left, height+1); unsigned int left_max = max_height(node->left, height+1); unsigned int right_max = max_height(node->right, height+1); if (left_max > right_max) { return left_max; } else { return right_max; } } void verify_tree_height(struct Node* root) { if (root == NULL) return; unsigned int min_h = min_height(root, 1); unsigned int max_h = max_height(root, 1); if (max_h >= 2*min_h) { printf("llrb-condition violated.\n"); printf("\tmin-height %u", min_h); printf("\tmax-height %u", max_h); exit(EXIT_FAILURE); } }