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

  FileName    [abcOdc.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Scalable computation of observability don't-cares.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: abcOdc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "base/abc/abc.h"

ABC_NAMESPACE_IMPL_START


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

#define ABC_DC_MAX_NODES   (1<<15)

typedef unsigned short Odc_Lit_t;

typedef struct Odc_Obj_t_ Odc_Obj_t;     // 16 bytes
struct Odc_Obj_t_
{
    Odc_Lit_t               iFan0;       // first fanin
    Odc_Lit_t               iFan1;       // second fanin
    Odc_Lit_t               iNext;       // next node in the hash table
    unsigned short          TravId;      // the traversal ID
    unsigned                uData;       // the computed data
    unsigned                uMask;       // the variable mask 
};

struct Odc_Man_t_
{
    // dont'-care parameters
    int                     nVarsMax;    // the max number of cut variables
    int                     nLevels;     // the number of ODC levels
    int                     fVerbose;    // the verbosiness flag
    int                     fVeryVerbose;// the verbosiness flag to print per-node stats
    int                     nPercCutoff; // cutoff percentage

    // windowing
    Abc_Obj_t *             pNode;       // the node for windowing
    Vec_Ptr_t *             vLeaves;     // the number of the cut
    Vec_Ptr_t *             vRoots;      // the roots of the cut
    Vec_Ptr_t *             vBranches;   // additional inputs 

    // internal AIG package
    // objects
    int                     nPis;        // number of PIs (nVarsMax + 32)
    int                     nObjs;       // number of objects (Const1, PIs, ANDs)
    int                     nObjsAlloc;  // number of objects allocated
    Odc_Obj_t *             pObjs;       // objects 
    Odc_Lit_t               iRoot;       // the root object
    unsigned short          nTravIds;    // the number of travIDs
    // structural hashing
    Odc_Lit_t *             pTable;      // hash table
    int                     nTableSize;  // hash table size
    Vec_Int_t *             vUsedSpots;  // the used spots

    // truth tables
    int                     nBits;       // the number of bits
    int                     nWords;      // the number of words 
    Vec_Ptr_t *             vTruths;     // truth tables for each node
    Vec_Ptr_t *             vTruthsElem; // elementary truth tables for the PIs
    unsigned *              puTruth;     // the place where the resulting truth table does

    // statistics
    int                     nWins;       // the number of windows processed
    int                     nWinsEmpty;  // the number of empty windows
    int                     nSimsEmpty;  // the number of empty simulation infos
    int                     nQuantsOver; // the number of quantification overflows
    int                     nWinsFinish; // the number of windows that finished
    int                     nTotalDcs;   // total percentage of DCs

    // runtime
    abctime                 timeClean;   // windowing
    abctime                 timeWin;     // windowing
    abctime                 timeMiter;   // computing the miter
    abctime                 timeSim;     // simulation
    abctime                 timeQuant;   // quantification
    abctime                 timeTruth;   // truth table
    abctime                 timeTotal;   // useful runtime
    abctime                 timeAbort;   // aborted runtime
};


// quantity of different objects
static inline int           Odc_PiNum( Odc_Man_t * p )                     { return p->nPis;                       }
static inline int           Odc_NodeNum( Odc_Man_t * p )                   { return p->nObjs - p->nPis - 1;        }
static inline int           Odc_ObjNum( Odc_Man_t * p )                    { return p->nObjs;                      }

// complemented attributes of objects
static inline int           Odc_IsComplement( Odc_Lit_t Lit )              { return Lit &  (Odc_Lit_t)1;           }
static inline Odc_Lit_t     Odc_Regular( Odc_Lit_t Lit )                   { return Lit & ~(Odc_Lit_t)1;           }
static inline Odc_Lit_t     Odc_Not( Odc_Lit_t Lit )                       { return Lit ^  (Odc_Lit_t)1;           }
static inline Odc_Lit_t     Odc_NotCond( Odc_Lit_t Lit, int c )            { return Lit ^  (Odc_Lit_t)(c!=0);      }

// specialized Literals
static inline Odc_Lit_t     Odc_Const0()                                   { return 1;                             }
static inline Odc_Lit_t     Odc_Const1()                                   { return 0;                             }
static inline Odc_Lit_t     Odc_Var( Odc_Man_t * p, int i )                { assert( i >= 0 && i < p->nPis ); return (i+1) << 1;  }
static inline int           Odc_IsConst( Odc_Lit_t Lit )                   { return Lit <  (Odc_Lit_t)2;           }
static inline int           Odc_IsTerm( Odc_Man_t * p, Odc_Lit_t Lit )     { return (int)(Lit>>1) <= p->nPis;      }

// accessing internal storage
static inline Odc_Obj_t *   Odc_ObjNew( Odc_Man_t * p )                    { assert( p->nObjs < p->nObjsAlloc ); return p->pObjs + p->nObjs++;        }
static inline Odc_Lit_t     Odc_Obj2Lit( Odc_Man_t * p, Odc_Obj_t * pObj ) { assert( pObj ); return (pObj - p->pObjs) << 1;                           }
static inline Odc_Obj_t *   Odc_Lit2Obj( Odc_Man_t * p, Odc_Lit_t Lit )    { assert( !(Lit & 1) && (int)(Lit>>1) < p->nObjs ); return p->pObjs + (Lit>>1); }

// fanins and their complements
static inline Odc_Lit_t     Odc_ObjChild0( Odc_Obj_t * pObj )              { return pObj->iFan0;                   }
static inline Odc_Lit_t     Odc_ObjChild1( Odc_Obj_t * pObj )              { return pObj->iFan1;                   }
static inline Odc_Lit_t     Odc_ObjFanin0( Odc_Obj_t * pObj )              { return Odc_Regular(pObj->iFan0);      }
static inline Odc_Lit_t     Odc_ObjFanin1( Odc_Obj_t * pObj )              { return Odc_Regular(pObj->iFan1);      }
static inline int           Odc_ObjFaninC0( Odc_Obj_t * pObj )             { return Odc_IsComplement(pObj->iFan0); }
static inline int           Odc_ObjFaninC1( Odc_Obj_t * pObj )             { return Odc_IsComplement(pObj->iFan1); }

// traversal IDs
static inline void          Odc_ManIncrementTravId( Odc_Man_t * p )                         { p->nTravIds++;                                    }
static inline void          Odc_ObjSetTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                       }
static inline int           Odc_ObjIsTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj )       { return (int )((int)pObj->TravId == p->nTravIds);  }

// truth tables
static inline unsigned *    Odc_ObjTruth( Odc_Man_t * p, Odc_Lit_t Lit )   { assert( !(Lit & 1) ); return (unsigned *) Vec_PtrEntry(p->vTruths, Lit >> 1);  }

// iterators 
#define Odc_ForEachPi( p, Lit, i )                                                 \
    for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ )
#define Odc_ForEachAnd( p, pObj, i )                                               \
    for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ )


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

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

  Synopsis    [Allocates the don't-care manager.]

  Description [The parameters are the max number of cut variables, 
  the number of fanout levels used for the ODC computation, and verbosiness.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose )
{
    Odc_Man_t * p;
    unsigned * pData;
    int i, k;
    p = ABC_ALLOC( Odc_Man_t, 1 );
    memset( p, 0, sizeof(Odc_Man_t) );
    assert( nVarsMax > 4 && nVarsMax < 16 );
    assert( nLevels > 0 && nLevels < 10 );

    srand( 0xABC );

    // dont'-care parameters
    p->nVarsMax     = nVarsMax;
    p->nLevels      = nLevels;
    p->fVerbose     = fVerbose;
    p->fVeryVerbose = fVeryVerbose;
    p->nPercCutoff  = 10;

    // windowing
    p->vRoots    = Vec_PtrAlloc( 128 );
    p->vBranches = Vec_PtrAlloc( 128 );

    // internal AIG package
    // allocate room for objects
    p->nObjsAlloc = ABC_DC_MAX_NODES; 
    p->pObjs = ABC_ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
    p->nPis  = nVarsMax + 32;
    p->nObjs = 1 + p->nPis;
    memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
    // set the PI masks
    for ( i = 0; i < 32; i++ )
        p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
    // allocate hash table
    p->nTableSize = p->nObjsAlloc/3 + 1;
    p->pTable = ABC_ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
    memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
    p->vUsedSpots = Vec_IntAlloc( 1000 );

    // truth tables
    p->nWords = Abc_TruthWordNum( p->nVarsMax );
    p->nBits = p->nWords * 8 * sizeof(unsigned);
    p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords );
    p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords );

    // set elementary truth tables
    Abc_InfoFill( (unsigned *)Vec_PtrEntry(p->vTruths, 0), p->nWords );
    for ( k = 0; k < p->nVarsMax; k++ )
    {
//        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        pData = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
        Abc_InfoClear( pData, p->nWords );
        for ( i = 0; i < p->nBits; i++ )
            if ( i & (1 << k) )
                pData[i>>5] |= (1 << (i&31));
    }

    // set random truth table for the additional inputs
    for ( k = p->nVarsMax; k < p->nPis; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        Abc_InfoRandom( pData, p->nWords );
    }

    // set the miter to the unused value
    p->iRoot = 0xffff;
    return p;
}

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

  Synopsis    [Clears the manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareClear( Odc_Man_t * p )
{
    abctime clk = Abc_Clock();
    // clean the structural hashing table
    if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
        memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
    else
    {
        int iSpot, i;
        Vec_IntForEachEntry( p->vUsedSpots, iSpot, i )
            p->pTable[iSpot] = 0;
    }
    Vec_IntClear( p->vUsedSpots ); 
    // reset the number of nodes
    p->nObjs = 1 + p->nPis;
    // reset the root node
    p->iRoot = 0xffff;

p->timeClean += Abc_Clock() - clk;
}

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

  Synopsis    [Frees the don't-care manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareFree( Odc_Man_t * p )
{
    if ( p->fVerbose )
    {
        printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n", 
            p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish );
        printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", 
            1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
        printf( "Runtime stats of the ODC manager:\n" );
        ABC_PRT( "Cleaning    ", p->timeClean );
        ABC_PRT( "Windowing   ", p->timeWin   );
        ABC_PRT( "Miter       ", p->timeMiter );
        ABC_PRT( "Simulation  ", p->timeSim   );
        ABC_PRT( "Quantifying ", p->timeQuant );
        ABC_PRT( "Truth table ", p->timeTruth );
        ABC_PRT( "TOTAL       ", p->timeTotal );
        ABC_PRT( "Aborted     ", p->timeAbort );
    }
    Vec_PtrFree( p->vRoots );
    Vec_PtrFree( p->vBranches );
    Vec_PtrFree( p->vTruths );
    Vec_PtrFree( p->vTruthsElem );
    Vec_IntFree( p->vUsedSpots );
    ABC_FREE( p->pObjs );
    ABC_FREE( p->pTable );
    ABC_FREE( p );
}


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

  Synopsis    [Marks the TFO of the collected nodes up to the given level.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
{
    Abc_Obj_t * pFanout;
    int i;
    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
        return;
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return;
    Abc_NodeSetTravIdCurrent( pObj );
    ////////////////////////////////////////
    // try to reduce the runtime
    if ( Abc_ObjFanoutNum(pObj) > 100 )
        return;
    ////////////////////////////////////////
    Abc_ObjForEachFanout( pObj, pFanout, i )
        Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
}

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

  Synopsis    [Marks the TFO of the collected nodes up to the given level.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareWinSweepLeafTfo( Odc_Man_t * p )
{
    Abc_Obj_t * pObj;
    int i;
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
        Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode );
}

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

  Synopsis    [Recursively collects the roots.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareWinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
{
    Abc_Obj_t * pFanout;
    int i;
    assert( Abc_ObjIsNode(pObj) );
    assert( Abc_NodeIsTravIdCurrent(pObj) );
    // check if the node has all fanouts marked
    Abc_ObjForEachFanout( pObj, pFanout, i )
        if ( !Abc_NodeIsTravIdCurrent(pFanout) )
            break;
    // if some of the fanouts are unmarked, add the node to the root
    if ( i < Abc_ObjFanoutNum(pObj) ) 
    {
        Vec_PtrPushUnique( vRoots, pObj );
        return;
    }
    // otherwise, call recursively
    Abc_ObjForEachFanout( pObj, pFanout, i )
        Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots );
}

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

  Synopsis    [Collects the roots of the window.]

  Description [Roots of the window are the nodes that have at least
  one fanout that it not in the TFO of the leaves.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareWinCollectRoots( Odc_Man_t * p )
{
    assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
    // mark the node with the old traversal ID
    Abc_NodeSetTravIdCurrent( p->pNode ); 
    // collect the roots
    Vec_PtrClear( p->vRoots );
    Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots );
}
 
/**Function*************************************************************

  Synopsis    [Recursively adds missing nodes and leaves.]

  Description []
               
  SideEffects []

  SeeAlso     [] 

***********************************************************************/
int Abc_NtkDontCareWinAddMissing_rec( Odc_Man_t * p, Abc_Obj_t * pObj )
{
    Abc_Obj_t * pFanin;
    int i;
    // skip the already collected leaves and branches
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return 1;
    // if this is not an internal node - make it a new branch
    if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves )
    {
        Abc_NodeSetTravIdCurrent( pObj );
        Vec_PtrPush( p->vBranches, pObj );
        return Vec_PtrSize(p->vBranches) <= 32;
    }
    // visit the fanins of the node
    Abc_ObjForEachFanin( pObj, pFanin, i )
        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) )
            return 0;
    return 1;
}

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

  Synopsis    [Adds to the window nodes and leaves in the TFI of the roots.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareWinAddMissing( Odc_Man_t * p )
{
    Abc_Obj_t * pObj;
    int i;
    // set the leaves
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
        Abc_NodeSetTravIdCurrent( pObj );        
    // explore from the roots
    Vec_PtrClear( p->vBranches );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) )
            return 0;
    return 1;
}

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

  Synopsis    [Computes window for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareWindow( Odc_Man_t * p )
{
    // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
    Abc_NtkDontCareWinSweepLeafTfo( p );
    // find the roots of the window
    Abc_NtkDontCareWinCollectRoots( p );
    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
    {
//        printf( "Empty window\n" );
        return 0;
    }
    // add the nodes in the TFI of the roots that are not yet in the window
    if ( !Abc_NtkDontCareWinAddMissing( p ) )
    {
//        printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) );
        return 0;
    }
    return 1;
}


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

  Synopsis    [Performing hashing of two AIG Literals.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned Odc_HashKey( Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize ) 
{
    unsigned Key = 0;
    Key ^= Odc_Regular(iFan0) * 7937;
    Key ^= Odc_Regular(iFan1) * 2971;
    Key ^= Odc_IsComplement(iFan0) * 911;
    Key ^= Odc_IsComplement(iFan1) * 353;
    return Key % TableSize;
}

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

  Synopsis    [Checks if the given name node already exists in the table.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Odc_Lit_t * Odc_HashLookup( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
{
    Odc_Obj_t * pObj;
    Odc_Lit_t * pEntry;
    unsigned uHashKey;
    assert( iFan0 < iFan1 );
    // get the hash key for this node
    uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize );
    // remember the spot in the hash table that will be used
    if ( p->pTable[uHashKey] == 0 )
        Vec_IntPush( p->vUsedSpots, uHashKey );
    // find the entry
    for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext )
    {
        pObj = Odc_Lit2Obj( p, *pEntry );
        if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 )
            return pEntry;
    }
    return pEntry;
}

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

  Synopsis    [Finds node by structural hashing or creates a new node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Odc_Lit_t Odc_And( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
{
    Odc_Obj_t * pObj;
    Odc_Lit_t * pEntry;
    unsigned uMask0, uMask1;
    int Temp;
    // consider trivial cases
    if ( iFan0 == iFan1 )
        return iFan0;
    if ( iFan0 == Odc_Not(iFan1) )
        return Odc_Const0();
    if ( Odc_Regular(iFan0) == Odc_Const1() )
        return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0();
    if ( Odc_Regular(iFan1) == Odc_Const1() )
        return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0();
    // canonicize the fanin order
    if ( iFan0 > iFan1 )
        Temp = iFan0, iFan0 = iFan1, iFan1 = Temp;
    // check if a node with these fanins exists
    pEntry = Odc_HashLookup( p, iFan0, iFan1 );
    if ( *pEntry )
        return *pEntry;
    // create a new node
    pObj = Odc_ObjNew( p );
    pObj->iFan0 = iFan0;
    pObj->iFan1 = iFan1;
    pObj->iNext = 0;
    pObj->TravId = 0;
    // set the mask
    uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask;
    uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask;
    pObj->uMask = uMask0 | uMask1;
    // add to the table
    *pEntry = Odc_Obj2Lit( p, pObj );
    return *pEntry;
}

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

  Synopsis    [Boolean OR.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Odc_Lit_t Odc_Or( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
{
    return Odc_Not( Odc_And(p, Odc_Not(iFan0), Odc_Not(iFan1)) );
}

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

  Synopsis    [Boolean XOR.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Odc_Lit_t Odc_Xor( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
{
    return Odc_Or( p, Odc_And(p, iFan0, Odc_Not(iFan1)), Odc_And(p, Odc_Not(iFan0), iFan1) );
}


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

  Synopsis    [Transfers the window into the AIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t * pPivot )
{
    unsigned uData0, uData1;
    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
    assert( !Abc_ObjIsComplement(pNode) );
    // skip visited objects
    if ( Abc_NodeIsTravIdCurrent(pNode) )
        return pNode->pCopy;
    Abc_NodeSetTravIdCurrent(pNode);
    assert( Abc_ObjIsNode(pNode) );
    // consider the case when the node is the pivot
    if ( pNode == pPivot )
        return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
    // compute the cofactors
    uData0 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
    uData1 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
    // find the 0-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
    uRes0 = Odc_And( p, uLit0, uLit1 );
    // find the 1-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
    uRes1 = Odc_And( p, uLit0, uLit1 );
    // find the result
    return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uRes1 << 16) | uRes0);
}

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

  Synopsis    [Transfers the window into the AIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareTransfer( Odc_Man_t * p )
{
    Abc_Obj_t * pObj;
    Odc_Lit_t uRes0, uRes1;
    Odc_Lit_t uLit;
    unsigned uData;
    int i;
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    // set elementary variables at the leaves 
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
    {
        uLit = Odc_Var( p, i );
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
        Abc_NodeSetTravIdCurrent(pObj);
    }
    // set elementary variables at the branched 
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vBranches, pObj, i )
    {
        uLit = Odc_Var( p, i+p->nVarsMax );
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
        Abc_NodeSetTravIdCurrent(pObj);
    }
    // compute the AIG for the window
    p->iRoot = Odc_Const0();
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
    {
        uData = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
        // get the cofactors
        uRes0 = uData & 0xffff;
        uRes1 = uData >> 16;
        // compute the miter
//        assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root
        uLit = Odc_Xor( p, uRes0, uRes1 );
        p->iRoot = Odc_Or( p, p->iRoot, uLit );
    }
    return 1;
}


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

  Synopsis    [Recursively computes the pair of cofactors.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uMask )
{
    Odc_Obj_t * pObj;
    unsigned uData0, uData1;
    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
    assert( !Odc_IsComplement(Lit) );
    // skip visited objects
    pObj = Odc_Lit2Obj( p, Lit );
    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
        return pObj->uData;
    Odc_ObjSetTravIdCurrent(p, pObj);
    // skip objects out of the cone
    if ( (pObj->uMask & uMask) == 0 )
        return pObj->uData = ((Lit << 16) | Lit);
    // consider the case when the node is the var
    if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) )
        return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0());
    // compute the cofactors
    uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask );
    uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask );
    // find the 0-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) );
    uRes0 = Odc_And( p, uLit0, uLit1 );
    // find the 1-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
    uRes1 = Odc_And( p, uLit0, uLit1 );
    // find the result
    return pObj->uData = ((uRes1 << 16) | uRes0);
}

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

  Synopsis    [Quantifies the branch variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareQuantify( Odc_Man_t * p )
{   
    Odc_Lit_t uRes0, uRes1;
    unsigned uData;
    int i;
    assert( p->iRoot < 0xffff );
    assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
    for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
    {
        // compute the cofactors w.r.t. this variable
        Odc_ManIncrementTravId( p );
        uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
        uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
        uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16),    Odc_IsComplement(p->iRoot) );
        // quantify this variable existentially
        p->iRoot = Odc_Or( p, uRes0, uRes1 );
        // check the limit
        if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 )
            return 0;
    }
    assert( p->nObjs <= p->nObjsAlloc );
    return 1;
}


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

  Synopsis    [Set elementary truth tables for PIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareSimulateSetElem2( Odc_Man_t * p )
{
    unsigned * pData;
    int i, k;
    for ( k = 0; k < p->nVarsMax; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        Abc_InfoClear( pData, p->nWords );
        for ( i = 0; i < p->nBits; i++ )
            if ( i & (1 << k) )
                pData[i>>5] |= (1 << (i&31));
    }
}

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

  Synopsis    [Set elementary truth tables for PIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareSimulateSetElem( Odc_Man_t * p )
{
    unsigned * pData, * pData2;
    int k;
    for ( k = 0; k < p->nVarsMax; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        pData2 = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
        Abc_InfoCopy( pData, pData2, p->nWords );
    }
}

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

  Synopsis    [Set random simulation words for PIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareSimulateSetRand( Odc_Man_t * p )
{
    unsigned * pData;
    int w, k, Number;
    for ( w = 0; w < p->nWords; w++ )
    {
        Number = rand();
        for ( k = 0; k < p->nVarsMax; k++ )
        {
            pData = Odc_ObjTruth( p, Odc_Var(p, k) );
            pData[w] = (Number & (1<<k)) ? ~0 : 0;
        }
    }
}

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

  Synopsis    [Set random simulation words for PIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareCountMintsWord( Odc_Man_t * p, unsigned * puTruth )
{
    int w, Counter = 0;
    for ( w = 0; w < p->nWords; w++ )
        if ( puTruth[w] )
            Counter++;
    return Counter;
}

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

  Synopsis    [Simulates one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareTruthOne( Odc_Man_t * p, Odc_Lit_t Lit )
{
    Odc_Obj_t * pObj;
    unsigned * pInfo, * pInfo1, * pInfo2;
    int k, fComp1, fComp2;
    assert( !Odc_IsComplement( Lit ) );
    assert( !Odc_IsTerm( p, Lit ) );
    // get the truth tables
    pObj   = Odc_Lit2Obj( p, Lit );
    pInfo  = Odc_ObjTruth( p, Lit );
    pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) );
    pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) );
    fComp1 = Odc_ObjFaninC0( pObj );
    fComp2 = Odc_ObjFaninC1( pObj );
    // simulate
    if ( fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
    else if ( fComp1 && !fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
    else if ( !fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
    else // if ( fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] =  pInfo1[k] &  pInfo2[k];
}

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

  Synopsis    [Computes the truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDontCareSimulate_rec( Odc_Man_t * p, Odc_Lit_t Lit )
{
    Odc_Obj_t * pObj;
    assert( !Odc_IsComplement(Lit) );
    // skip terminals
    if ( Odc_IsTerm(p, Lit) )
        return;
    // skip visited objects
    pObj = Odc_Lit2Obj( p, Lit );
    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
        return;
    Odc_ObjSetTravIdCurrent(p, pObj);
    // call recursively
    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) );
    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) );
    // construct the truth table
    Abc_NtkDontCareTruthOne( p, Lit );
}

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

  Synopsis    [Computes the truth table of the care set.]

  Description [Returns the number of ones in the simulation info.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareSimulate( Odc_Man_t * p, unsigned * puTruth )
{
    Odc_ManIncrementTravId( p );
    Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) );
    Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords );
    if ( Odc_IsComplement(p->iRoot) )
        Abc_InfoNot( puTruth, p->nWords );
    return Extra_TruthCountOnes( puTruth, p->nVarsMax );
}

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

  Synopsis    [Computes the truth table of the care set.]

  Description [Returns the number of ones in the simulation info.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
{
    int nIters = 2;
    int nRounds, Counter, r;
    // decide how many rounds to simulate
    nRounds = p->nBits / p->nWords;
    Counter = 0;
    for ( r = 0; r < nIters; r++ )
    {
        Abc_NtkDontCareSimulateSetRand( p );
        Abc_NtkDontCareSimulate( p, puTruth );
        Counter += Abc_NtkDontCareCountMintsWord( p, puTruth );
    }
    // normalize
    Counter = Counter * nRounds / nIters;
    return Counter;
}

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

  Synopsis    [Computes ODCs for the node in terms of the cut variables.]

  Description [Returns the number of don't care minterms in the truth table.
  In particular, this procedure returns 0 if there is no don't-cares.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
{
    int nMints, RetValue;
    abctime clk, clkTotal = Abc_Clock();

    p->nWins++;
    
    // set the parameters
    assert( !Abc_ObjIsComplement(pNode) );
    assert( Abc_ObjIsNode(pNode) );
    assert( Vec_PtrSize(vLeaves) <= p->nVarsMax );
    p->vLeaves = vLeaves;
    p->pNode = pNode;

    // compute the window
clk = Abc_Clock();
    RetValue = Abc_NtkDontCareWindow( p );
p->timeWin += Abc_Clock() - clk;
    if ( !RetValue )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        Abc_InfoFill( puTruth, p->nWords );
        p->nWinsEmpty++;        
        return 0;
    }

    if ( p->fVeryVerbose )
    {
        printf( " %5d : ", pNode->Id );
        printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) );
        printf( "Root = %2d ", Vec_PtrSize(p->vRoots) );
        printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) );
        printf( " |  " );
    }

    // transfer the window into the AIG package
clk = Abc_Clock();
    Abc_NtkDontCareTransfer( p );
p->timeMiter += Abc_Clock() - clk;

    // simulate to estimate the amount of don't-cares
clk = Abc_Clock();
    nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
p->timeSim += Abc_Clock() - clk;
    if ( p->fVeryVerbose )
    {
        printf( "AIG = %5d ", Odc_NodeNum(p) );
        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
    }

    // if there is less then the given percentage of don't-cares, skip
    if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        if ( p->fVeryVerbose )
            printf( "Simulation cutoff.\n" );
        Abc_InfoFill( puTruth, p->nWords );
        p->nSimsEmpty++;
        return 0;
    }

    // quantify external variables
clk = Abc_Clock();
    RetValue = Abc_NtkDontCareQuantify( p );
p->timeQuant += Abc_Clock() - clk;
    if ( !RetValue )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        if ( p->fVeryVerbose )
            printf( "=== Overflow! ===\n" );
        Abc_InfoFill( puTruth, p->nWords );
        p->nQuantsOver++;
        return 0;
    }

    // get the truth table
clk = Abc_Clock();
    Abc_NtkDontCareSimulateSetElem( p );
    nMints = Abc_NtkDontCareSimulate( p, puTruth );
p->timeTruth += Abc_Clock() - clk;
    if ( p->fVeryVerbose )
    {
        printf( "AIG = %5d ", Odc_NodeNum(p) );
        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
        printf( "\n" );
    }
p->timeTotal += Abc_Clock() - clkTotal;
    p->nWinsFinish++;
    p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
    return nMints;
}


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


ABC_NAMESPACE_IMPL_END