Version abc80701

2 files changed, 354 insertions, 12 deletions

diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 3739205d..9ecc00fd 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -20,6 +20,7 @@
 ***********************************************************************/
 
 #include "ioAbc.h"
+#include <bzlib.h>
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -85,6 +86,92 @@ Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
     return vLits;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the file into a character buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+typedef struct buflist {
+  char buf[1<<20];
+  int nBuf;
+  struct buflist * next;
+} buflist;
+
+static char * Ioa_ReadLoadFileBz2Aig( char * pFileName )
+{
+    FILE    * pFile;
+    int       nFileSize = 0;
+    char    * pContents;
+    BZFILE  * b;
+    int       bzError;
+    struct buflist * pNext;
+    buflist * bufHead = NULL, * buf = NULL;
+
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Ioa_ReadLoadFileBz2(): The file is unavailable (absent or open).\n" );
+        return NULL;
+    }
+    b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0);
+    if (bzError != BZ_OK) {
+        printf( "Ioa_ReadLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError );
+        return NULL;
+    }
+    do {
+        if (!bufHead)
+            buf = bufHead = ALLOC( buflist, 1 );
+        else
+            buf = buf->next = ALLOC( buflist, 1 );
+        nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20);
+        buf->next = NULL;
+    } while (bzError == BZ_OK);
+    if (bzError == BZ_STREAM_END) {
+        // we're okay
+        char * p;
+        int nBytes = 0;
+        BZ2_bzReadClose(&bzError,b);
+        p = pContents = ALLOC( char, nFileSize + 10 );
+        buf = bufHead;
+        do {
+            memcpy(p+nBytes,buf->buf,buf->nBuf);
+            nBytes += buf->nBuf;
+//        } while((buf = buf->next));
+            pNext = buf->next;
+            free( buf );
+        } while((buf = pNext));
+    } else if (bzError == BZ_DATA_ERROR_MAGIC) {
+        // not a BZIP2 file
+        BZ2_bzReadClose(&bzError,b);
+        fseek( pFile, 0, SEEK_END );
+        nFileSize = ftell( pFile );
+        if ( nFileSize == 0 )
+        {
+            printf( "Ioa_ReadLoadFileBz2(): The file is empty.\n" );
+            return NULL;
+        }
+        pContents = ALLOC( char, nFileSize + 10 );
+        rewind( pFile );
+        fread( pContents, nFileSize, 1, pFile );
+    } else { 
+        // Some other error.
+        printf( "Ioa_ReadLoadFileBz2(): Unable to read the compressed BLIF.\n" );
+        return NULL;
+    }
+    fclose( pFile );
+    // finish off the file with the spare .end line
+    // some benchmarks suddenly break off without this line
+    strcpy( pContents + nFileSize, "\n.end\n" );
+    return pContents;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Reads the AIG in the binary AIGER format.]
@@ -109,11 +196,18 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     unsigned uLit0, uLit1, uLit;
 
     // read the file into the buffer
-    nFileSize = Extra_FileSize( pFileName );
-    pFile = fopen( pFileName, "rb" );
-    pContents = ALLOC( char, nFileSize );
-    fread( pContents, nFileSize, 1, pFile );
-    fclose( pFile );
+    if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
+        pContents = Ioa_ReadLoadFileBz2Aig( pFileName );
+    else
+    {
+//        pContents = Ioa_ReadLoadFile( pFileName );
+        nFileSize = Extra_FileSize( pFileName );
+        pFile = fopen( pFileName, "rb" );
+        pContents = ALLOC( char, nFileSize );
+        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') )
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index fb107e77..9e5ee8b4 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -21,6 +21,13 @@
 
 #include "ioAbc.h"
 
+#include <bzlib.h>
+#include <stdarg.h>
+
+#ifdef _WIN32
+#define vsnprintf _vsnprintf
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -248,7 +255,7 @@ Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
+void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
 {
     ProgressBar * pProgress;
     FILE * pFile;
@@ -258,6 +265,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     unsigned uLit0, uLit1, uLit;
 
     assert( Abc_NtkIsStrash(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( !Abc_LatchIsInit0(pObj) )
+        {
+            fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
+            return;
+        }
+
     // start the output stream
     pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
@@ -265,12 +279,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
         fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        if ( !Abc_LatchIsInit0(pObj) )
-        {
-            fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
-            return;
-        }
 
     // set the node numbers to be used in the output file
     nNodes = 0;
@@ -368,6 +376,246 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     fclose( pFile );
 }
 
+ 
+/**Function*************************************************************
+
+  Synopsis    [Procedure to write data into BZ2 file.]
+
+  Description [Based on the vsnprintf() man page.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+typedef struct bz2file {
+  FILE   * f;
+  BZFILE * b;
+  char   * buf;
+  int      nBytes;
+  int      nBytesMax;
+} bz2file;
+
+int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
+    if (b->b) {
+        char * newBuf;
+        int bzError;
+        va_list ap;
+        while (1) {
+            va_start(ap,fmt);
+            b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap);
+            va_end(ap);
+            if (b->nBytes > -1 && b->nBytes < b->nBytesMax)
+                break;
+            if (b->nBytes > -1)
+                b->nBytesMax = b->nBytes + 1;
+            else
+                b->nBytesMax *= 2;
+            if ((newBuf = REALLOC( char,b->buf,b->nBytesMax )) == NULL)
+                return -1;
+            else
+                b->buf = newBuf;
+        }
+        BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes );
+        if (bzError == BZ_IO_ERROR) {
+            fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" );
+            return -1;
+        }
+        return b->nBytes;
+    } else {
+        int n;
+        va_list ap;
+        va_start(ap,fmt);
+        n = vfprintf( b->f, fmt, ap);
+        va_end(ap);
+        return n;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
+{
+    ProgressBar * pProgress;
+//    FILE * pFile;
+    Abc_Obj_t * pObj, * pDriver;
+    int i, nNodes, Pos, nBufferSize, bzError;
+    unsigned char * pBuffer;
+    unsigned uLit0, uLit1, uLit;
+    bz2file b;
+
+    // check that the network is valid
+    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( !Abc_LatchIsInit0(pObj) )
+        {
+            fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
+            return;
+        }
+
+    memset(&b,0,sizeof(b));
+    b.nBytesMax = (1<<12);
+    b.buf = ALLOC( char,b.nBytesMax );
+
+    // start the output stream
+    b.f = fopen( pFileName, "wb" ); 
+    if ( b.f == NULL )
+    {
+        fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
+        FREE(b.buf);
+        return;
+    }
+    if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) {
+        b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 );
+        if ( bzError != BZ_OK ) {
+            BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
+            fprintf( stdout, "Ioa_WriteBlif(): Cannot start compressed stream.\n" );
+            fclose( b.f );
+            FREE(b.buf);
+            return;
+        }
+    }
+
+    // set the node numbers to be used in the output file
+    nNodes = 0;
+    Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Io_ObjSetAigerNum( pObj, nNodes++ );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Io_ObjSetAigerNum( pObj, nNodes++ );
+
+    // write the header "M I L O A" where M = I + L + A
+    fprintfBz2Aig( &b, "aig%s %u %u %u %u %u\n", 
+        fCompact? "2" : "",
+        Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
+        Abc_NtkPiNum(pNtk),
+        Abc_NtkLatchNum(pNtk),
+        Abc_NtkPoNum(pNtk),
+        Abc_NtkNodeNum(pNtk) );
+
+    // if the driver node is a constant, we need to complement the literal below
+    // because, in the AIGER format, literal 0/1 is represented as number 0/1
+    // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
+
+    if ( !fCompact ) 
+    {
+        // write latch drivers
+        Abc_NtkForEachLatchInput( pNtk, pObj, i )
+        {
+            pDriver = Abc_ObjFanin0(pObj);
+            fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+        }
+        // write PO drivers
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            pDriver = Abc_ObjFanin0(pObj);
+            fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+        }
+    }
+    else
+    {
+        Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
+        Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
+        if ( !b.b )
+            fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f );
+        else
+        {
+            BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) );
+            if (bzError == BZ_IO_ERROR) {
+                fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
+                fclose( b.f );
+                FREE(b.buf);
+                return;
+            }
+        }
+        Vec_StrFree( vBinary );
+        Vec_IntFree( vLits );
+    }
+
+    // write the nodes into the buffer
+    Pos = 0;
+    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
+    pBuffer = ALLOC( unsigned char, nBufferSize );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        uLit  = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
+        uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
+        uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
+        assert( uLit0 < uLit1 );
+        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit  - uLit1) );
+        Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
+        if ( Pos > nBufferSize - 10 )
+        {
+            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
+            fclose( b.f );
+            FREE(b.buf);
+            return;
+        }
+    }
+    assert( Pos < nBufferSize );
+    Extra_ProgressBarStop( pProgress );
+
+    // write the buffer
+    if ( !b.b )
+        fwrite( pBuffer, 1, Pos, b.f );
+    else
+    {
+        BZ2_bzWrite( &bzError, b.b, pBuffer, Pos );
+        if (bzError == BZ_IO_ERROR) {
+            fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
+            fclose( b.f );
+            FREE(b.buf);
+            return;
+        }
+    }
+    free( pBuffer );
+
+    // write the symbol table
+    if ( fWriteSymbols )
+    {
+        // write PIs
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) );
+        // write latches
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+        // write POs
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) );
+    }
+
+    // write the comment
+    fprintfBz2Aig( &b, "c\n" );
+    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
+        fprintfBz2Aig( &b, ".model %s\n", pNtk->pName );
+    fprintfBz2Aig( &b, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
+    fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+
+    // close the file
+    if (b.b) {
+        BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL );
+        if (bzError == BZ_IO_ERROR) {
+            fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" );
+            fclose( b.f );
+            FREE(b.buf);
+            return;
+        }
+    }
+    fclose( b.f );
+    FREE(b.buf);
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////