abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddDecomp.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddDecomp.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Functions for BDD decomposition.]
8 
9  Description [External procedures included in this file:
10  <ul>
11  <li> Cudd_bddApproxConjDecomp()
12  <li> Cudd_bddApproxDisjDecomp()
13  <li> Cudd_bddIterConjDecomp()
14  <li> Cudd_bddIterDisjDecomp()
15  <li> Cudd_bddGenConjDecomp()
16  <li> Cudd_bddGenDisjDecomp()
17  <li> Cudd_bddVarConjDecomp()
18  <li> Cudd_bddVarDisjDecomp()
19  </ul>
20  Static procedures included in this module:
21  <ul>
22  <li> cuddConjunctsAux()
23  <li> CreateBotDist()
24  <li> BuildConjuncts()
25  <li> ConjunctsFree()
26  </ul>]
27 
28  Author [Kavita Ravi, Fabio Somenzi]
29 
30  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
31 
32  All rights reserved.
33 
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37 
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40 
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44 
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48 
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61 
62 ******************************************************************************/
63 
64 #include "misc/util/util_hack.h"
65 #include "cuddInt.h"
66 
67 ABC_NAMESPACE_IMPL_START
68 
69 
70 
71 /*---------------------------------------------------------------------------*/
72 /* Constant declarations */
73 /*---------------------------------------------------------------------------*/
74 #define DEPTH 5
75 #define THRESHOLD 10
76 #define NONE 0
77 #define PAIR_ST 1
78 #define PAIR_CR 2
79 #define G_ST 3
80 #define G_CR 4
81 #define H_ST 5
82 #define H_CR 6
83 #define BOTH_G 7
84 #define BOTH_H 8
85 
86 /*---------------------------------------------------------------------------*/
87 /* Stucture declarations */
88 /*---------------------------------------------------------------------------*/
89 
90 /*---------------------------------------------------------------------------*/
91 /* Type declarations */
92 /*---------------------------------------------------------------------------*/
93 typedef struct Conjuncts {
94  DdNode *g;
95  DdNode *h;
96 } Conjuncts;
97 
98 typedef struct NodeStat {
99  int distance;
100  int localRef;
101 } NodeStat;
102 
103 
104 /*---------------------------------------------------------------------------*/
105 /* Variable declarations */
106 /*---------------------------------------------------------------------------*/
107 
108 #ifndef lint
109 static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $";
110 #endif
111 
112 static DdNode *one, *zero;
113 long lastTimeG;
114 
115 /*---------------------------------------------------------------------------*/
116 /* Macro declarations */
117 /*---------------------------------------------------------------------------*/
118 
119 
120 #define FactorsNotStored(factors) ((int)((long)(factors) & 01))
121 
122 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
123 
124 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
125 
126 /**AutomaticStart*************************************************************/
127 
128 /*---------------------------------------------------------------------------*/
129 /* Static function prototypes */
130 /*---------------------------------------------------------------------------*/
131 
132 static NodeStat * CreateBotDist (DdNode * node, st__table * distanceTable);
133 static double CountMinterms (DdNode * node, double max, st__table * mintermTable, FILE *fp);
134 static void ConjunctsFree (DdManager * dd, Conjuncts * factors);
135 static int PairInTables (DdNode * g, DdNode * h, st__table * ghTable);
136 static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st__table * ghTable, st__table * cacheTable);
137 static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st__table * ghTable, st__table * cacheTable);
138 static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st__table * ghTable, st__table * cacheTable, int * outOfMem);
139 static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st__table * ghTable, st__table * cacheTable, int switched);
140 static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st__table * distanceTable, st__table * cacheTable, int approxDistance, int maxLocalRef, st__table * ghTable, st__table * mintermTable);
141 static int cuddConjunctsAux (DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2);
142 
143 /**AutomaticEnd***************************************************************/
144 
145 
146 /*---------------------------------------------------------------------------*/
147 /* Definition of exported functions */
148 /*---------------------------------------------------------------------------*/
149 
150 
151 /**Function********************************************************************
152 
153  Synopsis [Performs two-way conjunctive decomposition of a BDD.]
154 
155  Description [Performs two-way conjunctive decomposition of a
156  BDD. This procedure owes its name to the use of supersetting to
157  obtain an initial factor of the given function. Returns the number
158  of conjuncts produced, that is, 2 if successful; 1 if no meaningful
159  decomposition was found; 0 otherwise. The conjuncts produced by this
160  procedure tend to be imbalanced.]
161 
162  SideEffects [The factors are returned in an array as side effects.
163  The array is allocated by this function. It is the caller's responsibility
164  to free it. On successful completion, the conjuncts are already
165  referenced. If the function returns 0, the array for the conjuncts is
166  not allocated. If the function returns 1, the only factor equals the
167  function to be decomposed.]
168 
169  SeeAlso [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp
170  Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
171  Cudd_bddSqueeze Cudd_bddLICompaction]
172 
173 ******************************************************************************/
174 int
175 Cudd_bddApproxConjDecomp(
176  DdManager * dd /* manager */,
177  DdNode * f /* function to be decomposed */,
178  DdNode *** conjuncts /* address of the first factor */)
179 {
180  DdNode *superset1, *superset2, *glocal, *hlocal;
181  int nvars = Cudd_SupportSize(dd,f);
182 
183  /* Find a tentative first factor by overapproximation and minimization. */
184  superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
185  if (superset1 == NULL) return(0);
186  cuddRef(superset1);
187  superset2 = Cudd_bddSqueeze(dd,f,superset1);
188  if (superset2 == NULL) {
189  Cudd_RecursiveDeref(dd,superset1);
190  return(0);
191  }
192  cuddRef(superset2);
193  Cudd_RecursiveDeref(dd,superset1);
194 
195  /* Compute the second factor by minimization. */
196  hlocal = Cudd_bddLICompaction(dd,f,superset2);
197  if (hlocal == NULL) {
198  Cudd_RecursiveDeref(dd,superset2);
199  return(0);
200  }
201  cuddRef(hlocal);
202 
203  /* Refine the first factor by minimization. If h turns out to be f, this
204  ** step guarantees that g will be 1. */
205  glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
206  if (glocal == NULL) {
207  Cudd_RecursiveDeref(dd,superset2);
208  Cudd_RecursiveDeref(dd,hlocal);
209  return(0);
210  }
211  cuddRef(glocal);
212  Cudd_RecursiveDeref(dd,superset2);
213 
214  if (glocal != DD_ONE(dd)) {
215  if (hlocal != DD_ONE(dd)) {
216  *conjuncts = ABC_ALLOC(DdNode *,2);
217  if (*conjuncts == NULL) {
218  Cudd_RecursiveDeref(dd,glocal);
219  Cudd_RecursiveDeref(dd,hlocal);
220  dd->errorCode = CUDD_MEMORY_OUT;
221  return(0);
222  }
223  (*conjuncts)[0] = glocal;
224  (*conjuncts)[1] = hlocal;
225  return(2);
226  } else {
227  Cudd_RecursiveDeref(dd,hlocal);
228  *conjuncts = ABC_ALLOC(DdNode *,1);
229  if (*conjuncts == NULL) {
230  Cudd_RecursiveDeref(dd,glocal);
231  dd->errorCode = CUDD_MEMORY_OUT;
232  return(0);
233  }
234  (*conjuncts)[0] = glocal;
235  return(1);
236  }
237  } else {
238  Cudd_RecursiveDeref(dd,glocal);
239  *conjuncts = ABC_ALLOC(DdNode *,1);
240  if (*conjuncts == NULL) {
241  Cudd_RecursiveDeref(dd,hlocal);
242  dd->errorCode = CUDD_MEMORY_OUT;
243  return(0);
244  }
245  (*conjuncts)[0] = hlocal;
246  return(1);
247  }
248 
249 } /* end of Cudd_bddApproxConjDecomp */
250 
251 
252 /**Function********************************************************************
253 
254  Synopsis [Performs two-way disjunctive decomposition of a BDD.]
255 
256  Description [Performs two-way disjunctive decomposition of a BDD.
257  Returns the number of disjuncts produced, that is, 2 if successful;
258  1 if no meaningful decomposition was found; 0 otherwise. The
259  disjuncts produced by this procedure tend to be imbalanced.]
260 
261  SideEffects [The two disjuncts are returned in an array as side effects.
262  The array is allocated by this function. It is the caller's responsibility
263  to free it. On successful completion, the disjuncts are already
264  referenced. If the function returns 0, the array for the disjuncts is
265  not allocated. If the function returns 1, the only factor equals the
266  function to be decomposed.]
267 
268  SeeAlso [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp
269  Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
270 
271 ******************************************************************************/
272 int
273 Cudd_bddApproxDisjDecomp(
274  DdManager * dd /* manager */,
275  DdNode * f /* function to be decomposed */,
276  DdNode *** disjuncts /* address of the array of the disjuncts */)
277 {
278  int result, i;
279 
280  result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
281  for (i = 0; i < result; i++) {
282  (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
283  }
284  return(result);
285 
286 } /* end of Cudd_bddApproxDisjDecomp */
287 
288 
289 /**Function********************************************************************
290 
291  Synopsis [Performs two-way conjunctive decomposition of a BDD.]
292 
293  Description [Performs two-way conjunctive decomposition of a
294  BDD. This procedure owes its name to the iterated use of
295  supersetting to obtain a factor of the given function. Returns the
296  number of conjuncts produced, that is, 2 if successful; 1 if no
297  meaningful decomposition was found; 0 otherwise. The conjuncts
298  produced by this procedure tend to be imbalanced.]
299 
300  SideEffects [The factors are returned in an array as side effects.
301  The array is allocated by this function. It is the caller's responsibility
302  to free it. On successful completion, the conjuncts are already
303  referenced. If the function returns 0, the array for the conjuncts is
304  not allocated. If the function returns 1, the only factor equals the
305  function to be decomposed.]
306 
307  SeeAlso [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp
308  Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
309  Cudd_bddSqueeze Cudd_bddLICompaction]
310 
311 ******************************************************************************/
312 int
313 Cudd_bddIterConjDecomp(
314  DdManager * dd /* manager */,
315  DdNode * f /* function to be decomposed */,
316  DdNode *** conjuncts /* address of the array of conjuncts */)
317 {
318  DdNode *superset1, *superset2, *old[2], *res[2];
319  int sizeOld, sizeNew;
320  int nvars = Cudd_SupportSize(dd,f);
321 
322  old[0] = DD_ONE(dd);
323  cuddRef(old[0]);
324  old[1] = f;
325  cuddRef(old[1]);
326  sizeOld = Cudd_SharingSize(old,2);
327 
328  do {
329  /* Find a tentative first factor by overapproximation and
330  ** minimization. */
331  superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
332  if (superset1 == NULL) {
333  Cudd_RecursiveDeref(dd,old[0]);
334  Cudd_RecursiveDeref(dd,old[1]);
335  return(0);
336  }
337  cuddRef(superset1);
338  superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
339  if (superset2 == NULL) {
340  Cudd_RecursiveDeref(dd,old[0]);
341  Cudd_RecursiveDeref(dd,old[1]);
342  Cudd_RecursiveDeref(dd,superset1);
343  return(0);
344  }
345  cuddRef(superset2);
346  Cudd_RecursiveDeref(dd,superset1);
347  res[0] = Cudd_bddAnd(dd,old[0],superset2);
348  if (res[0] == NULL) {
349  Cudd_RecursiveDeref(dd,superset2);
350  Cudd_RecursiveDeref(dd,old[0]);
351  Cudd_RecursiveDeref(dd,old[1]);
352  return(0);
353  }
354  cuddRef(res[0]);
355  Cudd_RecursiveDeref(dd,superset2);
356  if (res[0] == old[0]) {
357  Cudd_RecursiveDeref(dd,res[0]);
358  break; /* avoid infinite loop */
359  }
360 
361  /* Compute the second factor by minimization. */
362  res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
363  if (res[1] == NULL) {
364  Cudd_RecursiveDeref(dd,old[0]);
365  Cudd_RecursiveDeref(dd,old[1]);
366  return(0);
367  }
368  cuddRef(res[1]);
369 
370  sizeNew = Cudd_SharingSize(res,2);
371  if (sizeNew <= sizeOld) {
372  Cudd_RecursiveDeref(dd,old[0]);
373  old[0] = res[0];
374  Cudd_RecursiveDeref(dd,old[1]);
375  old[1] = res[1];
376  sizeOld = sizeNew;
377  } else {
378  Cudd_RecursiveDeref(dd,res[0]);
379  Cudd_RecursiveDeref(dd,res[1]);
380  break;
381  }
382 
383  } while (1);
384 
385  /* Refine the first factor by minimization. If h turns out to
386  ** be f, this step guarantees that g will be 1. */
387  superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
388  if (superset1 == NULL) {
389  Cudd_RecursiveDeref(dd,old[0]);
390  Cudd_RecursiveDeref(dd,old[1]);
391  return(0);
392  }
393  cuddRef(superset1);
394  Cudd_RecursiveDeref(dd,old[0]);
395  old[0] = superset1;
396 
397  if (old[0] != DD_ONE(dd)) {
398  if (old[1] != DD_ONE(dd)) {
399  *conjuncts = ABC_ALLOC(DdNode *,2);
400  if (*conjuncts == NULL) {
401  Cudd_RecursiveDeref(dd,old[0]);
402  Cudd_RecursiveDeref(dd,old[1]);
403  dd->errorCode = CUDD_MEMORY_OUT;
404  return(0);
405  }
406  (*conjuncts)[0] = old[0];
407  (*conjuncts)[1] = old[1];
408  return(2);
409  } else {
410  Cudd_RecursiveDeref(dd,old[1]);
411  *conjuncts = ABC_ALLOC(DdNode *,1);
412  if (*conjuncts == NULL) {
413  Cudd_RecursiveDeref(dd,old[0]);
414  dd->errorCode = CUDD_MEMORY_OUT;
415  return(0);
416  }
417  (*conjuncts)[0] = old[0];
418  return(1);
419  }
420  } else {
421  Cudd_RecursiveDeref(dd,old[0]);
422  *conjuncts = ABC_ALLOC(DdNode *,1);
423  if (*conjuncts == NULL) {
424  Cudd_RecursiveDeref(dd,old[1]);
425  dd->errorCode = CUDD_MEMORY_OUT;
426  return(0);
427  }
428  (*conjuncts)[0] = old[1];
429  return(1);
430  }
431 
432 } /* end of Cudd_bddIterConjDecomp */
433 
434 
435 /**Function********************************************************************
436 
437  Synopsis [Performs two-way disjunctive decomposition of a BDD.]
438 
439  Description [Performs two-way disjunctive decomposition of a BDD.
440  Returns the number of disjuncts produced, that is, 2 if successful;
441  1 if no meaningful decomposition was found; 0 otherwise. The
442  disjuncts produced by this procedure tend to be imbalanced.]
443 
444  SideEffects [The two disjuncts are returned in an array as side effects.
445  The array is allocated by this function. It is the caller's responsibility
446  to free it. On successful completion, the disjuncts are already
447  referenced. If the function returns 0, the array for the disjuncts is
448  not allocated. If the function returns 1, the only factor equals the
449  function to be decomposed.]
450 
451  SeeAlso [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp
452  Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
453 
454 ******************************************************************************/
455 int
456 Cudd_bddIterDisjDecomp(
457  DdManager * dd /* manager */,
458  DdNode * f /* function to be decomposed */,
459  DdNode *** disjuncts /* address of the array of the disjuncts */)
460 {
461  int result, i;
462 
463  result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
464  for (i = 0; i < result; i++) {
465  (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
466  }
467  return(result);
468 
469 } /* end of Cudd_bddIterDisjDecomp */
470 
471 
472 /**Function********************************************************************
473 
474  Synopsis [Performs two-way conjunctive decomposition of a BDD.]
475 
476  Description [Performs two-way conjunctive decomposition of a
477  BDD. This procedure owes its name to the fact tht it generalizes the
478  decomposition based on the cofactors with respect to one
479  variable. Returns the number of conjuncts produced, that is, 2 if
480  successful; 1 if no meaningful decomposition was found; 0
481  otherwise. The conjuncts produced by this procedure tend to be
482  balanced.]
483 
484  SideEffects [The two factors are returned in an array as side effects.
485  The array is allocated by this function. It is the caller's responsibility
486  to free it. On successful completion, the conjuncts are already
487  referenced. If the function returns 0, the array for the conjuncts is
488  not allocated. If the function returns 1, the only factor equals the
489  function to be decomposed.]
490 
491  SeeAlso [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp
492  Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]
493 
494 ******************************************************************************/
495 int
496 Cudd_bddGenConjDecomp(
497  DdManager * dd /* manager */,
498  DdNode * f /* function to be decomposed */,
499  DdNode *** conjuncts /* address of the array of conjuncts */)
500 {
501  int result;
502  DdNode *glocal, *hlocal;
503 
504  one = DD_ONE(dd);
505  zero = Cudd_Not(one);
506 
507  do {
508  dd->reordered = 0;
509  result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
510  } while (dd->reordered == 1);
511 
512  if (result == 0) {
513  return(0);
514  }
515 
516  if (glocal != one) {
517  if (hlocal != one) {
518  *conjuncts = ABC_ALLOC(DdNode *,2);
519  if (*conjuncts == NULL) {
520  Cudd_RecursiveDeref(dd,glocal);
521  Cudd_RecursiveDeref(dd,hlocal);
522  dd->errorCode = CUDD_MEMORY_OUT;
523  return(0);
524  }
525  (*conjuncts)[0] = glocal;
526  (*conjuncts)[1] = hlocal;
527  return(2);
528  } else {
529  Cudd_RecursiveDeref(dd,hlocal);
530  *conjuncts = ABC_ALLOC(DdNode *,1);
531  if (*conjuncts == NULL) {
532  Cudd_RecursiveDeref(dd,glocal);
533  dd->errorCode = CUDD_MEMORY_OUT;
534  return(0);
535  }
536  (*conjuncts)[0] = glocal;
537  return(1);
538  }
539  } else {
540  Cudd_RecursiveDeref(dd,glocal);
541  *conjuncts = ABC_ALLOC(DdNode *,1);
542  if (*conjuncts == NULL) {
543  Cudd_RecursiveDeref(dd,hlocal);
544  dd->errorCode = CUDD_MEMORY_OUT;
545  return(0);
546  }
547  (*conjuncts)[0] = hlocal;
548  return(1);
549  }
550 
551 } /* end of Cudd_bddGenConjDecomp */
552 
553 
554 /**Function********************************************************************
555 
556  Synopsis [Performs two-way disjunctive decomposition of a BDD.]
557 
558  Description [Performs two-way disjunctive decomposition of a BDD.
559  Returns the number of disjuncts produced, that is, 2 if successful;
560  1 if no meaningful decomposition was found; 0 otherwise. The
561  disjuncts produced by this procedure tend to be balanced.]
562 
563  SideEffects [The two disjuncts are returned in an array as side effects.
564  The array is allocated by this function. It is the caller's responsibility
565  to free it. On successful completion, the disjuncts are already
566  referenced. If the function returns 0, the array for the disjuncts is
567  not allocated. If the function returns 1, the only factor equals the
568  function to be decomposed.]
569 
570  SeeAlso [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp
571  Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]
572 
573 ******************************************************************************/
574 int
575 Cudd_bddGenDisjDecomp(
576  DdManager * dd /* manager */,
577  DdNode * f /* function to be decomposed */,
578  DdNode *** disjuncts /* address of the array of the disjuncts */)
579 {
580  int result, i;
581 
582  result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
583  for (i = 0; i < result; i++) {
584  (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
585  }
586  return(result);
587 
588 } /* end of Cudd_bddGenDisjDecomp */
589 
590 
591 /**Function********************************************************************
592 
593  Synopsis [Performs two-way conjunctive decomposition of a BDD.]
594 
595  Description [Conjunctively decomposes one BDD according to a
596  variable. If <code>f</code> is the function of the BDD and
597  <code>x</code> is the variable, the decomposition is
598  <code>(f+x)(f+x')</code>. The variable is chosen so as to balance
599  the sizes of the two conjuncts and to keep them small. Returns the
600  number of conjuncts produced, that is, 2 if successful; 1 if no
601  meaningful decomposition was found; 0 otherwise.]
602 
603  SideEffects [The two factors are returned in an array as side effects.
604  The array is allocated by this function. It is the caller's responsibility
605  to free it. On successful completion, the conjuncts are already
606  referenced. If the function returns 0, the array for the conjuncts is
607  not allocated. If the function returns 1, the only factor equals the
608  function to be decomposed.]
609 
610  SeeAlso [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp
611  Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]
612 
613 *****************************************************************************/
614 int
615 Cudd_bddVarConjDecomp(
616  DdManager * dd /* manager */,
617  DdNode * f /* function to be decomposed */,
618  DdNode *** conjuncts /* address of the array of conjuncts */)
619 {
620  int best;
621  int min;
622  DdNode *support, *scan, *var, *glocal, *hlocal;
623 
624  /* Find best cofactoring variable. */
625  support = Cudd_Support(dd,f);
626  if (support == NULL) return(0);
627  if (Cudd_IsConstant(support)) {
628  *conjuncts = ABC_ALLOC(DdNode *,1);
629  if (*conjuncts == NULL) {
630  dd->errorCode = CUDD_MEMORY_OUT;
631  return(0);
632  }
633  (*conjuncts)[0] = f;
634  cuddRef((*conjuncts)[0]);
635  return(1);
636  }
637  cuddRef(support);
638  min = 1000000000;
639  best = -1;
640  scan = support;
641  while (!Cudd_IsConstant(scan)) {
642  int i = scan->index;
643  int est1 = Cudd_EstimateCofactor(dd,f,i,1);
644  int est0 = Cudd_EstimateCofactor(dd,f,i,0);
645  /* Minimize the size of the larger of the two cofactors. */
646  int est = (est1 > est0) ? est1 : est0;
647  if (est < min) {
648  min = est;
649  best = i;
650  }
651  scan = cuddT(scan);
652  }
653 #ifdef DD_DEBUG
654  assert(best >= 0 && best < dd->size);
655 #endif
656  Cudd_RecursiveDeref(dd,support);
657 
658  var = Cudd_bddIthVar(dd,best);
659  glocal = Cudd_bddOr(dd,f,var);
660  if (glocal == NULL) {
661  return(0);
662  }
663  cuddRef(glocal);
664  hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
665  if (hlocal == NULL) {
666  Cudd_RecursiveDeref(dd,glocal);
667  return(0);
668  }
669  cuddRef(hlocal);
670 
671  if (glocal != DD_ONE(dd)) {
672  if (hlocal != DD_ONE(dd)) {
673  *conjuncts = ABC_ALLOC(DdNode *,2);
674  if (*conjuncts == NULL) {
675  Cudd_RecursiveDeref(dd,glocal);
676  Cudd_RecursiveDeref(dd,hlocal);
677  dd->errorCode = CUDD_MEMORY_OUT;
678  return(0);
679  }
680  (*conjuncts)[0] = glocal;
681  (*conjuncts)[1] = hlocal;
682  return(2);
683  } else {
684  Cudd_RecursiveDeref(dd,hlocal);
685  *conjuncts = ABC_ALLOC(DdNode *,1);
686  if (*conjuncts == NULL) {
687  Cudd_RecursiveDeref(dd,glocal);
688  dd->errorCode = CUDD_MEMORY_OUT;
689  return(0);
690  }
691  (*conjuncts)[0] = glocal;
692  return(1);
693  }
694  } else {
695  Cudd_RecursiveDeref(dd,glocal);
696  *conjuncts = ABC_ALLOC(DdNode *,1);
697  if (*conjuncts == NULL) {
698  Cudd_RecursiveDeref(dd,hlocal);
699  dd->errorCode = CUDD_MEMORY_OUT;
700  return(0);
701  }
702  (*conjuncts)[0] = hlocal;
703  return(1);
704  }
705 
706 } /* end of Cudd_bddVarConjDecomp */
707 
708 
709 /**Function********************************************************************
710 
711  Synopsis [Performs two-way disjunctive decomposition of a BDD.]
712 
713  Description [Performs two-way disjunctive decomposition of a BDD
714  according to a variable. If <code>f</code> is the function of the
715  BDD and <code>x</code> is the variable, the decomposition is
716  <code>f*x + f*x'</code>. The variable is chosen so as to balance
717  the sizes of the two disjuncts and to keep them small. Returns the
718  number of disjuncts produced, that is, 2 if successful; 1 if no
719  meaningful decomposition was found; 0 otherwise.]
720 
721  SideEffects [The two disjuncts are returned in an array as side effects.
722  The array is allocated by this function. It is the caller's responsibility
723  to free it. On successful completion, the disjuncts are already
724  referenced. If the function returns 0, the array for the disjuncts is
725  not allocated. If the function returns 1, the only factor equals the
726  function to be decomposed.]
727 
728  SeeAlso [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp
729  Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]
730 
731 ******************************************************************************/
732 int
733 Cudd_bddVarDisjDecomp(
734  DdManager * dd /* manager */,
735  DdNode * f /* function to be decomposed */,
736  DdNode *** disjuncts /* address of the array of the disjuncts */)
737 {
738  int result, i;
739 
740  result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
741  for (i = 0; i < result; i++) {
742  (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
743  }
744  return(result);
745 
746 } /* end of Cudd_bddVarDisjDecomp */
747 
748 
749 /*---------------------------------------------------------------------------*/
750 /* Definition of internal functions */
751 /*---------------------------------------------------------------------------*/
752 
753 /*---------------------------------------------------------------------------*/
754 /* Definition of static functions */
755 /*---------------------------------------------------------------------------*/
756 
757 
758 /**Function********************************************************************
759 
760  Synopsis [Get longest distance of node from constant.]
761 
762  Description [Get longest distance of node from constant. Returns the
763  distance of the root from the constant if successful; CUDD_OUT_OF_MEM
764  otherwise.]
765 
766  SideEffects [None]
767 
768  SeeAlso []
769 
770 ******************************************************************************/
771 static NodeStat *
772 CreateBotDist(
773  DdNode * node,
774  st__table * distanceTable)
775 {
776  DdNode *N, *Nv, *Nnv;
777  int distance, distanceNv, distanceNnv;
778  NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;
779 
780 #if 0
781  if (Cudd_IsConstant(node)) {
782  return(0);
783  }
784 #endif
785 
786  /* Return the entry in the table if found. */
787  N = Cudd_Regular(node);
788  if ( st__lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
789  nodeStat->localRef++;
790  return(nodeStat);
791  }
792 
793  Nv = cuddT(N);
794  Nnv = cuddE(N);
795  Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
796  Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
797 
798  /* Recur on the children. */
799  nodeStatNv = CreateBotDist(Nv, distanceTable);
800  if (nodeStatNv == NULL) return(NULL);
801  distanceNv = nodeStatNv->distance;
802 
803  nodeStatNnv = CreateBotDist(Nnv, distanceTable);
804  if (nodeStatNnv == NULL) return(NULL);
805  distanceNnv = nodeStatNnv->distance;
806  /* Store max distance from constant; note sometimes this distance
807  ** may be to 0.
808  */
809  distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
810 
811  nodeStat = ABC_ALLOC(NodeStat, 1);
812  if (nodeStat == NULL) {
813  return(0);
814  }
815  nodeStat->distance = distance;
816  nodeStat->localRef = 1;
817 
818  if ( st__insert(distanceTable, (char *)N, (char *)nodeStat) ==
819  st__OUT_OF_MEM) {
820  return(0);
821 
822  }
823  return(nodeStat);
824 
825 } /* end of CreateBotDist */
826 
827 
828 /**Function********************************************************************
829 
830  Synopsis [Count the number of minterms of each node ina a BDD and
831  store it in a hash table.]
832 
833  Description []
834 
835  SideEffects [None]
836 
837  SeeAlso []
838 
839 ******************************************************************************/
840 static double
841 CountMinterms(
842  DdNode * node,
843  double max,
844  st__table * mintermTable,
845  FILE *fp)
846 {
847  DdNode *N, *Nv, *Nnv;
848  double min, minNv, minNnv;
849  double *dummy;
850 
851  N = Cudd_Regular(node);
852 
853  if (cuddIsConstant(N)) {
854  if (node == zero) {
855  return(0);
856  } else {
857  return(max);
858  }
859  }
860 
861  /* Return the entry in the table if found. */
862  if ( st__lookup(mintermTable, (const char *)node, (char **)&dummy)) {
863  min = *dummy;
864  return(min);
865  }
866 
867  Nv = cuddT(N);
868  Nnv = cuddE(N);
869  Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
870  Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
871 
872  /* Recur on the children. */
873  minNv = CountMinterms(Nv, max, mintermTable, fp);
874  if (minNv == -1.0) return(-1.0);
875  minNnv = CountMinterms(Nnv, max, mintermTable, fp);
876  if (minNnv == -1.0) return(-1.0);
877  min = minNv / 2.0 + minNnv / 2.0;
878  /* store
879  */
880 
881  dummy = ABC_ALLOC(double, 1);
882  if (dummy == NULL) return(-1.0);
883  *dummy = min;
884  if ( st__insert(mintermTable, (char *)node, (char *)dummy) == st__OUT_OF_MEM) {
885  (void) fprintf(fp, "st table insert failed\n");
886  }
887  return(min);
888 
889 } /* end of CountMinterms */
890 
891 
892 /**Function********************************************************************
893 
894  Synopsis [Free factors structure]
895 
896  Description []
897 
898  SideEffects [None]
899 
900  SeeAlso []
901 
902 ******************************************************************************/
903 static void
904 ConjunctsFree(
905  DdManager * dd,
906  Conjuncts * factors)
907 {
908  Cudd_RecursiveDeref(dd, factors->g);
909  Cudd_RecursiveDeref(dd, factors->h);
910  ABC_FREE(factors);
911  return;
912 
913 } /* end of ConjunctsFree */
914 
915 
916 /**Function********************************************************************
917 
918  Synopsis [Check whether the given pair is in the tables.]
919 
920  Description [.Check whether the given pair is in the tables. gTable
921  and hTable are combined.
922  absence in both is indicated by 0,
923  presence in gTable is indicated by 1,
924  presence in hTable by 2 and
925  presence in both by 3.
926  The values returned by this function are PAIR_ST,
927  PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
928  PAIR_ST implies g in gTable and h in hTable
929  PAIR_CR implies g in hTable and h in gTable
930  G_ST implies g in gTable and h not in any table
931  G_CR implies g in hTable and h not in any table
932  H_ST implies h in hTable and g not in any table
933  H_CR implies h in gTable and g not in any table
934  BOTH_G implies both in gTable
935  BOTH_H implies both in hTable
936  NONE implies none in table; ]
937 
938  SideEffects []
939 
940  SeeAlso [CheckTablesCacheAndReturn CheckInTables]
941 
942 ******************************************************************************/
943 static int
944 PairInTables(
945  DdNode * g,
946  DdNode * h,
947  st__table * ghTable)
948 {
949  int valueG, valueH, gPresent, hPresent;
950 
951  valueG = valueH = gPresent = hPresent = 0;
952 
953  gPresent = st__lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
954  hPresent = st__lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
955 
956  if (!gPresent && !hPresent) return(NONE);
957 
958  if (!hPresent) {
959  if (valueG & 1) return(G_ST);
960  if (valueG & 2) return(G_CR);
961  }
962  if (!gPresent) {
963  if (valueH & 1) return(H_CR);
964  if (valueH & 2) return(H_ST);
965  }
966  /* both in tables */
967  if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
968  if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
969 
970  if (valueG & 1) {
971  return(BOTH_G);
972  } else {
973  return(BOTH_H);
974  }
975 
976 } /* end of PairInTables */
977 
978 
979 /**Function********************************************************************
980 
981  Synopsis [Check the tables for the existence of pair and return one
982  combination, cache the result.]
983 
984  Description [Check the tables for the existence of pair and return
985  one combination, cache the result. The assumption is that one of the
986  conjuncts is already in the tables.]
987 
988  SideEffects [g and h referenced for the cache]
989 
990  SeeAlso [ZeroCase]
991 
992 ******************************************************************************/
993 static Conjuncts *
994 CheckTablesCacheAndReturn(
995  DdNode * node,
996  DdNode * g,
997  DdNode * h,
998  st__table * ghTable,
999  st__table * cacheTable)
1000 {
1001  int pairValue;
1002  int value;
1003  Conjuncts *factors;
1004 
1005  value = 0;
1006  /* check tables */
1007  pairValue = PairInTables(g, h, ghTable);
1008  assert(pairValue != NONE);
1009  /* if both dont exist in table, we know one exists(either g or h).
1010  * Therefore store the other and proceed
1011  */
1012  factors = ABC_ALLOC(Conjuncts, 1);
1013  if (factors == NULL) return(NULL);
1014  if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
1015  if (g != one) {
1016  value = 0;
1017  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
1018  value |= 1;
1019  } else {
1020  value = 1;
1021  }
1022  if ( st__insert(ghTable, (char *)Cudd_Regular(g),
1023  (char *)(long)value) == st__OUT_OF_MEM) {
1024  return(NULL);
1025  }
1026  }
1027  factors->g = g;
1028  factors->h = h;
1029  } else if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
1030  if (h != one) {
1031  value = 0;
1032  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
1033  value |= 2;
1034  } else {
1035  value = 2;
1036  }
1037  if ( st__insert(ghTable, (char *)Cudd_Regular(h),
1038  (char *)(long)value) == st__OUT_OF_MEM) {
1039  return(NULL);
1040  }
1041  }
1042  factors->g = g;
1043  factors->h = h;
1044  } else if (pairValue == H_CR) {
1045  if (g != one) {
1046  value = 2;
1047  if ( st__insert(ghTable, (char *)Cudd_Regular(g),
1048  (char *)(long)value) == st__OUT_OF_MEM) {
1049  return(NULL);
1050  }
1051  }
1052  factors->g = h;
1053  factors->h = g;
1054  } else if (pairValue == G_CR) {
1055  if (h != one) {
1056  value = 1;
1057  if ( st__insert(ghTable, (char *)Cudd_Regular(h),
1058  (char *)(long)value) == st__OUT_OF_MEM) {
1059  return(NULL);
1060  }
1061  }
1062  factors->g = h;
1063  factors->h = g;
1064  } else if (pairValue == PAIR_CR) {
1065  /* pair exists in table */
1066  factors->g = h;
1067  factors->h = g;
1068  } else if (pairValue == PAIR_ST) {
1069  factors->g = g;
1070  factors->h = h;
1071  }
1072 
1073  /* cache the result for this node */
1074  if ( st__insert(cacheTable, (char *)node, (char *)factors) == st__OUT_OF_MEM) {
1075  ABC_FREE(factors);
1076  return(NULL);
1077  }
1078 
1079  return(factors);
1080 
1081 } /* end of CheckTablesCacheAndReturn */
1082 
1083 /**Function********************************************************************
1084 
1085  Synopsis [Check the tables for the existence of pair and return one
1086  combination, store in cache.]
1087 
1088  Description [Check the tables for the existence of pair and return
1089  one combination, store in cache. The pair that has more pointers to
1090  it is picked. An approximation of the number of local pointers is
1091  made by taking the reference count of the pairs sent. ]
1092 
1093  SideEffects []
1094 
1095  SeeAlso [ZeroCase BuildConjuncts]
1096 
1097 ******************************************************************************/
1098 static Conjuncts *
1099 PickOnePair(
1100  DdNode * node,
1101  DdNode * g1,
1102  DdNode * h1,
1103  DdNode * g2,
1104  DdNode * h2,
1105  st__table * ghTable,
1106  st__table * cacheTable)
1107 {
1108  int value;
1109  Conjuncts *factors;
1110  int oneRef, twoRef;
1111 
1112  factors = ABC_ALLOC(Conjuncts, 1);
1113  if (factors == NULL) return(NULL);
1114 
1115  /* count the number of pointers to pair 2 */
1116  if (h2 == one) {
1117  twoRef = (Cudd_Regular(g2))->ref;
1118  } else if (g2 == one) {
1119  twoRef = (Cudd_Regular(h2))->ref;
1120  } else {
1121  twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
1122  }
1123 
1124  /* count the number of pointers to pair 1 */
1125  if (h1 == one) {
1126  oneRef = (Cudd_Regular(g1))->ref;
1127  } else if (g1 == one) {
1128  oneRef = (Cudd_Regular(h1))->ref;
1129  } else {
1130  oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
1131  }
1132 
1133  /* pick the pair with higher reference count */
1134  if (oneRef >= twoRef) {
1135  factors->g = g1;
1136  factors->h = h1;
1137  } else {
1138  factors->g = g2;
1139  factors->h = h2;
1140  }
1141 
1142  /*
1143  * Store computed factors in respective tables to encourage
1144  * recombination.
1145  */
1146  if (factors->g != one) {
1147  /* insert g in htable */
1148  value = 0;
1149  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
1150  if (value == 2) {
1151  value |= 1;
1152  if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g),
1153  (char *)(long)value) == st__OUT_OF_MEM) {
1154  ABC_FREE(factors);
1155  return(NULL);
1156  }
1157  }
1158  } else {
1159  value = 1;
1160  if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g),
1161  (char *)(long)value) == st__OUT_OF_MEM) {
1162  ABC_FREE(factors);
1163  return(NULL);
1164  }
1165  }
1166  }
1167 
1168  if (factors->h != one) {
1169  /* insert h in htable */
1170  value = 0;
1171  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
1172  if (value == 1) {
1173  value |= 2;
1174  if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h),
1175  (char *)(long)value) == st__OUT_OF_MEM) {
1176  ABC_FREE(factors);
1177  return(NULL);
1178  }
1179  }
1180  } else {
1181  value = 2;
1182  if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h),
1183  (char *)(long)value) == st__OUT_OF_MEM) {
1184  ABC_FREE(factors);
1185  return(NULL);
1186  }
1187  }
1188  }
1189 
1190  /* Store factors in cache table for later use. */
1191  if ( st__insert(cacheTable, (char *)node, (char *)factors) ==
1192  st__OUT_OF_MEM) {
1193  ABC_FREE(factors);
1194  return(NULL);
1195  }
1196 
1197  return(factors);
1198 
1199 } /* end of PickOnePair */
1200 
1201 
1202 /**Function********************************************************************
1203 
1204  Synopsis [Check if the two pairs exist in the table, If any of the
1205  conjuncts do exist, store in the cache and return the corresponding pair.]
1206 
1207  Description [Check if the two pairs exist in the table. If any of
1208  the conjuncts do exist, store in the cache and return the
1209  corresponding pair.]
1210 
1211  SideEffects []
1212 
1213  SeeAlso [ZeroCase BuildConjuncts]
1214 
1215 ******************************************************************************/
1216 static Conjuncts *
1217 CheckInTables(
1218  DdNode * node,
1219  DdNode * g1,
1220  DdNode * h1,
1221  DdNode * g2,
1222  DdNode * h2,
1223  st__table * ghTable,
1224  st__table * cacheTable,
1225  int * outOfMem)
1226 {
1227  int pairValue1, pairValue2;
1228  Conjuncts *factors;
1229  int value;
1230 
1231  *outOfMem = 0;
1232 
1233  /* check existence of pair in table */
1234  pairValue1 = PairInTables(g1, h1, ghTable);
1235  pairValue2 = PairInTables(g2, h2, ghTable);
1236 
1237  /* if none of the 4 exist in the gh tables, return NULL */
1238  if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
1239  return NULL;
1240  }
1241 
1242  factors = ABC_ALLOC(Conjuncts, 1);
1243  if (factors == NULL) {
1244  *outOfMem = 1;
1245  return NULL;
1246  }
1247 
1248  /* pairs that already exist in the table get preference. */
1249  if (pairValue1 == PAIR_ST) {
1250  factors->g = g1;
1251  factors->h = h1;
1252  } else if (pairValue2 == PAIR_ST) {
1253  factors->g = g2;
1254  factors->h = h2;
1255  } else if (pairValue1 == PAIR_CR) {
1256  factors->g = h1;
1257  factors->h = g1;
1258  } else if (pairValue2 == PAIR_CR) {
1259  factors->g = h2;
1260  factors->h = g2;
1261  } else if (pairValue1 == G_ST) {
1262  /* g exists in the table, h is not found in either table */
1263  factors->g = g1;
1264  factors->h = h1;
1265  if (h1 != one) {
1266  value = 2;
1267  if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
1268  (char *)(long)value) == st__OUT_OF_MEM) {
1269  *outOfMem = 1;
1270  ABC_FREE(factors);
1271  return(NULL);
1272  }
1273  }
1274  } else if (pairValue1 == BOTH_G) {
1275  /* g and h are found in the g table */
1276  factors->g = g1;
1277  factors->h = h1;
1278  if (h1 != one) {
1279  value = 3;
1280  if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
1281  (char *)(long)value) == st__OUT_OF_MEM) {
1282  *outOfMem = 1;
1283  ABC_FREE(factors);
1284  return(NULL);
1285  }
1286  }
1287  } else if (pairValue1 == H_ST) {
1288  /* h exists in the table, g is not found in either table */
1289  factors->g = g1;
1290  factors->h = h1;
1291  if (g1 != one) {
1292  value = 1;
1293  if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
1294  (char *)(long)value) == st__OUT_OF_MEM) {
1295  *outOfMem = 1;
1296  ABC_FREE(factors);
1297  return(NULL);
1298  }
1299  }
1300  } else if (pairValue1 == BOTH_H) {
1301  /* g and h are found in the h table */
1302  factors->g = g1;
1303  factors->h = h1;
1304  if (g1 != one) {
1305  value = 3;
1306  if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
1307  (char *)(long)value) == st__OUT_OF_MEM) {
1308  *outOfMem = 1;
1309  ABC_FREE(factors);
1310  return(NULL);
1311  }
1312  }
1313  } else if (pairValue2 == G_ST) {
1314  /* g exists in the table, h is not found in either table */
1315  factors->g = g2;
1316  factors->h = h2;
1317  if (h2 != one) {
1318  value = 2;
1319  if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
1320  (char *)(long)value) == st__OUT_OF_MEM) {
1321  *outOfMem = 1;
1322  ABC_FREE(factors);
1323  return(NULL);
1324  }
1325  }
1326  } else if (pairValue2 == BOTH_G) {
1327  /* g and h are found in the g table */
1328  factors->g = g2;
1329  factors->h = h2;
1330  if (h2 != one) {
1331  value = 3;
1332  if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
1333  (char *)(long)value) == st__OUT_OF_MEM) {
1334  *outOfMem = 1;
1335  ABC_FREE(factors);
1336  return(NULL);
1337  }
1338  }
1339  } else if (pairValue2 == H_ST) {
1340  /* h exists in the table, g is not found in either table */
1341  factors->g = g2;
1342  factors->h = h2;
1343  if (g2 != one) {
1344  value = 1;
1345  if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
1346  (char *)(long)value) == st__OUT_OF_MEM) {
1347  *outOfMem = 1;
1348  ABC_FREE(factors);
1349  return(NULL);
1350  }
1351  }
1352  } else if (pairValue2 == BOTH_H) {
1353  /* g and h are found in the h table */
1354  factors->g = g2;
1355  factors->h = h2;
1356  if (g2 != one) {
1357  value = 3;
1358  if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
1359  (char *)(long)value) == st__OUT_OF_MEM) {
1360  *outOfMem = 1;
1361  ABC_FREE(factors);
1362  return(NULL);
1363  }
1364  }
1365  } else if (pairValue1 == G_CR) {
1366  /* g found in h table and h in none */
1367  factors->g = h1;
1368  factors->h = g1;
1369  if (h1 != one) {
1370  value = 1;
1371  if ( st__insert(ghTable, (char *)Cudd_Regular(h1),
1372  (char *)(long)value) == st__OUT_OF_MEM) {
1373  *outOfMem = 1;
1374  ABC_FREE(factors);
1375  return(NULL);
1376  }
1377  }
1378  } else if (pairValue1 == H_CR) {
1379  /* h found in g table and g in none */
1380  factors->g = h1;
1381  factors->h = g1;
1382  if (g1 != one) {
1383  value = 2;
1384  if ( st__insert(ghTable, (char *)Cudd_Regular(g1),
1385  (char *)(long)value) == st__OUT_OF_MEM) {
1386  *outOfMem = 1;
1387  ABC_FREE(factors);
1388  return(NULL);
1389  }
1390  }
1391  } else if (pairValue2 == G_CR) {
1392  /* g found in h table and h in none */
1393  factors->g = h2;
1394  factors->h = g2;
1395  if (h2 != one) {
1396  value = 1;
1397  if ( st__insert(ghTable, (char *)Cudd_Regular(h2),
1398  (char *)(long)value) == st__OUT_OF_MEM) {
1399  *outOfMem = 1;
1400  ABC_FREE(factors);
1401  return(NULL);
1402  }
1403  }
1404  } else if (pairValue2 == H_CR) {
1405  /* h found in g table and g in none */
1406  factors->g = h2;
1407  factors->h = g2;
1408  if (g2 != one) {
1409  value = 2;
1410  if ( st__insert(ghTable, (char *)Cudd_Regular(g2),
1411  (char *)(long)value) == st__OUT_OF_MEM) {
1412  *outOfMem = 1;
1413  ABC_FREE(factors);
1414  return(NULL);
1415  }
1416  }
1417  }
1418 
1419  /* Store factors in cache table for later use. */
1420  if ( st__insert(cacheTable, (char *)node, (char *)factors) ==
1421  st__OUT_OF_MEM) {
1422  *outOfMem = 1;
1423  ABC_FREE(factors);
1424  return(NULL);
1425  }
1426  return factors;
1427 } /* end of CheckInTables */
1428 
1429 
1430 
1431 /**Function********************************************************************
1432 
1433  Synopsis [If one child is zero, do explicitly what Restrict does or better]
1434 
1435  Description [If one child is zero, do explicitly what Restrict does or better.
1436  First separate a variable and its child in the base case. In case of a cube
1437  times a function, separate the cube and function. As a last resort, look in
1438  tables.]
1439 
1440  SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed
1441  because it is freed above.]
1442 
1443  SeeAlso [BuildConjuncts]
1444 
1445 ******************************************************************************/
1446 static Conjuncts *
1447 ZeroCase(
1448  DdManager * dd,
1449  DdNode * node,
1450  Conjuncts * factorsNv,
1451  st__table * ghTable,
1452  st__table * cacheTable,
1453  int switched)
1454 {
1455  int topid;
1456  DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv;
1457  DdNode *Hv, *Hnv;
1458  int value;
1459  int outOfMem;
1460  Conjuncts *factors;
1461 
1462  /* get var at this node */
1463  N = Cudd_Regular(node);
1464  topid = N->index;
1465  x = dd->vars[topid];
1466  x = (switched) ? Cudd_Not(x): x;
1467  cuddRef(x);
1468 
1469  /* Seprate variable and child */
1470  if (factorsNv->g == one) {
1471  Cudd_RecursiveDeref(dd, factorsNv->g);
1472  factors = ABC_ALLOC(Conjuncts, 1);
1473  if (factors == NULL) {
1474  dd->errorCode = CUDD_MEMORY_OUT;
1475  Cudd_RecursiveDeref(dd, factorsNv->h);
1476  Cudd_RecursiveDeref(dd, x);
1477  return(NULL);
1478  }
1479  factors->g = x;
1480  factors->h = factorsNv->h;
1481  /* cache the result*/
1482  if ( st__insert(cacheTable, (char *)node, (char *)factors) == st__OUT_OF_MEM) {
1483  dd->errorCode = CUDD_MEMORY_OUT;
1484  Cudd_RecursiveDeref(dd, factorsNv->h);
1485  Cudd_RecursiveDeref(dd, x);
1486  ABC_FREE(factors);
1487  return NULL;
1488  }
1489 
1490  /* store x in g table, the other node is already in the table */
1491  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1492  value |= 1;
1493  } else {
1494  value = 1;
1495  }
1496  if ( st__insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == st__OUT_OF_MEM) {
1497  dd->errorCode = CUDD_MEMORY_OUT;
1498  return NULL;
1499  }
1500  return(factors);
1501  }
1502 
1503  /* Seprate variable and child */
1504  if (factorsNv->h == one) {
1505  Cudd_RecursiveDeref(dd, factorsNv->h);
1506  factors = ABC_ALLOC(Conjuncts, 1);
1507  if (factors == NULL) {
1508  dd->errorCode = CUDD_MEMORY_OUT;
1509  Cudd_RecursiveDeref(dd, factorsNv->g);
1510  Cudd_RecursiveDeref(dd, x);
1511  return(NULL);
1512  }
1513  factors->g = factorsNv->g;
1514  factors->h = x;
1515  /* cache the result. */
1516  if ( st__insert(cacheTable, (char *)node, (char *)factors) == st__OUT_OF_MEM) {
1517  dd->errorCode = CUDD_MEMORY_OUT;
1518  Cudd_RecursiveDeref(dd, factorsNv->g);
1519  Cudd_RecursiveDeref(dd, x);
1520  ABC_FREE(factors);
1521  return(NULL);
1522  }
1523  /* store x in h table, the other node is already in the table */
1524  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1525  value |= 2;
1526  } else {
1527  value = 2;
1528  }
1529  if ( st__insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == st__OUT_OF_MEM) {
1530  dd->errorCode = CUDD_MEMORY_OUT;
1531  return NULL;
1532  }
1533  return(factors);
1534  }
1535 
1536  G = Cudd_Regular(factorsNv->g);
1537  Gv = cuddT(G);
1538  Gnv = cuddE(G);
1539  Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node));
1540  Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
1541  /* if the child below is a variable */
1542  if ((Gv == zero) || (Gnv == zero)) {
1543  h = factorsNv->h;
1544  g = cuddBddAndRecur(dd, x, factorsNv->g);
1545  if (g != NULL) cuddRef(g);
1546  Cudd_RecursiveDeref(dd, factorsNv->g);
1547  Cudd_RecursiveDeref(dd, x);
1548  if (g == NULL) {
1549  Cudd_RecursiveDeref(dd, factorsNv->h);
1550  return NULL;
1551  }
1552  /* CheckTablesCacheAndReturn responsible for allocating
1553  * factors structure., g,h referenced for cache store the
1554  */
1555  factors = CheckTablesCacheAndReturn(node,
1556  g,
1557  h,
1558  ghTable,
1559  cacheTable);
1560  if (factors == NULL) {
1561  dd->errorCode = CUDD_MEMORY_OUT;
1562  Cudd_RecursiveDeref(dd, g);
1563  Cudd_RecursiveDeref(dd, h);
1564  }
1565  return(factors);
1566  }
1567 
1568  H = Cudd_Regular(factorsNv->h);
1569  Hv = cuddT(H);
1570  Hnv = cuddE(H);
1571  Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node));
1572  Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
1573  /* if the child below is a variable */
1574  if ((Hv == zero) || (Hnv == zero)) {
1575  g = factorsNv->g;
1576  h = cuddBddAndRecur(dd, x, factorsNv->h);
1577  if (h!= NULL) cuddRef(h);
1578  Cudd_RecursiveDeref(dd, factorsNv->h);
1579  Cudd_RecursiveDeref(dd, x);
1580  if (h == NULL) {
1581  Cudd_RecursiveDeref(dd, factorsNv->g);
1582  return NULL;
1583  }
1584  /* CheckTablesCacheAndReturn responsible for allocating
1585  * factors structure.g,h referenced for table store
1586  */
1587  factors = CheckTablesCacheAndReturn(node,
1588  g,
1589  h,
1590  ghTable,
1591  cacheTable);
1592  if (factors == NULL) {
1593  dd->errorCode = CUDD_MEMORY_OUT;
1594  Cudd_RecursiveDeref(dd, g);
1595  Cudd_RecursiveDeref(dd, h);
1596  }
1597  return(factors);
1598  }
1599 
1600  /* build g1 = x*g; h1 = h */
1601  /* build g2 = g; h2 = x*h */
1602  Cudd_RecursiveDeref(dd, x);
1603  h1 = factorsNv->h;
1604  g1 = cuddBddAndRecur(dd, x, factorsNv->g);
1605  if (g1 != NULL) cuddRef(g1);
1606  if (g1 == NULL) {
1607  Cudd_RecursiveDeref(dd, factorsNv->g);
1608  Cudd_RecursiveDeref(dd, factorsNv->h);
1609  return NULL;
1610  }
1611 
1612  g2 = factorsNv->g;
1613  h2 = cuddBddAndRecur(dd, x, factorsNv->h);
1614  if (h2 != NULL) cuddRef(h2);
1615  if (h2 == NULL) {
1616  Cudd_RecursiveDeref(dd, factorsNv->h);
1617  Cudd_RecursiveDeref(dd, factorsNv->g);
1618  return NULL;
1619  }
1620 
1621  /* check whether any pair is in tables */
1622  factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1623  if (outOfMem) {
1624  dd->errorCode = CUDD_MEMORY_OUT;
1625  Cudd_RecursiveDeref(dd, g1);
1626  Cudd_RecursiveDeref(dd, h1);
1627  Cudd_RecursiveDeref(dd, g2);
1628  Cudd_RecursiveDeref(dd, h2);
1629  return NULL;
1630  }
1631  if (factors != NULL) {
1632  if ((factors->g == g1) || (factors->g == h1)) {
1633  Cudd_RecursiveDeref(dd, g2);
1634  Cudd_RecursiveDeref(dd, h2);
1635  } else {
1636  Cudd_RecursiveDeref(dd, g1);
1637  Cudd_RecursiveDeref(dd, h1);
1638  }
1639  return factors;
1640  }
1641 
1642  /* check for each pair in tables and choose one */
1643  factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1644  if (factors == NULL) {
1645  dd->errorCode = CUDD_MEMORY_OUT;
1646  Cudd_RecursiveDeref(dd, g1);
1647  Cudd_RecursiveDeref(dd, h1);
1648  Cudd_RecursiveDeref(dd, g2);
1649  Cudd_RecursiveDeref(dd, h2);
1650  } else {
1651  /* now free what was created and not used */
1652  if ((factors->g == g1) || (factors->g == h1)) {
1653  Cudd_RecursiveDeref(dd, g2);
1654  Cudd_RecursiveDeref(dd, h2);
1655  } else {
1656  Cudd_RecursiveDeref(dd, g1);
1657  Cudd_RecursiveDeref(dd, h1);
1658  }
1659  }
1660 
1661  return(factors);
1662 } /* end of ZeroCase */
1663 
1664 
1665 /**Function********************************************************************
1666 
1667  Synopsis [Builds the conjuncts recursively, bottom up.]
1668 
1669  Description [Builds the conjuncts recursively, bottom up. Constants
1670  are returned as (f, f). The cache is checked for previously computed
1671  result. The decomposition points are determined by the local
1672  reference count of this node and the longest distance from the
1673  constant. At the decomposition point, the factors returned are (f,
1674  1). Recur on the two children. The order is determined by the
1675  heavier branch. Combine the factors of the two children and pick the
1676  one that already occurs in the gh table. Occurence in g is indicated
1677  by value 1, occurence in h by 2, occurence in both 3.]
1678 
1679  SideEffects []
1680 
1681  SeeAlso [cuddConjunctsAux]
1682 
1683 ******************************************************************************/
1684 static Conjuncts *
1685 BuildConjuncts(
1686  DdManager * dd,
1687  DdNode * node,
1688  st__table * distanceTable,
1689  st__table * cacheTable,
1690  int approxDistance,
1691  int maxLocalRef,
1692  st__table * ghTable,
1693  st__table * mintermTable)
1694 {
1695  int topid, distance;
1696  Conjuncts *factorsNv = NULL, *factorsNnv = NULL, *factors;
1697  Conjuncts *dummy;
1698  DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
1699  double minNv = 0.0, minNnv = 0.0;
1700  double *doubleDummy;
1701  int switched =0;
1702  int outOfMem;
1703  int freeNv = 0, freeNnv = 0, freeTemp;
1704  NodeStat *nodeStat;
1705  int value;
1706 
1707  /* if f is constant, return (f,f) */
1708  if (Cudd_IsConstant(node)) {
1709  factors = ABC_ALLOC(Conjuncts, 1);
1710  if (factors == NULL) {
1711  dd->errorCode = CUDD_MEMORY_OUT;
1712  return(NULL);
1713  }
1714  factors->g = node;
1715  factors->h = node;
1716  return(FactorsComplement(factors));
1717  }
1718 
1719  /* If result (a pair of conjuncts) in cache, return the factors. */
1720  if ( st__lookup(cacheTable, (const char *)node, (char **)&dummy)) {
1721  factors = dummy;
1722  return(factors);
1723  }
1724 
1725  /* check distance and local reference count of this node */
1726  N = Cudd_Regular(node);
1727  if (! st__lookup(distanceTable, (const char *)N, (char **)&nodeStat)) {
1728  (void) fprintf(dd->err, "Not in table, Something wrong\n");
1729  dd->errorCode = CUDD_INTERNAL_ERROR;
1730  return(NULL);
1731  }
1732  distance = nodeStat->distance;
1733 
1734  /* at or below decomposition point, return (f, 1) */
1735  if (((nodeStat->localRef > maxLocalRef*2/3) &&
1736  (distance < approxDistance*2/3)) ||
1737  (distance <= approxDistance/4)) {
1738  factors = ABC_ALLOC(Conjuncts, 1);
1739  if (factors == NULL) {
1740  dd->errorCode = CUDD_MEMORY_OUT;
1741  return(NULL);
1742  }
1743  /* alternate assigning (f,1) */
1744  value = 0;
1745  if ( st__lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
1746  if (value == 3) {
1747  if (!lastTimeG) {
1748  factors->g = node;
1749  factors->h = one;
1750  lastTimeG = 1;
1751  } else {
1752  factors->g = one;
1753  factors->h = node;
1754  lastTimeG = 0;
1755  }
1756  } else if (value == 1) {
1757  factors->g = node;
1758  factors->h = one;
1759  } else {
1760  factors->g = one;
1761  factors->h = node;
1762  }
1763  } else if (!lastTimeG) {
1764  factors->g = node;
1765  factors->h = one;
1766  lastTimeG = 1;
1767  value = 1;
1768  if ( st__insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == st__OUT_OF_MEM) {
1769  dd->errorCode = CUDD_MEMORY_OUT;
1770  ABC_FREE(factors);
1771  return NULL;
1772  }
1773  } else {
1774  factors->g = one;
1775  factors->h = node;
1776  lastTimeG = 0;
1777  value = 2;
1778  if ( st__insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == st__OUT_OF_MEM) {
1779  dd->errorCode = CUDD_MEMORY_OUT;
1780  ABC_FREE(factors);
1781  return NULL;
1782  }
1783  }
1784  return(FactorsComplement(factors));
1785  }
1786 
1787  /* get the children and recur */
1788  Nv = cuddT(N);
1789  Nnv = cuddE(N);
1790  Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1791  Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1792 
1793  /* Choose which subproblem to solve first based on the number of
1794  * minterms. We go first where there are more minterms.
1795  */
1796  if (!Cudd_IsConstant(Nv)) {
1797  if (! st__lookup(mintermTable, (const char *)Nv, (char **)&doubleDummy)) {
1798  (void) fprintf(dd->err, "Not in table: Something wrong\n");
1799  dd->errorCode = CUDD_INTERNAL_ERROR;
1800  return(NULL);
1801  }
1802  minNv = *doubleDummy;
1803  }
1804 
1805  if (!Cudd_IsConstant(Nnv)) {
1806  if (! st__lookup(mintermTable, (const char *)Nnv, (char **)&doubleDummy)) {
1807  (void) fprintf(dd->err, "Not in table: Something wrong\n");
1808  dd->errorCode = CUDD_INTERNAL_ERROR;
1809  return(NULL);
1810  }
1811  minNnv = *doubleDummy;
1812  }
1813 
1814  if (minNv < minNnv) {
1815  temp = Nv;
1816  Nv = Nnv;
1817  Nnv = temp;
1818  switched = 1;
1819  }
1820 
1821  /* build gt, ht recursively */
1822  if (Nv != zero) {
1823  factorsNv = BuildConjuncts(dd, Nv, distanceTable,
1824  cacheTable, approxDistance, maxLocalRef,
1825  ghTable, mintermTable);
1826  if (factorsNv == NULL) return(NULL);
1827  freeNv = FactorsNotStored(factorsNv);
1828  factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
1829  cuddRef(factorsNv->g);
1830  cuddRef(factorsNv->h);
1831 
1832  /* Deal with the zero case */
1833  if (Nnv == zero) {
1834  /* is responsible for freeing factorsNv */
1835  factors = ZeroCase(dd, node, factorsNv, ghTable,
1836  cacheTable, switched);
1837  if (freeNv) ABC_FREE(factorsNv);
1838  return(factors);
1839  }
1840  }
1841 
1842  /* build ge, he recursively */
1843  if (Nnv != zero) {
1844  factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
1845  cacheTable, approxDistance, maxLocalRef,
1846  ghTable, mintermTable);
1847  if (factorsNnv == NULL) {
1848  Cudd_RecursiveDeref(dd, factorsNv->g);
1849  Cudd_RecursiveDeref(dd, factorsNv->h);
1850  if (freeNv) ABC_FREE(factorsNv);
1851  return(NULL);
1852  }
1853  freeNnv = FactorsNotStored(factorsNnv);
1854  factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
1855  cuddRef(factorsNnv->g);
1856  cuddRef(factorsNnv->h);
1857 
1858  /* Deal with the zero case */
1859  if (Nv == zero) {
1860  /* is responsible for freeing factorsNv */
1861  factors = ZeroCase(dd, node, factorsNnv, ghTable,
1862  cacheTable, switched);
1863  if (freeNnv) ABC_FREE(factorsNnv);
1864  return(factors);
1865  }
1866  }
1867 
1868  /* construct the 2 pairs */
1869  /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
1870  /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
1871  if (switched) {
1872  factors = factorsNnv;
1873  factorsNnv = factorsNv;
1874  factorsNv = factors;
1875  freeTemp = freeNv;
1876  freeNv = freeNnv;
1877  freeNnv = freeTemp;
1878  }
1879 
1880  /* Build the factors for this node. */
1881  topid = N->index;
1882  topv = dd->vars[topid];
1883 
1884  g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
1885  if (g1 == NULL) {
1886  Cudd_RecursiveDeref(dd, factorsNv->g);
1887  Cudd_RecursiveDeref(dd, factorsNv->h);
1888  Cudd_RecursiveDeref(dd, factorsNnv->g);
1889  Cudd_RecursiveDeref(dd, factorsNnv->h);
1890  if (freeNv) ABC_FREE(factorsNv);
1891  if (freeNnv) ABC_FREE(factorsNnv);
1892  return(NULL);
1893  }
1894 
1895  cuddRef(g1);
1896 
1897  h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
1898  if (h1 == NULL) {
1899  Cudd_RecursiveDeref(dd, factorsNv->g);
1900  Cudd_RecursiveDeref(dd, factorsNv->h);
1901  Cudd_RecursiveDeref(dd, factorsNnv->g);
1902  Cudd_RecursiveDeref(dd, factorsNnv->h);
1903  Cudd_RecursiveDeref(dd, g1);
1904  if (freeNv) ABC_FREE(factorsNv);
1905  if (freeNnv) ABC_FREE(factorsNnv);
1906  return(NULL);
1907  }
1908 
1909  cuddRef(h1);
1910 
1911  g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
1912  if (g2 == NULL) {
1913  Cudd_RecursiveDeref(dd, factorsNv->h);
1914  Cudd_RecursiveDeref(dd, factorsNv->g);
1915  Cudd_RecursiveDeref(dd, factorsNnv->g);
1916  Cudd_RecursiveDeref(dd, factorsNnv->h);
1917  Cudd_RecursiveDeref(dd, g1);
1918  Cudd_RecursiveDeref(dd, h1);
1919  if (freeNv) ABC_FREE(factorsNv);
1920  if (freeNnv) ABC_FREE(factorsNnv);
1921  return(NULL);
1922  }
1923  cuddRef(g2);
1924  Cudd_RecursiveDeref(dd, factorsNv->g);
1925  Cudd_RecursiveDeref(dd, factorsNnv->h);
1926 
1927  h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
1928  if (h2 == NULL) {
1929  Cudd_RecursiveDeref(dd, factorsNv->g);
1930  Cudd_RecursiveDeref(dd, factorsNv->h);
1931  Cudd_RecursiveDeref(dd, factorsNnv->g);
1932  Cudd_RecursiveDeref(dd, factorsNnv->h);
1933  Cudd_RecursiveDeref(dd, g1);
1934  Cudd_RecursiveDeref(dd, h1);
1935  Cudd_RecursiveDeref(dd, g2);
1936  if (freeNv) ABC_FREE(factorsNv);
1937  if (freeNnv) ABC_FREE(factorsNnv);
1938  return(NULL);
1939  }
1940  cuddRef(h2);
1941  Cudd_RecursiveDeref(dd, factorsNv->h);
1942  Cudd_RecursiveDeref(dd, factorsNnv->g);
1943  if (freeNv) ABC_FREE(factorsNv);
1944  if (freeNnv) ABC_FREE(factorsNnv);
1945 
1946  /* check for each pair in tables and choose one */
1947  factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1948  if (outOfMem) {
1949  dd->errorCode = CUDD_MEMORY_OUT;
1950  Cudd_RecursiveDeref(dd, g1);
1951  Cudd_RecursiveDeref(dd, h1);
1952  Cudd_RecursiveDeref(dd, g2);
1953  Cudd_RecursiveDeref(dd, h2);
1954  return(NULL);
1955  }
1956  if (factors != NULL) {
1957  if ((factors->g == g1) || (factors->g == h1)) {
1958  Cudd_RecursiveDeref(dd, g2);
1959  Cudd_RecursiveDeref(dd, h2);
1960  } else {
1961  Cudd_RecursiveDeref(dd, g1);
1962  Cudd_RecursiveDeref(dd, h1);
1963  }
1964  return(factors);
1965  }
1966 
1967  /* if not in tables, pick one pair */
1968  factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1969  if (factors == NULL) {
1970  dd->errorCode = CUDD_MEMORY_OUT;
1971  Cudd_RecursiveDeref(dd, g1);
1972  Cudd_RecursiveDeref(dd, h1);
1973  Cudd_RecursiveDeref(dd, g2);
1974  Cudd_RecursiveDeref(dd, h2);
1975  } else {
1976  /* now free what was created and not used */
1977  if ((factors->g == g1) || (factors->g == h1)) {
1978  Cudd_RecursiveDeref(dd, g2);
1979  Cudd_RecursiveDeref(dd, h2);
1980  } else {
1981  Cudd_RecursiveDeref(dd, g1);
1982  Cudd_RecursiveDeref(dd, h1);
1983  }
1984  }
1985 
1986  return(factors);
1987 
1988 } /* end of BuildConjuncts */
1989 
1990 
1991 /**Function********************************************************************
1992 
1993  Synopsis [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]
1994 
1995  Description [Procedure to compute two conjunctive factors of f and
1996  place in *c1 and *c2. Sets up the required data - table of distances
1997  from the constant and local reference count. Also minterm table. ]
1998 
1999  SideEffects []
2000 
2001  SeeAlso []
2002 
2003 ******************************************************************************/
2004 static int
2005 cuddConjunctsAux(
2006  DdManager * dd,
2007  DdNode * f,
2008  DdNode ** c1,
2009  DdNode ** c2)
2010 {
2011  st__table *distanceTable = NULL;
2012  st__table *cacheTable = NULL;
2013  st__table *mintermTable = NULL;
2014  st__table *ghTable = NULL;
2015  st__generator *stGen;
2016  char *key, *value;
2017  Conjuncts *factors;
2018  int distance, approxDistance;
2019  double max, minterms;
2020  int freeFactors;
2021  NodeStat *nodeStat;
2022  int maxLocalRef;
2023 
2024  /* initialize */
2025  *c1 = NULL;
2026  *c2 = NULL;
2027 
2028  /* initialize distances table */
2029  distanceTable = st__init_table( st__ptrcmp, st__ptrhash);
2030  if (distanceTable == NULL) goto outOfMem;
2031 
2032  /* make the entry for the constant */
2033  nodeStat = ABC_ALLOC(NodeStat, 1);
2034  if (nodeStat == NULL) goto outOfMem;
2035  nodeStat->distance = 0;
2036  nodeStat->localRef = 1;
2037  if ( st__insert(distanceTable, (char *)one, (char *)nodeStat) == st__OUT_OF_MEM) {
2038  goto outOfMem;
2039  }
2040 
2041  /* Count node distances from constant. */
2042  nodeStat = CreateBotDist(f, distanceTable);
2043  if (nodeStat == NULL) goto outOfMem;
2044 
2045  /* set the distance for the decomposition points */
2046  approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH;
2047  distance = nodeStat->distance;
2048 
2049  if (distance < approxDistance) {
2050  /* Too small to bother. */
2051  *c1 = f;
2052  *c2 = DD_ONE(dd);
2053  cuddRef(*c1); cuddRef(*c2);
2054  stGen = st__init_gen(distanceTable);
2055  if (stGen == NULL) goto outOfMem;
2056  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2057  ABC_FREE(value);
2058  }
2059  st__free_gen(stGen); stGen = NULL;
2060  st__free_table(distanceTable);
2061  return(1);
2062  }
2063 
2064  /* record the maximum local reference count */
2065  maxLocalRef = 0;
2066  stGen = st__init_gen(distanceTable);
2067  if (stGen == NULL) goto outOfMem;
2068  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2069  nodeStat = (NodeStat *)value;
2070  maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
2071  nodeStat->localRef : maxLocalRef;
2072  }
2073  st__free_gen(stGen); stGen = NULL;
2074 
2075 
2076  /* Count minterms for each node. */
2077  max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
2078  mintermTable = st__init_table( st__ptrcmp, st__ptrhash);
2079  if (mintermTable == NULL) goto outOfMem;
2080  minterms = CountMinterms(f, max, mintermTable, dd->err);
2081  if (minterms == -1.0) goto outOfMem;
2082 
2083  lastTimeG = Cudd_Random() & 1;
2084  cacheTable = st__init_table( st__ptrcmp, st__ptrhash);
2085  if (cacheTable == NULL) goto outOfMem;
2086  ghTable = st__init_table( st__ptrcmp, st__ptrhash);
2087  if (ghTable == NULL) goto outOfMem;
2088 
2089  /* Build conjuncts. */
2090  factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
2091  approxDistance, maxLocalRef, ghTable, mintermTable);
2092  if (factors == NULL) goto outOfMem;
2093 
2094  /* free up tables */
2095  stGen = st__init_gen(distanceTable);
2096  if (stGen == NULL) goto outOfMem;
2097  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2098  ABC_FREE(value);
2099  }
2100  st__free_gen(stGen); stGen = NULL;
2101  st__free_table(distanceTable); distanceTable = NULL;
2102  st__free_table(ghTable); ghTable = NULL;
2103 
2104  stGen = st__init_gen(mintermTable);
2105  if (stGen == NULL) goto outOfMem;
2106  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2107  ABC_FREE(value);
2108  }
2109  st__free_gen(stGen); stGen = NULL;
2110  st__free_table(mintermTable); mintermTable = NULL;
2111 
2112  freeFactors = FactorsNotStored(factors);
2113  factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
2114  if (factors != NULL) {
2115  *c1 = factors->g;
2116  *c2 = factors->h;
2117  cuddRef(*c1);
2118  cuddRef(*c2);
2119  if (freeFactors) ABC_FREE(factors);
2120 
2121 #if 0
2122  if ((*c1 == f) && (!Cudd_IsConstant(f))) {
2123  assert(*c2 == one);
2124  }
2125  if ((*c2 == f) && (!Cudd_IsConstant(f))) {
2126  assert(*c1 == one);
2127  }
2128 
2129  if ((*c1 != one) && (!Cudd_IsConstant(f))) {
2130  assert(!Cudd_bddLeq(dd, *c2, *c1));
2131  }
2132  if ((*c2 != one) && (!Cudd_IsConstant(f))) {
2133  assert(!Cudd_bddLeq(dd, *c1, *c2));
2134  }
2135 #endif
2136  }
2137 
2138  stGen = st__init_gen(cacheTable);
2139  if (stGen == NULL) goto outOfMem;
2140  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2141  ConjunctsFree(dd, (Conjuncts *)value);
2142  }
2143  st__free_gen(stGen); stGen = NULL;
2144 
2145  st__free_table(cacheTable); cacheTable = NULL;
2146 
2147  return(1);
2148 
2149 outOfMem:
2150  if (distanceTable != NULL) {
2151  stGen = st__init_gen(distanceTable);
2152  if (stGen == NULL) goto outOfMem;
2153  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2154  ABC_FREE(value);
2155  }
2156  st__free_gen(stGen); stGen = NULL;
2157  st__free_table(distanceTable); distanceTable = NULL;
2158  }
2159  if (mintermTable != NULL) {
2160  stGen = st__init_gen(mintermTable);
2161  if (stGen == NULL) goto outOfMem;
2162  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2163  ABC_FREE(value);
2164  }
2165  st__free_gen(stGen); stGen = NULL;
2166  st__free_table(mintermTable); mintermTable = NULL;
2167  }
2168  if (ghTable != NULL) st__free_table(ghTable);
2169  if (cacheTable != NULL) {
2170  stGen = st__init_gen(cacheTable);
2171  if (stGen == NULL) goto outOfMem;
2172  while( st__gen(stGen, (const char **)&key, (char **)&value)) {
2173  ConjunctsFree(dd, (Conjuncts *)value);
2174  }
2175  st__free_gen(stGen); stGen = NULL;
2176  st__free_table(cacheTable); cacheTable = NULL;
2177  }
2178  dd->errorCode = CUDD_MEMORY_OUT;
2179  return(0);
2180 
2181 } /* end of cuddConjunctsAux */
2182 
2183 
2184 ABC_NAMESPACE_IMPL_END
2185 
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
PAIR_ST
#define PAIR_ST
Definition: cuddDecomp.c:77
G_CR
#define G_CR
Definition: cuddDecomp.c:80
Cudd_bddIterDisjDecomp
int Cudd_bddIterDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:456
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DEPTH
#define DEPTH
Definition: cuddDecomp.c:74
G_ST
#define G_ST
Definition: cuddDecomp.c:79
NodeStat::localRef
int localRef
Definition: cuddDecomp.c:100
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
st__free_gen
void st__free_gen(st__generator *gen)
Definition: st.c:556
H_CR
#define H_CR
Definition: cuddDecomp.c:82
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
DD_UNUSED
static char rcsid[] DD_UNUSED
Definition: cuddDecomp.c:109
NONE
#define NONE
Definition: cuddDecomp.c:76
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_RemapOverApprox
DdNode * Cudd_RemapOverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:366
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
Conjuncts::h
DdNode * h
Definition: cuddDecomp.c:95
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
DdManager::err
FILE * err
Definition: cuddInt.h:442
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
st__lookup_int
int st__lookup_int(st__table *table, char *key, int *value)
Definition: st.c:134
ConjunctsFree
static void ConjunctsFree(DdManager *dd, Conjuncts *factors)
Definition: cuddDecomp.c:904
H_ST
#define H_ST
Definition: cuddDecomp.c:81
Cudd_bddLICompaction
DdNode * Cudd_bddLICompaction(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:570
Cudd_bddGenDisjDecomp
int Cudd_bddGenDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:575
Conjuncts
struct Conjuncts Conjuncts
util_hack.h
BOTH_H
#define BOTH_H
Definition: cuddDecomp.c:84
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
CheckInTables
static Conjuncts * CheckInTables(DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st__table *ghTable, st__table *cacheTable, int *outOfMem)
Definition: cuddDecomp.c:1217
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Conjuncts::g
DdNode * g
Definition: cuddDecomp.c:94
PickOnePair
static Conjuncts * PickOnePair(DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st__table *ghTable, st__table *cacheTable)
Definition: cuddDecomp.c:1099
Cudd_Random
long Cudd_Random(void)
Definition: cuddUtil.c:2702
FactorsUncomplement
#define FactorsUncomplement(factors)
Definition: cuddDecomp.c:124
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
FactorsComplement
#define FactorsComplement(factors)
Definition: cuddDecomp.c:122
one
static DdNode * one
Definition: cuddDecomp.c:112
st__table
Definition: st.h:52
Cudd_bddVarConjDecomp
int Cudd_bddVarConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:615
BuildConjuncts
static Conjuncts * BuildConjuncts(DdManager *dd, DdNode *node, st__table *distanceTable, st__table *cacheTable, int approxDistance, int maxLocalRef, st__table *ghTable, st__table *mintermTable)
Definition: cuddDecomp.c:1685
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
if
if(last==0)
Definition: sparse_int.h:34
max
static double max
Definition: cuddSubsetHB.c:134
Cudd_bddApproxConjDecomp
int Cudd_bddApproxConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:175
BOTH_G
#define BOTH_G
Definition: cuddDecomp.c:83
size
static int size
Definition: cuddSign.c:86
CheckTablesCacheAndReturn
static Conjuncts * CheckTablesCacheAndReturn(DdNode *node, DdNode *g, DdNode *h, st__table *ghTable, st__table *cacheTable)
Definition: cuddDecomp.c:994
Cudd_bddApproxDisjDecomp
int Cudd_bddApproxDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:273
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__init_gen
st__generator * st__init_gen(st__table *table)
Definition: st.c:486
Cudd_EstimateCofactor
int Cudd_EstimateCofactor(DdManager *dd, DdNode *node, int i, int phase)
Definition: cuddUtil.c:477
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
PairInTables
static int PairInTables(DdNode *g, DdNode *h, st__table *ghTable)
Definition: cuddDecomp.c:944
PAIR_CR
#define PAIR_CR
Definition: cuddDecomp.c:78
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_bddVarDisjDecomp
int Cudd_bddVarDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:733
NodeStat
struct NodeStat NodeStat
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
CreateBotDist
static NodeStat * CreateBotDist(DdNode *node, st__table *distanceTable)
Definition: cuddDecomp.c:772
key
enum keys key
Definition: misc/espresso/main.h:25
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_bddIterConjDecomp
int Cudd_bddIterConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:313
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
NodeStat::distance
int distance
Definition: cuddDecomp.c:99
value
int value
Definition: misc/espresso/main.h:90
FactorsNotStored
#define FactorsNotStored(factors)
Definition: cuddDecomp.c:120
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_bddGenConjDecomp
int Cudd_bddGenConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:496
result
static int result
Definition: cuddGenetic.c:125
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
pyabc_split.best
best
Definition: pyabc_split.py:400
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
lastTimeG
long lastTimeG
Definition: cuddDecomp.c:113
cuddConjunctsAux
static int cuddConjunctsAux(DdManager *dd, DdNode *f, DdNode **c1, DdNode **c2)
Definition: cuddDecomp.c:2005
Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
minterms
pset minterms()
st__gen
int st__gen(st__generator *gen, const char **key_p, char **value_p)
Definition: st.c:502
st__generator
Definition: st.h:64
zero
static DdNode * zero
Definition: cuddDecomp.c:112
Cudd_bddSqueeze
DdNode * Cudd_bddSqueeze(DdManager *dd, DdNode *l, DdNode *u)
Definition: cuddGenCof.c:602
ZeroCase
static Conjuncts * ZeroCase(DdManager *dd, DdNode *node, Conjuncts *factorsNv, st__table *ghTable, st__table *cacheTable, int switched)
Definition: cuddDecomp.c:1447
CountMinterms
static double CountMinterms(DdNode *node, double max, st__table *mintermTable, FILE *fp)
Definition: cuddDecomp.c:841
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:633