abc70930: src/opt/rwr/rwrLib.c Source File

00001 
00021 #include "rwr.h"
00022 
00026 
00027 static Rwr_Node_t *        Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
00028 static void                Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
00029 
00033 
00045 void Rwr_ManPrecompute( Rwr_Man_t * p )
00046 {
00047     Rwr_Node_t * p0, * p1;
00048     int i, k, Level, Volume;
00049     int LevelOld = -1;
00050     int nNodes;
00051 
00052     Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
00053     Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
00054     {
00055         if ( LevelOld < (int)p0->Level )
00056         {
00057             LevelOld = p0->Level;
00058             printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
00059             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00060                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00061         }
00062 
00063         if ( k == i )
00064             break;
00065 //        if ( p0->Level + p1->Level > 6 ) // hard
00066 //            break;
00067 
00068         if ( p0->Level + p1->Level > 5 ) // easy 
00069             break;
00070 
00071 //        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
00072 //            break;
00073 
00074         // compute the level and volume of the new nodes
00075         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
00076         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
00077         // try four different AND nodes
00078         Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
00079         Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
00080         Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
00081         Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
00082         // try EXOR
00083         Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
00084         // report the progress
00085         if ( p->nConsidered % 50000000 == 0 )
00086             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00087                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00088         // quit after some time
00089         if ( p->vForest->nSize == RWR_LIMIT + 5 )
00090         {
00091             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00092                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00093             goto save;
00094         }
00095     }
00096 save :
00097 
00098     // mark the relevant ones
00099     Rwr_ManIncTravId( p );
00100     k = 5;
00101     nNodes = 0;
00102     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00103         if ( p0->uTruth == p->puCanons[p0->uTruth] )
00104         {
00105             Rwr_MarkUsed_rec( p, p0 );
00106             nNodes++;
00107         }
00108 
00109     // compact the array by throwing away non-canonical
00110     k = 5;
00111     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00112         if ( p0->fUsed )
00113         {
00114             p->vForest->pArray[k] = p0;
00115             p0->Id = k++;
00116         }
00117     p->vForest->nSize = k;
00118     printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
00119 }
00120 
00132 Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
00133 {
00134     Rwr_Node_t * pOld, * pNew, ** ppPlace;
00135     unsigned uTruth;
00136     // compute truth table, level, volume
00137     p->nConsidered++;
00138     if ( fExor )
00139     {
00140 //        printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
00141         uTruth = (p0->uTruth ^ p1->uTruth);
00142     }
00143     else
00144         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
00145                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
00146     // skip non-practical classes
00147     if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
00148         return NULL;
00149     // enumerate through the nodes with the same canonical form
00150     ppPlace = p->pTable + uTruth;
00151     for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
00152     {
00153         if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
00154             return NULL;
00155         if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
00156             return NULL;
00157 //        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
00158 //            return NULL;
00159     }
00160 /*
00161     // enumerate through the nodes with the opposite polarity
00162     for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
00163     {
00164         if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
00165             return NULL;
00166         if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
00167             return NULL;
00168 //        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
00169 //            return NULL;
00170     }
00171 */
00172     // count the classes
00173     if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
00174         p->nClasses++;
00175     // create the new node
00176     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00177     pNew->Id     = p->vForest->nSize;
00178     pNew->TravId = 0;
00179     pNew->uTruth = uTruth;
00180     pNew->Level  = Level;
00181     pNew->Volume = Volume;
00182     pNew->fUsed  = 0;
00183     pNew->fExor  = fExor;
00184     pNew->p0     = p0;
00185     pNew->p1     = p1;
00186     pNew->pNext  = NULL;
00187     Vec_PtrPush( p->vForest, pNew );
00188     *ppPlace     = pNew;
00189     return pNew;
00190 }
00191 
00203 Rwr_Node_t * Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
00204 {
00205     Rwr_Node_t * pNew;
00206     unsigned uTruth;
00207     // compute truth table, leve, volume
00208     p->nConsidered++;
00209     if ( fExor )
00210         uTruth = (p0->uTruth ^ p1->uTruth);
00211     else
00212         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
00213                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
00214     // create the new node
00215     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00216     pNew->Id     = p->vForest->nSize;
00217     pNew->TravId = 0;
00218     pNew->uTruth = uTruth;
00219     pNew->Level  = Level;
00220     pNew->Volume = Volume;
00221     pNew->fUsed  = 0;
00222     pNew->fExor  = fExor;
00223     pNew->p0     = p0;
00224     pNew->p1     = p1;
00225     pNew->pNext  = NULL;
00226     Vec_PtrPush( p->vForest, pNew );
00227     // do not add if the node is not essential
00228     if ( uTruth != p->puCanons[uTruth] )
00229         return pNew;
00230 
00231     // add to the list
00232     p->nAdded++;
00233     if ( p->pTable[uTruth] == NULL )
00234         p->nClasses++;
00235     Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00236     return pNew;
00237 }
00238 
00250 Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute )
00251 {
00252     Rwr_Node_t * pNew;
00253     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00254     pNew->Id     = p->vForest->nSize;
00255     pNew->TravId = 0;
00256     pNew->uTruth = uTruth;
00257     pNew->Level  = 0;
00258     pNew->Volume = 0;
00259     pNew->fUsed  = 1;
00260     pNew->fExor  = 0;
00261     pNew->p0     = NULL;
00262     pNew->p1     = NULL;    
00263     pNew->pNext  = NULL;
00264     Vec_PtrPush( p->vForest, pNew );
00265     if ( fPrecompute )
00266         Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00267     return pNew;
00268 }
00269 
00270 
00271 
00283 void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
00284 {
00285     if ( pNode->fUsed || pNode->TravId == p->nTravIds )
00286         return;
00287     pNode->TravId = p->nTravIds;
00288     pNode->fUsed = 1;
00289     Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
00290     Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
00291 }
00292 
00304 void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
00305 {
00306     if ( pNode->fUsed || pNode->TravId == p->nTravIds )
00307         return;
00308     pNode->TravId = p->nTravIds;
00309     (*pVolume)++;
00310     if ( pNode->fExor )
00311         (*pVolume)++;
00312     Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
00313     Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
00314 }
00315 
00327 int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
00328 {
00329     int Volume = 0;
00330     Rwr_ManIncTravId( p );
00331     Rwr_Trav_rec( p, p0, &Volume );
00332     Rwr_Trav_rec( p, p1, &Volume );
00333     return Volume;
00334 }
00335 
00347 void Rwr_ManIncTravId( Rwr_Man_t * p )
00348 {
00349     Rwr_Node_t * pNode;
00350     int i;
00351     if ( p->nTravIds++ < 0x8FFFFFFF )
00352         return;
00353     Vec_PtrForEachEntry( p->vForest, pNode, i )
00354         pNode->TravId = 0;
00355     p->nTravIds = 1;
00356 }
00357 
00361 
00362