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

  FileName    [kLiveConstraints.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.]

  Revision    [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]

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

#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"

ABC_NAMESPACE_IMPL_START

extern Aig_Man_t *Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
//extern Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo);

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

struct aigPoIndices *allocAigPoIndices()
{
	struct aigPoIndices *newAigPoIndices;

	newAigPoIndices = (struct aigPoIndices *)malloc(sizeof (struct aigPoIndices));
	newAigPoIndices->attrPendingSignalIndex = -1;
	newAigPoIndices->attrHintSingalBeginningMarker = -1;
	newAigPoIndices->attrHintSingalEndMarker = -1;
	newAigPoIndices->attrSafetyInvarIndex = -1;

	assert( newAigPoIndices != NULL );
	return newAigPoIndices;
}

void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices)
{
	assert(toBeDeletedAigPoIndices != NULL );
	free(toBeDeletedAigPoIndices);
}

struct monotoneVectorsStruct
{
	Vec_Int_t *attrKnownMonotone;
	Vec_Int_t *attrCandMonotone;
	Vec_Int_t *attrHintMonotone;
};

struct monotoneVectorsStruct *allocPointersToMonotoneVectors()
{
	struct monotoneVectorsStruct *newPointersToMonotoneVectors;

	newPointersToMonotoneVectors = (struct monotoneVectorsStruct *)malloc(sizeof (struct monotoneVectorsStruct));

	newPointersToMonotoneVectors->attrKnownMonotone = NULL;
	newPointersToMonotoneVectors->attrCandMonotone = NULL;
	newPointersToMonotoneVectors->attrHintMonotone = NULL;
		
	assert( newPointersToMonotoneVectors != NULL );
	return newPointersToMonotoneVectors;
}

void deallocPointersToMonotoneVectors(struct monotoneVectorsStruct *toBeDeleted)
{
	assert( toBeDeleted != NULL );
	free( toBeDeleted );
}

Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk)
{
	int i, numElementPush = 0;
	Abc_Obj_t *pNode;
	Vec_Int_t *vHintPoIntdex;

	vHintPoIntdex = Vec_IntAlloc(0);
	Abc_NtkForEachPo( pNtk, pNode, i )
	{
		if( strstr( Abc_ObjName( pNode ), "hint_" ) != NULL )
		{
			Vec_IntPush( vHintPoIntdex, i );
			numElementPush++;
		}
	}	
	
	if( numElementPush == 0 )
		return NULL;
	else
		return vHintPoIntdex;
}

int findPendingSignal(Abc_Ntk_t *pNtk)
{
	int i, pendingSignalIndex = -1;
	Abc_Obj_t *pNode;

	Abc_NtkForEachPo( pNtk, pNode, i )
	{
		if( strstr( Abc_ObjName( pNode ), "pendingSignal" ) != NULL )
		{
			pendingSignalIndex = i;
			break;
		}
	}	
	
	return pendingSignalIndex;
}

int checkSanityOfKnownMonotone( Vec_Int_t *vKnownMonotone, Vec_Int_t *vCandMonotone, Vec_Int_t *vHintMonotone )
{
	int iElem, i;

	Vec_IntForEachEntry( vKnownMonotone, iElem, i )
		printf("%d ", iElem);
	printf("\n");
	Vec_IntForEachEntry( vCandMonotone, iElem, i )
		printf("%d ", iElem);
	printf("\n");
	Vec_IntForEachEntry( vHintMonotone, iElem, i )
		printf("%d ", iElem);
	printf("\n");
	return 1;
}

Aig_Man_t *createMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo)
{
	Aig_Man_t *pNewAig;
	int iElem, i, nRegCount, oldPoNum, poSerialNum, iElemHint;
	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, *pHintSignalLo, *pHintMonotoneFlop, *pObjTemp1, *pObjTemp2, *pObjKnownMonotoneAnd;
	Vec_Ptr_t *vHintMonotoneLocalDriverNew;
	Vec_Ptr_t *vHintMonotoneLocalFlopOutput;
	Vec_Ptr_t *vHintMonotoneLocalProp;

	int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
	int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
	//int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;

	Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
	Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
	Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;
	
	//****************************************************************
	// 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") + 1 );
	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 
	//****************************************************************
	vHintMonotoneLocalFlopOutput = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
	Vec_IntForEachEntry( vHintMonotoneLocal, iElem, i )
	{
		loCreated++;
		pHintMonotoneFlop = Aig_ObjCreateCi( pNewAig );
		Vec_PtrPush( vHintMonotoneLocalFlopOutput, pHintMonotoneFlop );
	}

	nRegCount = loCreated + loCopied;
	printf("\nnRegCount = %d\n", nRegCount);

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

	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 );

	oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
	pObjKnownMonotoneAnd = Aig_ManConst1( pNewAig );
	#if 1
	if( vKnownMonotoneLocal )
	{
		assert( checkSanityOfKnownMonotone( vKnownMonotoneLocal, vCandMonotoneLocal, vHintMonotoneLocal ) );

		Vec_IntForEachEntry( vKnownMonotoneLocal, iElemHint, i )
		{
			iElem = (iElemHint - hintSingalBeginningMarkerLocal) + 1 + pendingSignalIndexLocal;
			printf("\nProcessing knownMonotone = %d\n", iElem);
			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));
			pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, iElem - oldPoNum);
			pObjTemp1 = Aig_Or( pNewAig, Aig_And(pNewAig, pObjDriverNew, pHintSignalLo), 
						Aig_And(pNewAig, Aig_Not(pObjDriverNew), Aig_Not(pHintSignalLo)) );
			
			pObjKnownMonotoneAnd = Aig_And( pNewAig, pObjKnownMonotoneAnd, pObjTemp1 );
		}
		pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingAndNextPending, pObjKnownMonotoneAnd );
	}
	#endif

	vHintMonotoneLocalDriverNew = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
	vHintMonotoneLocalProp = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
	Vec_IntForEachEntry( vHintMonotoneLocal, 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));

		if( vKnownMonotoneLocal != NULL && Vec_IntFind( vKnownMonotoneLocal, iElem ) != -1 )
		{
			Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
		}
		else
		{
			poSerialNum = Vec_IntFind( vHintMonotoneLocal, iElem );
			pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, poSerialNum );
			pObjTemp1 = Aig_And( pNewAig, pObjPendingAndNextPending, pHintSignalLo);
			pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), pObjDriverNew );
			//pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), Aig_ManConst1( pNewAig ));
			//pObjTemp2 = Aig_ManConst1( pNewAig );
			Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
			Vec_PtrPush(vHintMonotoneLocalProp, pObjTemp2); 
		}
	}

	//********************************************************************
	// 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 *, vHintMonotoneLocalProp, 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 *, vHintMonotoneLocalDriverNew, pObj, i )
	{
		liCreated++;
		Aig_ObjCreateCo( pNewAig, pObj );
	}

	printf("\npoCopied = %d, poCreated = %d\n", poCopied, poCreated);
	printf("\nliCreated++ = %d\n", liCreated );
	Aig_ManSetRegNum( pNewAig, nRegCount );
	Aig_ManCleanup( pNewAig );
	
	assert( Aig_ManCheck( pNewAig ) );
	assert( loCopied + loCreated == liCopied + liCreated );

	printf("\nSaig_ManPoNum = %d\n", Saig_ManPoNum(pNewAig));
	return pNewAig;
}


Vec_Int_t *findNewMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg )
{
	Aig_Man_t *pAigNew;
	Aig_Obj_t *pObjTargetPo;
	int poMarker, oldPoNum;
	int i, RetValue;
	Pdr_Par_t Pars, * pPars = &Pars;
	Abc_Cex_t * pCex = NULL;
	Vec_Int_t *vMonotoneIndex;

	int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
	int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
	//int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;

	//Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
	//Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
	//Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;

	pAigNew = createMonotoneTester(pAig, aigPoIndicesArg, monotoneVectorArg, &poMarker );
	oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);

	vMonotoneIndex = Vec_IntAlloc(0);
	printf("\nSaig_ManPoNum(pAigNew) = %d, poMarker = %d\n", Saig_ManPoNum(pAigNew), poMarker);
	for( i=poMarker; i<Saig_ManPoNum(pAigNew); i++ )
	{
		pObjTargetPo = Aig_ManCo( pAigNew, i );
		Aig_ObjChild0Flip( pObjTargetPo );

		Pdr_ManSetDefaultParams( pPars );
		pCex = NULL;
		pPars->fVerbose = 0;
		//pPars->iOutput = i;
		//RetValue = Pdr_ManSolve( pAigNew, pPars, &pCex );	
		RetValue = Pdr_ManSolve( pAigNew, pPars );	
		if( RetValue == 1 )
		{
			printf("\ni = %d, RetValue = %d : %s (Frame %d)\n", i - oldPoNum + hintSingalBeginningMarkerLocal, RetValue, "Property Proved", pCex? (pCex)->iFrame : -1 );
			Vec_IntPush( vMonotoneIndex, i - (pendingSignalIndexLocal + 1) + hintSingalBeginningMarkerLocal);
		}
		Aig_ObjChild0Flip( pObjTargetPo );
	}
	
	if( Vec_IntSize( vMonotoneIndex ) > 0 )
		return vMonotoneIndex;
	else
		return NULL;
}

Vec_Int_t *findRemainingMonotoneCandidates(Vec_Int_t *vKnownMonotone, Vec_Int_t *vHintMonotone)
{
	Vec_Int_t *vCandMonotone;
	int iElem, i;

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

Vec_Int_t *findMonotoneSignals( Abc_Ntk_t *pNtk )
{
	Aig_Man_t *pAig;
	Vec_Int_t *vCandidateMonotoneSignals;
	Vec_Int_t *vKnownMonotoneSignals;
	//Vec_Int_t *vKnownMonotoneSignalsNew;
	//Vec_Int_t *vRemainingCanMonotone;
	int i, iElem;
	int pendingSignalIndex;
	Abc_Ntk_t *pNtkTemp;
	int hintSingalBeginningMarker;
	int hintSingalEndMarker;
	struct aigPoIndices *aigPoIndicesInstance;
	struct monotoneVectorsStruct *monotoneVectorsInstance;
	
	/*******************************************/	
	//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;

	/****************************************************/
	//Allocating "struct" with necessary monotone vectors
	/****************************************************/
	monotoneVectorsInstance = allocPointersToMonotoneVectors();
	monotoneVectorsInstance->attrCandMonotone = vCandidateMonotoneSignals;
	monotoneVectorsInstance->attrHintMonotone = 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
	/*******************************************/	
	vKnownMonotoneSignals = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
	monotoneVectorsInstance->attrKnownMonotone = vKnownMonotoneSignals;

	/*******************************************/	
	//finding LEVEL >1 monotone signals
	/*******************************************/	
	#if 0
	if( vKnownMonotoneSignals )
	{
		printf("\nsize = %d\n", Vec_IntSize(vKnownMonotoneSignals) );
		vRemainingCanMonotone = findRemainingMonotoneCandidates(vKnownMonotoneSignals, vCandidateMonotoneSignals);
		monotoneVectorsInstance->attrCandMonotone = vRemainingCanMonotone; 
		vKnownMonotoneSignalsNew = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
	}
	#endif 

	deallocAigPoIndices(aigPoIndicesInstance);
	deallocPointersToMonotoneVectors(monotoneVectorsInstance);
	return NULL;
}

ABC_NAMESPACE_IMPL_END