abcBridge-0.10.0.0: abc-build/src/proof/live/disjunctiveMonotone.c

/**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