diff options
Diffstat (limited to 'src/sat/aig/fraigEngine.c')
| -rw-r--r-- | src/sat/aig/fraigEngine.c | 125 |
1 files changed, 84 insertions, 41 deletions
diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c index 6214bf3b..17468e8f 100644 --- a/src/sat/aig/fraigEngine.c +++ b/src/sat/aig/fraigEngine.c @@ -30,6 +30,39 @@ /**Function************************************************************* + Synopsis [Simulates all nodes using random simulation for the first time.] + + Description [Assigns the original simulation info and the storage for the + future simulation info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ) +{ + Aig_SimInfo_t * pInfoPi, * pInfoAll; + assert( !p->pInfo && !p->pInfoTemp ); + // create random PI info + pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 ); + Aig_SimInfoRandom( pInfoPi ); + // allocate sim info for all nodes + pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 1 ); + // simulate though the circuit + Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); + // detect classes + p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); + Aig_SimInfoFree( pInfoAll ); + // save simulation info + p->pInfo = pInfoPi; + p->pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), Aig_ManPiNum(p)+1, 0 ); + p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1, 1 ); + p->pPatMask = Aig_PatternAlloc( Aig_ManPiNum(p)+1 ); +} + +/**Function************************************************************* + Synopsis [Starts the simulation engine for the first time.] Description [Tries several random patterns and their distance-1 @@ -43,15 +76,55 @@ void Aig_EngineSimulateFirst( Aig_Man_t * p ) { Aig_Pattern_t * pPat; - int i; - assert( Vec_PtrSize(p->vPats) == 0 ); - for ( i = 0; i < p->nPatsMax; i++ ) + int i, Counter; + + // simulate the pattern of all zeros + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternClean( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + + // simulate the pattern of all ones + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternFill( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + + // simulate random until the number of new patterns is reasonable + do { + // generate random PI siminfo + Aig_SimInfoRandom( p->pInfoPi ); + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL ); + if ( Vec_VecSize(p->vClasses) == 0 ) + return; + // count the number of useful patterns + Counter = Aig_PatternCount(p->pPatMask); + } + while ( Counter > p->nPatsMax/2 ); + + // perform targetted simulation + for ( i = 0; i < 3; i++ ) { - pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); - Aig_PatternRandom( pPat ); - Vec_PtrPush( p->vPats, pPat ); - if ( !Aig_EngineSimulate( p ) ) + assert( Vec_PtrSize(p->vPats) == 0 ); + // generate random PI siminfo + Aig_SimInfoRandom( p->pInfoPi ); + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats ); + if ( Vec_VecSize(p->vClasses) == 0 ) return; + // simulate the remaining patters + if ( Vec_PtrSize(p->vPats) > 0 ) + if ( !Aig_EngineSimulate( p ) ) + return; } } @@ -79,51 +152,21 @@ int Aig_EngineSimulate( Aig_Man_t * p ) { // get the pattern and create new siminfo pPat = Vec_PtrPop(p->vPats); + assert( pPat->nBits == Aig_ManPiNum(p) ); // create the new siminfo Aig_SimInfoFromPattern( p->pInfoPi, pPat ); - // free the patter + // free the pattern Aig_PatternFree( pPat ); // simulate this info Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); // split the classes and collect the new patterns - Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses ); + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats ); } return Vec_VecSize(p->vClasses) > 0; } -/**Function************************************************************* - - Synopsis [Simulates all nodes using random simulation for the first time.] - - Description [Assigns the original simulation info and the storage for the - future simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ) -{ - Aig_SimInfo_t * pInfoPi, * pInfoAll; - assert( !p->pInfo && !p->pInfoTemp ); - // create random PI info - pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 ); - Aig_SimInfoRandom( pInfoPi ); - // allocate sim info for all nodes - pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); - // simulate though the circuit - Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); - // detect classes - p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); - Aig_SimInfoFree( pInfoAll ); - // save simulation info - p->pInfo = pInfoPi; - p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 ); - p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |