Various changes.

7 files changed, 200 insertions, 27 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 8a5137fe..73602a03 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -171,6 +171,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vCoReqs;       // CO required times
     Vec_Int_t *    vCoArrs;       // CO arrival times
     Vec_Int_t *    vCoAttrs;      // CO attributes
+    Vec_Int_t *    vWeights;      // object attributes
     int            And2Delay;     // delay of the AND gate 
     float          DefInArrs;     // default PI arrival times
     float          DefOutReqs;    // default PO required times
@@ -179,6 +180,7 @@ struct Gia_Man_t_
     int            nTravIdsAlloc; // the number of trav IDs allocated
     Vec_Ptr_t *    vNamesIn;      // the input names 
     Vec_Ptr_t *    vNamesOut;     // the output names
+    Vec_Ptr_t *    vNamesNode;    // the node names
     Vec_Int_t *    vUserPiIds;    // numbers assigned to PIs by the user
     Vec_Int_t *    vUserPoIds;    // numbers assigned to POs by the user
     Vec_Int_t *    vUserFfIds;    // numbers assigned to FFs by the user
@@ -480,6 +482,8 @@ static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          {
 static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
 static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
 static inline int          Gia_ObjPhaseDiff( Gia_Man_t * p, int i, int k )     { return Gia_ManObj(p, i)->fPhase ^ Gia_ManObj(p, k)->fPhase; }
+static inline char *       Gia_ObjName( Gia_Man_t * p, int i )                 { return p->vNamesNode ? (char*)Vec_PtrEntry(p->vNamesNode, i) : NULL; }
+static inline char *       Gia_ObjNameObj( Gia_Man_t * p, Gia_Obj_t * pObj )   { return p->vNamesNode ? (char*)Vec_PtrEntry(p->vNamesNode, Gia_ObjId(p, pObj)) : NULL; }
 
 static inline int          Gia_ObjIsTerm( Gia_Obj_t * pObj )                   { return pObj->fTerm;                             } 
 static inline int          Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj )            { return!pObj->fTerm;                             } 
@@ -618,6 +622,8 @@ static inline void         Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id )
 static inline void         Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id )                { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1;                 }
 static inline int          Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id )                  { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds);           }
 static inline int          Gia_ObjIsTravIdPreviousId( Gia_Man_t * p, int Id )                 { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds - 1);       }
+static inline int          Gia_ObjUpdateTravIdCurrentId( Gia_Man_t * p, int Id )              { if ( Gia_ObjIsTravIdCurrentId(p, Id) )  return 1; Gia_ObjSetTravIdCurrentId(p, Id);  return 0; }
+static inline int          Gia_ObjUpdateTravIdPreviousId( Gia_Man_t * p, int Id )             { if ( Gia_ObjIsTravIdPreviousId(p, Id) ) return 1; Gia_ObjSetTravIdPreviousId(p, Id); return 0; }
 
 static inline void         Gia_ManTimeClean( Gia_Man_t * p )                                  { int i; assert( p->vTiming != NULL ); Vec_FltFill(p->vTiming, 3*Gia_ManObjNum(p), 0); for ( i = 0; i < Gia_ManObjNum(p); i++ )  Vec_FltWriteEntry( p->vTiming, 3*i+1, (float)(ABC_INFINITY) ); }
 static inline void         Gia_ManTimeStart( Gia_Man_t * p )                                  { assert( p->vTiming == NULL ); p->vTiming = Vec_FltAlloc(0); Gia_ManTimeClean( p );  }
@@ -1305,6 +1311,7 @@ extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo );
+extern Gia_Man_t *         Gia_ManDupDfsRehash( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value );  
 extern Gia_Man_t *         Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value );  
 extern Gia_Man_t *         Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 );
@@ -1567,6 +1574,7 @@ extern int                 Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, in
 extern int                 Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
 /*=== giaSimBase.c ============================================================*/
 extern Vec_Wrd_t *         Gia_ManSimPatSim( Gia_Man_t * p );
+extern Vec_Wrd_t *         Gia_ManSimPatSimOut( Gia_Man_t * pGia, Vec_Wrd_t * vSimsPi, int fOuts );
 /*=== giaSpeedup.c ============================================================*/
 extern float               Gia_ManDelayTraceLut( Gia_Man_t * p );
 extern float               Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index c2c0e969..1bb70612 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -176,7 +176,7 @@ Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits )
 Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck )
 {
     Gia_Man_t * pNew, * pTemp;
-    Vec_Ptr_t * vNamesIn = NULL, * vNamesOut = NULL, * vNamesRegIn = NULL, * vNamesRegOut = NULL;
+    Vec_Ptr_t * vNamesIn = NULL, * vNamesOut = NULL, * vNamesRegIn = NULL, * vNamesRegOut = NULL, * vNamesNode = NULL;
     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
     Vec_Int_t * vNodes, * vDrivers, * vInits = NULL;
     int iObj, iNode0, iNode1, fHieOnly = 0;
@@ -388,7 +388,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
                 char * pType = (char *)pCur;
                 char * pName = NULL;
                 // check terminal type
-                if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l'  )
+                if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l' && *pCur != 'n' )
                 {
                     fError = 1;
                     break;
@@ -442,6 +442,18 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
                     Vec_PtrPush( vNamesRegIn,  Abc_UtilStrsav(Buffer) );
                     Vec_PtrPush( vNamesRegOut, Abc_UtilStrsav(pName) );
                 }
+                else if ( *pType == 'n' )
+                {
+                    if ( Vec_IntSize(&pNew->vHTable) != 0 )
+                    {
+                        printf( "Structural hashing should be disabled to read internal nodes names.\n" );
+                        fError = 1;
+                        break;
+                    }
+                    if ( vNamesNode == NULL )
+                        vNamesNode = Vec_PtrStart( Gia_ManObjNum(pNew) );
+                    Vec_PtrWriteEntry( vNamesNode, iTerm, Abc_UtilStrsav(pName) );
+                }
                 else
                 {
                     fError = 1;
@@ -451,11 +463,12 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
             }
             if ( fError )
             {
-                printf( "Error occurred when reading signal names.\n" );
+                printf( "Error occurred when reading signal names. Signal names ignored.\n" );
                 if ( vNamesIn ) Vec_PtrFreeFree( vNamesIn ), vNamesIn = NULL;
                 if ( vNamesOut ) Vec_PtrFreeFree( vNamesOut ), vNamesOut = NULL;
                 if ( vNamesRegIn ) Vec_PtrFreeFree( vNamesRegIn ), vNamesRegIn = NULL;
                 if ( vNamesRegOut ) Vec_PtrFreeFree( vNamesRegOut ), vNamesRegOut = NULL;
+                if ( vNamesNode )    Vec_PtrFreeFree( vNamesNode ),    vNamesNode = NULL;
             }
         }
         else
@@ -976,6 +989,10 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
             vNamesRegIn = NULL;
         }
     }
+    if ( vNamesNode && Gia_ManObjNum(pNew) != Vec_PtrSize(vNamesNode) )
+        Abc_Print( 0, "The size of the node name array does not match the number of objects. Names are not entered.\n" );
+    else if ( vNamesNode )
+        pNew->vNamesNode = vNamesNode, vNamesNode = NULL;
     if ( vNamesIn ) Vec_PtrFreeFree( vNamesIn );
     if ( vNamesOut ) Vec_PtrFreeFree( vNamesOut );
     if ( vNamesRegIn ) Vec_PtrFreeFree( vNamesRegIn );
@@ -1311,6 +1328,14 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Gia_ManForEachPo( p, pObj, i )
             fprintf( pFile, "o%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesOut, i) );
     }
+    if ( p->vNamesNode && Vec_PtrSize(p->vNamesNode) != Gia_ManObjNum(p) )
+        Abc_Print( 0, "The size of the node name array does not match the number of objects. Names are not written.\n" );
+    else if ( p->vNamesNode )
+    {
+        Gia_ManForEachAnd( p, pObj, i )
+            if ( Vec_PtrEntry(p->vNamesNode, i) )
+                fprintf( pFile, "n%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesNode, i) );
+    }
 
     // write the comment
     if ( fWriteNewLine ) 
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index c1da11da..65eff161 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1610,6 +1610,52 @@ Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = p->nConstrs;
+    if ( p->pCexSeq )
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Cofactors w.r.t. a primary input variable.]
 
   Description []
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 2f2566d1..ae87277a 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -2222,10 +2222,11 @@ void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia )
         p->DefOutReqs  = pGia->DefOutReqs;
         p->And2Delay   = pGia->And2Delay;
     }
-    if ( pGia->vNamesIn || pGia->vNamesOut )
+    if ( pGia->vNamesIn || pGia->vNamesOut || pGia->vNamesNode )
     {
         p->vNamesIn     = pGia->vNamesIn;     pGia->vNamesIn     = NULL;
         p->vNamesOut    = pGia->vNamesOut;    pGia->vNamesOut    = NULL;
+        p->vNamesNode   = pGia->vNamesNode;   pGia->vNamesNode   = NULL;
     }
     if ( pGia->vConfigs || pGia->pCellStr )
     {
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index e4c9afd0..bb1305be 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -90,6 +90,7 @@ void Gia_ManStop( Gia_Man_t * p )
     assert( p->pManTime == NULL );
     Vec_PtrFreeFree( p->vNamesIn );
     Vec_PtrFreeFree( p->vNamesOut );
+    Vec_PtrFreeFree( p->vNamesNode );
     Vec_IntFreeP( &p->vSwitching );
     Vec_IntFreeP( &p->vSuper );
     Vec_IntFreeP( &p->vStore );
@@ -148,6 +149,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vCoReqs );
     Vec_IntFreeP( &p->vCoArrs );
     Vec_IntFreeP( &p->vCoAttrs );
+    Vec_IntFreeP( &p->vWeights );
     Gia_ManStopP( &p->pAigExtra );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
@@ -202,6 +204,7 @@ double Gia_ManMemory( Gia_Man_t * p )
     Memory += Vec_FltMemory( p->vOutReqs );
     Memory += Vec_PtrMemory( p->vNamesIn );
     Memory += Vec_PtrMemory( p->vNamesOut );
+    Memory += Vec_PtrMemory( p->vNamesNode );
     return Memory;
 }
 
diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index 06e002af..660440c3 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -558,11 +558,11 @@ int Gia_ManConstructFromMap( Gia_Man_t * pNew, Vec_Int_t * vGates, int nVars, Ve
     iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 );
     return iLitRes;
 }
-Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nVars )
+Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nDivs )
 {
     Vec_Int_t * vGates; int i, k, iLit;
     Vec_Int_t * vCopy = Vec_IntAlloc( 100 );
-    Vec_Int_t * vUsed = Vec_IntStartFull( nVars );
+    Vec_Int_t * vUsed = Vec_IntStartFull( nDivs );
     Gia_Man_t * pNew = Gia_ManStart( 100 );
     pNew->pName = Abc_UtilStrsav( "resub" );
     Vec_WecForEachLevel( vFuncs, vGates, i )
@@ -571,7 +571,7 @@ Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nVars )
         Vec_IntForEachEntry( vGates, iLit, k )
         {
             int iVar = Abc_Lit2Var(iLit);
-            if ( iVar > 0 && iVar < nVars && Vec_IntEntry(vUsed, iVar) == -1 )
+            if ( iVar > 0 && iVar < nDivs && Vec_IntEntry(vUsed, iVar) == -1 )
                 Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) );
         }
     }
@@ -580,16 +580,77 @@ Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nVars )
         int iLitRes, iTopLit = Vec_IntEntryLast( vGates );
         if ( Abc_Lit2Var(iTopLit) == 0 )
             iLitRes = 0;
-        else if ( Abc_Lit2Var(iTopLit) < nVars )
-            iLitRes = Gia_ManAppendCi(pNew);
+        else if ( Abc_Lit2Var(iTopLit) < nDivs )
+            iLitRes = Vec_IntEntry( vUsed, Abc_Lit2Var(iTopLit) );
         else
-            iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 0 );
+            iLitRes = Gia_ManConstructFromMap( pNew, vGates, nDivs, vUsed, vCopy, 0 );
         Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) );
     }
     Vec_IntFree( vCopy );
     Vec_IntFree( vUsed );
     return pNew;
 }
+Gia_Man_t * Gia_ManConstructFromGates2( Vec_Wec_t * vFuncs, Vec_Wec_t * vDivs, int nObjs, Vec_Int_t ** pvSupp )
+{
+    Vec_Int_t * vGates; int i, k, iVar, iLit;
+    Vec_Int_t * vSupp  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vCopy  = Vec_IntAlloc( 100 );
+    Vec_Wec_t * vUseds = Vec_WecStart( Vec_WecSize(vDivs) );
+    Vec_Int_t * vMap   = Vec_IntStartFull( nObjs );
+    Gia_Man_t * pNew   = Gia_ManStart( 100 );
+    pNew->pName = Abc_UtilStrsav( "resub" );
+    assert( Vec_WecSize(vFuncs) == Vec_WecSize(vDivs) );
+    Vec_WecForEachLevel( vFuncs, vGates, i )
+    {
+        Vec_Int_t * vDiv = Vec_WecEntry( vDivs, i );
+        assert( Vec_IntSize(vGates) % 2 == 1 );
+        Vec_IntForEachEntry( vGates, iLit, k )
+        {
+            int iVar = Abc_Lit2Var(iLit);
+            if ( iVar > 0 && iVar < Vec_IntSize(vDiv) && Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) == -1 )
+                Vec_IntWriteEntry( vMap, Vec_IntPushReturn(vSupp, Vec_IntEntry(vDiv, iVar)), 0 );
+        }
+    }
+    Vec_IntSort( vSupp, 0 );
+    Vec_IntForEachEntry( vSupp, iVar, k )
+        Vec_IntWriteEntry( vMap, iVar, Gia_ManAppendCi(pNew) );
+    Vec_WecForEachLevel( vFuncs, vGates, i )
+    {
+        Vec_Int_t * vDiv  = Vec_WecEntry( vDivs, i );
+        Vec_Int_t * vUsed = Vec_WecEntry( vUseds, i );
+        Vec_IntFill( vUsed, Vec_IntSize(vDiv), -1 );
+        Vec_IntForEachEntry( vGates, iLit, k )
+        {
+            int iVar = Abc_Lit2Var(iLit);
+            if ( iVar > 0 && iVar < Vec_IntSize(vDiv) )
+            {
+                assert( Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) > 0 );
+                Vec_IntWriteEntry( vUsed, iVar, Vec_IntEntry(vMap, Vec_IntEntry(vDiv, iVar)) );
+            }
+        }
+    }
+    Vec_WecForEachLevel( vFuncs, vGates, i )
+    {
+        Vec_Int_t * vDiv  = Vec_WecEntry( vDivs, i );
+        Vec_Int_t * vUsed = Vec_WecEntry( vUseds, i );
+        int iLitRes, iTopLit = Vec_IntEntryLast( vGates );
+        if ( Abc_Lit2Var(iTopLit) == 0 )
+            iLitRes = 0;
+        else if ( Abc_Lit2Var(iTopLit) < Vec_IntSize(vDiv) )
+            iLitRes = Vec_IntEntry( vUsed, Abc_Lit2Var(iTopLit) );
+        else
+            iLitRes = Gia_ManConstructFromMap( pNew, vGates, Vec_IntSize(vDiv), vUsed, vCopy, 0 );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) );
+    }
+    Vec_IntFree( vMap );
+    Vec_IntFree( vCopy );
+    Vec_WecFree( vUseds );
+    if ( pvSupp )
+        *pvSupp = vSupp;
+    else
+        Vec_IntFree( vSupp );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -1118,11 +1179,13 @@ int Gia_ManResubAddNode( Gia_ResbMan_t * p, int iLit0, int iLit1, int Type )
     Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iFan0, Type==1), Abc_LitNotCond(iFan1, Type==1) );
     return Abc_Var2Lit( iNode, Type==1 );
 }
-int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit )
+int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit, int Depth )
 {
-    extern int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit );
+    extern int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth );
     int iDivBest, iResLit0, iResLit1, nNodes;
     word * pDiv, * pCopy[2];
+    if ( Depth == 0 )
+        return -1;
     if ( nLimit < 3 )
         return -1;
     iDivBest = Gia_ManResubFindBestBinate( p );
@@ -1136,7 +1199,10 @@ int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit )
     Abc_TtAndSharp( p->pSets[0], pCopy[0], pDiv, p->nWords, !Abc_LitIsCompl(iDivBest) );
     Abc_TtAndSharp( p->pSets[1], pCopy[1], pDiv, p->nWords, !Abc_LitIsCompl(iDivBest) );
     nNodes = Vec_IntSize(p->vGates)/2;
-    iResLit0 = Gia_ManResubPerform_rec( p, nLimit-3 );
+    //iResLit0 = Gia_ManResubPerform_rec( p, nLimit-3 );
+    iResLit0 = Gia_ManResubPerform_rec( p, nLimit, 0 );
+    if ( iResLit0 == -1 )
+        iResLit0 = Gia_ManResubPerformMux_rec( p, nLimit, Depth-1 );
     if ( iResLit0 == -1 )
     {
         ABC_FREE( pCopy[0] );
@@ -1150,7 +1216,10 @@ int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit )
     nNodes = Vec_IntSize(p->vGates)/2 - nNodes;
     if ( nLimit-nNodes < 3 )
         return -1;
-    iResLit1 = Gia_ManResubPerform_rec( p, nLimit-3-nNodes );
+    //iResLit1 = Gia_ManResubPerform_rec( p, nLimit-3-nNodes );
+    iResLit1 = Gia_ManResubPerform_rec( p, nLimit, 0 );
+    if ( iResLit1 == -1 )
+        iResLit1 = Gia_ManResubPerformMux_rec( p, nLimit, Depth-1 );
     if ( iResLit1 == -1 )
         return -1;
     else
@@ -1172,7 +1241,7 @@ int Gia_ManResubPerformMux_rec( Gia_ResbMan_t * p, int nLimit )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
+int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth )
 {
     int TopOneW[2] = {0}, TopTwoW[2] = {0}, Max1, Max2, iResLit, nVars = Vec_PtrSize(p->vDivs);
     if ( p->fVerbose )
@@ -1205,7 +1274,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
         return Abc_Var2Lit( iNode, fComp );
     }
     Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars );
-    //return Gia_ManResubPerformMux_rec( p, nLimit );
+    if ( Depth )
+        return Gia_ManResubPerformMux_rec( p, nLimit, Depth );
     if ( Vec_IntSize(p->vBinateVars) > p->nDivsMax )
         Vec_IntShrink( p->vBinateVars, p->nDivsMax );
     if ( p->fVerbose ) printf( "  B = %3d", Vec_IntSize(p->vBinateVars) );
@@ -1304,7 +1374,7 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
             Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp );
             if ( p->fVerbose )
                 printf( "\n" ); 
-            iResLit = Gia_ManResubPerform_rec( p, nLimit-1 );
+            iResLit = Gia_ManResubPerform_rec( p, nLimit-1, Depth );
             if ( iResLit >= 0 ) 
             {
                 int iNode = nVars + Vec_IntSize(p->vGates)/2;
@@ -1348,7 +1418,7 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
             Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp );
             if ( p->fVerbose )
                 printf( "\n" ); 
-            iResLit = Gia_ManResubPerform_rec( p, nLimit-2 );
+            iResLit = Gia_ManResubPerform_rec( p, nLimit-2, Depth );
             if ( iResLit >= 0 ) 
             {
                 int iNode = nVars + Vec_IntSize(p->vGates)/2;
@@ -1383,11 +1453,11 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
     }
     return -1;
 }
-void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose )
+void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int Depth )
 {
     int Res;
     Gia_ResbInit( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, fVerbose );
-    Res = Gia_ManResubPerform_rec( p, nLimit );
+    Res = Gia_ManResubPerform_rec( p, nLimit, Depth );
     if ( Res >= 0 ) 
         Vec_IntPush( p->vGates, Res );
     else
@@ -1395,11 +1465,11 @@ void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int
     if ( fVerbose )
         printf( "\n" );
 }
-Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc )
+Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc, int Depth )
 {
     Vec_Int_t * vRes;
     Gia_ResbMan_t * p = Gia_ResbAlloc( nWords );
-    Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose );
+    Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, Depth );
     if ( fVerbose )
         Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) );
     if ( fVerbose )
@@ -1444,7 +1514,7 @@ int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit,
 {
     Vec_Ptr_t Divs = { nDivs, nDivs, ppDivs };
     assert( s_pResbMan != NULL ); // first call Abc_ResubPrepareManager()
-    Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2 );
+    Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2, 0 );
     if ( fVerbose )
     {
         int nGates = Vec_IntSize(s_pResbMan->vGates)/2;
@@ -1563,7 +1633,7 @@ void Gia_ManResubTest3_()
         printf( " " );
         Dau_DsdPrintFromTruth2( &Truth, 6 );
         printf( "       " );
-        Gia_ManResubPerform( p, vDivs, 1, 100, 0, 50, 1, 1, 0 );
+        Gia_ManResubPerform( p, vDivs, 1, 100, 0, 50, 1, 1, 0, 0 );
     }
     Gia_ResbFree( p );
     Vec_IntFree( vRes );
@@ -1604,7 +1674,7 @@ void Gia_ManResubPair( Vec_Wrd_t * vOn, Vec_Wrd_t * vOff, int nWords, int nIns )
             memmove( pSim+nWords, Vec_WrdEntryP(vOff, (i-2)*nWords), sizeof(word)*nWords );
         }
     }
-    Gia_ManResubPerform( p, vDivs, nWords*2, 100, 0, 50, 1, 1, 0 );
+    Gia_ManResubPerform( p, vDivs, nWords*2, 100, 0, 50, 1, 1, 0, 0 );
     Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) );
     printf( "\n" );
     //Vec_PtrFree( vDivs );
@@ -1672,7 +1742,7 @@ Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, i
         Vec_PtrShrink( vDivs, (1<<14)-1 );
     }
     assert( Vec_PtrSize(vDivs) < (1<<14) );
-    Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1 );
+    Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1, 0 );
     if ( Vec_IntSize(p->vGates) )
     {
         Vec_Wec_t * vGates = Vec_WecStart(1);
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 79377310..42318f5c 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -134,6 +134,27 @@ Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
         Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
     return vSims;
 }
+Vec_Wrd_t * Gia_ManSimPatSimOut( Gia_Man_t * pGia, Vec_Wrd_t * vSimsPi, int fOuts )
+{
+    Gia_Obj_t * pObj;
+    int i, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(pGia);
+    Vec_Wrd_t * vSimsCo = fOuts ? Vec_WrdStart( Gia_ManCoNum(pGia) * nWords ) : NULL;
+    Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
+    assert( Vec_WrdSize(vSimsPi) % Gia_ManCiNum(pGia) == 0 );
+    Gia_ManSimPatAssignInputs( pGia, nWords, vSims, vSimsPi );
+    Gia_ManForEachAnd( pGia, pObj, i ) 
+        Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims );
+    Gia_ManForEachCo( pGia, pObj, i )
+        Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
+    Gia_ManForEachCo( pGia, pObj, i )
+        Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
+    if ( !fOuts )
+        return vSims;
+    Gia_ManForEachCo( pGia, pObj, i )
+        memcpy( Vec_WrdEntryP(vSimsCo, i*nWords), Vec_WrdEntryP(vSims, Gia_ObjId(pGia, pObj)*nWords), sizeof(word)*nWords );
+    Vec_WrdFree( vSims );
+    return vSimsCo;
+}
 void Gia_ManSimPatResim( Gia_Man_t * pGia, Vec_Int_t * vObjs, int nWords, Vec_Wrd_t * vSims )
 {
     Gia_Obj_t * pObj; int i;
@@ -550,7 +571,6 @@ Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCex
     return vSimsRes;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []