Version abc70926

22 files changed, 386 insertions, 85 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index fe237142..63456b5d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -68,19 +68,23 @@ typedef enum {
 // the AIG node
 struct Aig_Obj_t_  // 8 words
 {
-    void *           pData;          // misc (cuts, copy, etc)
     Aig_Obj_t *      pNext;          // strashing table
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
-    unsigned long    Type    :  3;   // object type
-    unsigned long    fPhase  :  1;   // value under 000...0 pattern
-    unsigned long    fMarkA  :  1;   // multipurpose mask
-    unsigned long    fMarkB  :  1;   // multipurpose mask
-    unsigned long    nRefs   : 26;   // reference count 
+    unsigned int     Type    :  3;   // object type
+    unsigned int     fPhase  :  1;   // value under 000...0 pattern
+    unsigned int     fMarkA  :  1;   // multipurpose mask
+    unsigned int     fMarkB  :  1;   // multipurpose mask
+    unsigned int     nRefs   : 26;   // reference count 
     unsigned         Level   : 24;   // the level of this node
     unsigned         nCuts   :  8;   // the number of cuts
     int              TravId;         // unique ID of last traversal involving the node
     int              Id;             // unique ID of the node
+    union {                          // temporary store for user's data
+        void *       pData;
+        int          iData;
+        float        dData;
+    };
 };
 
 // the AIG manager
@@ -133,6 +137,10 @@ struct Aig_Man_t_
     void (*pImpFunc) (void*, void*); // implication checking precedure
     void *           pImpData;       // implication checking data
     Aig_TMan_t *     pManTime;       // the timing manager
+    Vec_Int_t *      vPiIds;
+    Vec_Int_t *      vPoIds;
+    Vec_Ptr_t *      vMapped;
+    Vec_Int_t *      vFlopNums;      
     // timing statistics
     int              time1;
     int              time2;
@@ -497,6 +505,7 @@ extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
 extern void            Aig_ManDump( Aig_Man_t * p );
 extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
  
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index f4a6bf6b..8c53e635 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -89,7 +89,8 @@ int Aig_ManCheck( Aig_Man_t * p )
         }
     }
     // count the total number of nodes
-    if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
+    if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + 
+        Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
     {
         printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
         printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 9cfaf69c..e9821bdc 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -270,22 +270,22 @@ int Aig_ManCountLevels( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     int i, LevelsMax, Level0, Level1;
     // initialize the levels
-    Aig_ManConst1(p)->pData = NULL;
+    Aig_ManConst1(p)->iData = 0;
     Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = NULL;
+        pObj->iData = 0;
     // compute levels in a DFS order
     vNodes = Aig_ManDfs( p );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        Level0 = (int)Aig_ObjFanin0(pObj)->pData;
-        Level1 = (int)Aig_ObjFanin1(pObj)->pData;
-        pObj->pData = (void *)(1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
+        Level0 = Aig_ObjFanin0(pObj)->iData;
+        Level1 = Aig_ObjFanin1(pObj)->iData;
+        pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
     }
     Vec_PtrFree( vNodes );
     // get levels of the POs
     LevelsMax = 0;
     Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->pData );
+        LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
     return LevelsMax;
 }
 
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 1e0ee278..d2714380 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -139,6 +139,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -226,6 +228,8 @@ void Aig_ManStop( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
+    if ( p->vMapped )
+        Vec_PtrFree( p->vMapped );
     // print time
     if ( p->time1 ) { PRT( "time1", p->time1 ); }
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
@@ -246,6 +250,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vBufs )    Vec_PtrFree( p->vBufs );
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
+    if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
     FREE( p->pName );
     FREE( p->pObjCopies );
     FREE( p->pReprs );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 4c879ee8..65e35fc4 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -890,7 +890,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
 
     // start the total fraiged AIG
     pAigTotal = Aig_ManStartFrom( pAig );
-    Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) );
+    Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 );
     vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
 
     // set the PI numbers
@@ -932,7 +932,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
         Aig_ManForEachObj( pAigPart, pObj, k )
             ppData[k] = pObj->pData;
         // report the process
-        printf( "Fraiging part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
+        printf( "Part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
             i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), 
             Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
         // compute equivalence classes (to be stored in pNew->pReprs)
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 787ede49..6356afd3 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -270,6 +270,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 2f00a7eb..abd424c1 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -50,6 +50,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -152,6 +154,20 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
     // if some latches are removed, update PIs/POs
     if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
     {
+        if ( p->vFlopNums )
+        {
+            int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p);
+            // remember numbers of flops in the flops
+            Aig_ManForEachLiSeq( p, pObj, i )
+                pObj->pNext = (void *)Vec_IntEntry( p->vFlopNums, i - nTruePos );
+            // reset the flop numbers
+            Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos )
+                Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)pObj->pNext );
+            Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos );
+            // clean the next pointer
+            Aig_ManForEachLiSeq( p, pObj, i )
+                pObj->pNext = NULL;
+        }
         // collect new CIs/COs
         vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
         Aig_ManForEachPi( p, pObj, i )
@@ -184,6 +200,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
         Vec_PtrFree( p->vPos );    p->vPos = vCos;
         p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
         p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+                
     }
     Vec_PtrFree( vNodes );
     // remove dangling nodes
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 86cd02ce..2fba3cb1 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -672,13 +672,13 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     // collect nodes in the DFS order
     vNodes = Aig_ManDfs( p );
     // assign IDs to objects
-    Aig_ManConst1(p)->pData = (void *)Counter++;
+    Aig_ManConst1(p)->iData = Counter++;
     Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = (void *)Counter++;
+        pObj->iData = Counter++;
     Aig_ManForEachPo( p, pObj, i )
-        pObj->pData = (void *)Counter++;
+        pObj->iData = Counter++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = (void *)Counter++;
+        pObj->iData = Counter++;
     nDigits = Aig_Base10Log( Counter );
     // write the file
     pFile = fopen( pFileName, "w" );
@@ -688,51 +688,157 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     // write PIs
     fprintf( pFile, ".inputs" );
     Aig_ManForEachPiSeq( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
+        fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write POs
     fprintf( pFile, ".outputs" );
     Aig_ManForEachPoSeq( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
+        fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write latches
     if ( Aig_ManRegNum(p) )
     {
     fprintf( pFile, "\n" );
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-        fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData );
+        fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
     fprintf( pFile, "\n" );
     }
     // write nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", 
-            nDigits, (int)Aig_ObjFanin0(pObj)->pData, 
-            nDigits, (int)Aig_ObjFanin1(pObj)->pData, 
-            nDigits, (int)pObj->pData );
+            nDigits, Aig_ObjFanin0(pObj)->iData, 
+            nDigits, Aig_ObjFanin1(pObj)->iData, 
+            nDigits, pObj->iData );
         fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
     }
     // write POs
     Aig_ManForEachPo( p, pObj, i )
     {
-        if ( (int)pObj->pData == 1359 )
-        {
-            int x = 0;
-        }
         fprintf( pFile, ".names n%0*d n%0*d\n", 
-            nDigits, (int)Aig_ObjFanin0(pObj)->pData, 
-            nDigits, (int)pObj->pData );
+            nDigits, Aig_ObjFanin0(pObj)->iData, 
+            nDigits, pObj->iData );
         fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
             pConst1 = Aig_ManConst1(p);
     }
     if ( pConst1 )
-        fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData );
+        fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
     fprintf( pFile, ".end\n\n" );
     fclose( pFile );
     Vec_PtrFree( vNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG into the BLIF file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
+    int i, nDigits, Counter = 0;
+    if ( Aig_ManPoNum(p) == 0 )
+    {
+        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
+        return;
+    }
+    // collect nodes in the DFS order
+    vNodes = Aig_ManDfs( p );
+    // assign IDs to objects
+    Aig_ManConst1(p)->iData = Counter++;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->iData = Counter++;
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->iData = Counter++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->iData = Counter++;
+    nDigits = Aig_Base10Log( Counter );
+    // write the file
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog() in ABC\n" );
+    fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+    fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
+    Aig_ManForEachPoSeq( p, pObj, i )
+        fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
+    fprintf( pFile, " );\n" );
+
+    // write PIs
+    Aig_ManForEachPiSeq( p, pObj, i )
+        fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
+    // write POs
+    Aig_ManForEachPoSeq( p, pObj, i )
+        fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
+    // write latches
+    if ( Aig_ManRegNum(p) )
+    {
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
+    }
+    // write nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
+    // write nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", 
+            nDigits, pObj->iData,
+            !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData, 
+            !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
+            );
+    }
+    // write POs
+    Aig_ManForEachPoSeq( p, pObj, i )
+    {
+        fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
+            nDigits, pObj->iData,
+            !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
+        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
+            pConst1 = Aig_ManConst1(p);
+    }
+    if ( Aig_ManRegNum(p) )
+    {
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        {
+            fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
+                nDigits, pObjLi->iData,
+                !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
+            if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObjLi)) )
+                pConst1 = Aig_ManConst1(p);
+        }
+    }
+    if ( pConst1 )
+        fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
+
+    // write initial state
+    if ( Aig_ManRegNum(p) )
+    {
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+            fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n", 
+                 nDigits, pObjLo->iData,
+                 nDigits, pObjLi->iData );
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+            fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n", 
+                 nDigits, pObjLo->iData );
+    }
+
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+    Vec_PtrFree( vNodes );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index d1b1cd3b..c35e7121 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -13,6 +13,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigScl.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigTable.c \
+    src/aig/aig/aigTime.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \
     src/aig/aig/aigTsim.c \
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index d4266103..989535f2 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -57,6 +57,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index a5435862..142c7721 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -463,7 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
 ***********************************************************************/
 int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 {
-    ProgressBar * pProgress;
+    Bar_Progress_t * pProgress;
     Ref_Man_t * p;
     Vec_Ptr_t * vCut, * vCut2;
     Aig_Obj_t * pObj, * pObjNew;
@@ -485,10 +485,10 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     vCut2 = Vec_VecEntry( p->vCuts, 1 );
     p->nNodesInit = Aig_ManNodeNum(pAig);
     nNodesOld = Vec_PtrSize( pAig->vObjs );
-    pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+    pProgress = Bar_ProgressStart( stdout, nNodesOld );
     Aig_ManForEachObj( pAig, pObj, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Bar_ProgressUpdate( pProgress, i, NULL );
         if ( !Aig_ObjIsNode(pObj) )
             continue;
         if ( i > nNodesOld )
@@ -564,7 +564,7 @@ p->timeEval += clock() - clk;
 p->timeTotal = clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
-    Extra_ProgressBarStop( pProgress );
+    Bar_ProgressStop( pProgress );
     // put the nodes into the DFS order and reassign their IDs
 //    Aig_NtkReassignIds( p );
     // fix the levels
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 98025280..f45e8af0 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -147,6 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
 
     // add timeframes
+//    pManFraig->fAddStrash = 1;
     for ( f = 0; f < p->nFramesAll - 1; f++ )
     {
         // set the constraints on the latch outputs
@@ -163,6 +164,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
             Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
     }
+//    pManFraig->fAddStrash = 0;
     // mark the asserts
     pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
     // add the POs for the latch outputs of the last frame
@@ -348,7 +350,9 @@ PRT( "Time", clock() - clk );
         // mark the classes as non-refined
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
+clk2 = clock();
         p->pManFraig = Fra_FramesWithClasses( p );
+p->timeTrav += clock() - clk2;
 //Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
 
         // perform AIG rewriting
@@ -406,6 +410,9 @@ PRT( "Time", clock() - clk );
         p->nSatCallsRecent = 0;
         p->nSatCallsSkipped = 0;
         Fra_FraigSweep( p );
+
+//        Sat_SolverPrintStats( stdout, p->pSat );
+
         // remove FRAIG and SAT solver
         Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
         sat_solver_delete( p->pSat );  p->pSat = NULL; 
@@ -425,7 +432,7 @@ PRT( "Time", clock() - clk );
         }
     }
 /*
-    // check implications using simulation
+    // verify implications using simulation
     if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
     {
         int Temp, clk = clock();
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 0919e035..f9bbfe44 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -169,7 +169,7 @@ PRT( "Time", clock() - clk );
 
     // perform fraiging
 clk = clock();
-    pNew = Fra_FraigEquivence( pTemp = pNew, 1000 );
+    pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
     {
@@ -199,13 +199,14 @@ PRT( "Time", clock() - clk );
 clk = clock();
         pNew = Aig_ManDup( pTemp = pNew, 1 );
         Aig_ManStop( pTemp );
-        pNew = Dar_ManRewriteDefault( pTemp = pNew );
+        pNew = Dar_ManRewriteDefault( pNew );
         if ( fVerbose )
         {
             printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         } 
+
         // perform retiming
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -218,6 +219,7 @@ clk = clock();
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
+
         if ( pNew->nRegs )
         pNew = Aig_ManConstReduce( pNew, 0 );
 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d379cf53..b77c775a 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -432,12 +432,11 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
 //        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
 
         // flip one bit of the last frame
-        if ( fUseDist1 && p->nFrames == 2 )
+        if ( fUseDist1 ) //&& p->nFrames == 2 )
         {
             Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
             for ( i = 0; i < Limit; i++ )
-                Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
-//            Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
+                Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
         }
     }
 }
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index c5815a2c..e8e916cc 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -67,11 +67,11 @@ struct Hop_Obj_t_  // 6 words
     Hop_Obj_t *      pNext;          // strashing table
     Hop_Obj_t *      pFanin0;        // fanin
     Hop_Obj_t *      pFanin1;        // fanin
-    unsigned long    Type    :  3;   // object type
-    unsigned long    fPhase  :  1;   // value under 000...0 pattern
-    unsigned long    fMarkA  :  1;   // multipurpose mask
-    unsigned long    fMarkB  :  1;   // multipurpose mask
-    unsigned long    nRefs   : 26;   // reference count (level)
+    unsigned int     Type    :  3;   // object type
+    unsigned int     fPhase  :  1;   // value under 000...0 pattern
+    unsigned int     fMarkA  :  1;   // multipurpose mask
+    unsigned int     fMarkB  :  1;   // multipurpose mask
+    unsigned int     nRefs   : 26;   // reference count (level)
     int              Id;             // unique ID of the node
 };
 
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 74462bbd..a6c23fd4 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -249,7 +249,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
 */
     // write the comment
     fprintf( pFile, "c\n" );
-    fprintf( pFile, "%s\n", pMan->pName );
+    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, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
     fclose( pFile );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 81ed895e..1ab91dd2 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2101,8 +2101,8 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
         // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+//        pLits[0] = toLit( 0 );
+//        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
@@ -2235,8 +2235,8 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
         // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+//        pLits[0] = toLit( 0 );
+//        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/kit/kitAig.c b/src/aig/kit/kitAig.c
new file mode 100644
index 00000000..0d5c1686
--- /dev/null
+++ b/src/aig/kit/kitAig.c
@@ -0,0 +1,121 @@
+/**CFile****************************************************************
+
+  FileName    [kitAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation kit.]
+
+  Synopsis    [Procedures involving AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 6, 2006.]
+
+  Revision    [$Id: kitAig.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph )
+{
+    Kit_Node_t * pNode;
+    Aig_Obj_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Kit_GraphIsConst(pGraph) )
+        return Aig_NotCond( Aig_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Kit_GraphIsVar(pGraph) )
+        return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Kit_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
+    }
+    // complement the result if necessary
+    return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t * pGraph )
+{
+    Kit_Node_t * pNode;
+    int i;
+    // collect the fanins
+    Kit_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = pFanins[i];
+    // perform strashing
+    return Kit_GraphToAigInternal( pMan, pGraph );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashed onen logic nodes using its truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
+{
+    Aig_Obj_t * pObj;
+    Kit_Graph_t * pGraph;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
+    // derive the AIG for the decomposition tree
+    pObj = Kit_GraphToAig( pMan, pFanins, pGraph );
+    Kit_GraphFree( pGraph );
+    return pObj;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index abd07e68..e24a9964 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -2058,7 +2058,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk );
-    if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
+    if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
 
diff --git a/src/aig/kit/kitIsop.c b/src/aig/kit/kitIsop.c
index cc61a6bd..42fae2ea 100644
--- a/src/aig/kit/kitIsop.c
+++ b/src/aig/kit/kitIsop.c
@@ -58,7 +58,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
     assert( nVars >= 0 && nVars < 16 );
     // if nVars < 5, make sure it does not depend on those vars
 //    for ( i = nVars; i < 5; i++ )
-//        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+//        assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
     // prepare memory manager
     Vec_IntClear( vMemory );
     Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
@@ -69,7 +69,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
         vMemory->nSize = -1;
         return -1;
     }
-    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+    assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
     if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
     {
         vMemory->pArray[0] = 0;
@@ -79,18 +79,18 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
     if ( fTryBoth )
     {
         // compute ISOP for the complemented polarity
-        Extra_TruthNot( puTruth, puTruth, nVars );
+        Kit_TruthNot( puTruth, puTruth, nVars );
         pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
         if ( pcRes2->nCubes >= 0 )
         {
-            assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+            assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
             if ( pcRes->nCubes > pcRes2->nCubes )
             {
                 RetValue = 1;
                 pcRes = pcRes2;
             }
         }
-        Extra_TruthNot( puTruth, puTruth, nVars );
+        Kit_TruthNot( puTruth, puTruth, nVars );
     }
 //    printf( "%d ", vMemory->nSize );
     // move the cover representation to the beginning of the memory buffer
@@ -117,9 +117,9 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
     unsigned * puRes0, * puRes1, * puRes2;
     unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
     int i, k, Var, nWords, nWordsAll;
-//    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+//    assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
     // allocate room for the resulting truth table
-    nWordsAll = Extra_TruthWordNum( nVars );
+    nWordsAll = Kit_TruthWordNum( nVars );
     pTemp = Vec_IntFetch( vStore, nWordsAll );
     if ( pTemp == NULL )
     {
@@ -127,14 +127,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
         return NULL;
     }
     // check for constants
-    if ( Extra_TruthIsConst0( puOn, nVars ) )
+    if ( Kit_TruthIsConst0( puOn, nVars ) )
     {
         pcRes->nCubes = 0;
         pcRes->pCubes = NULL;
-        Extra_TruthClear( pTemp, nVars );
+        Kit_TruthClear( pTemp, nVars );
         return pTemp;
     }
-    if ( Extra_TruthIsConst1( puOnDc, nVars ) )
+    if ( Kit_TruthIsConst1( puOnDc, nVars ) )
     {
         pcRes->nCubes = 1;
         pcRes->pCubes = Vec_IntFetch( vStore, 1 );
@@ -144,14 +144,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
             return NULL;
         }
         pcRes->pCubes[0] = 0;
-        Extra_TruthFill( pTemp, nVars );
+        Kit_TruthFill( pTemp, nVars );
         return pTemp;
     }
     assert( nVars > 0 );
     // find the topmost var
     for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || 
-             Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
+        if ( Kit_TruthVarInSupport( puOn, nVars, Var ) || 
+             Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
              break;
     assert( Var >= 0 );
     // consider a simple case when one-word computation can be used
@@ -163,30 +163,30 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
         return pTemp;
     }
     assert( Var >= 5 );
-    nWords = Extra_TruthWordNum( Var );
+    nWords = Kit_TruthWordNum( Var );
     // cofactor
     puOn0   = puOn;    puOn1   = puOn + nWords;
     puOnDc0 = puOnDc;  puOnDc1 = puOnDc + nWords;
     pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
     // solve for cofactors
-    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
+    Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
     puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
     if ( pcRes0->nCubes == -1 )
     {
         pcRes->nCubes = -1;
         return NULL;
     }
-    Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
+    Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
     puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
     if ( pcRes1->nCubes == -1 )
     {
         pcRes->nCubes = -1;
         return NULL;
     }
-    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
-    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
-    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
-    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
+    Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
+    Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
+    Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
+    Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
     puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
     if ( pcRes2->nCubes == -1 )
     {
@@ -210,16 +210,16 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit
         pcRes->pCubes[k++] = pcRes2->pCubes[i];
     assert( k == pcRes->nCubes );
     // create the resulting truth table
-    Extra_TruthOr( pTemp0, puRes0, puRes2, Var );
-    Extra_TruthOr( pTemp1, puRes1, puRes2, Var );
+    Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
+    Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
     // copy the table if needed
     nWords <<= 1;
     for ( i = 1; i < nWordsAll/nWords; i++ )
         for ( k = 0; k < nWords; k++ )
             pTemp[i*nWords + k] = pTemp[k];
     // verify in the end
-//    assert( Extra_TruthIsImply( puOn, pTemp, nVars ) );
-//    assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) );
+//    assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
+//    assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
     return pTemp;
 }
 
@@ -264,17 +264,17 @@ unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t
     assert( nVars > 0 );
     // find the topmost var
     for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || 
-             Extra_TruthVarInSupport( &uOnDc, 5, Var ) )
+        if ( Kit_TruthVarInSupport( &uOn, 5, Var ) || 
+             Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
              break;
     assert( Var >= 0 );
     // cofactor
     uOn0   = uOn1   = uOn;
     uOnDc0 = uOnDc1 = uOnDc;
-    Extra_TruthCofactor0( &uOn0, Var + 1, Var );
-    Extra_TruthCofactor1( &uOn1, Var + 1, Var );
-    Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
-    Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
+    Kit_TruthCofactor0( &uOn0, Var + 1, Var );
+    Kit_TruthCofactor1( &uOn1, Var + 1, Var );
+    Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
+    Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
     // solve for cofactors
     uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
     if ( pcRes0->nCubes == -1 )
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 65389ef9..5360ad7f 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -1634,6 +1634,33 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the hex unsigned into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
+{
+    int nDigits, Digit, k;
+    // write the number into the file
+    nDigits = (1 << nVars) / 4;
+    for ( k = nDigits - 1; k >= 0; k-- )
+    {
+        Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'a' + Digit-10 );
+    }
+//    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Fast counting minterms for the functions.]
 
   Description [Returns 0 if the function is a constant.]
@@ -1665,7 +1692,7 @@ void Kit_TruthCountMintermsPrecomp()
         uWord |= (bit_count[i & 0x33] << 16);
         uWord |= (bit_count[i & 0x0f] << 24);
         printf( "0x" );
-        Extra_PrintHexadecimal( stdout, &uWord, 5 );
+        Kit_PrintHexadecimal( stdout, &uWord, 5 );
         printf( ", " );
     }
 }
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index 25c8e767..ea62381b 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -1,4 +1,5 @@
-SRC +=  src/aig/kit/kitBdd.c \
+SRC +=  src/aig/kit/kitAig.c \
+    src/aig/kit/kitBdd.c \
     src/aig/kit/kitCloud.c src/aig/kit/cloud.c \
     src/aig/kit/kitDsd.c \
     src/aig/kit/kitFactor.c \