Version abc60803

35 files changed, 1791 insertions, 4234 deletions

diff --git a/src/temp/deco/deco.h b/src/temp/deco/deco.h
index 89119c78..67126902 100644
--- a/src/temp/deco/deco.h
+++ b/src/temp/deco/deco.h
@@ -51,11 +51,15 @@ struct Dec_Node_t_
     Dec_Edge_t        eEdge1;          // the right child of the node
     // other info
     void *            pFunc;           // the function of the node (BDD or AIG)
-    unsigned          Level    : 16;   // the level of this node in the global AIG
+    unsigned          Level    : 14;   // the level of this node in the global AIG
     // printing info 
     unsigned          fNodeOr  :  1;   // marks the original OR node
     unsigned          fCompl0  :  1;   // marks the original complemented edge
     unsigned          fCompl1  :  1;   // marks the original complemented edge
+    // latch info
+    unsigned          nLat0    :  5;   // the number of latches on the first edge
+    unsigned          nLat1    :  5;   // the number of latches on the second edge
+    unsigned          nLat2    :  5;   // the number of latches on the output edge
 };
 
 typedef struct Dec_Graph_t_ Dec_Graph_t;
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 8c5f130b..7fb054f7 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -80,6 +80,8 @@ struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)
     int              nRefs;          // reference counter
     Ivy_Obj_t *      pFanin0;        // fanin
     Ivy_Obj_t *      pFanin1;        // fanin
+    Ivy_Obj_t *      pFanout;        // fanout
+    Ivy_Obj_t *      pEquiv;         // equivalent node
 };
 
 // the AIG manager
@@ -136,6 +138,9 @@ struct Ivy_Store_t_
     Ivy_Cut_t   pCuts[IVY_CUT_LIMIT]; // storage for cuts
 };
 
+#define IVY_LEAF_MASK     255
+#define IVY_LEAF_BITS       8
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -170,9 +175,9 @@ static inline Ivy_Edge_t   Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond )   { ret
 static inline Ivy_Edge_t   Ivy_EdgeFromNode( Ivy_Obj_t * pNode )           { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) );          }
 static inline Ivy_Obj_t *  Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
 
-static inline int          Ivy_LeafCreate( int Id, int Lat )      { return (Id << 4) | Lat;                     }
-static inline int          Ivy_LeafId( int Leaf )                 { return Leaf >> 4;                           }
-static inline int          Ivy_LeafLat( int Leaf )                { return Leaf & 15;                           }
+static inline int          Ivy_LeafCreate( int Id, int Lat )      { return (Id << IVY_LEAF_BITS) | Lat;         }
+static inline int          Ivy_LeafId( int Leaf )                 { return Leaf >> IVY_LEAF_BITS;               }
+static inline int          Ivy_LeafLat( int Leaf )                { return Leaf & IVY_LEAF_MASK;                }
 
 static inline int          Ivy_ManPiNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PI];                    }
 static inline int          Ivy_ManPoNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PO];                    }
@@ -261,12 +266,16 @@ static inline int          Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout
 static inline Ivy_Obj_t *  Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )    
 {
     Ivy_Obj_t * pGhost, * pTemp;
+    assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) );
+    assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) );
+    assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) );
+    assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) );
+//    assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) );
     pGhost = Ivy_ManGhost(p);
     pGhost->Type = Type;
     pGhost->Init = Init;
     pGhost->pFanin0 = p0;
     pGhost->pFanin1 = p1;
-    assert( Type == IVY_PI || Ivy_ObjFanin0(pGhost) != Ivy_ObjFanin1(pGhost) );
     if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
         pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
     return pGhost;
@@ -384,6 +393,7 @@ extern Vec_Int_t *     Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches );
 extern void            Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
 extern Vec_Vec_t *     Ivy_ManLevelize( Ivy_Man_t * p );
 extern Vec_Int_t *     Ivy_ManRequiredLevels( Ivy_Man_t * p );
+extern int             Ivy_ManIsAcyclic( Ivy_Man_t * p );
 /*=== ivyDsd.c ==========================================================*/
 extern int             Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
 extern void            Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -400,11 +410,14 @@ extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
 extern Ivy_Obj_t *     Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+/*=== ivyIsop.c ==========================================================*/
+extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover );
+extern void            Ivy_TruthManStop();
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
 extern void            Ivy_ManStop( Ivy_Man_t * p );
 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
-extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p );
+extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
 extern void            Ivy_ManPrintStats( Ivy_Man_t * p );
 extern void            Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits );
 /*=== ivyMem.c ==========================================================*/
@@ -425,8 +438,8 @@ extern void            Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew );
 extern void            Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
 extern void            Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
-extern void            Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop );
-extern void            Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode );
+extern void            Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel );
+extern void            Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel );
 /*=== ivyOper.c =========================================================*/
 extern Ivy_Obj_t *     Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
 extern Ivy_Obj_t *     Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
@@ -442,6 +455,8 @@ extern Ivy_Man_t *     Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbo
 extern int             Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
 extern int             Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
 extern int             Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
+/*=== ivySeq.c =========================================================*/
+extern int             Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
 /*=== ivyTable.c ========================================================*/
 extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
@@ -456,6 +471,7 @@ extern unsigned *      Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_In
 extern Vec_Int_t *     Ivy_ManLatches( Ivy_Man_t * p );
 extern int             Ivy_ManLevels( Ivy_Man_t * p );
 extern void            Ivy_ManResetLevels( Ivy_Man_t * p );
+extern int             Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew );
 extern int             Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index 4331c07e..36222f72 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -107,8 +107,8 @@ int Ivy_ManCheck( Ivy_Man_t * p )
             printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
             return 0;
         }
-//        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
-//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
+        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
+            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
         pObj2 = Ivy_TableLookup( p, pObj );
         if ( pObj2 != pObj )
             printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
@@ -124,6 +124,8 @@ int Ivy_ManCheck( Ivy_Man_t * p )
         printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
     }
+    if ( !Ivy_ManIsAcyclic(p) )
+        return 0;
     return 1;
 }
 
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 7d1ec63a..56f872e9 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Ivy_NodeCutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -580,6 +582,88 @@ static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the cut can be constructed; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_NodeCutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 )
+{
+    int i;
+    if ( pCut->nSize < pCut->nSizeMax )
+        return 1;
+    for ( i = 0; i < pCut->nSize; i++ )
+        if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_NodeCutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+    unsigned uHash = 0;
+    int i, k; 
+    assert( pCut->nSize > 0 );
+    assert( IdNew0 < IdNew1 );
+    for ( i = k = 0; i < pCut->nSize; i++ )
+    {
+        if ( pCut->pArray[i] == IdOld )
+            continue;
+        if ( IdNew0 <= pCut->pArray[i] )
+        {
+            if ( IdNew0 < pCut->pArray[i] )
+            {
+                pCutNew->pArray[ k++ ] = IdNew0;
+                uHash |= Ivy_NodeCutHashValue( IdNew0 );
+            }
+            IdNew0 = 0x7FFFFFFF;
+        }
+        if ( IdNew1 <= pCut->pArray[i] )
+        {
+            if ( IdNew1 < pCut->pArray[i] )
+            {
+                pCutNew->pArray[ k++ ] = IdNew1;
+                uHash |= Ivy_NodeCutHashValue( IdNew1 );
+            }
+            IdNew1 = 0x7FFFFFFF;
+        }
+        pCutNew->pArray[ k++ ] = pCut->pArray[i];
+        uHash |= Ivy_NodeCutHashValue( pCut->pArray[i] );
+    }
+    if ( IdNew0 < 0x7FFFFFFF )
+    {
+        pCutNew->pArray[ k++ ] = IdNew0;
+        uHash |= Ivy_NodeCutHashValue( IdNew0 );
+    }
+    if ( IdNew1 < 0x7FFFFFFF )
+    {
+        pCutNew->pArray[ k++ ] = IdNew1;
+        uHash |= Ivy_NodeCutHashValue( IdNew1 );
+    }
+    pCutNew->nSize = k;
+    pCutNew->uHash = uHash;
+    assert( pCutNew->nSize <= pCut->nSizeMax );
+//    for ( i = 1; i < pCutNew->nSize; i++ )
+//        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Check if the cut exists.]
 
   Description [Returns 1 if the cut exists.]
@@ -789,7 +873,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
     Ivy_Man_t * pMan = p;
     Ivy_Obj_t * pLeaf;
-    int i, k;
+    int i, k, iLeaf0, iLeaf1;
 
     assert( nLeaves <= IVY_CUT_INPUT );
 
@@ -818,6 +902,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
             pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
             if ( Ivy_ObjIsCi(pLeaf) )
                 continue;
+/*
             *pCutNew = *pCut;
             Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
             if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
@@ -825,6 +910,12 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
             if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
                 continue;
             Ivy_NodeCutHash( pCutNew );
+*/
+            iLeaf0 = Ivy_ObjFaninId0(pLeaf);
+            iLeaf1 = Ivy_ObjFaninId1(pLeaf);
+            if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
+                continue;
+            Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
             Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
             if ( pCutStore->nCuts == IVY_CUT_LIMIT )
                 break;
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index fb938c42..30671baf 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -250,6 +250,105 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
     return vLevelsR;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Recursively detects combinational loops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+{
+    if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
+        return 1;
+    assert( Ivy_ObjIsNode( pNode ) );
+    // make sure the node is not visited
+    assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
+    // check if the node is part of the combinational loop
+    if ( Ivy_ObjIsTravIdCurrent(p, pNode) )
+    {
+        fprintf( stdout, "Manager contains combinational loop!\n" );
+        fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n",  Ivy_ObjId(pNode) );
+        fprintf( stdout, " %d",  Ivy_ObjId(pNode) );
+        return 0;
+    }
+    // mark this node as a node on the current path
+    Ivy_ObjSetTravIdCurrent( p, pNode );
+    // check if the fanin is visited
+    if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) ) 
+    {
+        // traverse the fanin's cone searching for the loop
+        if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+        {
+            // return as soon as the loop is detected
+            fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) );
+            return 0;
+        }
+    }
+    // check if the fanin is visited
+    if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) 
+    {
+        // traverse the fanin's cone searching for the loop
+        if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
+        {
+            // return as soon as the loop is detected
+            fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin1(pNode)) );
+            return 0;
+        }
+    }
+    // mark this node as a visited node
+    Ivy_ObjSetTravIdPrevious( p, pNode );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects combinational loops.]
+
+  Description [This procedure is based on the idea suggested by Donald Chai. 
+  As we traverse the network and visit the nodes, we need to distinquish 
+  three types of nodes: (1) those that are visited for the first time, 
+  (2) those that have been visited in this traversal but are currently not 
+  on the traversal path, (3) those that have been visited and are currently 
+  on the travesal path. When the node of type (3) is encountered, it means 
+  that there is a combinational loop. To mark the three types of nodes, 
+  two new values of the traversal IDs are used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManIsAcyclic( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pNode;
+    int fAcyclic, i;
+    // set the traversal ID for this DFS ordering
+    Ivy_ManIncrementTravId( p );   
+    Ivy_ManIncrementTravId( p );   
+    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
+    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
+    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
+    // traverse the network to detect cycles
+    fAcyclic = 1;
+    Ivy_ManForEachCo( p, pNode, i )
+    {
+        if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
+            continue;
+        // traverse the output logic cone
+        if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
+            continue;
+        // stop as soon as the first loop is detected
+        fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) );
+        break;
+    }
+    return fAcyclic;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c
index 5911e051..2295516d 100644
--- a/src/temp/ivy/ivyFanout.c
+++ b/src/temp/ivy/ivyFanout.c
@@ -153,6 +153,7 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
         assert( *ppSpot == pFanout );
         *ppSpot = NULL;
     }
+//    printf( " %d", Ivy_ObjFanoutNum(p, pObj) );
 }
 
 /**Function*************************************************************
diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c
index f53e513d..2d0101a7 100644
--- a/src/temp/ivy/ivyIsop.c
+++ b/src/temp/ivy/ivyIsop.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ivy.h"
+#include "mem.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -33,7 +34,8 @@ struct Ivy_Sop_t_
 
 static Mem_Flex_t * s_Man = NULL;
 
-static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes );
+static unsigned   Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,7 +43,7 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Deallocates memory used for computing ISOPs from TTs.]
 
   Description []
                
@@ -50,14 +52,15 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TruthManStart()
+void Ivy_TruthManStop()
 {
-    s_Man = Mem_FlexStart();
+    Mem_FlexStop( s_Man, 0 );
+    s_Man = NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes ISOP from TT.]
 
   Description []
                
@@ -66,15 +69,37 @@ void Ivy_TruthManStart()
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TruthManStop()
+int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
 {
-    Mem_FlexStop( s_Man, 0 );
-    s_Man = NULL;
+    Ivy_Sop_t cRes, * pcRes = &cRes;
+    unsigned * pResult;
+    int i;
+    assert( nVars >= 0 && nVars < 16 );
+    // if nVars < 5, make sure it does not depend on those vars
+    for ( i = nVars; i < 5; i++ )
+        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+    // prepare memory manager
+    if ( s_Man == NULL )
+        s_Man = Mem_FlexStart();
+    else
+        Mem_FlexRestart( s_Man );
+    // compute ISOP
+    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+//    Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
+//    Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
+    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
+//printf( "%d ", pcRes->nCubes );
+    // copy the truth table
+    Vec_IntClear( vCover );
+    for ( i = 0; i < pcRes->nCubes; i++ )
+        Vec_IntPush( vCover, pcRes->pCubes[i] );
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes ISOP from TT.]
 
   Description []
                
@@ -83,13 +108,51 @@ void Ivy_TruthManStop()
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars )
+int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
 {
+    Ivy_Sop_t cRes, * pcRes = &cRes;
+    unsigned * pResult;
+    int i;
+    assert( nVars >= 0 && nVars < 16 );
+    // if nVars < 5, make sure it does not depend on those vars
+    for ( i = nVars; i < 5; i++ )
+        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+    // prepare memory manager
+    if ( s_Man == NULL )
+        s_Man = Mem_FlexStart();
+    else
+        Mem_FlexRestart( s_Man );
+    // compute ISOP
+    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+//    Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
+//    Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
+    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
+//printf( "%d ", pcRes->nCubes );
+    // copy the truth table
+    Vec_IntClear( vCover );
+    for ( i = 0; i < pcRes->nCubes; i++ )
+        Vec_IntPush( vCover, pcRes->pCubes[i] );
+
+    // try other polarity
+    Mem_FlexRestart( s_Man );
+    Extra_TruthNot( puTruth, puTruth, nVars );
+    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
+    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+    Extra_TruthNot( puTruth, puTruth, nVars );
+    if ( Vec_IntSize(vCover) < pcRes->nCubes )
+        return 0;
+
+    // copy the truth table
+    Vec_IntClear( vCover );
+    for ( i = 0; i < pcRes->nCubes; i++ )
+        Vec_IntPush( vCover, pcRes->pCubes[i] );
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes ISOP for 5 variables or less.]
+  Synopsis    [Computes ISOP 6 variables or more.]
 
   Description []
                
@@ -103,54 +166,59 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
     Ivy_Sop_t cRes0, cRes1, cRes2;
     Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
     unsigned * puRes0, * puRes1, * puRes2;
-    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1;
-    int i, k, Var, nWords;
-    assert( nVars > 5 );
+    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
+    int i, k, Var, nWords, nWordsAll;
     assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+    // allocate room for the resulting truth table
+    nWordsAll = Extra_TruthWordNum( nVars );
+    pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll );
+    // check for constants
     if ( Extra_TruthIsConst0( puOn, nVars ) )
     {
         pcRes->nCubes = 0;
         pcRes->pCubes = NULL;
-        return puOn;
+        Extra_TruthClear( pTemp, nVars );
+        return pTemp;
     }
     if ( Extra_TruthIsConst1( puOnDc, nVars ) )
     {
         pcRes->nCubes = 1;
         pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
         pcRes->pCubes[0] = 0;
-        return puOnDc;
+        Extra_TruthFill( pTemp, nVars );
+        return pTemp;
     }
+    assert( nVars > 0 );
     // find the topmost var
     for ( Var = nVars-1; Var >= 0; Var-- )
         if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || 
              Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
              break;
     assert( Var >= 0 );
+    // consider a simple case when one-word computation can be used
     if ( Var < 5 )
     {
-        unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
-        *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes );
-        return puRes;
+        unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes );
+        for ( i = 0; i < nWordsAll; i++ )
+            pTemp[i] = uRes;
+        return pTemp;
     }
-    nWords = Extra_TruthWordNum( Var+1 );
+    assert( Var >= 5 );
+    nWords = Extra_TruthWordNum( Var );
     // cofactor
-    puOn0 = puOn;
-    puOn1 = puOn + nWords;
-    puOnDc0 = puOnDc;
-    puOnDc1 = puOnDc + nWords;
-    // intermediate copies
-    pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
-    pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+    puOn0   = puOn;    puOn1   = puOn + nWords;
+    puOnDc0 = puOnDc;  puOnDc1 = puOnDc + nWords;
+    pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
     // solve for cofactors
-    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 );
-    puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 );
-    Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 );
-    puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 );
-    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 );
-    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 );
-    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 );
-    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 );
-    puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 );
+    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
+    puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 );
+    Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
+    puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 );
+    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
+    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
+    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
+    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
+    puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 );
     // create the resulting cover
     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
     pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
@@ -159,13 +227,21 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
     for ( i = 0; i < pcRes1->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
-    for ( i = 0; i < pcRes1->nCubes; i++ )
+    for ( i = 0; i < pcRes2->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes2->pCubes[i];
     assert( k == pcRes->nCubes );
     // create the resulting truth table
-    Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 );
-    Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 );
-    return pTemp0;
+    Extra_TruthOr( pTemp0, puRes0, puRes2, Var );
+    Extra_TruthOr( pTemp1, puRes1, puRes2, Var );
+    // copy the table if needed
+    nWords <<= 1;
+    for ( i = 1; i < nWordsAll/nWords; i++ )
+        for ( k = 0; k < nWords; k++ )
+            pTemp[i*nWords + k] = pTemp[k];
+    // verify in the end
+//    assert( Extra_TruthIsImply( puOn, pTemp, nVars ) );
+//    assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) );
+    return pTemp;
 }
 
 /**Function*************************************************************
@@ -184,12 +260,11 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
     unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
     Ivy_Sop_t cRes0, cRes1, cRes2;
     Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
-    unsigned uRes0, uRes1, uRes2;
-    unsigned uOn0, uOn1, uOnDc0, uOnDc1;
+    unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
     int i, k, Var;
     assert( nVars <= 5 );
-    assert( uOn & ~uOnDc == 0 );
-    if ( Extra_TruthIsConst0( uOn == 0 )
+    assert( (uOn & ~uOnDc) == 0 );
+    if ( uOn == 0 )
     {
         pcRes->nCubes = 0;
         pcRes->pCubes = NULL;
@@ -202,6 +277,7 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
         pcRes->pCubes[0] = 0;
         return 0xFFFFFFFF;
     }
+    assert( nVars > 0 );
     // find the topmost var
     for ( Var = nVars-1; Var >= 0; Var-- )
         if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || 
@@ -209,16 +285,16 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
              break;
     assert( Var >= 0 );
     // cofactor
-    uOn0 = uOn1 = uOn;
+    uOn0   = uOn1   = uOn;
     uOnDc0 = uOnDc1 = uOnDc;
-    Extra_TruthCofactor0( &uOn0, 5, Var );
-    Extra_TruthCofactor1( &uOn1, 5, Var );
-    Extra_TruthCofactor0( &uOnDc0, 5, Var );
-    Extra_TruthCofactor1( &uOnDc1, 5, Var );
+    Extra_TruthCofactor0( &uOn0, Var + 1, Var );
+    Extra_TruthCofactor1( &uOn1, Var + 1, Var );
+    Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
+    Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
     // solve for cofactors
-    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 );
-    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 );
-    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 );
+    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 );
+    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 );
+    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 );
     // create the resulting cover
     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
     pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
@@ -227,10 +303,14 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
     for ( i = 0; i < pcRes1->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
-    for ( i = 0; i < pcRes1->nCubes; i++ )
+    for ( i = 0; i < pcRes2->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes2->pCubes[i];
     assert( k == pcRes->nCubes );
-    return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2;
+    // derive the final truth table
+    uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
+//    assert( (uOn & ~uRes2) == 0 );
+//    assert( (uRes2 & ~uOnDc) == 0 );
+    return uRes2;
 }
 
 
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index d1aca8a6..c5b66ad0 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -109,9 +109,10 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
     Ivy_Obj_t * pNode;
     int i, nNodesOld;
     nNodesOld = Ivy_ManNodeNum(p);
-    Ivy_ManForEachNode( p, pNode, i )
-        if ( Ivy_ObjRefs(pNode) == 0 )
-            Ivy_ObjDelete_rec( p, pNode, 1 );
+    Ivy_ManForEachObj( p, pNode, i )
+        if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
+            if ( Ivy_ObjRefs(pNode) == 0 )
+                Ivy_ObjDelete_rec( p, pNode, 1 );
     return nNodesOld - Ivy_ManNodeNum(p);
 }
 
@@ -126,7 +127,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
+int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
 {
     Ivy_Obj_t * pNode;
     int nSteps;
@@ -135,7 +136,7 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
         pNode = Vec_PtrEntryLast(p->vBufs);
         while ( Ivy_ObjIsBuf(pNode) )
             pNode = Ivy_ObjReadFirstFanout( p, pNode );
-        Ivy_NodeFixBufferFanins( p, pNode );
+        Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
     }
 //    printf( "Number of steps = %d\n", nSteps );
     return nSteps;
@@ -200,6 +201,9 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
         pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i );
         pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init );
         Ivy_ObjDisconnect( p, pObj );
+        // recycle the old PO object
+        Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+        Ivy_ManRecycleMemory( p, pObj );
         // convert the corresponding PI to a buffer and connect it to the latch
         pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i );
         pObj->Type = IVY_BUF;
@@ -215,8 +219,21 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
     p->nObjs[IVY_PO] -= nLatches;
     p->nObjs[IVY_BUF] += nLatches;
     p->nDeleted -= 2 * nLatches;
+    // remove dangling nodes
+    Ivy_ManCleanup(p);
+/* 
+    // check for dangling nodes
+    Ivy_ManForEachObj( p, pObj, i )
+        if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsConst1(pObj) )
+        {
+            assert( Ivy_ObjRefs(pObj) > 0 );
+            assert( Ivy_ObjRefs(pObj) == Ivy_ObjFanoutNum(p, pObj) );
+        }
+*/
     // perform hashing by propagating the buffers
-    Ivy_ManPropagateBuffers( p );
+    Ivy_ManPropagateBuffers( p, 0 );
+    // fix the levels
+    Ivy_ManResetLevels( p );
     // check the resulting network
     if ( !Ivy_ManCheck(p) )
         printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index de67c560..735d79c3 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -300,7 +300,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop )
+void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel )
 {
     int nRefsOld;
     // the object to be replaced cannot be complemented
@@ -315,26 +315,32 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
         pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
     assert( !Ivy_IsComplement(pObjNew) );
-    // if the new node's arrival time is different, recursively update arrival time of the fanouts
-    if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+    if ( fUpdateLevel )
     {
-        assert( Ivy_ObjIsNode(pObjOld) );
-        pObjOld->Level = pObjNew->Level;
-        Ivy_ObjUpdateLevel_rec( p, pObjOld );
-    }
-    // if the new node's required time has changed, recursively update required time of the fanins
-    if ( p->vRequired )
-    {
-        int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
-        if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+        // if the new node's arrival time is different, recursively update arrival time of the fanouts
+        if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+        {
+            assert( Ivy_ObjIsNode(pObjOld) );
+            pObjOld->Level = pObjNew->Level;
+            Ivy_ObjUpdateLevel_rec( p, pObjOld );
+        }
+        // if the new node's required time has changed, recursively update required time of the fanins
+        if ( p->vRequired )
         {
-            Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
-            Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+            int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
+            if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+            {
+                Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
+                Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+            }
         }
     }
     // delete the old object
     if ( fDeleteOld )
         Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
+    // make sure object is pointing to itself
+    assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
+    assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
     // transfer the old object
     assert( Ivy_ObjRefs(pObjNew) == 0 );
     nRefsOld = pObjOld->nRefs;  
@@ -370,7 +376,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel )
 {
     Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
     if ( Ivy_ObjIsPo(pNode) )
@@ -394,7 +400,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode )
     else 
         assert( 0 );
     // perform the replacement
-    Ivy_ObjReplace( p, pNode, pResult, 1, 0 ); 
+    Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel ); 
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c
index 234827ff..fc48deb0 100644
--- a/src/temp/ivy/ivyRwrAlg.c
+++ b/src/temp/ivy/ivyRwrAlg.c
@@ -80,7 +80,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
         // the case of constant 0 cone
         if ( RetValue == -1 )
         {
-            Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 ); 
+            Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); 
             continue;
         }
         assert( Vec_PtrSize(vLeaves) > 2 );
@@ -94,7 +94,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
         if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
             Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
         else
-            Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++; 
+            Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; 
     }
     printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
     Vec_PtrFree( vFront );
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
index d2a1697e..537b64ff 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -27,9 +27,8 @@
 ////////////////////////////////////////////////////////////////////////
 
 static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums );
-static int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 static int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
-static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, 
+static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, 
     Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth );
 
 static int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
@@ -74,7 +73,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
     Ivy_ManForEachNode( p, pNode, i )
     {
         // fix the fanin buffer problem
-        Ivy_NodeFixBufferFanins( p, pNode );
+        Ivy_NodeFixBufferFanins( p, pNode, 1 );
         if ( Ivy_ObjIsBuf(pNode) )
             continue;
         // stop if all nodes have been tried once
@@ -120,8 +119,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
     // fix the levels
     if ( fUpdateLevel )
         Vec_IntFree( p->vRequired ), p->vRequired = NULL;
-//    else
-//        Ivy_ManResetLevels( p );
+    else
+        Ivy_ManResetLevels( p );
     // check
     if ( i = Ivy_ManCleanup(p) )
         printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
@@ -182,7 +181,11 @@ clk = clock();
             if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, pCut->pArray[i]) ) )
                 break;
         if ( i != pCut->nSize )
+        {
+            p->nCutsBad++;
             continue;
+        }
+        p->nCutsGood++;
         // get the fanin permutation
 clk2 = clock();
         uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize );  // truth table
@@ -211,7 +214,7 @@ clk2 = clock();
             Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
         // label MFFC with current ID
         Ivy_ManIncrementTravId( pMan );
-        nNodesSaved = Ivy_NodeMffcLabel( pMan, pNode );
+        nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
@@ -219,7 +222,7 @@ p->timeMffc += clock() - clk2;
 
         // evaluate the cut
 clk2 = clock();
-        pGraph = Rwt_CutEvaluate( pMan, p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+        pGraph = Rwt_CutEvaluate( pMan, p, pNode, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
 p->timeEval += clock() - clk2;
 
         // check if the cut is better than the current best one
@@ -289,75 +292,6 @@ p->timeRes += clock() - clk;
     return GainBest;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [References/references the node and returns MFFC size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_NodeRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    int Counter;
-    // label visited nodes
-    if ( fLabel )
-        Ivy_ObjSetTravIdCurrent( p, pNode );
-    // skip the CI
-    if ( Ivy_ObjIsCi(pNode) )
-        return 0;
-    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
-    // process the internal node
-    pNode0 = Ivy_ObjFanin0(pNode);
-    pNode1 = Ivy_ObjFanin1(pNode);
-    Counter = Ivy_ObjIsNode(pNode);
-    if ( fReference )
-    {
-        if ( pNode0->nRefs++ == 0 )
-            Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
-        if ( pNode1 && pNode1->nRefs++ == 0 )
-            Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
-    }
-    else
-    {
-        assert( pNode0->nRefs > 0 );
-        assert( pNode1 == NULL || pNode1->nRefs > 0 );
-        if ( --pNode0->nRefs == 0 )
-            Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
-        if ( pNode1 && --pNode1->nRefs == 0 )
-            Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the size of MFFC and labels nodes with the current TravId.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
-{
-    int nConeSize1, nConeSize2;
-    assert( !Ivy_IsComplement( pNode ) );
-    assert( Ivy_ObjIsNode( pNode ) );
-    nConeSize1 = Ivy_NodeRefDeref( p, pNode, 0, 1 ); // dereference
-    nConeSize2 = Ivy_NodeRefDeref( p, pNode, 1, 0 ); // reference
-    assert( nConeSize1 == nConeSize2 );
-    assert( nConeSize1 > 0 );
-    return nConeSize1;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Computes the truth table.]
@@ -418,7 +352,7 @@ unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
+Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
 {
     Vec_Ptr_t * vSubgraphs;
     Dec_Graph_t * pGraphBest, * pGraphCur;
@@ -596,12 +530,12 @@ void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGr
         printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
     printf( " " );
 */
-    Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0 );
+    Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 1 );
     // compare the gains
     nNodesNew = Ivy_ManNodeNum(p);
     assert( nGain <= nNodesOld - nNodesNew );
     // propagate the buffer
-    Ivy_ManPropagateBuffers( p );
+    Ivy_ManPropagateBuffers( p, 1 );
 }
 
 /**Function*************************************************************
@@ -649,7 +583,7 @@ void Ivy_GraphUpdateNetwork3( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pG
         printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
     printf( " " );
 */
-    Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0 );
+    Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0, 1 );
 //printf( "Replace = %d. ", Ivy_ManNodeNum(p) );
 
     // delete remaining dangling nodes
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 1cfa8c4b..8fd1b63b 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -13,17 +13,28 @@
   Affiliation [UC Berkeley]
 
   Date        [Ver. 1.0. Started - May 11, 2006.]
-
+ 
   Revision    [$Id: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
 #include "ivy.h"
+#include "deco.h"
+#include "rwt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost );
+static void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm );
+static unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums );
+static Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth );
+static int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax );
+static Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph );
+static void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
+static Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
+
 static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
 
 ////////////////////////////////////////////////////////////////////////
@@ -32,6 +43,295 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
 
 /**Function*************************************************************
 
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
+{
+    Rwt_Man_t * pManRwt;
+    Ivy_Obj_t * pNode;
+    int i, nNodes, nGain;
+    int clk, clkStart = clock();
+    // start the rewriting manager
+    pManRwt = Rwt_ManStart( 0 );
+    p->pData = pManRwt;
+    if ( pManRwt == NULL )
+        return 0; 
+    // create fanouts
+    if ( p->vFanouts == NULL )
+        Ivy_ManStartFanout( p );
+    // resynthesize each node once
+    nNodes = Ivy_ManObjIdMax(p);
+    Ivy_ManForEachNode( p, pNode, i )
+    {
+        assert( !Ivy_ObjIsBuf(pNode) );
+        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) );
+        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) );
+        // fix the fanin buffer problem
+//        Ivy_NodeFixBufferFanins( p, pNode );
+//        if ( Ivy_ObjIsBuf(pNode) )
+//            continue;
+        // stop if all nodes have been tried once
+        if ( i > nNodes )
+            break;
+        if ( i == 8648 )
+        {
+            int x = 0;
+        }
+        // for each cut, try to resynthesize it
+        nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
+        if ( nGain > 0 || nGain == 0 && fUseZeroCost )
+        {
+            Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
+            int fCompl           = Rwt_ManReadCompl(pManRwt);
+            // complement the FF if needed
+clk = clock();
+            if ( fCompl ) Dec_GraphComplement( pGraph );
+            Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
+            if ( fCompl ) Dec_GraphComplement( pGraph );
+Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+/*
+            if ( !Ivy_ManIsAcyclic(p) )
+            {
+                int x = 0;
+            }
+*/
+        }
+    }
+Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+    // print stats
+    if ( fVerbose )
+        Rwt_ManPrintStats( pManRwt );
+    // delete the managers
+    Rwt_ManStop( pManRwt );
+    p->pData = NULL;
+    // fix the levels
+    Ivy_ManResetLevels( p );
+    // check
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs rewriting for one node.]
+
+  Description [This procedure considers all the cuts computed for the node
+  and tries to rewrite each of them using the "forest" of different AIG
+  structures precomputed and stored in the RWR manager. 
+  Determines the best rewriting and computes the gain in the number of AIG
+  nodes in the final network. In the end, p->vFanins contains information 
+  about the best cut that can be used for rewriting, while p->pGraph gives 
+  the decomposition dag (represented using decomposition graph data structure).
+  Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost )
+{
+    int fVeryVerbose = 0;
+    Dec_Graph_t * pGraph;
+    Ivy_Store_t * pStore;
+    Ivy_Cut_t * pCut;
+    Ivy_Obj_t * pFanin;
+    unsigned uPhase, uTruthBest, uTruth;
+    char * pPerm;
+    int nNodesSaved, nNodesSaveCur;
+    int i, c, GainCur, GainBest = -1;
+    int clk, clk2;
+
+    p->nNodesConsidered++;
+    // get the node's cuts
+clk = clock();
+    pStore = Ivy_CutComputeForNode( pMan, pNode, 5 );
+p->timeCut += clock() - clk;
+
+    // go through the cuts
+clk = clock();
+    for ( c = 1; c < pStore->nCuts; c++ )
+    {
+        pCut = pStore->pCuts + c;
+        // consider only 4-input cuts
+        if ( pCut->nSize != 4 )
+            continue;
+        // skip the cuts with buffers
+        for ( i = 0; i < (int)pCut->nSize; i++ )
+            if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) )
+                break;
+        if ( i != pCut->nSize )
+        {
+            p->nCutsBad++;
+            continue;
+        }
+        p->nCutsGood++;
+        // get the fanin permutation
+clk2 = clock();
+        uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize );  // truth table
+p->timeTruth += clock() - clk2;
+        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+        uPhase = p->pPhases[uTruth];
+        // collect fanins with the corresponding permutation/phase
+        Vec_PtrClear( p->vFaninsCur );
+        Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
+        for ( i = 0; i < (int)pCut->nSize; i++ )
+        {
+            pFanin = Ivy_ManObj( pMan, Ivy_LeafId( pCut->pArray[pPerm[i]] ) );
+            assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) || Ivy_ObjIsConst1(pFanin) );
+            pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
+            Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
+        }
+clk2 = clock();
+        // mark the fanin boundary 
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
+        // label MFFC with current ID
+        Ivy_ManIncrementTravId( pMan );
+        nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
+        // unmark the fanin boundary
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+p->timeMffc += clock() - clk2;
+/*
+if ( pNode->Id == 8648 )
+{
+    int i;
+    printf( "Trying cut : {" );
+    for ( i = 0; i < pCut->nSize; i++ )
+        printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+//    printf( " }\n" );
+    printf( " }   " );
+    Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
+}
+*/
+
+        // evaluate the cut
+clk2 = clock();
+        pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
+p->timeEval += clock() - clk2;
+
+
+        // check if the cut is better than the current best one
+        if ( pGraph != NULL && GainBest < GainCur )
+        {
+            // save this form
+            nNodesSaveCur = nNodesSaved;
+            GainBest   = GainCur;
+            p->pGraph  = pGraph;
+            p->pCut    = pCut;
+            p->pPerm   = pPerm;
+            p->fCompl  = ((uPhase & (1<<4)) > 0);
+            uTruthBest = uTruth;
+            // collect fanins in the
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+                Vec_PtrPush( p->vFanins, pFanin );
+        }
+    }
+p->timeRes += clock() - clk;
+
+    if ( GainBest == -1 )
+        return -1;
+
+    // copy the leaves
+    Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
+
+    p->nScores[p->pMap[uTruthBest]]++;
+    p->nNodesGained += GainBest;
+    if ( fUseZeroCost || GainBest > 0 )
+        p->nNodesRewritten++;
+
+/*
+    if ( GainBest > 0 )
+    {
+        Ivy_Cut_t * pCut = p->pCut;
+        printf( "Useful cut : {" );
+        for ( i = 0; i < pCut->nSize; i++ )
+            printf( "   %5d[%2d](%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]), 
+                Ivy_ObjRefs( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) );
+        printf( " }\n" );
+    }
+*/
+
+    // report the progress
+    if ( fVeryVerbose && GainBest > 0 )
+    {
+        printf( "Node %6d :   ", Ivy_ObjId(pNode) );
+        printf( "Fanins = %d. ", p->vFanins->nSize );
+        printf( "Save = %d.  ", nNodesSaveCur );
+        printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
+        printf( "GAIN = %d.  ", GainBest );
+        printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+        printf( "Class = %d.  ", p->pMap[uTruthBest] );
+        printf( "\n" );
+    }
+    return GainBest;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth )
+{
+    Vec_Ptr_t * vSubgraphs;
+    Dec_Graph_t * pGraphBest, * pGraphCur;
+    Rwt_Node_t * pNode;
+    int nNodesAdded, GainBest, i;
+    // find the matching class of subgraphs
+    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+    p->nSubgraphs += vSubgraphs->nSize;
+    // determine the best subgraph
+    GainBest = -1;
+    Vec_PtrForEachEntry( vSubgraphs, pNode, i )
+    {
+        // get the current graph
+        pGraphCur = (Dec_Graph_t *)pNode->pNext;
+
+//        if ( pRoot->Id == 8648 )
+//        Dec_GraphPrint( stdout, pGraphCur, NULL, NULL );
+        // copy the leaves
+//        Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+//            Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
+        Ivy_GraphPrepare( pGraphCur, pCut, vFaninsCur, pPerm );
+
+        // detect how many unlabeled nodes will be reused
+        nNodesAdded = Ivy_GraphToNetworkSeqCountSeq( pMan, pRoot, pGraphCur, nNodesSaved );
+        if ( nNodesAdded == -1 )
+            continue;
+        assert( nNodesSaved >= nNodesAdded );
+        // count the gain at this node
+        if ( GainBest < nNodesSaved - nNodesAdded )
+        {
+            GainBest   = nNodesSaved - nNodesAdded;
+            pGraphBest = pGraphCur;
+        }
+    }
+    if ( GainBest == -1 )
+        return NULL;
+    *pGainBest = GainBest;
+    return pGraphBest;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -41,8 +341,250 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
   SeeAlso     []
 
 ***********************************************************************/
+void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm )
+{
+    Dec_Node_t * pNode, * pNode0, * pNode1;
+    int i;
+    assert( Dec_GraphLeaveNum(pGraph) == pCut->nSize );
+    assert( Vec_PtrSize(vFanins) == pCut->nSize );
+    // label the leaves with latch numbers
+    Dec_GraphForEachLeaf( pGraph, pNode, i )
+    {
+        pNode->pFunc = Vec_PtrEntry( vFanins, i );
+        pNode->nLat2 = Ivy_LeafLat( pCut->pArray[pPerm[i]] );
+    }
+    // propagate latches through the nodes
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        // get the children of this node
+        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+        // distribute the latches
+        pNode->nLat2 = IVY_MIN( pNode0->nLat2, pNode1->nLat2 );
+        pNode->nLat0 = pNode0->nLat2 - pNode->nLat2;
+        pNode->nLat1 = pNode1->nLat2 - pNode->nLat2;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of new nodes added when using this graph.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
+  of the leaves of the graph before calling this procedure. 
+  Returns -1 if the number of nodes and levels exceeded the given limit or 
+  the number of levels exceeded the maximum allowed level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax )
+{
+    Dec_Node_t * pNode, * pNode0, * pNode1;
+    Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
+    int i, k, Counter, fCompl;
+    // check for constant function or a literal
+    if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+        return 0;
+    // compute the AIG size after adding the internal nodes
+    Counter = 0;
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        // get the children of this node
+        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+        // get the AIG nodes corresponding to the children 
+        pAnd0 = pNode0->pFunc; 
+        pAnd1 = pNode1->pFunc; 
+        // skip the latches
+        for ( k = 0; pAnd0 && k < (int)pNode->nLat0; k++ )
+        {
+            fCompl = Ivy_IsComplement(pAnd0);
+            pAnd0 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd0), NULL, IVY_LATCH, IVY_INIT_DC) );
+            if ( pAnd0 )
+                pAnd0 = Ivy_NotCond( pAnd0, fCompl );
+        }
+        for ( k = 0; pAnd1 && k < (int)pNode->nLat1; k++ )
+        {
+            fCompl = Ivy_IsComplement(pAnd1);
+            pAnd1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd1), NULL, IVY_LATCH, IVY_INIT_DC) );
+            if ( pAnd1 )
+                pAnd1 = Ivy_NotCond( pAnd1, fCompl );
+        }
+        // get the new node
+        if ( pAnd0 && pAnd1 )
+        {
+            // if they are both present, find the resulting node
+            pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
+            pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
+            assert( !Ivy_ObjIsLatch(Ivy_Regular(pAnd0)) || !Ivy_ObjIsLatch(Ivy_Regular(pAnd1)) );
+            if ( Ivy_Regular(pAnd0) == Ivy_Regular(pAnd1) || Ivy_ObjIsConst1(Ivy_Regular(pAnd0)) || Ivy_ObjIsConst1(Ivy_Regular(pAnd1)) )
+                pAnd = Ivy_And( p, pAnd0, pAnd1 );
+            else
+                pAnd = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
+            // return -1 if the node is the same as the original root
+            if ( Ivy_Regular(pAnd) == pRoot )
+                return -1;
+        }
+        else
+            pAnd = NULL;
+        // count the number of added nodes
+        if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) )
+        {
+            if ( ++Counter > NodeMax )
+                return -1;
+        }
+        pNode->pFunc = pAnd;
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+  of the leaves of the graph before calling this procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph )
+{
+    Ivy_Obj_t * pAnd0, * pAnd1;
+    Dec_Node_t * pNode;
+    int i, k;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+    {
+        // get the variable node
+        pNode = Dec_GraphVar(pGraph);
+        // add the remaining latches
+        for ( k = 0; k < (int)pNode->nLat2; k++ )
+            pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
+        return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+    }
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        // add the latches
+        for ( k = 0; k < (int)pNode->nLat0; k++ )
+            pAnd0 = Ivy_Latch( p, pAnd0, IVY_INIT_DC );
+        for ( k = 0; k < (int)pNode->nLat1; k++ )
+            pAnd1 = Ivy_Latch( p, pAnd1, IVY_INIT_DC );
+        // create the node
+        pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 );
+    }
+    // add the remaining latches
+    for ( k = 0; k < (int)pNode->nLat2; k++ )
+        pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
+    // complement the result if necessary
+    return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
+{
+    Ivy_Obj_t * pRootNew;
+    int nNodesNew, nNodesOld;
+    nNodesOld = Ivy_ManNodeNum(p);
+    // create the new structure of nodes
+    pRootNew = Ivy_GraphToNetworkSeq( p, pGraph );
+    Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 0 );
+    // compare the gains
+    nNodesNew = Ivy_ManNodeNum(p);
+    assert( nGain <= nNodesOld - nNodesNew );
+    // propagate the buffer
+    Ivy_ManPropagateBuffers( p, 0 );
+}
+
+
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_CutGetTruth_rec( Ivy_Man_t * p, int Leaf, int * pNums, int nNums )
+{
+    static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned uTruth0, uTruth1;
+    Ivy_Obj_t * pObj;
+    int i;
+    for ( i = 0; i < nNums; i++ )
+        if ( Leaf == pNums[i] )
+            return uMasks[i];
+    pObj = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
+    if ( Ivy_ObjIsLatch(pObj) )
+    {
+        assert( !Ivy_ObjFaninC0(pObj) );
+        Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) + 1 );
+        return Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+    }
+    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+    Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) );
+    uTruth0 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+    if ( Ivy_ObjFaninC0(pObj) )
+        uTruth0 = ~uTruth0;
+    if ( Ivy_ObjIsBuf(pObj) )
+        return uTruth0;
+    Leaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pObj), Ivy_LeafLat(Leaf) );
+    uTruth1 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
+    if ( Ivy_ObjFaninC1(pObj) )
+        uTruth1 = ~uTruth1;
+    return uTruth0 & uTruth1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table.]
 
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+    assert( Ivy_ObjIsNode(pObj) );
+    assert( nNums < 6 );
+    return Ivy_CutGetTruth_rec( p, Ivy_LeafCreate(pObj->Id, 0), pNums, nNums );
+}
 
 
 
@@ -50,6 +592,28 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the cut can be constructed; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_CutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 )
+{
+    int i;
+    if ( pCut->nSize < pCut->nSizeMax )
+        return 1;
+    for ( i = 0; i < pCut->nSize; i++ )
+        if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives new cut.]
 
   Description []
@@ -59,7 +623,7 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+static inline int Ivy_CutDeriveNew2( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
 {
     unsigned uHash = 0;
     int i, k;
@@ -126,6 +690,130 @@ static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int I
 
 /**Function*************************************************************
 
+  Synopsis    [Derives new cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+    unsigned uHash = 0;
+    int i, k; 
+    assert( pCut->nSize > 0 );
+    assert( IdNew0 < IdNew1 );
+    for ( i = k = 0; i < pCut->nSize; i++ )
+    {
+        if ( pCut->pArray[i] == IdOld )
+            continue;
+        if ( IdNew0 <= pCut->pArray[i] )
+        {
+            if ( IdNew0 < pCut->pArray[i] )
+            {
+                pCutNew->pArray[ k++ ] = IdNew0;
+                uHash |= Ivy_CutHashValue( IdNew0 );
+            }
+            IdNew0 = 0x7FFFFFFF;
+        }
+        if ( IdNew1 <= pCut->pArray[i] )
+        {
+            if ( IdNew1 < pCut->pArray[i] )
+            {
+                pCutNew->pArray[ k++ ] = IdNew1;
+                uHash |= Ivy_CutHashValue( IdNew1 );
+            }
+            IdNew1 = 0x7FFFFFFF;
+        }
+        pCutNew->pArray[ k++ ] = pCut->pArray[i];
+        uHash |= Ivy_CutHashValue( pCut->pArray[i] );
+    }
+    if ( IdNew0 < 0x7FFFFFFF )
+    {
+        pCutNew->pArray[ k++ ] = IdNew0;
+        uHash |= Ivy_CutHashValue( IdNew0 );
+    }
+    if ( IdNew1 < 0x7FFFFFFF )
+    {
+        pCutNew->pArray[ k++ ] = IdNew1;
+        uHash |= Ivy_CutHashValue( IdNew1 );
+    }
+    pCutNew->nSize = k;
+    pCutNew->uHash = uHash;
+    assert( pCutNew->nSize <= pCut->nSizeMax );
+//    for ( i = 1; i < pCutNew->nSize; i++ )
+//        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the hash value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut )
+{
+    int i;
+    pCut->uHash = 0;
+    for ( i = 0; i < pCut->nSize; i++ )
+        pCut->uHash |= (1 << (pCut->pArray[i] % 31));
+    return pCut->uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_CutDeriveNew3( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
+{
+    int i, k; 
+    assert( pCut->nSize > 0 );
+    assert( IdNew0 < IdNew1 );
+    for ( i = k = 0; i < pCut->nSize; i++ )
+    {
+        if ( pCut->pArray[i] == IdOld )
+            continue;
+        if ( IdNew0 <= pCut->pArray[i] )
+        {
+            if ( IdNew0 < pCut->pArray[i] )
+                pCutNew->pArray[ k++ ] = IdNew0;
+            IdNew0 = 0x7FFFFFFF;
+        }
+        if ( IdNew1 <= pCut->pArray[i] )
+        {
+            if ( IdNew1 < pCut->pArray[i] )
+                pCutNew->pArray[ k++ ] = IdNew1;
+            IdNew1 = 0x7FFFFFFF;
+        }
+        pCutNew->pArray[ k++ ] = pCut->pArray[i];
+    }
+    if ( IdNew0 < 0x7FFFFFFF )
+        pCutNew->pArray[ k++ ] = IdNew0;
+    if ( IdNew1 < 0x7FFFFFFF )
+        pCutNew->pArray[ k++ ] = IdNew1;
+    pCutNew->nSize = k;
+    assert( pCutNew->nSize <= pCut->nSizeMax );
+    Ivy_NodeCutHash( pCutNew );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if pDom is contained in pCut.]
 
   Description []
@@ -295,9 +983,12 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
 ***********************************************************************/
 static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
 {
+    int iLeaf;
     assert( !Ivy_IsComplement(pFanin) );
     if ( !Ivy_ObjIsLatch(pFanin) )
         return Ivy_LeafCreate( pFanin->Id, 0 );
+    iLeaf = Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
+    assert( Ivy_LeafLat(iLeaf) < IVY_LEAF_MASK );
     return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
 }
 
@@ -345,13 +1036,20 @@ Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeave
         for ( k = 0; k < pCut->nSize; k++ )
         {
             pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) );
-            if ( Ivy_ObjIsCi(pLeaf) )
+            if ( Ivy_ObjIsCi(pLeaf) || Ivy_ObjIsConst1(pLeaf) )
                 continue;
             assert( Ivy_ObjIsNode(pLeaf) );
             nLats = Ivy_LeafLat(pCut->pArray[k]);
+
             // get the fanins fanins
-            iLeaf0 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
-            iLeaf1 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
+            iLeaf0 = Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
+            iLeaf1 = Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
+            assert( nLats + Ivy_LeafLat(iLeaf0) < IVY_LEAF_MASK && nLats + Ivy_LeafLat(iLeaf1) < IVY_LEAF_MASK );
+            iLeaf0 = nLats + iLeaf0;
+            iLeaf1 = nLats + iLeaf1;
+            if ( !Ivy_CutPrescreen( pCut, iLeaf0, iLeaf1 ) )
+                continue;
+            // the given cut exist
             if ( iLeaf0 > iLeaf1 )
                 Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp;
             // create the new cut
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
index f2617699..fe9c3570 100644
--- a/src/temp/ivy/ivyTable.c
+++ b/src/temp/ivy/ivyTable.c
@@ -74,8 +74,8 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj )
         return NULL;
     assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
     assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) );
-//    if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
-//        return NULL;
+    if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (Ivy_ObjChild1(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
+        return NULL;
     for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
     {
         pEntry = Ivy_ManObj( p, p->pTable[i] );
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 3b77bf41..77a55a39 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -265,7 +265,7 @@ int Ivy_ManLevels( Ivy_Man_t * p )
 ***********************************************************************/
 int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
 {
-    if ( pObj->Level || Ivy_ObjIsCi(pObj) )
+    if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
         return pObj->Level;
     if ( Ivy_ObjIsBuf(pObj) )
         return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
@@ -292,12 +292,81 @@ void Ivy_ManResetLevels( Ivy_Man_t * p )
     int i;
     Ivy_ManForEachObj( p, pObj, i )
         pObj->Level = 0;
-    Ivy_ManForEachPo( p, pObj, i )
+    Ivy_ManForEachCo( p, pObj, i )
         Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
 }
 
 /**Function*************************************************************
 
+  Synopsis    [References/references the node and returns MFFC size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
+{
+    Ivy_Obj_t * pNode0, * pNode1;
+    int Counter;
+    // label visited nodes
+    if ( fLabel )
+        Ivy_ObjSetTravIdCurrent( p, pNode );
+    // skip the CI
+    if ( Ivy_ObjIsPi(pNode) )
+        return 0;
+    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) );
+    // process the internal node
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    Counter = Ivy_ObjIsNode(pNode);
+    if ( fReference )
+    {
+        if ( pNode0->nRefs++ == 0 )
+            Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
+        if ( pNode1 && pNode1->nRefs++ == 0 )
+            Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
+    }
+    else
+    {
+        assert( pNode0->nRefs > 0 );
+        assert( pNode1 == NULL || pNode1->nRefs > 0 );
+        if ( --pNode0->nRefs == 0 )
+            Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
+        if ( pNode1 && --pNode1->nRefs == 0 )
+            Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Labels MFFC with the current label.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
+{
+    int nConeSize1, nConeSize2;
+    assert( !Ivy_IsComplement( pNode ) );
+    assert( Ivy_ObjIsNode( pNode ) );
+    nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference
+    nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    return nConeSize1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Recursively updates fanout levels.]
 
   Description []
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index a8f6a824..e7ba865a 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -5,6 +5,7 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyDfs.c \
     src/temp/ivy/ivyDsd.c \
     src/temp/ivy/ivyFanout.c \
+    src/temp/ivy/ivyIsop.c \
     src/temp/ivy/ivyMan.c \
     src/temp/ivy/ivyMem.c \
     src/temp/ivy/ivyMulti.c \
diff --git a/src/temp/mem/mem.c b/src/temp/mem/mem.c
index 26d6485d..15199755 100644
--- a/src/temp/mem/mem.c
+++ b/src/temp/mem/mem.c
@@ -302,7 +302,7 @@ Mem_Flex_t * Mem_FlexStart()
     p->pCurrent      = NULL;
     p->pEnd          = NULL;
 
-    p->nChunkSize    = (1 << 12);
+    p->nChunkSize    = (1 << 14);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
     p->pChunks       = ALLOC( char *, p->nChunksAlloc );
@@ -390,6 +390,34 @@ char * Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes )
 
   Synopsis    []
 
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mem_FlexRestart( Mem_Flex_t * p )
+{
+    int i;
+    if ( p->nChunks == 0 )
+        return;
+    // deallocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    p->nChunks  = 1;
+    p->nMemoryAlloc = p->nChunkSize;
+    // transform these entries into a linked list
+    p->pCurrent = p->pChunks[0];
+    p->pEnd     = p->pCurrent + p->nChunkSize;
+    p->nEntriesUsed = 0;
+    p->nMemoryUsed = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
   Description []
                
   SideEffects []
@@ -399,7 +427,7 @@ char * Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes )
 ***********************************************************************/
 int Mem_FlexReadMemUsage( Mem_Flex_t * p )
 {
-    return p->nMemoryAlloc;
+    return p->nMemoryUsed;
 }
 
 
diff --git a/src/temp/mem/mem.h b/src/temp/mem/mem.h
index 21296d99..611c968d 100644
--- a/src/temp/mem/mem.h
+++ b/src/temp/mem/mem.h
@@ -49,6 +49,7 @@ extern int           Mem_FixedReadMemUsage( Mem_Fixed_t * p );
 extern Mem_Flex_t *  Mem_FlexStart();
 extern void          Mem_FlexStop( Mem_Flex_t * p, int fVerbose );
 extern char *        Mem_FlexEntryFetch( Mem_Flex_t * p, int nBytes );
+extern void          Mem_FlexRestart( Mem_Flex_t * p );
 extern int           Mem_FlexReadMemUsage( Mem_Flex_t * p );
 // hierarchical memory manager
 extern Mem_Step_t *  Mem_StepStart( int nSteps );
diff --git a/src/temp/player/module.make b/src/temp/player/module.make
index 5185f56e..37e236bb 100644
--- a/src/temp/player/module.make
+++ b/src/temp/player/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/temp/player/playerToAbc.c \
+    src/temp/player/playerFast.c \
     src/temp/player/playerCore.c \
     src/temp/player/playerMan.c \
     src/temp/player/playerUtil.c
diff --git a/src/temp/player/player.h b/src/temp/player/player.h
index 7f9598d8..b0bb0ec4 100644
--- a/src/temp/player/player.h
+++ b/src/temp/player/player.h
@@ -86,9 +86,13 @@ static inline Pla_Obj_t *   Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj )  {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== playerToAbc.c ==============================================================*/
-extern void *        Abc_NtkPlayer( void * pNtk, int nLutMax, int nFaninMax, int fVerbose );
+extern void *        Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
 /*=== playerCore.c =============================================================*/
 extern Pla_Man_t *   Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
+/*=== playerFast.c =============================================================*/
+extern void          Pla_ManFastLutMap( Ivy_Man_t * pAig, int nLimit );
+extern void          Pla_ManFastLutMapStop( Ivy_Man_t * pAig );
+extern void          Pla_ManFastLutMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
 /*=== playerMan.c ==============================================================*/
 extern Pla_Man_t *   Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax );
 extern void          Pla_ManFree( Pla_Man_t * p );
diff --git a/src/temp/player/playerAbc.c b/src/temp/player/playerAbc.c
index 8b045d94..8e3823d5 100644
--- a/src/temp/player/playerAbc.c
+++ b/src/temp/player/playerAbc.c
@@ -45,7 +45,7 @@ static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p );
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose )
+void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
 {
     int fUseRewriting = 1;
     Ivy_Man_t * pMan, * pManExt;
diff --git a/src/temp/player/playerFast.c b/src/temp/player/playerFast.c
new file mode 100644
index 00000000..c8edc1db
--- /dev/null
+++ b/src/temp/player/playerFast.c
@@ -0,0 +1,367 @@
+/**CFile****************************************************************
+
+  FileName    [playerFast.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [PLA decomposition package.]
+
+  Synopsis    [Fast 8-LUT mapper.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: playerFast.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "player.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_SuppMan_t_ Ivy_SuppMan_t;
+struct Ivy_SuppMan_t_ 
+{
+    int    nLimit;    // the limit on the number of inputs
+    int    nObjs;     // the number of entries
+    int    nSize;     // size of each entry in bytes
+    char * pMem;      // memory allocated
+};
+
+typedef struct Ivy_Supp_t_ Ivy_Supp_t;
+struct Ivy_Supp_t_ 
+{
+    char  nSize;      // the number of support nodes
+    char  fMark;      // the node was processed for area counting
+    short Delay;      // the delay of the node
+    int   pArray[0];  // the support nodes
+};
+
+static inline Ivy_Supp_t * Ivy_ObjSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj )      
+{ 
+    return (Ivy_Supp_t *)(((Ivy_SuppMan_t*)pAig->pData)->pMem + pObj->Id * ((Ivy_SuppMan_t*)pAig->pData)->nSize); 
+}
+static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ) 
+{ 
+    Ivy_Supp_t * pSupp;
+    pSupp = Ivy_ObjSupp( pAig, pObj );
+    pSupp->fMark = 0;
+    pSupp->Delay = 0;
+    pSupp->nSize = 1;
+    pSupp->pArray[0] = pObj->Id;
+    return pSupp;
+}
+
+static int  Pla_ManFastLutMapDelay( Ivy_Man_t * pAig );
+static int  Pla_ManFastLutMapArea( Ivy_Man_t * pAig );
+static void Pla_ManFastLutMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
+static int  Pla_ManFastLutMapMerge( Ivy_Supp_t * pSupp0, Ivy_Supp_t * pSupp1, Ivy_Supp_t * pSupp, int nLimit );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast K-LUT mapping of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pla_ManFastLutMap( Ivy_Man_t * pAig, int nLimit )
+{
+    Ivy_SuppMan_t * pMan;
+    Ivy_Obj_t * pObj;
+    int i, Delay, Area;
+    int clk = clock(), clk2;
+    // start the memory for supports
+    pMan = ALLOC( Ivy_SuppMan_t, 1 );
+    memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
+    pMan->nLimit = nLimit;
+    pMan->nObjs  = Ivy_ManObjIdMax(pAig) + 1;
+    pMan->nSize  = sizeof(Ivy_Supp_t) + nLimit * sizeof(int);
+    pMan->pMem   = (char *)malloc( pMan->nObjs * pMan->nSize );
+    pAig->pData  = pMan;
+clk2 = clock();
+    // set the PI mapping
+    Ivy_ObjSuppStart( pAig, Ivy_ManConst1(pAig) );
+    Ivy_ManForEachPi( pAig, pObj, i )
+        Ivy_ObjSuppStart( pAig, pObj );
+    // iterate through all nodes in the topological order
+    Ivy_ManForEachNode( pAig, pObj, i )
+        Pla_ManFastLutMapNode( pAig, pObj, nLimit );
+    // find the best arrival time and area
+    Delay = Pla_ManFastLutMapDelay( pAig );
+    Area  = Pla_ManFastLutMapArea( pAig );
+clk2 = clock() - clk2;
+    // print the report
+    printf( "LUT levels = %3d. LUT number = %6d. ", Delay, Area );
+    PRT( "Mapping time", clk2 );
+//    PRT( "Total", clock() - clk );
+//    Pla_ManFastLutMapStop( pAig );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans memory used for decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pla_ManFastLutMapStop( Ivy_Man_t * pAig )
+{
+    free( ((Ivy_SuppMan_t*)pAig->pData)->pMem );
+    free( pAig->pData );
+    pAig->pData = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay after LUT mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pla_ManFastLutMapDelay( Ivy_Man_t * pAig )
+{
+    Ivy_Supp_t * pSupp;
+    Ivy_Obj_t * pObj;
+    int i, DelayMax = 0;
+    Ivy_ManForEachPo( pAig, pObj, i )
+    {
+        pObj = Ivy_ObjFanin0(pObj);
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        pSupp = Ivy_ObjSupp( pAig, pObj );
+        if ( DelayMax < pSupp->Delay )
+            DelayMax = pSupp->Delay;
+    }
+    return DelayMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pla_ManFastLutMapArea_rec( Ivy_Man_t * pAig, Ivy_Obj_t * pObj )
+{
+    Ivy_Supp_t * pSupp;
+    int i, Counter;
+    pSupp = Ivy_ObjSupp( pAig, pObj );
+    // skip visited nodes and PIs
+    if ( pSupp->fMark || pSupp->nSize == 1 )
+        return 0;
+    pSupp->fMark = 1;
+    // compute the area of this node
+    Counter = 0;
+    for ( i = 0; i < pSupp->nSize; i++ )
+        Counter += Pla_ManFastLutMapArea_rec( pAig, Ivy_ManObj(pAig, pSupp->pArray[i]) );
+    return 1 + Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pla_ManFastLutMapArea( Ivy_Man_t * pAig )
+{
+    Ivy_Obj_t * pObj;
+    int i, Counter = 0;
+    Ivy_ManForEachPo( pAig, pObj, i )
+        Counter += Pla_ManFastLutMapArea_rec( pAig, Ivy_ObjFanin0(pObj) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pla_ManFastLutMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
+{
+    Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+    int RetValue;
+    assert( Ivy_ObjIsNode(pObj) );
+    // get the supports
+    pSupp0 = Ivy_ObjSupp( pAig, Ivy_ObjFanin0(pObj) );
+    pSupp1 = Ivy_ObjSupp( pAig, Ivy_ObjFanin1(pObj) );
+    pSupp  = Ivy_ObjSupp( pAig, pObj );
+    pSupp->fMark = 0;
+    // get the delays
+    if ( pSupp0->Delay == pSupp1->Delay )
+        pSupp->Delay = (pSupp0->Delay == 0) ? pSupp0->Delay + 1: pSupp0->Delay;
+    else if ( pSupp0->Delay > pSupp1->Delay )
+    {
+        pSupp->Delay = pSupp0->Delay;
+        pSupp1 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+        pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj);
+    }
+    else // if ( pSupp0->Delay < pSupp1->Delay )
+    {
+        pSupp->Delay = pSupp1->Delay;
+        pSupp0 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+        pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj);
+    }
+    // merge the cuts
+    if ( pSupp0->nSize < pSupp1->nSize )
+        RetValue = Pla_ManFastLutMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+    else
+        RetValue = Pla_ManFastLutMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+    if ( !RetValue )
+    {
+        pSupp->Delay++;
+        pSupp->nSize = 2;
+        pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+        pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+    }
+    assert( pSupp->Delay > 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two supports]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pla_ManFastLutMapMerge( Ivy_Supp_t * pSupp0, Ivy_Supp_t * pSupp1, Ivy_Supp_t * pSupp, int nLimit )
+{ 
+    int i, k, c;
+    assert( pSupp0->nSize >= pSupp1->nSize );
+    // the case of the largest cut sizes
+    if ( pSupp0->nSize == nLimit && pSupp1->nSize == nLimit )
+    {
+        for ( i = 0; i < pSupp0->nSize; i++ )
+            if ( pSupp0->pArray[i] != pSupp1->pArray[i] )
+                return 0;
+        for ( i = 0; i < pSupp0->nSize; i++ )
+            pSupp->pArray[i] = pSupp0->pArray[i];
+        pSupp->nSize = pSupp0->nSize;
+        return 1;
+    }
+    // the case when one of the cuts is the largest
+    if ( pSupp0->nSize == nLimit )
+    {
+        for ( i = 0; i < pSupp1->nSize; i++ )
+        {
+            for ( k = pSupp0->nSize - 1; k >= 0; k-- )
+                if ( pSupp0->pArray[k] == pSupp1->pArray[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return 0;
+        }
+        for ( i = 0; i < pSupp0->nSize; i++ )
+            pSupp->pArray[i] = pSupp0->pArray[i];
+        pSupp->nSize = pSupp0->nSize;
+        return 1;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < nLimit; c++ )
+    {
+        if ( k == pSupp1->nSize )
+        {
+            if ( i == pSupp0->nSize )
+            {
+                pSupp->nSize = c;
+                return 1;
+            }
+            pSupp->pArray[c] = pSupp0->pArray[i++];
+            continue;
+        }
+        if ( i == pSupp0->nSize )
+        {
+            if ( k == pSupp1->nSize )
+            {
+                pSupp->nSize = c;
+                return 1;
+            }
+            pSupp->pArray[c] = pSupp1->pArray[k++];
+            continue;
+        }
+        if ( pSupp0->pArray[i] < pSupp1->pArray[k] )
+        {
+            pSupp->pArray[c] = pSupp0->pArray[i++];
+            continue;
+        }
+        if ( pSupp0->pArray[i] > pSupp1->pArray[k] )
+        {
+            pSupp->pArray[c] = pSupp1->pArray[k++];
+            continue;
+        }
+        pSupp->pArray[c] = pSupp0->pArray[i++]; 
+        k++;
+    }
+    if ( i < pSupp0->nSize || k < pSupp1->nSize )
+        return 0;
+    pSupp->nSize = c;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates integer vector with the support of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pla_ManFastLutMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves )
+{
+    Ivy_Supp_t * pSupp;
+    pSupp = Ivy_ObjSupp( pAig, pObj );
+    vLeaves->nCap   = 8;
+    vLeaves->nSize  = pSupp->nSize;
+    vLeaves->pArray = pSupp->pArray;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index 09bf5088..fc5e01ea 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -26,9 +26,11 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p );
-static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p );
+static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode );
 static Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp );
+static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp );
 static Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp );
+static int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose );
 
 static inline void        Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) {  assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc );  }
 static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )                      {  return Vec_PtrEntry( p->pCopy, IvyId );         }
@@ -39,7 +41,7 @@ static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )
 
 /**Function*************************************************************
 
-  Synopsis    [Gives the current ABC network to PLAyer for processing.]
+  Synopsis    [Applies PLA/LUT mapping to the ABC network.]
 
   Description []
                
@@ -48,12 +50,12 @@ static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose )
+void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
 {
-    int fUseRewriting = 1;
+    int fUseRewriting = 0;
     Pla_Man_t * p;
     Ivy_Man_t * pMan, * pManExt;
-    Abc_Ntk_t * pNtkAig;
+    Abc_Ntk_t * pNtkNew;
     if ( !Abc_NtkIsStrash(pNtk) )
         return NULL;
     // convert to the new AIG manager
@@ -75,20 +77,33 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose )
         if ( fVerbose )
             Ivy_ManPrintStats( pMan );
     }
-    // perform decomposition/mapping into PLAs/LUTs
-    p = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose );
-    // convert from the extended AIG manager into an SOP network
-    pNtkAig = Ivy_ManToAbc( pNtk, pMan, p );
-    Pla_ManFree( p );
+    // perform decomposition
+    if ( fFastMode )
+    {
+        // perform mapping into LUTs
+        Pla_ManFastLutMap( pMan, nLutMax );
+        // convert from the extended AIG manager into an SOP network
+        pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode );
+        Pla_ManFastLutMapStop( pMan );
+    }
+    else
+    {
+        // perform decomposition/mapping into PLAs/LUTs
+        p = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose );
+        // convert from the extended AIG manager into an SOP network
+        pNtkNew = Ivy_ManToAbc( pNtk, pMan, p, fFastMode );
+        Pla_ManFree( p );
+    }
     Ivy_ManStop( pMan );
     // chech the resulting network
-    if ( !Abc_NtkCheck( pNtkAig ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkPlayer: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkAig );
+        Abc_NtkDelete( pNtkNew );
         return NULL;
     }
-    return pNtkAig;
+    Abc_NtkPlayerCost( pNtkNew, RankCost, fVerbose );
+    return pNtkNew;
 }
 
 /**Function*************************************************************
@@ -134,7 +149,7 @@ Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p )
+Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode )
 {
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObjAbc, * pObj;
@@ -155,7 +170,11 @@ Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p )
     Ivy_ManForEachPo( pMan, pObjIvy, i )
     {
         // get the new ABC node corresponding to the old fanin of the PO in IVY
-        pObjAbc = Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp );
+        if ( fFastMode )
+            pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp );
+        else
+            pObjAbc = Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp );
+        // consider the case of complemented fanin of the PO
         if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
         {
             if ( Abc_ObjIsCi(pObjAbc) )
@@ -236,17 +255,20 @@ Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t *
             Abc_ObjAddFanin( pObjAbc, Abc_ObjGetIvy2Abc(pMan, Entry) );
         // check if the truth table is constant 0
         puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp );
-        for ( i = 0; i < 8; i++ )
-            if ( puTruth[i] )
-                break;
-        // create constant 0 node
-        if ( i == 8 )
+        // if the function is constant 0, create constant 0 node
+        if ( Extra_TruthIsConst0(puTruth, 8) )
         {
             pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
             pObjAbc = Abc_NodeCreateConst0( pNtkNew );  
         }
         else
-            pObjAbc->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, Vec_IntSize(vSupp), puTruth );
+        {
+            int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+            pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
+            if ( fCompl ) Abc_SopComplement(pObjAbc->pData); 
+//            printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) );
+//            pObjAbc->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, Vec_IntSize(vSupp), puTruth );
+        }
     }
     else
     {
@@ -309,6 +331,149 @@ Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t *
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively construct the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp )
+{
+    Vec_Int_t Supp, * vSupp = &Supp;
+    Abc_Obj_t * pObjAbc, * pFaninAbc;
+    int i, Entry;
+    unsigned * puTruth;
+    // skip the node if it is a constant or already processed
+    pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
+    if ( pObjAbc )
+        return pObjAbc;
+    assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
+    // get the support of K-LUT
+    Pla_ManFastLutMapReadSupp( pMan, pObjIvy, vSupp );
+    // create new ABC node and its fanins
+    pObjAbc = Abc_NtkCreateNode( pNtkNew );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes, vTemp );
+        Abc_ObjAddFanin( pObjAbc, pFaninAbc );
+    }
+    // check if the truth table is constant 0
+    puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp );
+    // if the function is constant 0, create constant 0 node
+    if ( Extra_TruthIsConst0(puTruth, 8) )
+    {
+        pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
+        pObjAbc = Abc_NodeCreateConst0( pNtkNew );  
+    }
+    else
+    {
+        int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+        pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
+        if ( fCompl ) Abc_SopComplement(pObjAbc->pData); 
+    }
+    Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc ); 
+    return pObjAbc;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cost of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_NodePlayerCost( int nFanins )
+{
+    if ( nFanins <= 4 )
+        return 1;
+    if ( nFanins <= 6 )
+        return 2;
+    if ( nFanins <= 8 )
+        return 4;
+    if ( nFanins <= 16 )
+        return 8;
+    if ( nFanins <= 32 )
+        return 16;
+    if ( nFanins <= 64 )
+        return 32;
+    if ( nFanins <= 128 )
+        return 64;
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of ranks needed for one level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost )
+{
+    return (nCost / RankCost) + ((nCost % RankCost) > 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cost function for the network (number of ranks).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int nFanins, nLevels, * pLevelCosts, CostTotal, nRanksTotal, i; 
+    // compute the costs for each level
+    nLevels = Abc_NtkGetLevelNum( pNtk );
+    pLevelCosts = ALLOC( int, nLevels + 1 );
+    memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+            continue;
+        pLevelCosts[ pObj->Level ] += Abc_NodePlayerCost( nFanins );
+    }
+    // compute the total cost
+    CostTotal = nRanksTotal = 0;
+    for ( i = 1; i <= nLevels; i++ )
+    {
+        CostTotal   += pLevelCosts[i];
+        nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
+    }
+    // print out statistics
+    if ( fVerbose )
+    {
+        for ( i = 1; i <= nLevels; i++ )
+            printf( "Level %2d : Cost = %6d. Ranks = %6.3f.\n", i, pLevelCosts[i], ((double)pLevelCosts[i])/RankCost );
+        printf( "TOTAL    : Cost = %6d. Ranks = %3d.\n", CostTotal, nRanksTotal );
+    }
+    return nRanksTotal;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/rwt/rwt.h b/src/temp/rwt/rwt.h
index f9c4dc51..8f24842b 100644
--- a/src/temp/rwt/rwt.h
+++ b/src/temp/rwt/rwt.h
@@ -70,7 +70,9 @@ struct Rwt_Man_t_
     int                nClasses;         // the number of NN classes
     // the result of resynthesis
     int                fCompl;           // indicates if the output of FF should be complemented
+    void *             pCut;             // the decomposition tree (temporary)
     void *             pGraph;           // the decomposition tree (temporary)
+    char *             pPerm;            // permutation used for the best cut
     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
     Vec_Ptr_t *        vFaninsCur;       // the fanins array (temporary)
     Vec_Int_t *        vLevNums;         // the array of levels (temporary)
diff --git a/src/temp/rwt/rwtMan.c b/src/temp/rwt/rwtMan.c
index f7dd38a7..869043a4 100644
--- a/src/temp/rwt/rwtMan.c
+++ b/src/temp/rwt/rwtMan.c
@@ -200,7 +200,7 @@ void Rwt_ManPrintStats( Rwt_Man_t * p )
     PRT( "Update      ", p->timeUpdate );
     PRT( "TOTAL       ", p->timeTotal );
 
-
+/*
     printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
@@ -210,7 +210,7 @@ void Rwt_ManPrintStats( Rwt_Man_t * p )
             Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
         }
     printf( "\n" );
-
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/temp/xyz/module.make b/src/temp/xyz/module.make
deleted file mode 100644
index f84fa8cc..00000000
--- a/src/temp/xyz/module.make
+++ /dev/null
@@ -1,8 +0,0 @@
-SRC +=    src/temp/xyz/xyzBuild.c \
-    src/temp/xyz/xyzCore.c \
-    src/temp/xyz/xyzMan.c \
-    src/temp/xyz/xyzMinEsop.c \
-    src/temp/xyz/xyzMinMan.c \
-    src/temp/xyz/xyzMinSop.c \
-    src/temp/xyz/xyzMinUtil.c \
-    src/temp/xyz/xyzTest.c 
diff --git a/src/temp/xyz/xyz.h b/src/temp/xyz/xyz.h
deleted file mode 100644
index 4fec2150..00000000
--- a/src/temp/xyz/xyz.h
+++ /dev/null
@@ -1,110 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyz.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __XYZ_H__
-#define __XYZ_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#include "abc.h"
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Xyz_Man_t_  Xyz_Man_t;
-typedef struct Xyz_Obj_t_  Xyz_Obj_t;
-
-// storage for node information
-struct Xyz_Obj_t_
-{
-    Min_Cube_t *      pCover[3];    // pos/neg/esop
-    Vec_Int_t *       vSupp;        // computed support (all nodes except CIs)
-};
-
-// storage for additional information
-struct Xyz_Man_t_
-{
-    // general characteristics
-    int               nFaninMax;    // the number of vars
-    int               nCubesMax;    // the limit on the number of cubes in the intermediate covers
-    int               nWords;       // the number of words
-    Vec_Int_t *       vFanCounts;   // fanout counts
-    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
-    Vec_Int_t *       vPairs0;      // the first var in each pair of common vars
-    Vec_Int_t *       vPairs1;      // the second var in each pair of common vars
-    Vec_Int_t *       vTriv0;       // trival support of the first node
-    Vec_Int_t *       vTriv1;       // trival support of the second node
-    // statistics
-    int               nSupps;       // supports created
-    int               nSuppsMax;    // the maximum number of supports
-    int               nBoundary;    // the boundary size
-    int               nNodes;       // the number of nodes processed
-};
-
-static inline Xyz_Obj_t *  Abc_ObjGetStr( Abc_Obj_t * pObj )                       { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
-
-static inline void         Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec )    { Abc_ObjGetStr(pObj)->vSupp = vVec;   }
-static inline Vec_Int_t *  Abc_ObjGetSupp( Abc_Obj_t * pObj )                      { return Abc_ObjGetStr(pObj)->vSupp;   }
-
-static inline void         Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj )                    { return Abc_ObjGetStr(pObj)->pCover[2]; }
-
-static inline void         Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol )                    { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== xyzBuild.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-/*=== xyzCore.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-/*=== xyzMan.c ============================================================*/
-extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
-extern void        Xyz_ManFree( Xyz_Man_t * p );
-extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
-/*=== xyzTest.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-
diff --git a/src/temp/xyz/xyzBuild.c b/src/temp/xyz/xyzBuild.c
deleted file mode 100644
index e32721e7..00000000
--- a/src/temp/xyz/xyzBuild.c
+++ /dev/null
@@ -1,379 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzBuild.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Network construction procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
-{
-    Vec_Int_t * vLits;
-    Abc_Obj_t * pNodeNew, * pFanin;
-    int i, iFanin, Lit;
-    // create empty cube
-    if ( pCube->nLits == 0 )
-        return Abc_NodeCreateConst1(pNtkNew);
-    // get the literals of this cube
-    vLits = Vec_IntAlloc( 10 );
-    Min_CubeGetLits( pCube, vLits );
-    assert( pCube->nLits == (unsigned)vLits->nSize );
-    // create special case when there is only one literal
-    if ( pCube->nLits == 1 )
-    {
-        iFanin = Vec_IntEntry(vLits,0);
-        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
-        Lit = Min_CubeGetVar(pCube, iFanin);
-        assert( Lit == 1 || Lit == 2 );
-        Vec_IntFree( vLits );
-        if ( Lit == 1 )// negative
-            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
-        return pFanin->pCopy;
-    }
-    assert( pCube->nLits > 1 );
-    // create the AND cube
-    pNodeNew = Abc_NtkCreateNode( pNtkNew );
-    for ( i = 0; i < vLits->nSize; i++ )
-    {
-        iFanin = Vec_IntEntry(vLits,i);
-        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
-        Lit = Min_CubeGetVar(pCube, iFanin);
-        assert( Lit == 1 || Lit == 2 );
-        Vec_IntWriteEntry( vLits, i, Lit==1 );
-        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
-    }
-    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
-    Vec_IntFree( vLits );
-    return pNodeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level )
-{
-    Min_Cube_t * pCover, * pCube;
-    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
-    Vec_Int_t * vSupp;
-    int Entry, nCubes, i;
-
-    if ( Abc_ObjIsCi(pObj) )
-        return pObj->pCopy;
-    assert( Abc_ObjIsNode(pObj) );
-    // skip if already computed
-    if ( pObj->pCopy )
-        return pObj->pCopy;
-
-    // get the support and the cover
-    vSupp  = Abc_ObjGetSupp( pObj ); 
-    pCover = Abc_ObjGetCover2( pObj );
-    assert( vSupp );
-/*
-    if ( pCover &&  pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 )
-    {
-        printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) );
-        Min_CoverWrite( stdout, pCover );
-    }
-*/
-/*
-    // print the support of this node
-    printf( "{ " );
-    Vec_IntForEachEntry( vSupp, Entry, i )
-        printf( "%d ", Entry );
-    printf( "}  cubes = %d\n", Min_CoverCountCubes( pCover ) );
-*/
-    // process the fanins
-    Vec_IntForEachEntry( vSupp, Entry, i )
-    {
-        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
-        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 );
-    }
-
-    // for each cube, construct the node
-    nCubes = Min_CoverCountCubes( pCover );
-    if ( nCubes == 0 )
-        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
-    else if ( nCubes == 1 )
-        pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp );
-    else
-    {
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );
-        Min_CoverForEachCube( pCover, pCube )
-        {
-            pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp );
-            Abc_ObjAddFanin( pNodeNew, pFaninNew );
-        }
-        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
-    }
-/*
-    printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
-    Vec_IntForEachEntry( vSupp, Entry, i )
-    {
-        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
-        printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
-    }
-    printf( "\n" );
-    Min_CoverWrite( stdout, pCover );
-*/
-    pObj->pCopy = pNodeNew;
-    return pNodeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
-    // reconstruct the network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 );
-//        printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id );
-    }
-    // add the COs
-    Abc_NtkFinalize( pNtk, pNtkNew );
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkXyzDerive: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-    return pNtkNew;
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
-{
-    assert( pObj->pCopy );
-    if ( !fCompl )
-        return pObj->pCopy;
-    if ( pObj->pCopy->pCopy == NULL )
-        pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
-    return pObj->pCopy->pCopy;
- }
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
-{
-    Vec_Int_t * vLits;
-    Abc_Obj_t * pNodeNew, * pFanin;
-    int i, iFanin, Lit;
-    // create empty cube
-    if ( pCube->nLits == 0 )
-        return Abc_NodeCreateConst1(pNtkNew);
-    // get the literals of this cube
-    vLits = Vec_IntAlloc( 10 );
-    Min_CubeGetLits( pCube, vLits );
-    assert( pCube->nLits == (unsigned)vLits->nSize );
-    // create special case when there is only one literal
-    if ( pCube->nLits == 1 )
-    {
-        iFanin = Vec_IntEntry(vLits,0);
-        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
-        Lit = Min_CubeGetVar(pCube, iFanin);
-        assert( Lit == 1 || Lit == 2 );
-        Vec_IntFree( vLits );
-//        if ( Lit == 1 )// negative
-//            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
-//        return pFanin->pCopy;
-        return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 );
-    }
-    assert( pCube->nLits > 1 );
-    // create the AND cube
-    pNodeNew = Abc_NtkCreateNode( pNtkNew );
-    for ( i = 0; i < vLits->nSize; i++ )
-    {
-        iFanin = Vec_IntEntry(vLits,i);
-        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
-        Lit = Min_CubeGetVar(pCube, iFanin);
-        assert( Lit == 1 || Lit == 2 );
-        Vec_IntWriteEntry( vLits, i, Lit==1 );
-//        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
-        Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) );
-    }
-//    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
-    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL );
-    Vec_IntFree( vLits );
-    return pNodeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
-{
-    Min_Cube_t * pCover, * pCube;
-    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
-    Vec_Int_t * vSupp;
-    int Entry, nCubes, i;
-
-    // skip if already computed
-    if ( pObj->pCopy )
-        return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
-    assert( Abc_ObjIsNode(pObj) );
-
-    // get the support and the cover
-    vSupp  = Abc_ObjGetSupp( pObj ); 
-    pCover = Abc_ObjGetCover2( pObj );
-    assert( vSupp );
-
-    // process the fanins
-    Vec_IntForEachEntry( vSupp, Entry, i )
-    {
-        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
-        Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 );
-    }
-
-    // for each cube, construct the node
-    nCubes = Min_CoverCountCubes( pCover );
-    if ( nCubes == 0 )
-        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
-    else if ( nCubes == 1 )
-        pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp );
-    else
-    {
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );
-        Min_CoverForEachCube( pCover, pCube )
-        {
-            pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
-            Abc_ObjAddFanin( pNodeNew, pFaninNew );
-        }
-        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
-    }
-
-    pObj->pCopy = pNodeNew;
-    return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the decomposed network.]
-
-  Description [The resulting network contains only pure AND/OR/EXOR gates
-  and inverters. This procedure is usedful to generate Verilog.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pNodeNew;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
-    // reconstruct the network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
-        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
-    }
-    // add the COs
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-    return pNtkNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzCore.c b/src/temp/xyz/xyzCore.c
deleted file mode 100644
index e5089788..00000000
--- a/src/temp/xyz/xyzCore.c
+++ /dev/null
@@ -1,1025 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Core procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-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                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose )
-{
-    Abc_Ntk_t * pNtkNew;
-    Xyz_Man_t * p;
-
-    assert( Abc_NtkIsStrash(pNtk) );
-
-    // create the manager
-    p = Xyz_ManAlloc( pNtk, nFaninMax );
-    p->fUseEsop = fUseEsop;
-    p->fUseSop  = 1;//fUseSop;
-    pNtk->pManCut = p;
-
-    // perform mapping
-    Abc_NtkXyzCovers( p, pNtk, fVerbose );
-
-    // derive the final network
-    if ( fUseInvs )
-        pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
-    else
-        pNtkNew = Abc_NtkXyzDerive( p, pNtk );
-//    pNtkNew = NULL;
-
-
-    Xyz_ManFree( p );
-    pNtk->pManCut = NULL;
-
-    // make sure that everything is okay
-    if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkXyz: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute the supports.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
-{
-    Abc_Obj_t * pObj;
-    int i, clk = clock();
-
-    // start the manager
-    p->vFanCounts = Abc_NtkFanoutCounts(pNtk);
-
-    // set trivial cuts for the constant and the CIs
-    pObj = Abc_NtkConst1(pNtk);
-    pObj->fMarkA = 1;
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->fMarkA = 1;
-
-    // perform iterative decomposition
-    for ( i = 0; ; i++ )
-    {
-        if ( fVerbose )
-        printf( "Iter %d : ", i+1 );
-        if ( Abc_NtkXyzCoversOne(p, pNtk, fVerbose) )
-            break;
-    }
-
-    // clean the cut-point markers
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        pObj->fMarkA = 0;
-
-if ( fVerbose )
-{
-PRT( "Total", clock() - clk );
-}
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute the supports.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
-{
-    ProgressBar * pProgress;
-    Abc_Obj_t * pObj;
-    Vec_Ptr_t * vBoundary;
-    int i, clk = clock();
-    int Counter = 0;
-    int fStop = 1;
-
-    // array to collect the nodes in the new boundary
-    vBoundary = Vec_PtrAlloc( 100 );
-
-    // start from the COs and mark visited nodes using pObj->fMarkB
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // skip the solved nodes (including the CIs)
-        pObj = Abc_ObjFanin0(pObj);
-        if ( pObj->fMarkA )
-        {
-            Counter++;
-            continue;
-        } 
-
-        // traverse the cone starting from this node
-        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
-            Counter++;
-
-/*
-        printf( "%-15s : ", Abc_ObjName(pObj) ); 
-        printf( "lev = %5d  ", pObj->Level );
-        if ( Abc_ObjGetSupp(pObj) == NULL )
-        {
-            printf( "\n" );
-            continue;
-        }
-        printf( "supp = %3d  ", Abc_ObjGetSupp(pObj)->nSize ); 
-        printf( "esop = %3d  ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); 
-        printf( "\n" );
-*/
-    }
-    Extra_ProgressBarStop( pProgress );
-
-    // clean visited nodes
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        pObj->fMarkB = 0;
-
-    // create the new boundary
-    p->nBoundary = 0;
-    Vec_PtrForEachEntry( vBoundary, pObj, i )
-    {
-        if ( !pObj->fMarkA )
-        {
-            pObj->fMarkA = 1;
-            p->nBoundary++;
-        }
-    }
-    Vec_PtrFree( vBoundary );
-
-if ( fVerbose )
-{
-    printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d  Bound = %4d  ", 
-        Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary );
-PRT( "T", clock() - clk );
-}
-    return fStop;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary )
-{
-    Abc_Obj_t * pObj0, * pObj1;
-    // return if the support is already computed
-    if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
-        return;
-    // mark as visited
-    pObj->fMarkB = 1;
-    // get the fanins
-    pObj0 = Abc_ObjFanin0(pObj);
-    pObj1 = Abc_ObjFanin1(pObj);
-    // solve for the fanins
-    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_NodeXyzPropagate( p, pObj ) )           // node's support or covers cannot be computed
-    {
-        // save the nodes of the future boundary
-        if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
-            Vec_PtrPush( vBoundary, pObj0 );
-        if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) )
-            Vec_PtrPush( vBoundary, pObj1 );
-        return;
-    }
-    // consider dropping the fanin supports
-//    Abc_NodeXyzDropData( p, pObj0 );
-//    Abc_NodeXyzDropData( p, pObj1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 )
-{
-    Vec_Int_t * vSupp;
-    int k0, k1;
-
-    assert( vSupp0 && vSupp1 );
-    Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
-    Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
-    Vec_IntClear( p->vPairs0 );
-    Vec_IntClear( p->vPairs1 );
-
-    vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize );
-    for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
-    {
-        if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
-        {
-            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
-            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
-            Vec_IntPush( p->vPairs0, k0 );
-            Vec_IntPush( p->vPairs1, k1 );
-            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
-            k0++; k1++;
-        }
-        else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
-        {
-            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
-            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
-            k0++;
-        }
-        else 
-        {
-            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
-            Vec_IntPush( vSupp, vSupp1->pArray[k1] );
-            k1++;
-        }
-    }
-    for ( ; k0 < vSupp0->nSize; k0++ )
-    {
-        Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
-        Vec_IntPush( vSupp, vSupp0->pArray[k0] );
-    }
-    for ( ; k1 < vSupp1->nSize; k1++ )
-    {
-        Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
-        Vec_IntPush( vSupp, vSupp1->pArray[k1] );
-    }
-/*
-    printf( "Zero : " );
-    for ( k0 = 0; k0 < vSupp0->nSize; k0++ )
-        printf( "%d ", vSupp0->pArray[k0] );
-    printf( "\n" );
-
-    printf( "One  : " );
-    for ( k1 = 0; k1 < vSupp1->nSize; k1++ )
-        printf( "%d ", vSupp1->pArray[k1] );
-    printf( "\n" );
-
-    printf( "Sum  : " );
-    for ( k0 = 0; k0 < vSupp->nSize; k0++ )
-        printf( "%d ", vSupp->pArray[k0] );
-    printf( "\n" );
-    printf( "\n" );
-*/
-    return vSupp;
-}
-
-/**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 []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
-{
-    Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1;
-    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
-
-    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 covers
-    pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
-    pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
-
-    // complement the first if needed
-    if ( !Abc_ObjFaninC0(pObj) )
-        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 ( !Abc_ObjFaninC1(pObj) )
-        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 and minimize the cover (quit if too large)
-    if ( !Abc_NodeXyzProductEsop( p, pCover0, pCover1, vSupp->nSize ) )
-    {
-        pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
-        Min_CoverRecycle( p->pManMin, pCover );
-        Vec_IntFree( vSupp );
-        return 0;
-    }
-
-    // minimize the cover
-    Min_EsopMinimize( p->pManMin );
-    pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
-
-    // quit if the cover is too large
-    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
-    {
-        Min_CoverRecycle( p->pManMin, pCover );
-        Vec_IntFree( vSupp );
-        return 0;
-    }
-
-    // count statistics
-    p->nSupps++;
-    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
-
-    // set the covers
-    assert( Abc_ObjGetSupp(pObj) == NULL );
-    Abc_ObjSetSupp( pObj, vSupp );
-    Abc_ObjSetCover2( pObj, pCover );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
-{
-    Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1;
-    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
-    int fCompl0, fCompl1;
-
-    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);
-   
-    // prepare the positive cover
-    pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
-    pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
-
-    // derive and minimize the cover (quit if too large)
-    if ( !pCover0 || !pCover1 )
-        pCoverP = NULL;
-    else if ( !Abc_NodeXyzProductSop( p, pCover0, pCover1, vSupp->nSize ) )
-    {
-        pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
-        Min_CoverRecycle( p->pManMin, pCoverP );
-        pCoverP = NULL;
-    }
-    else
-    {
-        Min_SopMinimize( p->pManMin );
-        pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
-        // quit if the cover is too large
-        if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax )
-        {
-            Min_CoverRecycle( p->pManMin, pCoverP );
-            pCoverP = NULL;
-        }
-    }
-   
-    // prepare the negative cover
-    pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
-    pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
-
-    // derive and minimize the cover (quit if too large)
-    if ( !pCover0 || !pCover1 )
-        pCoverN = NULL;
-    else if ( !Abc_NodeXyzUnionSop( p, pCover0, pCover1, vSupp->nSize ) )
-    {
-        pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
-        Min_CoverRecycle( p->pManMin, pCoverN );
-        pCoverN = NULL;
-    }
-    else
-    {
-        Min_SopMinimize( p->pManMin );
-        pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
-        // quit if the cover is too large
-        if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax )
-        {
-            Min_CoverRecycle( p->pManMin, pCoverN );
-            pCoverN = NULL;
-        }
-    }
-
-    if ( pCoverP == NULL && pCoverN == NULL )
-    {
-        Vec_IntFree( vSupp );
-        return 0;
-    }
-
-    // count statistics
-    p->nSupps++;
-    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
-
-    // set the covers
-    assert( Abc_ObjGetSupp(pObj) == NULL );
-    Abc_ObjSetSupp( pObj, vSupp );
-    Abc_ObjSetCover( pObj, pCoverP, 0 );
-    Abc_ObjSetCover( pObj, pCoverN, 1 );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
-    Min_Cube_t * pCube, * pCube0, * pCube1;
-    int i, Val0, Val1;
-
-    // clean storage
-    Min_ManClean( p->pManMin, nSupp );
-    if ( pCover0 == NULL || pCover1 == NULL )
-        return 1;
-
-    // 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 )
-            return 0;
-
-        // 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
-        Min_EsopAddCube( p->pManMin, pCube );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
-    return 1;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
-    Min_Cube_t * pCube, * pCube0, * pCube1;
-    int i, Val0, Val1;
-
-    // clean storage
-    Min_ManClean( p->pManMin, nSupp );
-    if ( pCover0 )
-    {
-        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 )
-                return 0;
-            // add the cube to storage
-            Min_EsopAddCube( p->pManMin, pCube );
-        }
-    }
-    if ( pCover1 )
-    {
-        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 )
-                return 0;
-            // add the cube to storage
-            Min_EsopAddCube( p->pManMin, pCube );
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
-    return 1;
-}
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzInt.h b/src/temp/xyz/xyzInt.h
deleted file mode 100644
index 656612aa..00000000
--- a/src/temp/xyz/xyzInt.h
+++ /dev/null
@@ -1,642 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzInt.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Internal declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Min_Man_t_  Min_Man_t;
-typedef struct Min_Cube_t_ Min_Cube_t;
-
-struct Min_Man_t_
-{
-    int               nVars;          // the number of vars
-    int               nWords;         // the number of words
-    Extra_MmFixed_t * pMemMan;        // memory manager for cubes
-    // temporary cubes
-    Min_Cube_t *      pOne0;          // tautology cube
-    Min_Cube_t *      pOne1;          // tautology cube
-    Min_Cube_t *      pTriv0[2];      // trivial cube
-    Min_Cube_t *      pTriv1[2];      // trivial cube
-    Min_Cube_t *      pTemp;          // cube for computing the distance
-    Min_Cube_t *      pBubble;        // cube used as a separator
-    // temporary storage for the new cover
-    int               nCubes;         // the number of cubes
-    Min_Cube_t **     ppStore;        // storage for cubes by number of literals
-};
-
-struct Min_Cube_t_
-{
-    Min_Cube_t *      pNext;          // the pointer to the next cube in the cover
-    unsigned          nVars    : 10;  // the number of variables
-    unsigned          nWords   : 12;  // the number of machine words
-    unsigned          nLits    : 10;  // the number of literals in the cube
-    unsigned          uData[1];       // the bit-data for the cube
-};
-
-
-// iterators through the entries in the linked lists of cubes
-#define Min_CoverForEachCube( pCover, pCube )                   \
-    for ( pCube = pCover;                                       \
-          pCube;                                                \
-          pCube = pCube->pNext )
-#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )       \
-    for ( pCube = pCover,                                       \
-          pCube2 = pCube? pCube->pNext: NULL;                   \
-          pCube;                                                \
-          pCube = pCube2,                                       \
-          pCube2 = pCube? pCube->pNext: NULL )
-#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev )       \
-    for ( pCube = pCover,                                       \
-          ppPrev = &(pCover);                                   \
-          pCube;                                                \
-          ppPrev = &pCube->pNext,                               \
-          pCube = pCube->pNext )
-
-// macros to get hold of bits and values in the cubes
-static inline int  Min_CubeHasBit( Min_Cube_t * p, int i )              { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0;     }
-static inline void Min_CubeSetBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] |= (1<<((i) & 31));                 }
-static inline void Min_CubeXorBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] ^= (1<<((i) & 31));                 }
-static inline int  Min_CubeGetVar( Min_Cube_t * p, int Var )            { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
-static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31));     }
-
-/*=== xyzMinEsop.c ==========================================================*/
-extern void         Min_EsopMinimize( Min_Man_t * p );
-extern void         Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
-/*=== xyzMinSop.c ==========================================================*/
-extern void         Min_SopMinimize( Min_Man_t * p );
-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 );
-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 );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
-{
-    Min_Cube_t * pCube;
-    pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
-    pCube->pNext  = NULL;
-    pCube->nVars  = p->nVars;
-    pCube->nWords = p->nWords;
-    pCube->nLits  = 0;
-    memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
-    return pCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the cube representing elementary var.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
-{
-    Min_Cube_t * pCube;
-    pCube = Min_CubeAlloc( p );
-    Min_CubeXorBit( pCube, iVar*2+fCompl );
-    pCube->nLits = 1;
-    return pCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recycles the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
-{
-    Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recycles the cube cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube, * pCube2;
-    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
-        Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of cubes in the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubeCountLits( Min_Cube_t * pCube )
-{
-    unsigned uData;
-    int Count = 0, i, w;
-    for ( w = 0; w < (int)pCube->nWords; w++ )
-    {
-        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
-        for ( i = 0; i < 32; i += 2 )
-            if ( uData & (1 << i) )
-                Count++;
-    }
-    return Count;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of cubes in the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
-{
-    unsigned uData;
-    int i, w;
-    Vec_IntClear( vLits );
-    for ( w = 0; w < (int)pCube->nWords; w++ )
-    {
-        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
-        for ( i = 0; i < 32; i += 2 )
-            if ( uData & (1 << i) )
-                Vec_IntPush( vLits, w*16 + i/2 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of cubes in the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube;
-    int Count = 0;
-    Min_CoverForEachCube( pCover, pCube )
-        Count++;
-    return Count;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if two cubes are disjoint.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
-    unsigned uData;
-    int i;
-    assert( pCube0->nVars == pCube1->nVars );
-    for ( i = 0; i < (int)pCube0->nWords; i++ )
-    {
-        uData = pCube0->uData[i] & pCube1->uData[i];
-        uData = (uData | (uData >> 1)) & 0x55555555;
-        if ( uData != 0x55555555 )
-            return 1;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the disjoint variables of the two cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
-{
-    unsigned uData;
-    int i, w;
-    Vec_IntClear( vVars );
-    for ( w = 0; w < (int)pCube->nWords; w++ )
-    {
-        uData  = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
-        uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
-        if ( uData == 0 )
-            continue;
-        for ( i = 0; i < 32; i += 2 )
-            if ( uData & (1 << i) )
-                Vec_IntPush( vVars, w*16 + i/2 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if two cubes are disjoint.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
-{
-    unsigned uData;
-    int i, fFound = 0;
-    for ( i = 0; i < (int)pCube0->nWords; i++ )
-    {
-        uData = pCube0->uData[i] ^ pCube1->uData[i];
-        if ( uData == 0 )
-        {
-            if ( pTemp ) pTemp->uData[i] = 0;
-            continue;
-        }
-        if ( fFound )
-            return 0;
-        uData = (uData | (uData >> 1)) & 0x55555555;
-        if ( (uData & (uData-1)) > 0 ) // more than one 1
-            return 0;
-        if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
-        fFound = 1;
-    }
-    if ( fFound == 0 )
-    {
-        printf( "\n" );
-        Min_CubeWrite( stdout, pCube0 );
-        Min_CubeWrite( stdout, pCube1 );
-        printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if two cubes are disjoint.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
-{
-    unsigned uData;//, uData2;
-    int i, k, Var0 = -1, Var1 = -1;
-    for ( i = 0; i < (int)pCube0->nWords; i++ )
-    {
-        uData = pCube0->uData[i] ^ pCube1->uData[i];
-        if ( uData == 0 )
-            continue;
-        if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
-            return 0;
-        uData = (uData | (uData >> 1)) & 0x55555555;
-        if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
-            return 0;
-        for ( k = 0; k < 32; k += 2 )
-            if ( uData & (1 << k) )
-            {
-                if ( Var0 == -1 )
-                    Var0 = 16 * i + k/2;
-                else if ( Var1 == -1 )
-                    Var1 = 16 * i + k/2;
-                else
-                    return 0;
-            }
-        /*
-        if ( Var0 >= 0 )
-        {
-            uData &= 0xFFFF;
-            uData2 = (uData >> 16);
-            if ( uData && uData2 )
-                return 0;
-            if ( uData )
-            {
-            }
-            uData }= uData2;
-            uData &= 0x
-        }
-        */
-    }
-    if ( Var0 >= 0 && Var1 >= 0 )
-    {
-        *pVar0 = Var0;
-        *pVar1 = Var1;
-        return 1;
-    }
-    if ( Var0 == -1 || Var1 == -1 )
-    {
-        printf( "\n" );
-        Min_CubeWrite( stdout, pCube0 );
-        Min_CubeWrite( stdout, pCube1 );
-        printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the produce of two cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
-    Min_Cube_t * pCube;
-    int i;
-    assert( pCube0->nVars == pCube1->nVars );
-    pCube = Min_CubeAlloc( p );
-    for ( i = 0; i < p->nWords; i++ )
-        pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
-    pCube->nLits = Min_CubeCountLits( pCube );
-    return pCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the produce of two cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
-    Min_Cube_t * pCube;
-    int i;
-    assert( pCube0->nVars == pCube1->nVars );
-    pCube = Min_CubeAlloc( p );
-    for ( i = 0; i < p->nWords; i++ )
-        pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
-    pCube->nLits = Min_CubeCountLits( pCube );
-    return pCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the produce of two cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
-    int i;
-    for ( i = 0; i < (int)pCube0->nWords; i++ )
-        if ( pCube0->uData[i] != pCube1->uData[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pCube1 is contained in pCube0, bitwise.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
-    int i;
-    for ( i = 0; i < (int)pCube0->nWords; i++ )
-        if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transforms the cube into the result of merging.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
-{
-    int w;
-    for ( w = 0; w < (int)pCube->nWords; w++ )
-    {
-        pCube->uData[w]  =  pCube->uData[w] ^ pDist->uData[w];
-        pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
-    }
-}
-
-/**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*************************************************************
-
-  Synopsis    [Sorts the cover in the increasing number of literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube, * pCube2, * pThis;
-    if ( pCover == NULL )
-    {
-        Min_ManClean( p, p->nVars );
-        return;
-    }
-    Min_ManClean( p, pCover->nVars );
-    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
-    {
-        // go through the linked list
-        Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
-            if ( Min_CubesAreEqual( pCube, pThis ) )
-            {
-                Min_CubeRecycle( p, pCube );
-                break;
-            }
-        if ( pThis != NULL )
-            continue;
-        pCube->pNext = p->ppStore[pCube->nLits];
-        p->ppStore[pCube->nLits] = pCube;
-        p->nCubes++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the given cube is contained in one of the cubes of the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
-{
-    Min_Cube_t * pThis;
-    int i;
-/*
-    // 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;
-    }
-    return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzMan.c b/src/temp/xyz/xyzMan.c
deleted file mode 100644
index 844e8c13..00000000
--- a/src/temp/xyz/xyzMan.c
+++ /dev/null
@@ -1,144 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Decomposition manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
-{
-    Xyz_Man_t * pMan;
-    Xyz_Obj_t * pMem;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( pNtk->pManCut == NULL );
-
-    // start the manager
-    pMan = ALLOC( Xyz_Man_t, 1 );
-    memset( pMan, 0, sizeof(Xyz_Man_t) );
-    pMan->nFaninMax = nFaninMax;
-    pMan->nCubesMax = 2 * pMan->nFaninMax;
-    pMan->nWords    = Abc_BitWordNum( nFaninMax * 2 );
-
-    // get the cubes
-    pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
-    pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
-    pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
-    pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
-    pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
-    pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
-
-    // allocate memory for object structures
-    pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
-    memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
-    // allocate storage for the pointers to the memory
-    pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
-    Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
-    // create the cube manager
-    pMan->pManMin = Min_ManAlloc( nFaninMax );
-    return pMan;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Xyz_ManFree( Xyz_Man_t * p )
-{
-    Vec_Int_t * vSupp;
-    int i;
-    for ( i = 0; i < p->vObjStrs->nSize; i++ )
-    {
-        vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
-        if ( vSupp ) Vec_IntFree( vSupp );
-    }
-
-    Min_ManFree( p->pManMin );
-    Vec_PtrFree( p->vObjStrs );
-    Vec_IntFree( p->vFanCounts );
-    Vec_IntFree( p->vTriv0 );
-    Vec_IntFree( p->vTriv1 );
-    Vec_IntFree( p->vComTo0 );
-    Vec_IntFree( p->vComTo1 );
-    Vec_IntFree( p->vPairs0 );
-    Vec_IntFree( p->vPairs1 );
-    free( p->pMemory );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Drop the covers at the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
-{
-    int nFanouts;
-    assert( p->vFanCounts );
-    nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
-    assert( nFanouts > 0 );
-    if ( --nFanouts == 0 )
-    {
-        Vec_IntFree( Abc_ObjGetSupp(pObj) );
-        Abc_ObjSetSupp( pObj, NULL );
-        Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
-        Abc_ObjSetCover2( pObj, NULL );
-        p->nSupps--;
-    }
-    Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzMinEsop.c b/src/temp/xyz/xyzMinEsop.c
deleted file mode 100644
index 839e2410..00000000
--- a/src/temp/xyz/xyzMinEsop.c
+++ /dev/null
@@ -1,299 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzMinEsop.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [ESOP manipulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Min_EsopRewrite( Min_Man_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_EsopMinimize( Min_Man_t * p )
-{
-    int nCubesInit, nCubesOld, nIter;
-    if ( p->nCubes < 3 )
-        return;
-    nIter = 0;
-    nCubesInit = p->nCubes;
-    do {
-        nCubesOld = p->nCubes;
-        Min_EsopRewrite( p );
-        nIter++;
-    }
-    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
-
-//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
-
-  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 []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_EsopRewrite( Min_Man_t * p )
-{
-    Min_Cube_t * pCube, ** ppPrev;
-    Min_Cube_t * pThis, ** ppPrevT;
-    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
-    int nPairs = 0;
-
-    // insert the bubble before the first cube
-    p->pBubble->pNext = p->ppStore[0];
-    p->ppStore[0] = p->pBubble;
-    p->pBubble->nLits = 0;
-
-    // go through the cubes
-    while ( 1 )
-    {
-        // get the index of the bubble
-        Index = p->pBubble->nLits;
-
-        // find the bubble
-        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
-            if ( pCube == p->pBubble )
-                break;
-        assert( pCube == p->pBubble );
-
-        // remove the bubble, get the next cube after the bubble
-        *ppPrev = p->pBubble->pNext;
-        pCube = p->pBubble->pNext;
-        if ( pCube == NULL )
-            for ( Index++; Index <= p->nVars; Index++ )
-                if ( p->ppStore[Index] )
-                {
-                    ppPrev = &(p->ppStore[Index]);
-                    pCube = p->ppStore[Index];
-                    break;
-                }
-        // stop if there is no more cubes
-        if ( pCube == NULL )
-            break;
-
-        // find the first dist2 cube
-        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
-            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
-                break;
-        if ( pThis == NULL && Index < p->nVars )
-        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
-            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
-                break;
-        if ( pThis == NULL && Index < p->nVars - 1 )
-        Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
-            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
-                break;
-        // continue if there is no dist2 cube
-        if ( pThis == NULL )
-        {
-            // insert the bubble after the cube
-            p->pBubble->pNext = pCube->pNext;
-            pCube->pNext = p->pBubble;
-            p->pBubble->nLits = pCube->nLits;
-            continue;
-        }
-        nPairs++;
-
-        // remove the cubes, insert the bubble instead of pCube
-        *ppPrevT = pThis->pNext;
-        *ppPrev = p->pBubble;
-        p->pBubble->pNext = pCube->pNext;
-        p->pBubble->nLits = pCube->nLits;
-        p->nCubes -= 2;
-
-        // Exorlink-2:
-        // A{v00}     B{v01}      +  A{v10}     B{v11}     =
-        // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} =
-        // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11}
-
-        // save the dist2 parameters
-        v00 = Min_CubeGetVar( pCube, Var0 );
-        v01 = Min_CubeGetVar( pCube, Var1 );
-        v10 = Min_CubeGetVar( pThis, Var0 );
-        v11 = Min_CubeGetVar( pThis, Var1 );
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
-        // derive the first pair of resulting cubes
-        Min_CubeXorVar( pCube, Var0, v10 );
-        pCube->nLits -= (v00 != 3);
-        pCube->nLits += ((v00 ^ v10) != 3);
-        Min_CubeXorVar( pThis, Var1, v01 );
-        pThis->nLits -= (v11 != 3);
-        pThis->nLits += ((v01 ^ v11) != 3);
-
-        // add the cubes
-        nCubesOld = p->nCubes;
-        Min_EsopAddCube( p, pCube );
-        Min_EsopAddCube( p, pThis );
-        // check if the cubes were absorbed
-        if ( p->nCubes < nCubesOld + 2 )
-            continue;
-
-        // pull out both cubes
-        assert( pThis == p->ppStore[pThis->nLits] );
-        p->ppStore[pThis->nLits] = pThis->pNext;
-        assert( pCube == p->ppStore[pCube->nLits] );
-        p->ppStore[pCube->nLits] = pCube->pNext;
-        p->nCubes -= 2;
-
-        // derive the second pair of resulting cubes
-        Min_CubeXorVar( pCube, Var0, v10 );
-        pCube->nLits -= ((v00 ^ v10) != 3);
-        pCube->nLits += (v00 != 3);
-        Min_CubeXorVar( pCube, Var1, v11 );
-        pCube->nLits -= (v01 != 3);
-        pCube->nLits += ((v01 ^ v11) != 3);
-
-        Min_CubeXorVar( pThis, Var0, v00 );
-        pThis->nLits -= (v10 != 3);
-        pThis->nLits += ((v00 ^ v10) != 3);
-        Min_CubeXorVar( pThis, Var1, v01 );
-        pThis->nLits -= ((v01 ^ v11) != 3);
-        pThis->nLits += (v11 != 3);
-
-        // add them anyhow
-        Min_EsopAddCube( p, pCube );
-        Min_EsopAddCube( p, pThis );
-    }
-//    printf( "Pairs = %d  ", nPairs );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the 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 []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
-{
-    Min_Cube_t * pThis, ** ppPrev;
-    // try to find the identical cube
-    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
-    {
-        if ( Min_CubesAreEqual( pCube, pThis ) )
-        {
-            *ppPrev = pThis->pNext;
-            Min_CubeRecycle( p, pCube );
-            Min_CubeRecycle( p, pThis );
-            p->nCubes--;
-            return 0;
-        }
-    }
-    // find a distance-1 cube if it exists
-    if ( pCube->nLits < pCube->nVars )
-    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
-    {
-        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
-        {
-            *ppPrev = pThis->pNext;
-            Min_CubesTransform( pCube, pThis, p->pTemp );
-            pCube->nLits++;
-            Min_CubeRecycle( p, pThis );
-            p->nCubes--;
-            return 1;
-        }
-    }
-    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
-    {
-        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
-        {
-            *ppPrev = pThis->pNext;
-            Min_CubesTransform( pCube, pThis, p->pTemp );
-            pCube->nLits--;
-            Min_CubeRecycle( p, pThis );
-            p->nCubes--;
-            return 1;
-        }
-    }
-    if ( pCube->nLits > 0 )
-    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
-    {
-        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
-        {
-            *ppPrev = pThis->pNext;
-            Min_CubesTransform( pCube, pThis, p->pTemp );
-            Min_CubeRecycle( p, pThis );
-            p->nCubes--;
-            return 1;
-        }
-    }
-    // add the cube
-    pCube->pNext = p->ppStore[pCube->nLits];
-    p->ppStore[pCube->nLits] = pCube;
-    p->nCubes++;
-    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/temp/xyz/xyzMinMan.c b/src/temp/xyz/xyzMinMan.c
deleted file mode 100644
index 20314698..00000000
--- a/src/temp/xyz/xyzMinMan.c
+++ /dev/null
@@ -1,113 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzMinMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [SOP manipulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the minimization manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Min_Man_t * Min_ManAlloc( int nVars )
-{
-    Min_Man_t * pMan;
-    // start the manager
-    pMan = ALLOC( Min_Man_t, 1 );
-    memset( pMan, 0, sizeof(Min_Man_t) );
-    pMan->nVars   = nVars;
-    pMan->nWords  = Abc_BitWordNum( nVars * 2 );
-    pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
-    // allocate storage for the temporary cover
-    pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 );
-    // create tautology cubes
-    Min_ManClean( pMan, nVars );
-    pMan->pOne0  = Min_CubeAlloc( pMan );
-    pMan->pOne1  = Min_CubeAlloc( pMan );
-    pMan->pTemp  = Min_CubeAlloc( pMan );
-    pMan->pBubble = Min_CubeAlloc( pMan );  pMan->pBubble->uData[0] = 0;
-    // create trivial cubes
-    Min_ManClean( pMan, 1 );
-    pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
-    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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the minimization manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_ManClean( Min_Man_t * p, int nSupp )
-{
-    // set the size of the cube manager
-    p->nVars  = nSupp;
-    p->nWords = Abc_BitWordNum(2*nSupp);
-    // clean the storage
-    memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
-    p->nCubes = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the minimization manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_ManFree( Min_Man_t * p )
-{
-    Extra_MmFixedStop ( p->pMemMan, 0 );
-    free( p->ppStore );
-    free( p );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzMinSop.c b/src/temp/xyz/xyzMinSop.c
deleted file mode 100644
index a5d57c66..00000000
--- a/src/temp/xyz/xyzMinSop.c
+++ /dev/null
@@ -1,615 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzMinSop.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [SOP manipulation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Min_SopRewrite( Min_Man_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_SopMinimize( Min_Man_t * p )
-{
-    int nCubesInit, nCubesOld, nIter;
-    if ( p->nCubes < 3 )
-        return;
-    nIter = 0;
-    nCubesInit = p->nCubes;
-    do {
-        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" );
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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, 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];
-    p->ppStore[0] = p->pBubble;
-    p->pBubble->nLits = 0;
-
-    // go through the cubes
-    while ( 1 )
-    {
-        // get the index of the bubble
-        Index = p->pBubble->nLits;
-
-        // find the bubble
-        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
-            if ( pCube == p->pBubble )
-                break;
-        assert( pCube == p->pBubble );
-
-        // remove the bubble, get the next cube after the bubble
-        *ppPrev = p->pBubble->pNext;
-        pCube = p->pBubble->pNext;
-        if ( pCube == NULL )
-            for ( Index++; Index <= p->nVars; Index++ )
-                if ( p->ppStore[Index] )
-                {
-                    ppPrev = &(p->ppStore[Index]);
-                    pCube = p->ppStore[Index];
-                    break;
-                }
-        // stop if there is no more cubes
-        if ( pCube == NULL )
-            break;
-
-        // find the first dist2 cube
-        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
-            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
-                break;
-        if ( pThis == NULL && Index < p->nVars )
-        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
-            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
-                break;
-        // continue if there is no dist2 cube
-        if ( pThis == NULL )
-        {
-            // insert the bubble after the cube
-            p->pBubble->pNext = pCube->pNext;
-            pCube->pNext = p->pBubble;
-            p->pBubble->nLits = pCube->nLits;
-            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;
-        p->pBubble->pNext = pCube->pNext;
-        p->pBubble->nLits = pCube->nLits;
-        p->nCubes -= 2;
-
-        assert( pCube != p->pBubble && pThis != p->pBubble );
-
-
-        // save the dist2 parameters
-        v00 = Min_CubeGetVar( pCube, Var0 );
-        v01 = Min_CubeGetVar( pCube, Var1 );
-        v10 = Min_CubeGetVar( pThis, Var0 );
-        v11 = Min_CubeGetVar( pThis, Var1 );
-        assert( v00 != v10 && v01 != v11 );
-        assert( v00 != 3   || v01 != 3 );
-        assert( v10 != 3   || v11 != 3 );
-
-//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;
-        }
-
-        // make sure the first cube has first var DC
-        if ( v00 != 3 )
-        {
-            assert( v01 == 3 );
-            Index = Var0; Var0 = Var1; Var1 = Index;
-            Index = v00; v00 = v01; v01 = Index;
-            Index = v10; v10 = v11; v11 = Index;
-        }
-
-        // consider both cases: both have DC lit
-        if ( v00 == 3 && v11 == 3 )
-        {
-            assert( v01 != 3 && v10 != 3 );
-            // 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 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 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds cube to the SOP cover stored in the manager.]
-
-  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_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
-{
-    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    [Adds the cube to storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
-{
-    assert( Min_CubeCheck( pCube ) );
-    assert( pCube != p->pBubble );
-    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
-    while ( Min_SopAddCubeInt( p, pCube ) );
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_SopContain( Min_Man_t * p )
-{
-    Min_Cube_t * pCube, * pCube2, ** ppPrev;
-    int i, k;
-    for ( i = 0; i <= p->nVars; i++ )
-    {
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-        Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
-        {
-            if ( !Min_CubesAreEqual( pCube, pCube2 ) )
-                continue;
-            *ppPrev = pCube2->pNext;
-            Min_CubeRecycle( p, pCube2 );
-            p->nCubes--;
-        }
-        for ( k = i + 1; k <= p->nVars; k++ )
-        Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
-        {
-            if ( !Min_CubeIsContained( pCube, pCube2 ) )
-                continue;
-            *ppPrev = pCube2->pNext;
-            Min_CubeRecycle( p, pCube2 );
-            p->nCubes--;
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  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;
-     Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
-     int Num, Value, i;
-
-     // get the variables
-     vVars = Vec_IntAlloc( 100 );
-    // create the tautology cube
-     pCover = Min_CubeAlloc( p );
-     // sharp it with all cubes
-     Min_CoverForEachCube( pSharp, pCube )
-     Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
-     {
-        if ( Min_CubesDisjoint( pThis, pCube ) )
-            continue;
-        // remember the next pointer
-        pNext = pThis->pNext;
-        // get the variables, in which pThis is '-' while pCube is fixed
-        Min_CoverGetDisjVars( pThis, pCube, vVars );
-        // generate the disjoint cubes
-        pReady = pThis;
-        Vec_IntForEachEntryReverse( vVars, Num, i )
-        {
-            // correct the literal
-            Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
-            if ( i == 0 )
-                break;
-            // create the new cube and clean this value
-            Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
-            pReady = Min_CubeDup( p, pReady );
-            Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
-            // add to the cover
-            *ppPrev = pReady;
-            ppPrev = &pReady->pNext;
-        }
-        pThis = pReady;
-        pThis->pNext = pNext;
-     }
-     Vec_IntFree( vVars );
-
-     // perform dist-1 merge and contain
-     Min_CoverExpandRemoveEqual( p, pCover );
-     Min_SopDist1Merge( p );
-     Min_SopContain( p );
-     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/temp/xyz/xyzMinUtil.c b/src/temp/xyz/xyzMinUtil.c
deleted file mode 100644
index 9ec5f83f..00000000
--- a/src/temp/xyz/xyzMinUtil.c
+++ /dev/null
@@ -1,277 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzMinUtil.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Utilities.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
-{
-    int i;
-    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
-    for ( i = 0; i < (int)pCube->nVars; i++ )
-        if ( Min_CubeHasBit(pCube, i*2) )
-        {
-            if ( Min_CubeHasBit(pCube, i*2+1) )
-                fprintf( pFile, "-" );
-            else
-                fprintf( pFile, "0" );
-        }
-        else
-        {
-            if ( Min_CubeHasBit(pCube, i*2+1) )
-                fprintf( pFile, "1" );
-            else
-                fprintf( pFile, "?" );
-        }
-    fprintf( pFile, " 1\n" );
-//    fprintf( pFile, " %d\n", pCube->nLits );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube;
-    Min_CoverForEachCube( pCover, pCube )
-        Min_CubeWrite( pFile, pCube );
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  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.%s", pName, fEsop? "esop" : "pla" );
-    for ( i = strlen(Buffer) - 1; i >= 0; i-- )
-        if ( Buffer[i] == '<' || Buffer[i] == '>' )
-            Buffer[i] = '_';
-    pFile = fopen( Buffer, "w" );
-    fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
-    fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
-    fprintf( pFile, ".o %d\n", 1 );
-    fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
-    if ( fEsop ) fprintf( pFile, ".type esop\n" );
-    Min_CoverForEachCube( pCover, pCube )
-        Min_CubeWrite( pFile, pCube );
-    fprintf( pFile, ".e\n" );
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_CoverCheck( Min_Man_t * p )
-{
-    Min_Cube_t * pCube;
-    int i;
-    for ( i = 0; i <= p->nVars; i++ )
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-            assert( i == (int)pCube->nLits );
-}
-
-
-/**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 []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
-{
-    Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
-    Min_Cube_t * pCube, * pCube2;
-    int i;
-    for ( i = 0; i <= nSuppSize; i++ )
-    {
-        Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
-        {
-            assert( i == (int)pCube->nLits );
-            *ppTail = pCube; 
-            ppTail = &pCube->pNext;
-            assert( pCube->uData[0] ); // not a bubble
-        }
-    }
-    *ppTail = NULL;
-    return pCov;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorts the cover in the increasing number of literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube, * pCube2;
-    Min_ManClean( p, p->nVars );
-    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
-    {
-        pCube->pNext = p->ppStore[pCube->nLits];
-        p->ppStore[pCube->nLits] = pCube;
-        p->nCubes++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorts the cover in the increasing number of literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
-{
-    Min_Cube_t * pCube;
-    int i, Counter;
-    if ( pCover == NULL )
-        return 0;
-    // clean the cube
-    for ( i = 0; i < (int)pCover->nWords; i++ )
-        p->pTemp->uData[i]  = ~((unsigned)0);
-    // add the bit data
-    Min_CoverForEachCube( pCover, pCube )
-        for ( i = 0; i < (int)pCover->nWords; i++ )
-            p->pTemp->uData[i] &= pCube->uData[i];
-    // count the vars
-    Counter = 0;
-    for ( i = 0; i < (int)pCover->nVars; i++ )
-        Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
-    return Counter;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/xyz/xyzTest.c b/src/temp/xyz/xyzTest.c
deleted file mode 100644
index 38580790..00000000
--- a/src/temp/xyz/xyzTest.c
+++ /dev/null
@@ -1,417 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [xyzTest.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Cover manipulation package.]
-
-  Synopsis    [Testing procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
-{
-    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                                ///
-////////////////////////////////////////////////////////////////////////
-
-