#include "fra.h"
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*************************************************************
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 }
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 }
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 }
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 }
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 [
] 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 }
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 []
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 }