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

  FileName    [arenaViolation.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Liveness property checking.]

  Synopsis    [module for addition of arena violator detector
		induced by stabilizing constraints]

  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"

//#define DISJUNCTIVE_CONSTRAINT_ENABLE_MODE
#define BARRIER_MONOTONE_TEST

ABC_NAMESPACE_IMPL_START

Vec_Ptr_t * createArenaLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
{
	Vec_Ptr_t *vArenaLO;
	int barrierCount;
	Aig_Obj_t *pObj;
	int i;

	if( vBarriers == NULL )
		return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
		return NULL;

	vArenaLO = Vec_PtrAlloc(barrierCount);	
	for( i=0; i<barrierCount; i++ )
	{
		pObj = Aig_ObjCreateCi( pAigNew );
		Vec_PtrPush( vArenaLO, pObj );
	}

	return vArenaLO;
}

Vec_Ptr_t * createArenaLi( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal )
{
	Vec_Ptr_t *vArenaLi;
	int barrierCount;
	int i;
	Aig_Obj_t *pObj, *pObjDriver;

	if( vBarriers == NULL )
		return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
		return NULL;

	vArenaLi = Vec_PtrAlloc(barrierCount);	
	for( i=0; i<barrierCount; i++ )
	{
		pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i );
		pObj = Aig_ObjCreateCo( pAigNew, pObjDriver );
		Vec_PtrPush( vArenaLi, pObj );
	}

	return vArenaLi;
}

Vec_Ptr_t *createMonotoneBarrierLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
{
	Vec_Ptr_t *vMonotoneLO;
	int barrierCount;
	Aig_Obj_t *pObj;
	int i;

	if( vBarriers == NULL )
		return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
		return NULL;

	vMonotoneLO = Vec_PtrAlloc(barrierCount);	
	for( i=0; i<barrierCount; i++ )
	{
		pObj = Aig_ObjCreateCi( pAigNew );
		Vec_PtrPush( vMonotoneLO, pObj );
	}

	return vMonotoneLO;
}

Aig_Obj_t *driverToPoNew( Aig_Man_t *pAig, Aig_Obj_t *pObjPo )
{
	Aig_Obj_t *poDriverOld;
	Aig_Obj_t *poDriverNew;	
	
	//Aig_ObjPrint( pAig, pObjPo );
	//printf("\n");

	assert( Aig_ObjIsCo(pObjPo) );
	poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
	assert( !Aig_ObjIsCo(poDriverOld) );
	poDriverNew = !Aig_IsComplement(poDriverOld)? 
			(Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) : 
			Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData));
	//assert( !Aig_ObjIsCo(poDriverNew) );
	return poDriverNew;
}

Vec_Ptr_t *collectBarrierDisjunctions(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
{
	int barrierCount, i, j, jElem;
	Vec_Int_t *vIthBarrier;
	Aig_Obj_t *pObjBarrier, *pObjCurr, *pObjTargetPoOld;
	Vec_Ptr_t *vNewBarrierSignals;

	if( vBarriers == NULL )
		return NULL;
	barrierCount = Vec_PtrSize( vBarriers );
	if( barrierCount <= 0 )
		return NULL;

	vNewBarrierSignals = Vec_PtrAlloc( barrierCount );

	for( i=0; i<barrierCount; i++ )
	{
		vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i );
		assert( Vec_IntSize( vIthBarrier ) >= 1 );
		pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew));
		Vec_IntForEachEntry( vIthBarrier, jElem, j )
		{
			pObjTargetPoOld = Aig_ManCo( pAigOld, jElem );
			//Aig_ObjPrint( pAigOld, pObjTargetPoOld );
			//printf("\n");
			pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld );
			pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier );
		}
		assert( pObjBarrier );
		Vec_PtrPush(vNewBarrierSignals, pObjBarrier);
	}
	assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount );

	return vNewBarrierSignals;
}

Aig_Obj_t *Aig_Xor( Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2 )
{
	return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
}

Aig_Obj_t *createArenaViolation(
		Aig_Man_t *pAigOld,
		Aig_Man_t *pAigNew, 
		Aig_Obj_t *pWindowBegins, 
		Aig_Obj_t *pWithinWindow, 
		Vec_Ptr_t *vMasterBarriers, 
		Vec_Ptr_t *vBarrierLo,
		Vec_Ptr_t *vBarrierLiDriver,
		Vec_Ptr_t *vMonotoneDisjunctionNodes
		)
{
	Aig_Obj_t *pWindowBeginsLocal = pWindowBegins;
	Aig_Obj_t *pWithinWindowLocal = pWithinWindow;
	int i;
	Aig_Obj_t *pObj, *pObjAnd1, *pObjOr1, *pObjAnd2, *pObjBarrierLo, *pObjBarrierSwitch, *pObjArenaViolation;
	Vec_Ptr_t *vBarrierSignals;

	assert( vBarrierLiDriver != NULL );
	assert( vMonotoneDisjunctionNodes != NULL );

	pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew ));

	vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers);
	assert( vBarrierSignals != NULL );

	assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 );
	Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
		Vec_PtrPush( vMonotoneDisjunctionNodes, pObj );
	assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) );

	Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
	{
		//pObjNew = driverToPoNew( pAigOld, pObj );
		pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal);
		pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i );
		pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo);
		Vec_PtrPush( vBarrierLiDriver, pObjOr1 );

		pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo );
		pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal );
		pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation );
	}

	Vec_PtrFree(vBarrierSignals);
	return pObjArenaViolation;
}

Aig_Obj_t *createConstrained0LiveConeWithDSC( Aig_Man_t *pNewAig, Vec_Ptr_t *signalList )
{
	Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj;
	int i, numSigAntecedent;
	
	numSigAntecedent = Vec_PtrSize( signalList ) - 1;

	pAntecedent = Aig_ManConst1( pNewAig );
	pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
	pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );

	for(i=0; i<numSigAntecedent; i++ )
	{
		pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
		assert( Aig_Regular(pObj)->pData );
		pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
	}

	p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );

	return p0LiveCone;
}

Vec_Ptr_t *collectCSSignalsWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
	int i;
	Aig_Obj_t *pObj, *pConsequent = NULL;
	Vec_Ptr_t *vNodeArray;

	vNodeArray = Vec_PtrAlloc(1);

	Saig_ManForEachPo( pAig, pObj, i )
	{
		if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
			Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );	
		else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
			pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
	}
	assert( pConsequent );
	Vec_PtrPush( vNodeArray, pConsequent );	
	return vNodeArray;
}

int collectWindowBeginSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
		if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL )
		{
			return i;			
		}
	}
	
	return -1;
}

int collectWithinWindowSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
		if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL )
			return i;			
	}
	
	return -1;
}

int collectPendingSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
		if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL )
			return i;			
	}
	
	return -1;
}

Aig_Obj_t *createAndGateForMonotonicityVerification(
				Aig_Man_t *pNewAig,
				Vec_Ptr_t *vDisjunctionSignals,
				Vec_Ptr_t *vDisjunctionLo,
				Aig_Obj_t *pendingLo,
				Aig_Obj_t *pendingSignal
				)
{
	Aig_Obj_t *pObjBigAnd, *pObj, *pObjLo, *pObjImply;
	Aig_Obj_t *pObjPendingAndPendingLo;
	int i;

	pObjBigAnd = Aig_ManConst1( pNewAig );
	pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal );
	Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i )
	{
		pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i );	
		pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)),
					pObj );
		pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply );
	}
	return pObjBigAnd;
}

Aig_Man_t *createNewAigWith0LivePoWithDSC( Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers )
{
	Aig_Man_t *pNewAig;
	Aig_Obj_t *pObj, *pObjNewPoDriver;
	int i;
	int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0;
	Aig_Obj_t *pObjWindowBeginsNew, *pObjWithinWindowNew, *pObjArenaViolation, *pObjTarget, *pObjArenaViolationLiDriver;
	Aig_Obj_t *pObjNewPoDriverArenaViolated, *pObjArenaViolationLo;
	Vec_Ptr_t *vBarrierLo, *vBarrierLiDriver, *vBarrierLi;
	Vec_Ptr_t *vMonotoneNodes;

#ifdef BARRIER_MONOTONE_TEST
	Aig_Obj_t *pObjPendingSignal;
	Aig_Obj_t *pObjPendingFlopLo;
	Vec_Ptr_t *vMonotoneBarrierLo;
	Aig_Obj_t *pObjPendingAndPendingSignal, *pObjMonotoneAnd, *pObjCurrMonotoneLo;
#endif

	//assert( Vec_PtrSize( signalList ) > 1 );

	//****************************************************************
	// 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("_0Live") + 1 );
	sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
    	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 )
	{
		pObj->pData = Aig_ObjCreateCi( pNewAig );
	}

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

	//****************************************************************
	// Step 4.a: create register outputs for the barrier flops
	//****************************************************************
	vBarrierLo = createArenaLO( pNewAig, vBarriers );
	loCreated = Vec_PtrSize(vBarrierLo);

	//****************************************************************
	// Step 4.b: create register output for arenaViolationFlop
	//****************************************************************
	pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig );
	loCreated++;

#ifdef BARRIER_MONOTONE_TEST
	//****************************************************************
	// Step 4.c: create register output for pendingFlop
	//****************************************************************
	pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig );
	loCreated++;

	//****************************************************************
	// Step 4.d: create register outputs for the barrier flops
	// for asserting monotonicity
	//****************************************************************
	vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers );
	loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo);
#endif

	//********************************************************************
	// Step 5: create internal nodes
	//********************************************************************
    	Aig_ManForEachNode( pAig, pObj, i )
	{
		pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
	}

	//********************************************************************
	// Step 5.a: create internal nodes corresponding to arenaViolation
	//********************************************************************
	pObjTarget = Aig_ManCo( pAig, windowBeginIndex );
	pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget );

	pObjTarget = Aig_ManCo( pAig, withinWindowIndex );
	pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget );

	vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
	vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );

	pObjArenaViolation = createArenaViolation( pAig, pNewAig, 
				pObjWindowBeginsNew, pObjWithinWindowNew, 
				vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes ); 
	assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) );

#ifdef ARENA_VIOLATION_CONSTRAINT

#endif

	pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo );

#ifdef BARRIER_MONOTONE_TEST
	//********************************************************************
	// Step 5.b: Create internal nodes for monotone testing
	//********************************************************************

	pObjTarget = Aig_ManCo( pAig, pendingSignalIndex );
	pObjPendingSignal = driverToPoNew( pAig, pObjTarget );
	
	pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo );
	pObjMonotoneAnd = Aig_ManConst1( pNewAig );
	Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
	{
		pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i);
		pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd,
			Aig_Or( pNewAig, 
			Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)),
			pObj ) );
	}
#endif

	//********************************************************************
	// Step 6: create primary outputs
	//********************************************************************

	Saig_ManForEachPo( pAig, pObj, i )
	{
		pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
	}

	pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList );
	pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo );
#ifdef BARRIER_MONOTONE_TEST
	pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd );
#endif
	Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated );

	*index0Live = i;

	//********************************************************************
	// Step 7: create register inputs
	//********************************************************************

	Saig_ManForEachLi( pAig, pObj, i )
	{
		liCopied++;
		pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
	}

	//********************************************************************
	// Step 7.a: create register inputs for barrier flops
	//********************************************************************
	assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) );
	vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver );
	liCreated = Vec_PtrSize( vBarrierLi );

	//********************************************************************
	// Step 7.b: create register inputs for arenaViolation flop
	//********************************************************************
	Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver );
	liCreated++;

#ifdef BARRIER_MONOTONE_TEST
	//****************************************************************
	// Step 7.c: create register input for pendingFlop
	//****************************************************************
	Aig_ObjCreateCo( pNewAig, pObjPendingSignal);
	liCreated++;

	//********************************************************************
	// Step 7.d: create register inputs for the barrier flops
	// for asserting monotonicity
	//********************************************************************
	Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
	{
		Aig_ObjCreateCo( pNewAig, pObj );
		liCreated++;
	}
#endif

	assert(loCopied + loCreated == liCopied + liCreated);
	//next step should be changed
	Aig_ManSetRegNum( pNewAig, loCopied + loCreated );
	Aig_ManCleanup( pNewAig );

	assert( Aig_ManCheck( pNewAig ) );

	Vec_PtrFree(vBarrierLo);
	Vec_PtrFree(vMonotoneBarrierLo);
	Vec_PtrFree(vBarrierLiDriver);
	Vec_PtrFree(vBarrierLi);
	Vec_PtrFree(vMonotoneNodes);

	return pNewAig;
}

Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers )
{
	Vec_Ptr_t *vSignalVector;
	Aig_Man_t *pAigNew;
	int pObjWithinWindow;
	int pObjWindowBegin;
	int pObjPendingSignal;

	vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );	

	pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
	pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
	pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );

	pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
	Vec_PtrFree(vSignalVector);

	return pAigNew;
}

ABC_NAMESPACE_IMPL_END