Version abc80121

18 files changed, 687 insertions, 377 deletions

diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 4ccb48e3..c6bdc20e 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -276,7 +276,7 @@ PRT( "Time", clock() - clkTotal );
         printf( "Networks are UNDECIDED.   " );
 PRT( "Time", clock() - clkTotal );
         sprintf( pFileName, "sm%03d.aig", Counter++ );
-        Ioa_WriteAiger( pNew, pFileName, 0 );
+        Ioa_WriteAiger( pNew, pFileName, 0, 0 );
         printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
     }
     Aig_ManStop( pNew );
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index 3458d12e..e697a729 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -36,7 +36,7 @@ extern "C" {
 #include <time.h>
 
 #include "vec.h"
-#include "bar.h"
+//#include "bar.h"
 #include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -62,7 +62,7 @@ extern "C" {
 /*=== ioaReadAig.c ========================================================*/
 extern Aig_Man_t *    Ioa_ReadAiger( char * pFileName, int fCheck );
 /*=== ioaWriteAig.c =======================================================*/
-extern void           Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols );
+extern void           Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
 /*=== ioaUtil.c =======================================================*/
 extern int            Ioa_FileSize( char * pFileName );
 extern char *         Ioa_FileNameGeneric( char * FileName );
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index 937e446f..498cdd30 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -25,14 +25,69 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-unsigned Ioa_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 Ioa_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 * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
+{
+    Vec_Int_t * vLits;
+    int Lit, LitPrev, Diff, i;
+    vLits = Vec_IntAlloc( nEntries );
+    LitPrev = Ioa_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 = Ioa_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 []
@@ -44,8 +99,9 @@ unsigned Ioa_ReadAigerDecode( char ** ppPos );
 ***********************************************************************/
 Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
 {
-    Bar_Progress_t * pProgress;
+//    Bar_Progress_t * pProgress;
     FILE * pFile;
+    Vec_Int_t * vLits = NULL;
     Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
     Aig_Obj_t * pObj, * pNode0, * pNode1;
     Aig_Man_t * pManNew;
@@ -61,7 +117,7 @@ Aig_Man_t * Ioa_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;
@@ -127,21 +183,27 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
 //        Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
 //        printf( "Creating latch %s with input %d and output %d.\n", Aig_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
+    {
+        // scroll to the beginning of the binary data
+        for ( i = 0; i < nLatches + nOutputs; )
+            if ( *pCur++ == '\n' )
+                i++;
+    }
+    else // modified AIGER
+    {
+        vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
+    }
 
     // create the AND gates
-    pProgress = Bar_ProgressStart( stdout, nAnds );
+//    pProgress = Bar_ProgressStart( stdout, nAnds );
     for ( i = 0; i < nAnds; i++ )
     {
-        Bar_ProgressUpdate( pProgress, i, NULL );
+//        Bar_ProgressUpdate( pProgress, i, NULL );
         uLit = ((i + 1 + nInputs + nLatches) << 1);
         uLit1 = uLit  - Ioa_ReadAigerDecode( &pCur );
         uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
@@ -151,33 +213,50 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
         assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
         Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
     }
-    Bar_ProgressStop( pProgress );
+//    Bar_ProgressStop( pProgress );
 
     // remember the place where symbols begin
     pSymbols = pCur;
 
     // read the latch driver literals
     vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
-    pCur = pDrivers;
-//    Aig_ManForEachLatchInput( pManNew, pObj, i )
-    for ( i = 0; i < nLatches; i++ )
+    if ( pContents[3] == ' ' ) // standard AIGER
     {
-        uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-//        Aig_ObjAddFanin( pObj, pNode0 );
-        Vec_PtrPush( vDrivers, pNode0 );
+        pCur = pDrivers;
+        for ( i = 0; i < nLatches; i++ )
+        {
+            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
+            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Vec_PtrPush( vDrivers, pNode0 );
+        }
+        // read the PO driver literals
+        for ( i = 0; i < nOutputs; i++ )
+        {
+            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
+            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Vec_PtrPush( vDrivers, pNode0 );
+        }
+
     }
-    // read the PO driver literals
-//    Aig_ManForEachPo( pManNew, pObj, i )
-    for ( i = 0; i < nOutputs; i++ )
+    else
     {
-        uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
-//        Aig_ObjAddFanin( pObj, pNode0 );
-        Vec_PtrPush( vDrivers, pNode0 );
+        // read the latch driver literals
+        for ( i = 0; i < nLatches; i++ )
+        {
+            uLit0 = Vec_IntEntry( vLits, i );
+            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Vec_PtrPush( vDrivers, pNode0 );
+        }
+        // read the PO driver literals
+        for ( i = 0; i < nOutputs; i++ )
+        {
+            uLit0 = Vec_IntEntry( vLits, i+nLatches );
+            pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+            Vec_PtrPush( vDrivers, pNode0 );
+        }
+        Vec_IntFree( vLits );
     }
 
-
     // create the POs
     for ( i = 0; i < nOutputs; i++ )
         Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
@@ -280,31 +359,6 @@ Aig_Man_t * Ioa_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 Ioa_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/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index a6c23fd4..166dca4b 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -125,11 +125,9 @@ Binary Format Definition
 
 */
 
-static unsigned Ioa_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;    }
-static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj )                   { return (unsigned)pObj->pData;  }
-static void     Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num )  { pObj->pData = (void *)Num;     }
-
-int      Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+static int      Ioa_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;  }
+static int      Ioa_ObjAigerNum( Aig_Obj_t * pObj )                   { return pObj->iData;          }
+static void     Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num )  { pObj->iData = Num;           }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -137,6 +135,111 @@ int      Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
 
 /**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 Ioa_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 * Ioa_WriteAigerLiterals( Aig_Man_t * pMan )
+{
+    Vec_Int_t * vLits;
+    Aig_Obj_t * pObj, * pDriver;
+    int i;
+    vLits = Vec_IntAlloc( Aig_ManPoNum(pMan) );
+    Aig_ManForEachLiSeq( pMan, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
+    }
+    Aig_ManForEachPoSeq( pMan, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
+    }
+    return vLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the binary encoded array of literals.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Ioa_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 = Ioa_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 = Ioa_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 * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries );
+        char * pPos = Vec_StrArray( vBinary );
+        Vec_Int_t * vTemp = Ioa_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 );
+        }
+        Vec_IntFree( vTemp );
+    }
+*/
+    return vBinary;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the AIG in the binary AIGER format.]
 
   Description []
@@ -146,9 +249,9 @@ int      Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
   SeeAlso     []
 
 ***********************************************************************/
-void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
+void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
 {
-    Bar_Progress_t * pProgress;
+//    Bar_Progress_t * pProgress;
     FILE * pFile;
     Aig_Obj_t * pObj, * pDriver;
     int i, nNodes, Pos, nBufferSize;
@@ -180,7 +283,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
         Ioa_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" : "",
         Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), 
         Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
         Aig_ManRegNum(pMan),
@@ -191,34 +295,45 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, 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
-    Aig_ManForEachLiSeq( pMan, pObj, i )
+    if ( !fCompact ) 
     {
-        pDriver = Aig_ObjFanin0(pObj);
-        fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
-    }
+        // write latch drivers
+        Aig_ManForEachLiSeq( pMan, pObj, i )
+        {
+            pDriver = Aig_ObjFanin0(pObj);
+            fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
+        }
 
-    // write PO drivers
-    Aig_ManForEachPoSeq( pMan, pObj, i )
+        // write PO drivers
+        Aig_ManForEachPoSeq( pMan, pObj, i )
+        {
+            pDriver = Aig_ObjFanin0(pObj);
+            fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
+        }
+    }
+    else
     {
-        pDriver = Aig_ObjFanin0(pObj);
-        fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
+        Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
+        Vec_Str_t * vBinary = Ioa_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 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
-    pBuffer = ALLOC( char, nBufferSize );
-    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
+    pBuffer = ALLOC( unsigned char, nBufferSize );
+//    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
     Aig_ManForEachNode( pMan, pObj, i )
     {
-        Bar_ProgressUpdate( pProgress, i, NULL );
+//        Bar_ProgressUpdate( pProgress, i, NULL );
         uLit  = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
         uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
         uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
         assert( uLit0 < uLit1 );
-        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
-        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit  - uLit1) );
+        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
         if ( Pos > nBufferSize - 10 )
         {
             printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
@@ -227,7 +342,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
         }
     }
     assert( Pos < nBufferSize );
-    Bar_ProgressStop( pProgress );
+//    Bar_ProgressStop( pProgress );
 
     // write the buffer
     fwrite( pBuffer, 1, Pos, pFile );
@@ -251,40 +366,11 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
     fprintf( pFile, "c\n" );
     if ( pMan->pName )
         fprintf( pFile, ".model %s\n", pMan->pName );
-    fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
+    fprintf( pFile, "This file was produced by the AIG package on %s\n", Ioa_TimeStamp() );
     fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
     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 Ioa_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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 364f7d20..1bd21089 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -45,7 +45,7 @@ struct Tim_Man_t_
 {
     Vec_Ptr_t *      vBoxes;         // the timing boxes
     Vec_Ptr_t *      vDelayTables;   // pointers to the delay tables
-    Mem_Flex_t *   pMemObj;        // memory manager for boxes
+    Mem_Flex_t *     pMemObj;        // memory manager for boxes
     int              nTravIds;       // traversal ID of the manager
     int              nPis;           // the number of PIs
     int              nPos;           // the number of POs
@@ -74,13 +74,27 @@ struct Tim_Obj_t_
     float            timeReq;        // required time of the object
 };
 
+static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i )                           { assert( i < p->nPis ); return p->pPis + i;    }
+static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i )                           { assert( i < p->nPos ); return p->pPos + i;    }
+
+static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i )                        { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); }
+static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i )                        { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); }
+
+static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { return p->pPos + pBox->Inouts[i];               }
+static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { return p->pPis + pBox->Inouts[pBox->nInputs+i]; }
+
+#define Tim_ManBoxForEachInput( p, pBox, pObj, i )                                  \
+    for ( i = 0; (i < (pBox)->nInputs) && ((pObj) = Tim_ManBoxInput(p, pBox, i)); i++ )
+#define Tim_ManBoxForEachOutput( p, pBox, pObj, i )                                 \
+    for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the network manager.]
+  Synopsis    [Starts the timing manager.]
 
   Description []
                
@@ -113,7 +127,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
 
 /**Function*************************************************************
 
-  Synopsis    [Stops the network manager.]
+  Synopsis    [Stops the timing manager.]
 
   Description []
                
@@ -141,7 +155,7 @@ void Tim_ManStop( Tim_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Increments the trav ID of the manager.]
+  Synopsis    [Sets the vector of timing tables associated with the manager.]
 
   Description []
                
@@ -252,7 +266,7 @@ void Tim_ManIncrementTravId( Tim_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the new timing box.]
+  Synopsis    [Initializes arrival time of the PI.]
 
   Description []
                
@@ -269,7 +283,7 @@ void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the new timing box.]
+  Synopsis    [Initializes required time of the PO.]
 
   Description []
                
@@ -286,7 +300,7 @@ void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the new timing box.]
+  Synopsis    [Updates arrival time of the PO.]
 
   Description []
                
@@ -305,7 +319,7 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns PI arrival time.]
+  Synopsis    [Updates required time of the PI.]
 
   Description []
                
@@ -314,52 +328,18 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
+void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
 {
-    Tim_Box_t * pBox;
-    Tim_Obj_t * pObj;
-    float * pDelays;
-    float DelayMax;
-    int i, k;
     assert( iPi < p->nPis );
-    if ( p->pPis[iPi].iObj2Box < 0 )
-        return p->pPis[iPi].timeArr;
-    pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
-    // check if box timing is updated
-    if ( pBox->TravId == p->nTravIds )
-    {
-        assert( pBox->TravId == p->nTravIds );
-        return p->pPis[iPi].timeArr;
-    }
-    pBox->TravId = p->nTravIds;
-    // update box timing
-    // get the arrival times of the inputs of the box (POs)
-    for ( i = 0; i < pBox->nInputs; i++ )
-    {
-        pObj = p->pPos + pBox->Inouts[i];
-        if ( pObj->TravId != p->nTravIds )
-            printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
-    }
-    // compute the required times for each output of the box (PIs)
-    for ( i = 0; i < pBox->nOutputs; i++ )
-    {
-        pDelays = pBox->pDelayTable + i * pBox->nInputs;
-        DelayMax = -AIG_INFINITY;
-        for ( k = 0; k < pBox->nInputs; k++ )
-        {
-            pObj = p->pPos + pBox->Inouts[k];
-            DelayMax = AIG_MAX( DelayMax, pObj->timeArr + pDelays[k] );
-        }
-        pObj = p->pPis + pBox->Inouts[pBox->nInputs+i];
-        pObj->timeArr = DelayMax;
-        pObj->TravId = p->nTravIds;
-    }
-    return p->pPis[iPi].timeArr;
+    assert( p->pPis[iPi].TravId != p->nTravIds );
+    p->pPis[iPi].timeReq = Delay;
+    p->pPis[iPi].TravId = p->nTravIds;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Returns PO required time.]
+  Synopsis    [Returns PI arrival time.]
 
   Description []
                
@@ -368,12 +348,33 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
+float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
 {
-    assert( iPi < p->nPis );
-    assert( p->pPis[iPi].TravId != p->nTravIds );
-    p->pPis[iPi].timeReq = Delay;
-    p->pPis[iPi].TravId = p->nTravIds;
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj, * pObjRes;
+    float * pDelays, DelayBest;
+    int i, k;
+    // consider the main PI or the already processed PI
+    pBox = Tim_ManPiBox( p, iPi );
+    if ( pBox == NULL || pBox->TravId == p->nTravIds )
+        return Tim_ManPi(p, iPi)->timeArr;
+    // update box timing
+    pBox->TravId = p->nTravIds;
+    // get the arrival times of the inputs of the box (POs)
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
+    // compute the required times for each output of the box (PIs)
+    Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
+    {
+        pDelays = pBox->pDelayTable + i * pBox->nInputs;
+        DelayBest = -AIG_INFINITY;
+        Tim_ManBoxForEachInput( p, pBox, pObj, k )
+            DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
+        pObjRes->timeArr = DelayBest;
+        pObjRes->TravId = p->nTravIds;
+    }
+    return Tim_ManPi(p, iPi)->timeArr;
 }
 
 /**Function*************************************************************
@@ -389,7 +390,33 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
 ***********************************************************************/
 float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
 {
-    return 0.0;
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj, * pObjRes;
+    float * pDelays, DelayBest;
+    int i, k;
+    // consider the main PO or the already processed PO
+    pBox = Tim_ManPoBox( p, iPo );
+    if ( pBox == NULL || pBox->TravId == p->nTravIds )
+        return Tim_ManPo(p, iPo)->timeReq;
+    // update box timing
+    pBox->TravId = p->nTravIds;
+    // get the arrival times of the inputs of the box (POs)
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Tim_ManGetPoRequired(): PI required times of the box are not up to date!\n" );
+    // compute the required times for each output of the box (PIs)
+    Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
+    {
+        DelayBest = AIG_INFINITY;
+        Tim_ManBoxForEachOutput( p, pBox, pObj, k )
+        {
+            pDelays = pBox->pDelayTable + k * pBox->nInputs;
+            DelayBest = AIG_MIN( DelayBest, pObj->timeReq + pDelays[i] );
+        }
+        pObjRes->timeReq = DelayBest;
+        pObjRes->TravId = p->nTravIds;
+    }
+    return Tim_ManPo(p, iPo)->timeReq;
 }
 
 
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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 17040742..07816790 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -326,8 +326,13 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 extern int             If_ManPerformMapping( If_Man_t * p );
 extern int             If_ManPerformMappingComb( If_Man_t * p );
 /*=== ifCut.c ============================================================*/
+extern int             If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
+extern void            If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
+extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
 extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
 extern void            If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
+extern void            If_CutLift( If_Cut_t * pCut );
+extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
 extern float           If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
@@ -339,12 +344,6 @@ extern float           If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
-extern int             If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
-extern void            If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
-extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
-extern void            If_CutLift( If_Cut_t * pCut );
-extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
-extern void            If_ManSortCuts( If_Man_t * p, int Mode );
 /*=== ifMan.c =============================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
 extern void            If_ManRestart( If_Man_t * p );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 915cedf9..cc842c19 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -311,21 +311,21 @@ int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareDelay( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
+    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
         return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
+    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
     if ( pC0->nLeaves > pC1->nLeaves )
         return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
+    if ( pC0->Area < pC1->Area - p->fEpsilon )
         return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
+    if ( pC0->Area > pC1->Area + p->fEpsilon )
         return 1;
     return 0;
 }
@@ -341,17 +341,17 @@ int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareDelayOld( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
+    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
         return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
+    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
         return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
+    if ( pC0->Area < pC1->Area - p->fEpsilon )
         return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
+    if ( pC0->Area > pC1->Area + p->fEpsilon )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
@@ -371,13 +371,13 @@ int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+int If_CutCompareArea( If_Man_t * p, If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
+    if ( pC0->Area < pC1->Area - p->fEpsilon )
         return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
+    if ( pC0->Area > pC1->Area + p->fEpsilon )
         return 1;
     if ( pC0->AveRefs > pC1->AveRefs )
         return -1;
@@ -387,9 +387,9 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
         return -1;
     if ( pC0->nLeaves > pC1->nLeaves )
         return 1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
+    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
         return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
+    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
         return 1;
     return 0;
 }
@@ -433,13 +433,13 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
 {
     if ( p->SortMode == 1 ) // area
     {
-        if ( pC0->Area < pC1->Area - 0.0001 )
+        if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
-        if ( pC0->Area > pC1->Area + 0.0001 )
+        if ( pC0->Area > pC1->Area + p->fEpsilon )
             return 1;
-        if ( pC0->Edge < pC1->Edge - 0.0001 )
+        if ( pC0->Edge < pC1->Edge - p->fEpsilon )
             return -1;
-        if ( pC0->Edge > pC1->Edge + 0.0001 )
+        if ( pC0->Edge > pC1->Edge + p->fEpsilon )
             return 1;
         if ( pC0->AveRefs > pC1->AveRefs )
             return -1;
@@ -449,44 +449,44 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
             return -1;
         if ( pC0->nLeaves > pC1->nLeaves )
             return 1;
-        if ( pC0->Delay < pC1->Delay - 0.0001 )
+        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
-        if ( pC0->Delay > pC1->Delay + 0.0001 )
+        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
             return 1;
         return 0;
     }
     if ( p->SortMode == 0 ) // delay
     {
-        if ( pC0->Delay < pC1->Delay - 0.0001 )
+        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
-        if ( pC0->Delay > pC1->Delay + 0.0001 )
+        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
             return 1;
         if ( pC0->nLeaves < pC1->nLeaves )
             return -1;
         if ( pC0->nLeaves > pC1->nLeaves )
             return 1;
-        if ( pC0->Area < pC1->Area - 0.0001 )
+        if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
-        if ( pC0->Area > pC1->Area + 0.0001 )
+        if ( pC0->Area > pC1->Area + p->fEpsilon )
             return 1;
-        if ( pC0->Edge < pC1->Edge - 0.0001 )
+        if ( pC0->Edge < pC1->Edge - p->fEpsilon )
             return -1;
-        if ( pC0->Edge > pC1->Edge + 0.0001 )
+        if ( pC0->Edge > pC1->Edge + p->fEpsilon )
             return 1;
         return 0;
     }
     assert( p->SortMode == 2 ); // delay old
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
+    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
         return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
+    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
         return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
+    if ( pC0->Area < pC1->Area - p->fEpsilon )
         return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
+    if ( pC0->Area > pC1->Area + p->fEpsilon )
         return 1;
-    if ( pC0->Edge < pC1->Edge - 0.0001 )
+    if ( pC0->Edge < pC1->Edge - p->fEpsilon )
         return -1;
-    if ( pC0->Edge > pC1->Edge + 0.0001 )
+    if ( pC0->Edge > pC1->Edge + p->fEpsilon )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
@@ -510,9 +510,9 @@ static inline int If_ManSortCompare_old( If_Man_t * p, If_Cut_t * pC0, If_Cut_t
 {
     if ( p->SortMode == 1 ) // area
     {
-        if ( pC0->Area < pC1->Area - 0.0001 )
+        if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
-        if ( pC0->Area > pC1->Area + 0.0001 )
+        if ( pC0->Area > pC1->Area + p->fEpsilon )
             return 1;
         if ( pC0->AveRefs > pC1->AveRefs )
             return -1;
@@ -522,36 +522,36 @@ static inline int If_ManSortCompare_old( If_Man_t * p, If_Cut_t * pC0, If_Cut_t
             return -1;
         if ( pC0->nLeaves > pC1->nLeaves )
             return 1;
-        if ( pC0->Delay < pC1->Delay - 0.0001 )
+        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
-        if ( pC0->Delay > pC1->Delay + 0.0001 )
+        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
             return 1;
         return 0;
     }
     if ( p->SortMode == 0 ) // delay
     {
-        if ( pC0->Delay < pC1->Delay - 0.0001 )
+        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
-        if ( pC0->Delay > pC1->Delay + 0.0001 )
+        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
             return 1;
         if ( pC0->nLeaves < pC1->nLeaves )
             return -1;
         if ( pC0->nLeaves > pC1->nLeaves )
             return 1;
-        if ( pC0->Area < pC1->Area - 0.0001 )
+        if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
-        if ( pC0->Area > pC1->Area + 0.0001 )
+        if ( pC0->Area > pC1->Area + p->fEpsilon )
             return 1;
         return 0;
     }
     assert( p->SortMode == 2 ); // delay old
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
+    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
         return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
+    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
         return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
+    if ( pC0->Area < pC1->Area - p->fEpsilon )
         return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
+    if ( pC0->Area > pC1->Area + p->fEpsilon )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
@@ -646,6 +646,56 @@ void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Moves the cut over the latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutLift( If_Cut_t * pCut )
+{
+    unsigned i;
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        assert( (pCut->pLeaves[i] & 255) < 255 );
+        pCut->pLeaves[i]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
+{
+    int * pLeaves;
+    char * pPerm;
+    unsigned * pTruth;
+    // save old arrays
+    pLeaves = pCutDest->pLeaves;
+    pPerm   = pCutDest->pPerm;
+    pTruth  = pCutDest->pTruth;
+    // copy the cut info
+    memcpy( pCutDest, pCutSrc, p->nCutBytes );
+    // restore the arrays
+    pCutDest->pLeaves = pLeaves;
+    pCutDest->pPerm   = pPerm;
+    pCutDest->pTruth  = pTruth;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes area flow.]
 
   Description []
@@ -931,55 +981,6 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    [Moves the cut over the latch.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutLift( If_Cut_t * pCut )
-{
-    unsigned i;
-    for ( i = 0; i < pCut->nLeaves; i++ )
-    {
-        assert( (pCut->pLeaves[i] & 255) < 255 );
-        pCut->pLeaves[i]++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
-{
-    int * pLeaves;
-    char * pPerm;
-    unsigned * pTruth;
-    // save old arrays
-    pLeaves = pCutDest->pLeaves;
-    pPerm   = pCutDest->pPerm;
-    pTruth  = pCutDest->pTruth;
-    // copy the cut info
-    memcpy( pCutDest, pCutSrc, p->nCutBytes );
-    // restore the arrays
-    pCutDest->pLeaves = pLeaves;
-    pCutDest->pPerm   = pPerm;
-    pCutDest->pTruth  = pTruth;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 50ce63e9..977d69c9 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -68,8 +68,8 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
 //    p->pMemSet     = Mem_FixedStart( p->nSetBytes );
     // report expected memory usage
     if ( p->pPars->fVerbose )
-        printf( "Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n", 
-            4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
+        printf( "K = %d. Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n", 
+            p->pPars->nLutSize, 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
     // room for temporary truth tables
     p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
     p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index ab7de609..0912a965 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -150,6 +150,7 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     int CostBef, CostAft, i;
     float DelayOld, AreaBef, AreaAft;
     pCut = If_ObjCutBest(pObj);
+    pCut->Delay = If_CutDelay( p, pCut );
     assert( pCut->Delay <= pObj->Required + p->fEpsilon );
     if ( pObj->nRefs == 0 )
         return;
@@ -449,8 +450,8 @@ int If_ManImproveNodeFaninCompact_int( If_Man_t * p, If_Obj_t * pObj, int nLimit
         return 1;
     if (  Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact1(p, pObj, nLimit, vFront, vVisited) )
         return 1;
-    if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
-        return 1;
+//    if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
+//        return 1;
     assert( Vec_PtrSize(vFront) <= nLimit );
     return 0;
 }
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f4fcf94a..3bb39e2f 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -212,7 +212,7 @@ void If_ManComputeRequired( If_Man_t * p )
     Vec_PtrForEachEntry( p->vMapped, pObj, i )
         If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Computes area, references, and nodes used in the mapping.]
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make