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

  FileName    [cecSynth.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Combinational equivalence checking.]

  Synopsis    [Partitioned sequential synthesis.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "cecInt.h"
#include "aig/gia/giaAig.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Populate sequential synthesis parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * p )
{
    memset( p, 0, sizeof(Cec_ParSeq_t) );
    p->fUseLcorr    =    0;  // enables latch correspondence
    p->fUseScorr    =    0;  // enables signal correspondence
    p->nBTLimit     = 1000;  // (scorr/lcorr) conflict limit at a node
    p->nFrames      =    1;  // (scorr only) the number of timeframes
    p->nLevelMax    =   -1;  // (scorr only) the max number of levels
    p->fConsts      =    1;  // (scl only) merging constants
    p->fEquivs      =    1;  // (scl only) merging equivalences
    p->fUseMiniSat  =    0;  // enables MiniSat in lcorr/scorr
    p->nMinDomSize  =  100;  // the size of minimum clock domain
    p->fVeryVerbose =    0;  // verbose stats
    p->fVerbose     =    0;  // verbose stats
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p )
{
    return p->nMinDomSize;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_SeqReadVerbose( Cec_ParSeq_t * p )
{
    return p->fVerbose;
}

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

  Synopsis    [Computes partitioning of registers.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManRegCreatePart( Gia_Man_t * p, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack )
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    Vec_Int_t * vNodes, * vRoots;
    int i, iOut, nCountPis, nCountRegs;
    int * pMapBack;
    // collect/mark nodes/PIs in the DFS order from the roots
    Gia_ManIncrementTravId( p );
    vRoots  = Vec_IntAlloc( Vec_IntSize(vPart) );
    Vec_IntForEachEntry( vPart, iOut, i )
        Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) );
    vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) );
    Vec_IntFree( vRoots );
    // unmark register outputs
    Vec_IntForEachEntry( vPart, iOut, i )
        Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) );
    // count pure PIs
    nCountPis = nCountRegs = 0;
    Gia_ManForEachPi( p, pObj, i )
        nCountPis += Gia_ObjIsTravIdCurrent(p, pObj);
    // count outputs of other registers
    Gia_ManForEachRo( p, pObj, i )
        nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ???
    if ( pnCountPis )
        *pnCountPis = nCountPis;
    if ( pnCountRegs )
        *pnCountRegs = nCountRegs;
    // clean old manager
    Gia_ManFillValue(p);
    Gia_ManConst0(p)->Value = 0;
    // create the new manager
    pNew = Gia_ManStart( Vec_IntSize(vNodes) );
    // create the PIs
    Gia_ManForEachCi( p, pObj, i )
        if ( Gia_ObjIsTravIdCurrent(p, pObj) )
            pObj->Value = Gia_ManAppendCi(pNew);
    // add variables for the register outputs
    // create fake POs to hold the register outputs
    Vec_IntForEachEntry( vPart, iOut, i )
    {
        pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
        pObj->Value = Gia_ManAppendCi(pNew);
        Gia_ManAppendCo( pNew, pObj->Value );
        Gia_ObjSetTravIdCurrent( p, pObj ); // added
    }
    // create the nodes
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        if ( Gia_ObjIsAnd(pObj) )
            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    // add real POs for the registers
    Vec_IntForEachEntry( vPart, iOut, i )
    {
        pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut );
        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) );
    // create map
    if ( ppMapBack )
    {
        pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
        // map constant nodes
        pMapBack[0] = 0;
        // logic cones of register outputs
        Gia_ManForEachObjVec( vNodes, p, pObj, i )
        {
//            pObjNew = Aig_Regular(pObj->pData);
//            pMapBack[pObjNew->Id] = pObj->Id;
            assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
            assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
            pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
        }
        // map register outputs
        Vec_IntForEachEntry( vPart, iOut, i )
        {
            pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
//            pObjNew = pObj->pData;
//            pMapBack[pObjNew->Id] = pObj->Id;
            assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
            assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
            pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
        }
        *ppMapBack = pMapBack;
    }
    Vec_IntFree( vNodes );
    return pNew;
}

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

  Synopsis    [Transfers the classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_TransferMappedClasses( Gia_Man_t * pPart, int * pMapBack, int * pReprs )
{
    Gia_Obj_t * pObj;
    int i, Id1, Id2, nClasses;
    if ( pPart->pReprs == NULL ) 
        return 0;
    nClasses = 0;
    Gia_ManForEachObj( pPart, pObj, i )
    {
        if ( Gia_ObjRepr(pPart, i) == GIA_VOID )
            continue;
        assert( i                     < Gia_ManObjNum(pPart) );
        assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) );
        Id1 = pMapBack[ i ];
        Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ];
        if ( Id1 == Id2 )
            continue;
        if ( Id1 < Id2 )
            pReprs[Id2] = Id1;
        else
            pReprs[Id1] = Id2;
        nClasses++;
    }
    return nClasses;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManFindRepr_rec( int * pReprs, int Id )
{
    if ( pReprs[Id] == 0 )
        return 0;
    if ( pReprs[Id] == ~0 )
        return Id;
    return Gia_ManFindRepr_rec( pReprs, pReprs[Id] );
}

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

  Synopsis    [Normalizes equivalences.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManNormalizeEquivalences( Gia_Man_t * p, int * pReprs )
{
    int i, iRepr;
    assert( p->pReprs == NULL );
    assert( p->pNexts == NULL );
    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
    for ( i = 0; i < Gia_ManObjNum(p); i++ )
        Gia_ObjSetRepr( p, i, GIA_VOID );
    for ( i = 0; i < Gia_ManObjNum(p); i++ )
    {
        if ( pReprs[i] == ~0 )
            continue;
        iRepr = Gia_ManFindRepr_rec( pReprs, i );
        Gia_ObjSetRepr( p, i, iRepr );
    }
    p->pNexts = Gia_ManDeriveNexts( p );
}

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

  Synopsis    [Partitioned sequential synthesis.]

  Description [Returns AIG annotated with equivalence classes.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
{
    int fPrintParts = 0;
    char Buffer[100];
    Gia_Man_t * pTemp;
    Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms;
    Vec_Int_t * vPart;
    int * pMapBack, * pReprs;
    int i, nCountPis, nCountRegs;
    int nClasses;
    abctime clk = Abc_Clock();

    // save parameters
    if ( fPrintParts )
    {
        // print partitions
        Abc_Print( 1, "The following clock domains are used:\n" );
        Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
        {
            pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
            sprintf( Buffer, "part%03d.aig", i );
            Gia_AigerWrite( pTemp, Buffer, 0, 0 );
            Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
                i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
            Gia_ManStop( pTemp );
        }
    }

    // perform sequential synthesis for clock domains
    pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
    {
        pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack );
        if ( nCountPis > 0 ) 
        {
            if ( pPars->fUseScorr )
            {
                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
                Cec_ManCorSetDefaultParams( pCorPars );
                pCorPars->nBTLimit   = pPars->nBTLimit;
                pCorPars->nLevelMax  = pPars->nLevelMax;
                pCorPars->fVerbose   = pPars->fVeryVerbose;
                pCorPars->fUseCSat   = 1;
                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
            }
            else if ( pPars->fUseLcorr )
            {
                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
                Cec_ManCorSetDefaultParams( pCorPars );
                pCorPars->fLatchCorr = 1;
                pCorPars->nBTLimit   = pPars->nBTLimit;
                pCorPars->fVerbose   = pPars->fVeryVerbose;
                pCorPars->fUseCSat   = 1;
                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
            }
            else
            {
//                pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
//                Gia_ManStop( pNew );
                Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
            }
//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) );
            nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs );
            if ( pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n", 
                    i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses );
            }
        }
        Gia_ManStop( pTemp );
        ABC_FREE( pMapBack );
    }

    // generate resulting equivalences
    Gia_ManNormalizeEquivalences( p, pReprs );
//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) );
    ABC_FREE( pReprs );
    if ( pPars->fVerbose )
    {
        Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
    }
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar )
{
    Gia_Obj_t * pObj; 
    int iVar, iVar0, iVar1;
    if ( Vec_IntEntry(vSatVar, iObj) >= 0 )
        return Vec_IntEntry(vSatVar, iObj);
    iVar = sat_solver_addvar(pSat);
    Vec_IntWriteEntry( vSatVar, iObj, iVar );
    pObj = Gia_ManObj( p, iObj );
    if ( Gia_ObjIsAnd(pObj) )
    {
        iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar );
        iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar );
        sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
    }
    return iVar;
}
int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase )
{
    int Lits[2] = {1}, status;
    sat_solver * pSat = sat_solver_new();
    Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) );
    Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) );
    sat_solver_addclause( pSat, Lits, Lits + 1 );
    Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar );
    Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar );
    Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 );
    Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase );
    status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
    if ( status == l_False )
    {
        Lits[0] = Abc_LitNot( Lits[0] );
        Lits[1] = Abc_LitNot( Lits[1] );
        status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
    }
    Vec_IntFree( vSatVar );
    sat_solver_delete( pSat );
    return status;
}


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


ABC_NAMESPACE_IMPL_END