distr/cudd/cuddZddMisc.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddMisc.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Miscellaneous utility functions for ZDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddDagSize()
  12                     <li> Cudd_zddCountMinterm()
  13                     <li> Cudd_zddPrintSubtable()
  14                     </ul>
  15                Internal procedures included in this module:
  16                     <ul>
  17                     </ul>
  18                Static procedures included in this module:
  19                     <ul>
  20                     <li> cuddZddDagInt()
  21                     </ul>
  22               ]
  23
  24   SeeAlso     []
  25
  26   Author      [Hyong-Kyoon Shin, In-Ho Moon]
  27
  28   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  29
  30   All rights reserved.
  31
  32   Redistribution and use in source and binary forms, with or without
  33   modification, are permitted provided that the following conditions
  34   are met:
  35
  36   Redistributions of source code must retain the above copyright
  37   notice, this list of conditions and the following disclaimer.
  38
  39   Redistributions in binary form must reproduce the above copyright
  40   notice, this list of conditions and the following disclaimer in the
  41   documentation and/or other materials provided with the distribution.
  42
  43   Neither the name of the University of Colorado nor the names of its
  44   contributors may be used to endorse or promote products derived from
  45   this software without specific prior written permission.
  46
  47   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  48   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  49   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  50   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  51   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  52   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  53   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  54   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  55   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  56   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  57   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  58   POSSIBILITY OF SUCH DAMAGE.]
  59
  60 ******************************************************************************/
  61
  62 #include <math.h>
  63 #include "util.h"
  64 #include "cuddInt.h"
  65
  66 /*---------------------------------------------------------------------------*/
  67 /* Constant declarations                                                     */
  68 /*---------------------------------------------------------------------------*/
  69
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Stucture declarations                                                     */
  73 /*---------------------------------------------------------------------------*/
  74
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Type declarations                                                         */
  78 /*---------------------------------------------------------------------------*/
  79
  80
  81 /*---------------------------------------------------------------------------*/
  82 /* Variable declarations                                                     */
  83 /*---------------------------------------------------------------------------*/
  84
  85 #ifndef lint
  86 static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.16 2009/02/20 02:14:58 fabio Exp $";
  87 #endif
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Macro declarations                                                        */
  91 /*---------------------------------------------------------------------------*/
  92
  93
  94 /**AutomaticStart*************************************************************/
  95
  96 /*---------------------------------------------------------------------------*/
  97 /* Static function prototypes                                                */
  98 /*---------------------------------------------------------------------------*/
  99
 100 static int cuddZddDagInt (DdNode *n, st_table *tab);
 101
 102 /**AutomaticEnd***************************************************************/
 103
 104
 105 /*---------------------------------------------------------------------------*/
 106 /* Definition of exported functions                                          */
 107 /*---------------------------------------------------------------------------*/
 108
 109
 110 /**Function********************************************************************
 111
 112   Synopsis    [Counts the number of nodes in a ZDD.]
 113
 114   Description [Counts the number of nodes in a ZDD. This function
 115   duplicates Cudd_DagSize and is only retained for compatibility.]
 116
 117   SideEffects [None]
 118
 119   SeeAlso     [Cudd_DagSize]
 120
 121 ******************************************************************************/
 122 int
 123 Cudd_zddDagSize(
 124   DdNode * p_node)
 125 {
 126
 127     int         i;
 128     st_table    *table;
 129
 130     table = st_init_table(st_ptrcmp, st_ptrhash);
 131     i = cuddZddDagInt(p_node, table);
 132     st_free_table(table);
 133     return(i);
 134
 135 } /* end of Cudd_zddDagSize */
 136
 137
 138 /**Function********************************************************************
 139
 140   Synopsis    [Counts the number of minterms of a ZDD.]
 141
 142   Description [Counts the number of minterms of the ZDD rooted at
 143   <code>node</code>. This procedure takes a parameter
 144   <code>path</code> that specifies how many variables are in the
 145   support of the function. If the procedure runs out of memory, it
 146   returns (double) CUDD_OUT_OF_MEM.]
 147
 148   SideEffects [None]
 149
 150   SeeAlso     [Cudd_zddCountDouble]
 151
 152 ******************************************************************************/
 153 double
 154 Cudd_zddCountMinterm(
 155   DdManager * zdd,
 156   DdNode * node,
 157   int  path)
 158 {
 159     double      dc_var, minterms;
 160
 161     dc_var = (double)((double)(zdd->sizeZ) - (double)path);
 162     minterms = Cudd_zddCountDouble(zdd, node) / pow(2.0, dc_var);
 163     return(minterms);
 164
 165 } /* end of Cudd_zddCountMinterm */
 166
 167
 168 /**Function********************************************************************
 169
 170   Synopsis    [Prints the ZDD table.]
 171
 172   Description [Prints the ZDD table for debugging purposes.]
 173
 174   SideEffects [None]
 175
 176   SeeAlso     []
 177
 178 ******************************************************************************/
 179 void
 180 Cudd_zddPrintSubtable(
 181   DdManager * table)
 182 {
 183     int         i, j;
 184     DdNode      *z1, *z1_next, *base;
 185     DdSubtable  *ZSubTable;
 186
 187     base = table->one;
 188     for (i = table->sizeZ - 1; i >= 0; i--) {
 189         ZSubTable = &(table->subtableZ[i]);
 190         printf("subtable[%d]:\n", i);
 191         for (j = ZSubTable->slots - 1; j >= 0; j--) {
 192             z1 = ZSubTable->nodelist[j];
 193             while (z1 != NIL(DdNode)) {
 194                 (void) fprintf(table->out,
 195 #if SIZEOF_VOID_P == 8
 196                     "ID = 0x%lx\tindex = %u\tr = %u\t",
 197                     (ptruint) z1 / (ptruint) sizeof(DdNode),
 198                     z1->index, z1->ref);
 199 #else
 200                     "ID = 0x%x\tindex = %hu\tr = %hu\t",
 201                     (ptruint) z1 / (ptruint) sizeof(DdNode),
 202                     z1->index, z1->ref);
 203 #endif
 204                 z1_next = cuddT(z1);
 205                 if (Cudd_IsConstant(z1_next)) {
 206                     (void) fprintf(table->out, "T = %d\t\t",
 207                         (z1_next == base));
 208                 }
 209                 else {
 210 #if SIZEOF_VOID_P == 8
 211                     (void) fprintf(table->out, "T = 0x%lx\t",
 212                         (ptruint) z1_next / (ptruint) sizeof(DdNode));
 213 #else
 214                     (void) fprintf(table->out, "T = 0x%x\t",
 215                         (ptruint) z1_next / (ptruint) sizeof(DdNode));
 216 #endif
 217                 }
 218                 z1_next = cuddE(z1);
 219                 if (Cudd_IsConstant(z1_next)) {
 220                     (void) fprintf(table->out, "E = %d\n",
 221                         (z1_next == base));
 222                 }
 223                 else {
 224 #if SIZEOF_VOID_P == 8
 225                     (void) fprintf(table->out, "E = 0x%lx\n",
 226                         (ptruint) z1_next / (ptruint) sizeof(DdNode));
 227 #else
 228                     (void) fprintf(table->out, "E = 0x%x\n",
 229                         (ptruint) z1_next / (ptruint) sizeof(DdNode));
 230 #endif
 231                 }
 232
 233                 z1_next = z1->next;
 234                 z1 = z1_next;
 235             }
 236         }
 237     }
 238     putchar('\n');
 239
 240 } /* Cudd_zddPrintSubtable */
 241
 242
 243 /*---------------------------------------------------------------------------*/
 244 /* Definition of static functions                                            */
 245 /*---------------------------------------------------------------------------*/
 246
 247
 248 /**Function********************************************************************
 249
 250   Synopsis    [Performs the recursive step of Cudd_zddDagSize.]
 251
 252   Description [Performs the recursive step of Cudd_zddDagSize. Does
 253   not check for out-of-memory conditions.]
 254
 255   SideEffects [None]
 256
 257   SeeAlso     []
 258
 259 ******************************************************************************/
 260 static int
 261 cuddZddDagInt(
 262   DdNode * n,
 263   st_table * tab)
 264 {
 265     if (n == NIL(DdNode))
 266         return(0);
 267
 268     if (st_is_member(tab, (char *)n) == 1)
 269         return(0);
 270
 271     if (Cudd_IsConstant(n))
 272         return(0);
 273
 274     (void)st_insert(tab, (char *)n, NIL(char));
 275     return(1 + cuddZddDagInt(cuddT(n), tab) +
 276         cuddZddDagInt(cuddE(n), tab));
 277
 278 } /* cuddZddDagInt */