abc70930: src/sat/fraig/fraigUtil.c Source File

00001 
00019 #include "fraigInt.h"
00020 #include <limits.h>
00021 
00025 
00026 static int bit_count[256] = {
00027   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,
00028   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,
00029   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,
00030   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,
00031   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,
00032   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,
00033   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,
00034   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
00035 };
00036 
00037 static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv );
00038 static int  Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld );
00039 
00043 
00055 Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv )
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 }
00065 
00077 Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv )
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 }
00085 
00097 Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv )
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 }
00107 
00119 void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv )
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 }
00137 
00149 int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv )
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 }
00158 
00170 int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
00171 {
00172     assert( !Fraig_IsComplement(pOld) );
00173     assert( !Fraig_IsComplement(pNew) );
00174     pMan->nTravIds++;
00175     return Fraig_CheckTfi_rec( pMan, pNew, pOld );
00176 }
00177 
00189 int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld )
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 }
00210 
00211 
00223 int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
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 }
00232 
00248 void Fraig_ManMarkRealFanouts( Fraig_Man_t * p )
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 }
00273 
00285 int Fraig_BitStringCountOnes( unsigned * pString, int nWords )
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 }
00294 
00309 int Fraig_ManCheckConsistency( Fraig_Man_t * p )
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 }
00343 
00355 void Fraig_PrintNode( Fraig_Man_t * p, Fraig_Node_t * pNode )
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 }
00387 
00399 void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits )
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 }
00413 
00425 int Fraig_GetMaxLevel( Fraig_Man_t * pMan )
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 }
00434 
00446 int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fMaximum )
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 }
00481 
00496 void Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum )
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 }
00503 
00517 void Fraig_ManReportChoices( Fraig_Man_t * pMan )
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 }
00543 
00555 int Fraig_NodeIsExorType( Fraig_Node_t * pNode )
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 }
00576 
00588 int Fraig_NodeIsMuxType( Fraig_Node_t * pNode )
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 }
00618 
00630 int Fraig_NodeIsExor( Fraig_Node_t * pNode )
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 }
00640 
00655 Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE )
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 }
00727 
00739 int Fraig_ManCountExors( Fraig_Man_t * pMan )
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 }
00748 
00760 int Fraig_ManCountMuxes( Fraig_Man_t * pMan )
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 }
00769 
00781 int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
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 }
00802 
00814 int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums )
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 }
00825 
00826 
00827 
00839 int Fraig_ManPrintRefs( Fraig_Man_t * pMan )
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 }
00887 
00888 
00902 int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew )
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 }
00917 
00918 
00930 void Fraig_CollectSupergate_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, int fFirst, int fStopAtMux )
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 }
00945 
00957 Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux )
00958 {
00959     Fraig_NodeVec_t * vSuper;
00960     vSuper = Fraig_NodeVecAlloc( 8 );
00961     Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
00962     return vSuper;
00963 }
00964 
00965 
00977 void Fraig_ManIncrementTravId( Fraig_Man_t * pMan )
00978 {
00979     pMan->nTravIds2++;
00980 }
00981 
00993 void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
00994 {
00995     pNode->TravId2 = pMan->nTravIds2;
00996 }
00997 
01009 int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
01010 {
01011     return pNode->TravId2 == pMan->nTravIds2;
01012 }
01013 
01025 int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
01026 {
01027     return pNode->TravId2 == pMan->nTravIds2 - 1;
01028 }
01029 
01033 
01034