Version abc70930

1 files changed, 0 insertions, 657 deletions

diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
deleted file mode 100644
index b68bbe0e..00000000
--- a/src/sat/fraig/fraigTable.c
+++ /dev/null
@@ -1,657 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "fraigInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Fraig_TableResizeS( Fraig_HashTable_t * p );
-static void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fraig_HashTable_t * Fraig_HashTableCreate( int nSize )
-{
-    Fraig_HashTable_t * p;
-    // allocate the table
-    p = ALLOC( Fraig_HashTable_t, 1 );
-    memset( p, 0, sizeof(Fraig_HashTable_t) );
-    // allocate and clean the bins
-    p->nBins = Cudd_PrimeFraig(nSize);
-    p->pBins = ALLOC( Fraig_Node_t *, p->nBins );
-    memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the supergate hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_HashTableFree( Fraig_HashTable_t * p )
-{
-    FREE( p->pBins );
-    FREE( p );
-}
-
-/**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     []
-
-***********************************************************************/
-int Fraig_HashTableLookupS( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, Fraig_Node_t ** ppNodeRes )
-{
-    Fraig_HashTable_t * p = pMan->pTableS;
-    Fraig_Node_t * pEnt;
-    unsigned Key;
-
-    // order the arguments
-    if ( Fraig_Regular(p1)->Num > Fraig_Regular(p2)->Num )
-        pEnt = p1, p1 = p2, p2 = pEnt;
-
-    Key = Fraig_HashKey2( p1, p2, p->nBins );
-    Fraig_TableBinForEachEntryS( p->pBins[Key], pEnt )
-        if ( pEnt->p1 == p1 && pEnt->p2 == p2 )
-        {
-            *ppNodeRes = pEnt;
-            return 1;
-        }
-    // check if it is a good time for table resizing
-    if ( p->nEntries >= 2 * p->nBins )
-    {
-        Fraig_TableResizeS( p );
-        Key = Fraig_HashKey2( p1, p2, p->nBins );
-    }
-    // create the new node
-    pEnt = Fraig_NodeCreate( pMan, p1, p2 );
-    // add the node to the corresponding linked list in the table
-    pEnt->pNextS = p->pBins[Key];
-    p->pBins[Key] = pEnt;
-    *ppNodeRes = pEnt;
-    p->nEntries++;
-    return 0;
-}
-
-
-/**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     []
-
-***********************************************************************/
-Fraig_Node_t * Fraig_HashTableLookupF( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    Fraig_HashTable_t * p = pMan->pTableF;
-    Fraig_Node_t * pEnt, * pEntD;
-    unsigned Key;
-
-    // go through the hash table entries
-    Key = pNode->uHashR % p->nBins;
-    Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
-    {
-        // if their simulation info differs, skip
-        if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->nWordsRand, 1 ) )
-            continue;
-        // equivalent up to the complement
-        Fraig_TableBinForEachEntryD( pEnt, pEntD )
-        {
-            // if their simulation info differs, skip
-            if ( !Fraig_CompareSimInfo( pNode, pEntD, pMan->iWordStart, 0 ) )
-                continue;
-            // found a simulation-equivalent node
-            return pEntD; 
-        }
-        // did not find a simulation equivalent node
-        // add the node to the corresponding linked list
-        pNode->pNextD = pEnt->pNextD;
-        pEnt->pNextD  = pNode;
-        // return NULL, because there is no functional equivalence in this case
-        return NULL;
-    }
-
-    // check if it is a good time for table resizing
-    if ( p->nEntries >= 2 * p->nBins )
-    {
-        Fraig_TableResizeF( p, 1 );
-        Key = pNode->uHashR % p->nBins;
-    }
-
-    // add the node to the corresponding linked list in the table
-    pNode->pNextF = p->pBins[Key];
-    p->pBins[Key] = pNode;
-    p->nEntries++;
-    // return NULL, because there is no functional equivalence in this case
-    return NULL;
-}
-
-/**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     []
-
-***********************************************************************/
-Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    Fraig_HashTable_t * p = pMan->pTableF0;
-    Fraig_Node_t * pEnt;
-    unsigned Key;
-
-    // go through the hash table entries
-    Key = pNode->uHashD % p->nBins;
-    Fraig_TableBinForEachEntryF( p->pBins[Key], pEnt )
-    {
-        // if their simulation info differs, skip
-        if ( !Fraig_CompareSimInfo( pNode, pEnt, pMan->iWordStart, 0 ) )
-            continue;
-        // found a simulation-equivalent node
-        return pEnt; 
-    }
-
-    // check if it is a good time for table resizing
-    if ( p->nEntries >= 2 * p->nBins )
-    {
-        Fraig_TableResizeF( p, 0 );
-        Key = pNode->uHashD % p->nBins;
-    }
-
-    // add the node to the corresponding linked list in the table
-    pNode->pNextF = p->pBins[Key];
-    p->pBins[Key] = pNode;
-    p->nEntries++;
-    // return NULL, because there is no functional equivalence in this case
-    return NULL;
-}
-
-/**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     []
-
-***********************************************************************/
-void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
-{
-    Fraig_HashTable_t * p = pMan->pTableF0;
-    unsigned Key = pNode->uHashD % p->nBins;
-
-    pNode->pNextF = p->pBins[Key];
-    p->pBins[Key] = pNode;
-    p->nEntries++;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_TableResizeS( Fraig_HashTable_t * p )
-{
-    Fraig_Node_t ** pBinsNew;
-    Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
-    unsigned Key;
-
-clk = clock();
-    // get the new table size
-    nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
-    // allocate a new array
-    pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
-    memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < p->nBins; i++ )
-        Fraig_TableBinForEachEntrySafeS( p->pBins[i], pEnt, pEnt2 )
-        {
-            Key = Fraig_HashKey2( pEnt->p1, pEnt->p2, nBinsNew );
-            pEnt->pNextS = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            Counter++;
-        }
-    assert( Counter == p->nEntries );
-//    printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( p->pBins );
-    p->pBins = pBinsNew;
-    p->nBins = nBinsNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR )
-{
-    Fraig_Node_t ** pBinsNew;
-    Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
-    unsigned Key;
-
-clk = clock();
-    // get the new table size
-    nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
-    // allocate a new array
-    pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
-    memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < p->nBins; i++ )
-        Fraig_TableBinForEachEntrySafeF( p->pBins[i], pEnt, pEnt2 )
-        {
-            if ( fUseSimR )
-                Key = pEnt->uHashR % nBinsNew;
-            else
-                Key = pEnt->uHashD % nBinsNew;
-            pEnt->pNextF = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            Counter++;
-        }
-    assert( Counter == p->nEntries );
-//    printf( "Increasing the functional table size from %6d to %6d. ", p->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( p->pBins );
-    p->pBins = pBinsNew;
-    p->nBins = nBinsNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two pieces of simulation info.]
-
-  Description [Returns 1 if they are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
-{
-    int i;
-    assert( !Fraig_IsComplement(pNode1) );
-    assert( !Fraig_IsComplement(pNode2) );
-    if ( fUseRand )
-    {
-        // if their signatures differ, skip
-        if ( pNode1->uHashR != pNode2->uHashR )
-            return 0;
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
-                return 0;
-    }
-    else
-    {
-        // if their signatures differ, skip
-        if ( pNode1->uHashD != pNode2->uHashD )
-            return 0;
-        // check the simulation info
-        for ( i = 0; i < iWordLast; i++ )
-            if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
-                return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the number of the different pattern.]
-
-  Description [Returns -1 if there is no such pattern]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand )
-{
-    int i, v;
-    assert( !Fraig_IsComplement(pNode1) );
-    assert( !Fraig_IsComplement(pNode2) );
-    // take into account possible internal complementation
-    fCompl ^= pNode1->fInv;
-    fCompl ^= pNode2->fInv;
-    // find the pattern
-    if ( fCompl )
-    {
-        if ( fUseRand )
-        {
-            for ( i = 0; i < iWordLast; i++ )
-                if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] )
-                    for ( v = 0; v < 32; v++ )
-                        if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) )
-                            return i * 32 + v;
-        }
-        else
-        {
-            for ( i = 0; i < iWordLast; i++ )
-                if ( pNode1->puSimD[i] !=  ~pNode2->puSimD[i] )
-                    for ( v = 0; v < 32; v++ )
-                        if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) )
-                            return i * 32 + v;
-        }
-    }
-    else
-    {
-        if ( fUseRand )
-        {
-            for ( i = 0; i < iWordLast; i++ )
-                if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
-                    for ( v = 0; v < 32; v++ )
-                        if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
-                            return i * 32 + v;
-        }
-        else
-        {
-            for ( i = 0; i < iWordLast; i++ )
-                if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
-                    for ( v = 0; v < 32; v++ )
-                        if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
-                            return i * 32 + v;
-        }
-    }
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two pieces of simulation info.]
-
-  Description [Returns 1 if they are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask )
-{
-    unsigned * pSims1, * pSims2;
-    int i;
-    assert( !Fraig_IsComplement(pNode1) );
-    assert( !Fraig_IsComplement(pNode2) );
-    // get hold of simulation info
-    pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
-    pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
-    // check the simulation info
-    for ( i = 0; i < iWordLast; i++ )
-        if ( (pSims1[i] & puMask[i]) != (pSims2[i] & puMask[i]) )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two pieces of simulation info.]
-
-  Description [Returns 1 if they are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask )
-{
-    unsigned * pSims1, * pSims2;
-    int i;
-    assert( !Fraig_IsComplement(pNode1) );
-    assert( !Fraig_IsComplement(pNode2) );
-    // get hold of simulation info
-    pSims1 = fUseRand? pNode1->puSimR : pNode1->puSimD;
-    pSims2 = fUseRand? pNode2->puSimR : pNode2->puSimD;    
-    // check the simulation info
-    for ( i = 0; i < iWordLast; i++ )
-        puMask[i] = ( pSims1[i] ^ pSims2[i] );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints stats of the structural table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_TablePrintStatsS( Fraig_Man_t * pMan )
-{
-    Fraig_HashTable_t * pT = pMan->pTableS;
-    Fraig_Node_t * pNode;
-    int i, Counter;
-
-    printf( "Structural table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
-    for ( i = 0; i < pT->nBins; i++ )
-    {
-        Counter = 0;
-        Fraig_TableBinForEachEntryS( pT->pBins[i], pNode )
-            Counter++;
-        if ( Counter > 1 )
-        {
-            printf( "%d ", Counter );
-            if ( Counter > 50 )
-                printf( "{%d} ", i );
-        }
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints stats of the structural table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_TablePrintStatsF( Fraig_Man_t * pMan )
-{
-    Fraig_HashTable_t * pT = pMan->pTableF;
-    Fraig_Node_t * pNode;
-    int i, Counter;
-
-    printf( "Functional table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
-    for ( i = 0; i < pT->nBins; i++ )
-    {
-        Counter = 0;
-        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
-            Counter++;
-        if ( Counter > 1 )
-            printf( "{%d} ", Counter );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints stats of the structural table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_TablePrintStatsF0( Fraig_Man_t * pMan )
-{
-    Fraig_HashTable_t * pT = pMan->pTableF0;
-    Fraig_Node_t * pNode;
-    int i, Counter;
-
-    printf( "Zero-node table. Table size = %d. Number of entries = %d.\n", pT->nBins, pT->nEntries );
-    for ( i = 0; i < pT->nBins; i++ )
-    {
-        Counter = 0;
-        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
-            Counter++;
-        if ( Counter == 0 )
-            continue;
-/*
-        printf( "\nBin = %4d :  Number of entries = %4d\n", i, Counter );
-        Fraig_TableBinForEachEntryF( pT->pBins[i], pNode )
-            printf( "Node %5d. Hash = %10d.\n", pNode->Num, pNode->uHashD );
-*/
-    }
-    printf( "\n" );
-}
-
-/**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     []
-
-***********************************************************************/
-int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv )
-{
-    Fraig_HashTable_t * pT = pMan->pTableF0;
-    Fraig_Node_t ** pBinsNew;
-    Fraig_Node_t * pEntF, * pEntF2, * pEnt, * pEntD2, * pEntN;
-    int ReturnValue, Counter, i;
-    unsigned Key;
-
-    // allocate a new array of bins
-    pBinsNew = ALLOC( Fraig_Node_t *, pT->nBins );
-    memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins );
-
-    // rehash the entries in the table
-    // go through all the nodes in the F-lists (and possible in D-lists, if used)
-    Counter = 0;
-    ReturnValue = 0;
-    for ( i = 0; i < pT->nBins; i++ )
-        Fraig_TableBinForEachEntrySafeF( pT->pBins[i], pEntF, pEntF2 )
-        Fraig_TableBinForEachEntrySafeD( pEntF, pEnt, pEntD2 )
-        {
-            // decide where to put entry pEnt
-            Key = pEnt->uHashD % pT->nBins;
-            if ( fLinkEquiv )
-            {
-                // go through the entries in the new bin
-                Fraig_TableBinForEachEntryF( pBinsNew[Key], pEntN )
-                {
-                    // if they have different values skip
-                    if ( pEnt->uHashD != pEntN->uHashD )
-                        continue;
-                    // they have the same hash value, add pEnt to the D-list pEnt3
-                    pEnt->pNextD  = pEntN->pNextD;
-                    pEntN->pNextD = pEnt;
-                    ReturnValue = 1;
-                    Counter++;
-                    break;
-                }
-                if ( pEntN != NULL ) // already linked
-                    continue;
-                // we did not find equal entry
-            }
-            // link the new entry
-            pEnt->pNextF  = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            pEnt->pNextD  = NULL;
-            Counter++;
-        }
-    assert( Counter == pT->nEntries );
-    // replace the table and the parameters
-    free( pT->pBins );
-    pT->pBins = pBinsNew;
-    return ReturnValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-