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

  FileName    [absUtil.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Abstraction package.]

  Synopsis    [Interface to pthreads.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#include "abs.h"

ABC_NAMESPACE_IMPL_START 

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

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

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

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abs_ParSetDefaults( Abs_Par_t * p )
{
    memset( p, 0, sizeof(Abs_Par_t) );
    p->nFramesMax         =      0;   // maximum frames
    p->nFramesStart       =      0;   // starting frame 
    p->nFramesPast        =      4;   // overlap frames
    p->nConfLimit         =      0;   // conflict limit
    p->nLearnedMax        =   1000;   // max number of learned clauses
    p->nLearnedStart      =   1000;   // max number of learned clauses
    p->nLearnedDelta      =    200;   // max number of learned clauses
    p->nLearnedPerce      =     70;   // max number of learned clauses
    p->nTimeOut           =      0;   // timeout in seconds
    p->nRatioMin          =      0;   // stop when less than this % of object is abstracted
    p->nRatioMax          =     30;   // restart when more than this % of object is abstracted
    p->fUseTermVars       =      0;   // use terminal variables
    p->fUseRollback       =      0;   // use rollback to the starting number of frames
    p->fPropFanout        =      1;   // propagate fanouts during refinement
    p->fVerbose           =      0;   // verbose flag
    p->iFrame             =     -1;   // the number of frames covered 
    p->iFrameProved       =     -1;   // the number of frames proved
    p->nFramesNoChangeLim =      2;   // the number of frames without change to dump abstraction
}

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

  Synopsis    [Converting VTA vector to GLA vector.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
{
    Gia_Obj_t * pObj;
    Vec_Int_t * vGla;
    int nObjMask, nObjs = Gia_ManObjNum(p);
    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    // get the bitmask
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vGla = Vec_IntStart( nObjs );
    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
    {
        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
        Vec_IntAddToEntry( vGla, (Entry &  nObjMask), 1 );
    }
    Vec_IntWriteEntry( vGla, 0, nFrames );
    return vGla;
}

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

  Synopsis    [Converting GLA vector to VTA vector.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
{
    Vec_Int_t * vVta;
    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
    int i, k, j, Entry, Counter, nGlaSize;
    //. get the GLA size
    nGlaSize = Vec_IntSum(vGla);
    // get the bitmask
    nObjBits = Abc_Base2Log(nObjs);
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vVta = Vec_IntAlloc( 1000 );
    Vec_IntPush( vVta, nFrames );
    Counter = nFrames + 2;
    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
        Vec_IntPush( vVta, Counter );
    for ( i = 0; i < nFrames; i++ )
        for ( k = 0; k <= i; k++ )
            Vec_IntForEachEntry( vGla, Entry, j )
                if ( Entry ) 
                    Vec_IntPush( vVta, (k << nObjBits) | j );
    Counter = Vec_IntEntry(vVta, nFrames+1);
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    return vVta;
}

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

  Synopsis    [Converting GLA vector to FLA vector.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
    if ( Gia_ObjIsRo(p, pObj) )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
}

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

  Synopsis    [Converting FLA vector to GLA vector.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
{
    Vec_Int_t * vGla;
    Gia_Obj_t * pObj;
    int i;
    // mark const0 and relevant CI objects
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
    Gia_ManForEachPi( p, pObj, i )
        Gia_ObjSetTravIdCurrent(p, pObj);
    Gia_ManForEachRo( p, pObj, i )
        if ( !Vec_IntEntry(vFla, i) )
            Gia_ObjSetTravIdCurrent(p, pObj);
    // label all objects reachable from the PO and selected flops
    vGla = Vec_IntStart( Gia_ManObjNum(p) );
    Vec_IntWriteEntry( vGla, 0, 1 );
    Gia_ManForEachPo( p, pObj, i )
        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    Gia_ManForEachRi( p, pObj, i )
        if ( Vec_IntEntry(vFla, i) )
            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    return vGla;
}

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

  Synopsis    [Converting GLA vector to FLA vector.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
{
    Vec_Int_t * vFla;
    Gia_Obj_t * pObj;
    int i;
    vFla = Vec_IntStart( Gia_ManRegNum(p) );
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Vec_IntWriteEntry( vFla, i, 1 );
    return vFla;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla )
{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}
int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachAnd( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}


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


ABC_NAMESPACE_IMPL_END