Probably a bug in the function Dtc_ManCutMerge (in abc/src/proof/acec/acecFadds.c)

[Hinataee]

It seems that every element in vCutsXor/vCutsMaj is a Xor/Maj. However, in Function Gia_ManDetectFullAdders, it show that every 4 elements correspond to a Xor/Maj which include another 3 inputs ids. Maybe developers forgot to remove test codes? The part between ** in the following code probably should be modified.

void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor2, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj )
{
    int fVerbose = 0;
    Vec_Int_t * vTemp;
    int i, k, c, Type, * pCut0, * pCut1, pCut[4];
    if ( fVerbose )
        printf( "Object %d = :\n", iObj );
    Vec_IntFill( vCuts, 2, 1 );
    Vec_IntPush( vCuts, iObj );
    Dtc_ForEachCut( pList0, pCut0, i )
    Dtc_ForEachCut( pList1, pCut1, k )
    {
        if ( !Dtc_ManCutMergeOne(pCut0, pCut1, pCut) )
            continue;
        if ( Dtc_ManCutCheckEqual(vCuts, pCut) )
            continue;
        Vec_IntAddToEntry( vCuts, 0, 1 );  
        if ( fVerbose )
            printf( "%d : ", pCut[0] );
        for ( c = 0; c <= pCut[0]; c++ )
        {
            Vec_IntPush( vCuts, pCut[c] );
            if ( fVerbose && c )
                printf( "%d ", pCut[c] );
        }
        if ( fVerbose )
            printf( "\n" );
        if ( pCut[0] == 2 )
        {
            int Value = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
            assert( Value == 3 || Value == 0 );
            if ( Value == 3 )
            {
                Vec_IntPush( vCutsXor2, pCut[1] );
                Vec_IntPush( vCutsXor2, pCut[2] );
                Vec_IntPush( vCutsXor2, iObj );
            }
            continue;
        }
        if ( pCut[0] != 3 )
            continue;
        Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
        if ( Type == 0 )
            continue;
        vTemp = Type == 1 ? vCutsXor : vCutsMaj;
        **if ( 0 && Type == 2 )
        {
            fVerbose = 1;
            if ( fVerbose )
                printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
            for ( c = 1; c <= pCut[0]; c++ )
            {
                if ( fVerbose )
                    printf( " %d", pCut[c] );
                Vec_IntPush( vTemp, pCut[c] );
            }
            if ( fVerbose )
                printf( " )\n" );
            fVerbose = 0;
        }**
        Vec_IntPush( vTemp, iObj ); // only one element is put into vCutsXor/vCutsMaj
    }