src/sat/fraig/fraigInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "fraig.h"
#include "msat.h"
Include dependency graph for fraigInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Fraig_ManStruct_t_
struct  Fraig_NodeStruct_t_
struct  Fraig_NodeVecStruct_t_
struct  Fraig_HashTableStruct_t_

Defines

#define FRAIG_ENABLE_FANOUTS
#define FRAIG_PATTERNS_RANDOM   2048
#define FRAIG_PATTERNS_DYNAMIC   2048
#define FRAIG_MAX_PRIMES   1024
#define FRAIG_WORDS_STORE   5
#define FRAIG_MASK(n)   ((~((unsigned)0)) >> (32-(n)))
#define FRAIG_FULL   (~((unsigned)0))
#define FRAIG_NUM_WORDS(n)   (((n)>>5) + (((n)&31) > 0))
#define FRAIG_MIN(a, b)   (((a) < (b))? (a) : (b))
#define FRAIG_MAX(a, b)   (((a) > (b))? (a) : (b))
#define FRAIG_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
#define Fraig_BitStringSetBit(p, i)   ((p)[(i)>>5] |= (1<<((i) & 31)))
#define Fraig_BitStringXorBit(p, i)   ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define Fraig_BitStringHasBit(p, i)   (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
#define Fraig_NodeSetVarStr(p, i)   Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)
#define Fraig_NodeHasVarStr(p, i)   Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)
#define Fraig_PrintTime(a, t)   printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
#define Fraig_HashKey2(a, b, TSIZE)   (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE)
#define Fraig_NodeReadNextFanout(pNode, pFanout)
#define Fraig_NodeReadNextFanoutPlace(pNode, pFanout)
#define Fraig_NodeForEachFanout(pNode, pFanout)
#define Fraig_NodeForEachFanoutSafe(pNode, pFanout, pFanout2)
#define Fraig_TableBinForEachEntryS(pBin, pEnt)
#define Fraig_TableBinForEachEntrySafeS(pBin, pEnt, pEnt2)
#define Fraig_TableBinForEachEntryF(pBin, pEnt)
#define Fraig_TableBinForEachEntrySafeF(pBin, pEnt, pEnt2)
#define Fraig_TableBinForEachEntryD(pBin, pEnt)
#define Fraig_TableBinForEachEntrySafeD(pBin, pEnt, pEnt2)
#define Fraig_TableBinForEachEntryE(pBin, pEnt)
#define Fraig_TableBinForEachEntrySafeE(pBin, pEnt, pEnt2)

Typedefs

typedef struct Fraig_MemFixed_t_ Fraig_MemFixed_t

Functions

Fraig_Node_t * Fraig_NodeAndCanon (Fraig_Man_t *pMan, Fraig_Node_t *p1, Fraig_Node_t *p2)
void Fraig_NodeAddFaninFanout (Fraig_Node_t *pFanin, Fraig_Node_t *pFanout)
void Fraig_NodeRemoveFaninFanout (Fraig_Node_t *pFanin, Fraig_Node_t *pFanoutToRemove)
int Fraig_NodeGetFanoutNum (Fraig_Node_t *pNode)
void Fraig_FeedBackInit (Fraig_Man_t *p)
void Fraig_FeedBack (Fraig_Man_t *p, int *pModel, Msat_IntVec_t *vVars, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
void Fraig_FeedBackTest (Fraig_Man_t *p)
int Fraig_FeedBackCompress (Fraig_Man_t *p)
int * Fraig_ManAllocCounterExample (Fraig_Man_t *p)
int * Fraig_ManSaveCounterExample (Fraig_Man_t *p, Fraig_Node_t *pNode)
void Fraig_ManCreateSolver (Fraig_Man_t *p)
Fraig_MemFixed_t * Fraig_MemFixedStart (int nEntrySize)
void Fraig_MemFixedStop (Fraig_MemFixed_t *p, int fVerbose)
char * Fraig_MemFixedEntryFetch (Fraig_MemFixed_t *p)
void Fraig_MemFixedEntryRecycle (Fraig_MemFixed_t *p, char *pEntry)
void Fraig_MemFixedRestart (Fraig_MemFixed_t *p)
int Fraig_MemFixedReadMemUsage (Fraig_MemFixed_t *p)
Fraig_Node_t * Fraig_NodeCreateConst (Fraig_Man_t *p)
Fraig_Node_t * Fraig_NodeCreatePi (Fraig_Man_t *p)
Fraig_Node_t * Fraig_NodeCreate (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
void Fraig_NodeSimulate (Fraig_Node_t *pNode, int iWordStart, int iWordStop, int fUseRand)
unsigned int Cudd_PrimeFraig (unsigned int p)
int Fraig_NodeIsImplication (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
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_CompareSimInfoUnderMask (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand, unsigned *puMask)
int Fraig_FindFirstDiff (Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int fCompl, int iWordLast, int fUseRand)
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)
int Fraig_NodeCountPis (Msat_IntVec_t *vVars, int nVarsPi)
int Fraig_NodeCountSuppVars (Fraig_Man_t *p, Fraig_Node_t *pNode, int fSuppStr)
int Fraig_NodesCompareSupps (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int Fraig_NodeAndSimpleCase_rec (Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int Fraig_NodeIsExorType (Fraig_Node_t *pNode)
void Fraig_ManSelectBestChoice (Fraig_Man_t *p)
int Fraig_BitStringCountOnes (unsigned *pString, int nWords)
void Fraig_PrintBinary (FILE *pFile, unsigned *pSign, int nBits)
int Fraig_NodeIsExor (Fraig_Node_t *pNode)
int Fraig_NodeIsMuxType (Fraig_Node_t *pNode)
Fraig_Node_t * Fraig_NodeRecognizeMux (Fraig_Node_t *pNode, Fraig_Node_t **ppNodeT, Fraig_Node_t **ppNodeE)
int Fraig_ManCountExors (Fraig_Man_t *pMan)
int Fraig_ManCountMuxes (Fraig_Man_t *pMan)
int Fraig_NodeSimsContained (Fraig_Man_t *pMan, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2)
int Fraig_NodeIsInSupergate (Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Fraig_NodeVec_t * Fraig_CollectSupergate (Fraig_Node_t *pNode, int fStopAtMux)
int Fraig_CountPis (Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
void Fraig_ManIncrementTravId (Fraig_Man_t *pMan)
void Fraig_NodeSetTravIdCurrent (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int Fraig_NodeIsTravIdCurrent (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int Fraig_NodeIsTravIdPrevious (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
void Fraig_NodeVecSortByRefCount (Fraig_NodeVec_t *p)

Variables

int s_FraigPrimes [FRAIG_MAX_PRIMES]

Define Documentation

#define Fraig_BitStringHasBit ( p,
i   )     (((p)[(i)>>5] & (1<<((i) & 31))) > 0)

Definition at line 81 of file fraigInt.h.

#define Fraig_BitStringSetBit ( p,
i   )     ((p)[(i)>>5] |= (1<<((i) & 31)))

Definition at line 79 of file fraigInt.h.

#define Fraig_BitStringXorBit ( p,
i   )     ((p)[(i)>>5] ^= (1<<((i) & 31)))

Definition at line 80 of file fraigInt.h.

#define FRAIG_ENABLE_FANOUTS

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

FileName [fraigInt.h]

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

Synopsis [Internal declarations of the FRAIG package.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigInt.h,v 1.15 2005/07/08 01:01:31 alanmi Exp

] INCLUDES /// PARAMETERS /// MACRO DEFINITIONS ///

Definition at line 54 of file fraigInt.h.

#define FRAIG_FULL   (~((unsigned)0))

Definition at line 68 of file fraigInt.h.

#define Fraig_HashKey2 ( a,
b,
TSIZE   )     (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE)

Definition at line 109 of file fraigInt.h.

#define FRAIG_MASK ( n   )     ((~((unsigned)0)) >> (32-(n)))

Definition at line 67 of file fraigInt.h.

#define FRAIG_MAX ( a,
b   )     (((a) > (b))? (a) : (b))

Definition at line 73 of file fraigInt.h.

#define FRAIG_MAX_PRIMES   1024

Definition at line 57 of file fraigInt.h.

#define FRAIG_MIN ( a,
b   )     (((a) < (b))? (a) : (b))

Definition at line 72 of file fraigInt.h.

#define Fraig_NodeForEachFanout ( pNode,
pFanout   ) 
Value:
for ( pFanout = (pNode)->pFanPivot; pFanout;                  \
          pFanout = Fraig_NodeReadNextFanout(pNode, pFanout) )

Definition at line 309 of file fraigInt.h.

#define Fraig_NodeForEachFanoutSafe ( pNode,
pFanout,
pFanout2   ) 
Value:
for ( pFanout  = (pNode)->pFanPivot,                          \
          pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout);    \
          pFanout;                                                \
          pFanout  = pFanout2,                                    \
          pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout) )

Definition at line 313 of file fraigInt.h.

#define Fraig_NodeHasVarStr ( p,
i   )     Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)

Definition at line 87 of file fraigInt.h.

#define Fraig_NodeReadNextFanout ( pNode,
pFanout   ) 
Value:
( ( pFanout == NULL )? NULL :                                 \
        ((Fraig_Regular((pFanout)->p1) == (pNode))?               \
             (pFanout)->pFanFanin1 : (pFanout)->pFanFanin2) )

Definition at line 300 of file fraigInt.h.

#define Fraig_NodeReadNextFanoutPlace ( pNode,
pFanout   ) 
Value:
( (Fraig_Regular((pFanout)->p1) == (pNode))?                  \
         &(pFanout)->pFanFanin1 : &(pFanout)->pFanFanin2 )

Definition at line 305 of file fraigInt.h.

#define Fraig_NodeSetVarStr ( p,
i   )     Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)

Definition at line 86 of file fraigInt.h.

#define FRAIG_NUM_WORDS ( n   )     (((n)>>5) + (((n)&31) > 0))

Definition at line 69 of file fraigInt.h.

#define FRAIG_PATTERNS_DYNAMIC   2048

Definition at line 56 of file fraigInt.h.

#define FRAIG_PATTERNS_RANDOM   2048

Definition at line 55 of file fraigInt.h.

#define Fraig_PrintTime ( a,
t   )     printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )

Definition at line 107 of file fraigInt.h.

#define FRAIG_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))

Definition at line 76 of file fraigInt.h.

#define Fraig_TableBinForEachEntryD ( pBin,
pEnt   ) 
Value:
for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextD )

Definition at line 344 of file fraigInt.h.

#define Fraig_TableBinForEachEntryE ( pBin,
pEnt   ) 
Value:
for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextE )

Definition at line 355 of file fraigInt.h.

#define Fraig_TableBinForEachEntryF ( pBin,
pEnt   ) 
Value:
for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextF )

Definition at line 333 of file fraigInt.h.

#define Fraig_TableBinForEachEntryS ( pBin,
pEnt   ) 
Value:
for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = pEnt->pNextS )

Definition at line 322 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeD ( pBin,
pEnt,
pEnt2   ) 
Value:
for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextD: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextD: NULL )

Definition at line 348 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeE ( pBin,
pEnt,
pEnt2   ) 
Value:
for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextE: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextE: NULL )

Definition at line 359 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeF ( pBin,
pEnt,
pEnt2   ) 
Value:
for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextF: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextF: NULL )

Definition at line 337 of file fraigInt.h.

#define Fraig_TableBinForEachEntrySafeS ( pBin,
pEnt,
pEnt2   ) 
Value:
for ( pEnt = pBin,                                            \
          pEnt2 = pEnt? pEnt->pNextS: NULL;                       \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? pEnt->pNextS: NULL )

Definition at line 326 of file fraigInt.h.

#define FRAIG_WORDS_STORE   5

Definition at line 64 of file fraigInt.h.

Typedef Documentation

typedef struct Fraig_MemFixed_t_ Fraig_MemFixed_t

STRUCTURE DEFINITIONS ///

Definition at line 122 of file fraigInt.h.

Function Documentation

unsigned int Cudd_PrimeFraig ( unsigned int  p  ) 

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

Synopsis [Returns the next prime >= p.]

Description [Copied from CUDD, for stand-aloneness.]

SideEffects [None]

SeeAlso []

Definition at line 115 of file fraigPrime.c.

00116 {
00117     int i,pn;
00118 
00119     p--;
00120     do {
00121         p++;
00122         if (p&1) {
00123             pn = 1;
00124             i = 3;
00125             while ((unsigned) (i * i) <= p) {
00126                 if (p % i == 0) {
00127                     pn = 0;
00128                     break;
00129                 }
00130                 i += 2;
00131             }
00132         } else {
00133             pn = 0;
00134         }
00135     } while (!pn);
00136     return(p);
00137 
00138 } /* end of Cudd_Prime */

int Fraig_BitStringCountOnes ( unsigned *  pString,
int  nWords 
)

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

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file fraigUtil.c.

00286 {
00287     unsigned char * pSuppBytes = (unsigned char *)pString;
00288     int i, nOnes, nBytes = sizeof(unsigned) * nWords;
00289     // count the number of ones in the simulation vector
00290     for ( i = nOnes = 0; i < nBytes; i++ )
00291         nOnes += bit_count[pSuppBytes[i]];
00292     return nOnes;
00293 }

Fraig_NodeVec_t* Fraig_CollectSupergate ( Fraig_Node_t *  pNode,
int  fStopAtMux 
)

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 957 of file fraigUtil.c.

00958 {
00959     Fraig_NodeVec_t * vSuper;
00960     vSuper = Fraig_NodeVecAlloc( 8 );
00961     Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
00962     return vSuper;
00963 }

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_CountPis ( Fraig_Man_t *  p,
Msat_IntVec_t *  vVarNums 
)

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

Synopsis [Count the number of PI variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 814 of file fraigUtil.c.

00815 {
00816     int * pVars, nVars, i, Counter;
00817 
00818     nVars = Msat_IntVecReadSize(vVarNums);
00819     pVars = Msat_IntVecReadArray(vVarNums);
00820     Counter = 0;
00821     for ( i = 0; i < nVars; i++ )
00822         Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] );
00823     return Counter;
00824 }

void Fraig_FeedBack ( Fraig_Man_t *  p,
int *  pModel,
Msat_IntVec_t *  vVars,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)

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 []

Definition at line 77 of file fraigFeed.c.

00078 {
00079     int nVarsPi, nWords;
00080     int i, clk = clock();
00081 
00082     // get the number of PI vars in the feedback (also sets the PI values)
00083     nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars );
00084 
00085     // set the PI values
00086     nWords = Fraig_FeedBackInsert( p, nVarsPi );
00087     assert( p->iWordStart + nWords <= p->nWordsDyna );
00088 
00089     // resimulates the words from p->iWordStart to iWordStop
00090     for ( i = 1; i < p->vNodes->nSize; i++ )
00091         if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) )
00092             Fraig_NodeSimulate( p->vNodes->pArray[i], p->iWordStart, p->iWordStart + nWords, 0 );
00093 
00094     if ( p->fDoSparse )
00095         Fraig_TableRehashF0( p, 0 );
00096 
00097     if ( !p->fChoicing )
00098     Fraig_FeedBackVerify( p, pOld, pNew );
00099 
00100     // if there is no room left, compress the patterns
00101     if ( p->iWordStart + nWords == p->nWordsDyna )
00102         p->iWordStart = Fraig_FeedBackCompress( p );
00103     else  // otherwise, update the starting word
00104         p->iWordStart += nWords;
00105 
00106 p->timeFeed += clock() - clk;
00107 }

int Fraig_FeedBackCompress ( Fraig_Man_t *  p  ) 

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

Synopsis [Compress the simulation patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file fraigFeed.c.

00275 {
00276     unsigned * pSims;
00277     unsigned uHash;
00278     int i, w, t, nPats, * pPats;
00279     int fPerformChecks = (p->nBTLimit == -1);
00280 
00281     // solve the covering problem
00282     if ( fPerformChecks )
00283     {
00284         Fraig_FeedBackCheckTable( p );
00285         if ( p->fDoSparse ) 
00286             Fraig_FeedBackCheckTableF0( p );
00287     }
00288 
00289     // solve the covering problem
00290     Fraig_FeedBackCovering( p, p->vPatsReal );
00291 
00292 
00293     // get the number of additional patterns
00294     nPats = Msat_IntVecReadSize( p->vPatsReal );
00295     pPats = Msat_IntVecReadArray( p->vPatsReal );
00296     // get the new starting word
00297     p->iWordStart = FRAIG_NUM_WORDS( p->iPatsPerm + nPats );
00298 
00299     // set the simulation info for the PIs
00300     for ( i = 0; i < p->vInputs->nSize; i++ )
00301     {
00302         // get hold of the simulation info for this PI
00303         pSims = p->vInputs->pArray[i]->puSimD;
00304         // clean the storage for the new patterns
00305         for ( w = p->iWordPerm; w < p->iWordStart; w++ )
00306             p->pSimsTemp[w] = 0;
00307         // set the patterns
00308         for ( t = 0; t < nPats; t++ )
00309             if ( Fraig_BitStringHasBit( pSims, pPats[t] ) )
00310             {
00311                 // check if this pattern falls into temporary storage
00312                 if ( p->iPatsPerm + t < p->iWordPerm * 32 )
00313                     Fraig_BitStringSetBit( pSims, p->iPatsPerm + t );
00314                 else
00315                     Fraig_BitStringSetBit( p->pSimsTemp, p->iPatsPerm + t );
00316             }
00317         // copy the pattern 
00318         for ( w = p->iWordPerm; w < p->iWordStart; w++ )
00319             pSims[w] = p->pSimsTemp[w];
00320         // recompute the hashing info
00321         uHash = 0;
00322         for ( w = 0; w < p->iWordStart; w++ )
00323             uHash ^= pSims[w] * s_FraigPrimes[w];
00324         p->vInputs->pArray[i]->uHashD = uHash;
00325     }
00326 
00327     // update info about the permanently stored patterns
00328     p->iWordPerm = p->iWordStart;
00329     p->iPatsPerm += nPats;
00330     assert( p->iWordPerm == FRAIG_NUM_WORDS( p->iPatsPerm ) );
00331 
00332     // resimulate and recompute the hash values
00333     for ( i = 1; i < p->vNodes->nSize; i++ )
00334         if ( Fraig_NodeIsAnd(p->vNodes->pArray[i]) )
00335         {
00336             p->vNodes->pArray[i]->uHashD = 0;
00337             Fraig_NodeSimulate( p->vNodes->pArray[i], 0, p->iWordPerm, 0 );
00338         }
00339 
00340     // double-check that the nodes are still distinguished
00341     if ( fPerformChecks )
00342         Fraig_FeedBackCheckTable( p );
00343 
00344     // rehash the values in the F0 table
00345     if ( p->fDoSparse ) 
00346     {
00347         Fraig_TableRehashF0( p, 0 );
00348         if ( fPerformChecks )
00349             Fraig_FeedBackCheckTableF0( p );
00350     }
00351 
00352     // check if we need to resize the simulation info
00353     // if less than FRAIG_WORDS_STORE words are left, reallocate simulation info
00354     if ( p->iWordPerm + FRAIG_WORDS_STORE > p->nWordsDyna )
00355         Fraig_ReallocateSimulationInfo( p );
00356 
00357     // set the real patterns
00358     Msat_IntVecClear( p->vPatsReal );
00359     memset( p->pSimsReal, 0, sizeof(unsigned)*p->nWordsDyna );
00360     for ( w = 0; w < p->iWordPerm; w++ )
00361         p->pSimsReal[w] = FRAIG_FULL;
00362     if ( p->iPatsPerm % 32 > 0 )
00363         p->pSimsReal[p->iWordPerm-1] = FRAIG_MASK( p->iPatsPerm % 32 );
00364 //    printf( "The number of permanent words = %d.\n", p->iWordPerm );
00365     return p->iWordStart;
00366 }

void Fraig_FeedBackInit ( Fraig_Man_t *  p  ) 

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

Synopsis [Initializes the feedback information.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file fraigFeed.c.

00055 {
00056     p->vCones    = Fraig_NodeVecAlloc( 500 );
00057     p->vPatsReal = Msat_IntVecAlloc( 1000 ); 
00058     p->pSimsReal = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00059     memset( p->pSimsReal, 0, sizeof(unsigned) * p->nWordsDyna );
00060     p->pSimsTemp = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00061     p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00062 }

void Fraig_FeedBackTest ( Fraig_Man_t *  p  ) 
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 }

int* Fraig_ManAllocCounterExample ( Fraig_Man_t *  p  ) 

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

Synopsis [Generated trivial counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 784 of file fraigFeed.c.

00785 {
00786     int * pModel;
00787     pModel = ALLOC( int, p->vInputs->nSize );
00788     memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
00789     return pModel;
00790 }

int Fraig_ManCountExors ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Counts the number of EXOR type nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 739 of file fraigUtil.c.

00740 {
00741     int i, nExors;
00742     nExors = 0;
00743     for ( i = 0; i < pMan->vNodes->nSize; i++ )
00744         nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] );
00745     return nExors;
00746 
00747 }

int Fraig_ManCountMuxes ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Counts the number of EXOR type nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 760 of file fraigUtil.c.

00761 {
00762     int i, nMuxes;
00763     nMuxes = 0;
00764     for ( i = 0; i < pMan->vNodes->nSize; i++ )
00765         nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] );
00766     return nMuxes;
00767 
00768 }

void Fraig_ManCreateSolver ( Fraig_Man_t *  p  ) 

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

Synopsis [Prepares the SAT solver to run on the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file fraigMan.c.

00322 {
00323     extern int timeSelect;
00324     extern int timeAssign;
00325     assert( p->pSat == NULL );
00326     // allocate data for SAT solving
00327     p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
00328     p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
00329     p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
00330     p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
00331     timeSelect = 0;
00332     timeAssign = 0;
00333 }

void Fraig_ManIncrementTravId ( Fraig_Man_t *  pMan  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 977 of file fraigUtil.c.

00978 {
00979     pMan->nTravIds2++;
00980 }

int* Fraig_ManSaveCounterExample ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 857 of file fraigFeed.c.

00858 {
00859     int * pModel;
00860     int iPattern;
00861     int i, fCompl;
00862 
00863     // the node can be complemented
00864     fCompl = Fraig_IsComplement(pNode);
00865     // because we compare with constant 0, p->pConst1 should also be complemented
00866     fCompl = !fCompl;
00867 
00868     // derive the model
00869     pModel = Fraig_ManAllocCounterExample( p );
00870     iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 );
00871     if ( iPattern >= 0 )
00872     {
00873         for ( i = 0; i < p->vInputs->nSize; i++ )
00874             if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
00875                 pModel[i] = 1;
00876 /*
00877 printf( "SAT solver's pattern:\n" );
00878 for ( i = 0; i < p->vInputs->nSize; i++ )
00879     printf( "%d", pModel[i] );
00880 printf( "\n" );
00881 */
00882         assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
00883         return pModel;
00884     }
00885     iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 );
00886     if ( iPattern >= 0 )
00887     {
00888         for ( i = 0; i < p->vInputs->nSize; i++ )
00889             if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
00890                 pModel[i] = 1;
00891 /*
00892 printf( "SAT solver's pattern:\n" );
00893 for ( i = 0; i < p->vInputs->nSize; i++ )
00894     printf( "%d", pModel[i] );
00895 printf( "\n" );
00896 */
00897         assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
00898         return pModel;
00899     }
00900     FREE( pModel );
00901     return NULL;
00902 }

void Fraig_ManSelectBestChoice ( Fraig_Man_t *  p  ) 
char* Fraig_MemFixedEntryFetch ( Fraig_MemFixed_t *  p  ) 

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

Synopsis [Extracts one entry from the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file fraigMem.c.

00129 {
00130     char * pTemp;
00131     int i;
00132 
00133     // check if there are still free entries
00134     if ( p->nEntriesUsed == p->nEntriesAlloc )
00135     { // need to allocate more entries
00136         assert( p->pEntriesFree == NULL );
00137         if ( p->nChunks == p->nChunksAlloc )
00138         {
00139             p->nChunksAlloc *= 2;
00140             p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
00141         }
00142         p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
00143         p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
00144         // transform these entries into a linked list
00145         pTemp = p->pEntriesFree;
00146         for ( i = 1; i < p->nChunkSize; i++ )
00147         {
00148             *((char **)pTemp) = pTemp + p->nEntrySize;
00149             pTemp += p->nEntrySize;
00150         }
00151         // set the last link
00152         *((char **)pTemp) = NULL;
00153         // add the chunk to the chunk storage
00154         p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
00155         // add to the number of entries allocated
00156         p->nEntriesAlloc += p->nChunkSize;
00157     }
00158     // incrememt the counter of used entries
00159     p->nEntriesUsed++;
00160     if ( p->nEntriesMax < p->nEntriesUsed )
00161         p->nEntriesMax = p->nEntriesUsed;
00162     // return the first entry in the free entry list
00163     pTemp = p->pEntriesFree;
00164     p->pEntriesFree = *((char **)pTemp);
00165     return pTemp;
00166 }

void Fraig_MemFixedEntryRecycle ( Fraig_MemFixed_t *  p,
char *  pEntry 
)

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

Synopsis [Returns one entry into the memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 179 of file fraigMem.c.

00180 {
00181     // decrement the counter of used entries
00182     p->nEntriesUsed--;
00183     // add the entry to the linked list of free entries
00184     *((char **)pEntry) = p->pEntriesFree;
00185     p->pEntriesFree = pEntry;
00186 }

int Fraig_MemFixedReadMemUsage ( Fraig_MemFixed_t *  p  ) 

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

Synopsis [Reports the memory usage.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file fraigMem.c.

00238 {
00239     return p->nMemoryAlloc;
00240 }

void Fraig_MemFixedRestart ( Fraig_MemFixed_t *  p  ) 

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

Synopsis [Frees all associated memory and resets the manager.]

Description [Relocates all the memory except the first chunk.]

SideEffects []

SeeAlso []

Definition at line 199 of file fraigMem.c.

00200 {
00201     int i;
00202     char * pTemp;
00203 
00204     // deallocate all chunks except the first one
00205     for ( i = 1; i < p->nChunks; i++ )
00206         free( p->pChunks[i] );
00207     p->nChunks = 1;
00208     // transform these entries into a linked list
00209     pTemp = p->pChunks[0];
00210     for ( i = 1; i < p->nChunkSize; i++ )
00211     {
00212         *((char **)pTemp) = pTemp + p->nEntrySize;
00213         pTemp += p->nEntrySize;
00214     }
00215     // set the last link
00216     *((char **)pTemp) = NULL;
00217     // set the free entry list
00218     p->pEntriesFree  = p->pChunks[0];
00219     // set the correct statistics
00220     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
00221     p->nMemoryUsed   = 0;
00222     p->nEntriesAlloc = p->nChunkSize;
00223     p->nEntriesUsed  = 0;
00224 }

Fraig_MemFixed_t* Fraig_MemFixedStart ( int  nEntrySize  ) 

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

Synopsis [Starts the internal memory manager.]

Description [Can only work with entry size at least 4 byte long.]

SideEffects []

SeeAlso []

Definition at line 60 of file fraigMem.c.

00061 {
00062     Fraig_MemFixed_t * p;
00063 
00064     p = ALLOC( Fraig_MemFixed_t, 1 );
00065     memset( p, 0, sizeof(Fraig_MemFixed_t) );
00066 
00067     p->nEntrySize    = nEntrySize;
00068     p->nEntriesAlloc = 0;
00069     p->nEntriesUsed  = 0;
00070     p->pEntriesFree  = NULL;
00071 
00072     if ( nEntrySize * (1 << 10) < (1<<16) )
00073         p->nChunkSize = (1 << 10);
00074     else
00075         p->nChunkSize = (1<<16) / nEntrySize;
00076     if ( p->nChunkSize < 8 )
00077         p->nChunkSize = 8;
00078 
00079     p->nChunksAlloc  = 64;
00080     p->nChunks       = 0;
00081     p->pChunks       = ALLOC( char *, p->nChunksAlloc );
00082 
00083     p->nMemoryUsed   = 0;
00084     p->nMemoryAlloc  = 0;
00085     return p;
00086 }

void Fraig_MemFixedStop ( Fraig_MemFixed_t *  p,
int  fVerbose 
)

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

Synopsis [Stops the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file fraigMem.c.

00100 {
00101     int i;
00102     if ( p == NULL )
00103         return;
00104     if ( fVerbose )
00105     {
00106         printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
00107             p->nEntrySize, p->nChunkSize, p->nChunks );
00108         printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
00109             p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
00110     }
00111     for ( i = 0; i < p->nChunks; i++ )
00112         free( p->pChunks[i] );
00113     free( p->pChunks );
00114     free( p );
00115 }

void Fraig_NodeAddFaninFanout ( Fraig_Node_t *  pFanin,
Fraig_Node_t *  pFanout 
)
Fraig_Node_t* Fraig_NodeAndCanon ( Fraig_Man_t *  pMan,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

GLOBAL VARIABLES /// FUNCTION DEFINITIONS ///

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

FileName [fraigCanon.c]

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

Synopsis [AND-node creation and elementary AND-operation.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigCanon.c,v 1.4 2005/07/08 01:01:31 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [The internal AND operation for the two FRAIG nodes.]

Description [This procedure is the core of the FRAIG package, because it performs the two-step canonicization of FRAIG nodes. The first step involves the lookup in the structural hash table (which hashes two ANDs into a node that has them as fanins, if such a node exists). If the node is not found in the structural hash table, an attempt is made to find a functionally equivalent node in another hash table (which hashes the simulation info into the nodes, which has this simulation info). Some tricks used on the way are described in the comments to the code and in the paper "FRAIGs: Functionally reduced AND-INV graphs".]

SideEffects []

SeeAlso []

Definition at line 49 of file fraigCanon.c.

00050 {
00051     Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
00052     int fUseSatCheck;
00053 //    int RetValue;
00054 
00055     // check for trivial cases
00056     if ( p1 == p2 )
00057         return p1;
00058     if ( p1 == Fraig_Not(p2) )
00059         return Fraig_Not(pMan->pConst1);
00060     if ( Fraig_NodeIsConst(p1) )
00061     {
00062         if ( p1 == pMan->pConst1 )
00063             return p2;
00064         return Fraig_Not(pMan->pConst1);
00065     }
00066     if ( Fraig_NodeIsConst(p2) )
00067     {
00068         if ( p2 == pMan->pConst1 )
00069             return p1;
00070         return Fraig_Not(pMan->pConst1);
00071     }
00072 /*
00073     // check for less trivial cases
00074     if ( Fraig_IsComplement(p1) )
00075     {
00076         if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p1), p2 ) )
00077         {
00078             if ( RetValue == -1 )
00079                 pMan->nImplies0++;
00080             else
00081                 pMan->nImplies1++;
00082 
00083             if ( RetValue == -1 )
00084                 return p2;
00085         }
00086     }
00087     else
00088     {
00089         if ( RetValue = Fraig_NodeIsInSupergate( p1, p2 ) )
00090         {
00091             if ( RetValue == 1 )
00092                 pMan->nSimplifies1++;
00093             else
00094                 pMan->nSimplifies0++;
00095 
00096             if ( RetValue == 1 )
00097                 return p1;
00098             return Fraig_Not(pMan->pConst1);
00099         }
00100     }
00101  
00102     if ( Fraig_IsComplement(p2) )
00103     {
00104         if ( RetValue = Fraig_NodeIsInSupergate( Fraig_Regular(p2), p1 ) )
00105         {
00106             if ( RetValue == -1 )
00107                 pMan->nImplies0++;
00108             else
00109                 pMan->nImplies1++;
00110 
00111             if ( RetValue == -1 )
00112                 return p1;
00113         }
00114     }
00115     else
00116     {
00117         if ( RetValue = Fraig_NodeIsInSupergate( p2, p1 ) )
00118         {
00119             if ( RetValue == 1 )
00120                 pMan->nSimplifies1++;
00121             else
00122                 pMan->nSimplifies0++;
00123 
00124             if ( RetValue == 1 )
00125                 return p2;
00126             return Fraig_Not(pMan->pConst1);
00127         }
00128     }
00129 */
00130     // perform level-one structural hashing
00131     if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
00132     {
00133         // if the existent node is part of the cone of unused logic
00134         // (that is logic feeding the node which is equivalent to the given node)
00135         // return the canonical representative of this node
00136         // determine the phase of the given node, with respect to its canonical form
00137         pNodeRepr = Fraig_Regular(pNodeNew)->pRepr;
00138         if ( pMan->fFuncRed && pNodeRepr )
00139             return Fraig_NotCond( pNodeRepr, Fraig_IsComplement(pNodeNew) ^ Fraig_NodeComparePhase(Fraig_Regular(pNodeNew), pNodeRepr) );
00140         // otherwise, the node is itself a canonical representative, return it
00141         return pNodeNew;
00142     }
00143     // the same node is not found, but the new one is created
00144 
00145     // if one level hashing is requested (without functionality hashing), return
00146     if ( !pMan->fFuncRed )
00147         return pNodeNew;
00148 
00149     // check if the new node is unique using the simulation info
00150     if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 )
00151     {
00152         pMan->nSatZeros++;
00153         if ( !pMan->fDoSparse ) // if we do not do sparse functions, skip
00154             return pNodeNew;
00155         // check the sparse function simulation hash table
00156         pNodeOld = Fraig_HashTableLookupF0( pMan, pNodeNew );
00157         if ( pNodeOld == NULL ) // the node is unique (it is added to the table)
00158             return pNodeNew;
00159     }
00160     else
00161     {
00162         // check the simulation hash table
00163         pNodeOld = Fraig_HashTableLookupF( pMan, pNodeNew );
00164         if ( pNodeOld == NULL ) // the node is unique
00165             return pNodeNew;
00166     }
00167     assert( pNodeOld->pRepr == 0 );
00168     // there is another node which looks the same according to simulation
00169 
00170     // use SAT to resolve the ambiguity
00171     fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); 
00172     if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
00173     {
00174         // set the node to be equivalent with this node
00175         // to prevent loops, only set if the old node is not in the TFI of the new node
00176         // the loop may happen in the following case: suppose 
00177         // NodeC = AND(NodeA, NodeB) and at the same time NodeA => NodeB
00178         // in this case, NodeA and NodeC are functionally equivalent
00179         // however, NodeA is a fanin of node NodeC (this leads to the loop)
00180         // add the node to the list of equivalent nodes or dereference it
00181         if ( pMan->fChoicing && !Fraig_CheckTfi( pMan, pNodeOld, pNodeNew ) )
00182         { 
00183             // if the old node is not in the TFI of the new node and choicing 
00184             // is enabled, add the new node to the list of equivalent ones
00185             pNodeNew->pNextE = pNodeOld->pNextE;
00186             pNodeOld->pNextE = pNodeNew;
00187         }
00188         // set the canonical representative of this node
00189         pNodeNew->pRepr = pNodeOld;
00190         // return the equivalent node
00191         return Fraig_NotCond( pNodeOld, Fraig_NodeComparePhase(pNodeOld, pNodeNew) );
00192     }
00193 
00194     // now we add another member to this simulation class
00195     if ( pNodeNew->nOnes == 0 || pNodeNew->nOnes == (unsigned)pMan->nWordsRand * 32 )
00196     {
00197         Fraig_Node_t * pNodeTemp;
00198         assert( pMan->fDoSparse );
00199         pNodeTemp = Fraig_HashTableLookupF0( pMan, pNodeNew );
00200 //        assert( pNodeTemp == NULL );
00201 //        Fraig_HashTableInsertF0( pMan, pNodeNew );
00202     }
00203     else
00204     {
00205         pNodeNew->pNextD = pNodeOld->pNextD;
00206         pNodeOld->pNextD = pNodeNew;
00207     }
00208     // return the new node
00209     assert( pNodeNew->pRepr == 0 );
00210     return pNodeNew;
00211 }

int Fraig_NodeAndSimpleCase_rec ( Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)
int Fraig_NodeCountPis ( Msat_IntVec_t *  vVars,
int  nVarsPi 
)
int Fraig_NodeCountSuppVars ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode,
int  fSuppStr 
)
Fraig_Node_t* Fraig_NodeCreate ( Fraig_Man_t *  p,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

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

Synopsis [Creates a new node.]

Description [This procedure should be called to create the constant node and the PI nodes first.]

SideEffects []

SeeAlso []

Definition at line 156 of file fraigNode.c.

00157 {
00158     Fraig_Node_t * pNode;
00159     int clk;
00160 
00161     // create the node
00162     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00163     memset( pNode, 0, sizeof(Fraig_Node_t) );
00164 
00165     // assign the children
00166     pNode->p1  = p1;  Fraig_Ref(p1);  Fraig_Regular(p1)->nRefs++;
00167     pNode->p2  = p2;  Fraig_Ref(p2);  Fraig_Regular(p2)->nRefs++;
00168 
00169     // assign the number and add to the array of nodes
00170     pNode->Num = p->vNodes->nSize;
00171     Fraig_NodeVecPush( p->vNodes,  pNode );
00172 
00173     // assign the PI number
00174     pNode->NumPi = -1;
00175 
00176     // compute the level of this node
00177     pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
00178     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
00179     pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
00180 
00181     // derive the simulation info 
00182 clk = clock();
00183     // allocate memory for the simulation info
00184     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00185     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00186     // derive random simulation info
00187     pNode->uHashR = 0;
00188     Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 );
00189     // derive dynamic simulation info
00190     pNode->uHashD = 0;
00191     Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 );
00192     // count the number of ones in the random simulation info
00193     pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
00194     if ( pNode->fInv )
00195         pNode->nOnes = p->nWordsRand * 32 - pNode->nOnes;
00196     // add to the runtime of simulation
00197 p->timeSims += clock() - clk;
00198 
00199 #ifdef FRAIG_ENABLE_FANOUTS
00200     // create the fanout info
00201     Fraig_NodeAddFaninFanout( Fraig_Regular(p1), pNode );
00202     Fraig_NodeAddFaninFanout( Fraig_Regular(p2), pNode );
00203 #endif
00204     return pNode;
00205 }

Fraig_Node_t* Fraig_NodeCreateConst ( Fraig_Man_t *  p  ) 

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

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigNode.c.

00044 {
00045     Fraig_Node_t * pNode;
00046 
00047     // create the node
00048     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00049     memset( pNode, 0, sizeof(Fraig_Node_t) );
00050 
00051     // assign the number and add to the array of nodes
00052     pNode->Num   = p->vNodes->nSize;
00053     Fraig_NodeVecPush( p->vNodes,  pNode );
00054     pNode->NumPi = -1;  // this is not a PI, so its number is -1
00055     pNode->Level =  0;  // just like a PI, it has 0 level
00056     pNode->nRefs =  1;  // it is a persistent node, which comes referenced
00057     pNode->fInv  =  1;  // the simulation info is complemented
00058 
00059     // create the simulation info
00060     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00061     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00062     memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand );
00063     memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
00064 
00065     // count the number of ones in the simulation vector
00066     pNode->nOnes = p->nWordsRand * sizeof(unsigned) * 8;
00067 
00068     // insert it into the hash table
00069     Fraig_HashTableLookupF0( p, pNode );
00070     return pNode;
00071 }

Fraig_Node_t* Fraig_NodeCreatePi ( Fraig_Man_t *  p  ) 

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

Synopsis [Creates a primary input node.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file fraigNode.c.

00085 {
00086     Fraig_Node_t * pNode, * pNodeRes;
00087     int i, clk;
00088 
00089     // create the node
00090     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00091     memset( pNode, 0, sizeof(Fraig_Node_t) );
00092     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00093     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00094     memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
00095 
00096     // assign the number and add to the array of nodes
00097     pNode->Num   = p->vNodes->nSize;
00098     Fraig_NodeVecPush( p->vNodes,  pNode );
00099 
00100     // assign the PI number and add to the array of primary inputs
00101     pNode->NumPi = p->vInputs->nSize;   
00102     Fraig_NodeVecPush( p->vInputs, pNode );
00103 
00104     pNode->Level =  0;  // PI has 0 level
00105     pNode->nRefs =  1;  // it is a persistent node, which comes referenced
00106     pNode->fInv  =  0;  // the simulation info of the PI is not complemented
00107 
00108     // derive the simulation info for the new node
00109 clk = clock();
00110     // set the random simulation info for the primary input
00111     pNode->uHashR = 0;
00112     for ( i = 0; i < p->nWordsRand; i++ )
00113     {
00114         // generate the simulation info
00115         pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
00116         // for reasons that take very long to explain, it makes sense to have (0000000...) 
00117         // pattern in the set (this helps if we need to return the counter-examples)
00118         if ( i == 0 )
00119             pNode->puSimR[i] <<= 1;
00120         // compute the hash key
00121         pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
00122     }
00123     // count the number of ones in the simulation vector
00124     pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
00125 
00126     // set the systematic simulation info for the primary input
00127     pNode->uHashD = 0;
00128     for ( i = 0; i < p->iWordStart; i++ )
00129     {
00130         // generate the simulation info
00131         pNode->puSimD[i] = FRAIG_RANDOM_UNSIGNED;
00132         // compute the hash key
00133         pNode->uHashD ^= pNode->puSimD[i] * s_FraigPrimes[i];
00134     }
00135 p->timeSims += clock() - clk;
00136 
00137     // insert it into the hash table
00138     pNodeRes = Fraig_HashTableLookupF( p, pNode );
00139     assert( pNodeRes == NULL );
00140     // add to the runtime of simulation
00141     return pNode;
00142 }

int Fraig_NodeGetFanoutNum ( Fraig_Node_t *  pNode  ) 
int Fraig_NodeIsExor ( Fraig_Node_t *  pNode  ) 

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

Synopsis [Returns 1 if the node is EXOR, 0 if it is NEXOR.]

Description [The node should be EXOR type and not complemented.]

SideEffects []

SeeAlso []

Definition at line 630 of file fraigUtil.c.

00631 {
00632     Fraig_Node_t * pNode1;
00633     assert( !Fraig_IsComplement(pNode) );
00634     assert( Fraig_NodeIsExorType(pNode) );
00635     assert( Fraig_IsComplement(pNode->p1) );
00636     // get children
00637     pNode1 = Fraig_Regular(pNode->p1);
00638     return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2);
00639 }

int Fraig_NodeIsExorType ( Fraig_Node_t *  pNode  ) 

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

Synopsis [Returns 1 if the node is the root of EXOR/NEXOR gate.]

Description [The node can be complemented.]

SideEffects []

SeeAlso []

Definition at line 555 of file fraigUtil.c.

00556 {
00557     Fraig_Node_t * pNode1, * pNode2;
00558     // make the node regular (it does not matter for EXOR/NEXOR)
00559     pNode = Fraig_Regular(pNode);
00560     // if the node or its children are not ANDs or not compl, this cannot be EXOR type
00561     if ( !Fraig_NodeIsAnd(pNode) )
00562         return 0;
00563     if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
00564         return 0;
00565     if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
00566         return 0;
00567 
00568     // get children
00569     pNode1 = Fraig_Regular(pNode->p1);
00570     pNode2 = Fraig_Regular(pNode->p2);
00571     assert( pNode1->Num < pNode2->Num );
00572 
00573     // compare grandchildren
00574     return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2);
00575 }

int Fraig_NodeIsImplication ( Fraig_Man_t *  p,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew,
int  nBTLimit 
)

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

Synopsis [Checks whether pOld => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 547 of file fraigSat.c.

00548 {
00549     int RetValue, RetValue1, i, fComp, clk;
00550     int fVerbose = 0;
00551 
00552     // make sure the nodes are not complemented
00553     assert( !Fraig_IsComplement(pNew) );
00554     assert( !Fraig_IsComplement(pOld) );
00555     assert( pNew != pOld );
00556 
00557     p->nSatCallsImp++;
00558 
00559     // make sure the solver is allocated and has enough variables
00560     if ( p->pSat == NULL )
00561         Fraig_ManCreateSolver( p );
00562     // make sure the SAT solver has enough variables
00563     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00564         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00565 
00566    // get the logic cone
00567 clk = clock();
00568     Fraig_OrderVariables( p, pOld, pNew );
00569 //    Fraig_PrepareCones( p, pOld, pNew );
00570 p->timeTrav += clock() - clk;
00571 
00572 if ( fVerbose )
00573     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
00574 
00575 
00576     // get the complemented attribute
00577     fComp = Fraig_NodeComparePhase( pOld, pNew );
00578 //Msat_SolverPrintClauses( p->pSat );
00579 
00581     // prepare the solver to run incrementally on these variables
00582 //clk = clock();
00583     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00584 //p->time3 += clock() - clk;
00585 
00586     // solve under assumptions
00587     // A = 1; B = 0     OR     A = 1; B = 1 
00588     Msat_IntVecClear( p->vProj );
00589     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00590     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00591     // run the solver
00592 clk = clock();
00593     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
00594 p->timeSat += clock() - clk;
00595 
00596     if ( RetValue1 == MSAT_FALSE )
00597     {
00598 //p->time1 += clock() - clk;
00599 
00600 if ( fVerbose )
00601 {
00602     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00603 PRT( "time", clock() - clk );
00604 }
00605 
00606         // add the clause
00607         Msat_IntVecClear( p->vProj );
00608         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00609         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00610         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00611         assert( RetValue );
00612 //        p->nSatProofImp++;
00613         return 1;
00614     }
00615     else if ( RetValue1 == MSAT_TRUE )
00616     {
00617 //p->time2 += clock() - clk;
00618 
00619 if ( fVerbose )
00620 {
00621     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00622 PRT( "time", clock() - clk );
00623 }
00624         // record the counter example
00625         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00626         p->nSatCounterImp++;
00627         return 0;
00628     }
00629     else // if ( RetValue1 == MSAT_UNKNOWN )
00630     {
00631 p->time3 += clock() - clk;
00632         p->nSatFailsImp++;
00633         return 0;
00634     }
00635 }

int Fraig_NodeIsInSupergate ( Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)

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

Synopsis [Checks if pNew exists among the implication fanins of pOld.]

Description [If pNew is an implication fanin of pOld, returns 1. If Fraig_Not(pNew) is an implication fanin of pOld, return -1. Otherwise returns 0.]

SideEffects []

SeeAlso []

Definition at line 902 of file fraigUtil.c.

00903 {
00904     int RetValue1, RetValue2;
00905     if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) )
00906         return (pOld == pNew)? 1 : -1;
00907     if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) )
00908         return 0;
00909     RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew );
00910     RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew );
00911     if ( RetValue1 == -1 || RetValue2 == -1 )
00912         return -1;
00913     if ( RetValue1 ==  1 || RetValue2 ==  1 )
00914         return 1;
00915     return 0;
00916 }

int Fraig_NodeIsMuxType ( Fraig_Node_t *  pNode  ) 

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

Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

Description [The node can be complemented.]

SideEffects []

SeeAlso []

Definition at line 588 of file fraigUtil.c.

00589 {
00590     Fraig_Node_t * pNode1, * pNode2;
00591 
00592     // make the node regular (it does not matter for EXOR/NEXOR)
00593     pNode = Fraig_Regular(pNode);
00594     // if the node or its children are not ANDs or not compl, this cannot be EXOR type
00595     if ( !Fraig_NodeIsAnd(pNode) )
00596         return 0;
00597     if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
00598         return 0;
00599     if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
00600         return 0;
00601 
00602     // get children
00603     pNode1 = Fraig_Regular(pNode->p1);
00604     pNode2 = Fraig_Regular(pNode->p2);
00605     assert( pNode1->Num < pNode2->Num );
00606 
00607     // compare grandchildren
00608     // node is an EXOR/NEXOR
00609     if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) )
00610         return 1; 
00611 
00612     // otherwise the node is MUX iff it has a pair of equal grandchildren
00613     return pNode1->p1 == Fraig_Not(pNode2->p1) || 
00614            pNode1->p1 == Fraig_Not(pNode2->p2) ||
00615            pNode1->p2 == Fraig_Not(pNode2->p1) ||
00616            pNode1->p2 == Fraig_Not(pNode2->p2);
00617 }

int Fraig_NodeIsTravIdCurrent ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1009 of file fraigUtil.c.

01010 {
01011     return pNode->TravId2 == pMan->nTravIds2;
01012 }

int Fraig_NodeIsTravIdPrevious ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1025 of file fraigUtil.c.

01026 {
01027     return pNode->TravId2 == pMan->nTravIds2 - 1;
01028 }

Fraig_Node_t* Fraig_NodeRecognizeMux ( Fraig_Node_t *  pNode,
Fraig_Node_t **  ppNodeT,
Fraig_Node_t **  ppNodeE 
)

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

Synopsis [Recognizes what nodes are control and data inputs of a MUX.]

Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]

SideEffects []

SeeAlso []

Definition at line 655 of file fraigUtil.c.

00656 {
00657     Fraig_Node_t * pNode1, * pNode2;
00658     assert( !Fraig_IsComplement(pNode) );
00659     assert( Fraig_NodeIsMuxType(pNode) );
00660     // get children
00661     pNode1 = Fraig_Regular(pNode->p1);
00662     pNode2 = Fraig_Regular(pNode->p2);
00663     // find the control variable
00664     if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
00665     {
00666         if ( Fraig_IsComplement(pNode1->p1) )
00667         { // pNode2->p1 is positive phase of C
00668             *ppNodeT = Fraig_Not(pNode2->p2);
00669             *ppNodeE = Fraig_Not(pNode1->p2);
00670             return pNode2->p1;
00671         }
00672         else
00673         { // pNode1->p1 is positive phase of C
00674             *ppNodeT = Fraig_Not(pNode1->p2);
00675             *ppNodeE = Fraig_Not(pNode2->p2);
00676             return pNode1->p1;
00677         }
00678     }
00679     else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
00680     {
00681         if ( Fraig_IsComplement(pNode1->p1) )
00682         { // pNode2->p2 is positive phase of C
00683             *ppNodeT = Fraig_Not(pNode2->p1);
00684             *ppNodeE = Fraig_Not(pNode1->p2);
00685             return pNode2->p2;
00686         }
00687         else
00688         { // pNode1->p1 is positive phase of C
00689             *ppNodeT = Fraig_Not(pNode1->p2);
00690             *ppNodeE = Fraig_Not(pNode2->p1);
00691             return pNode1->p1;
00692         }
00693     }
00694     else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
00695     {
00696         if ( Fraig_IsComplement(pNode1->p2) )
00697         { // pNode2->p1 is positive phase of C
00698             *ppNodeT = Fraig_Not(pNode2->p2);
00699             *ppNodeE = Fraig_Not(pNode1->p1);
00700             return pNode2->p1;
00701         }
00702         else
00703         { // pNode1->p2 is positive phase of C
00704             *ppNodeT = Fraig_Not(pNode1->p1);
00705             *ppNodeE = Fraig_Not(pNode2->p2);
00706             return pNode1->p2;
00707         }
00708     }
00709     else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
00710     {
00711         if ( Fraig_IsComplement(pNode1->p2) )
00712         { // pNode2->p2 is positive phase of C
00713             *ppNodeT = Fraig_Not(pNode2->p1);
00714             *ppNodeE = Fraig_Not(pNode1->p1);
00715             return pNode2->p2;
00716         }
00717         else
00718         { // pNode1->p2 is positive phase of C
00719             *ppNodeT = Fraig_Not(pNode1->p1);
00720             *ppNodeE = Fraig_Not(pNode2->p1);
00721             return pNode1->p2;
00722         }
00723     }
00724     assert( 0 ); // this is not MUX
00725     return NULL;
00726 }

void Fraig_NodeRemoveFaninFanout ( Fraig_Node_t *  pFanin,
Fraig_Node_t *  pFanoutToRemove 
)
int Fraig_NodesCompareSupps ( Fraig_Man_t *  p,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)
void Fraig_NodeSetTravIdCurrent ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 993 of file fraigUtil.c.

00994 {
00995     pNode->TravId2 = pMan->nTravIds2;
00996 }

int Fraig_NodeSimsContained ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2 
)

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

Synopsis [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.]

Description []

SideEffects []

SeeAlso []

Definition at line 781 of file fraigUtil.c.

00782 {
00783     unsigned * pUnsigned1, * pUnsigned2;
00784     int i;
00785 
00786     // compare random siminfo
00787     pUnsigned1 = pNode1->puSimR;
00788     pUnsigned2 = pNode2->puSimR;
00789     for ( i = 0; i < pMan->nWordsRand; i++ )
00790         if ( pUnsigned1[i] & ~pUnsigned2[i] )
00791             return 0;
00792 
00793     // compare systematic siminfo
00794     pUnsigned1 = pNode1->puSimD;
00795     pUnsigned2 = pNode2->puSimD;
00796     for ( i = 0; i < pMan->iWordStart; i++ )
00797         if ( pUnsigned1[i] & ~pUnsigned2[i] )
00798             return 0;
00799 
00800     return 1;
00801 }

void Fraig_NodeSimulate ( Fraig_Node_t *  pNode,
int  iWordStart,
int  iWordStop,
int  fUseRand 
)

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

Synopsis [Simulates the node.]

Description [Simulates the random or dynamic simulation info through the node. Uses phases of the children to determine their real simulation info. Uses phase of the node to determine the way its simulation info is stored. The resulting info is guaranteed to be 0 for the first pattern.]

SideEffects [This procedure modified the hash value of the simulation info.]

SeeAlso []

Definition at line 222 of file fraigNode.c.

00223 {
00224     unsigned * pSims, * pSims1, * pSims2;
00225     unsigned uHash;
00226     int fCompl, fCompl1, fCompl2, i;
00227 
00228     assert( !Fraig_IsComplement(pNode) );
00229 
00230     // get hold of the simulation information
00231     pSims  = fUseRand? pNode->puSimR                    : pNode->puSimD;
00232     pSims1 = fUseRand? Fraig_Regular(pNode->p1)->puSimR : Fraig_Regular(pNode->p1)->puSimD;
00233     pSims2 = fUseRand? Fraig_Regular(pNode->p2)->puSimR : Fraig_Regular(pNode->p2)->puSimD;
00234 
00235     // get complemented attributes of the children using their random info
00236     fCompl  = pNode->fInv;
00237     fCompl1 = Fraig_NodeIsSimComplement(pNode->p1);
00238     fCompl2 = Fraig_NodeIsSimComplement(pNode->p2);
00239 
00240     // simulate
00241     uHash = 0;
00242     if ( fCompl1 && fCompl2 )
00243     {
00244         if ( fCompl )
00245             for ( i = iWordStart; i < iWordStop; i++ )
00246             {
00247                 pSims[i] = (pSims1[i] | pSims2[i]);
00248                 uHash ^= pSims[i] * s_FraigPrimes[i];
00249             }
00250         else
00251             for ( i = iWordStart; i < iWordStop; i++ )
00252             {
00253                 pSims[i] = ~(pSims1[i] | pSims2[i]);
00254                 uHash ^= pSims[i] * s_FraigPrimes[i];
00255             }
00256     }
00257     else if ( fCompl1 && !fCompl2 )
00258     {
00259         if ( fCompl )
00260             for ( i = iWordStart; i < iWordStop; i++ )
00261             {
00262                 pSims[i] = (pSims1[i] | ~pSims2[i]);
00263                 uHash ^= pSims[i] * s_FraigPrimes[i];
00264             }
00265         else
00266             for ( i = iWordStart; i < iWordStop; i++ )
00267             {
00268                 pSims[i] = (~pSims1[i] & pSims2[i]);
00269                 uHash ^= pSims[i] * s_FraigPrimes[i];
00270             }
00271     }
00272     else if ( !fCompl1 && fCompl2 )
00273     {
00274         if ( fCompl )
00275             for ( i = iWordStart; i < iWordStop; i++ )
00276             {
00277                 pSims[i] = (~pSims1[i] | pSims2[i]);
00278                 uHash ^= pSims[i] * s_FraigPrimes[i];
00279             }
00280         else
00281             for ( i = iWordStart; i < iWordStop; i++ )
00282             {
00283                 pSims[i] = (pSims1[i] & ~pSims2[i]);
00284                 uHash ^= pSims[i] * s_FraigPrimes[i];
00285             }
00286     }
00287     else // if ( !fCompl1 && !fCompl2 )
00288     {
00289         if ( fCompl )
00290             for ( i = iWordStart; i < iWordStop; i++ )
00291             {
00292                 pSims[i] = ~(pSims1[i] & pSims2[i]);
00293                 uHash ^= pSims[i] * s_FraigPrimes[i];
00294             }
00295         else
00296             for ( i = iWordStart; i < iWordStop; i++ )
00297             {
00298                 pSims[i] = (pSims1[i] & pSims2[i]);
00299                 uHash ^= pSims[i] * s_FraigPrimes[i];
00300             }
00301     }
00302 
00303     if ( fUseRand )
00304         pNode->uHashR ^= uHash;
00305     else
00306         pNode->uHashD ^= uHash;
00307 }

void Fraig_NodeVecSortByRefCount ( Fraig_NodeVec_t *  p  ) 

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 536 of file fraigVec.c.

00537 {
00538     qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00539             (int (*)(const void *, const void *)) Fraig_NodeVecCompareRefCounts );
00540 }

void Fraig_PrintBinary ( FILE *  pFile,
unsigned *  pSign,
int  nBits 
)

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

Synopsis [Prints the bit string.]

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file fraigUtil.c.

00400 {
00401     int Remainder, nWords;
00402     int w, i;
00403 
00404     Remainder = (nBits%(sizeof(unsigned)*8));
00405     nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
00406 
00407     for ( w = nWords-1; w >= 0; w-- )
00408         for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
00409             fprintf( pFile, "%c", '0' + (int)((pSign[w] & (1<<i)) > 0) );
00410 
00411 //  fprintf( pFile, "\n" );
00412 }

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 }

Variable Documentation

int s_FraigPrimes[FRAIG_MAX_PRIMES]

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

FileName [fraigPrime.c]

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

Synopsis [The table of the first 1000 primes.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigPrime.c,v 1.4 2005/07/08 01:01:32 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file fraigPrime.c.

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