src/aig/fra/fraImp.c File Reference

#include "fra.h"
Include dependency graph for fraImp.c:

Go to the source code of this file.

Functions

static int Fra_SmlCountOnesOne (Fra_Sml_t *p, int Node)
static int * Fra_SmlCountOnes (Fra_Sml_t *p)
static int Sml_NodeCheckImp (Fra_Sml_t *p, int Left, int Right)
static int Sml_NodeNotImpWeight (Fra_Sml_t *p, int Left, int Right)
static void Sml_NodeSaveNotImpPatterns (Fra_Sml_t *p, int Left, int Right, unsigned *pResult)
Vec_Ptr_t * Fra_SmlSortUsingOnes (Fra_Sml_t *p, int fLatchCorr)
Vec_Int_t * Fra_SmlSelectMaxCost (Vec_Int_t *vImps, int *pCosts, int nCostMax, int nImpLimit, int *pCostRange)
int Sml_CompareMaxId (unsigned short *pImp1, unsigned short *pImp2)
Vec_Int_t * Fra_ImpDerive (Fra_Man_t *p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr)
void Fra_ImpAddToSolver (Fra_Man_t *p, Vec_Int_t *vImps, int *pSatVarNums)
int Fra_ImpCheckForNode (Fra_Man_t *p, Vec_Int_t *vImps, Aig_Obj_t *pNode, int Pos)
int Fra_ImpRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vImps)
void Fra_ImpCompactArray (Vec_Int_t *vImps)
double Fra_ImpComputeStateSpaceRatio (Fra_Man_t *p)
int Fra_ImpVerifyUsingSimulation (Fra_Man_t *p)
void Fra_ImpRecordInManager (Fra_Man_t *p, Aig_Man_t *pNew)

Function Documentation

void Fra_ImpAddToSolver ( Fra_Man_t *  p,
Vec_Int_t *  vImps,
int *  pSatVarNums 
)

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

Synopsis [Add implication clauses to the SAT solver.]

Description [Note that implications should be checked in the first frame!]

SideEffects []

SeeAlso []

Definition at line 419 of file fraImp.c.

00420 {
00421     sat_solver * pSat = p->pSat;
00422     Aig_Obj_t * pLeft, * pRight;
00423     Aig_Obj_t * pLeftF, * pRightF;
00424     int pLits[2], Imp, Left, Right, i, f, status;
00425     int fComplL, fComplR;
00426     Vec_IntForEachEntry( vImps, Imp, i )
00427     {
00428         // get the corresponding nodes
00429         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00430         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00431         // check if all the nodes are present
00432         for ( f = 0; f < p->pPars->nFramesK; f++ )
00433         {
00434             // map these info fraig
00435             pLeftF = Fra_ObjFraig( pLeft, f );
00436             pRightF = Fra_ObjFraig( pRight, f );
00437             if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
00438             {
00439                 Vec_IntWriteEntry( vImps, i, 0 );
00440                 break;
00441             }
00442         }
00443         if ( f < p->pPars->nFramesK )
00444             continue;
00445         // add constraints in each timeframe
00446         for ( f = 0; f < p->pPars->nFramesK; f++ )
00447         {
00448             // map these info fraig
00449             pLeftF = Fra_ObjFraig( pLeft, f );
00450             pRightF = Fra_ObjFraig( pRight, f );
00451             // get the corresponding SAT numbers
00452             Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
00453             Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
00454             assert( Left > 0  && Left < p->nSatVars );
00455             assert( Right > 0 && Right < p->nSatVars );
00456             // get the complemented attributes
00457             fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
00458             fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
00459             // get the constraint
00460             // L => R      L' v R     (complement = L & R')
00461             pLits[0] = 2 * Left  + !fComplL;
00462             pLits[1] = 2 * Right +  fComplR;
00463             // add contraint to solver
00464             if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
00465             {
00466                 sat_solver_delete( pSat );
00467                 p->pSat = NULL;
00468                 return;
00469             }
00470         }
00471     }
00472     status = sat_solver_simplify(pSat);
00473     if ( status == 0 )
00474     {
00475         sat_solver_delete( pSat );
00476         p->pSat = NULL;
00477     }
00478 //    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
00479     Fra_ImpCompactArray( vImps );
00480 //    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
00481 }

int Fra_ImpCheckForNode ( Fra_Man_t *  p,
Vec_Int_t *  vImps,
Aig_Obj_t *  pNode,
int  Pos 
)

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

Synopsis [Check implications for the node (if they are present).]

Description [Returns the new position in the array.]

SideEffects []

SeeAlso []

Definition at line 494 of file fraImp.c.

00495 {
00496     Aig_Obj_t * pLeft, * pRight;
00497     Aig_Obj_t * pLeftF, * pRightF;
00498     int i, Imp, Left, Right, Max, RetValue;
00499     int fComplL, fComplR;
00500     Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
00501     {
00502         if ( Imp == 0 )
00503             continue;
00504         Left = Fra_ImpLeft(Imp);
00505         Right = Fra_ImpRight(Imp);
00506         Max = AIG_MAX( Left, Right );
00507         assert( Max >= pNode->Id );
00508         if ( Max > pNode->Id )
00509             return i;
00510         // get the corresponding nodes
00511         pLeft  = Aig_ManObj( p->pManAig, Left );
00512         pRight = Aig_ManObj( p->pManAig, Right );
00513         // get the corresponding FRAIG nodes
00514         pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
00515         pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
00516         // get the complemented attributes
00517         fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
00518         fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
00519         // check equality
00520         if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
00521         {
00522             if ( fComplL == fComplR ) // x => x  - always true
00523                 continue;
00524             assert( fComplL != fComplR );
00525             // consider 4 possibilities:
00526             // NOT(1) => 1    or   0 => 1  - always true
00527             // 1 => NOT(1)    or   1 => 0  - never true
00528             // NOT(x) => x    or   x       - not always true
00529             // x => NOT(x)    or   NOT(x)  - not always true
00530             if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
00531                 continue;
00532             // disproved implication
00533             p->pCla->fRefinement = 1;
00534             Vec_IntWriteEntry( vImps, i, 0 );
00535             continue;
00536         }
00537         // check the implication 
00538         // - if true, a clause is added
00539         // - if false, a cex is simulated
00540         // make sure the implication is refined
00541         RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
00542         if ( RetValue != 1 )
00543         {
00544             p->pCla->fRefinement = 1;
00545             if ( RetValue == 0 )
00546                 Fra_SmlResimulate( p );
00547             if ( Vec_IntEntry(vImps, i) != 0 )
00548                 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
00549             assert( Vec_IntEntry(vImps, i) == 0 );
00550         }
00551     }
00552     return i;
00553 }

void Fra_ImpCompactArray ( Vec_Int_t *  vImps  ) 

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

Synopsis [Removes empty implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 598 of file fraImp.c.

00599 {
00600     int i, k, Imp;
00601     k = 0;
00602     Vec_IntForEachEntry( vImps, Imp, i )
00603         if ( Imp )
00604             Vec_IntWriteEntry( vImps, k++, Imp );
00605     Vec_IntShrink( vImps, k );
00606 }

double Fra_ImpComputeStateSpaceRatio ( Fra_Man_t *  p  ) 

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

Synopsis [Determines the ratio of the state space by computed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file fraImp.c.

00620 {
00621     int nSimWords = 64;
00622     Fra_Sml_t * pComb;
00623     unsigned * pResult;
00624     double Ratio = 0.0;
00625     int Left, Right, Imp, i;
00626     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00627         return Ratio;
00628     // simulate the AIG manager with combinational patterns
00629     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
00630     // go through the implications and collect where they do not hold
00631     pResult = Fra_ObjSim( pComb, 0 );
00632     assert( pResult[0] == 0 );
00633     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00634     {
00635         Left = Fra_ImpLeft(Imp);
00636         Right = Fra_ImpRight(Imp);
00637         Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
00638     }
00639     // count the number of ones in this area
00640     Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
00641     Fra_SmlStop( pComb );
00642     return Ratio;
00643 }

Vec_Int_t* Fra_ImpDerive ( Fra_Man_t *  p,
int  nImpMaxLimit,
int  nImpUseLimit,
int  fLatchCorr 
)

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

Synopsis [Derives implication candidates.]

Description [Implication candidates have the property that (1) they hold using sequential simulation information (2) they do not hold using combinational simulation information (3) they have as high expressive power as possible (heuristically) that is, they are easy to disprove combinationally meaning they cover relatively larger sequential subspace.]

SideEffects []

SeeAlso []

Definition at line 318 of file fraImp.c.

00319 {
00320     int nSimWords = 64;
00321     Fra_Sml_t * pSeq, * pComb;
00322     Vec_Int_t * vImps, * vTemp;
00323     Vec_Ptr_t * vNodes;
00324     int * pImpCosts, * pNodesI, * pNodesK;
00325     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
00326     int CostMin = AIG_INFINITY, CostMax = 0;
00327     int i, k, Imp, CostRange, clk = clock();
00328     assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
00329     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
00330     // normalize both managers
00331     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
00332     pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
00333     // get the nodes sorted by the number of 1s
00334     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
00335     // count the total number of implications
00336     for ( k = nSimWords * 32; k > 0; k-- )
00337     for ( i = k - 1; i > 0; i-- )
00338     for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
00339     for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
00340         nImpsTotal++;
00341 
00342     // compute implications and their costs
00343     pImpCosts = ALLOC( int, nImpMaxLimit );
00344     vImps = Vec_IntAlloc( nImpMaxLimit );
00345     for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
00346         for ( i = k - 1; i > 0; i-- )
00347         {
00348             for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
00349             for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
00350             {
00351                 nImpsTried++;
00352                 if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
00353                 {
00354                     nImpsNonSeq++;
00355                     continue;
00356                 }
00357                 if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
00358                 {
00359                     nImpsComb++;
00360                     continue;
00361                 }
00362                 nImpsCollected++;
00363                 Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
00364                 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
00365                 CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
00366                 CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
00367                 Vec_IntPush( vImps, Imp );
00368                 if ( Vec_IntSize(vImps) == nImpMaxLimit )
00369                     goto finish;
00370             } 
00371         }
00372 finish:
00373     Fra_SmlStop( pComb );
00374     Fra_SmlStop( pSeq );
00375 
00376     // select implications with the highest cost
00377     CostRange = CostMin;
00378     if ( Vec_IntSize(vImps) > nImpUseLimit )
00379     {
00380         vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
00381         Vec_IntFree( vTemp );  
00382     }
00383 
00384     // dealloc
00385     free( pImpCosts ); 
00386     free( Vec_PtrEntry(vNodes, 0) );
00387     Vec_PtrFree( vNodes );
00388     // reorder implications topologically
00389     qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
00390             (int (*)(const void *, const void *)) Sml_CompareMaxId );
00391 if ( p->pPars->fVerbose )
00392 {
00393 printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
00394     nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
00395 printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
00396        CostMin, CostRange, CostMax );
00397 PRT( "Time", clock() - clk );
00398 }
00399     return vImps;
00400 }

void Fra_ImpRecordInManager ( Fra_Man_t *  p,
Aig_Man_t *  pNew 
)

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

Synopsis [Record proven implications in the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 696 of file fraImp.c.

00697 {
00698     Aig_Obj_t * pLeft, * pRight, * pMiter;
00699     int nPosOld, Imp, i;
00700     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00701         return;
00702     // go through the implication
00703     nPosOld = Aig_ManPoNum(pNew);
00704     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00705     {
00706         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00707         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00708         // record the implication: L' + R
00709         pMiter = Aig_Or( pNew, 
00710             Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
00711             Aig_NotCond(pRight->pData, pRight->fPhase) ); 
00712         Aig_ObjCreatePo( pNew, pMiter );
00713     }
00714     pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
00715 }

int Fra_ImpRefineUsingCex ( Fra_Man_t *  p,
Vec_Int_t *  vImps 
)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 566 of file fraImp.c.

00567 {
00568     Aig_Obj_t * pLeft, * pRight;
00569     int Imp, i, RetValue = 0;
00570     Vec_IntForEachEntry( vImps, Imp, i )
00571     {
00572         if ( Imp == 0 )
00573             continue;
00574         // get the corresponding nodes
00575         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00576         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00577         // check if implication holds using this simulation info
00578         if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
00579         {
00580             Vec_IntWriteEntry( vImps, i, 0 );
00581             RetValue = 1;
00582         }
00583     }
00584     return RetValue;
00585 }

int Fra_ImpVerifyUsingSimulation ( Fra_Man_t *  p  ) 

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

Synopsis [Returns the number of failed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 656 of file fraImp.c.

00657 {
00658     int nFrames = 2000;
00659     int nSimWords = 8;
00660     Fra_Sml_t * pSeq;
00661     char * pfFails;
00662     int Left, Right, Imp, i, Counter;
00663     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00664         return 0;
00665     // simulate the AIG manager with combinational patterns
00666     pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
00667     // go through the implications and check how many of them do not hold
00668     pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
00669     memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
00670     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00671     {
00672         Left = Fra_ImpLeft(Imp);
00673         Right = Fra_ImpRight(Imp);
00674         pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
00675     }
00676     // count how many has failed
00677     Counter = 0;
00678     for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
00679         Counter += pfFails[i];
00680     free( pfFails );
00681     Fra_SmlStop( pSeq );
00682     return Counter;
00683 }

static int* Fra_SmlCountOnes ( Fra_Sml_t *  p  )  [inline, static]

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

Synopsis [Counts the number of 1s in each siminfo of each node.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file fraImp.c.

00064 {
00065     Aig_Obj_t * pObj;
00066     int i, * pnBits; 
00067     pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
00068     memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
00069     Aig_ManForEachObj( p->pAig, pObj, i )
00070         pnBits[i] = Fra_SmlCountOnesOne( p, i );
00071     return pnBits;
00072 }

static int Fra_SmlCountOnesOne ( Fra_Sml_t *  p,
int  Node 
) [inline, static]

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

FileName [fraImp.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Detecting and proving implications.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id
fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Counts the number of 1s in each siminfo of each node.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file fraImp.c.

00043 {
00044     unsigned * pSim;
00045     int k, Counter = 0;
00046     pSim = Fra_ObjSim( p, Node );
00047     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00048         Counter += Aig_WordCountOnes( pSim[k] );
00049     return Counter;
00050 }

Vec_Int_t* Fra_SmlSelectMaxCost ( Vec_Int_t *  vImps,
int *  pCosts,
int  nCostMax,
int  nImpLimit,
int *  pCostRange 
)

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

Synopsis [Returns the array of implications with the highest cost.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file fraImp.c.

00242 {
00243     Vec_Int_t * vImpsNew;
00244     int * pCostCount, nImpCount, Imp, i, c;
00245     assert( Vec_IntSize(vImps) >= nImpLimit );
00246     // count how many implications have each cost
00247     pCostCount = ALLOC( int, nCostMax + 1 );
00248     memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
00249     for ( i = 0; i < Vec_IntSize(vImps); i++ )
00250     {
00251         assert( pCosts[i] <= nCostMax );
00252         pCostCount[ pCosts[i] ]++;
00253     }
00254     assert( pCostCount[0] == 0 );
00255     // select the bound on the cost (above this bound, implication will be included)
00256     nImpCount = 0;
00257     for ( c = nCostMax; c > 0; c-- )
00258     {
00259         nImpCount += pCostCount[c];
00260         if ( nImpCount >= nImpLimit )
00261             break;
00262     }
00263 //    printf( "Cost range >= %d.\n", c );
00264     // collect implications with the given costs
00265     vImpsNew = Vec_IntAlloc( nImpLimit );
00266     Vec_IntForEachEntry( vImps, Imp, i )
00267     {
00268         if ( pCosts[i] < c )
00269             continue;
00270         Vec_IntPush( vImpsNew, Imp );
00271         if ( Vec_IntSize( vImpsNew ) == nImpLimit )
00272             break;
00273     }
00274     free( pCostCount );
00275     if ( pCostRange )
00276         *pCostRange = c;
00277     return vImpsNew;
00278 }

Vec_Ptr_t* Fra_SmlSortUsingOnes ( Fra_Sml_t *  p,
int  fLatchCorr 
)

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

Synopsis [Returns the array of nodes sorted by the number of 1s.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file fraImp.c.

00152 {
00153     Aig_Obj_t * pObj;
00154     Vec_Ptr_t * vNodes;
00155     int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
00156     assert( p->nWordsTotal > 0 );
00157     // count 1s in each node's siminfo
00158     pnBits = Fra_SmlCountOnes( p );
00159     // count number of nodes having that many 1s
00160     nNodes = 0;
00161     nBits = p->nWordsTotal * 32;
00162     pnNodes = ALLOC( int, nBits + 1 );
00163     memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
00164     Aig_ManForEachObj( p->pAig, pObj, i )
00165     {
00166         if ( i == 0 ) continue;
00167         // skip non-PI and non-internal nodes
00168         if ( fLatchCorr )
00169         {
00170             if ( !Aig_ObjIsPi(pObj) )
00171                 continue;
00172         }
00173         else
00174         {
00175             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00176                 continue;
00177         }
00178         // skip nodes participating in the classes
00179 //        if ( Fra_ClassObjRepr(pObj) )
00180 //            continue;
00181         assert( pnBits[i] <= nBits ); // "<" because of normalized info
00182         pnNodes[pnBits[i]]++;
00183         nNodes++;
00184     }
00185     // allocate memory for all the nodes
00186     pMemory = ALLOC( int, nNodes + nBits + 1 );  
00187     // markup the memory for each node
00188     vNodes = Vec_PtrAlloc( nBits + 1 );
00189     Vec_PtrPush( vNodes, pMemory );
00190     for ( i = 1; i <= nBits; i++ )
00191     {
00192         pMemory += pnNodes[i-1] + 1;
00193         Vec_PtrPush( vNodes, pMemory );
00194     }
00195     // add the nodes
00196     memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
00197     Aig_ManForEachObj( p->pAig, pObj, i )
00198     {
00199         if ( i == 0 ) continue;
00200         // skip non-PI and non-internal nodes
00201         if ( fLatchCorr )
00202         {
00203             if ( !Aig_ObjIsPi(pObj) )
00204                 continue;
00205         }
00206         else
00207         {
00208             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00209                 continue;
00210         }
00211         // skip nodes participating in the classes
00212 //        if ( Fra_ClassObjRepr(pObj) )
00213 //            continue;
00214         pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
00215         pMemory[ pnNodes[pnBits[i]]++ ] = i;
00216     }
00217     // add 0s in the end
00218     nTotal = 0;
00219     Vec_PtrForEachEntry( vNodes, pMemory, i )
00220     {
00221         pMemory[ pnNodes[i]++ ] = 0;
00222         nTotal += pnNodes[i];
00223     }
00224     assert( nTotal == nNodes + nBits + 1 );
00225     free( pnNodes );
00226     free( pnBits );
00227     return vNodes;
00228 }

int Sml_CompareMaxId ( unsigned short *  pImp1,
unsigned short *  pImp2 
)

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

Synopsis [Compares two implications using their largest ID.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file fraImp.c.

00292 {
00293     int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
00294     int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
00295     if ( Max1 < Max2 )
00296         return -1;
00297     if ( Max1 > Max2  )
00298         return 1;
00299     return 0; 
00300 }

static int Sml_NodeCheckImp ( Fra_Sml_t *  p,
int  Left,
int  Right 
) [inline, static]

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

Synopsis [Returns 1 if implications holds.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file fraImp.c.

00086 {
00087     unsigned * pSimL, * pSimR;
00088     int k;
00089     pSimL = Fra_ObjSim( p, Left );
00090     pSimR = Fra_ObjSim( p, Right );
00091     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00092         if ( pSimL[k] & ~pSimR[k] )
00093             return 0;
00094     return 1;
00095 }

static int Sml_NodeNotImpWeight ( Fra_Sml_t *  p,
int  Left,
int  Right 
) [inline, static]

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

Synopsis [Counts the number of 1s in the complement of the implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file fraImp.c.

00109 {
00110     unsigned * pSimL, * pSimR;
00111     int k, Counter = 0;
00112     pSimL = Fra_ObjSim( p, Left );
00113     pSimR = Fra_ObjSim( p, Right );
00114     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00115         Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
00116     return Counter;
00117 }

static void Sml_NodeSaveNotImpPatterns ( Fra_Sml_t *  p,
int  Left,
int  Right,
unsigned *  pResult 
) [inline, static]

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

Synopsis [Computes the complement of the implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file fraImp.c.

00131 {
00132     unsigned * pSimL, * pSimR;
00133     int k;
00134     pSimL = Fra_ObjSim( p, Left );
00135     pSimR = Fra_ObjSim( p, Right );
00136     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00137         pResult[k] |= pSimL[k] & ~pSimR[k];
00138 }

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