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

  FileName    [disjunctiveMonotone.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Liveness property checking.]

  Synopsis    [Constraint analysis module for the k-Liveness algorithm
        invented by Koen Classen, Niklas Sorensson.]

  Author      [Sayak Ray]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - October 31, 2012.]

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

#include <stdio.h>
#include "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>
#include "base/main/mainInt.h"
#include "proof/pdr/pdr.h"
#include <time.h>

ABC_NAMESPACE_IMPL_START

struct aigPoIndices
{
    int attrPendingSignalIndex;
    int attrHintSingalBeginningMarker;
    int attrHintSingalEndMarker;
    int attrSafetyInvarIndex;
};

extern struct aigPoIndices *allocAigPoIndices();
extern void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices);
extern int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk);

struct antecedentConsequentVectorsStruct
{
    Vec_Int_t *attrAntecedents;
    Vec_Int_t *attrConsequentCandidates;
};

struct antecedentConsequentVectorsStruct *allocAntecedentConsequentVectorsStruct()
{
    struct antecedentConsequentVectorsStruct *newStructure;

    newStructure = (struct antecedentConsequentVectorsStruct *)malloc(sizeof (struct antecedentConsequentVectorsStruct));

    newStructure->attrAntecedents = NULL;
    newStructure->attrConsequentCandidates = NULL;
        
    assert( newStructure != NULL );
    return newStructure;
}

void deallocAntecedentConsequentVectorsStruct(struct antecedentConsequentVectorsStruct *toBeDeleted)
{
    assert( toBeDeleted != NULL );
    if(toBeDeleted->attrAntecedents) 
        Vec_IntFree( toBeDeleted->attrAntecedents );
    if(toBeDeleted->attrConsequentCandidates)
        Vec_IntFree( toBeDeleted->attrConsequentCandidates );
    free( toBeDeleted );
}

Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, 
                    struct antecedentConsequentVectorsStruct *anteConseVectors, int *startMonotonePropPo)
{
    Aig_Man_t *pNewAig;
    int iElem, i, nRegCount;
    int piCopied = 0, liCopied = 0, liCreated = 0, loCopied = 0, loCreated = 0;
    int poCopied = 0, poCreated = 0;
    Aig_Obj_t *pObj, *pObjPo, *pObjDriver, *pObjDriverNew, *pObjPendingDriverNew, *pObjPendingAndNextPending;
    Aig_Obj_t *pPendingFlop, *pObjConseCandFlop, *pObjSafetyInvariantPoDriver;
    //Vec_Ptr_t *vHintMonotoneLocalDriverNew;
    Vec_Ptr_t *vConseCandFlopOutput;
    //Vec_Ptr_t *vHintMonotoneLocalProp;

    Aig_Obj_t *pObjAnteDisjunction, *pObjConsecDriver, *pObjConsecDriverNew, *pObjCandMonotone, *pObjPrevCandMonotone, *pObjMonotonePropDriver;
    Vec_Ptr_t *vCandMonotoneProp;
    Vec_Ptr_t *vCandMonotoneFlopInput;

    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;

    Vec_Int_t *vAntecedentsLocal = anteConseVectors->attrAntecedents;
    Vec_Int_t *vConsequentCandidatesLocal = anteConseVectors->attrConsequentCandidates;

    if( vConsequentCandidatesLocal == NULL )
        return NULL; //no candidates for consequent is provided, hence no need to generate a new AIG

    
    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_monotone") + 2 );
    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "monotone");
        pNewAig->pSpec = NULL;

    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
        pObj = Aig_ManConst1( pAig );
        pObj->pData = Aig_ManConst1( pNewAig );

    //****************************************************************
        // Step 3: create true PIs
    //****************************************************************
        Saig_ManForEachPi( pAig, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
    }

    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
        Saig_ManForEachLo( pAig, pObj, i )
        {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
        }

    //****************************************************************
    // Step 6: create "D" register output for PENDING flop 
    //****************************************************************
    loCreated++;
    pPendingFlop = Aig_ObjCreateCi( pNewAig );

    //****************************************************************
    // Step 6.a: create "D" register output for HINT_MONOTONE flop 
    //****************************************************************
    vConseCandFlopOutput = Vec_PtrAlloc(Vec_IntSize(vConsequentCandidatesLocal));
    Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
    {
        loCreated++;
        pObjConseCandFlop = Aig_ObjCreateCi( pNewAig );
        Vec_PtrPush( vConseCandFlopOutput, pObjConseCandFlop );
    }

    nRegCount = loCreated + loCopied;

    //********************************************************************
    // Step 7: create internal nodes
    //********************************************************************
        Aig_ManForEachNode( pAig, pObj, i )
    {
        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
    
    //********************************************************************
    // Step 8: mapping appropriate new flop drivers 
    //********************************************************************

    if( aigPoIndicesArg->attrSafetyInvarIndex != -1 )
    {
        pObjPo = Aig_ManCo( pAig, aigPoIndicesArg->attrSafetyInvarIndex );
        pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
        pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
        pObjSafetyInvariantPoDriver = pObjDriverNew;
    }
    else
        pObjSafetyInvariantPoDriver = Aig_ManConst1(pNewAig);

    pObjPo = Aig_ManCo( pAig, pendingSignalIndexLocal );
    pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
    pObjPendingDriverNew = !Aig_IsComplement(pObjDriver)? 
                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));

    pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingDriverNew, pPendingFlop );

    pObjAnteDisjunction = Aig_Not(Aig_ManConst1( pNewAig ));
    if( vAntecedentsLocal )
    {
        Vec_IntForEachEntry( vAntecedentsLocal, iElem, i )
        {
            pObjPo = Aig_ManCo( pAig, iElem );
            pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
            pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
                    (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));

            pObjAnteDisjunction = Aig_Or( pNewAig, pObjDriverNew, pObjAnteDisjunction );
        }
    }

    vCandMonotoneProp = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
    vCandMonotoneFlopInput = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
    Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
    {
        pObjPo = Aig_ManCo( pAig, iElem );
        pObjConsecDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
        pObjConsecDriverNew = !Aig_IsComplement(pObjConsecDriver)? 
                    (Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData) : 
                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData));

        pObjCandMonotone = Aig_Or( pNewAig, pObjConsecDriverNew, pObjAnteDisjunction );
        pObjPrevCandMonotone = (Aig_Obj_t *)(Vec_PtrEntry( vConseCandFlopOutput, i ));
        pObjMonotonePropDriver = Aig_Or( pNewAig, Aig_Not( Aig_And( pNewAig, pObjPendingAndNextPending, pObjPrevCandMonotone ) ), 
                        pObjCandMonotone );

        //Conjunting safety invar
        pObjMonotonePropDriver = Aig_And( pNewAig, pObjMonotonePropDriver, pObjSafetyInvariantPoDriver );
                        
        Vec_PtrPush( vCandMonotoneFlopInput, pObjCandMonotone );
        Vec_PtrPush( vCandMonotoneProp, pObjMonotonePropDriver );
    }

    //********************************************************************
    // Step 9: create primary outputs 
    //********************************************************************
    Saig_ManForEachPo( pAig, pObj, i )
    {
        poCopied++;
        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
    }

    *startMonotonePropPo = i;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneProp, pObj, i )
    {
        poCreated++;
        pObjPo = Aig_ObjCreateCo( pNewAig, pObj ); 
    }

    //********************************************************************
    // Step 9: create latch inputs 
    //********************************************************************

    Saig_ManForEachLi( pAig, pObj, i )
    {
        liCopied++;
        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
    }
    
    //********************************************************************
    // Step 9.a: create latch input for PENDING_FLOP
    //********************************************************************

    liCreated++;
    Aig_ObjCreateCo( pNewAig, pObjPendingDriverNew );

    //********************************************************************
    // Step 9.b: create latch input for MONOTONE_FLOP
    //********************************************************************

    Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneFlopInput, pObj, i )
    {
        liCreated++;
        Aig_ObjCreateCo( pNewAig, pObj );
    }

    Aig_ManSetRegNum( pNewAig, nRegCount );
    Aig_ManCleanup( pNewAig );
    
    assert( Aig_ManCheck( pNewAig ) );
    assert( loCopied + loCreated == liCopied + liCreated );

    Vec_PtrFree(vConseCandFlopOutput);
    Vec_PtrFree(vCandMonotoneProp);
    Vec_PtrFree(vCandMonotoneFlopInput);
    return pNewAig;
}

Vec_Int_t *findNewDisjunctiveMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct antecedentConsequentVectorsStruct *anteConseVectors )
{
    Aig_Man_t *pAigNew;
    Aig_Obj_t *pObjTargetPo;
    int poMarker;
    //int i, RetValue, poSerialNum;
    int i, poSerialNum;
    Pdr_Par_t Pars, * pPars = &Pars;
    //Abc_Cex_t * pCex = NULL;
    Vec_Int_t *vMonotoneIndex;
    //char fileName[20];
    Abc_Cex_t * cexElem;

    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;

    pAigNew = createDisjunctiveMonotoneTester(pAig, aigPoIndicesArg, anteConseVectors, &poMarker );

    //printf("enter an integer : ");
    //waitForInteger = getchar();
    //putchar(waitForInteger);

    vMonotoneIndex = Vec_IntAlloc(0);

    for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
    {
        pObjTargetPo = Aig_ManCo( pAigNew, i );
        Aig_ObjChild0Flip( pObjTargetPo );
    }

    Pdr_ManSetDefaultParams( pPars );
    pPars->fVerbose = 0;
    pPars->fNotVerbose = 1;
    pPars->fSolveAll = 1;
    pAigNew->vSeqModelVec = NULL;
    Pdr_ManSolve( pAigNew, pPars );    

    if( pAigNew->vSeqModelVec )
    {
        Vec_PtrForEachEntry( Abc_Cex_t *, pAigNew->vSeqModelVec, cexElem, i )
        {
            if( cexElem == NULL  && i >= pendingSignalIndexLocal + 1)
            {
                poSerialNum = i - (pendingSignalIndexLocal + 1);
                Vec_IntPush( vMonotoneIndex, Vec_IntEntry( anteConseVectors->attrConsequentCandidates, poSerialNum ));
            }
        }
    }
    for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
    {
        pObjTargetPo = Aig_ManCo( pAigNew, i );
        Aig_ObjChild0Flip( pObjTargetPo );
    }
    
    //if(pAigNew->vSeqModelVec)
    //    Vec_PtrFree(pAigNew->vSeqModelVec);

    Aig_ManStop(pAigNew);
    
    if( Vec_IntSize( vMonotoneIndex ) > 0 )
    {
        return vMonotoneIndex;
    }
    else
    {
        Vec_IntFree(vMonotoneIndex);
        return NULL;
    }
}

Vec_Int_t *updateAnteConseVectors(struct antecedentConsequentVectorsStruct *anteConse )
{
    Vec_Int_t *vCandMonotone;
    int iElem, i;

    //if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
    //    return vHintMonotone;
    if( anteConse->attrAntecedents == NULL  || Vec_IntSize(anteConse->attrAntecedents) <= 0 )
        return anteConse->attrConsequentCandidates;
    vCandMonotone = Vec_IntAlloc(0);
    Vec_IntForEachEntry( anteConse->attrConsequentCandidates, iElem, i )
    {
        if( Vec_IntFind( anteConse->attrAntecedents, iElem ) == -1 )
            Vec_IntPush( vCandMonotone, iElem );
    }
    
    return vCandMonotone;
}

Vec_Int_t *vectorDifference(Vec_Int_t *A, Vec_Int_t *B)
{
    Vec_Int_t *C;
    int iElem, i;

    C = Vec_IntAlloc(0);
    Vec_IntForEachEntry( A, iElem, i )
    {
        if( Vec_IntFind( B, iElem ) == -1 )
        {
            Vec_IntPush( C, iElem );
        }
    }

    return C;
}

Vec_Int_t *createSingletonIntVector( int iElem )
{
    Vec_Int_t *myVec = Vec_IntAlloc(1);
    
    Vec_IntPush(myVec, iElem);
    return myVec;
}

#if 0
Vec_Ptr_t *generateDisjuntiveMonotone_rec()
{
    nextLevelSignals = ;
    if level is not exhausted
    for all x \in nextLevelSignals
    {
        append x in currAntecendent
        recond it as a monotone predicate
        resurse with level - 1 
    }
}
#endif

#if 0
Vec_Ptr_t *generateDisjuntiveMonotoneLevels(Aig_Man_t *pAig, 
            struct aigPoIndices *aigPoIndicesInstance, 
            struct antecedentConsequentVectorsStruct *anteConsecInstanceOrig,
            int level )
{
    Vec_Int_t *firstLevelMonotone;
    Vec_Int_t *currVecInt;
    Vec_Ptr_t *hierarchyList;
    int iElem, i;

    assert( level >= 1 );
    firstLevelMonotone = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
    if( firstLevelMonotone == NULL || Vec_IntSize(firstLevelMonotone) <= 0 )
        return NULL;
    
    hierarchyList = Vec_PtrAlloc(Vec_IntSize(firstLevelMonotone));
    
    Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
    {
        currVecInt = createSingletonIntVector( iElem );
        Vec_PtrPush( hierarchyList, currVecInt );
    }

    if( level > 1 )
    {
        Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
        {
            currVecInt = (Vec_Int_t *)Vec_PtrEntry( hierarchyList, i );
            
            
        }
    }

    return hierarchyList;
}
#endif

int Vec_IntPushUniqueLocal( Vec_Int_t * p, int Entry )
{
    int i;
    for ( i = 0; i < p->nSize; i++ )
        if ( p->pArray[i] == Entry )
            return 1;
    Vec_IntPush( p, Entry );
    return 0;
}

Vec_Ptr_t *findNextLevelDisjunctiveMonotone( 
        Aig_Man_t *pAig, 
        struct aigPoIndices *aigPoIndicesInstance, 
        struct antecedentConsequentVectorsStruct *anteConsecInstance, 
        Vec_Ptr_t *previousMonotoneVectors )
{
    Vec_Ptr_t *newLevelPtrVec;
    Vec_Int_t *vElem, *vNewDisjunctVector, *newDisjunction;
    int i, j, iElem;
    struct antecedentConsequentVectorsStruct *anteConsecInstanceLocal;
    Vec_Int_t *vUnionPrevMonotoneVector, *vDiffVector;

    newLevelPtrVec = Vec_PtrAlloc(0);
    vUnionPrevMonotoneVector = Vec_IntAlloc(0);
    Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
        Vec_IntForEachEntry( vElem, iElem, j )
            Vec_IntPushUniqueLocal( vUnionPrevMonotoneVector, iElem );

    Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
    {
        anteConsecInstanceLocal = allocAntecedentConsequentVectorsStruct();

        anteConsecInstanceLocal->attrAntecedents = Vec_IntDup(vElem);    
        vDiffVector = vectorDifference( anteConsecInstance->attrConsequentCandidates, vUnionPrevMonotoneVector);
        anteConsecInstanceLocal->attrConsequentCandidates = vDiffVector;
        assert( vDiffVector );

        //printf("Calling target function %d\n", i);
        vNewDisjunctVector = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstanceLocal );

        if( vNewDisjunctVector )
        {
            Vec_IntForEachEntry(vNewDisjunctVector, iElem, j)
            {
                newDisjunction = Vec_IntDup(vElem);
                Vec_IntPush( newDisjunction, iElem );
                Vec_PtrPush( newLevelPtrVec, newDisjunction );
            }
            Vec_IntFree(vNewDisjunctVector);
        }
        deallocAntecedentConsequentVectorsStruct( anteConsecInstanceLocal );
    }

    Vec_IntFree(vUnionPrevMonotoneVector);

    return newLevelPtrVec;
}

void printAllIntVectors(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
{
    Vec_Int_t *vElem;
    int i, j, iElem;
    char *name, *hintSubStr;
    FILE *fp;

    fp = fopen( fileName, "a" );

    Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
    {    
        fprintf(fp, "( ");
        Vec_IntForEachEntry( vElem, iElem, j )
        {
            name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
            hintSubStr = strstr( name, "hint");
            assert( hintSubStr );
            fprintf(fp, "%s", hintSubStr);
            if( j < Vec_IntSize(vElem) - 1 )
            {
                fprintf(fp, " || ");
            }
            else
            {
                fprintf(fp, " )\n");
            }
        }
    }
    fclose(fp);
}

void printAllIntVectorsStabil(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
{
    Vec_Int_t *vElem;
    int i, j, iElem;
    char *name, *hintSubStr;
    FILE *fp;

    fp = fopen( fileName, "a" );

    Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
    {    
        printf("INT[%d] : ( ", i);
        fprintf(fp, "( ");
        Vec_IntForEachEntry( vElem, iElem, j )
        {
            name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
            hintSubStr = strstr( name, "csLevel1Stabil");
            assert( hintSubStr );
            printf("%s", hintSubStr);
            fprintf(fp, "%s", hintSubStr);
            if( j < Vec_IntSize(vElem) - 1 )
            {
                printf(" || ");
                fprintf(fp, " || ");
            }
            else
            {
                printf(" )\n");
                fprintf(fp, " )\n");
            }
        }
        //printf(")\n");
    }
    fclose(fp);
}


void appendVecToMasterVecInt(Vec_Ptr_t *masterVec, Vec_Ptr_t *candVec )
{
    int i;
    Vec_Int_t *vCand;
    Vec_Int_t *vNewIntVec;

    assert(masterVec != NULL);
    assert(candVec != NULL);
    Vec_PtrForEachEntry( Vec_Int_t *, candVec, vCand, i )
    {
        vNewIntVec = Vec_IntDup(vCand);    
        Vec_PtrPush(masterVec, vNewIntVec);
    }
}

void deallocateVecOfIntVec( Vec_Ptr_t *vecOfIntVec )
{
    Vec_Int_t *vInt;
    int i;

    if( vecOfIntVec )
    {
        Vec_PtrForEachEntry( Vec_Int_t *, vecOfIntVec, vInt, i )
        {
            Vec_IntFree( vInt );
        }
        Vec_PtrFree(vecOfIntVec);
    }    
}

Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
{
    Aig_Man_t *pAig;
    Vec_Int_t *vCandidateMonotoneSignals;
    Vec_Int_t *vKnownMonotoneSignals;
    //Vec_Int_t *vKnownMonotoneSignalsRoundTwo;
    //Vec_Int_t *vOldConsequentVector;
    //Vec_Int_t *vRemainingConsecVector;
    int i;
    int iElem;
    int pendingSignalIndex;
    Abc_Ntk_t *pNtkTemp;
    int hintSingalBeginningMarker;
    int hintSingalEndMarker;
    struct aigPoIndices *aigPoIndicesInstance;
    //struct monotoneVectorsStruct *monotoneVectorsInstance;
    struct antecedentConsequentVectorsStruct *anteConsecInstance;
    //Aig_Obj_t *safetyDriverNew;
    Vec_Int_t *newIntVec;
    Vec_Ptr_t *levelOneMonotne, *levelTwoMonotne;
    //Vec_Ptr_t *levelThreeMonotne;

    Vec_Ptr_t *vMasterDisjunctions;

    extern int findPendingSignal(Abc_Ntk_t *pNtk);
    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);    
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );

    //system("rm monotone.dat");
    
    /*******************************************/    
    //Finding the PO index of the pending signal 
    /*******************************************/    
    pendingSignalIndex = findPendingSignal(pNtk);
    if( pendingSignalIndex == -1 )
    {
        printf("\nNo Pending Signal Found\n");
        return NULL;
    }
    //else
        //printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );

    /*******************************************/    
    //Finding the PO indices of all hint signals
    /*******************************************/    
    vCandidateMonotoneSignals = findHintOutputs(pNtk);
    if( vCandidateMonotoneSignals == NULL )
        return NULL;
    else
    {
        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
    }

    /**********************************************/
    //Allocating "struct" with necessary parameters
    /**********************************************/
    aigPoIndicesInstance = allocAigPoIndices();
    aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
    aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
    aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
    aigPoIndicesInstance->attrSafetyInvarIndex = collectSafetyInvariantPOIndex(pNtk);

    /****************************************************/
    //Allocating "struct" with necessary monotone vectors
    /****************************************************/
    anteConsecInstance = allocAntecedentConsequentVectorsStruct();
    anteConsecInstance->attrAntecedents = NULL;
    anteConsecInstance->attrConsequentCandidates = vCandidateMonotoneSignals;

    /*******************************************/    
    //Generate AIG from Ntk
    /*******************************************/    
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }

    /*******************************************/    
    //finding LEVEL 1 monotone signals
    /*******************************************/    
    //printf("Calling target function outside loop\n");
    vKnownMonotoneSignals = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
    levelOneMonotne = Vec_PtrAlloc(0);
    Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
    {
        newIntVec = createSingletonIntVector( iElem );
        Vec_PtrPush( levelOneMonotne, newIntVec );
        //printf("Monotone Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
    }
    //printAllIntVectors( levelOneMonotne, pNtk, "monotone.dat" );

    vMasterDisjunctions = Vec_PtrAlloc( Vec_PtrSize( levelOneMonotne ));
    appendVecToMasterVecInt(vMasterDisjunctions, levelOneMonotne );

    /*******************************************/    
    //finding LEVEL >1 monotone signals
    /*******************************************/    
    #if 0
    if( vKnownMonotoneSignals )
    {
        Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
        {
            printf("\n**************************************************************\n");
            printf("Exploring Second Layer : Reference Po[%d] = %s", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ));
            printf("\n**************************************************************\n");
            anteConsecInstance->attrAntecedents = createSingletonIntVector( iElem );
            vOldConsequentVector = anteConsecInstance->attrConsequentCandidates;
            vRemainingConsecVector = updateAnteConseVectors(anteConsecInstance);
            if( anteConsecInstance->attrConsequentCandidates != vRemainingConsecVector )
            {
                anteConsecInstance->attrConsequentCandidates = vRemainingConsecVector;
            }
            vKnownMonotoneSignalsRoundTwo = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
            Vec_IntForEachEntry( vKnownMonotoneSignalsRoundTwo, iElemTwo, iTwo )
            {
                printf("Monotone Po[%d] = %s, (%d, %d)\n", iElemTwo, Abc_ObjName( Abc_NtkPo(pNtk, iElemTwo) ), iElem, iElemTwo );
            }
            Vec_IntFree(vKnownMonotoneSignalsRoundTwo);
            Vec_IntFree(anteConsecInstance->attrAntecedents);
            if(anteConsecInstance->attrConsequentCandidates != vOldConsequentVector)
            {
                Vec_IntFree(anteConsecInstance->attrConsequentCandidates);
                anteConsecInstance->attrConsequentCandidates = vOldConsequentVector;
            }
        }
    }
    #endif 

#if 1
    levelTwoMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelOneMonotne );
    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
    appendVecToMasterVecInt(vMasterDisjunctions, levelTwoMonotne );
#endif

    //levelThreeMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelTwoMonotne );
    //printAllIntVectors( levelThreeMonotne );
    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
    //appendVecToMasterVecInt(vMasterDisjunctions, levelThreeMonotne );

    deallocAigPoIndices(aigPoIndicesInstance);
    deallocAntecedentConsequentVectorsStruct(anteConsecInstance);
    //deallocPointersToMonotoneVectors(monotoneVectorsInstance);

    deallocateVecOfIntVec( levelOneMonotne );
    deallocateVecOfIntVec( levelTwoMonotne );

    Aig_ManStop(pAig);
    Vec_IntFree(vKnownMonotoneSignals);

    return vMasterDisjunctions;
}

ABC_NAMESPACE_IMPL_END