diff options
Diffstat (limited to 'src/proof/live/disjunctiveMonotone.c')
-rw-r--r-- | src/proof/live/disjunctiveMonotone.c | 757 |
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 |