src/map/mapper/mapperUtils.c

Go to the documentation of this file.

#include "mapperInt.h"


#define MAP_CO_LIST_SIZE 5

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( Map_Node_t ** ppNode1, Map_Node_t ** ppNode2 );
static void  Map_MappingFindLatest( Map_Man_t * p, int * pNodes, int nNodesMax );
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;



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;
}

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;
}

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 );
}



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 );
}

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 );
}


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 );
}

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 );
}



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;
}

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;
}

void Map_MappingUnmark( Map_Man_t * pMan )
{
    int i;
    for ( i = 0; i < pMan->nOutputs; i++ )
        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
}

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 );
}

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) );
}

int Map_MappingCompareOutputDelay( Map_Node_t ** ppNode1, Map_Node_t ** ppNode2 )
{
    Map_Node_t * pNode1 = Map_Regular(*ppNode1);
    Map_Node_t * pNode2 = Map_Regular(*ppNode2);
    int fPhase1 = !Map_IsComplement(*ppNode1);
    int fPhase2 = !Map_IsComplement(*ppNode2);
    float Arrival1 = pNode1->tArrival[fPhase1].Worst;
    float Arrival2 = pNode2->tArrival[fPhase2].Worst;
    if ( Arrival1 < Arrival2 )
        return -1;
    if ( Arrival1 > Arrival2 )
        return 1;
    return 0;
}

void Map_MappingFindLatest( Map_Man_t * p, int * pNodes, int nNodesMax )
{
    int nNodes, i, k, v;
    assert( p->nOutputs >= nNodesMax );
    pNodes[0] = 0;
    nNodes = 1;
    for ( i = 1; i < p->nOutputs; i++ )
    {
        for ( k = nNodes - 1; k >= 0; k-- )
            if ( Map_MappingCompareOutputDelay( &p->pOutputs[pNodes[k]], &p->pOutputs[i] ) >= 0 )
                break;
        if ( k == nNodesMax - 1 )
            continue;
        if ( nNodes < nNodesMax )
            nNodes++;
        for ( v = nNodes - 1; v > k+1; v-- )
            pNodes[v] = pNodes[v-1];
        pNodes[k+1] = i;
    }
}

void Map_MappingPrintOutputArrivals( Map_Man_t * p )
{
    int pSorted[MAP_CO_LIST_SIZE];
    Map_Time_t * pTimes;
    Map_Node_t * pNode;
    int fPhase, Limit, i;
    int MaxNameSize;

    // determine the number of nodes to print
    Limit = (p->nOutputs > MAP_CO_LIST_SIZE)? MAP_CO_LIST_SIZE : p->nOutputs;

    // determine the order
    Map_MappingFindLatest( p, pSorted, Limit );

    // determine max size of the node's name
    MaxNameSize = 0;
    for ( i = 0; i < Limit; i++ )
        if ( MaxNameSize < (int)strlen(p->ppOutputNames[pSorted[i]]) )
            MaxNameSize = strlen(p->ppOutputNames[pSorted[i]]);

    // print the latest outputs
    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( "Output  %-*s : ", MaxNameSize + 3, p->ppOutputNames[pSorted[i]] );
        printf( "Delay = (%5.2f, %5.2f)  ", (double)pTimes->Rise, (double)pTimes->Fall );
        printf( "%s", fPhase? "POS" : "NEG" );
        printf( "\n" );
    }
}

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;
}

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" );
*/
}

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;
    }
}

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;
}

int Map_MappingNodeIsViolator( Map_Node_t * pNode, Map_Cut_t * pCut, int fPosPol )
{
    return pNode->nRefAct[fPosPol] > (int)pCut->M[fPosPol].pSuperBest->nFanLimit;
}

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;
}


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;
}

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 );
}


int Map_CompareNodesByPointer( Map_Node_t ** ppS1, Map_Node_t ** ppS2 )
{
    if ( *ppS1 < *ppS2 )
        return -1;
    if ( *ppS1 > *ppS2 )
        return 1;
    return 0;
}

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;
}


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;
}

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;
}

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];
}

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 );    
}

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;
}


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;
}

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;
}

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 );
}

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_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;
}


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;
}


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;    
}

---