abc70930: src/aig/kit/kitCloud.c Source File

00001 
00021 #include "kit.h"
00022 
00026 
00027 // internal representation of the function to be decomposed
00028 typedef struct Kit_Mux_t_ Kit_Mux_t;
00029 struct Kit_Mux_t_
00030 {
00031     unsigned      v  :  5;          // variable 
00032     unsigned      t  : 12;          // then edge
00033     unsigned      e  : 12;          // else edge
00034     unsigned      c  :  1;          // complemented attr of else edge
00035     unsigned      i  :  1;          // complemented attr of top node
00036 };
00037 
00041 
00053 CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
00054 {
00055     static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00056     CloudNode * pCof0, * pCof1;
00057     unsigned uCof0, uCof1;
00058     assert( nVars <= 5 );
00059     if ( uTruth == 0 )
00060         return dd->zero;
00061     if ( uTruth == ~0 )
00062         return dd->one;
00063     if ( nVars == 1 )
00064     {
00065         if ( uTruth == uVars[0] )
00066             return dd->vars[nVarsAll-1];
00067         if ( uTruth == ~uVars[0] )
00068             return Cloud_Not(dd->vars[nVarsAll-1]);
00069         assert( 0 );
00070     }
00071 //    Count++;
00072     assert( nVars > 1 );
00073     uCof0 = uTruth & ~uVars[nVars-1];
00074     uCof1 = uTruth &  uVars[nVars-1];
00075     uCof0 |= uCof0 << (1<<(nVars-1));
00076     uCof1 |= uCof1 >> (1<<(nVars-1));
00077     if ( uCof0 == uCof1 )
00078         return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00079     if ( uCof0 == ~uCof1 )
00080     {
00081         pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00082         pCof1 = Cloud_Not( pCof0 );
00083     }
00084     else
00085     {
00086         pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00087         pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
00088     }
00089     return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
00090 }
00091 
00103 CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
00104 {
00105     CloudNode * pCof0, * pCof1;
00106     unsigned * pTruth0, * pTruth1;
00107     if ( nVars <= 5 )
00108         return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
00109     if ( Kit_TruthIsConst0(pTruth, nVars) )
00110         return dd->zero;
00111     if ( Kit_TruthIsConst1(pTruth, nVars) )
00112         return dd->one;
00113 //    Count++;
00114     pTruth0 = pTruth;
00115     pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
00116     if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
00117         return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00118     if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
00119     {
00120         pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00121         pCof1 = Cloud_Not( pCof0 );
00122     }
00123     else
00124     {
00125         pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00126         pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
00127     }
00128     return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
00129 }
00130 
00142 CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
00143 {
00144     CloudNode * pRes;
00145     pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
00146 //    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
00147     return pRes;
00148 }
00149 
00161 int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
00162 {
00163     Kit_Mux_t Mux;
00164     int nNodes, i;
00165     // collect BDD nodes
00166     nNodes = Cloud_DagCollect( dd, pFunc );
00167     if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
00168         return 0;
00169     assert( nNodes == Cloud_DagSize( dd, pFunc ) );
00170     assert( nNodes < dd->nNodesLimit );
00171     Vec_IntClear( vNodes );
00172     Vec_IntPush( vNodes, 0 ); // const1 node
00173     dd->ppNodes[0]->s = 0;
00174     for ( i = 1; i < nNodes; i++ )
00175     {
00176         dd->ppNodes[i]->s = i;
00177         Mux.v = dd->ppNodes[i]->v;
00178         Mux.t = dd->ppNodes[i]->t->s;
00179         Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
00180         Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
00181         Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
00182         // put the MUX into the array
00183         Vec_IntPush( vNodes, *((int *)&Mux) );
00184     }
00185     assert( Vec_IntSize(vNodes) == nNodes );
00186     // reset signatures
00187     for ( i = 0; i < nNodes; i++ )
00188         dd->ppNodes[i]->s = dd->nSignCur;
00189     return 1;
00190 }
00191 
00203 int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
00204 {
00205     CloudNode * pFunc;
00206     Cloud_Restart( dd );
00207     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00208     Vec_IntClear( vNodes );
00209     return Kit_CreateCloud( dd, pFunc, vNodes );
00210 }
00211 
00223 unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
00224 {
00225     unsigned * pThis, * pFan0, * pFan1;
00226     Kit_Mux_t Mux;
00227     int i, Entry;
00228     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00229     pThis = Vec_PtrEntry( vStore, 0 );
00230     Kit_TruthFill( pThis, nVars );
00231     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00232     {
00233         Mux = *((Kit_Mux_t *)&Entry);
00234         assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
00235         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00236         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00237         pThis = Vec_PtrEntry( vStore, i );
00238         Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
00239     } 
00240     // complement the result
00241     if ( Mux.i )
00242         Kit_TruthNot( pThis, pThis, nVars );
00243     return pThis;
00244 }
00245 
00257 unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, 
00258     unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
00259 {
00260     CloudNode * pFunc;
00261     unsigned * pThis, * pFan0, * pFan1;
00262     Kit_Mux_t Mux;
00263     int i, Entry, RetValue;
00264     // derive BDD from truth table
00265     Cloud_Restart( dd );
00266     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00267     // convert it into nodes
00268     RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
00269     if ( RetValue == 0 )
00270         printf( "Kit_TruthCompose(): Internal failure!!!\n" );
00271     // verify the result
00272 //    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
00273 //    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
00274 //        printf( "Failed!\n" );
00275     // compute truth table from the BDD
00276     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00277     pThis = Vec_PtrEntry( vStore, 0 );
00278     Kit_TruthFill( pThis, nVarsAll );
00279     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00280     {
00281         Mux = *((Kit_Mux_t *)&Entry);
00282         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00283         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00284         pThis = Vec_PtrEntry( vStore, i );
00285         Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
00286     }
00287     // complement the result
00288     if ( Mux.i )
00289         Kit_TruthNot( pThis, pThis, nVarsAll );
00290     return pThis;
00291 }
00292 
00304 void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
00305 {
00306     Kit_Mux_t Mux;
00307     unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
00308     int i, v, Var, Entry, nSupps;
00309     nSupps = 2 * nVars;
00310 
00311     // extend storage
00312     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
00313         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
00314     puSuppAll = Vec_IntArray( vMemory );
00315     // clear storage for the const node
00316     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00317     // compute supports from nodes
00318     Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
00319     {
00320         Mux = *((Kit_Mux_t *)&Entry);
00321         Var = nVars - 1 - Mux.v;
00322         pFan0 = puSuppAll + nSupps * Mux.e;
00323         pFan1 = puSuppAll + nSupps * Mux.t;
00324         pThis = puSuppAll + nSupps * i;
00325         for ( v = 0; v < nSupps; v++ )
00326             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00327         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00328         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00329         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00330         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00331     }
00332     // copy the result
00333     memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
00334     // compute the inverse
00335 
00336     // extend storage
00337     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
00338         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
00339     puSuppAll = Vec_IntArray( vMemory );
00340     // clear storage for the const node
00341     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00342     // compute supports from nodes
00343     Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
00344     {
00345         Mux = *((Kit_Mux_t *)&Entry);
00346 //        Var = nVars - 1 - Mux.v;
00347         Var = Mux.v;
00348         pFan0 = puSuppAll + nSupps * Mux.e;
00349         pFan1 = puSuppAll + nSupps * Mux.t;
00350         pThis = puSuppAll + nSupps * i;
00351         for ( v = 0; v < nSupps; v++ )
00352             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00353         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00354         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00355         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00356         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00357     }
00358 
00359     // merge supports
00360     for ( Var = 0; Var < nSupps; Var++ )
00361         puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
00362 }
00363 
00367 
00368