/**CFile****************************************************************

  FileName    [fraigUtil.c]

  PackageName [FRAIG: Functionally reduced AND-INV graphs.]

  Synopsis    [Various utilities.]

  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 2.0. Started - October 1, 2004]

  Revision    [$Id: fraigUtil.c,v 1.15 2005/07/08 01:01:34 alanmi Exp $]

***********************************************************************/

#include "fraigInt.h"
#include <limits.h>

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static int bit_count[256] = {
  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};

static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv );
static int  Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Computes the DFS ordering of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv )
{
    Fraig_NodeVec_t * vNodes;
    int i;
    pMan->nTravIds++;
    vNodes = Fraig_NodeVecAlloc( 100 );
    for ( i = 0; i < pMan->vOutputs->nSize; i++ )
        Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv );
    return vNodes;
}

/**Function*************************************************************

  Synopsis    [Computes the DFS ordering of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv )
{
    Fraig_NodeVec_t * vNodes;
    pMan->nTravIds++;
    vNodes = Fraig_NodeVecAlloc( 100 );
    Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv );
    return vNodes;
}

/**Function*************************************************************

  Synopsis    [Computes the DFS ordering of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv )
{
    Fraig_NodeVec_t * vNodes;
    int i;
    pMan->nTravIds++;
    vNodes = Fraig_NodeVecAlloc( 100 );
    for ( i = 0; i < nNodes; i++ )
        Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv );
    return vNodes;
}

/**Function*************************************************************

  Synopsis    [Recursively computes the DFS ordering of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv )
{
    assert( !Fraig_IsComplement(pNode) );
    // skip the visited node
    if ( pNode->TravId == pMan->nTravIds )
        return;
    pNode->TravId = pMan->nTravIds;
    // visit the transitive fanin
    if ( Fraig_NodeIsAnd(pNode) )
    {
        Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p1), vNodes, fEquiv );
        Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p2), vNodes, fEquiv );
    }
    if ( fEquiv && pNode->pNextE )
        Fraig_Dfs_rec( pMan, pNode->pNextE, vNodes, fEquiv );
    // save the node
    Fraig_NodeVecPush( vNodes, pNode );
}

/**Function*************************************************************

  Synopsis    [Computes the DFS ordering of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv )
{
    Fraig_NodeVec_t * vNodes;
    int RetValue;
    vNodes = Fraig_Dfs( pMan, fEquiv );
    RetValue = vNodes->nSize;
    Fraig_NodeVecFree( vNodes );
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
{
    assert( !Fraig_IsComplement(pOld) );
    assert( !Fraig_IsComplement(pNew) );
    pMan->nTravIds++;
    return Fraig_CheckTfi_rec( pMan, pNew, pOld );
}

/**Function*************************************************************

  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld )
{
    // check the trivial cases
    if ( pNode == NULL )
        return 0;
    if ( pNode->Num < pOld->Num && !pMan->fChoicing )
        return 0;
    if ( pNode == pOld )
        return 1;
    // skip the visited node
    if ( pNode->TravId == pMan->nTravIds )
        return 0;
    pNode->TravId = pMan->nTravIds;
    // check the children
    if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p1), pOld ) )
        return 1;
    if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p2), pOld ) )
        return 1;
    // check equivalent nodes
    return Fraig_CheckTfi_rec( pMan, pNode->pNextE, pOld );
}


/**Function*************************************************************

  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
{
    Fraig_NodeVec_t * vNodes;
    int RetValue;
    vNodes = Fraig_DfsOne( pMan, pNew, 1 );
    RetValue = (pOld->TravId == pMan->nTravIds);
    Fraig_NodeVecFree( vNodes );
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Sets the number of fanouts (none, one, or many).]

  Description [This procedure collects the nodes reachable from
  the POs of the AIG and sets the type of fanout counter (none, one,
  or many) for each node. This procedure is useful to determine
  fanout-free cones of AND-nodes, which is helpful for rebalancing
  the AIG (see procedure Fraig_ManRebalance, or something like that).]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_ManMarkRealFanouts( Fraig_Man_t * p )
{
    Fraig_NodeVec_t * vNodes;
    Fraig_Node_t * pNodeR;
    int i;
    // collect the nodes reachable
    vNodes = Fraig_Dfs( p, 0 );
    // clean the fanouts field
    for ( i = 0; i < vNodes->nSize; i++ )
    {
        vNodes->pArray[i]->nFanouts = 0;
        vNodes->pArray[i]->pData0 = NULL;
    }
    // mark reachable nodes by setting the two-bit counter pNode->nFans
    for ( i = 0; i < vNodes->nSize; i++ )
    {
        pNodeR = Fraig_Regular(vNodes->pArray[i]->p1);
        if ( pNodeR && ++pNodeR->nFanouts == 3 )
            pNodeR->nFanouts = 2;
        pNodeR = Fraig_Regular(vNodes->pArray[i]->p2);
        if ( pNodeR && ++pNodeR->nFanouts == 3 )
            pNodeR->nFanouts = 2;
    }
    Fraig_NodeVecFree( vNodes );
}

/**Function*************************************************************

  Synopsis    [Creates the constant 1 node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_BitStringCountOnes( unsigned * pString, int nWords )
{
    unsigned char * pSuppBytes = (unsigned char *)pString;
    int i, nOnes, nBytes = sizeof(unsigned) * nWords;
    // count the number of ones in the simulation vector
    for ( i = nOnes = 0; i < nBytes; i++ )
        nOnes += bit_count[pSuppBytes[i]];
    return nOnes;
}

/**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 Fraig_ManCheckConsistency( Fraig_Man_t * p )
{
    Fraig_Node_t * pNode;
    Fraig_NodeVec_t * pVec;
    int i;
    pVec = Fraig_Dfs( p, 0 );
    for ( i = 0; i < pVec->nSize; i++ )
    {
        pNode = pVec->pArray[i];
        if ( Fraig_NodeIsVar(pNode) )
        {
            if ( pNode->pRepr )
                printf( "Primary input %d is a secondary node.\n", pNode->Num );
        }
        else if ( Fraig_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 ( Fraig_Regular(pNode->p1)->pRepr )
                printf( "Internal node %d has first fanin %d that is a secondary node.\n", 
                    pNode->Num, Fraig_Regular(pNode->p1)->Num );
            if ( Fraig_Regular(pNode->p2)->pRepr )
                printf( "Internal node %d has second fanin %d that is a secondary node.\n", 
                    pNode->Num, Fraig_Regular(pNode->p2)->Num );
        }
    }
    Fraig_NodeVecFree( pVec );
    return 1;
}

/**Function*************************************************************

  Synopsis    [Prints the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_PrintNode( Fraig_Man_t * p, Fraig_Node_t * pNode )
{
    Fraig_NodeVec_t * vNodes;
    Fraig_Node_t * pTemp;
    int fCompl1, fCompl2, i;

    vNodes = Fraig_DfsOne( p, pNode, 0 );
    for ( i = 0; i < vNodes->nSize; i++ )
    {
        pTemp = vNodes->pArray[i];
        if ( Fraig_NodeIsVar(pTemp) )
        {
            printf( "%3d : PI          ", pTemp->Num );
            Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
            printf( "   " );
            Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
            printf( "  %d\n", pTemp->fInv );
            continue;
        }

        fCompl1 = Fraig_IsComplement(pTemp->p1);
        fCompl2 = Fraig_IsComplement(pTemp->p2);
        printf( "%3d : %c%3d %c%3d   ", pTemp->Num,
            (fCompl1? '-':'+'), Fraig_Regular(pTemp->p1)->Num,
            (fCompl2? '-':'+'), Fraig_Regular(pTemp->p2)->Num );
        Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
        printf( "   " );
        Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
        printf( "  %d\n", pTemp->fInv );
    }
    Fraig_NodeVecFree( vNodes );
}

/**Function*************************************************************

  Synopsis    [Prints the bit string.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits )
{
    int Remainder, nWords;
    int w, i;

    Remainder = (nBits%(sizeof(unsigned)*8));
    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);

    for ( w = nWords-1; w >= 0; w-- )
        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
            fprintf( pFile, "%c", '0' + (int)((pSign[w] & (1<<i)) > 0) );

//  fprintf( pFile, "\n" );
}

/**Function*************************************************************

  Synopsis    [Sets up the mask.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_GetMaxLevel( Fraig_Man_t * pMan )
{
    int nLevelMax, i;
    nLevelMax = 0;
    for ( i = 0; i < pMan->vOutputs->nSize; i++ )
        nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? 
                nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level;
    return nLevelMax;
}

/**Function*************************************************************

  Synopsis    [Analyses choice nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fMaximum )
{
    Fraig_Node_t * pTemp;
    int Level1, Level2, LevelE;
    assert( !Fraig_IsComplement(pNode) );
    if ( !Fraig_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 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum );
    Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum );
    pNode->Level = 1 + FRAIG_MAX( Level1, Level2 );
    if ( pNode->pNextE )
    {
        LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
        if ( fMaximum )
        {
            if ( pNode->Level < LevelE )
                pNode->Level = LevelE;
        }
        else
        {
            if ( pNode->Level > 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 Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum )
{
    int i;
    pMan->nTravIds++;
    for ( i = 0; i < pMan->vOutputs->nSize; i++ )
        Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum );
}

/**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 Fraig_ManReportChoices( Fraig_Man_t * pMan )
{
    Fraig_Node_t * pNode, * pTemp;
    int nChoiceNodes, nChoices;
    int i, LevelMax1, LevelMax2;

    // report the number of levels
    LevelMax1 = Fraig_GetMaxLevel( pMan );
    Fraig_MappingSetChoiceLevels( pMan, 0 );
    LevelMax2 = Fraig_GetMaxLevel( pMan );

    // report statistics about choices
    nChoiceNodes = nChoices = 0;
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
    {
        pNode = pMan->vNodes->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 );
}

/**Function*************************************************************

  Synopsis    [Returns 1 if the node is the root of EXOR/NEXOR gate.]

  Description [The node can be complemented.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsExorType( Fraig_Node_t * pNode )
{
    Fraig_Node_t * pNode1, * pNode2;
    // make the node regular (it does not matter for EXOR/NEXOR)
    pNode = Fraig_Regular(pNode);
    // if the node or its children are not ANDs or not compl, this cannot be EXOR type
    if ( !Fraig_NodeIsAnd(pNode) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
        return 0;

    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    assert( pNode1->Num < pNode2->Num );

    // compare grandchildren
    return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2);
}

/**Function*************************************************************

  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

  Description [The node can be complemented.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsMuxType( Fraig_Node_t * pNode )
{
    Fraig_Node_t * pNode1, * pNode2;

    // make the node regular (it does not matter for EXOR/NEXOR)
    pNode = Fraig_Regular(pNode);
    // if the node or its children are not ANDs or not compl, this cannot be EXOR type
    if ( !Fraig_NodeIsAnd(pNode) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
        return 0;
    if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
        return 0;

    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    assert( pNode1->Num < pNode2->Num );

    // compare grandchildren
    // node is an EXOR/NEXOR
    if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) )
        return 1; 

    // otherwise the node is MUX iff it has a pair of equal grandchildren
    return pNode1->p1 == Fraig_Not(pNode2->p1) || 
           pNode1->p1 == Fraig_Not(pNode2->p2) ||
           pNode1->p2 == Fraig_Not(pNode2->p1) ||
           pNode1->p2 == Fraig_Not(pNode2->p2);
}

/**Function*************************************************************

  Synopsis    [Returns 1 if the node is EXOR, 0 if it is NEXOR.]

  Description [The node should be EXOR type and not complemented.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsExor( Fraig_Node_t * pNode )
{
    Fraig_Node_t * pNode1;
    assert( !Fraig_IsComplement(pNode) );
    assert( Fraig_NodeIsExorType(pNode) );
    assert( Fraig_IsComplement(pNode->p1) );
    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2);
}

/**Function*************************************************************

  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]

  Description [If the node is a MUX, returns the control variable C.
  Assigns nodes T and E to be the then and else variables of the MUX. 
  Node C is never complemented. Nodes T and E can be complemented.
  This function also recognizes EXOR/NEXOR gates as MUXes.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE )
{
    Fraig_Node_t * pNode1, * pNode2;
    assert( !Fraig_IsComplement(pNode) );
    assert( Fraig_NodeIsMuxType(pNode) );
    // get children
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    // find the control variable
    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p1;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p2;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p1;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p2;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p2;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p2;
        }
    }
    assert( 0 ); // this is not MUX
    return NULL;
}

/**Function*************************************************************

  Synopsis    [Counts the number of EXOR type nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_ManCountExors( Fraig_Man_t * pMan )
{
    int i, nExors;
    nExors = 0;
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
        nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] );
    return nExors;

}

/**Function*************************************************************

  Synopsis    [Counts the number of EXOR type nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_ManCountMuxes( Fraig_Man_t * pMan )
{
    int i, nMuxes;
    nMuxes = 0;
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
        nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] );
    return nMuxes;

}

/**Function*************************************************************

  Synopsis    [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
{
    unsigned * pUnsigned1, * pUnsigned2;
    int i;

    // compare random siminfo
    pUnsigned1 = pNode1->puSimR;
    pUnsigned2 = pNode2->puSimR;
    for ( i = 0; i < pMan->nWordsRand; i++ )
        if ( pUnsigned1[i] & ~pUnsigned2[i] )
            return 0;

    // compare systematic siminfo
    pUnsigned1 = pNode1->puSimD;
    pUnsigned2 = pNode2->puSimD;
    for ( i = 0; i < pMan->iWordStart; i++ )
        if ( pUnsigned1[i] & ~pUnsigned2[i] )
            return 0;

    return 1;
}

/**Function*************************************************************

  Synopsis    [Count the number of PI variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums )
{
    int * pVars, nVars, i, Counter;

    nVars = Msat_IntVecReadSize(vVarNums);
    pVars = Msat_IntVecReadArray(vVarNums);
    Counter = 0;
    for ( i = 0; i < nVars; i++ )
        Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] );
    return Counter;
}



/**Function*************************************************************

  Synopsis    [Counts the number of EXOR type nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_ManPrintRefs( Fraig_Man_t * pMan )
{
    Fraig_NodeVec_t * vPivots;
    Fraig_Node_t * pNode, * pNode2;
    int i, k, Counter, nProved;
    int clk;

    vPivots = Fraig_NodeVecAlloc( 1000 );
    for ( i = 0; i < pMan->vNodes->nSize; i++ )
    {
        pNode = pMan->vNodes->pArray[i];

        if ( pNode->nOnes == 0 || pNode->nOnes == (unsigned)pMan->nWordsRand * 32 )
            continue;

        if ( pNode->nRefs > 5 )
        {
            Fraig_NodeVecPush( vPivots, pNode );
//            printf( "Node %6d : nRefs = %2d   Level = %3d.\n", pNode->Num, pNode->nRefs, pNode->Level );
        }
    }
    printf( "Total nodes = %d. Referenced nodes = %d.\n", pMan->vNodes->nSize, vPivots->nSize );

clk = clock();
    // count implications
    Counter = nProved = 0;
    for ( i = 0; i < vPivots->nSize; i++ )
        for ( k = i+1; k < vPivots->nSize; k++ )
        {
            pNode  = vPivots->pArray[i];
            pNode2 = vPivots->pArray[k];
            if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
            {
                if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
                    nProved++;
                Counter++;
            }
            else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
            {
                if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
                    nProved++;
                Counter++;
            }
        }
    printf( "Number of candidate pairs = %d.  Proved = %d.\n", Counter, nProved );
PRT( "Time", clock() - clk );
    return 0;
}


/**Function*************************************************************

  Synopsis    [Checks if pNew exists among the implication fanins of pOld.]

  Description [If pNew is an implication fanin of pOld, returns 1. 
  If Fraig_Not(pNew) is an implication fanin of pOld, return -1.
  Otherwise returns 0.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew )
{
    int RetValue1, RetValue2;
    if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) )
        return (pOld == pNew)? 1 : -1;
    if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) )
        return 0;
    RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew );
    RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew );
    if ( RetValue1 == -1 || RetValue2 == -1 )
        return -1;
    if ( RetValue1 ==  1 || RetValue2 ==  1 )
        return 1;
    return 0;
}


/**Function*************************************************************

  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_CollectSupergate_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, int fFirst, int fStopAtMux )
{
    // if the new node is complemented or a PI, another gate begins
//    if ( Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || Fraig_NodeIsMuxType(pNode) )
    if ( (!fFirst && Fraig_Regular(pNode)->nRefs > 1) || 
          Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || 
          (fStopAtMux && Fraig_NodeIsMuxType(pNode)) )
    {
        Fraig_NodeVecPushUnique( vSuper, pNode );
        return;
    }
    // go through the branches
    Fraig_CollectSupergate_rec( pNode->p1, vSuper, 0, fStopAtMux );
    Fraig_CollectSupergate_rec( pNode->p2, vSuper, 0, fStopAtMux );
}

/**Function*************************************************************

  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux )
{
    Fraig_NodeVec_t * vSuper;
    vSuper = Fraig_NodeVecAlloc( 8 );
    Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
    return vSuper;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_ManIncrementTravId( Fraig_Man_t * pMan )
{
    pMan->nTravIds2++;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
{
    pNode->TravId2 = pMan->nTravIds2;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
{
    return pNode->TravId2 == pMan->nTravIds2;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
{
    return pNode->TravId2 == pMan->nTravIds2 - 1;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


