Improvements to ISOP.

1 files changed, 784 insertions, 278 deletions

diff --git a/src/misc/util/utilIsop.c b/src/misc/util/utilIsop.c
index a62fc84d..ea03c027 100644
--- a/src/misc/util/utilIsop.c
+++ b/src/misc/util/utilIsop.c
@@ -32,7 +32,11 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef int FUNC_ISOP( word *, word *, word *, int *, int );
+#define ABC_ISOP_MAX_VAR  16
+#define ABC_ISOP_MAX_WORD (ABC_ISOP_MAX_VAR > 6 ? (1 << (ABC_ISOP_MAX_VAR-6)) : 1)
+#define ABC_ISOP_MAX_CUBE  0xFFFF
+
+typedef word FUNC_ISOP( word *, word *, word *, word, int * );
 
 static FUNC_ISOP Abc_Isop7Cover; 
 static FUNC_ISOP Abc_Isop8Cover;
@@ -66,8 +70,12 @@ static FUNC_ISOP * s_pFuncIsopCover[17] =
     Abc_Isop16Cover  // 16
 };
 
-extern int Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, int nCostLim, int * pCover );
-extern int Abc_EsopCheck( word * pOn, int nVars, int nCostLim, int * pCover );
+extern word Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover );
+extern word Abc_EsopCheck( word * pOn,                            int nVars, word CostLim, int * pCover );
+
+static inline word Abc_Cube2Cost( int nCubes )    { return (word)nCubes << 32;       }
+static inline int  Abc_CostCubes( word Cost )     { return (int)(Cost >> 32);        }
+static inline int  Abc_CostLits( word Cost )      { return (int)(Cost & 0xFFFFFFFF); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -84,21 +92,23 @@ extern int Abc_EsopCheck( word * pOn, int nVars, int nCostLim, int * pCover );
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Abc_IsopAddLits( int * pCover, int nCost0, int nCost1, int Var )
+static inline void Abc_IsopAddLits( int * pCover, word Cost0, word Cost1, int Var )
 {
-    int c;
-    if ( pCover == NULL ) return;
-    nCost0 >>= 16;
-    nCost1 >>= 16;
-    for ( c = 0; c < nCost0; c++ )
-        pCover[c] |= (1 << Abc_Var2Lit(Var,0));
-    for ( c = 0; c < nCost1; c++ )
-        pCover[nCost0+c] |= (1 << Abc_Var2Lit(Var,1));
+    if ( pCover ) 
+    {
+        int c, nCubes0, nCubes1;
+        nCubes0 = Abc_CostCubes( Cost0 );
+        nCubes1 = Abc_CostCubes( Cost1 );
+        for ( c = 0; c < nCubes0; c++ )
+            pCover[c] |= (1 << Abc_Var2Lit(Var,0));
+        for ( c = 0; c < nCubes1; c++ )
+            pCover[nCubes0+c] |= (1 << Abc_Var2Lit(Var,1));
+    }
 }
-int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
+word Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, word CostLim, int * pCover )
 {
     word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
-    int Var, nCost0, nCost1, nCost2;
+    word Cost0, Cost1, Cost2;  int Var; 
     assert( nVars <= 6 );
     assert( (uOn & ~uOnDc) == 0 );
     if ( uOn == 0 )
@@ -110,7 +120,7 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
     {
         pRes[0] = ~(word)0;
         if ( pCover ) pCover[0] = 0;
-        return (1 << 16);
+        return Abc_Cube2Cost(1);
     }
     assert( nVars > 0 );
     // find the topmost var
@@ -124,64 +134,63 @@ int Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, int nCostLim,
     uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
     uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
     // solve for cofactors
-    nCost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
-    nCost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
+    Cost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    Cost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    Cost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
     // derive the final truth table
     *pRes = uRes2 | (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
     assert( (uOn & ~*pRes) == 0 && (*pRes & ~uOnDc) == 0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, Var );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
+    Abc_IsopAddLits( pCover, Cost0, Cost1, Var );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop7Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop7Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
     word uOn0, uOn1, uOn2, uOnDc2, uRes0, uRes1, uRes2;
-    int nCost0, nCost1, nCost2, nVars = 6;
+    word Cost0, Cost1, Cost2;  int nVars = 6; 
     assert( (pOn[0] & ~pOnDc[0]) == 0 );
     assert( (pOn[1] & ~pOnDc[1]) == 0 );
     // cofactor
     uOn0 = pOn[0] & ~pOnDc[1];
     uOn1 = pOn[1] & ~pOnDc[0];
     // solve for cofactors
-    nCost0 = Abc_IsopCheck( &uOn0, pOnDc,   &uRes0, nVars, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_IsopCheck( &uOn1, pOnDc+1, &uRes1, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
+    Cost0 = Abc_IsopCheck( &uOn0, pOnDc,   &uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    Cost1 = Abc_IsopCheck( &uOn1, pOnDc+1, &uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
     uOn2 = (pOn[0] & ~uRes0) | (pOn[1] & ~uRes1);
     uOnDc2 = pOnDc[0] & pOnDc[1];
-    nCost2 = Abc_IsopCheck( &uOn2, &uOnDc2,  &uRes2, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
+    Cost2 = Abc_IsopCheck( &uOn2, &uOnDc2,  &uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
     // derive the final truth table
     pRes[0] = uRes2 | uRes0;
     pRes[1] = uRes2 | uRes1;
     assert( (pOn[0] & ~pRes[0]) == 0 && (pRes[0] & ~pOnDc[0]) == 0 );
     assert( (pOn[1] & ~pRes[1]) == 0 && (pRes[1] & ~pOnDc[1]) == 0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, nVars );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop8Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop8Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
-    int nCost0, nCost1, nCost2, nVars = 7;
-    // cofactor
-    uOn0[0] = pOn[0] & ~pOnDc[2];
-    uOn0[1] = pOn[1] & ~pOnDc[3];
-    uOn1[0] = pOn[2] & ~pOnDc[0];
-    uOn1[1] = pOn[3] & ~pOnDc[1];
-    // solve for cofactors
-    nCost0 = Abc_IsopCheck( uOn0, pOnDc,   uRes0, nVars, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_IsopCheck( uOn1, pOnDc+2, uRes1, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
-    uOn2[0] = (pOn[0] & ~uRes0[0]) | (pOn[2] & ~uRes1[0]);
-    uOn2[1] = (pOn[1] & ~uRes0[1]) | (pOn[3] & ~uRes1[1]);
-    uOnDc2[0] = pOnDc[0] & pOnDc[2];
-    uOnDc2[1] = pOnDc[1] & pOnDc[3];
-    nCost2 = Abc_IsopCheck( uOn2, uOnDc2,  uRes2, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
+    word uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
+    word Cost0, Cost1, Cost2;  int nVars = 7;
+    // negative cofactor
+    uOn2[0] = pOn[0] & ~pOnDc[2];
+    uOn2[1] = pOn[1] & ~pOnDc[3];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,   uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    uOn2[0] = pOn[2] & ~pOnDc[0];
+    uOn2[1] = pOn[3] & ~pOnDc[1];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+2, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    uOn2[0] = (pOn[0] & ~uRes0[0]) | (pOn[2] & ~uRes1[0]); uOnDc2[0] = pOnDc[0] & pOnDc[2];
+    uOn2[1] = (pOn[1] & ~uRes0[1]) | (pOn[3] & ~uRes1[1]); uOnDc2[1] = pOnDc[1] & pOnDc[3];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,  uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
     // derive the final truth table
     pRes[0] = uRes2[0] | uRes0[0];
     pRes[1] = uRes2[1] | uRes0[1];
@@ -189,101 +198,358 @@ int Abc_Isop8Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCo
     pRes[3] = uRes2[1] | uRes1[1];
     assert( (pOn[0] & ~pRes[0]) == 0 && (pOn[1] & ~pRes[1]) == 0 && (pOn[2] & ~pRes[2]) == 0 && (pOn[3] & ~pRes[3]) == 0 );
     assert( (pRes[0] & ~pOnDc[0])==0 && (pRes[1] & ~pOnDc[1])==0 && (pRes[2] & ~pOnDc[2])==0 && (pRes[3] & ~pOnDc[3])==0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, nVars );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop9Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop9Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    word uOn0[4], uOn1[4], uOn2[4], uOnDc2[4], uRes0[4], uRes1[4], uRes2[4];
-    int c, nCost0, nCost1, nCost2, nVars = 8, nWords = 4;
-    // cofactor
+    word uOn2[4], uOnDc2[4], uRes0[4], uRes1[4], uRes2[4];
+    word Cost0, Cost1, Cost2; int c, nVars = 8, nWords = 4;
+    // negative cofactor
     for ( c = 0; c < nWords; c++ )
-        uOn0[c] = pOn[c] & ~pOnDc[c+nWords], uOn1[c] = pOn[c+nWords] & ~pOnDc[c];
-    // solve for cofactors
-    nCost0 = Abc_IsopCheck( uOn0, pOnDc,        uRes0, nVars, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_IsopCheck( uOn1, pOnDc+nWords, uRes1, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
     for ( c = 0; c < nWords; c++ )
         uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
-    nCost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
     // derive the final truth table
     for ( c = 0; c < nWords; c++ )
         pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
     // verify
     for ( c = 0; c < (nWords<<1); c++ )
         assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, nVars );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop10Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop10Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    word uOn0[8], uOn1[8], uOn2[8], uOnDc2[8], uRes0[8], uRes1[8], uRes2[8];
-    int c, nCost0, nCost1, nCost2, nVars = 9, nWords = 8;
-    // cofactor
+    word uOn2[8], uOnDc2[8], uRes0[8], uRes1[8], uRes2[8];
+    word Cost0, Cost1, Cost2; int c, nVars = 9, nWords = 8;
+    // negative cofactor
     for ( c = 0; c < nWords; c++ )
-        uOn0[c] = pOn[c] & ~pOnDc[c+nWords], uOn1[c] = pOn[c+nWords] & ~pOnDc[c];
-    // solve for cofactors
-    nCost0 = Abc_IsopCheck( uOn0, pOnDc,        uRes0, nVars, nCostLim, pCover );
-    if ( nCost0 >= nCostLim ) return nCostLim;
-    nCost1 = Abc_IsopCheck( uOn1, pOnDc+nWords, uRes1, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) : NULL );
-    if ( nCost0 + nCost1 >= nCostLim ) return nCostLim;
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
     for ( c = 0; c < nWords; c++ )
         uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
-    nCost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, nCostLim, pCover ? pCover + (nCost0 >> 16) + (nCost1 >> 16) : NULL );
-    if ( nCost0 + nCost1 + nCost2 >= nCostLim ) return nCostLim;
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
     // derive the final truth table
     for ( c = 0; c < nWords; c++ )
         pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
     // verify
     for ( c = 0; c < (nWords<<1); c++ )
         assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
-    Abc_IsopAddLits( pCover, nCost0, nCost1, nVars );
-    return nCost0 + nCost1 + nCost2 + (nCost0 >> 16) + (nCost1 >> 16);
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop11Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop11Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[16], uOnDc2[16], uRes0[16], uRes1[16], uRes2[16];
+    word Cost0, Cost1, Cost2; int c, nVars = 10, nWords = 16;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop12Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop12Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[32], uOnDc2[32], uRes0[32], uRes1[32], uRes2[32];
+    word Cost0, Cost1, Cost2; int c, nVars = 11, nWords = 32;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop13Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop13Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[64], uOnDc2[64], uRes0[64], uRes1[64], uRes2[64];
+    word Cost0, Cost1, Cost2; int c, nVars = 12, nWords = 64;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop14Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop14Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[128], uOnDc2[128], uRes0[128], uRes1[128], uRes2[128];
+    word Cost0, Cost1, Cost2; int c, nVars = 13, nWords = 128;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop15Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop15Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[256], uOnDc2[256], uRes0[256], uRes1[256], uRes2[256];
+    word Cost0, Cost1, Cost2; int c, nVars = 14, nWords = 256;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_Isop16Cover( word * pOn, word * pOnDc, word * pRes, int * pCover, int nCostLim )
+word Abc_Isop16Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
 {
-    return 0;
+    word uOn2[512], uOnDc2[512], uRes0[512], uRes1[512], uRes2[512];
+    word Cost0, Cost1, Cost2; int c, nVars = 15, nWords = 512;
+    // negative cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
+    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
+    if ( Cost0 >= CostLim ) return CostLim;
+    // positive cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
+    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
+    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
+    // middle cofactor
+    for ( c = 0; c < nWords; c++ )
+        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
+    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
+    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
+    // derive the final truth table
+    for ( c = 0; c < nWords; c++ )
+        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
+    // verify
+    for ( c = 0; c < (nWords<<1); c++ )
+        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
+    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
+    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
 }
-int Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, int nCostLim, int * pCover )
+word Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover )
 {
-    int nVarsNew, Cost;
+    int nVarsNew; word Cost;
     if ( nVars <= 6 )
-        return Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVars, nCostLim, pCover );
+        return Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVars, CostLim, pCover );
     for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
         if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) || Abc_TtHasVar( pOnDc, nVars, nVarsNew-1 ) )
             break;
     if ( nVarsNew == 6 )
-        Cost = Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVarsNew, nCostLim, pCover );
+        Cost = Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVarsNew, CostLim, pCover );
     else
-        Cost = s_pFuncIsopCover[nVarsNew]( pOn, pOnDc, pRes, pCover, nCostLim );
+        Cost = s_pFuncIsopCover[nVarsNew]( pOn, pOnDc, pRes, CostLim, pCover );
     Abc_TtStretch6( pRes, nVarsNew, nVars );
     return Cost;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Create truth table for the given cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word ** Abc_IsopTtElems()
+{
+    static word TtElems[ABC_ISOP_MAX_VAR+1][ABC_ISOP_MAX_WORD], * pTtElems[ABC_ISOP_MAX_VAR+1] = {NULL};
+    if ( pTtElems[0] == NULL )
+    {
+        int v;
+        for ( v = 0; v <= ABC_ISOP_MAX_VAR; v++ )
+            pTtElems[v] = TtElems[v];
+        Abc_TtElemInit( pTtElems, ABC_ISOP_MAX_VAR );
+    }
+    return pTtElems;
+}
+void Abc_IsopBuildTruth( Vec_Int_t * vCover, int nVars, word * pRes, int fXor, int fCompl )
+{
+    word ** pTtElems = Abc_IsopTtElems();
+    word pCube[ABC_ISOP_MAX_WORD];
+    int nWords = Abc_TtWordNum( nVars );
+    int c, v, Cube;
+    assert( nVars <= ABC_ISOP_MAX_VAR );
+    Abc_TtClear( pRes, nWords );
+    Vec_IntForEachEntry( vCover, Cube, c )
+    {
+        Abc_TtFill( pCube, nWords );
+        for ( v = 0; v < nVars; v++ )
+            if ( ((Cube >> (v << 1)) & 3) == 1 )
+                Abc_TtSharp( pCube, pCube, pTtElems[v], nWords );
+            else if ( ((Cube >> (v << 1)) & 3) == 2 )
+                Abc_TtAnd( pCube, pCube, pTtElems[v], nWords, 0 );
+        if ( fXor )
+            Abc_TtXor( pRes, pRes, pCube, nWords, 0 );
+        else
+            Abc_TtOr( pRes, pRes, pCube, nWords );
+    }
+    if ( fCompl )
+        Abc_TtNot( pRes, nWords );
+}
+static inline void Abc_IsopVerify( word * pFunc, int nVars, word * pRes, Vec_Int_t * vCover, int fXor, int fCompl )
+{
+    Abc_IsopBuildTruth( vCover, nVars, pRes, fXor, fCompl );
+    if ( !Abc_TtEqual( pFunc, pRes, Abc_TtWordNum(nVars) ) )
+        printf( "Verification failed.\n" );
+//    else
+//        printf( "Verification succeeded.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure assumes that function has exact support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_Isop( word * pFunc, int nVars, int nCubeLim, Vec_Int_t * vCover, int fTryBoth )
+{
+    word pRes[ABC_ISOP_MAX_WORD];
+    word Cost0, Cost1, Cost, CostInit = Abc_Cube2Cost(nCubeLim);
+    assert( nVars <= ABC_ISOP_MAX_VAR );
+    Vec_IntGrow( vCover, 1 << (nVars-1) );
+    if ( fTryBoth )
+    {
+        Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, NULL );
+        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
+        Cost1 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Cost0, NULL );
+        Cost = Abc_MinWord( Cost0, Cost1 );
+        if ( Cost == CostInit )
+        {
+            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
+            return -1;
+        }
+        if ( Cost == Cost0 )
+        {
+            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
+            Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
+        }
+        else // if ( Cost == Cost1 )
+        {
+            Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
+            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
+        }
+    }
+    else
+    {
+        Cost = Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
+        if ( Cost == CostInit )
+            return -1;
+    }
+    vCover->nSize = Abc_CostCubes(Cost);
+    assert( vCover->nSize <= vCover->nCap );
+//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, Cost != Cost0 );
+    return Cost != Cost0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Compute CNF assuming it does not exceed the limit.]
 
   Description [Please note that pCover should have at least 32 extra entries!]
@@ -295,30 +561,97 @@ int Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, int nCostLi
 ***********************************************************************/
 int Abc_IsopCnf( word * pFunc, int nVars, int nCubeLim, int * pCover )
 {
-    word pRes[1024];
-    int c, Cost0, Cost1, CostLim = nCubeLim << 16;
+    word pRes[ABC_ISOP_MAX_WORD];
+    word Cost0, Cost1, CostInit = Abc_Cube2Cost(nCubeLim);
+    int c, nCubes0, nCubes1;
+    assert( nVars <= ABC_ISOP_MAX_VAR );
     assert( Abc_TtHasVar( pFunc, nVars, nVars - 1 ) );
     if ( nVars > 6 )
-        Cost0 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, pCover, CostLim );
+        Cost0 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover );
     else
-        Cost0 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostLim, pCover );
-    if ( Cost0 >= CostLim )
-        return CostLim;
+        Cost0 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover );
+    if ( Cost0 >= CostInit )
+        return CostInit;
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
     if ( nVars > 6 )
-        Cost1 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, pCover ? pCover + (Cost0 >> 16) : NULL, CostLim );
+        Cost1 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
     else
-        Cost1 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostLim, pCover ? pCover + (Cost0 >> 16) : NULL );
+        Cost1 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-    if ( Cost0 + Cost1 >= CostLim )
-        return CostLim;
-    if ( pCover == NULL )
-        return Cost0 + Cost1;
-    for ( c = 0; c < (Cost0 >> 16); c++ )
-        pCover[c] |= (1 << Abc_Var2Lit(nVars, 0));
-    for ( c = 0; c < (Cost1 >> 16); c++ )
-        pCover[c+(Cost0 >> 16)] |= (1 << Abc_Var2Lit(nVars, 1));
-    return Cost0 + Cost1;
+    if ( Cost0 + Cost1 >= CostInit )
+        return CostInit;
+    nCubes0 = Abc_CostCubes(Cost0);
+    nCubes1 = Abc_CostCubes(Cost1);
+    if ( pCover )
+    {
+        for ( c = 0; c < nCubes0; c++ )
+            pCover[c] |= (1 << Abc_Var2Lit(nVars, 0));
+        for ( c = 0; c < nCubes1; c++ )
+            pCover[c+nCubes0] |= (1 << Abc_Var2Lit(nVars, 1));
+    }
+    return nCubes0 + nCubes1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_IsopCountLits( Vec_Int_t * vCover, int nVars )
+{
+    int i, k, Entry, Literal, nLits = 0;
+    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
+        return 0;
+    Vec_IntForEachEntry( vCover, Entry, i )
+    { 
+        for ( k = 0; k < nVars; k++ )
+        {
+            Literal = 3 & (Entry >> (k << 1));
+            if ( Literal == 1 ) // neg literal
+                nLits++;
+            else if ( Literal == 2 ) // pos literal
+                nLits++;
+            else if ( Literal != 0 ) 
+                assert( 0 );
+        }
+    }
+    return nLits;
+}
+void Abc_IsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl )
+{
+    int i, k, Entry, Literal;
+    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
+    {
+        printf( "Constant %d\n", Vec_IntSize(vCover) );
+        return;
+    }
+    Vec_IntForEachEntry( vCover, Entry, i )
+    { 
+        for ( k = 0; k < nVars; k++ )
+        {
+            Literal = 3 & (Entry >> (k << 1));
+            if ( Literal == 1 ) // neg literal
+                printf( "0" );
+            else if ( Literal == 2 ) // pos literal
+                printf( "1" );
+            else if ( Literal == 0 ) 
+                printf( "-" );
+            else assert( 0 );
+        }
+        printf( " %d\n", !fCompl );
+    }
+}
+void Abc_IsopPrint( word * t, int nVars, Vec_Int_t * vCover, int fTryBoth )
+{
+    int fCompl = Abc_Isop( t, nVars, ABC_ISOP_MAX_CUBE, vCover, fTryBoth );
+    Abc_IsopPrintCover( vCover, nVars, fCompl );
 }
 
 
@@ -333,61 +666,62 @@ int Abc_IsopCnf( word * pFunc, int nVars, int nCubeLim, int * pCover )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_EsopAddLits( int * pCover, int r0, int r1, int r2, int Max, int Var )
+static inline int Abc_EsopAddLits( int * pCover, word r0, word r1, word r2, word Max, int Var )
 {
-    int i;
+    int i, c0, c1, c2;
     if ( Max == r0 )
     {
-        r2 >>= 16;
+        c2 = Abc_CostCubes(r2);
         if ( pCover )
         {
-            r0 >>= 16;
-            r1 >>= 16;
-            for ( i = 0; i < r1; i++ )
-                pCover[i] = pCover[r0+i];
-            for ( i = 0; i < r2; i++ )
-                pCover[r1+i] = pCover[r0+r1+i] | (1 << Abc_Var2Lit(Var,0));
+            c0 = Abc_CostCubes(r0);
+            c1 = Abc_CostCubes(r1);
+            for ( i = 0; i < c1; i++ )
+                pCover[i] = pCover[c0+i];
+            for ( i = 0; i < c2; i++ )
+                pCover[c1+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,0));
         }
-        return r2;
+        return c2;
     }
     else if ( Max == r1 )
     {
-        r2 >>= 16;
+        c2 = Abc_CostCubes(r2);
         if ( pCover )
         {
-            r0 >>= 16;
-            r1 >>= 16;
-            for ( i = 0; i < r2; i++ )
-                pCover[r0+i] = pCover[r0+r1+i] | (1 << Abc_Var2Lit(Var,1));
+            c0 = Abc_CostCubes(r0);
+            c1 = Abc_CostCubes(r1);
+            for ( i = 0; i < c2; i++ )
+                pCover[c0+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,1));
         }
-        return r2;
+        return c2;
     }
     else
     {
-        r0 >>= 16;
-        r1 >>= 16;
+        c0 = Abc_CostCubes(r0);
+        c1 = Abc_CostCubes(r1);
         if ( pCover )
         {
-            r2 >>= 16;
-            for ( i = 0; i < r0; i++ )
+            c2 = Abc_CostCubes(r2);
+            for ( i = 0; i < c0; i++ )
                 pCover[i] |= (1 << Abc_Var2Lit(Var,0));
-            for ( i = 0; i < r1; i++ )
-                pCover[r0+i] |= (1 << Abc_Var2Lit(Var,1));
+            for ( i = 0; i < c1; i++ )
+                pCover[c0+i] |= (1 << Abc_Var2Lit(Var,1));
         }
-        return r0 + r1;
+        return c0 + c1;
     }
 }
-int Abc_Esop6Cover( word t, int nVars, int nCostLim, int * pCover )
+word Abc_Esop6Cover( word t, int nVars, word CostLim, int * pCover )
 {
     word c0, c1;
-    int Var, r0, r1, r2, Max;
+    word r0, r1, r2, Max;
+    int Var;
     assert( nVars <= 6 );
     if ( t == 0 )
         return 0;
     if ( t == ~(word)0 )
     {
         if ( pCover ) *pCover = 0;
-        return 1 << 16;
+        return Abc_Cube2Cost(1);
     }
     assert( nVars > 0 );
     // find the topmost var
@@ -399,53 +733,55 @@ int Abc_Esop6Cover( word t, int nVars, int nCostLim, int * pCover )
     c0 = Abc_Tt6Cofactor0( t, Var );
     c1 = Abc_Tt6Cofactor1( t, Var );
     // call recursively
-    r0 = Abc_Esop6Cover( c0,      Var, nCostLim, pCover ? pCover : NULL );
-    if ( r0 >= nCostLim ) return nCostLim;
-    r1 = Abc_Esop6Cover( c1,      Var, nCostLim, pCover ? pCover + (r0 >> 16) : NULL );
-    if ( r1 >= nCostLim ) return nCostLim;
-    r2 = Abc_Esop6Cover( c0 ^ c1, Var, nCostLim, pCover ? pCover + (r0 >> 16) + (r1 >> 16) : NULL );
-    if ( r2 >= nCostLim ) return nCostLim;
-    Max = Abc_MaxInt( r0, Abc_MaxInt(r1, r2) );
-    if ( r0 + r1 + r2 - Max >= nCostLim ) return nCostLim;
+    r0 = Abc_Esop6Cover( c0,      Var, CostLim, pCover ? pCover : NULL );
+    if ( r0 >= CostLim ) return CostLim;
+    r1 = Abc_Esop6Cover( c1,      Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
+    if ( r1 >= CostLim ) return CostLim;
+    r2 = Abc_Esop6Cover( c0 ^ c1, Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
+    if ( r2 >= CostLim ) return CostLim;
+    Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
+    if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
     return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, Var );
 }
-int Abc_EsopCover( word * pOn, int nVars, int nCostLim, int * pCover )
+word Abc_EsopCover( word * pOn, int nVars, word CostLim, int * pCover )
 {
-    int c, r0, r1, r2, Max, nWords = (1 << (nVars - 7));
+    word r0, r1, r2, Max;
+    int c, nWords = (1 << (nVars - 7));
     assert( nVars > 6 );
     assert( Abc_TtHasVar( pOn, nVars, nVars - 1 ) );
-    r0 = Abc_EsopCheck( pOn,        nVars-1, nCostLim, pCover );
-    if ( r0 >= nCostLim ) return nCostLim;
-    r1 = Abc_EsopCheck( pOn+nWords, nVars-1, nCostLim, pCover ? pCover + (r0 >> 16) : NULL );
-    if ( r1 >= nCostLim ) return nCostLim;
+    r0 = Abc_EsopCheck( pOn,        nVars-1, CostLim, pCover );
+    if ( r0 >= CostLim ) return CostLim;
+    r1 = Abc_EsopCheck( pOn+nWords, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
+    if ( r1 >= CostLim ) return CostLim;
     for ( c = 0; c < nWords; c++ )
         pOn[c] ^= pOn[nWords+c];
-    r2 = Abc_EsopCheck( pOn, nVars-1, nCostLim, pCover ? pCover + (r0 >> 16) + (r1 >> 16) : NULL );
+    r2 = Abc_EsopCheck( pOn, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
     for ( c = 0; c < nWords; c++ )
         pOn[c] ^= pOn[nWords+c];
-    if ( r2 >= nCostLim ) return nCostLim;
-    Max = Abc_MaxInt( r0, Abc_MaxInt(r1, r2) );
-    if ( r0 + r1 + r2 - Max >= nCostLim ) return nCostLim;
+    if ( r2 >= CostLim ) return CostLim;
+    Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
+    if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
     return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, nVars-1 );
 }
-int Abc_EsopCheck( word * pOn, int nVars, int nCostLim, int * pCover )
+word Abc_EsopCheck( word * pOn, int nVars, word CostLim, int * pCover )
 {
-    int nVarsNew, Cost;
+    int nVarsNew; word Cost;
     if ( nVars <= 6 )
-        return Abc_Esop6Cover( *pOn, nVars, nCostLim, pCover );
+        return Abc_Esop6Cover( *pOn, nVars, CostLim, pCover );
     for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
         if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) )
             break;
     if ( nVarsNew == 6 )
-        Cost = Abc_Esop6Cover( *pOn, nVarsNew, nCostLim, pCover );
+        Cost = Abc_Esop6Cover( *pOn, nVarsNew, CostLim, pCover );
     else
-        Cost = Abc_EsopCover( pOn, nVarsNew, nCostLim, pCover );
+        Cost = Abc_EsopCover( pOn, nVarsNew, CostLim, pCover );
     return Cost;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [This procedure assumes that function has exact support.]
+  Synopsis    [Perform ISOP computation by subtracting cubes.]
 
   Description []
                
@@ -454,114 +790,222 @@ int Abc_EsopCheck( word * pOn, int nVars, int nCostLim, int * pCover )
   SeeAlso     []
 
 ***********************************************************************/
-#define ABC_ISOP_MAX_VAR 12
-static inline word ** Abc_IsopTtElems()
+static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords )
 {
-    static word TtElems[ABC_ISOP_MAX_VAR+1][ABC_ISOP_MAX_VAR > 6 ? (1 << (ABC_ISOP_MAX_VAR-6)) : 1], * pTtElems[ABC_ISOP_MAX_VAR+1] = {NULL};
-    if ( pTtElems[0] == NULL )
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] & pIn2[w] )
+            return 1;
+    return 0;
+}
+static inline int Abc_TtCheckWithCubePos2Neg( word * t, word * c, int nWords, int iVar )
+{
+    if ( iVar < 6 )
     {
-        int v;
-        for ( v = 0; v <= ABC_ISOP_MAX_VAR; v++ )
-            pTtElems[v] = TtElems[v];
-        Abc_TtElemInit( pTtElems, ABC_ISOP_MAX_VAR );
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & (c[i] >> Shift) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[Step+i] & c[i] )
+                    return 0;
+        return 1;
     }
-    return pTtElems;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Create truth table for the given cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_IsopBuildTruth( Vec_Int_t * vCover, int nVars, word * pRes, int fXor, int fCompl )
+static inline int Abc_TtCheckWithCubeNeg2Pos( word * t, word * c, int nWords, int iVar )
 {
-    word ** pTtElems = Abc_IsopTtElems();
-    word pCube[1024];
-    int nWords = Abc_TtWordNum( nVars );
-    int c, v, Cube;
-    Abc_TtClear( pRes, nWords );
-    Vec_IntForEachEntry( vCover, Cube, c )
+    if ( iVar < 6 )
     {
-        Abc_TtFill( pCube, nWords );
-        for ( v = 0; v < nVars; v++ )
-            if ( ((Cube >> (v << 1)) & 3) == 1 )
-                Abc_TtSharp( pCube, pCube, pTtElems[v], nWords );
-            else if ( ((Cube >> (v << 1)) & 3) == 2 )
-                Abc_TtAnd( pCube, pCube, pTtElems[v], nWords, 0 );
-        if ( fXor )
-            Abc_TtXor( pRes, pRes, pCube, nWords, 0 );
-        else
-            Abc_TtOr( pRes, pRes, pCube, nWords );
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & (c[i] << Shift) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] & c[Step+i] )
+                    return 0;
+        return 1;
     }
-    if ( fCompl )
-        Abc_TtNot( pRes, nWords );
 }
-static inline void Abc_IsopVerify( word * pFunc, int nVars, word * pRes, Vec_Int_t * vCover, int fXor, int fCompl )
+static inline void Abc_TtExpandCubePos2Neg( word * t, int nWords, int iVar )
 {
-    Abc_IsopBuildTruth( vCover, nVars, pRes, fXor, fCompl );
-    if ( !Abc_TtEqual( pFunc, pRes, Abc_TtWordNum(nVars) ) )
-        printf( "Verification failed.\n" );
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            t[i] |= (t[i] >> Shift);
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                t[i] = t[Step+i];
+    }
 }
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure assumes that function has exact support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_Isop( word * pFunc, int nVars, int Type, int nCubeLim, Vec_Int_t * vCover )
+static inline void Abc_TtExpandCubeNeg2Pos( word * t, int nWords, int iVar )
 {
-    word pRes[1024];
-    int Limit = nCubeLim ? nCubeLim : 0xFFFF; 
-    int LimitXor = nCubeLim ? 3 * Limit : 3 * (nVars + 1); 
-    int nCost0 = -1, nCost1 = -1, nCost2 = -1;
-    assert( nVars <= 16 );
-    assert( Abc_TtHasVar( pFunc, nVars, nVars - 1 ) );
-    assert( !(Type & 4) );
-    // xor polarity
-    if ( Type & 4 )
-        nCost2 = Abc_EsopCheck( pFunc, nVars, LimitXor << 16, NULL );
-    // direct polarity
-    if ( Type & 1 )
-        nCost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_MinInt(Limit, 3*nCost2) << 16, NULL );
-    // opposite polarity
-    if ( Type & 2 )
+    if ( iVar < 6 )
     {
-        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-        nCost1 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_MinInt(nCost0, Abc_MinInt(Limit, 3*nCost2)) << 16, NULL );
-        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            t[i] |= (t[i] << Shift);
     }
-    assert( nCost0 >= 0 || nCost1 >= 0 );
-    // find minimum cover
-    if ( nCost0 <= nCost1 || nCost0 != -1 )
+    else
     {
-        Vec_IntFill( vCover, -1, nCost0 >> 16 );
-        Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
-        Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
-        return 0;
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                t[Step+i] = t[i];
     }
-    if ( nCost1 < nCost0 || nCost1 != -1 )
+}
+word Abc_IsopNew( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover )
+{
+    word pCube[ABC_ISOP_MAX_WORD];
+    word pOnset[ABC_ISOP_MAX_WORD];
+    word pOffset[ABC_ISOP_MAX_WORD];
+    int pBlocks[16], nBlocks, vTwo, uTwo;
+    int nWords = Abc_TtWordNum(nVars);
+    int c, v, u, iMint, Cube, nLits = 0;
+    assert( nVars <= ABC_ISOP_MAX_VAR );
+    Abc_TtClear( pRes, nWords );
+    Abc_TtCopy( pOnset, pOn, nWords, 0 ); 
+    Abc_TtCopy( pOffset, pOnDc, nWords, 1 ); 
+    if ( nVars < 6 )
+        pOnset[0] >>= (64 - (1 << nVars));
+    for ( c = 0; !Abc_TtIsConst0(pOnset, nWords); c++ )
     {
-        Vec_IntFill( vCover, -1, nCost1 >> 16 );
-        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-        Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
-        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-        Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
-        return 1;
+        // pick one minterm
+        iMint = Abc_TtFindFirstBit(pOnset, nVars);
+        for ( Cube = v = 0; v < nVars; v++ )
+            Cube |= (1 << Abc_Var2Lit(v, (iMint >> v) & 1));
+        // check expansion for the minterm
+        nBlocks = 0;
+        for ( v = 0; v < nVars; v++ )
+            if ( (pBlocks[v] = Abc_TtGetBit(pOffset, iMint ^ (1 << v))) )
+                nBlocks++;
+        // check second step
+        if ( nBlocks == nVars ) // cannot expand
+        {
+            Abc_TtSetBit( pRes, iMint );
+            Abc_TtXorBit( pOnset, iMint );
+            pCover[c] = Cube;
+            nLits += nVars;
+            continue;
+        }
+        // check dual expansion
+        vTwo = uTwo = -1;
+        if ( nBlocks < nVars - 1 )
+        {
+            for ( v = 0; v < nVars && vTwo == -1; v++ )
+            if ( !pBlocks[v] )
+            for ( u = v + 1; u < nVars; u++ )
+            if ( !pBlocks[u] )
+            {
+                if ( Abc_TtGetBit( pOffset, iMint ^ (1 << v) ^ (1 << u) ) )
+                    continue;
+                // can expand both directions
+                vTwo = v;
+                uTwo = u;
+                break;
+            }
+        }
+        if ( vTwo == -1 ) // can expand only one
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( !pBlocks[v] )
+                    break;
+            Abc_TtSetBit( pRes, iMint );
+            Abc_TtSetBit( pRes, iMint ^ (1 << v) );
+            Abc_TtXorBit( pOnset, iMint );
+            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << v)) )
+                Abc_TtXorBit( pOnset, iMint ^ (1 << v) );
+            pCover[c] = Cube & ~(3 << Abc_Var2Lit(v, 0));
+            nLits += nVars - 1;
+            continue;
+        }
+        if ( nBlocks == nVars - 2 && vTwo >= 0 ) // can expand only these two
+        {
+            Abc_TtSetBit( pRes, iMint );
+            Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) );
+            Abc_TtSetBit( pRes, iMint ^ (1 << uTwo) );
+            Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
+            Abc_TtXorBit( pOnset, iMint );
+            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo)) )
+                Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) );
+            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << uTwo)) )
+                Abc_TtXorBit( pOnset, iMint ^ (1 << uTwo) );
+            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo)) )
+                Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
+            pCover[c] = Cube & ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
+            nLits += nVars - 2;
+            continue;
+        }
+        // can expand others as well
+        Abc_TtClear( pCube, nWords );
+        Abc_TtSetBit( pCube, iMint );
+        Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) );
+        Abc_TtSetBit( pCube, iMint ^ (1 << uTwo) );
+        Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
+        Cube &= ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
+        assert( !Abc_TtIntersect(pCube, pOffset, nWords) );        
+        // expand against offset
+        for ( v = 0; v < nVars; v++ )
+        if ( v != vTwo && v != uTwo )
+        {
+            int Shift = Abc_Var2Lit( v, 0 );
+            if ( (Cube >> Shift) == 2 && Abc_TtCheckWithCubePos2Neg(pOffset, pCube, nWords, v) ) // pos literal
+            {
+                Abc_TtExpandCubePos2Neg( pCube, nWords, v );
+                Cube &= ~(3 << Shift);
+            }
+            else if ( (Cube >> Shift) == 1 && Abc_TtCheckWithCubeNeg2Pos(pOffset, pCube, nWords, v) ) // neg literal
+            {
+                Abc_TtExpandCubeNeg2Pos( pCube, nWords, v );
+                Cube &= ~(3 << Shift);
+            }
+            else 
+                nLits++;
+        }
+        // add cube to solution
+        Abc_TtOr( pRes, pRes, pCube, nWords );
+        Abc_TtSharp( pOnset, pOnset, pCube, nWords );
+        pCover[c] = Cube;
     }
-    assert( 0 );
-    return -1;
+    pRes[0] = Abc_Tt6Stretch( pRes[0], nVars );
+    return Abc_Cube2Cost(c) | nLits;
+}
+void Abc_IsopTestNew()
+{
+    int nVars = 4;
+    Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
+    word r, t = (s_Truths6[0] & s_Truths6[1]) ^ (s_Truths6[2] & s_Truths6[3]), copy = t;
+//    word r, t = ~s_Truths6[0] | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]), copy = t;
+//    word r, t = 0xABCDABCDABCDABCD, copy = t;
+//    word r, t = 0x6996000000006996, copy = t;
+//    word Cost = Abc_IsopNew( &t, &t, &r, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
+    word Cost = Abc_EsopCheck( &t, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
+    vCover->nSize = Abc_CostCubes(Cost);
+    assert( vCover->nSize <= vCover->nCap );
+    printf( "Cubes = %d.  Lits = %d.\n", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+    Abc_IsopPrintCover( vCover, nVars, 0 );
+    Abc_IsopVerify( &copy, nVars, &r, vCover, 1, 0 );
+    Vec_IntFree( vCover );
 }
 
 /**Function*************************************************************
@@ -577,53 +1021,115 @@ int Abc_Isop( word * pFunc, int nVars, int Type, int nCubeLim, Vec_Int_t * vCove
 ***********************************************************************/
 int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
 {
-    int Cost, fVerbose = 0;
-    word pRes[1024];
+    int fVerbose = 0;    
+    static word TotalCost[6] = {0};
+    static abctime TotalTime[6] = {0};
+    static int Counter;
+    word pRes[ABC_ISOP_MAX_WORD];
+    word Cost;
+    abctime clk;
+    Counter++;
+    if ( Counter == 9999 )
+    {
+        Abc_PrintTime( 1, "0", TotalTime[0] );
+        Abc_PrintTime( 1, "1", TotalTime[1] );
+        Abc_PrintTime( 1, "2", TotalTime[2] );
+        Abc_PrintTime( 1, "3", TotalTime[3] );
+        Abc_PrintTime( 1, "4", TotalTime[4] );
+        Abc_PrintTime( 1, "5", TotalTime[5] );
+    }
+    assert( nVars <= ABC_ISOP_MAX_VAR );
 //    if ( fVerbose )
 //    Dau_DsdPrintFromTruth( pFunc, nVars ), printf( "         " );
 
-    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
-    vCover->nSize = Cost >> 16;
+    clk = Abc_Clock();
+    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
+    vCover->nSize = Abc_CostCubes(Cost);
     assert( vCover->nSize <= vCover->nCap );
     if ( fVerbose )
-    printf( "%5d(%5d) ", Cost >> 16, Cost & 0xFFFF );
-    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
+    printf( "%5d %7d  ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
+    TotalCost[0] += Abc_CostCubes(Cost);
+    TotalTime[0] += Abc_Clock() - clk;
 
 
+    clk = Abc_Clock();
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
+    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-    vCover->nSize = Cost >> 16;
+    vCover->nSize = Abc_CostCubes(Cost);
     assert( vCover->nSize <= vCover->nCap );
     if ( fVerbose )
-    printf( "%5d(%5d) ", Cost >> 16, Cost & 0xFFFF );
-    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
-
-
-    Cost = Abc_EsopCheck( pFunc, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
-    vCover->nSize = Cost >> 16;
+    printf( "%5d %7d  ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
+    TotalCost[1] += Abc_CostCubes(Cost);
+    TotalTime[1] += Abc_Clock() - clk;
+
+/*
+    clk = Abc_Clock();
+    Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
+    vCover->nSize = Abc_CostCubes(Cost);
     assert( vCover->nSize <= vCover->nCap );
     if ( fVerbose )
-    printf( "%5d(%5d)  ", Cost >> 16, Cost & 0xFFFF );
-    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 0 );
+    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 0 );
+    TotalCost[2] += Abc_CostCubes(Cost);
+    TotalTime[2] += Abc_Clock() - clk;
 
 
+    clk = Abc_Clock();
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-    Cost = Abc_EsopCheck( pFunc, nVars, ABC_INFINITY, Vec_IntArray(vCover) );
+    Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
     Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
-    vCover->nSize = Cost >> 16;
+    vCover->nSize = Abc_CostCubes(Cost);
     assert( vCover->nSize <= vCover->nCap );
     if ( fVerbose )
-    printf( "%5d(%5d)  ", Cost >> 16, Cost & 0xFFFF );
-    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
+    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
+    TotalCost[3] += Abc_CostCubes(Cost);
+    TotalTime[3] += Abc_Clock() - clk;
+*/
+
+/*
+    // try new computation
+    clk = Abc_Clock();
+    Cost = Abc_IsopNew( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
+    vCover->nSize = Abc_CostCubes(Cost);
+    assert( vCover->nSize <= vCover->nCap );
+    if ( fVerbose )
+    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
+    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
+    TotalCost[4] += Abc_CostCubes(Cost);
+    TotalTime[4] += Abc_Clock() - clk;
+*/
+
+    // try old computation
+    clk = Abc_Clock();
+    Cost = Kit_TruthIsop( (unsigned *)pFunc, nVars, vCover, 1 );
+    vCover->nSize = Vec_IntSize(vCover);
+    assert( vCover->nSize <= vCover->nCap );
+    if ( fVerbose )
+    printf( "%5d %7d   ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
+    TotalCost[4] += Vec_IntSize(vCover);
+    TotalTime[4] += Abc_Clock() - clk;
 
 
+    clk = Abc_Clock();
+    Cost = Abc_Isop( pFunc, nVars, ABC_ISOP_MAX_CUBE, vCover, 1 );
+    if ( fVerbose )
+    printf( "%5d %7d   ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
+    TotalCost[5] += Vec_IntSize(vCover);
+    TotalTime[5] += Abc_Clock() - clk;
+
+    if ( fVerbose )
+    printf( "  | %8d %8d %8d %8d %8d %8d", (int)TotalCost[0], (int)TotalCost[1], (int)TotalCost[2], (int)TotalCost[3], (int)TotalCost[4], (int)TotalCost[5] );
     if ( fVerbose )
     printf( "\n" );
-//Kit_TruthIsopPrintCover( vCover, nVars, 0 );
+//Abc_IsopPrintCover( vCover, nVars, 0 );
     return 1; 
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////