distr/nanotrav/ntr.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [ntr.c]
   4
   5   PackageName [ntr]
   6
   7   Synopsis    [A very simple reachability analysis program.]
   8
   9   Description []
  10
  11   SeeAlso     []
  12
  13   Author      [Fabio Somenzi]
  14
  15   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  16
  17   All rights reserved.
  18
  19   Redistribution and use in source and binary forms, with or without
  20   modification, are permitted provided that the following conditions
  21   are met:
  22
  23   Redistributions of source code must retain the above copyright
  24   notice, this list of conditions and the following disclaimer.
  25
  26   Redistributions in binary form must reproduce the above copyright
  27   notice, this list of conditions and the following disclaimer in the
  28   documentation and/or other materials provided with the distribution.
  29
  30   Neither the name of the University of Colorado nor the names of its
  31   contributors may be used to endorse or promote products derived from
  32   this software without specific prior written permission.
  33
  34   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  35   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  36   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  37   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  38   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  39   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  40   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  41   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  42   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  43   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  44   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  45   POSSIBILITY OF SUCH DAMAGE.]
  46
  47 ******************************************************************************/
  48
  49 #include "ntr.h"
  50
  51 /*---------------------------------------------------------------------------*/
  52 /* Constant declarations                                                     */
  53 /*---------------------------------------------------------------------------*/
  54
  55 #define NTR_MAX_DEP_SIZE 20
  56
  57 /*---------------------------------------------------------------------------*/
  58 /* Stucture declarations                                                     */
  59 /*---------------------------------------------------------------------------*/
  60
  61 /*---------------------------------------------------------------------------*/
  62 /* Type declarations                                                         */
  63 /*---------------------------------------------------------------------------*/
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Variable declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69 #ifndef lint
  70 static char rcsid[] UTIL_UNUSED = "$Id: ntr.c,v 1.27 2009/02/21 06:00:31 fabio Exp fabio $";
  71 #endif
  72
  73 static const char *onames[] = { "T", "R" };     /* names of functions to be dumped */
  74 static double *signatures;              /* signatures for all variables */
  75 static BnetNetwork *staticNet;  /* pointer to network used by qsort
  76                                 ** comparison function */
  77 static DdNode **staticPart;     /* pointer to parts used by qsort
  78                                 ** comparison function */
  79
  80 /*---------------------------------------------------------------------------*/
  81 /* Macro declarations                                                        */
  82 /*---------------------------------------------------------------------------*/
  83
  84 /**AutomaticStart*************************************************************/
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Static function prototypes                                                */
  88 /*---------------------------------------------------------------------------*/
  89
  90 static DdNode * makecube (DdManager *dd, DdNode **x, int n);
  91 static void ntrInitializeCount (BnetNetwork *net, NtrOptions *option);
  92 static void ntrCountDFS (BnetNetwork *net, BnetNode *node);
  93 static DdNode * ntrImage (DdManager *dd, NtrPartTR *TR, DdNode *from, NtrOptions *option);
  94 static DdNode * ntrPreimage (DdManager *dd, NtrPartTR *T, DdNode *from);
  95 static DdNode * ntrChooseFrom (DdManager *dd, DdNode *neW, DdNode *reached, NtrOptions *option);
  96 static DdNode * ntrUpdateReached (DdManager *dd, DdNode *oldreached, DdNode *to);
  97 static int ntrLatchDependencies (DdManager *dd, DdNode *reached, BnetNetwork *net, NtrOptions *option);
  98 static NtrPartTR * ntrEliminateDependencies (DdManager *dd, NtrPartTR *TR, DdNode **states, NtrOptions *option);
  99 static int ntrUpdateQuantificationSchedule (DdManager *dd, NtrPartTR *T);
 100 static int ntrSignatureCompare (int * ptrX, int * ptrY);
 101 static int ntrSignatureCompare2 (int * ptrX, int * ptrY);
 102 static int ntrPartCompare (int * ptrX, int * ptrY);
 103 static char ** ntrAllocMatrix (int nrows, int ncols);
 104 static void ntrFreeMatrix (char **matrix);
 105 static void ntrPermuteParts (DdNode **a, DdNode **b, int *comesFrom, int *goesTo, int size);
 106
 107 /**AutomaticEnd***************************************************************/
 108
 109 /*---------------------------------------------------------------------------*/
 110 /* Definition of exported functions                                          */
 111 /*---------------------------------------------------------------------------*/
 112
 113
 114 /**Function********************************************************************
 115
 116   Synopsis    [Builds DDs for a network outputs and next state
 117   functions.]
 118
 119   Description [Builds DDs for a network outputs and next state
 120   functions. The method is really brain-dead, but it is very simple.
 121   Returns 1 in case of success; 0 otherwise. Some inputs to the network
 122   may be shared with another network whose DDs have already been built.
 123   In this case we want to share the DDs as well.]
 124
 125   SideEffects [the dd fields of the network nodes are modified. Uses the
 126   count fields of the nodes.]
 127
 128   SeeAlso     []
 129
 130 ******************************************************************************/
 131 int
 132 Ntr_buildDDs(
 133   BnetNetwork * net /* network for which DDs are to be built */,
 134   DdManager * dd /* DD manager */,
 135   NtrOptions * option /* option structure */,
 136   BnetNetwork * net2 /* companion network with which inputs may be shared */)
 137 {
 138     int pr = option->verb;
 139     int result;
 140     int i;
 141     BnetNode *node, *node2;
 142
 143     /* If some inputs or present state variables are shared with
 144     ** another network, we initialize their BDDs from that network.
 145     */
 146     if (net2 != NULL) {
 147         for (i = 0; i < net->npis; i++) {
 148             if (!st_lookup(net->hash,net->inputs[i],&node)) {
 149                 return(0);
 150             }
 151             if (!st_lookup(net2->hash,net->inputs[i],&node2)) {
 152                 /* This input is not shared. */
 153                 result = Bnet_BuildNodeBDD(dd,node,net->hash,
 154                                            option->locGlob,option->nodrop);
 155                 if (result == 0) return(0);
 156             } else {
 157                 if (node2->dd == NULL) return(0);
 158                 node->dd = node2->dd;
 159                 Cudd_Ref(node->dd);
 160                 node->var = node2->var;
 161                 node->active = node2->active;
 162             }
 163         }
 164         for (i = 0; i < net->nlatches; i++) {
 165             if (!st_lookup(net->hash,net->latches[i][1],&node)) {
 166                 return(0);
 167             }
 168             if (!st_lookup(net2->hash,net->latches[i][1],&node2)) {
 169                 /* This present state variable is not shared. */
 170                 result = Bnet_BuildNodeBDD(dd,node,net->hash,
 171                                            option->locGlob,option->nodrop);
 172                 if (result == 0) return(0);
 173             } else {
 174                 if (node2->dd == NULL) return(0);
 175                 node->dd = node2->dd;
 176                 Cudd_Ref(node->dd);
 177                 node->var = node2->var;
 178                 node->active = node2->active;
 179             }
 180         }
 181     } else {
 182         /* First assign variables to inputs if the order is provided.
 183         ** (Either in the .blif file or in an order file.)
 184         */
 185         if (option->ordering == PI_PS_FROM_FILE) {
 186             /* Follow order given in input file. First primary inputs
 187             ** and then present state variables.
 188             */
 189             for (i = 0; i < net->npis; i++) {
 190                 if (!st_lookup(net->hash,net->inputs[i],&node)) {
 191                     return(0);
 192                 }
 193                 result = Bnet_BuildNodeBDD(dd,node,net->hash,
 194                                            option->locGlob,option->nodrop);
 195                 if (result == 0) return(0);
 196             }
 197             for (i = 0; i < net->nlatches; i++) {
 198                 if (!st_lookup(net->hash,net->latches[i][1],&node)) {
 199                     return(0);
 200                 }
 201                 result = Bnet_BuildNodeBDD(dd,node,net->hash,
 202                                            option->locGlob,option->nodrop);
 203                 if (result == 0) return(0);
 204             }
 205         } else if (option->ordering == PI_PS_GIVEN) {
 206             result = Bnet_ReadOrder(dd,option->orderPiPs,net,option->locGlob,
 207                                     option->nodrop);
 208             if (result == 0) return(0);
 209         } else {
 210             result = Bnet_DfsVariableOrder(dd,net);
 211             if (result == 0) return(0);
 212         }
 213     }
 214     /* At this point the BDDs of all primary inputs and present state
 215     ** variables have been built. */
 216
 217     /* Currently noBuild doesn't do much. */
 218     if (option->noBuild == TRUE)
 219         return(1);
 220
 221     if (option->locGlob == BNET_LOCAL_DD) {
 222         node = net->nodes;
 223         while (node != NULL) {
 224             result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_LOCAL_DD,TRUE);
 225             if (result == 0) {
 226                 return(0);
 227             }
 228             if (pr > 2) {
 229                 (void) fprintf(stdout,"%s",node->name);
 230                 Cudd_PrintDebug(dd,node->dd,Cudd_ReadSize(dd),pr);
 231             }
 232             node = node->next;
 233         }
 234     } else { /* option->locGlob == BNET_GLOBAL_DD */
 235         /* Create BDDs with DFS from the primary outputs and the next
 236         ** state functions. If the inputs had not been ordered yet,
 237         ** this would result in a DFS order for the variables.
 238         */
 239
 240         ntrInitializeCount(net,option);
 241
 242         if (option->node != NULL &&
 243             option->closestCube == FALSE && option->dontcares == FALSE) {
 244             if (!st_lookup(net->hash,option->node,&node)) {
 245                 return(0);
 246             }
 247             result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
 248                                        option->nodrop);
 249             if (result == 0) return(0);
 250         } else {
 251             if (option->stateOnly == FALSE) {
 252                 for (i = 0; i < net->npos; i++) {
 253                     if (!st_lookup(net->hash,net->outputs[i],&node)) {
 254                         continue;
 255                     }
 256                     result = Bnet_BuildNodeBDD(dd,node,net->hash,
 257                                                BNET_GLOBAL_DD,option->nodrop);
 258                     if (result == 0) return(0);
 259                     if (option->progress)  {
 260                         (void) fprintf(stdout,"%s\n",node->name);
 261                     }
 262 #if 0
 263                     Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
 264 #endif
 265                 }
 266             }
 267             for (i = 0; i < net->nlatches; i++) {
 268                 if (!st_lookup(net->hash,net->latches[i][0],&node)) {
 269                     continue;
 270                 }
 271                 result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
 272                                            option->nodrop);
 273                 if (result == 0) return(0);
 274                 if (option->progress)  {
 275                     (void) fprintf(stdout,"%s\n",node->name);
 276                 }
 277 #if 0
 278                 Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
 279 #endif
 280             }
 281         }
 282         /* Make sure all inputs have a DD and dereference the DDs of
 283         ** the nodes that are not reachable from the outputs.
 284         */
 285         for (i = 0; i < net->npis; i++) {
 286             if (!st_lookup(net->hash,net->inputs[i],&node)) {
 287                 return(0);
 288             }
 289             result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
 290                                        option->nodrop);
 291             if (result == 0) return(0);
 292             if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
 293         }
 294         for (i = 0; i < net->nlatches; i++) {
 295             if (!st_lookup(net->hash,net->latches[i][1],&node)) {
 296                 return(0);
 297             }
 298             result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
 299                                        option->nodrop);
 300             if (result == 0) return(0);
 301             if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
 302         }
 303
 304         /* Dispose of the BDDs of the internal nodes if they have not
 305         ** been dropped already.
 306         */
 307         if (option->nodrop == TRUE) {
 308             for (node = net->nodes; node != NULL; node = node->next) {
 309                 if (node->dd != NULL && node->count != -1 &&
 310                     (node->type == BNET_INTERNAL_NODE ||
 311                     node->type == BNET_INPUT_NODE ||
 312                     node->type == BNET_PRESENT_STATE_NODE)) {
 313                     Cudd_RecursiveDeref(dd,node->dd);
 314                     if (node->type == BNET_INTERNAL_NODE) node->dd = NULL;
 315                 }
 316             }
 317         }
 318     }
 319
 320     return(1);
 321
 322 } /* end of buildDD */
 323
 324
 325 /**Function********************************************************************
 326
 327   Synopsis    [Builds the transition relation for a network.]
 328
 329   Description [Builds the transition relation for a network. Returns a
 330   pointer to the transition relation structure if successful; NULL
 331   otherwise.]
 332
 333   SideEffects [None]
 334
 335   SeeAlso     []
 336
 337 ******************************************************************************/
 338 NtrPartTR *
 339 Ntr_buildTR(
 340   DdManager * dd /* manager */,
 341   BnetNetwork * net /* network */,
 342   NtrOptions * option /* options */,
 343   int  image /* image type: monolithic ... */)
 344 {
 345     NtrPartTR *TR;
 346     DdNode *T, *delta, *support, *scan, *tmp, *preiabs, *prepabs;
 347     DdNode **part, **absicubes, **abspcubes, **nscube, *mnscube;
 348     DdNode **x, **y;
 349     DdNode **pi;
 350     int i;
 351     int xlevel;
 352     BnetNode *node;
 353     int *schedule;
 354     int depth = 0;
 355
 356     /* Initialize transition relation structure. */
 357     TR = ALLOC(NtrPartTR,1);
 358     if (TR == NULL) goto endgame;
 359     TR->nlatches = net->nlatches;
 360     if (image == NTR_IMAGE_MONO) {
 361         TR->nparts = 1;
 362     } else if (image == NTR_IMAGE_PART || image == NTR_IMAGE_CLIP ||
 363                image == NTR_IMAGE_DEPEND) {
 364         TR->nparts = net->nlatches;
 365     } else {
 366         (void) fprintf(stderr,"Unrecognized image method (%d). Using part.\n",
 367                        image);
 368         TR->nparts = net->nlatches;
 369     }
 370     TR->factors = Ntr_InitHeap(TR->nlatches);
 371     if (TR->factors == NULL) goto endgame;
 372     /* Allocate arrays for present state and next state variables. */
 373     TR->x = x = ALLOC(DdNode *,TR->nlatches);
 374     if (x == NULL) goto endgame;
 375     TR->y = y = ALLOC(DdNode *,TR->nlatches);
 376     if (y == NULL) goto endgame;
 377     /* Allocate array for primary input variables. */
 378     pi = ALLOC(DdNode *,net->npis);
 379     if (pi == NULL) goto endgame;
 380     /* Allocate array for partitioned transition relation. */
 381     part = ALLOC(DdNode *,net->nlatches);
 382     if (part == NULL) goto endgame;
 383     /* Allocate array of next state cubes. */
 384     nscube = ALLOC(DdNode *,net->nlatches);
 385     if (nscube == NULL) goto endgame;
 386     /* Allocate array for quantification schedule and initialize it. */
 387     schedule = ALLOC(int,Cudd_ReadSize(dd));
 388     if (schedule == NULL) goto endgame;
 389     for (i = 0; i < Cudd_ReadSize(dd); i++) {
 390         schedule[i] = -1;
 391     }
 392
 393     /* Create partitioned transition relation from network. */
 394     TR->xw = Cudd_ReadOne(dd);
 395     Cudd_Ref(TR->xw);
 396     for (i = 0; i < net->nlatches; i++) {
 397         if (!st_lookup(net->hash,net->latches[i][1],&node)) {
 398             goto endgame;
 399         }
 400         x[i] = node->dd;
 401         Cudd_Ref(x[i]);
 402         /* Add present state variable to cube TR->xw. */
 403         tmp = Cudd_bddAnd(dd,TR->xw,x[i]);
 404         if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
 405         Cudd_RecursiveDeref(dd,TR->xw);
 406         TR->xw = tmp;
 407         /* Create new y variable immediately above the x variable. */
 408         xlevel = Cudd_ReadPerm(dd,x[i]->index);
 409         y[i] = Cudd_bddNewVarAtLevel(dd,xlevel);
 410         Cudd_Ref(y[i]);
 411         /* Initialize cube of next state variables for this part. */
 412         nscube[i] = y[i];
 413         Cudd_Ref(nscube[i]);
 414         /* Group present and next state variable if so requested. */
 415         if (option->groupnsps != NTR_GROUP_NONE) {
 416             int method = option->groupnsps == NTR_GROUP_DEFAULT ?
 417                 MTR_DEFAULT : MTR_FIXED;
 418             if (Cudd_MakeTreeNode(dd,y[i]->index,2,method) == NULL)
 419                 goto endgame;
 420         }
 421         /* Get next state function and create transition relation part. */
 422         if (!st_lookup(net->hash,net->latches[i][0],&node)) {
 423             goto endgame;
 424         }
 425         delta = node->dd;
 426         if (image != NTR_IMAGE_DEPEND) {
 427             part[i] = Cudd_bddXnor(dd,delta,y[i]);
 428             if (part[i] == NULL) goto endgame;
 429         } else {
 430             part[i] = delta;
 431         }
 432         Cudd_Ref(part[i]);
 433         /* Collect scheduling info for this delta. At the end of this loop
 434         ** schedule[i] == j means that the variable of index i does not
 435         ** appear in any part with index greater than j, unless j == -1,
 436         ** in which case the variable appears in no part.
 437         */
 438         support = Cudd_Support(dd,delta);
 439         Cudd_Ref(support);
 440         scan = support;
 441         while (!Cudd_IsConstant(scan)) {
 442             schedule[scan->index] = i;
 443             scan = Cudd_T(scan);
 444         }
 445         Cudd_RecursiveDeref(dd,support);
 446     }
 447
 448     /* Collect primary inputs. */
 449     for (i = 0; i < net->npis; i++) {
 450         if (!st_lookup(net->hash,net->inputs[i],&node)) {
 451             goto endgame;
 452         }
 453         pi[i] = node->dd;
 454         tmp  = Cudd_bddAnd(dd,TR->xw,pi[i]);
 455         if (tmp == NULL) goto endgame; Cudd_Ref(tmp);
 456         Cudd_RecursiveDeref(dd,TR->xw);
 457         TR->xw = tmp;
 458     }
 459
 460     /* Build abstraction cubes. First primary input variables that go
 461     ** in the abstraction cubes for both monolithic and partitioned
 462     ** transition relations. */
 463     absicubes = ALLOC(DdNode *, net->nlatches);
 464     if (absicubes == NULL) goto endgame;
 465     abspcubes = ALLOC(DdNode *, net->nlatches);
 466     if (abspcubes == NULL) goto endgame;
 467
 468     for (i = 0; i < net->nlatches; i++) {
 469         absicubes[i] = Cudd_ReadOne(dd);
 470         Cudd_Ref(absicubes[i]);
 471     }
 472     preiabs = Cudd_ReadOne(dd);
 473     Cudd_Ref(preiabs);
 474
 475     for (i = 0; i < net->npis; i++) {
 476         int j = pi[i]->index;
 477         int k = schedule[j];
 478         if (k >= 0) {
 479             tmp = Cudd_bddAnd(dd,absicubes[k],pi[i]);
 480             if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
 481             Cudd_RecursiveDeref(dd,absicubes[k]);
 482             absicubes[k] = tmp;
 483         } else {
 484             tmp = Cudd_bddAnd(dd,preiabs,pi[i]);
 485             if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
 486             Cudd_RecursiveDeref(dd,preiabs);
 487             preiabs = tmp;
 488         }
 489     }
 490     FREE(pi);
 491
 492     /* Build preimage abstraction cubes from image abstraction cubes. */
 493     for (i = 0; i < net->nlatches; i++) {
 494         abspcubes[i] = Cudd_bddAnd(dd,absicubes[i],nscube[i]);
 495         if (abspcubes[i] == NULL) return(NULL);
 496         Cudd_Ref(abspcubes[i]);
 497     }
 498     Cudd_Ref(prepabs = preiabs);
 499
 500     /* For partitioned transition relations we add present state variables
 501     ** to the image abstraction cubes. */
 502     if (image != NTR_IMAGE_MONO) {
 503         for (i = 0; i < net->nlatches; i++) {
 504             int j = x[i]->index;
 505             int k = schedule[j];
 506             if (k >= 0) {
 507                 tmp = Cudd_bddAnd(dd,absicubes[k],x[i]);
 508                 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
 509                 Cudd_RecursiveDeref(dd,absicubes[k]);
 510                 absicubes[k] = tmp;
 511             } else {
 512                 tmp = Cudd_bddAnd(dd,preiabs,x[i]);
 513                 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
 514                 Cudd_RecursiveDeref(dd,preiabs);
 515                 preiabs = tmp;
 516             }
 517         }
 518     }
 519     FREE(schedule);
 520
 521     if (image != NTR_IMAGE_MONO) {
 522         TR->part = part;
 523         TR->icube = absicubes;
 524         TR->pcube = abspcubes;
 525         TR->nscube = nscube;
 526         TR->preiabs = preiabs;
 527         TR->prepabs = prepabs;
 528         return(TR);
 529     }
 530
 531     /* Here we are building a monolithic TR. */
 532
 533     /* Reinitialize the cube of variables to be quantified before
 534     ** image computation. */
 535     Cudd_RecursiveDeref(dd,preiabs);
 536     preiabs = Cudd_ReadOne(dd);
 537     Cudd_Ref(preiabs);
 538
 539     if (option->imageClip != 1.0) {
 540         depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
 541     }
 542
 543     /* Collapse transition relation. */
 544     T = Cudd_ReadOne(dd);
 545     Cudd_Ref(T);
 546     mnscube = Cudd_ReadOne(dd);
 547     Cudd_Ref(mnscube);
 548     for (i = 0; i < net->nlatches; i++) {
 549         /* Eliminate the primary inputs that do not appear in other parts. */
 550         if (depth != 0) {
 551             tmp = Cudd_bddClippingAndAbstract(dd,T,part[i],absicubes[i],
 552                                               depth,option->approx);
 553         } else {
 554             tmp = Cudd_bddAndAbstract(dd,T,part[i],absicubes[i]);
 555         }
 556         Cudd_Ref(tmp);
 557         Cudd_RecursiveDeref(dd,T);
 558         Cudd_RecursiveDeref(dd,part[i]);
 559         Cudd_RecursiveDeref(dd,absicubes[i]);
 560         Cudd_RecursiveDeref(dd,abspcubes[i]);
 561         if (option->threshold >= 0) {
 562             if (option->approx) {
 563                 T = Cudd_RemapOverApprox(dd,tmp,2*net->nlatches,
 564                                          option->threshold,option->quality);
 565             } else {
 566                 T = Cudd_RemapUnderApprox(dd,tmp,2*net->nlatches,
 567                                           option->threshold,option->quality);
 568             }
 569         } else {
 570             T = tmp;
 571         }
 572         if (T == NULL) return(NULL);
 573         Cudd_Ref(T);
 574         Cudd_RecursiveDeref(dd,tmp);
 575         /* Add the next state variables of this part to the cube of all
 576         ** next state variables. */
 577         tmp = Cudd_bddAnd(dd,mnscube,nscube[i]);
 578         if (tmp == NULL) return(NULL);
 579         Cudd_Ref(tmp);
 580         Cudd_RecursiveDeref(dd,mnscube);
 581         mnscube = tmp;
 582         Cudd_RecursiveDeref(dd,nscube[i]);
 583         (void) printf("@"); fflush(stdout);
 584     }
 585     (void) printf("\n");
 586 #if 0
 587     (void) printf("T"); Cudd_PrintDebug(dd,T,2*net->nlatches,2);
 588 #endif
 589
 590     /* Clean up. */
 591     FREE(absicubes);
 592     FREE(abspcubes);
 593     FREE(part);
 594     FREE(nscube);
 595
 596     TR->part = part = ALLOC(DdNode *,1);
 597     if (part == NULL) goto endgame;
 598     part[0] = T;
 599
 600     /* Build cube of x (present state) variables for abstraction. */
 601     TR->icube = absicubes = ALLOC(DdNode *,1);
 602     if (absicubes == NULL) goto endgame;
 603     absicubes[0] = makecube(dd,x,TR->nlatches);
 604     if (absicubes[0] == NULL) return(0);
 605     Cudd_Ref(absicubes[0]);
 606     /* Build cube of y (next state) variables for abstraction. */
 607     TR->pcube = abspcubes = ALLOC(DdNode *,1);
 608     if (abspcubes == NULL) goto endgame;
 609     abspcubes[0] = makecube(dd,y,TR->nlatches);
 610     if (abspcubes[0] == NULL) return(0);
 611     Cudd_Ref(abspcubes[0]);
 612     TR->preiabs = preiabs;
 613     TR->prepabs = prepabs;
 614
 615     TR->nscube = ALLOC(DdNode *,1);
 616     if (TR->nscube == NULL) return(NULL);
 617     TR->nscube[0] = mnscube;
 618
 619     return(TR);
 620
 621 endgame:
 622
 623     return(NULL);
 624
 625 } /* end of Ntr_buildTR */
 626
 627
 628 /**Function********************************************************************
 629
 630   Synopsis    [Frees the transition relation for a network.]
 631
 632   Description []
 633
 634   SideEffects [None]
 635
 636   SeeAlso     []
 637
 638 ******************************************************************************/
 639 void
 640 Ntr_freeTR(
 641   DdManager * dd,
 642   NtrPartTR * TR)
 643 {
 644     int i;
 645     for (i = 0; i < TR->nlatches; i++) {
 646         Cudd_RecursiveDeref(dd,TR->x[i]);
 647         Cudd_RecursiveDeref(dd,TR->y[i]);
 648     }
 649     FREE(TR->x);
 650     FREE(TR->y);
 651     for (i = 0; i < TR->nparts; i++) {
 652         Cudd_RecursiveDeref(dd,TR->part[i]);
 653         Cudd_RecursiveDeref(dd,TR->icube[i]);
 654         Cudd_RecursiveDeref(dd,TR->pcube[i]);
 655         Cudd_RecursiveDeref(dd,TR->nscube[i]);
 656     }
 657     FREE(TR->part);
 658     FREE(TR->icube);
 659     FREE(TR->pcube);
 660     FREE(TR->nscube);
 661     Cudd_RecursiveDeref(dd,TR->preiabs);
 662     Cudd_RecursiveDeref(dd,TR->prepabs);
 663     Cudd_RecursiveDeref(dd,TR->xw);
 664     for (i = 0; i < TR->factors->nslots; i++) {
 665         Cudd_RecursiveDeref(dd, (DdNode *) TR->factors->slots[i].item);
 666     }
 667     Ntr_FreeHeap(TR->factors);
 668     FREE(TR);
 669
 670     return;
 671
 672 } /* end of Ntr_freeTR */
 673
 674
 675 /**Function********************************************************************
 676
 677   Synopsis    [Makes a copy of a transition relation.]
 678
 679   Description [Makes a copy of a transition relation. Returns a pointer
 680   to the copy if successful; NULL otherwise.]
 681
 682   SideEffects [None]
 683
 684   SeeAlso     [Ntr_buildTR Ntr_freeTR]
 685
 686 ******************************************************************************/
 687 NtrPartTR *
 688 Ntr_cloneTR(
 689   NtrPartTR *TR)
 690 {
 691     NtrPartTR *T;
 692     int nparts, nlatches, i;
 693
 694     T = ALLOC(NtrPartTR,1);
 695     if (T == NULL) return(NULL);
 696     nparts = T->nparts = TR->nparts;
 697     nlatches = T->nlatches = TR->nlatches;
 698     T->part = ALLOC(DdNode *,nparts);
 699     if (T->part == NULL) {
 700         FREE(T);
 701         return(NULL);
 702     }
 703     T->icube = ALLOC(DdNode *,nparts);
 704     if (T->icube == NULL) {
 705         FREE(T->part);
 706         FREE(T);
 707         return(NULL);
 708     }
 709     T->pcube = ALLOC(DdNode *,nparts);
 710     if (T->pcube == NULL) {
 711         FREE(T->icube);
 712         FREE(T->part);
 713         FREE(T);
 714         return(NULL);
 715     }
 716     T->x = ALLOC(DdNode *,nlatches);
 717     if (T->x == NULL) {
 718         FREE(T->pcube);
 719         FREE(T->icube);
 720         FREE(T->part);
 721         FREE(T);
 722         return(NULL);
 723     }
 724     T->y = ALLOC(DdNode *,nlatches);
 725     if (T->y == NULL) {
 726         FREE(T->x);
 727         FREE(T->pcube);
 728         FREE(T->icube);
 729         FREE(T->part);
 730         FREE(T);
 731         return(NULL);
 732     }
 733     T->nscube = ALLOC(DdNode *,nparts);
 734     if (T->nscube == NULL) {
 735         FREE(T->y);
 736         FREE(T->x);
 737         FREE(T->pcube);
 738         FREE(T->icube);
 739         FREE(T->part);
 740         FREE(T);
 741         return(NULL);
 742     }
 743     T->factors = Ntr_HeapClone(TR->factors);
 744     if (T->factors == NULL) {
 745         FREE(T->nscube);
 746         FREE(T->y);
 747         FREE(T->x);
 748         FREE(T->pcube);
 749         FREE(T->icube);
 750         FREE(T->part);
 751         FREE(T);
 752         return(NULL);
 753     }
 754     for (i = 0; i < T->factors->nslots; i++) {
 755         Cudd_Ref((DdNode *) T->factors->slots[i].item);
 756     }
 757     for (i = 0; i < nparts; i++) {
 758         T->part[i] = TR->part[i];
 759         Cudd_Ref(T->part[i]);
 760         T->icube[i] = TR->icube[i];
 761         Cudd_Ref(T->icube[i]);
 762         T->pcube[i] = TR->pcube[i];
 763         Cudd_Ref(T->pcube[i]);
 764         T->nscube[i] = TR->nscube[i];
 765         Cudd_Ref(T->nscube[i]);
 766     }
 767     T->preiabs = TR->preiabs;
 768     Cudd_Ref(T->preiabs);
 769     T->prepabs = TR->prepabs;
 770     Cudd_Ref(T->prepabs);
 771     T->xw = TR->xw;
 772     Cudd_Ref(T->xw);
 773     for (i = 0; i < nlatches; i++) {
 774         T->x[i] = TR->x[i];
 775         Cudd_Ref(T->x[i]);
 776         T->y[i] = TR->y[i];
 777         Cudd_Ref(T->y[i]);
 778     }
 779
 780     return(T);
 781
 782 } /* end of Ntr_cloneTR */
 783
 784
 785 /**Function********************************************************************
 786
 787   Synopsis    [Poor man's traversal procedure.]
 788
 789   Description [Poor man's traversal procedure. based on the monolithic
 790   transition relation.  Returns 1 in case of success; 0 otherwise.]
 791
 792   SideEffects [None]
 793
 794   SeeAlso     [Ntr_ClosureTrav]
 795
 796 ******************************************************************************/
 797 int
 798 Ntr_Trav(
 799   DdManager * dd /* DD manager */,
 800   BnetNetwork * net /* network */,
 801   NtrOptions * option /* options */)
 802 {
 803     NtrPartTR *TR;              /* Transition relation */
 804     DdNode *init;               /* initial state(s) */
 805     DdNode *from;
 806     DdNode *to;
 807     DdNode *reached;
 808     DdNode *neW;
 809     DdNode *one, *zero;
 810     int depth;
 811     int retval;
 812     int pr = option->verb;
 813     int initReord = Cudd_ReadReorderings(dd);
 814
 815     if (option->traverse == FALSE || net->nlatches == 0) return(1);
 816     (void) printf("Building transition relation. Time = %s\n",
 817                   util_print_time(util_cpu_time() - option->initialTime));
 818     one = Cudd_ReadOne(dd);
 819     zero = Cudd_Not(one);
 820
 821     /* Build transition relation and initial states. */
 822     TR = Ntr_buildTR(dd,net,option,option->image);
 823     if (TR == NULL) return(0);
 824     retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
 825     (void) printf("Transition relation: %d parts %d latches %d nodes\n",
 826                   TR->nparts, TR->nlatches,
 827                   Cudd_SharingSize(TR->part, TR->nparts));
 828     (void) printf("Traversing. Time = %s\n",
 829                   util_print_time(util_cpu_time() - option->initialTime));
 830     init = Ntr_initState(dd,net,option);
 831     if (init == NULL) return(0);
 832
 833     /* Initialize From. */
 834     Cudd_Ref(from = init);
 835     (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
 836
 837     /* Initialize Reached. */
 838     Cudd_Ref(reached = from);
 839
 840     /* Start traversal. */
 841     for (depth = 0; ; depth++) {
 842         /* Image computation. */
 843         to = ntrImage(dd,TR,from,option);
 844         if (to == NULL) {
 845             Cudd_RecursiveDeref(dd,reached);
 846             Cudd_RecursiveDeref(dd,from);
 847             return(0);
 848         }
 849         Cudd_RecursiveDeref(dd,from);
 850
 851         /* Find new states. */
 852         neW = Cudd_bddAnd(dd,to,Cudd_Not(reached));
 853         if (neW == NULL) {
 854             Cudd_RecursiveDeref(dd,reached);
 855             Cudd_RecursiveDeref(dd,to);
 856             return(0);
 857         }
 858         Cudd_Ref(neW);
 859         Cudd_RecursiveDeref(dd,to);
 860
 861         /* Check for convergence. */
 862         if (neW == zero) break;
 863
 864         /* Dump current reached states if requested. */
 865         if (option->store == depth) {
 866             int ok = Dddmp_cuddBddStore(dd, NULL, reached, NULL,
 867                                         NULL, DDDMP_MODE_TEXT, DDDMP_VARIDS,
 868                                         option->storefile, NULL);
 869             if (ok == 0) return(0);
 870             (void) printf("Storing reached in %s after %i iterations.\n",
 871                           option->storefile, depth);
 872             break;
 873         }
 874
 875         /* Update reached. */
 876         reached = ntrUpdateReached(dd,reached,neW);
 877         if (reached == NULL) {
 878             Cudd_RecursiveDeref(dd,neW);
 879             return(0);
 880         }
 881
 882         /* Prepare for new iteration. */
 883         from = ntrChooseFrom(dd,neW,reached,option);
 884         if (from == NULL) {
 885             Cudd_RecursiveDeref(dd,reached);
 886             Cudd_RecursiveDeref(dd,neW);
 887             return(0);
 888         }
 889         Cudd_RecursiveDeref(dd,neW);
 890         (void) printf("From[%d]",depth+1);
 891         Cudd_PrintDebug(dd,from,TR->nlatches,pr);
 892         (void) printf("Reached[%d]",depth+1);
 893         Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
 894         if (pr > 0) {
 895             if (!Cudd_ApaPrintMinterm(stdout, dd, reached, TR->nlatches))
 896                 return(0);
 897             if (!Cudd_ApaPrintMintermExp(stdout, dd, reached, TR->nlatches, 6))
 898                 return(0);
 899         } else {
 900             (void) printf("\n");
 901         }
 902     }
 903
 904     /* Print out result. */
 905     (void) printf("depth = %d\n", depth);
 906     (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
 907
 908     /* Dump to file if requested. */
 909     if (option->bdddump) {
 910         DdNode *dfunc[2];       /* addresses of the functions to be dumped */
 911         char *onames[2];        /* names of the functions to be dumped */
 912         dfunc[0] = TR->part[0];         onames[0] = (char *) "T";
 913         dfunc[1] = reached;             onames[1] = (char *) "R";
 914         retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
 915                                    onames, 2, option->dumpFmt);
 916         if (retval == 0) return(0);
 917     }
 918
 919     if (option->depend) {
 920         retval = ntrLatchDependencies(dd, reached, net, option);
 921         if (retval == -1) return(0);
 922         (void) printf("%d latches are redundant\n", retval);
 923     }
 924     /* Clean up. */
 925     Cudd_RecursiveDeref(dd,reached);
 926     Cudd_RecursiveDeref(dd,neW);
 927     Cudd_RecursiveDeref(dd,init);
 928     Ntr_freeTR(dd,TR);
 929
 930     if (Cudd_ReadReorderings(dd) > initReord) {
 931         (void) printf("Order at the end of reachability analysis\n");
 932         retval = Bnet_PrintOrder(net,dd);
 933         if (retval == 0) return(0);
 934     }
 935     return(1);
 936
 937 } /* end of Ntr_Trav */
 938
 939
 940 /**Function********************************************************************
 941
 942   Synopsis    [Computes the SCCs of the STG.]
 943
 944   Description [Computes the strongly connected components of the state
 945   transition graph.  Only the first 10 SCCs are computed. Returns 1 in
 946   case of success; 0 otherwise.]
 947
 948   SideEffects [None]
 949
 950   SeeAlso     [Ntr_Trav]
 951
 952 ******************************************************************************/
 953 int
 954 Ntr_SCC(
 955   DdManager * dd /* DD manager */,
 956   BnetNetwork * net /* network */,
 957   NtrOptions * option /* options */)
 958 {
 959     NtrPartTR *TR;              /* Transition relation */
 960     DdNode *init;               /* initial state(s) */
 961     DdNode *from;
 962     DdNode *to;
 963     DdNode *reached, *reaching;
 964     DdNode *neW;
 965     DdNode *one, *zero;
 966     DdNode *states, *scc;
 967     DdNode *tmp;
 968     DdNode *SCCs[10];
 969     int depth;
 970     int nscc = 0;
 971     int retval;
 972     int pr = option->verb;
 973     int i;
 974
 975     if (option->scc == FALSE || net->nlatches == 0) return(1);
 976     (void) printf("Building transition relation. Time = %s\n",
 977                   util_print_time(util_cpu_time() - option->initialTime));
 978     one = Cudd_ReadOne(dd);
 979     zero = Cudd_Not(one);
 980
 981     /* Build transition relation and initial states. */
 982     TR = Ntr_buildTR(dd,net,option,option->image);
 983     if (TR == NULL) return(0);
 984     retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
 985     (void) printf("Transition relation: %d parts %d latches %d nodes\n",
 986                   TR->nparts, TR->nlatches,
 987                   Cudd_SharingSize(TR->part, TR->nparts));
 988     (void) printf("Computing SCCs. Time = %s\n",
 989                   util_print_time(util_cpu_time() - option->initialTime));
 990
 991     /* Consider all SCCs, including those not reachable. */
 992     states = one;
 993     Cudd_Ref(states);
 994
 995     while (states != zero) {
 996         if (nscc == 0) {
 997             tmp = Ntr_initState(dd,net,option);
 998             if (tmp == NULL) return(0);
 999             init = Cudd_bddPickOneMinterm(dd,tmp,TR->x,TR->nlatches);
1000         } else {
1001             init = Cudd_bddPickOneMinterm(dd,states,TR->x,TR->nlatches);
1002         }
1003         if (init == NULL) return(0);
1004         Cudd_Ref(init);
1005         if (nscc == 0) {
1006             Cudd_RecursiveDeref(dd,tmp);
1007         }
1008         /* Initialize From. */
1009         Cudd_Ref(from = init);
1010         (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1011
1012         /* Initialize Reached. */
1013         Cudd_Ref(reached = from);
1014
1015         /* Start forward traversal. */
1016         for (depth = 0; ; depth++) {
1017             /* Image computation. */
1018             to = ntrImage(dd,TR,from,option);
1019             if (to == NULL) {
1020                 return(0);
1021             }
1022             Cudd_RecursiveDeref(dd,from);
1023
1024             /* Find new states. */
1025             tmp = Cudd_bddAnd(dd,to,states);
1026             if (tmp == NULL) return(0); Cudd_Ref(tmp);
1027             Cudd_RecursiveDeref(dd,to);
1028             neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reached));
1029             if (neW == NULL) return(0); Cudd_Ref(neW);
1030             Cudd_RecursiveDeref(dd,tmp);
1031
1032             /* Check for convergence. */
1033             if (neW == zero) break;
1034
1035             /* Update reached. */
1036             reached = ntrUpdateReached(dd,reached,neW);
1037             if (reached == NULL) {
1038                 return(0);
1039             }
1040
1041             /* Prepare for new iteration. */
1042             from = ntrChooseFrom(dd,neW,reached,option);
1043             if (from == NULL) {
1044                 return(0);
1045             }
1046             Cudd_RecursiveDeref(dd,neW);
1047             (void) printf("From[%d]",depth+1);
1048             Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1049             (void) printf("Reached[%d]",depth+1);
1050             Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1051             if (pr <= 0) {
1052                 (void) printf("\n");
1053             }
1054         }
1055         Cudd_RecursiveDeref(dd,neW);
1056
1057         /* Express reached in terms of y variables. This allows us to
1058         ** efficiently test for termination during the backward traversal. */
1059         tmp = Cudd_bddVarMap(dd,reached);
1060         if (tmp == NULL) return(0);
1061         Cudd_Ref(tmp);
1062         Cudd_RecursiveDeref(dd,reached);
1063         reached = tmp;
1064
1065         /* Initialize from and reaching. */
1066         from = Cudd_bddVarMap(dd,init);
1067         Cudd_Ref(from);
1068         (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1069         Cudd_Ref(reaching = from);
1070
1071         /* Start backward traversal. */
1072         for (depth = 0; ; depth++) {
1073             /* Preimage computation. */
1074             to = ntrPreimage(dd,TR,from);
1075             if (to == NULL) {
1076                 return(0);
1077             }
1078             Cudd_RecursiveDeref(dd,from);
1079
1080             /* Find new states. */
1081             tmp = Cudd_bddAnd(dd,to,reached);
1082             if (tmp == NULL) return(0); Cudd_Ref(tmp);
1083             Cudd_RecursiveDeref(dd,to);
1084             neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reaching));
1085             if (neW == NULL) return(0); Cudd_Ref(neW);
1086             Cudd_RecursiveDeref(dd,tmp);
1087
1088             /* Check for convergence. */
1089             if (neW == zero) break;
1090
1091             /* Update reaching. */
1092             reaching = ntrUpdateReached(dd,reaching,neW);
1093             if (reaching == NULL) {
1094                 return(0);
1095             }
1096
1097             /* Prepare for new iteration. */
1098             from = ntrChooseFrom(dd,neW,reaching,option);
1099             if (from == NULL) {
1100                 return(0);
1101             }
1102             Cudd_RecursiveDeref(dd,neW);
1103             (void) printf("From[%d]",depth+1);
1104             Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1105             (void) printf("Reaching[%d]",depth+1);
1106             Cudd_PrintDebug(dd,reaching,TR->nlatches,pr);
1107             if (pr <= 0) {
1108                 (void) printf("\n");
1109             }
1110         }
1111
1112         scc = Cudd_bddAnd(dd,reached,reaching);
1113         if (scc == NULL) {
1114             return(0);
1115         }
1116         Cudd_Ref(scc);
1117         SCCs[nscc] = Cudd_bddVarMap(dd,scc);
1118         if (SCCs[nscc] == NULL) return(0);
1119         Cudd_Ref(SCCs[nscc]);
1120         Cudd_RecursiveDeref(dd,scc);
1121         /* Print out result. */
1122         (void) printf("SCC[%d]",nscc);
1123         Cudd_PrintDebug(dd,SCCs[nscc],TR->nlatches,pr);
1124         tmp = Cudd_bddAnd(dd,states,Cudd_Not(SCCs[nscc]));
1125         if (tmp == NULL) {
1126             return(0);
1127         }
1128         Cudd_Ref(tmp);
1129         Cudd_RecursiveDeref(dd,states);
1130         states = tmp;
1131         Cudd_RecursiveDeref(dd,reached);
1132         Cudd_RecursiveDeref(dd,reaching);
1133         Cudd_RecursiveDeref(dd,neW);
1134         Cudd_RecursiveDeref(dd,init);
1135         nscc++;
1136         if (nscc > 9) break;
1137     }
1138
1139     if (states != zero) {
1140         (void) fprintf(stdout,"More than 10 SCCs. Only the first 10 are computed.\n");
1141     }
1142
1143     /* Dump to file if requested. */
1144     if (option->bdddump) {
1145         char *sccnames[10];     /* names of the SCCs */
1146         sccnames[0] = (char *) "SCC0";
1147         sccnames[1] = (char *) "SCC1";
1148         sccnames[2] = (char *) "SCC2";
1149         sccnames[3] = (char *) "SCC3";
1150         sccnames[4] = (char *) "SCC4";
1151         sccnames[5] = (char *) "SCC5";
1152         sccnames[6] = (char *) "SCC6";
1153         sccnames[7] = (char *) "SCC7";
1154         sccnames[8] = (char *) "SCC8";
1155         sccnames[9] = (char *) "SCC9";
1156         retval = Bnet_bddArrayDump(dd, net, option->dumpfile, SCCs,
1157                                    sccnames, nscc, option->dumpFmt);
1158         if (retval == 0) return(0);
1159     }
1160
1161     /* Verify that the SCCs form a partition of the universe. */
1162     scc = zero;
1163     Cudd_Ref(scc);
1164     for (i = 0; i < nscc; i++) {
1165         assert(Cudd_bddLeq(dd,SCCs[i],Cudd_Not(scc)));
1166         tmp = Cudd_bddOr(dd,SCCs[i],scc);
1167         if (tmp == NULL) return(0);
1168         Cudd_Ref(tmp);
1169         Cudd_RecursiveDeref(dd,scc);
1170         scc = tmp;
1171         Cudd_RecursiveDeref(dd,SCCs[i]);
1172     }
1173     assert(scc == Cudd_Not(states));
1174
1175     /* Clean up. */
1176     Cudd_RecursiveDeref(dd,scc);
1177     Cudd_RecursiveDeref(dd,states);
1178     Ntr_freeTR(dd,TR);
1179
1180     return(1);
1181
1182 } /* end of Ntr_SCC */
1183
1184
1185 /**Function********************************************************************
1186
1187   Synopsis    [Transitive closure traversal procedure.]
1188
1189   Description [Traversal procedure. based on the transitive closure of the
1190   transition relation.  Returns 1 in case of success; 0 otherwise.]
1191
1192   SideEffects [None]
1193
1194   SeeAlso     [Ntr_Trav]
1195
1196 ******************************************************************************/
1197 int
1198 Ntr_ClosureTrav(
1199   DdManager * dd /* DD manager */,
1200   BnetNetwork * net /* network */,
1201   NtrOptions * option /* options */)
1202 {
1203     DdNode *init;
1204     DdNode *T;
1205     NtrPartTR *TR;
1206     int retval;
1207     int pr = option->verb;      /* verbosity level */
1208     DdNode *dfunc[2];           /* addresses of the functions to be dumped */
1209     char *onames[2];            /* names of the functions to be dumped */
1210     DdNode *reached, *reachedy, *reachedx;
1211
1212     /* Traverse if requested and if the circuit is sequential. */
1213     if (option->closure == FALSE || net->nlatches == 0) return(1);
1214
1215     TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1216     if (TR == NULL) return(0);
1217     (void) printf("TR"); Cudd_PrintDebug(dd,TR->part[0],2*TR->nlatches,pr);
1218     T = Ntr_TransitiveClosure(dd,TR,option);
1219     if (T == NULL) return(0);
1220     Cudd_Ref(T);
1221     (void) printf("TC"); Cudd_PrintDebug(dd,T,2*TR->nlatches,pr);
1222
1223     init = Ntr_initState(dd,net,option);
1224     if (init == NULL) return(0);
1225     (void) printf("S0"); Cudd_PrintDebug(dd,init,TR->nlatches,pr);
1226
1227     /* Image computation. */
1228     if (option->closureClip != 1.0) {
1229         int depth = (int) ((double) Cudd_ReadSize(dd) * option->closureClip);
1230         reachedy = Cudd_bddClippingAndAbstract(dd,T,init,TR->icube[0],
1231                                                depth,option->approx);
1232     } else {
1233         reachedy = Cudd_bddAndAbstract(dd,T,init,TR->icube[0]);
1234     }
1235     if (reachedy == NULL) return(0);
1236     Cudd_Ref(reachedy);
1237
1238     /* Express in terms of present state variables. */
1239     reachedx = Cudd_bddSwapVariables(dd,reachedy,TR->x,TR->y,TR->nlatches);
1240     if (reachedx == NULL) return(0);
1241     Cudd_Ref(reachedx);
1242     Cudd_RecursiveDeref(dd,reachedy);
1243
1244     /* Add initial state. */
1245     reached = Cudd_bddOr(dd,reachedx,init);
1246     if (reached == NULL) return(0);
1247     Cudd_Ref(reached);
1248     Cudd_RecursiveDeref(dd,reachedx);
1249
1250     /* Print out result. */
1251     (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1252
1253     /* Dump to file if requested. */
1254     if (option->bdddump) {
1255         dfunc[0] = T;           onames[0] = (char *) "TC";
1256         dfunc[1] = reached;     onames[1] = (char *) "R";
1257         retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
1258                                    onames, 2, option->dumpFmt);
1259         if (retval == 0) return(0);
1260     }
1261
1262     /* Clean up. */
1263     Cudd_RecursiveDeref(dd,reached);
1264     Cudd_RecursiveDeref(dd,init);
1265     Cudd_RecursiveDeref(dd,T);
1266     Ntr_freeTR(dd,TR);
1267
1268     return(1);
1269
1270 } /* end of Ntr_ClosureTrav */
1271
1272
1273 /**Function********************************************************************
1274
1275   Synopsis    [Builds the transitive closure of a transition relation.]
1276
1277   Description [Builds the transitive closure of a transition relation.
1278   Returns a BDD if successful; NULL otherwise. Uses a simple squaring
1279   algorithm.]
1280
1281   SideEffects [None]
1282
1283   SeeAlso     []
1284
1285 ******************************************************************************/
1286 DdNode *
1287 Ntr_TransitiveClosure(
1288   DdManager * dd,
1289   NtrPartTR * TR,
1290   NtrOptions * option)
1291 {
1292     DdNode *T,*oldT,*Txz,*Tzy,*Tred,*square,*zcube;
1293     DdNode **z;
1294     int i;
1295     int depth = 0;
1296     int ylevel;
1297     int done;
1298
1299     if (option->image != NTR_IMAGE_MONO) return(NULL);
1300
1301     /* Create array of auxiliary variables. */
1302     z = ALLOC(DdNode *,TR->nlatches);
1303     if (z == NULL)
1304         return(NULL);
1305     for (i = 0; i < TR->nlatches; i++) {
1306         ylevel = Cudd_ReadIndex(dd,TR->y[i]->index);
1307         z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1308         if (z[i] == NULL)
1309             return(NULL);
1310     }
1311     /* Build cube of auxiliary variables. */
1312     zcube = makecube(dd,z,TR->nlatches);
1313     if (zcube == NULL) return(NULL);
1314     Cudd_Ref(zcube);
1315
1316     if (option->closureClip != 1.0) {
1317         depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1318     }
1319
1320     T = TR->part[0];
1321     Cudd_Ref(T);
1322     for (i = 0; ; i++) {
1323         if (option->threshold >= 0) {
1324             if (option->approx) {
1325                 Tred = Cudd_RemapOverApprox(dd,T,TR->nlatches*2,
1326                                             option->threshold,
1327                                             option->quality);
1328             } else {
1329                 Tred = Cudd_RemapUnderApprox(dd,T,TR->nlatches*2,
1330                                              option->threshold,
1331                                              option->quality);
1332             }
1333         } else {
1334             Tred = T;
1335         }
1336         if (Tred == NULL) return(NULL);
1337         Cudd_Ref(Tred);
1338         /* Express T in terms of z and y variables. */
1339         Tzy = Cudd_bddSwapVariables(dd,Tred,TR->x,z,TR->nlatches);
1340         if (Tzy == NULL) return(NULL);
1341         Cudd_Ref(Tzy);
1342         /* Express T in terms of x and z variables. */
1343         Txz = Cudd_bddSwapVariables(dd,Tred,TR->y,z,TR->nlatches);
1344         if (Txz == NULL) return(NULL);
1345         Cudd_Ref(Txz);
1346         Cudd_RecursiveDeref(dd,Tred);
1347         /* Square */
1348         if (depth == 0) {
1349             square = Cudd_bddAndAbstract(dd,Txz,Tzy,zcube);
1350         } else {
1351             square = Cudd_bddClippingAndAbstract(dd,Txz,Tzy,zcube,depth,
1352                                                  option->approx);
1353         }
1354         if (square == NULL) return(NULL);
1355         Cudd_Ref(square);
1356         Cudd_RecursiveDeref(dd,Tzy);
1357         Cudd_RecursiveDeref(dd,Txz);
1358         oldT = T;
1359         T = Cudd_bddOr(dd,square,TR->part[0]);
1360         if (T == NULL) return(NULL);
1361         Cudd_Ref(T);
1362         Cudd_RecursiveDeref(dd,square);
1363         done = T == oldT;
1364         Cudd_RecursiveDeref(dd,oldT);
1365         if (done) break;
1366         (void) fprintf(stdout,"@"); fflush(stdout);
1367     }
1368     (void) fprintf(stdout, "\n");
1369
1370     Cudd_RecursiveDeref(dd,zcube);
1371     Cudd_Deref(T);
1372     FREE(z);
1373     return(T);
1374
1375 } /* end of Ntr_TransitiveClosure */
1376
1377
1378 /**Function********************************************************************
1379
1380   Synopsis    [Builds the BDD of the initial state(s).]
1381
1382   Description [Builds the BDD of the initial state(s).  Returns a BDD
1383   if successful; NULL otherwise.]
1384
1385   SideEffects [None]
1386
1387   SeeAlso     []
1388
1389 ******************************************************************************/
1390 DdNode *
1391 Ntr_initState(
1392   DdManager * dd,
1393   BnetNetwork * net,
1394   NtrOptions * option)
1395 {
1396     DdNode *res, *x, *w, *one;
1397     BnetNode *node;
1398     int i;
1399
1400     if (option->load) {
1401         res = Dddmp_cuddBddLoad(dd, DDDMP_VAR_MATCHIDS, NULL, NULL, NULL,
1402                                 DDDMP_MODE_DEFAULT, option->loadfile, NULL);
1403     } else {
1404         one = Cudd_ReadOne(dd);
1405         Cudd_Ref(res = one);
1406
1407         if (net->nlatches == 0) return(res);
1408
1409         for (i = 0; i < net->nlatches; i++) {
1410             if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1411                 goto endgame;
1412             }
1413             x = node->dd;
1414             switch (net->latches[i][2][0]) {
1415             case '0':
1416                 w = Cudd_bddAnd(dd,res,Cudd_Not(x));
1417                 break;
1418             case '1':
1419                 w = Cudd_bddAnd(dd,res,x);
1420                 break;
1421             default: /* don't care */
1422                 w = res;
1423                 break;
1424             }
1425
1426             if (w == NULL) {
1427                 Cudd_RecursiveDeref(dd,res);
1428                 return(NULL);
1429             }
1430             Cudd_Ref(w);
1431             Cudd_RecursiveDeref(dd,res);
1432             res = w;
1433         }
1434     }
1435     return(res);
1436
1437 endgame:
1438
1439     return(NULL);
1440
1441 } /* end of Ntr_initState */
1442
1443
1444 /**Function********************************************************************
1445
1446   Synopsis    [Reads a state cube from a file or creates a random one.]
1447
1448   Description [Reads a state cube from a file or create a random one.
1449   Returns a pointer to the BDD of the sink nodes if successful; NULL
1450   otherwise.]
1451
1452   SideEffects [None]
1453
1454   SeeAlso     []
1455
1456 *****************************************************************************/
1457 DdNode *
1458 Ntr_getStateCube(
1459   DdManager * dd,
1460   BnetNetwork * net,
1461   char * filename,
1462   int  pr)
1463 {
1464     FILE *fp;
1465     DdNode *cube;
1466     DdNode *w;
1467     char *state;
1468     int i;
1469     int err;
1470     BnetNode *node;
1471     DdNode *x;
1472     char c[2];
1473
1474     cube = Cudd_ReadOne(dd);
1475     if (net->nlatches == 0) {
1476         Cudd_Ref(cube);
1477         return(cube);
1478     }
1479
1480     state = ALLOC(char,net->nlatches+1);
1481     if (state == NULL)
1482         return(NULL);
1483     state[net->nlatches] = 0;
1484
1485     if (filename == NULL) {
1486         /* Pick one random minterm. */
1487         for (i = 0; i < net->nlatches; i++) {
1488             state[i] = (char) ((Cudd_Random() & 0x2000) ? '1' : '0');
1489         }
1490     } else {
1491         if ((fp = fopen(filename,"r")) == NULL) {
1492             (void) fprintf(stderr,"Unable to open %s\n",filename);
1493             return(NULL);
1494         }
1495
1496         /* Read string from file. Allow arbitrary amount of white space. */
1497         for (i = 0; !feof(fp); i++) {
1498             err = fscanf(fp, "%1s", c);
1499             state[i] = c[0];
1500             if (err == EOF || i == net->nlatches - 1) {
1501                 break;
1502             } else if (err != 1 || strchr("012xX-", c[0]) == NULL ) {
1503                 FREE(state);
1504                 return(NULL);
1505             }
1506         }
1507         err = fclose(fp);
1508         if (err == EOF) {
1509             FREE(state);
1510             return(NULL);
1511         }
1512     }
1513
1514     /* Echo the chosen state(s). */
1515     if (pr > 0) {(void) fprintf(stdout,"%s\n", state);}
1516
1517     Cudd_Ref(cube);
1518     for (i = 0; i < net->nlatches; i++) {
1519         if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1520             Cudd_RecursiveDeref(dd,cube);
1521             FREE(state);
1522             return(NULL);
1523         }
1524         x = node->dd;
1525         switch (state[i]) {
1526         case '0':
1527             w = Cudd_bddAnd(dd,cube,Cudd_Not(x));
1528             break;
1529         case '1':
1530             w = Cudd_bddAnd(dd,cube,x);
1531             break;
1532         default: /* don't care */
1533             w = cube;
1534             break;
1535         }
1536
1537         if (w == NULL) {
1538             Cudd_RecursiveDeref(dd,cube);
1539             FREE(state);
1540             return(NULL);
1541         }
1542         Cudd_Ref(w);
1543         Cudd_RecursiveDeref(dd,cube);
1544         cube = w;
1545     }
1546
1547     FREE(state);
1548     return(cube);
1549
1550 } /* end of Ntr_getStateCube */
1551
1552
1553 /**Function********************************************************************
1554
1555   Synopsis    [Poor man's outer envelope computation.]
1556
1557   Description [ Poor man's outer envelope computation based on the
1558   monolithic transition relation. Returns 1 in case of success; 0
1559   otherwise.]
1560
1561   SideEffects [None]
1562
1563   SeeAlso     []
1564
1565 ******************************************************************************/
1566 int
1567 Ntr_Envelope(
1568   DdManager * dd /* DD manager */,
1569   NtrPartTR * TR /* transition relation */,
1570   FILE * dfp /* pointer to file for DD dump */,
1571   NtrOptions * option /* program options */)
1572 {
1573     DdNode **x; /* array of x variables */
1574     DdNode **y; /* array of y variables */
1575     int ns;     /* number of x and y variables */
1576     DdNode *dfunc[2];   /* addresses of the functions to be dumped */
1577     DdNode *envelope, *oldEnvelope;
1578     DdNode *one;
1579     int depth;
1580     int retval;
1581     int pr = option->verb;
1582     int dumpFmt = option->dumpFmt;
1583
1584     x = TR->x;
1585     y = TR->y;
1586     ns = TR->nlatches;
1587
1588     one = Cudd_ReadOne(dd);
1589     retval = Cudd_SetVarMap(dd,x,y,ns);
1590
1591     /* Initialize From. */
1592     envelope = one;
1593     if (envelope == NULL) return(0);
1594     Cudd_Ref(envelope);
1595     (void) printf("S0"); Cudd_PrintDebug(dd,envelope,ns,pr);
1596
1597     /* Start traversal. */
1598     for (depth = 0; ; depth++) {
1599         oldEnvelope = envelope;
1600         /* Image computation. */
1601         envelope = ntrImage(dd,TR,oldEnvelope,option);
1602         if (envelope == NULL) {
1603             Cudd_RecursiveDeref(dd,oldEnvelope);
1604             return(0);
1605         }
1606
1607         /* Check for convergence. */
1608         if (envelope == oldEnvelope) break;
1609
1610         /* Prepare for new iteration. */
1611         Cudd_RecursiveDeref(dd,oldEnvelope);
1612         (void) fprintf(stdout,"Envelope[%d]%s",depth+1,(pr>0)? "" : "\n");
1613         Cudd_PrintDebug(dd,envelope,ns,pr);
1614
1615     }
1616     /* Clean up. */
1617     Cudd_RecursiveDeref(dd,oldEnvelope);
1618
1619     /* Print out result. */
1620     (void) printf("depth = %d\n", depth);
1621     (void) printf("Envelope"); Cudd_PrintDebug(dd,envelope,ns,pr);
1622
1623     /* Write dump file if requested. */
1624     if (dfp != NULL) {
1625         dfunc[0] = TR->part[0];
1626         dfunc[1] = envelope;
1627         if (dumpFmt == 1) {
1628             retval = Cudd_DumpBlif(dd,2,dfunc,NULL,(char **)onames,NULL,dfp,0);
1629         } else if (dumpFmt == 2) {
1630             retval = Cudd_DumpDaVinci(dd,2,dfunc,NULL,(char **)onames,dfp);
1631         } else if (dumpFmt == 3) {
1632             retval = Cudd_DumpDDcal(dd,2,dfunc,NULL,(char **)onames,dfp);
1633         } else if (dumpFmt == 4) {
1634             retval = Cudd_DumpFactoredForm(dd,2,dfunc,NULL,
1635                                            (char **)onames,dfp);
1636         } else if (dumpFmt == 5) {
1637             retval = Cudd_DumpBlif(dd,2,dfunc,NULL,(char **)onames,NULL,dfp,1);
1638         } else {
1639             retval = Cudd_DumpDot(dd,2,dfunc,NULL,(char **)onames,dfp);
1640         }
1641         if (retval != 1) {
1642             (void) fprintf(stderr,"abnormal termination\n");
1643             return(0);
1644         }
1645         fclose(dfp);
1646     }
1647
1648     /* Clean up. */
1649     Cudd_RecursiveDeref(dd,envelope);
1650
1651     return(1);
1652
1653 } /* end of Ntr_Envelope */
1654
1655
1656 /**Function********************************************************************
1657
1658   Synopsis    [Maximum 0-1 flow between source and sink states.]
1659
1660   Description [Maximum 0-1 flow between source and sink
1661   states. Returns 1 in case of success; 0 otherwise.]
1662
1663   SideEffects [Creates two new sets of variables.]
1664
1665   SeeAlso     []
1666
1667 ******************************************************************************/
1668 int
1669 Ntr_maxflow(
1670   DdManager * dd,
1671   BnetNetwork * net,
1672   NtrOptions * option)
1673 {
1674     DdNode **x = NULL;
1675     DdNode **y = NULL;
1676     DdNode **z = NULL;
1677     DdNode *E = NULL;
1678     DdNode *F = NULL;
1679     DdNode *cut = NULL;
1680     DdNode *sx = NULL;
1681     DdNode *ty = NULL;
1682     DdNode *tx = NULL;
1683     int n;
1684     int pr;
1685     int ylevel;
1686     int i;
1687     double flow;
1688     int result = 0;
1689     NtrPartTR *TR;
1690
1691     n = net->nlatches;
1692     pr = option->verb;
1693     TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1694     if (TR == NULL)
1695         goto endgame;
1696     E = TR->part[0];
1697     x = TR->x;
1698     y = TR->y;
1699     /* Create array of auxiliary variables. */
1700     z = ALLOC(DdNode *,n);
1701     if (z == NULL)
1702         goto endgame;
1703     for (i = 0; i < n; i++) {
1704         ylevel = Cudd_ReadIndex(dd,y[i]->index);
1705         z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1706         if (z[i] == NULL)
1707             goto endgame;
1708         Cudd_Ref(z[i]);
1709     }
1710     /* Create BDDs for source and sink. */
1711     sx = Ntr_initState(dd,net,option);
1712     if (sx == NULL)
1713         goto endgame;
1714     if (pr > 0) (void) fprintf(stdout, "Sink(s): ");
1715     tx = Ntr_getStateCube(dd,net,option->sinkfile,pr);
1716     if (tx == NULL)
1717         goto endgame;
1718     ty = Cudd_bddSwapVariables(dd,tx,x,y,n);
1719     if (ty == NULL)
1720         goto endgame;
1721     Cudd_Ref(ty);
1722     Cudd_RecursiveDeref(dd,tx);
1723     tx = NULL;
1724
1725     flow = Ntr_maximum01Flow(dd, sx, ty, E, &F, &cut, x, y, z, n, pr);
1726     if (flow >= 0.0)
1727         result = 1;
1728     if (pr >= 0) {
1729         (void) fprintf(stdout,"Maximum flow = %g\n", flow);
1730         (void) fprintf(stdout,"E"); Cudd_PrintDebug(dd,E,2*n,pr);
1731         (void) fprintf(stdout,"F"); Cudd_PrintDebug(dd,F,2*n,pr);
1732         (void) fprintf(stdout,"cut"); Cudd_PrintDebug(dd,cut,2*n,pr);
1733     }
1734 endgame:
1735     /* Clean up. */
1736     if (TR != NULL) Ntr_freeTR(dd,TR);
1737     for (i = 0; i < n; i++) {
1738         if (z != NULL && z[i] != NULL) Cudd_RecursiveDeref(dd,z[i]);
1739     }
1740     if (z != NULL) FREE(z);
1741     if (F != NULL) Cudd_RecursiveDeref(dd,F);
1742     if (cut != NULL) Cudd_RecursiveDeref(dd,cut);
1743     if (sx != NULL) Cudd_RecursiveDeref(dd,sx);
1744     if (ty != NULL) Cudd_RecursiveDeref(dd,ty);
1745     return(result);
1746
1747 } /* end of Ntr_Maxflow */
1748
1749 /*---------------------------------------------------------------------------*/
1750 /* Definition of internal functions                                          */
1751 /*---------------------------------------------------------------------------*/
1752
1753 /*---------------------------------------------------------------------------*/
1754 /* Definition of static functions                                            */
1755 /*---------------------------------------------------------------------------*/
1756
1757
1758 /**Function********************************************************************
1759
1760   Synopsis    [Builds a positive cube of all the variables in x.]
1761
1762   Description [Builds a positive cube of all the variables in x. Returns
1763   a BDD for the cube if successful; NULL otherwise.]
1764
1765   SideEffects [None]
1766
1767   SeeAlso     []
1768
1769 ******************************************************************************/
1770 static DdNode *
1771 makecube(
1772   DdManager * dd,
1773   DdNode ** x,
1774   int  n)
1775 {
1776     DdNode *res, *w, *one;
1777     int i;
1778
1779     one = Cudd_ReadOne(dd);
1780     Cudd_Ref(res = one);
1781
1782     for (i = n-1; i >= 0; i--) {
1783         w = Cudd_bddAnd(dd,res,x[i]);
1784         if (w == NULL) {
1785             Cudd_RecursiveDeref(dd,res);
1786             return(NULL);
1787         }
1788         Cudd_Ref(w);
1789         Cudd_RecursiveDeref(dd,res);
1790         res = w;
1791     }
1792     Cudd_Deref(res);
1793     return(res);
1794
1795 } /* end of makecube */
1796
1797
1798 /**Function********************************************************************
1799
1800   Synopsis    [Initializes the count fields used to drop DDs.]
1801
1802   Description [Initializes the count fields used to drop DDs.
1803   Before actually building the BDDs, we perform a DFS from the outputs
1804   to initialize the count fields of the nodes.  The initial value of the
1805   count field will normally coincide with the fanout of the node.
1806   However, if there are nodes with no path to any primary output or next
1807   state variable, then the initial value of count for some nodes will be
1808   less than the fanout. For primary outputs and next state functions we
1809   add 1, so that we will never try to free their DDs. The count fields
1810   of the nodes that are not reachable from the outputs are set to -1.]
1811
1812   SideEffects [Changes the count fields of the network nodes. Uses the
1813   visited fields.]
1814
1815   SeeAlso     []
1816
1817 ******************************************************************************/
1818 static void
1819 ntrInitializeCount(
1820   BnetNetwork * net,
1821   NtrOptions * option)
1822 {
1823     BnetNode *node;
1824     int i;
1825
1826     if (option->node != NULL &&
1827         option->closestCube == FALSE && option->dontcares == FALSE) {
1828         if (!st_lookup(net->hash,option->node,&node)) {
1829             (void) fprintf(stdout, "Warning: node %s not found!\n",
1830                            option->node);
1831         } else {
1832             ntrCountDFS(net,node);
1833             node->count++;
1834         }
1835     } else {
1836         if (option->stateOnly == FALSE) {
1837             for (i = 0; i < net->npos; i++) {
1838                 if (!st_lookup(net->hash,net->outputs[i],&node)) {
1839                     (void) fprintf(stdout,
1840                                    "Warning: output %s is not driven!\n",
1841                                    net->outputs[i]);
1842                     continue;
1843                 }
1844                 ntrCountDFS(net,node);
1845                 node->count++;
1846             }
1847         }
1848         for (i = 0; i < net->nlatches; i++) {
1849             if (!st_lookup(net->hash,net->latches[i][0],&node)) {
1850                 (void) fprintf(stdout,
1851                                "Warning: latch input %s is not driven!\n",
1852                                net->outputs[i]);
1853                 continue;
1854             }
1855             ntrCountDFS(net,node);
1856             node->count++;
1857         }
1858     }
1859
1860     /* Clear visited flags. */
1861     node = net->nodes;
1862     while (node != NULL) {
1863         if (node->visited == 0) {
1864             node->count = -1;
1865         } else {
1866             node->visited = 0;
1867         }
1868         node = node->next;
1869     }
1870
1871 } /* end of ntrInitializeCount */
1872
1873
1874 /**Function********************************************************************
1875
1876   Synopsis    [Does a DFS from a node setting the count field.]
1877
1878   Description []
1879
1880   SideEffects [Changes the count and visited fields of the nodes it
1881   visits.]
1882
1883   SeeAlso     [ntrLevelDFS]
1884
1885 ******************************************************************************/
1886 static void
1887 ntrCountDFS(
1888   BnetNetwork * net,
1889   BnetNode * node)
1890 {
1891     int i;
1892     BnetNode *auxnd;
1893
1894     node->count++;
1895
1896     if (node->visited == 1) {
1897         return;
1898     }
1899
1900     node->visited = 1;
1901
1902     for (i = 0; i < node->ninp; i++) {
1903         if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
1904             exit(2);
1905         }
1906         ntrCountDFS(net,auxnd);
1907     }
1908
1909 } /* end of ntrCountDFS */
1910
1911
1912 /**Function********************************************************************
1913
1914   Synopsis    [Computes the image of a set given a transition relation.]
1915
1916   Description [Computes the image of a set given a transition relation.
1917   Returns a pointer to the result if successful; NULL otherwise. The image is
1918   returned in terms of the present state variables; its reference count is
1919   already increased.]
1920
1921   SideEffects [None]
1922
1923   SeeAlso     [Ntr_Trav]
1924
1925 ******************************************************************************/
1926 static DdNode *
1927 ntrImage(
1928   DdManager * dd,
1929   NtrPartTR * TR,
1930   DdNode * from,
1931   NtrOptions * option)
1932 {
1933     int i;
1934     DdNode *image;
1935     DdNode *to;
1936     NtrPartTR *T;
1937     int depth = 0;
1938
1939     if (option->image == NTR_IMAGE_CLIP) {
1940         depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1941     }
1942
1943     /* Existentially quantify the present state variables that are not
1944     ** in the support of any next state function. */
1945     image = Cudd_bddExistAbstract(dd,from,TR->preiabs);
1946     if (image == NULL) return(NULL);
1947     Cudd_Ref(image);
1948     if (option->image == NTR_IMAGE_DEPEND) {
1949         /* Simplify the transition relation based on dependencies
1950         ** and build the conjuncts from the deltas. */
1951         T = ntrEliminateDependencies(dd,TR,&image,option);
1952     } else {
1953         T = TR;
1954     }
1955     if (T == NULL) return(NULL);
1956     for (i = 0; i < T->nparts; i++) {
1957 #if 0
1958         (void) printf("  Intermediate product[%d]: %d nodes\n",
1959                       i,Cudd_DagSize(image));
1960 #endif
1961         if (option->image == NTR_IMAGE_CLIP) {
1962             to = Cudd_bddClippingAndAbstract(dd,T->part[i],image,T->icube[i],
1963                                              depth,option->approx);
1964         } else {
1965             to = Cudd_bddAndAbstract(dd,T->part[i],image,T->icube[i]);
1966         }
1967         if (to == NULL) return(NULL);
1968         Cudd_Ref(to);
1969         if (option->image == NTR_IMAGE_DEPEND) {
1970             /* Extract dependencies from intermediate product. */
1971             DdNode *abs, *positive, *absabs, *phi, *exnor, *tmp;
1972             abs = Cudd_bddExistAbstract(dd,to,T->xw);
1973             if (abs == NULL) return(NULL); Cudd_Ref(abs);
1974             if (Cudd_bddVarIsDependent(dd,abs,T->nscube[i]) &&
1975                 Cudd_EstimateCofactor(dd,abs,T->nscube[i]->index,1) <=
1976                 T->nlatches) {
1977                 int retval, sizex;
1978                 positive = Cudd_Cofactor(dd,abs,T->nscube[i]);
1979                 if (positive == NULL) return(NULL); Cudd_Ref(positive);
1980                 absabs = Cudd_bddExistAbstract(dd,abs,T->nscube[i]);
1981                 if (absabs == NULL) return(NULL); Cudd_Ref(absabs);
1982                 Cudd_RecursiveDeref(dd,abs);
1983                 phi = Cudd_bddLICompaction(dd,positive,absabs);
1984                 if (phi == NULL) return(NULL); Cudd_Ref(phi);
1985                 Cudd_RecursiveDeref(dd,positive);
1986                 Cudd_RecursiveDeref(dd,absabs);
1987                 exnor = Cudd_bddXnor(dd,T->nscube[i],phi);
1988                 if (exnor == NULL) return(NULL); Cudd_Ref(exnor);
1989                 Cudd_RecursiveDeref(dd,phi);
1990                 sizex = Cudd_DagSize(exnor);
1991                 (void) printf("new factor of %d nodes\n", sizex);
1992                 retval = Ntr_HeapInsert(T->factors,exnor,sizex);
1993                 if (retval == 0) return(NULL);
1994                 tmp = Cudd_bddExistAbstract(dd,to,T->nscube[i]);
1995                 if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
1996                 Cudd_RecursiveDeref(dd,to);
1997                 to = tmp;
1998             } else {
1999                 Cudd_RecursiveDeref(dd,abs);
2000             }
2001         }
2002         Cudd_RecursiveDeref(dd,image);
2003         image = to;
2004     }
2005     if (option->image == NTR_IMAGE_DEPEND) {
2006         int size1, size2;
2007         DdNode *factor1, *factor2, *tmp;
2008         int retval;
2009         size1 = Cudd_DagSize(image);
2010         retval = Ntr_HeapInsert(T->factors,image,size1);
2011         if (retval == 0) return(NULL);
2012         (void) printf("Merging %d factors. Independent image: %d nodes\n",
2013                       Ntr_HeapCount(T->factors), size1);
2014         while (Ntr_HeapCount(T->factors) > 1) {
2015             retval = Ntr_HeapExtractMin(T->factors,&factor1,&size1);
2016             if (retval == 0) return(NULL);
2017             retval = Ntr_HeapExtractMin(T->factors,&factor2,&size2);
2018             if (retval == 0) return(NULL);
2019             tmp = Cudd_bddAnd(dd,factor1,factor2);
2020             if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2021             size1 = Cudd_DagSize(tmp);
2022             (void) printf("new factor %d nodes\n", size1);
2023             Cudd_RecursiveDeref(dd,factor1);
2024             Cudd_RecursiveDeref(dd,factor2);
2025             retval = Ntr_HeapInsert(T->factors,tmp,size1);
2026             if (retval == 0) return(NULL);
2027         }
2028         retval = Ntr_HeapExtractMin(T->factors,&image,&size1);
2029         if (retval == 0) return(NULL);
2030         Ntr_freeTR(dd,T);
2031     }
2032
2033     /* Express image in terms of x variables. */
2034     to = Cudd_bddVarMap(dd,image);
2035     if (to == NULL) {
2036         Cudd_RecursiveDeref(dd,image);
2037         return(NULL);
2038     }
2039     Cudd_Ref(to);
2040     Cudd_RecursiveDeref(dd,image);
2041     return(to);
2042
2043 } /* end of ntrImage */
2044
2045
2046 /**Function********************************************************************
2047
2048   Synopsis    [Computes the preimage of a set given a transition relation.]
2049
2050   Description [Computes the preimage of a set given a transition relation.
2051   Returns a pointer to the result if successful; NULL otherwise. The preimage
2052   is returned in terms of the next state variables; its reference count is
2053   already increased.]
2054
2055   SideEffects [None]
2056
2057   SeeAlso     [ntrImage Ntr_SCC]
2058
2059 ******************************************************************************/
2060 static DdNode *
2061 ntrPreimage(
2062   DdManager * dd,
2063   NtrPartTR * T,
2064   DdNode * from)
2065 {
2066     int i;
2067     DdNode *preimage;
2068     DdNode *to;
2069
2070     /* Existentially quantify the present state variables that are not
2071     ** in the support of any next state function. */
2072     preimage = Cudd_bddExistAbstract(dd,from,T->prepabs);
2073     if (preimage == NULL) return(NULL);
2074     Cudd_Ref(preimage);
2075     for (i = 0; i < T->nparts; i++) {
2076 #if 0
2077         (void) printf("  Intermediate product[%d]: %d nodes\n",
2078                       i,Cudd_DagSize(preimage));
2079 #endif
2080         to = Cudd_bddAndAbstract(dd,T->part[i],preimage,T->pcube[i]);
2081         if (to == NULL) return(NULL);
2082         Cudd_Ref(to);
2083         Cudd_RecursiveDeref(dd,preimage);
2084         preimage = to;
2085     }
2086
2087     /* Express preimage in terms of x variables. */
2088     to = Cudd_bddVarMap(dd,preimage);
2089     if (to == NULL) {
2090         Cudd_RecursiveDeref(dd,preimage);
2091         return(NULL);
2092     }
2093     Cudd_Ref(to);
2094     Cudd_RecursiveDeref(dd,preimage);
2095     return(to);
2096
2097 } /* end of ntrPreimage */
2098
2099
2100 /**Function********************************************************************
2101
2102   Synopsis    [Chooses the initial states for a BFS step.]
2103
2104   Description [Chooses the initial states for a BFS step. Returns a
2105   pointer to the chose set if successful; NULL otherwise. The
2106   reference count of the result is already incremented.]
2107
2108   SideEffects [none]
2109
2110   SeeAlso     [Ntr_Trav]
2111
2112 ******************************************************************************/
2113 static DdNode *
2114 ntrChooseFrom(
2115   DdManager * dd,
2116   DdNode * neW,
2117   DdNode * reached,
2118   NtrOptions * option)
2119 {
2120     DdNode *min, *c;
2121     int threshold;
2122
2123     switch (option->from) {
2124     case NTR_FROM_NEW:
2125         Cudd_Ref(neW);
2126         return(neW);
2127     case NTR_FROM_REACHED:
2128         Cudd_Ref(reached);
2129         return(reached);
2130     case NTR_FROM_RESTRICT:
2131         c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2132         if (c == NULL) return(NULL);
2133         Cudd_Ref(c);
2134         min = Cudd_bddRestrict(dd,neW,c);
2135         if (min == NULL) {
2136             Cudd_RecursiveDeref(dd, c);
2137             return(NULL);
2138         }
2139         Cudd_Ref(min);
2140         Cudd_RecursiveDeref(dd, c);
2141         return(min);
2142     case NTR_FROM_COMPACT:
2143         c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2144         if (c == NULL) return(NULL);
2145         Cudd_Ref(c);
2146         min = Cudd_bddLICompaction(dd,neW,c);
2147         if (min == NULL) {
2148             Cudd_RecursiveDeref(dd, c);
2149             return(NULL);
2150         }
2151         Cudd_Ref(min);
2152         Cudd_RecursiveDeref(dd, c);
2153         return(min);
2154     case NTR_FROM_SQUEEZE:
2155         min = Cudd_bddSqueeze(dd,neW,reached);
2156         if (min == NULL) return(NULL);
2157         Cudd_Ref(min);
2158         return(min);
2159     case NTR_FROM_UNDERAPPROX:
2160         threshold = (option->threshold < 0) ? 0 : option->threshold;
2161         min = Cudd_RemapUnderApprox(dd,neW,Cudd_SupportSize(dd,neW),
2162                 threshold,option->quality);
2163         if (min == NULL) return(NULL);
2164         Cudd_Ref(min);
2165         return(min);
2166     case NTR_FROM_OVERAPPROX:
2167         threshold = (option->threshold < 0) ? 0 : option->threshold;
2168         min = Cudd_RemapOverApprox(dd,neW,Cudd_SupportSize(dd,neW),
2169                 threshold,option->quality);
2170         if (min == NULL) return(NULL);
2171         Cudd_Ref(min);
2172         return(min);
2173     default:
2174         return(NULL);
2175     }
2176
2177 } /* end of ntrChooseFrom */
2178
2179
2180 /**Function********************************************************************
2181
2182   Synopsis    [Updates the reached states after a traversal step.]
2183
2184   Description [Updates the reached states after a traversal
2185   step. Returns a pointer to the new reached set if successful; NULL
2186   otherwise. The reference count of the result is already incremented.]
2187
2188   SideEffects [The old reached set is dereferenced.]
2189
2190   SeeAlso     [Ntr_Trav]
2191
2192 ******************************************************************************/
2193 static DdNode *
2194 ntrUpdateReached(
2195   DdManager * dd /* manager */,
2196   DdNode * oldreached /* old reached state set */,
2197   DdNode * to /* result of last image computation */)
2198 {
2199     DdNode *reached;
2200
2201     reached = Cudd_bddOr(dd,oldreached,to);
2202     if (reached == NULL) {
2203         Cudd_RecursiveDeref(dd,oldreached);
2204         return(NULL);
2205     }
2206     Cudd_Ref(reached);
2207     Cudd_RecursiveDeref(dd,oldreached);
2208     return(reached);
2209
2210 } /* end of ntrUpdateReached */
2211
2212
2213 /**Function********************************************************************
2214
2215   Synopsis    [Analyzes the reached states after traversal to find
2216   dependent latches.]
2217
2218   Description [Analyzes the reached states after traversal to find
2219   dependent latches.  Returns the number of latches that can be
2220   eliminated because they are stuck at a constant value or are
2221   dependent on others if successful; -1 otherwise. The algorithm is
2222   greedy and determines a local optimum, not a global one.]
2223
2224   SideEffects []
2225
2226   SeeAlso     [Ntr_Trav]
2227
2228 ******************************************************************************/
2229 static int
2230 ntrLatchDependencies(
2231   DdManager *dd,
2232   DdNode *reached,
2233   BnetNetwork *net,
2234   NtrOptions *option)
2235 {
2236     int i;
2237     int howMany;                /* number of latches that can be eliminated */
2238     DdNode *var, *newreached, *abs, *positive, *phi;
2239     char *name;
2240     BnetNode *node;
2241     int initVars, finalVars;
2242     double initStates, finalStates;
2243     DdNode **roots;
2244     char **onames;
2245     int howManySmall = 0;
2246     int *candidates;
2247     double minStates;
2248     int totalVars;
2249
2250     (void) printf("Analyzing latch dependencies\n");
2251     roots = ALLOC(DdNode *, net->nlatches);
2252     if (roots == NULL) return(-1);
2253     onames = ALLOC(char *, net->nlatches);
2254     if (onames == NULL) return(-1);
2255
2256     candidates = ALLOC(int,net->nlatches);
2257     if (candidates == NULL) return(-1);
2258     for (i = 0; i < net->nlatches; i++) {
2259         candidates[i] = i;
2260     }
2261     /* The signatures of the variables in a function are the number
2262     ** of minterms of the positive cofactors with respect to the
2263     ** variables themselves. */
2264     newreached = reached;
2265     Cudd_Ref(newreached);
2266     signatures = Cudd_CofMinterm(dd,newreached);
2267     if (signatures == NULL) return(-1);
2268     /* We now extract a positive quantity which is higher for those
2269     ** variables that are closer to being essential. */
2270     totalVars = Cudd_ReadSize(dd);
2271     minStates = signatures[totalVars];
2272 #if 0
2273     (void) printf("Raw signatures (minStates = %g)\n", minStates);
2274     for (i = 0; i < net->nlatches; i++) {
2275         int j = candidates[i];
2276         if (!st_lookup(net->hash,net->latches[j][1],(char **) &node)) {
2277             return(-1);
2278         }
2279         (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2280     }
2281 #endif
2282     for (i = 0; i < totalVars; i++) {
2283         double z = signatures[i] / minStates - 1.0;
2284         signatures[i] = (z >= 0.0) ? z : -z;    /* make positive */
2285     }
2286     staticNet = net;
2287     qsort((void *)candidates,net->nlatches,sizeof(int),
2288           (DD_QSFP)ntrSignatureCompare2);
2289 #if 0
2290     (void) printf("Cooked signatures\n");
2291     for (i = 0; i < net->nlatches; i++) {
2292         int j = candidates[i];
2293         if (!st_lookup(net->hash,net->latches[j][1],(char **) &node)) {
2294             return(-1);
2295         }
2296         (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2297     }
2298 #endif
2299     FREE(signatures);
2300
2301     /* Extract simple dependencies. */
2302     for (i = 0; i < net->nlatches; i++) {
2303         int j = candidates[i];
2304         if (!st_lookup(net->hash,net->latches[j][1],&node)) {
2305             return(-1);
2306         }
2307         var = node->dd;
2308         name = node->name;
2309         if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2310             positive = Cudd_Cofactor(dd,newreached,var);
2311             if (positive == NULL) return(-1); Cudd_Ref(positive);
2312             abs = Cudd_bddExistAbstract(dd,newreached,var);
2313             if (abs == NULL) return(-1); Cudd_Ref(abs);
2314             phi = Cudd_bddLICompaction(dd,positive,abs);
2315             if (phi == NULL) return(-1); Cudd_Ref(phi);
2316             Cudd_RecursiveDeref(dd,positive);
2317             if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2318                 if (Cudd_bddLeq(dd,newreached,var)) {
2319                     (void) printf("%s is stuck at 1\n",name);
2320                 } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2321                     (void) printf("%s is stuck at 0\n",name);
2322                 } else {
2323                     (void) printf("%s depends on the other variables\n",name);
2324                 }
2325                 roots[howManySmall] = phi;
2326                 onames[howManySmall] = util_strsav(name);
2327                 Cudd_RecursiveDeref(dd,newreached);
2328                 newreached = abs;
2329                 howManySmall++;
2330                 candidates[i] = -1; /* do not reconsider */
2331             } else {
2332                 Cudd_RecursiveDeref(dd,abs);
2333                 Cudd_RecursiveDeref(dd,phi);
2334             }
2335         } else {
2336             candidates[i] = -1; /* do not reconsider */
2337         }
2338     }
2339     /* Now remove remaining dependent variables. */
2340     howMany = howManySmall;
2341     for (i = 0; i < net->nlatches; i++) {
2342         int j = candidates[i];
2343         if (j == -1) continue;
2344         if (!st_lookup(net->hash,net->latches[j][1],&node)) {
2345             return(-1);
2346         }
2347         var = node->dd;
2348         name = node->name;
2349         if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2350             if (Cudd_bddLeq(dd,newreached,var)) {
2351                 (void) printf("%s is stuck at 1\n",name);
2352             } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2353                 (void) printf("%s is stuck at 0\n",name);
2354             } else {
2355                 (void) printf("%s depends on the other variables\n",name);
2356             }
2357             abs = Cudd_bddExistAbstract(dd,newreached,var);
2358             if (abs == NULL) return(-1); Cudd_Ref(abs);
2359             Cudd_RecursiveDeref(dd,newreached);
2360             newreached = abs;
2361             howMany++;
2362         }
2363     }
2364     FREE(candidates);
2365     if (howManySmall > 0) {
2366         if (!Bnet_bddArrayDump(dd,net,(char *)"-",roots,onames,howManySmall,1))
2367             return(-1);
2368     }
2369     for (i = 0; i < howManySmall; i++) {
2370         Cudd_RecursiveDeref(dd,roots[i]);
2371         FREE(onames[i]);
2372     }
2373     FREE(roots);
2374     FREE(onames);
2375
2376     initVars = net->nlatches;
2377     initStates = Cudd_CountMinterm(dd,reached,initVars);
2378     finalVars = initVars - howMany;
2379     finalStates = Cudd_CountMinterm(dd,newreached,finalVars);
2380     if (initStates != finalStates) {
2381         (void) printf("Error: the number of states changed from %g to %g\n",
2382                       initStates, finalStates);
2383         return(-1);
2384     }
2385     (void) printf("new reached");
2386     Cudd_PrintDebug(dd,newreached,finalVars,option->verb);
2387     Cudd_RecursiveDeref(dd,newreached);
2388     return(howMany);
2389
2390 } /* end of ntrLatchDependencies */
2391
2392
2393 /**Function********************************************************************
2394
2395   Synopsis    [Eliminates dependent variables from a transition relation.]
2396
2397   Description [Eliminates dependent variables from a transition
2398   relation.  Returns a simplified copy of the given transition
2399   relation if successful; NULL otherwise.]
2400
2401   SideEffects [The modified set of states is returned as a side effect.]
2402
2403   SeeAlso     [ntrImage]
2404
2405 ******************************************************************************/
2406 static NtrPartTR *
2407 ntrEliminateDependencies(
2408   DdManager *dd,
2409   NtrPartTR *TR,
2410   DdNode **states,
2411   NtrOptions *option)
2412 {
2413     NtrPartTR *T;               /* new TR without dependent vars */
2414     int pr = option->verb;
2415     int i, j;
2416     int howMany = 0;            /* number of latches that can be eliminated */
2417     DdNode *var, *newstates, *abs, *positive, *phi;
2418     DdNode *support, *scan, *tmp;
2419     int finalSize;              /* size of the TR after substitutions */
2420     int nvars;                  /* vars in the support of the state set */
2421     int *candidates;            /* vars to be considered for elimination */
2422     int totalVars;
2423     double minStates;
2424
2425     /* Initialize the new transition relation by copying the old one. */
2426     T = Ntr_cloneTR(TR);
2427     if (T == NULL) return(NULL);
2428     newstates = *states;
2429     Cudd_Ref(newstates);
2430
2431     /* Find and rank the candidate variables. */
2432     support = Cudd_Support(dd,newstates);
2433     if (support == NULL) {
2434         Ntr_freeTR(dd,T);
2435         return(NULL);
2436     }
2437     Cudd_Ref(support);
2438     nvars = Cudd_DagSize(support) - 1;
2439     candidates = ALLOC(int,nvars);
2440     if (candidates == NULL) {
2441         Cudd_RecursiveDeref(dd,support);
2442         Ntr_freeTR(dd,T);
2443         return(NULL);
2444     }
2445     scan  = support;
2446     for (i = 0; i < nvars; i++) {
2447         candidates[i] = scan->index;
2448         scan = Cudd_T(scan);
2449     }
2450     Cudd_RecursiveDeref(dd,support);
2451     /* The signatures of the variables in a function are the number
2452     ** of minterms of the positive cofactors with respect to the
2453     ** variables themselves. */
2454     signatures = Cudd_CofMinterm(dd,newstates);
2455     if (signatures == NULL) {
2456         FREE(candidates);
2457         Ntr_freeTR(dd,T);
2458         return(NULL);
2459     }
2460     /* We now extract a positive quantity which is higher for those
2461     ** variables that are closer to being essential. */
2462     totalVars = Cudd_ReadSize(dd);
2463     minStates = signatures[totalVars];
2464     for (i = 0; i < totalVars; i++) {
2465         double z = signatures[i] / minStates - 1.0;
2466         signatures[i] = (z < 0.0) ? -z : z;     /* make positive */
2467     }
2468     /* Sort candidates in decreasing order of signature. */
2469     qsort((void *)candidates,nvars,sizeof(int),
2470           (DD_QSFP)ntrSignatureCompare);
2471     FREE(signatures);
2472
2473     /* Now process the candidates in the given order. */
2474     for (i = 0; i < nvars; i++) {
2475         var = Cudd_bddIthVar(dd,candidates[i]);
2476         if (Cudd_bddVarIsDependent(dd,newstates,var)) {
2477             abs = Cudd_bddExistAbstract(dd,newstates,var);
2478             if (abs == NULL) return(NULL); Cudd_Ref(abs);
2479             positive = Cudd_Cofactor(dd,newstates,var);
2480             if (positive == NULL) return(NULL); Cudd_Ref(positive);
2481             phi = Cudd_bddLICompaction(dd,positive,abs);
2482             if (phi == NULL) return(NULL); Cudd_Ref(phi);
2483             Cudd_RecursiveDeref(dd,positive);
2484 #if 0
2485             if (pr > 0) {
2486                 (void) printf("Phi");
2487                 Cudd_PrintDebug(dd,phi,T->nlatches,pr);
2488             }
2489 #endif
2490             if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2491                 howMany++;
2492                 for (j = 0; j < T->nparts; j++) {
2493                     tmp = Cudd_bddCompose(dd,T->part[j],phi,candidates[i]);
2494                     if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2495                     Cudd_RecursiveDeref(dd,T->part[j]);
2496                     T->part[j] = tmp;
2497                 }
2498                 Cudd_RecursiveDeref(dd,newstates);
2499                 newstates = abs;
2500             } else {
2501                 Cudd_RecursiveDeref(dd,abs);
2502             }
2503             Cudd_RecursiveDeref(dd,phi);
2504         }
2505     }
2506     FREE(candidates);
2507
2508     if (pr > 0) {
2509         finalSize = Cudd_SharingSize(T->part,T->nparts);
2510         (void) printf("Eliminated %d vars. Transition function %d nodes.\n",
2511                       howMany,finalSize);
2512     }
2513
2514     if (!ntrUpdateQuantificationSchedule(dd,T)) return(NULL);
2515
2516     /* Quantify out of states variables that no longer appear in any part. */
2517     Cudd_RecursiveDeref(dd,*states);
2518     *states = Cudd_bddExistAbstract(dd,newstates,T->preiabs);
2519     if (*states == NULL) return(NULL); Cudd_Ref(*states);
2520     Cudd_RecursiveDeref(dd,newstates);
2521     return(T);
2522
2523 } /* end of ntrEliminateDependencies */
2524
2525
2526 /**Function********************************************************************
2527
2528   Synopsis    [Updates the quantification schedule of a transition relation.]
2529
2530   Description [Updates the quantification schedule of a transition relation.
2531   Returns 1 if successful; 0 otherwise.]
2532
2533   SideEffects [None]
2534
2535   SeeAlso     [ntrEliminateDependencies]
2536
2537 ******************************************************************************/
2538 static int
2539 ntrUpdateQuantificationSchedule(
2540   DdManager *dd,
2541   NtrPartTR *T)
2542 {
2543     int i, j, k;
2544     int *schedule;
2545     DdNode *one, *support, *scan, *var, *tmp;
2546     char **matrix;
2547     int *position, *row;
2548     char *flags;
2549     int nparts, nvars;
2550     int extracted;
2551 #if 0
2552     int schedcost;
2553 #endif
2554
2555     nparts = T->nparts;
2556     nvars = Cudd_ReadSize(dd);
2557     one = Cudd_ReadOne(dd);
2558
2559     /* Reinitialize the abstraction cubes. */
2560     Cudd_RecursiveDeref(dd,T->preiabs);
2561     T->preiabs = one;
2562     Cudd_Ref(one);
2563     for (i = 0; i < nparts; i++) {
2564         Cudd_RecursiveDeref(dd,T->icube[i]);
2565         T->icube[i] = one;
2566         Cudd_Ref(one);
2567     }
2568
2569     /* Initialize row permutations to the identity. */
2570     position = ALLOC(int,nparts);
2571     if (position == NULL) return(0);
2572     for (i = 0; i < nparts; i++) {
2573         position[i] = i;
2574     }
2575     /* Sort parts so that parts that differ only
2576     ** in the index of the next state variable are contiguous. */
2577     staticPart = T->part;
2578     qsort((void *)position,nparts,sizeof(int), (DD_QSFP)ntrPartCompare);
2579     /* Extract repeated parts. */
2580     extracted = 0;
2581     for (i = 0; i < nparts - 1; i += j) {
2582         int pi, pij;
2583         DdNode *eq;
2584         j = 1;
2585         pi = position[i];
2586         eq = one;
2587         Cudd_Ref(eq);
2588         pij = position[i+j];
2589         while (Cudd_Regular(staticPart[pij]) == Cudd_Regular(staticPart[pi])) {
2590             int comple = staticPart[pij] != staticPart[pi];
2591             DdNode *xnor = Cudd_bddXnor(dd,T->nscube[pi],
2592                                         Cudd_NotCond(T->nscube[pij],comple));
2593             if (xnor == NULL) return(0); Cudd_Ref(xnor);
2594             tmp = Cudd_bddAnd(dd,xnor,eq);
2595             if (tmp == NULL) return(0); Cudd_Ref(tmp);
2596             Cudd_RecursiveDeref(dd,xnor);
2597             Cudd_RecursiveDeref(dd,eq);
2598             eq = tmp;
2599             Cudd_RecursiveDeref(dd,T->part[pij]);
2600             Cudd_RecursiveDeref(dd,T->icube[pij]);
2601             Cudd_RecursiveDeref(dd,T->nscube[pij]);
2602             T->part[pij] = NULL;
2603             j++;
2604             if (i+j == nparts) break;
2605             pij = position[i+j];
2606         }
2607         if (eq != one) {
2608             int retval = Ntr_HeapInsert(T->factors,eq,Cudd_DagSize(eq));
2609             if (retval == 0) return(0);
2610             extracted += j - 1;
2611         } else {
2612             Cudd_RecursiveDeref(dd,eq);
2613         }
2614     }
2615     /* Compact the part array by removing extracted parts. */
2616     for (i = 0, j = 0; i < nparts; i++) {
2617         if (T->part[i] != NULL) {
2618             T->part[j] = T->part[i];
2619             T->icube[j] = T->icube[i];
2620             T->nscube[j] = T->nscube[i];
2621             j++;
2622         }
2623     }
2624     nparts = T->nparts -= extracted;
2625     (void) printf("Extracted %d repeated parts in %d factors.\n",
2626                   extracted, Ntr_HeapCount(T->factors));
2627
2628     /* Build the support matrix. Each row corresponds to a part of the
2629     ** transition relation; each column corresponds to a variable in
2630     ** the manager. A 1 in position (i,j) means that Part i depends
2631     ** on Variable j. */
2632     matrix = ntrAllocMatrix(nparts,nvars);
2633     if (matrix == NULL) return(0);
2634
2635     /* Allocate array for quantification schedule and initialize it. */
2636     schedule = ALLOC(int,nvars);
2637     if (schedule == NULL) return(0);
2638     for (i = 0; i < nvars; i++) {
2639         schedule[i] = -1;
2640     }
2641     /* Collect scheduling info for this part. At the end of this loop
2642     ** schedule[i] == j means that the variable of index i does not
2643     ** appear in any part with index greater than j, unless j == -1,
2644     ** in which case the variable appears in no part.
2645     */
2646     for (i = 0; i < nparts; i++) {
2647         support = Cudd_Support(dd,T->part[i]);
2648         if (support == NULL) return(0); Cudd_Ref(support);
2649         scan = support;
2650         while (!Cudd_IsConstant(scan)) {
2651             int index = scan->index;
2652             schedule[index] = i;
2653             matrix[i][index] = 1;
2654             scan = Cudd_T(scan);
2655         }
2656         Cudd_RecursiveDeref(dd,support);
2657     }
2658 #if 0
2659     (void) printf("Initial schedule:");
2660     schedcost = 0;
2661     for (i = 0; i < nvars; i++) {
2662         (void) printf(" %d", schedule[i]);
2663         if (schedule[i] != -1) schedcost += schedule[i];
2664     }
2665     (void) printf("\nCost = %d\n", schedcost);
2666 #endif
2667
2668     /* Initialize direct and inverse row permutations to the identity
2669     ** permutation. */
2670     row = ALLOC(int,nparts);
2671     if (row == NULL) return(0);
2672     for (i = 0; i < nparts; i++) {
2673         position[i] = row[i] = i;
2674     }
2675
2676     /* Sift the matrix. */
2677     flags = ALLOC(char,nvars);
2678     if (flags == NULL) return(0);
2679     for (i = 0; i < nparts; i++) {
2680         int cost = 0;           /* cost of moving the row */
2681         int bestcost = 0;
2682         int posn = position[i];
2683         int bestposn = posn;
2684         /* Sift up. */
2685         /* Initialize the flags to one is for the variables that are
2686         ** currently scheduled to be quantified after this part gets
2687         ** multiplied. When we cross a row of a part that depends on
2688         ** a variable whose flag is 1, we know that the row being sifted
2689         ** is no longer responsible for that variable. */
2690         for (k = 0; k < nvars; k++) {
2691             flags[k] = (char) (schedule[k] == i);
2692         }
2693         for (j = posn - 1; j >= 0; j--) {
2694             for (k = 0; k < nvars; k++) {
2695                 if (schedule[k] == row[j]) {
2696                     cost++;
2697                 } else {
2698                     flags[k] &= matrix[row[j]][k] == 0;
2699                     cost -= flags[k];
2700                 }
2701             }
2702             if (cost < bestcost) {
2703                 bestposn = j;
2704                 bestcost = cost;
2705             }
2706         }
2707         /* Sift down. */
2708         /* Reinitialize the flags. (We are implicitly undoing the sift
2709         ** down step.) */
2710         for (k = 0; k < nvars; k++) {
2711             flags[k] = (char) (schedule[k] == i);
2712         }
2713         for (j = posn + 1; j < nparts; j++) {
2714             for (k = 0; k < nvars; k++) {
2715                 if (schedule[k] == row[j]) {
2716                     flags[k] |= matrix[i][k] == 1;
2717                     cost -= flags[k] == 0;
2718                 } else {
2719                     cost += flags[k];
2720                 }
2721             }
2722             if (cost < bestcost) {
2723                 bestposn = j;
2724                 bestcost = cost;
2725             }
2726         }
2727         /* Move to best position. */
2728         if (bestposn < posn) {
2729             for (j = posn; j >= bestposn; j--) {
2730                 k = row[j];
2731                 if (j > 0) row[j] = row[j-1];
2732                 position[k]++;
2733             }
2734         } else {
2735             for (j = posn; j <= bestposn; j++) {
2736                 k = row[j];
2737                 if (j < nparts - 1) row[j] = row[j+1];
2738                 position[k]--;
2739             }
2740         }
2741         position[i] = bestposn;
2742         row[bestposn] = i;
2743         /* Fix the schedule. */
2744         for (k = 0; k < nvars; k++) {
2745             if (matrix[i][k] == 1) {
2746                 if (position[schedule[k]] < bestposn) {
2747                     schedule[k] = i;
2748                 } else {
2749                     for (j = nparts - 1; j >= position[i]; j--) {
2750                         if (matrix[row[j]][k] == 1) break;
2751                     }
2752                     schedule[k] = row[j];
2753                 }
2754             }
2755         }
2756     }
2757     ntrFreeMatrix(matrix);
2758     FREE(flags);
2759
2760     /* Update schedule to account for the permutation. */
2761     for (i = 0; i < nvars; i++) {
2762         if (schedule[i] >= 0) {
2763             schedule[i] = position[schedule[i]];
2764         }
2765     }
2766     /* Sort parts. */
2767     ntrPermuteParts(T->part,T->nscube,row,position,nparts);
2768     FREE(position);
2769     FREE(row);
2770 #if 0
2771     (void) printf("New schedule:");
2772     schedcost = 0;
2773     for (i = 0; i < nvars; i++) {
2774         (void) printf(" %d", schedule[i]);
2775         if (schedule[i] != -1) schedcost += schedule[i];
2776     }
2777     (void) printf("\nCost = %d\n", schedcost);
2778 #endif
2779
2780     /* Mark the next state varibles so that they do not go in the
2781     ** abstraction cubes. */
2782     for (i = 0; i < T->nlatches; i++) {
2783         schedule[T->y[i]->index] = -2;
2784     }
2785
2786     /* Rebuild the cubes from the schedule. */
2787     for (i = 0; i < nvars; i++) {
2788         k = schedule[i];
2789         var = Cudd_bddIthVar(dd,i);
2790         if (k >= 0) {
2791             tmp = Cudd_bddAnd(dd,T->icube[k],var);
2792             if (tmp == NULL) return(0); Cudd_Ref(tmp);
2793             Cudd_RecursiveDeref(dd,T->icube[k]);
2794             T->icube[k] = tmp;
2795         } else if (k != -2) {
2796             tmp = Cudd_bddAnd(dd,T->preiabs,var);
2797             if (tmp == NULL) return(0); Cudd_Ref(tmp);
2798             Cudd_RecursiveDeref(dd,T->preiabs);
2799             T->preiabs = tmp;
2800         }
2801     }
2802     FREE(schedule);
2803
2804     /* Build the conjuncts. */
2805     for (i = 0; i < nparts; i++) {
2806         tmp = Cudd_bddXnor(dd,T->nscube[i],T->part[i]);
2807         if (tmp == NULL) return(0); Cudd_Ref(tmp);
2808         Cudd_RecursiveDeref(dd,T->part[i]);
2809         T->part[i] = tmp;
2810     }
2811
2812     return(1);
2813
2814 } /* end of ntrUpdateQuantificationSchedule */
2815
2816
2817 /**Function********************************************************************
2818
2819   Synopsis    [Comparison function used by qsort.]
2820
2821   Description [Comparison function used by qsort to order the
2822   variables according to their signatures.]
2823
2824   SideEffects [None]
2825
2826 ******************************************************************************/
2827 static int
2828 ntrSignatureCompare(
2829   int * ptrX,
2830   int * ptrY)
2831 {
2832     if (signatures[*ptrY] > signatures[*ptrX]) return(1);
2833     if (signatures[*ptrY] < signatures[*ptrX]) return(-1);
2834     return(0);
2835
2836 } /* end of ntrSignatureCompare */
2837
2838
2839 /**Function********************************************************************
2840
2841   Synopsis    [Comparison function used by qsort.]
2842
2843   Description [Comparison function used by qsort to order the
2844   variables according to their signatures.]
2845
2846   SideEffects [None]
2847
2848 ******************************************************************************/
2849 static int
2850 ntrSignatureCompare2(
2851   int * ptrX,
2852   int * ptrY)
2853 {
2854     BnetNode *node;
2855     int x,y;
2856     if (!st_lookup(staticNet->hash,staticNet->latches[*ptrX][1],&node)) {
2857         return(0);
2858     }
2859     x = node->dd->index;
2860     if (!st_lookup(staticNet->hash,staticNet->latches[*ptrY][1],&node)) {
2861         return(0);
2862     }
2863     y = node->dd->index;
2864     if (signatures[x] < signatures[y]) return(1);
2865     if (signatures[x] > signatures[y]) return(-1);
2866     return(0);
2867
2868 } /* end of ntrSignatureCompare2 */
2869
2870
2871 /**Function********************************************************************
2872
2873   Synopsis    [Comparison function used by qsort.]
2874
2875   Description [Comparison function used by qsort to order the
2876   parts according to the BDD addresses.]
2877
2878   SideEffects [None]
2879
2880 ******************************************************************************/
2881 static int
2882 ntrPartCompare(
2883   int * ptrX,
2884   int * ptrY)
2885 {
2886     if (staticPart[*ptrY] > staticPart[*ptrX]) return(1);
2887     if (staticPart[*ptrY] < staticPart[*ptrX]) return(-1);
2888     return(0);
2889
2890 } /* end of ntrPartCompare */
2891
2892
2893 /**Function********************************************************************
2894
2895   Synopsis    [Allocates a matrix.]
2896
2897   Description [Allocates a matrix of char's. Returns a pointer to the matrix
2898   if successful; NULL otherwise.]
2899
2900   SideEffects [None]
2901
2902   SeeAlso     []
2903
2904 ******************************************************************************/
2905 static char **
2906 ntrAllocMatrix(
2907   int nrows,
2908   int ncols)
2909 {
2910     int i;
2911     char **matrix;
2912
2913     matrix = ALLOC(char *,nrows);
2914     if (matrix == NULL) return(NULL);
2915     matrix[0] = ALLOC(char,nrows * ncols);
2916     if (matrix[0] == NULL) {
2917         FREE(matrix);
2918         return(NULL);
2919     }
2920     for (i = 1; i < nrows; i++) {
2921         matrix[i] = matrix[i-1] + ncols;
2922     }
2923     for (i = 0; i < nrows * ncols; i++) {
2924         matrix[0][i] = 0;
2925     }
2926     return(matrix);
2927
2928 } /* end of ntrAllocMatrix */
2929
2930
2931 /**Function********************************************************************
2932
2933   Synopsis    [Frees a matrix of char's.]
2934
2935   Description []
2936
2937   SideEffects [None]
2938
2939   SeeAlso     []
2940
2941 ******************************************************************************/
2942 static void
2943 ntrFreeMatrix(
2944   char **matrix)
2945 {
2946     FREE(matrix[0]);
2947     FREE(matrix);
2948     return;
2949
2950 } /* end of ntrFreeMatrix */
2951
2952
2953 /**Function********************************************************************
2954
2955   Synopsis    [Sorts parts according to given permutation.]
2956
2957   Description []
2958
2959   SideEffects [The permutation arrays are turned into the identity
2960   permutations.]
2961
2962   SeeAlso     []
2963
2964 ******************************************************************************/
2965 static void
2966 ntrPermuteParts(
2967   DdNode **a,
2968   DdNode **b,
2969   int *comesFrom,
2970   int *goesTo,
2971   int size)
2972 {
2973     int i, j;
2974     DdNode *tmp;
2975
2976     for (i = 0; i < size; i++) {
2977         if (comesFrom[i] == i) continue;
2978         j = comesFrom[i];
2979         tmp = a[i]; a[i] = a[j]; a[j] = tmp;
2980         tmp = b[i]; b[i] = b[j]; b[j] = tmp;
2981         comesFrom[goesTo[i]] = j;
2982         comesFrom[i] = i;
2983         goesTo[j] = goesTo[i];
2984         goesTo[i] = i;
2985     }
2986     return;
2987
2988 } /* end of ntrPermuteParts */