Version abc80121

6 files changed, 250 insertions, 108 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0a27ee15..396cf598 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6384,7 +6384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
     extern void Abc_NtkDarTestBlif( char * pFileName );
 
@@ -6543,6 +6543,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for logic circuits.\n" );
         return 0;
     }
+*/
 
 //    pNtkRes = Abc_NtkDar( pNtk );
 //    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
@@ -6555,7 +6556,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
+
 
 //    Abc_NtkDarHaigRecord( pNtk );
 //    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
@@ -10363,8 +10364,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // disable cut-expansion if edge-based heuristics are selected
-    if ( pPars->fEdge )
-        pPars->fExpRed = 0;
+//    if ( pPars->fEdge )
+//        pPars->fExpRed = 0;
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
diff --git a/src/base/io/io.c b/src/base/io/io.c
index ed314fcd..fe88a285 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1174,17 +1174,22 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int fWriteSymbols;
+    int fCompact;
     int c;
 
-    fWriteSymbols = 1;
+    fCompact      = 1;
+    fWriteSymbols = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF )
     {
         switch ( c )
         {
             case 's':
                 fWriteSymbols ^= 1;
                 break;
+            case 'c':
+                fCompact ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1196,23 +1201,19 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    if ( fWriteSymbols )
-        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
-    else
+    if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
     {
-        if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
-        {
-            fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
-            return 1;
-        }
-        Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 );
+        fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
+        return 1;
     }
+    Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
     fprintf( pAbc->Err, "\t         write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
     fprintf( pAbc->Err, "\t-s     : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-c     : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .aig)\n" );
     return 1;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 45762b77..126de332 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -87,7 +87,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fCheck );
 /*=== abcReadVerilog.c ========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
-extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols );
+extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
 /*=== abcWriteBaf.c ===========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 273b2d5a..4820bced 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -25,14 +25,68 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-unsigned Io_ReadAigerDecode( char ** ppPos );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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 Io_ReadAigerDecode( char ** ppPos )
+{
+    unsigned x = 0, i = 0;
+    unsigned char ch;
+
+//    while ((ch = getnoneofch (file)) & 0x80)
+    while ((ch = *(*ppPos)++) & 0x80)
+        x |= (ch & 0x7f) << (7 * i++);
+
+    return x | (ch << (7 * i));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Decodes the encoded array of literals.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
+{
+    Vec_Int_t * vLits;
+    int Lit, LitPrev, Diff, i;
+    vLits = Vec_IntAlloc( nEntries );
+    LitPrev = Io_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 = Io_ReadAigerDecode( ppPos );
+        Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
+        Lit  = Diff + LitPrev;
+        Vec_IntPush( vLits, Lit );
+        LitPrev = Lit;
+    }
+    return vLits;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the AIG in the binary AIGER format.]
 
   Description []
@@ -47,6 +101,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     ProgressBar * pProgress;
     FILE * pFile;
     Vec_Ptr_t * vNodes, * vTerms;
+    Vec_Int_t * vLits = NULL;
     Abc_Obj_t * pObj, * pNode0, * pNode1;
     Abc_Ntk_t * pNtkNew;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
@@ -61,7 +116,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     fclose( pFile );
 
     // check if the input file format is correct
-    if ( strncmp(pContents, "aig", 3) != 0 )
+    if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
     {
         fprintf( stdout, "Wrong input file format.\n" );
         return NULL;
@@ -125,13 +180,20 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
 //        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
     } 
     
-    // remember the beginning of latch/PO literals
-    pDrivers = pCur;
 
-    // scroll to the beginning of the binary data
-    for ( i = 0; i < nLatches + nOutputs; )
-        if ( *pCur++ == '\n' )
-            i++;
+    if ( pContents[3] == ' ' ) // standard AIGER
+    {
+        // remember the beginning of latch/PO literals
+        pDrivers = pCur;
+        // scroll to the beginning of the binary data
+        for ( i = 0; i < nLatches + nOutputs; )
+            if ( *pCur++ == '\n' )
+                i++;
+    }
+    else // modified AIGER
+    {
+        vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
+    }
 
     // create the AND gates
     pProgress = Extra_ProgressBarStart( stdout, nAnds );
@@ -154,21 +216,39 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
 
     // read the latch driver literals
     pCur = pDrivers;
-    Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+    if ( pContents[3] == ' ' ) // standard AIGER
     {
-        uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-        Abc_ObjAddFanin( pObj, pNode0 );
-
-//        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
-
+        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+        {
+            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
+            pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Abc_ObjAddFanin( pObj, pNode0 );
+        }
+        // read the PO driver literals
+        Abc_NtkForEachPo( pNtkNew, pObj, i )
+        {
+            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
+            pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Abc_ObjAddFanin( pObj, pNode0 );
+        }
     }
-    // read the PO driver literals
-    Abc_NtkForEachPo( pNtkNew, pObj, i )
+    else
     {
-        uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-        Abc_ObjAddFanin( pObj, pNode0 );
+        // read the latch driver literals
+        Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
+        {
+            uLit0 = Vec_IntEntry( vLits, i );
+            pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Abc_ObjAddFanin( pObj, pNode0 );
+        }
+        // read the PO driver literals
+        Abc_NtkForEachPo( pNtkNew, pObj, i )
+        {
+            uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
+            pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Abc_ObjAddFanin( pObj, pNode0 );
+        }
+        Vec_IntFree( vLits );
     }
  
     // read the names if present
@@ -278,30 +358,6 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
 }
 
 
-/**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 Io_ReadAigerDecode( char ** ppPos )
-{
-    unsigned x = 0, i = 0;
-    unsigned char ch;
-
-//    while ((ch = getnoneofch (file)) & 0x80)
-    while ((ch = *(*ppPos)++) & 0x80)
-        x |= (ch & 0x7f) << (7 * i++);
-
-    return x | (ch << (7 * i));
-}
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 94ec4316..4f9f2e9f 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( FileType == IO_FILE_AIGER )
-            Io_WriteAiger( pNtk, pFileName, 1 );
+            Io_WriteAiger( pNtk, pFileName, 1, 0 );
         else // if ( FileType == IO_FILE_BAF )
             Io_WriteBaf( pNtk, pFileName );
         return;
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index ff34b177..758e5335 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -129,14 +129,116 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (V
 static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)pObj->pCopy;  }
 static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (void *)Num;     }
 
-int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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 Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
+{
+    unsigned char ch;
+    while (x & ~0x7f)
+    {
+        ch = (x & 0x7f) | 0x80;
+//        putc (ch, file);
+        pBuffer[Pos++] = ch;
+        x >>= 7;
+    }
+    ch = x;
+//    putc (ch, file);
+    pBuffer[Pos++] = ch;
+    return Pos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the array of literals to be written.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vLits;
+    Abc_Obj_t * pObj, * pDriver;
+    int i;
+    vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+    }
+    return vLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the binary encoded array of literals.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Io_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 = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev ); 
+    Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
+    {
+        Diff = Lit - LitPrev;
+        Diff = (Lit < LitPrev)? -Diff : Diff;
+        Diff = (Diff << 1) | (int)(Lit < LitPrev);
+        Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff );
+        LitPrev = Lit;
+        if ( Pos + 10 > vBinary->nCap )
+            Vec_StrGrow( vBinary, vBinary->nCap+1 );
+    }
+    vBinary->nSize = Pos;
+/*
+    // verify
+    {
+        extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
+        char * pPos = Vec_StrArray( vBinary );
+        Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
+        for ( i = 0; i < Vec_IntSize(vLits); i++ )
+        {
+            int Entry1 = Vec_IntEntry(vLits,i);
+            int Entry2 = Vec_IntEntry(vTemp,i);
+            assert( Entry1 == Entry2 );
+        }
+    }
+*/
+    return vBinary;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the AIG in the binary AIGER format.]
 
   Description []
@@ -146,7 +248,7 @@ int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
 {
     ProgressBar * pProgress;
     FILE * pFile;
@@ -179,7 +281,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
         Io_ObjSetAigerNum( pObj, nNodes++ );
 
     // write the header "M I L O A" where M = I + L + A
-    fprintf( pFile, "aig %u %u %u %u %u\n", 
+    fprintf( pFile, "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),
@@ -190,24 +293,34 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
     // 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
 
-    // write latch drivers
-    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+    if ( !fCompact ) 
     {
-        pDriver = Abc_ObjFanin0(pObj);
-        fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+        // write latch drivers
+        Abc_NtkForEachLatchInput( pNtk, pObj, i )
+        {
+            pDriver = Abc_ObjFanin0(pObj);
+            fprintf( pFile, "%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);
+            fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+        }
     }
-
-    // write PO drivers
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    else
     {
-        pDriver = Abc_ObjFanin0(pObj);
-        fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+        Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
+        Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
+        fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
+        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( char, nBufferSize );
+    pBuffer = ALLOC( unsigned char, nBufferSize );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
@@ -216,8 +329,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
         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, uLit  - uLit1 );
-        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+        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" );
@@ -255,35 +368,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
     fclose( pFile );
 }
 
-/**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 Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
-{
-    unsigned char ch;
-    while (x & ~0x7f)
-    {
-        ch = (x & 0x7f) | 0x80;
-//        putc (ch, file);
-        pBuffer[Pos++] = ch;
-        x >>= 7;
-    }
-    ch = x;
-//    putc (ch, file);
-    pBuffer[Pos++] = ch;
-    return Pos;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////