123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319 |
- /*
- * This file is part of the UCB release of Plan 9. It is subject to the license
- * terms in the LICENSE file found in the top-level directory of this
- * distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
- * part of the UCB release of Plan 9, including this file, may be copied,
- * modified, propagated, or distributed except according to the terms contained
- * in the LICENSE file.
- */
- /***** 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;
- void
- ini_rewrt(void)
- {
- 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);
- if (t != ZS)
- cmp = strcmp(s->name, t->name);
- else
- cmp = 0;
- 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;
- }
|