1 /***** spin: pangen4.h *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 * 8 * The DFA code below was written by Anuj Puri and Gerard J. Holzmann in 9 * May 1997, and was inspired by earlier work on data compression using 10 * sharing tree data structures and graph-encoded sets by J-Ch. Gregoire 11 * (INRS Telecom, Quebec, Canada) and D.Zampunieris (Univ.Namur, Belgium) 12 * The splay routine code included here is based on the public domain 13 * version written by D. Sleator <sleator@cs.cmu.edu> in 1992. 14 */ 15 16 static const char *Dfa[] = { 17 "#ifdef MA", 18 #if 0 19 "/*", 20 "#include <stdio.h>", 21 "#define uchar unsigned char", 22 "*/", 23 "#define ulong unsigned long", 24 "#define ushort unsigned short", 25 "", 26 #endif 27 "#define TWIDTH 256", 28 "#define HASH(y,n) (n)*(((long)y))", 29 "#define INRANGE(e,h) ((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))", 30 "", 31 "extern char *emalloc(unsigned long); /* imported routine */", 32 "extern void dfa_init(ushort); /* 4 exported routines */", 33 "extern int dfa_member(ulong);", 34 "extern int dfa_store(uchar *);", 35 "extern void dfa_stats(void);", 36 "", 37 "typedef struct Edge {", 38 " uchar From, To; /* max range 0..255 */", 39 " uchar s, S; /* if s=1, S is singleton */", 40 " struct Vertex *Dst;", 41 " struct Edge *Nxt;", 42 "} Edge;", 43 "", 44 "typedef struct Vertex {", 45 " ulong key, num; /* key for splay tree, nr incoming edges */", 46 " uchar from[2], to[2]; /* in-node predefined edge info */", 47 " struct Vertex *dst[2];/* most nodes have 2 or more edges */", 48 " struct Edge *Succ; /* in case there are more edges */", 49 " struct Vertex *lnk, *left, *right; /* splay tree plumbing */", 50 "} Vertex;", 51 "", 52 "static Edge *free_edges;", 53 "static Vertex *free_vertices;", 54 "static Vertex **layers; /* one splay tree of nodes per layer */", 55 "static Vertex **path; /* run of word in the DFA */", 56 "static Vertex *R, *F, *NF; /* Root, Final, Not-Final */", 57 "static uchar *word, *lastword;/* string, and last string inserted */", 58 "static int dfa_depth, iv=0, nv=0, pfrst=0, Tally;", 59 "", 60 "static void insert_it(Vertex *, int); /* splay-tree code */", 61 "static void delete_it(Vertex *, int);", 62 "static Vertex *find_it(Vertex *, Vertex *, uchar, int);", 63 "", 64 "static void", 65 "recyc_edges(Edge *e)", 66 "{", 67 " if (!e) return;", 68 " recyc_edges(e->Nxt);", 69 " e->Nxt = free_edges;", 70 " free_edges = e;", 71 "}", 72 "", 73 "static Edge *", 74 "new_edge(Vertex *dst)", 75 "{ Edge *e;", 76 "", 77 " if (free_edges)", 78 " { e = free_edges;", 79 " free_edges = e->Nxt;", 80 " e->From = e->To = e->s = e->S = 0;", 81 " e->Nxt = (Edge *) 0;", 82 " } else", 83 " e = (Edge *) emalloc(sizeof(Edge));", 84 " e->Dst = dst;", 85 "", 86 " return e;", 87 "}", 88 "", 89 "static void", 90 "recyc_vertex(Vertex *v)", 91 "{", 92 " recyc_edges(v->Succ);", 93 " v->Succ = (Edge *) free_vertices;", 94 " free_vertices = v;", 95 " nr_states--;", 96 "}", 97 "", 98 "static Vertex *", 99 "new_vertex(void)", 100 "{ Vertex *v;", 101 "", 102 " if (free_vertices)", 103 " { v = free_vertices;", 104 " free_vertices = (Vertex *) v->Succ;", 105 " v->Succ = (Edge *) 0;", 106 " v->num = 0;", 107 " } else", 108 " v = (Vertex *) emalloc(sizeof(Vertex));", 109 "", 110 " nr_states++;", 111 " return v; ", 112 "}", 113 "", 114 "static Vertex *", 115 "allDelta(Vertex *v, int n)", 116 "{ Vertex *dst = new_vertex();", 117 "", 118 " v->from[0] = 0;", 119 " v->to[0] = 255;", 120 " v->dst[0] = dst;", 121 " dst->num = 256;", 122 " insert_it(v, n);", 123 " return dst;", 124 "}", 125 "", 126 "static void", 127 "insert_edge(Vertex *v, Edge *e)", 128 "{ /* put new edge first */", 129 " if (!v->dst[0])", 130 " { v->dst[0] = e->Dst;", 131 " v->from[0] = e->From;", 132 " v->to[0] = e->To;", 133 " recyc_edges(e);", 134 " return;", 135 " }", 136 " if (!v->dst[1])", 137 " { v->from[1] = v->from[0]; v->from[0] = e->From;", 138 " v->to[1] = v->to[0]; v->to[0] = e->To;", 139 " v->dst[1] = v->dst[0]; v->dst[0] = e->Dst;", 140 " recyc_edges(e);", 141 " return;", 142 " } /* shift */", 143 " { int f = v->from[1];", 144 " int t = v->to[1];", 145 " Vertex *d = v->dst[1];", 146 " v->from[1] = v->from[0]; v->from[0] = e->From;", 147 " v->to[1] = v->to[0]; v->to[0] = e->To;", 148 " v->dst[1] = v->dst[0]; v->dst[0] = e->Dst;", 149 " e->From = f;", 150 " e->To = t;", 151 " e->Dst = d;", 152 " }", 153 " e->Nxt = v->Succ;", 154 " v->Succ = e;", 155 "}", 156 "", 157 "static void", 158 "copyRecursive(Vertex *v, Edge *e)", 159 "{ Edge *f;", 160 " if (e->Nxt) copyRecursive(v, e->Nxt);", 161 " f = new_edge(e->Dst);", 162 " f->From = e->From;", 163 " f->To = e->To;", 164 " f->s = e->s;", 165 " f->S = e->S;", 166 " f->Nxt = v->Succ;", 167 " v->Succ = f;", 168 "}", 169 "", 170 "static void", 171 "copyEdges(Vertex *to, Vertex *from)", 172 "{ int i;", 173 " for (i = 0; i < 2; i++)", 174 " { to->from[i] = from->from[i];", 175 " to->to[i] = from->to[i];", 176 " to->dst[i] = from->dst[i];", 177 " }", 178 " if (from->Succ) copyRecursive(to, from->Succ);", 179 "}", 180 "", 181 "static Edge *", 182 "cacheDelta(Vertex *v, int h, int first)", 183 "{ static Edge *ov, tmp; int i;", 184 "", 185 " if (!first && INRANGE(ov,h))", 186 " return ov; /* intercepts about 10%% */", 187 " for (i = 0; i < 2; i++)", 188 " if (v->dst[i] && h >= v->from[i] && h <= v->to[i])", 189 " { tmp.From = v->from[i];", 190 " tmp.To = v->to[i];", 191 " tmp.Dst = v->dst[i];", 192 " tmp.s = tmp.S = 0;", 193 " ov = &tmp;", 194 " return ov;", 195 " }", 196 " for (ov = v->Succ; ov; ov = ov->Nxt)", 197 " if (INRANGE(ov,h)) return ov;", 198 "", 199 " Uerror(\"cannot get here, cacheDelta\");", 200 " return (Edge *) 0;", 201 "}", 202 "", 203 "static Vertex *", 204 "Delta(Vertex *v, int h) /* v->delta[h] */", 205 "{ Edge *e;", 206 "", 207 " if (v->dst[0] && h >= v->from[0] && h <= v->to[0])", 208 " return v->dst[0]; /* oldest edge */", 209 " if (v->dst[1] && h >= v->from[1] && h <= v->to[1])", 210 " return v->dst[1];", 211 " for (e = v->Succ; e; e = e->Nxt)", 212 " if (INRANGE(e,h))", 213 " return e->Dst;", 214 " Uerror(\"cannot happen Delta\");", 215 " return (Vertex *) 0;", 216 "}", 217 "", 218 "static void", 219 "numDelta(Vertex *v, int d)", 220 "{ Edge *e;", 221 " ulong cnt;", 222 " int i;", 223 "", 224 " for (i = 0; i < 2; i++)", 225 " if (v->dst[i])", 226 " { cnt = v->dst[i]->num + d*(1 + v->to[i] - v->from[i]);", 227 " if (d == 1 && cnt < v->dst[i]->num) goto bad;", 228 " v->dst[i]->num = cnt;", 229 " }", 230 " for (e = v->Succ; e; e = e->Nxt)", 231 " { cnt = e->Dst->num + d*(1 + e->To - e->From + e->s);", 232 " if (d == 1 && cnt < e->Dst->num)", 233 "bad: Uerror(\"too many incoming edges\");", 234 " e->Dst->num = cnt;", 235 " }", 236 "}", 237 "", 238 "static void", 239 "setDelta(Vertex *v, int h, Vertex *newdst) /* v->delta[h] = newdst; */", 240 "{ Edge *e, *f = (Edge *) 0, *g;", 241 " int i;", 242 "", 243 " /* remove the old entry, if there */", 244 " for (i = 0; i < 2; i++)", 245 " if (v->dst[i] && h >= v->from[i] && h <= v->to[i])", 246 " { if (h == v->from[i])", 247 " { if (h == v->to[i])", 248 " { v->dst[i] = (Vertex *) 0;", 249 " v->from[i] = v->to[i] = 0;", 250 " } else", 251 " v->from[i]++;", 252 " } else if (h == v->to[i])", 253 " { v->to[i]--;", 254 " } else", 255 " { g = new_edge(v->dst[i]);/* same dst */", 256 " g->From = v->from[i];", 257 " g->To = h-1; /* left half */", 258 " v->from[i] = h+1; /* right half */", 259 " insert_edge(v, g);", 260 " }", 261 " goto part2;", 262 " }", 263 " for (e = v->Succ; e; f = e, e = e->Nxt)", 264 " { if (e->s == 1 && e->S == h)", 265 " { e->s = e->S = 0;", 266 " goto rem_tst;", 267 " }", 268 " if (h >= e->From && h <= e->To)", 269 " { if (h == e->From)", 270 " { if (h == e->To)", 271 " { if (e->s)", 272 " { e->From = e->To = e->S;", 273 " e->s = 0;", 274 " break;", 275 " } else", 276 " goto rem_do;", 277 " } else", 278 " e->From++;", 279 " } else if (h == e->To)", 280 " { e->To--;", 281 " } else /* split */", 282 " { g = new_edge(e->Dst); /* same dst */", 283 " g->From = e->From;", 284 " g->To = h-1; /* g=left half */", 285 " e->From = h+1; /* e=right half */", 286 " g->Nxt = e->Nxt; /* insert g */", 287 " e->Nxt = g; /* behind e */", 288 " break; /* done */", 289 " }", 290 "", 291 "rem_tst: if (e->From > e->To)", 292 " { if (e->s == 0) {", 293 "rem_do: if (f)", 294 " f->Nxt = e->Nxt;", 295 " else", 296 " v->Succ = e->Nxt;", 297 " e->Nxt = (Edge *) 0;", 298 " recyc_edges(e);", 299 " } else", 300 " { e->From = e->To = e->S;", 301 " e->s = 0;", 302 " } }", 303 " break;", 304 " } }", 305 "part2:", 306 " /* check if newdst is already there */", 307 " for (i = 0; i < 2; i++)", 308 " if (v->dst[i] == newdst)", 309 " { if (h+1 == (int) v->from[i])", 310 " { v->from[i] = h;", 311 " return;", 312 " }", 313 " if (h == (int) v->to[i]+1)", 314 " { v->to[i] = h;", 315 " return;", 316 " } }", 317 " for (e = v->Succ; e; e = e->Nxt)", 318 " { if (e->Dst == newdst)", 319 " { if (h+1 == (int) e->From)", 320 " { e->From = h;", 321 " if (e->s == 1 && e->S+1 == e->From)", 322 " { e->From = e->S;", 323 " e->s = e->S = 0;", 324 " }", 325 " return;", 326 " }", 327 " if (h == (int) e->To+1)", 328 " { e->To = h;", 329 " if (e->s == 1 && e->S == e->To+1)", 330 " { e->To = e->S;", 331 " e->s = e->S = 0;", 332 " }", 333 " return;", 334 " }", 335 " if (e->s == 0)", 336 " { e->s = 1;", 337 " e->S = h;", 338 " return;", 339 " } } }", 340 " /* add as a new edge */", 341 " e = new_edge(newdst);", 342 " e->From = e->To = h;", 343 " insert_edge(v, e);", 344 "}", 345 "", 346 "static ulong", 347 "cheap_key(Vertex *v)", 348 "{ ulong vk2 = 0;", 349 "", 350 " if (v->dst[0])", 351 " { vk2 = (ulong) v->dst[0];", 352 " if ((ulong) v->dst[1] > vk2)", 353 " vk2 = (ulong) v->dst[1];", 354 " } else if (v->dst[1])", 355 " vk2 = (ulong) v->dst[1]; ", 356 " if (v->Succ)", 357 " { Edge *e;", 358 " for (e = v->Succ; e; e = e->Nxt)", 359 " if ((ulong) e->Dst > vk2)", 360 " vk2 = (ulong) e->Dst;", 361 " }", 362 " Tally = (vk2>>2)&(TWIDTH-1);", 363 " return v->key;", 364 "}", 365 "", 366 "static ulong", 367 "mk_key(Vertex *v) /* not sensitive to order */", 368 "{ ulong m = 0, vk2 = 0;", 369 " Edge *e;", 370 "", 371 " if (v->dst[0])", 372 " { m += HASH(v->dst[0], v->to[0] - v->from[0] + 1);", 373 " vk2 = (ulong) v->dst[0]; ", 374 " }", 375 " if (v->dst[1])", 376 " { m += HASH(v->dst[1], v->to[1] - v->from[1] + 1);", 377 " if ((ulong) v->dst[1] > vk2) vk2 = (ulong) v->dst[1]; ", 378 " }", 379 " for (e = v->Succ; e; e = e->Nxt)", 380 " { m += HASH(e->Dst, e->To - e->From + 1 + e->s);", 381 " if ((ulong) e->Dst > vk2) vk2 = (ulong) e->Dst; ", 382 " }", 383 " Tally = (vk2>>2)&(TWIDTH-1);", 384 " return m;", 385 "}", 386 "", 387 "static ulong", 388 "mk_special(int sigma, Vertex *n, Vertex *v)", 389 "{ ulong m = 0, vk2 = 0;", 390 " Edge *f;", 391 " int i;", 392 "", 393 " for (i = 0; i < 2; i++)", 394 " if (v->dst[i])", 395 " { if (sigma >= v->from[i] && sigma <= v->to[i])", 396 " { m += HASH(v->dst[i], v->to[i]-v->from[i]);", 397 " if ((ulong) v->dst[i] > vk2", 398 " && v->to[i] > v->from[i])", 399 " vk2 = (ulong) v->dst[i]; ", 400 " } else", 401 " { m += HASH(v->dst[i], v->to[i]-v->from[i]+1);", 402 " if ((ulong) v->dst[i] > vk2)", 403 " vk2 = (ulong) v->dst[i]; ", 404 " } }", 405 " for (f = v->Succ; f; f = f->Nxt)", 406 " { if (sigma >= f->From && sigma <= f->To)", 407 " { m += HASH(f->Dst, f->To - f->From + f->s);", 408 " if ((ulong) f->Dst > vk2", 409 " && f->To - f->From + f->s > 0)", 410 " vk2 = (ulong) f->Dst; ", 411 " } else if (f->s == 1 && sigma == f->S)", 412 " { m += HASH(f->Dst, f->To - f->From + 1);", 413 " if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; ", 414 " } else", 415 " { m += HASH(f->Dst, f->To - f->From + 1 + f->s);", 416 " if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; ", 417 " } }", 418 "", 419 " if ((ulong) n > vk2) vk2 = (ulong) n; ", 420 " Tally = (vk2>>2)&(TWIDTH-1);", 421 " m += HASH(n, 1);", 422 " return m;", 423 "}", 424 "", 425 "void ", 426 "dfa_init(ushort nr_layers)", 427 "{ int i; Vertex *r, *t;", 428 "", 429 " dfa_depth = nr_layers; /* one byte per layer */", 430 " path = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));", 431 " layers = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));", 432 " lastword = (uchar *) emalloc((dfa_depth+1)*sizeof(uchar));", 433 " lastword[dfa_depth] = lastword[0] = 255;", 434 " path[0] = R = new_vertex(); F = new_vertex();", 435 "", 436 " for (i = 1, r = R; i < dfa_depth; i++, r = t)", 437 " t = allDelta(r, i-1);", 438 " NF = allDelta(r, i-1);", 439 "}", 440 "", 441 "#if 0", 442 "static void complement_dfa(void) { Vertex *tmp = F; F = NF; NF = tmp; }", 443 "#endif", 444 "", 445 "double", 446 "tree_stats(Vertex *t)", 447 "{ Edge *e; double cnt=0.0;", 448 " if (!t) return 0;", 449 " if (!t->key) return 0;", 450 " t->key = 0; /* precaution */", 451 " if (t->dst[0]) cnt++;", 452 " if (t->dst[1]) cnt++;", 453 " for (e = t->Succ; e; e = e->Nxt)", 454 " cnt++;", 455 " cnt += tree_stats(t->lnk);", 456 " cnt += tree_stats(t->left);", 457 " cnt += tree_stats(t->right);", 458 " return cnt;", 459 "}", 460 "", 461 "void", 462 "dfa_stats(void)", 463 "{ int i, j; double cnt = 0.0;", 464 " for (j = 0; j < TWIDTH; j++)", 465 " for (i = 0; i < dfa_depth+1; i++)", 466 " cnt += tree_stats(layers[i*TWIDTH+j]);", 467 " printf(\"Minimized Automaton:\t%%6lu nodes and %%6g edges\\n\",", 468 " nr_states, cnt);", 469 "}", 470 "", 471 "int", 472 "dfa_member(ulong n)", 473 "{ Vertex **p, **q;", 474 " uchar *w = &word[n];", 475 " int i;", 476 "", 477 " p = &path[n]; q = (p+1);", 478 " for (i = n; i < dfa_depth; i++)", 479 " *q++ = Delta(*p++, *w++);", 480 " return (*p == F);", 481 "}", 482 "", 483 "int", 484 "dfa_store(uchar *sv)", 485 "{ Vertex **p, **q, *s, *y, *old, *new = F;", 486 " uchar *w, *u = lastword;", 487 " int i, j, k;", 488 "", 489 " w = word = sv;", 490 " while (*w++ == *u++) /* find first byte that differs */", 491 " ;", 492 " pfrst = (int) (u - lastword) - 1;", 493 " memcpy(&lastword[pfrst], &sv[pfrst], dfa_depth-pfrst);", 494 " if (pfrst > iv) pfrst = iv;", 495 " if (pfrst > nv) pfrst = nv;", 496 "/* phase1: */", 497 " p = &path[pfrst]; q = (p+1); w = &word[pfrst];", 498 " for (i = pfrst; i < dfa_depth; i++)", 499 " *q++ = Delta(*p++, *w++); /* (*p)->delta[*w++]; */", 500 "", 501 " if (*p == F) return 1; /* it's already there */", 502 "/* phase2: */", 503 " iv = dfa_depth;", 504 " do { iv--;", 505 " old = new;", 506 " new = find_it(path[iv], old, word[iv], iv);", 507 " } while (new && iv > 0);", 508 "", 509 "/* phase3: */", 510 " nv = k = 0; s = path[0];", 511 " for (j = 1; j <= iv; ++j) ", 512 " if (path[j]->num > 1)", 513 " { y = new_vertex();", 514 " copyEdges(y, path[j]);", 515 " insert_it(y, j);", 516 " numDelta(y, 1);", 517 " delete_it(s, j-1);", 518 " setDelta(s, word[j-1], y);", 519 " insert_it(s, j-1);", 520 " y->num = 1; /* initial value 1 */", 521 " s = y;", 522 " path[j]->num--; /* only 1 moved from j to y */", 523 " k = 1;", 524 " } else", 525 " { s = path[j];", 526 " if (!k) nv = j;", 527 " }", 528 " y = Delta(s, word[iv]);", 529 " y->num--;", 530 " delete_it(s, iv); ", 531 " setDelta(s, word[iv], old);", 532 " insert_it(s, iv); ", 533 " old->num++;", 534 "", 535 " for (j = iv+1; j < dfa_depth; j++)", 536 " if (path[j]->num == 0)", 537 " { numDelta(path[j], -1);", 538 " delete_it(path[j], j);", 539 " recyc_vertex(path[j]);", 540 " } else", 541 " break;", 542 " return 0;", 543 "}", 544 "", 545 "static Vertex *", 546 "splay(ulong i, Vertex *t)", 547 "{ Vertex N, *l, *r, *y;", 548 "", 549 " if (!t) return t;", 550 " N.left = N.right = (Vertex *) 0;", 551 " l = r = &N;", 552 " for (;;)", 553 " { if (i < t->key)", 554 " { if (!t->left) break;", 555 " if (i < t->left->key)", 556 " { y = t->left;", 557 " t->left = y->right;", 558 " y->right = t;", 559 " t = y;", 560 " if (!t->left) break;", 561 " }", 562 " r->left = t;", 563 " r = t;", 564 " t = t->left;", 565 " } else if (i > t->key)", 566 " { if (!t->right) break;", 567 " if (i > t->right->key)", 568 " { y = t->right;", 569 " t->right = y->left;", 570 " y->left = t;", 571 " t = y;", 572 " if (!t->right) break;", 573 " }", 574 " l->right = t;", 575 " l = t;", 576 " t = t->right;", 577 " } else", 578 " break;", 579 " }", 580 " l->right = t->left;", 581 " r->left = t->right;", 582 " t->left = N.right;", 583 " t->right = N.left;", 584 " return t;", 585 "}", 586 "", 587 "static void", 588 "insert_it(Vertex *v, int L)", 589 "{ Vertex *new, *t;", 590 " ulong i; int nr;", 591 "", 592 " i = mk_key(v);", 593 " nr = ((L*TWIDTH)+Tally);", 594 " t = layers[nr];", 595 "", 596 " v->key = i; ", 597 " if (!t)", 598 " { layers[nr] = v;", 599 " return;", 600 " }", 601 " t = splay(i, t);", 602 " if (i < t->key)", 603 " { new = v;", 604 " new->left = t->left;", 605 " new->right = t;", 606 " t->left = (Vertex *) 0;", 607 " } else if (i > t->key)", 608 " { new = v;", 609 " new->right = t->right;", 610 " new->left = t;", 611 " t->right = (Vertex *) 0;", 612 " } else /* it's already there */", 613 " { v->lnk = t->lnk; /* put in linked list off v */", 614 " t->lnk = v;", 615 " new = t;", 616 " }", 617 " layers[nr] = new;", 618 "}", 619 "", 620 "static int", 621 "checkit(Vertex *h, Vertex *v, Vertex *n, uchar sigma)", 622 "{ Edge *g, *f;", 623 " int i, k, j = 1;", 624 "", 625 " for (k = 0; k < 2; k++)", 626 " if (h->dst[k])", 627 " { if (sigma >= h->from[k] && sigma <= h->to[k])", 628 " { if (h->dst[k] != n) goto no_match;", 629 " }", 630 " for (i = h->from[k]; i <= h->to[k]; i++)", 631 " { if (i == sigma) continue;", 632 " g = cacheDelta(v, i, j); j = 0;", 633 " if (h->dst[k] != g->Dst)", 634 " goto no_match;", 635 " if (g->s == 0 || g->S != i)", 636 " i = g->To;", 637 " } }", 638 " for (f = h->Succ; f; f = f->Nxt)", 639 " { if (INRANGE(f,sigma))", 640 " { if (f->Dst != n) goto no_match;", 641 " }", 642 " for (i = f->From; i <= f->To; i++)", 643 " { if (i == sigma) continue;", 644 " g = cacheDelta(v, i, j); j = 0;", 645 " if (f->Dst != g->Dst)", 646 " goto no_match;", 647 " if (g->s == 1 && i == g->S)", 648 " continue;", 649 " i = g->To;", 650 " }", 651 " if (f->s && f->S != sigma)", 652 " { g = cacheDelta(v, f->S, 1);", 653 " if (f->Dst != g->Dst)", 654 " goto no_match;", 655 " }", 656 " }", 657 " if (h->Succ || h->dst[0] || h->dst[1]) return 1;", 658 "no_match:", 659 " return 0;", 660 "}", 661 "", 662 "static Vertex *", 663 "find_it(Vertex *v, Vertex *n, uchar sigma, int L)", 664 "{ Vertex *z, *t;", 665 " ulong i; int nr;", 666 "", 667 " i = mk_special(sigma,n,v);", 668 " nr = ((L*TWIDTH)+Tally);", 669 " t = layers[nr];", 670 "", 671 " if (!t) return (Vertex *) 0;", 672 " layers[nr] = t = splay(i, t);", 673 " if (i == t->key)", 674 " for (z = t; z; z = z->lnk)", 675 " if (checkit(z, v, n, sigma))", 676 " return z;", 677 "", 678 " return (Vertex *) 0;", 679 "}", 680 "", 681 "static void", 682 "delete_it(Vertex *v, int L)", 683 "{ Vertex *x, *t;", 684 " ulong i; int nr;", 685 "", 686 " i = cheap_key(v);", 687 " nr = ((L*TWIDTH)+Tally);", 688 " t = layers[nr];", 689 " if (!t) return;", 690 "", 691 " t = splay(i, t);", 692 " if (i == t->key)", 693 " { Vertex *z, *y = (Vertex *) 0;", 694 " for (z = t; z && z != v; y = z, z = z->lnk)", 695 " ;", 696 " if (z != v) goto bad;", 697 " if (y)", 698 " { y->lnk = z->lnk;", 699 " z->lnk = (Vertex *) 0;", 700 " layers[nr] = t;", 701 " return;", 702 " } else if (z->lnk) /* z == t == v */", 703 " { y = z->lnk;", 704 " y->left = t->left;", 705 " y->right = t->right;", 706 " t->left = t->right = t->lnk = (Vertex *) 0;", 707 " layers[nr] = y;", 708 " return;", 709 " }", 710 " /* delete the node itself */", 711 " if (!t->left)", 712 " { x = t->right;", 713 " } else", 714 " { x = splay(i, t->left);", 715 " x->right = t->right;", 716 " }", 717 " t->left = t->right = t->lnk = (Vertex *) 0;", 718 " layers[nr] = x;", 719 " return;", 720 " }", 721 "bad: Uerror(\"cannot happen delete\");", 722 "}", 723 "#endif", /* MA */ 724 0, 725 }; 726