/**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