Experimental resubstitution.

2 files changed, 450 insertions, 233 deletions

diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index 092603ed..7b57db15 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -26,7 +26,6 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -290,6 +289,7 @@ typedef struct Gia_ResbMan_t_ Gia_ResbMan_t;
 struct Gia_ResbMan_t_
 {
     int         nWords;
+    int         fVerbose;
     Vec_Ptr_t * vDivs;
     Vec_Int_t * vGates;
     Vec_Int_t * vUnateLits[2];
@@ -298,15 +298,15 @@ struct Gia_ResbMan_t_
     Vec_Int_t * vBinateVars;
     Vec_Int_t * vUnateLitsW[2];
     Vec_Int_t * vUnatePairsW[2];
+    word *      pSets[2];
     word *      pDivA;
     word *      pDivB;
+    Vec_Wrd_t * vSims;
 };
-Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates )
+Gia_ResbMan_t * Gia_ResbAlloc( int nWords )
 {
     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 );
@@ -318,12 +318,22 @@ Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates
     p->vUnatePairsW[0]  = Vec_IntAlloc( 100 );
     p->vUnatePairsW[1]  = Vec_IntAlloc( 100 );
     p->vBinateVars      = Vec_IntAlloc( 100 );
+    p->pSets[0]         = ABC_CALLOC( word, nWords );
+    p->pSets[1]         = ABC_CALLOC( word, nWords );
     p->pDivA            = ABC_CALLOC( word, nWords );
     p->pDivB            = ABC_CALLOC( word, nWords );
+    p->vSims            = Vec_WrdAlloc( 100 );
     return p;
 }
-void Gia_ResbReset( Gia_ResbMan_t * p )
+void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int fVerbose )
 {
+    assert( p->nWords == nWords );
+    p->fVerbose = fVerbose;
+    Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 );
+    Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 );
+    p->vDivs  = vDivs;
+    p->vGates = vGates;
+    Vec_IntClear( p->vGates );
     Vec_IntClear( p->vUnateLits[0]    );
     Vec_IntClear( p->vUnateLits[1]    );
     Vec_IntClear( p->vNotUnateVars[0] );
@@ -349,6 +359,9 @@ void Gia_ResbFree( Gia_ResbMan_t * p )
     Vec_IntFree( p->vUnatePairsW[0]  );
     Vec_IntFree( p->vUnatePairsW[1]  );
     Vec_IntFree( p->vBinateVars      );
+    Vec_WrdFree( p->vSims            );
+    ABC_FREE( p->pSets[0] );
+    ABC_FREE( p->pSets[1] );
     ABC_FREE( p->pDivA );
     ABC_FREE( p->pDivB );
     ABC_FREE( p );
@@ -356,6 +369,61 @@ void Gia_ResbFree( Gia_ResbMan_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Print resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl )
+{
+    extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit );
+    int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 );
+    int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 );
+    assert( iLit0 != iLit1 );
+    if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor
+    {
+        printf( "~" );
+        fCompl = 0;
+    }
+    printf( "(" );
+    Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) );
+    printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') );
+    Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) );
+    printf( ")" );
+}
+void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit )
+{
+    if ( Abc_Lit2Var(iLit) < nVars )
+    {
+        if ( nVars < 26 )
+            printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 );
+        else
+            printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 );
+    }
+    else
+        Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) );
+}
+int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars )
+{
+    int iTopLit;
+    if ( Vec_IntSize(vRes) == 0 )
+        return printf( "none" );
+    assert( Vec_IntSize(vRes) % 2 == 1 );
+    iTopLit = Vec_IntEntryLast(vRes);
+    if ( iTopLit == 0 )
+        return printf( "const0" );
+    if ( iTopLit == 1 )
+        return printf( "const1" );
+    Gia_ManResubPrintLit( vRes, nVars, iTopLit );
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Verify resubstitution.]
 
   Description []
@@ -365,54 +433,54 @@ void Gia_ResbFree( Gia_ResbMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManResubVerify( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int iTopLit )
+int Gia_ManResubVerify( Gia_ResbMan_t * p )
 {
-    int i, iLit0, iLit1, RetValue, nDivs = Vec_PtrSize(vDivs);
-    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
-    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
+    int nVars = Vec_PtrSize(p->vDivs);
+    int iTopLit, RetValue;
     word * pDivRes; 
-    Vec_Wrd_t * vSims = NULL;
-    if ( iTopLit <= -1 )
+    if ( Vec_IntSize(p->vGates) == 0 )
         return -1;
+    iTopLit = Vec_IntEntryLast(p->vGates);
+    assert( iTopLit >= 0 );
     if ( iTopLit == 0 )
-        return Abc_TtIsConst0( pOnSet, nWords );
+        return Abc_TtIsConst0( p->pSets[1], p->nWords );
     if ( iTopLit == 1 )
-        return Abc_TtIsConst0( pOffSet, nWords );
-    if ( Abc_Lit2Var(iTopLit) < nDivs )
+        return Abc_TtIsConst0( p->pSets[0], p->nWords );
+    if ( Abc_Lit2Var(iTopLit) < nVars )
     {
-        assert( Vec_IntSize(vGates) == 0 );
-        pDivRes = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iTopLit) );
+        assert( Vec_IntSize(p->vGates) == 1 );
+        pDivRes = (word *)Vec_PtrEntry( p->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 i, iLit0, iLit1;
+        assert( Vec_IntSize(p->vGates) > 1 );
+        assert( Vec_IntSize(p->vGates) % 2 == 1 );
+        assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 );
+        Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 );
+        Vec_IntForEachEntryDouble( p->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);
+            word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars));
+            word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars));
+            word * pDiv  = Vec_WrdEntryP(p->vSims, p->nWords*i/2);
             if ( iVar0 < iVar1 )
-                Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords );
+                Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords );
             else if ( iVar0 > iVar1 )
             {
                 assert( !Abc_LitIsCompl(iLit0) );
                 assert( !Abc_LitIsCompl(iLit1) );
-                Abc_TtXor( pDiv, pDiv0, pDiv1, nWords, 0 );
+                Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 );
             }
             else assert( 0 );
         }
-        pDivRes = Vec_WrdEntryP( vSims, nWords*(Vec_IntSize(vGates)/2-1) );
+        pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) );
     }
     if ( Abc_LitIsCompl(iTopLit) )
-        RetValue = !Abc_TtIntersectOne(pOnSet,  0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 1, nWords);
+        RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords);
     else
-        RetValue = !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOnSet,  0, pDivRes, 1, nWords);
-    Vec_WrdFreeP( &vSims );
+        RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords);
     return RetValue;
 }
 
@@ -433,32 +501,36 @@ int Gia_ManGetVar( Gia_Man_t * pNew, Vec_Int_t * vUsed, int iVar )
         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 )
+Gia_Man_t * Gia_ManConstructFromGates( Vec_Int_t * vGates, int nVars )
 {
-    int i, iLit0, iLit1, iLitRes;
-    Gia_Man_t * pNew = Gia_ManStart( 100 );
+    int i, iLit0, iLit1, iTopLit, iLitRes;
+    Gia_Man_t * pNew;
+    if ( Vec_IntSize(vGates) == 0 )
+        return NULL;
+    assert( Vec_IntSize(vGates) % 2 == 1 );
+    pNew = Gia_ManStart( 100 );
     pNew->pName = Abc_UtilStrsav( "resub" );
-    assert( iTopLit >= 0 );
+    iTopLit = Vec_IntEntryLast( vGates );
     if ( iTopLit == 0 || iTopLit == 1 )
         iLitRes = 0;
     else if ( Abc_Lit2Var(iTopLit) < nVars )
     {
-        assert( Vec_IntSize(vGates) == 0 );
+        assert( Vec_IntSize(vGates) == 1 );
         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( Vec_IntSize(vGates) > 1 );
+        assert( Vec_IntSize(vGates) % 2 == 1 );
         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);
+            int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars);
+            int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars);
             if ( iVar0 < iVar1 )
                 iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) );
             else if ( iVar0 > iVar1 )
@@ -491,7 +563,7 @@ Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLi
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose )
 {
     int * pBeg1 = vArr1->pArray;
     int * pBeg2 = vArr2->pArray;
@@ -521,7 +593,7 @@ static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr
         *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) );
+    if ( fVerbose ) printf( "Removed %d duplicated entries.  Array1 = %d.  Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) );
     return -1;
 }
 
@@ -538,20 +610,17 @@ void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, i
         else
             Vec_IntPush( vNotUnateVars, i );
 }
-int Gia_ManFindOneUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2] )
+int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose )
 {
-    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 );
+        Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] );
+        if ( fVerbose ) printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), n );
     }
-    return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+    return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose );
 }
 
 static inline int Gia_ManDivCover( word * pOffSet, word * pOnSet, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords )
@@ -568,61 +637,54 @@ int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, in
     {
         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);
+        if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) )
+            return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1);
     }
     return -1;
 }
-int Gia_ManFindTwoUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] )
+int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], int fVerbose )
 {
-    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] );
+        int nPairs = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2;
+        if ( fVerbose ) printf( "Trying %d pairs of %d-unate divs.\n", nPairs, n );
+        iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n] );
         if ( iLit >= 0 )
-            return Abc_LitNotCond(iLit, !n);
-        ABC_SWAP( word *, pOffSet, pOnSet );
+            return Abc_LitNotCond(iLit, n);
     }
     return -1;
 }
 
-void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
+void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs )
 {
     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) );
+            Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 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) );
+            Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) );
     }
 }
-int Gia_ManFindXor( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
+int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose )
 {
-    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 );
+        Vec_IntClear( vUnatePairs[n] );
+        Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] );
+        if ( fVerbose ) printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnatePairs[n]), n );
     }
-    return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+    return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose );
 }
 
-void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
+void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs )
 {
     int n, i, k, iDiv0, iDiv1;
-    Vec_IntClear( vUnateLits );
     Vec_IntForEachEntry( vBinate, iDiv1, i )
     Vec_IntForEachEntryStop( vBinate, iDiv0, k, i )
     {
@@ -632,56 +694,67 @@ void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinat
         {
             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) );
+            if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) )
+                Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) );
         }
     }
 }
-void Gia_ManFindUnatePairs( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
+void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose )
 {
-    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 );
+        int nBefore = Vec_IntSize(vUnatePairs[n]);
+        Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] );
+        if ( fVerbose ) printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnatePairs[n])-nBefore, n );
     }
-    RetValue = Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
+    RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose );
     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 )
+void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes )
+{
+    int fComp = Abc_LitIsCompl(iDiv);
+    int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF;
+    int iDiv1 = Abc_Lit2Var(iDiv) >> 15;
+    word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
+    word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1));
+    if ( iDiv0 < iDiv1 )
+    {
+        assert( !fComp );
+        Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords );
+    }
+    else 
+    {
+        assert( !Abc_LitIsCompl(iDiv0) );
+        assert( !Abc_LitIsCompl(iDiv1) );
+        Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 );
+    }
+}
+int Gia_ManFindDivGateInt( 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);
+    int Limit1 = Abc_MinInt( Vec_IntSize(vUnateLits), 1000 );
+    int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 );
+    Vec_IntForEachEntryStop( vUnateLits, iDiv0, i, Limit1 )
+    Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, Limit2 )
+    {
+        word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
+        int fComp1   = Abc_LitIsCompl(iDiv1);
+        Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp );
+        if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) )
+            return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1);
     }
     return -1;
 }
-int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], word * pDivTemp )
+int Gia_ManFindDivGate( word * pSets[2], 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 );
+        iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp );
+        if ( iLit >= 0 )
+            return Abc_LitNotCond( iLit, n );
     }
     return -1;
 }
@@ -689,39 +762,29 @@ int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2]
 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 Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 );
+    Vec_IntForEachEntryStop( vUnatePairs, iDiv1, i, Limit2 )
+    {
+        int fCompB = Abc_LitIsCompl(iDiv1);
+        Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB );
+        Vec_IntForEachEntryStop( vUnatePairs, iDiv0, k, i )
         {
-            int fCompB = Abc_LitIsCompl(iDiv1);
-            int iDiv10 = Abc_Lit2Var(iDiv1 >> 16);
-            int iDiv11 = Abc_Lit2Var(iDiv1 & 0xFFF);
-            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);
+            int fCompA = Abc_LitIsCompl(iDiv0);
+            Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA );
+            if ( Gia_ManDivCover(pOffSet, pOnSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) )
+                return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1);
         }
     }
     return -1;
 }
-int Gia_ManFindGateGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], word * pDivTempA, word * pDivTempB )
+int Gia_ManFindGateGate( word * pSets[2], 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;
+        iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB );
+        if ( iLit >= 0 )
+            return Abc_LitNotCond( iLit, n );
     }
     return -1;
 }
@@ -734,33 +797,36 @@ void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDi
     {
         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)) );
+        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] )
+void Gia_ManComputeLitWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int TopW[2], int fVerbose )
 {
-    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
-    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
-    int n;
+    int n, TopNum = 5;
+    TopW[0] = TopW[1] = 0;
     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 );
-    }
+        Gia_ManComputeLitWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n] );
     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++ )
+        if ( Vec_IntSize(vUnateLitsW[n]) )
         {
-            printf( "%5d : ", i );
-            printf( "Obj = %5d  ",  Vec_IntEntry(vUnateLits[n], pPerm[i]) );
-            printf( "Cost = %5d\n", Vec_IntEntry(vUnateLitsW[n], pPerm[i]) );
+            int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) );
+            TopW[n] = -Vec_IntEntry(vUnateLitsW[n], pPerm[0]);
+            if ( fVerbose ) 
+            {
+                printf( "Top %d %d-unate divs:\n", TopNum, n );
+                for ( i = 0; i < TopNum && i < Vec_IntSize(vUnateLits[n]); i++ )
+                {
+                    printf( "%5d : ", i );
+                    printf( "Lit = %5d  ",  Vec_IntEntry(vUnateLits[n], pPerm[i]) );
+                    printf( "Cost = %5d\n", -Vec_IntEntry(vUnateLitsW[n], pPerm[i]) );
+                }
+            }
+            for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ )
+                pPerm[i] = Vec_IntEntry(vUnateLits[n], pPerm[i]);
+            for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ )
+                vUnateLits[n]->pArray[i] = pPerm[i];
+            ABC_FREE( pPerm );
         }
-        ABC_FREE( pPerm );
-    }
 }
 
 void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW )
@@ -769,50 +835,59 @@ void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vD
     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;
+        int fComp = Abc_LitIsCompl(iPair);
+        int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF;
+        int iLit1 = Abc_Lit2Var(iPair) >> 15;
         word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) );
         word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) );
         if ( iLit0 < iLit1 )
         {
-            assert( !fCompl );
+            assert( !fComp );
             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) );
+            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) );
+            assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, fComp, nWords ) );
+            Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOnSet, nWords) );
         }
     }
 }
-void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2] )
+void Gia_ManComputePairWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], int TopW[2], int fVerbose )
 {
-    word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
-    word * pOnSet  = (word *)Vec_PtrEntry( vDivs, 1 );
-    int n;
+    int n, TopNum = 5;
+    TopW[0] = TopW[1] = 0;
     for ( n = 0; n < 2; n++ )
-    {
-        Gia_ManComputePairWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] );
-        ABC_SWAP( word *, pOffSet, pOnSet );
-    }
+        Gia_ManComputePairWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] );
     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++ )
+        if ( Vec_IntSize(vUnatePairsW[n]) )
         {
-            printf( "%5d : ", i );
-            printf( "Obj = %5d  ",  Vec_IntEntry(vUnatePairs[n], pPerm[i]) );
-            printf( "Cost = %5d\n", Vec_IntEntry(vUnatePairsW[n], pPerm[i]) );
+            int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) );
+            TopW[n] = -Vec_IntEntry(vUnatePairsW[n], pPerm[0]);
+            if ( fVerbose ) 
+            {
+                printf( "Top %d %d-unate pairs:\n", TopNum, n );
+                for ( i = 0; i < TopNum && i < Vec_IntSize(vUnatePairs[n]); i++ )
+                {
+                    int Pair = Vec_IntEntry(vUnatePairs[n], pPerm[i]);
+                    int Div0 = Abc_Lit2Var(Pair) & 0x7FFF;
+                    int Div1 = Abc_Lit2Var(Pair) >> 15;
+                    printf( "%5d : ", i );
+                    printf( "Compl = %5d  ", Abc_LitIsCompl(Pair) );
+                    printf( "Type = %s  ",   Div0 < Div1 ? "and" : "xor" );
+                    printf( "Div0 = %5d  ",  Div0 );
+                    printf( "Div1 = %5d  ",  Div1 );
+                    printf( "Cost = %5d\n",  -Vec_IntEntry(vUnatePairsW[n], pPerm[i]) );
+                }
+            }
+            for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ )
+                pPerm[i] = Vec_IntEntry(vUnatePairs[n], pPerm[i]);
+            for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ )
+                vUnatePairs[n]->pArray[i] = pPerm[i];
+            ABC_FREE( pPerm );
         }
-        ABC_FREE( pPerm );
-    }
 }
 
 
@@ -827,28 +902,32 @@ void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnat
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManResubInt2( Vec_Ptr_t * vDivs, int nWords, int NodeLimit, int ChoiceType, Vec_Int_t * vGates )
+int Gia_ManResubPerformInt( Gia_ResbMan_t * p )
 {
-    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
+    int TopOneW[2], TopTwoW[2], Max, iResLit, nVars = Vec_PtrSize(p->vDivs);
+    if ( p->fVerbose )
     {
-        printf( "Creating %s (%d).\n", Abc_LitIsCompl(iResLit) ? "inverter" : "buffer", Abc_Lit2Var(iResLit) );
-        return iResLit;
+        printf( "\nCalling decomposition for ISF: " ); 
+        printf( "OFF = %5d (%6.2f %%)  ", Abc_TtCountOnesVec(p->pSets[0], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[0], p->nWords)/(64*p->nWords) );
+        printf( "ON = %5d (%6.2f %%)\n",  Abc_TtCountOnesVec(p->pSets[1], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[1], p->nWords)/(64*p->nWords) );
     }
-    iResLit = Gia_ManFindTwoUnate( p->vDivs, p->nWords, p->vUnateLits );
+    if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) )
+        return 0;
+    if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) )
+        return 1;
+    iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose );
+    if ( iResLit >= 0 ) // buffer
+        return iResLit;
+    iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->fVerbose );
     if ( iResLit >= 0 ) // and
     {
-        int fCompl = Abc_LitIsCompl(iResLit);
-        int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
-        int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
+        int iNode = nVars + Vec_IntSize(p->vGates)/2;
+        int fComp = Abc_LitIsCompl(iResLit);
+        int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF;
+        int iDiv1 = Abc_Lit2Var(iResLit) >> 15;
+        assert( iDiv0 < iDiv1 );
         Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
-        printf( "Creating one AND-gate.\n" );
-        return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl );
+        return Abc_Var2Lit( iNode, fComp );
     }
     Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars );
     if ( Vec_IntSize(p->vBinateVars) > 1000 )
@@ -856,43 +935,181 @@ int Gia_ManResubInt( Gia_ResbMan_t * p )
         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 );
+    iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose );
     if ( iResLit >= 0 ) // xor
     {
-        int fCompl = Abc_LitIsCompl(iResLit);
-        int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
-        int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
+        int iNode = nVars + Vec_IntSize(p->vGates)/2;
+        int fComp = Abc_LitIsCompl(iResLit);
+        int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF;
+        int iDiv1 = Abc_Lit2Var(iResLit) >> 15;
         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" );
+        assert( iDiv0 > iDiv1 );
+        Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
+        return Abc_Var2Lit( iNode, fComp );
+    }
+    Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose );
+    iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA );
+    if ( iResLit >= 0 ) // and(div,pair)
+    {
+        int iNode  = nVars + Vec_IntSize(p->vGates)/2;
+
+        int fComp  = Abc_LitIsCompl(iResLit);
+        int iDiv0  = Abc_Lit2Var(iResLit) & 0x7FFF; // div
+        int iDiv1  = Abc_Lit2Var(iResLit) >> 15;    // pair
+
+        int Div1   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
+        int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
+        int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
+        int iDiv11 = Abc_Lit2Var(Div1) >> 15;   
+
+        Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
+        Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) );
+        return Abc_Var2Lit( iNode+1, fComp );
+    }
+    iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB );
+    if ( iResLit >= 0 ) // and(pair,pair)
+    {
+        int iNode  = nVars + Vec_IntSize(p->vGates)/2;
+
+        int fComp  = Abc_LitIsCompl(iResLit);
+        int iDiv0  = Abc_Lit2Var(iResLit) & 0x7FFF; // pair
+        int iDiv1  = Abc_Lit2Var(iResLit) >> 15;    // pair
+
+        int Div0   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) );
+        int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0);
+        int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF;
+        int iDiv01 = Abc_Lit2Var(Div0) >> 15;   
+        
+        int Div1   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
+        int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
+        int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
+        int iDiv11 = Abc_Lit2Var(Div1) >> 15;   
+        
+        Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 );
+        Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
+        Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) );
+        return Abc_Var2Lit( iNode+2, fComp );
+    }
+    if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 )
         return -1;
+    Gia_ManComputeLitWeights( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, TopOneW, p->fVerbose );
+    Gia_ManComputePairWeights( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, TopTwoW, p->fVerbose );
+    //Max = Abc_MaxInt( Abc_MaxInt(TopOneW[0], TopOneW[1]), Abc_MaxInt(TopTwoW[0], TopTwoW[1]) );
+    Max = Abc_MaxInt(TopOneW[0], TopOneW[1]);
+    if ( Max == 0 )
+        return -1;
+    if ( Max == TopOneW[0] || Max == TopOneW[1] )
+    {
+        int fUseOr  = Max == TopOneW[0];
+        int iDiv    = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 );
+        int fComp   = Abc_LitIsCompl(iDiv);
+        word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) );
+        Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp );
+        iResLit = Gia_ManResubPerformInt( p );
+        if ( iResLit >= 0 ) 
+        {
+            int iNode = nVars + Vec_IntSize(p->vGates)/2;
+            Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) );
+            return Abc_Var2Lit( iNode, fUseOr );
+        }
+    }
+    if ( Max == TopTwoW[0] || Max == TopTwoW[1] )
+    {
+        int fUseOr  = Max == TopTwoW[0];
+        int iDiv    = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 );
+        int fComp   = Abc_LitIsCompl(iDiv);
+        Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA );
+        Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp );
+        iResLit = Gia_ManResubPerformInt( p );
+        if ( iResLit >= 0 ) 
+        {
+            int iNode = nVars + Vec_IntSize(p->vGates)/2;
+            int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF;   
+            int iDiv1 = Abc_Lit2Var(iDiv) >> 15;      
+            Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
+            Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) );
+            return Abc_Var2Lit( iNode+1, fUseOr );
+        }
     }
-*/
-    Gia_ManComputeLitWeights( p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW );
-    Gia_ManComputePairWeights( p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW );
     return -1;
 }
+void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vRes, int fVerbose )
+{
+    int Res;
+    Vec_IntClear( vRes );
+    Gia_ResbInit( p, vDivs, nWords, vRes, fVerbose );
+    Res = Gia_ManResubPerformInt( p );
+    if ( Res == -1 )
+    {
+        printf( "\n" );
+        return;
+    }
+    Vec_IntPush( vRes, Res );
+    Gia_ManResubPrint( vRes, Vec_PtrSize(vDivs) );
+    printf( "          Verification %s.\n", Gia_ManResubVerify(p) ? "succeeded" : "FAILED *******************************" );
+}
+void Gia_ManResubTest3()
+{
+    int nVars = 3;
+    Gia_ResbMan_t * p = Gia_ResbAlloc( 1 );
+    word Divs[6] = { 0, 0, 
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0xCCCCCCCCCCCCCCCC),
+        ABC_CONST(0xF0F0F0F0F0F0F0F0),
+        ABC_CONST(0xFF00FF00FF00FF00) 
+    };
+    Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 );
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    int i; 
+    for ( i = 0; i < 6; i++ )
+        Vec_PtrPush( vDivs, Divs+i );
+    for ( i = 0; i < (1<<(1<<nVars)); i++ )
+    {
+        word Truth = Abc_Tt6Stretch( i, nVars );
+        Divs[0] = ~Truth;
+        Divs[1] =  Truth;
+        printf( "%3d : ", i );
+        Extra_PrintHex( stdout, (unsigned*)&Truth, nVars );
+        printf( " " );
+        Dau_DsdPrintFromTruth2( (unsigned*)&Truth, nVars );
+        printf( "       " );
+        Gia_ManResubPerform( p, vDivs, 1, vRes, 0 );
+    }
+    Gia_ResbFree( p );
+    Vec_IntFree( vRes );
+    Vec_PtrFree( vDivs );
+}
+void Gia_ManResubTest3_()
+{
+    Gia_ResbMan_t * p = Gia_ResbAlloc( 1 );
+    word Divs[6] = { 0, 0, 
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0xCCCCCCCCCCCCCCCC),
+        ABC_CONST(0xF0F0F0F0F0F0F0F0),
+        ABC_CONST(0xFF00FF00FF00FF00) 
+    };
+    Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 );
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    int i; 
+    for ( i = 0; i < 6; i++ )
+        Vec_PtrPush( vDivs, Divs+i );
+
+    {
+        word Truth = (Divs[2] | Divs[3]) & (Divs[4] & Divs[5]);
+//        word Truth = (~Divs[2] | Divs[3]) | ~Divs[4];
+        Divs[0] = ~Truth;
+        Divs[1] =  Truth;
+        Extra_PrintHex( stdout, (unsigned*)&Truth, 6 );
+        printf( " " );
+        Dau_DsdPrintFromTruth2( (unsigned*)&Truth, 6 );
+        printf( "       " );
+        Gia_ManResubPerform( p, vDivs, 1, vRes, 0 );
+    }
+    Gia_ResbFree( p );
+    Vec_IntFree( vRes );
+    Vec_PtrFree( vDivs );
+}
 
 /**Function*************************************************************
 
@@ -942,30 +1159,22 @@ Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, i
 }
 Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose )
 {
-    int iTopLit, nWords = 0;
+    int 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((word *)Vec_PtrEntry(vDivs, 0), nWords), 100.0*Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 0), nWords)/(64*nWords) );
-    printf( "ON = %5d (%6.2f %%)\n",  Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 1), nWords), 100.0*Abc_TtCountOnesVec((word *)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_ResbMan_t * p = Gia_ResbAlloc( nWords );
 //    Gia_ManCheckResub( vDivs, nWords );
-    iTopLit = Gia_ManResubInt( p );
-    if ( iTopLit >= 0 )
+    if ( Vec_PtrSize(vDivs) >= (1<<14) )
     {
-        printf( "Verification %s.\n", Gia_ManResubVerify( vDivs, nWords, vGates, iTopLit ) ? "succeeded" : "FAILED" );
-        pMan = Gia_ManConstructFromGates( Vec_PtrSize(vDivs), vGates, iTopLit );
+        printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 );
+        Vec_PtrShrink( vDivs, (1<<14)-1 );
     }
+    assert( Vec_PtrSize(vDivs) < (1<<14) );
+    Gia_ManResubPerform( p, vDivs, nWords, vGates, 1 );
+    if ( Vec_IntSize(vGates) )
+        pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) );
     else
         printf( "Decomposition did not succeed.\n" );
     Gia_ResbFree( p );
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index b1e7e0d8..3e11a15d 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -1973,6 +1973,14 @@ void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit )
     Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
     fprintf( stdout, "%s\n", pRes );
 }
+void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit )
+{
+    char pRes[DAU_MAX_STR];
+    word pTemp[DAU_MAX_WORD];
+    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
+    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
+    fprintf( stdout, "%s", pRes );
+}
 
 void Dau_DsdTest44()
 {