abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddUtil.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddUtil.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Utility functions.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_PrintMinterm()
12  <li> Cudd_bddPrintCover()
13  <li> Cudd_PrintDebug()
14  <li> Cudd_DagSize()
15  <li> Cudd_EstimateCofactor()
16  <li> Cudd_EstimateCofactorSimple()
17  <li> Cudd_SharingSize()
18  <li> Cudd_CountMinterm()
19  <li> Cudd_EpdCountMinterm()
20  <li> Cudd_CountPath()
21  <li> Cudd_CountPathsToNonZero()
22  <li> Cudd_Support()
23  <li> Cudd_SupportIndex()
24  <li> Cudd_SupportSize()
25  <li> Cudd_VectorSupport()
26  <li> Cudd_VectorSupportIndex()
27  <li> Cudd_VectorSupportSize()
28  <li> Cudd_ClassifySupport()
29  <li> Cudd_CountLeaves()
30  <li> Cudd_bddPickOneCube()
31  <li> Cudd_bddPickOneMinterm()
32  <li> Cudd_bddPickArbitraryMinterms()
33  <li> Cudd_SubsetWithMaskVars()
34  <li> Cudd_FirstCube()
35  <li> Cudd_NextCube()
36  <li> Cudd_bddComputeCube()
37  <li> Cudd_addComputeCube()
38  <li> Cudd_FirstNode()
39  <li> Cudd_NextNode()
40  <li> Cudd_GenFree()
41  <li> Cudd_IsGenEmpty()
42  <li> Cudd_IndicesToCube()
43  <li> Cudd_PrintVersion()
44  <li> Cudd_AverageDistance()
45  <li> Cudd_Random()
46  <li> Cudd_Srandom()
47  <li> Cudd_Density()
48  </ul>
49  Internal procedures included in this module:
50  <ul>
51  <li> cuddP()
52  <li> cuddStCountfree()
53  <li> cuddCollectNodes()
54  <li> cuddNodeArray()
55  </ul>
56  Static procedures included in this module:
57  <ul>
58  <li> dp2()
59  <li> ddPrintMintermAux()
60  <li> ddDagInt()
61  <li> ddCountMintermAux()
62  <li> ddEpdCountMintermAux()
63  <li> ddCountPathAux()
64  <li> ddSupportStep()
65  <li> ddClearFlag()
66  <li> ddLeavesInt()
67  <li> ddPickArbitraryMinterms()
68  <li> ddPickRepresentativeCube()
69  <li> ddEpdFree()
70  </ul>]
71 
72  Author [Fabio Somenzi]
73 
74  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
75 
76  All rights reserved.
77 
78  Redistribution and use in source and binary forms, with or without
79  modification, are permitted provided that the following conditions
80  are met:
81 
82  Redistributions of source code must retain the above copyright
83  notice, this list of conditions and the following disclaimer.
84 
85  Redistributions in binary form must reproduce the above copyright
86  notice, this list of conditions and the following disclaimer in the
87  documentation and/or other materials provided with the distribution.
88 
89  Neither the name of the University of Colorado nor the names of its
90  contributors may be used to endorse or promote products derived from
91  this software without specific prior written permission.
92 
93  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
94  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
95  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
96  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
97  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
98  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
99  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
100  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
101  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
102  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
103  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
104  POSSIBILITY OF SUCH DAMAGE.]
105 
106 ******************************************************************************/
107 
108 #include "misc/util/util_hack.h"
109 #include "cuddInt.h"
110 
111 ABC_NAMESPACE_IMPL_START
112 
113 
114 
115 /*---------------------------------------------------------------------------*/
116 /* Constant declarations */
117 /*---------------------------------------------------------------------------*/
118 
119 /* Random generator constants. */
120 #define MODULUS1 2147483563
121 #define LEQA1 40014
122 #define LEQQ1 53668
123 #define LEQR1 12211
124 #define MODULUS2 2147483399
125 #define LEQA2 40692
126 #define LEQQ2 52774
127 #define LEQR2 3791
128 #define STAB_SIZE 64
129 #define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
130 
131 /*---------------------------------------------------------------------------*/
132 /* Stucture declarations */
133 /*---------------------------------------------------------------------------*/
134 
135 /*---------------------------------------------------------------------------*/
136 /* Type declarations */
137 /*---------------------------------------------------------------------------*/
138 
139 
140 /*---------------------------------------------------------------------------*/
141 /* Variable declarations */
142 /*---------------------------------------------------------------------------*/
143 
144 #ifndef lint
145 static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $";
146 #endif
147 
148 static DdNode *background, *zero;
149 
150 static long cuddRand = 0;
151 static long cuddRand2;
152 static long shuffleSelect;
153 static long shuffleTable[STAB_SIZE];
154 
155 /*---------------------------------------------------------------------------*/
156 /* Macro declarations */
157 /*---------------------------------------------------------------------------*/
158 
159 #define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
160 
161 #ifdef __cplusplus
162 extern "C" {
163 #endif
164 
165 /**AutomaticStart*************************************************************/
166 
167 /*---------------------------------------------------------------------------*/
168 /* Static function prototypes */
169 /*---------------------------------------------------------------------------*/
170 
171 static int dp2 (DdManager *dd, DdNode *f, st__table *t);
172 static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
173 static int ddDagInt (DdNode *n);
174 static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
175 static int cuddEstimateCofactor (DdManager *dd, st__table *table, DdNode * node, int i, int phase, DdNode ** ptr);
176 static DdNode * cuddUniqueLookup (DdManager * unique, int index, DdNode * T, DdNode * E);
177 static int cuddEstimateCofactorSimple (DdNode * node, int i);
178 static double ddCountMintermAux (DdNode *node, double max, DdHashTable *table);
179 static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st__table *table);
180 static double ddCountPathAux (DdNode *node, st__table *table);
181 static double ddCountPathsToNonZero (DdNode * N, st__table * table);
182 static void ddSupportStep (DdNode *f, int *support);
183 static void ddClearFlag (DdNode *f);
184 static int ddLeavesInt (DdNode *n);
185 static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
186 static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
187 static enum st__retval ddEpdFree (char * key, char * value, char * arg);
188 
189 /**AutomaticEnd***************************************************************/
190 
191 #ifdef __cplusplus
192 }
193 #endif
194 
195 /*---------------------------------------------------------------------------*/
196 /* Definition of exported functions */
197 /*---------------------------------------------------------------------------*/
198 
199 
200 /**Function********************************************************************
201 
202  Synopsis [Prints a disjoint sum of products.]
203 
204  Description [Prints a disjoint sum of product cover for the function
205  rooted at node. Each product corresponds to a path from node to a
206  leaf node different from the logical zero, and different from the
207  background value. Uses the package default output file. Returns 1
208  if successful; 0 otherwise.]
209 
210  SideEffects [None]
211 
212  SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover]
213 
214 ******************************************************************************/
215 int
216 Cudd_PrintMinterm(
217  DdManager * manager,
218  DdNode * node)
219 {
220  int i, *list;
221 
222  background = manager->background;
223  zero = Cudd_Not(manager->one);
224  list = ABC_ALLOC(int,manager->size);
225  if (list == NULL) {
226  manager->errorCode = CUDD_MEMORY_OUT;
227  return(0);
228  }
229  for (i = 0; i < manager->size; i++) list[i] = 2;
230  ddPrintMintermAux(manager,node,list);
231  ABC_FREE(list);
232  return(1);
233 
234 } /* end of Cudd_PrintMinterm */
235 
236 
237 /**Function********************************************************************
238 
239  Synopsis [Prints a sum of prime implicants of a BDD.]
240 
241  Description [Prints a sum of product cover for an incompletely
242  specified function given by a lower bound and an upper bound. Each
243  product is a prime implicant obtained by expanding the product
244  corresponding to a path from node to the constant one. Uses the
245  package default output file. Returns 1 if successful; 0 otherwise.]
246 
247  SideEffects [None]
248 
249  SeeAlso [Cudd_PrintMinterm]
250 
251 ******************************************************************************/
252 int
253 Cudd_bddPrintCover(
254  DdManager *dd,
255  DdNode *l,
256  DdNode *u)
257 {
258  int *array;
259  int q, result;
260  DdNode *lb;
261 #ifdef DD_DEBUG
262  DdNode *cover;
263 #endif
264 
265  array = ABC_ALLOC(int, Cudd_ReadSize(dd));
266  if (array == NULL) return(0);
267  lb = l;
268  cuddRef(lb);
269 #ifdef DD_DEBUG
270  cover = Cudd_ReadLogicZero(dd);
271  cuddRef(cover);
272 #endif
273  while (lb != Cudd_ReadLogicZero(dd)) {
274  DdNode *implicant, *prime, *tmp;
275  int length;
276  implicant = Cudd_LargestCube(dd,lb,&length);
277  if (implicant == NULL) {
278  Cudd_RecursiveDeref(dd,lb);
279  ABC_FREE(array);
280  return(0);
281  }
282  cuddRef(implicant);
283  prime = Cudd_bddMakePrime(dd,implicant,u);
284  if (prime == NULL) {
285  Cudd_RecursiveDeref(dd,lb);
286  Cudd_RecursiveDeref(dd,implicant);
287  ABC_FREE(array);
288  return(0);
289  }
290  cuddRef(prime);
291  Cudd_RecursiveDeref(dd,implicant);
292  tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
293  if (tmp == NULL) {
294  Cudd_RecursiveDeref(dd,lb);
295  Cudd_RecursiveDeref(dd,prime);
296  ABC_FREE(array);
297  return(0);
298  }
299  cuddRef(tmp);
300  Cudd_RecursiveDeref(dd,lb);
301  lb = tmp;
302  result = Cudd_BddToCubeArray(dd,prime,array);
303  if (result == 0) {
304  Cudd_RecursiveDeref(dd,lb);
305  Cudd_RecursiveDeref(dd,prime);
306  ABC_FREE(array);
307  return(0);
308  }
309  for (q = 0; q < dd->size; q++) {
310  switch (array[q]) {
311  case 0:
312  (void) fprintf(dd->out, "0");
313  break;
314  case 1:
315  (void) fprintf(dd->out, "1");
316  break;
317  case 2:
318  (void) fprintf(dd->out, "-");
319  break;
320  default:
321  (void) fprintf(dd->out, "?");
322  }
323  }
324  (void) fprintf(dd->out, " 1\n");
325 #ifdef DD_DEBUG
326  tmp = Cudd_bddOr(dd,prime,cover);
327  if (tmp == NULL) {
328  Cudd_RecursiveDeref(dd,cover);
329  Cudd_RecursiveDeref(dd,lb);
330  Cudd_RecursiveDeref(dd,prime);
331  ABC_FREE(array);
332  return(0);
333  }
334  cuddRef(tmp);
335  Cudd_RecursiveDeref(dd,cover);
336  cover = tmp;
337 #endif
338  Cudd_RecursiveDeref(dd,prime);
339  }
340  (void) fprintf(dd->out, "\n");
341  Cudd_RecursiveDeref(dd,lb);
342  ABC_FREE(array);
343 #ifdef DD_DEBUG
344  if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
345  Cudd_RecursiveDeref(dd,cover);
346  return(0);
347  }
348  Cudd_RecursiveDeref(dd,cover);
349 #endif
350  return(1);
351 
352 } /* end of Cudd_bddPrintCover */
353 
354 
355 /**Function********************************************************************
356 
357  Synopsis [Prints to the standard output a DD and its statistics.]
358 
359  Description [Prints to the standard output a DD and its statistics.
360  The statistics include the number of nodes, the number of leaves, and
361  the number of minterms. (The number of minterms is the number of
362  assignments to the variables that cause the function to be different
363  from the logical zero (for BDDs) and from the background value (for
364  ADDs.) The statistics are printed if pr &gt; 0. Specifically:
365  <ul>
366  <li> pr = 0 : prints nothing
367  <li> pr = 1 : prints counts of nodes and minterms
368  <li> pr = 2 : prints counts + disjoint sum of product
369  <li> pr = 3 : prints counts + list of nodes
370  <li> pr &gt; 3 : prints counts + disjoint sum of product + list of nodes
371  </ul>
372  For the purpose of counting the number of minterms, the function is
373  supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]
374 
375  SideEffects [None]
376 
377  SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
378  Cudd_PrintMinterm]
379 
380 ******************************************************************************/
381 int
382 Cudd_PrintDebug(
383  DdManager * dd,
384  DdNode * f,
385  int n,
386  int pr)
387 {
388  DdNode *azero, *bzero;
389  int nodes;
390  int leaves;
391  double minterms;
392  int retval = 1;
393 
394  if (f == NULL) {
395  (void) fprintf(dd->out,": is the NULL DD\n");
396  (void) fflush(dd->out);
397  return(0);
398  }
399  azero = DD_ZERO(dd);
400  bzero = Cudd_Not(DD_ONE(dd));
401  if ((f == azero || f == bzero) && pr > 0){
402  (void) fprintf(dd->out,": is the zero DD\n");
403  (void) fflush(dd->out);
404  return(1);
405  }
406  if (pr > 0) {
407  nodes = Cudd_DagSize(f);
408  if (nodes == CUDD_OUT_OF_MEM) retval = 0;
409  leaves = Cudd_CountLeaves(f);
410  if (leaves == CUDD_OUT_OF_MEM) retval = 0;
411  minterms = Cudd_CountMinterm(dd, f, n);
412  if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
413  (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
414  nodes, leaves, minterms);
415  if (pr > 2) {
416  if (!cuddP(dd, f)) retval = 0;
417  }
418  if (pr == 2 || pr > 3) {
419  if (!Cudd_PrintMinterm(dd,f)) retval = 0;
420  (void) fprintf(dd->out,"\n");
421  }
422  (void) fflush(dd->out);
423  }
424  return(retval);
425 
426 } /* end of Cudd_PrintDebug */
427 
428 
429 /**Function********************************************************************
430 
431  Synopsis [Counts the number of nodes in a DD.]
432 
433  Description [Counts the number of nodes in a DD. Returns the number
434  of nodes in the graph rooted at node.]
435 
436  SideEffects [None]
437 
438  SeeAlso [Cudd_SharingSize Cudd_PrintDebug]
439 
440 ******************************************************************************/
441 int
442 Cudd_DagSize(
443  DdNode * node)
444 {
445  int i;
446 
447  i = ddDagInt(Cudd_Regular(node));
448  ddClearFlag(Cudd_Regular(node));
449 
450  return(i);
451 
452 } /* end of Cudd_DagSize */
453 
454 
455 /**Function********************************************************************
456 
457  Synopsis [Estimates the number of nodes in a cofactor of a DD.]
458 
459  Description [Estimates the number of nodes in a cofactor of a DD.
460  Returns an estimate of the number of nodes in a cofactor of
461  the graph rooted at node with respect to the variable whose index is i.
462  In case of failure, returns CUDD_OUT_OF_MEM.
463  This function uses a refinement of the algorithm of Cabodi et al.
464  (ICCAD96). The refinement allows the procedure to account for part
465  of the recombination that may occur in the part of the cofactor above
466  the cofactoring variable. This procedure does no create any new node.
467  It does keep a small table of results; therefore it may run out of memory.
468  If this is a concern, one should use Cudd_EstimateCofactorSimple, which
469  is faster, does not allocate any memory, but is less accurate.]
470 
471  SideEffects [None]
472 
473  SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple]
474 
475 ******************************************************************************/
476 int
477 Cudd_EstimateCofactor(
478  DdManager *dd /* manager */,
479  DdNode * f /* function */,
480  int i /* index of variable */,
481  int phase /* 1: positive; 0: negative */
482  )
483 {
484  int val;
485  DdNode *ptr;
486  st__table *table;
487 
488  table = st__init_table( st__ptrcmp, st__ptrhash);
489  if (table == NULL) return(CUDD_OUT_OF_MEM);
490  val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
491  ddClearFlag(Cudd_Regular(f));
492  st__free_table(table);
493 
494  return(val);
495 
496 } /* end of Cudd_EstimateCofactor */
497 
498 
499 /**Function********************************************************************
500 
501  Synopsis [Estimates the number of nodes in a cofactor of a DD.]
502 
503  Description [Estimates the number of nodes in a cofactor of a DD.
504  Returns an estimate of the number of nodes in the positive cofactor of
505  the graph rooted at node with respect to the variable whose index is i.
506  This procedure implements with minor changes the algorithm of Cabodi et al.
507  (ICCAD96). It does not allocate any memory, it does not change the
508  state of the manager, and it is fast. However, it has been observed to
509  overestimate the size of the cofactor by as much as a factor of 2.]
510 
511  SideEffects [None]
512 
513  SeeAlso [Cudd_DagSize]
514 
515 ******************************************************************************/
516 int
517 Cudd_EstimateCofactorSimple(
518  DdNode * node,
519  int i)
520 {
521  int val;
522 
523  val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
524  ddClearFlag(Cudd_Regular(node));
525 
526  return(val);
527 
528 } /* end of Cudd_EstimateCofactorSimple */
529 
530 
531 /**Function********************************************************************
532 
533  Synopsis [Counts the number of nodes in an array of DDs.]
534 
535  Description [Counts the number of nodes in an array of DDs. Shared
536  nodes are counted only once. Returns the total number of nodes.]
537 
538  SideEffects [None]
539 
540  SeeAlso [Cudd_DagSize]
541 
542 ******************************************************************************/
543 int
544 Cudd_SharingSize(
545  DdNode ** nodeArray,
546  int n)
547 {
548  int i,j;
549 
550  i = 0;
551  for (j = 0; j < n; j++) {
552  i += ddDagInt(Cudd_Regular(nodeArray[j]));
553  }
554  for (j = 0; j < n; j++) {
555  ddClearFlag(Cudd_Regular(nodeArray[j]));
556  }
557  return(i);
558 
559 } /* end of Cudd_SharingSize */
560 
561 
562 /**Function********************************************************************
563 
564  Synopsis [Counts the number of minterms of a DD.]
565 
566  Description [Counts the number of minterms of a DD. The function is
567  assumed to depend on nvars variables. The minterm count is
568  represented as a double, to allow for a larger number of variables.
569  Returns the number of minterms of the function rooted at node if
570  successful; (double) CUDD_OUT_OF_MEM otherwise.]
571 
572  SideEffects [None]
573 
574  SeeAlso [Cudd_PrintDebug Cudd_CountPath]
575 
576 ******************************************************************************/
577 double
578 Cudd_CountMinterm(
579  DdManager * manager,
580  DdNode * node,
581  int nvars)
582 {
583  double max;
584  DdHashTable *table;
585  double res;
586  CUDD_VALUE_TYPE epsilon;
587 
588  background = manager->background;
589  zero = Cudd_Not(manager->one);
590 
591  max = pow(2.0,(double)nvars);
592  table = cuddHashTableInit(manager,1,2);
593  if (table == NULL) {
594  return((double)CUDD_OUT_OF_MEM);
595  }
596  epsilon = Cudd_ReadEpsilon(manager);
597  Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
598  res = ddCountMintermAux(node,max,table);
599  cuddHashTableQuit(table);
600  Cudd_SetEpsilon(manager,epsilon);
601 
602  return(res);
603 
604 } /* end of Cudd_CountMinterm */
605 
606 
607 /**Function********************************************************************
608 
609  Synopsis [Counts the number of paths of a DD.]
610 
611  Description [Counts the number of paths of a DD. Paths to all
612  terminal nodes are counted. The path count is represented as a
613  double, to allow for a larger number of variables. Returns the
614  number of paths of the function rooted at node if successful;
615  (double) CUDD_OUT_OF_MEM otherwise.]
616 
617  SideEffects [None]
618 
619  SeeAlso [Cudd_CountMinterm]
620 
621 ******************************************************************************/
622 double
623 Cudd_CountPath(
624  DdNode * node)
625 {
626 
627  st__table *table;
628  double i;
629 
630  table = st__init_table( st__ptrcmp, st__ptrhash);
631  if (table == NULL) {
632  return((double)CUDD_OUT_OF_MEM);
633  }
634  i = ddCountPathAux(Cudd_Regular(node),table);
635  st__foreach(table, cuddStCountfree, NULL);
636  st__free_table(table);
637  return(i);
638 
639 } /* end of Cudd_CountPath */
640 
641 
642 /**Function********************************************************************
643 
644  Synopsis [Counts the number of minterms of a DD with extended precision.]
645 
646  Description [Counts the number of minterms of a DD with extended precision.
647  The function is assumed to depend on nvars variables. The minterm count is
648  represented as an EpDouble, to allow any number of variables.
649  Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]
650 
651  SideEffects [None]
652 
653  SeeAlso [Cudd_PrintDebug Cudd_CountPath]
654 
655 ******************************************************************************/
656 int
657 Cudd_EpdCountMinterm(
658  DdManager * manager,
659  DdNode * node,
660  int nvars,
661  EpDouble * epd)
662 {
663  EpDouble max, tmp;
664  st__table *table;
665  int status;
666 
667  background = manager->background;
668  zero = Cudd_Not(manager->one);
669 
670  EpdPow2(nvars, &max);
671  table = st__init_table(EpdCmp, st__ptrhash);
672  if (table == NULL) {
673  EpdMakeZero(epd, 0);
674  return(CUDD_OUT_OF_MEM);
675  }
676  status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
677  st__foreach(table, ddEpdFree, NULL);
678  st__free_table(table);
679  if (status == CUDD_OUT_OF_MEM) {
680  EpdMakeZero(epd, 0);
681  return(CUDD_OUT_OF_MEM);
682  }
683  if (Cudd_IsComplement(node)) {
684  EpdSubtract3(&max, epd, &tmp);
685  EpdCopy(&tmp, epd);
686  }
687  return(0);
688 
689 } /* end of Cudd_EpdCountMinterm */
690 
691 
692 /**Function********************************************************************
693 
694  Synopsis [Counts the number of paths to a non-zero terminal of a DD.]
695 
696  Description [Counts the number of paths to a non-zero terminal of a
697  DD. The path count is
698  represented as a double, to allow for a larger number of variables.
699  Returns the number of paths of the function rooted at node.]
700 
701  SideEffects [None]
702 
703  SeeAlso [Cudd_CountMinterm Cudd_CountPath]
704 
705 ******************************************************************************/
706 double
707 Cudd_CountPathsToNonZero(
708  DdNode * node)
709 {
710 
711  st__table *table;
712  double i;
713 
714  table = st__init_table( st__ptrcmp, st__ptrhash);
715  if (table == NULL) {
716  return((double)CUDD_OUT_OF_MEM);
717  }
718  i = ddCountPathsToNonZero(node,table);
719  st__foreach(table, cuddStCountfree, NULL);
720  st__free_table(table);
721  return(i);
722 
723 } /* end of Cudd_CountPathsToNonZero */
724 
725 
726 /**Function********************************************************************
727 
728  Synopsis [Finds the variables on which a DD depends.]
729 
730  Description [Finds the variables on which a DD depends.
731  Returns a BDD consisting of the product of the variables if
732  successful; NULL otherwise.]
733 
734  SideEffects [None]
735 
736  SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]
737 
738 ******************************************************************************/
739 DdNode *
740 Cudd_Support(
741  DdManager * dd /* manager */,
742  DdNode * f /* DD whose support is sought */)
743 {
744  int *support;
745  DdNode *res, *tmp, *var;
746  int i,j;
747  int size;
748 
749  /* Allocate and initialize support array for ddSupportStep. */
750  size = ddMax(dd->size, dd->sizeZ);
751  support = ABC_ALLOC(int,size);
752  if (support == NULL) {
753  dd->errorCode = CUDD_MEMORY_OUT;
754  return(NULL);
755  }
756  for (i = 0; i < size; i++) {
757  support[i] = 0;
758  }
759 
760  /* Compute support and clean up markers. */
761  ddSupportStep(Cudd_Regular(f),support);
762  ddClearFlag(Cudd_Regular(f));
763 
764  /* Transform support from array to cube. */
765  do {
766  dd->reordered = 0;
767  res = DD_ONE(dd);
768  cuddRef(res);
769  for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
770  i = (j >= dd->size) ? j : dd->invperm[j];
771  if (support[i] == 1) {
772  /* The following call to cuddUniqueInter is guaranteed
773  ** not to trigger reordering because the node we look up
774  ** already exists. */
775  var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
776  cuddRef(var);
777  tmp = cuddBddAndRecur(dd,res,var);
778  if (tmp == NULL) {
779  Cudd_RecursiveDeref(dd,res);
780  Cudd_RecursiveDeref(dd,var);
781  res = NULL;
782  break;
783  }
784  cuddRef(tmp);
785  Cudd_RecursiveDeref(dd,res);
786  Cudd_RecursiveDeref(dd,var);
787  res = tmp;
788  }
789  }
790  } while (dd->reordered == 1);
791 
792  ABC_FREE(support);
793  if (res != NULL) cuddDeref(res);
794  return(res);
795 
796 } /* end of Cudd_Support */
797 
798 
799 /**Function********************************************************************
800 
801  Synopsis [Finds the variables on which a DD depends.]
802 
803  Description [Finds the variables on which a DD depends. Returns an
804  index array of the variables if successful; NULL otherwise. The
805  size of the array equals the number of variables in the manager.
806  Each entry of the array is 1 if the corresponding variable is in the
807  support of the DD and 0 otherwise.]
808 
809  SideEffects [None]
810 
811  SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
812 
813 ******************************************************************************/
814 int *
815 Cudd_SupportIndex(
816  DdManager * dd /* manager */,
817  DdNode * f /* DD whose support is sought */)
818 {
819  int *support;
820  int i;
821  int size;
822 
823  /* Allocate and initialize support array for ddSupportStep. */
824  size = ddMax(dd->size, dd->sizeZ);
825  support = ABC_ALLOC(int,size);
826  if (support == NULL) {
827  dd->errorCode = CUDD_MEMORY_OUT;
828  return(NULL);
829  }
830  for (i = 0; i < size; i++) {
831  support[i] = 0;
832  }
833 
834  /* Compute support and clean up markers. */
835  ddSupportStep(Cudd_Regular(f),support);
836  ddClearFlag(Cudd_Regular(f));
837 
838  return(support);
839 
840 } /* end of Cudd_SupportIndex */
841 
842 
843 /**Function********************************************************************
844 
845  Synopsis [Counts the variables on which a DD depends.]
846 
847  Description [Counts the variables on which a DD depends.
848  Returns the number of the variables if successful; CUDD_OUT_OF_MEM
849  otherwise.]
850 
851  SideEffects [None]
852 
853  SeeAlso [Cudd_Support]
854 
855 ******************************************************************************/
856 int
857 Cudd_SupportSize(
858  DdManager * dd /* manager */,
859  DdNode * f /* DD whose support size is sought */)
860 {
861  int *support;
862  int i;
863  int size;
864  int count;
865 
866  /* Allocate and initialize support array for ddSupportStep. */
867  size = ddMax(dd->size, dd->sizeZ);
868  support = ABC_ALLOC(int,size);
869  if (support == NULL) {
870  dd->errorCode = CUDD_MEMORY_OUT;
871  return(CUDD_OUT_OF_MEM);
872  }
873  for (i = 0; i < size; i++) {
874  support[i] = 0;
875  }
876 
877  /* Compute support and clean up markers. */
878  ddSupportStep(Cudd_Regular(f),support);
879  ddClearFlag(Cudd_Regular(f));
880 
881  /* Count support variables. */
882  count = 0;
883  for (i = 0; i < size; i++) {
884  if (support[i] == 1) count++;
885  }
886 
887  ABC_FREE(support);
888  return(count);
889 
890 } /* end of Cudd_SupportSize */
891 
892 
893 /**Function********************************************************************
894 
895  Synopsis [Finds the variables on which a set of DDs depends.]
896 
897  Description [Finds the variables on which a set of DDs depends.
898  The set must contain either BDDs and ADDs, or ZDDs.
899  Returns a BDD consisting of the product of the variables if
900  successful; NULL otherwise.]
901 
902  SideEffects [None]
903 
904  SeeAlso [Cudd_Support Cudd_ClassifySupport]
905 
906 ******************************************************************************/
907 DdNode *
908 Cudd_VectorSupport(
909  DdManager * dd /* manager */,
910  DdNode ** F /* array of DDs whose support is sought */,
911  int n /* size of the array */)
912 {
913  int *support;
914  DdNode *res, *tmp, *var;
915  int i,j;
916  int size;
917 
918  /* Allocate and initialize support array for ddSupportStep. */
919  size = ddMax(dd->size, dd->sizeZ);
920  support = ABC_ALLOC(int,size);
921  if (support == NULL) {
922  dd->errorCode = CUDD_MEMORY_OUT;
923  return(NULL);
924  }
925  for (i = 0; i < size; i++) {
926  support[i] = 0;
927  }
928 
929  /* Compute support and clean up markers. */
930  for (i = 0; i < n; i++) {
931  ddSupportStep(Cudd_Regular(F[i]),support);
932  }
933  for (i = 0; i < n; i++) {
934  ddClearFlag(Cudd_Regular(F[i]));
935  }
936 
937  /* Transform support from array to cube. */
938  res = DD_ONE(dd);
939  cuddRef(res);
940  for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
941  i = (j >= dd->size) ? j : dd->invperm[j];
942  if (support[i] == 1) {
943  var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
944  cuddRef(var);
945  tmp = Cudd_bddAnd(dd,res,var);
946  if (tmp == NULL) {
947  Cudd_RecursiveDeref(dd,res);
948  Cudd_RecursiveDeref(dd,var);
949  ABC_FREE(support);
950  return(NULL);
951  }
952  cuddRef(tmp);
953  Cudd_RecursiveDeref(dd,res);
954  Cudd_RecursiveDeref(dd,var);
955  res = tmp;
956  }
957  }
958 
959  ABC_FREE(support);
960  cuddDeref(res);
961  return(res);
962 
963 } /* end of Cudd_VectorSupport */
964 
965 
966 /**Function********************************************************************
967 
968  Synopsis [Finds the variables on which a set of DDs depends.]
969 
970  Description [Finds the variables on which a set of DDs depends.
971  The set must contain either BDDs and ADDs, or ZDDs.
972  Returns an index array of the variables if successful; NULL otherwise.]
973 
974  SideEffects [None]
975 
976  SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]
977 
978 ******************************************************************************/
979 int *
980 Cudd_VectorSupportIndex(
981  DdManager * dd /* manager */,
982  DdNode ** F /* array of DDs whose support is sought */,
983  int n /* size of the array */)
984 {
985  int *support;
986  int i;
987  int size;
988 
989  /* Allocate and initialize support array for ddSupportStep. */
990  size = ddMax(dd->size, dd->sizeZ);
991  support = ABC_ALLOC(int,size);
992  if (support == NULL) {
993  dd->errorCode = CUDD_MEMORY_OUT;
994  return(NULL);
995  }
996  for (i = 0; i < size; i++) {
997  support[i] = 0;
998  }
999 
1000  /* Compute support and clean up markers. */
1001  for (i = 0; i < n; i++) {
1002  ddSupportStep(Cudd_Regular(F[i]),support);
1003  }
1004  for (i = 0; i < n; i++) {
1005  ddClearFlag(Cudd_Regular(F[i]));
1006  }
1007 
1008  return(support);
1009 
1010 } /* end of Cudd_VectorSupportIndex */
1011 
1012 
1013 /**Function********************************************************************
1014 
1015  Synopsis [Counts the variables on which a set of DDs depends.]
1016 
1017  Description [Counts the variables on which a set of DDs depends.
1018  The set must contain either BDDs and ADDs, or ZDDs.
1019  Returns the number of the variables if successful; CUDD_OUT_OF_MEM
1020  otherwise.]
1021 
1022  SideEffects [None]
1023 
1024  SeeAlso [Cudd_VectorSupport Cudd_SupportSize]
1025 
1026 ******************************************************************************/
1027 int
1028 Cudd_VectorSupportSize(
1029  DdManager * dd /* manager */,
1030  DdNode ** F /* array of DDs whose support is sought */,
1031  int n /* size of the array */)
1032 {
1033  int *support;
1034  int i;
1035  int size;
1036  int count;
1037 
1038  /* Allocate and initialize support array for ddSupportStep. */
1039  size = ddMax(dd->size, dd->sizeZ);
1040  support = ABC_ALLOC(int,size);
1041  if (support == NULL) {
1042  dd->errorCode = CUDD_MEMORY_OUT;
1043  return(CUDD_OUT_OF_MEM);
1044  }
1045  for (i = 0; i < size; i++) {
1046  support[i] = 0;
1047  }
1048 
1049  /* Compute support and clean up markers. */
1050  for (i = 0; i < n; i++) {
1051  ddSupportStep(Cudd_Regular(F[i]),support);
1052  }
1053  for (i = 0; i < n; i++) {
1054  ddClearFlag(Cudd_Regular(F[i]));
1055  }
1056 
1057  /* Count vriables in support. */
1058  count = 0;
1059  for (i = 0; i < size; i++) {
1060  if (support[i] == 1) count++;
1061  }
1062 
1063  ABC_FREE(support);
1064  return(count);
1065 
1066 } /* end of Cudd_VectorSupportSize */
1067 
1068 
1069 /**Function********************************************************************
1070 
1071  Synopsis [Classifies the variables in the support of two DDs.]
1072 
1073  Description [Classifies the variables in the support of two DDs
1074  <code>f</code> and <code>g</code>, depending on whther they appear
1075  in both DDs, only in <code>f</code>, or only in <code>g</code>.
1076  Returns 1 if successful; 0 otherwise.]
1077 
1078  SideEffects [The cubes of the three classes of variables are
1079  returned as side effects.]
1080 
1081  SeeAlso [Cudd_Support Cudd_VectorSupport]
1082 
1083 ******************************************************************************/
1084 int
1085 Cudd_ClassifySupport(
1086  DdManager * dd /* manager */,
1087  DdNode * f /* first DD */,
1088  DdNode * g /* second DD */,
1089  DdNode ** common /* cube of shared variables */,
1090  DdNode ** onlyF /* cube of variables only in f */,
1091  DdNode ** onlyG /* cube of variables only in g */)
1092 {
1093  int *supportF, *supportG;
1094  DdNode *tmp, *var;
1095  int i,j;
1096  int size;
1097 
1098  /* Allocate and initialize support arrays for ddSupportStep. */
1099  size = ddMax(dd->size, dd->sizeZ);
1100  supportF = ABC_ALLOC(int,size);
1101  if (supportF == NULL) {
1102  dd->errorCode = CUDD_MEMORY_OUT;
1103  return(0);
1104  }
1105  supportG = ABC_ALLOC(int,size);
1106  if (supportG == NULL) {
1107  dd->errorCode = CUDD_MEMORY_OUT;
1108  ABC_FREE(supportF);
1109  return(0);
1110  }
1111  for (i = 0; i < size; i++) {
1112  supportF[i] = 0;
1113  supportG[i] = 0;
1114  }
1115 
1116  /* Compute supports and clean up markers. */
1117  ddSupportStep(Cudd_Regular(f),supportF);
1118  ddClearFlag(Cudd_Regular(f));
1119  ddSupportStep(Cudd_Regular(g),supportG);
1120  ddClearFlag(Cudd_Regular(g));
1121 
1122  /* Classify variables and create cubes. */
1123  *common = *onlyF = *onlyG = DD_ONE(dd);
1124  cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
1125  for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
1126  i = (j >= dd->size) ? j : dd->invperm[j];
1127  if (supportF[i] == 0 && supportG[i] == 0) continue;
1128  var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
1129  cuddRef(var);
1130  if (supportG[i] == 0) {
1131  tmp = Cudd_bddAnd(dd,*onlyF,var);
1132  if (tmp == NULL) {
1133  Cudd_RecursiveDeref(dd,*common);
1134  Cudd_RecursiveDeref(dd,*onlyF);
1135  Cudd_RecursiveDeref(dd,*onlyG);
1136  Cudd_RecursiveDeref(dd,var);
1137  ABC_FREE(supportF); ABC_FREE(supportG);
1138  return(0);
1139  }
1140  cuddRef(tmp);
1141  Cudd_RecursiveDeref(dd,*onlyF);
1142  *onlyF = tmp;
1143  } else if (supportF[i] == 0) {
1144  tmp = Cudd_bddAnd(dd,*onlyG,var);
1145  if (tmp == NULL) {
1146  Cudd_RecursiveDeref(dd,*common);
1147  Cudd_RecursiveDeref(dd,*onlyF);
1148  Cudd_RecursiveDeref(dd,*onlyG);
1149  Cudd_RecursiveDeref(dd,var);
1150  ABC_FREE(supportF); ABC_FREE(supportG);
1151  return(0);
1152  }
1153  cuddRef(tmp);
1154  Cudd_RecursiveDeref(dd,*onlyG);
1155  *onlyG = tmp;
1156  } else {
1157  tmp = Cudd_bddAnd(dd,*common,var);
1158  if (tmp == NULL) {
1159  Cudd_RecursiveDeref(dd,*common);
1160  Cudd_RecursiveDeref(dd,*onlyF);
1161  Cudd_RecursiveDeref(dd,*onlyG);
1162  Cudd_RecursiveDeref(dd,var);
1163  ABC_FREE(supportF); ABC_FREE(supportG);
1164  return(0);
1165  }
1166  cuddRef(tmp);
1167  Cudd_RecursiveDeref(dd,*common);
1168  *common = tmp;
1169  }
1170  Cudd_RecursiveDeref(dd,var);
1171  }
1172 
1173  ABC_FREE(supportF); ABC_FREE(supportG);
1174  cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
1175  return(1);
1176 
1177 } /* end of Cudd_ClassifySupport */
1178 
1179 
1180 /**Function********************************************************************
1181 
1182  Synopsis [Counts the number of leaves in a DD.]
1183 
1184  Description [Counts the number of leaves in a DD. Returns the number
1185  of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
1186  otherwise.]
1187 
1188  SideEffects [None]
1189 
1190  SeeAlso [Cudd_PrintDebug]
1191 
1192 ******************************************************************************/
1193 int
1194 Cudd_CountLeaves(
1195  DdNode * node)
1196 {
1197  int i;
1198 
1199  i = ddLeavesInt(Cudd_Regular(node));
1200  ddClearFlag(Cudd_Regular(node));
1201  return(i);
1202 
1203 } /* end of Cudd_CountLeaves */
1204 
1205 
1206 /**Function********************************************************************
1207 
1208  Synopsis [Picks one on-set cube randomly from the given DD.]
1209 
1210  Description [Picks one on-set cube randomly from the given DD. The
1211  cube is written into an array of characters. The array must have at
1212  least as many entries as there are variables. Returns 1 if
1213  successful; 0 otherwise.]
1214 
1215  SideEffects [None]
1216 
1217  SeeAlso [Cudd_bddPickOneMinterm]
1218 
1219 ******************************************************************************/
1220 int
1221 Cudd_bddPickOneCube(
1222  DdManager * ddm,
1223  DdNode * node,
1224  char * string)
1225 {
1226  DdNode *N, *T, *E;
1227  DdNode *one, *bzero;
1228  char dir;
1229  int i;
1230 
1231  if (string == NULL || node == NULL) return(0);
1232 
1233  /* The constant 0 function has no on-set cubes. */
1234  one = DD_ONE(ddm);
1235  bzero = Cudd_Not(one);
1236  if (node == bzero) return(0);
1237 
1238  for (i = 0; i < ddm->size; i++) string[i] = 2;
1239 
1240  for (;;) {
1241 
1242  if (node == one) break;
1243 
1244  N = Cudd_Regular(node);
1245 
1246  T = cuddT(N); E = cuddE(N);
1247  if (Cudd_IsComplement(node)) {
1248  T = Cudd_Not(T); E = Cudd_Not(E);
1249  }
1250  if (T == bzero) {
1251  string[N->index] = 0;
1252  node = E;
1253  } else if (E == bzero) {
1254  string[N->index] = 1;
1255  node = T;
1256  } else {
1257  dir = (char) ((Cudd_Random() & 0x2000) >> 13);
1258  string[N->index] = dir;
1259  node = dir ? T : E;
1260  }
1261  }
1262  return(1);
1263 
1264 } /* end of Cudd_bddPickOneCube */
1265 
1266 
1267 /**Function********************************************************************
1268 
1269  Synopsis [Picks one on-set minterm randomly from the given DD.]
1270 
1271  Description [Picks one on-set minterm randomly from the given
1272  DD. The minterm is in terms of <code>vars</code>. The array
1273  <code>vars</code> should contain at least all variables in the
1274  support of <code>f</code>; if this condition is not met the minterm
1275  built by this procedure may not be contained in
1276  <code>f</code>. Builds a BDD for the minterm and returns a pointer
1277  to it if successful; NULL otherwise. There are three reasons why the
1278  procedure may fail:
1279  <ul>
1280  <li> It may run out of memory;
1281  <li> the function <code>f</code> may be the constant 0;
1282  <li> the minterm may not be contained in <code>f</code>.
1283  </ul>]
1284 
1285  SideEffects [None]
1286 
1287  SeeAlso [Cudd_bddPickOneCube]
1288 
1289 ******************************************************************************/
1290 DdNode *
1291 Cudd_bddPickOneMinterm(
1292  DdManager * dd /* manager */,
1293  DdNode * f /* function from which to pick one minterm */,
1294  DdNode ** vars /* array of variables */,
1295  int n /* size of <code>vars</code> */)
1296 {
1297  char *string;
1298  int i, size;
1299  int *indices;
1300  int result;
1301  DdNode *old, *neW;
1302 
1303  size = dd->size;
1304  string = ABC_ALLOC(char, size);
1305  if (string == NULL) {
1306  dd->errorCode = CUDD_MEMORY_OUT;
1307  return(NULL);
1308  }
1309  indices = ABC_ALLOC(int,n);
1310  if (indices == NULL) {
1311  dd->errorCode = CUDD_MEMORY_OUT;
1312  ABC_FREE(string);
1313  return(NULL);
1314  }
1315 
1316  for (i = 0; i < n; i++) {
1317  indices[i] = vars[i]->index;
1318  }
1319 
1320  result = Cudd_bddPickOneCube(dd,f,string);
1321  if (result == 0) {
1322  ABC_FREE(string);
1323  ABC_FREE(indices);
1324  return(NULL);
1325  }
1326 
1327  /* Randomize choice for don't cares. */
1328  for (i = 0; i < n; i++) {
1329  if (string[indices[i]] == 2)
1330  string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
1331  }
1332 
1333  /* Build result BDD. */
1334  old = Cudd_ReadOne(dd);
1335  cuddRef(old);
1336 
1337  for (i = n-1; i >= 0; i--) {
1338  neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
1339  if (neW == NULL) {
1340  ABC_FREE(string);
1341  ABC_FREE(indices);
1342  Cudd_RecursiveDeref(dd,old);
1343  return(NULL);
1344  }
1345  cuddRef(neW);
1346  Cudd_RecursiveDeref(dd,old);
1347  old = neW;
1348  }
1349 
1350 #ifdef DD_DEBUG
1351  /* Test. */
1352  if (Cudd_bddLeq(dd,old,f)) {
1353  cuddDeref(old);
1354  } else {
1355  Cudd_RecursiveDeref(dd,old);
1356  old = NULL;
1357  }
1358 #else
1359  cuddDeref(old);
1360 #endif
1361 
1362  ABC_FREE(string);
1363  ABC_FREE(indices);
1364  return(old);
1365 
1366 } /* end of Cudd_bddPickOneMinterm */
1367 
1368 
1369 /**Function********************************************************************
1370 
1371  Synopsis [Picks k on-set minterms evenly distributed from given DD.]
1372 
1373  Description [Picks k on-set minterms evenly distributed from given DD.
1374  The minterms are in terms of <code>vars</code>. The array
1375  <code>vars</code> should contain at least all variables in the
1376  support of <code>f</code>; if this condition is not met the minterms
1377  built by this procedure may not be contained in
1378  <code>f</code>. Builds an array of BDDs for the minterms and returns a
1379  pointer to it if successful; NULL otherwise. There are three reasons
1380  why the procedure may fail:
1381  <ul>
1382  <li> It may run out of memory;
1383  <li> the function <code>f</code> may be the constant 0;
1384  <li> the minterms may not be contained in <code>f</code>.
1385  </ul>]
1386 
1387  SideEffects [None]
1388 
1389  SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]
1390 
1391 ******************************************************************************/
1392 DdNode **
1393 Cudd_bddPickArbitraryMinterms(
1394  DdManager * dd /* manager */,
1395  DdNode * f /* function from which to pick k minterms */,
1396  DdNode ** vars /* array of variables */,
1397  int n /* size of <code>vars</code> */,
1398  int k /* number of minterms to find */)
1399 {
1400  char **string;
1401  int i, j, l, size;
1402  int *indices;
1403  int result;
1404  DdNode **old, *neW;
1405  double minterms;
1406  char *saveString;
1407  int saveFlag, savePoint = -1, isSame;
1408 
1409  minterms = Cudd_CountMinterm(dd,f,n);
1410  if ((double)k > minterms) {
1411  return(NULL);
1412  }
1413 
1414  size = dd->size;
1415  string = ABC_ALLOC(char *, k);
1416  if (string == NULL) {
1417  dd->errorCode = CUDD_MEMORY_OUT;
1418  return(NULL);
1419  }
1420  for (i = 0; i < k; i++) {
1421  string[i] = ABC_ALLOC(char, size + 1);
1422  if (string[i] == NULL) {
1423  for (j = 0; j < i; j++)
1424  ABC_FREE(string[i]);
1425  ABC_FREE(string);
1426  dd->errorCode = CUDD_MEMORY_OUT;
1427  return(NULL);
1428  }
1429  for (j = 0; j < size; j++) string[i][j] = '2';
1430  string[i][size] = '\0';
1431  }
1432  indices = ABC_ALLOC(int,n);
1433  if (indices == NULL) {
1434  dd->errorCode = CUDD_MEMORY_OUT;
1435  for (i = 0; i < k; i++)
1436  ABC_FREE(string[i]);
1437  ABC_FREE(string);
1438  return(NULL);
1439  }
1440 
1441  for (i = 0; i < n; i++) {
1442  indices[i] = vars[i]->index;
1443  }
1444 
1445  result = ddPickArbitraryMinterms(dd,f,n,k,string);
1446  if (result == 0) {
1447  for (i = 0; i < k; i++)
1448  ABC_FREE(string[i]);
1449  ABC_FREE(string);
1450  ABC_FREE(indices);
1451  return(NULL);
1452  }
1453 
1454  old = ABC_ALLOC(DdNode *, k);
1455  if (old == NULL) {
1456  dd->errorCode = CUDD_MEMORY_OUT;
1457  for (i = 0; i < k; i++)
1458  ABC_FREE(string[i]);
1459  ABC_FREE(string);
1460  ABC_FREE(indices);
1461  return(NULL);
1462  }
1463  saveString = ABC_ALLOC(char, size + 1);
1464  if (saveString == NULL) {
1465  dd->errorCode = CUDD_MEMORY_OUT;
1466  for (i = 0; i < k; i++)
1467  ABC_FREE(string[i]);
1468  ABC_FREE(string);
1469  ABC_FREE(indices);
1470  ABC_FREE(old);
1471  return(NULL);
1472  }
1473  saveFlag = 0;
1474 
1475  /* Build result BDD array. */
1476  for (i = 0; i < k; i++) {
1477  isSame = 0;
1478  if (!saveFlag) {
1479  for (j = i + 1; j < k; j++) {
1480  if (strcmp(string[i], string[j]) == 0) {
1481  savePoint = i;
1482  strcpy(saveString, string[i]);
1483  saveFlag = 1;
1484  break;
1485  }
1486  }
1487  } else {
1488  if (strcmp(string[i], saveString) == 0) {
1489  isSame = 1;
1490  } else {
1491  saveFlag = 0;
1492  for (j = i + 1; j < k; j++) {
1493  if (strcmp(string[i], string[j]) == 0) {
1494  savePoint = i;
1495  strcpy(saveString, string[i]);
1496  saveFlag = 1;
1497  break;
1498  }
1499  }
1500  }
1501  }
1502  /* Randomize choice for don't cares. */
1503  for (j = 0; j < n; j++) {
1504  if (string[i][indices[j]] == '2')
1505  string[i][indices[j]] =
1506  (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1507  }
1508 
1509  while (isSame) {
1510  isSame = 0;
1511  for (j = savePoint; j < i; j++) {
1512  if (strcmp(string[i], string[j]) == 0) {
1513  isSame = 1;
1514  break;
1515  }
1516  }
1517  if (isSame) {
1518  strcpy(string[i], saveString);
1519  /* Randomize choice for don't cares. */
1520  for (j = 0; j < n; j++) {
1521  if (string[i][indices[j]] == '2')
1522  string[i][indices[j]] =
1523  (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1524  }
1525  }
1526  }
1527 
1528  old[i] = Cudd_ReadOne(dd);
1529  cuddRef(old[i]);
1530 
1531  for (j = 0; j < n; j++) {
1532  if (string[i][indices[j]] == '0') {
1533  neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
1534  } else {
1535  neW = Cudd_bddAnd(dd,old[i],vars[j]);
1536  }
1537  if (neW == NULL) {
1538  ABC_FREE(saveString);
1539  for (l = 0; l < k; l++)
1540  ABC_FREE(string[l]);
1541  ABC_FREE(string);
1542  ABC_FREE(indices);
1543  for (l = 0; l <= i; l++)
1544  Cudd_RecursiveDeref(dd,old[l]);
1545  ABC_FREE(old);
1546  return(NULL);
1547  }
1548  cuddRef(neW);
1549  Cudd_RecursiveDeref(dd,old[i]);
1550  old[i] = neW;
1551  }
1552 
1553  /* Test. */
1554  if (!Cudd_bddLeq(dd,old[i],f)) {
1555  ABC_FREE(saveString);
1556  for (l = 0; l < k; l++)
1557  ABC_FREE(string[l]);
1558  ABC_FREE(string);
1559  ABC_FREE(indices);
1560  for (l = 0; l <= i; l++)
1561  Cudd_RecursiveDeref(dd,old[l]);
1562  ABC_FREE(old);
1563  return(NULL);
1564  }
1565  }
1566 
1567  ABC_FREE(saveString);
1568  for (i = 0; i < k; i++) {
1569  cuddDeref(old[i]);
1570  ABC_FREE(string[i]);
1571  }
1572  ABC_FREE(string);
1573  ABC_FREE(indices);
1574  return(old);
1575 
1576 } /* end of Cudd_bddPickArbitraryMinterms */
1577 
1578 
1579 /**Function********************************************************************
1580 
1581  Synopsis [Extracts a subset from a BDD.]
1582 
1583  Description [Extracts a subset from a BDD in the following procedure.
1584  1. Compute the weight for each mask variable by counting the number of
1585  minterms for both positive and negative cofactors of the BDD with
1586  respect to each mask variable. (weight = #positive - #negative)
1587  2. Find a representative cube of the BDD by using the weight. From the
1588  top variable of the BDD, for each variable, if the weight is greater
1589  than 0.0, choose THEN branch, othereise ELSE branch, until meeting
1590  the constant 1.
1591  3. Quantify out the variables not in maskVars from the representative
1592  cube and if a variable in maskVars is don't care, replace the
1593  variable with a constant(1 or 0) depending on the weight.
1594  4. Make a subset of the BDD by multiplying with the modified cube.]
1595 
1596  SideEffects [None]
1597 
1598  SeeAlso []
1599 
1600 ******************************************************************************/
1601 DdNode *
1602 Cudd_SubsetWithMaskVars(
1603  DdManager * dd /* manager */,
1604  DdNode * f /* function from which to pick a cube */,
1605  DdNode ** vars /* array of variables */,
1606  int nvars /* size of <code>vars</code> */,
1607  DdNode ** maskVars /* array of variables */,
1608  int mvars /* size of <code>maskVars</code> */)
1609 {
1610  double *weight;
1611  char *string;
1612  int i, size;
1613  int *indices, *mask;
1614  int result;
1615  DdNode *zero, *cube, *newCube, *subset;
1616  DdNode *cof;
1617 
1618  DdNode *support;
1619  support = Cudd_Support(dd,f);
1620  cuddRef(support);
1621  Cudd_RecursiveDeref(dd,support);
1622 
1623  zero = Cudd_Not(dd->one);
1624  size = dd->size;
1625 
1626  weight = ABC_ALLOC(double,size);
1627  if (weight == NULL) {
1628  dd->errorCode = CUDD_MEMORY_OUT;
1629  return(NULL);
1630  }
1631  for (i = 0; i < size; i++) {
1632  weight[i] = 0.0;
1633  }
1634  for (i = 0; i < mvars; i++) {
1635  cof = Cudd_Cofactor(dd, f, maskVars[i]);
1636  cuddRef(cof);
1637  weight[i] = Cudd_CountMinterm(dd, cof, nvars);
1638  Cudd_RecursiveDeref(dd,cof);
1639 
1640  cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
1641  cuddRef(cof);
1642  weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
1643  Cudd_RecursiveDeref(dd,cof);
1644  }
1645 
1646  string = ABC_ALLOC(char, size + 1);
1647  if (string == NULL) {
1648  dd->errorCode = CUDD_MEMORY_OUT;
1649  ABC_FREE(weight);
1650  return(NULL);
1651  }
1652  mask = ABC_ALLOC(int, size);
1653  if (mask == NULL) {
1654  dd->errorCode = CUDD_MEMORY_OUT;
1655  ABC_FREE(weight);
1656  ABC_FREE(string);
1657  return(NULL);
1658  }
1659  for (i = 0; i < size; i++) {
1660  string[i] = '2';
1661  mask[i] = 0;
1662  }
1663  string[size] = '\0';
1664  indices = ABC_ALLOC(int,nvars);
1665  if (indices == NULL) {
1666  dd->errorCode = CUDD_MEMORY_OUT;
1667  ABC_FREE(weight);
1668  ABC_FREE(string);
1669  ABC_FREE(mask);
1670  return(NULL);
1671  }
1672  for (i = 0; i < nvars; i++) {
1673  indices[i] = vars[i]->index;
1674  }
1675 
1676  result = ddPickRepresentativeCube(dd,f,weight,string);
1677  if (result == 0) {
1678  ABC_FREE(weight);
1679  ABC_FREE(string);
1680  ABC_FREE(mask);
1681  ABC_FREE(indices);
1682  return(NULL);
1683  }
1684 
1685  cube = Cudd_ReadOne(dd);
1686  cuddRef(cube);
1687  zero = Cudd_Not(Cudd_ReadOne(dd));
1688  for (i = 0; i < nvars; i++) {
1689  if (string[indices[i]] == '0') {
1690  newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1691  } else if (string[indices[i]] == '1') {
1692  newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1693  } else
1694  continue;
1695  if (newCube == NULL) {
1696  ABC_FREE(weight);
1697  ABC_FREE(string);
1698  ABC_FREE(mask);
1699  ABC_FREE(indices);
1700  Cudd_RecursiveDeref(dd,cube);
1701  return(NULL);
1702  }
1703  cuddRef(newCube);
1704  Cudd_RecursiveDeref(dd,cube);
1705  cube = newCube;
1706  }
1707  Cudd_RecursiveDeref(dd,cube);
1708 
1709  for (i = 0; i < mvars; i++) {
1710  mask[maskVars[i]->index] = 1;
1711  }
1712  for (i = 0; i < nvars; i++) {
1713  if (mask[indices[i]]) {
1714  if (string[indices[i]] == '2') {
1715  if (weight[indices[i]] >= 0.0)
1716  string[indices[i]] = '1';
1717  else
1718  string[indices[i]] = '0';
1719  }
1720  } else {
1721  string[indices[i]] = '2';
1722  }
1723  }
1724 
1725  cube = Cudd_ReadOne(dd);
1726  cuddRef(cube);
1727  zero = Cudd_Not(Cudd_ReadOne(dd));
1728 
1729  /* Build result BDD. */
1730  for (i = 0; i < nvars; i++) {
1731  if (string[indices[i]] == '0') {
1732  newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1733  } else if (string[indices[i]] == '1') {
1734  newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1735  } else
1736  continue;
1737  if (newCube == NULL) {
1738  ABC_FREE(weight);
1739  ABC_FREE(string);
1740  ABC_FREE(mask);
1741  ABC_FREE(indices);
1742  Cudd_RecursiveDeref(dd,cube);
1743  return(NULL);
1744  }
1745  cuddRef(newCube);
1746  Cudd_RecursiveDeref(dd,cube);
1747  cube = newCube;
1748  }
1749 
1750  subset = Cudd_bddAnd(dd,f,cube);
1751  cuddRef(subset);
1752  Cudd_RecursiveDeref(dd,cube);
1753 
1754  /* Test. */
1755  if (Cudd_bddLeq(dd,subset,f)) {
1756  cuddDeref(subset);
1757  } else {
1758  Cudd_RecursiveDeref(dd,subset);
1759  subset = NULL;
1760  }
1761 
1762  ABC_FREE(weight);
1763  ABC_FREE(string);
1764  ABC_FREE(mask);
1765  ABC_FREE(indices);
1766  return(subset);
1767 
1768 } /* end of Cudd_SubsetWithMaskVars */
1769 
1770 
1771 /**Function********************************************************************
1772 
1773  Synopsis [Finds the first cube of a decision diagram.]
1774 
1775  Description [Defines an iterator on the onset of a decision diagram
1776  and finds its first cube. Returns a generator that contains the
1777  information necessary to continue the enumeration if successful; NULL
1778  otherwise.<p>
1779  A cube is represented as an array of literals, which are integers in
1780  {0, 1, 2}; 0 represents a complemented literal, 1 represents an
1781  uncomplemented literal, and 2 stands for don't care. The enumeration
1782  produces a disjoint cover of the function associated with the diagram.
1783  The size of the array equals the number of variables in the manager at
1784  the time Cudd_FirstCube is called.<p>
1785  For each cube, a value is also returned. This value is always 1 for a
1786  BDD, while it may be different from 1 for an ADD.
1787  For BDDs, the offset is the set of cubes whose value is the logical zero.
1788  For ADDs, the offset is the set of cubes whose value is the
1789  background value. The cubes of the offset are not enumerated.]
1790 
1791  SideEffects [The first cube and its value are returned as side effects.]
1792 
1793  SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
1794  Cudd_FirstNode]
1795 
1796 ******************************************************************************/
1797 DdGen *
1798 Cudd_FirstCube(
1799  DdManager * dd,
1800  DdNode * f,
1801  int ** cube,
1802  CUDD_VALUE_TYPE * value)
1803 {
1804  DdGen *gen;
1805  DdNode *top, *treg, *next, *nreg, *prev, *preg;
1806  int i;
1807  int nvars;
1808 
1809  /* Sanity Check. */
1810  if (dd == NULL || f == NULL) return(NULL);
1811 
1812  /* Allocate generator an initialize it. */
1813  gen = ABC_ALLOC(DdGen,1);
1814  if (gen == NULL) {
1815  dd->errorCode = CUDD_MEMORY_OUT;
1816  return(NULL);
1817  }
1818 
1819  gen->manager = dd;
1820  gen->type = CUDD_GEN_CUBES;
1821  gen->status = CUDD_GEN_EMPTY;
1822  gen->gen.cubes.cube = NULL;
1823  gen->gen.cubes.value = DD_ZERO_VAL;
1824  gen->stack.sp = 0;
1825  gen->stack.stack = NULL;
1826  gen->node = NULL;
1827 
1828  nvars = dd->size;
1829  gen->gen.cubes.cube = ABC_ALLOC(int,nvars);
1830  if (gen->gen.cubes.cube == NULL) {
1831  dd->errorCode = CUDD_MEMORY_OUT;
1832  ABC_FREE(gen);
1833  return(NULL);
1834  }
1835  for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
1836 
1837  /* The maximum stack depth is one plus the number of variables.
1838  ** because a path may have nodes at all levels, including the
1839  ** constant level.
1840  */
1841  gen->stack.stack = ABC_ALLOC(DdNodePtr, nvars+1);
1842  if (gen->stack.stack == NULL) {
1843  dd->errorCode = CUDD_MEMORY_OUT;
1844  ABC_FREE(gen->gen.cubes.cube);
1845  ABC_FREE(gen);
1846  return(NULL);
1847  }
1848  for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
1849 
1850  /* Find the first cube of the onset. */
1851  gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
1852 
1853  while (1) {
1854  top = gen->stack.stack[gen->stack.sp-1];
1855  treg = Cudd_Regular(top);
1856  if (!cuddIsConstant(treg)) {
1857  /* Take the else branch first. */
1858  gen->gen.cubes.cube[treg->index] = 0;
1859  next = cuddE(treg);
1860  if (top != treg) next = Cudd_Not(next);
1861  gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1862  } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1863  /* Backtrack */
1864  while (1) {
1865  if (gen->stack.sp == 1) {
1866  /* The current node has no predecessor. */
1867  gen->status = CUDD_GEN_EMPTY;
1868  gen->stack.sp--;
1869  goto done;
1870  }
1871  prev = gen->stack.stack[gen->stack.sp-2];
1872  preg = Cudd_Regular(prev);
1873  nreg = cuddT(preg);
1874  if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1875  if (next != top) { /* follow the then branch next */
1876  gen->gen.cubes.cube[preg->index] = 1;
1877  gen->stack.stack[gen->stack.sp-1] = next;
1878  break;
1879  }
1880  /* Pop the stack and try again. */
1881  gen->gen.cubes.cube[preg->index] = 2;
1882  gen->stack.sp--;
1883  top = gen->stack.stack[gen->stack.sp-1];
1884  treg = Cudd_Regular(top);
1885  }
1886  } else {
1887  gen->status = CUDD_GEN_NONEMPTY;
1888  gen->gen.cubes.value = cuddV(top);
1889  goto done;
1890  }
1891  }
1892 
1893 done:
1894  *cube = gen->gen.cubes.cube;
1895  *value = gen->gen.cubes.value;
1896  return(gen);
1897 
1898 } /* end of Cudd_FirstCube */
1899 
1900 
1901 /**Function********************************************************************
1902 
1903  Synopsis [Generates the next cube of a decision diagram onset.]
1904 
1905  Description [Generates the next cube of a decision diagram onset,
1906  using generator gen. Returns 0 if the enumeration is completed; 1
1907  otherwise.]
1908 
1909  SideEffects [The cube and its value are returned as side effects. The
1910  generator is modified.]
1911 
1912  SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
1913  Cudd_NextNode]
1914 
1915 ******************************************************************************/
1916 int
1917 Cudd_NextCube(
1918  DdGen * gen,
1919  int ** cube,
1920  CUDD_VALUE_TYPE * value)
1921 {
1922  DdNode *top, *treg, *next, *nreg, *prev, *preg;
1923  DdManager *dd = gen->manager;
1924 
1925  /* Backtrack from previously reached terminal node. */
1926  while (1) {
1927  if (gen->stack.sp == 1) {
1928  /* The current node has no predecessor. */
1929  gen->status = CUDD_GEN_EMPTY;
1930  gen->stack.sp--;
1931  goto done;
1932  }
1933  top = gen->stack.stack[gen->stack.sp-1];
1934  treg = Cudd_Regular(top);
1935  prev = gen->stack.stack[gen->stack.sp-2];
1936  preg = Cudd_Regular(prev);
1937  nreg = cuddT(preg);
1938  if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1939  if (next != top) { /* follow the then branch next */
1940  gen->gen.cubes.cube[preg->index] = 1;
1941  gen->stack.stack[gen->stack.sp-1] = next;
1942  break;
1943  }
1944  /* Pop the stack and try again. */
1945  gen->gen.cubes.cube[preg->index] = 2;
1946  gen->stack.sp--;
1947  }
1948 
1949  while (1) {
1950  top = gen->stack.stack[gen->stack.sp-1];
1951  treg = Cudd_Regular(top);
1952  if (!cuddIsConstant(treg)) {
1953  /* Take the else branch first. */
1954  gen->gen.cubes.cube[treg->index] = 0;
1955  next = cuddE(treg);
1956  if (top != treg) next = Cudd_Not(next);
1957  gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1958  } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1959  /* Backtrack */
1960  while (1) {
1961  if (gen->stack.sp == 1) {
1962  /* The current node has no predecessor. */
1963  gen->status = CUDD_GEN_EMPTY;
1964  gen->stack.sp--;
1965  goto done;
1966  }
1967  prev = gen->stack.stack[gen->stack.sp-2];
1968  preg = Cudd_Regular(prev);
1969  nreg = cuddT(preg);
1970  if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1971  if (next != top) { /* follow the then branch next */
1972  gen->gen.cubes.cube[preg->index] = 1;
1973  gen->stack.stack[gen->stack.sp-1] = next;
1974  break;
1975  }
1976  /* Pop the stack and try again. */
1977  gen->gen.cubes.cube[preg->index] = 2;
1978  gen->stack.sp--;
1979  top = gen->stack.stack[gen->stack.sp-1];
1980  treg = Cudd_Regular(top);
1981  }
1982  } else {
1983  gen->status = CUDD_GEN_NONEMPTY;
1984  gen->gen.cubes.value = cuddV(top);
1985  goto done;
1986  }
1987  }
1988 
1989 done:
1990  if (gen->status == CUDD_GEN_EMPTY) return(0);
1991  *cube = gen->gen.cubes.cube;
1992  *value = gen->gen.cubes.value;
1993  return(1);
1994 
1995 } /* end of Cudd_NextCube */
1996 
1997 
1998 /**Function********************************************************************
1999 
2000  Synopsis [Finds the first prime of a Boolean function.]
2001 
2002  Description [Defines an iterator on a pair of BDDs describing a
2003  (possibly incompletely specified) Boolean functions and finds the
2004  first cube of a cover of the function. Returns a generator
2005  that contains the information necessary to continue the enumeration
2006  if successful; NULL otherwise.<p>
2007 
2008  The two argument BDDs are the lower and upper bounds of an interval.
2009  It is a mistake to call this function with a lower bound that is not
2010  less than or equal to the upper bound.<p>
2011 
2012  A cube is represented as an array of literals, which are integers in
2013  {0, 1, 2}; 0 represents a complemented literal, 1 represents an
2014  uncomplemented literal, and 2 stands for don't care. The enumeration
2015  produces a prime and irredundant cover of the function associated
2016  with the two BDDs. The size of the array equals the number of
2017  variables in the manager at the time Cudd_FirstCube is called.<p>
2018 
2019  This iterator can only be used on BDDs.]
2020 
2021  SideEffects [The first cube is returned as side effect.]
2022 
2023  SeeAlso [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty
2024  Cudd_FirstCube Cudd_FirstNode]
2025 
2026 ******************************************************************************/
2027 DdGen *
2028 Cudd_FirstPrime(
2029  DdManager *dd,
2030  DdNode *l,
2031  DdNode *u,
2032  int **cube)
2033 {
2034  DdGen *gen;
2035  DdNode *implicant, *prime, *tmp;
2036  int length, result;
2037 
2038  /* Sanity Check. */
2039  if (dd == NULL || l == NULL || u == NULL) return(NULL);
2040 
2041  /* Allocate generator an initialize it. */
2042  gen = ABC_ALLOC(DdGen,1);
2043  if (gen == NULL) {
2044  dd->errorCode = CUDD_MEMORY_OUT;
2045  return(NULL);
2046  }
2047 
2048  gen->manager = dd;
2049  gen->type = CUDD_GEN_PRIMES;
2050  gen->status = CUDD_GEN_EMPTY;
2051  gen->gen.primes.cube = NULL;
2052  gen->gen.primes.ub = u;
2053  gen->stack.sp = 0;
2054  gen->stack.stack = NULL;
2055  gen->node = l;
2056  cuddRef(l);
2057 
2058  gen->gen.primes.cube = ABC_ALLOC(int,dd->size);
2059  if (gen->gen.primes.cube == NULL) {
2060  dd->errorCode = CUDD_MEMORY_OUT;
2061  ABC_FREE(gen);
2062  return(NULL);
2063  }
2064 
2065  if (gen->node == Cudd_ReadLogicZero(dd)) {
2066  gen->status = CUDD_GEN_EMPTY;
2067  } else {
2068  implicant = Cudd_LargestCube(dd,gen->node,&length);
2069  if (implicant == NULL) {
2070  Cudd_RecursiveDeref(dd,gen->node);
2071  ABC_FREE(gen->gen.primes.cube);
2072  ABC_FREE(gen);
2073  return(NULL);
2074  }
2075  cuddRef(implicant);
2076  prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2077  if (prime == NULL) {
2078  Cudd_RecursiveDeref(dd,gen->node);
2079  Cudd_RecursiveDeref(dd,implicant);
2080  ABC_FREE(gen->gen.primes.cube);
2081  ABC_FREE(gen);
2082  return(NULL);
2083  }
2084  cuddRef(prime);
2085  Cudd_RecursiveDeref(dd,implicant);
2086  tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2087  if (tmp == NULL) {
2088  Cudd_RecursiveDeref(dd,gen->node);
2089  Cudd_RecursiveDeref(dd,prime);
2090  ABC_FREE(gen->gen.primes.cube);
2091  ABC_FREE(gen);
2092  return(NULL);
2093  }
2094  cuddRef(tmp);
2095  Cudd_RecursiveDeref(dd,gen->node);
2096  gen->node = tmp;
2097  result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2098  if (result == 0) {
2099  Cudd_RecursiveDeref(dd,gen->node);
2100  Cudd_RecursiveDeref(dd,prime);
2101  ABC_FREE(gen->gen.primes.cube);
2102  ABC_FREE(gen);
2103  return(NULL);
2104  }
2105  Cudd_RecursiveDeref(dd,prime);
2106  gen->status = CUDD_GEN_NONEMPTY;
2107  }
2108  *cube = gen->gen.primes.cube;
2109  return(gen);
2110 
2111 } /* end of Cudd_FirstPrime */
2112 
2113 
2114 /**Function********************************************************************
2115 
2116  Synopsis [Generates the next prime of a Boolean function.]
2117 
2118  Description [Generates the next cube of a Boolean function,
2119  using generator gen. Returns 0 if the enumeration is completed; 1
2120  otherwise.]
2121 
2122  SideEffects [The cube and is returned as side effects. The
2123  generator is modified.]
2124 
2125  SeeAlso [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty
2126  Cudd_NextCube Cudd_NextNode]
2127 
2128 ******************************************************************************/
2129 int
2130 Cudd_NextPrime(
2131  DdGen *gen,
2132  int **cube)
2133 {
2134  DdNode *implicant, *prime, *tmp;
2135  DdManager *dd = gen->manager;
2136  int length, result;
2137 
2138  if (gen->node == Cudd_ReadLogicZero(dd)) {
2139  gen->status = CUDD_GEN_EMPTY;
2140  } else {
2141  implicant = Cudd_LargestCube(dd,gen->node,&length);
2142  if (implicant == NULL) {
2143  gen->status = CUDD_GEN_EMPTY;
2144  return(0);
2145  }
2146  cuddRef(implicant);
2147  prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2148  if (prime == NULL) {
2149  Cudd_RecursiveDeref(dd,implicant);
2150  gen->status = CUDD_GEN_EMPTY;
2151  return(0);
2152  }
2153  cuddRef(prime);
2154  Cudd_RecursiveDeref(dd,implicant);
2155  tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2156  if (tmp == NULL) {
2157  Cudd_RecursiveDeref(dd,prime);
2158  gen->status = CUDD_GEN_EMPTY;
2159  return(0);
2160  }
2161  cuddRef(tmp);
2162  Cudd_RecursiveDeref(dd,gen->node);
2163  gen->node = tmp;
2164  result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2165  if (result == 0) {
2166  Cudd_RecursiveDeref(dd,prime);
2167  gen->status = CUDD_GEN_EMPTY;
2168  return(0);
2169  }
2170  Cudd_RecursiveDeref(dd,prime);
2171  gen->status = CUDD_GEN_NONEMPTY;
2172  }
2173  if (gen->status == CUDD_GEN_EMPTY) return(0);
2174  *cube = gen->gen.primes.cube;
2175  return(1);
2176 
2177 } /* end of Cudd_NextPrime */
2178 
2179 
2180 /**Function********************************************************************
2181 
2182  Synopsis [Computes the cube of an array of BDD variables.]
2183 
2184  Description [Computes the cube of an array of BDD variables. If
2185  non-null, the phase argument indicates which literal of each
2186  variable should appear in the cube. If phase\[i\] is nonzero, then the
2187  positive literal is used. If phase is NULL, the cube is positive unate.
2188  Returns a pointer to the result if successful; NULL otherwise.]
2189 
2190  SideEffects [None]
2191 
2192  SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]
2193 
2194 ******************************************************************************/
2195 DdNode *
2196 Cudd_bddComputeCube(
2197  DdManager * dd,
2198  DdNode ** vars,
2199  int * phase,
2200  int n)
2201 {
2202  DdNode *cube;
2203  DdNode *fn;
2204  int i;
2205 
2206  cube = DD_ONE(dd);
2207  cuddRef(cube);
2208 
2209  for (i = n - 1; i >= 0; i--) {
2210  if (phase == NULL || phase[i] != 0) {
2211  fn = Cudd_bddAnd(dd,vars[i],cube);
2212  } else {
2213  fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
2214  }
2215  if (fn == NULL) {
2216  Cudd_RecursiveDeref(dd,cube);
2217  return(NULL);
2218  }
2219  cuddRef(fn);
2220  Cudd_RecursiveDeref(dd,cube);
2221  cube = fn;
2222  }
2223  cuddDeref(cube);
2224 
2225  return(cube);
2226 
2227 } /* end of Cudd_bddComputeCube */
2228 
2229 
2230 /**Function********************************************************************
2231 
2232  Synopsis [Computes the cube of an array of ADD variables.]
2233 
2234  Description [Computes the cube of an array of ADD variables. If
2235  non-null, the phase argument indicates which literal of each
2236  variable should appear in the cube. If phase\[i\] is nonzero, then the
2237  positive literal is used. If phase is NULL, the cube is positive unate.
2238  Returns a pointer to the result if successful; NULL otherwise.]
2239 
2240  SideEffects [none]
2241 
2242  SeeAlso [Cudd_bddComputeCube]
2243 
2244 ******************************************************************************/
2245 DdNode *
2246 Cudd_addComputeCube(
2247  DdManager * dd,
2248  DdNode ** vars,
2249  int * phase,
2250  int n)
2251 {
2252  DdNode *cube, *zero;
2253  DdNode *fn;
2254  int i;
2255 
2256  cube = DD_ONE(dd);
2257  cuddRef(cube);
2258  zero = DD_ZERO(dd);
2259 
2260  for (i = n - 1; i >= 0; i--) {
2261  if (phase == NULL || phase[i] != 0) {
2262  fn = Cudd_addIte(dd,vars[i],cube,zero);
2263  } else {
2264  fn = Cudd_addIte(dd,vars[i],zero,cube);
2265  }
2266  if (fn == NULL) {
2267  Cudd_RecursiveDeref(dd,cube);
2268  return(NULL);
2269  }
2270  cuddRef(fn);
2271  Cudd_RecursiveDeref(dd,cube);
2272  cube = fn;
2273  }
2274  cuddDeref(cube);
2275 
2276  return(cube);
2277 
2278 } /* end of Cudd_addComputeCube */
2279 
2280 
2281 /**Function********************************************************************
2282 
2283  Synopsis [Builds the BDD of a cube from a positional array.]
2284 
2285  Description [Builds a cube from a positional array. The array must
2286  have one integer entry for each BDD variable. If the i-th entry is
2287  1, the variable of index i appears in true form in the cube; If the
2288  i-th entry is 0, the variable of index i appears complemented in the
2289  cube; otherwise the variable does not appear in the cube. Returns a
2290  pointer to the BDD for the cube if successful; NULL otherwise.]
2291 
2292  SideEffects [None]
2293 
2294  SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]
2295 
2296 ******************************************************************************/
2297 DdNode *
2298 Cudd_CubeArrayToBdd(
2299  DdManager *dd,
2300  int *array)
2301 {
2302  DdNode *cube, *var, *tmp;
2303  int i;
2304  int size = Cudd_ReadSize(dd);
2305 
2306  cube = DD_ONE(dd);
2307  cuddRef(cube);
2308  for (i = size - 1; i >= 0; i--) {
2309  if ((array[i] & ~1) == 0) {
2310  var = Cudd_bddIthVar(dd,i);
2311  tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
2312  if (tmp == NULL) {
2313  Cudd_RecursiveDeref(dd,cube);
2314  return(NULL);
2315  }
2316  cuddRef(tmp);
2317  Cudd_RecursiveDeref(dd,cube);
2318  cube = tmp;
2319  }
2320  }
2321  cuddDeref(cube);
2322  return(cube);
2323 
2324 } /* end of Cudd_CubeArrayToBdd */
2325 
2326 
2327 /**Function********************************************************************
2328 
2329  Synopsis [Builds a positional array from the BDD of a cube.]
2330 
2331  Description [Builds a positional array from the BDD of a cube.
2332  Array must have one entry for each BDD variable. The positional
2333  array has 1 in i-th position if the variable of index i appears in
2334  true form in the cube; it has 0 in i-th position if the variable of
2335  index i appears in complemented form in the cube; finally, it has 2
2336  in i-th position if the variable of index i does not appear in the
2337  cube. Returns 1 if successful (the BDD is indeed a cube); 0
2338  otherwise.]
2339 
2340  SideEffects [The result is in the array passed by reference.]
2341 
2342  SeeAlso [Cudd_CubeArrayToBdd]
2343 
2344 ******************************************************************************/
2345 int
2346 Cudd_BddToCubeArray(
2347  DdManager *dd,
2348  DdNode *cube,
2349  int *array)
2350 {
2351  DdNode *scan, *t, *e;
2352  int i;
2353  int size = Cudd_ReadSize(dd);
2354  DdNode *zero = Cudd_Not(DD_ONE(dd));
2355 
2356  for (i = size-1; i >= 0; i--) {
2357  array[i] = 2;
2358  }
2359  scan = cube;
2360  while (!Cudd_IsConstant(scan)) {
2361  int index = Cudd_Regular(scan)->index;
2362  cuddGetBranches(scan,&t,&e);
2363  if (t == zero) {
2364  array[index] = 0;
2365  scan = e;
2366  } else if (e == zero) {
2367  array[index] = 1;
2368  scan = t;
2369  } else {
2370  return(0); /* cube is not a cube */
2371  }
2372  }
2373  if (scan == zero) {
2374  return(0);
2375  } else {
2376  return(1);
2377  }
2378 
2379 } /* end of Cudd_BddToCubeArray */
2380 
2381 
2382 /**Function********************************************************************
2383 
2384  Synopsis [Finds the first node of a decision diagram.]
2385 
2386  Description [Defines an iterator on the nodes of a decision diagram
2387  and finds its first node. Returns a generator that contains the
2388  information necessary to continue the enumeration if successful;
2389  NULL otherwise. The nodes are enumerated in a reverse topological
2390  order, so that a node is always preceded in the enumeration by its
2391  descendants.]
2392 
2393  SideEffects [The first node is returned as a side effect.]
2394 
2395  SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
2396  Cudd_FirstCube]
2397 
2398 ******************************************************************************/
2399 DdGen *
2400 Cudd_FirstNode(
2401  DdManager * dd,
2402  DdNode * f,
2403  DdNode ** node)
2404 {
2405  DdGen *gen;
2406  int size;
2407 
2408  /* Sanity Check. */
2409  if (dd == NULL || f == NULL) return(NULL);
2410 
2411  /* Allocate generator an initialize it. */
2412  gen = ABC_ALLOC(DdGen,1);
2413  if (gen == NULL) {
2414  dd->errorCode = CUDD_MEMORY_OUT;
2415  return(NULL);
2416  }
2417 
2418  gen->manager = dd;
2419  gen->type = CUDD_GEN_NODES;
2420  gen->status = CUDD_GEN_EMPTY;
2421  gen->stack.sp = 0;
2422  gen->node = NULL;
2423 
2424  /* Collect all the nodes on the generator stack for later perusal. */
2425  gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
2426  if (gen->stack.stack == NULL) {
2427  ABC_FREE(gen);
2428  dd->errorCode = CUDD_MEMORY_OUT;
2429  return(NULL);
2430  }
2431  gen->gen.nodes.size = size;
2432 
2433  /* Find the first node. */
2434  if (gen->stack.sp < gen->gen.nodes.size) {
2435  gen->status = CUDD_GEN_NONEMPTY;
2436  gen->node = gen->stack.stack[gen->stack.sp];
2437  *node = gen->node;
2438  }
2439 
2440  return(gen);
2441 
2442 } /* end of Cudd_FirstNode */
2443 
2444 
2445 /**Function********************************************************************
2446 
2447  Synopsis [Finds the next node of a decision diagram.]
2448 
2449  Description [Finds the node of a decision diagram, using generator
2450  gen. Returns 0 if the enumeration is completed; 1 otherwise.]
2451 
2452  SideEffects [The next node is returned as a side effect.]
2453 
2454  SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
2455  Cudd_NextCube]
2456 
2457 ******************************************************************************/
2458 int
2459 Cudd_NextNode(
2460  DdGen * gen,
2461  DdNode ** node)
2462 {
2463  /* Find the next node. */
2464  gen->stack.sp++;
2465  if (gen->stack.sp < gen->gen.nodes.size) {
2466  gen->node = gen->stack.stack[gen->stack.sp];
2467  *node = gen->node;
2468  return(1);
2469  } else {
2470  gen->status = CUDD_GEN_EMPTY;
2471  return(0);
2472  }
2473 
2474 } /* end of Cudd_NextNode */
2475 
2476 
2477 /**Function********************************************************************
2478 
2479  Synopsis [Frees a CUDD generator.]
2480 
2481  Description [Frees a CUDD generator. Always returns 0, so that it can
2482  be used in mis-like foreach constructs.]
2483 
2484  SideEffects [None]
2485 
2486  SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2487  Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
2488 
2489 ******************************************************************************/
2490 int
2491 Cudd_GenFree(
2492  DdGen * gen)
2493 {
2494  if (gen == NULL) return(0);
2495  switch (gen->type) {
2496  case CUDD_GEN_CUBES:
2497  case CUDD_GEN_ZDD_PATHS:
2498  ABC_FREE(gen->gen.cubes.cube);
2499  ABC_FREE(gen->stack.stack);
2500  break;
2501  case CUDD_GEN_PRIMES:
2502  ABC_FREE(gen->gen.primes.cube);
2503  Cudd_RecursiveDeref(gen->manager,gen->node);
2504  break;
2505  case CUDD_GEN_NODES:
2506  ABC_FREE(gen->stack.stack);
2507  break;
2508  default:
2509  return(0);
2510  }
2511  ABC_FREE(gen);
2512  return(0);
2513 
2514 } /* end of Cudd_GenFree */
2515 
2516 
2517 /**Function********************************************************************
2518 
2519  Synopsis [Queries the status of a generator.]
2520 
2521  Description [Queries the status of a generator. Returns 1 if the
2522  generator is empty or NULL; 0 otherswise.]
2523 
2524  SideEffects [None]
2525 
2526  SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2527  Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
2528 
2529 ******************************************************************************/
2530 int
2531 Cudd_IsGenEmpty(
2532  DdGen * gen)
2533 {
2534  if (gen == NULL) return(1);
2535  return(gen->status == CUDD_GEN_EMPTY);
2536 
2537 } /* end of Cudd_IsGenEmpty */
2538 
2539 
2540 /**Function********************************************************************
2541 
2542  Synopsis [Builds a cube of BDD variables from an array of indices.]
2543 
2544  Description [Builds a cube of BDD variables from an array of indices.
2545  Returns a pointer to the result if successful; NULL otherwise.]
2546 
2547  SideEffects [None]
2548 
2549  SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd]
2550 
2551 ******************************************************************************/
2552 DdNode *
2553 Cudd_IndicesToCube(
2554  DdManager * dd,
2555  int * array,
2556  int n)
2557 {
2558  DdNode *cube, *tmp;
2559  int i;
2560 
2561  cube = DD_ONE(dd);
2562  cuddRef(cube);
2563  for (i = n - 1; i >= 0; i--) {
2564  tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
2565  if (tmp == NULL) {
2566  Cudd_RecursiveDeref(dd,cube);
2567  return(NULL);
2568  }
2569  cuddRef(tmp);
2570  Cudd_RecursiveDeref(dd,cube);
2571  cube = tmp;
2572  }
2573 
2574  cuddDeref(cube);
2575  return(cube);
2576 
2577 } /* end of Cudd_IndicesToCube */
2578 
2579 
2580 /**Function********************************************************************
2581 
2582  Synopsis [Prints the package version number.]
2583 
2584  Description []
2585 
2586  SideEffects [None]
2587 
2588  SeeAlso []
2589 
2590 ******************************************************************************/
2591 void
2592 Cudd_PrintVersion(
2593  FILE * fp)
2594 {
2595  (void) fprintf(fp, "%s\n", CUDD_VERSION);
2596 
2597 } /* end of Cudd_PrintVersion */
2598 
2599 
2600 /**Function********************************************************************
2601 
2602  Synopsis [Computes the average distance between adjacent nodes.]
2603 
2604  Description [Computes the average distance between adjacent nodes in
2605  the manager. Adjacent nodes are node pairs such that the second node
2606  is the then child, else child, or next node in the collision list.]
2607 
2608  SideEffects [None]
2609 
2610  SeeAlso []
2611 
2612 ******************************************************************************/
2613 double
2614 Cudd_AverageDistance(
2615  DdManager * dd)
2616 {
2617  double tetotal, nexttotal;
2618  double tesubtotal, nextsubtotal;
2619  double temeasured, nextmeasured;
2620  int i, j;
2621  int slots, nvars;
2622  long diff;
2623  DdNode *scan;
2624  DdNodePtr *nodelist;
2625  DdNode *sentinel = &(dd->sentinel);
2626 
2627  nvars = dd->size;
2628  if (nvars == 0) return(0.0);
2629 
2630  /* Initialize totals. */
2631  tetotal = 0.0;
2632  nexttotal = 0.0;
2633  temeasured = 0.0;
2634  nextmeasured = 0.0;
2635 
2636  /* Scan the variable subtables. */
2637  for (i = 0; i < nvars; i++) {
2638  nodelist = dd->subtables[i].nodelist;
2639  tesubtotal = 0.0;
2640  nextsubtotal = 0.0;
2641  slots = dd->subtables[i].slots;
2642  for (j = 0; j < slots; j++) {
2643  scan = nodelist[j];
2644  while (scan != sentinel) {
2645  diff = (long) scan - (long) cuddT(scan);
2646  tesubtotal += (double) ddAbs(diff);
2647  diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
2648  tesubtotal += (double) ddAbs(diff);
2649  temeasured += 2.0;
2650  if (scan->next != sentinel) {
2651  diff = (long) scan - (long) scan->next;
2652  nextsubtotal += (double) ddAbs(diff);
2653  nextmeasured += 1.0;
2654  }
2655  scan = scan->next;
2656  }
2657  }
2658  tetotal += tesubtotal;
2659  nexttotal += nextsubtotal;
2660  }
2661 
2662  /* Scan the constant table. */
2663  nodelist = dd->constants.nodelist;
2664  nextsubtotal = 0.0;
2665  slots = dd->constants.slots;
2666  for (j = 0; j < slots; j++) {
2667  scan = nodelist[j];
2668  while (scan != NULL) {
2669  if (scan->next != NULL) {
2670  diff = (long) scan - (long) scan->next;
2671  nextsubtotal += (double) ddAbs(diff);
2672  nextmeasured += 1.0;
2673  }
2674  scan = scan->next;
2675  }
2676  }
2677  nexttotal += nextsubtotal;
2678 
2679  return((tetotal + nexttotal) / (temeasured + nextmeasured));
2680 
2681 } /* end of Cudd_AverageDistance */
2682 
2683 
2684 /**Function********************************************************************
2685 
2686  Synopsis [Portable random number generator.]
2687 
2688  Description [Portable number generator based on ran2 from "Numerical
2689  Recipes in C." It is a long period (> 2 * 10^18) random number generator
2690  of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
2691  distributed between 0 and 2147483561 (inclusive of the endpoint values).
2692  The random generator can be explicitly initialized by calling
2693  Cudd_Srandom. If no explicit initialization is performed, then the
2694  seed 1 is assumed.]
2695 
2696  SideEffects [None]
2697 
2698  SeeAlso [Cudd_Srandom]
2699 
2700 ******************************************************************************/
2701 long
2702 Cudd_Random(void)
2703 {
2704  int i; /* index in the shuffle table */
2705  long int w; /* work variable */
2706 
2707  /* cuddRand == 0 if the geneartor has not been initialized yet. */
2708  if (cuddRand == 0) Cudd_Srandom(1);
2709 
2710  /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
2711  ** overflows by Schrage's method.
2712  */
2713  w = cuddRand / LEQQ1;
2714  cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2715  cuddRand += (cuddRand < 0) * MODULUS1;
2716 
2717  /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
2718  ** overflows by Schrage's method.
2719  */
2720  w = cuddRand2 / LEQQ2;
2721  cuddRand2 = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
2722  cuddRand2 += (cuddRand2 < 0) * MODULUS2;
2723 
2724  /* cuddRand is shuffled with the Bays-Durham algorithm.
2725  ** shuffleSelect and cuddRand2 are combined to generate the output.
2726  */
2727 
2728  /* Pick one element from the shuffle table; "i" will be in the range
2729  ** from 0 to STAB_SIZE-1.
2730  */
2731  i = (int) (shuffleSelect / STAB_DIV);
2732  /* Mix the element of the shuffle table with the current iterate of
2733  ** the second sub-generator, and replace the chosen element of the
2734  ** shuffle table with the current iterate of the first sub-generator.
2735  */
2736  shuffleSelect = shuffleTable[i] - cuddRand2;
2737  shuffleTable[i] = cuddRand;
2738  shuffleSelect += (shuffleSelect < 1) * (MODULUS1 - 1);
2739  /* Since shuffleSelect != 0, and we want to be able to return 0,
2740  ** here we subtract 1 before returning.
2741  */
2742  return(shuffleSelect - 1);
2743 
2744 } /* end of Cudd_Random */
2745 
2746 
2747 /**Function********************************************************************
2748 
2749  Synopsis [Initializer for the portable random number generator.]
2750 
2751  Description [Initializer for the portable number generator based on
2752  ran2 in "Numerical Recipes in C." The input is the seed for the
2753  generator. If it is negative, its absolute value is taken as seed.
2754  If it is 0, then 1 is taken as seed. The initialized sets up the two
2755  recurrences used to generate a long-period stream, and sets up the
2756  shuffle table.]
2757 
2758  SideEffects [None]
2759 
2760  SeeAlso [Cudd_Random]
2761 
2762 ******************************************************************************/
2763 void
2764 Cudd_Srandom(
2765  long seed)
2766 {
2767  int i;
2768 
2769  if (seed < 0) cuddRand = -seed;
2770  else if (seed == 0) cuddRand = 1;
2771  else cuddRand = seed;
2772  cuddRand2 = cuddRand;
2773  /* Load the shuffle table (after 11 warm-ups). */
2774  for (i = 0; i < STAB_SIZE + 11; i++) {
2775  long int w;
2776  w = cuddRand / LEQQ1;
2777  cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2778  cuddRand += (cuddRand < 0) * MODULUS1;
2779  shuffleTable[i % STAB_SIZE] = cuddRand;
2780  }
2781  shuffleSelect = shuffleTable[1 % STAB_SIZE];
2782 
2783 } /* end of Cudd_Srandom */
2784 
2785 
2786 /**Function********************************************************************
2787 
2788  Synopsis [Computes the density of a BDD or ADD.]
2789 
2790  Description [Computes the density of a BDD or ADD. The density is
2791  the ratio of the number of minterms to the number of nodes. If 0 is
2792  passed as number of variables, the number of variables existing in
2793  the manager is used. Returns the density if successful; (double)
2794  CUDD_OUT_OF_MEM otherwise.]
2795 
2796  SideEffects [None]
2797 
2798  SeeAlso [Cudd_CountMinterm Cudd_DagSize]
2799 
2800 ******************************************************************************/
2801 double
2802 Cudd_Density(
2803  DdManager * dd /* manager */,
2804  DdNode * f /* function whose density is sought */,
2805  int nvars /* size of the support of f */)
2806 {
2807  double minterms;
2808  int nodes;
2809  double density;
2810 
2811  if (nvars == 0) nvars = dd->size;
2812  minterms = Cudd_CountMinterm(dd,f,nvars);
2813  if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
2814  nodes = Cudd_DagSize(f);
2815  density = minterms / (double) nodes;
2816  return(density);
2817 
2818 } /* end of Cudd_Density */
2819 
2820 
2821 /**Function********************************************************************
2822 
2823  Synopsis [Warns that a memory allocation failed.]
2824 
2825  Description [Warns that a memory allocation failed.
2826  This function can be used as replacement of MMout_of_memory to prevent
2827  the safe_mem functions of the util package from exiting when malloc
2828  returns NULL. One possible use is in case of discretionary allocations;
2829  for instance, the allocation of memory to enlarge the computed table.]
2830 
2831  SideEffects [None]
2832 
2833  SeeAlso []
2834 
2835 ******************************************************************************/
2836 void
2837 Cudd_OutOfMem(
2838  long size /* size of the allocation that failed */)
2839 {
2840  (void) fflush(stdout);
2841  (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
2842  return;
2843 
2844 } /* end of Cudd_OutOfMem */
2845 
2846 
2847 /*---------------------------------------------------------------------------*/
2848 /* Definition of internal functions */
2849 /*---------------------------------------------------------------------------*/
2850 
2851 
2852 /**Function********************************************************************
2853 
2854  Synopsis [Prints a DD to the standard output. One line per node is
2855  printed.]
2856 
2857  Description [Prints a DD to the standard output. One line per node is
2858  printed. Returns 1 if successful; 0 otherwise.]
2859 
2860  SideEffects [None]
2861 
2862  SeeAlso [Cudd_PrintDebug]
2863 
2864 ******************************************************************************/
2865 int
2866 cuddP(
2867  DdManager * dd,
2868  DdNode * f)
2869 {
2870  int retval;
2871  st__table *table = st__init_table( st__ptrcmp, st__ptrhash);
2872 
2873  if (table == NULL) return(0);
2874 
2875  retval = dp2(dd,f,table);
2876  st__free_table(table);
2877  (void) fputc('\n',dd->out);
2878  return(retval);
2879 
2880 } /* end of cuddP */
2881 
2882 
2883 /**Function********************************************************************
2884 
2885  Synopsis [Frees the memory used to store the minterm counts recorded
2886  in the visited table.]
2887 
2888  Description [Frees the memory used to store the minterm counts
2889  recorded in the visited table. Returns st__CONTINUE.]
2890 
2891  SideEffects [None]
2892 
2893 ******************************************************************************/
2894 enum st__retval
2895 cuddStCountfree(
2896  char * key,
2897  char * value,
2898  char * arg)
2899 {
2900  double *d;
2901 
2902  d = (double *)value;
2903  ABC_FREE(d);
2904  return( st__CONTINUE);
2905 
2906 } /* end of cuddStCountfree */
2907 
2908 
2909 /**Function********************************************************************
2910 
2911  Synopsis [Recursively collects all the nodes of a DD in a symbol
2912  table.]
2913 
2914  Description [Traverses the DD f and collects all its nodes in a
2915  symbol table. f is assumed to be a regular pointer and
2916  cuddCollectNodes guarantees this assumption in the recursive calls.
2917  Returns 1 in case of success; 0 otherwise.]
2918 
2919  SideEffects [None]
2920 
2921  SeeAlso []
2922 
2923 ******************************************************************************/
2924 int
2925 cuddCollectNodes(
2926  DdNode * f,
2927  st__table * visited)
2928 {
2929  DdNode *T, *E;
2930  int retval;
2931 
2932 #ifdef DD_DEBUG
2933  assert(!Cudd_IsComplement(f));
2934 #endif
2935 
2936  /* If already visited, nothing to do. */
2937  if ( st__is_member(visited, (char *) f) == 1)
2938  return(1);
2939 
2940  /* Check for abnormal condition that should never happen. */
2941  if (f == NULL)
2942  return(0);
2943 
2944  /* Mark node as visited. */
2945  if ( st__add_direct(visited, (char *) f, NULL) == st__OUT_OF_MEM)
2946  return(0);
2947 
2948  /* Check terminal case. */
2949  if (cuddIsConstant(f))
2950  return(1);
2951 
2952  /* Recursive calls. */
2953  T = cuddT(f);
2954  retval = cuddCollectNodes(T,visited);
2955  if (retval != 1) return(retval);
2956  E = Cudd_Regular(cuddE(f));
2957  retval = cuddCollectNodes(E,visited);
2958  return(retval);
2959 
2960 } /* end of cuddCollectNodes */
2961 
2962 
2963 /**Function********************************************************************
2964 
2965  Synopsis [Recursively collects all the nodes of a DD in an array.]
2966 
2967  Description [Traverses the DD f and collects all its nodes in an array.
2968  The caller should free the array returned by cuddNodeArray.
2969  Returns a pointer to the array of nodes in case of success; NULL
2970  otherwise. The nodes are collected in reverse topological order, so
2971  that a node is always preceded in the array by all its descendants.]
2972 
2973  SideEffects [The number of nodes is returned as a side effect.]
2974 
2975  SeeAlso [Cudd_FirstNode]
2976 
2977 ******************************************************************************/
2978 DdNodePtr *
2979 cuddNodeArray(
2980  DdNode *f,
2981  int *n)
2982 {
2983  DdNodePtr *table;
2984  int size, retval;
2985 
2986  size = ddDagInt(Cudd_Regular(f));
2987  table = ABC_ALLOC(DdNodePtr, size);
2988  if (table == NULL) {
2989  ddClearFlag(Cudd_Regular(f));
2990  return(NULL);
2991  }
2992 
2993  retval = cuddNodeArrayRecur(f, table, 0);
2994  assert(retval == size);
2995 
2996  *n = size;
2997  return(table);
2998 
2999 } /* cuddNodeArray */
3000 
3001 
3002 /*---------------------------------------------------------------------------*/
3003 /* Definition of static functions */
3004 /*---------------------------------------------------------------------------*/
3005 
3006 
3007 /**Function********************************************************************
3008 
3009  Synopsis [Performs the recursive step of cuddP.]
3010 
3011  Description [Performs the recursive step of cuddP. Returns 1 in case
3012  of success; 0 otherwise.]
3013 
3014  SideEffects [None]
3015 
3016 ******************************************************************************/
3017 static int
3018 dp2(
3019  DdManager *dd,
3020  DdNode * f,
3021  st__table * t)
3022 {
3023  DdNode *g, *n, *N;
3024  int T,E;
3025 
3026  if (f == NULL) {
3027  return(0);
3028  }
3029  g = Cudd_Regular(f);
3030  if (cuddIsConstant(g)) {
3031 #if SIZEOF_VOID_P == 8
3032  (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
3033  (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3034 #else
3035  (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
3036  (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3037 #endif
3038  return(1);
3039  }
3040  if ( st__is_member(t,(char *) g) == 1) {
3041  return(1);
3042  }
3043  if ( st__add_direct(t,(char *) g,NULL) == st__OUT_OF_MEM)
3044  return(0);
3045 #ifdef DD_STATS
3046 #if SIZEOF_VOID_P == 8
3047  (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
3048  (ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
3049 #else
3050  (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
3051  (ptruint) g / (ptruint) sizeof(DdNode),g->index,g->ref);
3052 #endif
3053 #else
3054 #if SIZEOF_VOID_P == 8
3055  (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %u\t", bang(f),
3056  (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3057 #else
3058  (void) fprintf(dd->out,"ID = %c0x%x\tindex = %hu\t", bang(f),
3059  (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3060 #endif
3061 #endif
3062  n = cuddT(g);
3063  if (cuddIsConstant(n)) {
3064  (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
3065  T = 1;
3066  } else {
3067 #if SIZEOF_VOID_P == 8
3068  (void) fprintf(dd->out,"T = 0x%lx\t",(ptruint) n / (ptruint) sizeof(DdNode));
3069 #else
3070  (void) fprintf(dd->out,"T = 0x%x\t",(ptruint) n / (ptruint) sizeof(DdNode));
3071 #endif
3072  T = 0;
3073  }
3074 
3075  n = cuddE(g);
3076  N = Cudd_Regular(n);
3077  if (cuddIsConstant(N)) {
3078  (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
3079  E = 1;
3080  } else {
3081 #if SIZEOF_VOID_P == 8
3082  (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3083 #else
3084  (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3085 #endif
3086  E = 0;
3087  }
3088  if (E == 0) {
3089  if (dp2(dd,N,t) == 0)
3090  return(0);
3091  }
3092  if (T == 0) {
3093  if (dp2(dd,cuddT(g),t) == 0)
3094  return(0);
3095  }
3096  return(1);
3097 
3098 } /* end of dp2 */
3099 
3100 
3101 /**Function********************************************************************
3102 
3103  Synopsis [Performs the recursive step of Cudd_PrintMinterm.]
3104 
3105  Description []
3106 
3107  SideEffects [None]
3108 
3109 ******************************************************************************/
3110 static void
3111 ddPrintMintermAux(
3112  DdManager * dd /* manager */,
3113  DdNode * node /* current node */,
3114  int * list /* current recursion path */)
3115 {
3116  DdNode *N,*Nv,*Nnv;
3117  int i,v,index;
3118 
3119  N = Cudd_Regular(node);
3120 
3121  if (cuddIsConstant(N)) {
3122  /* Terminal case: Print one cube based on the current recursion
3123  ** path, unless we have reached the background value (ADDs) or
3124  ** the logical zero (BDDs).
3125  */
3126  if (node != background && node != zero) {
3127  for (i = 0; i < dd->size; i++) {
3128  v = list[i];
3129  if (v == 0) (void) fprintf(dd->out,"0");
3130  else if (v == 1) (void) fprintf(dd->out,"1");
3131  else (void) fprintf(dd->out,"-");
3132  }
3133  (void) fprintf(dd->out," % g\n", cuddV(node));
3134  }
3135  } else {
3136  Nv = cuddT(N);
3137  Nnv = cuddE(N);
3138  if (Cudd_IsComplement(node)) {
3139  Nv = Cudd_Not(Nv);
3140  Nnv = Cudd_Not(Nnv);
3141  }
3142  index = N->index;
3143  list[index] = 0;
3144  ddPrintMintermAux(dd,Nnv,list);
3145  list[index] = 1;
3146  ddPrintMintermAux(dd,Nv,list);
3147  list[index] = 2;
3148  }
3149  return;
3150 
3151 } /* end of ddPrintMintermAux */
3152 
3153 
3154 /**Function********************************************************************
3155 
3156  Synopsis [Performs the recursive step of Cudd_DagSize.]
3157 
3158  Description [Performs the recursive step of Cudd_DagSize. Returns the
3159  number of nodes in the graph rooted at n.]
3160 
3161  SideEffects [None]
3162 
3163 ******************************************************************************/
3164 static int
3165 ddDagInt(
3166  DdNode * n)
3167 {
3168  int tval, eval;
3169 
3170  if (Cudd_IsComplement(n->next)) {
3171  return(0);
3172  }
3173  n->next = Cudd_Not(n->next);
3174  if (cuddIsConstant(n)) {
3175  return(1);
3176  }
3177  tval = ddDagInt(cuddT(n));
3178  eval = ddDagInt(Cudd_Regular(cuddE(n)));
3179  return(1 + tval + eval);
3180 
3181 } /* end of ddDagInt */
3182 
3183 
3184 /**Function********************************************************************
3185 
3186  Synopsis [Performs the recursive step of cuddNodeArray.]
3187 
3188  Description [Performs the recursive step of cuddNodeArray. Returns
3189  an the number of nodes in the DD. Clear the least significant bit
3190  of the next field that was used as visited flag by
3191  cuddNodeArrayRecur when counting the nodes. node is supposed to be
3192  regular; the invariant is maintained by this procedure.]
3193 
3194  SideEffects [None]
3195 
3196  SeeAlso []
3197 
3198 ******************************************************************************/
3199 static int
3200 cuddNodeArrayRecur(
3201  DdNode *f,
3202  DdNodePtr *table,
3203  int index)
3204 {
3205  int tindex, eindex;
3206 
3207  if (!Cudd_IsComplement(f->next)) {
3208  return(index);
3209  }
3210  /* Clear visited flag. */
3211  f->next = Cudd_Regular(f->next);
3212  if (cuddIsConstant(f)) {
3213  table[index] = f;
3214  return(index + 1);
3215  }
3216  tindex = cuddNodeArrayRecur(cuddT(f), table, index);
3217  eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
3218  table[eindex] = f;
3219  return(eindex + 1);
3220 
3221 } /* end of cuddNodeArrayRecur */
3222 
3223 
3224 /**Function********************************************************************
3225 
3226  Synopsis [Performs the recursive step of Cudd_CofactorEstimate.]
3227 
3228  Description [Performs the recursive step of Cudd_CofactorEstimate.
3229  Returns an estimate of the number of nodes in the DD of a
3230  cofactor of node. Uses the least significant bit of the next field as
3231  visited flag. node is supposed to be regular; the invariant is maintained
3232  by this procedure.]
3233 
3234  SideEffects [None]
3235 
3236  SeeAlso []
3237 
3238 ******************************************************************************/
3239 static int
3240 cuddEstimateCofactor(
3241  DdManager *dd,
3242  st__table *table,
3243  DdNode * node,
3244  int i,
3245  int phase,
3246  DdNode ** ptr)
3247 {
3248  int tval, eval, val;
3249  DdNode *ptrT, *ptrE;
3250 
3251  if (Cudd_IsComplement(node->next)) {
3252  if (! st__lookup(table,(char *)node,(char **)ptr)) {
3253  if ( st__add_direct(table,(char *)node,(char *)node) ==
3254  st__OUT_OF_MEM)
3255  return(CUDD_OUT_OF_MEM);
3256  *ptr = node;
3257  }
3258  return(0);
3259  }
3260  node->next = Cudd_Not(node->next);
3261  if (cuddIsConstant(node)) {
3262  *ptr = node;
3263  if ( st__add_direct(table,(char *)node,(char *)node) == st__OUT_OF_MEM)
3264  return(CUDD_OUT_OF_MEM);
3265  return(1);
3266  }
3267  if ((int) node->index == i) {
3268  if (phase == 1) {
3269  *ptr = cuddT(node);
3270  val = ddDagInt(cuddT(node));
3271  } else {
3272  *ptr = cuddE(node);
3273  val = ddDagInt(Cudd_Regular(cuddE(node)));
3274  }
3275  if (node->ref > 1) {
3276  if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
3277  st__OUT_OF_MEM)
3278  return(CUDD_OUT_OF_MEM);
3279  }
3280  return(val);
3281  }
3282  if (dd->perm[node->index] > dd->perm[i]) {
3283  *ptr = node;
3284  tval = ddDagInt(cuddT(node));
3285  eval = ddDagInt(Cudd_Regular(cuddE(node)));
3286  if (node->ref > 1) {
3287  if ( st__add_direct(table,(char *)node,(char *)node) ==
3288  st__OUT_OF_MEM)
3289  return(CUDD_OUT_OF_MEM);
3290  }
3291  val = 1 + tval + eval;
3292  return(val);
3293  }
3294  tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
3295  eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
3296  phase,&ptrE);
3297  ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
3298  if (ptrT == ptrE) { /* recombination */
3299  *ptr = ptrT;
3300  val = tval;
3301  if (node->ref > 1) {
3302  if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
3303  st__OUT_OF_MEM)
3304  return(CUDD_OUT_OF_MEM);
3305  }
3306  } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
3307  (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
3308  if (Cudd_IsComplement((*ptr)->next)) {
3309  val = 0;
3310  } else {
3311  val = 1 + tval + eval;
3312  }
3313  if (node->ref > 1) {
3314  if ( st__add_direct(table,(char *)node,(char *)*ptr) ==
3315  st__OUT_OF_MEM)
3316  return(CUDD_OUT_OF_MEM);
3317  }
3318  } else {
3319  *ptr = node;
3320  val = 1 + tval + eval;
3321  }
3322  return(val);
3323 
3324 } /* end of cuddEstimateCofactor */
3325 
3326 
3327 /**Function********************************************************************
3328 
3329  Synopsis [Checks the unique table for the existence of an internal node.]
3330 
3331  Description [Checks the unique table for the existence of an internal
3332  node. Returns a pointer to the node if it is in the table; NULL otherwise.]
3333 
3334  SideEffects [None]
3335 
3336  SeeAlso [cuddUniqueInter]
3337 
3338 ******************************************************************************/
3339 static DdNode *
3340 cuddUniqueLookup(
3341  DdManager * unique,
3342  int index,
3343  DdNode * T,
3344  DdNode * E)
3345 {
3346  int posn;
3347  unsigned int level;
3348  DdNodePtr *nodelist;
3349  DdNode *looking;
3350  DdSubtable *subtable;
3351 
3352  if (index >= unique->size) {
3353  return(NULL);
3354  }
3355 
3356  level = unique->perm[index];
3357  subtable = &(unique->subtables[level]);
3358 
3359 #ifdef DD_DEBUG
3360  assert(level < (unsigned) cuddI(unique,T->index));
3361  assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
3362 #endif
3363 
3364  posn = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
3365  nodelist = subtable->nodelist;
3366  looking = nodelist[posn];
3367 
3368  while (T < cuddT(looking)) {
3369  looking = Cudd_Regular(looking->next);
3370  }
3371  while (T == cuddT(looking) && E < cuddE(looking)) {
3372  looking = Cudd_Regular(looking->next);
3373  }
3374  if (cuddT(looking) == T && cuddE(looking) == E) {
3375  return(looking);
3376  }
3377 
3378  return(NULL);
3379 
3380 } /* end of cuddUniqueLookup */
3381 
3382 
3383 /**Function********************************************************************
3384 
3385  Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.]
3386 
3387  Description [Performs the recursive step of Cudd_CofactorEstimateSimple.
3388  Returns an estimate of the number of nodes in the DD of the positive
3389  cofactor of node. Uses the least significant bit of the next field as
3390  visited flag. node is supposed to be regular; the invariant is maintained
3391  by this procedure.]
3392 
3393  SideEffects [None]
3394 
3395  SeeAlso []
3396 
3397 ******************************************************************************/
3398 static int
3399 cuddEstimateCofactorSimple(
3400  DdNode * node,
3401  int i)
3402 {
3403  int tval, eval;
3404 
3405  if (Cudd_IsComplement(node->next)) {
3406  return(0);
3407  }
3408  node->next = Cudd_Not(node->next);
3409  if (cuddIsConstant(node)) {
3410  return(1);
3411  }
3412  tval = cuddEstimateCofactorSimple(cuddT(node),i);
3413  if ((int) node->index == i) return(tval);
3414  eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
3415  return(1 + tval + eval);
3416 
3417 } /* end of cuddEstimateCofactorSimple */
3418 
3419 
3420 /**Function********************************************************************
3421 
3422  Synopsis [Performs the recursive step of Cudd_CountMinterm.]
3423 
3424  Description [Performs the recursive step of Cudd_CountMinterm.
3425  It is based on the following identity. Let |f| be the
3426  number of minterms of f. Then:
3427  <xmp>
3428  |f| = (|f0|+|f1|)/2
3429  </xmp>
3430  where f0 and f1 are the two cofactors of f. Does not use the
3431  identity |f'| = max - |f|, to minimize loss of accuracy due to
3432  roundoff. Returns the number of minterms of the function rooted at
3433  node.]
3434 
3435  SideEffects [None]
3436 
3437 ******************************************************************************/
3438 static double
3439 ddCountMintermAux(
3440  DdNode * node,
3441  double max,
3442  DdHashTable * table)
3443 {
3444  DdNode *N, *Nt, *Ne;
3445  double min, minT, minE;
3446  DdNode *res;
3447 
3448  N = Cudd_Regular(node);
3449 
3450  if (cuddIsConstant(N)) {
3451  if (node == background || node == zero) {
3452  return(0.0);
3453  } else {
3454  return(max);
3455  }
3456  }
3457  if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
3458  min = cuddV(res);
3459  if (res->ref == 0) {
3460  table->manager->dead++;
3461  table->manager->constants.dead++;
3462  }
3463  return(min);
3464  }
3465 
3466  Nt = cuddT(N); Ne = cuddE(N);
3467  if (Cudd_IsComplement(node)) {
3468  Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3469  }
3470 
3471  minT = ddCountMintermAux(Nt,max,table);
3472  if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3473  minT *= 0.5;
3474  minE = ddCountMintermAux(Ne,max,table);
3475  if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3476  minE *= 0.5;
3477  min = minT + minE;
3478 
3479  if (N->ref != 1) {
3480  ptrint fanout = (ptrint) N->ref;
3481  cuddSatDec(fanout);
3482  res = cuddUniqueConst(table->manager,min);
3483  if (!cuddHashTableInsert1(table,node,res,fanout)) {
3484  cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
3485  return((double)CUDD_OUT_OF_MEM);
3486  }
3487  }
3488 
3489  return(min);
3490 
3491 } /* end of ddCountMintermAux */
3492 
3493 
3494 /**Function********************************************************************
3495 
3496  Synopsis [Performs the recursive step of Cudd_CountPath.]
3497 
3498  Description [Performs the recursive step of Cudd_CountPath.
3499  It is based on the following identity. Let |f| be the
3500  number of paths of f. Then:
3501  <xmp>
3502  |f| = |f0|+|f1|
3503  </xmp>
3504  where f0 and f1 are the two cofactors of f. Uses the
3505  identity |f'| = |f|, to improve the utilization of the (local) cache.
3506  Returns the number of paths of the function rooted at node.]
3507 
3508  SideEffects [None]
3509 
3510 ******************************************************************************/
3511 static double
3512 ddCountPathAux(
3513  DdNode * node,
3514  st__table * table)
3515 {
3516 
3517  DdNode *Nv, *Nnv;
3518  double paths, *ppaths, paths1, paths2;
3519  double *dummy;
3520 
3521 
3522  if (cuddIsConstant(node)) {
3523  return(1.0);
3524  }
3525  if ( st__lookup(table, (const char *)node, (char **)&dummy)) {
3526  paths = *dummy;
3527  return(paths);
3528  }
3529 
3530  Nv = cuddT(node); Nnv = cuddE(node);
3531 
3532  paths1 = ddCountPathAux(Nv,table);
3533  if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3534  paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
3535  if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3536  paths = paths1 + paths2;
3537 
3538  ppaths = ABC_ALLOC(double,1);
3539  if (ppaths == NULL) {
3540  return((double)CUDD_OUT_OF_MEM);
3541  }
3542 
3543  *ppaths = paths;
3544 
3545  if ( st__add_direct(table,(char *)node, (char *)ppaths) == st__OUT_OF_MEM) {
3546  ABC_FREE(ppaths);
3547  return((double)CUDD_OUT_OF_MEM);
3548  }
3549  return(paths);
3550 
3551 } /* end of ddCountPathAux */
3552 
3553 
3554 /**Function********************************************************************
3555 
3556  Synopsis [Performs the recursive step of Cudd_EpdCountMinterm.]
3557 
3558  Description [Performs the recursive step of Cudd_EpdCountMinterm.
3559  It is based on the following identity. Let |f| be the
3560  number of minterms of f. Then:
3561  <xmp>
3562  |f| = (|f0|+|f1|)/2
3563  </xmp>
3564  where f0 and f1 are the two cofactors of f. Does not use the
3565  identity |f'| = max - |f|, to minimize loss of accuracy due to
3566  roundoff. Returns the number of minterms of the function rooted at
3567  node.]
3568 
3569  SideEffects [None]
3570 
3571 ******************************************************************************/
3572 static int
3573 ddEpdCountMintermAux(
3574  DdNode * node,
3575  EpDouble * max,
3576  EpDouble * epd,
3577  st__table * table)
3578 {
3579  DdNode *Nt, *Ne;
3580  EpDouble *min, minT, minE;
3581  EpDouble *res;
3582  int status;
3583 
3584  /* node is assumed to be regular */
3585  if (cuddIsConstant(node)) {
3586  if (node == background || node == zero) {
3587  EpdMakeZero(epd, 0);
3588  } else {
3589  EpdCopy(max, epd);
3590  }
3591  return(0);
3592  }
3593  if (node->ref != 1 && st__lookup(table, (const char *)node, (char **)&res)) {
3594  EpdCopy(res, epd);
3595  return(0);
3596  }
3597 
3598  Nt = cuddT(node); Ne = cuddE(node);
3599 
3600  status = ddEpdCountMintermAux(Nt,max,&minT,table);
3601  if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3602  EpdMultiply(&minT, (double)0.5);
3603  status = ddEpdCountMintermAux(Cudd_Regular(Ne),max,&minE,table);
3604  if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3605  if (Cudd_IsComplement(Ne)) {
3606  EpdSubtract3(max, &minE, epd);
3607  EpdCopy(epd, &minE);
3608  }
3609  EpdMultiply(&minE, (double)0.5);
3610  EpdAdd3(&minT, &minE, epd);
3611 
3612  if (node->ref > 1) {
3613  min = EpdAlloc();
3614  if (!min)
3615  return(CUDD_OUT_OF_MEM);
3616  EpdCopy(epd, min);
3617  if ( st__insert(table, (char *)node, (char *)min) == st__OUT_OF_MEM) {
3618  EpdFree(min);
3619  return(CUDD_OUT_OF_MEM);
3620  }
3621  }
3622 
3623  return(0);
3624 
3625 } /* end of ddEpdCountMintermAux */
3626 
3627 
3628 /**Function********************************************************************
3629 
3630  Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.]
3631 
3632  Description [Performs the recursive step of Cudd_CountPathsToNonZero.
3633  It is based on the following identity. Let |f| be the
3634  number of paths of f. Then:
3635  <xmp>
3636  |f| = |f0|+|f1|
3637  </xmp>
3638  where f0 and f1 are the two cofactors of f. Returns the number of
3639  paths of the function rooted at node.]
3640 
3641  SideEffects [None]
3642 
3643 ******************************************************************************/
3644 static double
3645 ddCountPathsToNonZero(
3646  DdNode * N,
3647  st__table * table)
3648 {
3649 
3650  DdNode *node, *Nt, *Ne;
3651  double paths, *ppaths, paths1, paths2;
3652  double *dummy;
3653 
3654  node = Cudd_Regular(N);
3655  if (cuddIsConstant(node)) {
3656  return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
3657  }
3658  if ( st__lookup(table, (const char *)N, (char **)&dummy)) {
3659  paths = *dummy;
3660  return(paths);
3661  }
3662 
3663  Nt = cuddT(node); Ne = cuddE(node);
3664  if (node != N) {
3665  Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3666  }
3667 
3668  paths1 = ddCountPathsToNonZero(Nt,table);
3669  if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3670  paths2 = ddCountPathsToNonZero(Ne,table);
3671  if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3672  paths = paths1 + paths2;
3673 
3674  ppaths = ABC_ALLOC(double,1);
3675  if (ppaths == NULL) {
3676  return((double)CUDD_OUT_OF_MEM);
3677  }
3678 
3679  *ppaths = paths;
3680 
3681  if ( st__add_direct(table,(char *)N, (char *)ppaths) == st__OUT_OF_MEM) {
3682  ABC_FREE(ppaths);
3683  return((double)CUDD_OUT_OF_MEM);
3684  }
3685  return(paths);
3686 
3687 } /* end of ddCountPathsToNonZero */
3688 
3689 
3690 /**Function********************************************************************
3691 
3692  Synopsis [Performs the recursive step of Cudd_Support.]
3693 
3694  Description [Performs the recursive step of Cudd_Support. Performs a
3695  DFS from f. The support is accumulated in supp as a side effect. Uses
3696  the LSB of the then pointer as visited flag.]
3697 
3698  SideEffects [None]
3699 
3700  SeeAlso [ddClearFlag]
3701 
3702 ******************************************************************************/
3703 static void
3704 ddSupportStep(
3705  DdNode * f,
3706  int * support)
3707 {
3708  if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
3709  return;
3710  }
3711 
3712  support[f->index] = 1;
3713  ddSupportStep(cuddT(f),support);
3714  ddSupportStep(Cudd_Regular(cuddE(f)),support);
3715  /* Mark as visited. */
3716  f->next = Cudd_Not(f->next);
3717  return;
3718 
3719 } /* end of ddSupportStep */
3720 
3721 
3722 /**Function********************************************************************
3723 
3724  Synopsis [Performs a DFS from f, clearing the LSB of the next
3725  pointers.]
3726 
3727  Description []
3728 
3729  SideEffects [None]
3730 
3731  SeeAlso [ddSupportStep ddDagInt]
3732 
3733 ******************************************************************************/
3734 static void
3735 ddClearFlag(
3736  DdNode * f)
3737 {
3738  if (!Cudd_IsComplement(f->next)) {
3739  return;
3740  }
3741  /* Clear visited flag. */
3742  f->next = Cudd_Regular(f->next);
3743  if (cuddIsConstant(f)) {
3744  return;
3745  }
3746  ddClearFlag(cuddT(f));
3747  ddClearFlag(Cudd_Regular(cuddE(f)));
3748  return;
3749 
3750 } /* end of ddClearFlag */
3751 
3752 
3753 /**Function********************************************************************
3754 
3755  Synopsis [Performs the recursive step of Cudd_CountLeaves.]
3756 
3757  Description [Performs the recursive step of Cudd_CountLeaves. Returns
3758  the number of leaves in the DD rooted at n.]
3759 
3760  SideEffects [None]
3761 
3762  SeeAlso [Cudd_CountLeaves]
3763 
3764 ******************************************************************************/
3765 static int
3766 ddLeavesInt(
3767  DdNode * n)
3768 {
3769  int tval, eval;
3770 
3771  if (Cudd_IsComplement(n->next)) {
3772  return(0);
3773  }
3774  n->next = Cudd_Not(n->next);
3775  if (cuddIsConstant(n)) {
3776  return(1);
3777  }
3778  tval = ddLeavesInt(cuddT(n));
3779  eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
3780  return(tval + eval);
3781 
3782 } /* end of ddLeavesInt */
3783 
3784 
3785 /**Function********************************************************************
3786 
3787  Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]
3788 
3789  Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms.
3790  Returns 1 if successful; 0 otherwise.]
3791 
3792  SideEffects [none]
3793 
3794  SeeAlso [Cudd_bddPickArbitraryMinterms]
3795 
3796 ******************************************************************************/
3797 static int
3798 ddPickArbitraryMinterms(
3799  DdManager *dd,
3800  DdNode *node,
3801  int nvars,
3802  int nminterms,
3803  char **string)
3804 {
3805  DdNode *N, *T, *E;
3806  DdNode *one, *bzero;
3807  int i, t, result;
3808  double min1, min2;
3809 
3810  if (string == NULL || node == NULL) return(0);
3811 
3812  /* The constant 0 function has no on-set cubes. */
3813  one = DD_ONE(dd);
3814  bzero = Cudd_Not(one);
3815  if (nminterms == 0 || node == bzero) return(1);
3816  if (node == one) {
3817  return(1);
3818  }
3819 
3820  N = Cudd_Regular(node);
3821  T = cuddT(N); E = cuddE(N);
3822  if (Cudd_IsComplement(node)) {
3823  T = Cudd_Not(T); E = Cudd_Not(E);
3824  }
3825 
3826  min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
3827  if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
3828  min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
3829  if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
3830 
3831  t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
3832  for (i = 0; i < t; i++)
3833  string[i][N->index] = '1';
3834  for (i = t; i < nminterms; i++)
3835  string[i][N->index] = '0';
3836 
3837  result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
3838  if (result == 0)
3839  return(0);
3840  result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
3841  return(result);
3842 
3843 } /* end of ddPickArbitraryMinterms */
3844 
3845 
3846 /**Function********************************************************************
3847 
3848  Synopsis [Finds a representative cube of a BDD.]
3849 
3850  Description [Finds a representative cube of a BDD with the weight of
3851  each variable. From the top variable, if the weight is greater than or
3852  equal to 0.0, choose THEN branch unless the child is the constant 0.
3853  Otherwise, choose ELSE branch unless the child is the constant 0.]
3854 
3855  SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]
3856 
3857 ******************************************************************************/
3858 static int
3859 ddPickRepresentativeCube(
3860  DdManager *dd,
3861  DdNode *node,
3862  double *weight,
3863  char *string)
3864 {
3865  DdNode *N, *T, *E;
3866  DdNode *one, *bzero;
3867 
3868  if (string == NULL || node == NULL) return(0);
3869 
3870  /* The constant 0 function has no on-set cubes. */
3871  one = DD_ONE(dd);
3872  bzero = Cudd_Not(one);
3873  if (node == bzero) return(0);
3874 
3875  if (node == DD_ONE(dd)) return(1);
3876 
3877  for (;;) {
3878  N = Cudd_Regular(node);
3879  if (N == one)
3880  break;
3881  T = cuddT(N);
3882  E = cuddE(N);
3883  if (Cudd_IsComplement(node)) {
3884  T = Cudd_Not(T);
3885  E = Cudd_Not(E);
3886  }
3887  if (weight[N->index] >= 0.0) {
3888  if (T == bzero) {
3889  node = E;
3890  string[N->index] = '0';
3891  } else {
3892  node = T;
3893  string[N->index] = '1';
3894  }
3895  } else {
3896  if (E == bzero) {
3897  node = T;
3898  string[N->index] = '1';
3899  } else {
3900  node = E;
3901  string[N->index] = '0';
3902  }
3903  }
3904  }
3905  return(1);
3906 
3907 } /* end of ddPickRepresentativeCube */
3908 
3909 
3910 /**Function********************************************************************
3911 
3912  Synopsis [Frees the memory used to store the minterm counts recorded
3913  in the visited table.]
3914 
3915  Description [Frees the memory used to store the minterm counts
3916  recorded in the visited table. Returns st__CONTINUE.]
3917 
3918  SideEffects [None]
3919 
3920 ******************************************************************************/
3921 static enum st__retval
3922 ddEpdFree(
3923  char * key,
3924  char * value,
3925  char * arg)
3926 {
3927  EpDouble *epd;
3928 
3929  epd = (EpDouble *) value;
3930  EpdFree(epd);
3931  return( st__CONTINUE);
3932 
3933 } /* end of ddEpdFree */
3934 
3935 
3936 ABC_NAMESPACE_IMPL_END
3937 
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
Cudd_bddPickOneMinterm
DdNode * Cudd_bddPickOneMinterm(DdManager *dd, DdNode *f, DdNode **vars, int n)
Definition: cuddUtil.c:1291
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
ddCountPathsToNonZero
static double ddCountPathsToNonZero(DdNode *N, st__table *table)
Definition: cuddUtil.c:3645
DdGen::node
DdNode * node
Definition: cuddInt.h:232
Cudd_FirstPrime
DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube)
Definition: cuddUtil.c:2028
Cudd_SubsetWithMaskVars
DdNode * Cudd_SubsetWithMaskVars(DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars)
Definition: cuddUtil.c:1602
CUDD_OUT_OF_MEM
#define CUDD_OUT_OF_MEM
Definition: cudd.h:95
Cudd_NextNode
int Cudd_NextNode(DdGen *gen, DdNode **node)
Definition: cuddUtil.c:2459
Cudd_bddPickArbitraryMinterms
DdNode ** Cudd_bddPickArbitraryMinterms(DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
Definition: cuddUtil.c:1393
DdGen::type
int type
Definition: cuddInt.h:206
cuddEstimateCofactor
static int cuddEstimateCofactor(DdManager *dd, st__table *table, DdNode *node, int i, int phase, DdNode **ptr)
Definition: cuddUtil.c:3240
ddHash
#define ddHash(f, g, s)
Definition: cuddInt.h:737
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
CUDD_VERSION
#define CUDD_VERSION
Definition: cudd.h:75
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
EpdCmp
int EpdCmp(const char *key1, const char *key2)
Definition: epd.c:93
Cudd_Density
double Cudd_Density(DdManager *dd, DdNode *f, int nvars)
Definition: cuddUtil.c:2802
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Cudd_Srandom
void Cudd_Srandom(long seed)
Definition: cuddUtil.c:2764
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_PrintVersion
void Cudd_PrintVersion(FILE *fp)
Definition: cuddUtil.c:2592
CUDD_GEN_ZDD_PATHS
#define CUDD_GEN_ZDD_PATHS
Definition: cuddInt.h:195
LEQQ1
#define LEQQ1
Definition: cuddUtil.c:122
DdGen::cubes
struct DdGen::@30::@32 cubes
EpdCopy
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Cudd_bddComputeCube
DdNode * Cudd_bddComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Definition: cuddUtil.c:2196
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
DdHashTable::manager
DdManager * manager
Definition: cuddInt.h:313
LEQQ2
#define LEQQ2
Definition: cuddUtil.c:126
CUDD_GEN_NODES
#define CUDD_GEN_NODES
Definition: cuddInt.h:194
ddPickArbitraryMinterms
static int ddPickArbitraryMinterms(DdManager *dd, DdNode *node, int nvars, int nminterms, char **string)
Definition: cuddUtil.c:3798
DdManager::size
int size
Definition: cuddInt.h:361
cuddEstimateCofactorSimple
static int cuddEstimateCofactorSimple(DdNode *node, int i)
Definition: cuddUtil.c:3399
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
dp2
static int dp2(DdManager *dd, DdNode *f, st__table *t)
Definition: cuddUtil.c:3018
Cudd_PrintDebug
int Cudd_PrintDebug(DdManager *dd, DdNode *f, int n, int pr)
Definition: cuddUtil.c:382
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddStCountfree
enum st__retval cuddStCountfree(char *key, char *value, char *arg)
Definition: cuddUtil.c:2895
ddEpdFree
static enum st__retval ddEpdFree(char *key, char *value, char *arg)
Definition: cuddUtil.c:3922
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
Cudd_EstimateCofactor
int Cudd_EstimateCofactor(DdManager *dd, DdNode *f, int i, int phase)
Definition: cuddUtil.c:477
Cudd_OutOfMem
void Cudd_OutOfMem(long size)
Definition: cuddUtil.c:2837
cuddUniqueLookup
static DdNode * cuddUniqueLookup(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddUtil.c:3340
MODULUS1
#define MODULUS1
Definition: cuddUtil.c:120
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
cuddGetBranches
void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0)
Definition: cuddCof.c:162
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdGen
Definition: cuddInt.h:204
DdManager::subtables
DdSubtable * subtables
Definition: cuddInt.h:365
DD_ZERO_VAL
#define DD_ZERO_VAL
Definition: cuddInt.h:108
Cudd_FirstCube
DdGen * Cudd_FirstCube(DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
Definition: cuddUtil.c:1798
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Cudd_addComputeCube
DdNode * Cudd_addComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Definition: cuddUtil.c:2246
st__is_member
#define st__is_member(table, key)
Definition: st.h:70
Cudd_FirstNode
DdGen * Cudd_FirstNode(DdManager *dd, DdNode *f, DdNode **node)
Definition: cuddUtil.c:2400
background
static DdNode * background
Definition: cuddUtil.c:148
ddPickRepresentativeCube
static int ddPickRepresentativeCube(DdManager *dd, DdNode *node, double *weight, char *string)
Definition: cuddUtil.c:3859
LEQR2
#define LEQR2
Definition: cuddUtil.c:127
Cudd_NextCube
int Cudd_NextCube(DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
Definition: cuddUtil.c:1917
EpdPow2
void EpdPow2(int n, EpDouble *epd)
Definition: epd.c:917
for
for(p=first;p->value< newval;p=p->next)
cuddHashTableLookup1
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
Definition: cuddLCache.c:819
EpdSubtract3
void EpdSubtract3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
Definition: epd.c:850
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
bang
#define bang(f)
Definition: cuddUtil.c:159
Cudd_CountPathsToNonZero
double Cudd_CountPathsToNonZero(DdNode *node)
Definition: cuddUtil.c:707
CUDD_GEN_NONEMPTY
#define CUDD_GEN_NONEMPTY
Definition: cuddInt.h:197
DdNode
struct DdNode DdNode
Definition: cudd.h:270
util_hack.h
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
Cudd_LargestCube
DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length)
Definition: cuddSat.c:285
shuffleSelect
static long shuffleSelect
Definition: cuddUtil.c:152
strcmp
int strcmp()
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
ptruint
ABC_PTRUINT_T ptruint
Definition: cuddInt.h:261
st__retval
st__retval
Definition: st.h:73
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Cudd_Random
long Cudd_Random(void)
Definition: cuddUtil.c:2702
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
shuffleTable
static long shuffleTable[STAB_SIZE]
Definition: cuddUtil.c:153
cuddRand
static long cuddRand
Definition: cuddUtil.c:150
Cudd_AverageDistance
double Cudd_AverageDistance(DdManager *dd)
Definition: cuddUtil.c:2614
STAB_SIZE
#define STAB_SIZE
Definition: cuddUtil.c:128
Cudd_bddPrintCover
int Cudd_bddPrintCover(DdManager *dd, DdNode *l, DdNode *u)
Definition: cuddUtil.c:253
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DD_UNUSED
static char rcsid[] DD_UNUSED
Definition: cuddUtil.c:145
Cudd_SetEpsilon
void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep)
Definition: cuddAPI.c:2451
DdManager::sentinel
DdNode sentinel
Definition: cuddInt.h:344
Cudd_bddMakePrime
DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
Definition: cuddSat.c:864
EpdAdd3
void EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
Definition: epd.c:660
Cudd_BddToCubeArray
int Cudd_BddToCubeArray(DdManager *dd, DdNode *cube, int *array)
Definition: cuddUtil.c:2346
DdGen::stack
DdNode ** stack
Definition: cuddInt.h:227
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
Cudd_IndicesToCube
DdNode * Cudd_IndicesToCube(DdManager *dd, int *array, int n)
Definition: cuddUtil.c:2553
Cudd_NextPrime
int Cudd_NextPrime(DdGen *gen, int **cube)
Definition: cuddUtil.c:2130
DdSubtable::dead
unsigned int dead
Definition: cuddInt.h:332
one
static DdNode * one
Definition: cuddDecomp.c:112
DdManager::out
FILE * out
Definition: cuddInt.h:441
Cudd_GenFree
int Cudd_GenFree(DdGen *gen)
Definition: cuddUtil.c:2491
ptrint
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
LEQA2
#define LEQA2
Definition: cuddUtil.c:125
st__table
Definition: st.h:52
Cudd_PrintMinterm
int Cudd_PrintMinterm(DdManager *manager, DdNode *node)
Definition: cuddUtil.c:216
DdNode::next
DdNode * next
Definition: cudd.h:281
DdGen::manager
DdManager * manager
Definition: cuddInt.h:205
Cudd_VectorSupport
DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:908
ddSupportStep
static void ddSupportStep(DdNode *f, int *support)
Definition: cuddUtil.c:3704
ddAbs
#define ddAbs(x)
Definition: cuddInt.h:846
Cudd_CountLeaves
int Cudd_CountLeaves(DdNode *node)
Definition: cuddUtil.c:1194
Cudd_CountPath
double Cudd_CountPath(DdNode *node)
Definition: cuddUtil.c:623
ddPrintMintermAux
static void ddPrintMintermAux(DdManager *dd, DdNode *node, int *list)
Definition: cuddUtil.c:3111
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ddMax
#define ddMax(x, y)
Definition: cuddInt.h:832
zero
static DdNode * zero
Definition: cuddUtil.c:148
if
if(last==0)
Definition: sparse_int.h:34
max
static double max
Definition: cuddSubsetHB.c:134
EpdMakeZero
void EpdMakeZero(EpDouble *epd, int sign)
Definition: epd.c:1137
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:327
size
static int size
Definition: cuddSign.c:86
Cudd_EpdCountMinterm
int Cudd_EpdCountMinterm(DdManager *manager, DdNode *node, int nvars, EpDouble *epd)
Definition: cuddUtil.c:657
ddCountPathAux
static double ddCountPathAux(DdNode *node, st__table *table)
Definition: cuddUtil.c:3512
cuddF2L
#define cuddF2L(f)
Definition: cuddInt.h:718
cuddP
int cuddP(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:2866
EpdAlloc
ABC_NAMESPACE_IMPL_START EpDouble * EpdAlloc(void)
Definition: epd.c:72
cuddNodeArray
DdNodePtr * cuddNodeArray(DdNode *f, int *n)
Definition: cuddUtil.c:2979
ddDagInt
static int ddDagInt(DdNode *n)
Definition: cuddUtil.c:3165
LEQR1
#define LEQR1
Definition: cuddUtil.c:123
st__foreach
int st__foreach(st__table *table, enum st__retval(*func)(char *, char *, char *), char *arg)
Definition: st.c:421
cuddHashTableQuit
void cuddHashTableQuit(DdHashTable *hash)
Definition: cuddLCache.c:595
Cudd_IsGenEmpty
int Cudd_IsGenEmpty(DdGen *gen)
Definition: cuddUtil.c:2531
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
strcpy
char * strcpy()
st__OUT_OF_MEM
#define st__OUT_OF_MEM
Definition: st.h:113
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdGen::gen
union DdGen::@30 gen
phase
static pcube phase
Definition: cvrm.c:405
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
ddLeavesInt
static int ddLeavesInt(DdNode *n)
Definition: cuddUtil.c:3766
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
Cudd_bddPickOneCube
int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string)
Definition: cuddUtil.c:1221
cuddHashTableInsert1
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
Definition: cuddLCache.c:767
Cudd_CubeArrayToBdd
DdNode * Cudd_CubeArrayToBdd(DdManager *dd, int *array)
Definition: cuddUtil.c:2298
CUDD_GEN_EMPTY
#define CUDD_GEN_EMPTY
Definition: cuddInt.h:196
DdGen::primes
struct DdGen::@30::@33 primes
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:329
key
enum keys key
Definition: misc/espresso/main.h:25
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
CUDD_GEN_CUBES
#define CUDD_GEN_CUBES
Definition: cuddInt.h:192
Cudd_VectorSupportIndex
int * Cudd_VectorSupportIndex(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:980
DdManager::one
DdNode * one
Definition: cuddInt.h:345
STAB_DIV
#define STAB_DIV
Definition: cuddUtil.c:129
cuddRand2
static long cuddRand2
Definition: cuddUtil.c:151
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
st__add_direct
int st__add_direct(st__table *table, char *key, char *value)
Definition: st.c:205
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
EpdMultiply
void EpdMultiply(EpDouble *epd1, double value)
Definition: epd.c:205
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
cuddCollectNodes
int cuddCollectNodes(DdNode *f, st__table *visited)
Definition: cuddUtil.c:2925
ddClearFlag
static void ddClearFlag(DdNode *f)
Definition: cuddUtil.c:3735
value
int value
Definition: misc/espresso/main.h:90
ddCountMintermAux
static double ddCountMintermAux(DdNode *node, double max, DdHashTable *table)
Definition: cuddUtil.c:3439
cuddSatDec
#define cuddSatDec(x)
Definition: cuddInt.h:896
DdGen::nodes
struct DdGen::@30::@34 nodes
cuddHashTableInit
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Definition: cuddLCache.c:538
EpdFree
void EpdFree(EpDouble *epd)
Definition: epd.c:117
MODULUS2
#define MODULUS2
Definition: cuddUtil.c:124
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_EstimateCofactorSimple
int Cudd_EstimateCofactorSimple(DdNode *node, int i)
Definition: cuddUtil.c:517
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
Cudd_VectorSupportSize
int Cudd_VectorSupportSize(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:1028
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:367
result
static int result
Definition: cuddGenetic.c:125
Cudd_SupportIndex
int * Cudd_SupportIndex(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:815
ddEpdCountMintermAux
static int ddEpdCountMintermAux(DdNode *node, EpDouble *max, EpDouble *epd, st__table *table)
Definition: cuddUtil.c:3573
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdSubtable::shift
int shift
Definition: cuddInt.h:328
Cudd_ClassifySupport
int Cudd_ClassifySupport(DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG)
Definition: cuddUtil.c:1085
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
CUDD_GEN_PRIMES
#define CUDD_GEN_PRIMES
Definition: cuddInt.h:193
LEQA1
#define LEQA1
Definition: cuddUtil.c:121
DdManager::perm
int * perm
Definition: cuddInt.h:386
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
Cudd_ReadEpsilon
CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd)
Definition: cuddAPI.c:2430
minterms
pset minterms()
DdManager::background
DdNode * background
Definition: cuddInt.h:349
cuddNodeArrayRecur
static int cuddNodeArrayRecur(DdNode *f, DdNodePtr *table, int index)
Definition: cuddUtil.c:3200
DdGen::status
int status
Definition: cuddInt.h:207
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927