abc/src/proof/acec/acecXor.c
// collects XOR trees belonging to each of XOR roots
collects XOR trees belonging to each of XOR roots
collects XOR trees belonging to each of XOR roots
Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots )
{
    Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
    int i, k, Entry;
    Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); 
    Vec_IntForEachEntry( vXorRoots, Entry, i )
        Vec_IntWriteEntry( vRanks, Entry, i );
    for ( i = Vec_IntSize(vXors)/4 - 1; i >= 0; i-- )
    {
        int Root = Vec_IntEntry( vXors, 4*i );
        int Rank = Vec_IntEntry( vRanks, Root );
        if ( Rank == -1 )
            continue;
        for ( k = 1; k < 4; k++ )
        {
            int Node = Vec_IntEntry( vXors, 4*i+k );
            if ( Node == 0 ) 
                continue;
            Entry = Vec_IntEntry( vRanks, Node );
            if ( Entry == Rank ) 
                continue;
            if ( Entry == -1 )
                Vec_IntWriteEntry( vRanks, Node, Rank );
            else
                Vec_IntPush( vDoubles, Node );
            if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Node)))
            printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
        }
    }
    Vec_IntForEachEntry( vDoubles, Entry, i )
        Vec_IntWriteEntry( vRanks, Entry, -1 );
    Vec_IntFree( vDoubles );
    return vRanks;
}
Vec_Int_t * Acec_RankTrees ( Gia_Man_t * p , Vec_Int_t * vXors , Vec_Int_t * vXorRoots ) { Vec_Int_t * vDoubles = Vec_IntAlloc ( 100 ) ; int i , k , Entry ; Vec_Int_t * vRanks = Vec_IntStartFull ( Gia_ManObjNum ( p ) ) ; Vec_IntForEachEntry ( vXorRoots , Entry , i ) Vec_IntWriteEntry ( vRanks , Entry , i ) ; for ( i = Vec_IntSize ( vXors ) / 4 - 1 ; i >= 0 ; i -- ) { int Root = Vec_IntEntry ( vXors , 4 * i ) ; int Rank = Vec_IntEntry ( vRanks , Root ) ; if ( Rank == -1 ) continue ; for ( k = 1 ; k < 4 ; k ++ ) { int Node = Vec_IntEntry ( vXors , 4 * i + k ) ; if ( Node == 0 ) continue ; Entry = Vec_IntEntry ( vRanks , Node ) ; if ( Entry == Rank ) continue ; if ( Entry == -1 ) Vec_IntWriteEntry ( vRanks , Node , Rank ) ; else Vec_IntPush ( vDoubles , Node ) ; if ( Entry != -1 && Gia_ObjIsAnd ( Gia_ManObj ( p , Node ) ) ) printf ( " \n " , Node , Entry , Rank ) ; } } Vec_IntForEachEntry ( vDoubles , Entry , i ) Vec_IntWriteEntry ( vRanks , Entry , -1 ) ; Vec_IntFree ( vDoubles ) ; return vRanks ; }
collects XOR trees belonging to each of XOR roots
collects XOR trees belonging to each of XOR roots
// map roots into their ranks // map nodes into their ranks // skip XORs that are not part of any tree // iterate through XOR inputs // HA // the same tree // remove duplicated entries