abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddApprox.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddApprox.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Procedures to approximate a given BDD.]
8 
9  Description [External procedures provided by this module:
10  <ul>
11  <li> Cudd_UnderApprox()
12  <li> Cudd_OverApprox()
13  <li> Cudd_RemapUnderApprox()
14  <li> Cudd_RemapOverApprox()
15  <li> Cudd_BiasedUnderApprox()
16  <li> Cudd_BiasedOverApprox()
17  </ul>
18  Internal procedures included in this module:
19  <ul>
20  <li> cuddUnderApprox()
21  <li> cuddRemapUnderApprox()
22  <li> cuddBiasedUnderApprox()
23  </ul>
24  Static procedures included in this module:
25  <ul>
26  <li> gatherInfoAux()
27  <li> gatherInfo()
28  <li> computeSavings()
29  <li> UAmarkNodes()
30  <li> UAbuildSubset()
31  <li> updateRefs()
32  <li> RAmarkNodes()
33  <li> BAmarkNodes()
34  <li> RAbuildSubset()
35  </ul>
36  ]
37 
38  SeeAlso [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]
39 
40  Author [Fabio Somenzi]
41 
42  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
43 
44  All rights reserved.
45 
46  Redistribution and use in source and binary forms, with or without
47  modification, are permitted provided that the following conditions
48  are met:
49 
50  Redistributions of source code must retain the above copyright
51  notice, this list of conditions and the following disclaimer.
52 
53  Redistributions in binary form must reproduce the above copyright
54  notice, this list of conditions and the following disclaimer in the
55  documentation and/or other materials provided with the distribution.
56 
57  Neither the name of the University of Colorado nor the names of its
58  contributors may be used to endorse or promote products derived from
59  this software without specific prior written permission.
60 
61  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72  POSSIBILITY OF SUCH DAMAGE.]
73 
74 ******************************************************************************/
75 
76 #ifdef __STDC__
77 #include <float.h>
78 #else
79 #define DBL_MAX_EXP 1024
80 #endif
81 #include "misc/util/util_hack.h"
82 #include "cuddInt.h"
83 
85 
86 
87 
88 /*---------------------------------------------------------------------------*/
89 /* Constant declarations */
90 /*---------------------------------------------------------------------------*/
91 
92 #define NOTHING 0
93 #define REPLACE_T 1
94 #define REPLACE_E 2
95 #define REPLACE_N 3
96 #define REPLACE_TT 4
97 #define REPLACE_TE 5
98 
99 #define DONT_CARE 0
100 #define CARE 1
101 #define TOTAL_CARE 2
102 #define CARE_ERROR 3
103 
104 /*---------------------------------------------------------------------------*/
105 /* Stucture declarations */
106 /*---------------------------------------------------------------------------*/
107 
108 /*---------------------------------------------------------------------------*/
109 /* Type declarations */
110 /*---------------------------------------------------------------------------*/
111 
112 /* Data structure to store the information on each node. It keeps the
113 ** number of minterms of the function rooted at this node in terms of
114 ** the number of variables specified by the user; the number of
115 ** minterms of the complement; the impact of the number of minterms of
116 ** this function on the number of minterms of the root function; the
117 ** reference count of the node from within the root function; the
118 ** reference count of the node from an internal node; and the flag
119 ** that says whether the node should be replaced and how. */
120 typedef struct NodeData {
121  double mintermsP; /* minterms for the regular node */
122  double mintermsN; /* minterms for the complemented node */
123  int functionRef; /* references from within this function */
124  char care; /* node intersects care set */
125  char replace; /* replacement decision */
126  short int parity; /* 1: even; 2: odd; 3: both */
127  DdNode *resultP; /* result for even parity */
128  DdNode *resultN; /* result for odd parity */
129 } NodeData;
130 
131 typedef struct ApproxInfo {
132  DdNode *one; /* one constant */
133  DdNode *zero; /* BDD zero constant */
134  NodeData *page; /* per-node information */
135  st__table *table; /* hash table to access the per-node info */
136  int index; /* index of the current node */
137  double max; /* max number of minterms */
138  int size; /* how many nodes are left */
139  double minterms; /* how many minterms are left */
140 } ApproxInfo;
141 
142 /* Item of the queue used in the levelized traversal of the BDD. */
143 #ifdef __osf__
144 #pragma pointer_size save
145 #pragma pointer_size short
146 #endif
147 typedef struct GlobalQueueItem {
151  double impactP;
152  double impactN;
154 
155 typedef struct LocalQueueItem {
159  int localRef;
161 #ifdef __osf__
162 #pragma pointer_size restore
163 #endif
164 
165 
166 /*---------------------------------------------------------------------------*/
167 /* Variable declarations */
168 /*---------------------------------------------------------------------------*/
169 
170 #ifndef lint
171 static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $";
172 #endif
173 
174 /*---------------------------------------------------------------------------*/
175 /* Macro declarations */
176 /*---------------------------------------------------------------------------*/
177 
178 /**AutomaticStart*************************************************************/
179 
180 /*---------------------------------------------------------------------------*/
181 /* Static function prototypes */
182 /*---------------------------------------------------------------------------*/
183 
184 static void updateParity (DdNode *node, ApproxInfo *info, int newparity);
185 static NodeData * gatherInfoAux (DdNode *node, ApproxInfo *info, int parity);
186 static ApproxInfo * gatherInfo (DdManager *dd, DdNode *node, int numVars, int parity);
187 static int computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
188 static int updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
189 static int UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality);
190 static DdNode * UAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
191 static int RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality);
192 static int BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0);
193 static DdNode * RAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
194 static int BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache);
195 
196 /**AutomaticEnd***************************************************************/
197 
198 
199 /*---------------------------------------------------------------------------*/
200 /* Definition of exported functions */
201 /*---------------------------------------------------------------------------*/
202 
203 /**Function********************************************************************
204 
205  Synopsis [Extracts a dense subset from a BDD with Shiple's
206  underapproximation method.]
207 
208  Description [Extracts a dense subset from a BDD. This procedure uses
209  a variant of Tom Shiple's underapproximation method. The main
210  difference from the original method is that density is used as cost
211  function. Returns a pointer to the BDD of the subset if
212  successful. NULL if the procedure runs out of memory. The parameter
213  numVars is the maximum number of variables to be used in minterm
214  calculation. The optimal number should be as close as possible to
215  the size of the support of f. However, it is safe to pass the value
216  returned by Cudd_ReadSize for numVars when the number of variables
217  is under 1023. If numVars is larger than 1023, it will cause
218  overflow. If a 0 parameter is passed then the procedure will compute
219  a value which will avoid overflow but will cause underflow with 2046
220  variables or more.]
221 
222  SideEffects [None]
223 
224  SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]
225 
226 ******************************************************************************/
227 DdNode *
229  DdManager * dd /* manager */,
230  DdNode * f /* function to be subset */,
231  int numVars /* number of variables in the support of f */,
232  int threshold /* when to stop approximation */,
233  int safe /* enforce safe approximation */,
234  double quality /* minimum improvement for accepted changes */)
235 {
236  DdNode *subset;
237 
238  do {
239  dd->reordered = 0;
240  subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
241  } while (dd->reordered == 1);
242 
243  return(subset);
244 
245 } /* end of Cudd_UnderApprox */
246 
247 
248 /**Function********************************************************************
249 
250  Synopsis [Extracts a dense superset from a BDD with Shiple's
251  underapproximation method.]
252 
253  Description [Extracts a dense superset from a BDD. The procedure is
254  identical to the underapproximation procedure except for the fact that it
255  works on the complement of the given function. Extracting the subset
256  of the complement function is equivalent to extracting the superset
257  of the function.
258  Returns a pointer to the BDD of the superset if successful. NULL if
259  intermediate result causes the procedure to run out of memory. The
260  parameter numVars is the maximum number of variables to be used in
261  minterm calculation. The optimal number
262  should be as close as possible to the size of the support of f.
263  However, it is safe to pass the value returned by Cudd_ReadSize for
264  numVars when the number of variables is under 1023. If numVars is
265  larger than 1023, it will overflow. If a 0 parameter is passed then
266  the procedure will compute a value which will avoid overflow but
267  will cause underflow with 2046 variables or more.]
268 
269  SideEffects [None]
270 
271  SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
272 
273 ******************************************************************************/
274 DdNode *
276  DdManager * dd /* manager */,
277  DdNode * f /* function to be superset */,
278  int numVars /* number of variables in the support of f */,
279  int threshold /* when to stop approximation */,
280  int safe /* enforce safe approximation */,
281  double quality /* minimum improvement for accepted changes */)
282 {
283  DdNode *subset, *g;
284 
285  g = Cudd_Not(f);
286  do {
287  dd->reordered = 0;
288  subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
289  } while (dd->reordered == 1);
290 
291  return(Cudd_NotCond(subset, (subset != NULL)));
292 
293 } /* end of Cudd_OverApprox */
294 
295 
296 /**Function********************************************************************
297 
298  Synopsis [Extracts a dense subset from a BDD with the remapping
299  underapproximation method.]
300 
301  Description [Extracts a dense subset from a BDD. This procedure uses
302  a remapping technique and density as the cost function.
303  Returns a pointer to the BDD of the subset if
304  successful. NULL if the procedure runs out of memory. The parameter
305  numVars is the maximum number of variables to be used in minterm
306  calculation. The optimal number should be as close as possible to
307  the size of the support of f. However, it is safe to pass the value
308  returned by Cudd_ReadSize for numVars when the number of variables
309  is under 1023. If numVars is larger than 1023, it will cause
310  overflow. If a 0 parameter is passed then the procedure will compute
311  a value which will avoid overflow but will cause underflow with 2046
312  variables or more.]
313 
314  SideEffects [None]
315 
316  SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize]
317 
318 ******************************************************************************/
319 DdNode *
321  DdManager * dd /* manager */,
322  DdNode * f /* function to be subset */,
323  int numVars /* number of variables in the support of f */,
324  int threshold /* when to stop approximation */,
325  double quality /* minimum improvement for accepted changes */)
326 {
327  DdNode *subset;
328 
329  do {
330  dd->reordered = 0;
331  subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
332  } while (dd->reordered == 1);
333 
334  return(subset);
335 
336 } /* end of Cudd_RemapUnderApprox */
337 
338 
339 /**Function********************************************************************
340 
341  Synopsis [Extracts a dense superset from a BDD with the remapping
342  underapproximation method.]
343 
344  Description [Extracts a dense superset from a BDD. The procedure is
345  identical to the underapproximation procedure except for the fact that it
346  works on the complement of the given function. Extracting the subset
347  of the complement function is equivalent to extracting the superset
348  of the function.
349  Returns a pointer to the BDD of the superset if successful. NULL if
350  intermediate result causes the procedure to run out of memory. The
351  parameter numVars is the maximum number of variables to be used in
352  minterm calculation. The optimal number
353  should be as close as possible to the size of the support of f.
354  However, it is safe to pass the value returned by Cudd_ReadSize for
355  numVars when the number of variables is under 1023. If numVars is
356  larger than 1023, it will overflow. If a 0 parameter is passed then
357  the procedure will compute a value which will avoid overflow but
358  will cause underflow with 2046 variables or more.]
359 
360  SideEffects [None]
361 
362  SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
363 
364 ******************************************************************************/
365 DdNode *
367  DdManager * dd /* manager */,
368  DdNode * f /* function to be superset */,
369  int numVars /* number of variables in the support of f */,
370  int threshold /* when to stop approximation */,
371  double quality /* minimum improvement for accepted changes */)
372 {
373  DdNode *subset, *g;
374 
375  g = Cudd_Not(f);
376  do {
377  dd->reordered = 0;
378  subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
379  } while (dd->reordered == 1);
380 
381  return(Cudd_NotCond(subset, (subset != NULL)));
382 
383 } /* end of Cudd_RemapOverApprox */
384 
385 
386 /**Function********************************************************************
387 
388  Synopsis [Extracts a dense subset from a BDD with the biased
389  underapproximation method.]
390 
391  Description [Extracts a dense subset from a BDD. This procedure uses
392  a biased remapping technique and density as the cost function. The bias
393  is a function. This procedure tries to approximate where the bias is 0
394  and preserve the given function where the bias is 1.
395  Returns a pointer to the BDD of the subset if
396  successful. NULL if the procedure runs out of memory. The parameter
397  numVars is the maximum number of variables to be used in minterm
398  calculation. The optimal number should be as close as possible to
399  the size of the support of f. However, it is safe to pass the value
400  returned by Cudd_ReadSize for numVars when the number of variables
401  is under 1023. If numVars is larger than 1023, it will cause
402  overflow. If a 0 parameter is passed then the procedure will compute
403  a value which will avoid overflow but will cause underflow with 2046
404  variables or more.]
405 
406  SideEffects [None]
407 
408  SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox
409  Cudd_RemapUnderApprox Cudd_ReadSize]
410 
411 ******************************************************************************/
412 DdNode *
414  DdManager *dd /* manager */,
415  DdNode *f /* function to be subset */,
416  DdNode *b /* bias function */,
417  int numVars /* number of variables in the support of f */,
418  int threshold /* when to stop approximation */,
419  double quality1 /* minimum improvement for accepted changes when b=1 */,
420  double quality0 /* minimum improvement for accepted changes when b=0 */)
421 {
422  DdNode *subset;
423 
424  do {
425  dd->reordered = 0;
426  subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
427  quality0);
428  } while (dd->reordered == 1);
429 
430  return(subset);
431 
432 } /* end of Cudd_BiasedUnderApprox */
433 
434 
435 /**Function********************************************************************
436 
437  Synopsis [Extracts a dense superset from a BDD with the biased
438  underapproximation method.]
439 
440  Description [Extracts a dense superset from a BDD. The procedure is
441  identical to the underapproximation procedure except for the fact that it
442  works on the complement of the given function. Extracting the subset
443  of the complement function is equivalent to extracting the superset
444  of the function.
445  Returns a pointer to the BDD of the superset if successful. NULL if
446  intermediate result causes the procedure to run out of memory. The
447  parameter numVars is the maximum number of variables to be used in
448  minterm calculation. The optimal number
449  should be as close as possible to the size of the support of f.
450  However, it is safe to pass the value returned by Cudd_ReadSize for
451  numVars when the number of variables is under 1023. If numVars is
452  larger than 1023, it will overflow. If a 0 parameter is passed then
453  the procedure will compute a value which will avoid overflow but
454  will cause underflow with 2046 variables or more.]
455 
456  SideEffects [None]
457 
458  SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
459  Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]
460 
461 ******************************************************************************/
462 DdNode *
464  DdManager *dd /* manager */,
465  DdNode *f /* function to be superset */,
466  DdNode *b /* bias function */,
467  int numVars /* number of variables in the support of f */,
468  int threshold /* when to stop approximation */,
469  double quality1 /* minimum improvement for accepted changes when b=1*/,
470  double quality0 /* minimum improvement for accepted changes when b=0 */)
471 {
472  DdNode *subset, *g;
473 
474  g = Cudd_Not(f);
475  do {
476  dd->reordered = 0;
477  subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
478  quality0);
479  } while (dd->reordered == 1);
480 
481  return(Cudd_NotCond(subset, (subset != NULL)));
482 
483 } /* end of Cudd_BiasedOverApprox */
484 
485 
486 /*---------------------------------------------------------------------------*/
487 /* Definition of internal functions */
488 /*---------------------------------------------------------------------------*/
489 
490 
491 /**Function********************************************************************
492 
493  Synopsis [Applies Tom Shiple's underappoximation algorithm.]
494 
495  Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
496  in three phases:
497  <ul>
498  <li> collect information on each node in the BDD; this is done via DFS.
499  <li> traverse the BDD in top-down fashion and compute for each node
500  whether its elimination increases density.
501  <li> traverse the BDD via DFS and actually perform the elimination.
502  </ul>
503  Returns the approximated BDD if successful; NULL otherwise.]
504 
505  SideEffects [None]
506 
507  SeeAlso [Cudd_UnderApprox]
508 
509 ******************************************************************************/
510 DdNode *
512  DdManager * dd /* DD manager */,
513  DdNode * f /* current DD */,
514  int numVars /* maximum number of variables */,
515  int threshold /* threshold under which approximation stops */,
516  int safe /* enforce safe approximation */,
517  double quality /* minimum improvement for accepted changes */)
518 {
519  ApproxInfo *info;
520  DdNode *subset;
521  int result;
522 
523  if (f == NULL) {
524  fprintf(dd->err, "Cannot subset, nil object\n");
525  return(NULL);
526  }
527 
528  if (Cudd_IsConstant(f)) {
529  return(f);
530  }
531 
532  /* Create table where node data are accessible via a hash table. */
533  info = gatherInfo(dd, f, numVars, safe);
534  if (info == NULL) {
535  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
537  return(NULL);
538  }
539 
540  /* Mark nodes that should be replaced by zero. */
541  result = UAmarkNodes(dd, f, info, threshold, safe, quality);
542  if (result == 0) {
543  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
544  ABC_FREE(info->page);
545  st__free_table(info->table);
546  ABC_FREE(info);
548  return(NULL);
549  }
550 
551  /* Build the result. */
552  subset = UAbuildSubset(dd, f, info);
553 #if 1
554  if (subset && info->size < Cudd_DagSize(subset))
555  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
556  info->size, Cudd_DagSize(subset));
557 #endif
558  ABC_FREE(info->page);
559  st__free_table(info->table);
560  ABC_FREE(info);
561 
562 #ifdef DD_DEBUG
563  if (subset != NULL) {
564  cuddRef(subset);
565 #if 0
566  (void) Cudd_DebugCheck(dd);
567  (void) Cudd_CheckKeys(dd);
568 #endif
569  if (!Cudd_bddLeq(dd, subset, f)) {
570  (void) fprintf(dd->err, "Wrong subset\n");
572  }
573  cuddDeref(subset);
574  }
575 #endif
576  return(subset);
577 
578 } /* end of cuddUnderApprox */
579 
580 
581 /**Function********************************************************************
582 
583  Synopsis [Applies the remapping underappoximation algorithm.]
584 
585  Description [Applies the remapping underappoximation algorithm.
586  Proceeds in three phases:
587  <ul>
588  <li> collect information on each node in the BDD; this is done via DFS.
589  <li> traverse the BDD in top-down fashion and compute for each node
590  whether remapping increases density.
591  <li> traverse the BDD via DFS and actually perform the elimination.
592  </ul>
593  Returns the approximated BDD if successful; NULL otherwise.]
594 
595  SideEffects [None]
596 
597  SeeAlso [Cudd_RemapUnderApprox]
598 
599 ******************************************************************************/
600 DdNode *
602  DdManager * dd /* DD manager */,
603  DdNode * f /* current DD */,
604  int numVars /* maximum number of variables */,
605  int threshold /* threshold under which approximation stops */,
606  double quality /* minimum improvement for accepted changes */)
607 {
608  ApproxInfo *info;
609  DdNode *subset;
610  int result;
611 
612  if (f == NULL) {
613  fprintf(dd->err, "Cannot subset, nil object\n");
615  return(NULL);
616  }
617 
618  if (Cudd_IsConstant(f)) {
619  return(f);
620  }
621 
622  /* Create table where node data are accessible via a hash table. */
623  info = gatherInfo(dd, f, numVars, TRUE);
624  if (info == NULL) {
625  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
627  return(NULL);
628  }
629 
630  /* Mark nodes that should be replaced by zero. */
631  result = RAmarkNodes(dd, f, info, threshold, quality);
632  if (result == 0) {
633  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
634  ABC_FREE(info->page);
635  st__free_table(info->table);
636  ABC_FREE(info);
638  return(NULL);
639  }
640 
641  /* Build the result. */
642  subset = RAbuildSubset(dd, f, info);
643 #if 1
644  if (subset && info->size < Cudd_DagSize(subset))
645  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
646  info->size, Cudd_DagSize(subset));
647 #endif
648  ABC_FREE(info->page);
649  st__free_table(info->table);
650  ABC_FREE(info);
651 
652 #ifdef DD_DEBUG
653  if (subset != NULL) {
654  cuddRef(subset);
655 #if 0
656  (void) Cudd_DebugCheck(dd);
657  (void) Cudd_CheckKeys(dd);
658 #endif
659  if (!Cudd_bddLeq(dd, subset, f)) {
660  (void) fprintf(dd->err, "Wrong subset\n");
661  }
662  cuddDeref(subset);
664  }
665 #endif
666  return(subset);
667 
668 } /* end of cuddRemapUnderApprox */
669 
670 
671 /**Function********************************************************************
672 
673  Synopsis [Applies the biased remapping underappoximation algorithm.]
674 
675  Description [Applies the biased remapping underappoximation algorithm.
676  Proceeds in three phases:
677  <ul>
678  <li> collect information on each node in the BDD; this is done via DFS.
679  <li> traverse the BDD in top-down fashion and compute for each node
680  whether remapping increases density.
681  <li> traverse the BDD via DFS and actually perform the elimination.
682  </ul>
683  Returns the approximated BDD if successful; NULL otherwise.]
684 
685  SideEffects [None]
686 
687  SeeAlso [Cudd_BiasedUnderApprox]
688 
689 ******************************************************************************/
690 DdNode *
692  DdManager *dd /* DD manager */,
693  DdNode *f /* current DD */,
694  DdNode *b /* bias function */,
695  int numVars /* maximum number of variables */,
696  int threshold /* threshold under which approximation stops */,
697  double quality1 /* minimum improvement for accepted changes when b=1 */,
698  double quality0 /* minimum improvement for accepted changes when b=0 */)
699 {
700  ApproxInfo *info;
701  DdNode *subset;
702  int result;
703  DdHashTable *cache;
704 
705  if (f == NULL) {
706  fprintf(dd->err, "Cannot subset, nil object\n");
708  return(NULL);
709  }
710 
711  if (Cudd_IsConstant(f)) {
712  return(f);
713  }
714 
715  /* Create table where node data are accessible via a hash table. */
716  info = gatherInfo(dd, f, numVars, TRUE);
717  if (info == NULL) {
718  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
720  return(NULL);
721  }
722 
723  cache = cuddHashTableInit(dd,2,2);
724  result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
725  if (result == CARE_ERROR) {
726  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
727  cuddHashTableQuit(cache);
728  ABC_FREE(info->page);
729  st__free_table(info->table);
730  ABC_FREE(info);
732  return(NULL);
733  }
734  cuddHashTableQuit(cache);
735 
736  /* Mark nodes that should be replaced by zero. */
737  result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
738  if (result == 0) {
739  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
740  ABC_FREE(info->page);
741  st__free_table(info->table);
742  ABC_FREE(info);
744  return(NULL);
745  }
746 
747  /* Build the result. */
748  subset = RAbuildSubset(dd, f, info);
749 #if 1
750  if (subset && info->size < Cudd_DagSize(subset))
751  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
752  info->size, Cudd_DagSize(subset));
753 #endif
754  ABC_FREE(info->page);
755  st__free_table(info->table);
756  ABC_FREE(info);
757 
758 #ifdef DD_DEBUG
759  if (subset != NULL) {
760  cuddRef(subset);
761 #if 0
762  (void) Cudd_DebugCheck(dd);
763  (void) Cudd_CheckKeys(dd);
764 #endif
765  if (!Cudd_bddLeq(dd, subset, f)) {
766  (void) fprintf(dd->err, "Wrong subset\n");
767  }
768  cuddDeref(subset);
770  }
771 #endif
772  return(subset);
773 
774 } /* end of cuddBiasedUnderApprox */
775 
776 
777 /*---------------------------------------------------------------------------*/
778 /* Definition of static functions */
779 /*---------------------------------------------------------------------------*/
780 
781 
782 /**Function********************************************************************
783 
784  Synopsis [Recursively update the parity of the paths reaching a node.]
785 
786  Description [Recursively update the parity of the paths reaching a node.
787  Assumes that node is regular and propagates the invariant.]
788 
789  SideEffects [None]
790 
791  SeeAlso [gatherInfoAux]
792 
793 ******************************************************************************/
794 static void
796  DdNode * node /* function to analyze */,
797  ApproxInfo * info /* info on BDD */,
798  int newparity /* new parity for node */)
799 {
800  NodeData *infoN;
801  DdNode *E;
802 
803  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) return;
804  if ((infoN->parity & newparity) != 0) return;
805  infoN->parity |= (short) newparity;
806  if (Cudd_IsConstant(node)) return;
807  updateParity(cuddT(node),info,newparity);
808  E = cuddE(node);
809  if (Cudd_IsComplement(E)) {
810  updateParity(Cudd_Not(E),info,3-newparity);
811  } else {
812  updateParity(E,info,newparity);
813  }
814  return;
815 
816 } /* end of updateParity */
817 
818 
819 /**Function********************************************************************
820 
821  Synopsis [Recursively counts minterms and computes reference counts
822  of each node in the BDD.]
823 
824  Description [Recursively counts minterms and computes reference
825  counts of each node in the BDD. Similar to the cuddCountMintermAux
826  which recursively counts the number of minterms for the dag rooted
827  at each node in terms of the total number of variables (max). It assumes
828  that the node pointer passed to it is regular and it maintains the
829  invariant.]
830 
831  SideEffects [None]
832 
833  SeeAlso [gatherInfo]
834 
835 ******************************************************************************/
836 static NodeData *
838  DdNode * node /* function to analyze */,
839  ApproxInfo * info /* info on BDD */,
840  int parity /* gather parity information */)
841 {
842  DdNode *N, *Nt, *Ne;
843  NodeData *infoN, *infoT, *infoE;
844 
845  N = Cudd_Regular(node);
846 
847  /* Check whether entry for this node exists. */
848  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
849  if (parity) {
850  /* Update parity and propagate. */
851  updateParity(N, info, 1 + (int) Cudd_IsComplement(node));
852  }
853  return(infoN);
854  }
855 
856  /* Compute the cofactors. */
857  Nt = Cudd_NotCond(cuddT(N), N != node);
858  Ne = Cudd_NotCond(cuddE(N), N != node);
859 
860  infoT = gatherInfoAux(Nt, info, parity);
861  if (infoT == NULL) return(NULL);
862  infoE = gatherInfoAux(Ne, info, parity);
863  if (infoE == NULL) return(NULL);
864 
865  infoT->functionRef++;
866  infoE->functionRef++;
867 
868  /* Point to the correct location in the page. */
869  infoN = &(info->page[info->index++]);
870  infoN->parity |= (short) (1 + Cudd_IsComplement(node));
871 
872  infoN->mintermsP = infoT->mintermsP/2;
873  infoN->mintermsN = infoT->mintermsN/2;
874  if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
875  infoN->mintermsP += infoE->mintermsN/2;
876  infoN->mintermsN += infoE->mintermsP/2;
877  } else {
878  infoN->mintermsP += infoE->mintermsP/2;
879  infoN->mintermsN += infoE->mintermsN/2;
880  }
881 
882  /* Insert entry for the node in the table. */
883  if ( st__insert(info->table,(char *)N, (char *)infoN) == st__OUT_OF_MEM) {
884  return(NULL);
885  }
886  return(infoN);
887 
888 } /* end of gatherInfoAux */
889 
890 
891 /**Function********************************************************************
892 
893  Synopsis [Gathers information about each node.]
894 
895  Description [Counts minterms and computes reference counts of each
896  node in the BDD . The minterm count is separately computed for the
897  node and its complement. This is to avoid cancellation
898  errors. Returns a pointer to the data structure holding the
899  information gathered if successful; NULL otherwise.]
900 
901  SideEffects [None]
902 
903  SeeAlso [cuddUnderApprox gatherInfoAux]
904 
905 ******************************************************************************/
906 static ApproxInfo *
908  DdManager * dd /* manager */,
909  DdNode * node /* function to be analyzed */,
910  int numVars /* number of variables node depends on */,
911  int parity /* gather parity information */)
912 {
913  ApproxInfo *info;
914  NodeData *infoTop;
915 
916  /* If user did not give numVars value, set it to the maximum
917  ** exponent that the pow function can take. The -1 is due to the
918  ** discrepancy in the value that pow takes and the value that
919  ** log gives.
920  */
921  if (numVars == 0) {
922  numVars = DBL_MAX_EXP - 1;
923  }
924 
925  info = ABC_ALLOC(ApproxInfo,1);
926  if (info == NULL) {
928  return(NULL);
929  }
930  info->max = pow(2.0,(double) numVars);
931  info->one = DD_ONE(dd);
932  info->zero = Cudd_Not(info->one);
933  info->size = Cudd_DagSize(node);
934  /* All the information gathered will be stored in a contiguous
935  ** piece of memory, which is allocated here. This can be done
936  ** efficiently because we have counted the number of nodes of the
937  ** BDD. info->index points to the next available entry in the array
938  ** that stores the per-node information. */
939  info->page = ABC_ALLOC(NodeData,info->size);
940  if (info->page == NULL) {
942  ABC_FREE(info);
943  return(NULL);
944  }
945  memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
947  if (info->table == NULL) {
948  ABC_FREE(info->page);
949  ABC_FREE(info);
950  return(NULL);
951  }
952  /* We visit the DAG in post-order DFS. Hence, the constant node is
953  ** in first position, and the root of the DAG is in last position. */
954 
955  /* Info for the constant node: Initialize only fields different from 0. */
956  if ( st__insert(info->table, (char *)info->one, (char *)info->page) == st__OUT_OF_MEM) {
957  ABC_FREE(info->page);
958  ABC_FREE(info);
959  st__free_table(info->table);
960  return(NULL);
961  }
962  info->page[0].mintermsP = info->max;
963  info->index = 1;
964 
965  infoTop = gatherInfoAux(node,info,parity);
966  if (infoTop == NULL) {
967  ABC_FREE(info->page);
968  st__free_table(info->table);
969  ABC_FREE(info);
970  return(NULL);
971  }
972  if (Cudd_IsComplement(node)) {
973  info->minterms = infoTop->mintermsN;
974  } else {
975  info->minterms = infoTop->mintermsP;
976  }
977 
978  infoTop->functionRef = 1;
979  return(info);
980 
981 } /* end of gatherInfo */
982 
983 
984 /**Function********************************************************************
985 
986  Synopsis [Counts the nodes that would be eliminated if a given node
987  were replaced by zero.]
988 
989  Description [Counts the nodes that would be eliminated if a given
990  node were replaced by zero. This procedure uses a queue passed by
991  the caller for efficiency: since the queue is left empty at the
992  endof the search, it can be reused as is by the next search. Returns
993  the count (always striclty positive) if successful; 0 otherwise.]
994 
995  SideEffects [None]
996 
997  SeeAlso [cuddUnderApprox]
998 
999 ******************************************************************************/
1000 static int
1002  DdManager * dd,
1003  DdNode * f,
1004  DdNode * skip,
1005  ApproxInfo * info,
1006  DdLevelQueue * queue)
1007 {
1008  NodeData *infoN;
1009  LocalQueueItem *item;
1010  DdNode *node;
1011  int savings = 0;
1012 
1013  node = Cudd_Regular(f);
1014  skip = Cudd_Regular(skip);
1015  /* Insert the given node in the level queue. Its local reference
1016  ** count is set equal to the function reference count so that the
1017  ** search will continue from it when it is retrieved. */
1018  item = (LocalQueueItem *)
1019  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1020  if (item == NULL)
1021  return(0);
1022  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1023  item->localRef = infoN->functionRef;
1024 
1025  /* Process the queue. */
1026  while (queue->first != NULL) {
1027  item = (LocalQueueItem *) queue->first;
1028  node = item->node;
1029  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1030  if (node == skip) continue;
1031  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1032  if (item->localRef != infoN->functionRef) {
1033  /* This node is shared. */
1034  continue;
1035  }
1036  savings++;
1037  if (!cuddIsConstant(cuddT(node))) {
1038  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1039  cuddI(dd,cuddT(node)->index));
1040  if (item == NULL) return(0);
1041  item->localRef++;
1042  }
1043  if (!Cudd_IsConstant(cuddE(node))) {
1044  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1045  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1046  if (item == NULL) return(0);
1047  item->localRef++;
1048  }
1049  }
1050 
1051 #ifdef DD_DEBUG
1052  /* At the end of a local search the queue should be empty. */
1053  assert(queue->size == 0);
1054 #endif
1055  return(savings);
1056 
1057 } /* end of computeSavings */
1058 
1059 
1060 /**Function********************************************************************
1061 
1062  Synopsis [Update function reference counts.]
1063 
1064  Description [Update function reference counts to account for replacement.
1065  Returns the number of nodes saved if successful; 0 otherwise.]
1066 
1067  SideEffects [None]
1068 
1069  SeeAlso [UAmarkNodes RAmarkNodes]
1070 
1071 ******************************************************************************/
1072 static int
1074  DdManager * dd,
1075  DdNode * f,
1076  DdNode * skip,
1077  ApproxInfo * info,
1078  DdLevelQueue * queue)
1079 {
1080  NodeData *infoN;
1081  LocalQueueItem *item;
1082  DdNode *node;
1083  int savings = 0;
1084 
1085  node = Cudd_Regular(f);
1086  /* Insert the given node in the level queue. Its function reference
1087  ** count is set equal to 0 so that the search will continue from it
1088  ** when it is retrieved. */
1089  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1090  if (item == NULL)
1091  return(0);
1092  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1093  infoN->functionRef = 0;
1094 
1095  if (skip != NULL) {
1096  /* Increase the function reference count of the node to be skipped
1097  ** by 1 to account for the node pointing to it that will be created. */
1098  skip = Cudd_Regular(skip);
1099  (void) st__lookup(info->table, (const char *)skip, (char **)&infoN);
1100  infoN->functionRef++;
1101  }
1102 
1103  /* Process the queue. */
1104  while (queue->first != NULL) {
1105  item = (LocalQueueItem *) queue->first;
1106  node = item->node;
1107  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1108  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1109  if (infoN->functionRef != 0) {
1110  /* This node is shared or must be skipped. */
1111  continue;
1112  }
1113  savings++;
1114  if (!cuddIsConstant(cuddT(node))) {
1115  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1116  cuddI(dd,cuddT(node)->index));
1117  if (item == NULL) return(0);
1118  (void) st__lookup(info->table, (const char *)cuddT(node), (char **)&infoN);
1119  infoN->functionRef--;
1120  }
1121  if (!Cudd_IsConstant(cuddE(node))) {
1122  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1123  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1124  if (item == NULL) return(0);
1125  (void) st__lookup(info->table, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN);
1126  infoN->functionRef--;
1127  }
1128  }
1129 
1130 #ifdef DD_DEBUG
1131  /* At the end of a local search the queue should be empty. */
1132  assert(queue->size == 0);
1133 #endif
1134  return(savings);
1135 
1136 } /* end of updateRefs */
1137 
1138 
1139 /**Function********************************************************************
1140 
1141  Synopsis [Marks nodes for replacement by zero.]
1142 
1143  Description [Marks nodes for replacement by zero. Returns 1 if successful;
1144  0 otherwise.]
1145 
1146  SideEffects [None]
1147 
1148  SeeAlso [cuddUnderApprox]
1149 
1150 ******************************************************************************/
1151 static int
1153  DdManager * dd /* manager */,
1154  DdNode * f /* function to be analyzed */,
1155  ApproxInfo * info /* info on BDD */,
1156  int threshold /* when to stop approximating */,
1157  int safe /* enforce safe approximation */,
1158  double quality /* minimum improvement for accepted changes */)
1159 {
1160  DdLevelQueue *queue;
1161  DdLevelQueue *localQueue;
1162  NodeData *infoN;
1163  GlobalQueueItem *item;
1164  DdNode *node;
1165  double numOnset;
1166  double impactP, impactN;
1167  int savings;
1168 
1169 #if 0
1170  (void) printf("initial size = %d initial minterms = %g\n",
1171  info->size, info->minterms);
1172 #endif
1173  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1174  if (queue == NULL) {
1175  return(0);
1176  }
1177  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1178  dd->initSlots);
1179  if (localQueue == NULL) {
1180  cuddLevelQueueQuit(queue);
1181  return(0);
1182  }
1183  node = Cudd_Regular(f);
1184  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1185  if (item == NULL) {
1186  cuddLevelQueueQuit(queue);
1187  cuddLevelQueueQuit(localQueue);
1188  return(0);
1189  }
1190  if (Cudd_IsComplement(f)) {
1191  item->impactP = 0.0;
1192  item->impactN = 1.0;
1193  } else {
1194  item->impactP = 1.0;
1195  item->impactN = 0.0;
1196  }
1197  while (queue->first != NULL) {
1198  /* If the size of the subset is below the threshold, quit. */
1199  if (info->size <= threshold)
1200  break;
1201  item = (GlobalQueueItem *) queue->first;
1202  node = item->node;
1203  node = Cudd_Regular(node);
1204  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1205  if (safe && infoN->parity == 3) {
1206  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1207  continue;
1208  }
1209  impactP = item->impactP;
1210  impactN = item->impactN;
1211  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1212  savings = computeSavings(dd,node,NULL,info,localQueue);
1213  if (savings == 0) {
1214  cuddLevelQueueQuit(queue);
1215  cuddLevelQueueQuit(localQueue);
1216  return(0);
1217  }
1218  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1219 #if 0
1220  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1221  node, impactP, impactN, numOnset, savings);
1222 #endif
1223  if ((1 - numOnset / info->minterms) >
1224  quality * (1 - (double) savings / info->size)) {
1225  infoN->replace = TRUE;
1226  info->size -= savings;
1227  info->minterms -=numOnset;
1228 #if 0
1229  (void) printf("replace: new size = %d new minterms = %g\n",
1230  info->size, info->minterms);
1231 #endif
1232  savings -= updateRefs(dd,node,NULL,info,localQueue);
1233  assert(savings == 0);
1234  continue;
1235  }
1236  if (!cuddIsConstant(cuddT(node))) {
1237  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1238  cuddI(dd,cuddT(node)->index));
1239  item->impactP += impactP/2.0;
1240  item->impactN += impactN/2.0;
1241  }
1242  if (!Cudd_IsConstant(cuddE(node))) {
1243  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1244  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1245  if (Cudd_IsComplement(cuddE(node))) {
1246  item->impactP += impactN/2.0;
1247  item->impactN += impactP/2.0;
1248  } else {
1249  item->impactP += impactP/2.0;
1250  item->impactN += impactN/2.0;
1251  }
1252  }
1253  }
1254 
1255  cuddLevelQueueQuit(queue);
1256  cuddLevelQueueQuit(localQueue);
1257  return(1);
1258 
1259 } /* end of UAmarkNodes */
1260 
1261 
1262 /**Function********************************************************************
1263 
1264  Synopsis [Builds the subset BDD.]
1265 
1266  Description [Builds the subset BDD. Based on the info table,
1267  replaces selected nodes by zero. Returns a pointer to the result if
1268  successful; NULL otherwise.]
1269 
1270  SideEffects [None]
1271 
1272  SeeAlso [cuddUnderApprox]
1273 
1274 ******************************************************************************/
1275 static DdNode *
1277  DdManager * dd /* DD manager */,
1278  DdNode * node /* current node */,
1279  ApproxInfo * info /* node info */)
1280 {
1281 
1282  DdNode *Nt, *Ne, *N, *t, *e, *r;
1283  NodeData *infoN;
1284 
1285  if (Cudd_IsConstant(node))
1286  return(node);
1287 
1288  N = Cudd_Regular(node);
1289 
1290  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
1291  if (infoN->replace == TRUE) {
1292  return(info->zero);
1293  }
1294  if (N == node ) {
1295  if (infoN->resultP != NULL) {
1296  return(infoN->resultP);
1297  }
1298  } else {
1299  if (infoN->resultN != NULL) {
1300  return(infoN->resultN);
1301  }
1302  }
1303  } else {
1304  (void) fprintf(dd->err,
1305  "Something is wrong, ought to be in info table\n");
1307  return(NULL);
1308  }
1309 
1310  Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
1311  Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
1312 
1313  t = UAbuildSubset(dd, Nt, info);
1314  if (t == NULL) {
1315  return(NULL);
1316  }
1317  cuddRef(t);
1318 
1319  e = UAbuildSubset(dd, Ne, info);
1320  if (e == NULL) {
1321  Cudd_RecursiveDeref(dd,t);
1322  return(NULL);
1323  }
1324  cuddRef(e);
1325 
1326  if (Cudd_IsComplement(t)) {
1327  t = Cudd_Not(t);
1328  e = Cudd_Not(e);
1329  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1330  if (r == NULL) {
1331  Cudd_RecursiveDeref(dd, e);
1332  Cudd_RecursiveDeref(dd, t);
1333  return(NULL);
1334  }
1335  r = Cudd_Not(r);
1336  } else {
1337  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1338  if (r == NULL) {
1339  Cudd_RecursiveDeref(dd, e);
1340  Cudd_RecursiveDeref(dd, t);
1341  return(NULL);
1342  }
1343  }
1344  cuddDeref(t);
1345  cuddDeref(e);
1346 
1347  if (N == node) {
1348  infoN->resultP = r;
1349  } else {
1350  infoN->resultN = r;
1351  }
1352 
1353  return(r);
1354 
1355 } /* end of UAbuildSubset */
1356 
1357 
1358 /**Function********************************************************************
1359 
1360  Synopsis [Marks nodes for remapping.]
1361 
1362  Description [Marks nodes for remapping. Returns 1 if successful; 0
1363  otherwise.]
1364 
1365  SideEffects [None]
1366 
1367  SeeAlso [cuddRemapUnderApprox]
1368 
1369 ******************************************************************************/
1370 static int
1372  DdManager * dd /* manager */,
1373  DdNode * f /* function to be analyzed */,
1374  ApproxInfo * info /* info on BDD */,
1375  int threshold /* when to stop approximating */,
1376  double quality /* minimum improvement for accepted changes */)
1377 {
1378  DdLevelQueue *queue;
1379  DdLevelQueue *localQueue;
1380  NodeData *infoN, *infoT, *infoE;
1381  GlobalQueueItem *item;
1382  DdNode *node, *T, *E;
1383  DdNode *shared; /* grandchild shared by the two children of node */
1384  double numOnset;
1385  double impact, impactP, impactN;
1386  double minterms;
1387  int savings;
1388  int replace;
1389 
1390 #if 0
1391  (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1392  info->size, info->minterms);
1393 #endif
1394  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1395  if (queue == NULL) {
1396  return(0);
1397  }
1398  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1399  dd->initSlots);
1400  if (localQueue == NULL) {
1401  cuddLevelQueueQuit(queue);
1402  return(0);
1403  }
1404  /* Enqueue regular pointer to root and initialize impact. */
1405  node = Cudd_Regular(f);
1406  item = (GlobalQueueItem *)
1407  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1408  if (item == NULL) {
1409  cuddLevelQueueQuit(queue);
1410  cuddLevelQueueQuit(localQueue);
1411  return(0);
1412  }
1413  if (Cudd_IsComplement(f)) {
1414  item->impactP = 0.0;
1415  item->impactN = 1.0;
1416  } else {
1417  item->impactP = 1.0;
1418  item->impactN = 0.0;
1419  }
1420  /* The nodes retrieved here are guaranteed to be non-terminal.
1421  ** The initial node is not terminal because constant nodes are
1422  ** dealt with in the calling procedure. Subsequent nodes are inserted
1423  ** only if they are not terminal. */
1424  while (queue->first != NULL) {
1425  /* If the size of the subset is below the threshold, quit. */
1426  if (info->size <= threshold)
1427  break;
1428  item = (GlobalQueueItem *) queue->first;
1429  node = item->node;
1430 #ifdef DD_DEBUG
1431  assert(item->impactP >= 0 && item->impactP <= 1.0);
1432  assert(item->impactN >= 0 && item->impactN <= 1.0);
1433  assert(!Cudd_IsComplement(node));
1434  assert(!Cudd_IsConstant(node));
1435 #endif
1436  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
1437  cuddLevelQueueQuit(queue);
1438  cuddLevelQueueQuit(localQueue);
1439  return(0);
1440  }
1441 #ifdef DD_DEBUG
1442  assert(infoN->parity >= 1 && infoN->parity <= 3);
1443 #endif
1444  if (infoN->parity == 3) {
1445  /* This node can be reached through paths of different parity.
1446  ** It is not safe to replace it, because remapping will give
1447  ** an incorrect result, while replacement by 0 may cause node
1448  ** splitting. */
1449  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1450  continue;
1451  }
1452  T = cuddT(node);
1453  E = cuddE(node);
1454  shared = NULL;
1455  impactP = item->impactP;
1456  impactN = item->impactN;
1457  if (Cudd_bddLeq(dd,T,E)) {
1458  /* Here we know that E is regular. */
1459 #ifdef DD_DEBUG
1461 #endif
1462  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1463  (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1464  if (infoN->parity == 1) {
1465  impact = impactP;
1466  minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1467  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1468  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1469  if (savings == 1) {
1470  cuddLevelQueueQuit(queue);
1471  cuddLevelQueueQuit(localQueue);
1472  return(0);
1473  }
1474  } else {
1475  savings = 1;
1476  }
1477  replace = REPLACE_E;
1478  } else {
1479 #ifdef DD_DEBUG
1480  assert(infoN->parity == 2);
1481 #endif
1482  impact = impactN;
1483  minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1484  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1485  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1486  if (savings == 1) {
1487  cuddLevelQueueQuit(queue);
1488  cuddLevelQueueQuit(localQueue);
1489  return(0);
1490  }
1491  } else {
1492  savings = 1;
1493  }
1494  replace = REPLACE_T;
1495  }
1496  numOnset = impact * minterms;
1497  } else if (Cudd_bddLeq(dd,E,T)) {
1498  /* Here E may be complemented. */
1499  DdNode *Ereg = Cudd_Regular(E);
1500  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1501  (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1502  if (infoN->parity == 1) {
1503  impact = impactP;
1504  minterms = infoT->mintermsP/2.0 -
1505  ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1506  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1507  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1508  if (savings == 1) {
1509  cuddLevelQueueQuit(queue);
1510  cuddLevelQueueQuit(localQueue);
1511  return(0);
1512  }
1513  } else {
1514  savings = 1;
1515  }
1516  replace = REPLACE_T;
1517  } else {
1518 #ifdef DD_DEBUG
1519  assert(infoN->parity == 2);
1520 #endif
1521  impact = impactN;
1522  minterms = ((E == Ereg) ? infoE->mintermsN :
1523  infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1524  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1525  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1526  if (savings == 1) {
1527  cuddLevelQueueQuit(queue);
1528  cuddLevelQueueQuit(localQueue);
1529  return(0);
1530  }
1531  } else {
1532  savings = 1;
1533  }
1534  replace = REPLACE_E;
1535  }
1536  numOnset = impact * minterms;
1537  } else {
1538  DdNode *Ereg = Cudd_Regular(E);
1539  DdNode *TT = cuddT(T);
1540  DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1541  if (T->index == Ereg->index && TT == ET) {
1542  shared = TT;
1543  replace = REPLACE_TT;
1544  } else {
1545  DdNode *TE = cuddE(T);
1546  DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1547  if (T->index == Ereg->index && TE == EE) {
1548  shared = TE;
1549  replace = REPLACE_TE;
1550  } else {
1551  replace = REPLACE_N;
1552  }
1553  }
1554  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1555  savings = computeSavings(dd,node,shared,info,localQueue);
1556  if (shared != NULL) {
1557  NodeData *infoS;
1558  (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1559  if (Cudd_IsComplement(shared)) {
1560  numOnset -= (infoS->mintermsN * impactP +
1561  infoS->mintermsP * impactN)/2.0;
1562  } else {
1563  numOnset -= (infoS->mintermsP * impactP +
1564  infoS->mintermsN * impactN)/2.0;
1565  }
1566  savings--;
1567  }
1568  }
1569 
1570  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1571 #if 0
1572  if (replace == REPLACE_T || replace == REPLACE_E)
1573  (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1574  node, impact, numOnset, savings);
1575  else
1576  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1577  node, impactP, impactN, numOnset, savings);
1578 #endif
1579  if ((1 - numOnset / info->minterms) >
1580  quality * (1 - (double) savings / info->size)) {
1581  infoN->replace = (char) replace;
1582  info->size -= savings;
1583  info->minterms -=numOnset;
1584 #if 0
1585  (void) printf("remap(%d): new size = %d new minterms = %g\n",
1586  replace, info->size, info->minterms);
1587 #endif
1588  if (replace == REPLACE_N) {
1589  savings -= updateRefs(dd,node,NULL,info,localQueue);
1590  } else if (replace == REPLACE_T) {
1591  savings -= updateRefs(dd,node,E,info,localQueue);
1592  } else if (replace == REPLACE_E) {
1593  savings -= updateRefs(dd,node,T,info,localQueue);
1594  } else {
1595 #ifdef DD_DEBUG
1596  assert(replace == REPLACE_TT || replace == REPLACE_TE);
1597 #endif
1598  savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1599  }
1600  assert(savings == 0);
1601  } else {
1602  replace = NOTHING;
1603  }
1604  if (replace == REPLACE_N) continue;
1605  if ((replace == REPLACE_E || replace == NOTHING) &&
1606  !cuddIsConstant(cuddT(node))) {
1607  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1608  cuddI(dd,cuddT(node)->index));
1609  if (replace == REPLACE_E) {
1610  item->impactP += impactP;
1611  item->impactN += impactN;
1612  } else {
1613  item->impactP += impactP/2.0;
1614  item->impactN += impactN/2.0;
1615  }
1616  }
1617  if ((replace == REPLACE_T || replace == NOTHING) &&
1618  !Cudd_IsConstant(cuddE(node))) {
1619  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1620  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1621  if (Cudd_IsComplement(cuddE(node))) {
1622  if (replace == REPLACE_T) {
1623  item->impactP += impactN;
1624  item->impactN += impactP;
1625  } else {
1626  item->impactP += impactN/2.0;
1627  item->impactN += impactP/2.0;
1628  }
1629  } else {
1630  if (replace == REPLACE_T) {
1631  item->impactP += impactP;
1632  item->impactN += impactN;
1633  } else {
1634  item->impactP += impactP/2.0;
1635  item->impactN += impactN/2.0;
1636  }
1637  }
1638  }
1639  if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1640  !Cudd_IsConstant(shared)) {
1641  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1642  cuddI(dd,Cudd_Regular(shared)->index));
1643  if (Cudd_IsComplement(shared)) {
1644  item->impactP += impactN;
1645  item->impactN += impactP;
1646  } else {
1647  item->impactP += impactP;
1648  item->impactN += impactN;
1649  }
1650  }
1651  }
1652 
1653  cuddLevelQueueQuit(queue);
1654  cuddLevelQueueQuit(localQueue);
1655  return(1);
1656 
1657 } /* end of RAmarkNodes */
1658 
1659 
1660 /**Function********************************************************************
1661 
1662  Synopsis [Marks nodes for remapping.]
1663 
1664  Description [Marks nodes for remapping. Returns 1 if successful; 0
1665  otherwise.]
1666 
1667  SideEffects [None]
1668 
1669  SeeAlso [cuddRemapUnderApprox]
1670 
1671 ******************************************************************************/
1672 static int
1674  DdManager *dd /* manager */,
1675  DdNode *f /* function to be analyzed */,
1676  ApproxInfo *info /* info on BDD */,
1677  int threshold /* when to stop approximating */,
1678  double quality1 /* minimum improvement for accepted changes when b=1 */,
1679  double quality0 /* minimum improvement for accepted changes when b=0 */)
1680 {
1681  DdLevelQueue *queue;
1682  DdLevelQueue *localQueue;
1683  NodeData *infoN, *infoT, *infoE;
1684  GlobalQueueItem *item;
1685  DdNode *node, *T, *E;
1686  DdNode *shared; /* grandchild shared by the two children of node */
1687  double numOnset;
1688  double impact, impactP, impactN;
1689  double minterms;
1690  double quality;
1691  int savings;
1692  int replace;
1693 
1694 #if 0
1695  (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1696  info->size, info->minterms);
1697 #endif
1698  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1699  if (queue == NULL) {
1700  return(0);
1701  }
1702  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1703  dd->initSlots);
1704  if (localQueue == NULL) {
1705  cuddLevelQueueQuit(queue);
1706  return(0);
1707  }
1708  /* Enqueue regular pointer to root and initialize impact. */
1709  node = Cudd_Regular(f);
1710  item = (GlobalQueueItem *)
1711  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1712  if (item == NULL) {
1713  cuddLevelQueueQuit(queue);
1714  cuddLevelQueueQuit(localQueue);
1715  return(0);
1716  }
1717  if (Cudd_IsComplement(f)) {
1718  item->impactP = 0.0;
1719  item->impactN = 1.0;
1720  } else {
1721  item->impactP = 1.0;
1722  item->impactN = 0.0;
1723  }
1724  /* The nodes retrieved here are guaranteed to be non-terminal.
1725  ** The initial node is not terminal because constant nodes are
1726  ** dealt with in the calling procedure. Subsequent nodes are inserted
1727  ** only if they are not terminal. */
1728  while (queue->first != NULL) {
1729  /* If the size of the subset is below the threshold, quit. */
1730  if (info->size <= threshold)
1731  break;
1732  item = (GlobalQueueItem *) queue->first;
1733  node = item->node;
1734 #ifdef DD_DEBUG
1735  assert(item->impactP >= 0 && item->impactP <= 1.0);
1736  assert(item->impactN >= 0 && item->impactN <= 1.0);
1737  assert(!Cudd_IsComplement(node));
1738  assert(!Cudd_IsConstant(node));
1739 #endif
1740  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
1741  cuddLevelQueueQuit(queue);
1742  cuddLevelQueueQuit(localQueue);
1743  return(0);
1744  }
1745  quality = infoN->care ? quality1 : quality0;
1746 #ifdef DD_DEBUG
1747  assert(infoN->parity >= 1 && infoN->parity <= 3);
1748 #endif
1749  if (infoN->parity == 3) {
1750  /* This node can be reached through paths of different parity.
1751  ** It is not safe to replace it, because remapping will give
1752  ** an incorrect result, while replacement by 0 may cause node
1753  ** splitting. */
1754  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1755  continue;
1756  }
1757  T = cuddT(node);
1758  E = cuddE(node);
1759  shared = NULL;
1760  impactP = item->impactP;
1761  impactN = item->impactN;
1762  if (Cudd_bddLeq(dd,T,E)) {
1763  /* Here we know that E is regular. */
1764 #ifdef DD_DEBUG
1766 #endif
1767  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1768  (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1769  if (infoN->parity == 1) {
1770  impact = impactP;
1771  minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1772  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1773  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1774  if (savings == 1) {
1775  cuddLevelQueueQuit(queue);
1776  cuddLevelQueueQuit(localQueue);
1777  return(0);
1778  }
1779  } else {
1780  savings = 1;
1781  }
1782  replace = REPLACE_E;
1783  } else {
1784 #ifdef DD_DEBUG
1785  assert(infoN->parity == 2);
1786 #endif
1787  impact = impactN;
1788  minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1789  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1790  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1791  if (savings == 1) {
1792  cuddLevelQueueQuit(queue);
1793  cuddLevelQueueQuit(localQueue);
1794  return(0);
1795  }
1796  } else {
1797  savings = 1;
1798  }
1799  replace = REPLACE_T;
1800  }
1801  numOnset = impact * minterms;
1802  } else if (Cudd_bddLeq(dd,E,T)) {
1803  /* Here E may be complemented. */
1804  DdNode *Ereg = Cudd_Regular(E);
1805  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1806  (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1807  if (infoN->parity == 1) {
1808  impact = impactP;
1809  minterms = infoT->mintermsP/2.0 -
1810  ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1811  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1812  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1813  if (savings == 1) {
1814  cuddLevelQueueQuit(queue);
1815  cuddLevelQueueQuit(localQueue);
1816  return(0);
1817  }
1818  } else {
1819  savings = 1;
1820  }
1821  replace = REPLACE_T;
1822  } else {
1823 #ifdef DD_DEBUG
1824  assert(infoN->parity == 2);
1825 #endif
1826  impact = impactN;
1827  minterms = ((E == Ereg) ? infoE->mintermsN :
1828  infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1829  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1830  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1831  if (savings == 1) {
1832  cuddLevelQueueQuit(queue);
1833  cuddLevelQueueQuit(localQueue);
1834  return(0);
1835  }
1836  } else {
1837  savings = 1;
1838  }
1839  replace = REPLACE_E;
1840  }
1841  numOnset = impact * minterms;
1842  } else {
1843  DdNode *Ereg = Cudd_Regular(E);
1844  DdNode *TT = cuddT(T);
1845  DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1846  if (T->index == Ereg->index && TT == ET) {
1847  shared = TT;
1848  replace = REPLACE_TT;
1849  } else {
1850  DdNode *TE = cuddE(T);
1851  DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1852  if (T->index == Ereg->index && TE == EE) {
1853  shared = TE;
1854  replace = REPLACE_TE;
1855  } else {
1856  replace = REPLACE_N;
1857  }
1858  }
1859  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1860  savings = computeSavings(dd,node,shared,info,localQueue);
1861  if (shared != NULL) {
1862  NodeData *infoS;
1863  (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1864  if (Cudd_IsComplement(shared)) {
1865  numOnset -= (infoS->mintermsN * impactP +
1866  infoS->mintermsP * impactN)/2.0;
1867  } else {
1868  numOnset -= (infoS->mintermsP * impactP +
1869  infoS->mintermsN * impactN)/2.0;
1870  }
1871  savings--;
1872  }
1873  }
1874 
1875  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1876 #if 0
1877  if (replace == REPLACE_T || replace == REPLACE_E)
1878  (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1879  node, impact, numOnset, savings);
1880  else
1881  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1882  node, impactP, impactN, numOnset, savings);
1883 #endif
1884  if ((1 - numOnset / info->minterms) >
1885  quality * (1 - (double) savings / info->size)) {
1886  infoN->replace = (char) replace;
1887  info->size -= savings;
1888  info->minterms -=numOnset;
1889 #if 0
1890  (void) printf("remap(%d): new size = %d new minterms = %g\n",
1891  replace, info->size, info->minterms);
1892 #endif
1893  if (replace == REPLACE_N) {
1894  savings -= updateRefs(dd,node,NULL,info,localQueue);
1895  } else if (replace == REPLACE_T) {
1896  savings -= updateRefs(dd,node,E,info,localQueue);
1897  } else if (replace == REPLACE_E) {
1898  savings -= updateRefs(dd,node,T,info,localQueue);
1899  } else {
1900 #ifdef DD_DEBUG
1901  assert(replace == REPLACE_TT || replace == REPLACE_TE);
1902 #endif
1903  savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1904  }
1905  assert(savings == 0);
1906  } else {
1907  replace = NOTHING;
1908  }
1909  if (replace == REPLACE_N) continue;
1910  if ((replace == REPLACE_E || replace == NOTHING) &&
1911  !cuddIsConstant(cuddT(node))) {
1912  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1913  cuddI(dd,cuddT(node)->index));
1914  if (replace == REPLACE_E) {
1915  item->impactP += impactP;
1916  item->impactN += impactN;
1917  } else {
1918  item->impactP += impactP/2.0;
1919  item->impactN += impactN/2.0;
1920  }
1921  }
1922  if ((replace == REPLACE_T || replace == NOTHING) &&
1923  !Cudd_IsConstant(cuddE(node))) {
1924  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1925  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1926  if (Cudd_IsComplement(cuddE(node))) {
1927  if (replace == REPLACE_T) {
1928  item->impactP += impactN;
1929  item->impactN += impactP;
1930  } else {
1931  item->impactP += impactN/2.0;
1932  item->impactN += impactP/2.0;
1933  }
1934  } else {
1935  if (replace == REPLACE_T) {
1936  item->impactP += impactP;
1937  item->impactN += impactN;
1938  } else {
1939  item->impactP += impactP/2.0;
1940  item->impactN += impactN/2.0;
1941  }
1942  }
1943  }
1944  if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1945  !Cudd_IsConstant(shared)) {
1946  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1947  cuddI(dd,Cudd_Regular(shared)->index));
1948  if (Cudd_IsComplement(shared)) {
1949  if (replace == REPLACE_T) {
1950  item->impactP += impactN;
1951  item->impactN += impactP;
1952  } else {
1953  item->impactP += impactN/2.0;
1954  item->impactN += impactP/2.0;
1955  }
1956  } else {
1957  if (replace == REPLACE_T) {
1958  item->impactP += impactP;
1959  item->impactN += impactN;
1960  } else {
1961  item->impactP += impactP/2.0;
1962  item->impactN += impactN/2.0;
1963  }
1964  }
1965  }
1966  }
1967 
1968  cuddLevelQueueQuit(queue);
1969  cuddLevelQueueQuit(localQueue);
1970  return(1);
1971 
1972 } /* end of BAmarkNodes */
1973 
1974 
1975 /**Function********************************************************************
1976 
1977  Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]
1978 
1979  Description [Builds the subset BDDfor cuddRemapUnderApprox. Based
1980  on the info table, performs remapping or replacement at selected
1981  nodes. Returns a pointer to the result if successful; NULL
1982  otherwise.]
1983 
1984  SideEffects [None]
1985 
1986  SeeAlso [cuddRemapUnderApprox]
1987 
1988 ******************************************************************************/
1989 static DdNode *
1991  DdManager * dd /* DD manager */,
1992  DdNode * node /* current node */,
1993  ApproxInfo * info /* node info */)
1994 {
1995  DdNode *Nt, *Ne, *N, *t, *e, *r;
1996  NodeData *infoN;
1997 
1998  if (Cudd_IsConstant(node))
1999  return(node);
2000 
2001  N = Cudd_Regular(node);
2002 
2003  Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
2004  Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
2005 
2006  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
2007  if (N == node ) {
2008  if (infoN->resultP != NULL) {
2009  return(infoN->resultP);
2010  }
2011  } else {
2012  if (infoN->resultN != NULL) {
2013  return(infoN->resultN);
2014  }
2015  }
2016  if (infoN->replace == REPLACE_T) {
2017  r = RAbuildSubset(dd, Ne, info);
2018  return(r);
2019  } else if (infoN->replace == REPLACE_E) {
2020  r = RAbuildSubset(dd, Nt, info);
2021  return(r);
2022  } else if (infoN->replace == REPLACE_N) {
2023  return(info->zero);
2024  } else if (infoN->replace == REPLACE_TT) {
2025  DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
2026  Cudd_IsComplement(node));
2027  int index = cuddT(N)->index;
2028  e = info->zero;
2029  t = RAbuildSubset(dd, Ntt, info);
2030  if (t == NULL) {
2031  return(NULL);
2032  }
2033  cuddRef(t);
2034  if (Cudd_IsComplement(t)) {
2035  t = Cudd_Not(t);
2036  e = Cudd_Not(e);
2037  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2038  if (r == NULL) {
2039  Cudd_RecursiveDeref(dd, t);
2040  return(NULL);
2041  }
2042  r = Cudd_Not(r);
2043  } else {
2044  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2045  if (r == NULL) {
2046  Cudd_RecursiveDeref(dd, t);
2047  return(NULL);
2048  }
2049  }
2050  cuddDeref(t);
2051  return(r);
2052  } else if (infoN->replace == REPLACE_TE) {
2053  DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
2054  Cudd_IsComplement(node));
2055  int index = cuddT(N)->index;
2056  t = info->one;
2057  e = RAbuildSubset(dd, Nte, info);
2058  if (e == NULL) {
2059  return(NULL);
2060  }
2061  cuddRef(e);
2062  e = Cudd_Not(e);
2063  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2064  if (r == NULL) {
2065  Cudd_RecursiveDeref(dd, e);
2066  return(NULL);
2067  }
2068  r =Cudd_Not(r);
2069  cuddDeref(e);
2070  return(r);
2071  }
2072  } else {
2073  (void) fprintf(dd->err,
2074  "Something is wrong, ought to be in info table\n");
2076  return(NULL);
2077  }
2078 
2079  t = RAbuildSubset(dd, Nt, info);
2080  if (t == NULL) {
2081  return(NULL);
2082  }
2083  cuddRef(t);
2084 
2085  e = RAbuildSubset(dd, Ne, info);
2086  if (e == NULL) {
2087  Cudd_RecursiveDeref(dd,t);
2088  return(NULL);
2089  }
2090  cuddRef(e);
2091 
2092  if (Cudd_IsComplement(t)) {
2093  t = Cudd_Not(t);
2094  e = Cudd_Not(e);
2095  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2096  if (r == NULL) {
2097  Cudd_RecursiveDeref(dd, e);
2098  Cudd_RecursiveDeref(dd, t);
2099  return(NULL);
2100  }
2101  r = Cudd_Not(r);
2102  } else {
2103  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2104  if (r == NULL) {
2105  Cudd_RecursiveDeref(dd, e);
2106  Cudd_RecursiveDeref(dd, t);
2107  return(NULL);
2108  }
2109  }
2110  cuddDeref(t);
2111  cuddDeref(e);
2112 
2113  if (N == node) {
2114  infoN->resultP = r;
2115  } else {
2116  infoN->resultN = r;
2117  }
2118 
2119  return(r);
2120 
2121 } /* end of RAbuildSubset */
2122 
2123 
2124 /**Function********************************************************************
2125 
2126  Synopsis [Finds don't care nodes.]
2127 
2128  Description [Finds don't care nodes by traversing f and b in parallel.
2129  Returns the care status of the visited f node if successful; CARE_ERROR
2130  otherwise.]
2131 
2132  SideEffects [None]
2133 
2134  SeeAlso [cuddBiasedUnderApprox]
2135 
2136 ******************************************************************************/
2137 static int
2139  DdManager *dd,
2140  DdNode *f,
2141  DdNode *b,
2142  ApproxInfo *info,
2143  DdHashTable *cache)
2144 {
2145  DdNode *one, *zero, *res;
2146  DdNode *Ft, *Fe, *B, *Bt, *Be;
2147  unsigned int topf, topb;
2148  NodeData *infoF;
2149  int careT, careE;
2150 
2151  one = DD_ONE(dd);
2152  zero = Cudd_Not(one);
2153 
2154  if (! st__lookup(info->table, (const char *)f, (char **)&infoF))
2155  return(CARE_ERROR);
2156  if (f == one) return(TOTAL_CARE);
2157  if (b == zero) return(infoF->care);
2158  if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
2159 
2160  if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
2161  (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
2162  if (res->ref == 0) {
2163  cache->manager->dead++;
2164  cache->manager->constants.dead++;
2165  }
2166  return(infoF->care);
2167  }
2168 
2169  topf = dd->perm[f->index];
2170  B = Cudd_Regular(b);
2171  topb = cuddI(dd,B->index);
2172  if (topf <= topb) {
2173  Ft = cuddT(f); Fe = cuddE(f);
2174  } else {
2175  Ft = Fe = f;
2176  }
2177  if (topb <= topf) {
2178  /* We know that b is not constant because f is not. */
2179  Bt = cuddT(B); Be = cuddE(B);
2180  if (Cudd_IsComplement(b)) {
2181  Bt = Cudd_Not(Bt);
2182  Be = Cudd_Not(Be);
2183  }
2184  } else {
2185  Bt = Be = b;
2186  }
2187 
2188  careT = BAapplyBias(dd, Ft, Bt, info, cache);
2189  if (careT == CARE_ERROR)
2190  return(CARE_ERROR);
2191  careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
2192  if (careE == CARE_ERROR)
2193  return(CARE_ERROR);
2194  if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2195  infoF->care = TOTAL_CARE;
2196  } else {
2197  infoF->care = CARE;
2198  }
2199 
2200  if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
2201  ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
2202  cuddSatDec(fanout);
2203  if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
2204  return(CARE_ERROR);
2205  }
2206  }
2207  return(infoF->care);
2208 
2209 } /* end of BAapplyBias */
2210 
2211 
2213 
char * memset()
DdHalfWord ref
Definition: cudd.h:280
void st__free_table(st__table *table)
Definition: st.c:81
#define cuddRef(n)
Definition: cuddInt.h:584
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
static int UAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality)
Definition: cuddApprox.c:1152
struct LocalQueueItem LocalQueueItem
#define cuddDeref(n)
Definition: cuddInt.h:604
static int updateRefs(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1073
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
static int BAapplyBias(DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)
Definition: cuddApprox.c:2138
static int computeSavings(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1001
static NodeData * gatherInfoAux(DdNode *node, ApproxInfo *info, int parity)
Definition: cuddApprox.c:837
DdNode * Cudd_BiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:413
DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:511
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
#define CARE_ERROR
Definition: cuddApprox.c:102
DdManager * manager
Definition: cuddInt.h:313
DdNode * Cudd_UnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:228
int size
Definition: cuddInt.h:361
#define Cudd_IsConstant(node)
Definition: cudd.h:352
#define Cudd_Regular(node)
Definition: cudd.h:397
struct GlobalQueueItem * cnext
Definition: cuddApprox.c:149
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
FILE * err
Definition: cuddInt.h:442
double max
Definition: cuddApprox.c:137
static DdNode * UAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1276
struct ApproxInfo ApproxInfo
double minterms
Definition: cuddApprox.c:139
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
void cuddLevelQueueQuit(DdLevelQueue *queue)
Definition: cuddLevelQ.c:244
#define REPLACE_TE
Definition: cuddApprox.c:97
#define REPLACE_E
Definition: cuddApprox.c:94
DdNode * node
Definition: cuddApprox.c:150
#define DBL_MAX_EXP
Definition: cuddApprox.c:79
static ApproxInfo * gatherInfo(DdManager *dd, DdNode *node, int numVars, int parity)
Definition: cuddApprox.c:907
int functionRef
Definition: cuddApprox.c:123
DdNode * resultP
Definition: cuddApprox.c:127
double mintermsP
Definition: cuddApprox.c:121
DdNode * resultN
Definition: cuddApprox.c:128
DdNode * zero
Definition: cuddApprox.c:133
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
unsigned int initSlots
Definition: cuddInt.h:379
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:691
int reordered
Definition: cuddInt.h:409
unsigned int dead
Definition: cuddInt.h:371
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets)
Definition: cuddLevelQ.c:169
char care
Definition: cuddApprox.c:124
struct GlobalQueueItem GlobalQueueItem
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdNode * Cudd_RemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:320
unsigned int dead
Definition: cuddInt.h:332
DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:601
static DdNode * one
Definition: cuddDecomp.c:112
FILE * out
Definition: cuddInt.h:441
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
Definition: st.h:52
double mintermsN
Definition: cuddApprox.c:122
#define REPLACE_N
Definition: cuddApprox.c:95
DdNode * Cudd_OverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:275
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define cuddIsConstant(node)
Definition: cuddInt.h:620
#define TOTAL_CARE
Definition: cuddApprox.c:101
static int BAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:1673
#define REPLACE_TT
Definition: cuddApprox.c:96
DdNode * one
Definition: cuddApprox.c:132
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
struct LocalQueueItem * cnext
Definition: cuddApprox.c:157
st__table * table
Definition: cuddApprox.c:135
void cuddHashTableQuit(DdHashTable *hash)
Definition: cuddLCache.c:595
#define cuddT(node)
Definition: cuddInt.h:636
void * first
Definition: cuddInt.h:509
struct NodeData NodeData
#define st__OUT_OF_MEM
Definition: st.h:113
int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
Definition: cuddLCache.c:874
static char rcsid[] DD_UNUSED
Definition: cuddApprox.c:171
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define TRUE
Definition: cudd.h:88
static int RAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality)
Definition: cuddApprox.c:1371
#define cuddI(dd, index)
Definition: cuddInt.h:686
#define DD_DEBUG
Definition: cuddPriority.c:88
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
struct GlobalQueueItem * next
Definition: cuddApprox.c:148
DdNode * Cudd_RemapOverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:366
struct LocalQueueItem * next
Definition: cuddApprox.c:156
DdNode * Cudd_BiasedOverApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:463
#define REPLACE_T
Definition: cuddApprox.c:93
#define CARE
Definition: cuddApprox.c:100
short int parity
Definition: cuddApprox.c:126
DdHalfWord index
Definition: cudd.h:279
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g)
Definition: cuddLCache.c:928
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
static DdNode * RAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1990
#define cuddE(node)
Definition: cuddInt.h:652
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
static void updateParity(DdNode *node, ApproxInfo *info, int newparity)
Definition: cuddApprox.c:795
#define cuddSatDec(x)
Definition: cuddInt.h:896
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Definition: cuddLCache.c:538
NodeData * page
Definition: cuddApprox.c:134
#define assert(ex)
Definition: util_old.h:213
DdSubtable constants
Definition: cuddInt.h:367
static int result
Definition: cuddGenetic.c:125
DdNode * node
Definition: cuddApprox.c:158
#define DD_ONE(dd)
Definition: cuddInt.h:911
int * perm
Definition: cuddInt.h:386
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
int st__ptrhash(const char *, int)
Definition: st.c:468
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
static DdNode * zero
Definition: cuddApa.c:100
pset minterms()
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
char replace
Definition: cuddApprox.c:125
#define NOTHING
Definition: cuddApprox.c:92