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

  FileName    [sswIslands.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Detection of islands of difference.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Creates pair of structurally equivalent nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
    pObj0->pData = pObj1;
    pObj1->pData = pObj0;
    Vec_IntPush( vPairs, pObj0->Id );
    Vec_IntPush( vPairs, pObj1->Id );
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
{
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // create matching
    Aig_ManCleanData( p0 );
    Aig_ManCleanData( p1 );
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
        pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
        assert( pObj0->pData == NULL );
        assert( pObj1->pData == NULL );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
    }
    // make sure constants are matched
    pObj0 = Aig_ManConst1( p0 );
    pObj1 = Aig_ManConst1( p1 );
    assert( pObj0->pData == pObj1 );
    assert( pObj1->pData == pObj0 );
    // make sure PIs are matched
    Saig_ManForEachPi( p0, pObj0, i )
    {
        pObj1 = Aig_ManCi( p1, i );
        assert( pObj0->pData == pObj1 );
        assert( pObj1->pData == pObj0 );
    }
    // make sure the POs are not matched
    Aig_ManForEachCo( p0, pObj0, i )
    {
        pObj1 = Aig_ManCo( p1, i );
        assert( pObj0->pData == NULL );
        assert( pObj1->pData == NULL );
    }

    // check that LIs/LOs are matched in sync
    Saig_ManForEachLo( p0, pObj0, i )
    {
        if ( pObj0->pData == NULL )
            continue;
        pObj1 = (Aig_Obj_t *)pObj0->pData;
        if ( !Saig_ObjIsLo(p1, pObj1) )
            Abc_Print( 1, "Mismatch between LO pairs.\n" );
    }
    Saig_ManForEachLo( p1, pObj1, i )
    {
        if ( pObj1->pData == NULL )
            continue;
        pObj0 = (Aig_Obj_t *)pObj1->pData;
        if ( !Saig_ObjIsLo(p0, pObj0) )
            Abc_Print( 1, "Mismatch between LO pairs.\n" );
    }
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
{
    Aig_Obj_t * pNext, * pObj;
    int i, k, iFan = -1;
    Vec_PtrClear( vNodes );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        if ( pObj->pData != NULL )
            continue;
        if ( Saig_ObjIsLo(p, pObj) )
        {
            pNext = Saig_ObjLoToLi(p, pObj);
            pNext = Aig_ObjFanin0(pNext);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
        if ( Aig_ObjIsNode(pObj) )
        {
            pNext = Aig_ObjFanin0(pObj);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
            pNext = Aig_ObjFanin1(pObj);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
        Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
        {
            if ( Saig_ObjIsPo(p, pNext) )
                continue;
            if ( Saig_ObjIsLi(p, pNext) )
                pNext = Saig_ObjLiToLo(p, pNext);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
    }
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_MatchingCountUnmached( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        if ( pObj->pData != NULL )
            continue;
        Counter++;
    }
    return Counter;
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
{
    Vec_Ptr_t * vNodes0, * vNodes1;
    Aig_Obj_t * pNext0, * pNext1;
    int d, k;
    Aig_ManFanoutStart(p0);
    Aig_ManFanoutStart(p1);
    vNodes0 = Vec_PtrAlloc( 1000 );
    vNodes1 = Vec_PtrAlloc( 1000 );
    if ( fVerbose )
    {
        int nUnmached = Ssw_MatchingCountUnmached(p0);
        Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
        Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
            0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
            nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
    }
    for ( d = 0; d < nDist; d++ )
    {
        Ssw_MatchingExtendOne( p0, vNodes0 );
        Ssw_MatchingExtendOne( p1, vNodes1 );
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
        {
            pNext1 = (Aig_Obj_t *)pNext0->pData;
            if ( pNext1 == NULL )
                continue;
            assert( pNext1->pData == pNext0 );
            if ( Saig_ObjIsPi(p0, pNext1) )
                continue;
            pNext0->pData = NULL;
            pNext1->pData = NULL;
        }
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
        {
            pNext1 = (Aig_Obj_t *)pNext0->pData;
            if ( pNext1 == NULL )
                continue;
            assert( pNext1->pData == pNext0 );
            if ( Saig_ObjIsPi(p1, pNext1) )
                continue;
            pNext0->pData = NULL;
            pNext1->pData = NULL;
        }
        if ( fVerbose )
        {
            int nUnmached = Ssw_MatchingCountUnmached(p0);
            Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
                d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
                nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
        }
    }
    Vec_PtrFree( vNodes0 );
    Vec_PtrFree( vNodes1 );
    Aig_ManFanoutStop(p0);
    Aig_ManFanoutStop(p1);
}

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

  Synopsis    [Used differences in p0 to complete p1.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Ptr_t * vNewLis;
    Aig_Obj_t * pObj0, * pObj0Li, * pObj1;
    int i;
    // create register outputs in p0 that are absent in p1
    vNewLis = Vec_PtrAlloc( 100 );
    Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i )
    {
        if ( pObj0->pData != NULL )
            continue;
        pObj1 = Aig_ObjCreateCi( p1 );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
        Vec_PtrPush( vNewLis, pObj0Li );
    }
    // add missing nodes in the topological order
    Aig_ManForEachNode( p0, pObj0, i )
    {
        if ( pObj0->pData != NULL )
            continue;
        pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
    }
    // create register outputs in p0 that are absent in p1
    Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
        Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
    // increment the number of registers
    Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
    Vec_PtrFree( vNewLis );
}


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

  Synopsis    [Derives matching for all pairs.]

  Description [Modifies both AIGs.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Int_t * vPairsNew;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // check correctness
    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
    assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
    assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
    // create complete pairs
    vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
    Aig_ManForEachObj( p0, pObj0, i )
    {
        if ( Aig_ObjIsCo(pObj0) )
            continue;
        pObj1 = (Aig_Obj_t *)pObj0->pData;
        Vec_IntPush( vPairsNew, pObj0->Id );
        Vec_IntPush( vPairsNew, pObj1->Id );
    }
    return vPairsNew;
}


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

  Synopsis    [Transfers the result of matching to miter.]

  Description [The array of pairs should be complete.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairsAll )
{
    Vec_Int_t * vPairsMiter;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // create matching of nodes in the miter
    vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
    for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 )
    {
        pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) );
        pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) );
        assert( pObj0->pData != NULL );
        assert( pObj1->pData != NULL );
        if ( pObj0->pData == pObj1->pData )
            continue;
        if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
            continue;
        // get the miter nodes
        pObj0 = (Aig_Obj_t *)pObj0->pData;
        pObj1 = (Aig_Obj_t *)pObj1->pData;
        assert( !Aig_IsComplement(pObj0) );
        assert( !Aig_IsComplement(pObj1) );
        assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
        if ( Aig_ObjIsCo(pObj0) )
            continue;
        assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
        assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
        assert( pObj0->Id < pObj1->Id );
        Vec_IntPush( vPairsMiter, pObj0->Id );
        Vec_IntPush( vPairsMiter, pObj1->Id );
    }
    return vPairsMiter;
}


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

  Synopsis    [Solves SEC using structural similarity.]

  Description [Modifies both p0 and p1 by adding extra logic.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
    Ssw_Man_t * p;
    Vec_Int_t * vPairsAll, * vPairsMiter;
    Aig_Man_t * pMiter, * pAigNew;
    // derive full matching
    Ssw_MatchingStart( p0, p1, vPairs );
    if ( pPars->nIsleDist )
        Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose );
    Ssw_MatchingComplete( p0, p1 );
    Ssw_MatchingComplete( p1, p0 );
    vPairsAll = Ssw_MatchingPairs( p0, p1 );
    // create miter and transfer matching
    pMiter = Saig_ManCreateMiter( p0, p1, 0 );
    vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll );
    Vec_IntFree( vPairsAll );
    // start the induction manager
    p = Ssw_ManCreate( pMiter, pPars );
    // create equivalence classes using these IDs
    if ( p->pPars->fPartSigCorr )
        p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
    else
        p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
    if ( p->pPars->fDumpSRInit )
    {
        if ( p->pPars->fPartSigCorr )
        {
            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
            Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
            Aig_ManStop( pSRed );
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
        }
        else
            Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
    }
    p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
    Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
    // cleanup
    Ssw_ManStop( p );
    Aig_ManStop( pMiter );
    Vec_IntFree( vPairsMiter );
    return pAigNew;
}

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

  Synopsis    [Solves SEC with structural similarity.]

  Description [The first two arguments are pointers to the AIG managers.
  The third argument is the array of pairs of IDs of structurally equivalent
  nodes from the first and second managers, respectively.]
               
  SideEffects [The managers will be updated by adding "islands of difference".]

  SeeAlso     []

***********************************************************************/
int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
    Ssw_Pars_t Pars;
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    // derive parameters if not given
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // reduce the AIG with pairs
    pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
    // report the result of verification
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    Aig_ManStop( pAigRes );
    return RetValue;
}

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

  Synopsis    [Dummy procedure to detect structural similarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Int_t * vPairs;
    Aig_Obj_t * pObj;
    int i;
    // create array of pairs
    vPairs = Vec_IntAlloc( 100 );
    Aig_ManForEachObj( p0, pObj, i )
    {
        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
            continue;
        Vec_IntPush( vPairs, i );
        Vec_IntPush( vPairs, i );
    }
    return vPairs;
}

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

  Synopsis    [Solves SEC with structural similarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
{
    Vec_Int_t * vPairs;
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
    if ( pPars->fVerbose )
        Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( pPars->fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            Abc_Print( 1, "Demitering has failed.\n" );
            return -1;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( pPars->fVerbose )
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
        if ( p1 == NULL )
        {
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
//        Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
        }
    }
    assert( Aig_ManRegNum(pPart0) > 0 );
    assert( Aig_ManRegNum(pPart1) > 0 );
    assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
    assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
    // derive pairs
//    vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
    vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
    RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Vec_IntFree( vPairs );
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END