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

  FileName    [saigIso.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Sequential cleanup.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: saigIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "aig/ioa/ioa.h"
#include "saig.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Find the canonical permutation of the COs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis )
{
    extern int Iso_ObjCompareByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
    Vec_Int_t * vPermCos;
    Aig_Obj_t * pObj, * pFanin;
    int i, Entry, Diff;
    assert( Vec_IntSize(vPermCis) == Aig_ManCiNum(pAig) );
    vPermCos = Vec_IntAlloc( Aig_ManCoNum(pAig) );
    if ( Saig_ManPoNum(pAig) == 1 )
        Vec_IntPush( vPermCos, 0 );
    else
    {
        Vec_Ptr_t * vRoots = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
        Saig_ManForEachPo( pAig, pObj, i )
        {
            pFanin = Aig_ObjFanin0(pObj);
            assert( Aig_ObjIsConst1(pFanin) || pFanin->iData > 0 );
            pObj->iData = Abc_Var2Lit( pFanin->iData, Aig_ObjFaninC0(pObj) );
            Vec_PtrPush( vRoots, pObj );
        }
        Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareByData );
        Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
            Vec_IntPush( vPermCos, Aig_ObjCioId(pObj) );
        Vec_PtrFree( vRoots );
    }
    // add flop outputs
    Diff = Saig_ManPoNum(pAig) - Saig_ManPiNum(pAig);
    Vec_IntForEachEntryStart( vPermCis, Entry, i, Saig_ManPiNum(pAig) )
        Vec_IntPush( vPermCos, Entry + Diff );
    return vPermCos;
}

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

  Synopsis    [Performs canonical duplication of the AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManDupIsoCanonical_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    assert( Aig_ObjIsNode(pObj) );
    if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) || !Aig_ObjIsNode(Aig_ObjFanin1(pObj)) )
    {
        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
    }
    else
    {
        assert( Aig_ObjFanin0(pObj)->iData != Aig_ObjFanin1(pObj)->iData );
        if ( Aig_ObjFanin0(pObj)->iData < Aig_ObjFanin1(pObj)->iData )
        {
            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
        }
        else
        {
            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
        }
    }
    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}

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

  Synopsis    [Performs canonical duplication of the AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    Vec_Int_t * vPerm, * vPermCo;
    int i, Entry;
    // derive permutations
    vPerm   = Saig_ManFindIsoPerm( pAig, fVerbose );
    vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm );
    // create the new manager
    pNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pNew->pName = Abc_UtilStrsav( pAig->pName );
    Aig_ManIncrementTravId( pAig );
    // create constant
    pObj = Aig_ManConst1(pAig);
    pObj->pData = Aig_ManConst1(pNew);
    Aig_ObjSetTravIdCurrent( pAig, pObj );
    // create PIs
    Vec_IntForEachEntry( vPerm, Entry, i )
    {
        pObj = Aig_ManCi(pAig, Entry);
        pObj->pData = Aig_ObjCreateCi(pNew);
        Aig_ObjSetTravIdCurrent( pAig, pObj );
    }
    // traverse from the POs
    Vec_IntForEachEntry( vPermCo, Entry, i )
    {
        pObj = Aig_ManCo(pAig, Entry);
        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
    }
    // create POs
    Vec_IntForEachEntry( vPermCo, Entry, i )
    {
        pObj = Aig_ManCo(pAig, Entry);
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
    Vec_IntFreeP( &vPerm );
    Vec_IntFreeP( &vPermCo );
    return pNew;
}





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

  Synopsis    [Checks structural equivalence of AIG1 and AIG2.]

  Description [Returns 1 if AIG1 and AIG2 are structurally equivalent 
  under this mapping.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose )
{
    Aig_Obj_t * pObj, * pFanin0, * pFanin1;
    int i;
    assert( Aig_ManCiNum(pAig1) == Aig_ManCiNum(pAig2) );
    assert( Aig_ManCoNum(pAig1) == Aig_ManCoNum(pAig2) );
    assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) );
    assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) );
    Aig_ManCleanData( pAig1 );
    // map const and PI nodes
    Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1);
    Aig_ManForEachCi( pAig2, pObj, i )
        pObj->pData = Aig_ManCi( pAig1, Vec_IntEntry(vMap2to1, i) );
    // try internal nodes
    Aig_ManForEachNode( pAig2, pObj, i )
    {
        pFanin0 = Aig_ObjChild0Copy( pObj );
        pFanin1 = Aig_ObjChild1Copy( pObj );
        pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 );
        if ( pObj->pData == NULL )
        {
            if ( fVerbose )
                printf( "Structural equivalence failed at node %d.\n", i );
            return 0;
        }
    }
    // make sure the first PO points to the same node
    if ( Aig_ManCoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManCo(pAig2, 0)) != Aig_ObjChild0(Aig_ManCo(pAig1, 0)) )
    {
        if ( fVerbose )
            printf( "Structural equivalence failed at primary output 0.\n" );
        return 0;
    }
    return 1;    
}

//static int s_Counter;

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    if ( pAig->nComplEdges > 0 )
        return pAig->nComplEdges;
    Aig_ManForEachObj( pAig, pObj, i )
        if ( Aig_ObjIsNode(pObj) )
        {
            Counter += Aig_ObjFaninC0(pObj);
            Counter += Aig_ObjFaninC1(pObj);
        }
        else if ( Aig_ObjIsCo(pObj) )
            Counter += Aig_ObjFaninC0(pObj);
    return (pAig->nComplEdges = Counter);
}

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

  Synopsis    [Finds mapping of CIs of AIG2 into those of AIG1.]

  Description [Returns the mapping of CIs of the two AIGs, or NULL
  if there is no mapping.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
{
    Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
    int i, Entry;
    if ( Aig_ManCiNum(pAig1) != Aig_ManCiNum(pAig2) )
        return NULL;
    if ( Aig_ManCoNum(pAig1) != Aig_ManCoNum(pAig2) )
        return NULL;
    if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) )
        return NULL;
    if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) )
        return NULL;
    if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) )
        return NULL;
//    if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
//        return NULL;
//    s_Counter++;

    if ( fVerbose ) 
        printf( "AIG1:\n" );
    vPerm1 = vPerm1_ ? vPerm1_ : Saig_ManFindIsoPerm( pAig1, fVerbose );
    if ( fVerbose )
        printf( "AIG1:\n" );
    vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose );
    if ( vPerm1_ )
        assert( Vec_IntSize(vPerm1_) == Aig_ManCiNum(pAig1) );
    if ( vPerm2_ )
        assert( Vec_IntSize(vPerm2_) == Aig_ManCiNum(pAig2) );
    // find canonical permutation
    // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
    vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
    Vec_IntForEachEntry( vInvPerm2, Entry, i )
    {
        assert( Entry >= 0 && Entry < Aig_ManCiNum(pAig1) );
        Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
    }
    if ( vPerm1_ == NULL )
        Vec_IntFree( vPerm1 );
    if ( vPerm2_ == NULL )
        Vec_IntFree( vPerm2 );
    // check if they are indeed equivalent
    if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
        Vec_IntFreeP( &vInvPerm2 );
    return vInvPerm2;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose )
{
    int fVeryVerbose = 0;
    Vec_Ptr_t * vParts, * vPerms, * vAigs;
    Vec_Int_t * vPos, * vMap;
    Aig_Man_t * pPart, * pTemp;
    int i, k, nPos;

    // derive AIG for each PO
    nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
    vParts = Vec_PtrAlloc( nPos );
    vPerms = Vec_PtrAlloc( nPos );
    for ( i = 0; i < nPos; i++ )
    {
        pPart = Saig_ManDupCones( pAig, &i, 1 );
        vMap  = Saig_ManFindIsoPerm( pPart, fVeryVerbose );
        Vec_PtrPush( vParts, pPart ); 
        Vec_PtrPush( vPerms, vMap );
    }
//    s_Counter = 0;

    // check AIGs for each PO
    vAigs = Vec_PtrAlloc( 1000 );
    vPos  = Vec_IntAlloc( 1000 );
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
    {
        if ( fVeryVerbose )
        {
            printf( "AIG %4d : ", i );
            Aig_ManPrintStats( pPart );
        }
        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
        {
            if ( fVeryVerbose )
                printf( "Comparing AIG %4d and AIG %4d.  ", Vec_IntEntry(vPos,k), i );
            vMap = Iso_ManFindMapping( pTemp, pPart, 
                (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)), 
                (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
                fVeryVerbose );
            if ( vMap != NULL )
            {
                if ( fVeryVerbose )
                    printf( "Found match\n" );
//                if ( fVerbose )
//                    printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
                Vec_IntFree( vMap );
                break;
            }
            if ( fVeryVerbose )
                printf( "No match.\n" );
        }
        if ( k == Vec_PtrSize(vAigs) )
        {
            Vec_PtrPush( vAigs, pPart );
            Vec_IntPush( vPos, i );
        }
    }
    // delete AIGs
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
        Aig_ManStop( pPart );
    Vec_PtrFree( vParts );
    Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
        Vec_IntFree( vMap );
    Vec_PtrFree( vPerms );
    // derive the resulting AIG
    pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
    Vec_PtrFree( vAigs );
    Vec_IntFree( vPos );

//    printf( "The number of all checks %d.  Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
    return pPart;
}

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

  Synopsis    [Takes multi-output sequential AIG.]

  Description [Returns candidate equivalence classes of POs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
{
    return Vec_StrCompareVec( *p1, *p2 );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
{
//    int fVeryVerbose = 0;
    Aig_Man_t * pPart, * pTemp;
    Vec_Ptr_t * vBuffers, * vClasses;
    Vec_Int_t * vLevel, * vRemain;
    Vec_Str_t * vStr, * vPrev;
    int i, nPos;
    abctime clk = Abc_Clock();
    abctime clkDup = 0, clkAig = 0, clkIso = 0, clk2;
    *pvPosEquivs = NULL;

    // derive AIG for each PO
    nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
    vBuffers = Vec_PtrAlloc( nPos );
    for ( i = 0; i < nPos; i++ )
    {
        if ( i % 100 == 0 )
            printf( "%6d finished...\r", i );

        clk2 = Abc_Clock();
        pPart = Saig_ManDupCones( pAig, &i, 1 );
        clkDup += Abc_Clock() - clk2;

        clk2 = Abc_Clock();
        pTemp = Saig_ManDupIsoCanonical( pPart, 0 );
        clkIso += Abc_Clock() - clk2;

        clk2 = Abc_Clock();
        vStr  = Ioa_WriteAigerIntoMemoryStr( pTemp );
        clkAig += Abc_Clock() - clk2;

        Vec_PtrPush( vBuffers, vStr );
        Aig_ManStop( pTemp );
        Aig_ManStop( pPart );
        // remember the output number in nCap (attention: hack!)
        vStr->nCap = i;
    }
//    s_Counter = 0;
    if ( fVerbose )
    {
    Abc_PrintTime( 1, "Duplicate time", clkDup );
    Abc_PrintTime( 1, "Isomorph  time", clkIso );
    Abc_PrintTime( 1, "AIGER     time", clkAig );
    }

    // sort the infos
    clk = Abc_Clock();
    Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr );

    // create classes
    clk = Abc_Clock();
    vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
    // start the first class
    Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
    vPrev = (Vec_Str_t *)Vec_PtrEntry( vBuffers, 0 );
    Vec_IntPush( vLevel, vPrev->nCap );
    // consider other classes
    Vec_PtrForEachEntryStart( Vec_Str_t *, vBuffers, vStr, i, 1 )
    {
        if ( Vec_StrCompareVec(vPrev, vStr) )
            Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
        vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
        Vec_IntPush( vLevel, vStr->nCap );
        vPrev = vStr;
    }
    Vec_VecFree( (Vec_Vec_t *)vBuffers );

    if ( fVerbose )
    Abc_PrintTime( 1, "Sorting   time", Abc_Clock() - clk );
//    Abc_PrintTime( 1, "Traversal time", time_Trav );

    // report the results
//    Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
//    printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
/*
    if ( fVerbose )
    {
        Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
            if ( Vec_IntSize(vLevel) > 1 )
                printf( "%d ", Vec_IntSize(vLevel) );
            else
                nUnique++;
        printf( " Unique = %d\n", nUnique );
    }
*/

    // canonicize order
    Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
        Vec_IntSort( vLevel, 0 );
     Vec_VecSortByFirstInt( (Vec_Vec_t *)vClasses, 0 );
       
    // collect the first ones
    vRemain = Vec_IntAlloc( 100 );
    Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
        Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );

    // derive the resulting AIG
    pPart = Saig_ManDupCones( pAig, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
    Vec_IntFree( vRemain );

//    return (Vec_Vec_t *)vClasses;
//    Vec_VecFree( (Vec_Vec_t *)vClasses );
    *pvPosEquivs = vClasses;
    return pPart;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
{
    Vec_Int_t * vPerm;
    abctime clk = Abc_Clock();
    vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
    Vec_IntFree( vPerm );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return NULL;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
{ 
    Aig_Man_t * pPart;
    abctime clk = Abc_Clock();
    pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
    printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( fVerbose && *pvPosEquivs && Saig_ManPoNum(pAig) != Vec_PtrSize(*pvPosEquivs) )
    {
        printf( "Nontrivial classes:\n" );
        Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 );
    }
//    Aig_ManStopP( &pPart );
    return pPart;
}

ABC_NAMESPACE_IMPL_END

#include "base/abc/abc.h"

ABC_NAMESPACE_IMPL_START

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose )
{
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
    Abc_Ntk_t * pNtk;
    Aig_Man_t * pAig2;
    Vec_Int_t * vMap;
    
    pNtk = Abc_NtkFromAigPhase( pAig1 );
    Abc_NtkPermute( pNtk, 1, 0, 1, NULL );
    pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
    Abc_NtkDelete( pNtk );

    vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
    Aig_ManStop( pAig2 );

    if ( vMap != NULL )
    {
        printf( "Mapping of AIGs is found.\n" );
        if ( fVerbose )
            Vec_IntPrint( vMap );
    }
    else
        printf( "Mapping of AIGs is NOT found.\n" );
    Vec_IntFreeP( &vMap );
    return NULL;
}

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


ABC_NAMESPACE_IMPL_END