/**CFile**************************************************************** FileName [fraigFeed.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] Synopsis [Procedures to support the solver feedback.] Author [Alan Mishchenko ] 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