giaSat.c

Go to the documentation of this file.

 
#include "gia.h"
 
ABC_NAMESPACE_IMPL_START
 

 
#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;
    };
};
 


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

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

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);
}

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;
}

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

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;
}

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 );
}

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;
}

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( ")" );
    }
}
 

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 );
}

 
 
ABC_NAMESPACE_IMPL_END