abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddCompose.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddCompose.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Functional composition and variable permutation of DDs.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_bddCompose()
12  <li> Cudd_addCompose()
13  <li> Cudd_addPermute()
14  <li> Cudd_addSwapVariables()
15  <li> Cudd_bddPermute()
16  <li> Cudd_bddVarMap()
17  <li> Cudd_SetVarMap()
18  <li> Cudd_bddSwapVariables()
19  <li> Cudd_bddAdjPermuteX()
20  <li> Cudd_addVectorCompose()
21  <li> Cudd_addGeneralVectorCompose()
22  <li> Cudd_addNonSimCompose()
23  <li> Cudd_bddVectorCompose()
24  </ul>
25  Internal procedures included in this module:
26  <ul>
27  <li> cuddBddComposeRecur()
28  <li> cuddAddComposeRecur()
29  </ul>
30  Static procedures included in this module:
31  <ul>
32  <li> cuddAddPermuteRecur()
33  <li> cuddBddPermuteRecur()
34  <li> cuddBddVarMapRecur()
35  <li> cuddAddVectorComposeRecur()
36  <li> cuddAddGeneralVectorComposeRecur()
37  <li> cuddAddNonSimComposeRecur()
38  <li> cuddBddVectorComposeRecur()
39  <li> ddIsIthAddVar()
40  <li> ddIsIthAddVarPair()
41  </ul>
42  The permutation functions use a local cache because the results to
43  be remembered depend on the permutation being applied. Since the
44  permutation is just an array, it cannot be stored in the global
45  cache. There are different procedured for BDDs and ADDs. This is
46  because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
47  the procedures could be merged.]
48 
49  Author [Fabio Somenzi and Kavita Ravi]
50 
51  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
52 
53  All rights reserved.
54 
55  Redistribution and use in source and binary forms, with or without
56  modification, are permitted provided that the following conditions
57  are met:
58 
59  Redistributions of source code must retain the above copyright
60  notice, this list of conditions and the following disclaimer.
61 
62  Redistributions in binary form must reproduce the above copyright
63  notice, this list of conditions and the following disclaimer in the
64  documentation and/or other materials provided with the distribution.
65 
66  Neither the name of the University of Colorado nor the names of its
67  contributors may be used to endorse or promote products derived from
68  this software without specific prior written permission.
69 
70  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
71  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
72  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
73  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
74  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
75  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
76  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
77  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
78  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
79  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
80  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
81  POSSIBILITY OF SUCH DAMAGE.]
82 
83 ******************************************************************************/
84 
85 #include "misc/util/util_hack.h"
86 #include "cuddInt.h"
87 
88 ABC_NAMESPACE_IMPL_START
89 
90 
91 
92 
93 /*---------------------------------------------------------------------------*/
94 /* Constant declarations */
95 /*---------------------------------------------------------------------------*/
96 
97 /*---------------------------------------------------------------------------*/
98 /* Stucture declarations */
99 /*---------------------------------------------------------------------------*/
100 
101 /*---------------------------------------------------------------------------*/
102 /* Type declarations */
103 /*---------------------------------------------------------------------------*/
104 
105 /*---------------------------------------------------------------------------*/
106 /* Variable declarations */
107 /*---------------------------------------------------------------------------*/
108 
109 #ifndef lint
110 static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
111 #endif
112 
113 #ifdef DD_DEBUG
114 static int addPermuteRecurHits;
115 static int bddPermuteRecurHits;
116 static int bddVectorComposeHits;
117 static int addVectorComposeHits;
118 
119 static int addGeneralVectorComposeHits;
120 #endif
121 
122 /*---------------------------------------------------------------------------*/
123 /* Macro declarations */
124 /*---------------------------------------------------------------------------*/
125 
126 
127 /**AutomaticStart*************************************************************/
128 
129 /*---------------------------------------------------------------------------*/
130 /* Static function prototypes */
131 /*---------------------------------------------------------------------------*/
132 
133 static DdNode * cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
134 static DdNode * cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
135 static DdNode * cuddBddVarMapRecur (DdManager *manager, DdNode *f);
136 static DdNode * cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
137 static DdNode * cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub);
138 static DdNode * cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
139 DD_INLINE static int ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i);
140 
141 static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest);
142 DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i);
143 
144 /**AutomaticEnd***************************************************************/
145 
146 
147 /*---------------------------------------------------------------------------*/
148 /* Definition of exported functions */
149 /*---------------------------------------------------------------------------*/
150 
151 
152 /**Function********************************************************************
153 
154  Synopsis [Substitutes g for x_v in the BDD for f.]
155 
156  Description [Substitutes g for x_v in the BDD for f. v is the index of the
157  variable to be substituted. Cudd_bddCompose passes the corresponding
158  projection function to the recursive procedure, so that the cache may
159  be used. Returns the composed BDD if successful; NULL otherwise.]
160 
161  SideEffects [None]
162 
163  SeeAlso [Cudd_addCompose]
164 
165 ******************************************************************************/
166 DdNode *
167 Cudd_bddCompose(
168  DdManager * dd,
169  DdNode * f,
170  DdNode * g,
171  int v)
172 {
173  DdNode *proj, *res;
174 
175  /* Sanity check. */
176  if (v < 0 || v >= dd->size) return(NULL);
177 
178  proj = dd->vars[v];
179  do {
180  dd->reordered = 0;
181  res = cuddBddComposeRecur(dd,f,g,proj);
182  } while (dd->reordered == 1);
183  return(res);
184 
185 } /* end of Cudd_bddCompose */
186 
187 
188 /**Function********************************************************************
189 
190  Synopsis [Substitutes g for x_v in the ADD for f.]
191 
192  Description [Substitutes g for x_v in the ADD for f. v is the index of the
193  variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
194  the corresponding projection function to the recursive procedure, so
195  that the cache may be used. Returns the composed ADD if successful;
196  NULL otherwise.]
197 
198  SideEffects [None]
199 
200  SeeAlso [Cudd_bddCompose]
201 
202 ******************************************************************************/
203 DdNode *
204 Cudd_addCompose(
205  DdManager * dd,
206  DdNode * f,
207  DdNode * g,
208  int v)
209 {
210  DdNode *proj, *res;
211 
212  /* Sanity check. */
213  if (v < 0 || v >= dd->size) return(NULL);
214 
215  proj = dd->vars[v];
216  do {
217  dd->reordered = 0;
218  res = cuddAddComposeRecur(dd,f,g,proj);
219  } while (dd->reordered == 1);
220  return(res);
221 
222 } /* end of Cudd_addCompose */
223 
224 
225 /**Function********************************************************************
226 
227  Synopsis [Permutes the variables of an ADD.]
228 
229  Description [Given a permutation in array permut, creates a new ADD
230  with permuted variables. There should be an entry in array permut
231  for each variable in the manager. The i-th entry of permut holds the
232  index of the variable that is to substitute the i-th
233  variable. Returns a pointer to the resulting ADD if successful; NULL
234  otherwise.]
235 
236  SideEffects [None]
237 
238  SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
239 
240 ******************************************************************************/
241 DdNode *
242 Cudd_addPermute(
243  DdManager * manager,
244  DdNode * node,
245  int * permut)
246 {
247  DdHashTable *table;
248  DdNode *res;
249 
250  do {
251  manager->reordered = 0;
252  table = cuddHashTableInit(manager,1,2);
253  if (table == NULL) return(NULL);
254  /* Recursively solve the problem. */
255  res = cuddAddPermuteRecur(manager,table,node,permut);
256  if (res != NULL) cuddRef(res);
257  /* Dispose of local cache. */
258  cuddHashTableQuit(table);
259  } while (manager->reordered == 1);
260 
261  if (res != NULL) cuddDeref(res);
262  return(res);
263 
264 } /* end of Cudd_addPermute */
265 
266 
267 /**Function********************************************************************
268 
269  Synopsis [Swaps two sets of variables of the same size (x and y) in
270  the ADD f.]
271 
272  Description [Swaps two sets of variables of the same size (x and y) in
273  the ADD f. The size is given by n. The two sets of variables are
274  assumed to be disjoint. Returns a pointer to the resulting ADD if
275  successful; NULL otherwise.]
276 
277  SideEffects [None]
278 
279  SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
280 
281 ******************************************************************************/
282 DdNode *
283 Cudd_addSwapVariables(
284  DdManager * dd,
285  DdNode * f,
286  DdNode ** x,
287  DdNode ** y,
288  int n)
289 {
290  DdNode *swapped;
291  int i, j, k;
292  int *permut;
293 
294  permut = ABC_ALLOC(int,dd->size);
295  if (permut == NULL) {
296  dd->errorCode = CUDD_MEMORY_OUT;
297  return(NULL);
298  }
299  for (i = 0; i < dd->size; i++) permut[i] = i;
300  for (i = 0; i < n; i++) {
301  j = x[i]->index;
302  k = y[i]->index;
303  permut[j] = k;
304  permut[k] = j;
305  }
306 
307  swapped = Cudd_addPermute(dd,f,permut);
308  ABC_FREE(permut);
309 
310  return(swapped);
311 
312 } /* end of Cudd_addSwapVariables */
313 
314 
315 /**Function********************************************************************
316 
317  Synopsis [Permutes the variables of a BDD.]
318 
319  Description [Given a permutation in array permut, creates a new BDD
320  with permuted variables. There should be an entry in array permut
321  for each variable in the manager. The i-th entry of permut holds the
322  index of the variable that is to substitute the i-th variable.
323  Returns a pointer to the resulting BDD if successful; NULL
324  otherwise.]
325 
326  SideEffects [None]
327 
328  SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
329 
330 ******************************************************************************/
331 DdNode *
332 Cudd_bddPermute(
333  DdManager * manager,
334  DdNode * node,
335  int * permut)
336 {
337  DdHashTable *table;
338  DdNode *res;
339 
340  do {
341  manager->reordered = 0;
342  table = cuddHashTableInit(manager,1,2);
343  if (table == NULL) return(NULL);
344  res = cuddBddPermuteRecur(manager,table,node,permut);
345  if (res != NULL) cuddRef(res);
346  /* Dispose of local cache. */
347  cuddHashTableQuit(table);
348 
349  } while (manager->reordered == 1);
350 
351  if (res != NULL) cuddDeref(res);
352  return(res);
353 
354 } /* end of Cudd_bddPermute */
355 
356 
357 /**Function********************************************************************
358 
359  Synopsis [Remaps the variables of a BDD using the default variable map.]
360 
361  Description [Remaps the variables of a BDD using the default
362  variable map. A typical use of this function is to swap two sets of
363  variables. The variable map must be registered with Cudd_SetVarMap.
364  Returns a pointer to the resulting BDD if successful; NULL
365  otherwise.]
366 
367  SideEffects [None]
368 
369  SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
370 
371 ******************************************************************************/
372 DdNode *
373 Cudd_bddVarMap(
374  DdManager * manager /* DD manager */,
375  DdNode * f /* function in which to remap variables */)
376 {
377  DdNode *res;
378 
379  if (manager->map == NULL) return(NULL);
380  do {
381  manager->reordered = 0;
382  res = cuddBddVarMapRecur(manager, f);
383  } while (manager->reordered == 1);
384 
385  return(res);
386 
387 } /* end of Cudd_bddVarMap */
388 
389 
390 /**Function********************************************************************
391 
392  Synopsis [Registers a variable mapping with the manager.]
393 
394  Description [Registers with the manager a variable mapping described
395  by two sets of variables. This variable mapping is then used by
396  functions like Cudd_bddVarMap. This function is convenient for
397  those applications that perform the same mapping several times.
398  However, if several different permutations are used, it may be more
399  efficient not to rely on the registered mapping, because changing
400  mapping causes the cache to be cleared. (The initial setting,
401  however, does not clear the cache.) The two sets of variables (x and
402  y) must have the same size (x and y). The size is given by n. The
403  two sets of variables are normally disjoint, but this restriction is
404  not imposeded by the function. When new variables are created, the
405  map is automatically extended (each new variable maps to
406  itself). The typical use, however, is to wait until all variables
407  are created, and then create the map. Returns 1 if the mapping is
408  successfully registered with the manager; 0 otherwise.]
409 
410  SideEffects [Modifies the manager. May clear the cache.]
411 
412  SeeAlso [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
413 
414 ******************************************************************************/
415 int
416 Cudd_SetVarMap (
417  DdManager *manager /* DD manager */,
418  DdNode **x /* first array of variables */,
419  DdNode **y /* second array of variables */,
420  int n /* length of both arrays */)
421 {
422  int i;
423 
424  if (manager->map != NULL) {
425  cuddCacheFlush(manager);
426  } else {
427  manager->map = ABC_ALLOC(int,manager->maxSize);
428  if (manager->map == NULL) {
429  manager->errorCode = CUDD_MEMORY_OUT;
430  return(0);
431  }
432  manager->memused += sizeof(int) * manager->maxSize;
433  }
434  /* Initialize the map to the identity. */
435  for (i = 0; i < manager->size; i++) {
436  manager->map[i] = i;
437  }
438  /* Create the map. */
439  for (i = 0; i < n; i++) {
440  manager->map[x[i]->index] = y[i]->index;
441  manager->map[y[i]->index] = x[i]->index;
442  }
443  return(1);
444 
445 } /* end of Cudd_SetVarMap */
446 
447 
448 /**Function********************************************************************
449 
450  Synopsis [Swaps two sets of variables of the same size (x and y) in
451  the BDD f.]
452 
453  Description [Swaps two sets of variables of the same size (x and y)
454  in the BDD f. The size is given by n. The two sets of variables are
455  assumed to be disjoint. Returns a pointer to the resulting BDD if
456  successful; NULL otherwise.]
457 
458  SideEffects [None]
459 
460  SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
461 
462 ******************************************************************************/
463 DdNode *
464 Cudd_bddSwapVariables(
465  DdManager * dd,
466  DdNode * f,
467  DdNode ** x,
468  DdNode ** y,
469  int n)
470 {
471  DdNode *swapped;
472  int i, j, k;
473  int *permut;
474 
475  permut = ABC_ALLOC(int,dd->size);
476  if (permut == NULL) {
477  dd->errorCode = CUDD_MEMORY_OUT;
478  return(NULL);
479  }
480  for (i = 0; i < dd->size; i++) permut[i] = i;
481  for (i = 0; i < n; i++) {
482  j = x[i]->index;
483  k = y[i]->index;
484  permut[j] = k;
485  permut[k] = j;
486  }
487 
488  swapped = Cudd_bddPermute(dd,f,permut);
489  ABC_FREE(permut);
490 
491  return(swapped);
492 
493 } /* end of Cudd_bddSwapVariables */
494 
495 
496 /**Function********************************************************************
497 
498  Synopsis [Rearranges a set of variables in the BDD B.]
499 
500  Description [Rearranges a set of variables in the BDD B. The size of
501  the set is given by n. This procedure is intended for the
502  `randomization' of the priority functions. Returns a pointer to the
503  BDD if successful; NULL otherwise.]
504 
505  SideEffects [None]
506 
507  SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables
508  Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
509 
510 ******************************************************************************/
511 DdNode *
512 Cudd_bddAdjPermuteX(
513  DdManager * dd,
514  DdNode * B,
515  DdNode ** x,
516  int n)
517 {
518  DdNode *swapped;
519  int i, j, k;
520  int *permut;
521 
522  permut = ABC_ALLOC(int,dd->size);
523  if (permut == NULL) {
524  dd->errorCode = CUDD_MEMORY_OUT;
525  return(NULL);
526  }
527  for (i = 0; i < dd->size; i++) permut[i] = i;
528  for (i = 0; i < n-2; i += 3) {
529  j = x[i]->index;
530  k = x[i+1]->index;
531  permut[j] = k;
532  permut[k] = j;
533  }
534 
535  swapped = Cudd_bddPermute(dd,B,permut);
536  ABC_FREE(permut);
537 
538  return(swapped);
539 
540 } /* end of Cudd_bddAdjPermuteX */
541 
542 
543 /**Function********************************************************************
544 
545  Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
546 
547  Description [Given a vector of 0-1 ADDs, creates a new ADD by
548  substituting the 0-1 ADDs for the variables of the ADD f. There
549  should be an entry in vector for each variable in the manager.
550  If no substitution is sought for a given variable, the corresponding
551  projection function should be specified in the vector.
552  This function implements simultaneous composition.
553  Returns a pointer to the resulting ADD if successful; NULL
554  otherwise.]
555 
556  SideEffects [None]
557 
558  SeeAlso [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
559  Cudd_bddVectorCompose]
560 
561 ******************************************************************************/
562 DdNode *
563 Cudd_addVectorCompose(
564  DdManager * dd,
565  DdNode * f,
566  DdNode ** vector)
567 {
568  DdHashTable *table;
569  DdNode *res;
570  int deepest;
571  int i;
572 
573  do {
574  dd->reordered = 0;
575  /* Initialize local cache. */
576  table = cuddHashTableInit(dd,1,2);
577  if (table == NULL) return(NULL);
578 
579  /* Find deepest real substitution. */
580  for (deepest = dd->size - 1; deepest >= 0; deepest--) {
581  i = dd->invperm[deepest];
582  if (!ddIsIthAddVar(dd,vector[i],i)) {
583  break;
584  }
585  }
586 
587  /* Recursively solve the problem. */
588  res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
589  if (res != NULL) cuddRef(res);
590 
591  /* Dispose of local cache. */
592  cuddHashTableQuit(table);
593  } while (dd->reordered == 1);
594 
595  if (res != NULL) cuddDeref(res);
596  return(res);
597 
598 } /* end of Cudd_addVectorCompose */
599 
600 
601 /**Function********************************************************************
602 
603  Synopsis [Composes an ADD with a vector of ADDs.]
604 
605  Description [Given a vector of ADDs, creates a new ADD by substituting the
606  ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
607  for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
608  be an entry in vector for each variable in the manager. If no substitution
609  is sought for a given variable, the corresponding projection function should
610  be specified in the vector. This function implements simultaneous
611  composition. Returns a pointer to the resulting ADD if successful; NULL
612  otherwise.]
613 
614  SideEffects [None]
615 
616  SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
617  Cudd_addCompose Cudd_bddVectorCompose]
618 
619 ******************************************************************************/
620 DdNode *
621 Cudd_addGeneralVectorCompose(
622  DdManager * dd,
623  DdNode * f,
624  DdNode ** vectorOn,
625  DdNode ** vectorOff)
626 {
627  DdHashTable *table;
628  DdNode *res;
629  int deepest;
630  int i;
631 
632  do {
633  dd->reordered = 0;
634  /* Initialize local cache. */
635  table = cuddHashTableInit(dd,1,2);
636  if (table == NULL) return(NULL);
637 
638  /* Find deepest real substitution. */
639  for (deepest = dd->size - 1; deepest >= 0; deepest--) {
640  i = dd->invperm[deepest];
641  if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
642  break;
643  }
644  }
645 
646  /* Recursively solve the problem. */
647  res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
648  vectorOff,deepest);
649  if (res != NULL) cuddRef(res);
650 
651  /* Dispose of local cache. */
652  cuddHashTableQuit(table);
653  } while (dd->reordered == 1);
654 
655  if (res != NULL) cuddDeref(res);
656  return(res);
657 
658 } /* end of Cudd_addGeneralVectorCompose */
659 
660 
661 /**Function********************************************************************
662 
663  Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
664 
665  Description [Given a vector of 0-1 ADDs, creates a new ADD by
666  substituting the 0-1 ADDs for the variables of the ADD f. There
667  should be an entry in vector for each variable in the manager.
668  This function implements non-simultaneous composition. If any of the
669  functions being composed depends on any of the variables being
670  substituted, then the result depends on the order of composition,
671  which in turn depends on the variable order: The variables farther from
672  the roots in the order are substituted first.
673  Returns a pointer to the resulting ADD if successful; NULL
674  otherwise.]
675 
676  SideEffects [None]
677 
678  SeeAlso [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
679 
680 ******************************************************************************/
681 DdNode *
682 Cudd_addNonSimCompose(
683  DdManager * dd,
684  DdNode * f,
685  DdNode ** vector)
686 {
687  DdNode *cube, *key, *var, *tmp, *piece;
688  DdNode *res;
689  int i, lastsub;
690 
691  /* The cache entry for this function is composed of three parts:
692  ** f itself, the replacement relation, and the cube of the
693  ** variables being substituted.
694  ** The replacement relation is the product of the terms (yi EXNOR gi).
695  ** This apporach allows us to use the global cache for this function,
696  ** with great savings in memory with respect to using arrays for the
697  ** cache entries.
698  ** First we build replacement relation and cube of substituted
699  ** variables from the vector specifying the desired composition.
700  */
701  key = DD_ONE(dd);
702  cuddRef(key);
703  cube = DD_ONE(dd);
704  cuddRef(cube);
705  for (i = (int) dd->size - 1; i >= 0; i--) {
706  if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
707  continue;
708  }
709  var = Cudd_addIthVar(dd,i);
710  if (var == NULL) {
711  Cudd_RecursiveDeref(dd,key);
712  Cudd_RecursiveDeref(dd,cube);
713  return(NULL);
714  }
715  cuddRef(var);
716  /* Update cube. */
717  tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
718  if (tmp == NULL) {
719  Cudd_RecursiveDeref(dd,key);
720  Cudd_RecursiveDeref(dd,cube);
721  Cudd_RecursiveDeref(dd,var);
722  return(NULL);
723  }
724  cuddRef(tmp);
725  Cudd_RecursiveDeref(dd,cube);
726  cube = tmp;
727  /* Update replacement relation. */
728  piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
729  if (piece == NULL) {
730  Cudd_RecursiveDeref(dd,key);
731  Cudd_RecursiveDeref(dd,var);
732  return(NULL);
733  }
734  cuddRef(piece);
735  Cudd_RecursiveDeref(dd,var);
736  tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
737  if (tmp == NULL) {
738  Cudd_RecursiveDeref(dd,key);
739  Cudd_RecursiveDeref(dd,piece);
740  return(NULL);
741  }
742  cuddRef(tmp);
743  Cudd_RecursiveDeref(dd,key);
744  Cudd_RecursiveDeref(dd,piece);
745  key = tmp;
746  }
747 
748  /* Now try composition, until no reordering occurs. */
749  do {
750  /* Find real substitution with largest index. */
751  for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
752  if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
753  break;
754  }
755  }
756 
757  /* Recursively solve the problem. */
758  dd->reordered = 0;
759  res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
760  if (res != NULL) cuddRef(res);
761 
762  } while (dd->reordered == 1);
763 
764  Cudd_RecursiveDeref(dd,key);
765  Cudd_RecursiveDeref(dd,cube);
766  if (res != NULL) cuddDeref(res);
767  return(res);
768 
769 } /* end of Cudd_addNonSimCompose */
770 
771 
772 /**Function********************************************************************
773 
774  Synopsis [Composes a BDD with a vector of BDDs.]
775 
776  Description [Given a vector of BDDs, creates a new BDD by
777  substituting the BDDs for the variables of the BDD f. There
778  should be an entry in vector for each variable in the manager.
779  If no substitution is sought for a given variable, the corresponding
780  projection function should be specified in the vector.
781  This function implements simultaneous composition.
782  Returns a pointer to the resulting BDD if successful; NULL
783  otherwise.]
784 
785  SideEffects [None]
786 
787  SeeAlso [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
788 
789 ******************************************************************************/
790 DdNode *
791 Cudd_bddVectorCompose(
792  DdManager * dd,
793  DdNode * f,
794  DdNode ** vector)
795 {
796  DdHashTable *table;
797  DdNode *res;
798  int deepest;
799  int i;
800 
801  do {
802  dd->reordered = 0;
803  /* Initialize local cache. */
804  table = cuddHashTableInit(dd,1,2);
805  if (table == NULL) return(NULL);
806 
807  /* Find deepest real substitution. */
808  for (deepest = dd->size - 1; deepest >= 0; deepest--) {
809  i = dd->invperm[deepest];
810  if (vector[i] != dd->vars[i]) {
811  break;
812  }
813  }
814 
815  /* Recursively solve the problem. */
816  res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
817  if (res != NULL) cuddRef(res);
818 
819  /* Dispose of local cache. */
820  cuddHashTableQuit(table);
821  } while (dd->reordered == 1);
822 
823  if (res != NULL) cuddDeref(res);
824  return(res);
825 
826 } /* end of Cudd_bddVectorCompose */
827 
828 
829 /*---------------------------------------------------------------------------*/
830 /* Definition of internal functions */
831 /*---------------------------------------------------------------------------*/
832 
833 
834 /**Function********************************************************************
835 
836  Synopsis [Performs the recursive step of Cudd_bddCompose.]
837 
838  Description [Performs the recursive step of Cudd_bddCompose.
839  Exploits the fact that the composition of f' with g
840  produces the complement of the composition of f with g to better
841  utilize the cache. Returns the composed BDD if successful; NULL
842  otherwise.]
843 
844  SideEffects [None]
845 
846  SeeAlso [Cudd_bddCompose]
847 
848 ******************************************************************************/
849 DdNode *
850 cuddBddComposeRecur(
851  DdManager * dd,
852  DdNode * f,
853  DdNode * g,
854  DdNode * proj)
855 {
856  DdNode *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
857  unsigned int v, topf, topg, topindex;
858  int comple;
859 
860  statLine(dd);
861  v = dd->perm[proj->index];
862  F = Cudd_Regular(f);
863  topf = cuddI(dd,F->index);
864 
865  /* Terminal case. Subsumes the test for constant f. */
866  if (topf > v) return(f);
867 
868  /* We solve the problem for a regular pointer, and then complement
869  ** the result if the pointer was originally complemented.
870  */
871  comple = Cudd_IsComplement(f);
872 
873  /* Check cache. */
874  r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
875  if (r != NULL) {
876  return(Cudd_NotCond(r,comple));
877  }
878 
879  if (topf == v) {
880  /* Compose. */
881  f1 = cuddT(F);
882  f0 = cuddE(F);
883  r = cuddBddIteRecur(dd, g, f1, f0);
884  if (r == NULL) return(NULL);
885  } else {
886  /* Compute cofactors of f and g. Remember the index of the top
887  ** variable.
888  */
889  G = Cudd_Regular(g);
890  topg = cuddI(dd,G->index);
891  if (topf > topg) {
892  topindex = G->index;
893  f1 = f0 = F;
894  } else {
895  topindex = F->index;
896  f1 = cuddT(F);
897  f0 = cuddE(F);
898  }
899  if (topg > topf) {
900  g1 = g0 = g;
901  } else {
902  g1 = cuddT(G);
903  g0 = cuddE(G);
904  if (g != G) {
905  g1 = Cudd_Not(g1);
906  g0 = Cudd_Not(g0);
907  }
908  }
909  /* Recursive step. */
910  t = cuddBddComposeRecur(dd, f1, g1, proj);
911  if (t == NULL) return(NULL);
912  cuddRef(t);
913  e = cuddBddComposeRecur(dd, f0, g0, proj);
914  if (e == NULL) {
915  Cudd_IterDerefBdd(dd, t);
916  return(NULL);
917  }
918  cuddRef(e);
919 
920  r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
921  if (r == NULL) {
922  Cudd_IterDerefBdd(dd, t);
923  Cudd_IterDerefBdd(dd, e);
924  return(NULL);
925  }
926  cuddRef(r);
927  Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
928  Cudd_IterDerefBdd(dd, e);
929  cuddDeref(r);
930  }
931 
932  cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);
933 
934  return(Cudd_NotCond(r,comple));
935 
936 } /* end of cuddBddComposeRecur */
937 
938 
939 /**Function********************************************************************
940 
941  Synopsis [Performs the recursive step of Cudd_addCompose.]
942 
943  Description [Performs the recursive step of Cudd_addCompose.
944  Returns the composed BDD if successful; NULL otherwise.]
945 
946  SideEffects [None]
947 
948  SeeAlso [Cudd_addCompose]
949 
950 ******************************************************************************/
951 DdNode *
952 cuddAddComposeRecur(
953  DdManager * dd,
954  DdNode * f,
955  DdNode * g,
956  DdNode * proj)
957 {
958  DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
959  unsigned int v, topf, topg, topindex;
960 
961  statLine(dd);
962  v = dd->perm[proj->index];
963  topf = cuddI(dd,f->index);
964 
965  /* Terminal case. Subsumes the test for constant f. */
966  if (topf > v) return(f);
967 
968  /* Check cache. */
969  r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
970  if (r != NULL) {
971  return(r);
972  }
973 
974  if (topf == v) {
975  /* Compose. */
976  f1 = cuddT(f);
977  f0 = cuddE(f);
978  r = cuddAddIteRecur(dd, g, f1, f0);
979  if (r == NULL) return(NULL);
980  } else {
981  /* Compute cofactors of f and g. Remember the index of the top
982  ** variable.
983  */
984  topg = cuddI(dd,g->index);
985  if (topf > topg) {
986  topindex = g->index;
987  f1 = f0 = f;
988  } else {
989  topindex = f->index;
990  f1 = cuddT(f);
991  f0 = cuddE(f);
992  }
993  if (topg > topf) {
994  g1 = g0 = g;
995  } else {
996  g1 = cuddT(g);
997  g0 = cuddE(g);
998  }
999  /* Recursive step. */
1000  t = cuddAddComposeRecur(dd, f1, g1, proj);
1001  if (t == NULL) return(NULL);
1002  cuddRef(t);
1003  e = cuddAddComposeRecur(dd, f0, g0, proj);
1004  if (e == NULL) {
1005  Cudd_RecursiveDeref(dd, t);
1006  return(NULL);
1007  }
1008  cuddRef(e);
1009 
1010  if (t == e) {
1011  r = t;
1012  } else {
1013  r = cuddUniqueInter(dd, (int) topindex, t, e);
1014  if (r == NULL) {
1015  Cudd_RecursiveDeref(dd, t);
1016  Cudd_RecursiveDeref(dd, e);
1017  return(NULL);
1018  }
1019  }
1020  cuddDeref(t);
1021  cuddDeref(e);
1022  }
1023 
1024  cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);
1025 
1026  return(r);
1027 
1028 } /* end of cuddAddComposeRecur */
1029 
1030 
1031 /*---------------------------------------------------------------------------*/
1032 /* Definition of static functions */
1033 /*---------------------------------------------------------------------------*/
1034 
1035 
1036 /**Function********************************************************************
1037 
1038  Synopsis [Implements the recursive step of Cudd_addPermute.]
1039 
1040  Description [ Recursively puts the ADD in the order given in the
1041  array permut. Checks for trivial cases to terminate recursion, then
1042  splits on the children of this node. Once the solutions for the
1043  children are obtained, it puts into the current position the node
1044  from the rest of the ADD that should be here. Then returns this ADD.
1045  The key here is that the node being visited is NOT put in its proper
1046  place by this instance, but rather is switched when its proper
1047  position is reached in the recursion tree.<p>
1048  The DdNode * that is returned is the same ADD as passed in as node,
1049  but in the new order.]
1050 
1051  SideEffects [None]
1052 
1053  SeeAlso [Cudd_addPermute cuddBddPermuteRecur]
1054 
1055 ******************************************************************************/
1056 static DdNode *
1057 cuddAddPermuteRecur(
1058  DdManager * manager /* DD manager */,
1059  DdHashTable * table /* computed table */,
1060  DdNode * node /* ADD to be reordered */,
1061  int * permut /* permutation array */)
1062 {
1063  DdNode *T,*E;
1064  DdNode *res,*var;
1065  int index;
1066 
1067  statLine(manager);
1068  /* Check for terminal case of constant node. */
1069  if (cuddIsConstant(node)) {
1070  return(node);
1071  }
1072 
1073  /* If problem already solved, look up answer and return. */
1074  if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
1075 #ifdef DD_DEBUG
1076  addPermuteRecurHits++;
1077 #endif
1078  return(res);
1079  }
1080 
1081  /* Split and recur on children of this node. */
1082  T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
1083  if (T == NULL) return(NULL);
1084  cuddRef(T);
1085  E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
1086  if (E == NULL) {
1087  Cudd_RecursiveDeref(manager, T);
1088  return(NULL);
1089  }
1090  cuddRef(E);
1091 
1092  /* Move variable that should be in this position to this position
1093  ** by creating a single var ADD for that variable, and calling
1094  ** cuddAddIteRecur with the T and E we just created.
1095  */
1096  index = permut[node->index];
1097  var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
1098  if (var == NULL) return(NULL);
1099  cuddRef(var);
1100  res = cuddAddIteRecur(manager,var,T,E);
1101  if (res == NULL) {
1102  Cudd_RecursiveDeref(manager,var);
1103  Cudd_RecursiveDeref(manager, T);
1104  Cudd_RecursiveDeref(manager, E);
1105  return(NULL);
1106  }
1107  cuddRef(res);
1108  Cudd_RecursiveDeref(manager,var);
1109  Cudd_RecursiveDeref(manager, T);
1110  Cudd_RecursiveDeref(manager, E);
1111 
1112  /* Do not keep the result if the reference count is only 1, since
1113  ** it will not be visited again.
1114  */
1115  if (node->ref != 1) {
1116  ptrint fanout = (ptrint) node->ref;
1117  cuddSatDec(fanout);
1118  if (!cuddHashTableInsert1(table,node,res,fanout)) {
1119  Cudd_RecursiveDeref(manager, res);
1120  return(NULL);
1121  }
1122  }
1123  cuddDeref(res);
1124  return(res);
1125 
1126 } /* end of cuddAddPermuteRecur */
1127 
1128 
1129 /**Function********************************************************************
1130 
1131  Synopsis [Implements the recursive step of Cudd_bddPermute.]
1132 
1133  Description [ Recursively puts the BDD in the order given in the array permut.
1134  Checks for trivial cases to terminate recursion, then splits on the
1135  children of this node. Once the solutions for the children are
1136  obtained, it puts into the current position the node from the rest of
1137  the BDD that should be here. Then returns this BDD.
1138  The key here is that the node being visited is NOT put in its proper
1139  place by this instance, but rather is switched when its proper position
1140  is reached in the recursion tree.<p>
1141  The DdNode * that is returned is the same BDD as passed in as node,
1142  but in the new order.]
1143 
1144  SideEffects [None]
1145 
1146  SeeAlso [Cudd_bddPermute cuddAddPermuteRecur]
1147 
1148 ******************************************************************************/
1149 static DdNode *
1150 cuddBddPermuteRecur(
1151  DdManager * manager /* DD manager */,
1152  DdHashTable * table /* computed table */,
1153  DdNode * node /* BDD to be reordered */,
1154  int * permut /* permutation array */)
1155 {
1156  DdNode *N,*T,*E;
1157  DdNode *res;
1158  int index;
1159 
1160  statLine(manager);
1161  N = Cudd_Regular(node);
1162 
1163  /* Check for terminal case of constant node. */
1164  if (cuddIsConstant(N)) {
1165  return(node);
1166  }
1167 
1168  /* If problem already solved, look up answer and return. */
1169  if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
1170 #ifdef DD_DEBUG
1171  bddPermuteRecurHits++;
1172 #endif
1173  return(Cudd_NotCond(res,N != node));
1174  }
1175 
1176  /* Split and recur on children of this node. */
1177  T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
1178  if (T == NULL) return(NULL);
1179  cuddRef(T);
1180  E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
1181  if (E == NULL) {
1182  Cudd_IterDerefBdd(manager, T);
1183  return(NULL);
1184  }
1185  cuddRef(E);
1186 
1187  /* Move variable that should be in this position to this position
1188  ** by retrieving the single var BDD for that variable, and calling
1189  ** cuddBddIteRecur with the T and E we just created.
1190  */
1191  index = permut[N->index];
1192  res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1193  if (res == NULL) {
1194  Cudd_IterDerefBdd(manager, T);
1195  Cudd_IterDerefBdd(manager, E);
1196  return(NULL);
1197  }
1198  cuddRef(res);
1199  Cudd_IterDerefBdd(manager, T);
1200  Cudd_IterDerefBdd(manager, E);
1201 
1202  /* Do not keep the result if the reference count is only 1, since
1203  ** it will not be visited again.
1204  */
1205  if (N->ref != 1) {
1206  ptrint fanout = (ptrint) N->ref;
1207  cuddSatDec(fanout);
1208  if (!cuddHashTableInsert1(table,N,res,fanout)) {
1209  Cudd_IterDerefBdd(manager, res);
1210  return(NULL);
1211  }
1212  }
1213  cuddDeref(res);
1214  return(Cudd_NotCond(res,N != node));
1215 
1216 } /* end of cuddBddPermuteRecur */
1217 
1218 
1219 /**Function********************************************************************
1220 
1221  Synopsis [Implements the recursive step of Cudd_bddVarMap.]
1222 
1223  Description [Implements the recursive step of Cudd_bddVarMap.
1224  Returns a pointer to the result if successful; NULL otherwise.]
1225 
1226  SideEffects [None]
1227 
1228  SeeAlso [Cudd_bddVarMap]
1229 
1230 ******************************************************************************/
1231 static DdNode *
1232 cuddBddVarMapRecur(
1233  DdManager *manager /* DD manager */,
1234  DdNode *f /* BDD to be remapped */)
1235 {
1236  DdNode *F, *T, *E;
1237  DdNode *res;
1238  int index;
1239 
1240  statLine(manager);
1241  F = Cudd_Regular(f);
1242 
1243  /* Check for terminal case of constant node. */
1244  if (cuddIsConstant(F)) {
1245  return(f);
1246  }
1247 
1248  /* If problem already solved, look up answer and return. */
1249  if (F->ref != 1 &&
1250  (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
1251  return(Cudd_NotCond(res,F != f));
1252  }
1253 
1254  if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
1255  return NULL;
1256 
1257  /* Split and recur on children of this node. */
1258  T = cuddBddVarMapRecur(manager,cuddT(F));
1259  if (T == NULL) return(NULL);
1260  cuddRef(T);
1261  E = cuddBddVarMapRecur(manager,cuddE(F));
1262  if (E == NULL) {
1263  Cudd_IterDerefBdd(manager, T);
1264  return(NULL);
1265  }
1266  cuddRef(E);
1267 
1268  /* Move variable that should be in this position to this position
1269  ** by retrieving the single var BDD for that variable, and calling
1270  ** cuddBddIteRecur with the T and E we just created.
1271  */
1272  index = manager->map[F->index];
1273  res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1274  if (res == NULL) {
1275  Cudd_IterDerefBdd(manager, T);
1276  Cudd_IterDerefBdd(manager, E);
1277  return(NULL);
1278  }
1279  cuddRef(res);
1280  Cudd_IterDerefBdd(manager, T);
1281  Cudd_IterDerefBdd(manager, E);
1282 
1283  /* Do not keep the result if the reference count is only 1, since
1284  ** it will not be visited again.
1285  */
1286  if (F->ref != 1) {
1287  cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
1288  }
1289  cuddDeref(res);
1290  return(Cudd_NotCond(res,F != f));
1291 
1292 } /* end of cuddBddVarMapRecur */
1293 
1294 
1295 /**Function********************************************************************
1296 
1297  Synopsis [Performs the recursive step of Cudd_addVectorCompose.]
1298 
1299  Description []
1300 
1301  SideEffects [None]
1302 
1303  SeeAlso []
1304 
1305 ******************************************************************************/
1306 static DdNode *
1307 cuddAddVectorComposeRecur(
1308  DdManager * dd /* DD manager */,
1309  DdHashTable * table /* computed table */,
1310  DdNode * f /* ADD in which to compose */,
1311  DdNode ** vector /* functions to substitute */,
1312  int deepest /* depth of deepest substitution */)
1313 {
1314  DdNode *T,*E;
1315  DdNode *res;
1316 
1317  statLine(dd);
1318  /* If we are past the deepest substitution, return f. */
1319  if (cuddI(dd,f->index) > deepest) {
1320  return(f);
1321  }
1322 
1323  if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1324 #ifdef DD_DEBUG
1325  addVectorComposeHits++;
1326 #endif
1327  return(res);
1328  }
1329 
1330  /* Split and recur on children of this node. */
1331  T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
1332  if (T == NULL) return(NULL);
1333  cuddRef(T);
1334  E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
1335  if (E == NULL) {
1336  Cudd_RecursiveDeref(dd, T);
1337  return(NULL);
1338  }
1339  cuddRef(E);
1340 
1341  /* Retrieve the 0-1 ADD for the current top variable and call
1342  ** cuddAddIteRecur with the T and E we just created.
1343  */
1344  res = cuddAddIteRecur(dd,vector[f->index],T,E);
1345  if (res == NULL) {
1346  Cudd_RecursiveDeref(dd, T);
1347  Cudd_RecursiveDeref(dd, E);
1348  return(NULL);
1349  }
1350  cuddRef(res);
1351  Cudd_RecursiveDeref(dd, T);
1352  Cudd_RecursiveDeref(dd, E);
1353 
1354  /* Do not keep the result if the reference count is only 1, since
1355  ** it will not be visited again
1356  */
1357  if (f->ref != 1) {
1358  ptrint fanout = (ptrint) f->ref;
1359  cuddSatDec(fanout);
1360  if (!cuddHashTableInsert1(table,f,res,fanout)) {
1361  Cudd_RecursiveDeref(dd, res);
1362  return(NULL);
1363  }
1364  }
1365  cuddDeref(res);
1366  return(res);
1367 
1368 } /* end of cuddAddVectorComposeRecur */
1369 
1370 
1371 /**Function********************************************************************
1372 
1373  Synopsis [Performs the recursive step of Cudd_addGeneralVectorCompose.]
1374 
1375  Description []
1376 
1377  SideEffects [None]
1378 
1379  SeeAlso []
1380 
1381 ******************************************************************************/
1382 static DdNode *
1383 cuddAddGeneralVectorComposeRecur(
1384  DdManager * dd /* DD manager */,
1385  DdHashTable * table /* computed table */,
1386  DdNode * f /* ADD in which to compose */,
1387  DdNode ** vectorOn /* functions to substitute for x_i */,
1388  DdNode ** vectorOff /* functions to substitute for x_i' */,
1389  int deepest /* depth of deepest substitution */)
1390 {
1391  DdNode *T,*E,*t,*e;
1392  DdNode *res;
1393 
1394  /* If we are past the deepest substitution, return f. */
1395  if (cuddI(dd,f->index) > deepest) {
1396  return(f);
1397  }
1398 
1399  if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1400 #ifdef DD_DEBUG
1401  addGeneralVectorComposeHits++;
1402 #endif
1403  return(res);
1404  }
1405 
1406  /* Split and recur on children of this node. */
1407  T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
1408  vectorOn,vectorOff,deepest);
1409  if (T == NULL) return(NULL);
1410  cuddRef(T);
1411  E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
1412  vectorOn,vectorOff,deepest);
1413  if (E == NULL) {
1414  Cudd_RecursiveDeref(dd, T);
1415  return(NULL);
1416  }
1417  cuddRef(E);
1418 
1419  /* Retrieve the compose ADDs for the current top variable and call
1420  ** cuddAddApplyRecur with the T and E we just created.
1421  */
1422  t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
1423  if (t == NULL) {
1424  Cudd_RecursiveDeref(dd,T);
1425  Cudd_RecursiveDeref(dd,E);
1426  return(NULL);
1427  }
1428  cuddRef(t);
1429  e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
1430  if (e == NULL) {
1431  Cudd_RecursiveDeref(dd,T);
1432  Cudd_RecursiveDeref(dd,E);
1433  Cudd_RecursiveDeref(dd,t);
1434  return(NULL);
1435  }
1436  cuddRef(e);
1437  res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
1438  if (res == NULL) {
1439  Cudd_RecursiveDeref(dd,T);
1440  Cudd_RecursiveDeref(dd,E);
1441  Cudd_RecursiveDeref(dd,t);
1442  Cudd_RecursiveDeref(dd,e);
1443  return(NULL);
1444  }
1445  cuddRef(res);
1446  Cudd_RecursiveDeref(dd,T);
1447  Cudd_RecursiveDeref(dd,E);
1448  Cudd_RecursiveDeref(dd,t);
1449  Cudd_RecursiveDeref(dd,e);
1450 
1451  /* Do not keep the result if the reference count is only 1, since
1452  ** it will not be visited again
1453  */
1454  if (f->ref != 1) {
1455  ptrint fanout = (ptrint) f->ref;
1456  cuddSatDec(fanout);
1457  if (!cuddHashTableInsert1(table,f,res,fanout)) {
1458  Cudd_RecursiveDeref(dd, res);
1459  return(NULL);
1460  }
1461  }
1462  cuddDeref(res);
1463  return(res);
1464 
1465 } /* end of cuddAddGeneralVectorComposeRecur */
1466 
1467 
1468 /**Function********************************************************************
1469 
1470  Synopsis [Performs the recursive step of Cudd_addNonSimCompose.]
1471 
1472  Description []
1473 
1474  SideEffects [None]
1475 
1476  SeeAlso []
1477 
1478 ******************************************************************************/
1479 static DdNode *
1480 cuddAddNonSimComposeRecur(
1481  DdManager * dd,
1482  DdNode * f,
1483  DdNode ** vector,
1484  DdNode * key,
1485  DdNode * cube,
1486  int lastsub)
1487 {
1488  DdNode *f1, *f0, *key1, *key0, *cube1, *var;
1489  DdNode *T,*E;
1490  DdNode *r;
1491  unsigned int top, topf, topk, topc;
1492  unsigned int index;
1493  int i;
1494  DdNode **vect1;
1495  DdNode **vect0;
1496 
1497  statLine(dd);
1498  /* If we are past the deepest substitution, return f. */
1499  if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
1500  return(f);
1501  }
1502 
1503  /* If problem already solved, look up answer and return. */
1504  r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
1505  if (r != NULL) {
1506  return(r);
1507  }
1508 
1509  /* Find top variable. we just need to look at f, key, and cube,
1510  ** because all the varibles in the gi are in key.
1511  */
1512  topf = cuddI(dd,f->index);
1513  topk = cuddI(dd,key->index);
1514  top = ddMin(topf,topk);
1515  topc = cuddI(dd,cube->index);
1516  top = ddMin(top,topc);
1517  index = dd->invperm[top];
1518 
1519  /* Compute the cofactors. */
1520  if (topf == top) {
1521  f1 = cuddT(f);
1522  f0 = cuddE(f);
1523  } else {
1524  f1 = f0 = f;
1525  }
1526  if (topc == top) {
1527  cube1 = cuddT(cube);
1528  /* We want to eliminate vector[index] from key. Otherwise
1529  ** cache performance is severely affected. Hence we
1530  ** existentially quantify the variable with index "index" from key.
1531  */
1532  var = Cudd_addIthVar(dd, (int) index);
1533  if (var == NULL) {
1534  return(NULL);
1535  }
1536  cuddRef(var);
1537  key1 = cuddAddExistAbstractRecur(dd, key, var);
1538  if (key1 == NULL) {
1539  Cudd_RecursiveDeref(dd,var);
1540  return(NULL);
1541  }
1542  cuddRef(key1);
1543  Cudd_RecursiveDeref(dd,var);
1544  key0 = key1;
1545  } else {
1546  cube1 = cube;
1547  if (topk == top) {
1548  key1 = cuddT(key);
1549  key0 = cuddE(key);
1550  } else {
1551  key1 = key0 = key;
1552  }
1553  cuddRef(key1);
1554  }
1555 
1556  /* Allocate two new vectors for the cofactors of vector. */
1557  vect1 = ABC_ALLOC(DdNode *,lastsub);
1558  if (vect1 == NULL) {
1559  dd->errorCode = CUDD_MEMORY_OUT;
1560  Cudd_RecursiveDeref(dd,key1);
1561  return(NULL);
1562  }
1563  vect0 = ABC_ALLOC(DdNode *,lastsub);
1564  if (vect0 == NULL) {
1565  dd->errorCode = CUDD_MEMORY_OUT;
1566  Cudd_RecursiveDeref(dd,key1);
1567  ABC_FREE(vect1);
1568  return(NULL);
1569  }
1570 
1571  /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
1572  ** we do not need them.
1573  */
1574  for (i = 0; i < lastsub; i++) {
1575  DdNode *gi = vector[i];
1576  if (gi == NULL) {
1577  vect1[i] = vect0[i] = NULL;
1578  } else if (gi->index == index) {
1579  vect1[i] = cuddT(gi);
1580  vect0[i] = cuddE(gi);
1581  } else {
1582  vect1[i] = vect0[i] = gi;
1583  }
1584  }
1585  vect1[index] = vect0[index] = NULL;
1586 
1587  /* Recur on children. */
1588  T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
1589  ABC_FREE(vect1);
1590  if (T == NULL) {
1591  Cudd_RecursiveDeref(dd,key1);
1592  ABC_FREE(vect0);
1593  return(NULL);
1594  }
1595  cuddRef(T);
1596  E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
1597  ABC_FREE(vect0);
1598  if (E == NULL) {
1599  Cudd_RecursiveDeref(dd,key1);
1600  Cudd_RecursiveDeref(dd,T);
1601  return(NULL);
1602  }
1603  cuddRef(E);
1604  Cudd_RecursiveDeref(dd,key1);
1605 
1606  /* Retrieve the 0-1 ADD for the current top variable from vector,
1607  ** and call cuddAddIteRecur with the T and E we just created.
1608  */
1609  r = cuddAddIteRecur(dd,vector[index],T,E);
1610  if (r == NULL) {
1611  Cudd_RecursiveDeref(dd,T);
1612  Cudd_RecursiveDeref(dd,E);
1613  return(NULL);
1614  }
1615  cuddRef(r);
1616  Cudd_RecursiveDeref(dd,T);
1617  Cudd_RecursiveDeref(dd,E);
1618  cuddDeref(r);
1619 
1620  /* Store answer to trim recursion. */
1621  cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);
1622 
1623  return(r);
1624 
1625 } /* end of cuddAddNonSimComposeRecur */
1626 
1627 
1628 /**Function********************************************************************
1629 
1630  Synopsis [Performs the recursive step of Cudd_bddVectorCompose.]
1631 
1632  Description []
1633 
1634  SideEffects [None]
1635 
1636  SeeAlso []
1637 
1638 ******************************************************************************/
1639 static DdNode *
1640 cuddBddVectorComposeRecur(
1641  DdManager * dd /* DD manager */,
1642  DdHashTable * table /* computed table */,
1643  DdNode * f /* BDD in which to compose */,
1644  DdNode ** vector /* functions to be composed */,
1645  int deepest /* depth of the deepest substitution */)
1646 {
1647  DdNode *F,*T,*E;
1648  DdNode *res;
1649 
1650  statLine(dd);
1651  F = Cudd_Regular(f);
1652 
1653  /* If we are past the deepest substitution, return f. */
1654  if (cuddI(dd,F->index) > deepest) {
1655  return(f);
1656  }
1657 
1658  /* If problem already solved, look up answer and return. */
1659  if ((res = cuddHashTableLookup1(table,F)) != NULL) {
1660 #ifdef DD_DEBUG
1661  bddVectorComposeHits++;
1662 #endif
1663  return(Cudd_NotCond(res,F != f));
1664  }
1665 
1666  /* Split and recur on children of this node. */
1667  T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
1668  if (T == NULL) return(NULL);
1669  cuddRef(T);
1670  E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
1671  if (E == NULL) {
1672  Cudd_IterDerefBdd(dd, T);
1673  return(NULL);
1674  }
1675  cuddRef(E);
1676 
1677  /* Call cuddBddIteRecur with the BDD that replaces the current top
1678  ** variable and the T and E we just created.
1679  */
1680  res = cuddBddIteRecur(dd,vector[F->index],T,E);
1681  if (res == NULL) {
1682  Cudd_IterDerefBdd(dd, T);
1683  Cudd_IterDerefBdd(dd, E);
1684  return(NULL);
1685  }
1686  cuddRef(res);
1687  Cudd_IterDerefBdd(dd, T);
1688  Cudd_IterDerefBdd(dd, E);
1689 
1690  /* Do not keep the result if the reference count is only 1, since
1691  ** it will not be visited again.
1692  */
1693  if (F->ref != 1) {
1694  ptrint fanout = (ptrint) F->ref;
1695  cuddSatDec(fanout);
1696  if (!cuddHashTableInsert1(table,F,res,fanout)) {
1697  Cudd_IterDerefBdd(dd, res);
1698  return(NULL);
1699  }
1700  }
1701  cuddDeref(res);
1702  return(Cudd_NotCond(res,F != f));
1703 
1704 } /* end of cuddBddVectorComposeRecur */
1705 
1706 
1707 /**Function********************************************************************
1708 
1709  Synopsis [Comparison of a function to the i-th ADD variable.]
1710 
1711  Description [Comparison of a function to the i-th ADD variable. Returns 1 if
1712  the function is the i-th ADD variable; 0 otherwise.]
1713 
1714  SideEffects [None]
1715 
1716  SeeAlso []
1717 
1718 ******************************************************************************/
1719 DD_INLINE
1720 static int
1721 ddIsIthAddVar(
1722  DdManager * dd,
1723  DdNode * f,
1724  unsigned int i)
1725 {
1726  return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));
1727 
1728 } /* end of ddIsIthAddVar */
1729 
1730 
1731 /**Function********************************************************************
1732 
1733  Synopsis [Comparison of a pair of functions to the i-th ADD variable.]
1734 
1735  Description [Comparison of a pair of functions to the i-th ADD
1736  variable. Returns 1 if the functions are the i-th ADD variable and its
1737  complement; 0 otherwise.]
1738 
1739  SideEffects [None]
1740 
1741  SeeAlso []
1742 
1743 ******************************************************************************/
1744 DD_INLINE
1745 static int
1746 ddIsIthAddVarPair(
1747  DdManager * dd,
1748  DdNode * f,
1749  DdNode * g,
1750  unsigned int i)
1751 {
1752  return(f->index == i && g->index == i &&
1753  cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
1754  cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
1755 
1756 } /* end of ddIsIthAddVarPair */
1757 
1758 
1759 ABC_NAMESPACE_IMPL_END
1760 
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
ddIsIthAddVarPair
static DD_INLINE int ddIsIthAddVarPair(DdManager *dd, DdNode *f, DdNode *g, unsigned int i)
Definition: cuddCompose.c:1746
cuddCacheFlush
void cuddCacheFlush(DdManager *table)
Definition: cuddCache.c:1047
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_addSwapVariables
DdNode * Cudd_addSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:283
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdManager::map
int * map
Definition: cuddInt.h:391
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddBddComposeRecur
DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Definition: cuddCompose.c:850
DdManager::size
int size
Definition: cuddInt.h:361
DD_ADD_COMPOSE_RECUR_TAG
#define DD_ADD_COMPOSE_RECUR_TAG
Definition: cuddInt.h:180
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Cudd_bddSwapVariables
DdNode * Cudd_bddSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:464
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Definition: cuddAddApply.c:809
Cudd_addNonSimCompose
DdNode * Cudd_addNonSimCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:682
cuddCacheInsert
void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)
Definition: cuddCache.c:222
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cudd_addGeneralVectorCompose
DdNode * Cudd_addGeneralVectorCompose(DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff)
Definition: cuddCompose.c:621
Cudd_addApply
DdNode * Cudd_addApply(DdManager *dd, DdNode *(*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)
cuddAddExistAbstractRecur
DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:256
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
cuddHashTableLookup1
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
Definition: cuddLCache.c:819
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
util_hack.h
ddIsIthAddVar
static DD_INLINE int ddIsIthAddVar(DdManager *dd, DdNode *f, unsigned int i)
Definition: cuddCompose.c:1721
DD_INLINE
#define DD_INLINE
Definition: cuddInt.h:90
DD_ADD_NON_SIM_COMPOSE_TAG
#define DD_ADD_NON_SIM_COMPOSE_TAG
Definition: cuddInt.h:181
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Cudd_addIthVar
DdNode * Cudd_addIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:384
Cudd_addXnor
DdNode * Cudd_addXnor(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:713
cuddAddVectorComposeRecur
static DdNode * cuddAddVectorComposeRecur(DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest)
Definition: cuddCompose.c:1307
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
Cudd_bddPermute
DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:332
ptrint
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
DdManager::maxSize
int maxSize
Definition: cuddInt.h:363
Cudd_addPlus
DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:168
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
cuddAddComposeRecur
DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Definition: cuddCompose.c:952
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddHashTableQuit
void cuddHashTableQuit(DdHashTable *hash)
Definition: cuddLCache.c:595
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
DdManager::memused
unsigned long memused
Definition: cuddInt.h:449
Cudd_bddVarMap
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:373
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
Cudd_addCompose
DdNode * Cudd_addCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Definition: cuddCompose.c:204
cuddHashTableInsert1
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
Definition: cuddLCache.c:767
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
key
enum keys key
Definition: misc/espresso/main.h:25
Cudd_bddAdjPermuteX
DdNode * Cudd_bddAdjPermuteX(DdManager *dd, DdNode *B, DdNode **x, int n)
Definition: cuddCompose.c:512
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
cuddSatDec
#define cuddSatDec(x)
Definition: cuddInt.h:896
cuddHashTableInit
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Definition: cuddLCache.c:538
DD_UNUSED
static ABC_NAMESPACE_IMPL_START char rcsid[] DD_UNUSED
Definition: cuddCompose.c:110
cuddAddPermuteRecur
static DdNode * cuddAddPermuteRecur(DdManager *manager, DdHashTable *table, DdNode *node, int *permut)
Definition: cuddCompose.c:1057
cuddBddVectorComposeRecur
static DdNode * cuddBddVectorComposeRecur(DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest)
Definition: cuddCompose.c:1640
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
Cudd_bddCompose
DdNode * Cudd_bddCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Definition: cuddCompose.c:167
Cudd_addVectorCompose
DdNode * Cudd_addVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:563
cuddAddNonSimComposeRecur
static DdNode * cuddAddNonSimComposeRecur(DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub)
Definition: cuddCompose.c:1480
cuddAddIteRecur
DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:445
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
Cudd_addTimes
DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:208
DD_BDD_COMPOSE_RECUR_TAG
#define DD_BDD_COMPOSE_RECUR_TAG
Definition: cuddInt.h:179
cuddAddGeneralVectorComposeRecur
static DdNode * cuddAddGeneralVectorComposeRecur(DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest)
Definition: cuddCompose.c:1383
cuddBddPermuteRecur
static DdNode * cuddBddPermuteRecur(DdManager *manager, DdHashTable *table, DdNode *node, int *permut)
Definition: cuddCompose.c:1150
Cudd_SetVarMap
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:416
DdManager::perm
int * perm
Definition: cuddInt.h:386
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
cuddCacheLookup
DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddCache.c:369
Cudd_bddVectorCompose
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:791
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
Cudd_addPermute
DdNode * Cudd_addPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:242
cuddBddVarMapRecur
static DdNode * cuddBddVarMapRecur(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:1232
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:633