Version abc50910

1 files changed, 170 insertions, 356 deletions

diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 8d16ac8a..e8a0bc87 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -25,36 +25,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node );
-static inline void        Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
-static inline int         Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList );
-
-static void               Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
-
-// iterator through all the cuts of the list
-#define Cut_ListForEachCut( pList, pCut )                 \
-    for ( pCut = pList;                                   \
-          pCut;                                           \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutStop( pList, pCut, pStop )      \
-    for ( pCut = pList;                                   \
-          pCut != pStop;                                  \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutSafe( pList, pCut, pCut2 )      \
-    for ( pCut = pList,                                   \
-          pCut2 = pCut? pCut->pNext: NULL;                \
-          pCut;                                           \
-          pCut = pCut2,                                   \
-          pCut2 = pCut? pCut->pNext: NULL )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
 
   Description []
                
@@ -63,49 +40,96 @@ static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+static inline int Cut_CutCheckDominance( Cut_Cut_t * pDom, Cut_Cut_t * pCut )
 {
-    if ( Node >= p->vCuts->nSize )
-        return NULL;
-    return Vec_PtrEntry( p->vCuts, Node );
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  Synopsis    [Checks containment for one cut.]
 
-  Description []
+  Description [Returns 1 if the cut is removed.]
                
-  SideEffects []
+  SideEffects [May remove other cuts in the set.]
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_Cut_t * pCut )
 {
-    Vec_PtrWriteEntry( p->vCuts, Node, pList );
-}
+    Cut_Cut_t * pTemp, * pTemp2, ** ppTail;
+    int a;
 
-/**Function*************************************************************
-
-  Synopsis    [Sets the trivial cut for the node.]
-
-  Description []
-               
-  SideEffects []
+    // check if this cut is filtered out by smaller cuts
+    for ( a = 2; a <= (int)pCut->nLeaves; a++ )
+    {
+        Cut_ListForEachCut( pSuperList->pHead[a], pTemp )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pTemp, pCut ) )
+            {
+                p->nCutsFilter++;
+                Cut_CutRecycle( p, pCut );
+                return 1;
+            }
+        }
+    }
 
-  SeeAlso     []
+    // filter out other cuts using this one
+    for ( a = pCut->nLeaves + 1; a <= (int)pCut->nVarsMax; a++ )
+    {
+        ppTail = pSuperList->pHead + a;
+        Cut_ListForEachCutSafe( pSuperList->pHead[a], pTemp, pTemp2 )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+            {
+                ppTail = &pTemp->pNext;
+                continue;
+            }
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pCut, pTemp ) )
+            {
+                p->nCutsFilter++;
+                p->nNodeCuts--;
+                // move the head
+                if ( pSuperList->pHead[a] == pTemp )
+                    pSuperList->pHead[a] = pTemp->pNext;
+                // move the tail
+                if ( pSuperList->ppTail[a] == &pTemp->pNext )
+                    pSuperList->ppTail[a] = ppTail;
+                // skip the given cut in the list
+                *ppTail = pTemp->pNext;
+                // recycle pTemp
+                Cut_CutRecycle( p, pTemp );
+            }
+            else
+                ppTail = &pTemp->pNext;
+        }
+        assert( ppTail == pSuperList->ppTail[a] );
+        assert( *ppTail == NULL );
+    }
 
-***********************************************************************/
-void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
-{
-    assert( Cut_NodeReadCuts(p, Node) == NULL );
-    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Deallocates the cuts at the node.]
+  Synopsis    [Filters cuts using dominance.]
 
   Description []
                
@@ -114,31 +138,79 @@ void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pList, * pCut, * pCut2;
-    pList = Cut_NodeReadCuts( p, Node );
-    if ( pList == NULL )
-        return;
-    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
-        Cut_CutRecycle( p, pCut );
-    Cut_NodeWriteCuts( p, Node, NULL );
+static inline void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
+{ 
+    Cut_Cut_t * pListR, ** ppListR = &pListR;
+    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
+    // save the first cut
+    *ppListR = pList, ppListR = &pList->pNext;
+    // try to filter out other cuts
+    pPrev = pList;
+    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
+    {
+        assert( pCut->nLeaves > 1 );
+        // go through all the previous cuts up to pCut
+        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
+        {
+            if ( pDom->nLeaves > pCut->nLeaves )
+                continue;
+            if ( (pDom->uSign & pCut->uSign) != pDom->uSign )
+                continue;
+            if ( Cut_CutCheckDominance( pDom, pCut ) )
+                break;
+        }
+        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
+        {
+            // make sure cuts are connected after removing
+            pPrev->pNext = pCut->pNext;
+            // recycle the cut
+            Cut_CutRecycle( p, pCut );
+        }
+        else // pDom is NOT contained in pCut - save pCut
+        {
+            *ppListR = pCut, ppListR = &pCut->pNext;
+            pPrev = pCut;
+        }
+    }
+    *ppListR = NULL;
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Processes two cuts.]
 
-  Description []
+  Description [Returns 1 if the limit has been reached.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
+static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
 {
+    Cut_Cut_t * pCut;
+    int RetValue;
+    // merge the cuts
+    if ( pCut0->nLeaves >= pCut1->nLeaves )
+        pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
+    else
+        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
+    if ( pCut == NULL )
+        return 0;
+    assert( pCut->nLeaves > 1 );
+    // set the signature
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
+    // check containment
+    RetValue = p->pParams->fFilter && Cut_CutFilterOne( p, pSuperList, pCut );
+    if ( RetValue )
+        return 0;
+    // compute the truth table
+    if ( p->pParams->fTruth )
+        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+    // add to the list
+    Cut_ListAdd( pSuperList, pCut );
+    // return status (0 if okay; 1 if exceeded the limit)
+    return ++p->nNodeCuts == p->pParams->nKeepMax;
 }
 
 /**Function*************************************************************
@@ -159,6 +231,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     int i, Limit = p->pParams->nVarsMax;
     int clk = clock();
     assert( p->pParams->nVarsMax <= 6 );
+
     // start the new list
     Cut_ListStart( &SuperList );
     // get the cut lists of children
@@ -180,27 +253,37 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     // start with the elementary cut
     pTemp0 = Cut_CutCreateTriv( p, Node );
     Cut_ListAdd( &SuperList, pTemp0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList0, pTemp0 )
+    // small by large
+    Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
+    {
+        if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
+            continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList1, pTemp1 )
+    }
+    // small by large
+    Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
     Cut_ListForEachCut( pStop0, pTemp0 )
+    {
+        if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
+            continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
+    }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
     {
         assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit );
+        if ( pTemp0->uSign != pTemp1->uSign )
+            continue;
         for ( i = 0; i < Limit; i++ )
             if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
                 break;
@@ -210,14 +293,13 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
             goto finish;
     }
 finish :
+    if ( p->nNodeCuts == p->pParams->nKeepMax )
+        p->nCutsLimit++;
     // set the list at the node
     Vec_PtrFillExtra( p->vCuts, Node + 1, NULL );
     assert( Cut_NodeReadCuts(p, Node) == NULL );
     pList0 = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Node, pList0 );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
     // consider dropping the fanins cuts
     if ( p->pParams->fDrop )
     {
@@ -227,8 +309,8 @@ finish :
 p->timeMerge += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList0 );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList0 );
 p->timeFilter += clock() - clk;
     p->nNodes++;
     return pList0;
@@ -236,46 +318,6 @@ p->timeFilter += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Processes two cuts.]
-
-  Description [Returns 1 if the limit has been reached.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
-{
-    Cut_Cut_t * pCut;
-    // merge the cuts
-    if ( pCut0->nLeaves >= pCut1->nLeaves )
-        pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
-    else
-        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
-    if ( pCut == NULL )
-        return 0;
-    assert( pCut->nLeaves > 1 );
-    // add the root if sequential
-    if ( p->pParams->fSeq )
-        pCut->pLeaves[pCut->nLeaves] = Root;
-    // check the lookup table
-    if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-    {
-        Cut_CutRecycle( p, pCut );
-        return 0;
-    }
-    // compute the truth table
-    if ( p->pParams->fTruth )
-        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
-    // add to the list
-    Cut_ListAdd( pSuperList, pCut );
-    // return status (0 if okay; 1 if exceeded the limit)
-    return ++p->nCutsNode == p->pParams->nKeepMax;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes the cuts by unioning cuts at a choice node.]
 
   Description []
@@ -299,7 +341,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 
     // remember the root node to save the resulting cuts
     Root = Vec_IntEntry( vNodes, 0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
 
     // collect small cuts first
     Vec_PtrClear( p->vTemp );
@@ -311,6 +353,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         assert( pList );
         // remember the starting point
         pListStart = pList->pNext;
+        pList->pNext = NULL;
         // save or recycle the elementary cut
         if ( i == 0 )
             Cut_ListAdd( &SuperList, pList ), pTop = pList;
@@ -324,20 +367,19 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 Vec_PtrPush( p->vTemp, pCut );
                 break;
             }
-            // check hash tables
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
                 continue;
-            }
             // set the complemented bit by comparing the first cut with the current cut
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
             // add to the list
             Cut_ListAdd( &SuperList, pCut );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts of this node
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle all cuts of other nodes
                 Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
@@ -349,25 +391,25 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 goto finish;
             }
         }
-    }
+    } 
     // collect larger cuts next
     Vec_PtrForEachEntry( p->vTemp, pList, i )
     {
         Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         {
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
                 continue;
-            }
             // set the complemented bit
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
             // add to the list
             Cut_ListAdd( &SuperList, pCut );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle the saved cuts of other nodes
                 Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
@@ -382,244 +424,16 @@ finish :
     assert( Cut_NodeReadCuts(p, Root) == NULL );
     pList = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Root, pList );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
 p->timeUnion += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList );
 p->timeFilter += clock() - clk;
     p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
-{
-    Cut_Cut_t * pCut;
-    // cut allocation
-    pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
-    memset( pCut, 0, sizeof(Cut_Cut_t) );
-    pCut->nVarsMax   = p->pParams->nVarsMax;
-    pCut->fSeq       = p->pParams->fSeq;
-    pCut->fSimul     = p->fSimul;
-    // statistics
-    p->nCutsAlloc++;
-    p->nCutsCur++;
-    if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
-        p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
-    return pCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pCut;
-    pCut = Cut_CutAlloc( p );
-    pCut->nLeaves = 1;
-    pCut->pLeaves[0] = Node;
-    if ( p->pParams->fTruth )
-        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
-    p->nCutsTriv++;
-    return pCut;
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
-{
-    p->nCutsDealloc++;
-    p->nCutsCur--;
-    if ( pCut->nLeaves == 1 )
-        p->nCutsTriv--;
-    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
-{
-    int nFanouts;
-    assert( p->vFanCounts );
-    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
-    assert( nFanouts > 0 );
-    if ( --nFanouts == 0 )
-        Cut_NodeFreeCuts( p, Node );
-    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Print the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrint( Cut_Cut_t * pCut )
-{
-    int i;
-    assert( pCut->nLeaves > 0 );
-    printf( "%d : {", pCut->nLeaves );
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
-    printf( " }" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    printf( "\n" );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut0->nLeaves, 
-        pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, 
-        pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, 
-        pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, 
-        pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, 
-        pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
-        );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut1->nLeaves, 
-        pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, 
-        pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, 
-        pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, 
-        pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, 
-        pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
-        );
-    if ( pCut == NULL )
-        printf( "Cannot merge\n" );
-    else
-        printf( "%d : %5d %5d %5d %5d %5d\n", 
-            pCut->nLeaves, 
-            pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, 
-            pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, 
-            pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, 
-            pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, 
-            pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
-            );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Filter the cuts using dominance.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
-{ 
-    Cut_Cut_t * pListR, ** ppListR = &pListR;
-    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
-    int i, k;
-    // save the first cut
-    *ppListR = pList, ppListR = &pList->pNext;
-    // try to filter out other cuts
-    pPrev = pList;
-    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
-    {
-        assert( pCut->nLeaves > 1 );
-        // go through all the previous cuts up to pCut
-        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
-        {
-            if ( pDom->nLeaves >= pCut->nLeaves )
-                continue;
-            // check if every node in pDom is contained in pCut
-            for ( i = 0; i < (int)pDom->nLeaves; i++ )
-            {
-                for ( k = 0; k < (int)pCut->nLeaves; k++ )
-                    if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                        break;
-                if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-                    break;
-            }
-            if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut
-                break;
-        }
-        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
-        {
-            // make sure cuts are connected after removing
-            pPrev->pNext = pCut->pNext;
-/*
-            // report
-            printf( "Recycling cut:   " );
-            Cut_CutPrint( pCut );
-            printf( "\n" );
-            printf( "As contained in: " );
-            Cut_CutPrint( pDom );
-            printf( "\n" );
-*/
-            // recycle the cut
-            Cut_CutRecycle( p, pCut );
-        }
-        else // pDom is NOT contained in pCut - save pCut
-        {
-            *ppListR = pCut, ppListR = &pCut->pNext;
-            pPrev = pCut;
-        }
-    }
-    *ppListR = NULL;
-}
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///