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

  FileName    [saigMiter.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Computes sequential miter of two sequential AIGs.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "saig.h"
#include "proof/fra/fra.h"

ABC_NAMESPACE_IMPL_START

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

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

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

  Synopsis    [Checks the status of the miter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p )
{
    Sec_MtrStatus_t Status;
    Aig_Obj_t * pObj, * pChild;
    int i;
    memset( &Status, 0, sizeof(Sec_MtrStatus_t) );
    Status.iOut = -1;
    Status.nInputs  = Saig_ManPiNum( p );
    Status.nNodes   = Aig_ManNodeNum( p );
    Status.nOutputs = Saig_ManPoNum(p);
    Saig_ManForEachPo( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
            Status.nUnsat++;
        // check if the output is constant 1
        else if ( pChild == Aig_ManConst1(p) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
        // check if the output is a primary input
        else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
    // check if the output is 1 for the 0000 pattern
        else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            Status.nSat++;
            if ( Status.iOut == -1 )
                Status.iOut = i;
        }
        else
            Status.nUndec++;
    }
    return Status;
}

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

  Synopsis    [Creates sequential miter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Saig_ManRegNum(p0) > 0 || Saig_ManRegNum(p1) > 0 );
    assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
    assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
    pNew->pName = Abc_UtilStrsav( "miter" );
    Aig_ManCleanData( p0 );
    Aig_ManCleanData( p1 );
    // map constant nodes
    Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
    // map primary inputs
    Saig_ManForEachPi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachPi( p1, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    // map register outputs
    Saig_ManForEachLo( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachLo( p1, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    // map internal nodes
    Aig_ManForEachNode( p0, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Aig_ManForEachNode( p1, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create primary outputs
    Saig_ManForEachPo( p0, pObj, i )
    {
        if ( Oper == 0 ) // XOR
            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
        else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1)  ...  complement is PO(p0) & !PO(p1) 
            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
        else
            assert( 0 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    // create register inputs
    Saig_ManForEachLi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Saig_ManForEachLi( p1, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // cleanup
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
//    Aig_ManCleanup( pNew );
    return pNew;
}

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

  Synopsis    [Creates combinational miter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
    pNew->pName = Abc_UtilStrsav( "miter" );
    // map constant nodes
    Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
    // map primary inputs and register outputs
    Aig_ManForEachCi( p0, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Aig_ManForEachCi( p1, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    // map internal nodes
    Aig_ManForEachNode( p0, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Aig_ManForEachNode( p1, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create primary outputs
    Aig_ManForEachCo( p0, pObj, i )
    {
        if ( Oper == 0 ) // XOR
            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
        else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1)  ...  complement is PO(p0) & !PO(p1) 
            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
        else
            assert( 0 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    // cleanup
    Aig_ManSetRegNum( pNew, 0 );
    Aig_ManCleanup( pNew );
    return pNew;
}

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

  Synopsis    [Derives dual-rail AIG.]

  Description [Orders nodes as follows: PIs, ANDs, POs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_AndDualRail( Aig_Man_t * pNew, Aig_Obj_t * pObj, Aig_Obj_t ** ppData, Aig_Obj_t ** ppNext )
{
    Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
    Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
    Aig_Obj_t * p0Data = Aig_ObjFaninC0(pObj)? pFanin0->pNext              : (Aig_Obj_t *)pFanin0->pData;
    Aig_Obj_t * p0Next = Aig_ObjFaninC0(pObj)? (Aig_Obj_t *)pFanin0->pData : pFanin0->pNext;
    Aig_Obj_t * p1Data = Aig_ObjFaninC1(pObj)? pFanin1->pNext              : (Aig_Obj_t *)pFanin1->pData;
    Aig_Obj_t * p1Next = Aig_ObjFaninC1(pObj)? (Aig_Obj_t *)pFanin1->pData : pFanin1->pNext;
    *ppData = Aig_Or( pNew, 
        Aig_And(pNew, p0Data, Aig_Not(p0Next)),
        Aig_And(pNew, p1Data, Aig_Not(p1Next)) );
    *ppNext = Aig_And( pNew, 
        Aig_And(pNew, Aig_Not(p0Data), p0Next),
        Aig_And(pNew, Aig_Not(p1Data), p1Next) );
}

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

  Synopsis    [Derives dual-rail AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pMiter;
    int i;
    Aig_ManCleanData( p );
    Aig_ManCleanNext( p );
    // create the new manager
    pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create the PIs 
    Aig_ManConst1(p)->pData = Aig_ManConst0(pNew);
    Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
    {
        pObj->pData = Aig_ObjCreateCi( pNew );
        pObj->pNext = Aig_ObjCreateCi( pNew );
    }
    // duplicate internal nodes
    Aig_ManForEachNode( p, pObj, i )
        Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext );
    // add the POs
    if ( fMiter )
    {
        pMiter = Aig_ManConst1(pNew);
        Saig_ManForEachLo( p, pObj, i )
        {
            pMiter = Aig_And( pNew, pMiter, 
                Aig_Or(pNew, (Aig_Obj_t *)pObj->pData, pObj->pNext) );
        } 
        Aig_ObjCreateCo( pNew, pMiter );
        Saig_ManForEachLi( p, pObj, i )
        {
            if ( !Aig_ObjFaninC0(pObj) )
            {
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
            }
            else
            {
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
            }
        }
    }
    else
    {
        Aig_ManForEachCo( p, pObj, i )
        {
            if ( !Aig_ObjFaninC0(pObj) )
            {
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
            }
            else
            {
                Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
            }
        }
    }
    Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) );
    Aig_ManCleanData( p );
    Aig_ManCleanNext( p );
    Aig_ManCleanup( pNew );
    // check the resulting network
    if ( !Aig_ManCheck(pNew) )
        printf( "Aig_ManDupSimple(): The check has failed.\n" );
    return pNew;
}

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

  Synopsis    [Create combinational timeframes by unrolling sequential circuits.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
{
    Aig_Man_t * p, * pAig;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f;
//    assert( nFrames > 1 );
    assert( Saig_ManPiNum(pBot) == Saig_ManPiNum(pTop) );
    assert( Saig_ManPoNum(pBot) == Saig_ManPoNum(pTop) );
    assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) );
    assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 );
    // start timeframes
    p = Aig_ManStart( nFrames * Abc_MaxInt(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
    p->pName = Abc_UtilStrsav( "frames" );
    // create variables for register outputs
    pAig = pBot;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( p );
    // add timeframes
    for ( f = 0; f < nFrames; f++ )
    {
        // create PI nodes for this frame
        Aig_ManConst1(pAig)->pData = Aig_ManConst1( p );
        Saig_ManForEachPi( pAig, pObj, i )
            pObj->pData = Aig_ObjCreateCi( p );
        // add internal nodes of this frame
        Aig_ManForEachNode( pAig, pObj, i )
            pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
        if ( f == nFrames - 1 )
        {
            // create POs for this frame
            Aig_ManForEachCo( pAig, pObj, i )
                Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) );
            break;
        }
        // create POs for this frame
        Saig_ManForEachPo( pAig, pObj, i )
            Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) );
        // save register inputs
        Saig_ManForEachLi( pAig, pObj, i )
            pObj->pData = Aig_ObjChild0Copy(pObj);
        // transfer to register outputs
        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
            pObjLo->pData = pObjLi->pData;
        if ( f == 0 )
        {
            // transfer from pOld to pNew
            Saig_ManForEachLo( pAig, pObj, i )
                Saig_ManLo(pTop, i)->pData = pObj->pData;
            pAig = pTop;
        }
    }
    Aig_ManCleanup( p );
    return p;
}

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

  Synopsis    [Duplicates the AIG while creating POs from the set.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet )
{
    Aig_Man_t * pNew, * pCopy;
    Aig_Obj_t * pObj;
    int i;
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
//    Saig_ManForEachPo( p, pObj, i )
//        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) );
    Saig_ManForEachLi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
    // cleanup and return a copy
    Aig_ManSeqCleanup( pNew );
    pCopy = Aig_ManDupSimpleDfs( pNew );
    Aig_ManStop( pNew );
    return pCopy;
}

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

  Synopsis    [Duplicates the AIG while creating POs from the set.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
{
    Aig_Man_t * pNew, * pCopy;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanData( p );
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Saig_ManForEachPi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    if ( iPart == 0 )
    {
        Saig_ManForEachLo( p, pObj, i )
            if ( i < Saig_ManRegNum(p)/2 )
                pObj->pData = Aig_ObjCreateCi( pNew );
    }
    else
    {
        Saig_ManForEachLo( p, pObj, i )
            if ( i >= Saig_ManRegNum(p)/2 )
                pObj->pData = Aig_ObjCreateCi( pNew );
    }
    Aig_ManForEachNode( p, pObj, i )
        if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
//    Saig_ManForEachPo( p, pObj, i )
//        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i )
    {
        assert( Aig_Regular(pObj)->pData != NULL );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) );
    }
    if ( iPart == 0 )
    {
        Saig_ManForEachLi( p, pObj, i )
            if ( i < Saig_ManRegNum(p)/2 )
                pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    else
    {
        Saig_ManForEachLi( p, pObj, i )
            if ( i >= Saig_ManRegNum(p)/2 )
                pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p)/2 );
    // cleanup and return a copy
//    Aig_ManSeqCleanup( pNew );
    Aig_ManCleanup( pNew );
    pCopy = Aig_ManDupSimpleDfs( pNew );
    Aig_ManStop( pNew );
    return pCopy;
}

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

  Synopsis    [Duplicates the AIG to have constant-0 initial state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
    Vec_Ptr_t * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
    int i, Counter = 0;
    assert( Saig_ManRegNum(p) % 2 == 0 );
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        pFanin = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsConst1( pFanin ) )
        {
            if ( !Aig_ObjFaninC0(pObj) )
                printf( "The output number %d of the miter is constant 1.\n", i );
            Counter++;
            continue;
        }
        if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
        {
            printf( "The miter cannot be demitered.\n" );
            Vec_PtrFree( vSet0 );
            Vec_PtrFree( vSet1 );
            return 0;
        }
        if ( Aig_ObjFaninC0(pObj) )
            pObj0 = Aig_Not(pObj0);

//        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
        {
            Vec_PtrPush( vSet0, pObj0 );
            Vec_PtrPush( vSet1, pObj1 );
        }
        else
        {
            Vec_PtrPush( vSet0, pObj1 );
            Vec_PtrPush( vSet1, pObj0 );
        }
    }
//    printf( "Miter has %d constant outputs.\n", Counter );
//    printf( "\n" );
    if ( ppAig0 )
    {
        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
        ABC_FREE( (*ppAig0)->pName );
        (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    }
    if ( ppAig1 )
    {
        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
        ABC_FREE( (*ppAig1)->pName );
        (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    }
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    return 1;
}

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

  Synopsis    [Returns 1 if PO can be demitered.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManDemiterMarkPos( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanMarkAB( p );
    Saig_ManForEachLo( p, pObj, i )
        if ( i < Saig_ManRegNum(p)/2 )
            pObj->fMarkA = 1;
        else
            pObj->fMarkB = 1;
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB | Aig_ObjFanin1(pObj)->fMarkB;
    }
}

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

  Synopsis    [Returns 1 if PO can be demitered.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0, Aig_Obj_t ** ppPo1 )
{
    Aig_Obj_t * pFanin, * pObj0, * pObj1, * pObjR0, * pObjR1;
    assert( Saig_ObjIsPo(p, pObj) );
    pFanin = Aig_ObjFanin0( pObj );
    if ( Aig_ObjIsConst1(pFanin) )
    {
        if ( !Aig_ObjFaninC0(pObj) )
            return 0;
        *ppPo0 = Aig_ManConst0(p);
        *ppPo1 = Aig_ManConst0(p);
        return 1;
    }
    if ( !Aig_ObjIsNode(pFanin) )
        return 0;
    if ( !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
        return 0;
    if ( Aig_ObjFaninC0(pObj) )
        pObj0 = Aig_Not(pObj0);
    // make sure they can reach only one
    pObjR0 = Aig_Regular(pObj0);
    pObjR1 = Aig_Regular(pObj1);
    if ( (pObjR0->fMarkA && pObjR0->fMarkB) || (pObjR1->fMarkA && pObjR1->fMarkB) || 
         (pObjR0->fMarkA && pObjR1->fMarkA) || (pObjR0->fMarkB && pObjR1->fMarkB) )
         return 0;

    if ( pObjR1->fMarkA && !pObjR0->fMarkA )
    {
        *ppPo0 = pObj1;
        *ppPo1 = pObj0;
    }
    else if ( pObjR0->fMarkA && !pObjR1->fMarkA )
    {
        *ppPo0 = pObj0;
        *ppPo1 = pObj1;
    }
    else
    {
/*
printf( "%d", pObjR0->fMarkA );
printf( "%d", pObjR0->fMarkB );
printf( ":" );
printf( "%d", pObjR1->fMarkA );
printf( "%d", pObjR1->fMarkB );
printf( "   " );
*/
        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
        {
            *ppPo0 = pObj0;
            *ppPo1 = pObj1;
        }
        else
        {
            *ppPo0 = pObj1;
            *ppPo1 = pObj0;
        }
    }
    return 1;
}

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

  Synopsis    [Returns 1 if AIG can be demitered.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
    Vec_Ptr_t * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pObj0, * pObj1;
    int i;
    if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) )
        return 0;
    Saig_ManDemiterMarkPos( p );
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) )
        {
            Vec_PtrFree( vSet0 );
            Vec_PtrFree( vSet1 );
            Aig_ManCleanMarkAB( p );
            return 0;
        }
        Vec_PtrPush( vSet0, pObj0 );
        Vec_PtrPush( vSet1, pObj1 );
    }
    // create new AIG
    *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
    ABC_FREE( (*ppAig0)->pName );
    (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    // create new AIGs
    *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
    ABC_FREE( (*ppAig1)->pName );
    (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    // cleanup
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    Aig_ManCleanMarkAB( p );
    return 1;
}

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

  Synopsis    [Returns 1 if AIG can be demitered.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
    Aig_Man_t * pTemp;
    Aig_Obj_t * pObj;
    int i, k;

    if ( p->pFanData )
        Aig_ManFanoutStop( p );

    k = 0;
    pTemp = Aig_ManDupSimple( p );
    Saig_ManForEachPo( pTemp, pObj, i )
    {
        if ( i & 1 )
            Aig_ObjDeletePo( pTemp, pObj );
        else
            Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    }
    Saig_ManForEachLi( pTemp, pObj, i )
        Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    Vec_PtrShrink( pTemp->vCos, k );
    pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
    Aig_ManSeqCleanup( pTemp );
    *ppAig0 = Aig_ManDupSimple( pTemp );
    Aig_ManStop( pTemp );

    k = 0;
    pTemp = Aig_ManDupSimple( p );
    Saig_ManForEachPo( pTemp, pObj, i )
    {
        if ( i & 1 )
            Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
        else
            Aig_ObjDeletePo( pTemp, pObj );
    }
    Saig_ManForEachLi( pTemp, pObj, i )
        Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
    Vec_PtrShrink( pTemp->vCos, k );
    pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
    Aig_ManSeqCleanup( pTemp );
    *ppAig1 = Aig_ManDupSimple( pTemp );
    Aig_ManStop( pTemp );

    return 1;
}

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

  Synopsis    [Duplicates the AIG to have constant-0 initial state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterSimpleDiff_old( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
    Vec_Ptr_t * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
    int i, Counter = 0;
//    assert( Saig_ManRegNum(p) % 2 == 0 );
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        pFanin = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsConst1( pFanin ) )
        {
            if ( !Aig_ObjFaninC0(pObj) )
                printf( "The output number %d of the miter is constant 1.\n", i );
            Counter++;
            continue;
        } 
        if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
        {
/*
            printf( "The miter cannot be demitered.\n" );
            Vec_PtrFree( vSet0 );
            Vec_PtrFree( vSet1 );
            return 0;
*/
            printf( "The output number %d cannot be demitered.\n", i );
            continue;
        }
        if ( Aig_ObjFaninC0(pObj) )
            pObj0 = Aig_Not(pObj0);

//        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
        {
            Vec_PtrPush( vSet0, pObj0 );
            Vec_PtrPush( vSet1, pObj1 );
        }
        else
        {
            Vec_PtrPush( vSet0, pObj1 );
            Vec_PtrPush( vSet1, pObj0 );
        }
    }
//    printf( "Miter has %d constant outputs.\n", Counter );
//    printf( "\n" );
    if ( ppAig0 )
    {
        *ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
        ABC_FREE( (*ppAig0)->pName );
        (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    }
    if ( ppAig1 )
    {
        *ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
        ABC_FREE( (*ppAig1)->pName );
        (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    }
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    return 1;
}

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

  Synopsis    [Labels logic reachable from the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManDemiterLabel_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Value ) 
        pObj->fMarkB = 1;
    else
        pObj->fMarkA = 1;
    if ( Saig_ObjIsPi(p, pObj) )
        return;
    if ( Saig_ObjIsLo(p, pObj) )
    {
        Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ), Value );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0(pObj), Value );
    Saig_ManDemiterLabel_rec( p, Aig_ObjFanin1(pObj), Value );
}

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

  Synopsis    [Returns the first labeled register encountered during traversal.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Obj_t * Saig_ManGetLabeledRegister_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pResult;
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return NULL;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Saig_ObjIsPi(p, pObj) )
        return NULL;
    if ( Saig_ObjIsLo(p, pObj) )
    {
        if ( pObj->fMarkA || pObj->fMarkB )
            return pObj;
        return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ) );
    }
    assert( Aig_ObjIsNode(pObj) );
    pResult = Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0(pObj) );
    if ( pResult )
        return pResult;
    return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin1(pObj) );
}

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

  Synopsis    [Duplicates the AIG to have constant-0 initial state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
    Vec_Ptr_t * vPairs, * vSet0, * vSet1;
    Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1;
    int i, Counter;
    assert( Saig_ManRegNum(p) > 0 );
    Aig_ManSetCioIds( p );
    // check if demitering is possible
    vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) );
    Saig_ManForEachPo( p, pObj, i )
    {
        if ( !Aig_ObjRecognizeExor( Aig_ObjFanin0(pObj), &pObj0, &pObj1 ) )
        {
            Vec_PtrFree( vPairs );
            return 0;
        }
        Vec_PtrPush( vPairs, pObj0 );
        Vec_PtrPush( vPairs, pObj1 );
    }
    // start array of outputs
    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
    // get the first pair of outputs
    pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 0 );
    pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 1 );
    // label registers reachable from the outputs
    Aig_ManIncrementTravId( p );
    Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj0), 0 );
    Vec_PtrPush( vSet0, pObj0 );
    Aig_ManIncrementTravId( p );
    Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj1), 1 );
    Vec_PtrPush( vSet1, pObj1 );
    // find where each output belongs
    for ( i = 2; i < Vec_PtrSize(vPairs); i += 2 )
    {
        pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i   );
        pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i+1 );

        Aig_ManIncrementTravId( p );
        pFlop0 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj0) );

        Aig_ManIncrementTravId( p );
        pFlop1 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj1) );

        if ( (pFlop0->fMarkA && pFlop0->fMarkB) || (pFlop1->fMarkA && pFlop1->fMarkB) || 
             (pFlop0->fMarkA && pFlop1->fMarkA) || (pFlop0->fMarkB && pFlop1->fMarkB)  )
            printf( "Ouput pair %4d: Difficult case...\n", i/2 );

        if ( pFlop0->fMarkB )
        {
            Saig_ManDemiterLabel_rec( p, pObj0, 1 );
            Vec_PtrPush( vSet0, pObj0 );
        }
        else // if ( pFlop0->fMarkA ) or none
        {
            Saig_ManDemiterLabel_rec( p, pObj0, 0 );
            Vec_PtrPush( vSet1, pObj0 );
        }

        if ( pFlop1->fMarkB )
        {
            Saig_ManDemiterLabel_rec( p, pObj1, 1 );
            Vec_PtrPush( vSet0, pObj1 );
        }
        else // if ( pFlop1->fMarkA ) or none
        {
            Saig_ManDemiterLabel_rec( p, pObj1, 0 );
            Vec_PtrPush( vSet1, pObj1 );
        }
    }
    // check if there are any flops in common
    Counter = 0;
    Saig_ManForEachLo( p, pObj, i )
        if ( pObj->fMarkA && pObj->fMarkB )
            Counter++;
    if ( Counter > 0 )
        printf( "The miters contains %d flops reachable from both AIGs.\n", Counter );

    // produce two miters
    if ( ppAig0 )
    {
        assert( 0 );
        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
        ABC_FREE( (*ppAig0)->pName );
        (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
    }
    if ( ppAig1 )
    {
        assert( 0 );
        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
        ABC_FREE( (*ppAig1)->pName );
        (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
    }
    Vec_PtrFree( vSet0 );
    Vec_PtrFree( vSet1 );
    Vec_PtrFree( vPairs );
    return 1;
}


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

  Synopsis    [Create specialized miter by unrolling two circuits.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames )
{
    Aig_Man_t * pFrames0, * pFrames1, * pMiter;
//    assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
    pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames );
    pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames );
    pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 );
    Aig_ManStop( pFrames0 );
    Aig_ManStop( pFrames1 );
    return pMiter;
}


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

  Synopsis    [Resimulates counter-example and returns the failed output number.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs )
{
    Aig_Obj_t * pObj;
    int i, RetValue = -1;
    *pnOutputs = 0;
    Aig_ManConst1(p)->fMarkA = 1;
    Aig_ManForEachCi( p, pObj, i )
        pObj->fMarkA = pModel[i];
    Aig_ManForEachNode( p, pObj, i )
        pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & 
                      ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) );
    Aig_ManForEachCo( p, pObj, i )
        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
    Aig_ManForEachCo( p, pObj, i )
        if ( pObj->fMarkA )
        {
            if ( RetValue == -1 )
                RetValue = i;
            (*pnOutputs)++;
        }
    Aig_ManCleanMarkA(p);
    return RetValue;
}

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

  Synopsis    [Reduces SEC to CEC for the special case of seq synthesis.]

  Description [The first circuit (pPart0) should be circuit before synthesis.
  The second circuit (pPart1) should be circuit after synthesis.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose )
{
//    extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
    int iOut, nOuts;
    Aig_Man_t * pMiterCec;
    int RetValue;
    abctime clkTotal = Abc_Clock();
    if ( fVerbose )
    {
        Aig_ManPrintStats( pPart0 );
        Aig_ManPrintStats( pPart1 );
    }
//    Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL );
//    Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL );
//    assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) );
/*
    if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
    {
        printf( "Warning: The design after synthesis is smaller!\n" );
        printf( "This warning may indicate that the order of designs is changed.\n" );
        printf( "The solver expects the original design as first argument and\n" );
        printf( "the modified design as the second argument in \"absec\".\n" );
    }
*/
    // create two-level miter
    pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames );
    if ( fVerbose )
    {
        Aig_ManPrintStats( pMiterCec );
//        Aig_ManDumpBlif( pMiterCec, "miter01.blif", NULL, NULL );
//        printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
    }
    // run CEC on this miter
    RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose );
    // transfer model if given
//    if ( pNtk2 == NULL )
//        pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL;
    // report the miter
    if ( RetValue == 1 )
    {
        printf( "Networks are equivalent.  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
    }
    else if ( RetValue == 0 )
    {
        printf( "Networks are NOT EQUIVALENT.  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        if ( pMiterCec->pData == NULL )
            printf( "Counter-example is not available.\n" );
        else
        {
            iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts );
            if ( iOut == -1 )
                printf( "Counter-example verification has failed.\n" );
            else 
            {
                if ( iOut < Saig_ManPoNum(pPart0) * nFrames )
                    printf( "Primary output %d has failed in frame %d.\n", 
                        iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) );
                else
                    printf( "Flop input %d has failed in the last frame.\n", 
                        iOut - Saig_ManPoNum(pPart0) * nFrames );
                printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts );
            }
        }
    }
    else
    {
        printf( "Networks are UNDECIDED.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
    }
    fflush( stdout );
    Aig_ManStop( pMiterCec );
    return RetValue;
}

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

  Synopsis    [Reduces SEC to CEC for the special case of seq synthesis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose )
{
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
    if ( fVerbose )
        printf( "Performing sequential verification using combinational A/B miter.\n" );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            printf( "Demitering has failed.\n" );
            return -1;
        }
        if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) )
        {
            Aig_ManStop( pPart0 );
            Aig_ManStop( pPart1 );
            printf( "After demitering AIGs have different number of flops. Quitting.\n" );
            return -1;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( fVerbose )
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
        if ( p1 == NULL )
        {
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
//        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
        }
    }
    assert( Aig_ManRegNum(pPart0) > 0 );
    assert( Aig_ManRegNum(pPart1) > 0 );
    assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
    assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
    assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) );
    RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
    if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
        RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    return RetValue;
}


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

  Synopsis    [Performs demitering of the network.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManDemiterNew( Aig_Man_t * pMan )
{
    Vec_Ptr_t * vSuper, * vSupp0, * vSupp1;
    Aig_Obj_t * pObj, * pTemp, * pFan0, * pFan1;
    int i, k;
    vSuper = Vec_PtrAlloc( 100 );
    Saig_ManForEachPo( pMan, pObj, i )
    {
        if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs )
            break;
        printf( "Output %3d : ", i );
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
        {
            if ( !Aig_ObjFaninC0(pObj) )
                printf( "Const1\n" );
            else
                printf( "Const0\n" );
            continue;
        }
        if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
        {
            printf( "Terminal\n" );
            continue;
        }
        // check AND
        if ( !Aig_ObjFaninC0(pObj) )
        { 
            printf( "AND  " );
            if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
                printf( " Yes" );
            else
                printf( " No" );
            printf( "\n" );
            continue;
        }
        // check OR
        Aig_ObjCollectSuper( Aig_ObjFanin0(pObj), vSuper );
        printf( "OR with %d inputs    ", Vec_PtrSize(vSuper) );
        if ( Vec_PtrSize(vSuper) == 2 )
        {
            if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
            {
                printf( " Yes" );
                printf( "\n" );

                vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) );
                Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k )
                    if ( Saig_ObjIsLo(pMan, pTemp) )
                        printf( " %d", Aig_ObjCioId(pTemp) );
                printf( "\n" );
                Vec_PtrFree( vSupp0 );

                vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) );
                Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k )
                    if ( Saig_ObjIsLo(pMan, pTemp) )
                        printf( " %d", Aig_ObjCioId(pTemp) );
                printf( "\n" );
                Vec_PtrFree( vSupp1 );
            }
            else
                printf( " No" );
            printf( "\n" );
            continue;
        }
/*
        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
            if ( Aig_ObjRecognizeExor(Aig_Regular(pTemp), &pFan0, &pFan1) )
            {
                printf( " Yes" );
                if ( Aig_IsComplement(pTemp) )
                    pFan0 = Aig_Not(pFan0);
            }
            else
                printf( " No" );
*/
        printf( "\n" );
    }
    Vec_PtrFree( vSuper );
    return 1;
}

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


ABC_NAMESPACE_IMPL_END