sys/src/cmd/spin/tl_rewrt.c

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