cuddApprox.c 76.2 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10
/**CFile***********************************************************************

  FileName    [cuddApprox.c]

  PackageName [cudd]

  Synopsis    [Procedures to approximate a given BDD.]

  Description [External procedures provided by this module:
                <ul>
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
                <li> Cudd_UnderApprox()
                <li> Cudd_OverApprox()
                <li> Cudd_RemapUnderApprox()
                <li> Cudd_RemapOverApprox()
                <li> Cudd_BiasedUnderApprox()
                <li> Cudd_BiasedOverApprox()
                </ul>
               Internal procedures included in this module:
                <ul>
                <li> cuddUnderApprox()
                <li> cuddRemapUnderApprox()
                <li> cuddBiasedUnderApprox()
                </ul>
               Static procedures included in this module:
                <ul>
                <li> gatherInfoAux()
                <li> gatherInfo()
                <li> computeSavings()
                <li> UAmarkNodes()
                <li> UAbuildSubset()
                <li> updateRefs()
                <li> RAmarkNodes()
                <li> BAmarkNodes()
                <li> RAbuildSubset()
                </ul>
                ]
Alan Mishchenko committed
37 38 39 40 41

  SeeAlso     [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]

  Author      [Fabio Somenzi]

42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]
Alan Mishchenko committed
73 74 75 76 77 78 79 80

******************************************************************************/

#ifdef __STDC__
#include <float.h>
#else
#define DBL_MAX_EXP 1024
#endif
81
#include "misc/util/util_hack.h"
Alan Mishchenko committed
82 83
#include "cuddInt.h"

84 85 86
ABC_NAMESPACE_IMPL_START


87

Alan Mishchenko committed
88 89 90 91
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

92 93 94 95 96 97
#define NOTHING         0
#define REPLACE_T       1
#define REPLACE_E       2
#define REPLACE_N       3
#define REPLACE_TT      4
#define REPLACE_TE      5
Alan Mishchenko committed
98

99 100 101 102
#define DONT_CARE       0
#define CARE            1
#define TOTAL_CARE      2
#define CARE_ERROR      3
Alan Mishchenko committed
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/* Data structure to store the information on each node. It keeps the
** number of minterms of the function rooted at this node in terms of
** the number of variables specified by the user; the number of
** minterms of the complement; the impact of the number of minterms of
** this function on the number of minterms of the root function; the
** reference count of the node from within the root function; the
** reference count of the node from an internal node; and the flag
** that says whether the node should be replaced and how. */
typedef struct NodeData {
121 122 123 124 125 126 127 128
    double mintermsP;           /* minterms for the regular node */
    double mintermsN;           /* minterms for the complemented node */
    int functionRef;            /* references from within this function */
    char care;                  /* node intersects care set */
    char replace;               /* replacement decision */
    short int parity;           /* 1: even; 2: odd; 3: both */
    DdNode *resultP;            /* result for even parity */
    DdNode *resultN;            /* result for odd parity */
Alan Mishchenko committed
129 130 131
} NodeData;

typedef struct ApproxInfo {
132 133 134
    DdNode *one;                /* one constant */
    DdNode *zero;               /* BDD zero constant */
    NodeData *page;             /* per-node information */
135
    st__table *table;            /* hash table to access the per-node info */
136 137 138 139
    int index;                  /* index of the current node */
    double max;                 /* max number of minterms */
    int size;                   /* how many nodes are left */
    double minterms;            /* how many minterms are left */
Alan Mishchenko committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
} ApproxInfo;

/* Item of the queue used in the levelized traversal of the BDD. */
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
typedef struct GlobalQueueItem {
    struct GlobalQueueItem *next;
    struct GlobalQueueItem *cnext;
    DdNode *node;
    double impactP;
    double impactN;
} GlobalQueueItem;
 
typedef struct LocalQueueItem {
    struct LocalQueueItem *next;
    struct LocalQueueItem *cnext;
    DdNode *node;
    int localRef;
} LocalQueueItem;
#ifdef __osf__
#pragma pointer_size restore
#endif

    
/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
171
static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $";
Alan Mishchenko committed
172 173 174 175 176 177 178 179 180 181 182 183
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

184 185 186 187 188 189 190 191 192 193 194
static void updateParity (DdNode *node, ApproxInfo *info, int newparity);
static NodeData * gatherInfoAux (DdNode *node, ApproxInfo *info, int parity);
static ApproxInfo * gatherInfo (DdManager *dd, DdNode *node, int numVars, int parity);
static int computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
static int updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
static int UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality);
static DdNode * UAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
static int RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality);
static int BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0);
static DdNode * RAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
static int BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache);
Alan Mishchenko committed
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Extracts a dense subset from a BDD with Shiple's
  underapproximation method.]

  Description [Extracts a dense subset from a BDD. This procedure uses
  a variant of Tom Shiple's underapproximation method. The main
  difference from the original method is that density is used as cost
  function.  Returns a pointer to the BDD of the subset if
  successful. NULL if the procedure runs out of memory. The parameter
  numVars is the maximum number of variables to be used in minterm
  calculation.  The optimal number should be as close as possible to
  the size of the support of f.  However, it is safe to pass the value
  returned by Cudd_ReadSize for numVars when the number of variables
  is under 1023.  If numVars is larger than 1023, it will cause
  overflow. If a 0 parameter is passed then the procedure will compute
  a value which will avoid overflow but will cause underflow with 2046
  variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_UnderApprox(
  DdManager * dd /* manager */,
  DdNode * f /* function to be subset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* when to stop approximation */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdNode *subset;

    do {
239 240
        dd->reordered = 0;
        subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
Alan Mishchenko committed
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_UnderApprox */


/**Function********************************************************************

  Synopsis    [Extracts a dense superset from a BDD with Shiple's
  underapproximation method.]

  Description [Extracts a dense superset from a BDD. The procedure is
  identical to the underapproximation procedure except for the fact that it
  works on the complement of the given function. Extracting the subset
  of the complement function is equivalent to extracting the superset
  of the function.
  Returns a pointer to the BDD of the superset if successful. NULL if
  intermediate result causes the procedure to run out of memory. The
  parameter numVars is the maximum number of variables to be used in
  minterm calculation.  The optimal number
  should be as close as possible to the size of the support of f.
  However, it is safe to pass the value returned by Cudd_ReadSize for
  numVars when the number of variables is under 1023.  If numVars is
  larger than 1023, it will overflow. If a 0 parameter is passed then
  the procedure will compute a value which will avoid overflow but
  will cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_OverApprox(
  DdManager * dd /* manager */,
  DdNode * f /* function to be superset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* when to stop approximation */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
287 288
        dd->reordered = 0;
        subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
Alan Mishchenko committed
289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_OverApprox */


/**Function********************************************************************

  Synopsis [Extracts a dense subset from a BDD with the remapping
  underapproximation method.]

  Description [Extracts a dense subset from a BDD. This procedure uses
  a remapping technique and density as the cost function.
  Returns a pointer to the BDD of the subset if
  successful. NULL if the procedure runs out of memory. The parameter
  numVars is the maximum number of variables to be used in minterm
  calculation.  The optimal number should be as close as possible to
  the size of the support of f.  However, it is safe to pass the value
  returned by Cudd_ReadSize for numVars when the number of variables
  is under 1023.  If numVars is larger than 1023, it will cause
  overflow. If a 0 parameter is passed then the procedure will compute
  a value which will avoid overflow but will cause underflow with 2046
  variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_RemapUnderApprox(
  DdManager * dd /* manager */,
  DdNode * f /* function to be subset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* when to stop approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdNode *subset;

    do {
330 331
        dd->reordered = 0;
        subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
Alan Mishchenko committed
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_RemapUnderApprox */


/**Function********************************************************************

  Synopsis    [Extracts a dense superset from a BDD with the remapping
  underapproximation method.]

  Description [Extracts a dense superset from a BDD. The procedure is
  identical to the underapproximation procedure except for the fact that it
  works on the complement of the given function. Extracting the subset
  of the complement function is equivalent to extracting the superset
  of the function.
  Returns a pointer to the BDD of the superset if successful. NULL if
  intermediate result causes the procedure to run out of memory. The
  parameter numVars is the maximum number of variables to be used in
  minterm calculation.  The optimal number
  should be as close as possible to the size of the support of f.
  However, it is safe to pass the value returned by Cudd_ReadSize for
  numVars when the number of variables is under 1023.  If numVars is
  larger than 1023, it will overflow. If a 0 parameter is passed then
  the procedure will compute a value which will avoid overflow but
  will cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_RemapOverApprox(
  DdManager * dd /* manager */,
  DdNode * f /* function to be superset */,
  int  numVars /* number of variables in the support of f */,
  int  threshold /* when to stop approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
377 378
        dd->reordered = 0;
        subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
Alan Mishchenko committed
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_RemapOverApprox */


/**Function********************************************************************

  Synopsis [Extracts a dense subset from a BDD with the biased
  underapproximation method.]

  Description [Extracts a dense subset from a BDD. This procedure uses
  a biased remapping technique and density as the cost function. The bias
  is a function. This procedure tries to approximate where the bias is 0
  and preserve the given function where the bias is 1.
  Returns a pointer to the BDD of the subset if
  successful. NULL if the procedure runs out of memory. The parameter
  numVars is the maximum number of variables to be used in minterm
  calculation.  The optimal number should be as close as possible to
  the size of the support of f.  However, it is safe to pass the value
  returned by Cudd_ReadSize for numVars when the number of variables
  is under 1023.  If numVars is larger than 1023, it will cause
  overflow. If a 0 parameter is passed then the procedure will compute
  a value which will avoid overflow but will cause underflow with 2046
  variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox
  Cudd_RemapUnderApprox Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_BiasedUnderApprox(
  DdManager *dd /* manager */,
  DdNode *f /* function to be subset */,
  DdNode *b /* bias function */,
  int numVars /* number of variables in the support of f */,
  int threshold /* when to stop approximation */,
  double quality1 /* minimum improvement for accepted changes when b=1 */,
  double quality0 /* minimum improvement for accepted changes when b=0 */)
{
    DdNode *subset;

    do {
425 426 427
        dd->reordered = 0;
        subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
                                       quality0);
Alan Mishchenko committed
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
    } while (dd->reordered == 1);

    return(subset);

} /* end of Cudd_BiasedUnderApprox */


/**Function********************************************************************

  Synopsis    [Extracts a dense superset from a BDD with the biased
  underapproximation method.]

  Description [Extracts a dense superset from a BDD. The procedure is
  identical to the underapproximation procedure except for the fact that it
  works on the complement of the given function. Extracting the subset
  of the complement function is equivalent to extracting the superset
  of the function.
  Returns a pointer to the BDD of the superset if successful. NULL if
  intermediate result causes the procedure to run out of memory. The
  parameter numVars is the maximum number of variables to be used in
  minterm calculation.  The optimal number
  should be as close as possible to the size of the support of f.
  However, it is safe to pass the value returned by Cudd_ReadSize for
  numVars when the number of variables is under 1023.  If numVars is
  larger than 1023, it will overflow. If a 0 parameter is passed then
  the procedure will compute a value which will avoid overflow but
  will cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
  Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_BiasedOverApprox(
  DdManager *dd /* manager */,
  DdNode *f /* function to be superset */,
  DdNode *b /* bias function */,
  int numVars /* number of variables in the support of f */,
  int threshold /* when to stop approximation */,
  double quality1 /* minimum improvement for accepted changes when b=1*/,
  double quality0 /* minimum improvement for accepted changes when b=0 */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    do {
476 477 478
        dd->reordered = 0;
        subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
                                      quality0);
Alan Mishchenko committed
479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
    } while (dd->reordered == 1);
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_BiasedOverApprox */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Applies Tom Shiple's underappoximation algorithm.]

  Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
  in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether its elimination increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_UnderApprox]

******************************************************************************/
DdNode *
cuddUnderApprox(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold under which approximation stops */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
524 525
        fprintf(dd->err, "Cannot subset, nil object\n");
        return(NULL);
Alan Mishchenko committed
526 527 528
    }

    if (Cudd_IsConstant(f)) {
529
        return(f);
Alan Mishchenko committed
530 531 532 533 534
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, safe);
    if (info == NULL) {
535 536 537
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
538 539 540 541 542
    }

    /* Mark nodes that should be replaced by zero. */
    result = UAmarkNodes(dd, f, info, threshold, safe, quality);
    if (result == 0) {
543 544
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        ABC_FREE(info->page);
545
        st__free_table(info->table);
546 547 548
        ABC_FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
549 550 551 552 553 554
    }

    /* Build the result. */
    subset = UAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
555 556
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
Alan Mishchenko committed
557
#endif
Alan Mishchenko committed
558
    ABC_FREE(info->page);
559
    st__free_table(info->table);
Alan Mishchenko committed
560
    ABC_FREE(info);
Alan Mishchenko committed
561 562 563

#ifdef DD_DEBUG
    if (subset != NULL) {
564
        cuddRef(subset);
Alan Mishchenko committed
565
#if 0
566 567
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
Alan Mishchenko committed
568
#endif
569 570 571 572 573
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
        }
        cuddDeref(subset);
Alan Mishchenko committed
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612
    }
#endif
    return(subset);

} /* end of cuddUnderApprox */


/**Function********************************************************************

  Synopsis    [Applies the remapping underappoximation algorithm.]

  Description [Applies the remapping underappoximation algorithm.
  Proceeds in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether remapping increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_RemapUnderApprox]

******************************************************************************/
DdNode *
cuddRemapUnderApprox(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold under which approximation stops */,
  double  quality /* minimum improvement for accepted changes */)
{
    ApproxInfo *info;
    DdNode *subset;
    int result;

    if (f == NULL) {
613 614 615
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
Alan Mishchenko committed
616 617 618
    }

    if (Cudd_IsConstant(f)) {
619
        return(f);
Alan Mishchenko committed
620 621 622 623 624
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
625 626 627
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
628 629 630 631 632
    }

    /* Mark nodes that should be replaced by zero. */
    result = RAmarkNodes(dd, f, info, threshold, quality);
    if (result == 0) {
633 634
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        ABC_FREE(info->page);
635
        st__free_table(info->table);
636 637 638
        ABC_FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
639 640 641 642 643 644
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
645 646
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
Alan Mishchenko committed
647
#endif
Alan Mishchenko committed
648
    ABC_FREE(info->page);
649
    st__free_table(info->table);
Alan Mishchenko committed
650
    ABC_FREE(info);
Alan Mishchenko committed
651 652 653

#ifdef DD_DEBUG
    if (subset != NULL) {
654
        cuddRef(subset);
Alan Mishchenko committed
655
#if 0
656 657
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
Alan Mishchenko committed
658
#endif
659 660 661 662 663
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
        }
        cuddDeref(subset);
        dd->errorCode = CUDD_INTERNAL_ERROR;
Alan Mishchenko committed
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
    }
#endif
    return(subset);

} /* end of cuddRemapUnderApprox */


/**Function********************************************************************

  Synopsis    [Applies the biased remapping underappoximation algorithm.]

  Description [Applies the biased remapping underappoximation algorithm.
  Proceeds in three phases:
  <ul>
  <li> collect information on each node in the BDD; this is done via DFS.
  <li> traverse the BDD in top-down fashion and compute for each node
  whether remapping increases density.
  <li> traverse the BDD via DFS and actually perform the elimination.
  </ul>
  Returns the approximated BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_BiasedUnderApprox]

******************************************************************************/
DdNode *
cuddBiasedUnderApprox(
  DdManager *dd /* DD manager */,
  DdNode *f /* current DD */,
  DdNode *b /* bias function */,
  int numVars /* maximum number of variables */,
  int threshold /* threshold under which approximation stops */,
  double quality1 /* minimum improvement for accepted changes when b=1 */,
698
  double quality0 /* minimum improvement for accepted changes when b=0 */)
Alan Mishchenko committed
699 700 701 702
{
    ApproxInfo *info;
    DdNode *subset;
    int result;
703
    DdHashTable *cache;
Alan Mishchenko committed
704 705

    if (f == NULL) {
706 707 708
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
Alan Mishchenko committed
709 710 711
    }

    if (Cudd_IsConstant(f)) {
712
        return(f);
Alan Mishchenko committed
713 714 715 716 717
    }

    /* Create table where node data are accessible via a hash table. */
    info = gatherInfo(dd, f, numVars, TRUE);
    if (info == NULL) {
718 719 720
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
721 722 723 724 725
    }

    cache = cuddHashTableInit(dd,2,2);
    result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
    if (result == CARE_ERROR) {
726 727 728
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        cuddHashTableQuit(cache);
        ABC_FREE(info->page);
729
        st__free_table(info->table);
730 731 732
        ABC_FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
733 734 735 736 737 738
    }
    cuddHashTableQuit(cache);

    /* Mark nodes that should be replaced by zero. */
    result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
    if (result == 0) {
739 740
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        ABC_FREE(info->page);
741
        st__free_table(info->table);
742 743 744
        ABC_FREE(info);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
745 746 747 748 749 750
    }

    /* Build the result. */
    subset = RAbuildSubset(dd, f, info);
#if 1
    if (subset && info->size < Cudd_DagSize(subset))
751 752
        (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                       info->size, Cudd_DagSize(subset));
Alan Mishchenko committed
753
#endif
Alan Mishchenko committed
754
    ABC_FREE(info->page);
755
    st__free_table(info->table);
Alan Mishchenko committed
756
    ABC_FREE(info);
Alan Mishchenko committed
757 758 759

#ifdef DD_DEBUG
    if (subset != NULL) {
760
        cuddRef(subset);
Alan Mishchenko committed
761
#if 0
762 763
        (void) Cudd_DebugCheck(dd);
        (void) Cudd_CheckKeys(dd);
Alan Mishchenko committed
764
#endif
765 766 767 768 769
        if (!Cudd_bddLeq(dd, subset, f)) {
            (void) fprintf(dd->err, "Wrong subset\n");
        }
        cuddDeref(subset);
        dd->errorCode = CUDD_INTERNAL_ERROR;
Alan Mishchenko committed
770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802
    }
#endif
    return(subset);

} /* end of cuddBiasedUnderApprox */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Recursively update the parity of the paths reaching a node.]

  Description [Recursively update the parity of the paths reaching a node.
  Assumes that node is regular and propagates the invariant.]

  SideEffects [None]

  SeeAlso     [gatherInfoAux]

******************************************************************************/
static void
updateParity(
  DdNode * node /* function to analyze */,
  ApproxInfo * info /* info on BDD */,
  int  newparity /* new parity for node */)
{
    NodeData *infoN;
    DdNode *E;

803
    if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) return;
Alan Mishchenko committed
804
    if ((infoN->parity & newparity) != 0) return;
805
    infoN->parity |= (short) newparity;
Alan Mishchenko committed
806 807 808 809
    if (Cudd_IsConstant(node)) return;
    updateParity(cuddT(node),info,newparity);
    E = cuddE(node);
    if (Cudd_IsComplement(E)) {
810
        updateParity(Cudd_Not(E),info,3-newparity);
Alan Mishchenko committed
811
    } else {
812
        updateParity(E,info,newparity);
Alan Mishchenko committed
813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841
    }
    return;

} /* end of updateParity */


/**Function********************************************************************

  Synopsis    [Recursively counts minterms and computes reference counts
  of each node in the BDD.]

  Description [Recursively counts minterms and computes reference
  counts of each node in the BDD.  Similar to the cuddCountMintermAux
  which recursively counts the number of minterms for the dag rooted
  at each node in terms of the total number of variables (max). It assumes
  that the node pointer passed to it is regular and it maintains the
  invariant.]

  SideEffects [None]

  SeeAlso     [gatherInfo]

******************************************************************************/
static NodeData *
gatherInfoAux(
  DdNode * node /* function to analyze */,
  ApproxInfo * info /* info on BDD */,
  int  parity /* gather parity information */)
{
842
    DdNode      *N, *Nt, *Ne;
Alan Mishchenko committed
843 844 845 846 847
    NodeData    *infoN, *infoT, *infoE;

    N = Cudd_Regular(node);

    /* Check whether entry for this node exists. */
848
    if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
849 850 851 852 853
        if (parity) {
            /* Update parity and propagate. */
            updateParity(N, info, 1 +  (int) Cudd_IsComplement(node));
        }
        return(infoN);
Alan Mishchenko committed
854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869
    }

    /* Compute the cofactors. */
    Nt = Cudd_NotCond(cuddT(N), N != node);
    Ne = Cudd_NotCond(cuddE(N), N != node);

    infoT = gatherInfoAux(Nt, info, parity);
    if (infoT == NULL) return(NULL);
    infoE = gatherInfoAux(Ne, info, parity);
    if (infoE == NULL) return(NULL);

    infoT->functionRef++;
    infoE->functionRef++;

    /* Point to the correct location in the page. */
    infoN = &(info->page[info->index++]);
870
    infoN->parity |= (short) (1 + Cudd_IsComplement(node));
Alan Mishchenko committed
871 872 873 874

    infoN->mintermsP = infoT->mintermsP/2;
    infoN->mintermsN = infoT->mintermsN/2;
    if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
875 876
        infoN->mintermsP += infoE->mintermsN/2;
        infoN->mintermsN += infoE->mintermsP/2;
Alan Mishchenko committed
877
    } else {
878 879
        infoN->mintermsP += infoE->mintermsP/2;
        infoN->mintermsN += infoE->mintermsN/2;
Alan Mishchenko committed
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);
Alan Mishchenko committed
885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912
    }
    return(infoN);

} /* end of gatherInfoAux */


/**Function********************************************************************

  Synopsis    [Gathers information about each node.]

  Description [Counts minterms and computes reference counts of each
  node in the BDD . The minterm count is separately computed for the
  node and its complement. This is to avoid cancellation
  errors. Returns a pointer to the data structure holding the
  information gathered if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox gatherInfoAux]

******************************************************************************/
static ApproxInfo *
gatherInfo(
  DdManager * dd /* manager */,
  DdNode * node /* function to be analyzed */,
  int  numVars /* number of variables node depends on */,
  int  parity /* gather parity information */)
{
913
    ApproxInfo  *info;
Alan Mishchenko committed
914 915 916 917 918 919 920 921
    NodeData *infoTop;

    /* If user did not give numVars value, set it to the maximum
    ** exponent that the pow function can take. The -1 is due to the
    ** discrepancy in the value that pow takes and the value that
    ** log gives.
    */
    if (numVars == 0) {
922
        numVars = DBL_MAX_EXP - 1;
Alan Mishchenko committed
923 924
    }

Alan Mishchenko committed
925
    info = ABC_ALLOC(ApproxInfo,1);
Alan Mishchenko committed
926
    if (info == NULL) {
927 928
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
Alan Mishchenko committed
929 930 931 932 933 934 935 936 937 938
    }
    info->max = pow(2.0,(double) numVars);
    info->one = DD_ONE(dd);
    info->zero = Cudd_Not(info->one);
    info->size = Cudd_DagSize(node);
    /* All the information gathered will be stored in a contiguous
    ** piece of memory, which is allocated here. This can be done
    ** efficiently because we have counted the number of nodes of the
    ** BDD. info->index points to the next available entry in the array
    ** that stores the per-node information. */
Alan Mishchenko committed
939
    info->page = ABC_ALLOC(NodeData,info->size);
Alan Mishchenko committed
940
    if (info->page == NULL) {
941 942 943
        dd->errorCode = CUDD_MEMORY_OUT;
        ABC_FREE(info);
        return(NULL);
Alan Mishchenko committed
944 945
    }
    memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
946
    info->table = st__init_table( st__ptrcmp, st__ptrhash);
Alan Mishchenko committed
947
    if (info->table == NULL) {
948 949 950
        ABC_FREE(info->page);
        ABC_FREE(info);
        return(NULL);
Alan Mishchenko committed
951 952 953 954 955
    }
    /* We visit the DAG in post-order DFS. Hence, the constant node is
    ** in first position, and the root of the DAG is in last position. */

    /* 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 958
        ABC_FREE(info->page);
        ABC_FREE(info);
959
        st__free_table(info->table);
960
        return(NULL);
Alan Mishchenko committed
961 962 963 964 965 966
    }
    info->page[0].mintermsP = info->max;
    info->index = 1;

    infoTop = gatherInfoAux(node,info,parity);
    if (infoTop == NULL) {
967
        ABC_FREE(info->page);
968
        st__free_table(info->table);
969 970
        ABC_FREE(info);
        return(NULL);
Alan Mishchenko committed
971 972
    }
    if (Cudd_IsComplement(node)) {
973
        info->minterms = infoTop->mintermsN;
Alan Mishchenko committed
974
    } else {
975
        info->minterms = infoTop->mintermsP;
Alan Mishchenko committed
976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018
    }

    infoTop->functionRef = 1;
    return(info);

} /* end of gatherInfo */


/**Function********************************************************************

  Synopsis    [Counts the nodes that would be eliminated if a given node
  were replaced by zero.]

  Description [Counts the nodes that would be eliminated if a given
  node were replaced by zero. This procedure uses a queue passed by
  the caller for efficiency: since the queue is left empty at the
  endof the search, it can be reused as is by the next search. Returns
  the count (always striclty positive) if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static int
computeSavings(
  DdManager * dd,
  DdNode * f,
  DdNode * skip,
  ApproxInfo * info,
  DdLevelQueue * queue)
{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    skip = Cudd_Regular(skip);
    /* Insert the given node in the level queue. Its local reference
    ** count is set equal to the function reference count so that the
    ** search will continue from it when it is retrieved. */
    item = (LocalQueueItem *)
1019
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
Alan Mishchenko committed
1020
    if (item == NULL)
1021
        return(0);
1022
    (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
Alan Mishchenko committed
1023 1024 1025 1026
    item->localRef = infoN->functionRef;

    /* Process the queue. */
    while (queue->first != NULL) {
1027 1028 1029 1030
        item = (LocalQueueItem *) queue->first;
        node = item->node;
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
        if (node == skip) continue;
1031
        (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048
        if (item->localRef != infoN->functionRef) {
            /* This node is shared. */
            continue;
        }
        savings++;
        if (!cuddIsConstant(cuddT(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (item == NULL) return(0);
            item->localRef++;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (item == NULL) return(0);
            item->localRef++;
        }
Alan Mishchenko committed
1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of computeSavings */


/**Function********************************************************************

  Synopsis    [Update function reference counts.]

  Description [Update function reference counts to account for replacement.
  Returns the number of nodes saved if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [UAmarkNodes RAmarkNodes]

******************************************************************************/
static int
updateRefs(
  DdManager * dd,
  DdNode * f,
  DdNode * skip,
  ApproxInfo * info,
  DdLevelQueue * queue)
{
    NodeData *infoN;
    LocalQueueItem *item;
    DdNode *node;
    int savings = 0;

    node = Cudd_Regular(f);
    /* Insert the given node in the level queue. Its function reference
    ** count is set equal to 0 so that the search will continue from it
    ** when it is retrieved. */
    item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL)
1091
        return(0);
1092
    (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
Alan Mishchenko committed
1093 1094 1095
    infoN->functionRef = 0;

    if (skip != NULL) {
1096 1097 1098
        /* Increase the function reference count of the node to be skipped
        ** by 1 to account for the node pointing to it that will be created. */
        skip = Cudd_Regular(skip);
1099
        (void) st__lookup(info->table, (const char *)skip, (char **)&infoN);
1100
        infoN->functionRef++;
Alan Mishchenko committed
1101 1102 1103 1104
    }

    /* Process the queue. */
    while (queue->first != NULL) {
1105 1106 1107
        item = (LocalQueueItem *) queue->first;
        node = item->node;
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1108
        (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1109 1110 1111 1112 1113 1114 1115 1116 1117
        if (infoN->functionRef != 0) {
            /* This node is shared or must be skipped. */
            continue;
        }
        savings++;
        if (!cuddIsConstant(cuddT(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (item == NULL) return(0);
1118
            (void) st__lookup(info->table, (const char *)cuddT(node), (char **)&infoN);
1119 1120 1121 1122 1123 1124
            infoN->functionRef--;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (item == NULL) return(0);
1125
            (void) st__lookup(info->table, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN);
1126 1127
            infoN->functionRef--;
        }
Alan Mishchenko committed
1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170
    }

#ifdef DD_DEBUG
    /* At the end of a local search the queue should be empty. */
    assert(queue->size == 0);
#endif
    return(savings);

} /* end of updateRefs */


/**Function********************************************************************

  Synopsis    [Marks nodes for replacement by zero.]

  Description [Marks nodes for replacement by zero. Returns 1 if successful;
  0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static int
UAmarkNodes(
  DdManager * dd /* manager */,
  DdNode * f /* function to be analyzed */,
  ApproxInfo * info /* info on BDD */,
  int  threshold /* when to stop approximating */,
  int  safe /* enforce safe approximation */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN;
    GlobalQueueItem *item;
    DdNode *node;
    double numOnset;
    double impactP, impactN;
    int savings;

#if 0
    (void) printf("initial size = %d initial minterms = %g\n",
1171
                  info->size, info->minterms);
Alan Mishchenko committed
1172 1173 1174
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
1175
        return(0);
Alan Mishchenko committed
1176 1177
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1178
                                    dd->initSlots);
Alan Mishchenko committed
1179
    if (localQueue == NULL) {
1180 1181
        cuddLevelQueueQuit(queue);
        return(0);
Alan Mishchenko committed
1182 1183 1184 1185
    }
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
    if (item == NULL) {
1186 1187 1188
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
Alan Mishchenko committed
1189 1190
    }
    if (Cudd_IsComplement(f)) {
1191 1192
        item->impactP = 0.0;
        item->impactN = 1.0;
Alan Mishchenko committed
1193
    } else {
1194 1195
        item->impactP = 1.0;
        item->impactN = 0.0;
Alan Mishchenko committed
1196 1197
    }
    while (queue->first != NULL) {
1198 1199 1200 1201 1202 1203
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
        node = Cudd_Regular(node);
1204
        (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217
        if (safe && infoN->parity == 3) {
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
        }
        impactP = item->impactP;
        impactN = item->impactN;
        numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
        savings = computeSavings(dd,node,NULL,info,localQueue);
        if (savings == 0) {
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
Alan Mishchenko committed
1218 1219
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
1220 1221
        (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                      node, impactP, impactN, numOnset, savings);
Alan Mishchenko committed
1222
#endif
1223 1224 1225 1226 1227
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = TRUE;
            info->size -= savings;
            info->minterms -=numOnset;
Alan Mishchenko committed
1228
#if 0
1229 1230
            (void) printf("replace: new size = %d new minterms = %g\n",
                          info->size, info->minterms);
Alan Mishchenko committed
1231
#endif
1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251
            savings -= updateRefs(dd,node,NULL,info,localQueue);
            assert(savings == 0);
            continue;
        }
        if (!cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            item->impactP += impactP/2.0;
            item->impactN += impactN/2.0;
        }
        if (!Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                item->impactP += impactN/2.0;
                item->impactN += impactP/2.0;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
Alan Mishchenko committed
1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of UAmarkNodes */


/**Function********************************************************************

  Synopsis    [Builds the subset BDD.] 

  Description [Builds the subset BDD. Based on the info table,
  replaces selected nodes by zero. Returns a pointer to the result if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddUnderApprox]

******************************************************************************/
static DdNode *
UAbuildSubset(
  DdManager * dd /* DD manager */,
  DdNode * node /* current node */,
  ApproxInfo * info /* node info */)
{

    DdNode *Nt, *Ne, *N, *t, *e, *r;
    NodeData *infoN;

    if (Cudd_IsConstant(node))
1286
        return(node);
Alan Mishchenko committed
1287 1288 1289

    N = Cudd_Regular(node);

1290
    if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
1291 1292
        if (infoN->replace == TRUE) {
            return(info->zero);
Alan Mishchenko committed
1293
        }
1294 1295 1296 1297 1298 1299 1300 1301
        if (N == node ) {
            if (infoN->resultP != NULL) {
                return(infoN->resultP);
            }
        } else {
            if (infoN->resultN != NULL) {
                return(infoN->resultN);
            }
Alan Mishchenko committed
1302 1303
        }
    } else {
1304 1305 1306 1307
        (void) fprintf(dd->err,
                       "Something is wrong, ought to be in info table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
        return(NULL);
Alan Mishchenko committed
1308 1309 1310 1311 1312 1313 1314
    }

    Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
    Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));

    t = UAbuildSubset(dd, Nt, info);
    if (t == NULL) {
1315
        return(NULL);
Alan Mishchenko committed
1316 1317 1318 1319 1320
    }
    cuddRef(t);

    e = UAbuildSubset(dd, Ne, info);
    if (e == NULL) {
1321 1322
        Cudd_RecursiveDeref(dd,t);
        return(NULL);
Alan Mishchenko committed
1323 1324 1325 1326
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
1327 1328 1329 1330 1331 1332 1333 1334 1335
        t = Cudd_Not(t);
        e = Cudd_Not(e);
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
        r = Cudd_Not(r);
Alan Mishchenko committed
1336
    } else {
1337 1338 1339 1340 1341 1342
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
Alan Mishchenko committed
1343 1344 1345 1346 1347
    }
    cuddDeref(t);
    cuddDeref(e);

    if (N == node) {
1348
        infoN->resultP = r;
Alan Mishchenko committed
1349
    } else {
1350
        infoN->resultN = r;
Alan Mishchenko committed
1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391
    }

    return(r);

} /* end of UAbuildSubset */


/**Function********************************************************************

  Synopsis    [Marks nodes for remapping.]

  Description [Marks nodes for remapping. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddRemapUnderApprox]

******************************************************************************/
static int
RAmarkNodes(
  DdManager * dd /* manager */,
  DdNode * f /* function to be analyzed */,
  ApproxInfo * info /* info on BDD */,
  int  threshold /* when to stop approximating */,
  double  quality /* minimum improvement for accepted changes */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1392
                  info->size, info->minterms);
Alan Mishchenko committed
1393 1394 1395
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
1396
        return(0);
Alan Mishchenko committed
1397 1398
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1399
                                    dd->initSlots);
Alan Mishchenko committed
1400
    if (localQueue == NULL) {
1401 1402
        cuddLevelQueueQuit(queue);
        return(0);
Alan Mishchenko committed
1403 1404 1405 1406
    }
    /* Enqueue regular pointer to root and initialize impact. */
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *)
1407
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
Alan Mishchenko committed
1408
    if (item == NULL) {
1409 1410 1411
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
Alan Mishchenko committed
1412 1413
    }
    if (Cudd_IsComplement(f)) {
1414 1415
        item->impactP = 0.0;
        item->impactN = 1.0;
Alan Mishchenko committed
1416
    } else {
1417 1418
        item->impactP = 1.0;
        item->impactN = 0.0;
Alan Mishchenko committed
1419 1420 1421 1422 1423 1424
    }
    /* The nodes retrieved here are guaranteed to be non-terminal.
    ** The initial node is not terminal because constant nodes are
    ** dealt with in the calling procedure. Subsequent nodes are inserted
    ** only if they are not terminal. */
    while (queue->first != NULL) {
1425 1426 1427 1428 1429
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
Alan Mishchenko committed
1430
#ifdef DD_DEBUG
1431 1432 1433 1434
        assert(item->impactP >= 0 && item->impactP <= 1.0);
        assert(item->impactN >= 0 && item->impactN <= 1.0);
        assert(!Cudd_IsComplement(node));
        assert(!Cudd_IsConstant(node));
Alan Mishchenko committed
1435
#endif
1436
        if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
Alan Mishchenko committed
1437 1438 1439 1440 1441
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
#ifdef DD_DEBUG
1442
        assert(infoN->parity >= 1 && infoN->parity <= 3);
Alan Mishchenko committed
1443
#endif
1444 1445 1446 1447 1448 1449 1450
        if (infoN->parity == 3) {
            /* This node can be reached through paths of different parity.
            ** It is not safe to replace it, because remapping will give
            ** an incorrect result, while replacement by 0 may cause node
            ** splitting. */
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
Alan Mishchenko committed
1451
        }
1452 1453 1454 1455 1456 1457 1458 1459 1460 1461
        T = cuddT(node);
        E = cuddE(node);
        shared = NULL;
        impactP = item->impactP;
        impactN = item->impactN;
        if (Cudd_bddLeq(dd,T,E)) {
            /* Here we know that E is regular. */
#ifdef DD_DEBUG
            assert(!Cudd_IsComplement(E));
#endif
1462 1463
            (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
            (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
Alan Mishchenko committed
1495
            }
1496 1497 1498 1499
            numOnset = impact * minterms;
        } else if (Cudd_bddLeq(dd,E,T)) {
            /* Here E may be complemented. */
            DdNode *Ereg = Cudd_Regular(E);
1500 1501
            (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
            (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoT->mintermsP/2.0 -
                    ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            } else {
Alan Mishchenko committed
1518
#ifdef DD_DEBUG
1519
                assert(infoN->parity == 2);
Alan Mishchenko committed
1520
#endif
1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534
                impact = impactN;
                minterms = ((E == Ereg) ? infoE->mintermsN :
                            infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
Alan Mishchenko committed
1535
            }
1536
            numOnset = impact * minterms;
Alan Mishchenko committed
1537
        } else {
1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557
            DdNode *Ereg = Cudd_Regular(E);
            DdNode *TT = cuddT(T);
            DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
            if (T->index == Ereg->index && TT == ET) {
                shared = TT;
                replace = REPLACE_TT;
            } else {
                DdNode *TE = cuddE(T);
                DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
                if (T->index == Ereg->index && TE == EE) {
                    shared = TE;
                    replace = REPLACE_TE;
                } else {
                    replace = REPLACE_N;
                }
            }
            numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
            savings = computeSavings(dd,node,shared,info,localQueue);
            if (shared != NULL) {
                NodeData *infoS;
1558
                (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1559 1560 1561 1562 1563 1564 1565 1566 1567
                if (Cudd_IsComplement(shared)) {
                    numOnset -= (infoS->mintermsN * impactP +
                        infoS->mintermsP * impactN)/2.0;
                } else {
                    numOnset -= (infoS->mintermsP * impactP +
                        infoS->mintermsN * impactN)/2.0;
                }
                savings--;
            }
Alan Mishchenko committed
1568 1569
        }

1570
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
Alan Mishchenko committed
1571
#if 0
1572 1573 1574 1575 1576 1577
        if (replace == REPLACE_T || replace == REPLACE_E)
            (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
                          node, impact, numOnset, savings);
        else
            (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                          node, impactP, impactN, numOnset, savings);
Alan Mishchenko committed
1578
#endif
1579 1580 1581 1582 1583
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = (char) replace;
            info->size -= savings;
            info->minterms -=numOnset;
Alan Mishchenko committed
1584
#if 0
1585 1586
            (void) printf("remap(%d): new size = %d new minterms = %g\n",
                          replace, info->size, info->minterms);
Alan Mishchenko committed
1587
#endif
1588 1589 1590 1591 1592 1593 1594
            if (replace == REPLACE_N) {
                savings -= updateRefs(dd,node,NULL,info,localQueue);
            } else if (replace == REPLACE_T) {
                savings -= updateRefs(dd,node,E,info,localQueue);
            } else if (replace == REPLACE_E) {
                savings -= updateRefs(dd,node,T,info,localQueue);
            } else {
Alan Mishchenko committed
1595
#ifdef DD_DEBUG
1596
                assert(replace == REPLACE_TT || replace == REPLACE_TE);
Alan Mishchenko committed
1597
#endif
1598 1599 1600
                savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
            }
            assert(savings == 0);
Alan Mishchenko committed
1601
        } else {
1602
            replace = NOTHING;
Alan Mishchenko committed
1603
        }
1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615
        if (replace == REPLACE_N) continue;
        if ((replace == REPLACE_E || replace == NOTHING) &&
            !cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (replace == REPLACE_E) {
                item->impactP += impactP;
                item->impactN += impactN;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
Alan Mishchenko committed
1616
        }
1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637
        if ((replace == REPLACE_T || replace == NOTHING) &&
            !Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
Alan Mishchenko committed
1638
        }
1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649
        if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
            !Cudd_IsConstant(shared)) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
                                         cuddI(dd,Cudd_Regular(shared)->index));
            if (Cudd_IsComplement(shared)) {
                item->impactP += impactN;
                item->impactN += impactP;
            } else {
                item->impactP += impactP;
                item->impactN += impactN;
            }
Alan Mishchenko committed
1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of RAmarkNodes */


/**Function********************************************************************

  Synopsis    [Marks nodes for remapping.]

  Description [Marks nodes for remapping. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddRemapUnderApprox]

******************************************************************************/
static int
BAmarkNodes(
  DdManager *dd /* manager */,
  DdNode *f /* function to be analyzed */,
  ApproxInfo *info /* info on BDD */,
  int threshold /* when to stop approximating */,
  double quality1 /* minimum improvement for accepted changes when b=1 */,
  double quality0 /* minimum improvement for accepted changes when b=0 */)
{
    DdLevelQueue *queue;
    DdLevelQueue *localQueue;
    NodeData *infoN, *infoT, *infoE;
    GlobalQueueItem *item;
    DdNode *node, *T, *E;
    DdNode *shared; /* grandchild shared by the two children of node */
    double numOnset;
    double impact, impactP, impactN;
    double minterms;
    double quality;
    int savings;
    int replace;

#if 0
    (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1696
                  info->size, info->minterms);
Alan Mishchenko committed
1697 1698 1699
#endif
    queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
    if (queue == NULL) {
1700
        return(0);
Alan Mishchenko committed
1701 1702
    }
    localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1703
                                    dd->initSlots);
Alan Mishchenko committed
1704
    if (localQueue == NULL) {
1705 1706
        cuddLevelQueueQuit(queue);
        return(0);
Alan Mishchenko committed
1707 1708 1709 1710
    }
    /* Enqueue regular pointer to root and initialize impact. */
    node = Cudd_Regular(f);
    item = (GlobalQueueItem *)
1711
        cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
Alan Mishchenko committed
1712
    if (item == NULL) {
1713 1714 1715
        cuddLevelQueueQuit(queue);
        cuddLevelQueueQuit(localQueue);
        return(0);
Alan Mishchenko committed
1716 1717
    }
    if (Cudd_IsComplement(f)) {
1718 1719
        item->impactP = 0.0;
        item->impactN = 1.0;
Alan Mishchenko committed
1720
    } else {
1721 1722
        item->impactP = 1.0;
        item->impactN = 0.0;
Alan Mishchenko committed
1723 1724 1725 1726 1727 1728
    }
    /* The nodes retrieved here are guaranteed to be non-terminal.
    ** The initial node is not terminal because constant nodes are
    ** dealt with in the calling procedure. Subsequent nodes are inserted
    ** only if they are not terminal. */
    while (queue->first != NULL) {
1729 1730 1731 1732 1733
        /* If the size of the subset is below the threshold, quit. */
        if (info->size <= threshold)
            break;
        item = (GlobalQueueItem *) queue->first;
        node = item->node;
Alan Mishchenko committed
1734
#ifdef DD_DEBUG
1735 1736 1737 1738
        assert(item->impactP >= 0 && item->impactP <= 1.0);
        assert(item->impactN >= 0 && item->impactN <= 1.0);
        assert(!Cudd_IsComplement(node));
        assert(!Cudd_IsConstant(node));
Alan Mishchenko committed
1739
#endif
1740
        if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
Alan Mishchenko committed
1741 1742 1743 1744
            cuddLevelQueueQuit(queue);
            cuddLevelQueueQuit(localQueue);
            return(0);
        }
1745
        quality = infoN->care ? quality1 : quality0;
Alan Mishchenko committed
1746
#ifdef DD_DEBUG
1747
        assert(infoN->parity >= 1 && infoN->parity <= 3);
Alan Mishchenko committed
1748
#endif
1749 1750 1751 1752 1753 1754 1755
        if (infoN->parity == 3) {
            /* This node can be reached through paths of different parity.
            ** It is not safe to replace it, because remapping will give
            ** an incorrect result, while replacement by 0 may cause node
            ** splitting. */
            cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
            continue;
Alan Mishchenko committed
1756
        }
1757 1758 1759 1760 1761 1762 1763 1764 1765 1766
        T = cuddT(node);
        E = cuddE(node);
        shared = NULL;
        impactP = item->impactP;
        impactN = item->impactN;
        if (Cudd_bddLeq(dd,T,E)) {
            /* Here we know that E is regular. */
#ifdef DD_DEBUG
            assert(!Cudd_IsComplement(E));
#endif
1767 1768
            (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
            (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
            } else {
#ifdef DD_DEBUG
                assert(infoN->parity == 2);
#endif
                impact = impactN;
                minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
Alan Mishchenko committed
1800
            }
1801 1802 1803 1804
            numOnset = impact * minterms;
        } else if (Cudd_bddLeq(dd,E,T)) {
            /* Here E may be complemented. */
            DdNode *Ereg = Cudd_Regular(E);
1805 1806
            (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
            (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822
            if (infoN->parity == 1) {
                impact = impactP;
                minterms = infoT->mintermsP/2.0 -
                    ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
                if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
                    savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_T;
            } else {
Alan Mishchenko committed
1823
#ifdef DD_DEBUG
1824
                assert(infoN->parity == 2);
Alan Mishchenko committed
1825
#endif
1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839
                impact = impactN;
                minterms = ((E == Ereg) ? infoE->mintermsN :
                            infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
                if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
                    savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
                    if (savings == 1) {
                        cuddLevelQueueQuit(queue);
                        cuddLevelQueueQuit(localQueue);
                        return(0);
                    }
                } else {
                    savings = 1;
                }
                replace = REPLACE_E;
Alan Mishchenko committed
1840
            }
1841
            numOnset = impact * minterms;
Alan Mishchenko committed
1842
        } else {
1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862
            DdNode *Ereg = Cudd_Regular(E);
            DdNode *TT = cuddT(T);
            DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
            if (T->index == Ereg->index && TT == ET) {
                shared = TT;
                replace = REPLACE_TT;
            } else {
                DdNode *TE = cuddE(T);
                DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
                if (T->index == Ereg->index && TE == EE) {
                    shared = TE;
                    replace = REPLACE_TE;
                } else {
                    replace = REPLACE_N;
                }
            }
            numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
            savings = computeSavings(dd,node,shared,info,localQueue);
            if (shared != NULL) {
                NodeData *infoS;
1863
                (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1864 1865 1866 1867 1868 1869 1870 1871 1872
                if (Cudd_IsComplement(shared)) {
                    numOnset -= (infoS->mintermsN * impactP +
                        infoS->mintermsP * impactN)/2.0;
                } else {
                    numOnset -= (infoS->mintermsP * impactP +
                        infoS->mintermsN * impactN)/2.0;
                }
                savings--;
            }
Alan Mishchenko committed
1873 1874
        }

1875
        cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
Alan Mishchenko committed
1876
#if 0
1877 1878 1879 1880 1881 1882
        if (replace == REPLACE_T || replace == REPLACE_E)
            (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
                          node, impact, numOnset, savings);
        else
            (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
                          node, impactP, impactN, numOnset, savings);
Alan Mishchenko committed
1883
#endif
1884 1885 1886 1887 1888
        if ((1 - numOnset / info->minterms) >
            quality * (1 - (double) savings / info->size)) {
            infoN->replace = (char) replace;
            info->size -= savings;
            info->minterms -=numOnset;
Alan Mishchenko committed
1889
#if 0
1890 1891
            (void) printf("remap(%d): new size = %d new minterms = %g\n",
                          replace, info->size, info->minterms);
Alan Mishchenko committed
1892
#endif
1893 1894 1895 1896 1897 1898 1899
            if (replace == REPLACE_N) {
                savings -= updateRefs(dd,node,NULL,info,localQueue);
            } else if (replace == REPLACE_T) {
                savings -= updateRefs(dd,node,E,info,localQueue);
            } else if (replace == REPLACE_E) {
                savings -= updateRefs(dd,node,T,info,localQueue);
            } else {
Alan Mishchenko committed
1900
#ifdef DD_DEBUG
1901
                assert(replace == REPLACE_TT || replace == REPLACE_TE);
Alan Mishchenko committed
1902
#endif
1903 1904 1905
                savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
            }
            assert(savings == 0);
Alan Mishchenko committed
1906
        } else {
1907
            replace = NOTHING;
Alan Mishchenko committed
1908
        }
1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920
        if (replace == REPLACE_N) continue;
        if ((replace == REPLACE_E || replace == NOTHING) &&
            !cuddIsConstant(cuddT(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
                                         cuddI(dd,cuddT(node)->index));
            if (replace == REPLACE_E) {
                item->impactP += impactP;
                item->impactN += impactN;
            } else {
                item->impactP += impactP/2.0;
                item->impactN += impactN/2.0;
            }
Alan Mishchenko committed
1921
        }
1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942
        if ((replace == REPLACE_T || replace == NOTHING) &&
            !Cudd_IsConstant(cuddE(node))) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
                                         cuddI(dd,Cudd_Regular(cuddE(node))->index));
            if (Cudd_IsComplement(cuddE(node))) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
Alan Mishchenko committed
1943
        }
1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964
        if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
            !Cudd_IsConstant(shared)) {
            item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
                                         cuddI(dd,Cudd_Regular(shared)->index));
            if (Cudd_IsComplement(shared)) {
                if (replace == REPLACE_T) {
                    item->impactP += impactN;
                    item->impactN += impactP;
                } else {
                    item->impactP += impactN/2.0;
                    item->impactN += impactP/2.0;
                }
            } else {
                if (replace == REPLACE_T) {
                    item->impactP += impactP;
                    item->impactN += impactN;
                } else {
                    item->impactP += impactP/2.0;
                    item->impactN += impactN/2.0;
                }
            }
Alan Mishchenko committed
1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998
        }
    }

    cuddLevelQueueQuit(queue);
    cuddLevelQueueQuit(localQueue);
    return(1);

} /* end of BAmarkNodes */


/**Function********************************************************************

  Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]

  Description [Builds the subset BDDfor cuddRemapUnderApprox.  Based
  on the info table, performs remapping or replacement at selected
  nodes. Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddRemapUnderApprox]

******************************************************************************/
static DdNode *
RAbuildSubset(
  DdManager * dd /* DD manager */,
  DdNode * node /* current node */,
  ApproxInfo * info /* node info */)
{
    DdNode *Nt, *Ne, *N, *t, *e, *r;
    NodeData *infoN;

    if (Cudd_IsConstant(node))
1999
        return(node);
Alan Mishchenko committed
2000 2001 2002 2003 2004 2005

    N = Cudd_Regular(node);

    Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
    Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));

2006
    if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
2007 2008 2009 2010
        if (N == node ) {
            if (infoN->resultP != NULL) {
                return(infoN->resultP);
            }
Alan Mishchenko committed
2011
        } else {
2012 2013 2014
            if (infoN->resultN != NULL) {
                return(infoN->resultN);
            }
Alan Mishchenko committed
2015
        }
2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070
        if (infoN->replace == REPLACE_T) {
            r = RAbuildSubset(dd, Ne, info);
            return(r);
        } else if (infoN->replace == REPLACE_E) {
            r = RAbuildSubset(dd, Nt, info);
            return(r);
        } else if (infoN->replace == REPLACE_N) {
            return(info->zero);
        } else if (infoN->replace == REPLACE_TT) {
            DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
                                       Cudd_IsComplement(node));
            int index = cuddT(N)->index;
            e = info->zero;
            t = RAbuildSubset(dd, Ntt, info);
            if (t == NULL) {
                return(NULL);
            }
            cuddRef(t);
            if (Cudd_IsComplement(t)) {
                t = Cudd_Not(t);
                e = Cudd_Not(e);
                r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
                if (r == NULL) {
                    Cudd_RecursiveDeref(dd, t);
                    return(NULL);
                }
                r = Cudd_Not(r);
            } else {
                r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
                if (r == NULL) {
                    Cudd_RecursiveDeref(dd, t);
                    return(NULL);
                }
            }
            cuddDeref(t);
            return(r);
        } else if (infoN->replace == REPLACE_TE) {
            DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
                                       Cudd_IsComplement(node));
            int index = cuddT(N)->index;
            t = info->one;
            e = RAbuildSubset(dd, Nte, info);
            if (e == NULL) {
                return(NULL);
            }
            cuddRef(e);
            e = Cudd_Not(e);
            r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
            if (r == NULL) {
                Cudd_RecursiveDeref(dd, e);
                return(NULL);
            }
            r =Cudd_Not(r);
            cuddDeref(e);
            return(r);
Alan Mishchenko committed
2071 2072
        }
    } else {
2073 2074 2075 2076
        (void) fprintf(dd->err,
                       "Something is wrong, ought to be in info table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
        return(NULL);
Alan Mishchenko committed
2077 2078 2079 2080
    }

    t = RAbuildSubset(dd, Nt, info);
    if (t == NULL) {
2081
        return(NULL);
Alan Mishchenko committed
2082 2083 2084 2085 2086
    }
    cuddRef(t);

    e = RAbuildSubset(dd, Ne, info);
    if (e == NULL) {
2087 2088
        Cudd_RecursiveDeref(dd,t);
        return(NULL);
Alan Mishchenko committed
2089 2090 2091 2092
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
2093 2094 2095 2096 2097 2098 2099 2100 2101
        t = Cudd_Not(t);
        e = Cudd_Not(e);
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
        r = Cudd_Not(r);
Alan Mishchenko committed
2102
    } else {
2103 2104 2105 2106 2107 2108
        r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
        if (r == NULL) {
            Cudd_RecursiveDeref(dd, e);
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
Alan Mishchenko committed
2109 2110 2111 2112 2113
    }
    cuddDeref(t);
    cuddDeref(e);

    if (N == node) {
2114
        infoN->resultP = r;
Alan Mishchenko committed
2115
    } else {
2116
        infoN->resultN = r;
Alan Mishchenko committed
2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153
    }

    return(r);

} /* end of RAbuildSubset */


/**Function********************************************************************

  Synopsis    [Finds don't care nodes.]

  Description [Finds don't care nodes by traversing f and b in parallel.
  Returns the care status of the visited f node if successful; CARE_ERROR
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddBiasedUnderApprox]

******************************************************************************/
static int
BAapplyBias(
  DdManager *dd,
  DdNode *f,
  DdNode *b,
  ApproxInfo *info,
  DdHashTable *cache)
{
    DdNode *one, *zero, *res;
    DdNode *Ft, *Fe, *B, *Bt, *Be;
    unsigned int topf, topb;
    NodeData *infoF;
    int careT, careE;

    one = DD_ONE(dd);
    zero = Cudd_Not(one);

2154
    if (! st__lookup(info->table, (const char *)f, (char **)&infoF))
2155
        return(CARE_ERROR);
Alan Mishchenko committed
2156 2157 2158 2159 2160
    if (f == one) return(TOTAL_CARE);
    if (b == zero) return(infoF->care);
    if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);

    if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
2161 2162 2163 2164 2165 2166
        (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
        if (res->ref == 0) {
            cache->manager->dead++;
            cache->manager->constants.dead++;
        }
        return(infoF->care);
Alan Mishchenko committed
2167 2168 2169 2170 2171 2172
    }

    topf = dd->perm[f->index];
    B = Cudd_Regular(b);
    topb = cuddI(dd,B->index);
    if (topf <= topb) {
2173
        Ft = cuddT(f); Fe = cuddE(f);
Alan Mishchenko committed
2174
    } else {
2175
        Ft = Fe = f;
Alan Mishchenko committed
2176 2177
    }
    if (topb <= topf) {
2178 2179 2180 2181 2182 2183
        /* We know that b is not constant because f is not. */
        Bt = cuddT(B); Be = cuddE(B);
        if (Cudd_IsComplement(b)) {
            Bt = Cudd_Not(Bt);
            Be = Cudd_Not(Be);
        }
Alan Mishchenko committed
2184
    } else {
2185
        Bt = Be = b;
Alan Mishchenko committed
2186 2187 2188 2189
    }

    careT = BAapplyBias(dd, Ft, Bt, info, cache);
    if (careT == CARE_ERROR)
2190
        return(CARE_ERROR);
Alan Mishchenko committed
2191 2192
    careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
    if (careE == CARE_ERROR)
2193
        return(CARE_ERROR);
Alan Mishchenko committed
2194
    if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2195
        infoF->care = TOTAL_CARE;
Alan Mishchenko committed
2196
    } else {
2197
        infoF->care = CARE;
Alan Mishchenko committed
2198 2199 2200
    }

    if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
2201 2202 2203 2204 2205
        ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
            return(CARE_ERROR);
        }
Alan Mishchenko committed
2206 2207 2208 2209
    }
    return(infoF->care);

} /* end of BAapplyBias */
2210 2211


2212 2213
ABC_NAMESPACE_IMPL_END