Unifification of custom extensions.

27 files changed, 813 insertions, 1147 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f29813e5..804a7759 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3411,6 +3411,10 @@ SOURCE=.\src\aig\gia\giaAiger.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaAigerExt.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaBidec.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 52db2cce..fbc9212e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -140,6 +140,10 @@ struct Gia_Man_t_
     Vec_Int_t *    vDoms;         // dominators
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
+    Gia_Man_t *    pAigExtra;     // combinational logic of holes
+    Vec_Flt_t *    vInArrs;       // PI arrival times
+    Vec_Flt_t *    vOutReqs;      // PO required times
+    Vec_Int_t *    vPacking;      // packing information
     int *          pTravIds;      // separate traversal ID representation
     int            nTravIdsAlloc; // the number of trav IDs allocated
     Vec_Ptr_t *    vNamesIn;      // the input names 
@@ -593,6 +597,52 @@ static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
         printf( "X" );
 }
 
+static inline int Gia_AigerReadInt( unsigned char * pPos )
+{
+    int i, Value = 0;
+    for ( i = 0; i < 4; i++ )
+        Value = (Value << 8) | *pPos++;
+    return Value;
+}
+static inline void Gia_AigerWriteInt( unsigned char * pPos, int Value )
+{
+    int i;
+    for ( i = 3; i >= 0; i-- )
+        *pPos++ = (Value >> (8*i)) & 255;
+}
+static inline unsigned Gia_AigerReadUnsigned( unsigned char ** ppPos )
+{
+    unsigned x = 0, i = 0;
+    unsigned char ch;
+    while ((ch = *(*ppPos)++) & 0x80)
+        x |= (ch & 0x7f) << (7 * i++);
+    return x | (ch << (7 * i));
+}
+static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x )
+{
+    unsigned char ch;
+    while (x & ~0x7f)
+    {
+        ch = (x & 0x7f) | 0x80;
+        Vec_StrPush( vStr, ch );
+        x >>= 7;
+    }
+    ch = x;
+    Vec_StrPush( vStr, ch );
+}
+static inline int Gia_AigerWriteUnsignedBuffer( unsigned char * pBuffer, int Pos, unsigned x )
+{
+    unsigned char ch;
+    while (x & ~0x7f)
+    {
+        ch = (x & 0x7f) | 0x80;
+        pBuffer[Pos++] = ch;
+        x >>= 7;
+    }
+    ch = x;
+    pBuffer[Pos++] = ch;
+    return Pos;
+}
 
 static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr );                  }
 static inline int         Gia_ObjRepr( Gia_Man_t * p, int Id )               { return p->pReprs[Id].iRepr;                                                }
@@ -712,13 +762,13 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
-extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
-extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck );
-extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
+extern Gia_Man_t *         Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
+extern Gia_Man_t *         Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck );
+extern void                Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
-extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p );
-extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
-extern void                Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName );
+extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );
+extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
+extern void                Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 0a35dab0..ea36add4 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -35,88 +35,30 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Extracts one unsigned AIG edge from the input buffer.]
-
-  Description [This procedure is a slightly modified version of Armin Biere's
-  procedure "unsigned decode (FILE * file)". ]
-  
-  SideEffects [Updates the current reading position.]
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Gia_ReadAigerDecode( unsigned char ** ppPos )
-{
-    unsigned x = 0, i = 0;
-    unsigned char ch;
-    while ((ch = *(*ppPos)++) & 0x80)
-        x |= (ch & 0x7f) << (7 * i++);
-    return x | (ch << (7 * i));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Decodes the encoded array of literals.]
+  Synopsis    []
 
   Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_WriteDecodeLiterals( unsigned char ** ppPos, int nEntries )
-{
-    Vec_Int_t * vLits;
-    int Lit, LitPrev, Diff, i;
-    vLits = Vec_IntAlloc( nEntries );
-    LitPrev = Gia_ReadAigerDecode( ppPos );
-    Vec_IntPush( vLits, LitPrev );
-    for ( i = 1; i < nEntries; i++ )
-    {
-//        Diff = Lit - LitPrev;
-//        Diff = (Lit < LitPrev)? -Diff : Diff;
-//        Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
-        Diff = Gia_ReadAigerDecode( ppPos );
-        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
-        Lit  = Diff + LitPrev;
-        Vec_IntPush( vLits, Lit );
-        LitPrev = Lit;
-    }
-    return vLits;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the file size.]
-
-  Description [The file should be closed.]
 
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_FixFileName( char * pFileName )
+void Gia_FileFixName( char * pFileName )
 {
     char * pName;
     for ( pName = pFileName; *pName; pName++ )
         if ( *pName == '>' )
             *pName = '\\';
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the file size.]
-
-  Description [The file should be closed.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
+char * Gia_FileNameGeneric( char * FileName )
+{
+    char * pDot, * pRes;
+    pRes = Abc_UtilStrsav( FileName );
+    if ( (pDot = strrchr( pRes, '.' )) )
+        *pDot = 0;
+    return pRes;
+}
 int Gia_FileSize( char * pFileName )
 {
     FILE * pFile;
@@ -132,112 +74,16 @@ int Gia_FileSize( char * pFileName )
     fclose( pFile );
     return nFileSize;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Gia_FileNameGeneric( char * FileName )
-{
-    char * pDot, * pRes;
-    pRes = Abc_UtilStrsav( FileName );
-    if ( (pDot = strrchr( pRes, '.' )) )
-        *pDot = 0;
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read integer from the string.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ReadInt( unsigned char * pPos )
-{
-    int i, Value = 0;
-    for ( i = 0; i < 4; i++ )
-        Value = (Value << 8) | *pPos++;
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads decoded value.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Gia_ReadDiffValue( unsigned char ** ppPos, int iPrev )
+void Gia_FileWriteBufferSize( FILE * pFile, int nSize )
 {
-    int Item = Gia_ReadAigerDecode( ppPos );
-    if ( Item & 1 )
-        return iPrev + (Item >> 1);
-    return iPrev - (Item >> 1);
+    unsigned char Buffer[5];
+    Gia_AigerWriteInt( Buffer, nSize );
+    fwrite( Buffer, 1, 4, pFile );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Read equivalence classes from the string.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
-{
-    Gia_Rpr_t * pReprs;
-    unsigned char * pStop;
-    int i, Item, fProved, iRepr, iNode;
-    pStop = *ppPos;
-    pStop += Gia_ReadInt( *ppPos ); *ppPos += 4;
-    pReprs = ABC_CALLOC( Gia_Rpr_t, nSize );
-    for ( i = 0; i < nSize; i++ )
-        pReprs[i].iRepr = GIA_VOID;
-    iRepr = iNode = 0;
-    while ( *ppPos < pStop )
-    {
-        Item = Gia_ReadAigerDecode( ppPos );
-        if ( Item & 1 )
-        {
-            iRepr += (Item >> 1);
-            iNode = iRepr;
-//printf( "\nRepr = %d ", iRepr );
-            continue;
-        }
-        Item >>= 1;
-        fProved = (Item & 1);
-        Item >>= 1;
-        iNode += Item;
-        pReprs[iNode].fProved = fProved;
-        pReprs[iNode].iRepr = iRepr;
-        assert( iRepr < iNode );
-//printf( "Node = %d ", iNode );
-    }
-    return pReprs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read flop classes from the string.]
+  Synopsis    [Create the array of literals to be written.]
 
   Description []
   
@@ -246,387 +92,72 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize )
+Vec_Int_t * Gia_AigerCollectLiterals( Gia_Man_t * p )
 {
-    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
-    assert( nAlloc/4 == nSize );
-    assert( Vec_IntSize(vClasses) == nSize );
-    memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize );
-    *ppPos += 4 * nSize;
+    Vec_Int_t * vLits;
+    Gia_Obj_t * pObj;
+    int i;
+    vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
+    Gia_ManForEachRi( p, pObj, i )
+        Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
+    return vLits;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Read equivalence classes from the string.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Gia_ReadMapping( unsigned char ** ppPos, int nSize )
+Vec_Int_t * Gia_AigerReadLiterals( unsigned char ** ppPos, int nEntries )
 {
-    int * pMapping;
-    unsigned char * pStop;
-    int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize;
-    pStop = *ppPos;
-    pStop += Gia_ReadInt( *ppPos ); *ppPos += 4;
-    nAlloc = nSize + pStop - *ppPos;
-    pMapping = ABC_CALLOC( int, nAlloc );
-    while ( *ppPos < pStop )
+    Vec_Int_t * vLits;
+    int Lit, LitPrev, Diff, i;
+    vLits = Vec_IntAlloc( nEntries );
+    LitPrev = Gia_AigerReadUnsigned( ppPos );
+    Vec_IntPush( vLits, LitPrev );
+    for ( i = 1; i < nEntries; i++ )
     {
-        k = iOffset;
-        pMapping[k++] = nFanins = Gia_ReadAigerDecode( ppPos );
-        for ( j = 0; j <= nFanins; j++ )
-            pMapping[k++] = iNode = Gia_ReadDiffValue( ppPos, iNode );
-        pMapping[iNode] = iOffset;
-        iOffset = k;
+//        Diff = Lit - LitPrev;
+//        Diff = (Lit < LitPrev)? -Diff : Diff;
+//        Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
+        Diff = Gia_AigerReadUnsigned( ppPos );
+        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
+        Lit  = Diff + LitPrev;
+        Vec_IntPush( vLits, Lit );
+        LitPrev = Lit;
     }
-    assert( iOffset <= nAlloc );
-    return pMapping;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read switching from the string.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize )
-{
-    unsigned char * pSwitching;
-    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
-    assert( nAlloc == nSize );
-    pSwitching = ABC_ALLOC( unsigned char, nSize );
-    memcpy( pSwitching, *ppPos, nSize );
-    *ppPos += nSize;
-    return pSwitching;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read placement from the string.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize )
-{
-    Gia_Plc_t * pPlacement;
-    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
-    assert( nAlloc/4 == nSize );
-    pPlacement = ABC_ALLOC( Gia_Plc_t, nSize );
-    memcpy( pPlacement, *ppPos, 4*nSize );
-    *ppPos += 4 * nSize;
-    return pPlacement;
+    return vLits;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the AIG in the binary AIGER format.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
+Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits )
 {
-    FILE * pFile;
-    Gia_Man_t * pNew;
-    Vec_Int_t * vLits = NULL;
-    Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
-    int iObj, iNode0, iNode1;
-    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
-    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
-    unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
-    char * pContents, * pName;
-    unsigned uLit0, uLit1, uLit;
-    int RetValue;
-
-    // read the file into the buffer
-    Gia_FixFileName( pFileName );
-    nFileSize = Gia_FileSize( pFileName );
-    pFile = fopen( pFileName, "rb" );
-    pContents = ABC_ALLOC( char, nFileSize );
-    RetValue = fread( pContents, nFileSize, 1, pFile );
-    fclose( pFile );
-
-    // check if the input file format is correct
-    if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
-    {
-        ABC_FREE( pContents );
-        fprintf( stdout, "Wrong input file format.\n" );
-        return NULL;
-    }
-
-    // read the parameters (M I L O A + B C J F)
-    pCur = (unsigned char *)pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
-    // read the number of objects
-    nTotal = atoi( (const char *)pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
-    // read the number of inputs
-    nInputs = atoi( (const char *)pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
-    // read the number of latches
-    nLatches = atoi( (const char *)pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
-    // read the number of outputs
-    nOutputs = atoi( (const char *)pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
-    // read the number of nodes
-    nAnds = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
-    if ( *pCur == ' ' )
-    {
-        assert( nOutputs == 0 );
-        // read the number of properties
-        pCur++;
-        nBad = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
-        nOutputs += nBad;
-    }
-    if ( *pCur == ' ' )
-    {
-        // read the number of properties
-        pCur++;
-        nConstr = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
-        nOutputs += nConstr;
-    }
-    if ( *pCur == ' ' )
-    {
-        // read the number of properties
-        pCur++;
-        nJust = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
-        nOutputs += nJust;
-    }
-    if ( *pCur == ' ' )
-    {
-        // read the number of properties
-        pCur++;
-        nFair = atoi( (const char *)pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
-        nOutputs += nFair;
-    }
-    if ( *pCur != '\n' )
-    {
-        fprintf( stdout, "The parameter line is in a wrong format.\n" );
-        ABC_FREE( pContents );
-        return NULL;
-    }
-    pCur++;
-
-    // check the parameters
-    if ( nTotal != nInputs + nLatches + nAnds )
-    {
-        fprintf( stdout, "The number of objects does not match.\n" );
-        ABC_FREE( pContents );
-        return NULL;
-    }
-    if ( nJust || nFair )
-    {
-        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
-        ABC_FREE( pContents );
-        return NULL;
-    }
-
-    if ( nConstr )
-    {
-        if ( nConstr == 1 )
-            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
-        else
-            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
-    }
-
-    // allocate the empty AIG
-    pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
-    pName = Gia_FileNameGeneric( pFileName );
-    pNew->pName = Abc_UtilStrsav( pName );
-    pNew->pSpec = Abc_UtilStrsav( pFileName );
-//    pNew->pSpec = Abc_UtilStrsav( pFileName );
-    ABC_FREE( pName );
-    pNew->nConstrs = nConstr;
-
-    // prepare the array of nodes
-    vNodes = Vec_IntAlloc( 1 + nTotal );
-    Vec_IntPush( vNodes, 0 );
-
-    // create the PIs
-    for ( i = 0; i < nInputs + nLatches; i++ )
-    {
-        iObj = Gia_ManAppendCi(pNew);    
-        Vec_IntPush( vNodes, iObj );
-    }
-
-    // remember the beginning of latch/PO literals
-    pDrivers = pCur;
-    if ( pContents[3] == ' ' ) // standard AIGER
-    {
-        // scroll to the beginning of the binary data
-        for ( i = 0; i < nLatches + nOutputs; )
-            if ( *pCur++ == '\n' )
-                i++;
-    }
-    else // modified AIGER
-    {
-        vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
-    }
-
-    // create the AND gates
-    for ( i = 0; i < nAnds; i++ )
-    {
-        uLit = ((i + 1 + nInputs + nLatches) << 1);
-        uLit1 = uLit  - Gia_ReadAigerDecode( &pCur );
-        uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
-//        assert( uLit1 > uLit0 );
-        iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
-        iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
-        assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
-//        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
-        Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
-    }
-
-    // remember the place where symbols begin
-    pSymbols = pCur;
-
-    // read the latch driver literals
-    vDrivers = Vec_IntAlloc( nLatches + nOutputs );
-    if ( pContents[3] == ' ' ) // standard AIGER
-    {
-        pCur = pDrivers;
-        for ( i = 0; i < nLatches; i++ )
-        {
-            uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
-            Vec_IntPush( vDrivers, iNode0 );
-        }
-        // read the PO driver literals
-        for ( i = 0; i < nOutputs; i++ )
-        {
-            uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
-            Vec_IntPush( vDrivers, iNode0 );
-        }
-
-    }
-    else
+    Vec_Str_t * vBinary;
+    int Pos = 0, Lit, LitPrev, Diff, i;
+    vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
+    LitPrev = Vec_IntEntry( vLits, 0 );
+    Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
+    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
     {
-        // read the latch driver literals
-        for ( i = 0; i < nLatches; i++ )
-        {
-            uLit0 = Vec_IntEntry( vLits, i );
-            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
-            Vec_IntPush( vDrivers, iNode0 );
-        }
-        // read the PO driver literals
-        for ( i = 0; i < nOutputs; i++ )
-        {
-            uLit0 = Vec_IntEntry( vLits, i+nLatches );
-            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
-            Vec_IntPush( vDrivers, iNode0 );
-        }
-        Vec_IntFree( vLits );
+        Diff = Lit - LitPrev;
+        Diff = (Lit < LitPrev)? -Diff : Diff;
+        Diff = (Diff << 1) | (int)(Lit < LitPrev);
+        Pos = Gia_AigerWriteUnsignedBuffer( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
+        LitPrev = Lit;
+        if ( Pos + 10 > vBinary->nCap )
+            Vec_StrGrow( vBinary, vBinary->nCap+1 );
     }
-
-    // create the POs
-    for ( i = 0; i < nOutputs; i++ )
-        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
-    for ( i = 0; i < nLatches; i++ )
-        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
-    Vec_IntFree( vDrivers );
-
-    // create the latches
-    Gia_ManSetRegNum( pNew, nLatches );
-
-    // check if there are other types of information to read
-    pCur = pSymbols;
-    if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
+    vBinary->nSize = Pos;
+/*
+    // verify
     {
-        pCur++;
-        if ( *pCur == 'e' )
-        {
-            pCur++;
-            // read equivalence classes
-            pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
-            pNew->pNexts = Gia_ManDeriveNexts( pNew );
-        }
-        if ( *pCur == 'f' )
-        {
-            pCur++;
-            // read flop classes
-            pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
-            Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) );
-        }
-        if ( *pCur == 'g' )
-        {
-            pCur++;
-            // read gate classes
-            pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) );
-            Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 'v' )
-        {
-            pCur++;
-            // read object classes
-            pNew->vObjClasses = Vec_IntStart( Gia_ReadInt(pCur)/4 ); pCur += 4;
-            memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) );
-            pCur += 4*Vec_IntSize(pNew->vObjClasses);
-        }
-        if ( *pCur == 'm' )
-        {
-            pCur++;
-            // read mapping
-            pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 'p' )
-        {
-            pCur++;
-            // read placement
-            pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 's' )
-        { 
-            pCur++;
-            // read switching activity
-            pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 'c' )
-        {
-            pCur++;
-            // read number of constraints
-            pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4;
-        }
-        if ( *pCur == 'n' )
+        extern Vec_Int_t * Gia_AigerReadLiterals( char ** ppPos, int nEntries );
+        char * pPos = Vec_StrArray( vBinary );
+        Vec_Int_t * vTemp = Gia_AigerReadLiterals( &pPos, Vec_IntSize(vLits) );
+        for ( i = 0; i < Vec_IntSize(vLits); i++ )
         {
-            pCur++;
-            // read model name
-            ABC_FREE( pNew->pName );
-            pNew->pName = Abc_UtilStrsav( (char *)pCur );
+            int Entry1 = Vec_IntEntry(vLits,i);
+            int Entry2 = Vec_IntEntry(vTemp,i);
+            assert( Entry1 == Entry2 );
         }
-    }
-    Vec_IntFree( vNodes );
-
-    // update polarity of the additional outputs
-    if ( nBad || nConstr || nJust || nFair )
-        Gia_ManInvertConstraints( pNew );
-
-    // skipping the comments
-/*
-    // check the result
-    if ( fCheck && !Gia_ManCheck( pNew ) )
-    {
-        printf( "Gia_ReadAiger: The network check has failed.\n" );
-        Gia_ManStop( pNew );
-        return NULL;
+        Vec_IntFree( vTemp );
     }
 */
-    return pNew;
+    return vBinary;
 }
 
 /**Function*************************************************************
@@ -640,7 +171,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck )
+Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck )
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
@@ -745,7 +276,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
     }
     else // modified AIGER
     {
-        vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
+        vLits = Gia_AigerReadLiterals( &pCur, nLatches + nOutputs );
     }
 
     // create the AND gates
@@ -754,8 +285,8 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
     for ( i = 0; i < nAnds; i++ )
     {
         uLit = ((i + 1 + nInputs + nLatches) << 1);
-        uLit1 = uLit  - Gia_ReadAigerDecode( &pCur );
-        uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
+        uLit1 = uLit  - Gia_AigerReadUnsigned( &pCur );
+        uLit0 = uLit1 - Gia_AigerReadUnsigned( &pCur );
 //        assert( uLit1 > uLit0 );
         iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
         iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
@@ -963,91 +494,151 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
     // check if there are other types of information to read
     if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
     {
+        Vec_Str_t * vStr;
+        char * pCurTemp;
         pCur++;
-        if ( *pCur == 'e' )
+        while ( 1 )
         {
-            pCur++;
+            // read extra AIG
+            if ( *pCur == 'a' )
+            {
+                pCur++;
+                vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );       pCur += 4;
+                memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
+                pCur += Vec_StrSize(vStr);
+                pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 );
+                Vec_StrFree( vStr );
+            }
+            // read number of constraints
+            else if ( *pCur == 'c' )
+            {
+                pCur++;
+                assert( Gia_AigerReadInt(pCur) == 4 );                pCur += 4;
+                pNew->nConstrs = Gia_AigerReadInt( pCur );            pCur += 4;
+            }
+            // read delay information
+            else if ( *pCur == 'd' )
+            {
+                pCur++;
+                assert( Gia_AigerReadInt(pCur) == 4*(Gia_ManPiNum(pNew) + Gia_ManPoNum(pNew)) );   pCur += 4;
+                pNew->vInArrs  = Vec_FltStart( Gia_ManPiNum(pNew) );
+                pNew->vOutReqs = Vec_FltStart( Gia_ManPoNum(pNew) );
+                memcpy( Vec_FltArray(pNew->vInArrs),  pCur, 4*Gia_ManPiNum(pNew) );   pCur += 4*Gia_ManPiNum(pNew);
+                memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*Gia_ManPoNum(pNew) );   pCur += 4*Gia_ManPoNum(pNew);
+            }
             // read equivalence classes
-            pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
-            pNew->pNexts = Gia_ManDeriveNexts( pNew );
-        }
-        if ( *pCur == 'f' )
-        {
-            pCur++;
+            else if ( *pCur == 'e' )
+            {
+                extern Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize );
+                pCur++;
+    //            pCurTemp = pCur + Gia_AigerReadInt(pCur);                    pCur += 4;
+                pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
+                pNew->pNexts = Gia_ManDeriveNexts( pNew );
+    //            assert( pCur == pCurTemp );
+            }
             // read flop classes
-            pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
-            Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) );
-        }
-        if ( *pCur == 'g' )
-        {
-            pCur++;
+            else if ( *pCur == 'f' )
+            {
+                pCur++;
+                assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) );   pCur += 4;
+                pNew->vFlopClasses  = Vec_IntStart( Gia_ManRegNum(pNew) );
+                memcpy( Vec_IntArray(pNew->vFlopClasses),  pCur, 4*Gia_ManRegNum(pNew) );   pCur += 4*Gia_ManRegNum(pNew);
+            }
             // read gate classes
-            pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) );
-            Gia_ReadFlopClasses( &pCur, pNew->vGateClasses, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 'v' )
-        {
-            pCur++;
-            // read object classes
-            pNew->vObjClasses = Vec_IntStart( Gia_ReadInt(pCur)/4 ); pCur += 4;
-            memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) );
-            pCur += 4*Vec_IntSize(pNew->vObjClasses);
-        }
-        if ( *pCur == 'm' )
-        {
-            pCur++;
+            else if ( *pCur == 'g' )
+            {
+                pCur++;
+                assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) );   pCur += 4;
+                pNew->vGateClasses  = Vec_IntStart( Gia_ManObjNum(pNew) );
+                memcpy( Vec_IntArray(pNew->vGateClasses),  pCur, 4*Gia_ManObjNum(pNew) );   pCur += 4*Gia_ManObjNum(pNew);
+            }
+            // read hierarchy information
+            else if ( *pCur == 'h' )
+            {
+                pCur++;
+                vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );          pCur += 4;
+                memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
+                pCur += Vec_StrSize(vStr);
+                pNew->pManTime = Tim_ManLoad( vStr, 1 );
+                Vec_StrFree( vStr );
+            }
+            // read packing
+            else if ( *pCur == 'k' )
+            {
+                extern Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize );
+                pCur++;
+                pCurTemp = pCur + Gia_AigerReadInt(pCur);               pCur += 4;
+                pNew->vPacking = Gia_AigerReadPacking( &pCur, pCurTemp - pCur ); 
+                assert( pCur == pCurTemp );
+            }
             // read mapping
-            pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 'p' )
-        {
-            pCur++;
+            else if ( *pCur == 'm' )
+            {
+                extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
+                pCur++;
+                pCurTemp = pCur + Gia_AigerReadInt(pCur);               pCur += 4;
+                pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) );
+                assert( pCur == pCurTemp );
+            }
+            // read model name
+            else if ( *pCur == 'n' )
+            {
+                pCur++;
+                if ( (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z') || (*pCur >= '0' && *pCur <= '9') )
+                {
+                    pNew->pName = Abc_UtilStrsav( (char *)pCur );       pCur += strlen(pNew->pName) + 1;
+                }
+                else
+                {
+                    pCurTemp = pCur + Gia_AigerReadInt(pCur);           pCur += 4;
+                    ABC_FREE( pNew->pName );
+                    pNew->pName = Abc_UtilStrsav( (char *)pCur );       pCur += strlen(pNew->pName) + 1;
+                    assert( pCur == pCurTemp );
+                }
+            }
             // read placement
-            pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 's' )
-        { 
-            pCur++;
+            else if ( *pCur == 'p' )
+            {
+                Gia_Plc_t * pPlacement;
+                pCur++;
+                pCurTemp = pCur + Gia_AigerReadInt(pCur);               pCur += 4;
+                pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) );
+                memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) );      pCur += 4*Gia_ManObjNum(pNew);
+                assert( pCur == pCurTemp );
+            }
             // read switching activity
-            pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) );
-        }
-        if ( *pCur == 't' )
-        {
-            Vec_Str_t * vStr;
-            pCur++;
+            else if ( *pCur == 's' )
+            { 
+                unsigned char * pSwitching;
+                pCur++;
+                pCurTemp = pCur + Gia_AigerReadInt(pCur);               pCur += 4;
+                pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) );
+                memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) );        pCur += Gia_ManObjNum(pNew);
+                assert( pCur == pCurTemp );
+            }
             // read timing manager
-            vStr = Vec_StrStart( Gia_ReadInt(pCur) ); pCur += 4;
-            memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
-            pCur += Vec_StrSize(vStr);
-            pNew->pManTime = Tim_ManLoad( vStr );
-            Vec_StrFree( vStr );
-        }
-        if ( *pCur == 'c' )
-        {
-            pCur++;
-            // read number of constraints
-            pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4;
-        }
-        if ( *pCur == 'n' )
-        {
-            pCur++;
-            // read model name
-            ABC_FREE( pNew->pName );
-            pNew->pName = Abc_UtilStrsav( (char *)pCur );
+            else if ( *pCur == 't' )
+            {
+                pCur++;
+                vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );          pCur += 4;
+                memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );  pCur += Vec_StrSize(vStr);
+                pNew->pManTime = Tim_ManLoad( vStr, 0 );
+                Vec_StrFree( vStr );
+            }
+            // read object classes
+            else if ( *pCur == 'v' )
+            {
+                pCur++;
+                pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4;
+                memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) );
+                pCur += 4*Vec_IntSize(pNew->vObjClasses);
+            }
+            else break;
         }
     }
 
     // skipping the comments
     Vec_IntFree( vNodes );
-/*
-    // check the result
-    if ( fCheck && !Gia_ManCheck( pNew ) )
-    {
-        printf( "Gia_ReadAiger: The network check has failed.\n" );
-        Gia_ManStop( pNew );
-        return NULL;
-    }
-*/
 
     // update polarity of the additional outputs
     if ( nBad || nConstr || nJust || nFair )
@@ -1083,6 +674,15 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
         pNew = Gia_ManDupUnnomalize( pTemp = pNew );
         Gia_ManStop( pTemp );
     }
+/*
+    // check the result
+    if ( fCheck && !Gia_ManCheck( pNew ) )
+    {
+        printf( "Gia_AigerRead: The network check has failed.\n" );
+        Gia_ManStop( pNew );
+        return NULL;
+    }
+*/
     return pNew;
 }
 
@@ -1097,7 +697,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck )
+Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
 {
     FILE * pFile;
     Gia_Man_t * pNew;
@@ -1106,14 +706,14 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck )
     int RetValue;
 
     // read the file into the buffer
-    Gia_FixFileName( pFileName );
+    Gia_FileFixName( pFileName );
     nFileSize = Gia_FileSize( pFileName );
     pFile = fopen( pFileName, "rb" );
     pContents = ABC_ALLOC( char, nFileSize );
     RetValue = fread( pContents, nFileSize, 1, pFile );
     fclose( pFile );
 
-    pNew = Gia_ReadAigerFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
+    pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
     ABC_FREE( pContents );
     if ( pNew )
     {
@@ -1132,237 +732,161 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds one unsigned AIG edge to the output buffer.]
-
-  Description [This procedure is a slightly modified version of Armin Biere's
-  procedure "void encode (FILE * file, unsigned x)" ]
-  
-  SideEffects [Returns the current writing position.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
-{
-    unsigned char ch;
-    while (x & ~0x7f)
-    {
-        ch = (x & 0x7f) | 0x80;
-        pBuffer[Pos++] = ch;
-        x >>= 7;
-    }
-    ch = x;
-    pBuffer[Pos++] = ch;
-    return Pos;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create the array of literals to be written.]
+  Synopsis    [Writes the AIG in into the memory buffer.]
 
-  Description []
+  Description [The resulting buffer constains the AIG in AIGER format. 
+  The resulting buffer should be deallocated by the user.]
   
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_WriteAigerLiterals( Gia_Man_t * p )
+Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p )
 {
-    Vec_Int_t * vLits;
+    Vec_Str_t * vBuffer;
     Gia_Obj_t * pObj;
-    int i;
-    vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
-    Gia_ManForEachRi( p, pObj, i )
-        Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
-    Gia_ManForEachPo( p, pObj, i )
-        Vec_IntPush( vLits, Gia_ObjFaninLit0p(p, pObj) );
-    return vLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the binary encoded array of literals.]
+    int nNodes = 0, i, uLit, uLit0, uLit1; 
+    // set the node numbers to be used in the output file
+    Gia_ManConst0(p)->Value = nNodes++;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = nNodes++;
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = nNodes++;
 
-  Description []
-  
-  SideEffects []
+    // write the header "M I L O A" where M = I + L + A
+    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
+    Vec_StrPrintStr( vBuffer, "aig " );
+    Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
+    Vec_StrPrintStr( vBuffer, "\n" );
 
-  SeeAlso     []
+    // write latch drivers
+    Gia_ManForEachRi( p, pObj, i )
+    {
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
+    }
 
-***********************************************************************/
-Vec_Str_t * Gia_WriteEncodeLiterals( Vec_Int_t * vLits )
-{
-    Vec_Str_t * vBinary;
-    int Pos = 0, Lit, LitPrev, Diff, i;
-    vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
-    LitPrev = Vec_IntEntry( vLits, 0 );
-    Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
-    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
+    // write PO drivers
+    Gia_ManForEachPo( p, pObj, i )
     {
-        Diff = Lit - LitPrev;
-        Diff = (Lit < LitPrev)? -Diff : Diff;
-        Diff = (Diff << 1) | (int)(Lit < LitPrev);
-        Pos = Gia_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
-        LitPrev = Lit;
-        if ( Pos + 10 > vBinary->nCap )
-            Vec_StrGrow( vBinary, vBinary->nCap+1 );
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
     }
-    vBinary->nSize = Pos;
-/*
-    // verify
+    // write the nodes into the buffer
+    Gia_ManForEachAnd( p, pObj, i )
     {
-        extern Vec_Int_t * Gia_WriteDecodeLiterals( char ** ppPos, int nEntries );
-        char * pPos = Vec_StrArray( vBinary );
-        Vec_Int_t * vTemp = Gia_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
-        for ( i = 0; i < Vec_IntSize(vLits); i++ )
+        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
+        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
+        assert( uLit0 != uLit1 );
+        if ( uLit0 > uLit1 )
         {
-            int Entry1 = Vec_IntEntry(vLits,i);
-            int Entry2 = Vec_IntEntry(vTemp,i);
-            assert( Entry1 == Entry2 );
+            int Temp = uLit0;
+            uLit0 = uLit1;
+            uLit1 = Temp;
         }
-        Vec_IntFree( vTemp );
+        Gia_AigerWriteUnsigned( vBuffer, uLit  - uLit1 );
+        Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
     }
-*/
-    return vBinary;
+    Vec_StrPrintStr( vBuffer, "c" );
+    return vBuffer;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Write integer into the string.]
+  Synopsis    [Writes the AIG in into the memory buffer.]
 
-  Description []
+  Description [The resulting buffer constains the AIG in AIGER format.
+  The CI/CO/AND nodes are assumed to be ordered according to some rule.
+  The resulting buffer should be deallocated by the user.]
   
-  SideEffects []
+  SideEffects [Note that in vCos, PIs are order first, followed by latches!]
 
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_WriteInt( unsigned char * pPos, int Value )
+Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
 {
-    int i;
-    for ( i = 3; i >= 0; i-- )
-        *pPos++ = (Value >> (8*i)) & 255;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read equivalence classes from the string.]
-
-  Description []
-  
-  SideEffects []
+    Vec_Str_t * vBuffer;
+    Gia_Obj_t * pObj;
+    int nNodes = 0, i, uLit, uLit0, uLit1; 
+    // set the node numbers to be used in the output file
+    Gia_ManConst0(p)->Value = nNodes++;
+    Gia_ManForEachObjVec( vCis, p, pObj, i )
+    {
+        assert( Gia_ObjIsCi(pObj) );
+        pObj->Value = nNodes++;
+    }
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        pObj->Value = nNodes++;
+    }
 
-  SeeAlso     []
+    // write the header "M I L O A" where M = I + L + A
+    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
+    Vec_StrPrintStr( vBuffer, "aig " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
+    Vec_StrPrintStr( vBuffer, "\n" );
 
-***********************************************************************/
-unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
-{
-    unsigned char * pBuffer;
-    int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos;
-    assert( p->pReprs && p->pNexts );
-    // count the number of entries to be written
-    nItems = 0;
-    for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ )
+    // write latch drivers
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
     {
-        nItems += Gia_ObjIsConst( p, iRepr );
-        if ( !Gia_ObjIsHead(p, iRepr) )
+        assert( Gia_ObjIsCo(pObj) );
+        if ( i < Vec_IntSize(vCos) - nRegs )
             continue;
-        Gia_ClassForEachObj( p, iRepr, iNode )
-            nItems++;
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
     }
-    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) );
-    // write constant class
-    iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) );
-//printf( "\nRepr = %d ", 0 );
-    iPrevNode = 0;
-    for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
-        if ( Gia_ObjIsConst(p, iNode) )
-        {
-//printf( "Node = %d ", iNode );
-            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
-            iPrevNode = iNode;
-            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
-        }
-    // write non-constant classes
-    iPrevRepr = 0;
-    Gia_ManForEachClass( p, iRepr )
+    // write output drivers
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
     {
-//printf( "\nRepr = %d ", iRepr );
-        iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
-        iPrevRepr = iPrevNode = iRepr;
-        Gia_ClassForEachObj1( p, iRepr, iNode )
-        {
-//printf( "Node = %d ", iNode );
-            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
-            iPrevNode = iNode;
-            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
-        }
+        assert( Gia_ObjIsCo(pObj) );
+        if ( i >= Vec_IntSize(vCos) - nRegs )
+            continue;
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
     }
-    Gia_WriteInt( pBuffer, iPos );
-    *pEquivSize = iPos;
-    return pBuffer;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads decoded value.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_WriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
-{
-    if ( iPrev < iThis )
-        return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
-    return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read equivalence classes from the string.]
-
-  Description []
-  
-  SideEffects []
 
-  SeeAlso     []
-
-***********************************************************************/
-unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize )
-{
-    unsigned char * pBuffer;
-    int i, k, iPrev, iFan, nItems, iPos = 4;
-    assert( p->pMapping );
-    // count the number of entries to be written
-    nItems = 0;
-    Gia_ManForEachLut( p, i )
-        nItems += 2 + Gia_ObjLutSize( p, i );
-    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
-    // write non-constant classes
-    iPrev = 0;
-    Gia_ManForEachLut( p, i )
+    // write the nodes into the buffer
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
     {
-//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) );
-        iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_ObjLutSize(p, i) );
-        Gia_LutForEachFanin( p, i, iFan, k )
+        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
+        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
+        assert( uLit0 != uLit1 );
+        if ( uLit0 > uLit1 )
         {
-//printf( "Fan = %d ", iFan );
-            iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, iFan );
-            iPrev = iFan;
+            int Temp = uLit0;
+            uLit0 = uLit1;
+            uLit1 = Temp;
         }
-        iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, i );
-        iPrev = i;
-//printf( "Node = %d ", i );
+        Gia_AigerWriteUnsigned( vBuffer, uLit  - uLit1 );
+        Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
     }
-//printf( "\n" );
-    Gia_WriteInt( pBuffer, iPos );
-    *pMapSize = iPos;
-    return pBuffer;
+    Vec_StrPrintStr( vBuffer, "c" );
+    return vBuffer;
 }
 
 /**Function*************************************************************
@@ -1376,11 +900,12 @@ unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
+void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
 {
     FILE * pFile;
     Gia_Man_t * p;
     Gia_Obj_t * pObj;
+    Vec_Str_t * vStrExt;
     int i, nBufferSize, Pos;
     unsigned char * pBuffer;
     unsigned uLit0, uLit1, uLit;
@@ -1395,14 +920,14 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Gia_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
+        fprintf( stdout, "Gia_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
 
     // create normalized AIG
     if ( !Gia_ManIsNormalized(pInit) )
     {
-//        printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
+//        printf( "Gia_AigerWrite(): Normalizing AIG for writing.\n" );
         p = Gia_ManDupNormalize( pInit );
         p->pManTime  = pInit->pManTime;  pInit->pManTime = NULL;
         p->vNamesIn  = pInit->vNamesIn;  pInit->vNamesIn = NULL;
@@ -1436,8 +961,8 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     }
     else
     {
-        Vec_Int_t * vLits = Gia_WriteAigerLiterals( p );
-        Vec_Str_t * vBinary = Gia_WriteEncodeLiterals( vLits );
+        Vec_Int_t * vLits = Gia_AigerCollectLiterals( p );
+        Vec_Str_t * vBinary = Gia_AigerWriteLiterals( vLits );
         fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
         Vec_StrFree( vBinary );
         Vec_IntFree( vLits );
@@ -1454,11 +979,11 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         uLit0 = Gia_ObjFaninLit0( pObj, i );
         uLit1 = Gia_ObjFaninLit1( pObj, i );
         assert( p->nPinTypes || uLit0 < uLit1 );
-        Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
-        Pos = Gia_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+        Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit  - uLit1 );
+        Pos = Gia_AigerWriteUnsignedBuffer( pBuffer, Pos, uLit1 - uLit0 );
         if ( Pos > nBufferSize - 10 )
         {
-            printf( "Gia_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
+            printf( "Gia_AigerWrite(): AIGER generation has failed because the allocated buffer is too small.\n" );
             fclose( pFile );
             if ( p != pInit )
                 Gia_ManStop( p );
@@ -1489,99 +1014,130 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
 
     // write the comment
     fprintf( pFile, "c" );
+
+    // write additional AIG
+    if ( p->pAigExtra )
+    {
+        fprintf( pFile, "a" );
+        vStrExt = Gia_AigerWriteIntoMemoryStr( p->pAigExtra );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
+    }
+/*
+    // write constraints
+    if ( p->nConstrs )
+    {
+        fprintf( pFile, "c" );
+        Gia_FileWriteBufferSize( pFile, 4 );
+        Gia_FileWriteBufferSize( pFile, p->nConstrs );
+    }
+*/
+    // write gate classes
+    if ( p->vInArrs && p->vOutReqs )
+    {
+        fprintf( pFile, "d" );
+        Gia_FileWriteBufferSize( pFile, 4*(Gia_ManPiNum(p) + Gia_ManPoNum(p)) );
+        assert( Vec_FltSize(p->vInArrs)  == Gia_ManPiNum(p) );
+        assert( Vec_FltSize(p->vOutReqs) == Gia_ManPoNum(p) );
+        fwrite( Vec_FltArray(p->vInArrs),  1, 4*Gia_ManPiNum(p), pFile );
+        fwrite( Vec_FltArray(p->vOutReqs), 1, 4*Gia_ManPoNum(p), pFile );
+    }
     // write equivalences
     if ( p->pReprs && p->pNexts )
     {
-        int nEquivSize;
-        unsigned char * pEquivs = Gia_WriteEquivClasses( p, &nEquivSize );
+        extern Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p );
         fprintf( pFile, "e" );
-        fwrite( pEquivs, 1, nEquivSize, pFile );
-        ABC_FREE( pEquivs );
+        vStrExt = Gia_WriteEquivClasses( p );
+//        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
     }
     // write flop classes
     if ( p->vFlopClasses )
     {
-        unsigned char Buffer[10];
-        int nSize = 4*Gia_ManRegNum(p);
-        Gia_WriteInt( Buffer, nSize );
         fprintf( pFile, "f" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile );
+        Gia_FileWriteBufferSize( pFile, 4*Gia_ManRegNum(p) );
+        assert( Vec_IntSize(p->vFlopClasses) == Gia_ManRegNum(p) );
+        fwrite( Vec_IntArray(p->vFlopClasses), 1, 4*Gia_ManRegNum(p), pFile );
     }
     // write gate classes
     if ( p->vGateClasses )
     {
-        unsigned char Buffer[10];
-        int nSize = 4*Gia_ManObjNum(p);
-        Gia_WriteInt( Buffer, nSize );
         fprintf( pFile, "g" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( Vec_IntArray(p->vGateClasses), 1, nSize, pFile );
+        Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
+        assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
+        fwrite( Vec_IntArray(p->vGateClasses), 1, 4*Gia_ManObjNum(p), pFile );
     }
-    // write object classes
-    if ( p->vObjClasses )
+    // write hierarchy info
+    if ( p->pManTime )
     {
-        unsigned char Buffer[10];
-        int nSize = 4*Vec_IntSize(p->vObjClasses);
-        Gia_WriteInt( Buffer, nSize );
-        fprintf( pFile, "v" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( Vec_IntArray(p->vObjClasses), 1, nSize, pFile );
+        fprintf( pFile, "h" );
+        vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 1 );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
+    }
+    // write packing
+    if ( p->vPacking )
+    {
+        extern Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking );
+        fprintf( pFile, "k" );
+        vStrExt = Gia_WritePacking( p->vPacking );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
     }
     // write mapping
     if ( p->pMapping )
     {
-        int nMapSize;
-        unsigned char * pMaps = Gia_WriteMapping( p, &nMapSize );
+        extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
         fprintf( pFile, "m" );
-        fwrite( pMaps, 1, nMapSize, pFile );
-        ABC_FREE( pMaps );
+        vStrExt = Gia_AigerWriteMapping( p );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
+    }
+    // write name
+    if ( p->pName )
+    {
+        fprintf( pFile, "n" );
+        Gia_FileWriteBufferSize( pFile, strlen(p->pName)+1 );
+        fwrite( p->pName, 1, strlen(p->pName), pFile );
+        fprintf( pFile, "\0" );
     }
     // write placement
     if ( p->pPlacement )
     {
-        unsigned char Buffer[10];
-        int nSize = 4*Gia_ManObjNum(p);
-        Gia_WriteInt( Buffer, nSize );
         fprintf( pFile, "p" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( p->pPlacement, 1, nSize, pFile );
+        Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
+        fwrite( p->pPlacement, 1, 4*Gia_ManObjNum(p), pFile );
     }
     // write switching activity
     if ( p->pSwitching )
     {
-        unsigned char Buffer[10];
-        int nSize = Gia_ManObjNum(p);
-        Gia_WriteInt( Buffer, nSize );
         fprintf( pFile, "s" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( p->pSwitching, 1, nSize, pFile );
+        Gia_FileWriteBufferSize( pFile, Gia_ManObjNum(p) );
+        fwrite( p->pSwitching, 1, Gia_ManObjNum(p), pFile );
     }
     // write timing information
     if ( p->pManTime )
     {
-        Vec_Str_t * vStr = Tim_ManSave( (Tim_Man_t *)p->pManTime );
-        unsigned char Buffer[10];
-        int nSize = Vec_StrSize(vStr);
-        Gia_WriteInt( Buffer, nSize );
         fprintf( pFile, "t" );
-        fwrite( Buffer, 1, 4, pFile );
-        fwrite( Vec_StrArray(vStr), 1, nSize, pFile );
-        Vec_StrFree( vStr );
+        vStrExt = Tim_ManSave( (Tim_Man_t *)p->pManTime, 0 );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
     }
-/*
-    // write constraints
-    if ( p->nConstrs )
+    // write object classes
+    if ( p->vObjClasses )
     {
-        unsigned char Buffer[10];
-        Gia_WriteInt( Buffer, p->nConstrs );
-        fprintf( pFile, "c" );
-        fwrite( Buffer, 1, 4, pFile );
+        fprintf( pFile, "v" );
+        Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
+        assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
+        fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
     }
-*/
-    // write name
-    if ( p->pName )
-        fprintf( pFile, "n%s%c", p->pName, '\0' );
+    // write comments
     fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
     fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
     fclose( pFile );
@@ -1609,195 +1165,7 @@ void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNu
 {
     char Buffer[100];
     sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
-    Gia_WriteAiger( p, Buffer, 0, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one unsigned AIG edge to the output buffer.]
-
-  Description [This procedure is a slightly modified version of Armin Biere's
-  procedure "void encode (FILE * file, unsigned x)" ]
-  
-  SideEffects [Returns the current writing position.]
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x )
-{
-    unsigned char ch;
-    while (x & ~0x7f)
-    {
-        ch = (x & 0x7f) | 0x80;
-//        putc (ch, file);
-//        pBuffer[Pos++] = ch;
-        Vec_StrPush( vStr, ch );
-        x >>= 7;
-    }
-    ch = x;
-//    putc (ch, file);
-//    pBuffer[Pos++] = ch;
-    Vec_StrPush( vStr, ch );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the AIG in into the memory buffer.]
-
-  Description [The resulting buffer constains the AIG in AIGER format. 
-  The resulting buffer should be deallocated by the user.]
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
-{
-    Vec_Str_t * vBuffer;
-    Gia_Obj_t * pObj;
-    int nNodes = 0, i, uLit, uLit0, uLit1; 
-    // set the node numbers to be used in the output file
-    Gia_ManConst0(p)->Value = nNodes++;
-    Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = nNodes++;
-    Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = nNodes++;
-
-    // write the header "M I L O A" where M = I + L + A
-    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
-    Vec_StrPrintStr( vBuffer, "aig " );
-    Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
-    Vec_StrPrintStr( vBuffer, "\n" );
-
-    // write latch drivers
-    Gia_ManForEachRi( p, pObj, i )
-    {
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        Vec_StrPrintNum( vBuffer, uLit );
-        Vec_StrPrintStr( vBuffer, "\n" );
-    }
-
-    // write PO drivers
-    Gia_ManForEachPo( p, pObj, i )
-    {
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        Vec_StrPrintNum( vBuffer, uLit );
-        Vec_StrPrintStr( vBuffer, "\n" );
-    }
-    // write the nodes into the buffer
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
-        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
-        assert( uLit0 != uLit1 );
-        if ( uLit0 > uLit1 )
-        {
-            int Temp = uLit0;
-            uLit0 = uLit1;
-            uLit1 = Temp;
-        }
-        Gia_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
-        Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
-    }
-    Vec_StrPrintStr( vBuffer, "c" );
-    return vBuffer;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the AIG in into the memory buffer.]
-
-  Description [The resulting buffer constains the AIG in AIGER format.
-  The CI/CO/AND nodes are assumed to be ordered according to some rule.
-  The resulting buffer should be deallocated by the user.]
-  
-  SideEffects [Note that in vCos, PIs are order first, followed by latches!]
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
-{
-    Vec_Str_t * vBuffer;
-    Gia_Obj_t * pObj;
-    int nNodes = 0, i, uLit, uLit0, uLit1; 
-    // set the node numbers to be used in the output file
-    Gia_ManConst0(p)->Value = nNodes++;
-    Gia_ManForEachObjVec( vCis, p, pObj, i )
-    {
-        assert( Gia_ObjIsCi(pObj) );
-        pObj->Value = nNodes++;
-    }
-    Gia_ManForEachObjVec( vAnds, p, pObj, i )
-    {
-        assert( Gia_ObjIsAnd(pObj) );
-        pObj->Value = nNodes++;
-    }
-
-    // write the header "M I L O A" where M = I + L + A
-    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
-    Vec_StrPrintStr( vBuffer, "aig " );
-    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, nRegs );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
-    Vec_StrPrintStr( vBuffer, " " );
-    Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
-    Vec_StrPrintStr( vBuffer, "\n" );
-
-    // write latch drivers
-    Gia_ManForEachObjVec( vCos, p, pObj, i )
-    {
-        assert( Gia_ObjIsCo(pObj) );
-        if ( i < Vec_IntSize(vCos) - nRegs )
-            continue;
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        Vec_StrPrintNum( vBuffer, uLit );
-        Vec_StrPrintStr( vBuffer, "\n" );
-    }
-    // write output drivers
-    Gia_ManForEachObjVec( vCos, p, pObj, i )
-    {
-        assert( Gia_ObjIsCo(pObj) );
-        if ( i >= Vec_IntSize(vCos) - nRegs )
-            continue;
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        Vec_StrPrintNum( vBuffer, uLit );
-        Vec_StrPrintStr( vBuffer, "\n" );
-    }
-
-    // write the nodes into the buffer
-    Gia_ManForEachObjVec( vAnds, p, pObj, i )
-    {
-        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
-        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
-        assert( uLit0 != uLit1 );
-        if ( uLit0 > uLit1 )
-        {
-            int Temp = uLit0;
-            uLit0 = uLit1;
-            uLit1 = Temp;
-        }
-        Gia_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
-        Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
-    }
-    Vec_StrPrintStr( vBuffer, "c" );
-    return vBuffer;
+    Gia_AigerWrite( p, Buffer, 0, 0 );
 }
 
 /**Function*************************************************************
@@ -1811,24 +1179,24 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName )
+void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName )
 {
     FILE * pFile;
     Vec_Str_t * vStr;
     if ( Gia_ManPoNum(pInit) == 0 )
     {
-        printf( "Gia_WriteAigerSimple(): AIG cannot be written because it has no POs.\n" );
+        printf( "Gia_AigerWriteSimple(): AIG cannot be written because it has no POs.\n" );
         return;
     }
     // start the output stream
     pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Gia_WriteAigerSimple(): Cannot open the output file \"%s\".\n", pFileName );
+        fprintf( stdout, "Gia_AigerWriteSimple(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
     // write the buffer
-    vStr = Gia_WriteAigerIntoMemoryStr( pInit );
+    vStr = Gia_AigerWriteIntoMemoryStr( pInit );
     fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
     Vec_StrFree( vStr );
     fclose( pFile );
diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c
new file mode 100644
index 00000000..fa79e589
--- /dev/null
+++ b/src/aig/gia/giaAigerExt.c
@@ -0,0 +1,240 @@
+/**CFile****************************************************************
+
+  FileName    [giaAigerExt.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Custom AIGER extensions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAigerExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Read/write equivalence classes information.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize )
+{
+    Gia_Rpr_t * pReprs;
+    unsigned char * pStop;
+    int i, Item, fProved, iRepr, iNode;
+    pStop = *ppPos;
+    pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
+    pReprs = ABC_CALLOC( Gia_Rpr_t, nSize );
+    for ( i = 0; i < nSize; i++ )
+        pReprs[i].iRepr = GIA_VOID;
+    iRepr = iNode = 0;
+    while ( *ppPos < pStop )
+    {
+        Item = Gia_AigerReadUnsigned( ppPos );
+        if ( Item & 1 )
+        {
+            iRepr += (Item >> 1);
+            iNode = iRepr;
+            continue;
+        }
+        Item >>= 1;
+        fProved = (Item & 1);
+        Item >>= 1;
+        iNode += Item;
+        pReprs[iNode].fProved = fProved;
+        pReprs[iNode].iRepr = iRepr;
+        assert( iRepr < iNode );
+    }
+    return pReprs;
+}
+unsigned char * Gia_WriteEquivClassesInt( Gia_Man_t * p, int * pEquivSize )
+{
+    unsigned char * pBuffer;
+    int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos;
+    assert( p->pReprs && p->pNexts );
+    // count the number of entries to be written
+    nItems = 0;
+    for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ )
+    {
+        nItems += Gia_ObjIsConst( p, iRepr );
+        if ( !Gia_ObjIsHead(p, iRepr) )
+            continue;
+        Gia_ClassForEachObj( p, iRepr, iNode )
+            nItems++;
+    }
+    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) );
+    // write constant class
+    iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, 4, Abc_Var2Lit(0, 1) );
+    iPrevNode = 0;
+    for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
+        if ( Gia_ObjIsConst(p, iNode) )
+        {
+            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+            iPrevNode = iNode;
+            iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
+        }
+    // write non-constant classes
+    iPrevRepr = 0;
+    Gia_ManForEachClass( p, iRepr )
+    {
+        iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
+        iPrevRepr = iPrevNode = iRepr;
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+        {
+            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+            iPrevNode = iNode;
+            iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
+        }
+    }
+    Gia_AigerWriteInt( pBuffer, iPos );
+    *pEquivSize = iPos;
+    return pBuffer;
+}
+Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p )
+{
+    int nEquivSize;
+    unsigned char * pBuffer = Gia_WriteEquivClassesInt( p, &nEquivSize );
+    return Vec_StrAllocArray( pBuffer, nEquivSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read/write mapping information.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Gia_AigerReadDiffValue( unsigned char ** ppPos, int iPrev )
+{
+    int Item = Gia_AigerReadUnsigned( ppPos );
+    if ( Item & 1 )
+        return iPrev + (Item >> 1);
+    return iPrev - (Item >> 1);
+}
+int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize )
+{
+    int * pMapping;
+    unsigned char * pStop;
+    int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize;
+    pStop = *ppPos;
+    pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
+    nAlloc = nSize + pStop - *ppPos;
+    pMapping = ABC_CALLOC( int, nAlloc );
+    while ( *ppPos < pStop )
+    {
+        k = iOffset;
+        pMapping[k++] = nFanins = Gia_AigerReadUnsigned( ppPos );
+        for ( j = 0; j <= nFanins; j++ )
+            pMapping[k++] = iNode = Gia_AigerReadDiffValue( ppPos, iNode );
+        pMapping[iNode] = iOffset;
+        iOffset = k;
+    }
+    assert( iOffset <= nAlloc );
+    return pMapping;
+}
+static inline int Gia_AigerWriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
+{
+    if ( iPrev < iThis )
+        return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
+    return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
+}
+unsigned char * Gia_AigerWriteMappingInt( Gia_Man_t * p, int * pMapSize )
+{
+    unsigned char * pBuffer;
+    int i, k, iPrev, iFan, nItems, iPos = 4;
+    assert( p->pMapping );
+    // count the number of entries to be written
+    nItems = 0;
+    Gia_ManForEachLut( p, i )
+        nItems += 2 + Gia_ObjLutSize( p, i );
+    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
+    // write non-constant classes
+    iPrev = 0;
+    Gia_ManForEachLut( p, i )
+    {
+//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) );
+        iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Gia_ObjLutSize(p, i) );
+        Gia_LutForEachFanin( p, i, iFan, k )
+        {
+//printf( "Fan = %d ", iFan );
+            iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, iFan );
+            iPrev = iFan;
+        }
+        iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, i );
+        iPrev = i;
+//printf( "Node = %d ", i );
+    }
+//printf( "\n" );
+    Gia_AigerWriteInt( pBuffer, iPos );
+    *pMapSize = iPos;
+    return pBuffer;
+}
+Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p )
+{
+    int nMapSize;
+    unsigned char * pBuffer = Gia_AigerWriteMappingInt( p, &nMapSize );
+    return Vec_StrAllocArray( pBuffer, nMapSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read/write packing information.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize )
+{
+    Vec_Int_t * vPacking = Vec_IntStart( nSize/4 );
+    assert( nSize % 4 == 0 );
+    memcpy( Vec_IntArray(vPacking), *ppPos, nSize );
+    *ppPos += nSize;
+    return vPacking;
+}
+Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking )
+{
+    Vec_Str_t * vBuffer = Vec_StrStart( 4*Vec_IntSize(vPacking) );
+    memcpy( Vec_StrArray(vBuffer), Vec_IntArray(vPacking), 4*sizeof(int) );
+    return vBuffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index d8545cd5..5ddd9b08 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1203,7 +1203,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
         return;
     }
     // read AIGER file
-    pMiter = Gia_ReadAiger( pFileName, 0, 0 );
+    pMiter = Gia_AigerRead( pFileName, 0, 0 );
     if ( pMiter == NULL )
     {
         Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
@@ -1722,14 +1722,14 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
             }
         }
         // write equivalence classes
-        Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
+        Gia_AigerWrite( pGia, "gore.aig", 0, 0 );
         // reduce the model
         pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
             Gia_ManStop( pAux );
-            Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
 //            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
 //          Gia_ManPrintStatsShort( pReduce );
             Gia_ManStop( pReduce );
@@ -1762,13 +1762,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
         Abc_Print( 1, "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_ReadAiger( pName1, 0, 0 );
+    pGia1 = Gia_AigerRead( pName1, 0, 0 );
     if ( pGia1 == NULL )
     {
         Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_ReadAiger( pName2, 0, 0 );
+    pGia2 = Gia_AigerRead( pName2, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
@@ -1901,13 +1901,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
         Abc_Print( 1, "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_ReadAiger( pName1, 0, 0 );
+    pGia1 = Gia_AigerRead( pName1, 0, 0 );
     if ( pGia1 == NULL )
     {
         Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_ReadAiger( pName2, 0, 0 );
+    pGia2 = Gia_AigerRead( pName2, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 6bf86523..11f81e0a 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -626,7 +626,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
         Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
             Gia_ManStop( pGia );
 
-        Gia_WriteAiger( pMiter, "m3.aig", 0, 0 );
+        Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
     }
     else 
     {
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index 088649ea..eab828db 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -1043,7 +1043,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
     {
         assert( Gia_ManPoNum(pPart) == 1 );
         assert( Gia_ManObjNum(pPart) == 2 );
-        vStr = Gia_WriteAigerIntoMemoryStr( pPart );
+        vStr = Gia_AigerWriteIntoMemoryStr( pPart );
         Gia_ManStop( pPart );
         if ( pvPiPerm )
             *pvPiPerm = Vec_IntAlloc( 0 );
@@ -1060,7 +1060,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
 //printf( "Internal: " );
 //Vec_IntPrint( vCis );
     // derive the AIGER string
-    vStr = Gia_WriteAigerIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
+    vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
     // cleanup
     Vec_IntFree( vCis );
     Vec_IntFree( vAnds );
@@ -1280,7 +1280,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
     // create AIG with two primary outputs (original and permuted)
     pPerm = Gia_ManDupPerm( p, vPiPerm );
     pDouble = Gia_ManDupAppendNew( p, pPerm );
-//Gia_WriteAiger( pDouble, "test.aig", 0, 0 );
+//Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
 
     // analyze the two-output miter
     pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 8e1bc7e2..1bc6398a 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -94,6 +94,10 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_WrdFreeP( &p->vTtMemory );
     Vec_PtrFreeP( &p->vTtInputs );
     Vec_IntFreeP( &p->vMapping );
+    Vec_IntFreeP( &p->vPacking );
+    Vec_FltFreeP( &p->vInArrs );
+    Vec_FltFreeP( &p->vOutReqs );
+    Gia_ManStopP( &p->pAigExtra );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
     ABC_FREE( p->pData2 );
@@ -161,10 +165,10 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p )
     {
         Gia_Man_t * pTemp;
         pTemp = Gia_ManDupFlopClass( p, 1 );
-        Gia_WriteAiger( pTemp, "dom1.aig", 0, 0 );
+        Gia_AigerWrite( pTemp, "dom1.aig", 0, 0 );
         Gia_ManStop( pTemp );
         pTemp = Gia_ManDupFlopClass( p, 2 );
-        Gia_WriteAiger( pTemp, "dom2.aig", 0, 0 );
+        Gia_AigerWrite( pTemp, "dom2.aig", 0, 0 );
         Gia_ManStop( pTemp );
     }
 }
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 49644fa8..c5cfd930 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
+    src/aig/gia/giaAigerExt.c \
     src/aig/gia/giaBidec.c \
     src/aig/gia/giaCCof.c \
     src/aig/gia/giaCex.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c65ee1bc..651b70ec 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12840,7 +12840,7 @@ int Abc_CommandRecStart2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 1, 0 );
+        pGia = Gia_AigerRead( FileName, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -13059,7 +13059,7 @@ int Abc_CommandRecDump2( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         // get the input file name
         FileName = pArgvNew[0];
-        Gia_WriteAiger( pGia, FileName, 0, 0 );
+        Gia_AigerWrite( pGia, FileName, 0, 0 );
     }
     return 0;
 
@@ -13188,7 +13188,7 @@ int Abc_CommandRecMerge2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 0, 0 );
+        pGia = Gia_AigerRead( FileName, 0, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -13299,7 +13299,7 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 1, 0 );
+        pGia = Gia_AigerRead( FileName, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -13531,7 +13531,7 @@ int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 0, "No structure in the library.\n" );
             return 1;
         }
-        Gia_WriteAiger( pGia, FileName, 0, 0 );
+        Gia_AigerWrite( pGia, FileName, 0, 0 );
     }
     return 0;
 
@@ -13605,7 +13605,7 @@ int Abc_CommandRecMerge3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 1, 0 );
+        pGia = Gia_AigerRead( FileName, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -23444,7 +23444,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
-    pAig = Gia_ReadAiger( FileName, fSkipStrash, 0 );
+    pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
     Abc_CommandUpdate9( pAbc, pAig );
     return 0;
 
@@ -23830,11 +23830,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fUnique )
     {
         Gia_Man_t * pGia = Gia_ManIsoCanonicize( pAbc->pGia, fVerbose );
-        Gia_WriteAigerSimple( pGia, pFileName );
+        Gia_AigerWriteSimple( pGia, pFileName );
         Gia_ManStop( pGia );
     }
     else
-        Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 );
+        Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
     return 0;
 
 usage:
@@ -25942,7 +25942,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_ReadAiger( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -26024,7 +26024,7 @@ int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_ReadAiger( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -26689,7 +26689,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
             Gia_ManStop( pAux );
         }
-        Gia_WriteAiger( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
+        Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
         Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
@@ -26702,7 +26702,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
             Gia_ManStop( pAux );
 
-            Gia_WriteAiger( pTemp, pFileName2, 0, 0 );
+            Gia_AigerWrite( pTemp, pFileName2, 0, 0 );
             Abc_Print( 1, "Reduced original network was written into file \"%s\".\n", pFileName2 );
             Gia_ManPrintStatsShort( pTemp );
             Gia_ManStop( pTemp );
@@ -26803,7 +26803,7 @@ int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
         Gia_ManStop( pAux );
 
-        Gia_WriteAiger( pTemp, pFileName, 0, 0 );
+        Gia_AigerWrite( pTemp, pFileName, 0, 0 );
         Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
@@ -27122,7 +27122,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_ReadAiger( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index b359f312..385ec520 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -581,7 +581,7 @@ void Abc_NtkRecFilter2(int nLimit)
     // remove dangling nodes and POs driven by constants
     newPGia = Abc_NtkDupWithoutDangling2(pGia);
     sprintf( fileName, "RecLib%d_Filtered%d.aig", p->nVars, nLimit);
-    Gia_WriteAiger( newPGia, fileName, 0, 0 );
+    Gia_AigerWrite( newPGia, fileName, 0, 0 );
     Abc_Print(1, "Library %s was written.", fileName);
     //Gia_ManHashStop(newPGia);
     Gia_ManStop(newPGia); 
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index 1544e1e2..41406ce4 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -223,7 +223,7 @@ void Abc_NtkTestPinGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose )
     Gia_Man_t * pGia;
     char * pFileName = "testpin.aig";
     pGia = Abc_NtkTestPinDeriveGia( pNtk, fWhiteBoxOnly, fVerbose );
-    Gia_WriteAiger( pGia, pFileName, 0, 0 );
+    Gia_AigerWrite( pGia, pFileName, 0, 0 );
     Gia_ManStop( pGia );
     printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n", 
         Abc_NtkName(pNtk), pFileName );
@@ -426,13 +426,13 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
         Gia_ManReverseClasses( pGia, 0 );
     }
     // write file
-    Gia_WriteAiger( pGia, pFileName, 0, 0 );
+    Gia_AigerWrite( pGia, pFileName, 0, 0 );
     // unnormalize choices
     if ( Gia_ManWithChoices(pGia) )
         Gia_ManReverseClasses( pGia, 1 );
 
     // read file
-    pGia2 = Gia_ReadAiger( pFileName, 1, 1 );
+    pGia2 = Gia_AigerRead( pFileName, 1, 1 );
 
     // normalize choices
     if ( Gia_ManWithChoices(pGia2) )
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index b89238fc..2aa95e85 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -391,7 +391,7 @@ Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken )
             fclose( pFile );
         }
         // derive AIG
-        pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0, 0 ); 
+        pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 ); 
     }
     Vec_StrFree( vStr );
     return pGia;
@@ -513,7 +513,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // create input file
-    Gia_WriteAiger( pAbc->pGia, pFileIn, 0, 0 );
+    Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 );
 
     // create command line
     vCommand = Vec_StrAlloc( 100 );
diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h
index b2009ec0..5fda0e59 100644
--- a/src/misc/tim/tim.h
+++ b/src/misc/tim/tim.h
@@ -122,8 +122,8 @@ extern float *         Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox );
 extern int             Tim_ManBoxCopy( Tim_Man_t * p, int iBox );
 extern void            Tim_ManBoxSetCopy( Tim_Man_t * p, int iBox, int iCopy );
 /*=== timDump.c ===========================================================*/
-extern Vec_Str_t *     Tim_ManSave( Tim_Man_t * p );
-extern Tim_Man_t *     Tim_ManLoad( Vec_Str_t * p );
+extern Vec_Str_t *     Tim_ManSave( Tim_Man_t * p, int fHieOnly );
+extern Tim_Man_t *     Tim_ManLoad( Vec_Str_t * p, int fHieOnly );
 /*=== timMan.c ===========================================================*/
 extern Tim_Man_t *     Tim_ManStart( int nCis, int nCos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fUnitDelay );
diff --git a/src/misc/tim/timDump.c b/src/misc/tim/timDump.c
index c7fb8861..1cda07b9 100644
--- a/src/misc/tim/timDump.c
+++ b/src/misc/tim/timDump.c
@@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
+Vec_Str_t * Tim_ManSave( Tim_Man_t * p, int fHieOnly )
 {
     Tim_Box_t * pBox;
     Tim_Obj_t * pObj;
@@ -71,6 +71,8 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
         Vec_StrPutI_ne( vStr, Tim_ManBoxDelayTableId(p, pBox->iBox) ); // can be -1 if delay table is not given
         Vec_StrPutI_ne( vStr, Tim_ManBoxCopy(p, pBox->iBox) );         // can be -1 if the copy is node defined
     }
+    if ( fHieOnly )
+        return vStr;
     // save the number of delay tables
     Vec_StrPutI_ne( vStr, Tim_ManDelayTableNum(p) );
     // save the delay tables
@@ -107,7 +109,7 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
+Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly )
 {
     Tim_Man_t * pMan;
     Tim_Obj_t * pObj;
@@ -149,6 +151,8 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
     curPo += nPos;
     assert( curPi == nCis );
     assert( curPo == nCos );
+    if ( fHieOnly )
+        return pMan;
     // create delay tables
     nTables = Vec_StrGetI_ne( p, &iStr );
     assert( pMan->vDelayTables == NULL );
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c
index 34c22da0..493047f7 100644
--- a/src/misc/util/utilBridge.c
+++ b/src/misc/util/utilBridge.c
@@ -41,11 +41,6 @@ ABC_NAMESPACE_IMPL_START
 #define BRIDGE_VALUE_0             2
 #define BRIDGE_VALUE_1             3
 
-extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
-
-extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos );
-extern void     Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -79,9 +74,9 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
 
     // write header
     vStr = Vec_StrAlloc( 1000 );
-    Gia_WriteAigerEncodeStr( vStr, Gia_ManPiNum(p) );
-    Gia_WriteAigerEncodeStr( vStr, Gia_ManRegNum(p) );
-    Gia_WriteAigerEncodeStr( vStr, Gia_ManAndNum(p) );
+    Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) );
+    Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) );
+    Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) );
 
     // write the nodes 
     Gia_ManForEachAnd( p, pObj, i )
@@ -89,24 +84,24 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
         uLit0 = Gia_ObjFanin0Copy( pObj );
         uLit1 = Gia_ObjFanin1Copy( pObj );
         assert( uLit0 != uLit1 );
-        Gia_WriteAigerEncodeStr( vStr, uLit0 << 1 );
-        Gia_WriteAigerEncodeStr( vStr, uLit1 );
+        Gia_AigerWriteUnsigned( vStr, uLit0 << 1 );
+        Gia_AigerWriteUnsigned( vStr, uLit1 );
     }
 
     // write latch drivers
     Gia_ManForEachRi( p, pObj, i )
     {
         uLit0 = Gia_ObjFanin0Copy( pObj );
-        Gia_WriteAigerEncodeStr( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
+        Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
     }
 
     // write PO drivers
-    Gia_WriteAigerEncodeStr( vStr, Gia_ManPoNum(p) );
+    Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) );
     Gia_ManForEachPo( p, pObj, i )
     {
         uLit0 = Gia_ObjFanin0Copy( pObj );
         // complement property output!!!
-        Gia_WriteAigerEncodeStr( vStr, Abc_LitNot(uLit0) );
+        Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) );
     }
     return vStr;
 }
@@ -209,20 +204,20 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
     Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
-    Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth
+    Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
 
-    Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete
-    Gia_WriteAigerEncodeStr( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
+    Gia_AigerWriteUnsigned( vStr, 1 ); // concrete
+    Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
     iBit = pCex->nRegs;
     for ( f = 0; f <= pCex->iFrame; f++ )
     {
-        Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs
+        Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs
         for ( i = 0; i < pCex->nPis; i++, iBit++ )
             Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
     }
     assert( iBit == pCex->nBits );
     Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
-    Gia_WriteAigerEncodeStr( vStr, pCex->nRegs ); // num of flops
+    Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops
     for ( i = 0; i < pCex->nRegs; i++ )
         Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
 //    RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
@@ -264,9 +259,9 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     int i, nInputs, nFlops, nGates, nProps;
     unsigned iFan0, iFan1;
 
-    nInputs = Gia_ReadAigerDecode( &pBuffer );
-    nFlops  = Gia_ReadAigerDecode( &pBuffer );
-    nGates  = Gia_ReadAigerDecode( &pBuffer );
+    nInputs = Gia_AigerReadUnsigned( &pBuffer );
+    nFlops  = Gia_AigerReadUnsigned( &pBuffer );
+    nGates  = Gia_AigerReadUnsigned( &pBuffer );
 
     vLits = Vec_IntAlloc( 1000 );
     Vec_IntPush( vLits, -999 );
@@ -289,8 +284,8 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
         Gia_ManHashAlloc( p );
     for ( i = 0; i < nGates; i++ )
     {
-        iFan0 = Gia_ReadAigerDecode( &pBuffer );
-        iFan1 = Gia_ReadAigerDecode( &pBuffer );
+        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
+        iFan1 = Gia_AigerReadUnsigned( &pBuffer );
         assert( !(iFan0 & 1) );
         iFan0 >>= 1;
         iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
@@ -308,14 +303,14 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     pBufferPivot = pBuffer;
     // scroll through flops
     for ( i = 0; i < nFlops; i++ )
-        Gia_ReadAigerDecode( &pBuffer );
+        Gia_AigerReadUnsigned( &pBuffer );
 
     // create POs
-    nProps = Gia_ReadAigerDecode( &pBuffer );
+    nProps = Gia_AigerReadUnsigned( &pBuffer );
     assert( nProps == 1 );
     for ( i = 0; i < nProps; i++ )
     {
-        iFan0 = Gia_ReadAigerDecode( &pBuffer );
+        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
         iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
         // complement property output!!!
         Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
@@ -328,7 +323,7 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     vInits = Vec_IntAlloc( nFlops );
     for ( i = 0; i < nFlops; i++ )
     {
-        iFan0 = Gia_ReadAigerDecode( &pBuffer );
+        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
         assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
         Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
         iFan0 >>= 2;
@@ -487,7 +482,7 @@ void Gia_ManFromBridgeTest( char * pFileName )
     fclose ( pFile );
 
     Gia_ManPrintStats( p, 0, 0, 0 );
-    Gia_WriteAiger( p, "temp.aig", 0, 0 );
+    Gia_AigerWrite( p, "temp.aig", 0, 0 );
 
     Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
     Gia_ManStop( p );
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 0ed9f450..3e933fa0 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1451,7 +1451,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         // dump abstraction map
         Vec_IntFreeP( &p->pGia->vGateClasses );
         p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
+        Gia_AigerWrite( p->pGia, pFileName, 0, 0 );
     }
     else if ( p->pPars->fDumpVabs )
     {
@@ -1464,7 +1464,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         vGateClasses = Ga2_ManAbsTranslate( p );
         pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
         Gia_ManCleanValue( p->pGia );
-        Gia_WriteAiger( pAbs, pFileName, 0, 0 );
+        Gia_AigerWrite( pAbs, pFileName, 0, 0 );
         Gia_ManStop( pAbs );
         Vec_IntFreeP( &vGateClasses );
     }
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 0a0315c2..343ec935 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -1620,7 +1620,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
     pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
     Vec_IntFreeP( &vGateClasses );
     // write into file
-    Gia_WriteAiger( pAbs, pFileName, 0, 0 );
+    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
     Gia_ManStop( pAbs );
 }
 
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index b217ef13..d94a93e5 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -1440,7 +1440,7 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
     pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
     Vec_IntFreeP( &p->pGia->vGateClasses );
     // send it out
-    Gia_WriteAiger( pAbs, pFileName, 0, 0 );
+    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
     Gia_ManStop( pAbs );
 }
 
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 30c930a0..72c3e7db 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -263,7 +263,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     {
         ABC_FREE( pNew->pReprs );
         ABC_FREE( pNew->pNexts );
-        Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
+        Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
         Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
     }
     if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c45bd974..40d5fba6 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -398,7 +398,7 @@ p->timeSim += clock() - clk;
         }
         pSrm = Cec_ManFraSpecReduction( p ); 
 
-//        Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
+//        Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
 
         if ( pPars->fVeryVerbose )
             Gia_ManPrintStats( pSrm, 0, 0, 0 );
@@ -481,7 +481,7 @@ p->timeSat += clock() - clk;
                     Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
                 if ( fOutputResult )
                 {
-                    Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 );
+                    Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
                     Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
                 }
             }
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index f3a84d3a..ed5f9a8e 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1124,7 +1124,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         pNew = Gia_ManCorrReduce( pAig );
         pNew = Gia_ManSeqCleanup( pTemp = pNew );
         Gia_ManStop( pTemp );
-        //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
+        //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
     }
     // report the results
     if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index da60de1d..43bfa99c 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         }
 
         // write equivalence classes
-        Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
+        Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
         // reduce the model
         pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
             Gia_ManStop( pAux );
-            Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
 //            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
 //          Gia_ManPrintStatsShort( pReduce );
             Gia_ManStop( pReduce );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index 41053cf0..d560c37a 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -710,7 +710,7 @@ clk2 = clock();
         if ( status == -1 )
         {
             Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
-            Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 );
+            Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
             Gia_ManStop( pTemp );
             Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
         }
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 6fc991a8..6ab88cbe 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -309,7 +309,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
         {
             pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
             sprintf( Buffer, "part%03d.aig", i );
-            Gia_WriteAiger( pTemp, Buffer, 0, 0 );
+            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 );
diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
index 076d744c..7301c3e4 100644
--- a/src/sat/bmc/bmcCexMin2.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -334,7 +334,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
         printf( "%3d : ", iFrameStart );
         Gia_ManPrintStats( pNew, 0, 0, 0 );
         if ( fVerbose )
-            Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
+            Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
         Gia_ManStop( pNew );
     }
     else // CEX min
@@ -345,7 +345,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
             printf( "%3d : ", f );
             Gia_ManPrintStats( pNew, 0, 0, 0 );
             if ( fVerbose )
-                Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
+                Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
             Gia_ManStop( pNew );
         }
     }
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 87d88fd0..bbf7d1ad 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
     clock_t clk = clock();
     pNew = Bmc_CexPerformUnrolling( p, pCex );
     Gia_ManPrintStats( pNew, 0, 0, 0 );
-    Gia_WriteAiger( pNew, "unroll.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
 //Bmc_CexDumpAogStats( pNew, clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unroll.aig\".\n" );
@@ -285,7 +285,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
     clock_t clk = clock();
     pNew = Bmc_CexBuildNetwork( p, pCex );
     Gia_ManPrintStats( pNew, 0, 0, 0 );
-    Gia_WriteAiger( pNew, "unate.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
 //Bmc_CexDumpAogStats( pNew, clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unate.aig\".\n" );