source: vis_dev/glu-2.3/src/cuBdd/cuddApprox.c @ 43

Last change on this file since 43 was 13, checked in by cecile, 13 years ago

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