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

  FileName    [ivyCheck.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [And-Inverter Graph package.]

  Synopsis    [AIG checking procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - May 11, 2006.]

  Revision    [$Id: ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]

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

#include "ivy.h"

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

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

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

  Synopsis    [Checks the consistency of the AIG manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ivy_ManCheck( Ivy_Man_t * p )
{
    Ivy_Obj_t * pObj, * pObj2;
    int i;
    Ivy_ManForEachObj( p, pObj, i )
    {
        // skip deleted nodes
        if ( Ivy_ObjId(pObj) != i )
        {
            printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
            return 0;
        }
        // consider the constant node and PIs
        if ( i == 0 || Ivy_ObjIsPi(pObj) )
        {
            if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
            {
                printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsPo(pObj) )
        {
            if ( Ivy_ObjFaninId1(pObj) )
            {
                printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsBuf(pObj) )
        {
            if ( Ivy_ObjFanin1(pObj) )
            {
                printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsLatch(pObj) )
        {
            if ( Ivy_ObjFanin1(pObj) )
            {
                printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
                return 0;
            }
            if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
            {
                printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
                return 0;
            }
            pObj2 = Ivy_TableLookup( p, pObj );
            if ( pObj2 != pObj )
                printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
                continue;
        }
        // consider the AND node
        if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
        {
            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
            return 0;
        }
        if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
        {
            printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
            return 0;
        }
        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
        pObj2 = Ivy_TableLookup( p, pObj );
        if ( pObj2 != pObj )
            printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
        if ( Ivy_ObjRefs(pObj) == 0 )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
        // check fanouts
        if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
    }
    // count the number of nodes in the table
    if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
    {
        printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
        return 0;
    }
//    if ( !Ivy_ManCheckFanouts(p) )
//        return 0;
    if ( !Ivy_ManIsAcyclic(p) )
        return 0;
    return 1; 
}

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

  Synopsis    [Verifies the fanouts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ivy_ManCheckFanoutNums( Ivy_Man_t * p )
{
    Ivy_Obj_t * pObj;
    int i, Counter = 0;
    Ivy_ManForEachObj( p, pObj, i )
        if ( Ivy_ObjIsNode(pObj) )
            Counter += (Ivy_ObjRefs(pObj) == 0);
    if ( Counter )
        printf( "Sequential AIG has %d dangling nodes.\n", Counter );
    return Counter;
}

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

  Synopsis    [Verifies the fanouts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ivy_ManCheckFanouts( Ivy_Man_t * p )
{
    Vec_Ptr_t * vFanouts;
    Ivy_Obj_t * pObj, * pFanout, * pFanin;
    int i, k, RetValue = 1;
    if ( !p->fFanout )
        return 1;
    vFanouts = Vec_PtrAlloc( 100 );
    // make sure every fanin is a fanout
    Ivy_ManForEachObj( p, pObj, i )
    {
        pFanin = Ivy_ObjFanin0(pObj);
        if ( pFanin == NULL )
            continue;
        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
            if ( pFanout == pObj )
                break;
        if ( k == Vec_PtrSize(vFanouts) )
        {
            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
            RetValue = 0;
        }

        pFanin = Ivy_ObjFanin1(pObj);
        if ( pFanin == NULL )
            continue;
        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
            if ( pFanout == pObj )
                break;
        if ( k == Vec_PtrSize(vFanouts) )
        {
            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
            RetValue = 0;
        }
        // check that the previous fanout has the same fanin
        if ( pObj->pPrevFan0 )
        {
            if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
            {
                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
                RetValue = 0;
            }
        }
        // check that the previous fanout has the same fanin
        if ( pObj->pPrevFan1 )
        {
            if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
            {
                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
                RetValue = 0;
            }
        }
    }
    // make sure every fanout is a fanin
    Ivy_ManForEachObj( p, pObj, i )
    {
        Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
            if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
            {
                printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
                RetValue = 0;
            }
    }
    Vec_PtrFree( vFanouts );
    return RetValue;
}

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

  Synopsis    [Checks that each choice node has exactly one node with fanouts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ivy_ManCheckChoices( Ivy_Man_t * p )
{
    Ivy_Obj_t * pObj, * pTemp;
    int i;
    Ivy_ManForEachObj( p->pHaig, pObj, i )
    {
        if ( Ivy_ObjRefs(pObj) == 0 )
            continue;
        // count the number of nodes in the loop
        assert( !Ivy_IsComplement(pObj->pEquiv) );
        for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
            if ( Ivy_ObjRefs(pTemp) > 1 )
                printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
    }
    return 1;
}

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