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

  FileName    [sswPairs.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Calls to the SAT solver.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Reports the status of the miter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
{
    Aig_Obj_t * pObj, * pChild;
    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
//    if ( p->pData )
//        return 0;
    Saig_ManForEachPo( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
        {
            CountConst0++;
            continue;
        }
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output is a primary input
        if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            CountNonConst0++;
            continue;
        }
        CountUndecided++;
    }

    if ( fVerbose )
    {
        Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) );
        Abc_Print( 1, "Const0 = %d.  ", CountConst0 );
        Abc_Print( 1, "NonConst0 = %d.  ", CountNonConst0 );
        Abc_Print( 1, "Undecided = %d.  ", CountUndecided );
        Abc_Print( 1, "\n" );
    }

    if ( CountNonConst0 )
        return 0;
    if ( CountUndecided )
        return -1;
    return 1;
}

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

  Synopsis    [Transfer equivalent pairs to the miter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2 )
{
    Vec_Int_t * vIds;
    Aig_Obj_t * pObj1, * pObj2;
    Aig_Obj_t * pObj1m, * pObj2m;
    int i;
    vIds = Vec_IntAlloc( 2 * Vec_IntSize(vIds1) );
    for ( i = 0; i < Vec_IntSize(vIds1); i++ )
    {
        pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) );
        pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) );
        pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData);
        pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData);
        assert( pObj1m && pObj2m );
        if ( pObj1m == pObj2m )
            continue;
        if ( pObj1m->Id < pObj2m->Id )
        {
            Vec_IntPush( vIds, pObj1m->Id );
            Vec_IntPush( vIds, pObj2m->Id );
        }
        else
        {
            Vec_IntPush( vIds, pObj2m->Id );
            Vec_IntPush( vIds, pObj1m->Id );
        }
    }
    return vIds;
}

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

  Synopsis    [Transform pairs into class representation.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumMax )
{
    Vec_Int_t ** pvClasses;   // vector of classes
    int * pReprs;             // mapping nodes into their representatives
    int Entry, idObj, idRepr, idReprObj, idReprRepr, i;
    // allocate data-structures
    pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax );
    pReprs    = ABC_ALLOC( int, nObjNumMax );
    for ( i = 0; i < nObjNumMax; i++ )
        pReprs[i] = -1;
    // consider pairs
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        // get both objects
        idRepr = Vec_IntEntry( vPairs, i   );
        idObj  = Vec_IntEntry( vPairs, i+1 );
        assert( idObj > 0 );
        assert( (pReprs[idRepr] == -1) || (pvClasses[pReprs[idRepr]] != NULL) );
        assert( (pReprs[idObj]  == -1) || (pvClasses[pReprs[idObj] ] != NULL) );
        // get representatives of both objects
        idReprRepr = pReprs[idRepr];
        idReprObj  = pReprs[idObj];
        // check different situations
        if ( idReprRepr == -1 && idReprObj == -1 )
        {   // they do not have classes
            // create a class
            pvClasses[idRepr] = Vec_IntAlloc( 4 );
            Vec_IntPush( pvClasses[idRepr], idRepr );
            Vec_IntPush( pvClasses[idRepr], idObj );
            pReprs[ idRepr ] = idRepr;
            pReprs[ idObj  ] = idRepr;
        }
        else if ( idReprRepr >= 0 && idReprObj == -1 )
        {   // representative has a class
            // add iObj to the same class
            Vec_IntPushUniqueOrder( pvClasses[idReprRepr], idObj );
            pReprs[ idObj ] = idReprRepr;
        }
        else if ( idReprRepr == -1 && idReprObj >= 0 )
        {   // object has a class
            assert( idReprObj != idRepr );
            if ( idReprObj < idRepr )
            { // add idRepr to the same class
                Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr );
                pReprs[ idRepr ] = idReprObj;
            }
            else // if ( idReprObj > idRepr )
            { // make idRepr new representative
                Vec_IntPushFirst( pvClasses[idReprObj], idRepr );
                pvClasses[idRepr] = pvClasses[idReprObj];
                pvClasses[idReprObj] = NULL;
                // set correct representatives of each node
                Vec_IntForEachEntry( pvClasses[idRepr], Entry, i )
                    pReprs[ Entry ] = idRepr;
            }
        }
        else // if ( idReprRepr >= 0 && idReprObj >= 0 )
        {   // both have classes
            if ( idReprRepr == idReprObj )
            {  // the classes are the same
                // nothing to do
            }
            else
            {  // the classes are different
                // find the repr of the new class
                if ( idReprRepr < idReprObj )
                {
                    Vec_IntForEachEntry( pvClasses[idReprObj], Entry, i )
                    {
                        Vec_IntPushUniqueOrder( pvClasses[idReprRepr], Entry );
                        pReprs[ Entry ] = idReprRepr;
                    }
                    Vec_IntFree( pvClasses[idReprObj] );
                    pvClasses[idReprObj] = NULL;
                }
                else // if ( idReprRepr > idReprObj )
                {
                    Vec_IntForEachEntry( pvClasses[idReprRepr], Entry, i )
                    {
                        Vec_IntPushUniqueOrder( pvClasses[idReprObj], Entry );
                        pReprs[ Entry ] = idReprObj;
                    }
                    Vec_IntFree( pvClasses[idReprRepr] );
                    pvClasses[idReprRepr] = NULL;
                }
            }
        }
    }
    ABC_FREE( pReprs );
    return pvClasses;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
{
    int i;
    for ( i = 0; i < nObjNumMax; i++ )
        if ( pvClasses[i] )
            Vec_IntFree( pvClasses[i] );
    ABC_FREE( pvClasses );
}

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

  Synopsis    [Performs signal correspondence for the miter of two AIGs with node pairs defined.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
{
    Ssw_Man_t * p;
    Aig_Man_t * pAigNew, * pMiter;
    Ssw_Pars_t Pars;
    Vec_Int_t * vPairs;
    Vec_Int_t ** pvClasses;
    assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
    // create sequential miter
    pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
    Aig_ManCleanup( pMiter );
    // transfer information to the miter
    vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
    // create representation of the classes
    pvClasses = Ssw_TransformPairsIntoTempClasses( vPairs, Aig_ManObjNumMax(pMiter) );
    Vec_IntFree( vPairs );
    // if parameters are not given, create them
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // start the induction manager
    p = Ssw_ManCreate( pMiter, pPars );
    // create equivalence classes using these IDs
    p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
    p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
    Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
    // cleanup
    Ssw_FreeTempClasses( pvClasses, Aig_ManObjNumMax(pMiter) );
    Ssw_ManStop( p );
    Aig_ManStop( pMiter );
    return pAigNew;
}

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

  Synopsis    [Runs inductive SEC for the miter of two AIGs with node pairs defined.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
{
    Aig_Man_t * pAigNew, * pAigRes;
    Ssw_Pars_t Pars, * pPars = &Pars;
    Vec_Int_t * vIds1, * vIds2;
    Aig_Obj_t * pObj, * pRepr;
    int RetValue, i;
    abctime clk = Abc_Clock();
    Ssw_ManSetDefaultParams( pPars );
    pPars->fVerbose = 1;
    pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
    // record pairs of equivalent nodes
    vIds1 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
    vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData);
        if ( pRepr == NULL )
            continue;
        if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL )
            continue;
/*
        if ( Aig_ObjIsNode(pObj) )
            Abc_Print( 1, "n " );
        else if ( Saig_ObjIsPi(pAig, pObj) )
            Abc_Print( 1, "pi " );
        else if ( Saig_ObjIsLo(pAig, pObj) )
            Abc_Print( 1, "lo " );
*/
        Vec_IntPush( vIds1, Aig_ObjId(pObj) );
        Vec_IntPush( vIds2, Aig_ObjId(pRepr) );
    }
    Abc_Print( 1, "Recorded %d pairs (before: %d  after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
    // try the new AIGs
    pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars );
    Vec_IntFree( vIds1 );
    Vec_IntFree( vIds2 );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with the counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigNew );
    return pAigRes;
}

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

  Synopsis    [Runs inductive SEC for the miter of two AIGs with node pairs defined.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
{
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    assert( vIds1 != NULL && vIds2 != NULL );
    // try the new AIGs
    Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
    pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

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

  Synopsis    [Runs inductive SEC for the miter of two AIGs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
{
    Aig_Man_t * pAigRes, * pMiter;
    int RetValue;
    abctime clk = Abc_Clock();
    // try the new AIGs
    Abc_Print( 1, "Performing general verification without node pairs.\n" );
    pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
    Aig_ManCleanup( pMiter );
    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
    Aig_ManStop( pMiter );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

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

  Synopsis    [Runs inductive SEC for the miter of two AIGs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
{
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    // try the new AIGs
//    Abc_Print( 1, "Performing general verification without node pairs.\n" );
    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END