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

  Synopsis    [Performs the recursive step of
  Cudd_bddLiteralSetIntersection.]

  Description [Performs the recursive step of
  Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,
  and checks whether they agree in phase.  Returns a pointer to the
  resulting cube if successful; NULL otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Performs the recursive step of
Cudd_bddLiteralSetIntersection.]

Description [Performs the recursive step of
Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,
and checks whether they agree in phase.  Returns a pointer to the
resulting cube if successful; NULL otherwise.]


Function Synopsis [ Performs the recursive step of Cudd_bddLiteralSetIntersection . ] Description [ Performs the recursive step of Cudd_bddLiteralSetIntersection . Scans the cubes for common variables and checks whether they agree in phase . Returns a pointer to the resulting cube if successful ; NULL otherwise . ]
DdNode *
cuddBddLiteralSetIntersectionRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *res, *tmp;
    DdNode *F, *G;
    DdNode *fc, *gc;
    DdNode *one;
    DdNode *zero;
    unsigned int topf, topg, comple;
    int phasef, phaseg;
    statLine(dd);
    if (f == g) return(f);
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    one = DD_ONE(dd);
    if (F == G) return(one);
    zero = Cudd_Not(one);
    topf = cuddI(dd,F->index);
    topg = cuddI(dd,G->index);
    while (topf != topg) {
        if (topf < topg) {      
            comple = f != F;
            f = cuddT(F);
            if (comple) f = Cudd_Not(f);
            if (f == zero) {
                f = cuddE(F);
                if (comple) f = Cudd_Not(f);
            }
            F = Cudd_Regular(f);
            topf = cuddI(dd,F->index);
        } else if (topg < topf) {
            comple = g != G;
            g = cuddT(G);
            if (comple) g = Cudd_Not(g);
            if (g == zero) {
                g = cuddE(G);
                if (comple) g = Cudd_Not(g);
            }
            G = Cudd_Regular(g);
            topg = cuddI(dd,G->index);
        }
    }
    if (f == one) return(one);
    res = cuddCacheLookup2(dd,Cudd_bddLiteralSetIntersection,f,g);
    if (res != NULL) {
        return(res);
    }
    comple = f != F;
    fc = cuddT(F);
    phasef = 1;
    if (comple) fc = Cudd_Not(fc);
    if (fc == zero) {
        fc = cuddE(F);
        phasef = 0;
        if (comple) fc = Cudd_Not(fc);
    }
    comple = g != G;
    gc = cuddT(G);
    phaseg = 1;
    if (comple) gc = Cudd_Not(gc);
    if (gc == zero) {
        gc = cuddE(G);
        phaseg = 0;
        if (comple) gc = Cudd_Not(gc);
    }
    tmp = cuddBddLiteralSetIntersectionRecur(dd,fc,gc);
    if (tmp == NULL) {
        return(NULL);
    }
    if (phasef != phaseg) {
        res = tmp;
    } else {
        cuddRef(tmp);
        if (phasef == 0) {
            res = cuddBddAndRecur(dd,Cudd_Not(dd->vars[F->index]),tmp);
        } else {
            res = cuddBddAndRecur(dd,dd->vars[F->index],tmp);
        }
        if (res == NULL) {
            Cudd_RecursiveDeref(dd,tmp);
            return(NULL);
        }
        cuddDeref(tmp); 
    }
    cuddCacheInsert2(dd,Cudd_bddLiteralSetIntersection,f,g,res);
    return(res);
}
DdNode * cuddBddLiteralSetIntersectionRecur ( DdManager * dd , DdNode * f , DdNode * g ) { DdNode * res , * tmp ; DdNode * F , * G ; DdNode * fc , * gc ; DdNode * one ; DdNode * zero ; unsigned int topf , topg , comple ; int phasef , phaseg ; statLine ( dd ) ; if ( f == g ) return ( f ) ; F = Cudd_Regular ( f ) ; G = Cudd_Regular ( g ) ; one = DD_ONE ( dd ) ; if ( F == G ) return ( one ) ; zero = Cudd_Not ( one ) ; topf = cuddI ( dd , F -> index ) ; topg = cuddI ( dd , G -> index ) ; while ( topf != topg ) { if ( topf < topg ) { comple = f != F ; f = cuddT ( F ) ; if ( comple ) f = Cudd_Not ( f ) ; if ( f == zero ) { f = cuddE ( F ) ; if ( comple ) f = Cudd_Not ( f ) ; } F = Cudd_Regular ( f ) ; topf = cuddI ( dd , F -> index ) ; } else if ( topg < topf ) { comple = g != G ; g = cuddT ( G ) ; if ( comple ) g = Cudd_Not ( g ) ; if ( g == zero ) { g = cuddE ( G ) ; if ( comple ) g = Cudd_Not ( g ) ; } G = Cudd_Regular ( g ) ; topg = cuddI ( dd , G -> index ) ; } } if ( f == one ) return ( one ) ; res = cuddCacheLookup2 ( dd , Cudd_bddLiteralSetIntersection , f , g ) ; if ( res != NULL ) { return ( res ) ; } comple = f != F ; fc = cuddT ( F ) ; phasef = 1 ; if ( comple ) fc = Cudd_Not ( fc ) ; if ( fc == zero ) { fc = cuddE ( F ) ; phasef = 0 ; if ( comple ) fc = Cudd_Not ( fc ) ; } comple = g != G ; gc = cuddT ( G ) ; phaseg = 1 ; if ( comple ) gc = Cudd_Not ( gc ) ; if ( gc == zero ) { gc = cuddE ( G ) ; phaseg = 0 ; if ( comple ) gc = Cudd_Not ( gc ) ; } tmp = cuddBddLiteralSetIntersectionRecur ( dd , fc , gc ) ; if ( tmp == NULL ) { return ( NULL ) ; } if ( phasef != phaseg ) { res = tmp ; } else { cuddRef ( tmp ) ; if ( phasef == 0 ) { res = cuddBddAndRecur ( dd , Cudd_Not ( dd -> vars [ F -> index ] ) , tmp ) ; } else { res = cuddBddAndRecur ( dd , dd -> vars [ F -> index ] , tmp ) ; } if ( res == NULL ) { Cudd_RecursiveDeref ( dd , tmp ) ; return ( NULL ) ; } cuddDeref ( tmp ) ; } cuddCacheInsert2 ( dd , Cudd_bddLiteralSetIntersection , f , g , res ) ; return ( res ) ; }
Function
Synopsis    [Performs the recursive step of
Cudd_bddLiteralSetIntersection.]
Function Synopsis [ Performs the recursive step of Cudd_bddLiteralSetIntersection . ]
/* Here f != g. If F == G, then f and g are complementary.
    ** Since they are two cubes, this case only occurs when f == v,
    ** g == v', and v is a variable or its complement.
    */ /* Look for a variable common to both cubes. If there are none, this
    ** loop will stop when the constant node is reached in both cubes.
    */ /* move down on f */ /* At this point, f == one <=> g == 1. It suffices to test one of them. */ /* Here f and g are both non constant and have the same top variable. */ /* Just cuddDeref, because it is included in result */