abc70930: src/aig/dar/darScript.c Source File

00001 
00021 #include "darInt.h"
00022 //#include "ioa.h"
00023 
00027 
00031 
00043 Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
00044 {
00045     Aig_Man_t * pTemp;
00046     Dar_RwrPar_t Pars, * pPars = &Pars;
00047     Dar_ManDefaultRwrParams( pPars );
00048     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00049     Aig_ManStop( pTemp );
00050     Dar_ManRewrite( pAig, pPars );
00051     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00052     Aig_ManStop( pTemp );
00053     return pAig;
00054 }
00055 
00067 Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
00068 //alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
00069 {
00070     Aig_Man_t * pTemp;
00071 
00072     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00073     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00074 
00075     Dar_ManDefaultRwrParams( pParsRwr );
00076     Dar_ManDefaultRefParams( pParsRef );
00077 
00078     pParsRwr->fUpdateLevel = 0;
00079     pParsRef->fUpdateLevel = 0;
00080 
00081     pParsRwr->fVerbose = fVerbose;
00082     pParsRef->fVerbose = fVerbose;
00083 
00084     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00085     Aig_ManStop( pTemp );
00086     
00087     // rewrite
00088     Dar_ManRewrite( pAig, pParsRwr );
00089     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00090     Aig_ManStop( pTemp );
00091     
00092     // refactor
00093     Dar_ManRefactor( pAig, pParsRef );
00094     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00095     Aig_ManStop( pTemp );
00096 
00097     // balance
00098     if ( fBalance )
00099     {
00100     pAig = Dar_ManBalance( pTemp = pAig, 0 );
00101     Aig_ManStop( pTemp );
00102     }
00103     
00104     // rewrite
00105     Dar_ManRewrite( pAig, pParsRwr );
00106     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00107     Aig_ManStop( pTemp );
00108 
00109     return pAig;
00110 }
00111 
00112 
00124 Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
00125 //alias compress2   "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
00126 {
00127     Aig_Man_t * pTemp;
00128 
00129     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00130     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00131 
00132     Dar_ManDefaultRwrParams( pParsRwr );
00133     Dar_ManDefaultRefParams( pParsRef );
00134 
00135     pParsRwr->fUpdateLevel = fUpdateLevel;
00136     pParsRef->fUpdateLevel = fUpdateLevel;
00137 
00138     pParsRwr->fVerbose = 0;//fVerbose;
00139     pParsRef->fVerbose = 0;//fVerbose;
00140 
00141     pAig = Aig_ManDup( pAig, 0 ); 
00142     if ( fVerbose ) Aig_ManPrintStats( pAig );
00143 
00144     // balance
00145     if ( fBalance )
00146     {
00147 //    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00148 //    Aig_ManStop( pTemp );
00149 //    if ( fVerbose ) Aig_ManPrintStats( pAig );
00150     }
00151     
00152     // rewrite
00153     Dar_ManRewrite( pAig, pParsRwr );
00154     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00155     Aig_ManStop( pTemp );
00156     if ( fVerbose ) Aig_ManPrintStats( pAig );
00157     
00158     // refactor
00159     Dar_ManRefactor( pAig, pParsRef );
00160     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00161     Aig_ManStop( pTemp );
00162     if ( fVerbose ) Aig_ManPrintStats( pAig );
00163 
00164     // balance
00165     if ( fBalance )
00166     {
00167     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00168     Aig_ManStop( pTemp );
00169     if ( fVerbose ) Aig_ManPrintStats( pAig );
00170     }
00171 
00172     pParsRwr->fUseZeros = 1;
00173     pParsRef->fUseZeros = 1;
00174     
00175     // rewrite
00176     Dar_ManRewrite( pAig, pParsRwr );
00177     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00178     Aig_ManStop( pTemp );
00179     if ( fVerbose ) Aig_ManPrintStats( pAig );
00180 
00181     return pAig;
00182 }
00183 
00195 Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
00196 //alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
00197 {
00198     Aig_Man_t * pTemp;
00199 
00200     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00201     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00202 
00203     Dar_ManDefaultRwrParams( pParsRwr );
00204     Dar_ManDefaultRefParams( pParsRef );
00205 
00206     pParsRwr->fUpdateLevel = fUpdateLevel;
00207     pParsRef->fUpdateLevel = fUpdateLevel;
00208 
00209     pParsRwr->fVerbose = 0;//fVerbose;
00210     pParsRef->fVerbose = 0;//fVerbose;
00211 
00212     pAig = Aig_ManDup( pAig, 0 ); 
00213     if ( fVerbose ) Aig_ManPrintStats( pAig );
00214 
00215     // balance
00216     if ( fBalance )
00217     {
00218 //    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00219 //    Aig_ManStop( pTemp );
00220 //    if ( fVerbose ) Aig_ManPrintStats( pAig );
00221     }
00222     
00223 
00224     // rewrite
00225     Dar_ManRewrite( pAig, pParsRwr );
00226     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00227     Aig_ManStop( pTemp );
00228     if ( fVerbose ) Aig_ManPrintStats( pAig );
00229     
00230     // refactor
00231     Dar_ManRefactor( pAig, pParsRef );
00232     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00233     Aig_ManStop( pTemp );
00234     if ( fVerbose ) Aig_ManPrintStats( pAig );
00235 
00236     // balance
00237 //    if ( fBalance )
00238     {
00239     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00240     Aig_ManStop( pTemp );
00241     if ( fVerbose ) Aig_ManPrintStats( pAig );
00242     }
00243     
00244     // rewrite
00245     Dar_ManRewrite( pAig, pParsRwr );
00246     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00247     Aig_ManStop( pTemp );
00248     if ( fVerbose ) Aig_ManPrintStats( pAig );
00249 
00250     pParsRwr->fUseZeros = 1;
00251     pParsRef->fUseZeros = 1;
00252     
00253     // rewrite
00254     Dar_ManRewrite( pAig, pParsRwr );
00255     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00256     Aig_ManStop( pTemp );
00257     if ( fVerbose ) Aig_ManPrintStats( pAig );
00258 
00259     // balance
00260     if ( fBalance )
00261     {
00262     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00263     Aig_ManStop( pTemp );
00264     if ( fVerbose ) Aig_ManPrintStats( pAig );
00265     }
00266     
00267     // refactor
00268     Dar_ManRefactor( pAig, pParsRef );
00269     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00270     Aig_ManStop( pTemp );
00271     if ( fVerbose ) Aig_ManPrintStats( pAig );
00272     
00273     // rewrite
00274     Dar_ManRewrite( pAig, pParsRwr );
00275     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00276     Aig_ManStop( pTemp );
00277     if ( fVerbose ) Aig_ManPrintStats( pAig );
00278 
00279     // balance
00280     if ( fBalance )
00281     {
00282     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00283     Aig_ManStop( pTemp );
00284     if ( fVerbose ) Aig_ManPrintStats( pAig );
00285     }
00286     return pAig;
00287 }
00288 
00300 Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
00301 //alias resyn    "b; rw; rwz; b; rwz; b"
00302 //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
00303 {
00304     Vec_Ptr_t * vAigs;
00305     vAigs = Vec_PtrAlloc( 3 );
00306     pAig = Aig_ManDup(pAig, 0);
00307     Vec_PtrPush( vAigs, pAig );
00308     pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
00309     Vec_PtrPush( vAigs, pAig );
00310     pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, fVerbose);
00311     Vec_PtrPush( vAigs, pAig );
00312     return vAigs;
00313 }
00314 
00326 /*
00327 Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
00328 {
00329     Vec_Ptr_t * vAigs;
00330     Aig_Man_t * pMan;
00331     vAigs = Vec_PtrAlloc( 3 );
00332     pMan = Ioa_ReadAiger( "i10_1.aig", 1 );
00333     Vec_PtrPush( vAigs, pMan );
00334     pMan = Ioa_ReadAiger( "i10_2.aig", 1 );
00335     Vec_PtrPush( vAigs, pMan );
00336     pMan = Ioa_ReadAiger( "i10_3.aig", 1 );
00337     Vec_PtrPush( vAigs, pMan );
00338     return vAigs;
00339 }
00340 */
00341 
00353 Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
00354 {
00355 /*
00356     Aig_Man_t * pMan, * pTemp;
00357     Vec_Ptr_t * vAigs;
00358     int i, clk;
00359 
00360 clk = clock();
00361 //    vAigs = Dar_ManChoiceSynthesisExt();
00362     vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, fVerbose );
00363 
00364     // swap the first and last network
00365     // this should lead to the primary choice being "better" because of synthesis
00366     pMan = Vec_PtrPop( vAigs );
00367     Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
00368     Vec_PtrWriteEntry( vAigs, 0, pMan );
00369 
00370 if ( fVerbose )
00371 {
00372 PRT( "Synthesis time", clock() - clk );
00373 }
00374 clk = clock();
00375     pMan = Aig_ManChoicePartitioned( vAigs, 300 );
00376     Vec_PtrForEachEntry( vAigs, pTemp, i )
00377         Aig_ManStop( pTemp );
00378     Vec_PtrFree( vAigs );
00379 if ( fVerbose )
00380 {
00381 PRT( "Choicing time ", clock() - clk );
00382 }
00383     return pMan;
00384 */
00385     return NULL;
00386 }
00387 
00391 
00392