libbanshee/points-to/andersen_terms.c

   1 /*
   2
   3 DO NOT edit this file
   4
   5 */
   6 #include <engine/list.h>
   7 #include <regions.h>
   8 #include <engine/banshee.h>
   9 #include <assert.h>
  10 #include <stdio.h>
  11 #include <engine/bool.h>
  12 #include <engine/ufind.h>
  13 #include <string.h>
  14 #include <engine/setif-sort.h>
  15 #include <engine/flowrow-sort.h>
  16 #include <engine/setif-sort.h>
  17
  18 #define REF_ 11
  19 #define REFPROJ0_ 12
  20 #define REFPROJ1_ 13
  21 #define REFPROJ2_ 14
  22 #define LAM_ 15
  23 #define LAMPROJ0_ 16
  24 #define LAMPROJ1_ 17
  25 #define LAMPROJ2_ 18
  26
  27 typedef gen_e label_term;
  28 typedef gen_e_list label_term_list;
  29
  30 typedef struct flowrow_field *argterm_field;
  31 typedef flowrow_map argterm_map;
  32 typedef gen_e argterm;
  33
  34 typedef gen_e aterm;
  35 typedef gen_e_list aterm_list;
  36
  37
  38 stamp label_term_get_stamp(gen_e arg1);
  39 bool label_term_is_var(gen_e arg1);
  40 DECLARE_OPAQUE_LIST(label_term_list,gen_e)
  41 label_term label_term_zero(void);
  42 label_term label_term_one(void);
  43 label_term label_term_fresh(const char *name);
  44 label_term label_term_union(label_term_list exprs) deletes;
  45 label_term label_term_inter(label_term_list exprs) deletes;
  46 label_term label_term_constant(const char *name) deletes;
  47 bool label_term_is_constant(label_term e,const char *name);
  48 label_term_list label_term_tlb(label_term e) deletes;
  49 void label_term_inclusion(label_term e1,label_term e2) deletes;
  50 void label_term_unify(label_term e1,label_term e2) deletes;
  51
  52 void label_term_print(FILE* arg1,label_term arg2) deletes;
  53 static bool label_term_res_proj(setif_var arg1,gen_e arg2) deletes;
  54 static void label_term_con_match(gen_e arg1,gen_e arg2) deletes;
  55 stamp argterm_get_stamp(gen_e arg1);
  56 bool argterm_is_var(gen_e arg1);
  57 DECLARE_OPAQUE_LIST(argterm_map,flowrow_field)
  58 void argterm_print(FILE *f,argterm row) deletes;
  59 stamp aterm_get_stamp(gen_e arg1);
  60 bool aterm_is_var(gen_e arg1);
  61 DECLARE_OPAQUE_LIST(aterm_list,gen_e)
  62 aterm aterm_zero(void);
  63 aterm aterm_one(void);
  64 aterm aterm_fresh(const char *name);
  65 aterm aterm_union(aterm_list exprs) deletes;
  66 aterm aterm_inter(aterm_list exprs) deletes;
  67 aterm aterm_constant(const char *name) deletes;
  68 bool aterm_is_constant(aterm e,const char *name);
  69 aterm_list aterm_tlb(aterm e) deletes;
  70 void aterm_inclusion(aterm e1,aterm e2) deletes;
  71 void aterm_unify(aterm e1,aterm e2) deletes;
  72
  73 aterm ref(label_term arg1,aterm arg2,aterm arg3) deletes;
  74 struct ref_decon ref_decon(aterm arg1);
  75 struct ref_
  76 {
  77 int type;
  78 stamp st;
  79 label_term f0;
  80 aterm f1;
  81 aterm f2;
  82 };
  83 struct ref_decon
  84 {
  85 label_term f0;
  86 aterm f1;
  87 aterm f2;
  88 };
  89 struct refProj0_
  90 {
  91 int type;
  92 stamp st;
  93 label_term f0;
  94 };
  95 static gen_e ref_pat0_con(gen_e arg1) deletes;
  96 aterm ref_pat0(label_term arg1) deletes;
  97 struct refProj1_
  98 {
  99 int type;
 100 stamp st;
 101 aterm f0;
 102 };
 103 static gen_e ref_pat1_con(gen_e arg1) deletes;
 104 aterm ref_pat1(aterm arg1) deletes;
 105 struct refProj2_
 106 {
 107 int type;
 108 stamp st;
 109 aterm f0;
 110 };
 111 static gen_e ref_pat2_con(gen_e arg1) deletes;
 112 aterm ref_pat2(aterm arg1) deletes;
 113 aterm lam(label_term arg1,argterm arg2,aterm arg3) deletes;
 114 struct lam_decon lam_decon(aterm arg1);
 115 struct lam_
 116 {
 117 int type;
 118 stamp st;
 119 label_term f0;
 120 argterm f1;
 121 aterm f2;
 122 };
 123 struct lam_decon
 124 {
 125 label_term f0;
 126 argterm f1;
 127 aterm f2;
 128 };
 129 struct lamProj0_
 130 {
 131 int type;
 132 stamp st;
 133 label_term f0;
 134 };
 135 static gen_e lam_pat0_con(gen_e arg1) deletes;
 136 aterm lam_pat0(label_term arg1) deletes;
 137 struct lamProj1_
 138 {
 139 int type;
 140 stamp st;
 141 argterm f0;
 142 };
 143 static gen_e lam_pat1_con(gen_e arg1) deletes;
 144 aterm lam_pat1(argterm arg1) deletes;
 145 struct lamProj2_
 146 {
 147 int type;
 148 stamp st;
 149 aterm f0;
 150 };
 151 static gen_e lam_pat2_con(gen_e arg1) deletes;
 152 aterm lam_pat2(aterm arg1) deletes;
 153 void aterm_print(FILE* arg1,aterm arg2) deletes;
 154 static bool aterm_res_proj(setif_var arg1,gen_e arg2) deletes;
 155 static void aterm_con_match(gen_e arg1,gen_e arg2) deletes;
 156
 157 stamp label_term_get_stamp(gen_e arg1)
 158 {
 159 return setif_get_stamp((gen_e)arg1);
 160 }
 161
 162 bool label_term_is_var(gen_e arg1)
 163 {
 164 return setif_is_var((gen_e)arg1);
 165 }
 166
 167 DEFINE_LIST(label_term_list,gen_e)
 168 label_term label_term_zero(void)
 169 {
 170  return setif_zero();
 171 }
 172
 173 label_term label_term_one(void)
 174 {
 175  return setif_one();
 176 }
 177
 178 label_term label_term_fresh(const char *name)
 179 {
 180  return setif_fresh(name);
 181 }
 182
 183 static label_term label_term_fresh_small(const char *name)
 184 {
 185  return setif_fresh_small(name);
 186 }
 187
 188 static label_term label_term_fresh_large(const char *name)
 189 {
 190  return setif_fresh_large(name);
 191 }
 192
 193 label_term label_term_union(label_term_list exprs) deletes
 194 {
 195  return setif_union(exprs);
 196 }
 197
 198 label_term label_term_inter(label_term_list exprs) deletes
 199 {
 200  return setif_inter(exprs);
 201 }
 202
 203 label_term label_term_constant(const char *name) deletes
 204 {
 205  return setif_constant(name);
 206 }
 207
 208 bool label_term_is_constant(label_term e, const char *name)
 209 {
 210  if (setif_is_constant(e))
 211 return (! strcmp(name,setif_get_constant_name(e)));
 212 else return FALSE;
 213 }
 214
 215 label_term_list label_term_tlb(label_term e) deletes
 216 {
 217  return setif_tlb(e);
 218 }
 219
 220 void label_term_inclusion(label_term e1, label_term e2) deletes
 221 {
 222  setif_inclusion(label_term_con_match,label_term_res_proj,e1,e2);
 223 }
 224
 225 static void label_term_inclusion_contra(label_term e1, label_term e2) deletes
 226 {
 227  setif_inclusion(label_term_con_match,label_term_res_proj,e2,e1);
 228 }
 229
 230 void label_term_unify(label_term e1, label_term e2) deletes
 231 {
 232  setif_inclusion(label_term_con_match,label_term_res_proj,e1,e2);
 233 setif_inclusion(label_term_con_match,label_term_res_proj,e2,e1);
 234 }
 235
 236 void label_term_print(FILE* arg1,label_term arg2) deletes
 237 {
 238 switch(((setif_term)arg2)->type)
 239 {
 240 case VAR_TYPE:
 241 fprintf(arg1,"%s",sv_get_name((setif_var)arg2));
 242 break;
 243 case ZERO_TYPE:
 244 fprintf(arg1,"0");
 245 break;
 246 case ONE_TYPE:
 247 fprintf(arg1,"1");
 248 break;
 249 case CONSTANT_TYPE:
 250 fprintf(arg1,setif_get_constant_name(arg2));
 251 break;
 252 case UNION_TYPE:
 253 {
 254 gen_e_list list = setif_get_union(arg2);
 255 gen_e_list_scanner scan;
 256 gen_e temp;
 257 gen_e_list_scan(list,&scan);
 258 if (gen_e_list_next(&scan,&temp))
 259 label_term_print(arg1,temp);
 260 while (gen_e_list_next(&scan,&temp))
 261 {
 262 fprintf(arg1," || ");
 263 label_term_print(arg1,temp);
 264 }
 265
 266 }
 267 break;
 268 case INTER_TYPE:
 269 {
 270 gen_e_list list = setif_get_inter(arg2);
 271 gen_e_list_scanner scan;
 272 gen_e temp;
 273 gen_e_list_scan(list,&scan);
 274 if (gen_e_list_next(&scan,&temp))
 275 label_term_print(arg1,temp);
 276 while (gen_e_list_next(&scan,&temp))
 277 {
 278 fprintf(arg1," && ");
 279 label_term_print(arg1,temp);
 280 }
 281
 282 }
 283 break;
 284
 285 default:
 286 return ;
 287 }
 288
 289 }
 290
 291 static bool label_term_res_proj(setif_var arg1,gen_e arg2) deletes
 292 {
 293 switch(((setif_term)arg2)->type)
 294 {
 295
 296 default:
 297 return FALSE;
 298 }
 299
 300 return FALSE;
 301 }
 302
 303 static void label_term_con_match(gen_e arg1,gen_e arg2) deletes
 304 {
 305 switch(((setif_term)arg1)->type)
 306 {
 307
 308 default:
 309 failure("Inconsistent system of constraints\n");
 310 }
 311
 312 return;
 313 }
 314
 315 stamp argterm_get_stamp(gen_e arg1)
 316 {
 317 return flowrow_get_stamp((gen_e)arg1);
 318 }
 319
 320 bool argterm_is_var(gen_e arg1)
 321 {
 322 return flowrow_is_var((gen_e)arg1);
 323 }
 324
 325 DEFINE_LIST(argterm_map,flowrow_field)
 326 argterm_field argterm_make_field(const char *label, aterm expr)
 327 {
 328  flowrow_field result = ralloc(flowrow_region, struct flowrow_field);
 329 result->label = rstrdup(flowrow_region,label);
 330 result->expr = (gen_e) expr;
 331 return result;
 332 }
 333
 334 argterm argterm_zero(void)
 335 {
 336  return flowrow_zero();
 337 }
 338
 339 argterm argterm_one(void)
 340 {
 341  return flowrow_one();
 342 }
 343
 344 argterm argterm_abs(void)
 345 {
 346 return flowrow_abs();
 347 }
 348
 349 argterm argterm_wild(void)
 350 {
 351 return flowrow_wild();
 352 }
 353
 354 argterm argterm_fresh(const char *name)
 355 {
 356 return flowrow_fresh(name);
 357 }
 358
 359 static argterm argterm_fresh_small(const char *name)
 360 {
 361 return flowrow_fresh_small(name);
 362 }
 363
 364 static argterm argterm_fresh_large(const char *name)
 365 {
 366 return flowrow_fresh_large(name);
 367 }
 368
 369 argterm argterm_row(argterm_map fields,argterm rest) deletes
 370 {
 371 return flowrow_row(aterm_get_stamp,fields,rest);
 372 }
 373
 374 aterm argterm_extract_field(const char *field_name, argterm row)
 375 {
 376 return flowrow_extract_field(field_name,row);
 377 }
 378
 379 argterm argterm_extract_rest(argterm row)
 380 {
 381 return flowrow_extract_rest(row);
 382 }
 383
 384 argterm_map argterm_extract_fields(argterm row)
 385 {
 386 return flowrow_extract_fields(row);
 387 }
 388
 389 void argterm_inclusion(argterm row1, argterm row2) deletes
 390 {
 391 flowrow_inclusion(aterm_fresh,aterm_get_stamp,aterm_inclusion,aterm_zero(), row1,row2);
 392 }
 393
 394 static void argterm_inclusion_contra(argterm row1, argterm row2) deletes
 395 {
 396 flowrow_inclusion(aterm_fresh,aterm_get_stamp,aterm_inclusion,aterm_zero(), row2,row1);
 397 }
 398
 399 void argterm_unify(argterm row1, argterm row2) deletes
 400 {
 401 argterm_inclusion(row1,row2);
 402 argterm_inclusion(row2,row1);
 403 }
 404
 405 void argterm_print(FILE *f,argterm row) deletes
 406 {
 407 flowrow_print(f,aterm_get_stamp,aterm_print,row);
 408 }
 409
 410 stamp aterm_get_stamp(gen_e arg1)
 411 {
 412 return setif_get_stamp((gen_e)arg1);
 413 }
 414
 415 bool aterm_is_var(gen_e arg1)
 416 {
 417 return setif_is_var((gen_e)arg1);
 418 }
 419
 420 DEFINE_LIST(aterm_list,gen_e)
 421 aterm aterm_zero(void)
 422 {
 423  return setif_zero();
 424 }
 425
 426 aterm aterm_one(void)
 427 {
 428  return setif_one();
 429 }
 430
 431 aterm aterm_fresh(const char *name)
 432 {
 433  return setif_fresh(name);
 434 }
 435
 436 static aterm aterm_fresh_small(const char *name)
 437 {
 438  return setif_fresh_small(name);
 439 }
 440
 441 static aterm aterm_fresh_large(const char *name)
 442 {
 443  return setif_fresh_large(name);
 444 }
 445
 446 aterm aterm_union(aterm_list exprs) deletes
 447 {
 448  return setif_union(exprs);
 449 }
 450
 451 aterm aterm_inter(aterm_list exprs) deletes
 452 {
 453  return setif_inter(exprs);
 454 }
 455
 456 aterm aterm_constant(const char *name) deletes
 457 {
 458  return setif_constant(name);
 459 }
 460
 461 bool aterm_is_constant(aterm e, const char *name)
 462 {
 463  if (setif_is_constant(e))
 464 return (! strcmp(name,setif_get_constant_name(e)));
 465 else return FALSE;
 466 }
 467
 468 aterm_list aterm_tlb(aterm e) deletes
 469 {
 470  return setif_tlb(e);
 471 }
 472
 473 void aterm_inclusion(aterm e1, aterm e2) deletes
 474 {
 475  setif_inclusion(aterm_con_match,aterm_res_proj,e1,e2);
 476 }
 477
 478 static void aterm_inclusion_contra(aterm e1, aterm e2) deletes
 479 {
 480  setif_inclusion(aterm_con_match,aterm_res_proj,e2,e1);
 481 }
 482
 483 void aterm_unify(aterm e1, aterm e2) deletes
 484 {
 485  setif_inclusion(aterm_con_match,aterm_res_proj,e1,e2);
 486 setif_inclusion(aterm_con_match,aterm_res_proj,e2,e1);
 487 }
 488
 489 bool aterm_is_ref(aterm e)
 490 {
 491  return ((setif_term)e)->type == 11;
 492 }
 493
 494 aterm ref(label_term arg1,aterm arg2,aterm arg3) deletes
 495 {
 496 struct ref_ *ret;
 497 stamp s[4];
 498 s[0] = REF_;
 499 s[1] = label_term_get_stamp((gen_e)arg1);
 500 s[2] = aterm_get_stamp((gen_e)arg2);
 501 s[3] = aterm_get_stamp((gen_e)arg3);
 502 if ((ret = (struct ref_ *)term_hash_find(setif_hash,s,4)) == NULL)
 503 {
 504 ret = ralloc(setif_region,struct ref_);
 505 ret->type = s[0];
 506 ret->st = stamp_fresh();
 507 ret->f0 = arg1;
 508 ret->f1 = arg2;
 509 ret->f2 = arg3;
 510 term_hash_insert(setif_hash,(gen_e)ret,s,4);
 511 }
 512 return (aterm)ret;
 513 }
 514
 515 struct ref_decon ref_decon(aterm arg1)
 516 {
 517 if (((setif_term)arg1)->type == REF_)
 518 {
 519 struct ref_* c = (struct ref_ *)arg1;
 520 return (struct ref_decon){c->f0,c->f1,c->f2};
 521
 522 }
 523 else
 524 return (struct ref_decon){NULL,NULL,NULL};
 525 }
 526
 527 static gen_e get_ref_proj0_arg(gen_e_list arg1)
 528 {
 529 gen_e temp;
 530 gen_e_list_scanner scan;
 531 gen_e_list_scan(arg1,&scan);
 532 while (gen_e_list_next(&scan,&temp))
 533 {
 534 if (((setif_term)temp)->type == REFPROJ0_)
 535 return (gen_e)((struct refProj0_ * ) temp)->f0;
 536 }
 537 return NULL;
 538 }
 539
 540 label_term ref_proj0(aterm arg1) deletes
 541  {
 542 label_term c;
 543 if (setif_is_var(arg1))
 544 {
 545 setif_var v = (setif_var)arg1;
 546 c = (label_term)sv_get_ub_proj(v,get_ref_proj0_arg);
 547 if (c != NULL)
 548 return c;
 549 else
 550 {
 551 aterm e;
 552 gen_e lb;
 553 gen_e_list_scanner scan;
 554 c = label_term_fresh(NULL);
 555 e = ref_pat0(c);
 556 sv_add_ub_proj(v,e);
 557 gen_e_list_scan(sv_get_lbs(v),&scan);
 558 while (gen_e_list_next(&scan,&lb))
 559 {
 560 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
 561 }
 562 return c;
 563 }
 564 }
 565 else if ( ((setif_term)arg1)->type == REF_)
 566 return ((struct ref_ * )arg1)->f0;
 567 else if ( setif_is_zero(arg1))
 568 return label_term_zero();
 569 else if ( setif_is_union(arg1))
 570 {
 571 c = get_ref_proj0_arg(setif_get_proj_cache(arg1));
 572 if (c != NULL)
 573 return c;
 574 else
 575 {
 576 aterm e;
 577 c = label_term_fresh(NULL);
 578 e = ref_pat0(c);
 579 setif_set_proj_cache(arg1,e);
 580 aterm_inclusion(arg1,e);
 581 return c;
 582 }
 583 }
 584 else
 585 {
 586 aterm e;
 587 c = label_term_fresh(NULL);
 588 e = ref_pat0(c);
 589 aterm_inclusion(arg1,e);
 590 return c;
 591 }
 592 }
 593
 594 static gen_e ref_pat0_con(gen_e arg1) deletes
 595 {
 596 return (gen_e)ref_pat0((label_term)arg1);
 597 }
 598
 599 aterm ref_pat0(label_term arg1) deletes
 600 {
 601 struct refProj0_* ret;
 602 stamp s[2];
 603 s[0] = REFPROJ0_;
 604 s[1] = label_term_get_stamp((gen_e)arg1);
 605 if ((ret = (struct refProj0_ *)term_hash_find(setif_hash,s,2)) == NULL)
 606 {
 607 ret = ralloc(setif_region,struct refProj0_);
 608 ret->type = REFPROJ0_;
 609 ret->st = stamp_fresh();
 610 ret->f0 = arg1;
 611 term_hash_insert(setif_hash,(gen_e)ret,s,2);
 612 }
 613 return (aterm)ret;
 614 }
 615
 616 static gen_e get_ref_proj1_arg(gen_e_list arg1)
 617 {
 618 gen_e temp;
 619 gen_e_list_scanner scan;
 620 gen_e_list_scan(arg1,&scan);
 621 while (gen_e_list_next(&scan,&temp))
 622 {
 623 if (((setif_term)temp)->type == REFPROJ1_)
 624 return (gen_e)((struct refProj1_ * ) temp)->f0;
 625 }
 626 return NULL;
 627 }
 628
 629 aterm ref_proj1(aterm arg1) deletes
 630  {
 631 aterm c;
 632 if (setif_is_var(arg1))
 633 {
 634 setif_var v = (setif_var)arg1;
 635 c = (aterm)sv_get_ub_proj(v,get_ref_proj1_arg);
 636 if (c != NULL)
 637 return c;
 638 else
 639 {
 640 aterm e;
 641 gen_e lb;
 642 gen_e_list_scanner scan;
 643 c = aterm_fresh(NULL);
 644 e = ref_pat1(c);
 645 sv_add_ub_proj(v,e);
 646 gen_e_list_scan(sv_get_lbs(v),&scan);
 647 while (gen_e_list_next(&scan,&lb))
 648 {
 649 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
 650 }
 651 return c;
 652 }
 653 }
 654 else if ( ((setif_term)arg1)->type == REF_)
 655 return ((struct ref_ * )arg1)->f1;
 656 else if ( setif_is_zero(arg1))
 657 return aterm_zero();
 658 else if ( setif_is_union(arg1))
 659 {
 660 c = get_ref_proj1_arg(setif_get_proj_cache(arg1));
 661 if (c != NULL)
 662 return c;
 663 else
 664 {
 665 aterm e;
 666 c = aterm_fresh(NULL);
 667 e = ref_pat1(c);
 668 setif_set_proj_cache(arg1,e);
 669 aterm_inclusion(arg1,e);
 670 return c;
 671 }
 672 }
 673 else
 674 {
 675 aterm e;
 676 c = aterm_fresh(NULL);
 677 e = ref_pat1(c);
 678 aterm_inclusion(arg1,e);
 679 return c;
 680 }
 681 }
 682
 683 static gen_e ref_pat1_con(gen_e arg1) deletes
 684 {
 685 return (gen_e)ref_pat1((aterm)arg1);
 686 }
 687
 688 aterm ref_pat1(aterm arg1) deletes
 689 {
 690 struct refProj1_* ret;
 691 stamp s[2];
 692 s[0] = REFPROJ1_;
 693 s[1] = aterm_get_stamp((gen_e)arg1);
 694 if ((ret = (struct refProj1_ *)term_hash_find(setif_hash,s,2)) == NULL)
 695 {
 696 ret = ralloc(setif_region,struct refProj1_);
 697 ret->type = REFPROJ1_;
 698 ret->st = stamp_fresh();
 699 ret->f0 = arg1;
 700 term_hash_insert(setif_hash,(gen_e)ret,s,2);
 701 }
 702 return (aterm)ret;
 703 }
 704
 705 static gen_e get_ref_proj2_arg(gen_e_list arg1)
 706 {
 707 gen_e temp;
 708 gen_e_list_scanner scan;
 709 gen_e_list_scan(arg1,&scan);
 710 while (gen_e_list_next(&scan,&temp))
 711 {
 712 if (((setif_term)temp)->type == REFPROJ2_)
 713 return (gen_e)((struct refProj2_ * ) temp)->f0;
 714 }
 715 return NULL;
 716 }
 717
 718 aterm ref_proj2(aterm arg1) deletes
 719  {
 720 aterm c;
 721 if (setif_is_var(arg1))
 722 {
 723 setif_var v = (setif_var)arg1;
 724 c = (aterm)sv_get_ub_proj(v,get_ref_proj2_arg);
 725 if (c != NULL)
 726 return c;
 727 else
 728 {
 729 aterm e;
 730 gen_e lb;
 731 gen_e_list_scanner scan;
 732 c = aterm_fresh(NULL);
 733 e = ref_pat2(c);
 734 sv_add_ub_proj(v,e);
 735 gen_e_list_scan(sv_get_lbs(v),&scan);
 736 while (gen_e_list_next(&scan,&lb))
 737 {
 738 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
 739 }
 740 return c;
 741 }
 742 }
 743 else if ( ((setif_term)arg1)->type == REF_)
 744 return ((struct ref_ * )arg1)->f2;
 745 else if ( setif_is_zero(arg1))
 746 return aterm_zero();
 747 else if ( setif_is_union(arg1))
 748 {
 749 c = get_ref_proj2_arg(setif_get_proj_cache(arg1));
 750 if (c != NULL)
 751 return c;
 752 else
 753 {
 754 aterm e;
 755 c = aterm_fresh(NULL);
 756 e = ref_pat2(c);
 757 setif_set_proj_cache(arg1,e);
 758 aterm_inclusion(arg1,e);
 759 return c;
 760 }
 761 }
 762 else
 763 {
 764 aterm e;
 765 c = aterm_fresh(NULL);
 766 e = ref_pat2(c);
 767 aterm_inclusion(arg1,e);
 768 return c;
 769 }
 770 }
 771
 772 static gen_e ref_pat2_con(gen_e arg1) deletes
 773 {
 774 return (gen_e)ref_pat2((aterm)arg1);
 775 }
 776
 777 aterm ref_pat2(aterm arg1) deletes
 778 {
 779 struct refProj2_* ret;
 780 stamp s[2];
 781 s[0] = REFPROJ2_;
 782 s[1] = aterm_get_stamp((gen_e)arg1);
 783 if ((ret = (struct refProj2_ *)term_hash_find(setif_hash,s,2)) == NULL)
 784 {
 785 ret = ralloc(setif_region,struct refProj2_);
 786 ret->type = REFPROJ2_;
 787 ret->st = stamp_fresh();
 788 ret->f0 = arg1;
 789 term_hash_insert(setif_hash,(gen_e)ret,s,2);
 790 }
 791 return (aterm)ret;
 792 }
 793
 794 bool aterm_is_lam(aterm e)
 795 {
 796  return ((setif_term)e)->type == 15;
 797 }
 798
 799 aterm lam(label_term arg1,argterm arg2,aterm arg3) deletes
 800 {
 801 struct lam_ *ret;
 802 stamp s[4];
 803 s[0] = LAM_;
 804 s[1] = label_term_get_stamp((gen_e)arg1);
 805 s[2] = argterm_get_stamp((gen_e)arg2);
 806 s[3] = aterm_get_stamp((gen_e)arg3);
 807 if ((ret = (struct lam_ *)term_hash_find(setif_hash,s,4)) == NULL)
 808 {
 809 ret = ralloc(setif_region,struct lam_);
 810 ret->type = s[0];
 811 ret->st = stamp_fresh();
 812 ret->f0 = arg1;
 813 ret->f1 = arg2;
 814 ret->f2 = arg3;
 815 term_hash_insert(setif_hash,(gen_e)ret,s,4);
 816 }
 817 return (aterm)ret;
 818 }
 819
 820 struct lam_decon lam_decon(aterm arg1)
 821 {
 822 if (((setif_term)arg1)->type == LAM_)
 823 {
 824 struct lam_* c = (struct lam_ *)arg1;
 825 return (struct lam_decon){c->f0,c->f1,c->f2};
 826
 827 }
 828 else
 829 return (struct lam_decon){NULL,NULL,NULL};
 830 }
 831
 832 static gen_e get_lam_proj0_arg(gen_e_list arg1)
 833 {
 834 gen_e temp;
 835 gen_e_list_scanner scan;
 836 gen_e_list_scan(arg1,&scan);
 837 while (gen_e_list_next(&scan,&temp))
 838 {
 839 if (((setif_term)temp)->type == LAMPROJ0_)
 840 return (gen_e)((struct lamProj0_ * ) temp)->f0;
 841 }
 842 return NULL;
 843 }
 844
 845 label_term lam_proj0(aterm arg1) deletes
 846  {
 847 label_term c;
 848 if (setif_is_var(arg1))
 849 {
 850 setif_var v = (setif_var)arg1;
 851 c = (label_term)sv_get_ub_proj(v,get_lam_proj0_arg);
 852 if (c != NULL)
 853 return c;
 854 else
 855 {
 856 aterm e;
 857 gen_e lb;
 858 gen_e_list_scanner scan;
 859 c = label_term_fresh(NULL);
 860 e = lam_pat0(c);
 861 sv_add_ub_proj(v,e);
 862 gen_e_list_scan(sv_get_lbs(v),&scan);
 863 while (gen_e_list_next(&scan,&lb))
 864 {
 865 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
 866 }
 867 return c;
 868 }
 869 }
 870 else if ( ((setif_term)arg1)->type == LAM_)
 871 return ((struct lam_ * )arg1)->f0;
 872 else if ( setif_is_zero(arg1))
 873 return label_term_zero();
 874 else if ( setif_is_union(arg1))
 875 {
 876 c = get_lam_proj0_arg(setif_get_proj_cache(arg1));
 877 if (c != NULL)
 878 return c;
 879 else
 880 {
 881 aterm e;
 882 c = label_term_fresh(NULL);
 883 e = lam_pat0(c);
 884 setif_set_proj_cache(arg1,e);
 885 aterm_inclusion(arg1,e);
 886 return c;
 887 }
 888 }
 889 else
 890 {
 891 aterm e;
 892 c = label_term_fresh(NULL);
 893 e = lam_pat0(c);
 894 aterm_inclusion(arg1,e);
 895 return c;
 896 }
 897 }
 898
 899 static gen_e lam_pat0_con(gen_e arg1) deletes
 900 {
 901 return (gen_e)lam_pat0((label_term)arg1);
 902 }
 903
 904 aterm lam_pat0(label_term arg1) deletes
 905 {
 906 struct lamProj0_* ret;
 907 stamp s[2];
 908 s[0] = LAMPROJ0_;
 909 s[1] = label_term_get_stamp((gen_e)arg1);
 910 if ((ret = (struct lamProj0_ *)term_hash_find(setif_hash,s,2)) == NULL)
 911 {
 912 ret = ralloc(setif_region,struct lamProj0_);
 913 ret->type = LAMPROJ0_;
 914 ret->st = stamp_fresh();
 915 ret->f0 = arg1;
 916 term_hash_insert(setif_hash,(gen_e)ret,s,2);
 917 }
 918 return (aterm)ret;
 919 }
 920
 921 static gen_e get_lam_proj1_arg(gen_e_list arg1)
 922 {
 923 gen_e temp;
 924 gen_e_list_scanner scan;
 925 gen_e_list_scan(arg1,&scan);
 926 while (gen_e_list_next(&scan,&temp))
 927 {
 928 if (((setif_term)temp)->type == LAMPROJ1_)
 929 return (gen_e)((struct lamProj1_ * ) temp)->f0;
 930 }
 931 return NULL;
 932 }
 933
 934 argterm lam_proj1(aterm arg1) deletes
 935  {
 936 argterm c;
 937 if (setif_is_var(arg1))
 938 {
 939 setif_var v = (setif_var)arg1;
 940 c = (argterm)sv_get_ub_proj(v,get_lam_proj1_arg);
 941 if (c != NULL)
 942 return c;
 943 else
 944 {
 945 aterm e;
 946 gen_e lb;
 947 gen_e_list_scanner scan;
 948 c = argterm_fresh(NULL);
 949 e = lam_pat1(c);
 950 sv_add_ub_proj(v,e);
 951 gen_e_list_scan(sv_get_lbs(v),&scan);
 952 while (gen_e_list_next(&scan,&lb))
 953 {
 954 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
 955 }
 956 return c;
 957 }
 958 }
 959 else if ( ((setif_term)arg1)->type == LAM_)
 960 return ((struct lam_ * )arg1)->f1;
 961 else if ( setif_is_zero(arg1))
 962 return argterm_zero();
 963 else if ( setif_is_union(arg1))
 964 {
 965 c = get_lam_proj1_arg(setif_get_proj_cache(arg1));
 966 if (c != NULL)
 967 return c;
 968 else
 969 {
 970 aterm e;
 971 c = argterm_fresh(NULL);
 972 e = lam_pat1(c);
 973 setif_set_proj_cache(arg1,e);
 974 aterm_inclusion(arg1,e);
 975 return c;
 976 }
 977 }
 978 else
 979 {
 980 aterm e;
 981 c = argterm_fresh(NULL);
 982 e = lam_pat1(c);
 983 aterm_inclusion(arg1,e);
 984 return c;
 985 }
 986 }
 987
 988 static gen_e lam_pat1_con(gen_e arg1) deletes
 989 {
 990 return (gen_e)lam_pat1((argterm)arg1);
 991 }
 992
 993 aterm lam_pat1(argterm arg1) deletes
 994 {
 995 struct lamProj1_* ret;
 996 stamp s[2];
 997 s[0] = LAMPROJ1_;
 998 s[1] = argterm_get_stamp((gen_e)arg1);
 999 if ((ret = (struct lamProj1_ *)term_hash_find(setif_hash,s,2)) == NULL)
1000 {
1001 ret = ralloc(setif_region,struct lamProj1_);
1002 ret->type = LAMPROJ1_;
1003 ret->st = stamp_fresh();
1004 ret->f0 = arg1;
1005 term_hash_insert(setif_hash,(gen_e)ret,s,2);
1006 }
1007 return (aterm)ret;
1008 }
1009
1010 static gen_e get_lam_proj2_arg(gen_e_list arg1)
1011 {
1012 gen_e temp;
1013 gen_e_list_scanner scan;
1014 gen_e_list_scan(arg1,&scan);
1015 while (gen_e_list_next(&scan,&temp))
1016 {
1017 if (((setif_term)temp)->type == LAMPROJ2_)
1018 return (gen_e)((struct lamProj2_ * ) temp)->f0;
1019 }
1020 return NULL;
1021 }
1022
1023 aterm lam_proj2(aterm arg1) deletes
1024  {
1025 aterm c;
1026 if (setif_is_var(arg1))
1027 {
1028 setif_var v = (setif_var)arg1;
1029 c = (aterm)sv_get_ub_proj(v,get_lam_proj2_arg);
1030 if (c != NULL)
1031 return c;
1032 else
1033 {
1034 aterm e;
1035 gen_e lb;
1036 gen_e_list_scanner scan;
1037 c = aterm_fresh(NULL);
1038 e = lam_pat2(c);
1039 sv_add_ub_proj(v,e);
1040 gen_e_list_scan(sv_get_lbs(v),&scan);
1041 while (gen_e_list_next(&scan,&lb))
1042 {
1043 setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
1044 }
1045 return c;
1046 }
1047 }
1048 else if ( ((setif_term)arg1)->type == LAM_)
1049 return ((struct lam_ * )arg1)->f2;
1050 else if ( setif_is_zero(arg1))
1051 return aterm_zero();
1052 else if ( setif_is_union(arg1))
1053 {
1054 c = get_lam_proj2_arg(setif_get_proj_cache(arg1));
1055 if (c != NULL)
1056 return c;
1057 else
1058 {
1059 aterm e;
1060 c = aterm_fresh(NULL);
1061 e = lam_pat2(c);
1062 setif_set_proj_cache(arg1,e);
1063 aterm_inclusion(arg1,e);
1064 return c;
1065 }
1066 }
1067 else
1068 {
1069 aterm e;
1070 c = aterm_fresh(NULL);
1071 e = lam_pat2(c);
1072 aterm_inclusion(arg1,e);
1073 return c;
1074 }
1075 }
1076
1077 static gen_e lam_pat2_con(gen_e arg1) deletes
1078 {
1079 return (gen_e)lam_pat2((aterm)arg1);
1080 }
1081
1082 aterm lam_pat2(aterm arg1) deletes
1083 {
1084 struct lamProj2_* ret;
1085 stamp s[2];
1086 s[0] = LAMPROJ2_;
1087 s[1] = aterm_get_stamp((gen_e)arg1);
1088 if ((ret = (struct lamProj2_ *)term_hash_find(setif_hash,s,2)) == NULL)
1089 {
1090 ret = ralloc(setif_region,struct lamProj2_);
1091 ret->type = LAMPROJ2_;
1092 ret->st = stamp_fresh();
1093 ret->f0 = arg1;
1094 term_hash_insert(setif_hash,(gen_e)ret,s,2);
1095 }
1096 return (aterm)ret;
1097 }
1098
1099 void aterm_print(FILE* arg1,aterm arg2) deletes
1100 {
1101 switch(((setif_term)arg2)->type)
1102 {
1103 case VAR_TYPE:
1104 fprintf(arg1,"%s",sv_get_name((setif_var)arg2));
1105 break;
1106 case ZERO_TYPE:
1107 fprintf(arg1,"0");
1108 break;
1109 case ONE_TYPE:
1110 fprintf(arg1,"1");
1111 break;
1112 case CONSTANT_TYPE:
1113 fprintf(arg1,setif_get_constant_name(arg2));
1114 break;
1115 case UNION_TYPE:
1116 {
1117 gen_e_list list = setif_get_union(arg2);
1118 gen_e_list_scanner scan;
1119 gen_e temp;
1120 gen_e_list_scan(list,&scan);
1121 if (gen_e_list_next(&scan,&temp))
1122 aterm_print(arg1,temp);
1123 while (gen_e_list_next(&scan,&temp))
1124 {
1125 fprintf(arg1," || ");
1126 aterm_print(arg1,temp);
1127 }
1128
1129 }
1130 break;
1131 case INTER_TYPE:
1132 {
1133 gen_e_list list = setif_get_inter(arg2);
1134 gen_e_list_scanner scan;
1135 gen_e temp;
1136 gen_e_list_scan(list,&scan);
1137 if (gen_e_list_next(&scan,&temp))
1138 aterm_print(arg1,temp);
1139 while (gen_e_list_next(&scan,&temp))
1140 {
1141 fprintf(arg1," && ");
1142 aterm_print(arg1,temp);
1143 }
1144
1145 }
1146 break;
1147 case REF_:
1148 {
1149 fprintf(arg1,"ref(");
1150 label_term_print(arg1,((struct ref_ *)arg2)->f0);
1151 fprintf(arg1,",");
1152 aterm_print(arg1,((struct ref_ *)arg2)->f1);
1153 fprintf(arg1,",");
1154 aterm_print(arg1,((struct ref_ *)arg2)->f2);
1155 fprintf(arg1,")");
1156
1157 }
1158 break;
1159 case LAM_:
1160 {
1161 fprintf(arg1,"lam(");
1162 label_term_print(arg1,((struct lam_ *)arg2)->f0);
1163 fprintf(arg1,",");
1164 argterm_print(arg1,((struct lam_ *)arg2)->f1);
1165 fprintf(arg1,",");
1166 aterm_print(arg1,((struct lam_ *)arg2)->f2);
1167 fprintf(arg1,")");
1168
1169 }
1170 break;
1171 case REFPROJ0_:
1172 {
1173 fprintf(arg1,"Proj[ref,0,");
1174 label_term_print(arg1,((struct refProj0_ *)arg2)->f0);
1175 fprintf(arg1,"]");
1176
1177 }
1178 break;
1179 case REFPROJ1_:
1180 {
1181 fprintf(arg1,"Proj[ref,1,");
1182 aterm_print(arg1,((struct refProj1_ *)arg2)->f0);
1183 fprintf(arg1,"]");
1184
1185 }
1186 break;
1187 case REFPROJ2_:
1188 {
1189 fprintf(arg1,"Proj[ref,2,");
1190 aterm_print(arg1,((struct refProj2_ *)arg2)->f0);
1191 fprintf(arg1,"]");
1192
1193 }
1194 break;
1195 case LAMPROJ0_:
1196 {
1197 fprintf(arg1,"Proj[lam,0,");
1198 label_term_print(arg1,((struct lamProj0_ *)arg2)->f0);
1199 fprintf(arg1,"]");
1200
1201 }
1202 break;
1203 case LAMPROJ1_:
1204 {
1205 fprintf(arg1,"Proj[lam,1,");
1206 argterm_print(arg1,((struct lamProj1_ *)arg2)->f0);
1207 fprintf(arg1,"]");
1208
1209 }
1210 break;
1211 case LAMPROJ2_:
1212 {
1213 fprintf(arg1,"Proj[lam,2,");
1214 aterm_print(arg1,((struct lamProj2_ *)arg2)->f0);
1215 fprintf(arg1,"]");
1216
1217 }
1218 break;
1219
1220 default:
1221 return ;
1222 }
1223
1224 }
1225
1226 static bool aterm_res_proj(setif_var arg1,gen_e arg2) deletes
1227 {
1228 switch(((setif_term)arg2)->type)
1229 {
1230 case REFPROJ0_:
1231 return setif_proj_merge(arg1,(gen_e)((struct refProj0_ *)arg2)->f0,get_ref_proj0_arg,ref_pat0_con,(fresh_large_fn_ptr)label_term_fresh_large,(incl_fn_ptr)label_term_inclusion,aterm_inclusion);
1232 break;
1233 case REFPROJ1_:
1234 return setif_proj_merge(arg1,(gen_e)((struct refProj1_ *)arg2)->f0,get_ref_proj1_arg,ref_pat1_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion_contra,aterm_inclusion);
1235 break;
1236 case REFPROJ2_:
1237 return setif_proj_merge(arg1,(gen_e)((struct refProj2_ *)arg2)->f0,get_ref_proj2_arg,ref_pat2_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion,aterm_inclusion);
1238 break;
1239 case LAMPROJ0_:
1240 return setif_proj_merge(arg1,(gen_e)((struct lamProj0_ *)arg2)->f0,get_lam_proj0_arg,lam_pat0_con,(fresh_large_fn_ptr)label_term_fresh_large,(incl_fn_ptr)label_term_inclusion,aterm_inclusion);
1241 break;
1242 case LAMPROJ1_:
1243 return setif_proj_merge(arg1,(gen_e)((struct lamProj1_ *)arg2)->f0,get_lam_proj1_arg,lam_pat1_con,(fresh_large_fn_ptr)argterm_fresh_large,(incl_fn_ptr)argterm_inclusion_contra,aterm_inclusion);
1244 break;
1245 case LAMPROJ2_:
1246 return setif_proj_merge(arg1,(gen_e)((struct lamProj2_ *)arg2)->f0,get_lam_proj2_arg,lam_pat2_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion,aterm_inclusion);
1247 break;
1248
1249 default:
1250 return FALSE;
1251 }
1252
1253 return FALSE;
1254 }
1255
1256 static void aterm_con_match(gen_e arg1,gen_e arg2) deletes
1257 {
1258 switch(((setif_term)arg1)->type)
1259 {
1260 case REF_:
1261 switch(((setif_term)arg2)->type)
1262 {
1263 case REF_:
1264 {
1265 label_term_inclusion(((struct ref_ *)arg1)->f0,((struct ref_ *)arg2)->f0);
1266 aterm_inclusion_contra(((struct ref_ *)arg1)->f1,((struct ref_ *)arg2)->f1);
1267 aterm_inclusion(((struct ref_ *)arg1)->f2,((struct ref_ *)arg2)->f2);
1268
1269 }
1270 break;
1271 case REFPROJ0_:
1272 label_term_inclusion(((struct ref_ *)arg1)->f0,((struct refProj0_ *)arg2)->f0);
1273 break;
1274 case REFPROJ1_:
1275 aterm_inclusion_contra(((struct ref_ *)arg1)->f1,((struct refProj1_ *)arg2)->f0);
1276 break;
1277 case REFPROJ2_:
1278 aterm_inclusion(((struct ref_ *)arg1)->f2,((struct refProj2_ *)arg2)->f0);
1279 break;
1280 case LAMPROJ0_:
1281 return ;
1282 break;
1283 case LAMPROJ1_:
1284 return ;
1285 break;
1286 case LAMPROJ2_:
1287 return ;
1288 break;
1289
1290 default:
1291 failure("Inconsistent system of constraints\n");
1292 }
1293
1294 break;
1295 case LAM_:
1296 switch(((setif_term)arg2)->type)
1297 {
1298 case LAM_:
1299 {
1300 label_term_inclusion(((struct lam_ *)arg1)->f0,((struct lam_ *)arg2)->f0);
1301 argterm_inclusion_contra(((struct lam_ *)arg1)->f1,((struct lam_ *)arg2)->f1);
1302 aterm_inclusion(((struct lam_ *)arg1)->f2,((struct lam_ *)arg2)->f2);
1303
1304 }
1305 break;
1306 case LAMPROJ0_:
1307 label_term_inclusion(((struct lam_ *)arg1)->f0,((struct lamProj0_ *)arg2)->f0);
1308 break;
1309 case LAMPROJ1_:
1310 argterm_inclusion_contra(((struct lam_ *)arg1)->f1,((struct lamProj1_ *)arg2)->f0);
1311 break;
1312 case LAMPROJ2_:
1313 aterm_inclusion(((struct lam_ *)arg1)->f2,((struct lamProj2_ *)arg2)->f0);
1314 break;
1315 case REFPROJ0_:
1316 return ;
1317 break;
1318 case REFPROJ1_:
1319 return ;
1320 break;
1321 case REFPROJ2_:
1322 return ;
1323 break;
1324
1325 default:
1326 failure("Inconsistent system of constraints\n");
1327 }
1328
1329 break;
1330
1331 default:
1332 failure("Inconsistent system of constraints\n");
1333 }
1334
1335 return;
1336 }
1337
1338 void andersen_terms_init(void)
1339 {
1340 engine_init();
1341 setif_init();
1342 setif_init();
1343 flowrow_init();
1344 }
1345
1346 void andersen_terms_reset(void) deletes
1347 {
1348 setif_reset();
1349 setif_reset();
1350 flowrow_reset();
1351 engine_reset();
1352 }
1353
1354 void andersen_terms_stats(FILE * arg1)
1355 {
1356 engine_stats(arg1);
1357 }
1358
1359 void andersen_terms_print_graph(FILE * arg1)
1360 {
1361 print_constraint_graphs(arg1);
1362 }
1363