Version abc51225

8 files changed, 1147 insertions, 91 deletions

diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
index f18686ff..ea488068 100644
--- a/src/opt/xyz/xyz.h
+++ b/src/opt/xyz/xyz.h
@@ -46,6 +46,8 @@ struct Xyz_Man_t_
     Vec_Ptr_t *       vObjStrs;     // object structures
     void *            pMemory;      // memory for the internal data strctures
     Min_Man_t *       pManMin;      // the cub manager
+    int               fUseEsop;     // enables ESOPs
+    int               fUseSop;      // enables SOPs
     // arrays to map local variables
     Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
     Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
index a48f749e..e5089788 100644
--- a/src/opt/xyz/xyzCore.c
+++ b/src/opt/xyz/xyzCore.c
@@ -27,13 +27,19 @@
 static void        Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
 static int         Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
 static void        Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
-
+/*
 static int         Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
 static int         Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
 static int         Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+*/
+
+static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj );
+static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -59,6 +65,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
 
     // create the manager
     p = Xyz_ManAlloc( pNtk, nFaninMax );
+    p->fUseEsop = fUseEsop;
+    p->fUseSop  = 1;//fUseSop;
     pNtk->pManCut = p;
 
     // perform mapping
@@ -69,6 +77,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
         pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
     else
         pNtkNew = Abc_NtkXyzDerive( p, pNtk );
+//    pNtkNew = NULL;
+
 
     Xyz_ManFree( p );
     pNtk->pManCut = NULL;
@@ -164,7 +174,10 @@ int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
         } 
 
         // traverse the cone starting from this node
-        Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+        if ( Abc_ObjGetSupp(pObj) == NULL )
+            Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+
+        // count the number of solved cones
         if ( Abc_ObjGetSupp(pObj) == NULL )
             fStop = 0;
         else
@@ -225,7 +238,7 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
 {
     Abc_Obj_t * pObj0, * pObj1;
     // return if the support is already computed
-    if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) )
+    if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
         return;
     // mark as visited
     pObj->fMarkB = 1;
@@ -236,9 +249,9 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
     Abc_NtkXyzCovers_rec( p, pObj0, vBoundary );
     Abc_NtkXyzCovers_rec( p, pObj1, vBoundary );
     // skip the node that spaced out
-    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||     // fanin is not ready
-         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||     // fanin is not ready
-         !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) )  // node's support or covers cannot be computed
+    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||  // fanin is not ready
+         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||  // fanin is not ready
+         !Abc_NodeXyzPropagate( p, pObj ) )           // node's support or covers cannot be computed
     {
         // save the nodes of the future boundary
         if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
@@ -331,6 +344,321 @@ Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * v
 
 /**Function*************************************************************
 
+  Synopsis    [Propagates all types of covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj )
+{
+    Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
+    Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
+    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
+    Abc_Obj_t * pObj0, * pObj1;
+    int fCompl0, fCompl1;
+
+    pObj0 = Abc_ObjFanin0( pObj );
+    pObj1 = Abc_ObjFanin1( pObj );
+
+    if ( pObj0->fMarkA )  Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
+    if ( pObj1->fMarkA )  Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
+
+    // get the resulting support
+    vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
+    vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
+    vSupp  = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
+
+    // quit if support if too large
+    if ( vSupp->nSize > p->nFaninMax )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // get the complemented attributes
+    fCompl0 = Abc_ObjFaninC0( pObj );
+    fCompl1 = Abc_ObjFaninC1( pObj );
+
+    // propagate ESOP
+    if ( p->fUseEsop )
+    {
+        // get the covers
+        pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
+        pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
+        if ( pCov0 && pCov1 )
+        {
+            // complement the first if needed
+            if ( !fCompl0 )
+                pCover0 = pCov0;
+            else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+                pCover0 = pCov0->pNext;
+            else
+                pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
+
+            // complement the second if needed
+            if ( !fCompl1 )
+                pCover1 = pCov1;
+            else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+                pCover1 = pCov1->pNext;
+            else
+                pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
+
+            // derive the new cover
+            pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize );
+        }
+    }
+    // propagate SOPs
+    if ( p->fUseSop )
+    {
+        // get the covers for the direct polarity
+        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
+        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
+        // derive the new cover
+        if ( pCover0 && pCover1 )
+            pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize );
+
+        // get the covers for the inverse polarity
+        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
+        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
+        // derive the new cover
+        if ( pCover0 && pCover1 )
+            pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize );
+    }
+
+    // if none of the covers can be computed quit
+    if ( !pCoverX && !pCoverP && !pCoverN )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // set the covers
+    assert( Abc_ObjGetSupp(pObj) == NULL );
+    Abc_ObjSetSupp( pObj, vSupp );
+    Abc_ObjSetCover( pObj, pCoverP, 0 );
+    Abc_ObjSetCover( pObj, pCoverN, 1 );
+    Abc_ObjSetCover2( pObj, pCoverX );
+//printf( "%3d : %4d  %4d  %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );
+
+    // count statistics
+    p->nSupps++;
+    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    Min_Cube_t * pCover;
+    int i, Val0, Val1;
+    assert( pCover0 && pCover1 );
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        // go through the support variables of the cubes
+        for ( i = 0; i < p->vPairs0->nSize; i++ )
+        {
+            Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
+            Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
+            if ( (Val0 & Val1) == 0 )
+                break;
+        }
+        // check disjointness
+        if ( i < p->vPairs0->nSize )
+            continue;
+
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+//Min_CoverWriteFile( pCover, "large", 1 );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+
+        // create the product cube
+        pCube = Min_CubeAlloc( p->pManMin );
+
+        // add the literals
+        pCube->nLits = 0;
+        for ( i = 0; i < nSupp; i++ )
+        {
+            if ( p->vComTo0->pArray[i] == -1 )
+                Val0 = 3;
+            else
+                Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+
+            if ( p->vComTo1->pArray[i] == -1 )
+                Val1 = 3;
+            else
+                Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+
+            if ( (Val0 & Val1) == 3 )
+                continue;
+
+            Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
+            pCube->nLits++;
+        }
+        // add the cube to storage
+        if ( fEsop ) 
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+
+    // minimize the cover
+    if ( fEsop ) 
+        Min_EsopMinimize( p->pManMin );
+    else
+        Min_SopMinimize( p->pManMin );
+    pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+    // quit if the cover is too large
+    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+    {
+/*        
+Min_CoverWriteFile( pCover, "large", 1 );
+        Min_CoverExpand( p->pManMin, pCover );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        pCover = Min_CoverCollect( p->pManMin, nSupp );
+*/
+        Min_CoverRecycle( p->pManMin, pCover );
+        return NULL;
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    Min_Cube_t * pCover;
+    int i, Val0, Val1;
+    assert( pCover0 && pCover1 );
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    Min_CoverForEachCube( pCover0, pCube0 )
+    {
+        // create the cube
+        pCube = Min_CubeAlloc( p->pManMin );
+        pCube->nLits = 0;
+        for ( i = 0; i < p->vComTo0->nSize; i++ )
+        {
+            if ( p->vComTo0->pArray[i] == -1 )
+                continue;
+            Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+            if ( Val0 == 3 )
+                continue;
+            Min_CubeXorVar( pCube, i, Val0 ^ 3 );
+            pCube->nLits++;
+        }
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+        // add the cube to storage
+        if ( fEsop )
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        // create the cube
+        pCube = Min_CubeAlloc( p->pManMin );
+        pCube->nLits = 0;
+        for ( i = 0; i < p->vComTo1->nSize; i++ )
+        {
+            if ( p->vComTo1->pArray[i] == -1 )
+                continue;
+            Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+            if ( Val1 == 3 )
+                continue;
+            Min_CubeXorVar( pCube, i, Val1 ^ 3 );
+            pCube->nLits++;
+        }
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+        // add the cube to storage
+        if ( fEsop )
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+
+    // minimize the cover
+    if ( fEsop ) 
+        Min_EsopMinimize( p->pManMin );
+    else
+        Min_SopMinimize( p->pManMin );
+    pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+    // quit if the cover is too large
+    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+    {
+        Min_CoverRecycle( p->pManMin, pCover );
+        return NULL;
+    }
+    return pCover;
+}
+
+
+
+
+
+
+
+#if 0
+
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -581,7 +909,7 @@ int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pC
             pCube->nLits++;
         }
         // add the cube to storage
-        while ( Min_EsopAddCube( p->pManMin, pCube ) );
+        Min_EsopAddCube( p->pManMin, pCube );
     }
     return 1;
 }
@@ -642,7 +970,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
             if ( p->pManMin->nCubes >= p->nCubesMax )
                 return 0;
             // add the cube to storage
-            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+            Min_EsopAddCube( p->pManMin, pCube );
         }
     }
     if ( pCover1 )
@@ -665,7 +993,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
             if ( p->pManMin->nCubes >= p->nCubesMax )
                 return 0;
             // add the cube to storage
-            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+            Min_EsopAddCube( p->pManMin, pCube );
         }
     }
     return 1;
@@ -688,7 +1016,7 @@ int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCove
 }
 
 
-
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
index 22950bfd..656612aa 100644
--- a/src/opt/xyz/xyzInt.h
+++ b/src/opt/xyz/xyzInt.h
@@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa
 
 /*=== xyzMinEsop.c ==========================================================*/
 extern void         Min_EsopMinimize( Min_Man_t * p );
-extern int          Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void         Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
 /*=== xyzMinSop.c ==========================================================*/
 extern void         Min_SopMinimize( Min_Man_t * p );
-extern int          Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void         Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
 /*=== xyzMinMan.c ==========================================================*/
 extern Min_Man_t *  Min_ManAlloc( int nVars );
 extern void         Min_ManClean( Min_Man_t * p, int nSupp );
@@ -92,8 +92,10 @@ extern void         Min_ManFree( Min_Man_t * p );
 /*=== xyzMinUtil.c ==========================================================*/
 extern void         Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
 extern void         Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
+extern void         Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
 extern void         Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
 extern void         Min_CoverCheck( Min_Man_t * p );
+extern int          Min_CubeCheck( Min_Cube_t * pCube );
 extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
 extern void         Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
 extern int          Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
@@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
     Min_Cube_t * pCube;
     pCube = Min_CubeAlloc( p );
     memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+    pCube->nLits = pCopy->nLits;
     return pCube;
 }
 
@@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms the cube into the result of distance-1 merging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
+{
+    int w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+        pCube->uData[w] |= pDist->uData[w];
+}
+
 
 
 /**Function*************************************************************
@@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
 
 /**Function*************************************************************
 
-  Synopsis    [Check if the cube is equal or dist1 or contained.]
+  Synopsis    [Returns 1 if the given cube is contained in one of the cubes of the cover.]
 
   Description []
                
@@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
+static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    Min_Cube_t * pCube;
+    Min_Cube_t * pThis;
     int i;
-    // check identity
-    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
-        if ( Min_CubesAreEqual( pCube, pNew ) )
+/*
+    // this cube cannot be equal to any cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeWrite( stdout, pCube );
+            assert( 0 );
+        }
+    }
+*/
+    // try to find a containing cube
+    for ( i = 0; i <= (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        // skip the bubble
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
             return 1;
-    // check containment
-    for ( i = 0; i < (int)pNew->nLits; i++ )
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-            if ( Min_CubeIsContained( pCube, pNew ) )
-                return 1;
+    }
     return 0;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Check if the cube is equal or dist1 or contained.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
-{
-    Min_Cube_t * pCube;
-    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
-        if ( Min_CubesDistOne( pCube, pNew, NULL ) )
-            return pCube;
-    return NULL;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
index 114e28a6..839e2410 100644
--- a/src/opt/xyz/xyzMinEsop.c
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p )
 
   Synopsis    [Performs one round of rewriting using distance 2 cubes.]
 
-  Description []
+  Description [The weakness of this procedure is that it tries each cube
+  with only one distance-2 cube. If this pair does not lead to improvement
+  the cube is inserted into the cover anyhow, and we try another pair.
+  A possible improvement would be to try this cube with all distance-2
+  cubes, until an improvement is found, or until all such cubes are tried.]
                
   SideEffects []
 
@@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p )
 
         // add the cubes
         nCubesOld = p->nCubes;
-        while ( Min_EsopAddCube( p, pCube ) );
-        while ( Min_EsopAddCube( p, pThis ) );
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
         // check if the cubes were absorbed
         if ( p->nCubes < nCubesOld + 2 )
             continue;
@@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p )
         pThis->nLits += (v11 != 3);
 
         // add them anyhow
-        while ( Min_EsopAddCube( p, pCube ) );
-        while ( Min_EsopAddCube( p, pThis ) );
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
     }
 //    printf( "Pairs = %d  ", nPairs );
 }
@@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p )
 
   Synopsis    [Adds the cube to storage.]
 
-  Description [If the distance one cube is found, returns the transformed
-  cube. If there is no distance one, adds the given cube to storage.
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.
   Do not forget to clean the storage!]
                
   SideEffects []
@@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
 {
     Min_Cube_t * pThis, ** ppPrev;
     // try to find the identical cube
@@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_EsopAddCubeInt( p, pCube ) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
index 423564c1..20314698 100644
--- a/src/opt/xyz/xyzMinMan.c
+++ b/src/opt/xyz/xyzMinMan.c
@@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars )
     pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );   
     pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
     pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    Min_ManClean( pMan, nVars );
     return pMan;
 }
 
diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
index 1c5951fe..a5d57c66 100644
--- a/src/opt/xyz/xyzMinSop.c
+++ b/src/opt/xyz/xyzMinSop.c
@@ -52,10 +52,11 @@ void Min_SopMinimize( Min_Man_t * p )
         nCubesOld = p->nCubes;
         Min_SopRewrite( p );
         nIter++;
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
     }
     while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+//    printf( "\n" );
 
-//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
 }
 
 /**Function*************************************************************
@@ -74,8 +75,17 @@ void Min_SopRewrite( Min_Man_t * p )
     Min_Cube_t * pCube, ** ppPrev;
     Min_Cube_t * pThis, ** ppPrevT;
     Min_Cube_t * pTemp;
-    int v00, v01, v10, v11, Var0, Var1, Index;
+    int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
     int nPairs = 0;
+/*    
+    {
+        Min_Cube_t * pCover;
+        pCover = Min_CoverCollect( p, p->nVars );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCover );
+        Min_CoverExpand( p, pCover );
+    }
+*/
 
     // insert the bubble before the first cube
     p->pBubble->pNext = p->ppStore[0];
@@ -127,7 +137,11 @@ void Min_SopRewrite( Min_Man_t * p )
             continue;
         }
         nPairs++;
-
+/*
+printf( "\n" );
+Min_CubeWrite( stdout, pCube );
+Min_CubeWrite( stdout, pThis );
+*/
         // remove the cubes, insert the bubble instead of pCube
         *ppPrevT = pThis->pNext;
         *ppPrev = p->pBubble;
@@ -135,6 +149,8 @@ void Min_SopRewrite( Min_Man_t * p )
         p->pBubble->nLits = pCube->nLits;
         p->nCubes -= 2;
 
+        assert( pCube != p->pBubble && pThis != p->pBubble );
+
 
         // save the dist2 parameters
         v00 = Min_CubeGetVar( pCube, Var0 );
@@ -145,22 +161,83 @@ void Min_SopRewrite( Min_Man_t * p )
         assert( v00 != 3   || v01 != 3 );
         assert( v10 != 3   || v11 != 3 );
 
-        // skip the case when rewriting is impossible
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // consider the case when both cubes have non-empty literals
         if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+        {
+            assert( v00 == (v10 ^ 3) );
+            assert( v01 == (v11 ^ 3) );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            Min_CubeXorVar( pCube, Var1, 3 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+            // check if this cube is contained
+            fCont1 = Min_CoverContainsCube( p, pCube );
+            // undo the change
+            Min_CubeXorVar( pCube, Var1, 3 );
+
+            // check if the cubes can be overwritten
+            if ( fCont0 && fCont1 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits -= 2;
+                Min_SopAddCube( p, pCube );
+            }
+            else if ( fCont0 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else if ( fCont1 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else
+            {
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+            // otherwise, no change is possible
             continue;
+        }
 
         // if one of them does not have DC lit, move it
         if ( v00 != 3 && v01 != 3 )
         {
+            assert( v10 == 3 || v11 == 3 );
             pTemp = pCube; pCube = pThis; pThis = pTemp;
             Index = v00; v00 = v10; v10 = Index;
             Index = v01; v01 = v11; v11 = Index;
         }
 
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
         // make sure the first cube has first var DC
         if ( v00 != 3 )
         {
@@ -174,13 +251,93 @@ void Min_SopRewrite( Min_Man_t * p )
         if ( v00 == 3 && v11 == 3 )
         {
             assert( v01 != 3 && v10 != 3 );
-            // try two reduced cubes
-
+            // try the remaining minterm
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits++;
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // undo the cube transformations
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits--;
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try two reduced cubes
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // remember the cubes
+                nCubesOld = p->nCubes;
+                Min_SopAddCube( p, pCube );
+                // check if the cube is absorbed
+                if ( p->nCubes < nCubesOld + 1 )
+                { // absorbed - add the second cube
+                    Min_SopAddCube( p, pThis );
+                }
+                else
+                { // remove this cube, and try another one
+                    assert( pCube == p->ppStore[pCube->nLits] );
+                    p->ppStore[pCube->nLits] = pCube->pNext;
+                    p->nCubes--;
+
+                    // return the cube to the previous state
+                    Min_CubeXorVar( pCube, Var0, v10 );
+                    pCube->nLits--;
+
+                    // generate another reduced cube
+                    Min_CubeXorVar( pThis, Var1, v01 );
+                    pThis->nLits++;
+
+                    // add both cubes
+                    Min_SopAddCube( p, pCube );
+                    Min_SopAddCube( p, pThis );
+                }
+            }
         }
         else // the first cube has DC lit
         {
             assert( v01 != 3 && v10 != 3 && v11 != 3 );
-            // try reduced and expanded cube
+            // try the remaining minterm
+            // create the temporary cube equal to the minterm
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pThis );
+            // undo the cube transformations
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try reshaping the cubes
+                // reduce the first cube
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // expand the second cube
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                // add both cubes
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
         }
     }
 //    printf( "Pairs = %d  ", nPairs );
@@ -188,26 +345,80 @@ void Min_SopRewrite( Min_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds cube to the SOP cover stored in the manager.]
 
-  Description []
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    return 1;
-}
-
+    Min_Cube_t * pThis, * pThis2, ** ppPrev;
+    int i;
+    // try to find the identical cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find a containing cube
+    for ( i = 0; i < (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find distance one in the same bin
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, NULL ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransformOr( pCube, pThis );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
 
+    // clean the other cubes using this one
+    for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
+    {
+        ppPrev = &p->ppStore[i];
+        Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
+        {
+            if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
+            {
+                *ppPrev = pThis->pNext;
+                Min_CubeRecycle( p, pThis );
+                p->nCubes--;
+            }
+            else
+                ppPrev = &pThis->pNext;
+        }
+    }
 
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds the cube to storage.]
 
   Description []
                
@@ -216,27 +427,18 @@ int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
   SeeAlso     []
 
 ***********************************************************************/
-void Min_SopDist1Merge( Min_Man_t * p )
+void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    Min_Cube_t * pCube, * pCube2, * pCubeNew;
-    int i;
-    for ( i = p->nVars; i >= 0; i-- )
-    {
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-        Min_CoverForEachCube( pCube->pNext, pCube2 )
-        {
-            assert( pCube->nLits == pCube2->nLits );
-            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
-                continue;
-            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
-            assert( pCubeNew->nLits == pCube->nLits - 1 );
-            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
-            p->ppStore[pCubeNew->nLits] = pCubeNew;
-            p->nCubes++;
-        }
-    }
+    assert( Min_CubeCheck( pCube ) );
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_SopAddCubeInt( p, pCube ) );
 }
 
+
+
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -286,6 +488,38 @@ void Min_SopContain( Min_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, * pCubeNew;
+    int i;
+    for ( i = p->nVars; i >= 0; i-- )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCube( pCube->pNext, pCube2 )
+        {
+            assert( pCube->nLits == pCube2->nLits );
+            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+                continue;
+            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+            assert( pCubeNew->nLits == pCube->nLits - 1 );
+            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+            p->ppStore[pCubeNew->nLits] = pCubeNew;
+            p->nCubes++;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
 {
      Vec_Int_t * vVars;
@@ -334,6 +568,46 @@ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
      return Min_CoverCollect( p, p->nVars );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pThis;
+    int i;
+
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, 2*0+1 );
+    Min_CubeXorBit( pCube, 2*1+1 );
+    Min_CubeXorBit( pCube, 2*2+0 );
+    Min_CubeXorBit( pCube, 2*3+0 );
+    Min_CubeXorBit( pCube, 2*4+0 );
+    Min_CubeXorBit( pCube, 2*5+1 );
+    Min_CubeXorBit( pCube, 2*6+1 );
+    pCube->nLits = 7;
+
+//    Min_CubeWrite( stdout, pCube );
+
+    // check that the cubes contain it
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pThis )
+            if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                return 1;
+            }
+    Min_CubeRecycle( p, pCube );
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
index 0aebb815..9ec5f83f 100644
--- a/src/opt/xyz/xyzMinUtil.c
+++ b/src/opt/xyz/xyzMinUtil.c
@@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
   SeeAlso     []
 
 ***********************************************************************/
+void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        {
+            printf( "%2d : ", i );
+            if ( pCube == p->pBubble )
+            {
+                printf( "Bubble\n" );
+                continue;
+            }
+            Min_CubeWrite( pFile, pCube );
+        }
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
 {
     char Buffer[1000];
     Min_Cube_t * pCube;
     FILE * pFile;
     int i;
-    sprintf( Buffer, "%s.esop", pName );
+    sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
     for ( i = strlen(Buffer) - 1; i >= 0; i-- )
         if ( Buffer[i] == '<' || Buffer[i] == '>' )
             Buffer[i] = '_';
@@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+  Synopsis    []
 
   Description []
                
@@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CubeCheck( Min_Cube_t * pCube )
+{
+    int i;
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeGetVar( pCube, i ) == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converts the cover from the sorted structure.]
 
   Description []
@@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
             assert( i == (int)pCube->nLits );
             *ppTail = pCube; 
             ppTail = &pCube->pNext;
+            assert( pCube->uData[0] ); // not a bubble
         }
     }
     *ppTail = NULL;
diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
index 6c0a63f3..38580790 100644
--- a/src/opt/xyz/xyzTest.c
+++ b/src/opt/xyz/xyzTest.c
@@ -39,11 +39,377 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
+Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
 {
-    return NULL;
+    Min_Cube_t * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
+{
+    Min_Cube_t * pCover;
+    Min_Cube_t * pThis, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // add the cubes to storage
+    Min_CoverForEachCube( pCover0, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_CoverForEachCube( pCover1, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCov0[2], * pCov1[2];
+    Min_Cube_t * pCoverP, * pCoverN;
+    Abc_Obj_t * pObj;
+    int i, nCubes, fCompl0, fCompl1;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+    {
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+        pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
+    }
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // get the complements
+        fCompl0 = Abc_ObjFaninC0(pObj);
+        fCompl1 = Abc_ObjFaninC1(pObj);
+        // get the covers
+        pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
+        pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
+        pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
+        pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
+        // compute the covers
+        pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
+        pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
+        // set the covers
+        pObj->pCopy = (Abc_Obj_t *)pCoverP;
+        pObj->pNext = (Abc_Obj_t *)pCoverN;
+    }
+
+     nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
+
+/*
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverP );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverN );
+*/
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    Min_CoverExpand( p, pCoverP );
+//    Min_SopMinimize( p );
+//    pCoverP = Min_CoverCollect( p, p->nVars );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    nCubes = Min_CoverCountCubes(pCoverP);
+
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+
+//    Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverN );
+    return nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestSop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkCleanNext(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 )
+{
+    Min_Cube_t * pCover0, * pCover1, * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+
+    // complement the first if needed
+    if ( !fComp0 )
+        pCover0 = pCov0;
+    else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+        pCover0 = pCov0->pNext;
+    else
+        pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
+
+    // complement the second if needed
+    if ( !fComp1 )
+        pCover1 = pCov1;
+    else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+        pCover1 = pCov1->pNext;
+    else
+        pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
+
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_EsopAddCube( p, pCube );
+    }
+ 
+    if ( p->nCubes > 10 )
+    {
+//        printf( "(%d,", p->nCubes );
+        Min_EsopMinimize( p );
+//        printf( "%d) ", p->nCubes );
+    }
+
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+
+//    if ( p->nCubes > 1000 )
+//        printf( "%d ", p->nCubes );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pCover = Abc_NodeDeriveCover( p,  
+            (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,  
+            (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
+            Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        pObj->pCopy = (Abc_Obj_t *)pCover;
+        if ( p->nCubes > 3000 )
+            return -1;
+    }
+
+    // add complement if needed
+    if ( Abc_ObjFaninC0(pRoot) )
+    {
+        if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
+        {
+            pCube = pCover;
+            pCover = pCover->pNext;
+            Min_CubeRecycle( p, pCube );
+            p->nCubes--;
+        }
+        else
+        {
+            pCube = Min_CubeAlloc( p );
+            pCube->pNext = pCover;
+            p->nCubes++;
+        }
+    }
+/*
+    Min_CoverExpand( p, pCover );
+    Min_EsopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+*/
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = NULL;
+
+//    Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
+//    Min_CoverWrite( stdout, pCover );
+    return p->nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestEsop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////