| /**CFile**************************************************************** |
| |
| FileName [fraigFeed.c] |
| |
| PackageName [FRAIG: Functionally reduced AND-INV graphs.] |
| |
| Synopsis [Procedures to support the solver feedback.] |
| |
| Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 2.0. Started - October 1, 2004] |
| |
| Revision [$Id: fraigFeed.c,v 1.8 2005/07/08 01:01:31 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "fraigInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static int Fraig_FeedBackPrepare( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars ); |
| static int Fraig_FeedBackInsert( Fraig_Man_t * p, int nVarsPi ); |
| static void Fraig_FeedBackVerify( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); |
| |
| static void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ); |
| static Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * pMan ); |
| static int Fraig_GetSmallestColumn( int * pHits, int nHits ); |
| static int Fraig_GetHittingPattern( unsigned * pSims, int nWords ); |
| static void Fraig_CancelCoveredColumns( Fraig_NodeVec_t * vColumns, int * pHits, int iPat ); |
| static void Fraig_FeedBackCheckTable( Fraig_Man_t * p ); |
| static void Fraig_FeedBackCheckTableF0( Fraig_Man_t * p ); |
| static void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ); |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Initializes the feedback information.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBackInit( Fraig_Man_t * p ) |
| { |
| p->vCones = Fraig_NodeVecAlloc( 500 ); |
| p->vPatsReal = Msat_IntVecAlloc( 1000 ); |
| p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); |
| memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna ); |
| p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); |
| p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the feedback from teh solver.] |
| |
| Description [Array pModel gives the value of each variable in the SAT |
| solver. Array vVars is the array of integer numbers of variables |
| involves in this conflict.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) |
| { |
| int nVarsPi, nWords; |
| int i; |
| abctime clk = Abc_Clock(); |
| |
| // get the number of PI vars in the feedback (also sets the PI values) |
| nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars ); |
| |
| // set the PI values |
| nWords = Fraig_FeedBackInsert( p, nVarsPi ); |
| assert( p->iWordStart + nWords <= p->nWordsDyna ); |
| |
| // resimulates the words from p->iWordStart to iWordStop |
| for ( i = 1; i < p->vNodes->nSize; i++ ) |
| if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) ) |
| Fraig_NodeSimulate( p->vNodes->pArray[i], p->iWordStart, p->iWordStart + nWords, 0 ); |
| |
| if ( p->fDoSparse ) |
| Fraig_TableRehashF0( p, 0 ); |
| |
| if ( !p->fChoicing ) |
| Fraig_FeedBackVerify( p, pOld, pNew ); |
| |
| // if there is no room left, compress the patterns |
| if ( p->iWordStart + nWords == p->nWordsDyna ) |
| p->iWordStart = Fraig_FeedBackCompress( p ); |
| else // otherwise, update the starting word |
| p->iWordStart += nWords; |
| |
| p->timeFeed += Abc_Clock() - clk; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Get the number and values of the PI variables.] |
| |
| Description [Returns the number of PI variables involved in this feedback. |
| Fills in the internal presence and value data for the primary inputs.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_FeedBackPrepare( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars ) |
| { |
| Fraig_Node_t * pNode; |
| int i, nVars, nVarsPis, * pVars; |
| |
| // clean the presence flag for all PIs |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| { |
| pNode = p->vInputs->pArray[i]; |
| pNode->fFeedUse = 0; |
| } |
| |
| // get the variables involved in the feedback |
| nVars = Msat_IntVecReadSize(vVars); |
| pVars = Msat_IntVecReadArray(vVars); |
| |
| // set the values for the present variables |
| nVarsPis = 0; |
| for ( i = 0; i < nVars; i++ ) |
| { |
| pNode = p->vNodes->pArray[ pVars[i] ]; |
| if ( !Fraig_NodeIsVar(pNode) ) |
| continue; |
| // set its value |
| pNode->fFeedUse = 1; |
| pNode->fFeedVal = !MSAT_LITSIGN(pModel[pVars[i]]); |
| nVarsPis++; |
| } |
| return nVarsPis; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts the new simulation patterns.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_FeedBackInsert( Fraig_Man_t * p, int nVarsPi ) |
| { |
| Fraig_Node_t * pNode; |
| int nWords, iPatFlip, nPatFlipLimit, i, w; |
| int fUseNoPats = 0; |
| int fUse2Pats = 0; |
| |
| // get the number of words |
| if ( fUse2Pats ) |
| nWords = FRAIG_NUM_WORDS( 2 * nVarsPi + 1 ); |
| else if ( fUseNoPats ) |
| nWords = 1; |
| else |
| nWords = FRAIG_NUM_WORDS( nVarsPi + 1 ); |
| // update the number of words if they do not fit into the simulation info |
| if ( nWords > p->nWordsDyna - p->iWordStart ) |
| nWords = p->nWordsDyna - p->iWordStart; |
| // determine the bound on the flipping bit |
| nPatFlipLimit = nWords * 32 - 2; |
| |
| // mark the real pattern |
| Msat_IntVecPush( p->vPatsReal, p->iWordStart * 32 ); |
| // record the real pattern |
| Fraig_BitStringSetBit( p->pSimsReal, p->iWordStart * 32 ); |
| |
| // set the values at the PIs |
| iPatFlip = 1; |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| { |
| pNode = p->vInputs->pArray[i]; |
| for ( w = p->iWordStart; w < p->iWordStart + nWords; w++ ) |
| if ( !pNode->fFeedUse ) |
| pNode->puSimD[w] = FRAIG_RANDOM_UNSIGNED; |
| else if ( pNode->fFeedVal ) |
| pNode->puSimD[w] = FRAIG_FULL; |
| else // if ( !pNode->fFeedVal ) |
| pNode->puSimD[w] = 0; |
| |
| if ( fUse2Pats ) |
| { |
| // flip two patterns |
| if ( pNode->fFeedUse && 2 * iPatFlip < nPatFlipLimit ) |
| { |
| Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip - 1 ); |
| Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip ); |
| Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, 2 * iPatFlip + 1 ); |
| iPatFlip++; |
| } |
| } |
| else if ( fUseNoPats ) |
| { |
| } |
| else |
| { |
| // flip the diagonal |
| if ( pNode->fFeedUse && iPatFlip < nPatFlipLimit ) |
| { |
| Fraig_BitStringXorBit( pNode->puSimD + p->iWordStart, iPatFlip ); |
| iPatFlip++; |
| // Extra_PrintBinary( stdout, &pNode->puSimD, 45 ); printf( "\n" ); |
| } |
| } |
| // clean the use mask |
| pNode->fFeedUse = 0; |
| |
| // add the info to the D hash value of the PIs |
| for ( w = p->iWordStart; w < p->iWordStart + nWords; w++ ) |
| pNode->uHashD ^= pNode->puSimD[w] * s_FraigPrimes[w]; |
| |
| } |
| return nWords; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks that the SAT solver pattern indeed distinquishes the nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBackVerify( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) |
| { |
| int fValue1, fValue2, iPat; |
| iPat = Msat_IntVecReadEntry( p->vPatsReal, Msat_IntVecReadSize(p->vPatsReal)-1 ); |
| fValue1 = (Fraig_BitStringHasBit( pOld->puSimD, iPat )); |
| fValue2 = (Fraig_BitStringHasBit( pNew->puSimD, iPat )); |
| /* |
| Fraig_PrintNode( p, pOld ); |
| printf( "\n" ); |
| Fraig_PrintNode( p, pNew ); |
| printf( "\n" ); |
| */ |
| // assert( fValue1 != fValue2 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compress the simulation patterns.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_FeedBackCompress( Fraig_Man_t * p ) |
| { |
| unsigned * pSims; |
| unsigned uHash; |
| int i, w, t, nPats, * pPats; |
| int fPerformChecks = (p->nBTLimit == -1); |
| |
| // solve the covering problem |
| if ( fPerformChecks ) |
| { |
| Fraig_FeedBackCheckTable( p ); |
| if ( p->fDoSparse ) |
| Fraig_FeedBackCheckTableF0( p ); |
| } |
| |
| // solve the covering problem |
| Fraig_FeedBackCovering( p, p->vPatsReal ); |
| |
| |
| // get the number of additional patterns |
| nPats = Msat_IntVecReadSize( p->vPatsReal ); |
| pPats = Msat_IntVecReadArray( p->vPatsReal ); |
| // get the new starting word |
| p->iWordStart = FRAIG_NUM_WORDS( p->iPatsPerm + nPats ); |
| |
| // set the simulation info for the PIs |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| { |
| // get hold of the simulation info for this PI |
| pSims = p->vInputs->pArray[i]->puSimD; |
| // clean the storage for the new patterns |
| for ( w = p->iWordPerm; w < p->iWordStart; w++ ) |
| p->pSimsTemp[w] = 0; |
| // set the patterns |
| for ( t = 0; t < nPats; t++ ) |
| if ( Fraig_BitStringHasBit( pSims, pPats[t] ) ) |
| { |
| // check if this pattern falls into temporary storage |
| if ( p->iPatsPerm + t < p->iWordPerm * 32 ) |
| Fraig_BitStringSetBit( pSims, p->iPatsPerm + t ); |
| else |
| Fraig_BitStringSetBit( p->pSimsTemp, p->iPatsPerm + t ); |
| } |
| // copy the pattern |
| for ( w = p->iWordPerm; w < p->iWordStart; w++ ) |
| pSims[w] = p->pSimsTemp[w]; |
| // recompute the hashing info |
| uHash = 0; |
| for ( w = 0; w < p->iWordStart; w++ ) |
| uHash ^= pSims[w] * s_FraigPrimes[w]; |
| p->vInputs->pArray[i]->uHashD = uHash; |
| } |
| |
| // update info about the permanently stored patterns |
| p->iWordPerm = p->iWordStart; |
| p->iPatsPerm += nPats; |
| assert( p->iWordPerm == FRAIG_NUM_WORDS( p->iPatsPerm ) ); |
| |
| // resimulate and recompute the hash values |
| for ( i = 1; i < p->vNodes->nSize; i++ ) |
| if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) ) |
| { |
| p->vNodes->pArray[i]->uHashD = 0; |
| Fraig_NodeSimulate( p->vNodes->pArray[i], 0, p->iWordPerm, 0 ); |
| } |
| |
| // double-check that the nodes are still distinguished |
| if ( fPerformChecks ) |
| Fraig_FeedBackCheckTable( p ); |
| |
| // rehash the values in the F0 table |
| if ( p->fDoSparse ) |
| { |
| Fraig_TableRehashF0( p, 0 ); |
| if ( fPerformChecks ) |
| Fraig_FeedBackCheckTableF0( p ); |
| } |
| |
| // check if we need to resize the simulation info |
| // if less than FRAIG_WORDS_STORE words are left, reallocate simulation info |
| if ( p->iWordPerm + FRAIG_WORDS_STORE > p->nWordsDyna ) |
| Fraig_ReallocateSimulationInfo( p ); |
| |
| // set the real patterns |
| Msat_IntVecClear( p->vPatsReal ); |
| memset( p->pSimsReal, 0, sizeof(unsigned)*p->nWordsDyna ); |
| for ( w = 0; w < p->iWordPerm; w++ ) |
| p->pSimsReal[w] = FRAIG_FULL; |
| if ( p->iPatsPerm % 32 > 0 ) |
| p->pSimsReal[p->iWordPerm-1] = FRAIG_MASK( p->iPatsPerm % 32 ); |
| // printf( "The number of permanent words = %d.\n", p->iWordPerm ); |
| return p->iWordStart; |
| } |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks the correctness of the functional simulation table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats ) |
| { |
| Fraig_NodeVec_t * vColumns; |
| unsigned * pSims; |
| int * pHits, iPat, iCol, i; |
| int nOnesTotal, nSolStarting; |
| int fVeryVerbose = 0; |
| |
| // collect the pairs to be distinguished |
| vColumns = Fraig_FeedBackCoveringStart( p ); |
| // collect the number of 1s in each simulation vector |
| nOnesTotal = 0; |
| pHits = ABC_ALLOC( int, vColumns->nSize ); |
| for ( i = 0; i < vColumns->nSize; i++ ) |
| { |
| pSims = (unsigned *)vColumns->pArray[i]; |
| pHits[i] = Fraig_BitStringCountOnes( pSims, p->iWordStart ); |
| nOnesTotal += pHits[i]; |
| // assert( pHits[i] > 0 ); |
| } |
| |
| // go through the patterns |
| nSolStarting = Msat_IntVecReadSize(vPats); |
| while ( (iCol = Fraig_GetSmallestColumn( pHits, vColumns->nSize )) != -1 ) |
| { |
| // find the pattern, which hits this column |
| iPat = Fraig_GetHittingPattern( (unsigned *)vColumns->pArray[iCol], p->iWordStart ); |
| // cancel the columns covered by this pattern |
| Fraig_CancelCoveredColumns( vColumns, pHits, iPat ); |
| // save the pattern |
| Msat_IntVecPush( vPats, iPat ); |
| } |
| |
| // free the set of columns |
| for ( i = 0; i < vColumns->nSize; i++ ) |
| Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] ); |
| |
| // print stats related to the covering problem |
| if ( p->fVerbose && fVeryVerbose ) |
| { |
| printf( "%3d\\%3d\\%3d ", p->nWordsRand, p->nWordsDyna, p->iWordPerm ); |
| printf( "Col (pairs) = %5d. ", vColumns->nSize ); |
| printf( "Row (pats) = %5d. ", p->iWordStart * 32 ); |
| printf( "Dns = %6.2f %%. ", vColumns->nSize==0? 0.0 : 100.0 * nOnesTotal / vColumns->nSize / p->iWordStart / 32 ); |
| printf( "Sol = %3d (%3d). ", Msat_IntVecReadSize(vPats), nSolStarting ); |
| printf( "\n" ); |
| } |
| Fraig_NodeVecFree( vColumns ); |
| ABC_FREE( pHits ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks the correctness of the functional simulation table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p ) |
| { |
| Fraig_NodeVec_t * vColumns; |
| Fraig_HashTable_t * pT = p->pTableF; |
| Fraig_Node_t * pEntF, * pEntD; |
| unsigned * pSims; |
| unsigned * pUnsigned1, * pUnsigned2; |
| int i, k, m, w;//, nOnes; |
| |
| // start the set of columns |
| vColumns = Fraig_NodeVecAlloc( 100 ); |
| |
| // go through the pairs of nodes to be distinguished |
| for ( i = 0; i < pT->nBins; i++ ) |
| Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) |
| { |
| p->vCones->nSize = 0; |
| Fraig_TableBinForEachEntryD( pEntF, pEntD ) |
| Fraig_NodeVecPush( p->vCones, pEntD ); |
| if ( p->vCones->nSize == 1 ) |
| continue; |
| //////////////////////////////// bug fix by alanmi, September 14, 2006 |
| if ( p->vCones->nSize > 20 ) |
| continue; |
| //////////////////////////////// |
| |
| for ( k = 0; k < p->vCones->nSize; k++ ) |
| for ( m = k+1; m < p->vCones->nSize; m++ ) |
| { |
| if ( !Fraig_CompareSimInfoUnderMask( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0, p->pSimsReal ) ) |
| continue; |
| |
| // primary simulation patterns (counter-examples) cannot distinguish this pair |
| // get memory to store the feasible simulation patterns |
| pSims = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); |
| // find the pattern that distinguish this column, exept the primary ones |
| pUnsigned1 = p->vCones->pArray[k]->puSimD; |
| pUnsigned2 = p->vCones->pArray[m]->puSimD; |
| for ( w = 0; w < p->iWordStart; w++ ) |
| pSims[w] = (pUnsigned1[w] ^ pUnsigned2[w]) & ~p->pSimsReal[w]; |
| // store the pattern |
| Fraig_NodeVecPush( vColumns, (Fraig_Node_t *)pSims ); |
| // nOnes = Fraig_BitStringCountOnes(pSims, p->iWordStart); |
| // assert( nOnes > 0 ); |
| } |
| } |
| |
| // if the flag is not set, do not consider sparse nodes in p->pTableF0 |
| if ( !p->fDoSparse ) |
| return vColumns; |
| |
| // recalculate their hash values based on p->pSimsReal |
| pT = p->pTableF0; |
| for ( i = 0; i < pT->nBins; i++ ) |
| Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) |
| { |
| pSims = pEntF->puSimD; |
| pEntF->uHashD = 0; |
| for ( w = 0; w < p->iWordStart; w++ ) |
| pEntF->uHashD ^= (pSims[w] & p->pSimsReal[w]) * s_FraigPrimes[w]; |
| } |
| |
| // rehash the table using these values |
| Fraig_TableRehashF0( p, 1 ); |
| |
| // collect the classes of equivalent node pairs |
| for ( i = 0; i < pT->nBins; i++ ) |
| Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) |
| { |
| p->vCones->nSize = 0; |
| Fraig_TableBinForEachEntryD( pEntF, pEntD ) |
| Fraig_NodeVecPush( p->vCones, pEntD ); |
| if ( p->vCones->nSize == 1 ) |
| continue; |
| |
| // primary simulation patterns (counter-examples) cannot distinguish all these pairs |
| for ( k = 0; k < p->vCones->nSize; k++ ) |
| for ( m = k+1; m < p->vCones->nSize; m++ ) |
| { |
| // get memory to store the feasible simulation patterns |
| pSims = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims ); |
| // find the patterns that are not distinquished |
| pUnsigned1 = p->vCones->pArray[k]->puSimD; |
| pUnsigned2 = p->vCones->pArray[m]->puSimD; |
| for ( w = 0; w < p->iWordStart; w++ ) |
| pSims[w] = (pUnsigned1[w] ^ pUnsigned2[w]) & ~p->pSimsReal[w]; |
| // store the pattern |
| Fraig_NodeVecPush( vColumns, (Fraig_Node_t *)pSims ); |
| // nOnes = Fraig_BitStringCountOnes(pSims, p->iWordStart); |
| // assert( nOnes > 0 ); |
| } |
| } |
| return vColumns; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Selects the column, which has the smallest number of hits.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_GetSmallestColumn( int * pHits, int nHits ) |
| { |
| int i, iColMin = -1, nHitsMin = 1000000; |
| for ( i = 0; i < nHits; i++ ) |
| { |
| // skip covered columns |
| if ( pHits[i] == 0 ) |
| continue; |
| // take the column if it can only be covered by one pattern |
| if ( pHits[i] == 1 ) |
| return i; |
| // find the column, which requires the smallest number of patterns |
| if ( nHitsMin > pHits[i] ) |
| { |
| nHitsMin = pHits[i]; |
| iColMin = i; |
| } |
| } |
| return iColMin; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Select the pattern, which hits this column.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_GetHittingPattern( unsigned * pSims, int nWords ) |
| { |
| int i, b; |
| for ( i = 0; i < nWords; i++ ) |
| { |
| if ( pSims[i] == 0 ) |
| continue; |
| for ( b = 0; b < 32; b++ ) |
| if ( pSims[i] & (1 << b) ) |
| return i * 32 + b; |
| } |
| return -1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cancel covered patterns.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_CancelCoveredColumns( Fraig_NodeVec_t * vColumns, int * pHits, int iPat ) |
| { |
| unsigned * pSims; |
| int i; |
| for ( i = 0; i < vColumns->nSize; i++ ) |
| { |
| pSims = (unsigned *)vColumns->pArray[i]; |
| if ( Fraig_BitStringHasBit( pSims, iPat ) ) |
| pHits[i] = 0; |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks the correctness of the functional simulation table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBackCheckTable( Fraig_Man_t * p ) |
| { |
| Fraig_HashTable_t * pT = p->pTableF; |
| Fraig_Node_t * pEntF, * pEntD; |
| int i, k, m, nPairs; |
| |
| nPairs = 0; |
| for ( i = 0; i < pT->nBins; i++ ) |
| Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) |
| { |
| p->vCones->nSize = 0; |
| Fraig_TableBinForEachEntryD( pEntF, pEntD ) |
| Fraig_NodeVecPush( p->vCones, pEntD ); |
| if ( p->vCones->nSize == 1 ) |
| continue; |
| for ( k = 0; k < p->vCones->nSize; k++ ) |
| for ( m = k+1; m < p->vCones->nSize; m++ ) |
| { |
| if ( Fraig_CompareSimInfo( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0 ) ) |
| printf( "Nodes %d and %d have the same D simulation info.\n", |
| p->vCones->pArray[k]->Num, p->vCones->pArray[m]->Num ); |
| nPairs++; |
| } |
| } |
| // printf( "\nThe total of %d node pairs have been verified.\n", nPairs ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks the correctness of the functional simulation table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_FeedBackCheckTableF0( Fraig_Man_t * p ) |
| { |
| Fraig_HashTable_t * pT = p->pTableF0; |
| Fraig_Node_t * pEntF; |
| int i, k, m, nPairs; |
| |
| nPairs = 0; |
| for ( i = 0; i < pT->nBins; i++ ) |
| { |
| p->vCones->nSize = 0; |
| Fraig_TableBinForEachEntryF( pT->pBins[i], pEntF ) |
| Fraig_NodeVecPush( p->vCones, pEntF ); |
| if ( p->vCones->nSize == 1 ) |
| continue; |
| for ( k = 0; k < p->vCones->nSize; k++ ) |
| for ( m = k+1; m < p->vCones->nSize; m++ ) |
| { |
| if ( Fraig_CompareSimInfo( p->vCones->pArray[k], p->vCones->pArray[m], p->iWordStart, 0 ) ) |
| printf( "Nodes %d and %d have the same D simulation info.\n", |
| p->vCones->pArray[k]->Num, p->vCones->pArray[m]->Num ); |
| nPairs++; |
| } |
| } |
| // printf( "\nThe total of %d node pairs have been verified.\n", nPairs ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Doubles the size of simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) |
| { |
| Fraig_MemFixed_t * mmSimsNew; // new memory manager for simulation info |
| Fraig_Node_t * pNode; |
| unsigned * pSimsNew; |
| unsigned uSignOld; |
| int i; |
| |
| // allocate a new memory manager |
| p->nWordsDyna *= 2; |
| mmSimsNew = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) ); |
| |
| // set the new data for the constant node |
| pNode = p->pConst1; |
| pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| pNode->puSimD = pNode->puSimR + p->nWordsRand; |
| memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand ); |
| memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna ); |
| |
| // copy the simulation info of the PIs |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| { |
| pNode = p->vInputs->pArray[i]; |
| // copy the simulation info |
| pSimsNew = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| memmove( pSimsNew, pNode->puSimR, sizeof(unsigned) * (p->nWordsRand + p->iWordStart) ); |
| // attach the new info |
| pNode->puSimR = pSimsNew; |
| pNode->puSimD = pNode->puSimR + p->nWordsRand; |
| // signatures remain without changes |
| } |
| |
| // replace the manager to free up some memory |
| Fraig_MemFixedStop( p->mmSims, 0 ); |
| p->mmSims = mmSimsNew; |
| |
| // resimulate the internal nodes (this should lead to the same signatures) |
| for ( i = 1; i < p->vNodes->nSize; i++ ) |
| { |
| pNode = p->vNodes->pArray[i]; |
| if ( !Fraig_NodeIsAnd(pNode) ) |
| continue; |
| // allocate memory for the simulation info |
| pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| pNode->puSimD = pNode->puSimR + p->nWordsRand; |
| // derive random simulation info |
| uSignOld = pNode->uHashR; |
| pNode->uHashR = 0; |
| Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 ); |
| assert( uSignOld == pNode->uHashR ); |
| // derive dynamic simulation info |
| uSignOld = pNode->uHashD; |
| pNode->uHashD = 0; |
| Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 ); |
| assert( uSignOld == pNode->uHashD ); |
| } |
| |
| // realloc temporary storage |
| p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna ); |
| p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generated trivial counter example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ) |
| { |
| int * pModel; |
| pModel = ABC_ALLOC( int, p->vInputs->nSize ); |
| memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); |
| return pModel; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Saves the counter example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_ManSimulateBitNode_rec( Fraig_Man_t * p, Fraig_Node_t * pNode ) |
| { |
| int Value0, Value1; |
| if ( Fraig_NodeIsTravIdCurrent( p, pNode ) ) |
| return pNode->fMark3; |
| Fraig_NodeSetTravIdCurrent( p, pNode ); |
| Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) ); |
| Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) ); |
| Value0 ^= Fraig_IsComplement(pNode->p1); |
| Value1 ^= Fraig_IsComplement(pNode->p2); |
| pNode->fMark3 = Value0 & Value1; |
| return pNode->fMark3; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Simulates one bit.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fraig_ManSimulateBitNode( Fraig_Man_t * p, Fraig_Node_t * pNode, int * pModel ) |
| { |
| int fCompl, RetValue, i; |
| // set the PI values |
| Fraig_ManIncrementTravId( p ); |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| { |
| Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] ); |
| p->vInputs->pArray[i]->fMark3 = pModel[i]; |
| } |
| // perform the traversal |
| fCompl = Fraig_IsComplement(pNode); |
| RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) ); |
| return fCompl ^ RetValue; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Saves the counter example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ) |
| { |
| int * pModel; |
| int iPattern; |
| int i, fCompl; |
| |
| // the node can be complemented |
| fCompl = Fraig_IsComplement(pNode); |
| // because we compare with constant 0, p->pConst1 should also be complemented |
| fCompl = !fCompl; |
| |
| // derive the model |
| pModel = Fraig_ManAllocCounterExample( p ); |
| iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 ); |
| if ( iPattern >= 0 ) |
| { |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) ) |
| pModel[i] = 1; |
| /* |
| printf( "SAT solver's pattern:\n" ); |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| printf( "%d", pModel[i] ); |
| printf( "\n" ); |
| */ |
| assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); |
| return pModel; |
| } |
| iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 ); |
| if ( iPattern >= 0 ) |
| { |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) ) |
| pModel[i] = 1; |
| /* |
| printf( "SAT solver's pattern:\n" ); |
| for ( i = 0; i < p->vInputs->nSize; i++ ) |
| printf( "%d", pModel[i] ); |
| printf( "\n" ); |
| */ |
| assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); |
| return pModel; |
| } |
| ABC_FREE( pModel ); |
| return NULL; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
