sys/src/cmd/spin/tl_rewrt.c

   1 /***** tl_spin: tl_rewrt.c *****/
   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  * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
   9  * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
  10  */
  11
  12 #include "tl.h"
  13
  14 extern int      tl_verbose;
  15
  16 static Node     *can = ZN;
  17
  18 void
  19 ini_rewrt(void)
  20 {
  21         can = ZN;
  22 }
  23
  24 Node *
  25 right_linked(Node *n)
  26 {
  27         if (!n) return n;
  28
  29         if (n->ntyp == AND || n->ntyp == OR)
  30                 while (n->lft && n->lft->ntyp == n->ntyp)
  31                 {       Node *tmp = n->lft;
  32                         n->lft = tmp->rgt;
  33                         tmp->rgt = n;
  34                         n = tmp;
  35                 }
  36
  37         n->lft = right_linked(n->lft);
  38         n->rgt = right_linked(n->rgt);
  39
  40         return n;
  41 }
  42
  43 Node *
  44 canonical(Node *n)
  45 {       Node *m;        /* assumes input is right_linked */
  46
  47         if (!n) return n;
  48         if ((m = in_cache(n)) != ZN)
  49                 return m;
  50
  51         n->rgt = canonical(n->rgt);
  52         n->lft = canonical(n->lft);
  53
  54         return cached(n);
  55 }
  56
  57 Node *
  58 push_negation(Node *n)
  59 {       Node *m;
  60
  61         Assert(n->ntyp == NOT, n->ntyp);
  62
  63         switch (n->lft->ntyp) {
  64         case TRUE:
  65                 Debug("!true => false\n");
  66                 releasenode(0, n->lft);
  67                 n->lft = ZN;
  68                 n->ntyp = FALSE;
  69                 break;
  70         case FALSE:
  71                 Debug("!false => true\n");
  72                 releasenode(0, n->lft);
  73                 n->lft = ZN;
  74                 n->ntyp = TRUE;
  75                 break;
  76         case NOT:
  77                 Debug("!!p => p\n");
  78                 m = n->lft->lft;
  79                 releasenode(0, n->lft);
  80                 n->lft = ZN;
  81                 releasenode(0, n);
  82                 n = m;
  83                 break;
  84         case V_OPER:
  85                 Debug("!(p V q) => (!p U !q)\n");
  86                 n->ntyp = U_OPER;
  87                 goto same;
  88         case U_OPER:
  89                 Debug("!(p U q) => (!p V !q)\n");
  90                 n->ntyp = V_OPER;
  91                 goto same;
  92 #ifdef NXT
  93         case NEXT:
  94                 Debug("!X -> X!\n");
  95                 n->ntyp = NEXT;
  96                 n->lft->ntyp = NOT;
  97                 n->lft = push_negation(n->lft);
  98                 break;
  99 #endif
 100         case  AND:
 101                 Debug("!(p && q) => !p || !q\n");
 102                 n->ntyp = OR;
 103                 goto same;
 104         case  OR:
 105                 Debug("!(p || q) => !p && !q\n");
 106                 n->ntyp = AND;
 107
 108 same:           m = n->lft->rgt;
 109                 n->lft->rgt = ZN;
 110
 111                 n->rgt = Not(m);
 112                 n->lft->ntyp = NOT;
 113                 m = n->lft;
 114                 n->lft = push_negation(m);
 115                 break;
 116         }
 117
 118         return rewrite(n);
 119 }
 120
 121 static void
 122 addcan(int tok, Node *n)
 123 {       Node    *m, *prev = ZN;
 124         Node    **ptr;
 125         Node    *N;
 126         Symbol  *s, *t; int cmp;
 127
 128         if (!n) return;
 129
 130         if (n->ntyp == tok)
 131         {       addcan(tok, n->rgt);
 132                 addcan(tok, n->lft);
 133                 return;
 134         }
 135
 136         N = dupnode(n);
 137         if (!can)
 138         {       can = N;
 139                 return;
 140         }
 141
 142         s = DoDump(N);
 143         if (!s)
 144         {       fatal("unexpected error 6", (char *) 0);
 145         }
 146         if (can->ntyp != tok)   /* only one element in list so far */
 147         {       ptr = &can;
 148                 goto insert;
 149         }
 150
 151         /* there are at least 2 elements in list */
 152         prev = ZN;
 153         for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt)
 154         {       t = DoDump(m->lft);
 155                 if (t != ZS)
 156                         cmp = strcmp(s->name, t->name);
 157                 else
 158                         cmp = 0;
 159                 if (cmp == 0)   /* duplicate */
 160                         return;
 161                 if (cmp < 0)
 162                 {       if (!prev)
 163                         {       can = tl_nn(tok, N, can);
 164                                 return;
 165                         } else
 166                         {       ptr = &(prev->rgt);
 167                                 goto insert;
 168         }       }       }
 169
 170         /* new entry goes at the end of the list */
 171         ptr = &(prev->rgt);
 172 insert:
 173         t = DoDump(*ptr);
 174         cmp = strcmp(s->name, t->name);
 175         if (cmp == 0)   /* duplicate */
 176                 return;
 177         if (cmp < 0)
 178                 *ptr = tl_nn(tok, N, *ptr);
 179         else
 180                 *ptr = tl_nn(tok, *ptr, N);
 181 }
 182
 183 static void
 184 marknode(int tok, Node *m)
 185 {
 186         if (m->ntyp != tok)
 187         {       releasenode(0, m->rgt);
 188                 m->rgt = ZN;
 189         }
 190         m->ntyp = -1;
 191 }
 192
 193 Node *
 194 Canonical(Node *n)
 195 {       Node *m, *p, *k1, *k2, *prev, *dflt = ZN;
 196         int tok;
 197
 198         if (!n) return n;
 199
 200         tok = n->ntyp;
 201         if (tok != AND && tok != OR)
 202                 return n;
 203
 204         can = ZN;
 205         addcan(tok, n);
 206 #if 0
 207         Debug("\nA0: "); Dump(can);
 208         Debug("\nA1: "); Dump(n); Debug("\n");
 209 #endif
 210         releasenode(1, n);
 211
 212         /* mark redundant nodes */
 213         if (tok == AND)
 214         {       for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
 215                 {       k1 = (m->ntyp == AND) ? m->lft : m;
 216                         if (k1->ntyp == TRUE)
 217                         {       marknode(AND, m);
 218                                 dflt = True;
 219                                 continue;
 220                         }
 221                         if (k1->ntyp == FALSE)
 222                         {       releasenode(1, can);
 223                                 can = False;
 224                                 goto out;
 225                 }       }
 226                 for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
 227                 for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN)
 228                 {       if (p == m
 229                         ||  p->ntyp == -1
 230                         ||  m->ntyp == -1)
 231                                 continue;
 232                         k1 = (m->ntyp == AND) ? m->lft : m;
 233                         k2 = (p->ntyp == AND) ? p->lft : p;
 234
 235                         if (isequal(k1, k2))
 236                         {       marknode(AND, p);
 237                                 continue;
 238                         }
 239                         if (anywhere(OR, k1, k2))
 240                         {       marknode(AND, p);
 241                                 continue;
 242                         }
 243         }       }
 244         if (tok == OR)
 245         {       for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
 246                 {       k1 = (m->ntyp == OR) ? m->lft : m;
 247                         if (k1->ntyp == FALSE)
 248                         {       marknode(OR, m);
 249                                 dflt = False;
 250                                 continue;
 251                         }
 252                         if (k1->ntyp == TRUE)
 253                         {       releasenode(1, can);
 254                                 can = True;
 255                                 goto out;
 256                 }       }
 257                 for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
 258                 for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN)
 259                 {       if (p == m
 260                         ||  p->ntyp == -1
 261                         ||  m->ntyp == -1)
 262                                 continue;
 263                         k1 = (m->ntyp == OR) ? m->lft : m;
 264                         k2 = (p->ntyp == OR) ? p->lft : p;
 265
 266                         if (isequal(k1, k2))
 267                         {       marknode(OR, p);
 268                                 continue;
 269                         }
 270                         if (anywhere(AND, k1, k2))
 271                         {       marknode(OR, p);
 272                                 continue;
 273                         }
 274         }       }
 275         for (m = can, prev = ZN; m; )   /* remove marked nodes */
 276         {       if (m->ntyp == -1)
 277                 {       k2 = m->rgt;
 278                         releasenode(0, m);
 279                         if (!prev)
 280                         {       m = can = can->rgt;
 281                         } else
 282                         {       m = prev->rgt = k2;
 283                                 /* if deleted the last node in a chain */
 284                                 if (!prev->rgt && prev->lft
 285                                 &&  (prev->ntyp == AND || prev->ntyp == OR))
 286                                 {       k1 = prev->lft;
 287                                         prev->ntyp = prev->lft->ntyp;
 288                                         prev->sym = prev->lft->sym;
 289                                         prev->rgt = prev->lft->rgt;
 290                                         prev->lft = prev->lft->lft;
 291                                         releasenode(0, k1);
 292                                 }
 293                         }
 294                         continue;
 295                 }
 296                 prev = m;
 297                 m = m->rgt;
 298         }
 299 out:
 300 #if 0
 301         Debug("A2: "); Dump(can); Debug("\n");
 302 #endif
 303         if (!can)
 304         {       if (!dflt)
 305                         fatal("cannot happen, Canonical", (char *) 0);
 306                 return dflt;
 307         }
 308
 309         return can;
 310 }