abc/src/proof/acec/acecFadds.c
// map SUM bits and topmost MAJ into topmost FADD number
map SUM bits and topmost MAJ into topmost FADD number
map SUM bits and topmost MAJ into topmost FADD number
Vec_Int_t * Gia_ManFindMapping( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains )
{
    Vec_Int_t * vChain;
    int i, k, iFadd = -1;
    Vec_Int_t * vMap2Chain = Vec_IntStartFull( Gia_ManObjNum(p) );
    Vec_WecForEachLevel( vChains, vChain, i )
    {
        assert( Vec_IntSize(vChain) > 0 );
        Vec_IntForEachEntry( vChain, iFadd, k )
        {
            assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3)) == -1 );
            Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3), i );
        }
        assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4)) == -1 );
        Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4), i );
    }
    return vMap2Chain;
}
Vec_Int_t * Gia_ManFindMapping ( Gia_Man_t * p , Vec_Int_t * vFadds , Vec_Int_t * vMap , Vec_Wec_t * vChains ) { Vec_Int_t * vChain ; int i , k , iFadd = -1 ; Vec_Int_t * vMap2Chain = Vec_IntStartFull ( Gia_ManObjNum ( p ) ) ; Vec_WecForEachLevel ( vChains , vChain , i ) { assert ( Vec_IntSize ( vChain ) > 0 ) ; Vec_IntForEachEntry ( vChain , iFadd , k ) { assert ( Vec_IntEntry ( vMap2Chain , Vec_IntEntry ( vFadds , 5 * iFadd + 3 ) ) == -1 ) ; Vec_IntWriteEntry ( vMap2Chain , Vec_IntEntry ( vFadds , 5 * iFadd + 3 ) , i ) ; } assert ( Vec_IntEntry ( vMap2Chain , Vec_IntEntry ( vFadds , 5 * iFadd + 4 ) ) == -1 ) ; Vec_IntWriteEntry ( vMap2Chain , Vec_IntEntry ( vFadds , 5 * iFadd + 4 ) , i ) ; } return vMap2Chain ; }
map SUM bits and topmost MAJ into topmost FADD number
map SUM bits and topmost MAJ into topmost FADD number
//printf( "Chain %d: setting SUM %d (obj %d)\n", i, k, Vec_IntEntry(vFadds, 5*iFadd+3) ); //printf( "Chain %d: setting CARRY (obj %d)\n", i, Vec_IntEntry(vFadds, 5*iFadd+4) );