Version abc80404

11 files changed, 291 insertions, 179 deletions

diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 574c72d9..5c9a144f 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -199,6 +199,14 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
             return;
         }
+        if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) )
+        {
+            if ( pObj3 == pObj2 )
+                return;
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+            return;
+        }
         pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
         if ( Aig_TableLookup( p, pGhost ) )
         {
@@ -394,7 +402,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 pObjNew = Aig_ObjCreatePi(pNew); 
                 pObj->pData = pObjNew;
                 // set the arrival time of the new PI
-                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+                arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
                 pObjNew->Level = (int)arrTime;
             }
             else if ( Aig_ObjIsPo(pObj) )
@@ -406,7 +414,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 Aig_ObjCreatePo( pNew, pObjNew );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
-                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+                Tim_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
             }
             else
                 assert( 0 );
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 0637fee0..09b9b3a4 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -600,10 +600,21 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     Aig_ManFanoutStop( pAig );
     if ( p->pPars->fUpdateLevel )
         Aig_ManStopReverseLevels( pAig );
+/*
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        if ( Aig_ObjIsNode(pObj) && Aig_ObjRefs(pObj) == 0 )
+        {
+            printf( "Unreferenced " );
+            Aig_ObjPrintVerbose( pObj, 0 );
+            printf( "\n" );
+        }
+*/
+    // remove dangling nodes (they should not be here!)
+    Aig_ManCleanup( pAig );
 
     // stop the rewriting manager
     Dar_ManRefStop( p );
-    Aig_ManCheckPhase( pAig );
+//    Aig_ManCheckPhase( pAig );
     if ( !Aig_ManCheck( pAig ) )
     {
         printf( "Dar_ManRefactor: The network check has failed.\n" );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 55356654..cd21c95f 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -387,7 +387,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
-        int LevelCur, LevelMax = -TIME_ETERNITY;
+        int LevelCur, LevelMax = -TIM_ETERNITY;
         Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
         {
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 81ea2a2c..2cf3caaa 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -974,9 +974,9 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput
     // find the delay number
     pTokenNum = Vec_PtrEntryLast(vTokens);
     if ( !strcmp( pTokenNum, "-inf" ) )
-        Delay = -TIME_ETERNITY;
+        Delay = -TIM_ETERNITY;
     else if ( !strcmp( pTokenNum, "inf" ) ) 
-        Delay = TIME_ETERNITY;
+        Delay = TIM_ETERNITY;
     else
         Delay = atof( pTokenNum );
     if ( Delay == 0.0 && pTokenNum[0] != '0' )
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index cf2ec0f1..94691ab8 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -90,11 +90,11 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     // unpack the data in the arrival times
     if ( pRoot->vArrivals )
         Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
-            Tim_ManInitPiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
+            Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
     // unpack the data in the required times
     if ( pRoot->vRequireds )
         Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
-            Tim_ManInitPoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
+            Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
     // derive timing tables
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index 308f4693..ed19f71a 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -114,14 +114,14 @@ int Nwk_ManLevelBackup( Nwk_Man_t * pNtk )
     {
         if ( Nwk_ObjIsCi(pObj) )
         {
-            Level = pManTimeUnit? (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId ) : 0;
+            Level = pManTimeUnit? (int)Tim_ManGetCiArrival( pManTimeUnit, pObj->PioId ) : 0;
             Nwk_ObjSetLevel( pObj, Level );
         }
         else if ( Nwk_ObjIsCo(pObj) )
         {
             Level = Nwk_ObjLevel( Nwk_ObjFanin0(pObj) );
             if ( pManTimeUnit )
-                Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level );
+                Tim_ManSetCoArrival( pManTimeUnit, pObj->PioId, (float)Level );
             Nwk_ObjSetLevel( pObj, Level );
             if ( LevelMax < Nwk_ObjLevel(pObj) )
                 LevelMax = Nwk_ObjLevel(pObj);
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index ee7f56ad..acbfbc0a 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -52,7 +52,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
-    pPars->Epsilon     =  (float)0.001;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index b5e2b387..8e49a586 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -114,14 +114,14 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
         if ( Nwk_ObjIsCi(pObj) )
         {
             pObjNew = Aig_ObjCreatePi(pMan);
-            Level = Tim_ManGetPiArrival( pMan->pManTime, pObj->PioId );
+            Level = Tim_ManGetCiArrival( pMan->pManTime, pObj->PioId );
             Aig_ObjSetLevel( pObjNew, Level );
         }
         else if ( Nwk_ObjIsCo(pObj) )
         {
             pObjNew = Aig_ObjCreatePo( pMan, Aig_NotCond(Nwk_ObjFanin0(pObj)->pCopy, pObj->fCompl) );
             Level = Aig_ObjLevel( pObjNew );
-            Tim_ManSetPoArrival( pMan->pManTime, pObj->PioId, (float)Level );
+            Tim_ManSetCoArrival( pMan->pManTime, pObj->PioId, (float)Level );
         }
         else if ( Nwk_ObjIsNode(pObj) )
         {
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 9bf1d6a1..c27f9d61 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -46,7 +46,7 @@ void Nwk_ManCleanTiming( Nwk_Man_t * pNtk )
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
         pObj->tArrival = pObj->tSlack = 0.0;
-        pObj->tRequired = TIME_ETERNITY;
+        pObj->tRequired = TIM_ETERNITY;
     }
 }
 
@@ -138,7 +138,7 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting )
         return Nwk_ObjArrival(pObj);
     if ( Nwk_ObjIsCo(pObj) )
         return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
-    tArrival = -TIME_ETERNITY;
+    tArrival = -TIM_ETERNITY;
     if ( pLutLib == NULL )
     {
         Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -196,7 +196,7 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting )
     assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
     if ( Nwk_ObjIsCo(pObj) )
         return Nwk_ObjRequired(pObj);
-    tRequired = TIME_ETERNITY;
+    tRequired = TIM_ETERNITY;
     if ( pLutLib == NULL )
     {
         Nwk_ObjForEachFanout( pObj, pFanout, k )
@@ -321,6 +321,7 @@ float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, int fUseSorting )
 ***********************************************************************/
 float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
 {
+    Vec_Ptr_t * vObjs;
     int fUseSorting = 1;
     If_Lib_t * pLutLib = pNtk->pLutLib;
     Vec_Ptr_t * vNodes;
@@ -333,7 +334,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
             pLutLib->LutMax, Nwk_ManGetFaninMax(pNtk) );
-        return -TIME_ETERNITY;
+        return -TIM_ETERNITY;
     }
 
     // compute the reverse order of all objects
@@ -345,18 +346,21 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
     // propagate arrival times
     if ( pNtk->pManTime )
         Tim_ManIncrementTravId( pNtk->pManTime );
-    Nwk_ManForEachObj( pNtk, pObj, i )
+//    Nwk_ManForEachObj( pNtk, pObj, i )
+    vObjs = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vObjs, pObj, i )
     {
         tArrival = Nwk_NodeComputeArrival( pObj, fUseSorting );
         if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
-            Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+            Tim_ManSetCoArrival( pNtk->pManTime, pObj->PioId, tArrival );
         if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
-            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+            tArrival = Tim_ManGetCiArrival( pNtk->pManTime, pObj->PioId );
         Nwk_ObjSetArrival( pObj, tArrival );
     }
+    Vec_PtrFree( vObjs );
 
     // get the latest arrival times
-    tArrival = -TIME_ETERNITY;
+    tArrival = -TIM_ETERNITY;
     Nwk_ManForEachPo( pNtk, pObj, i )
         if ( tArrival < Nwk_ObjArrival(pObj) )
             tArrival = Nwk_ObjArrival(pObj);
@@ -365,7 +369,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
     if ( pNtk->pManTime )
     {
         Tim_ManIncrementTravId( pNtk->pManTime );
-        Tim_ManSetPoRequiredAll( pNtk->pManTime, tArrival );
+        Tim_ManSetCoRequiredAll( pNtk->pManTime, tArrival );
     }
     else
     {
@@ -383,13 +387,13 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
         else if ( Nwk_ObjIsCi(pObj) )
         {
             if ( pNtk->pManTime )
-                Tim_ManSetPiRequired( pNtk->pManTime, pObj->PioId, Nwk_ObjRequired(pObj) );
+                Tim_ManSetCiRequired( pNtk->pManTime, pObj->PioId, Nwk_ObjRequired(pObj) );
         }
         else if ( Nwk_ObjIsCo(pObj) )
         {
             if ( pNtk->pManTime )
             {
-                tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+                tRequired = Tim_ManGetCoRequired( pNtk->pManTime, pObj->PioId );
                 Nwk_ObjSetRequired( pObj, tRequired );
             }
             if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > Nwk_ObjRequired(pObj) )
@@ -523,7 +527,6 @@ void Nwk_NodeUpdateAddToQueue( Vec_Ptr_t * vQueue, Nwk_Obj_t * pObj, int iCurren
             if ( Nwk_ObjLevel(pTemp2) >= Nwk_ObjLevel(pTemp1) )
                 break;
         }
-//        assert( i-1 > iCurrent );
         vQueue->pArray[i-1] = pTemp1;
         vQueue->pArray[i]   = pTemp2;
     }
@@ -557,7 +560,7 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
     float tArrival;
-    int i, k, iBox, iTerm1, nTerms;
+    int iCur, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
     // verify the arrival time
     tArrival = Nwk_NodeComputeArrival( pObj, 1 );
@@ -569,12 +572,12 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
     // process objects
     if ( pManTime )
         Tim_ManIncrementTravId( pManTime );
-    Vec_PtrForEachEntry( vQueue, pTemp, i )
+    Vec_PtrForEachEntry( vQueue, pTemp, iCur )
     {
         pTemp->MarkA = 0;
         tArrival = Nwk_NodeComputeArrival( pTemp, 1 );
         if ( Nwk_ObjIsCi(pTemp) && pManTime )
-            tArrival = Tim_ManGetPiArrival( pManTime, pTemp->PioId );
+            tArrival = Tim_ManGetCiArrival( pManTime, pTemp->PioId );
         if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.01 ) )
             continue;
         Nwk_ObjSetArrival( pTemp, tArrival );
@@ -583,19 +586,23 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival );
-                iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
-                if ( iBox >= 0 ) // this is not a true PO
+                // it may happen that a box-input (CO) was already marked as visited
+                // when some other box-input of the same box was visited - here we undo this
+                iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId );
+                if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) )
+                    Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox );
+                Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival );
+                if ( iBox >= 0 ) // this CO is an input of the box
                 {
                     Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
-                    for ( i = 0; i < nTerms; i++ )
+                    for ( k = 0; k < nTerms; k++ )
                     {
-                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + k);
                         if ( pNext->MarkA )
                             continue;
-                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 1 );
                         pNext->MarkA = 1;
                     }
                 }
@@ -607,7 +614,7 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
             {
                 if ( pNext->MarkA )
                     continue;
-                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 1 );
                 pNext->MarkA = 1;
             }
         }
@@ -632,7 +639,7 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
     float tRequired;
-    int i, k, iBox, iTerm1, nTerms;
+    int iCur, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
     // make sure the node's required time remained the same
     tRequired = Nwk_NodeComputeRequired( pObj, 1 );
@@ -649,12 +656,12 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
     // process objects
     if ( pManTime )
         Tim_ManIncrementTravId( pManTime );
-    Vec_PtrForEachEntry( vQueue, pTemp, i )
+    Vec_PtrForEachEntry( vQueue, pTemp, iCur )
     {
         pTemp->MarkA = 0;
         tRequired = Nwk_NodeComputeRequired( pTemp, 1 );
         if ( Nwk_ObjIsCo(pTemp) && pManTime )
-            tRequired = Tim_ManGetPoRequired( pManTime, pTemp->PioId );
+            tRequired = Tim_ManGetCoRequired( pManTime, pTemp->PioId );
         if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) )
             continue;
         Nwk_ObjSetRequired( pTemp, tRequired );
@@ -663,19 +670,23 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired );
-                iBox = Tim_ManBoxForCi( pManTime, pNext->PioId );
-                if ( iBox >= 0 ) // this is not a true PO
+                // it may happen that a box-output (CI) was already marked as visited
+                // when some other box-output of the same box was visited - here we undo this
+                iBox = Tim_ManBoxForCi( pManTime, pTemp->PioId );
+                if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) )
+                    Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox );
+                Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired );
+                if ( iBox >= 0 ) // this CI is an output of the box
                 {
                     Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( pManTime, iBox );
-                    for ( i = 0; i < nTerms; i++ )
+                    for ( k = 0; k < nTerms; k++ )
                     {
-                        pNext = Nwk_ManCo(pNext->pMan, iTerm1 + i);
+                        pNext = Nwk_ManCo(pNext->pMan, iTerm1 + k);
                         if ( pNext->MarkA )
                             continue;
-                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 0 );
                         pNext->MarkA = 1;
                     }
                 }
@@ -687,7 +698,7 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
             {
                 if ( pNext->MarkA )
                     continue;
-                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 0 );
                 pNext->MarkA = 1;
             }
         }
@@ -715,7 +726,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
         if ( pManTime )
         {
             iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
-            if ( iBox >= 0 ) // this is not a true PI
+            if ( iBox >= 0 ) // this CI is an output of the box
             {
                 iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
                 nTerms = Tim_ManBoxInputNum( pManTime, iBox );
@@ -751,14 +762,14 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
     Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
-    int LevelNew, i, k, iBox, iTerm1, nTerms;
+    int LevelNew, iCur, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
     // initialize the queue with the node
     Vec_PtrClear( vQueue );
     Vec_PtrPush( vQueue, pObj );
     pObj->MarkA = 1;
     // process objects
-    Vec_PtrForEachEntry( vQueue, pTemp, i )
+    Vec_PtrForEachEntry( vQueue, pTemp, iCur )
     {
         pTemp->MarkA = 0;
         LevelNew = Nwk_ObjLevelNew( pTemp );
@@ -770,18 +781,18 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
+                iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId );
                 if ( iBox >= 0 ) // this is not a true PO
                 {
                     Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
-                    for ( i = 0; i < nTerms; i++ )
+                    for ( k = 0; k < nTerms; k++ )
                     {
-                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + k);
                         if ( pNext->MarkA )
                             continue;
-                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 1 );
                         pNext->MarkA = 1;
                     }
                 }
@@ -793,7 +804,7 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
             {
                 if ( pNext->MarkA )
                     continue;
-                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, iCur, 1 );
                 pNext->MarkA = 1;
             }
         }
@@ -855,7 +866,7 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
     pObjNew->tArrival = pObj->tArrival;
     pObjNew->tRequired = pObj->tRequired;
     // update required times of the old fanins
-    pObj->tRequired = TIME_ETERNITY;
+    pObj->tRequired = TIM_ETERNITY;
     Nwk_NodeUpdateRequired( pObj );
     // remove the old node
     Nwk_ManDeleteNode_rec( pObj );
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 62e29fe9..51970425 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -47,10 +47,10 @@ struct Tim_Man_t_
     Mem_Flex_t *     pMemObj;        // memory manager for boxes
     int              nTravIds;       // traversal ID of the manager
     int              fUseTravId;     // enables the use of traversal ID
-    int              nPis;           // the number of PIs
-    int              nPos;           // the number of POs
-    Tim_Obj_t *      pPis;           // timing info for the PIs
-    Tim_Obj_t *      pPos;           // timing info for the POs
+    int              nCis;           // the number of PIs
+    int              nCos;           // the number of POs
+    Tim_Obj_t *      pCis;           // timing info for the PIs
+    Tim_Obj_t *      pCos;           // timing info for the POs
 };
 
 // timing box
@@ -75,26 +75,26 @@ 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_Obj_t * Tim_ManCi( Tim_Man_t * p, int i )                           { assert( i < p->nCis ); return p->pCis + i;    }
+static inline Tim_Obj_t * Tim_ManCo( Tim_Man_t * p, int i )                           { assert( i < p->nCos ); return p->pCos + i;    }
 static inline Tim_Box_t * Tim_ManBox( Tim_Man_t * p, int i )                          { return Vec_PtrEntry(p->vBoxes, 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_Box_t * Tim_ManCiBox( Tim_Man_t * p, int i )                        { return Tim_ManCi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManCi(p,i)->iObj2Box ); }
+static inline Tim_Box_t * Tim_ManCoBox( Tim_Man_t * p, int i )                        { return Tim_ManCo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManCo(p,i)->iObj2Box ); }
 
-static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { assert( i < pBox->nInputs  ); return p->pPos + pBox->Inouts[i];               }
-static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { assert( i < pBox->nOutputs ); return p->pPis + pBox->Inouts[pBox->nInputs+i]; }
+static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { assert( i < pBox->nInputs  ); return p->pCos + pBox->Inouts[i];               }
+static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { assert( i < pBox->nOutputs ); return p->pCis + 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++ )
 
-#define Tim_ManForEachPi( p, pObj, i )                                           \
-    for ( i = 0; (i < (p)->nPis) && ((pObj) = (p)->pPis + i); i++ )              \
+#define Tim_ManForEachCi( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nCis) && ((pObj) = (p)->pCis + i); i++ )              \
         if ( pObj->iObj2Box >= 0 ) {} else 
-#define Tim_ManForEachPo( p, pObj, i )                                           \
-    for ( i = 0; (i < (p)->nPos) && ((pObj) = (p)->pPos + i); i++ )              \
+#define Tim_ManForEachCo( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nCos) && ((pObj) = (p)->pCos + i); i++ )              \
         if ( pObj->iObj2Box >= 0 ) {} else 
 #define Tim_ManForEachBox( p, pBox, i )                                          \
     Vec_PtrForEachEntry( p->vBoxes, pBox, i )
@@ -114,7 +114,7 @@ static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int
   SeeAlso     []
 
 ***********************************************************************/
-Tim_Man_t * Tim_ManStart( int nPis, int nPos )
+Tim_Man_t * Tim_ManStart( int nCis, int nCos )
 {
     Tim_Man_t * p;
     int i;
@@ -122,27 +122,27 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
     memset( p, 0, sizeof(Tim_Man_t) );
     p->pMemObj = Mem_FlexStart();
     p->vBoxes  = Vec_PtrAlloc( 100 );
-    p->nPis = nPis;
-    p->nPos = nPos;
-    p->pPis = ALLOC( Tim_Obj_t, nPis );
-    memset( p->pPis, 0, sizeof(Tim_Obj_t) * nPis );
-    p->pPos = ALLOC( Tim_Obj_t, nPos );
-    memset( p->pPos, 0, sizeof(Tim_Obj_t) * nPos );
-    for ( i = 0; i < nPis; i++ )
+    p->nCis = nCis;
+    p->nCos = nCos;
+    p->pCis = ALLOC( Tim_Obj_t, nCis );
+    memset( p->pCis, 0, sizeof(Tim_Obj_t) * nCis );
+    p->pCos = ALLOC( Tim_Obj_t, nCos );
+    memset( p->pCos, 0, sizeof(Tim_Obj_t) * nCos );
+    for ( i = 0; i < nCis; i++ )
     {
-        p->pPis[i].Id = i;
-        p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
-        p->pPis[i].timeReq = TIME_ETERNITY;
-        p->pPis[i].timeArr = 0.0;
-        p->pPis[i].TravId = 0;
+        p->pCis[i].Id = i;
+        p->pCis[i].iObj2Box = p->pCis[i].iObj2Num = -1;
+        p->pCis[i].timeReq = TIM_ETERNITY;
+        p->pCis[i].timeArr = 0.0;
+        p->pCis[i].TravId = 0;
     }
-    for ( i = 0; i < nPos; i++ )
+    for ( i = 0; i < nCos; i++ )
     {
-        p->pPos[i].Id = i;
-        p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
-        p->pPos[i].timeReq = TIME_ETERNITY;
-        p->pPos[i].timeArr = 0.0;
-        p->pPos[i].TravId = 0;
+        p->pCos[i].Id = i;
+        p->pCos[i].iObj2Box = p->pCos[i].iObj2Num = -1;
+        p->pCos[i].timeReq = TIM_ETERNITY;
+        p->pCos[i].timeArr = 0.0;
+        p->pCos[i].TravId = 0;
     }
     p->fUseTravId = 1;
     return p;
@@ -166,17 +166,17 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
     Tim_Box_t * pBox;
     float * pDelayTableNew;
     int i, k;
-    pNew = Tim_ManStart( p->nPis, p->nPos );
-    memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
-    memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
-    for ( k = 0; k < p->nPis; k++ )
-        pNew->pPis[k].TravId = 0;
-    for ( k = 0; k < p->nPos; k++ )
-        pNew->pPos[k].TravId = 0;
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
+        pNew->pCis[k].TravId = 0;
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].TravId = 0;
     if ( fDiscrete )
     {
-        for ( k = 0; k < p->nPis; k++ )
-            pNew->pPis[k].timeArr = 0.0; // modify here
+        for ( k = 0; k < p->nCis; k++ )
+            pNew->pCis[k].timeArr = 0.0; // modify here
         // modify the required times
     }
     pNew->vDelayTables = Vec_PtrAlloc( 100 );
@@ -215,16 +215,16 @@ Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p )
     Tim_Box_t * pBox;
     float * pDelayTableNew;
     int i, k;
-    pNew = Tim_ManStart( p->nPis, p->nPos );
-    memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
-    memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
-    for ( k = 0; k < p->nPis; k++ )
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
     {
-        pNew->pPis[k].TravId = 0;
-        pNew->pPis[k].timeArr = 0.0; 
+        pNew->pCis[k].TravId = 0;
+        pNew->pCis[k].timeArr = 0.0; 
     }
-    for ( k = 0; k < p->nPos; k++ )
-        pNew->pPos[k].TravId = 0;
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].TravId = 0;
     pNew->vDelayTables = Vec_PtrAlloc( 100 );
     Tim_ManForEachBox( p, pBox, i )
     {
@@ -254,14 +254,14 @@ Tim_Man_t * Tim_ManDupApprox( Tim_Man_t * p )
 {
     Tim_Man_t * pNew;
     int k;
-    pNew = Tim_ManStart( p->nPis, p->nPos );
-    for ( k = 0; k < p->nPis; k++ )
-        if ( p->pPis[k].iObj2Box == -1 )
-            pNew->pPis[k].timeArr = p->pPis[k].timeArr;
+    pNew = Tim_ManStart( p->nCis, p->nCos );
+    for ( k = 0; k < p->nCis; k++ )
+        if ( p->pCis[k].iObj2Box == -1 )
+            pNew->pCis[k].timeArr = p->pCis[k].timeArr;
         else
-            pNew->pPis[k].timeArr = p->pPis[k].timeReq;
-    for ( k = 0; k < p->nPos; k++ )
-        pNew->pPos[k].timeReq = p->pPos[k].timeReq;
+            pNew->pCis[k].timeArr = p->pCis[k].timeReq;
+    for ( k = 0; k < p->nCos; k++ )
+        pNew->pCos[k].timeReq = p->pCos[k].timeReq;
     return pNew;
 }
 
@@ -288,8 +288,8 @@ void Tim_ManStop( Tim_Man_t * p )
     }
     Vec_PtrFree( p->vBoxes );
     Mem_FlexStop( p->pMemObj, 0 );
-    free( p->pPis );
-    free( p->pPos );
+    free( p->pCis );
+    free( p->pCos );
     free( p );
 }
 
@@ -310,9 +310,9 @@ void Tim_ManPrint( Tim_Man_t * p )
     Tim_Obj_t * pObj;
     int i;
     printf( "TIMING INFORMATION:\n" );
-    Tim_ManForEachPi( p, pObj, i )
+    Tim_ManForEachCi( p, pObj, i )
         printf( "pi%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
-    Tim_ManForEachPo( p, pObj, i )
+    Tim_ManForEachCo( p, pObj, i )
         printf( "po%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
     Tim_ManForEachBox( p, pBox, i )
     {
@@ -405,6 +405,84 @@ void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox )
 
 /**Function*************************************************************
 
+  Synopsis    [Label box inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPreviousTravIdBoxInputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Label box outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPreviousTravIdBoxOutputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManIsCiTravIdCurrent( Tim_Man_t * p, int iCi )
+{
+    assert( iCi < p->nCis );
+    assert( p->fUseTravId );
+    return p->pCis[iCi].TravId == p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManIsCoTravIdCurrent( Tim_Man_t * p, int iCo )
+{
+    assert( iCo < p->nCos );
+    assert( p->fUseTravId );
+    return p->pCos[iCo].TravId == p->nTravIds;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets the vector of timing tables associated with the manager.]
 
   Description []
@@ -444,17 +522,17 @@ void Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOu
     pBox->nOutputs = nOuts;
     for ( i = 0; i < nIns; i++ )
     {
-        assert( pIns[i] < p->nPos );
+        assert( pIns[i] < p->nCos );
         pBox->Inouts[i] = pIns[i];
-        p->pPos[pIns[i]].iObj2Box = pBox->iBox;
-        p->pPos[pIns[i]].iObj2Num = i;
+        p->pCos[pIns[i]].iObj2Box = pBox->iBox;
+        p->pCos[pIns[i]].iObj2Num = i;
     }
     for ( i = 0; i < nOuts; i++ )
     {
-        assert( pOuts[i] < p->nPis );
+        assert( pOuts[i] < p->nCis );
         pBox->Inouts[nIns+i] = pOuts[i];
-        p->pPis[pOuts[i]].iObj2Box = pBox->iBox;
-        p->pPis[pOuts[i]].iObj2Num = i;
+        p->pCis[pOuts[i]].iObj2Box = pBox->iBox;
+        p->pCis[pOuts[i]].iObj2Num = i;
     }
 }
 
@@ -482,17 +560,17 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut,
     pBox->nOutputs = nOuts;
     for ( i = 0; i < nIns; i++ )
     {
-        assert( firstIn+i < p->nPos );
+        assert( firstIn+i < p->nCos );
         pBox->Inouts[i] = firstIn+i;
-        p->pPos[firstIn+i].iObj2Box = pBox->iBox;
-        p->pPos[firstIn+i].iObj2Num = i;
+        p->pCos[firstIn+i].iObj2Box = pBox->iBox;
+        p->pCos[firstIn+i].iObj2Num = i;
     }
     for ( i = 0; i < nOuts; i++ )
     {
-        assert( firstOut+i < p->nPis );
+        assert( firstOut+i < p->nCis );
         pBox->Inouts[nIns+i] = firstOut+i;
-        p->pPis[firstOut+i].iObj2Box = pBox->iBox;
-        p->pPis[firstOut+i].iObj2Num = i;
+        p->pCis[firstOut+i].iObj2Box = pBox->iBox;
+        p->pCis[firstOut+i].iObj2Num = i;
     }
 }
 
@@ -515,10 +593,10 @@ void Tim_ManIncrementTravId( Tim_Man_t * p )
     if ( p->nTravIds >= (1<<30)-1 )
     {
         p->nTravIds = 0;
-        for ( i = 0; i < p->nPis; i++ )
-            p->pPis[i].TravId = 0;
-        for ( i = 0; i < p->nPos; i++ )
-            p->pPos[i].TravId = 0;
+        for ( i = 0; i < p->nCis; i++ )
+            p->pCis[i].TravId = 0;
+        for ( i = 0; i < p->nCos; i++ )
+            p->pCos[i].TravId = 0;
     }
     assert( p->nTravIds < (1<<30)-1 );
     p->nTravIds++;
@@ -535,10 +613,10 @@ void Tim_ManIncrementTravId( Tim_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
+void Tim_ManInitCiArrival( Tim_Man_t * p, int iCi, float Delay )
 {
-    assert( iPi < p->nPis );
-    p->pPis[iPi].timeArr = Delay;
+    assert( iCi < p->nCis );
+    p->pCis[iCi].timeArr = Delay;
 }
 
 /**Function*************************************************************
@@ -552,10 +630,10 @@ void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
+void Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Delay )
 {
-    assert( iPo < p->nPos );
-    p->pPos[iPo].timeReq = Delay;
+    assert( iCo < p->nCos );
+    p->pCos[iCo].timeReq = Delay;
 }
 
 /**Function*************************************************************
@@ -569,12 +647,12 @@ void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
+void Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay )
 {
-    assert( iPo < p->nPos );
-    assert( !p->fUseTravId || p->pPos[iPo].TravId != p->nTravIds );
-    p->pPos[iPo].timeArr = Delay;
-    p->pPos[iPo].TravId = p->nTravIds;
+    assert( iCo < p->nCos );
+    assert( !p->fUseTravId || p->pCos[iCo].TravId != p->nTravIds );
+    p->pCos[iCo].timeArr = Delay;
+    p->pCos[iCo].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
@@ -588,12 +666,12 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
+void Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay )
 {
-    assert( iPi < p->nPis );
-    assert( !p->fUseTravId || p->pPis[iPi].TravId != p->nTravIds );
-    p->pPis[iPi].timeReq = Delay;
-    p->pPis[iPi].TravId = p->nTravIds;
+    assert( iCi < p->nCis );
+    assert( !p->fUseTravId || p->pCis[iCi].TravId != p->nTravIds );
+    p->pCis[iCi].timeReq = Delay;
+    p->pCis[iCi].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
@@ -607,12 +685,12 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay )
+void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay )
 {
-    assert( iPo < p->nPos );
-    assert( !p->fUseTravId || p->pPos[iPo].TravId != p->nTravIds );
-    p->pPos[iPo].timeReq = Delay;
-    p->pPos[iPo].TravId = p->nTravIds;
+    assert( iCo < p->nCos );
+    assert( !p->fUseTravId || p->pCos[iCo].TravId != p->nTravIds );
+    p->pCos[iCo].timeReq = Delay;
+    p->pCos[iCo].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
@@ -626,12 +704,12 @@ void Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay )
+void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay )
 {
     Tim_Obj_t * pObj;
     int i;
-    Tim_ManForEachPo( p, pObj, i )
-        Tim_ManSetPoRequired( p, i, Delay );
+    Tim_ManForEachCo( p, pObj, i )
+        Tim_ManSetCoRequired( p, i, Delay );
 }
 
 
@@ -646,19 +724,19 @@ void Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
+float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi )
 {
     Tim_Box_t * pBox;
     Tim_Obj_t * pObjThis, * pObj, * pObjRes;
     float * pDelays, DelayBest;
     int i, k;
     // consider the already processed PI
-    pObjThis = Tim_ManPi( p, iPi );
+    pObjThis = Tim_ManCi( p, iCi );
     if ( p->fUseTravId && pObjThis->TravId == p->nTravIds )
         return pObjThis->timeArr;
     pObjThis->TravId = p->nTravIds;
     // consider the main PI
-    pBox = Tim_ManPiBox( p, iPi );
+    pBox = Tim_ManCiBox( p, iCi );
     if ( pBox == NULL )
         return pObjThis->timeArr;
     // update box timing
@@ -667,12 +745,12 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
     if ( p->fUseTravId )
     Tim_ManBoxForEachInput( p, pBox, pObj, i )
         if ( pObj->TravId != p->nTravIds )
-            printf( "Tim_ManGetPiArrival(): Input arrival times of the box are not up to date!\n" );
+            printf( "Tim_ManGetCiArrival(): Input arrival times of the box are not up to date!\n" );
     // compute the arrival times for each output of the box (PIs)
     Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
     {
         pDelays = pBox->pDelayTable + i * pBox->nInputs;
-        DelayBest = -TIME_ETERNITY;
+        DelayBest = -TIM_ETERNITY;
         Tim_ManBoxForEachInput( p, pBox, pObj, k )
             DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
         pObjRes->timeArr = DelayBest;
@@ -692,19 +770,19 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
   SeeAlso     []
 
 ***********************************************************************/
-float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
+float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
 {
     Tim_Box_t * pBox;
     Tim_Obj_t * pObjThis, * pObj, * pObjRes;
     float * pDelays, DelayBest;
     int i, k;
     // consider the already processed PO
-    pObjThis = Tim_ManPo( p, iPo );
+    pObjThis = Tim_ManCo( p, iCo );
     if ( p->fUseTravId && pObjThis->TravId == p->nTravIds )
         return pObjThis->timeReq;
     pObjThis->TravId = p->nTravIds;
     // consider the main PO
-    pBox = Tim_ManPoBox( p, iPo );
+    pBox = Tim_ManCoBox( p, iCo );
     if ( pBox == NULL )
         return pObjThis->timeReq;
     // update box timing
@@ -713,11 +791,11 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
     if ( p->fUseTravId )
     Tim_ManBoxForEachOutput( p, pBox, pObj, i )
         if ( pObj->TravId != p->nTravIds )
-            printf( "Tim_ManGetPoRequired(): Output required times of the box are not up to date!\n" );
+            printf( "Tim_ManGetCoRequired(): Output required times of the box are not up to date!\n" );
     // compute the required times for each input of the box (POs)
     Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
     {
-        DelayBest = TIME_ETERNITY;
+        DelayBest = TIM_ETERNITY;
         Tim_ManBoxForEachOutput( p, pBox, pObj, k )
         {
             pDelays = pBox->pDelayTable + k * pBox->nInputs;
@@ -742,9 +820,9 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
 ***********************************************************************/
 int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
 {
-    if ( iCi >= p->nPis )
+    if ( iCi >= p->nCis )
         return -1;
-    return p->pPis[iCi].iObj2Box;
+    return p->pCis[iCi].iObj2Box;
 }
 
 /**Function*************************************************************
@@ -760,9 +838,9 @@ int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
 ***********************************************************************/
 int Tim_ManBoxForCo( Tim_Man_t * p, int iCo )
 {
-    if ( iCo >= p->nPos )
+    if ( iCo >= p->nCos )
         return -1;
-    return p->pPos[iCo].iObj2Box;
+    return p->pCos[iCo].iObj2Box;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index d73a89d8..3b9707e0 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -43,7 +43,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define TIME_ETERNITY 10000
+#define TIM_ETERNITY 10000
 
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
@@ -58,7 +58,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 ////////////////////////////////////////////////////////////////////////
 
 /*=== time.c ===========================================================*/
-extern Tim_Man_t *     Tim_ManStart( int nPis, int nPos );
+extern Tim_Man_t *     Tim_ManStart( int nCis, int nCos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fDiscrete );
 extern Tim_Man_t *     Tim_ManDupUnit( Tim_Man_t * p );
 extern Tim_Man_t *     Tim_ManDupApprox( Tim_Man_t * p );
@@ -68,18 +68,22 @@ extern void            Tim_ManTravIdDisable( Tim_Man_t * p );
 extern void            Tim_ManTravIdEnable( Tim_Man_t * p );
 extern void            Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox );
 extern void            Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetPreviousTravIdBoxInputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetPreviousTravIdBoxOutputs( Tim_Man_t * p, int iBox );
+extern int             Tim_ManIsCiTravIdCurrent( Tim_Man_t * p, int iCi );
+extern int             Tim_ManIsCoTravIdCurrent( Tim_Man_t * p, int iCo );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
 extern void            Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
 extern void            Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
 extern void            Tim_ManIncrementTravId( Tim_Man_t * p );
-extern void            Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay );
-extern void            Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay );
-extern void            Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay );
-extern void            Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay );
-extern void            Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay );
-extern void            Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay );
-extern float           Tim_ManGetPiArrival( Tim_Man_t * p, int iPi );
-extern float           Tim_ManGetPoRequired( Tim_Man_t * p, int iPo );
+extern void            Tim_ManInitCiArrival( Tim_Man_t * p, int iCi, float Delay );
+extern void            Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay );
+extern void            Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay );
+extern float           Tim_ManGetCiArrival( Tim_Man_t * p, int iCi );
+extern float           Tim_ManGetCoRequired( Tim_Man_t * p, int iCo );
 extern int             Tim_ManBoxForCi( Tim_Man_t * p, int iCo );
 extern int             Tim_ManBoxForCo( Tim_Man_t * p, int iCi );
 extern int             Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox );