verif/Spin/Src5.1.6/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                 if (t != ZS)
 150                         cmp = strcmp(s->name, t->name);
 151                 else
 152                         cmp = 0;
 153                 if (cmp == 0)   /* duplicate */
 154                         return;
 155                 if (cmp < 0)
 156                 {       if (!prev)
 157                         {       can = tl_nn(tok, N, can);
 158                                 return;
 159                         } else
 160                         {       ptr = &(prev->rgt);
 161                                 goto insert;
 162         }       }       }
 163
 164         /* new entry goes at the end of the list */
 165         ptr = &(prev->rgt);
 166 insert:
 167         t = DoDump(*ptr);
 168         cmp = strcmp(s->name, t->name);
 169         if (cmp == 0)   /* duplicate */
 170                 return;
 171         if (cmp < 0)
 172                 *ptr = tl_nn(tok, N, *ptr);
 173         else
 174                 *ptr = tl_nn(tok, *ptr, N);
 175 }
 176
 177 static void
 178 marknode(int tok, Node *m)
 179 {
 180         if (m->ntyp != tok)
 181         {       releasenode(0, m->rgt);
 182                 m->rgt = ZN;
 183         }
 184         m->ntyp = -1;
 185 }
 186
 187 Node *
 188 Canonical(Node *n)
 189 {       Node *m, *p, *k1, *k2, *prev, *dflt = ZN;
 190         int tok;
 191
 192         if (!n) return n;
 193
 194         tok = n->ntyp;
 195         if (tok != AND && tok != OR)
 196                 return n;
 197
 198         can = ZN;
 199         addcan(tok, n);
 200 #if 0
 201         Debug("\nA0: "); Dump(can);
 202         Debug("\nA1: "); Dump(n); Debug("\n");
 203 #endif
 204         releasenode(1, n);
 205
 206         /* mark redundant nodes */
 207         if (tok == AND)
 208         {       for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
 209                 {       k1 = (m->ntyp == AND) ? m->lft : m;
 210                         if (k1->ntyp == TRUE)
 211                         {       marknode(AND, m);
 212                                 dflt = True;
 213                                 continue;
 214                         }
 215                         if (k1->ntyp == FALSE)
 216                         {       releasenode(1, can);
 217                                 can = False;
 218                                 goto out;
 219                 }       }
 220                 for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
 221                 for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN)
 222                 {       if (p == m
 223                         ||  p->ntyp == -1
 224                         ||  m->ntyp == -1)
 225                                 continue;
 226                         k1 = (m->ntyp == AND) ? m->lft : m;
 227                         k2 = (p->ntyp == AND) ? p->lft : p;
 228
 229                         if (isequal(k1, k2))
 230                         {       marknode(AND, p);
 231                                 continue;
 232                         }
 233                         if (anywhere(OR, k1, k2))
 234                         {       marknode(AND, p);
 235                                 continue;
 236                         }
 237         }       }
 238         if (tok == OR)
 239         {       for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
 240                 {       k1 = (m->ntyp == OR) ? m->lft : m;
 241                         if (k1->ntyp == FALSE)
 242                         {       marknode(OR, m);
 243                                 dflt = False;
 244                                 continue;
 245                         }
 246                         if (k1->ntyp == TRUE)
 247                         {       releasenode(1, can);
 248                                 can = True;
 249                                 goto out;
 250                 }       }
 251                 for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
 252                 for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN)
 253                 {       if (p == m
 254                         ||  p->ntyp == -1
 255                         ||  m->ntyp == -1)
 256                                 continue;
 257                         k1 = (m->ntyp == OR) ? m->lft : m;
 258                         k2 = (p->ntyp == OR) ? p->lft : p;
 259
 260                         if (isequal(k1, k2))
 261                         {       marknode(OR, p);
 262                                 continue;
 263                         }
 264                         if (anywhere(AND, k1, k2))
 265                         {       marknode(OR, p);
 266                                 continue;
 267                         }
 268         }       }
 269         for (m = can, prev = ZN; m; )   /* remove marked nodes */
 270         {       if (m->ntyp == -1)
 271                 {       k2 = m->rgt;
 272                         releasenode(0, m);
 273                         if (!prev)
 274                         {       m = can = can->rgt;
 275                         } else
 276                         {       m = prev->rgt = k2;
 277                                 /* if deleted the last node in a chain */
 278                                 if (!prev->rgt && prev->lft
 279                                 &&  (prev->ntyp == AND || prev->ntyp == OR))
 280                                 {       k1 = prev->lft;
 281                                         prev->ntyp = prev->lft->ntyp;
 282                                         prev->sym = prev->lft->sym;
 283                                         prev->rgt = prev->lft->rgt;
 284                                         prev->lft = prev->lft->lft;
 285                                         releasenode(0, k1);
 286                                 }
 287                         }
 288                         continue;
 289                 }
 290                 prev = m;
 291                 m = m->rgt;
 292         }
 293 out:
 294 #if 0
 295         Debug("A2: "); Dump(can); Debug("\n");
 296 #endif
 297         if (!can)
 298         {       if (!dflt)
 299                         fatal("cannot happen, Canonical", (char *) 0);
 300                 return dflt;
 301         }
 302
 303         return can;
 304 }