gia.c

Go to the documentation of this file.

 
#include "gia.h"
#include "misc/util/utilTruth.h"
 
ABC_NAMESPACE_IMPL_START
 

 
typedef struct Slv_Man_t_ Slv_Man_t;
struct Slv_Man_t_
{
    Vec_Int_t      vCis;
    Vec_Int_t      vCos;
    Vec_Int_t      vFanins;
    Vec_Int_t      vFanoutN;
    Vec_Int_t      vFanout0;
    Vec_Str_t      vValues;
    Vec_Int_t      vCopies;
};
 
static inline int  Slv_ManObjNum       ( Slv_Man_t * p )                      { return Vec_IntSize(&p->vFanins)/2;                       }
 
static inline int  Slv_ObjFaninLit     ( Slv_Man_t * p, int iObj, int f )     { return Vec_IntEntry(&p->vFanins, Abc_Var2Lit(iObj, f));  }
static inline int  Slv_ObjFanin        ( Slv_Man_t * p, int iObj, int f )     { return Abc_Lit2Var(Slv_ObjFaninLit(p, iObj, f));         }
static inline int  Slv_ObjFaninC       ( Slv_Man_t * p, int iObj, int f )     { return Abc_LitIsCompl(Slv_ObjFaninLit(p, iObj, f));      }
 
static inline int  Slv_ObjIsCi         ( Slv_Man_t * p, int iObj )            { return !Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
static inline int  Slv_ObjIsCo         ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) && !Slv_ObjFaninLit(p, iObj, 1);  }
static inline int  Slv_ObjIsAnd        ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
 
static inline int  Slv_ObjFanout0      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vFanout0, iObj);      }
static inline void Slv_ObjSetFanout0   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vFanout0, iObj, iLit);  }
 
static inline int  Slv_ObjNextFanout   ( Slv_Man_t * p, int iLit )            { return Vec_IntEntry(&p->vFanoutN, iLit);      }
static inline void Slv_ObjSetNextFanout( Slv_Man_t * p, int iLit, int iLitF ) { Vec_IntWriteEntry(&p->vFanoutN, iLit, iLitF); }
 
static inline int  Slv_ObjCopyLit      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vCopies, iObj);       }
static inline void Slv_ObjSetCopyLit   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vCopies, iObj, iLit);   }
 
#define Slv_ManForEachObj( p, iObj )                                  \
    for ( iObj = 1; iObj < Slv_ManObjNum(p); iObj++ )
 
#define Slv_ObjForEachFanout( p, iObj, iFanLit )                      \
    for ( iFanLit = Slv_ObjFanout0(p, iObj); iFanLit; iFanLit = Slv_ObjNextFanout(p, iFanLit) )


Slv_Man_t * Slv_ManAlloc( int nObjs )
{
    Slv_Man_t * p = ABC_CALLOC( Slv_Man_t, 1 );
    Vec_IntGrow( &p->vCis,     100 );
    Vec_IntGrow( &p->vCos,     100 );
    Vec_IntGrow( &p->vFanins,  2*nObjs );
    Vec_IntGrow( &p->vFanoutN, 2*nObjs );
    Vec_IntGrow( &p->vFanout0, nObjs );
    Vec_StrGrow( &p->vValues,  nObjs );
    // constant node
    Vec_IntFill( &p->vFanins,  2, 0 );
    Vec_IntFill( &p->vFanoutN, 2, 0 );
    Vec_IntFill( &p->vFanout0, 1, 0 );
    return p;
}
void Slv_ManFree( Slv_Man_t * p )
{
    Vec_IntErase( &p->vCis     );
    Vec_IntErase( &p->vCos     );
    Vec_IntErase( &p->vFanins  );
    Vec_IntErase( &p->vFanoutN );
    Vec_IntErase( &p->vFanout0 );
    Vec_StrErase( &p->vValues  );
    Vec_IntErase( &p->vCopies  );
    ABC_FREE( p );
}
void Slv_ManPrintFanouts( Slv_Man_t * p )
{
    int iObj, iFanLit;
    Slv_ManForEachObj( p, iObj )
    {
        printf( "Fanouts of node %d: ", iObj );
        Slv_ObjForEachFanout( p, iObj, iFanLit )
            printf( "%d ", Abc_Lit2Var(iFanLit) );
        printf( "\n" );
    }
}
static inline int Slv_ManAppendObj( Slv_Man_t * p, int iLit0, int iLit1 )
{
    int iObj = Slv_ManObjNum(p);
    Vec_StrPush( &p->vValues,  0 );
    Vec_IntPush( &p->vFanout0, 0 );
    Vec_IntPushTwo( &p->vFanoutN, 0, 0 );
    if ( !iLit0 )  // primary input
        assert(!iLit1), iLit1 = Vec_IntSize(&p->vCis)+1, Vec_IntPush(&p->vCis, iObj);
    else if ( !iLit1 )  // primary output
        assert(iLit0), Vec_IntPush(&p->vCos, iObj);
    else
    {
        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 0), Slv_ObjFanout0(p, Abc_Lit2Var(iLit0)) );
        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 1), Slv_ObjFanout0(p, Abc_Lit2Var(iLit1)) );
        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit0), Abc_Var2Lit(iObj, 0) );
        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit1), Abc_Var2Lit(iObj, 1) );
    }
    Vec_IntPushTwo( &p->vFanins, iLit0, iLit1 );
    return Abc_Var2Lit( iObj, 0 );
}

Slv_Man_t * Slv_ManFromGia( Gia_Man_t * p )
{
    Gia_Obj_t * pObj; int i;
    Slv_Man_t * pNew = Slv_ManAlloc( Gia_ManObjNum(p) );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachObj1( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)) );
        else if ( Gia_ObjIsCo(pObj) )
            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), 0 );
        else if ( Gia_ObjIsCi(pObj) )
            pObj->Value = Slv_ManAppendObj( pNew, 0, 0 );
        else
            assert( 0 );
    }
    assert( Gia_ManObjNum(p) == Slv_ManObjNum(pNew) );
    return pNew;
}
Gia_Man_t * Slv_ManToGia( Slv_Man_t * p )
{
    int iObj;
    Gia_Man_t * pNew = Gia_ManStart( Slv_ManObjNum(p) ); 
    Vec_IntFill( &p->vCopies,  Slv_ManObjNum(p), 0 );
    Slv_ManForEachObj( p, iObj )
        if ( Slv_ObjIsCi(p, iObj) )
            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCi(pNew) );
        else if ( Slv_ObjIsCo(p, iObj) )
        {
            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCo(pNew, iLit0) );
        }
        else if ( Slv_ObjIsAnd(p, iObj) )
        {
            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
            int iLit1 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 1)), Slv_ObjFaninC(p, iObj, 1) );
            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
        }
        else assert(0);
    assert( Gia_ManObjNum(pNew) == Slv_ManObjNum(p) );
    return pNew;
}
 
Gia_Man_t * Slv_ManToAig( Gia_Man_t * pGia )
{
    Slv_Man_t * p = Slv_ManFromGia( pGia );
    Gia_Man_t * pNew = Slv_ManToGia( p );
    pNew->pName = Abc_UtilStrsav( pGia->pName );
    pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
    Slv_ManPrintFanouts( p );
    Slv_ManFree( p );
    return pNew;
}
 
 

Gia_Man_t * Gia_ManCofPisVars( Gia_Man_t * p, int nVars )
{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj; int i, m;
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManForEachPi( p, pObj, i )
        Gia_ManAppendCi( pNew );
    Gia_ManHashStart( pNew );
    for ( m = 0; m < (1 << nVars); m++ )
    {
        Gia_ManFillValue( p );
        Gia_ManConst0(p)->Value = 0;
        Gia_ManForEachPi( p, pObj, i )
        {
            if ( i < nVars )
                pObj->Value = (m >> i) & 1;
            else
                pObj->Value = Gia_ObjToLit(pNew, Gia_ManCi(pNew, i));
        }
        Gia_ManForEachAnd( p, pObj, i )
            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        Gia_ManForEachPo( p, pObj, i )
            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    Gia_ManHashStop( pNew );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}
 
 

void Gia_ManStructExperiment( Gia_Man_t * p )
{
    extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
    Gia_Man_t * pTemp, * pUsed;
    Vec_Ptr_t * vGias = Vec_PtrAlloc( 100 );
    Gia_Obj_t * pObj; int i, k;
    Gia_ManForEachCo( p, pObj, i )
    {
        int iFan0 = Gia_ObjFaninId0p(p, pObj);
        pTemp = Gia_ManDupAndCones( p, &iFan0, 1, 1 );
        Vec_PtrForEachEntry( Gia_Man_t *, vGias, pUsed, k )
            if ( Gia_ManCiNum(pTemp) == Gia_ManCiNum(pUsed) && Cec_ManVerifyTwo(pTemp, pUsed, 0) == 1 )
            {
                ABC_SWAP( void *, Vec_PtrArray(vGias)[0], Vec_PtrArray(vGias)[k] );
                break;
            }
            else
                ABC_FREE( pTemp->pCexComb );
 
        printf( "\nOut %6d : ", i );
        if ( k == Vec_PtrSize(vGias) )
            printf( "Equiv to none    " );
        else
            printf( "Equiv to %6d  ", k );
        Gia_ManPrintStats( pTemp, NULL );
 
        if ( k == Vec_PtrSize(vGias) )
            Vec_PtrPush( vGias, pTemp );
        else
            Gia_ManStop( pTemp );
    }
    printf( "\nComputed %d classes.\n\n", Vec_PtrSize(vGias) );
    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
        Gia_ManStop( pTemp );
    Vec_PtrFree( vGias );
}

int Gia_EnumFirstUnused( int * pUsed, int nVars )
{
    int i;
    for ( i = 0; i < nVars; i++ )
        if ( pUsed[i] == 0 )
            return i;
    return -1;
}
void Gia_EnumPerms_rec( int * pUsed, int nVars, int * pPerm, int nPerm, int * pCount, FILE * pFile, int nLogVars )
{
    int i, k, New;
    if ( nPerm == nVars )
    {
        if ( pFile )
        {
            for ( i = 0; i < nLogVars; i++ )
                fprintf( pFile, "%c", '0' + ((*pCount) >> (nLogVars-1-i) & 1) );
            fprintf( pFile, " " );
            for ( i = 0; i < nVars; i++ )
            for ( k = 0; k < nVars; k++ )
                fprintf( pFile, "%c", '0' + (pPerm[i] == k) );
            fprintf( pFile, "\n" );
        }
        else
        {
            if ( *pCount < 20 )
            {
                printf( "%5d : ", (*pCount) );
                for ( i = 0; i < nVars; i += 2 )
                    printf( "%d %d  ", pPerm[i], pPerm[i+1] );
                printf( "\n" );
            }
        }
        (*pCount)++;
        return;
    }
    New = Gia_EnumFirstUnused( pUsed, nVars );
    assert( New >= 0 );
    pPerm[nPerm] = New;
    assert( pUsed[New] == 0 );
    pUsed[New] = 1;
    // try remaining ones
    for ( i = 0; i < nVars; i++ )
    {
        if ( pUsed[i] == 1 )
            continue;
        pPerm[nPerm+1] = i;
        assert( pUsed[i] == 0 );
        pUsed[i] = 1;
        Gia_EnumPerms_rec( pUsed, nVars, pPerm, nPerm+2, pCount, pFile, nLogVars );
        assert( pUsed[i] == 1 );
        pUsed[i] = 0;
    }
    assert( pUsed[New] == 1 );
    pUsed[New] = 0;
}
void Gia_EnumPerms( int nVars )
{
    int nLogVars = 0, Count = 0;
    int * pUsed = ABC_CALLOC( int, nVars );
    int * pPerm = ABC_CALLOC( int, nVars );
    FILE * pFile = fopen( "pairset.pla", "wb" );
    assert( nVars % 2 == 0 );
 
    printf( "Printing sets of pairs for %d objects:\n", nVars );
    Gia_EnumPerms_rec( pUsed, nVars, pPerm, 0, &Count, NULL, -1 ); 
    if ( Count > 20 )
        printf( "...\n" );
    printf( "Finished enumerating %d sets of pairs.\n", Count );
 
    nLogVars = Abc_Base2Log( Count );
    printf( "Need %d variables to encode %d sets.\n", nLogVars, Count );
    Count = 0;
    fprintf( pFile, ".i %d\n", nLogVars );
    fprintf( pFile, ".o %d\n", nVars*nVars );
    Gia_EnumPerms_rec( pUsed, nVars, pPerm, 0, &Count, pFile, nLogVars );   
    fprintf( pFile, ".e\n" );
    fclose( pFile );
    printf( "Finished dumping file \"%s\".\n", "pairset.pla" );
 
    ABC_FREE( pUsed );
    ABC_FREE( pPerm );
}

 
 
ABC_NAMESPACE_IMPL_END