src/sat/fraig/fraigUtil.c File Reference

#include "fraigInt.h"
#include <limits.h>
Include dependency graph for fraigUtil.c:

Go to the source code of this file.

Functions

static void Fraig_Dfs_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_NodeVec_t *vNodes, int fEquiv)
static int Fraig_CheckTfi_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_Node_t *pOld)
Fraig_NodeVec_t * Fraig_Dfs (Fraig_Man_t *pMan, int fEquiv)
Fraig_NodeVec_t * Fraig_DfsOne (Fraig_Man_t *pMan, Fraig_Node_t *pNode, int fEquiv)
Fraig_NodeVec_t * Fraig_DfsNodes (Fraig_Man_t *pMan, Fraig_Node_t **ppNodes, int nNodes, int fEquiv)
int Fraig_CountNodes (Fraig_Man_t *pMan, int fEquiv)
int Fraig_CheckTfi (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int Fraig_CheckTfi2 (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
void Fraig_ManMarkRealFanouts (Fraig_Man_t *p)
int Fraig_BitStringCountOnes (unsigned *pString, int nWords)
int Fraig_ManCheckConsistency (Fraig_Man_t *p)
void Fraig_PrintNode (Fraig_Man_t *p, Fraig_Node_t *pNode)
void Fraig_PrintBinary (FILE *pFile, unsigned *pSign, int nBits)
int Fraig_GetMaxLevel (Fraig_Man_t *pMan)
int Fraig_MappingUpdateLevel_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode, int fMaximum)
void Fraig_MappingSetChoiceLevels (Fraig_Man_t *pMan, int fMaximum)
void Fraig_ManReportChoices (Fraig_Man_t *pMan)
int Fraig_NodeIsExorType (Fraig_Node_t *pNode)
int Fraig_NodeIsMuxType (Fraig_Node_t *pNode)
int Fraig_NodeIsExor (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_CountPis (Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
int Fraig_ManPrintRefs (Fraig_Man_t *pMan)
int Fraig_NodeIsInSupergate (Fraig_Node_t *pOld, Fraig_Node_t *pNew)
void Fraig_CollectSupergate_rec (Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, int fFirst, int fStopAtMux)
Fraig_NodeVec_t * Fraig_CollectSupergate (Fraig_Node_t *pNode, int fStopAtMux)
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)

Variables

static int bit_count [256]

Function Documentation

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 }

int Fraig_CheckTfi ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file fraigUtil.c.

00171 {
00172     assert( !Fraig_IsComplement(pOld) );
00173     assert( !Fraig_IsComplement(pNew) );
00174     pMan->nTravIds++;
00175     return Fraig_CheckTfi_rec( pMan, pNew, pOld );
00176 }

int Fraig_CheckTfi2 ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file fraigUtil.c.

00224 {
00225     Fraig_NodeVec_t * vNodes;
00226     int RetValue;
00227     vNodes = Fraig_DfsOne( pMan, pNew, 1 );
00228     RetValue = (pOld->TravId == pMan->nTravIds);
00229     Fraig_NodeVecFree( vNodes );
00230     return RetValue;
00231 }

int Fraig_CheckTfi_rec ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode,
Fraig_Node_t *  pOld 
) [static]

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file fraigUtil.c.

00190 {
00191     // check the trivial cases
00192     if ( pNode == NULL )
00193         return 0;
00194     if ( pNode->Num < pOld->Num && !pMan->fChoicing )
00195         return 0;
00196     if ( pNode == pOld )
00197         return 1;
00198     // skip the visited node
00199     if ( pNode->TravId == pMan->nTravIds )
00200         return 0;
00201     pNode->TravId = pMan->nTravIds;
00202     // check the children
00203     if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p1), pOld ) )
00204         return 1;
00205     if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p2), pOld ) )
00206         return 1;
00207     // check equivalent nodes
00208     return Fraig_CheckTfi_rec( pMan, pNode->pNextE, pOld );
00209 }

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_CollectSupergate_rec ( Fraig_Node_t *  pNode,
Fraig_NodeVec_t *  vSuper,
int  fFirst,
int  fStopAtMux 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 930 of file fraigUtil.c.

00931 {
00932     // if the new node is complemented or a PI, another gate begins
00933 //    if ( Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || Fraig_NodeIsMuxType(pNode) )
00934     if ( (!fFirst && Fraig_Regular(pNode)->nRefs > 1) || 
00935           Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || 
00936           (fStopAtMux && Fraig_NodeIsMuxType(pNode)) )
00937     {
00938         Fraig_NodeVecPushUnique( vSuper, pNode );
00939         return;
00940     }
00941     // go through the branches
00942     Fraig_CollectSupergate_rec( pNode->p1, vSuper, 0, fStopAtMux );
00943     Fraig_CollectSupergate_rec( pNode->p2, vSuper, 0, fStopAtMux );
00944 }

int Fraig_CountNodes ( Fraig_Man_t *  pMan,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file fraigUtil.c.

00150 {
00151     Fraig_NodeVec_t * vNodes;
00152     int RetValue;
00153     vNodes = Fraig_Dfs( pMan, fEquiv );
00154     RetValue = vNodes->nSize;
00155     Fraig_NodeVecFree( vNodes );
00156     return RetValue;
00157 }

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 }

Fraig_NodeVec_t* Fraig_Dfs ( Fraig_Man_t *  pMan,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file fraigUtil.c.

00056 {
00057     Fraig_NodeVec_t * vNodes;
00058     int i;
00059     pMan->nTravIds++;
00060     vNodes = Fraig_NodeVecAlloc( 100 );
00061     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00062         Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv );
00063     return vNodes;
00064 }

void Fraig_Dfs_rec ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode,
Fraig_NodeVec_t *  vNodes,
int  fEquiv 
) [static]

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

Synopsis [Recursively computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file fraigUtil.c.

00120 {
00121     assert( !Fraig_IsComplement(pNode) );
00122     // skip the visited node
00123     if ( pNode->TravId == pMan->nTravIds )
00124         return;
00125     pNode->TravId = pMan->nTravIds;
00126     // visit the transitive fanin
00127     if ( Fraig_NodeIsAnd(pNode) )
00128     {
00129         Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p1), vNodes, fEquiv );
00130         Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p2), vNodes, fEquiv );
00131     }
00132     if ( fEquiv && pNode->pNextE )
00133         Fraig_Dfs_rec( pMan, pNode->pNextE, vNodes, fEquiv );
00134     // save the node
00135     Fraig_NodeVecPush( vNodes, pNode );
00136 }

Fraig_NodeVec_t* Fraig_DfsNodes ( Fraig_Man_t *  pMan,
Fraig_Node_t **  ppNodes,
int  nNodes,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file fraigUtil.c.

00098 {
00099     Fraig_NodeVec_t * vNodes;
00100     int i;
00101     pMan->nTravIds++;
00102     vNodes = Fraig_NodeVecAlloc( 100 );
00103     for ( i = 0; i < nNodes; i++ )
00104         Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv );
00105     return vNodes;
00106 }

Fraig_NodeVec_t* Fraig_DfsOne ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file fraigUtil.c.

00078 {
00079     Fraig_NodeVec_t * vNodes;
00080     pMan->nTravIds++;
00081     vNodes = Fraig_NodeVecAlloc( 100 );
00082     Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv );
00083     return vNodes;
00084 }

int Fraig_GetMaxLevel ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Sets up the mask.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file fraigUtil.c.

00426 {
00427     int nLevelMax, i;
00428     nLevelMax = 0;
00429     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00430         nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? 
00431                 nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level;
00432     return nLevelMax;
00433 }

int Fraig_ManCheckConsistency ( Fraig_Man_t *  p  ) 

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

Synopsis [Verify one useful property.]

Description [This procedure verifies one useful property. After the FRAIG construction with choice nodes is over, each primary node should have fanins that are primary nodes. The primary nodes is the one that does not have pNode->pRepr set to point to another node.]

SideEffects []

SeeAlso []

Definition at line 309 of file fraigUtil.c.

00310 {
00311     Fraig_Node_t * pNode;
00312     Fraig_NodeVec_t * pVec;
00313     int i;
00314     pVec = Fraig_Dfs( p, 0 );
00315     for ( i = 0; i < pVec->nSize; i++ )
00316     {
00317         pNode = pVec->pArray[i];
00318         if ( Fraig_NodeIsVar(pNode) )
00319         {
00320             if ( pNode->pRepr )
00321                 printf( "Primary input %d is a secondary node.\n", pNode->Num );
00322         }
00323         else if ( Fraig_NodeIsConst(pNode) )
00324         {
00325             if ( pNode->pRepr )
00326                 printf( "Constant 1 %d is a secondary node.\n", pNode->Num );
00327         }
00328         else
00329         {
00330             if ( pNode->pRepr )
00331                 printf( "Internal node %d is a secondary node.\n", pNode->Num );
00332             if ( Fraig_Regular(pNode->p1)->pRepr )
00333                 printf( "Internal node %d has first fanin %d that is a secondary node.\n", 
00334                     pNode->Num, Fraig_Regular(pNode->p1)->Num );
00335             if ( Fraig_Regular(pNode->p2)->pRepr )
00336                 printf( "Internal node %d has second fanin %d that is a secondary node.\n", 
00337                     pNode->Num, Fraig_Regular(pNode->p2)->Num );
00338         }
00339     }
00340     Fraig_NodeVecFree( pVec );
00341     return 1;
00342 }

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_ManIncrementTravId ( Fraig_Man_t *  pMan  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 977 of file fraigUtil.c.

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

void Fraig_ManMarkRealFanouts ( Fraig_Man_t *  p  ) 

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

Synopsis [Sets the number of fanouts (none, one, or many).]

Description [This procedure collects the nodes reachable from the POs of the AIG and sets the type of fanout counter (none, one, or many) for each node. This procedure is useful to determine fanout-free cones of AND-nodes, which is helpful for rebalancing the AIG (see procedure Fraig_ManRebalance, or something like that).]

SideEffects []

SeeAlso []

Definition at line 248 of file fraigUtil.c.

00249 {
00250     Fraig_NodeVec_t * vNodes;
00251     Fraig_Node_t * pNodeR;
00252     int i;
00253     // collect the nodes reachable
00254     vNodes = Fraig_Dfs( p, 0 );
00255     // clean the fanouts field
00256     for ( i = 0; i < vNodes->nSize; i++ )
00257     {
00258         vNodes->pArray[i]->nFanouts = 0;
00259         vNodes->pArray[i]->pData0 = NULL;
00260     }
00261     // mark reachable nodes by setting the two-bit counter pNode->nFans
00262     for ( i = 0; i < vNodes->nSize; i++ )
00263     {
00264         pNodeR = Fraig_Regular(vNodes->pArray[i]->p1);
00265         if ( pNodeR && ++pNodeR->nFanouts == 3 )
00266             pNodeR->nFanouts = 2;
00267         pNodeR = Fraig_Regular(vNodes->pArray[i]->p2);
00268         if ( pNodeR && ++pNodeR->nFanouts == 3 )
00269             pNodeR->nFanouts = 2;
00270     }
00271     Fraig_NodeVecFree( vNodes );
00272 }

int Fraig_ManPrintRefs ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Counts the number of EXOR type nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file fraigUtil.c.

00840 {
00841     Fraig_NodeVec_t * vPivots;
00842     Fraig_Node_t * pNode, * pNode2;
00843     int i, k, Counter, nProved;
00844     int clk;
00845 
00846     vPivots = Fraig_NodeVecAlloc( 1000 );
00847     for ( i = 0; i < pMan->vNodes->nSize; i++ )
00848     {
00849         pNode = pMan->vNodes->pArray[i];
00850 
00851         if ( pNode->nOnes == 0 || pNode->nOnes == (unsigned)pMan->nWordsRand * 32 )
00852             continue;
00853 
00854         if ( pNode->nRefs > 5 )
00855         {
00856             Fraig_NodeVecPush( vPivots, pNode );
00857 //            printf( "Node %6d : nRefs = %2d   Level = %3d.\n", pNode->Num, pNode->nRefs, pNode->Level );
00858         }
00859     }
00860     printf( "Total nodes = %d. Referenced nodes = %d.\n", pMan->vNodes->nSize, vPivots->nSize );
00861 
00862 clk = clock();
00863     // count implications
00864     Counter = nProved = 0;
00865     for ( i = 0; i < vPivots->nSize; i++ )
00866         for ( k = i+1; k < vPivots->nSize; k++ )
00867         {
00868             pNode  = vPivots->pArray[i];
00869             pNode2 = vPivots->pArray[k];
00870             if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
00871             {
00872                 if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
00873                     nProved++;
00874                 Counter++;
00875             }
00876             else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
00877             {
00878                 if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
00879                     nProved++;
00880                 Counter++;
00881             }
00882         }
00883     printf( "Number of candidate pairs = %d.  Proved = %d.\n", Counter, nProved );
00884 PRT( "Time", clock() - clk );
00885     return 0;
00886 }

void Fraig_ManReportChoices ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Reports statistics on choice nodes.]

Description [The number of choice nodes is the number of primary nodes, which has pNextE set to a pointer. The number of choices is the number of entries in the equivalent-node lists of the primary nodes.]

SideEffects []

SeeAlso []

Definition at line 517 of file fraigUtil.c.

00518 {
00519     Fraig_Node_t * pNode, * pTemp;
00520     int nChoiceNodes, nChoices;
00521     int i, LevelMax1, LevelMax2;
00522 
00523     // report the number of levels
00524     LevelMax1 = Fraig_GetMaxLevel( pMan );
00525     Fraig_MappingSetChoiceLevels( pMan, 0 );
00526     LevelMax2 = Fraig_GetMaxLevel( pMan );
00527 
00528     // report statistics about choices
00529     nChoiceNodes = nChoices = 0;
00530     for ( i = 0; i < pMan->vNodes->nSize; i++ )
00531     {
00532         pNode = pMan->vNodes->pArray[i];
00533         if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
00534         { // this is a choice node = the primary node that has equivalent nodes
00535             nChoiceNodes++;
00536             for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
00537                 nChoices++;
00538         }
00539     }
00540     printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
00541     printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
00542 }

void Fraig_MappingSetChoiceLevels ( Fraig_Man_t *  pMan,
int  fMaximum 
)

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

Synopsis [Resets the levels of the nodes in the choice graph.]

Description [Makes the level of the choice nodes to be equal to the maximum of the level of the nodes in the equivalence class. This way sorting by level leads to the reverse topological order, which is needed for the required time computation.]

SideEffects []

SeeAlso []

Definition at line 496 of file fraigUtil.c.

00497 {
00498     int i;
00499     pMan->nTravIds++;
00500     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00501         Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum );
00502 }

int Fraig_MappingUpdateLevel_rec ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode,
int  fMaximum 
)

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

Synopsis [Analyses choice nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file fraigUtil.c.

00447 {
00448     Fraig_Node_t * pTemp;
00449     int Level1, Level2, LevelE;
00450     assert( !Fraig_IsComplement(pNode) );
00451     if ( !Fraig_NodeIsAnd(pNode) )
00452         return pNode->Level;
00453     // skip the visited node
00454     if ( pNode->TravId == pMan->nTravIds )
00455         return pNode->Level;
00456     pNode->TravId = pMan->nTravIds;
00457     // compute levels of the children nodes
00458     Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum );
00459     Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum );
00460     pNode->Level = 1 + FRAIG_MAX( Level1, Level2 );
00461     if ( pNode->pNextE )
00462     {
00463         LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
00464         if ( fMaximum )
00465         {
00466             if ( pNode->Level < LevelE )
00467                 pNode->Level = LevelE;
00468         }
00469         else
00470         {
00471             if ( pNode->Level > LevelE )
00472                 pNode->Level = LevelE;
00473         }
00474         // set the level of all equivalent nodes to be the same minimum
00475         if ( pNode->pRepr == NULL ) // the primary node
00476             for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE )
00477                 pTemp->Level = pNode->Level;
00478     }
00479     return pNode->Level;
00480 }

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_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_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_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_PrintNode ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Prints the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 355 of file fraigUtil.c.

00356 {
00357     Fraig_NodeVec_t * vNodes;
00358     Fraig_Node_t * pTemp;
00359     int fCompl1, fCompl2, i;
00360 
00361     vNodes = Fraig_DfsOne( p, pNode, 0 );
00362     for ( i = 0; i < vNodes->nSize; i++ )
00363     {
00364         pTemp = vNodes->pArray[i];
00365         if ( Fraig_NodeIsVar(pTemp) )
00366         {
00367             printf( "%3d : PI          ", pTemp->Num );
00368             Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
00369             printf( "   " );
00370             Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
00371             printf( "  %d\n", pTemp->fInv );
00372             continue;
00373         }
00374 
00375         fCompl1 = Fraig_IsComplement(pTemp->p1);
00376         fCompl2 = Fraig_IsComplement(pTemp->p2);
00377         printf( "%3d : %c%3d %c%3d   ", pTemp->Num,
00378             (fCompl1? '-':'+'), Fraig_Regular(pTemp->p1)->Num,
00379             (fCompl2? '-':'+'), Fraig_Regular(pTemp->p2)->Num );
00380         Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
00381         printf( "   " );
00382         Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
00383         printf( "  %d\n", pTemp->fInv );
00384     }
00385     Fraig_NodeVecFree( vNodes );
00386 }

Variable Documentation

int bit_count[256] [static]
Initial value:
 {
  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
}

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

FileName [fraigUtil.c]

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

Synopsis [Various utilities.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigUtil.c,v 1.15 2005/07/08 01:01:34 alanmi Exp

] DECLARATIONS ///

Definition at line 26 of file fraigUtil.c.

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