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

  Synopsis [ADD restrict according to Coudert and Madre's algorithm
  (ICCAD90).]

  Description [ADD restrict according to Coudert and Madre's algorithm
  (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
  If application of restrict results in an ADD larger than the input
  ADD, the input ADD is returned.]

  SideEffects [None]

  SeeAlso     [Cudd_addConstrain Cudd_bddRestrict]

******************************************************************************/
Function
Synopsis [ADD restrict according to Coudert and Madre's algorithm
(ICCAD90).]

Description [ADD restrict according to Coudert and Madre's algorithm
(ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
If application of restrict results in an ADD larger than the input
ADD, the input ADD is returned.]




Function Synopsis [ ADD restrict according to Coudert and Madre ' s algorithm ( ICCAD90 ) . ] Description [ ADD restrict according to Coudert and Madre ' s algorithm ( ICCAD90 ) . Returns the restricted ADD if successful ; otherwise NULL . If application of restrict results in an ADD larger than the input ADD the input ADD is returned . ]
DdNode *
Cudd_addRestrict(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *supp_f, *supp_c;
    DdNode *res, *commonSupport;
    int intersection;
    int sizeF, sizeRes;
    supp_f = Cudd_Support(dd, f);
    if (supp_f == NULL) {
        return(NULL);
    }
    cuddRef(supp_f);
    supp_c = Cudd_Support(dd, c);
    if (supp_c == NULL) {
        Cudd_RecursiveDeref(dd,supp_f);
        return(NULL);
    }
    cuddRef(supp_c);
    commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
    if (commonSupport == NULL) {
        Cudd_RecursiveDeref(dd,supp_f);
        Cudd_RecursiveDeref(dd,supp_c);
        return(NULL);
    }
    cuddRef(commonSupport);
    Cudd_RecursiveDeref(dd,supp_f);
    Cudd_RecursiveDeref(dd,supp_c);
    intersection = commonSupport != DD_ONE(dd);
    Cudd_RecursiveDeref(dd,commonSupport);
    if (intersection) {
        do {
            dd->reordered = 0;
            res = cuddAddRestrictRecur(dd, f, c);
        } while (dd->reordered == 1);
        sizeF = Cudd_DagSize(f);
        sizeRes = Cudd_DagSize(res);
        if (sizeF <= sizeRes) {
            cuddRef(res);
            Cudd_RecursiveDeref(dd, res);
            return(f);
        } else {
            return(res);
        }
    } else {
        return(f);
    }
}
DdNode * Cudd_addRestrict ( DdManager * dd , DdNode * f , DdNode * c ) { DdNode * supp_f , * supp_c ; DdNode * res , * commonSupport ; int intersection ; int sizeF , sizeRes ; supp_f = Cudd_Support ( dd , f ) ; if ( supp_f == NULL ) { return ( NULL ) ; } cuddRef ( supp_f ) ; supp_c = Cudd_Support ( dd , c ) ; if ( supp_c == NULL ) { Cudd_RecursiveDeref ( dd , supp_f ) ; return ( NULL ) ; } cuddRef ( supp_c ) ; commonSupport = Cudd_bddLiteralSetIntersection ( dd , supp_f , supp_c ) ; if ( commonSupport == NULL ) { Cudd_RecursiveDeref ( dd , supp_f ) ; Cudd_RecursiveDeref ( dd , supp_c ) ; return ( NULL ) ; } cuddRef ( commonSupport ) ; Cudd_RecursiveDeref ( dd , supp_f ) ; Cudd_RecursiveDeref ( dd , supp_c ) ; intersection = commonSupport != DD_ONE ( dd ) ; Cudd_RecursiveDeref ( dd , commonSupport ) ; if ( intersection ) { do { dd -> reordered = 0 ; res = cuddAddRestrictRecur ( dd , f , c ) ; } while ( dd -> reordered == 1 ) ; sizeF = Cudd_DagSize ( f ) ; sizeRes = Cudd_DagSize ( res ) ; if ( sizeF <= sizeRes ) { cuddRef ( res ) ; Cudd_RecursiveDeref ( dd , res ) ; return ( f ) ; } else { return ( res ) ; } } else { return ( f ) ; } }
Function
Synopsis [ADD restrict according to Coudert and Madre's algorithm
(ICCAD90).]
Function Synopsis [ ADD restrict according to Coudert and Madre ' s algorithm ( ICCAD90 ) . ]
/* Check if supports intersect. */