src/sat/fraig/fraigTable.c File Reference

#include "fraigInt.h"
Include dependency graph for fraigTable.c:

Go to the source code of this file.

Functions

static void Fraig_TableResizeS (Fraig_HashTable_t *p)
static void Fraig_TableResizeF (Fraig_HashTable_t *p, int fUseSimR)
Fraig_HashTable_t * Fraig_HashTableCreate (int nSize)
void Fraig_HashTableFree (Fraig_HashTable_t *p)
int Fraig_HashTableLookupS (Fraig_Man_t *pMan, Fraig_Node_t *p1, Fraig_Node_t *p2, Fraig_Node_t **ppNodeRes)
Fraig_Node_t * Fraig_HashTableLookupF (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Fraig_Node_t * Fraig_HashTableLookupF0 (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
void Fraig_HashTableInsertF0 (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int Fraig_CompareSimInfo (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand)
int Fraig_FindFirstDiff (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int fCompl, int iWordLast, int fUseRand)
int Fraig_CompareSimInfoUnderMask (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand, unsigned *puMask)
void Fraig_CollectXors (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand, unsigned *puMask)
void Fraig_TablePrintStatsS (Fraig_Man_t *pMan)
void Fraig_TablePrintStatsF (Fraig_Man_t *pMan)
void Fraig_TablePrintStatsF0 (Fraig_Man_t *pMan)
int Fraig_TableRehashF0 (Fraig_Man_t *pMan, int fLinkEquiv)

Function Documentation

void Fraig_CollectXors ( Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  iWordLast,
int  fUseRand,
unsigned *  puMask 
)

Function*************************************************************

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 473 of file fraigTable.c.

00474 {
00475     unsigned * pSims1, * pSims2;
00476     int i;
00477     assert( !Fraig_IsComplement(pNode1) );
00478     assert( !Fraig_IsComplement(pNode2) );
00479     // get hold of simulation info
00480     pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
00481     pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
00482     // check the simulation info
00483     for ( i = 0; i < iWordLast; i++ )
00484         puMask[i] = ( pSims1[i] ^ pSims2[i] );
00485 }

int Fraig_CompareSimInfo ( Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  iWordLast,
int  fUseRand 
)

Function*************************************************************

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 346 of file fraigTable.c.

00347 {
00348     int i;
00349     assert( !Fraig_IsComplement(pNode1) );
00350     assert( !Fraig_IsComplement(pNode2) );
00351     if ( fUseRand )
00352     {
00353         // if their signatures differ, skip
00354         if ( pNode1->uHashR != pNode2->uHashR )
00355             return 0;
00356         // check the simulation info
00357         for ( i = 0; i < iWordLast; i++ )
00358             if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
00359                 return 0;
00360     }
00361     else
00362     {
00363         // if their signatures differ, skip
00364         if ( pNode1->uHashD != pNode2->uHashD )
00365             return 0;
00366         // check the simulation info
00367         for ( i = 0; i < iWordLast; i++ )
00368             if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
00369                 return 0;
00370     }
00371     return 1;
00372 }

int Fraig_CompareSimInfoUnderMask ( Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  iWordLast,
int  fUseRand,
unsigned *  puMask 
)

Function*************************************************************

Synopsis [Compares two pieces of simulation info.]

Description [Returns 1 if they are equal.]

SideEffects []

SeeAlso []

Definition at line 446 of file fraigTable.c.

00447 {
00448     unsigned * pSims1, * pSims2;
00449     int i;
00450     assert( !Fraig_IsComplement(pNode1) );
00451     assert( !Fraig_IsComplement(pNode2) );
00452     // get hold of simulation info
00453     pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
00454     pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
00455     // check the simulation info
00456     for ( i = 0; i < iWordLast; i++ )
00457         if ( (pSims1[i] & puMask[i]) != (pSims2[i] & puMask[i]) )
00458             return 0;
00459     return 1;
00460 }

int Fraig_FindFirstDiff ( Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  fCompl,
int  iWordLast,
int  fUseRand 
)

Function*************************************************************

Synopsis [Find the number of the different pattern.]

Description [Returns -1 if there is no such pattern]

SideEffects []

SeeAlso []

Definition at line 385 of file fraigTable.c.

00386 {
00387     int i, v;
00388     assert( !Fraig_IsComplement(pNode1) );
00389     assert( !Fraig_IsComplement(pNode2) );
00390     // take into account possible internal complementation
00391     fCompl ^= pNode1->fInv;
00392     fCompl ^= pNode2->fInv;
00393     // find the pattern
00394     if ( fCompl )
00395     {
00396         if ( fUseRand )
00397         {
00398             for ( i = 0; i < iWordLast; i++ )
00399                 if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] )
00400                     for ( v = 0; v < 32; v++ )
00401                         if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) )
00402                             return i * 32 + v;
00403         }
00404         else
00405         {
00406             for ( i = 0; i < iWordLast; i++ )
00407                 if ( pNode1->puSimD[i] !=  ~pNode2->puSimD[i] )
00408                     for ( v = 0; v < 32; v++ )
00409                         if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) )
00410                             return i * 32 + v;
00411         }
00412     }
00413     else
00414     {
00415         if ( fUseRand )
00416         {
00417             for ( i = 0; i < iWordLast; i++ )
00418                 if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
00419                     for ( v = 0; v < 32; v++ )
00420                         if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
00421                             return i * 32 + v;
00422         }
00423         else
00424         {
00425             for ( i = 0; i < iWordLast; i++ )
00426                 if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
00427                     for ( v = 0; v < 32; v++ )
00428                         if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
00429                             return i * 32 + v;
00430         }
00431     }
00432     return -1;
00433 }

Fraig_HashTable_t* Fraig_HashTableCreate ( int  nSize  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigTable.c.

00044 {
00045     Fraig_HashTable_t * p;
00046     // allocate the table
00047     p = ALLOC( Fraig_HashTable_t, 1 );
00048     memset( p, 0, sizeof(Fraig_HashTable_t) );
00049     // allocate and clean the bins
00050     p->nBins = Cudd_PrimeFraig(nSize);
00051     p->pBins = ALLOC( Fraig_Node_t *, p->nBins );
00052     memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins );
00053     return p;
00054 }

void Fraig_HashTableFree ( Fraig_HashTable_t *  p  ) 

Function*************************************************************

Synopsis [Deallocates the supergate hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 67 of file fraigTable.c.

00068 {
00069     FREE( p->pBins );
00070     FREE( p );
00071 }

void Fraig_HashTableInsertF0 ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Insert the entry in the functional hash table.]

Description [Unconditionally add the node to the corresponding linked list in the table.]

SideEffects []

SeeAlso []

Definition at line 234 of file fraigTable.c.

00235 {
00236     Fraig_HashTable_t * p = pMan->pTableF0;
00237     unsigned Key = pNode->uHashD % p->nBins;
00238 
00239     pNode->pNextF = p->pBins[Key];
00240     p->pBins[Key] = pNode;
00241     p->nEntries++;
00242 }

Fraig_Node_t* Fraig_HashTableLookupF ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Insert the entry in the functional hash table.]

Description [If the entry with the same key exists, return it right away. If the entry with the same key does not exists, inserts it and returns NULL. ]

SideEffects []

SeeAlso []

Definition at line 133 of file fraigTable.c.

00134 {
00135     Fraig_HashTable_t * p = pMan->pTableF;
00136     Fraig_Node_t * pEnt, * pEntD;
00137     unsigned Key;
00138 
00139     // go through the hash table entries
00140     Key = pNode->uHashR % p->nBins;
00141     Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
00142     {
00143         // if their simulation info differs, skip
00144         if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->nWordsRand, 1 ) )
00145             continue;
00146         // equivalent up to the complement
00147         Fraig_TableBinForEachEntryD( pEnt, pEntD )
00148         {
00149             // if their simulation info differs, skip
00150             if ( !Fraig_CompareSimInfo( pNode, pEntD, pMan->iWordStart, 0 ) )
00151                 continue;
00152             // found a simulation-equivalent node
00153             return pEntD; 
00154         }
00155         // did not find a simulation equivalent node
00156         // add the node to the corresponding linked list
00157         pNode->pNextD = pEnt->pNextD;
00158         pEnt->pNextD  = pNode;
00159         // return NULL, because there is no functional equivalence in this case
00160         return NULL;
00161     }
00162 
00163     // check if it is a good time for table resizing
00164     if ( p->nEntries >= 2 * p->nBins )
00165     {
00166         Fraig_TableResizeF( p, 1 );
00167         Key = pNode->uHashR % p->nBins;
00168     }
00169 
00170     // add the node to the corresponding linked list in the table
00171     pNode->pNextF = p->pBins[Key];
00172     p->pBins[Key] = pNode;
00173     p->nEntries++;
00174     // return NULL, because there is no functional equivalence in this case
00175     return NULL;
00176 }

Fraig_Node_t* Fraig_HashTableLookupF0 ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Insert the entry in the functional hash table.]

Description [If the entry with the same key exists, return it right away. If the entry with the same key does not exists, inserts it and returns NULL. ]

SideEffects []

SeeAlso []

Definition at line 190 of file fraigTable.c.

00191 {
00192     Fraig_HashTable_t * p = pMan->pTableF0;
00193     Fraig_Node_t * pEnt;
00194     unsigned Key;
00195 
00196     // go through the hash table entries
00197     Key = pNode->uHashD % p->nBins;
00198     Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
00199     {
00200         // if their simulation info differs, skip
00201         if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->iWordStart, 0 ) )
00202             continue;
00203         // found a simulation-equivalent node
00204         return pEnt; 
00205     }
00206 
00207     // check if it is a good time for table resizing
00208     if ( p->nEntries >= 2 * p->nBins )
00209     {
00210         Fraig_TableResizeF( p, 0 );
00211         Key = pNode->uHashD % p->nBins;
00212     }
00213 
00214     // add the node to the corresponding linked list in the table
00215     pNode->pNextF = p->pBins[Key];
00216     p->pBins[Key] = pNode;
00217     p->nEntries++;
00218     // return NULL, because there is no functional equivalence in this case
00219     return NULL;
00220 }

int Fraig_HashTableLookupS ( Fraig_Man_t *  pMan,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2,
Fraig_Node_t **  ppNodeRes 
)

Function*************************************************************

Synopsis [Looks up an entry in the structural hash table.]

Description [If the entry with the same children does not exists, creates it, inserts it into the table, and returns 0. If the entry with the same children exists, finds it, and return 1. In both cases, the new/old entry is returned in ppNodeRes.]

SideEffects []

SeeAlso []

Definition at line 87 of file fraigTable.c.

00088 {
00089     Fraig_HashTable_t * p = pMan->pTableS;
00090     Fraig_Node_t * pEnt;
00091     unsigned Key;
00092 
00093     // order the arguments
00094     if ( Fraig_Regular(p1)->Num > Fraig_Regular(p2)->Num )
00095         pEnt = p1, p1 = p2, p2 = pEnt;
00096 
00097     Key = Fraig_HashKey2( p1, p2, p->nBins );
00098     Fraig_TableBinForEachEntryS( p->pBins[Key], pEnt )
00099         if ( pEnt->p1 == p1 && pEnt->p2 == p2 )
00100         {
00101             *ppNodeRes = pEnt;
00102             return 1;
00103         }
00104     // check if it is a good time for table resizing
00105     if ( p->nEntries >= 2 * p->nBins )
00106     {
00107         Fraig_TableResizeS( p );
00108         Key = Fraig_HashKey2( p1, p2, p->nBins );
00109     }
00110     // create the new node
00111     pEnt = Fraig_NodeCreate( pMan, p1, p2 );
00112     // add the node to the corresponding linked list in the table
00113     pEnt->pNextS = p->pBins[Key];
00114     p->pBins[Key] = pEnt;
00115     *ppNodeRes = pEnt;
00116     p->nEntries++;
00117     return 0;
00118 }

void Fraig_TablePrintStatsF ( Fraig_Man_t *  pMan  ) 

Function*************************************************************

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 532 of file fraigTable.c.

00533 {
00534     Fraig_HashTable_t * pT = pMan->pTableF;
00535     Fraig_Node_t * pNode;
00536     int i, Counter;
00537 
00538     printf( "Functional table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
00539     for ( i = 0; i < pT->nBins; i++ )
00540     {
00541         Counter = 0;
00542         Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
00543             Counter++;
00544         if ( Counter > 1 )
00545             printf( "{%d} ", Counter );
00546     }
00547     printf( "\n" );
00548 }

void Fraig_TablePrintStatsF0 ( Fraig_Man_t *  pMan  ) 

Function*************************************************************

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 561 of file fraigTable.c.

00562 {
00563     Fraig_HashTable_t * pT = pMan->pTableF0;
00564     Fraig_Node_t * pNode;
00565     int i, Counter;
00566 
00567     printf( "Zero-node table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
00568     for ( i = 0; i < pT->nBins; i++ )
00569     {
00570         Counter = 0;
00571         Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
00572             Counter++;
00573         if ( Counter == 0 )
00574             continue;
00575 /*
00576         printf( "\nBin = %4d :  Number of entries = %4d\n", i, Counter );
00577         Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
00578             printf( "Node %5d. Hash = %10d.\n", pNode->Num, pNode->uHashD );
00579 */
00580     }
00581     printf( "\n" );
00582 }

void Fraig_TablePrintStatsS ( Fraig_Man_t *  pMan  ) 

Function*************************************************************

Synopsis [Prints stats of the structural table.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file fraigTable.c.

00500 {
00501     Fraig_HashTable_t * pT = pMan->pTableS;
00502     Fraig_Node_t * pNode;
00503     int i, Counter;
00504 
00505     printf( "Structural table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
00506     for ( i = 0; i < pT->nBins; i++ )
00507     {
00508         Counter = 0;
00509         Fraig_TableBinForEachEntryS( pT->pBins[i], pNode )
00510             Counter++;
00511         if ( Counter > 1 )
00512         {
00513             printf( "%d ", Counter );
00514             if ( Counter > 50 )
00515                 printf( "{%d} ", i );
00516         }
00517     }
00518     printf( "\n" );
00519 }

int Fraig_TableRehashF0 ( Fraig_Man_t *  pMan,
int  fLinkEquiv 
)

Function*************************************************************

Synopsis [Rehashes the table after the simulation info has changed.]

Description [Assumes that the hash values have been updated after performing additional simulation. Rehashes the table using the new hash values. Uses pNextF to link the entries in the bins. Uses pNextD to link the entries with identical hash values. Returns 1 if the identical entries have been found. Note that identical hash values may mean that the simulation data is different.]

SideEffects []

SeeAlso []

Definition at line 599 of file fraigTable.c.

00600 {
00601     Fraig_HashTable_t * pT = pMan->pTableF0;
00602     Fraig_Node_t ** pBinsNew;
00603     Fraig_Node_t * pEntF, * pEntF2, * pEnt, * pEntD2, * pEntN;
00604     int ReturnValue, Counter, i;
00605     unsigned Key;
00606 
00607     // allocate a new array of bins
00608     pBinsNew = ALLOC( Fraig_Node_t *, pT->nBins );
00609     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins );
00610 
00611     // rehash the entries in the table
00612     // go through all the nodes in the F-lists (and possible in D-lists, if used)
00613     Counter = 0;
00614     ReturnValue = 0;
00615     for ( i = 0; i < pT->nBins; i++ )
00616         Fraig_TableBinForEachEntrySafeF( pT->pBins[i], pEntF, pEntF2 )
00617         Fraig_TableBinForEachEntrySafeD( pEntF, pEnt, pEntD2 )
00618         {
00619             // decide where to put entry pEnt
00620             Key = pEnt->uHashD % pT->nBins;
00621             if ( fLinkEquiv )
00622             {
00623                 // go through the entries in the new bin
00624                 Fraig_TableBinForEachEntryF( pBinsNew[Key], pEntN )
00625                 {
00626                     // if they have different values skip
00627                     if ( pEnt->uHashD != pEntN->uHashD )
00628                         continue;
00629                     // they have the same hash value, add pEnt to the D-list pEnt3
00630                     pEnt->pNextD  = pEntN->pNextD;
00631                     pEntN->pNextD = pEnt;
00632                     ReturnValue = 1;
00633                     Counter++;
00634                     break;
00635                 }
00636                 if ( pEntN != NULL ) // already linked
00637                     continue;
00638                 // we did not find equal entry
00639             }
00640             // link the new entry
00641             pEnt->pNextF  = pBinsNew[Key];
00642             pBinsNew[Key] = pEnt;
00643             pEnt->pNextD  = NULL;
00644             Counter++;
00645         }
00646     assert( Counter == pT->nEntries );
00647     // replace the table and the parameters
00648     free( pT->pBins );
00649     pT->pBins = pBinsNew;
00650     return ReturnValue;
00651 }

void Fraig_TableResizeF ( Fraig_HashTable_t *  p,
int  fUseSimR 
) [static]

Function*************************************************************

Synopsis [Resizes the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file fraigTable.c.

00300 {
00301     Fraig_Node_t ** pBinsNew;
00302     Fraig_Node_t * pEnt, * pEnt2;
00303     int nBinsNew, Counter, i, clk;
00304     unsigned Key;
00305 
00306 clk = clock();
00307     // get the new table size
00308     nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
00309     // allocate a new array
00310     pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
00311     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
00312     // rehash the entries from the old table
00313     Counter = 0;
00314     for ( i = 0; i < p->nBins; i++ )
00315         Fraig_TableBinForEachEntrySafeF( p->pBins[i], pEnt, pEnt2 )
00316         {
00317             if ( fUseSimR )
00318                 Key = pEnt->uHashR % nBinsNew;
00319             else
00320                 Key = pEnt->uHashD % nBinsNew;
00321             pEnt->pNextF = pBinsNew[Key];
00322             pBinsNew[Key] = pEnt;
00323             Counter++;
00324         }
00325     assert( Counter == p->nEntries );
00326 //    printf( "Increasing the functional table size from %6d to %6d. ", p->nBins, nBinsNew );
00327 //    PRT( "Time", clock() - clk );
00328     // replace the table and the parameters
00329     free( p->pBins );
00330     p->pBins = pBinsNew;
00331     p->nBins = nBinsNew;
00332 }

void Fraig_TableResizeS ( Fraig_HashTable_t *  p  )  [static]

CFile****************************************************************

FileName [fraigTable.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Structural and functional hash tables.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id
fraigTable.c,v 1.7 2005/07/08 01:01:34 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Resizes the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 256 of file fraigTable.c.

00257 {
00258     Fraig_Node_t ** pBinsNew;
00259     Fraig_Node_t * pEnt, * pEnt2;
00260     int nBinsNew, Counter, i, clk;
00261     unsigned Key;
00262 
00263 clk = clock();
00264     // get the new table size
00265     nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
00266     // allocate a new array
00267     pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
00268     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
00269     // rehash the entries from the old table
00270     Counter = 0;
00271     for ( i = 0; i < p->nBins; i++ )
00272         Fraig_TableBinForEachEntrySafeS( p->pBins[i], pEnt, pEnt2 )
00273         {
00274             Key = Fraig_HashKey2( pEnt->p1, pEnt->p2, nBinsNew );
00275             pEnt->pNextS = pBinsNew[Key];
00276             pBinsNew[Key] = pEnt;
00277             Counter++;
00278         }
00279     assert( Counter == p->nEntries );
00280 //    printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );
00281 //    PRT( "Time", clock() - clk );
00282     // replace the table and the parameters
00283     free( p->pBins );
00284     p->pBins = pBinsNew;
00285     p->nBins = nBinsNew;
00286 }

Generated on Tue Jan 5 12:19:39 2010 for abc70930 by  doxygen 1.6.1