abc/src/bdd/cudd/cuddExact.c
/**Function********************************************************************

  Synopsis    [Computes a lower bound on the size of a BDD.]

  Description [Computes a lower bound on the size of a BDD from the
  following factors:
  <ul>
  <li> size of the lower part of it;
  <li> size of the part of the upper part not subjected to reordering;
  <li> number of roots in the part of the BDD subjected to reordering;
  <li> variable in the support of the roots in the upper part of the
       BDD subjected to reordering.
  <ul/>]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Computes a lower bound on the size of a BDD.]

Description [Computes a lower bound on the size of a BDD from the
following factors:

 size of the lower part of it;
 size of the part of the upper part not subjected to reordering;
 number of roots in the part of the BDD subjected to reordering;
 variable in the support of the roots in the upper part of the
BDD subjected to reordering.




Function Synopsis [ Computes a lower bound on the size of a BDD . ] Description [ Computes a lower bound on the size of a BDD from the following factors : size of the lower part of it ; size of the part of the upper part not subjected to reordering ; number of roots in the part of the BDD subjected to reordering ; variable in the support of the roots in the upper part of the BDD subjected to reordering .
static int
computeLB(
  DdManager * table             ,
  DdHalfWord * order            ,
  int  roots                    ,
  int  cost                     ,
  int  lower                    ,
  int  upper                    ,
  int  level                    
  )
{
    int i;
    int lb = cost;
    int lb1 = 0;
    int lb2;
    int support;
    DdHalfWord ref;
    for (i = 0; i < lower; i++) {
        lb += getLevelKeys(table,i);
    }
    for (i = lower; i <= lower+level; i++) {
        support = table->subtables[i].keys > 1 ||
            table->vars[order[i-lower]]->ref > 1;
        lb1 += support;
    }
    if (lower+level+1 < table->size) {
        if (lower+level < upper)
            ref = table->vars[order[level+1]]->ref;
        else
            ref = table->vars[table->invperm[upper+1]]->ref;
        lb2 = table->subtables[lower+level+1].keys -
            (ref > (DdHalfWord) 1) - roots;
    } else {
        lb2 = 0;
    }
    lb += lb1 > lb2 ? lb1 : lb2;
    return(lb);
}
static int computeLB ( DdManager * table , DdHalfWord * order , int roots , int cost , int lower , int upper , int level ) { int i ; int lb = cost ; int lb1 = 0 ; int lb2 ; int support ; DdHalfWord ref ; for ( i = 0 ; i < lower ; i ++ ) { lb += getLevelKeys ( table , i ) ; } for ( i = lower ; i <= lower + level ; i ++ ) { support = table -> subtables [ i ] . keys > 1 || table -> vars [ order [ i - lower ] ] -> ref > 1 ; lb1 += support ; } if ( lower + level + 1 < table -> size ) { if ( lower + level < upper ) ref = table -> vars [ order [ level + 1 ] ] -> ref ; else ref = table -> vars [ table -> invperm [ upper + 1 ] ] -> ref ; lb2 = table -> subtables [ lower + level + 1 ] . keys - ( ref > ( DdHalfWord ) 1 ) - roots ; } else { lb2 = 0 ; } lb += lb1 > lb2 ? lb1 : lb2 ; return ( lb ) ; }
Function
Synopsis    [Computes a lower bound on the size of a BDD.]
Function Synopsis [ Computes a lower bound on the size of a BDD . ]
/* manager */ /* optimal order for the subset */ /* roots between lower and upper */ /* minimum cost for the subset */ /* lower level to be reordered */ /* upper level to be reordered */ /* offset for the current top bottom var */ /* The levels not involved in reordering are not going to change.
    ** Add their sizes to the lower bound.
    */ /* If a variable is in the support, then there is going
    ** to be at least one node labeled by that variable.
    */ /* Estimate the number of nodes required to connect the roots to
    ** the nodes in the bottom part. */