Version abc50729

1 files changed, 1254 insertions, 0 deletions

diff --git a/src/map/mapper/mapperUtils.c b/src/map/mapper/mapperUtils.c
new file mode 100644
index 00000000..f8fd1a4c
--- /dev/null
+++ b/src/map/mapper/mapperUtils.c
@@ -0,0 +1,1254 @@
+/**CFile****************************************************************
+
+  FileName    [mapperUtils.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Generic technology mapping engine.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - June 1, 2004.]
+
+  Revision    [$Id: mapperUtils.c,v 1.8 2004/11/03 22:41:45 satrajit Exp $]
+
+***********************************************************************/
+
+#include "mapperInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void  Map_MappingDfs_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fCollectEquiv );
+static int   Map_MappingCountLevels_rec( Map_Node_t * pNode );
+static float Map_MappingSetRefsAndArea_rec( Map_Man_t * pMan, Map_Node_t * pNode );
+static float Map_MappingSetRefsAndSwitch_rec( Map_Man_t * pMan, Map_Node_t * pNode );
+static float Map_MappingSetRefsAndWire_rec( Map_Man_t * pMan, Map_Node_t * pNode );
+static void  Map_MappingDfsCuts_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes );
+static float Map_MappingArea_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_NodeVec_t * vNodes );
+static int   Map_MappingCompareOutputDelay( int * pOut1, int * pOut2 );
+static unsigned Map_MappingExpandTruth_rec( unsigned uTruth, int nVars );
+static void Map_MappingGetChoiceLevels( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2, int * pMin, int * pMax );
+static float Map_MappingGetChoiceVolumes( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 );
+static int Map_MappingCountUsedNodes( Map_Man_t * pMan, int fChoices );
+static Map_Man_t * s_pMan = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Map_NodeVec_t * Map_MappingDfs( Map_Man_t * pMan, int fCollectEquiv )
+{
+    Map_NodeVec_t * vNodes;
+    int i;
+    // perform the traversal
+    vNodes = Map_NodeVecAlloc( 100 );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingDfs_rec( Map_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        vNodes->pArray[i]->fMark0 = 0;
+//    for ( i = 0; i < pMan->nOutputs; i++ )
+//        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Map_NodeVec_t * Map_MappingDfsNodes( Map_Man_t * pMan, Map_Node_t ** ppCuts, int nNodes, int fEquiv )
+{
+    Map_NodeVec_t * vNodes;
+    int i;
+    // perform the traversal
+    vNodes = Map_NodeVecAlloc( 200 );
+    for ( i = 0; i < nNodes; i++ )
+        Map_MappingDfs_rec( ppCuts[i], vNodes, fEquiv );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        vNodes->pArray[i]->fMark0 = 0;
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingDfs_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fCollectEquiv )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark0 )
+        return;
+    // visit the transitive fanin
+    if ( Map_NodeIsAnd(pNode) )
+    {
+        Map_MappingDfs_rec( Map_Regular(pNode->p1), vNodes, fCollectEquiv );
+        Map_MappingDfs_rec( Map_Regular(pNode->p2), vNodes, fCollectEquiv );
+    }
+    // visit the equivalent nodes
+    if ( fCollectEquiv && pNode->pNextE )
+        Map_MappingDfs_rec( pNode->pNextE, vNodes, fCollectEquiv );
+    // make sure the node is not visited through the equivalent nodes
+    assert( pNode->fMark0 == 0 );
+    // mark the node as visited
+    pNode->fMark0 = 1;
+    // add the node to the list
+    Map_NodeVecPush( vNodes, pNode );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingDfsMarked1_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fFirst )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark0 )
+        return;
+    // visit the transitive fanin
+    if ( Map_NodeIsAnd(pNode) )
+    {
+        Map_MappingDfsMarked1_rec( Map_Regular(pNode->p1), vNodes, 0 );
+        Map_MappingDfsMarked1_rec( Map_Regular(pNode->p2), vNodes, 0 );
+    }
+    // visit the equivalent nodes
+    if ( !fFirst && pNode->pNextE )
+        Map_MappingDfsMarked1_rec( pNode->pNextE, vNodes, 0 );
+    // make sure the node is not visited through the equivalent nodes
+    assert( pNode->fMark0 == 0 );
+    // mark the node as visited
+    pNode->fMark0 = 1;
+    // add the node to the list
+    Map_NodeVecPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingDfsMarked2_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, Map_NodeVec_t * vBoundary, int fFirst )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark1 )
+        return;
+    if ( pNode->fMark0 || Map_NodeIsVar(pNode) )
+    {
+        pNode->fMark1 = 1;
+        Map_NodeVecPush(vBoundary, pNode);
+        return;
+    }
+    // visit the transitive fanin
+    if ( Map_NodeIsAnd(pNode) )
+    {
+        Map_MappingDfsMarked2_rec( Map_Regular(pNode->p1), vNodes, vBoundary, 0 );
+        Map_MappingDfsMarked2_rec( Map_Regular(pNode->p2), vNodes, vBoundary, 0 );
+    }
+    // visit the equivalent nodes
+    if ( !fFirst && pNode->pNextE )
+        Map_MappingDfsMarked2_rec( pNode->pNextE, vNodes, vBoundary, 0 );
+    // make sure the node is not visited through the equivalent nodes
+    assert( pNode->fMark1 == 0 );
+    // mark the node as visited
+    pNode->fMark1 = 1;
+    // add the node to the list
+    Map_NodeVecPush( vNodes, pNode );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingDfsMarked3_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark0 )
+        return;
+    // visit the transitive fanin
+    if ( Map_NodeIsAnd(pNode) )
+    {
+        Map_MappingDfsMarked3_rec( Map_Regular(pNode->p1), vNodes );
+        Map_MappingDfsMarked3_rec( Map_Regular(pNode->p2), vNodes );
+    }
+    // make sure the node is not visited through the equivalent nodes
+    assert( pNode->fMark0 == 0 );
+    // mark the node as visited
+    pNode->fMark0 = 1;
+    // add the node to the list
+    Map_NodeVecPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingDfsMarked4_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark1 )
+        return;
+    // visit the transitive fanin
+    if ( Map_NodeIsAnd(pNode) )
+    {
+        Map_MappingDfsMarked4_rec( Map_Regular(pNode->p1), vNodes );
+        Map_MappingDfsMarked4_rec( Map_Regular(pNode->p2), vNodes );
+    }
+    // make sure the node is not visited through the equivalent nodes
+    assert( pNode->fMark1 == 0 );
+    // mark the node as visited
+    pNode->fMark1 = 1;
+    // add the node to the list
+    Map_NodeVecPush( vNodes, pNode );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description []
+               
+  SideEffects [Note that this procedure will reassign the levels assigned
+  originally by NodeCreate() because it counts the number of levels with 
+  choices differently!]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCountLevels( Map_Man_t * pMan )
+{
+    int i, LevelsMax, LevelsCur;
+    // perform the traversal
+    LevelsMax = -1;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+    {
+        LevelsCur = Map_MappingCountLevels_rec( Map_Regular(pMan->pOutputs[i]) );
+        if ( LevelsMax < LevelsCur )
+            LevelsMax = LevelsCur;
+    }
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
+    return LevelsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the number of logic levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCountLevels_rec( Map_Node_t * pNode )
+{
+    int Level1, Level2;
+    assert( !Map_IsComplement(pNode) );
+    if ( !Map_NodeIsAnd(pNode) )
+    {
+        pNode->Level = 0;
+        return 0;
+    }
+    if ( pNode->fMark0 )
+        return pNode->Level;
+    pNode->fMark0 = 1;
+    // visit the transitive fanin
+    Level1 = Map_MappingCountLevels_rec( Map_Regular(pNode->p1) );
+    Level2 = Map_MappingCountLevels_rec( Map_Regular(pNode->p2) );
+    // set the number of levels
+    pNode->Level = 1 + ((Level1>Level2)? Level1: Level2);
+    return pNode->Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingUnmark( Map_Man_t * pMan )
+{
+    int i;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively unmarks the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingUnmark_rec( Map_Node_t * pNode )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark0 == 0 )
+        return;
+    pNode->fMark0 = 0;
+    if ( !Map_NodeIsAnd(pNode) )
+        return;
+    Map_MappingUnmark_rec( Map_Regular(pNode->p1) );
+    Map_MappingUnmark_rec( Map_Regular(pNode->p2) );
+    // visit the equivalent nodes
+    if ( pNode->pNextE )
+        Map_MappingUnmark_rec( pNode->pNextE );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingMark_rec( Map_Node_t * pNode )
+{
+    assert( !Map_IsComplement(pNode) );
+    if ( pNode->fMark0 == 1 )
+        return;
+    pNode->fMark0 = 1;
+    if ( !Map_NodeIsAnd(pNode) )
+        return;
+    // visit the transitive fanin of the selected cut
+    Map_MappingMark_rec( Map_Regular(pNode->p1) );
+    Map_MappingMark_rec( Map_Regular(pNode->p2) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints a bunch of latest arriving outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingPrintOutputArrivals( Map_Man_t * p )
+{
+    Map_Time_t * pTimes;
+    Map_Node_t * pNode;
+    int fPhase, Limit, i;
+    int nOutputs;
+    int * pSorted;
+
+    // sort outputs by arrival time
+    s_pMan = p;
+    pSorted = ALLOC( int, p->nOutputs );
+    nOutputs = 0;
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        if ( Map_NodeIsConst(p->pOutputs[i]) )
+            continue;
+        pSorted[nOutputs++] = i;        
+    }
+    qsort( (void *)pSorted, nOutputs, sizeof(int), 
+            (int (*)(const void *, const void *)) Map_MappingCompareOutputDelay );
+    assert( Map_MappingCompareOutputDelay( pSorted, pSorted + nOutputs - 1 ) <= 0 );
+    s_pMan = NULL;
+
+    // print the latest outputs
+    Limit = (nOutputs > 5)? 5 : nOutputs;
+    for ( i = 0; i < Limit; i++ )
+    {
+        // get the i-th latest output
+        pNode  = Map_Regular(p->pOutputs[pSorted[i]]);
+        fPhase =!Map_IsComplement(p->pOutputs[pSorted[i]]);
+        pTimes = pNode->tArrival + fPhase;
+        // print out the best arrival time
+        printf( "Out  %20s : ", p->ppOutputNames[pSorted[i]] );
+        printf( "Delay = (%5.2f, %5.2f)  ", (double)pTimes->Rise, (double)pTimes->Fall );
+        printf( "%s", fPhase? "POS" : "NEG" );
+        printf( "\n" );
+    }
+    free( pSorted );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the outputs by their arrival times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCompareOutputDelay( int * pOut1, int * pOut2 )
+{
+    Map_Node_t * pNode1 = Map_Regular(s_pMan->pOutputs[*pOut1]);
+    Map_Node_t * pNode2 = Map_Regular(s_pMan->pOutputs[*pOut2]);
+    int fPhase1 = (pNode1 == s_pMan->pOutputs[*pOut1]);
+    int fPhase2 = (pNode2 == s_pMan->pOutputs[*pOut2]);
+    float Arrival1 = pNode1->tArrival[fPhase1].Worst;
+    float Arrival2 = pNode2->tArrival[fPhase2].Worst;
+    if ( Arrival1 > Arrival2 )
+        return -1;
+    if ( Arrival1 < Arrival2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingSetupTruthTables( unsigned uTruths[][2] )
+{
+    int m, v;
+    // set up the truth tables
+    for ( m = 0; m < 32; m++ )
+        for ( v = 0; v < 5; v++ )
+            if ( m & (1 << v) )
+                uTruths[v][0] |= (1 << m);
+    // make adjustments for the case of 6 variables
+    for ( v = 0; v < 5; v++ )
+        uTruths[v][1] = uTruths[v][0];
+    uTruths[5][0] = 0;
+    uTruths[5][1] = MAP_FULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingSetupTruthTablesLarge( unsigned uTruths[][32] )
+{
+    int m, v;
+    // clean everything
+    for ( m = 0; m < 32; m++ )
+        for ( v = 0; v < 10; v++ )
+            uTruths[v][m] = 0;
+    // set up the truth tables
+    for ( m = 0; m < 32; m++ )
+        for ( v = 0; v < 5; v++ )
+            if ( m & (1 << v) )
+            {
+                uTruths[v][0] |= (1 << m);
+                uTruths[v+5][m] = MAP_FULL;
+            }
+    // extend this info for the rest of the first 5 variables
+    for ( m = 0; m < 32; m++ )
+        for ( v = 0; v < 5; v++ )
+            uTruths[v][m] = uTruths[v][0];
+/*
+    // verify
+    for ( m = 0; m < 1024; m++, printf("\n") )
+        for ( v = 0; v < 10; v++ )
+            if ( Map_InfoReadVar( uTruths[v], m ) )
+                printf( "1" );
+            else
+                printf( "0" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the mask.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingSetupMask( unsigned uMask[], int nVarsMax )
+{
+    if ( nVarsMax == 6 )
+        uMask[0] = uMask[1] = MAP_FULL;
+    else
+    {
+        uMask[0] = MAP_MASK(1 << nVarsMax);
+        uMask[1] = 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify one useful property.]
+
+  Description [This procedure verifies one useful property. After 
+  the FRAIG construction with choice nodes is over, each primary node 
+  should have fanins that are primary nodes. The primary nodes is the 
+  one that does not have pNode->pRepr set to point to another node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_ManCheckConsistency( Map_Man_t * p )
+{
+    Map_Node_t * pNode;
+    Map_NodeVec_t * pVec;
+    int i;
+    pVec = Map_MappingDfs( p, 0 );
+    for ( i = 0; i < pVec->nSize; i++ )
+    {
+        pNode = pVec->pArray[i];
+        if ( Map_NodeIsVar(pNode) )
+        {
+            if ( pNode->pRepr )
+                printf( "Primary input %d is a secondary node.\n", pNode->Num );
+        }
+        else if ( Map_NodeIsConst(pNode) )
+        {
+            if ( pNode->pRepr )
+                printf( "Constant 1 %d is a secondary node.\n", pNode->Num );
+        }
+        else
+        {
+            if ( pNode->pRepr )
+                printf( "Internal node %d is a secondary node.\n", pNode->Num );
+            if ( Map_Regular(pNode->p1)->pRepr )
+                printf( "Internal node %d has first fanin that is a secondary node.\n", pNode->Num );
+            if ( Map_Regular(pNode->p2)->pRepr )
+                printf( "Internal node %d has second fanin that is a secondary node.\n", pNode->Num );
+        }
+    }
+    Map_NodeVecFree( pVec );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if current mapping of the node violates fanout limits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingNodeIsViolator( Map_Node_t * pNode, Map_Cut_t * pCut, int fPosPol )
+{
+    return pNode->nRefAct[fPosPol] > (int)pCut->M[fPosPol].pSuperBest->nFanLimit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the total are flow of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Map_MappingGetAreaFlow( Map_Man_t * p )
+{
+    Map_Node_t * pNode;
+    Map_Cut_t * pCut;
+    float aFlowFlowTotal = 0;
+    int fPosPol, i;
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        pNode = Map_Regular(p->pOutputs[i]);
+        if ( !Map_NodeIsAnd(pNode) )
+            continue;
+        fPosPol = !Map_IsComplement(p->pOutputs[i]);
+        pCut = pNode->pCutBest[fPosPol];
+        if ( pCut == NULL )
+        {
+            fPosPol = !fPosPol;
+            pCut = pNode->pCutBest[fPosPol];
+        }
+        aFlowFlowTotal += pNode->pCutBest[fPosPol]->M[fPosPol].AreaFlow;
+    }
+    return aFlowFlowTotal;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the supergates by their level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_CompareNodesByLevel( Map_Node_t ** ppS1, Map_Node_t ** ppS2 )
+{
+    Map_Node_t * pN1 = Map_Regular(*ppS1);
+    Map_Node_t * pN2 = Map_Regular(*ppS2);
+    if ( pN1->Level > pN2->Level )
+        return -1;
+    if ( pN1->Level < pN2->Level )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders the nodes in the decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingSortByLevel( Map_Man_t * pMan, Map_NodeVec_t * vNodes )
+{
+    qsort( (void *)vNodes->pArray, vNodes->nSize, sizeof(Map_Node_t *), 
+            (int (*)(const void *, const void *)) Map_CompareNodesByLevel );
+//    assert( Map_CompareNodesByLevel( vNodes->pArray, vNodes->pArray + vNodes->nSize - 1 ) <= 0 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the supergates by their pointer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_CompareNodesByPointer( Map_Node_t ** ppS1, Map_Node_t ** ppS2 )
+{
+    if ( *ppS1 < *ppS2 )
+        return -1;
+    if ( *ppS1 > *ppS2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts how many AIG nodes are mapped in both polarities.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCountDoubles( Map_Man_t * pMan, Map_NodeVec_t * vNodes )
+{
+    Map_Node_t * pNode;
+    int Counter, i;
+    // count the number of equal adjacent nodes
+    Counter = 0;
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        pNode = vNodes->pArray[i];
+        if ( !Map_NodeIsAnd(pNode) )
+            continue;
+        if ( (pNode->nRefAct[0] && pNode->pCutBest[0]) && 
+             (pNode->nRefAct[1] && pNode->pCutBest[1]) )
+            Counter++;
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+st_table * Map_CreateTableGate2Super( Map_Man_t * pMan )
+{
+    Map_Super_t * pSuper;
+    st_table * tTable;
+    int i, nInputs, v;
+    tTable = st_init_table(strcmp, st_strhash);
+    for ( i = 0; i < pMan->pSuperLib->nSupersAll; i++ )
+    {
+        pSuper = pMan->pSuperLib->ppSupers[i];
+        if ( pSuper->nGates == 1 )
+        {
+            // skip different versions of the same root gate
+            nInputs = Mio_GateReadInputs(pSuper->pRoot);
+            for ( v = 0; v < nInputs; v++ )
+                if ( pSuper->pFanins[v]->Num != nInputs - 1 - v )
+                    break;
+            if ( v != nInputs )
+                continue;
+//            printf( "%s\n", Mio_GateReadName(pSuper->pRoot) );
+            if ( st_insert( tTable, (char *)pSuper->pRoot, (char *)pSuper ) )
+            {
+                assert( 0 );
+            }
+        }
+    }
+    return tTable;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Get the FRAIG node with phase.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_ManCleanData( Map_Man_t * p )
+{
+    int i;
+    for ( i = 0; i < p->vNodesAll->nSize; i++ )
+        p->vNodesAll->pArray[i]->pData0 = p->vNodesAll->pArray[i]->pData1 = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Expand the truth table]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingExpandTruth( unsigned uTruth[2], int nVars )
+{
+    assert( nVars < 7 );
+    if ( nVars == 6 )
+        return;
+    if ( nVars < 5 )
+    {
+        uTruth[0] &= MAP_MASK( (1<<nVars) );
+        uTruth[0]  = Map_MappingExpandTruth_rec( uTruth[0], nVars );
+    }
+    uTruth[1] = uTruth[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Expand the truth table]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Map_MappingExpandTruth_rec( unsigned uTruth, int nVars )
+{
+    assert( nVars < 6 );
+    if ( nVars == 5 )
+        return uTruth;
+    return Map_MappingExpandTruth_rec( uTruth | (uTruth << (1 << nVars)), nVars + 1 );    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the arrival times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Map_MappingComputeDelayWithFanouts( Map_Man_t * p )
+{
+    Map_Node_t * pNode;
+    float Result;
+    int i;
+    for ( i = 0; i < p->vAnds->nSize; i++ )
+    {
+        // skip primary inputs
+        pNode = p->vAnds->pArray[i];
+        if ( !Map_NodeIsAnd( pNode ) )
+            continue;
+        // skip a secondary node
+        if ( pNode->pRepr )
+            continue;
+        // count the switching nodes
+        if ( pNode->nRefAct[0] > 0 )
+            Map_TimeCutComputeArrival( pNode, pNode->pCutBest[0], 0, MAP_FLOAT_LARGE );
+        if ( pNode->nRefAct[1] > 0 )
+            Map_TimeCutComputeArrival( pNode, pNode->pCutBest[1], 1, MAP_FLOAT_LARGE );
+    }
+    Result = Map_TimeComputeArrivalMax(p);
+    printf( "Max arrival times with fanouts = %10.2f.\n", Result );
+    return Result;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the mask.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingGetMaxLevel( Map_Man_t * pMan )
+{
+    int nLevelMax, i;
+    nLevelMax = 0;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        nLevelMax = ((unsigned)nLevelMax) > Map_Regular(pMan->pOutputs[i])->Level? 
+                nLevelMax : Map_Regular(pMan->pOutputs[i])->Level;
+    return nLevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Analyses choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingUpdateLevel_rec( Map_Man_t * pMan, Map_Node_t * pNode, int fMaximum )
+{
+    Map_Node_t * pTemp;
+    int Level1, Level2, LevelE;
+    assert( !Map_IsComplement(pNode) );
+    if ( !Map_NodeIsAnd(pNode) )
+        return pNode->Level;
+    // skip the visited node
+    if ( pNode->TravId == pMan->nTravIds )
+        return pNode->Level;
+    pNode->TravId = pMan->nTravIds;
+    // compute levels of the children nodes
+    Level1 = Map_MappingUpdateLevel_rec( pMan, Map_Regular(pNode->p1), fMaximum );
+    Level2 = Map_MappingUpdateLevel_rec( pMan, Map_Regular(pNode->p2), fMaximum );
+    pNode->Level = 1 + MAP_MAX( Level1, Level2 );
+    if ( pNode->pNextE )
+    {
+        LevelE = Map_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
+        if ( fMaximum )
+        {
+            if ( pNode->Level < (unsigned)LevelE )
+                pNode->Level = LevelE;
+        }
+        else
+        {
+            if ( pNode->Level > (unsigned)LevelE )
+                pNode->Level = LevelE;
+        }
+        // set the level of all equivalent nodes to be the same minimum
+        if ( pNode->pRepr == NULL ) // the primary node
+            for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE )
+                pTemp->Level = pNode->Level;
+    }
+    return pNode->Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets the levels of the nodes in the choice graph.]
+
+  Description [Makes the level of the choice nodes to be equal to the
+  maximum of the level of the nodes in the equivalence class. This way
+  sorting by level leads to the reverse topological order, which is
+  needed for the required time computation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingSetChoiceLevels( Map_Man_t * pMan )
+{
+    int i;
+    pMan->nTravIds++;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports statistics on choice nodes.]
+
+  Description [The number of choice nodes is the number of primary nodes,
+  which has pNextE set to a pointer. The number of choices is the number
+  of entries in the equivalent-node lists of the primary nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingReportChoices( Map_Man_t * pMan )
+{
+    Map_Node_t * pNode, * pTemp;
+    int nChoiceNodes, nChoices;
+    int i, LevelMax1, LevelMax2;
+
+    // report the number of levels
+    LevelMax1 = Map_MappingGetMaxLevel( pMan );
+    pMan->nTravIds++;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 0 );
+    LevelMax2 = Map_MappingGetMaxLevel( pMan );
+
+    // report statistics about choices
+    nChoiceNodes = nChoices = 0;
+    for ( i = 0; i < pMan->vAnds->nSize; i++ )
+    {
+        pNode = pMan->vAnds->pArray[i];
+        if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
+        { // this is a choice node = the primary node that has equivalent nodes
+            nChoiceNodes++;
+            for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
+                nChoices++;
+        }
+    }
+    printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
+    printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
+}
+
+/*
+void Map_MappingReportChoices( Map_Man_t * pMan )
+{
+    Map_Node_t * pNode, * pTemp;
+    int nChoiceNodes, nChoices;
+    int i, LevelMax1, LevelMax2;
+    int DiffMaxTotal, DiffMinTotal, Min, Max;
+    int CounterByMin[300]={0}, CounterByMax[300]={0};
+
+    // report the number of levels
+    LevelMax1 = Map_MappingGetMaxLevel( pMan );
+    pMan->nTravIds++;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+//        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 0 );
+        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 1 );
+    LevelMax2 = Map_MappingGetMaxLevel( pMan );
+
+    // report statistics about choices
+    nChoiceNodes = nChoices = 0;
+    DiffMaxTotal = DiffMinTotal = 0;
+    for ( i = 0; i < pMan->vAnds->nSize; i++ )
+    {
+        pNode = pMan->vAnds->pArray[i];
+        if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
+        { // this is a choice node = the primary node that has equivalent nodes
+            nChoiceNodes++;
+            for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
+                nChoices++;
+            // call to compare the levels
+            Map_MappingGetChoiceLevels( pMan, pNode, pNode->pNextE, &Min, &Max );
+            assert( Min < (int)pNode->Level );
+            assert( Max < (int)pNode->Level );
+            DiffMinTotal += pNode->Level - Max;
+            DiffMaxTotal += pNode->Level - Min;
+
+            CounterByMin[pNode->Level - Max]++;
+            CounterByMax[pNode->Level - Min]++;
+
+        }
+    }
+    printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
+    printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
+    printf( "Choice depth:  Minimum = %4.2f. Maximum = %4.2f.\n", 
+        ((float)DiffMinTotal)/nChoiceNodes, ((float)DiffMaxTotal)/nChoiceNodes );
+
+    {
+    FILE * pTable;
+    pTable = fopen( "statsc.txt", "a+" );
+    fprintf( pTable, "%6d ", pMan->vAnds->nSize );
+    fprintf( pTable, "%5d ", LevelMax2 );
+    fprintf( pTable, "%5d ", nChoiceNodes );
+    fprintf( pTable, "%5d ", nChoices );
+    fprintf( pTable, "%5.2f ", ((float)DiffMinTotal)/nChoiceNodes );
+    fprintf( pTable, "%5.2f ", ((float)DiffMaxTotal)/nChoiceNodes );
+//    fprintf( pTable, "%4.2f\n", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+    }
+
+
+    printf( "Distribution by min/max levels:\n" );
+    for ( i = 0; i < LevelMax2; i++ )
+        printf( "%3d :  %5d  %5d\n", i, CounterByMin[i], CounterByMax[i] );
+    printf( "\n" );
+}
+*/
+
+/*
+void Map_MappingReportChoices( Map_Man_t * pMan )
+{
+    Map_Node_t * pNode, * pTemp;
+    int nChoiceNodes, nChoices;
+    int i, LevelMax1, LevelMax2;
+    int CounterByVol[1000]={0};
+    float VolumeAve, Volume;
+
+    // report the number of levels
+    LevelMax1 = Map_MappingGetMaxLevel( pMan );
+    pMan->nTravIds++;
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 0 );
+//        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 1 );
+    LevelMax2 = Map_MappingGetMaxLevel( pMan );
+
+    // report statistics about choices
+    nChoiceNodes = nChoices = 0;
+    VolumeAve = 0.0;
+    for ( i = 0; i < pMan->vAnds->nSize; i++ )
+    {
+        pNode = pMan->vAnds->pArray[i];
+        if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
+        { // this is a choice node = the primary node that has equivalent nodes
+            nChoiceNodes++;
+            for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
+                nChoices++;
+            Volume = Map_MappingGetChoiceVolumes( pMan, pNode, pNode->pNextE );
+            VolumeAve += Volume;
+            assert( Volume < 1000 );
+            CounterByVol[(int)Volume]++;
+        }
+    }
+    printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
+    printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
+    printf( "Average volume = %5.4f.\n", VolumeAve/nChoiceNodes );
+*/
+/*
+    {
+    FILE * pTable;
+    pTable = fopen( "statsv.txt", "a+" );
+    fprintf( pTable, "%6d ", Map_MappingCountUsedNodes(pMan,1) );
+    fprintf( pTable, "%6d ", Map_MappingCountUsedNodes(pMan,0) );
+    fprintf( pTable, "%5d ", LevelMax1 );
+    fprintf( pTable, "   " );
+    fprintf( pTable, "%5d ", nChoiceNodes );
+    fprintf( pTable, "%5d ", nChoices );
+    fprintf( pTable, "   " );
+    fprintf( pTable, "%5.4f ", VolumeAve/nChoiceNodes );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+    }
+    printf( "Distribution by volume:\n" );
+    for ( i = 0; i < 1000; i++ )
+        if ( CounterByVol[i] > 0 )
+        printf( "%3d :  %5d\n", i, CounterByVol[i] );
+    printf( "\n" );
+*/
+/*
+}
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the maximum and minimum levels of the choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_MappingGetChoiceLevels( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2, int * pMin, int * pMax )
+{
+    Map_NodeVec_t * vNodes;
+    Map_NodeVec_t * vBoundary;
+    Map_Node_t * pNode;
+    int i, Min, Max;
+
+    vNodes    = Map_NodeVecAlloc( 100 );
+    vBoundary = Map_NodeVecAlloc( 100 );
+    Map_MappingDfsMarked1_rec( p1, vNodes, 1 );
+    Map_MappingDfsMarked2_rec( p2, vNodes, vBoundary, 1 );
+    // clean the marks
+    Min =  100000;
+    Max = -100000;
+    for ( i = 0; i < vBoundary->nSize; i++ )
+    {
+        pNode = vBoundary->pArray[i];
+        if ( Min > (int)pNode->Level )
+            Min = pNode->Level;
+        if ( Max < (int)pNode->Level )
+            Max = pNode->Level;
+    }
+    Map_NodeVecFree( vBoundary );
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        pNode = vNodes->pArray[i];
+        pNode->fMark0 = pNode->fMark1 = 0;
+    }
+    Map_NodeVecFree( vNodes );
+    *pMin = Min;
+    *pMax = Max;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Map_MappingGetChoiceVolumes( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 )
+{
+    Map_NodeVec_t * vNodes;
+    Map_Node_t * pNode;
+    int i, nVolumeTotal, nVolumeUnique;
+
+    vNodes    = Map_NodeVecAlloc( 100 );
+    Map_MappingDfsMarked3_rec( p1, vNodes );
+    Map_MappingDfsMarked4_rec( p2, vNodes );
+    // clean the marks
+    nVolumeTotal = nVolumeUnique = 0;
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        pNode = vNodes->pArray[i];
+        if ( !Map_NodeIsAnd(pNode) )
+            continue;
+        nVolumeTotal++;
+        if ( pNode->fMark0 ^ pNode->fMark1 )
+            nVolumeUnique++;
+        pNode->fMark0 = pNode->fMark1 = 0;
+    }
+    Map_NodeVecFree( vNodes );
+//    return ((float)nVolumeUnique)/nVolumeTotal;
+    return (float)nVolumeUnique;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the maximum and minimum levels of the choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCountUsedNodes( Map_Man_t * pMan, int fChoices )
+{
+    Map_NodeVec_t * vNodes;
+    int Result;
+    vNodes = Map_MappingDfs( pMan, fChoices );
+    Result = vNodes->nSize;
+    Map_NodeVecFree( vNodes );
+    return Result;    
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+