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

  FileName    [giaSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [New constraint-propagation procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"

ABC_NAMESPACE_IMPL_START


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

#define GIA_LIMIT 10


typedef struct Gia_ManSat_t_ Gia_ManSat_t;
struct Gia_ManSat_t_
{
    Aig_MmFlex_t *    pMem;
};

typedef struct Gia_ObjSat1_t_ Gia_ObjSat1_t;
struct Gia_ObjSat1_t_
{
    char              nFans;
    char              nOffset;
    char              PathsH;
    char              PathsV;
};

typedef struct Gia_ObjSat2_t_ Gia_ObjSat2_t;
struct Gia_ObjSat2_t_
{
    unsigned          fTerm :  1;
    unsigned          iLit  : 31;
};

typedef struct Gia_ObjSat_t_ Gia_ObjSat_t;
struct Gia_ObjSat_t_
{
    union {
        Gia_ObjSat1_t Obj1;
        Gia_ObjSat2_t Obj2;
    };
};


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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_ManSat_t * Gia_ManSatStart()
{
    Gia_ManSat_t * p;
    p = ABC_CALLOC( Gia_ManSat_t, 1 );
    p->pMem = Aig_MmFlexStart();
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSatStop( Gia_ManSat_t * p )
{
    Aig_MmFlexStop( p->pMem, 0 );
    ABC_FREE( p );
}


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

  Synopsis    [Collects the supergate rooted at this ]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSatPartCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLits, int * pnLits )
{
    Gia_Obj_t * pFanin;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 || Gia_ObjFaninC0(pObj) )
        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC0(pObj));
    else
        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 || Gia_ObjFaninC1(pObj) )
        pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC1(pObj));
    else
        Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits);
}

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

  Synopsis    [Returns the number of words used.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManSatPartCreate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pObjPlace, int * pStore )
{
    Gia_Obj_t * pFanin;
    int i, nWordsUsed, nSuperSize = 0, Super[2*GIA_LIMIT];
    // make sure this is a valid node
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    // collect inputs to the supergate
    Gia_ManSatPartCollectSuper( p, pObj, Super, &nSuperSize );
    assert( nSuperSize <= 2*GIA_LIMIT );
    // create the root entry
    *pObjPlace = 0;
    ((Gia_ObjSat1_t *)pObjPlace)->nFans   = Gia_Var2Lit( nSuperSize, 0 );
    ((Gia_ObjSat1_t *)pObjPlace)->nOffset = pStore - pObjPlace;
    nWordsUsed = nSuperSize;
    for ( i = 0; i < nSuperSize; i++ )
    {
        pFanin = Gia_ManObj( p, Gia_Lit2Var(Super[i]) );
        if ( pFanin->fMark0 )
        {
            ((Gia_ObjSat2_t *)(pStore + i))->fTerm = 1;
            ((Gia_ObjSat2_t *)(pStore + i))->iLit  = Super[i];
        }
        else
        {
            assert( Gia_LitIsCompl(Super[i]) );
            nWordsUsed += Gia_ManSatPartCreate_rec( p, pFanin, pStore + i, pStore + nWordsUsed );
        }
    }
    return nWordsUsed;
}

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

  Synopsis    [Creates part and returns the number of words used.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManSatPartCreate( Gia_Man_t * p, Gia_Obj_t * pObj, int * pStore )
{
    return 1 + Gia_ManSatPartCreate_rec( p, pObj, pStore, pStore + 1 );
}


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

  Synopsis    [Count the number of internal nodes in the leaf-DAG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSatPartCountClauses( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnOnset, int * pnOffset )
{
    Gia_Obj_t * pFanin;
    int nOnset0, nOnset1, nOffset0, nOffset1;
    assert( Gia_ObjIsAnd(pObj) );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        nOnset0 = 1, nOffset0 = 1;
    else
    {
        Gia_ManSatPartCountClauses(p, pFanin, &nOnset0, &nOffset0);
        if ( Gia_ObjFaninC0(pObj) )
        {
            int Temp = nOnset0;
            nOnset0 = nOffset0;
            nOffset0 = Temp;
        }
    }
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        nOnset1 = 1, nOffset1 = 1;
    else
    {
        Gia_ManSatPartCountClauses(p, pFanin, &nOnset1, &nOffset1);
        if ( Gia_ObjFaninC1(pObj) )
        {
            int Temp = nOnset1;
            nOnset1 = nOffset1;
            nOffset1 = Temp;
        }
    }
    *pnOnset  = nOnset0  * nOnset1;
    *pnOffset = nOffset0 + nOffset1;
}

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

  Synopsis    [Count the number of internal nodes in the leaf-DAG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int * pnNodes )
{
    Gia_Obj_t * pFanin;
    int Level0 = 0, Level1 = 0;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    (*pnNodes)++;
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        (*pnLeaves)++;
    else
        Level0 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC0(pObj);
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        (*pnLeaves)++;
    else
        Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
    return Abc_MaxInt( Level0, Level1 );
}

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

  Synopsis    [Count the number of internal nodes in the leaf-DAG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManSatPartCountNodes( Gia_Man_t * p, Gia_Obj_t * pObj )
{
    Gia_Obj_t * pFanin;
    int nNodes0 = 0, nNodes1 = 0;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( !(pFanin->fMark0) )
        nNodes0 = Gia_ManSatPartCountNodes(p, pFanin);
    pFanin = Gia_ObjFanin1(pObj);
    if ( !(pFanin->fMark0) )
        nNodes1 = Gia_ManSatPartCountNodes(p, pFanin);
    return nNodes0 + nNodes1 + 1;
}

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

  Synopsis    [Count the number of internal nodes in the leaf-DAG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSatPartPrint( Gia_Man_t * p, Gia_Obj_t * pObj, int Step )
{
    Gia_Obj_t * pFanin;
    assert( Gia_ObjIsAnd(pObj) );
    assert( pObj->fMark0 == 0 );
    pFanin = Gia_ObjFanin0(pObj);
    if ( pFanin->fMark0 )
        printf( "%s%d", Gia_ObjFaninC0(pObj)?"!":"", Gia_ObjId(p,pFanin) );
    else
    {
        if ( Gia_ObjFaninC0(pObj) )
            printf( "(" );
        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC0(pObj));
        if ( Gia_ObjFaninC0(pObj) )
            printf( ")" );
    }
    printf( "%s", (Step & 1)? " + " : "*" );
    pFanin = Gia_ObjFanin1(pObj);
    if ( pFanin->fMark0 )
        printf( "%s%d", Gia_ObjFaninC1(pObj)?"!":"", Gia_ObjId(p,pFanin) );
    else
    {
        if ( Gia_ObjFaninC1(pObj) )
            printf( "(" );
        Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC1(pObj));
        if ( Gia_ObjFaninC1(pObj) )
            printf( ")" );
    }
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSatExperiment( Gia_Man_t * p )
{
    int nStored, Storage[1000], * pStart; 
    Gia_ManSat_t * pMan;
    Gia_Obj_t * pObj;
    int i, nLevels, nLeaves, nNodes, nCount[2*GIA_LIMIT+2] = {0}, nCountAll = 0;
    int Num0 = 0, Num1 = 0;
    clock_t clk = clock();
    int nWords = 0, nWords2 = 0;
    pMan = Gia_ManSatStart();
    // mark the nodes to become roots of leaf-DAGs
    Gia_ManCreateValueRefs( p );
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
        else if ( Gia_ObjIsCi(pObj) )
            pObj->fMark0 = 1;
        else if ( Gia_ObjIsAnd(pObj) )
        {
            if ( pObj->Value > 1 || Gia_ManSatPartCountNodes(p,pObj) >= GIA_LIMIT )
                pObj->fMark0 = 1;
        }
        pObj->Value = 0;
    }
    // compute the sizes of leaf-DAGs
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( pObj->fMark0 == 0 )
            continue;
        pObj->fMark0 = 0;

        nCountAll++;
        nStored = Gia_ManSatPartCreate( p, pObj, Storage );
        nWords2 += nStored;
        assert( nStored < 500 );
        pStart = (int *)Aig_MmFlexEntryFetch( pMan->pMem, sizeof(int) * nStored );
        memcpy( pStart, Storage, sizeof(int) * nStored );

        nLeaves = nNodes = 0;
        nLevels = 1+Gia_ManSatPartCount( p, pObj, &nLeaves, &nNodes );
        nWords += nLeaves + nNodes;
        if ( nNodes <= 2*GIA_LIMIT )
            nCount[nNodes]++;
        else
            nCount[2*GIA_LIMIT+1]++;
//        if ( nNodes > 10 && i % 100 == 0 )
//        if ( nNodes > 5 )
        if ( 0 )
        {
            Gia_ManSatPartCountClauses( p, pObj, &Num0, &Num1 );
            printf( "%8d :  And = %3d.  Lev = %2d. Clauses = %3d. (%3d + %3d).\n", i, nNodes, nLevels, Num0+Num1, Num0, Num1 );
            Gia_ManSatPartPrint( p, pObj, 0 );
            printf( "\n" );
        }

        pObj->fMark0 = 1;
    }
    printf( "\n" );
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = 0;
    Gia_ManSatStop( pMan );
    for ( i = 0; i < 2*GIA_LIMIT+2; i++ )
        printf( "%2d=%6d  %7.2f %%  %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) );
    ABC_PRMn( "MemoryEst", 4*nWords );
    ABC_PRMn( "MemoryReal", 4*nWords2 );
    printf( "%5.2f bpn  ", 4.0*nWords2/Gia_ManObjNum(p) );
    ABC_PRT( "Time", clock() - clk );
}

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


ABC_NAMESPACE_IMPL_END