| #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 |
| |
| long countCombination(long n, long k) |
| { |
| assert( n >= k ); |
| if( n == k ) return 1; |
| if( k == 1 ) return n; |
| return countCombination( n-1, k-1 ) + countCombination( n-1, k ); |
| } |
| |
| void listCombination(int n, int t) |
| { |
| Vec_Int_t *vC; |
| int i, j, combCounter = 0; |
| |
| //Initialization |
| vC = Vec_IntAlloc(t+3); |
| for(i=-1; i<t; i++) |
| Vec_IntPush( vC, i ); |
| Vec_IntPush( vC, n ); |
| Vec_IntPush( vC, 0 ); |
| |
| while(1) |
| { |
| //visit combination |
| printf("Comb-%3d : ", ++combCounter); |
| for( i=t; i>0; i--) |
| printf("vC[%d] = %d ", i, Vec_IntEntry(vC, i)); |
| printf("\n"); |
| |
| j = 1; |
| while( Vec_IntEntry( vC, j ) + 1 == Vec_IntEntry( vC, j+1 ) ) |
| { |
| //printf("\nGochon = %d, %d\n", Vec_IntEntry( vC, j ) + 1, Vec_IntEntry( vC, j+1 )); |
| Vec_IntWriteEntry( vC, j, j-1 ); |
| j = j + 1; |
| } |
| if( j > t ) break; |
| Vec_IntWriteEntry( vC, j, Vec_IntEntry( vC, j ) + 1 ); |
| } |
| |
| Vec_IntFree(vC); |
| } |
| |
| int generateCombinatorialStabil( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, |
| Vec_Int_t *vCandidateMonotoneSignals_, |
| Vec_Ptr_t *vDisj_nCk_, |
| int combN, int combK ) |
| { |
| Aig_Obj_t *pObjMonoCand, *pObj; |
| int targetPoIndex; |
| |
| //Knuth's Data Strcuture |
| int totalCombination_KNUTH = 0; |
| Vec_Int_t *vC_KNUTH; |
| int i_KNUTH, j_KNUTH; |
| |
| //Knuth's Data Structure Initialization |
| vC_KNUTH = Vec_IntAlloc(combK+3); |
| for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++) |
| Vec_IntPush( vC_KNUTH, i_KNUTH ); |
| Vec_IntPush( vC_KNUTH, combN ); |
| Vec_IntPush( vC_KNUTH, 0 ); |
| |
| while(1) |
| { |
| totalCombination_KNUTH++; |
| pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew)); |
| for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--) |
| { |
| targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH)); |
| pObj = Aig_ObjChild0Copy(Aig_ManCo( pAigOld, targetPoIndex )); |
| pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand ); |
| } |
| Vec_PtrPush(vDisj_nCk_, pObjMonoCand ); |
| |
| j_KNUTH = 1; |
| while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) ) |
| { |
| Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 ); |
| j_KNUTH = j_KNUTH + 1; |
| } |
| if( j_KNUTH > combK ) break; |
| Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 ); |
| } |
| |
| Vec_IntFree(vC_KNUTH); |
| |
| return totalCombination_KNUTH; |
| } |
| |
| int generateCombinatorialStabilExhaust( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, |
| Vec_Ptr_t *vDisj_nCk_, |
| int combN, int combK ) |
| { |
| Aig_Obj_t *pObjMonoCand, *pObj; |
| int targetPoIndex; |
| |
| //Knuth's Data Strcuture |
| int totalCombination_KNUTH = 0; |
| Vec_Int_t *vC_KNUTH; |
| int i_KNUTH, j_KNUTH; |
| |
| //Knuth's Data Structure Initialization |
| vC_KNUTH = Vec_IntAlloc(combK+3); |
| for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++) |
| Vec_IntPush( vC_KNUTH, i_KNUTH ); |
| Vec_IntPush( vC_KNUTH, combN ); |
| Vec_IntPush( vC_KNUTH, 0 ); |
| |
| while(1) |
| { |
| totalCombination_KNUTH++; |
| pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew)); |
| for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--) |
| { |
| //targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH)); |
| targetPoIndex = Vec_IntEntry(vC_KNUTH, i_KNUTH); |
| pObj = (Aig_Obj_t *)(Aig_ManLo( pAigOld, targetPoIndex )->pData); |
| pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand ); |
| } |
| Vec_PtrPush(vDisj_nCk_, pObjMonoCand ); |
| |
| j_KNUTH = 1; |
| while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) ) |
| { |
| Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 ); |
| j_KNUTH = j_KNUTH + 1; |
| } |
| if( j_KNUTH > combK ) break; |
| Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 ); |
| } |
| |
| Vec_IntFree(vC_KNUTH); |
| |
| return totalCombination_KNUTH; |
| } |
| |
| Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK ) |
| { |
| //AIG creation related data structure |
| Aig_Man_t *pNewAig; |
| int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0; |
| //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker; |
| int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker; |
| int combN_internal, combK_internal; //, targetPoIndex; |
| long longI, lCombinationCount; |
| //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk; |
| Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk; |
| Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk; |
| Vec_Int_t *vCandidateMonotoneSignals; |
| |
| extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk); |
| |
| //Knuth's Data Strcuture |
| //Vec_Int_t *vC_KNUTH; |
| //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0; |
| |
| //Collecting target HINT signals |
| vCandidateMonotoneSignals = findHintOutputs(pNtk); |
| if( vCandidateMonotoneSignals == NULL ) |
| { |
| printf("\nTraget Signal Set is Empty: Duplicating given AIG\n"); |
| combN_internal = 0; |
| } |
| 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 ); |
| combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1; |
| } |
| |
| //combK_internal = combK; |
| |
| //Knuth's Data Structure Initialization |
| //vC_KNUTH = Vec_IntAlloc(combK_internal+3); |
| //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++) |
| // Vec_IntPush( vC_KNUTH, i_KNUTH ); |
| //Vec_IntPush( vC_KNUTH, combN_internal ); |
| //Vec_IntPush( vC_KNUTH, 0 ); |
| |
| //Standard AIG duplication begins |
| //Standard AIG Manager Creation |
| pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) ); |
| pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 ); |
| sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk"); |
| pNewAig->pSpec = NULL; |
| |
| //Standard Mapping of Constant Nodes |
| pObj = Aig_ManConst1( pAig ); |
| pObj->pData = Aig_ManConst1( pNewAig ); |
| |
| //Standard AIG PI duplication |
| Saig_ManForEachPi( pAig, pObj, i ) |
| { |
| piCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //Standard AIG LO duplication |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| loCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //nCk LO creation |
| lCombinationCount = 0; |
| for(combK_internal=1; combK_internal<=combK; combK_internal++) |
| lCombinationCount += countCombination( combN_internal, combK_internal ); |
| assert( lCombinationCount > 0 ); |
| vLO_nCk = Vec_PtrAlloc(lCombinationCount); |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| loCreated++; |
| pObj = Aig_ObjCreateCi(pNewAig); |
| Vec_PtrPush( vLO_nCk, pObj ); |
| } |
| |
| //Standard Node duplication |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| } |
| |
| //nCk specific logic creation (i.e. nCk number of OR gates) |
| vDisj_nCk = Vec_PtrAlloc(lCombinationCount); |
| |
| |
| |
| //while(1) |
| //{ |
| // //visit combination |
| // //printf("Comb-%3d : ", ++combCounter_KNUTH); |
| // pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig)); |
| // for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--) |
| // { |
| // //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH)); |
| // targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH)); |
| // pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex )); |
| // pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand ); |
| // } |
| // Vec_PtrPush(vDisj_nCk, pObjMonoCand ); |
| // //printf("\n"); |
| |
| // j_KNUTH = 1; |
| // while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) ) |
| // { |
| // Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 ); |
| // j_KNUTH = j_KNUTH + 1; |
| // } |
| // if( j_KNUTH > combK_internal ) break; |
| // Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 ); |
| //} |
| for( combK_internal=1; combK_internal<=combK; combK_internal++ ) |
| generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals, |
| vDisj_nCk, combN_internal, combK_internal ); |
| |
| |
| //creation of implication logic |
| vPODriver_nCk = Vec_PtrAlloc(lCombinationCount); |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI )); |
| pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI )); |
| |
| pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk); |
| Vec_PtrPush(vPODriver_nCk, pObj); |
| } |
| |
| //Standard PO duplication |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| poCopied++; |
| pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| } |
| |
| //nCk specific PO creation |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) ); |
| } |
| |
| //Standard LI duplication |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| liCopied++; |
| Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| } |
| |
| //nCk specific LI creation |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| liCreated++; |
| Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) ); |
| } |
| |
| //clean-up, book-keeping |
| assert( liCopied + liCreated == loCopied + loCreated ); |
| nRegCount = loCopied + loCreated; |
| |
| Aig_ManSetRegNum( pNewAig, nRegCount ); |
| Aig_ManCleanup( pNewAig ); |
| assert( Aig_ManCheck( pNewAig ) ); |
| |
| //Vec_IntFree(vC_KNUTH); |
| return pNewAig; |
| } |
| |
| Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK ) |
| { |
| //AIG creation related data structure |
| Aig_Man_t *pNewAig; |
| int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0; |
| //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker; |
| int i, nRegCount; |
| int combN_internal, combK_internal; //, targetPoIndex; |
| long longI, lCombinationCount; |
| //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk; |
| Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk; |
| Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk; |
| |
| extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk); |
| |
| //Knuth's Data Strcuture |
| //Vec_Int_t *vC_KNUTH; |
| //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0; |
| |
| //Collecting target HINT signals |
| //vCandidateMonotoneSignals = findHintOutputs(pNtk); |
| //if( vCandidateMonotoneSignals == NULL ) |
| //{ |
| // printf("\nTraget Signal Set is Empty: Duplicating given AIG\n"); |
| // combN_internal = 0; |
| //} |
| //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 ); |
| // combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1; |
| //} |
| |
| combN_internal = Aig_ManRegNum(pAig); |
| |
| pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) ); |
| pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 ); |
| sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk"); |
| pNewAig->pSpec = NULL; |
| |
| //Standard Mapping of Constant Nodes |
| pObj = Aig_ManConst1( pAig ); |
| pObj->pData = Aig_ManConst1( pNewAig ); |
| |
| //Standard AIG PI duplication |
| Saig_ManForEachPi( pAig, pObj, i ) |
| { |
| piCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //Standard AIG LO duplication |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| loCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //nCk LO creation |
| lCombinationCount = 0; |
| for(combK_internal=1; combK_internal<=combK; combK_internal++) |
| lCombinationCount += countCombination( combN_internal, combK_internal ); |
| assert( lCombinationCount > 0 ); |
| vLO_nCk = Vec_PtrAlloc(lCombinationCount); |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| loCreated++; |
| pObj = Aig_ObjCreateCi(pNewAig); |
| Vec_PtrPush( vLO_nCk, pObj ); |
| } |
| |
| //Standard Node duplication |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| } |
| |
| //nCk specific logic creation (i.e. nCk number of OR gates) |
| vDisj_nCk = Vec_PtrAlloc(lCombinationCount); |
| |
| for( combK_internal=1; combK_internal<=combK; combK_internal++ ) |
| { |
| generateCombinatorialStabilExhaust( pNewAig, pAig, |
| vDisj_nCk, combN_internal, combK_internal ); |
| } |
| |
| |
| //creation of implication logic |
| vPODriver_nCk = Vec_PtrAlloc(lCombinationCount); |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI )); |
| pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI )); |
| |
| pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk); |
| Vec_PtrPush(vPODriver_nCk, pObj); |
| } |
| |
| //Standard PO duplication |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| poCopied++; |
| pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| } |
| |
| //nCk specific PO creation |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) ); |
| } |
| |
| //Standard LI duplication |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| liCopied++; |
| Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| } |
| |
| //nCk specific LI creation |
| for( longI = 0; longI < lCombinationCount; longI++ ) |
| { |
| liCreated++; |
| Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) ); |
| } |
| |
| //clean-up, book-keeping |
| assert( liCopied + liCreated == loCopied + loCreated ); |
| nRegCount = loCopied + loCreated; |
| |
| Aig_ManSetRegNum( pNewAig, nRegCount ); |
| Aig_ManCleanup( pNewAig ); |
| assert( Aig_ManCheck( pNewAig ) ); |
| |
| Vec_PtrFree(vLO_nCk); |
| Vec_PtrFree(vPODriver_nCk); |
| Vec_PtrFree(vDisj_nCk); |
| //Vec_IntFree(vC_KNUTH); |
| return pNewAig; |
| } |
| |
| ABC_NAMESPACE_IMPL_END |
