1 files changed, 757 insertions, 0 deletions
diff --git a/src/proof/live/disjunctiveMonotone.c b/src/proof/live/disjunctiveMonotone.c
new file mode 100644
index 00000000..505af774
--- /dev/null
+++ b/src/proof/live/disjunctiveMonotone.c
@@ -0,0 +1,757 @@
+/**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