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

  Synopsis    [Tests the functions related to the exclusive OR.]

  Description [Tests the functions related to the exclusive OR. It
  builds the boolean difference of the given function in three
  different ways and checks that the results is the same. Returns 1 if
  successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Tests the functions related to the exclusive OR.]

Description [Tests the functions related to the exclusive OR. It
builds the boolean difference of the given function in three
different ways and checks that the results is the same. Returns 1 if
successful; 0 otherwise.]




Function Synopsis [ Tests the functions related to the exclusive OR . ] Description [ Tests the functions related to the exclusive OR . It builds the boolean difference of the given function in three different ways and checks that the results is the same . Returns 1 if successful ; 0 otherwise . ]
static int
testXor(DdManager *dd, DdNode *f, int pr, int nvars)
{
    DdNode *f1, *f0, *res1, *res2;
    int x;
    x = nvars / 2;
    f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
    if (f1 == NULL) return(0);
    Cudd_Ref(f1);
    f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
    if (f0 == NULL) {
    Cudd_RecursiveDeref(dd,f1);
    return(0);
    }
    Cudd_Ref(f0);
    res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
    if (res1 == NULL) return(0);
    Cudd_Ref(res1);
    if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
    res2 = Cudd_bddXor(dd,f1,f0);
    if (res2 == NULL) {
    Cudd_RecursiveDeref(dd,res1);
    return(0);
    }
    Cudd_Ref(res2);
    if (res1 != res2) {
    if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,res2);
    return(0);
    }
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,f1);
    Cudd_RecursiveDeref(dd,f0);
    res1 = Cudd_bddBooleanDiff(dd,f,x);
    if (res1 == NULL) {
    Cudd_RecursiveDeref(dd,res2);
    return(0);
    }
    Cudd_Ref(res1);
    if (res1 != res2) {
    if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,res2);
    return(0);
    }
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,res2);
    return(1);
}
static int testXor ( DdManager * dd , DdNode * f , int pr , int nvars ) { DdNode * f1 , * f0 , * res1 , * res2 ; int x ; x = nvars / 2 ; f1 = Cudd_Cofactor ( dd , f , dd -> vars [ x ] ) ; if ( f1 == NULL ) return ( 0 ) ; Cudd_Ref ( f1 ) ; f0 = Cudd_Cofactor ( dd , f , Cudd_Not ( dd -> vars [ x ] ) ) ; if ( f0 == NULL ) { Cudd_RecursiveDeref ( dd , f1 ) ; return ( 0 ) ; } Cudd_Ref ( f0 ) ; res1 = Cudd_bddIte ( dd , f1 , Cudd_Not ( f0 ) , f0 ) ; if ( res1 == NULL ) return ( 0 ) ; Cudd_Ref ( res1 ) ; if ( pr > 0 ) { ( void ) printf ( " " ) ; Cudd_PrintDebug ( dd , res1 , nvars , pr ) ; } res2 = Cudd_bddXor ( dd , f1 , f0 ) ; if ( res2 == NULL ) { Cudd_RecursiveDeref ( dd , res1 ) ; return ( 0 ) ; } Cudd_Ref ( res2 ) ; if ( res1 != res2 ) { if ( pr > 0 ) { ( void ) printf ( " " ) ; Cudd_PrintDebug ( dd , res2 , nvars , pr ) ; } Cudd_RecursiveDeref ( dd , res1 ) ; Cudd_RecursiveDeref ( dd , res2 ) ; return ( 0 ) ; } Cudd_RecursiveDeref ( dd , res1 ) ; Cudd_RecursiveDeref ( dd , f1 ) ; Cudd_RecursiveDeref ( dd , f0 ) ; res1 = Cudd_bddBooleanDiff ( dd , f , x ) ; if ( res1 == NULL ) { Cudd_RecursiveDeref ( dd , res2 ) ; return ( 0 ) ; } Cudd_Ref ( res1 ) ; if ( res1 != res2 ) { if ( pr > 0 ) { ( void ) printf ( " " ) ; Cudd_PrintDebug ( dd , res1 , nvars , pr ) ; } Cudd_RecursiveDeref ( dd , res1 ) ; Cudd_RecursiveDeref ( dd , res2 ) ; return ( 0 ) ; } Cudd_RecursiveDeref ( dd , res1 ) ; Cudd_RecursiveDeref ( dd , res2 ) ; return ( 1 ) ; }
Function
Synopsis    [Tests the functions related to the exclusive OR.]
Function Synopsis [ Tests the functions related to the exclusive OR . ]
/* Extract cofactors w.r.t. mid variable. */ /* Compute XOR of cofactors with ITE. */ /* Compute XOR of cofactors with XOR. */ /* Compute boolean difference directly. */