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

  FileName    [ FxchDiv.c ]

  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]

  Synopsis    [ Divisor handling functions ]

  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]

  Affiliation [ UFRGS ]

  Date        [ Ver. 1.0. Started - March 6, 2016. ]

  Revision    []

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

#include "Fxch.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// FUNCTION DEFINITIONS
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree )
{
    int * L = Vec_IntArray(vCubeFree);
    int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1;
    assert( Vec_IntSize(vCubeFree) == 4 );
    if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars
    {
        if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) )
            return -1;
        LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]);
        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) )
        {
            assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) );
            LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]);
        }
        else
        {
            assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) );
            assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) );
            LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]);
        }
    }
    else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) )
    {
        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) )
            return -1;
        LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]);
        if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) )
            LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]);
        else
            LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]);
    }
    else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) )
    {
        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) )
            return -1;
        LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]);
        if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) )
            LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]);
        else
            LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]);
    }
    else
        return -1;
    assert( LitA0 == Abc_LitNot(LitB0) );
    if ( Abc_LitIsCompl(LitA0) )
    {
        ABC_SWAP( int, LitA0, LitB0 );
        ABC_SWAP( int, LitA1, LitB1 );
    }
    assert( !Abc_LitIsCompl(LitA0) );
    if ( Abc_LitIsCompl(LitA1) )
    {
        LitA1 = Abc_LitNot(LitA1);
        LitB1 = Abc_LitNot(LitB1);
        RetValue = 1;
    }
    assert( !Abc_LitIsCompl(LitA1) );
    // arrange literals in such as a way that
    // - the first two literals are control literals from different cubes
    // - the third literal is non-complented data input
    // - the forth literal is possibly complemented data input
    L[0] = Abc_Var2Lit( LitA0, 0 );
    L[1] = Abc_Var2Lit( LitB0, 1 );
    L[2] = Abc_Var2Lit( LitA1, 0 );
    L[3] = Abc_Var2Lit( LitB1, 1 );
    return RetValue;
}

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

  Synopsis    [ Creates a Divisor. ]

  Description [ This functions receive as input two sub-cubes and creates
                a divisor using their information. The divisor is stored 
                in vCubeFree vector of the pFxchMan structure.
                
                It returns the base value, which is the number of elements
                that the cubes pair used to generate the devisor have in
                common. ]

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
                    Fxch_SubCube_t* pSubCube0,
                    Fxch_SubCube_t* pSubCube1 )
{
    int Base = 0;

    int SC0_Lit0,
        SC0_Lit1,
        SC1_Lit0,
        SC1_Lit1;

    int Cube0Size,
        Cube1Size;

    Vec_IntClear( pFxchMan->vCubeFree );

    SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
    SC0_Lit1 = 0;
    SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
    SC1_Lit1 = 0;

    if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
    {
        Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
        Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
    }
    else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
    {
        int RetValue;

        SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
        SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );

        if ( SC0_Lit0 < SC1_Lit0 )
        {
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
        }
        else
        {
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
        }

        RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
        if ( RetValue == -1 )
            return -1;
    } 
    else
    {
        if ( pSubCube0->iLit1 > 0 )
        {
            SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );

            Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
            if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
            else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
        }
        else 
        {
            SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );

            Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
            if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
            else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
        }
    }

    if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
        return -1;

    if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
    {
        Vec_IntSort( pFxchMan->vCubeFree, 0 );

        Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
        Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
    }

    Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
    Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
    if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
    {
        Base = Abc_MinInt( Cube0Size, Cube1Size )
               -( Vec_IntSize( pFxchMan->vCubeFree ) / 2)  - 1; /* 1 or 2 Lits, 1 SOP NodeID */
    }
    else
        return -1;

    return Base;
}

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

  Synopsis    [ Add a divisor to the divisors hash table. ]

  Description [ This functions will try to add the divisor store in 
                vCubeFree to the divisor hash table. If the divisor
                is already present in the hash table it will just 
                increment its weight, otherwise it will add the divisor
                and asign an initial weight. ]

  SideEffects [ If the fUpdate option is set, the function will also
                update the divisor priority queue. ]

  SeeAlso     []

***********************************************************************/
int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
                 int fUpdate,
                 int fSingleCube,
                 int fBase )
{
    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );

    /* Verify if the divisor already exist */ 
    if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
    {
        Vec_WecPushLevel( pFxchMan->vDivCubePairs );

        /* Assign initial weight */
        if ( fSingleCube )
        {
            Vec_FltPush( pFxchMan->vDivWeights,
                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
                         -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
        }
        else
        {
            Vec_FltPush( pFxchMan->vDivWeights,
                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
                         -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
        }

    }

    /* Increment weight */
    if ( fSingleCube )
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
    else
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );

    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );

    if ( fUpdate )
        if ( pFxchMan->vDivPrio )
        {
            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
            else
                Vec_QuePush( pFxchMan->vDivPrio, iDiv );
        }

    return iDiv;
}

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

  Synopsis    [ Removes a divisor to the divisors hash table. ]

  Description [ This function don't effectively removes a divisor from
                the hash table (the hash table implementation don't 
                support such operation). It only assures its existence
                and decrement its weight. ]

  SideEffects [ If the fUpdate option is set, the function will also
                update the divisor priority queue. ]

  SeeAlso     []

***********************************************************************/
int Fxch_DivRemove( Fxch_Man_t* pFxchMan,
                    int fUpdate,
                    int fSingleCube,
                    int fBase )
{
    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );

    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );

    /* Decrement weight */
    if ( fSingleCube )
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
    else
        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );

    if ( fUpdate )
        if ( pFxchMan->vDivPrio )
        {
            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
        }

    return iDiv;
}

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

  Synopsis    [ Separete the cubes in present in a divisor ]

  Description [ In this implementation *all* stored divsors are composed 
                of two cubes. 

                In order to save space and to be able to use the Vec_Int_t
                hash table both cubes are stored in the same vector - using
                a little hack to differentiate which literal belongs to each
                cube.

                This function separetes the two cubes in their own vectors
                so that they can be added to the cover.

                *Note* that this also applies to single cube 
                divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxch_DivSepareteCubes( Vec_Int_t* vDiv,
                            Vec_Int_t* vCube0,
                            Vec_Int_t* vCube1 )
{
    int* pArray;
    int i,
        Lit;

    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl(Lit) )
            Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
        else
            Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );

    if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
    {
        assert( Vec_IntSize( vCube1 ) == 3 );

        pArray = Vec_IntArray( vCube0 );
        if ( pArray[1] > pArray[2] )
            ABC_SWAP( int, pArray[1], pArray[2] );

        pArray = Vec_IntArray( vCube1 );
        if ( pArray[1] > pArray[2] )
            ABC_SWAP( int, pArray[1], pArray[2] );
    }
}

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

  Synopsis    [ Removes the literals present in the divisor from their 
               original cubes. ]

  Description [ This function returns the numeber of removed literals
                which should be equal to the size of the divisor. ]

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxch_DivRemoveLits( Vec_Int_t* vCube0,
                        Vec_Int_t* vCube1,
                        Vec_Int_t* vDiv,
                        int *fCompl )
{
    int i,
        Lit,
        CountP = 0,
        CountN = 0,
        Count = 0,
        ret = 0;

    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
            CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
        else
            CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );

    Vec_IntForEachEntry( vDiv, Lit, i )
        Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );

   if ( Vec_IntSize( vDiv ) == 2 )
       Vec_IntForEachEntry( vDiv, Lit, i )
       {
           Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
           Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
       }

    ret = Count + CountP + CountN;

    if ( Vec_IntSize( vDiv ) == 4 )
    {
        int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
            Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
            Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
            Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );

        if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
            *fCompl = 1;

        if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
        {
            *fCompl = 1;

            Vec_IntForEachEntry( vDiv, Lit, i )
                ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );

            Vec_IntForEachEntry( vDiv, Lit, i )
                ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
        }
    }

    return ret;
}

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

  Synopsis    [ Print the divisor identified by iDiv. ]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
                    int iDiv )
{
    Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
    int i,
        Lit;

    printf( "Div %7d : ", iDiv );
    printf( "Weight %12.5f  ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );

    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( !Abc_LitIsCompl( Lit ) )
            printf( "%d(1)", Abc_Lit2Var( Lit ) );

    printf( " + " );

    Vec_IntForEachEntry( vDiv, Lit, i )
        if ( Abc_LitIsCompl( Lit ) )
            printf( "%d(2)", Abc_Lit2Var( Lit ) );

    printf( " Lits =%7d  ", pFxchMan->nLits );
    printf( "Divs =%8d  \n", Hsh_VecSize( pFxchMan->pDivHash ) );
}

int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv )
{
    int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
        Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) );

    if ( ( Vec_IntSize( vDiv ) == 2 )  && ( Lit0 == Abc_LitNot( Lit1 ) ) )
            return 0;

    return 1;
}

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

ABC_NAMESPACE_IMPL_END