Experimental resubstitution.

9 files changed, 1049 insertions, 5 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index ae9835ee..45291702 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1704,6 +1704,7 @@ extern int                 Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, i
 extern int                 Gia_ManCountPisWithFanout( Gia_Man_t * p );
 extern int                 Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
 extern void                Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
+extern Vec_Int_t *         Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index b8c0e294..4dd8951f 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -22,6 +22,7 @@
 #include "misc/vec/vecWec.h"
 #include "misc/vec/vecQue.h"
 #include "misc/vec/vecHsh.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -271,6 +272,214 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
 }
 
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resubstitution data-structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+typedef struct Gia_ResbMan_t_ Gia_ResbMan_t;
+struct Gia_ResbMan_t_
+{
+    int         nWords;
+    Vec_Ptr_t * vDivs;
+    Vec_Int_t * vGates;
+    Vec_Int_t * vUnateLits[2];
+    Vec_Int_t * vNotUnateVars[2];
+    Vec_Int_t * vUnatePairs[2];
+    Vec_Int_t * vBinateVars;
+    Vec_Int_t * vUnateLitsW[2];
+    Vec_Int_t * vUnatePairsW[2];
+    word *      pDivA;
+    word *      pDivB;
+};
+Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates )
+{
+    Gia_ResbMan_t * p   = ABC_CALLOC( Gia_ResbMan_t, 1 );
+    p->nWords           = nWords;
+    p->vDivs            = vDivs;
+    p->vGates           = vGates;
+    p->vUnateLits[0]    = Vec_IntAlloc( 100 );
+    p->vUnateLits[1]    = Vec_IntAlloc( 100 );
+    p->vNotUnateVars[0] = Vec_IntAlloc( 100 );
+    p->vNotUnateVars[1] = Vec_IntAlloc( 100 );
+    p->vUnatePairs[0]   = Vec_IntAlloc( 100 );
+    p->vUnatePairs[1]   = Vec_IntAlloc( 100 );
+    p->vUnateLitsW[0]   = Vec_IntAlloc( 100 );
+    p->vUnateLitsW[1]   = Vec_IntAlloc( 100 );
+    p->vUnatePairsW[0]  = Vec_IntAlloc( 100 );
+    p->vUnatePairsW[1]  = Vec_IntAlloc( 100 );
+    p->vBinateVars      = Vec_IntAlloc( 100 );
+    p->pDivA            = ABC_CALLOC( word, nWords );
+    p->pDivB            = ABC_CALLOC( word, nWords );
+    return p;
+}
+void Gia_ResbReset( Gia_ResbMan_t * p )
+{
+    Vec_IntClear( p->vUnateLits[0]    );
+    Vec_IntClear( p->vUnateLits[1]    );
+    Vec_IntClear( p->vNotUnateVars[0] );
+    Vec_IntClear( p->vNotUnateVars[1] );
+    Vec_IntClear( p->vUnatePairs[0]   );
+    Vec_IntClear( p->vUnatePairs[1]   );
+    Vec_IntClear( p->vUnateLitsW[0]   );
+    Vec_IntClear( p->vUnateLitsW[1]   );
+    Vec_IntClear( p->vUnatePairsW[0]  );
+    Vec_IntClear( p->vUnatePairsW[1]  );
+    Vec_IntClear( p->vBinateVars      );
+}
+void Gia_ResbFree( Gia_ResbMan_t * p )
+{
+    Vec_IntFree( p->vUnateLits[0]    );
+    Vec_IntFree( p->vUnateLits[1]    );
+    Vec_IntFree( p->vNotUnateVars[0] );
+    Vec_IntFree( p->vNotUnateVars[1] );
+    Vec_IntFree( p->vUnatePairs[0]   );
+    Vec_IntFree( p->vUnatePairs[1]   );
+    Vec_IntFree( p->vUnateLitsW[0]   );
+    Vec_IntFree( p->vUnateLitsW[1]   );
+    Vec_IntFree( p->vUnatePairsW[0]  );
+    Vec_IntFree( p->vUnatePairsW[1]  );
+    Vec_IntFree( p->vBinateVars      );
+    ABC_FREE( p->pDivA );
+    ABC_FREE( p->pDivB );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManResubVerify( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int iTopLit )
+{
+    int i, iLit0, iLit1, RetValue, nDivs = Vec_PtrSize(vDivs);
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    word * pDivRes; 
+    Vec_Wrd_t * vSims = NULL;
+    if ( iTopLit <= -1 )
+        return -1;
+    if ( iTopLit == 0 )
+        return Abc_TtIsConst0( pOnSet, nWords );
+    if ( iTopLit == 1 )
+        return Abc_TtIsConst0( pOffSet, nWords );
+    if ( Abc_Lit2Var(iTopLit) < nDivs )
+    {
+        assert( Vec_IntSize(vGates) == 0 );
+        pDivRes = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iTopLit) );
+    }
+    else
+    {
+        assert( Vec_IntSize(vGates) > 0 );
+        assert( Vec_IntSize(vGates) % 2 == 0 );
+        assert( Abc_Lit2Var(iTopLit)-nDivs == Vec_IntSize(vGates)/2-1 );
+        vSims = Vec_WrdStart( nWords * Vec_IntSize(vGates)/2 );
+        Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i )
+        {
+            int iVar0 = Abc_Lit2Var(iLit0);
+            int iVar1 = Abc_Lit2Var(iLit1);
+            word * pDiv0 = iVar0 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar0) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar0));
+            word * pDiv1 = iVar1 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar1) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar1));
+            word * pDiv  = Vec_WrdEntryP(vSims, nWords*i/2);
+            if ( iVar0 < iVar1 )
+                Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords );
+            else if ( iVar0 > iVar1 )
+            {
+                assert( !Abc_LitIsCompl(iLit0) );
+                assert( !Abc_LitIsCompl(iLit1) );
+                Abc_TtXor( pDiv, pDiv0, pDiv1, nWords, 0 );
+            }
+            else assert( 0 );
+        }
+        pDivRes = Vec_WrdEntryP( vSims, nWords*(Vec_IntSize(vGates)/2-1) );
+    }
+    if ( Abc_LitIsCompl(iTopLit) )
+        RetValue = !Abc_TtIntersectOne(pOnSet,  0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 1, nWords);
+    else
+        RetValue = !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOnSet,  0, pDivRes, 1, nWords);
+    Vec_WrdFreeP( &vSims );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Construct AIG manager from gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManGetVar( Gia_Man_t * pNew, Vec_Int_t * vUsed, int iVar )
+{
+    if ( Vec_IntEntry(vUsed, iVar) == -1 )
+        Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) );
+    return Vec_IntEntry(vUsed, iVar);
+}
+Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLit )
+{
+    int i, iLit0, iLit1, iLitRes;
+    Gia_Man_t * pNew = Gia_ManStart( 100 );
+    pNew->pName = Abc_UtilStrsav( "resub" );
+    assert( iTopLit >= 0 );
+    if ( iTopLit == 0 || iTopLit == 1 )
+        iLitRes = 0;
+    else if ( Abc_Lit2Var(iTopLit) < nVars )
+    {
+        assert( Vec_IntSize(vGates) == 0 );
+        iLitRes = Gia_ManAppendCi(pNew);
+    }
+    else
+    {
+        Vec_Int_t * vUsed = Vec_IntStartFull( nVars );
+        Vec_Int_t * vCopy = Vec_IntAlloc( Vec_IntSize(vGates)/2 );
+        assert( Vec_IntSize(vGates) > 0 );
+        assert( Vec_IntSize(vGates) % 2 == 0 );
+        assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 );
+        Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i )
+        {
+            int iVar0 = Abc_Lit2Var(iLit0);
+            int iVar1 = Abc_Lit2Var(iLit1);
+            int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, nVars - iVar0);
+            int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, nVars - iVar1);
+            if ( iVar0 < iVar1 )
+                iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) );
+            else if ( iVar0 > iVar1 )
+            {
+                assert( !Abc_LitIsCompl(iLit0) );
+                assert( !Abc_LitIsCompl(iLit1) );
+                iLitRes = Gia_ManAppendXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) );
+            }
+            else assert( 0 );
+            Vec_IntPush( vCopy, iLitRes );
+        }
+        assert( Vec_IntSize(vCopy) == Vec_IntSize(vGates)/2 );
+        iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 );
+        Vec_IntFree( vUsed );
+        Vec_IntFree( vCopy );
+    }
+    Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitRes, Abc_LitIsCompl(iTopLit)) );
+    return pNew;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Perform resubstitution.]
@@ -282,6 +491,492 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int * pStart1 = vArr1->pArray;
+    int * pStart2 = vArr2->pArray;
+    int nRemoved = 0;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) )
+        { 
+            if ( *pBeg1 != *pBeg2 ) 
+                return *pBeg1; 
+            else
+                pBeg1++, pBeg2++;
+            nRemoved++;
+        }
+        else if ( *pBeg1 < *pBeg2 )
+            *pStart1++ = *pBeg1++;
+        else 
+            *pStart2++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pStart1++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pStart2++ = *pBeg2++;
+    Vec_IntShrink( vArr1, pStart1 - vArr1->pArray );
+    Vec_IntShrink( vArr2, pStart2 - vArr2->pArray );
+    printf( "Removed %d duplicated entries.  Array1 = %d.  Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) );
+    return -1;
+}
+
+void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars )
+{
+    word * pDiv; int i;
+    Vec_IntClear( vUnateLits );
+    Vec_IntClear( vNotUnateVars );
+    Vec_PtrForEachEntryStart( word *, vDivs, pDiv, i, 2 )
+        if ( !Abc_TtIntersectOne( pOffSet, 0, pDiv, 0, nWords ) )
+            Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) );
+        else if ( !Abc_TtIntersectOne( pOffSet, 0, pDiv, 1, nWords ) )
+            Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) );
+        else
+            Vec_IntPush( vNotUnateVars, i );
+}
+int Gia_ManFindOneUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n;
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntClear( vUnateLits[n] );
+        Vec_IntClear( vNotUnateVars[n] );
+        Gia_ManFindOneUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vNotUnateVars[n] );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+        printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), n );
+    }
+    return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+}
+
+static inline int Gia_ManDivCover( word * pOffSet, word * pOnSet, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords )
+{
+    assert( !Abc_TtIntersectOne(pOffSet, 0, pDivA, ComplA, nWords) );
+    assert( !Abc_TtIntersectOne(pOffSet, 0, pDivB, ComplB, nWords) );
+    return !Abc_TtIntersectTwo( pOnSet, 0, pDivA, !ComplA, pDivB, !ComplB, nWords );
+}
+int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
+{
+    int i, k, iDiv0, iDiv1;
+    Vec_IntForEachEntry( vUnateLits, iDiv1, i )
+    Vec_IntForEachEntryStop( vUnateLits, iDiv0, k, i )
+    {
+        word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
+        word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1));
+        if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords) )
+            return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_LitNot(iDiv1), 0);
+    }
+    return -1;
+}
+int Gia_ManFindTwoUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n, iLit;
+    for ( n = 0; n < 2; n++ )
+    {
+        printf( "Trying %d pairs of %d-unate divs.\n", Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2, n );
+        iLit = Gia_ManFindTwoUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n] );
+        if ( iLit >= 0 )
+            return Abc_LitNotCond(iLit, !n);
+        ABC_SWAP( word *, pOffSet, pOnSet );
+    }
+    return -1;
+}
+
+void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
+{
+    int i, k, iDiv0, iDiv1;
+    Vec_IntClear( vUnateLits );
+    Vec_IntForEachEntry( vBinate, iDiv1, i )
+    Vec_IntForEachEntryStop( vBinate, iDiv0, k, i )
+    {
+        word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0);
+        word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1);
+        if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) )
+            Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 0) );
+        else if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 1, nWords ) )
+            Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 1) );
+    }
+}
+int Gia_ManFindXor( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n;
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntClear( vUnateLits[n] );
+        Gia_ManFindXorInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+        printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnateLits[n]), n );
+    }
+    return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+}
+
+void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
+{
+    int n, i, k, iDiv0, iDiv1;
+    Vec_IntClear( vUnateLits );
+    Vec_IntForEachEntry( vBinate, iDiv1, i )
+    Vec_IntForEachEntryStop( vBinate, iDiv0, k, i )
+    {
+        word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0);
+        word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1);
+        for ( n = 0; n < 4; n++ )
+        {
+            int iLit0 = Abc_Var2Lit( iDiv0, n&1 );
+            int iLit1 = Abc_Var2Lit( iDiv1, n>>1 );
+            if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, n&1, pDiv1, n>>1, nWords ) )
+                Vec_IntPush( vUnateLits, Abc_Var2Lit((iLit0 << 16) | iLit1, 0) );
+        }
+    }
+}
+void Gia_ManFindUnatePairs( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n, RetValue;
+    for ( n = 0; n < 2; n++ )
+    {
+        int nBefore = Vec_IntSize(vUnateLits[n]);
+        Gia_ManFindUnatePairsInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+        printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnateLits[n])-nBefore, n );
+    }
+    RetValue = Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+    assert( RetValue == -1 );
+}
+
+int Gia_ManFindAndGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, word * pDivTemp )
+{
+    int i, k, iDiv0, iDiv1;
+    Vec_IntForEachEntry( vUnateLits, iDiv0, i )
+    Vec_IntForEachEntry( vUnatePairs, iDiv1, k )
+    {
+        int fCompl = Abc_LitIsCompl(iDiv1);
+        int iDiv10 = Abc_Lit2Var(iDiv1) >> 16;
+        int iDiv11 = Abc_Lit2Var(iDiv1) & 0xFFF;
+        word * pDiv0  = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
+        word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10));
+        word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11));
+        Abc_TtAndCompl( pDivTemp, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords );
+        if ( Gia_ManDivCover(pOnSet, pOffSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fCompl, nWords) )
+            return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_Var2Lit(k, 1), 0);
+    }
+    return -1;
+}
+int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], word * pDivTemp )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n, iLit;
+    for ( n = 0; n < 2; n++ )
+    {
+        iLit = Gia_ManFindAndGateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp );
+        if ( iLit > 0 )
+            return Abc_LitNotCond( iLit, !n );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+    }
+    return -1;
+}
+
+int Gia_ManFindGateGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, word * pDivTempA, word * pDivTempB )
+{
+    int i, k, iDiv0, iDiv1;
+    Vec_IntForEachEntry( vUnatePairs, iDiv0, i )
+    {
+        int fCompA = Abc_LitIsCompl(iDiv0);
+        int iDiv00 = Abc_Lit2Var(iDiv0 >> 16);
+        int iDiv01 = Abc_Lit2Var(iDiv0 & 0xFFF);
+        word * pDiv00 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv00));
+        word * pDiv01 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv01));
+        Abc_TtAndCompl( pDivTempA, pDiv00, Abc_LitIsCompl(iDiv00), pDiv01, Abc_LitIsCompl(iDiv01), nWords );
+        Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, i )
+        {
+            int fCompB = Abc_LitIsCompl(iDiv1);
+            int iDiv10 = Abc_Lit2Var(iDiv1 >> 16);
+            int iDiv11 = Abc_Lit2Var(iDiv1 & 0xFFF);
+            word * pDiv0  = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
+            word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10));
+            word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11));
+            Abc_TtAndCompl( pDivTempB, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords );
+            if ( Gia_ManDivCover(pOnSet, pOffSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) )
+                return Abc_Var2Lit((iDiv1 << 16) | iDiv0, 0);
+        }
+    }
+    return -1;
+}
+int Gia_ManFindGateGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], word * pDivTempA, word * pDivTempB )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n, iLit;
+    for ( n = 0; n < 2; n++ )
+    {
+        iLit = Gia_ManFindGateGateInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+        if ( iLit > 0 )
+            return iLit;
+    }
+    return -1;
+}
+
+void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW )
+{
+    int i, iLit;
+    Vec_IntClear( vUnateLitsW );
+    Vec_IntForEachEntry( vUnateLits, iLit, i )
+    {
+        word * pDiv = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit) );
+        assert( !Abc_TtIntersectOne( pOffSet, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) );
+        Vec_IntPush( vUnateLitsW, Abc_TtCountOnesVecMask(pDiv, pOnSet, nWords, Abc_LitIsCompl(iLit)) );
+    }
+}
+void Gia_ManComputeLitWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n;
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntClear( vUnateLitsW[n] );
+        Gia_ManComputeLitWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnateLitsW[n] );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+    }
+    for ( n = 0; n < 2; n++ )
+    {
+        int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) );
+        Abc_ReverseOrder( pPerm, Vec_IntSize(vUnateLitsW[n]) );
+        printf( "Top 10 %d-unate:\n", n );
+        for ( i = 0; i < 10 && i < Vec_IntSize(vUnateLits[n]); i++ )
+        {
+            printf( "%5d : ", i );
+            printf( "Obj = %5d  ",  Vec_IntEntry(vUnateLits[n], pPerm[i]) );
+            printf( "Cost = %5d\n", Vec_IntEntry(vUnateLitsW[n], pPerm[i]) );
+        }
+        ABC_FREE( pPerm );
+    }
+}
+
+void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW )
+{
+    int i, iPair;
+    Vec_IntClear( vUnatePairsW );
+    Vec_IntForEachEntry( vUnatePairs, iPair, i )
+    {
+        int fCompl = Abc_LitIsCompl(iPair);
+        int Pair = Abc_Lit2Var(iPair);
+        int iLit0 = Pair >> 16;
+        int iLit1 = Pair & 0xFFFF;
+        word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) );
+        word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) );
+        if ( iLit0 < iLit1 )
+        {
+            assert( !fCompl );
+            assert( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) );
+            Vec_IntPush( vUnatePairsW, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOnSet, nWords) );
+        }
+        else
+        {
+            assert( !Abc_LitIsCompl(iLit0) );
+            assert( !Abc_LitIsCompl(iLit1) );
+            assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) );
+            Vec_IntPush( vUnatePairsW, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fCompl, pOnSet, nWords) );
+        }
+    }
+}
+void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2] )
+{
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int n;
+    for ( n = 0; n < 2; n++ )
+    {
+        Gia_ManComputePairWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] );
+        ABC_SWAP( word *, pOffSet, pOnSet );
+    }
+    for ( n = 0; n < 2; n++ )
+    {
+        int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) );
+        Abc_ReverseOrder( pPerm, Vec_IntSize(vUnatePairsW[n]) );
+        printf( "Top 10 %d-unate:\n", n );
+        for ( i = 0; i < 10 && i < Vec_IntSize(vUnatePairs[n]); i++ )
+        {
+            printf( "%5d : ", i );
+            printf( "Obj = %5d  ",  Vec_IntEntry(vUnatePairs[n], pPerm[i]) );
+            printf( "Cost = %5d\n", Vec_IntEntry(vUnatePairsW[n], pPerm[i]) );
+        }
+        ABC_FREE( pPerm );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Perform resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManResubInt2( Vec_Ptr_t * vDivs, int nWords, int NodeLimit, int ChoiceType, Vec_Int_t * vGates )
+{
+    return 0;
+}
+int Gia_ManResubInt( Gia_ResbMan_t * p )
+{
+    int nDivs = Vec_PtrSize(p->vDivs);
+    int iResLit = Gia_ManFindOneUnate( p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars );
+    if ( iResLit >= 0 ) // buffer
+    {
+        printf( "Creating %s (%d).\n", Abc_LitIsCompl(iResLit) ? "inverter" : "buffer", Abc_Lit2Var(iResLit) );
+        return iResLit;
+    }
+    iResLit = Gia_ManFindTwoUnate( p->vDivs, p->nWords, p->vUnateLits );
+    if ( iResLit >= 0 ) // and
+    {
+        int fCompl = Abc_LitIsCompl(iResLit);
+        int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
+        int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
+        Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
+        printf( "Creating one AND-gate.\n" );
+        return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl );
+    }
+    Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars );
+    if ( Vec_IntSize(p->vBinateVars) > 1000 )
+    {
+        printf( "Reducing binate divs from %d to 1000.\n", Vec_IntSize(p->vBinateVars) );
+        Vec_IntShrink( p->vBinateVars, 1000 );
+    }
+    iResLit = Gia_ManFindXor( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs );
+    if ( iResLit >= 0 ) // xor
+    {
+        int fCompl = Abc_LitIsCompl(iResLit);
+        int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
+        int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
+        assert( !Abc_LitIsCompl(iDiv0) );
+        assert( !Abc_LitIsCompl(iDiv1) );
+        Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); // xor
+        printf( "Creating one XOR-gate.\n" );
+        return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl );
+    }
+    Gia_ManFindUnatePairs( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs );
+/*
+    iResLit = Gia_ManFindAndGate( p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA );
+    if ( iResLit >= 0 ) // and-gate
+    {
+        int New = nDivs + Vec_IntSize(p->vGates)/2;
+        int fCompl = Abc_LitIsCompl(iResLit);
+        int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
+        int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
+        Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv1), Abc_LitNot(iDiv0) );
+        Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv0), New );
+        printf( "Creating one two gates.\n" );
+        return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, 1 );
+    }
+    iResLit = Gia_ManFindGateGate( p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB );
+    if ( iResLit >= 0 ) // and-(gate,gate)
+    {
+        printf( "Creating one three gates.\n" );
+        return -1;
+    }
+*/
+    Gia_ManComputeLitWeights( p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW );
+    Gia_ManComputePairWeights( p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Top level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCheckResub( Vec_Ptr_t * vDivs, int nWords )
+{
+    int i, Set[10] = { 2, 189, 2127, 2125, 177, 178 };
+    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
+    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    Vec_Int_t * vValue = Vec_IntStartFull( 1 << 6 );
+    printf( "Verifying resub:\n" );
+    for ( i = 0; i < 64*nWords; i++ )
+    {
+        int v, Mint = 0, Value = Abc_TtGetBit(pOnSet, i);
+        if ( !Abc_TtGetBit(pOffSet, i) && !Value )
+            continue;
+        for ( v = 0; v < 6; v++ )
+            if ( Abc_TtGetBit((word *)Vec_PtrEntry(vDivs, Set[v]), i) )
+                Mint |= 1 << v;
+        if ( Vec_IntEntry(vValue, Mint) == -1 )
+            Vec_IntWriteEntry(vValue, Mint, Value);
+        else if ( Vec_IntEntry(vValue, Mint) != Value )
+            printf( "Mismatch in pattern %d\n", i );
+    }
+    printf( "Finished verifying resub.\n" );
+    Vec_IntFree( vValue );
+}
+Vec_Ptr_t * Gia_ManDeriveDivs( Vec_Wrd_t * vSims, int nWords )
+{
+    int i, nDivs = Vec_WrdSize(vSims)/nWords;
+    Vec_Ptr_t * vDivs = Vec_PtrAlloc( nDivs );
+    for ( i = 0; i < nDivs; i++ )
+        Vec_PtrPush( vDivs, Vec_WrdEntryP(vSims, nWords*i) );
+    return vDivs;
+}
+Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose )
+{
+    return NULL;
+}
+Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose )
+{
+    extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords );
+    int iTopLit, nWords = 0;
+    Gia_Man_t * pMan   = NULL;
+    Vec_Wrd_t * vSims  = Gia_ManSimPatRead( pFileName, &nWords );
+    Vec_Ptr_t * vDivs  = vSims ? Gia_ManDeriveDivs( vSims, nWords ) : NULL;
+    Vec_Int_t * vGates = vDivs ? Vec_IntAlloc( 100 ) : NULL;
+    Gia_ResbMan_t * p  = vDivs ? Gia_ResbAlloc( vDivs, nWords, vGates ) : NULL;
+    if ( p == NULL )
+        return NULL;
+    assert( Vec_PtrSize(vDivs) < (1<<15) );
+    printf( "OFF = %5d (%6.2f %%)  ", Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 0), nWords), 100.0*Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 0), nWords)/(64*nWords) );
+    printf( "ON = %5d (%6.2f %%)\n",  Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 1), nWords), 100.0*Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 1), nWords)/(64*nWords) );
+    if ( Vec_PtrSize(vDivs) > 4000 )
+    {
+        printf( "Reducing all divs from %d to 4000.\n", Vec_PtrSize(vDivs) );
+        Vec_PtrShrink( vDivs, 4000 );
+    }
+    Gia_ResbReset( p );
+//    Gia_ManCheckResub( vDivs, nWords );
+    iTopLit = Gia_ManResubInt( p );
+    if ( iTopLit >= 0 )
+    {
+        printf( "Verification %s.\n", Gia_ManResubVerify( vDivs, nWords, vGates, iTopLit ) ? "succeeded" : "FAILED" );
+        pMan = Gia_ManConstructFromGates( Vec_PtrSize(vDivs), vGates, iTopLit );
+    }
+    else
+        printf( "Decomposition did not succeed.\n" );
+    Gia_ResbFree( p );
+    Vec_IntFree( vGates );
+    Vec_PtrFree( vDivs );
+    Vec_WrdFree( vSims );
+    return pMan;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index c53c1db8..f9539faf 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -343,7 +343,7 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
     for ( i = 0; i < nNodes; i++ )
         Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
     fclose( pFile );
-    printf( "Written %d words of simulation data into file \"%s\".\n", nWords, pFileName );
+    printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(vSimsIn)/nWords, pFileName );
 }
 int Gia_ManSimPatReadOne( char c )
 {
@@ -358,7 +358,7 @@ int Gia_ManSimPatReadOne( char c )
     assert( Digit >= 0 && Digit < 16 );
     return Digit;
 }
-Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
+Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords )
 {
     Vec_Wrd_t * vSimsIn = NULL; 
     int c, nWords = -1, nChars = 0; word Num = 0;
@@ -384,7 +384,9 @@ Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
     }
     assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
     fclose( pFile );
-    printf( "Read %d words of simulation data.\n", nWords );
+    printf( "Read %d words of simulation data for %d objects.\n", nWords, Vec_WrdSize(vSimsIn)/nWords );
+    if ( pnWords )
+        *pnWords = nWords;
     return vSimsIn;
 }
 
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index d0ec969f..5ee20e6a 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -2290,6 +2290,94 @@ Gia_Man_t * Gia_ManDupWithMuxPos( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect distance info.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRingAdd( Gia_Man_t * p, int iObj, Vec_Int_t * vRes, Vec_Int_t * vDists, int Dist )
+{
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    Vec_IntWriteEntry( vDists, iObj, Dist );
+    Vec_IntPush( vRes, iObj );
+}
+void Gia_ManCollectRing( Gia_Man_t * p, Vec_Int_t * vStart, Vec_Int_t * vRes, Vec_Int_t * vDists )
+{
+    int i, k, iObj, iFan;
+    Vec_IntForEachEntry( vStart, iObj, i )
+    {
+        int Weight = Vec_IntEntry( vDists, iObj );
+        Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+        assert( Weight > 0 );
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ManRingAdd( p, Gia_ObjFaninId0(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin0(pObj)) );
+            Gia_ManRingAdd( p, Gia_ObjFaninId1(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin1(pObj)) );
+        }
+        Gia_ObjForEachFanoutStaticId( p, iObj, iFan, k )
+            Gia_ManRingAdd( p, iFan, vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ManObj(p, iFan)) );
+    }
+}
+Vec_Int_t * Gia_ManComputeDistanceInt( Gia_Man_t * p, int iTarg, Vec_Int_t * vObjs, int fVerbose )
+{
+    int i, iObj;
+    Vec_Int_t * vDists, * vStart, * vNexts;
+    vStart = Vec_IntAlloc( 100 );
+    vNexts = Vec_IntAlloc( 100 );
+    vDists = Vec_IntStart( Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    if ( vObjs )
+    {
+        Vec_IntForEachEntry( vObjs, iObj, i )
+        {
+            Gia_ObjSetTravIdCurrentId(p, iObj);
+            Vec_IntWriteEntry( vDists, iObj, 1 );
+            Vec_IntPush( vStart, iObj );
+        }
+    }
+    else
+    {
+        Gia_ObjSetTravIdCurrentId(p, iTarg);
+        Vec_IntWriteEntry( vDists, iTarg, 1 );
+        Vec_IntPush( vStart, iTarg );
+    }
+    for ( i = 0; ; i++ )
+    {
+        if ( fVerbose )
+            printf( "Ring %2d : %6d\n", i, Vec_IntSize(vDists)-Vec_IntCountZero(vDists) );        
+        Gia_ManCollectRing( p, vStart, vNexts, vDists );
+        if ( Vec_IntSize(vNexts) == 0 )
+            break;
+        Vec_IntClear( vStart );
+        ABC_SWAP( Vec_Int_t, *vStart, *vNexts );
+    }
+    Vec_IntFree( vStart );
+    Vec_IntFree( vNexts );
+    return vDists;
+}
+Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose )
+{
+    Vec_Int_t * vDists;
+    if ( p->vFanoutNums )
+        vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose );
+    else
+    {
+        Gia_ManStaticFanoutStart( p );
+        vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose );
+        Gia_ManStaticFanoutStop( p );
+    }
+    return vDists;
+}
+
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 85053e18..70ef45ca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -437,6 +437,7 @@ static int Abc_CommandAbc9Shrink             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Fx                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Balance            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BalanceLut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resub              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn2               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn4               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1156,6 +1157,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&fx",           Abc_CommandAbc9Fx,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&b",            Abc_CommandAbc9Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&blut",         Abc_CommandAbc9BalanceLut,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&resub",        Abc_CommandAbc9Resub,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn2",         Abc_CommandAbc9Syn2,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn3",         Abc_CommandAbc9Syn3,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn4",         Abc_CommandAbc9Syn4,         0 );
@@ -34780,6 +34782,104 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Resub( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose );
+    extern Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose );
+    Gia_Man_t * pTemp;
+    int nNodes       =  0;
+    int nSupp        =  0;
+    int nDivs        =  0;
+    int c, fVerbose  =  0;
+    int fVeryVerbose =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NSDvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-N\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodes < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-S\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nSupp = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSupp < 0 )
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nDivs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nDivs < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pTemp = Gia_ManResub1( argv[globalUtilOptind], nNodes, nSupp, nDivs, fVerbose, fVeryVerbose );
+        Abc_FrameUpdateGia( pAbc, pTemp );
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Resub(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManResub2( pAbc->pGia, nNodes, nSupp, nDivs, fVerbose, fVeryVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &resub [-NSD num] [-vwh]\n" );
+    Abc_Print( -2, "\t           performs AIG resubstitution\n" );
+    Abc_Print( -2, "\t-N num   : the limit on added nodes (num >= 0) [default = %d]\n",     nNodes );
+    Abc_Print( -2, "\t-S num   : the limit on support size (num > 0) [default = %d]\n",     nSupp );
+    Abc_Print( -2, "\t-D num   : the limit on divisor count (num > 0) [default = %d]\n",    nDivs );
+    Abc_Print( -2, "\t-v       : toggles printing verbose information [default = %s]\n",    fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 8f72a00f..485a5e4e 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -1541,7 +1541,7 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve
     {
         if ( iMint == 1000 )
         {
-            //if ( Vec_IntSize(vDivVars) == 0 )
+            if ( Vec_IntSize(vDivVars) == 0 )
             {
                 printf( "Assuming constant 0 function.\n" );
                 Vec_StrClear( vTempSop );
@@ -2511,7 +2511,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4]
 
     abctime clk  = Abc_Clock();
     int nTargets = Vec_IntSize(&pNtkF->vTargets);
-    int TimeOut  = fCisOnly ? 0 : 60;  // 60 seconds
+    int TimeOut  = fCisOnly ? 0 : 120;  // 60 seconds
     int RetValue = 1;
 
     // compute various sets of nodes
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 2243541b..8a51bd3e 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -671,6 +671,8 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
         int nTargets = Vec_IntSize(&pNtkF->vTargets);
         Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF, fUseBuf, fUseXors, &pNtkF->vTargets, 0 );
         Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG, 0,       0,        NULL, nTargets );
+        pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pDesign->pSpec );
+        pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pDesign->pSpec );
         assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
         assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
         *ppGiaF  = pGiaF;
@@ -784,6 +786,8 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
         Gia_Man_t * pGiaG = Abc_NtkToGia2( pNtkG, 0 );
         assert( Abc_NtkCiNum(pNtkF) == Abc_NtkCiNum(pNtkG) );
         assert( Abc_NtkCoNum(pNtkF) == Abc_NtkCoNum(pNtkG) );
+        pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pSpec );
+        pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pSpec );
         *ppGiaF  = pGiaF;
         *ppGiaG  = pGiaG;
         *pvNodes = Abc_NtkCollectCopies( pNtkF, pGiaF, pvNodesR, pvPolar );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index e0ee1720..425ec27d 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -365,6 +365,141 @@ static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCo
     }
     return 0;
 }
+static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
+{
+    int w;
+    if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords )
+{
+    int w;
+    if ( fComp0 && fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else 
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords )
+{
+    int w;
+    if ( fComp01 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
 static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
 {
     int w;
@@ -1869,6 +2004,17 @@ static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
         Count += Abc_TtCountOnes( x[w] ^ y[w] );
     return Count;
 }
+static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords )
+{
+    int w, Count = 0;
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) );
+    else
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) );
+    return Count;
+}
 static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords )
 {
     int w, Count = 0;
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 514ce455..7125593b 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1397,6 +1397,14 @@ static inline void Vec_IntSortMulti( Vec_Int_t * p, int nMulti, int fReverse )
         qsort( (void *)p->pArray, (size_t)(p->nSize/nMulti), nMulti*sizeof(int), 
                 (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
 }
+static inline int Vec_IntIsSorted( Vec_Int_t * p, int fReverse )
+{
+    int i;
+    for ( i = 1; i < p->nSize; i++ )
+        if ( fReverse ? (p->pArray[i-1] < p->pArray[i]) : (p->pArray[i-1] > p->pArray[i]) )
+            return 0;
+    return 1;            
+}
 
 /**Function*************************************************************