ref: 01986adbbf75c07c613b11fcb81a8015a71e5664
dir: /sys/src/cmd/spin/tl_rewrt.c/
/***** tl_spin: tl_rewrt.c *****/ /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */ /* All Rights Reserved. This software is for educational purposes only. */ /* No guarantee whatsoever is expressed or implied by the distribution of */ /* this code. Permission is given to distribute this code provided that */ /* this introductory message is not removed and no monies are exchanged. */ /* Software written by Gerard J. Holzmann. For tool documentation see: */ /* http://spinroot.com/ */ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ #include "tl.h" extern int tl_verbose; static Node *can = ZN; Node * right_linked(Node *n) { if (!n) return n; if (n->ntyp == AND || n->ntyp == OR) while (n->lft && n->lft->ntyp == n->ntyp) { Node *tmp = n->lft; n->lft = tmp->rgt; tmp->rgt = n; n = tmp; } n->lft = right_linked(n->lft); n->rgt = right_linked(n->rgt); return n; } Node * canonical(Node *n) { Node *m; /* assumes input is right_linked */ if (!n) return n; if ((m = in_cache(n)) != ZN) return m; n->rgt = canonical(n->rgt); n->lft = canonical(n->lft); return cached(n); } Node * push_negation(Node *n) { Node *m; Assert(n->ntyp == NOT, n->ntyp); switch (n->lft->ntyp) { case TRUE: Debug("!true => false\n"); releasenode(0, n->lft); n->lft = ZN; n->ntyp = FALSE; break; case FALSE: Debug("!false => true\n"); releasenode(0, n->lft); n->lft = ZN; n->ntyp = TRUE; break; case NOT: Debug("!!p => p\n"); m = n->lft->lft; releasenode(0, n->lft); n->lft = ZN; releasenode(0, n); n = m; break; case V_OPER: Debug("!(p V q) => (!p U !q)\n"); n->ntyp = U_OPER; goto same; case U_OPER: Debug("!(p U q) => (!p V !q)\n"); n->ntyp = V_OPER; goto same; #ifdef NXT case NEXT: Debug("!X -> X!\n"); n->ntyp = NEXT; n->lft->ntyp = NOT; n->lft = push_negation(n->lft); break; #endif case AND: Debug("!(p && q) => !p || !q\n"); n->ntyp = OR; goto same; case OR: Debug("!(p || q) => !p && !q\n"); n->ntyp = AND; same: m = n->lft->rgt; n->lft->rgt = ZN; n->rgt = Not(m); n->lft->ntyp = NOT; m = n->lft; n->lft = push_negation(m); break; } return rewrite(n); } static void addcan(int tok, Node *n) { Node *m, *prev = ZN; Node **ptr; Node *N; Symbol *s, *t; int cmp; if (!n) return; if (n->ntyp == tok) { addcan(tok, n->rgt); addcan(tok, n->lft); return; } N = dupnode(n); if (!can) { can = N; return; } s = DoDump(N); if (can->ntyp != tok) /* only one element in list so far */ { ptr = &can; goto insert; } /* there are at least 2 elements in list */ prev = ZN; for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt) { t = DoDump(m->lft); cmp = strcmp(s->name, t->name); if (cmp == 0) /* duplicate */ return; if (cmp < 0) { if (!prev) { can = tl_nn(tok, N, can); return; } else { ptr = &(prev->rgt); goto insert; } } } /* new entry goes at the end of the list */ ptr = &(prev->rgt); insert: t = DoDump(*ptr); cmp = strcmp(s->name, t->name); if (cmp == 0) /* duplicate */ return; if (cmp < 0) *ptr = tl_nn(tok, N, *ptr); else *ptr = tl_nn(tok, *ptr, N); } static void marknode(int tok, Node *m) { if (m->ntyp != tok) { releasenode(0, m->rgt); m->rgt = ZN; } m->ntyp = -1; } Node * Canonical(Node *n) { Node *m, *p, *k1, *k2, *prev, *dflt = ZN; int tok; if (!n) return n; tok = n->ntyp; if (tok != AND && tok != OR) return n; can = ZN; addcan(tok, n); #if 0 Debug("\nA0: "); Dump(can); Debug("\nA1: "); Dump(n); Debug("\n"); #endif releasenode(1, n); /* mark redundant nodes */ if (tok == AND) { for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) { k1 = (m->ntyp == AND) ? m->lft : m; if (k1->ntyp == TRUE) { marknode(AND, m); dflt = True; continue; } if (k1->ntyp == FALSE) { releasenode(1, can); can = False; goto out; } } for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN) { if (p == m || p->ntyp == -1 || m->ntyp == -1) continue; k1 = (m->ntyp == AND) ? m->lft : m; k2 = (p->ntyp == AND) ? p->lft : p; if (isequal(k1, k2)) { marknode(AND, p); continue; } if (anywhere(OR, k1, k2)) { marknode(AND, p); continue; } } } if (tok == OR) { for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) { k1 = (m->ntyp == OR) ? m->lft : m; if (k1->ntyp == FALSE) { marknode(OR, m); dflt = False; continue; } if (k1->ntyp == TRUE) { releasenode(1, can); can = True; goto out; } } for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN) { if (p == m || p->ntyp == -1 || m->ntyp == -1) continue; k1 = (m->ntyp == OR) ? m->lft : m; k2 = (p->ntyp == OR) ? p->lft : p; if (isequal(k1, k2)) { marknode(OR, p); continue; } if (anywhere(AND, k1, k2)) { marknode(OR, p); continue; } } } for (m = can, prev = ZN; m; ) /* remove marked nodes */ { if (m->ntyp == -1) { k2 = m->rgt; releasenode(0, m); if (!prev) { m = can = can->rgt; } else { m = prev->rgt = k2; /* if deleted the last node in a chain */ if (!prev->rgt && prev->lft && (prev->ntyp == AND || prev->ntyp == OR)) { k1 = prev->lft; prev->ntyp = prev->lft->ntyp; prev->sym = prev->lft->sym; prev->rgt = prev->lft->rgt; prev->lft = prev->lft->lft; releasenode(0, k1); } } continue; } prev = m; m = m->rgt; } out: #if 0 Debug("A2: "); Dump(can); Debug("\n"); #endif if (!can) { if (!dflt) fatal("cannot happen, Canonical", (char *) 0); return dflt; } return can; }