Version abc50806

11 files changed, 290 insertions, 308 deletions

diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index 37726542..457c2384 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -127,12 +127,19 @@ int Fpga_MappingPostProcess( Fpga_Man_t * p )
     float aSwitchTotalPrev, aSwitchTotalCur;
     int Iter, clk;
 
+
 if ( p->fVerbose )
 {
 printf( "Iteration %dD :  Area = %11.1f  ", 0, Fpga_MappingArea( p ) );
 PRT( "Time", p->timeMatch );
 }
 
+
+//    Fpga_MappingExplore( p );
+//    p->fAreaGlo = Fpga_MappingArea( p );
+//    return;
+
+
 //    aAreaTotalCur = FPGA_FLOAT_LARGE;
     aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
 
@@ -159,6 +166,11 @@ PRT( "Time", clock() - clk );
     } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur );
 
 
+//    Fpga_MappingExplore( p );
+//    p->fAreaGlo = Fpga_MappingArea( p );
+//    return;
+
+
 /*
     // compute the area of each cut
     aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index 0fea9ec8..63308d53 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -334,6 +334,7 @@ extern float             Fpga_TimeComputeArrivalMax( Fpga_Man_t * p );
 extern void              Fpga_TimeComputeRequiredGlobal( Fpga_Man_t * p );
 extern void              Fpga_TimeComputeRequired( Fpga_Man_t * p, float fRequired );
 extern void              Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes );
+extern void              Fpga_TimePropagateArrival( Fpga_Man_t * p );
 /*=== fpgaTruth.c ===============================================================*/
 extern void              Fpga_MappingTruths( Fpga_Man_t * pMan );
 /*=== fpgaVec.c =============================================================*/
@@ -368,6 +369,7 @@ extern float             Fpga_MappingGetAreaFlow( Fpga_Man_t * p );
 extern float             Fpga_MappingArea( Fpga_Man_t * pMan );
 extern float             Fpga_MappingComputeCutAreas( Fpga_Man_t * pMan );
 extern float             Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan );
+extern Fpga_NodeVec_t *  Fpga_MappingCollectRefed( Fpga_Man_t * pMan );
 extern int               Fpga_MappingCountLevels( Fpga_Man_t * pMan );
 extern void              Fpga_MappingUnmark( Fpga_Man_t * pMan );
 extern void              Fpga_MappingUnmark_rec( Fpga_Node_t * pNode );
diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c
index 8668ce4b..599662f7 100644
--- a/src/map/fpga/fpgaMatch.c
+++ b/src/map/fpga/fpgaMatch.c
@@ -724,6 +724,112 @@ clk = clock();
 }
 
 #endif
+
+
+/**function*************************************************************
+
+  synopsis    [Performs area minimization using a heuristic algorithm.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Fpga_FindBestNode( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes, Fpga_Node_t ** ppNode, Fpga_Cut_t ** ppCutBest )
+{
+    Fpga_Node_t * pNode;
+    Fpga_Cut_t * pCut;
+    float Gain, CutArea1, CutArea2, CutArea3;
+    int i;
+
+    Gain = 0;
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        pNode = vNodes->pArray[i];
+        // deref the current cut
+        CutArea1 = Fpga_CutDeref( p, pNode, pNode->pCutBest, 0 );
+
+        // ref all the cuts
+        for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
+        {
+            if ( pCut == pNode->pCutBest )
+                continue;
+            if ( pCut->tArrival > pNode->tRequired )
+                continue;
+
+            CutArea2 = Fpga_CutGetAreaDerefed( p, pCut );
+            if ( Gain < CutArea1 - CutArea2 )
+            {
+                *ppNode = pNode;
+                *ppCutBest = pCut;
+                Gain = CutArea1 - CutArea2;
+            }
+        }
+        // ref the old cut
+        CutArea3 = Fpga_CutRef( p, pNode, pNode->pCutBest, 0 );
+        assert( CutArea1 == CutArea3 );
+    }
+    if ( Gain == 0 )
+        printf( "Returning no gain.\n" );
+
+    return Gain;
+}
+
+/**function*************************************************************
+
+  synopsis    [Performs area minimization using a heuristic algorithm.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+void Fpga_MappingExplore( Fpga_Man_t * p )
+{
+    Fpga_Cut_t * pCutBest;
+    Fpga_Node_t * pNodeBest;
+    Fpga_NodeVec_t * vNodes;
+    float Area, Gain, CutArea1, CutArea2;
+    int i;
+
+    // compute the arrival times
+    Fpga_TimePropagateArrival( p );
+    p->fRequiredGlo = Fpga_TimeComputeArrivalMax( p );
+    Fpga_TimeComputeRequired( p, p->fRequiredGlo );
+
+    // assign the refs
+    Area = Fpga_MappingSetRefsAndArea( p );
+    // collect the nodes
+    vNodes = Fpga_MappingCollectRefed( p );
+    // find the best node to update
+    for ( i = 0; Gain = Fpga_FindBestNode(p, vNodes, &pNodeBest, &pCutBest); i++ )
+    {
+        // update the node
+        assert( pNodeBest->pCutBest != pCutBest );
+        // deref the current cut
+        CutArea1 = Fpga_CutDeref( p, pNodeBest, pNodeBest->pCutBest, 0 );
+        // ref the new cut
+        CutArea2 = Fpga_CutRef( p, pNodeBest, pCutBest, 0 );
+        assert( CutArea1 - CutArea2 == Gain );
+        printf( "Iteration %2d: Gain = %5.2f.\n", i, Gain );
+        // update the node
+        pNodeBest->pCutBest = pCutBest;
+        // collect new nodes
+        Fpga_NodeVecFree( vNodes );
+        vNodes = Fpga_MappingCollectRefed( p );
+        // compute the arrival and required times
+        Fpga_TimePropagateArrival( p );
+        Fpga_TimeComputeRequired( p, p->fRequiredGlo );
+    }
+
+
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpgaTime.c b/src/map/fpga/fpgaTime.c
index df98faa1..066ae215 100644
--- a/src/map/fpga/fpgaTime.c
+++ b/src/map/fpga/fpgaTime.c
@@ -182,6 +182,34 @@ void Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes )
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the required times of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fpga_TimePropagateArrival( Fpga_Man_t * p )
+{
+    Fpga_Node_t * pNode;
+    Fpga_Cut_t * pCut;
+    int i;
+
+    // clean the required times and the fanout counts for all nodes
+    for ( i = 0; i < p->vAnds->nSize; i++ )
+    {
+        pNode = p->vAnds->pArray[i];
+        for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
+            pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c
index a5b2cb32..fc67d52b 100644
--- a/src/map/fpga/fpgaUtils.c
+++ b/src/map/fpga/fpgaUtils.c
@@ -493,6 +493,32 @@ float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Collect the referenced nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fpga_NodeVec_t * Fpga_MappingCollectRefed( Fpga_Man_t * pMan )
+{
+    Fpga_NodeVec_t * vNodes;
+    int i;
+    vNodes = Fpga_NodeVecAlloc( 100 );
+    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
+    {
+        if ( Fpga_NodeIsVar(pMan->vNodesAll->pArray[i]) )
+            continue;
+        if ( pMan->vNodesAll->pArray[i]->nRefs )
+            Fpga_NodeVecPush( vNodes, pMan->vNodesAll->pArray[i] );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
   Description []
diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index a6bfccf8..9ef8ee17 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -82,6 +82,8 @@ extern Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p );
 extern Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p );
 extern Mio_Library_t * Map_ManReadGenLib ( Map_Man_t * p );
 extern bool            Map_ManReadVerbose( Map_Man_t * p );
+extern float           Map_ManReadAreaFinal( Map_Man_t * p );
+extern float           Map_ManReadRequiredGlo( Map_Man_t * p );
 extern void            Map_ManSetTimeToMap( Map_Man_t * p, int Time );
 extern void            Map_ManSetTimeToNet( Map_Man_t * p, int Time );
 extern void            Map_ManSetTimeSweep( Map_Man_t * p, int Time );
@@ -125,6 +127,7 @@ extern Map_Node_t **   Map_CutReadLeaves( Map_Cut_t * p );
 extern unsigned        Map_CutReadPhaseBest( Map_Cut_t * p, int fPhase );
 extern unsigned        Map_CutReadPhase0( Map_Cut_t * p );
 extern unsigned        Map_CutReadPhase1( Map_Cut_t * p );
+extern Map_Cut_t *     Map_CutReadNext( Map_Cut_t * p );
 
 extern char *          Map_SuperReadFormula( Map_Super_t * p );
 extern Mio_Gate_t *    Map_SuperReadRoot( Map_Super_t * p );
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index 415e4974..e72b9134 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -82,8 +82,8 @@ int Map_Mapping( Map_Man_t * p )
     p->AreaBase = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Delay    : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
+printf( "Delay    : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
 PRT( "Time", p->timeMatch );
 }
     //////////////////////////////////////////////////////////////////////
@@ -103,8 +103,8 @@ PRT( "Time", p->timeMatch );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "AreaFlow : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, Map_MappingGetAreaFlow(p), p->AreaFinal, 
+printf( "AreaFlow : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }
@@ -127,8 +127,8 @@ PRT( "Time", clock() - clk );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Area     : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, 0.0, p->AreaFinal, 
+printf( "Area     : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, 0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }
@@ -151,8 +151,8 @@ PRT( "Time", clock() - clk );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Area     : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, 0.0, p->AreaFinal, 
+printf( "Area     : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, 0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }
diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c
index 61c90d1c..4d7ca7d0 100644
--- a/src/map/mapper/mapperCreate.c
+++ b/src/map/mapper/mapperCreate.c
@@ -52,6 +52,8 @@ Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p )                     { return
 Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p )               { return p->pInputArrivals;}
 Mio_Library_t * Map_ManReadGenLib ( Map_Man_t * p )                     { return p->pSuperLib->pGenlib; }
 bool            Map_ManReadVerbose( Map_Man_t * p )                     { return p->fVerbose;   }
+float           Map_ManReadAreaFinal( Map_Man_t * p )                   { return p->AreaFinal;  }
+float           Map_ManReadRequiredGlo( Map_Man_t * p )                 { return p->fRequiredGlo;  }
 void            Map_ManSetTimeToMap( Map_Man_t * p, int Time )          { p->timeToMap = Time;  }
 void            Map_ManSetTimeToNet( Map_Man_t * p, int Time )          { p->timeToNet = Time;  }
 void            Map_ManSetTimeSweep( Map_Man_t * p, int Time )          { p->timeSweep = Time;  }
@@ -126,6 +128,7 @@ Map_Node_t **   Map_CutReadLeaves( Map_Cut_t * p )                { return p->pp
 unsigned        Map_CutReadPhaseBest( Map_Cut_t * p, int fPhase ) { return p->M[fPhase].uPhaseBest;}
 unsigned        Map_CutReadPhase0( Map_Cut_t * p )                { return p->M[0].uPhaseBest;}
 unsigned        Map_CutReadPhase1( Map_Cut_t * p )                { return p->M[1].uPhaseBest;}
+Map_Cut_t *     Map_CutReadNext( Map_Cut_t * p )                  { return p->pNext;          }
 
 /**Function*************************************************************
 
@@ -190,7 +193,8 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->pSuperLib = Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame());
     p->nVarsMax  = p->pSuperLib->nVarsMax;
     p->fVerbose  = fVerbose;
-    p->fEpsilon  = (float)0.00001;
+//    p->fEpsilon  = (float)0.00001;
+    p->fEpsilon  = (float)0.001;
     assert( p->nVarsMax > 0 );
 
     // start various data structures
@@ -210,6 +214,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->vMapping   = Map_NodeVecAlloc( 100 );
     p->vInside    = Map_NodeVecAlloc( 100 );
     p->vFanins    = Map_NodeVecAlloc( 100 );
+    p->vVisited   = Map_NodeVecAlloc( 100 );
 
     // create the PI nodes
     p->nInputs = nInputs;
@@ -253,6 +258,8 @@ void Map_ManFree( Map_Man_t * p )
         Map_NodeVecFree( p->vNodesTemp );
     if ( p->vMapping )    
         Map_NodeVecFree( p->vMapping );
+    if ( p->vVisited )    
+        Map_NodeVecFree( p->vVisited );
     Extra_MmFixedStop( p->mmNodes, 0 );
     Extra_MmFixedStop( p->mmCuts, 0 );
     FREE( p->pInputArrivals );
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 87592365..8566c819 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -23,9 +23,9 @@
 ////////////////////////////////////////////////////////////////////////
 
 // the largest number of cuts considered
-#define  MAP_CUTS_MAX_COMPUTE   200
+#define  MAP_CUTS_MAX_COMPUTE   1000
 // the largest number of cuts used
-#define  MAP_CUTS_MAX_USE       50
+#define  MAP_CUTS_MAX_USE       250
 
 // temporary hash table to store the cuts
 typedef struct Map_CutTableStrutct_t Map_CutTable_t;
@@ -373,6 +373,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[i];
             pTemp2 = ppArray2[k];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )
@@ -397,6 +405,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[k];
             pTemp2 = ppArray2[i];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )
@@ -424,6 +440,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[k];
             pTemp2 = ppArray2[i];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index c5ecce73..d4262abb 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -121,6 +121,7 @@ struct Map_ManStruct_t_
     unsigned            uTruthsLarge[10][32]; // the elementary truth tables
     int                 nCounts[32];   // the counter of minterms
     int                 nCountsBest[32];// the counter of minterms
+    Map_NodeVec_t *     vVisited;      // the visited cuts during cut computation
 
     // simulation info from the FRAIG manager
     int                 nSimRounds;    // the number of words in the simulation info
@@ -262,13 +263,7 @@ struct Map_CutStruct_t_
     char                nVolume;       // the volume of this cut
     char                fMark;         // the mark to denote visited cut
     char                Phase;         // the mark to denote complemented cut
-//    float               fLevel;        // the average level of the fanins
-
-    unsigned            uTruthTemp[2]; // the temporary truth table used to derive other cuts
-    unsigned            uTruthZero[2]; // the temporary truth table used to derive other cuts
-    unsigned            uTruthDc[2];   // the don't-cares (SDCs) computed for this cut
-
-    Map_Match_t         M[2];          // the matches for the positive/negative phase
+    Map_Match_t         M[2];          // the matches for positive/negative phase
 };
 
 // the supergate internally represented
diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c
index 9388b42f..67ef029b 100644
--- a/src/map/mapper/mapperTruth.c
+++ b/src/map/mapper/mapperTruth.c
@@ -22,20 +22,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-//static void  Map_TruthsCutDcs( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] );
-static void  Map_TruthsCut( Map_Man_t * pMan, Map_Cut_t * pCut );
-static void  Map_TruthsCut_rec( Map_Cut_t * pCut, unsigned uTruth[] );
-static void  Map_TruthsUnmark_rec( Map_Cut_t * pCut );
-
-/*
-static int s_Same = 0;
-static int s_Diff = 0;
-static int s_Same2 = 0;
-static int s_Diff2 = 0;
-static int s_Truth = 0;
-static int s_Isop1 = 0;
-static int s_Isop2 = 0;
-*/
+static void Map_TruthsCut( Map_Man_t * pMan, Map_Cut_t * pCut );
+static void Map_TruthsCutOne( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] );
+static void Map_CutsCollect_rec( Map_Cut_t * pCut, Map_NodeVec_t * vVisited );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -85,10 +75,6 @@ void Map_MappingTruths( Map_Man_t * pMan )
         Extra_ProgressBarUpdate( pProgress, i, "Tables ..." );
     }
     Extra_ProgressBarStop( pProgress );
-
-//    printf( "Same  = %6d. Diff  = %6d.\n", s_Same, s_Diff );
-//    printf( "Same2 = %6d. Diff2 = %6d.\n", s_Same2, s_Diff2 );
-//    printf( "Truth = %6d. Isop1 = %6d. Isop2 = %6d.\n", s_Truth, s_Isop1, s_Isop2 );
 }
 
 /**Function*************************************************************
@@ -106,22 +92,11 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
 {
     unsigned uTruth[2], uCanon[2];
     unsigned char uPhases[16];
-    int i;
 
     // generally speaking, 1-input cut can be matched into a wire!
     if ( pCut->nLeaves == 1 )
         return;
-    // set the leaf truth tables
-    for ( i = 0; i < pCut->nLeaves; i++ )
-    {
-        pCut->ppLeaves[i]->pCuts->uTruthTemp[0] = p->uTruths[i][0];
-        pCut->ppLeaves[i]->pCuts->uTruthTemp[1] = p->uTruths[i][1];
-    }
-    // recursively compute the truth table
-    pCut->nVolume = 0;
-    Map_TruthsCut_rec( pCut, uTruth );
-    // recursively unmark the visited cuts
-    Map_TruthsUnmark_rec( pCut );
+    Map_TruthsCutOne( p, pCut, uTruth );
 
     // compute the canonical form for the positive phase
     Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
@@ -140,15 +115,11 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
     // restore the truth table
     uTruth[0] = ~uTruth[0];
     uTruth[1] = ~uTruth[1];
-    // enable don't-care computation
-//    Map_TruthsCutDcs( p, pCut, uTruth );
 }
 
-#if 0
-
 /**Function*************************************************************
 
-  Synopsis    [Adds several other choices using SDCs.]
+  Synopsis    [Computes the truth table of one cut.]
 
   Description []
                
@@ -157,141 +128,79 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void Map_TruthsCutDcs( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] )
+void Map_TruthsCutOne( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] )
 {
-    unsigned uIsop1[2], uIsop2[2], uCanon[2];
-    unsigned char uPhases[16];
+    unsigned uTruth1[2], uTruth2[2];
+    Map_Cut_t * pTemp;
+    int i;
+    // mark the cut leaves
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pTemp = pCut->ppLeaves[i]->pCuts;
+        pTemp->fMark = 1;
+        pTemp->M[0].uPhaseBest = p->uTruths[i][0];
+        pTemp->M[1].uPhaseBest = p->uTruths[i][1];
+    }
+    assert( pCut->fMark == 0 );
 
-    // add several other supergate classes derived using don't-cares
-    if ( pCut->uTruthDc[0] )
+    // collect the cuts in the cut cone
+    p->vVisited->nSize = 0;
+    Map_CutsCollect_rec( pCut, p->vVisited );
+    assert( p->vVisited->nSize > 0 );
+    pCut->nVolume = p->vVisited->nSize;
+
+    // compute the tables and unmark
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pTemp = pCut->ppLeaves[i]->pCuts;
+        pTemp->fMark = 0;
+    }
+    for ( i = 0; i < p->vVisited->nSize; i++ )
     {
-        int nOnes;
-        nOnes = Map_TruthCountOnes( pCut->uTruthDc, pCut->nLeaves );
-        if ( nOnes == 1 )
+        // get the cut
+        pTemp = (Map_Cut_t *)p->vVisited->pArray[i];
+        pTemp->fMark = 0;
+        // get truth table of the first branch
+        if ( Map_CutIsComplement(pTemp->pOne) )
+        {
+            uTruth1[0] = ~Map_CutRegular(pTemp->pOne)->M[0].uPhaseBest;
+            uTruth1[1] = ~Map_CutRegular(pTemp->pOne)->M[1].uPhaseBest;
+        }
+        else
+        {
+            uTruth1[0] = Map_CutRegular(pTemp->pOne)->M[0].uPhaseBest;
+            uTruth1[1] = Map_CutRegular(pTemp->pOne)->M[1].uPhaseBest;
+        }
+        // get truth table of the second branch
+        if ( Map_CutIsComplement(pTemp->pTwo) )
+        {
+            uTruth2[0] = ~Map_CutRegular(pTemp->pTwo)->M[0].uPhaseBest;
+            uTruth2[1] = ~Map_CutRegular(pTemp->pTwo)->M[1].uPhaseBest;
+        }
+        else
         {
-            uTruth[0] ^= pCut->uTruthDc[0];
-            uTruth[1] ^= pCut->uTruthDc[1];
-
-            // compute the canonical form for the positive phase
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[1].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // compute the canonical form for the negative phase
-            uTruth[0] = ~uTruth[0];
-            uTruth[1] = ~uTruth[1];
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[0].uPhase  = uPhases[0];
-            p->nCanons++;
+            uTruth2[0] = Map_CutRegular(pTemp->pTwo)->M[0].uPhaseBest;
+            uTruth2[1] = Map_CutRegular(pTemp->pTwo)->M[1].uPhaseBest;
         }
-        else if ( nOnes == 2 )
+        // get the truth table of the output
+        if ( !pTemp->Phase )
         {
-            int Num1, Num2, RetValue;
-            RetValue = Map_TruthDetectTwoFirst( pCut->uTruthDc, pCut->nLeaves );
-            Num1 =  RetValue & 255;
-            Num2 = (RetValue >> 8) & 255;
-
-            // add the first bit
-            Map_InfoFlipVar( uTruth, Num1 );
-
-            // compute the canonical form for the positive phase
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[1].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // compute the canonical form for the negative phase
-            uTruth[0] = ~uTruth[0];
-            uTruth[1] = ~uTruth[1];
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[0].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // add the first bit
-            Map_InfoFlipVar( uTruth, Num2 );
-
-            // compute the canonical form for the positive phase
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[1].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // compute the canonical form for the negative phase
-            uTruth[0] = ~uTruth[0];
-            uTruth[1] = ~uTruth[1];
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[0].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // add the first bit
-            Map_InfoFlipVar( uTruth, Num1 );
-
-            // compute the canonical form for the positive phase
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[1].uPhase  = uPhases[0];
-            p->nCanons++;
-
-            // compute the canonical form for the negative phase
-            uTruth[0] = ~uTruth[0];
-            uTruth[1] = ~uTruth[1];
-            Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
-            pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-            pCut->M[0].uPhase  = uPhases[0];
-            p->nCanons++;
+            pTemp->M[0].uPhaseBest = uTruth1[0] & uTruth2[0];
+            pTemp->M[1].uPhaseBest = uTruth1[1] & uTruth2[1];
         }
         else
         {
-            // compute the ISOPs
-            uIsop1[0] = Map_ComputeIsop_rec( p, uTruth[0] & ~pCut->uTruthDc[0], uTruth[0] | pCut->uTruthDc[0], 0, pCut->nLeaves, 0 );
-            uIsop1[1] = uIsop1[0];
-            if ( uIsop1[0] != uTruth[0] )
-            {
-                // compute the canonical form for the positive phase
-                Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uIsop1, uPhases, uCanon );
-                pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-                pCut->M[1].uPhase  = uPhases[0];
-                p->nCanons++;
-
-                // compute the canonical form for the negative phase
-                uIsop1[0] = ~uIsop1[0];
-                uIsop1[1] = ~uIsop1[1];
-                Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uIsop1, uPhases, uCanon );
-                pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-                pCut->M[0].uPhase  = uPhases[0];
-                p->nCanons++;
-            }
-
-            uIsop2[0] = Map_ComputeIsop_rec( p, uTruth[0] & ~pCut->uTruthDc[0], uTruth[0] | pCut->uTruthDc[0], pCut->nLeaves-1, pCut->nLeaves, 1 );
-            uIsop2[1] = uIsop2[0];
-            if ( uIsop2[0] != uTruth[0] && uIsop2[0] != uIsop1[0] )
-            {
-                // compute the canonical form for the positive phase
-                Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uIsop2, uPhases, uCanon );
-                pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-                p->nCanons++;
-
-                // compute the canonical form for the negative phase
-                uIsop2[0] = ~uIsop2[0];
-                uIsop2[1] = ~uIsop2[1];
-                Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uIsop2, uPhases, uCanon );
-                pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
-                pCut->M[0].uPhase  = uPhases[0];
-                p->nCanons++;
-            }
+            pTemp->M[0].uPhaseBest = ~(uTruth1[0] & uTruth2[0]);
+            pTemp->M[1].uPhaseBest = ~(uTruth1[1] & uTruth2[1]);
         }
     }
+    uTruth[0] = pTemp->M[0].uPhaseBest;
+    uTruth[1] = pTemp->M[1].uPhaseBest;
 }
 
-#endif
-
 /**Function*************************************************************
 
-  Synopsis    [Recursively derives the truth table for the cut.]
+  Synopsis    [Recursively collect the cuts.]
 
   Description []
                
@@ -300,147 +209,17 @@ void Map_TruthsCutDcs( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] )
   SeeAlso     []
 
 ***********************************************************************/
-void Map_TruthsCut_rec( Map_Cut_t * pCut, unsigned uTruthRes[] )
+void Map_CutsCollect_rec( Map_Cut_t * pCut, Map_NodeVec_t * vVisited )
 {
-    unsigned uTruth1[2], uTruth2[2];
-    // if this is the elementary cut, its truth table is already available
-    if ( pCut->nLeaves == 1 )
-    {
-        uTruthRes[0] = pCut->uTruthTemp[0];
-        uTruthRes[1] = pCut->uTruthTemp[1];
-        return;
-    }
-    // if this node was already visited, return its computed truth table
     if ( pCut->fMark )
-    {
-        uTruthRes[0] = pCut->uTruthTemp[0];
-        uTruthRes[1] = pCut->uTruthTemp[1];
         return;
-    }
+    Map_CutsCollect_rec( Map_CutRegular(pCut->pOne), vVisited );
+    Map_CutsCollect_rec( Map_CutRegular(pCut->pTwo), vVisited );
+    assert( pCut->fMark == 0 );
     pCut->fMark = 1;
-    pCut->nVolume++;
-
-    assert( !Map_IsComplement(pCut) );
-    Map_TruthsCut_rec( Map_CutRegular(pCut->pOne), uTruth1 );
-    if ( Map_CutIsComplement(pCut->pOne) )
-    {
-        uTruth1[0] = ~uTruth1[0];
-        uTruth1[1] = ~uTruth1[1];
-    }
-    Map_TruthsCut_rec( Map_CutRegular(pCut->pTwo), uTruth2 );
-    if ( Map_CutIsComplement(pCut->pTwo) )
-    {
-        uTruth2[0] = ~uTruth2[0];
-        uTruth2[1] = ~uTruth2[1];
-    }
-    if ( !pCut->Phase )
-    {
-        uTruthRes[0] = pCut->uTruthTemp[0] = uTruth1[0] & uTruth2[0];
-        uTruthRes[1] = pCut->uTruthTemp[1] = uTruth1[1] & uTruth2[1];
-    }
-    else
-    {
-        uTruthRes[0] = pCut->uTruthTemp[0] = ~(uTruth1[0] & uTruth2[0]);
-        uTruthRes[1] = pCut->uTruthTemp[1] = ~(uTruth1[1] & uTruth2[1]);
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively derives the truth table for the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_TruthsUnmark_rec( Map_Cut_t * pCut )
-{
-    if ( pCut->nLeaves == 1 )
-        return;
-    // if this node was already visited, return its computed truth table
-    if ( pCut->fMark == 0 )
-        return;
-    pCut->fMark = 0;
-    Map_TruthsUnmark_rec( Map_CutRegular(pCut->pOne) );
-    Map_TruthsUnmark_rec( Map_CutRegular(pCut->pTwo) );
+    Map_NodeVecPush( vVisited, (Map_Node_t *)pCut );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Returns the truth table of the don't-care set.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Map_TruthsCutDontCare( Map_Man_t * pMan, Map_Cut_t * pCut, unsigned * uTruthDc )
-{
-    if ( pCut->pOne || (pCut->uTruthZero[0] == 0 && pCut->uTruthZero[1] == 0) )
-        return 0;
-    assert( (pCut->uTruthTemp[0] & pCut->uTruthZero[0]) == 0 );
-    assert( (pCut->uTruthTemp[1] & pCut->uTruthZero[1]) == 0 );
-    uTruthDc[0] = ((~0) & (~pCut->uTruthTemp[0]) & (~pCut->uTruthZero[0]));
-    uTruthDc[1] = ((~0) & (~pCut->uTruthTemp[1]) & (~pCut->uTruthZero[1]));
-    if ( uTruthDc[0] == 0 && uTruthDc[1] == 0 )
-        return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Expand the truth table]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Map_TruthCountOnes( unsigned * uTruth, int nLeaves )
-{
-    int i, nMints, Counter;
-    nMints = (1 << nLeaves);
-    Counter = 0;
-    for ( i = 0; i < nMints; i++ )
-        Counter += Map_InfoReadVar( uTruth, i );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Expand the truth table]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Map_TruthDetectTwoFirst( unsigned * uTruth, int nLeaves )
-{
-    int i, nMints, Num1 = -1, Num2 = -1;
-    nMints = (1 << nLeaves);
-    for ( i = 0; i < nMints; i++ )
-        if ( Map_InfoReadVar( uTruth, i ) )
-        {
-            if ( Num1 == -1 )
-                Num1 = i;
-            else if ( Num2 == -1 )
-                Num2 = i;
-            else
-                break;
-        }
-    assert( Num1 != -1 && Num2 != -1 );
-    return (Num1 << 8) | Num2;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///