ifDec10.c

/**CFile****************************************************************

  FileName    [ifDec10.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [FPGA mapping based on priority cuts.]

  Synopsis    [Performs additional check.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - November 21, 2006.]

  Revision    [$Id: ifDec10.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]

***********************************************************************/

#include "if.h"
#include "misc/extra/extra.h"
#include "bool/kit/kit.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// the bit count for the first 256 integer numbers
static int BitCount8[256] = {
    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};
// variable swapping code
static word PMasks[5][3] = {
    { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
    { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
    { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
    { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
    { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
};
// elementary truth tables
static word Truth6[6] = {
    ABC_CONST(0xAAAAAAAAAAAAAAAA),
    ABC_CONST(0xCCCCCCCCCCCCCCCC),
    ABC_CONST(0xF0F0F0F0F0F0F0F0),
    ABC_CONST(0xFF00FF00FF00FF00),
    ABC_CONST(0xFFFF0000FFFF0000),
    ABC_CONST(0xFFFFFFFF00000000)
};
static word Truth10[10][16] = {
    {ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA)},
    {ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC)},
    {ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0)},
    {ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00)},
    {ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000)},
    {ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000)},
    {ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
    {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
    {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
    {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)}
};

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

static inline int If_Dec10WordNum( int nVars )
{
    return nVars <= 6 ? 1 : 1 << (nVars-6);
}
static void If_Dec10PrintConfigOne( unsigned z )
{
    unsigned t;
    t = (z & 0xffff) | ((z & 0xffff) << 16);
    Extra_PrintBinary( stdout, &t, 16 ); 
    printf( " " );
    Kit_DsdPrintFromTruth( &t, 4 );
    printf( " " );
    printf( " %d", (z >> 16) & 7 );
    printf( " %d", (z >> 20) & 7 );
    printf( " %d", (z >> 24) & 7 );
    printf( " %d", (z >> 28) & 7 );
    printf( "\n" );
}
void If_Dec10PrintConfig( unsigned * pZ )
{
    while ( *pZ )
        If_Dec10PrintConfigOne( *pZ++ );
}
static inline void If_Dec10ComposeLut4( int t, word ** pF, word * pR, int nVars )
{
    word pC[16];
    int m, w, v, nWords;
    assert( nVars <= 10 );
    nWords = If_Dec10WordNum( nVars );
    for ( w = 0; w < nWords; w++ )
        pR[w] = 0;
    for ( m = 0; m < 16; m++ )
    {
        if ( !((t >> m) & 1) )
            continue;
        for ( w = 0; w < nWords; w++ )
            pC[w] = ~(word)0;
        for ( v = 0; v < 4; v++ )
            for ( w = 0; w < nWords; w++ )
                pC[w] &= ((m >> v) & 1) ? pF[v][w] : ~pF[v][w];
        for ( w = 0; w < nWords; w++ )
            pR[w] |= pC[w];
    }
}
void If_Dec10Verify( word * pF, int nVars, unsigned * pZ )
{
    word pN[16][16], * pG[4];
    int i, w, v, k, nWords;
    unsigned z;
    nWords = If_Dec10WordNum( nVars );
    for ( k = 0; k < nVars; k++ )
        for ( w = 0; w < nWords; w++ )
            pN[k][w] = Truth10[k][w];
    for ( i = 0; (z = pZ[i]); i++, k++ )
    {
        for ( v = 0; v < 4; v++ )
            pG[v] = pN[ (z >> (16+(v<<2))) & 7 ];
        If_Dec10ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars );
    }
    k--;
    for ( w = 0; w < nWords; w++ )
        if ( pN[k][w] != pF[w] )
        {
            If_Dec10PrintConfig( pZ );
            Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
            Kit_DsdPrintFromTruth( (unsigned*)pN[k], nVars ); printf( "\n" );
            printf( "Verification failed!\n" );
            break;
        }
}


// count the number of unique cofactors
static inline int If_Dec10CofCount2( word * pF, int nVars )
{
    int nShift = (1 << (nVars - 4));
    word Mask  = (((word)1) << nShift) - 1;
    word iCof0 = pF[0] & Mask;
    word iCof1 = iCof0, iCof;
    int i;
    assert( nVars > 6 && nVars <= 10 );
    if ( nVars == 10 )
        Mask = ~(word)0;
    for ( i = 1; i < 16; i++ )
    {
        iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
        if ( iCof == iCof0 )
            continue;
        if ( iCof1 == iCof0 )
            iCof1 = iCof;
        else if ( iCof != iCof1 )
            return 3;
    }
    return 2;
}
static inline int If_Dec10CofCount( word * pF, int nVars )
{
    int nShift = (1 << (nVars - 4));
    word Mask  = (((word)1) << nShift) - 1;
    word iCofs[16], iCof;
    int i, c, nCofs = 1;
    if ( nVars == 10 )
        Mask = ~(word)0;
    iCofs[0] = pF[0] & Mask;
    for ( i = 1; i < 16; i++ )
    {
        iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
        for ( c = 0; c < nCofs; c++ )
            if ( iCof == iCofs[c] )
                break;
        if ( c == nCofs )
            iCofs[nCofs++] = iCof;
    }
    return nCofs;
}


// variable permutation for large functions
static inline void If_Dec10Copy( word * pOut, word * pIn, int nVars )
{
    int w, nWords = If_Dec10WordNum( nVars );
    for ( w = 0; w < nWords; w++ )
        pOut[w] = pIn[w];
}
static inline void If_Dec10SwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
{
    int i, k, nWords = If_Dec10WordNum( nVars );
    assert( iVar < nVars - 1 );
    if ( iVar < 5 )
    {
        int Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
    }
    else if ( iVar > 5 )
    {
        int Step = (1 << (iVar - 6));
        for ( k = 0; k < nWords; k += 4*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pIn[i];
            for ( i = 0; i < Step; i++ )
                pOut[Step+i] = pIn[2*Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[2*Step+i] = pIn[Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[3*Step+i] = pIn[3*Step+i];
            pIn  += 4*Step;
            pOut += 4*Step;
        }
    }
    else // if ( iVar == 5 )
    {
        for ( i = 0; i < nWords; i += 2 )
        {
            pOut[i]   = (pIn[i]   & ABC_CONST(0x00000000FFFFFFFF)) | ((pIn[i+1] & ABC_CONST(0x00000000FFFFFFFF)) << 32);
            pOut[i+1] = (pIn[i+1] & ABC_CONST(0xFFFFFFFF00000000)) | ((pIn[i]   & ABC_CONST(0xFFFFFFFF00000000)) >> 32);
        }
    }
}
static inline void If_Dec10MoveTo( word * pF, int nVars, int v, int p, int Pla2Var[], int Var2Pla[] )
{
    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
    int iPlace0, iPlace1, Count = 0;
    assert( Var2Pla[v] <= p );
    while ( Var2Pla[v] != p )
    {
        iPlace0 = Var2Pla[v];
        iPlace1 = Var2Pla[v]+1;
        If_Dec10SwapAdjacent( pOut, pIn, iPlace0, nVars );
        pTemp = pIn; pIn = pOut, pOut = pTemp;
        Var2Pla[Pla2Var[iPlace0]]++;
        Var2Pla[Pla2Var[iPlace1]]--;
        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
        Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
        Count++;
    }
    if ( Count & 1 )
        If_Dec10Copy( pF, pIn, nVars );
    assert( Pla2Var[p] == v );
}
/*
// derive binary function
static inline int If_Dec10DeriveCount2( word * pF, word * pRes, int nVars )
{
    int nShift = (1 << (nVars - 4));
    word Mask  = (((word)1) << nShift) - 1;
    int i, MaskDec = 0;
    word iCof0 = pF[0] & Mask;
    word iCof1 = pF[0] & Mask;
    word iCof, * pCof0, * pCof1;
    if ( nVars == 10 )
        Mask = ~(word)0;
    for ( i = 1; i < 16; i++ )
    {
        iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
        if ( *pCof0 != iCof )
        {
            *pCof1 = iCof;
            MaskDec |= (1 << i);
        }
    }
    *pRes = ((iCof1 << nShift) | iCof0);
    return MaskDec;
}
static inline word If_DecTruthStretch( word t, int nVars )
{
    assert( nVars > 1 );
    if ( nVars == 1 )
        nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
    if ( nVars == 2 )
        nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
    if ( nVars == 3 )
        nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
    if ( nVars == 4 )
        nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
    if ( nVars == 5 )
        nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
    assert( nVars >= 6 );
}
*/

// support minimization
static inline int If_DecSuppIsMinBase( int Supp )
{
    return (Supp & (Supp+1)) == 0;
}
static inline int If_Dec10HasVar( word * t, int nVars, int iVar )
{
    int nWords = If_Dec10WordNum( nVars );
    assert( iVar < nVars );
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
                return 1;
        return 0;
    }
    else
    {
        int i, k, Step = (1 << (iVar - 6));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                if ( t[i] != t[Step+i] )
                    return 1;
            t += 2*Step;
        }
        return 0;
    }
}
static inline int If_Dec10Support( word * t, int nVars )
{
    int v, Supp = 0;
    for ( v = 0; v < nVars; v++ )
        if ( If_Dec10HasVar( t, nVars, v ) )
            Supp |= (1 << v);
    return Supp;
}

// checks
void If_Dec10Cofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 )
{
    int nWords = If_Dec10WordNum( nVars );
    assert( iVar < nVars );
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
        {
            pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
            pCof1[i] = (pF[i] &  Truth6[iVar]) | ((pF[i] &  Truth6[iVar]) >> Shift);
        }
        return;
    }
    else
    {
        int i, k, Step = (1 << (iVar - 6));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pCof0[i] = pCof0[Step+i] = pF[i];
                pCof1[i] = pCof1[Step+i] = pF[Step+i];
            }
            pF    += 2*Step;
            pCof0 += 2*Step;
            pCof1 += 2*Step;
        }
        return;
    }
}
static inline int If_Dec10Count16( int Num16 )
{
    assert( Num16 < (1<<16)-1 );
    return BitCount8[Num16 & 255] + BitCount8[(Num16 >> 8) & 255];
}
static inline void If_DecVerifyPerm( int Pla2Var[10], int Var2Pla[10], int nVars )
{
    int i;
    for ( i = 0; i < nVars; i++ )
        assert( Pla2Var[Var2Pla[i]] == i );
} 
int If_Dec10Perform( word * pF, int nVars, int fDerive )
{ 
//    static int Cnt = 0;
    word pCof0[16], pCof1[16];
    int Pla2Var[10], Var2Pla[10], Count[210], Masks[210];
    int i, i0,i1,i2,i3, v, x;
    assert( nVars >= 6 && nVars <= 10 );
    // start arrays
    for ( i = 0; i < nVars; i++ )
    {
        assert( If_Dec10HasVar( pF, nVars, i ) );
        Pla2Var[i] = Var2Pla[i] = i;
    }
/*
    Cnt++;
//if ( Cnt == 108 )
{
printf( "%d\n", Cnt );
//Extra_PrintHex( stdout, (unsigned *)pF, nVars );
//printf( "\n" ); 
Kit_DsdPrintFromTruth( (unsigned *)pF, nVars );
printf( "\n" );
printf( "\n" );
}
*/
    // generate permutations
    v = 0;
    for ( i0 = 0;    i0 < nVars; i0++ )
    for ( i1 = i0+1; i1 < nVars; i1++ )
    for ( i2 = i1+1; i2 < nVars; i2++ )
    for ( i3 = i2+1; i3 < nVars; i3++, v++ )
    {
        If_Dec10MoveTo( pF, nVars, i0, nVars-1, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i1, nVars-2, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i2, nVars-3, Pla2Var, Var2Pla );
        If_Dec10MoveTo( pF, nVars, i3, nVars-4, Pla2Var, Var2Pla );
        If_DecVerifyPerm( Pla2Var, Var2Pla, nVars );
        Count[v] = If_Dec10CofCount( pF, nVars );
        Masks[v] = (1 << i0) | (1 << i1) | (1 << i2) | (1 << i3);
        assert( Count[v] > 1 );
//printf( "%d ", Count[v] );
        if ( Count[v] == 2 || Count[v] > 5 )
            continue;
        for ( x = 0; x < 4; x++ )
        {
            If_Dec10Cofactors( pF, nVars, nVars-1-x, pCof0, pCof1 );
            if ( If_Dec10CofCount2(pCof0, nVars) <= 2 && If_Dec10CofCount2(pCof1, nVars) <= 2 )
            {
                Count[v] = -Count[v];
                break;
            }
        }
    }
//printf( "\n" );
    assert( v <= 210 );
    // check if there are compatible bound sets
    for ( i0 = 0; i0 < v; i0++ )
    for ( i1 = i0+1; i1 < v; i1++ )
    {
        if ( If_Dec10Count16(Masks[i0] & Masks[i1]) > 10 - nVars )
            continue;
        if ( nVars == 10 )
        {
            if ( Count[i0] == 2 && Count[i1] == 2 )
                return 1;
        }
        else if ( nVars == 9 )
        {
            if ( (Count[i0] == 2 && Count[i1] == 2) || 
                 (Count[i0] == 2 && Count[i1] <  0) || 
                 (Count[i0] <  0 && Count[i1] == 2) )
                return 1;
        }
        else
        {
            if ( (Count[i0] == 2 && Count[i1] == 2) || 
                 (Count[i0] == 2 && Count[i1] <  0) || 
                 (Count[i0] <  0 && Count[i1] == 2) || 
                 (Count[i0] <  0 && Count[i1] <  0) )
                return 1;
        }
    }
//    printf( "not found\n" );
    return 0;
}


/**Function*************************************************************

  Synopsis    [Performs additional check.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
    int nSupp, fDerive = 0;
    word pF[16];
    if ( nLeaves <= 6 )
        return 1;
    If_Dec10Copy( pF, (word *)pTruth, nVars );
    nSupp = If_Dec10Support( pF, nLeaves );
    if ( !nSupp || !If_DecSuppIsMinBase(nSupp) )
        return 0;
    if ( If_Dec10Perform( pF, nLeaves, fDerive ) )
    {
//        printf( "1" );
        return 1;
//        If_Dec10Verify( t, nLeaves, NULL );
    }
//    printf( "0" );
    return 0;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END