Mercurial > hg > Gears > GearsAgda

annotate src/llrb/main.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 c13575c3dbe9
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 #include <stdio.h>
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 #include <stdlib.h>
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 #include <sys/time.h>
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 #include "llrbContext.h"
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 #include "origin_cs.h"
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 static double st_time;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 static double ed_time;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 static clock_t c1,c2;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 int num;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
72
5c4b9d116eda use stack for code segment
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
14 extern __code initLLRBContext(struct Context* context, int);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 extern void allocator(struct Context* context);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 static double getTime() {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 struct timeval tv;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 gettimeofday(&tv, NULL);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 return tv.tv_sec + (double)tv.tv_usec*1e-6;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 void print_tree(struct Node* node, int n) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 if (node != 0) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 print_tree(node->left, n+1);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 for (int i=0;i<n;i++)
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 printf(" ");
73
2667c3251a00 implement llrb deletion
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
28 printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 print_tree(node->right, n+1);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 /*
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 __code code1(Allocate allocate) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 allocate.size = sizeof(long);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 allocate.next = Code2;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 goto Allocate(allocate);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 */
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 __code code1(struct Context* context, struct Allocate *allocate) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 allocate->size = sizeof(struct Count);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 allocator(context);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 goto meta(context, Code2);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 __code code1_stub(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 goto code1(context, &context->data[Allocate]->allocate);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 /*
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 __code code2(Allocate allocate, Count count) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 count.count = 0;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 goto code3(count);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 */
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 __code code2(struct Context* context, struct Count* count) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 count->i = num;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 goto meta(context, Code3);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 __code code2_stub(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 goto code2(context, &context->data[context->dataNum]->count);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 __code code3(struct Context* context, struct Node* node, struct Count* count) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 if (count->i == 0) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 goto meta(context, Code4);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 print_tree(context->data[Tree]->tree.root, 0);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 puts("");
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 context->next = Code3;
83
c13575c3dbe9 use stack
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
75 node->key = rand()%100+1;
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 node->value = count->i;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 count->i--;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 goto meta(context, Put);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 __code code3_stub(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 goto code3(context, &context->data[Node]->node, &context->data[3]->count);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 __code code4(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 puts("---before---");
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 print_tree(context->data[Tree]->tree.root, 0);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 struct Node* node = &context->data[Node]->node;
81
dc6f665bb753 implement delete(tail call). do not work
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
91 node->key = 4;
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 context->next = Code5;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94
83
c13575c3dbe9 use stack
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
95 goto meta(context, Exit);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 __code code5(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 puts("---after---");
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 print_tree(context->data[Tree]->tree.root, 0);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 puts("--Number of Data--");
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 printf("%d\n", context->dataNum);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103
81
dc6f665bb753 implement delete(tail call). do not work
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
104 goto meta(context, Exit);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 __code find(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 context->data[Node]->node.key = 2;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 context->next = Not_find;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 goto meta(context, Get);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 __code not_find(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 context->data[Node]->node.key = 10;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 context->next = Code6;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 printf("%p\n", context->data[Tree]->tree.current);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 context->data[Tree]->tree.current = 0;
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 goto meta(context, Get);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 __code code6(struct Context* context) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 printf("%p\n", context->data[Tree]->tree.current);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
72
5c4b9d116eda use stack for code segment
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
126 stack_free(context->node_stack);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 goto meta(context, Exit);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 }
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 int main(int argc, char** argv) {
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 num = (int)atoi(argv[1]);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 struct Context* context = (struct Context*)malloc(sizeof(struct Context));
72
5c4b9d116eda use stack for code segment
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
134 initLLRBContext(context, num);
69
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 goto start_code(context, Code1);
368306e1bfed llrb deletion(not work).
Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 }