distr/nanotrav/ntrZddTest.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [ntrZddTest.c]
   4
   5   PackageName [ntr]
   6
   7   Synopsis    [ZDD test functions.]
   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 #include "cuddInt.h"
  51
  52 /*---------------------------------------------------------------------------*/
  53 /* Constant declarations                                                     */
  54 /*---------------------------------------------------------------------------*/
  55
  56 /*---------------------------------------------------------------------------*/
  57 /* Stucture declarations                                                     */
  58 /*---------------------------------------------------------------------------*/
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Type declarations                                                         */
  62 /*---------------------------------------------------------------------------*/
  63
  64 /*---------------------------------------------------------------------------*/
  65 /* Variable declarations                                                     */
  66 /*---------------------------------------------------------------------------*/
  67
  68 #ifndef lint
  69 static char rcsid[] UTIL_UNUSED = "$Id: ntrZddTest.c,v 1.14 2004/08/13 18:28:28 fabio Exp fabio $";
  70 #endif
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Macro declarations                                                        */
  74 /*---------------------------------------------------------------------------*/
  75
  76 /**AutomaticStart*************************************************************/
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Static function prototypes                                                */
  80 /*---------------------------------------------------------------------------*/
  81
  82 static int reorderZdd (BnetNetwork *net, DdManager *dd, NtrOptions *option);
  83
  84 /**AutomaticEnd***************************************************************/
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Definition of exported functions                                          */
  88 /*---------------------------------------------------------------------------*/
  89
  90
  91 /**Function********************************************************************
  92
  93   Synopsis    [Tests ZDDs.]
  94
  95   Description [Tests ZDDs. Returns 1 if successful; 0 otherwise.]
  96
  97   SideEffects [Creates ZDD variables in the manager.]
  98
  99   SeeAlso     []
 100
 101 ******************************************************************************/
 102 int
 103 Ntr_testZDD(
 104   DdManager * dd,
 105   BnetNetwork * net,
 106   NtrOptions * option)
 107 {
 108     DdNode **zdd;               /* array of converted outputs */
 109     int nz;                     /* actual number of ZDDs */
 110     int result;
 111     int i, j;
 112     BnetNode *node;             /* auxiliary pointer to network node */
 113     int pr = option->verb;
 114     int level;                  /* aux. var. used to print variable orders */
 115     char **names;               /* array used to print variable orders */
 116     int nvars;
 117
 118     /* Build an array of ZDDs for the output functions or for the
 119     ** specified node. */
 120     Cudd_AutodynDisable(dd);
 121     Cudd_AutodynDisableZdd(dd);
 122     zdd = ALLOC(DdNode *,net->noutputs);
 123     result = Cudd_zddVarsFromBddVars(dd,1);
 124     if (result == 0) return(0);
 125     if (option->node == NULL) {
 126         for (nz = 0; nz < net->noutputs; nz++) {
 127             if (!st_lookup(net->hash,net->outputs[nz],&node)) {
 128                 return(0);
 129             }
 130             zdd[nz] = Cudd_zddPortFromBdd(dd, node->dd);
 131             if (zdd[nz]) {
 132                 Cudd_Ref(zdd[nz]);
 133                 (void) printf("%s", node->name);
 134                 result = Cudd_zddPrintDebug(dd,zdd[nz],Cudd_ReadZddSize(dd),pr);
 135                 if (result == 0) return(0);
 136             } else {
 137                 (void) printf("Conversion to ZDD failed.\n");
 138             }
 139         }
 140     } else {
 141         if (!st_lookup(net->hash,option->node,&node)) {
 142             return(0);
 143         }
 144         zdd[0] = Cudd_zddPortFromBdd(dd, node->dd);
 145         if (zdd[0]) {
 146             Cudd_Ref(zdd[0]);
 147             (void) printf("%s", node->name);
 148             result = Cudd_zddPrintDebug(dd,zdd[0],Cudd_ReadZddSize(dd),pr);
 149             if (result == 0) return(0);
 150         } else {
 151             (void) printf("Conversion to ZDD failed.\n");
 152         }
 153         nz = 1;
 154     }
 155
 156 #ifdef DD_DEBUG
 157     result = Cudd_CheckKeys(dd);
 158     if (result != 0) {
 159         (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
 160         return(0);
 161     }
 162 #endif
 163
 164     if (option->autoDyn & 1) {
 165         Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
 166     }
 167     if (option->autoDyn & 2) {
 168         Cudd_AutodynEnableZdd(dd,CUDD_REORDER_SAME);
 169     }
 170
 171     /* Convert the ZDDs back to BDDs and check identity. */
 172     for (i = 0; i < nz; i++) {
 173         DdNode *checkBdd;
 174         checkBdd = Cudd_zddPortToBdd(dd,zdd[i]);
 175         if (checkBdd) {
 176             Cudd_Ref(checkBdd);
 177             if (option->node == NULL) {
 178                 if (!st_lookup(net->hash,net->outputs[i],&node)) {
 179                     return(0);
 180                 }
 181             } else {
 182                 if (!st_lookup(net->hash,option->node,&node)) {
 183                     return(0);
 184                 }
 185             }
 186             if (checkBdd != node->dd) {
 187                 (void) fprintf(stdout,"Equivalence failed at node %s",
 188                                node->name);
 189                 result = Cudd_PrintDebug(dd,checkBdd,Cudd_ReadZddSize(dd),pr);
 190                 if (result == 0) return(0);
 191             }
 192             Cudd_RecursiveDeref(dd,checkBdd);
 193         } else {
 194             (void) printf("Conversion to BDD failed.\n");
 195         }
 196     }
 197
 198 #ifdef DD_DEBUG
 199     result = Cudd_CheckKeys(dd);
 200     if (result != 0) {
 201         (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
 202         return(0);
 203     }
 204 #endif
 205
 206     /* Play with the ZDDs a little. */
 207     if (nz > 2) {
 208         DdNode *f;
 209         DdNode *g1, *g2, *g;
 210         f = Cudd_zddIte(dd,zdd[0],zdd[1],zdd[2]);
 211         if (f == NULL) return(0);
 212         cuddRef(f);
 213         g1 = Cudd_zddIntersect(dd,zdd[0],zdd[1]);
 214         if (g1 == NULL) {
 215             Cudd_RecursiveDerefZdd(dd,f);
 216             return(0);
 217         }
 218         cuddRef(g1);
 219         g2 = Cudd_zddDiff(dd,zdd[2],zdd[0]);
 220         if (g2 == NULL) {
 221             Cudd_RecursiveDerefZdd(dd,f);
 222             Cudd_RecursiveDerefZdd(dd,g1);
 223             return(0);
 224         }
 225         cuddRef(g2);
 226         g = Cudd_zddUnion(dd,g1,g2);
 227         if (g == NULL) {
 228             Cudd_RecursiveDerefZdd(dd,f);
 229             Cudd_RecursiveDerefZdd(dd,g1);
 230             Cudd_RecursiveDerefZdd(dd,g2);
 231             return(0);
 232         }
 233         cuddRef(g);
 234         Cudd_RecursiveDerefZdd(dd,g1);
 235         Cudd_RecursiveDerefZdd(dd,g2);
 236         if (g != f) {
 237             (void) fprintf(stderr,"f != g!\n");
 238         }
 239         Cudd_RecursiveDerefZdd(dd,g);
 240         Cudd_RecursiveDerefZdd(dd,f);
 241     }
 242
 243 #ifdef DD_DEBUG
 244     result = Cudd_CheckKeys(dd);
 245     if (result != 0) {
 246         (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
 247         return(0);
 248     }
 249 #endif
 250
 251     /* Perform ZDD reordering. */
 252     result = reorderZdd(net,dd,option);
 253     if (result == 0) return(0);
 254
 255     /* Print final ZDD order. */
 256     nvars = Cudd_ReadZddSize(dd);
 257     names = ALLOC(char *, nvars);
 258     if (names == NULL) return(0);
 259     for (i = 0; i < nvars; i++) {
 260         names[i] = NULL;
 261     }
 262     if (option->reordering != CUDD_REORDER_NONE) {
 263         for (i = 0; i < net->npis; i++) {
 264             if (!st_lookup(net->hash,net->inputs[i],&node)) {
 265                 FREE(names);
 266                 return(0);
 267             }
 268             level = Cudd_ReadPermZdd(dd,node->var);
 269             names[level] = node->name;
 270         }
 271         for (i = 0; i < net->nlatches; i++) {
 272             if (!st_lookup(net->hash,net->latches[i][1],&node)) {
 273                 FREE(names);
 274                 return(0);
 275             }
 276             level = Cudd_ReadPermZdd(dd,node->var);
 277             names[level] = node->name;
 278         }
 279         (void) printf("New order\n");
 280         for (i = 0, j = 0; i < nvars; i++) {
 281             if (names[i] == NULL) continue;
 282             if((j%8 == 0)&&j) (void) printf("\n");
 283             (void) printf("%s ",names[i]);
 284             j++;
 285         }
 286         (void) printf("\n");
 287     }
 288     FREE(names);
 289
 290     /* Dispose of ZDDs. */
 291     for (i = 0; i < nz; i++) {
 292         Cudd_RecursiveDerefZdd(dd,zdd[i]);
 293     }
 294     FREE(zdd);
 295     return(1);
 296
 297 } /* end of Ntr_testZDD */
 298
 299
 300 /**Function********************************************************************
 301
 302   Synopsis    [Builds ZDD covers.]
 303
 304   Description []
 305
 306   SideEffects [Creates ZDD variables in the manager.]
 307
 308   SeeAlso     []
 309
 310 ******************************************************************************/
 311 int
 312 Ntr_testISOP(
 313   DdManager * dd,
 314   BnetNetwork * net,
 315   NtrOptions * option)
 316 {
 317     DdNode **zdd;               /* array of converted outputs */
 318     DdNode *bdd;                /* return value of Cudd_zddIsop */
 319     int nz;                     /* actual number of ZDDs */
 320     int result;
 321     int i;
 322     BnetNode *node;             /* auxiliary pointer to network node */
 323     int pr = option->verb;
 324
 325     /* Build an array of ZDDs for the output functions or the specified
 326     ** node. */
 327     Cudd_zddRealignEnable(dd);
 328     Cudd_AutodynDisableZdd(dd);
 329     zdd = ALLOC(DdNode *,net->noutputs);
 330     result = Cudd_zddVarsFromBddVars(dd,2);
 331     if (result == 0) return(0);
 332     if (option->node == NULL) {
 333         nz = net->noutputs;
 334         for (i = 0; i < nz; i++) {
 335             if (!st_lookup(net->hash,net->outputs[i],&node)) {
 336                 return(0);
 337             }
 338             bdd = Cudd_zddIsop(dd, node->dd, node->dd, &zdd[i]);
 339             if (bdd != node->dd) return(0);
 340             Cudd_Ref(bdd);
 341             Cudd_RecursiveDeref(dd,bdd);
 342             if (zdd[i]) {
 343                 Cudd_Ref(zdd[i]);
 344                 (void) printf("%s", node->name);
 345                 result = Cudd_zddPrintDebug(dd,zdd[i],Cudd_ReadZddSize(dd),pr);
 346                 if (result == 0) return(0);
 347                 if (option->printcover) {
 348                     int *path;
 349                     DdGen *gen;
 350                     char *str = ALLOC(char,Cudd_ReadSize(dd)+1);
 351                     if (str == NULL) return(0);
 352                     (void) printf("Testing iterator on ZDD paths:\n");
 353                     Cudd_zddForeachPath(dd,zdd[i],gen,path) {
 354                         str = Cudd_zddCoverPathToString(dd,path,str);
 355                         (void) printf("%s 1\n", str);
 356                     }
 357                     (void) printf("\n");
 358                     FREE(str);
 359                     result = Cudd_zddPrintCover(dd,zdd[i]);
 360
 361                     if (result == 0) return(0);
 362                 }
 363             } else {
 364                 (void) printf("Conversion to ISOP failed.\n");
 365                 return(0);
 366             }
 367         }
 368     } else {
 369         nz = 1;
 370         if (!st_lookup(net->hash,option->node,&node)) {
 371             return(0);
 372         }
 373         bdd = Cudd_zddIsop(dd, node->dd, node->dd, &zdd[0]);
 374         if (bdd != node->dd) return(0);
 375         Cudd_Ref(bdd);
 376         Cudd_RecursiveDeref(dd,bdd);
 377         if (zdd[0]) {
 378             Cudd_Ref(zdd[0]);
 379             (void) printf("%s", node->name);
 380             result = Cudd_zddPrintDebug(dd,zdd[0],Cudd_ReadZddSize(dd),pr);
 381             if (result == 0) return(0);
 382             if (option->printcover) {
 383                 int *path;
 384                 DdGen *gen;
 385                 char *str = ALLOC(char,Cudd_ReadSize(dd)+1);
 386                 if (str == NULL) return(0);
 387                 (void) printf("Testing iterator on ZDD paths:\n");
 388                 Cudd_zddForeachPath(dd,zdd[0],gen,path) {
 389                     str = Cudd_zddCoverPathToString(dd,path,str);
 390                     (void) printf("%s 1\n", str);
 391                 }
 392                 (void) printf("\n");
 393                 FREE(str);
 394
 395                 result = Cudd_zddPrintCover(dd,zdd[0]);
 396                 if (result == 0) return(0);
 397             }
 398         } else {
 399             (void) printf("Conversion to ISOP failed.\n");
 400             return(0);
 401         }
 402     }
 403     if (option->autoDyn) {
 404         Cudd_AutodynEnableZdd(dd,CUDD_REORDER_SAME);
 405     }
 406
 407     /* Perform ZDD reordering. */
 408     result = reorderZdd(net,dd,option);
 409     if (result == 0) return(0);
 410
 411     /* Dispose of ZDDs. */
 412     for (i = 0; i < nz; i++) {
 413         Cudd_RecursiveDerefZdd(dd,zdd[i]);
 414     }
 415     FREE(zdd);
 416
 417     return(1);
 418
 419 } /* end of Ntr_testISOP */
 420
 421
 422 /*---------------------------------------------------------------------------*/
 423 /* Definition of internal functions                                          */
 424 /*---------------------------------------------------------------------------*/
 425
 426 /*---------------------------------------------------------------------------*/
 427 /* Definition of static functions                                            */
 428 /*---------------------------------------------------------------------------*/
 429
 430
 431 /**Function********************************************************************
 432
 433   Synopsis    [Applies reordering to the ZDDs.]
 434
 435   Description [Explicitly applies reordering to the ZDDs. Returns 1 if
 436   successful; 0 otherwise.]
 437
 438   SideEffects [None]
 439
 440   SeeAlso     []
 441
 442 *****************************************************************************/
 443 static int
 444 reorderZdd(
 445   BnetNetwork * net,
 446   DdManager * dd /* DD Manager */,
 447   NtrOptions * option)
 448 {
 449     int result;                 /* return value from functions */
 450
 451     /* Perform the final reordering. */
 452     if (option->reordering != CUDD_REORDER_NONE) {
 453         (void) printf("Number of inputs = %d\n",net->ninputs);
 454
 455         dd->siftMaxVar = 1000000;
 456         result = Cudd_zddReduceHeap(dd,option->reordering,1);
 457         if (result == 0) return(0);
 458
 459         /* Print symmetry stats if pertinent */
 460         if (option->reordering == CUDD_REORDER_SYMM_SIFT ||
 461             option->reordering == CUDD_REORDER_SYMM_SIFT_CONV)
 462             Cudd_zddSymmProfile(dd, 0, dd->sizeZ - 1);
 463     }
 464
 465     return(1);
 466
 467 } /* end of reorderZdd */
 468