abc/src/proof/acec/acecXor.c
// collects leaves of each XOR tree
collects leaves of each XOR tree
collects leaves of each XOR tree
Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks, Vec_Wec_t ** pvAddBoxes )
{
    Vec_Bit_t * vMapXors = Acec_MapXorOuts2( p, vXors, vRanks );
    Vec_Int_t * vMapMajs = Acec_MapMajOuts2( p, vAdds, vRanks );
    Vec_Wec_t * vXorLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) );
    Vec_Wec_t * vAddBoxes  = Vec_WecStart( Vec_IntSize(vXorRoots) );
    int i, k;
    for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
    {
        int Xor = Vec_IntEntry(vXors, 4*i);
        int Rank = Vec_IntEntry(vRanks, Xor);
        if ( Rank == -1 )
            continue;
        for ( k = 1; k < 4; k++ )
        {
            int Fanin = Vec_IntEntry(vXors, 4*i+k);
            if ( Fanin == 0 )
                continue;
            if ( Vec_BitEntry(vMapXors, Fanin) )
            {
                assert( Rank == Vec_IntEntry(vRanks, Fanin) );
                continue;
            }
            if ( Vec_IntEntry(vMapMajs, Fanin) == -1 ) 
                Vec_WecPush( vXorLeaves, Rank, Fanin );
            else if ( Vec_IntEntry(vRanks, Xor) > 0 ) 
                Vec_WecPush( vAddBoxes, Rank-1, Vec_IntEntry(vMapMajs, Fanin) );
        }
    }
    Vec_BitFree( vMapXors );
    Vec_IntFree( vMapMajs );
    if ( pvAddBoxes )
        *pvAddBoxes = vAddBoxes;
    return vXorLeaves;
}
Vec_Wec_t * Acec_FindXorLeaves ( Gia_Man_t * p , Vec_Int_t * vXors , Vec_Int_t * vAdds , Vec_Int_t * vXorRoots , Vec_Int_t * vRanks , Vec_Wec_t * * pvAddBoxes ) { Vec_Bit_t * vMapXors = Acec_MapXorOuts2 ( p , vXors , vRanks ) ; Vec_Int_t * vMapMajs = Acec_MapMajOuts2 ( p , vAdds , vRanks ) ; Vec_Wec_t * vXorLeaves = Vec_WecStart ( Vec_IntSize ( vXorRoots ) ) ; Vec_Wec_t * vAddBoxes = Vec_WecStart ( Vec_IntSize ( vXorRoots ) ) ; int i , k ; for ( i = 0 ; 4 * i < Vec_IntSize ( vXors ) ; i ++ ) { int Xor = Vec_IntEntry ( vXors , 4 * i ) ; int Rank = Vec_IntEntry ( vRanks , Xor ) ; if ( Rank == -1 ) continue ; for ( k = 1 ; k < 4 ; k ++ ) { int Fanin = Vec_IntEntry ( vXors , 4 * i + k ) ; if ( Fanin == 0 ) continue ; if ( Vec_BitEntry ( vMapXors , Fanin ) ) { assert ( Rank == Vec_IntEntry ( vRanks , Fanin ) ) ; continue ; } if ( Vec_IntEntry ( vMapMajs , Fanin ) == -1 ) Vec_WecPush ( vXorLeaves , Rank , Fanin ) ; else if ( Vec_IntEntry ( vRanks , Xor ) > 0 ) Vec_WecPush ( vAddBoxes , Rank - 1 , Vec_IntEntry ( vMapMajs , Fanin ) ) ; } } Vec_BitFree ( vMapXors ) ; Vec_IntFree ( vMapMajs ) ; if ( pvAddBoxes ) * pvAddBoxes = vAddBoxes ; return vXorLeaves ; }
collects leaves of each XOR tree
collects leaves of each XOR tree
//int RankFanin = Vec_IntEntry(vRanks, Fanin); //            if ( Vec_BitEntry(vMapXors, Fanin) && Rank == RankFanin ) //                continue; // no adder driving this input // save adder box