abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
darScript.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [darScript.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware AIG rewriting.]
8 
9  Synopsis [Rewriting scripts.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "darInt.h"
22 #include "proof/dch/dch.h"
23 #include "aig/gia/gia.h"
24 #include "aig/gia/giaAig.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39  Synopsis [Performs one iteration of AIG rewriting.]
40 
41  Description []
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
48 Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
49 {
50  Aig_Man_t * pTemp;
51  Dar_RwrPar_t Pars, * pPars = &Pars;
52  Dar_ManDefaultRwrParams( pPars );
53  pAig = Aig_ManDupDfs( pAig );
54  Dar_ManRewrite( pAig, pPars );
55  pAig = Aig_ManDupDfs( pTemp = pAig );
56  Aig_ManStop( pTemp );
57  return pAig;
58 }
59 
60 /**Function*************************************************************
61 
62  Synopsis [Reproduces script "rwsat".]
63 
64  Description []
65 
66  SideEffects [This procedure does not tighten level during restructuring.]
67 
68  SeeAlso []
69 
70 ***********************************************************************/
71 Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
72 //alias rwsat "st; rw -l; b -l; rw -l; rf -l"
73 {
74  Aig_Man_t * pTemp;
75  abctime Time = pAig->Time2Quit;
76 
77  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
78  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
79 
80  Dar_ManDefaultRwrParams( pParsRwr );
81  Dar_ManDefaultRefParams( pParsRef );
82 
83  pParsRwr->fUpdateLevel = 0;
84  pParsRef->fUpdateLevel = 0;
85 
86  pParsRwr->fVerbose = fVerbose;
87  pParsRef->fVerbose = fVerbose;
88 //printf( "1" );
89  pAig = Aig_ManDupDfs( pAig );
90  if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
91 
92 //printf( "2" );
93  // balance
94  if ( fBalance )
95  {
96  pAig->Time2Quit = Time;
97  pAig = Dar_ManBalance( pTemp = pAig, 0 );
98  Aig_ManStop( pTemp );
99  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
100  if ( Time && Abc_Clock() > Time )
101  { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
102  }
103 
104 //Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
105 //printf( "3" );
106  // rewrite
107  pAig->Time2Quit = Time;
108  Dar_ManRewrite( pAig, pParsRwr );
109  pAig = Aig_ManDupDfs( pTemp = pAig );
110  Aig_ManStop( pTemp );
111  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
112  if ( Time && Abc_Clock() > Time )
113  { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
114 
115 //printf( "4" );
116  // refactor
117  pAig->Time2Quit = Time;
118  Dar_ManRefactor( pAig, pParsRef );
119  pAig = Aig_ManDupDfs( pTemp = pAig );
120  Aig_ManStop( pTemp );
121  if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
122  if ( Time && Abc_Clock() > Time )
123  { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
124 
125 //printf( "5" );
126  // balance
127  if ( fBalance )
128  {
129  pAig->Time2Quit = Time;
130  pAig = Dar_ManBalance( pTemp = pAig, 0 );
131  Aig_ManStop( pTemp );
132  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
133  if ( Time && Abc_Clock() > Time )
134  { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
135  }
136 
137 //printf( "6" );
138  // rewrite
139  pAig->Time2Quit = Time;
140  Dar_ManRewrite( pAig, pParsRwr );
141  pAig = Aig_ManDupDfs( pTemp = pAig );
142  Aig_ManStop( pTemp );
143  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
144  if ( Time && Abc_Clock() > Time )
145  { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
146 
147 //printf( "7" );
148  return pAig;
149 }
150 
151 /**Function*************************************************************
152 
153  Synopsis [Reproduces script "compress".]
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
163 //alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
164 {
165  Aig_Man_t * pTemp;
166 
167  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
168  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
169 
170  Dar_ManDefaultRwrParams( pParsRwr );
171  Dar_ManDefaultRefParams( pParsRef );
172 
173  pParsRwr->fUpdateLevel = fUpdateLevel;
174  pParsRef->fUpdateLevel = fUpdateLevel;
175 
176  pParsRwr->fPower = fPower;
177 
178  pParsRwr->fVerbose = 0;//fVerbose;
179  pParsRef->fVerbose = 0;//fVerbose;
180 
181  pAig = Aig_ManDupDfs( pAig );
182  if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
183 /*
184  // balance
185  if ( fBalance )
186  {
187  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
188  Aig_ManStop( pTemp );
189  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
190  }
191 */
192  // rewrite
193  Dar_ManRewrite( pAig, pParsRwr );
194  pAig = Aig_ManDupDfs( pTemp = pAig );
195  Aig_ManStop( pTemp );
196  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
197 
198  // refactor
199  Dar_ManRefactor( pAig, pParsRef );
200  pAig = Aig_ManDupDfs( pTemp = pAig );
201  Aig_ManStop( pTemp );
202  if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
203 
204  // balance
205  if ( fBalance )
206  {
207  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
208  Aig_ManStop( pTemp );
209  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
210  }
211 
212  pParsRwr->fUseZeros = 1;
213  pParsRef->fUseZeros = 1;
214 
215  // rewrite
216  Dar_ManRewrite( pAig, pParsRwr );
217  pAig = Aig_ManDupDfs( pTemp = pAig );
218  Aig_ManStop( pTemp );
219  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
220 
221  return pAig;
222 }
223 
224 /**Function*************************************************************
225 
226  Synopsis [Reproduces script "compress2".]
227 
228  Description []
229 
230  SideEffects []
231 
232  SeeAlso []
233 
234 ***********************************************************************/
235 Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
236 //alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
237 {
238  Aig_Man_t * pTemp;
239 
240  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
241  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
242 
243  Dar_ManDefaultRwrParams( pParsRwr );
244  Dar_ManDefaultRefParams( pParsRef );
245 
246  pParsRwr->fUpdateLevel = fUpdateLevel;
247  pParsRef->fUpdateLevel = fUpdateLevel;
248  pParsRwr->fFanout = fFanout;
249  pParsRwr->fPower = fPower;
250 
251  pParsRwr->fVerbose = 0;//fVerbose;
252  pParsRef->fVerbose = 0;//fVerbose;
253 
254  pAig = Aig_ManDupDfs( pAig );
255  if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
256 /*
257  // balance
258  if ( fBalance )
259  {
260  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
261  Aig_ManStop( pTemp );
262  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
263  }
264 */
265  // rewrite
266 // Dar_ManRewrite( pAig, pParsRwr );
267  pParsRwr->fUpdateLevel = 0; // disable level update
268  Dar_ManRewrite( pAig, pParsRwr );
269  pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
270 
271  pAig = Aig_ManDupDfs( pTemp = pAig );
272  Aig_ManStop( pTemp );
273  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
274 
275  // refactor
276  Dar_ManRefactor( pAig, pParsRef );
277  pAig = Aig_ManDupDfs( pTemp = pAig );
278  Aig_ManStop( pTemp );
279  if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
280 
281  // balance
282 // if ( fBalance )
283  {
284  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
285  Aig_ManStop( pTemp );
286  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
287  }
288 
289  // rewrite
290  Dar_ManRewrite( pAig, pParsRwr );
291  pAig = Aig_ManDupDfs( pTemp = pAig );
292  Aig_ManStop( pTemp );
293  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
294 
295  pParsRwr->fUseZeros = 1;
296  pParsRef->fUseZeros = 1;
297 
298  // rewrite
299  Dar_ManRewrite( pAig, pParsRwr );
300  pAig = Aig_ManDupDfs( pTemp = pAig );
301  Aig_ManStop( pTemp );
302  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
303 
304  // balance
305  if ( fBalance )
306  {
307  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
308  Aig_ManStop( pTemp );
309  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
310  }
311 
312  // refactor
313  Dar_ManRefactor( pAig, pParsRef );
314  pAig = Aig_ManDupDfs( pTemp = pAig );
315  Aig_ManStop( pTemp );
316  if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
317 
318  // rewrite
319  Dar_ManRewrite( pAig, pParsRwr );
320  pAig = Aig_ManDupDfs( pTemp = pAig );
321  Aig_ManStop( pTemp );
322  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
323 
324  // balance
325  if ( fBalance )
326  {
327  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
328  Aig_ManStop( pTemp );
329  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
330  }
331  return pAig;
332 }
333 
334 /**Function*************************************************************
335 
336  Synopsis [Reproduces script "compress2".]
337 
338  Description []
339 
340  SideEffects []
341 
342  SeeAlso []
343 
344 ***********************************************************************/
345 Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
346 //alias resyn "b; rw; rwz; b; rwz; b"
347 //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
348 {
349  Vec_Ptr_t * vAigs;
350 
351  vAigs = Vec_PtrAlloc( 3 );
352  pAig = Aig_ManDupDfs(pAig);
353  Vec_PtrPush( vAigs, pAig );
354 
355  pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
356  Vec_PtrPush( vAigs, pAig );
357 //Aig_ManPrintStats( pAig );
358 
359  pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
360  Vec_PtrPush( vAigs, pAig );
361 //Aig_ManPrintStats( pAig );
362 
363  pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
364  return vAigs;
365 }
366 
367 /**Function*************************************************************
368 
369  Synopsis [Reproduces script "compress2".]
370 
371  Description []
372 
373  SideEffects []
374 
375  SeeAlso []
376 
377 ***********************************************************************/
378 Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
379 {
380  Aig_Man_t * pMan, * pTemp;
381  Vec_Ptr_t * vAigs;
382  int i;
383  abctime clk;
384 
385 clk = Abc_Clock();
386 // vAigs = Dar_ManChoiceSynthesisExt();
387  vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, 0, fVerbose );
388 
389  // swap the first and last network
390  // this should lead to the primary choice being "better" because of synthesis
391  // (it is also important when constructing choices)
392  if ( !fConstruct )
393  {
394  pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
395  Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
396  Vec_PtrWriteEntry( vAigs, 0, pMan );
397  }
398 
399 if ( fVerbose )
400 {
401 ABC_PRT( "Synthesis time", Abc_Clock() - clk );
402 }
403 clk = Abc_Clock();
404  if ( fConstruct )
405  pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
406  else
407  pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
408  Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
409  Aig_ManStop( pTemp );
410  Vec_PtrFree( vAigs );
411 if ( fVerbose )
412 {
413 ABC_PRT( "Choicing time ", Abc_Clock() - clk );
414 }
415  return pMan;
416 // return NULL;
417 }
418 
419 
420 /**Function*************************************************************
421 
422  Synopsis [Reproduces script "compress".]
423 
424  Description []
425 
426  SideEffects []
427 
428  SeeAlso []
429 
430 ***********************************************************************/
431 Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
432 //alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
433 {
434  Aig_Man_t * pTemp;
435 
436  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
437  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
438 
439  Dar_ManDefaultRwrParams( pParsRwr );
440  Dar_ManDefaultRefParams( pParsRef );
441 
442  pParsRwr->fUpdateLevel = fUpdateLevel;
443  pParsRef->fUpdateLevel = fUpdateLevel;
444 
445  pParsRwr->fPower = fPower;
446 
447  pParsRwr->fVerbose = 0;//fVerbose;
448  pParsRef->fVerbose = 0;//fVerbose;
449 
450 // pAig = Aig_ManDupDfs( pAig );
451  if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
452 
453  // rewrite
454  Dar_ManRewrite( pAig, pParsRwr );
455  pAig = Aig_ManDupDfs( pTemp = pAig );
456  Aig_ManStop( pTemp );
457  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
458 
459  // refactor
460  Dar_ManRefactor( pAig, pParsRef );
461  pAig = Aig_ManDupDfs( pTemp = pAig );
462  Aig_ManStop( pTemp );
463  if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
464 
465  // balance
466  if ( fBalance )
467  {
468  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
469  Aig_ManStop( pTemp );
470  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
471  }
472 
473  pParsRwr->fUseZeros = 1;
474  pParsRef->fUseZeros = 1;
475 
476  // rewrite
477  Dar_ManRewrite( pAig, pParsRwr );
478  pAig = Aig_ManDupDfs( pTemp = pAig );
479  Aig_ManStop( pTemp );
480  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
481 
482  return pAig;
483 }
484 
485 /**Function*************************************************************
486 
487  Synopsis [Reproduces script "compress2".]
488 
489  Description []
490 
491  SideEffects []
492 
493  SeeAlso []
494 
495 ***********************************************************************/
496 Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose )
497 //alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
498 {
499  Aig_Man_t * pTemp;
500 
501  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
502  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
503 
504  Dar_ManDefaultRwrParams( pParsRwr );
505  Dar_ManDefaultRefParams( pParsRef );
506 
507  pParsRwr->fUpdateLevel = fUpdateLevel;
508  pParsRef->fUpdateLevel = fUpdateLevel;
509  pParsRwr->fFanout = fFanout;
510  pParsRwr->fPower = fPower;
511 
512  pParsRwr->fVerbose = 0;//fVerbose;
513  pParsRef->fVerbose = 0;//fVerbose;
514 
515 // pAig = Aig_ManDupDfs( pAig );
516  if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
517 
518  // skip if lighter synthesis is requested
519  if ( !fLightSynth )
520  {
521  // rewrite
522  //Dar_ManRewrite( pAig, pParsRwr );
523 // pParsRwr->fUpdateLevel = 0; // disable level update // this change was requested in July and later disabled
524  Dar_ManRewrite( pAig, pParsRwr );
525 // pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
526 
527  pAig = Aig_ManDupDfs( pTemp = pAig );
528  Aig_ManStop( pTemp );
529  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
530 
531  // refactor
532  Dar_ManRefactor( pAig, pParsRef );
533  pAig = Aig_ManDupDfs( pTemp = pAig );
534  Aig_ManStop( pTemp );
535  if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
536  }
537 
538  // balance
539  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
540  Aig_ManStop( pTemp );
541  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
542 
543  // skip if lighter synthesis is requested
544  if ( !fLightSynth )
545  {
546  // rewrite
547  Dar_ManRewrite( pAig, pParsRwr );
548  pAig = Aig_ManDupDfs( pTemp = pAig );
549  Aig_ManStop( pTemp );
550  if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
551  }
552 
553  pParsRwr->fUseZeros = 1;
554  pParsRef->fUseZeros = 1;
555 
556  // rewrite
557  Dar_ManRewrite( pAig, pParsRwr );
558  pAig = Aig_ManDupDfs( pTemp = pAig );
559  Aig_ManStop( pTemp );
560  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
561 
562  // skip if lighter synthesis is requested
563  if ( !fLightSynth )
564  {
565  // balance
566  if ( fBalance )
567  {
568  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
569  Aig_ManStop( pTemp );
570  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
571  }
572  }
573 
574  // refactor
575  Dar_ManRefactor( pAig, pParsRef );
576  pAig = Aig_ManDupDfs( pTemp = pAig );
577  Aig_ManStop( pTemp );
578  if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
579 
580  // skip if lighter synthesis is requested
581  if ( !fLightSynth )
582  {
583  // rewrite
584  Dar_ManRewrite( pAig, pParsRwr );
585  pAig = Aig_ManDupDfs( pTemp = pAig );
586  Aig_ManStop( pTemp );
587  if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
588  }
589 
590  // balance
591  if ( fBalance )
592  {
593  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
594  Aig_ManStop( pTemp );
595  if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
596  }
597  return pAig;
598 }
599 
600 /**Function*************************************************************
601 
602  Synopsis [Count the number of nodes with very high fanout count.]
603 
604  Description []
605 
606  SideEffects []
607 
608  SeeAlso []
609 
610 ***********************************************************************/
611 int Dar_NewChoiceSynthesisGuard( Aig_Man_t * pAig )
612 {
613  Aig_Obj_t * pObj;
614  int i, Count = 0;
615  Aig_ManForEachNode( pAig, pObj, i )
616  if ( Aig_ObjRefs(pObj) > 1000 )
617  Count += Aig_ObjRefs(pObj) / 1000;
618  return (int)(Count > 10);
619 }
620 
621 /**Function*************************************************************
622 
623  Synopsis [Reproduces script "compress2".]
624 
625  Description [Takes AIG manager, consumes it, and produces GIA manager.]
626 
627  SideEffects []
628 
629  SeeAlso []
630 
631 ***********************************************************************/
632 Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose )
633 //alias resyn "b; rw; rwz; b; rwz; b"
634 //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
635 {
636  Vec_Ptr_t * vGias;
637  Gia_Man_t * pGia, * pTemp;
638  int i;
639 
640  if ( fUpdateLevel && Dar_NewChoiceSynthesisGuard(pAig) )
641  {
642  if ( fVerbose )
643  printf( "Warning: Due to high fanout count of some nodes, level updating is disabled.\n" );
644  fUpdateLevel = 0;
645  }
646 
647  vGias = Vec_PtrAlloc( 3 );
648  pGia = Gia_ManFromAig(pAig);
649  Vec_PtrPush( vGias, pGia );
650 
651  pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
652  pGia = Gia_ManFromAig(pAig);
653  Vec_PtrPush( vGias, pGia );
654 //Aig_ManPrintStats( pAig );
655 
656  pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
657  pGia = Gia_ManFromAig(pAig);
658  Vec_PtrPush( vGias, pGia );
659 //Aig_ManPrintStats( pAig );
660 
661  Aig_ManStop( pAig );
662 
663  // swap around the first and the last
664  pTemp = (Gia_Man_t *)Vec_PtrPop( vGias );
665  Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
666  Vec_PtrWriteEntry( vGias, 0, pTemp );
667 
668 // Aig_Man_t * pAig;
669 // int i;
670 // printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
671 // Vec_PtrForEachEntry( Aig_Man_t *, p->vAigs, pAig, i )
672 // Aig_ManPrintStats( pAig );
673 
674  // derive the miter
675  pGia = Gia_ManChoiceMiter( vGias );
676 
677  // cleanup
678  Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
679  Gia_ManStop( pTemp );
680  Vec_PtrFree( vGias );
681  return pGia;
682 }
683 
684 /**Function*************************************************************
685 
686  Synopsis [Reproduces script "compress2".]
687 
688  Description []
689 
690  SideEffects []
691 
692  SeeAlso []
693 
694 ***********************************************************************/
695 /*
696 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
697 {
698  extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
699  extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
700 
701  int fVerbose = pPars->fVerbose;
702  int fConstruct = 0;
703  Aig_Man_t * pMan, * pTemp;
704  Vec_Ptr_t * vAigs;
705  int i;
706  abctime clk;
707 
708 clk = Abc_Clock();
709 // vAigs = Dar_ManChoiceSynthesisExt();
710 // vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
711  vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
712 
713  // swap the first and last network
714  // this should lead to the primary choice being "better" because of synthesis
715  // (it is also important when constructing choices)
716  if ( !fConstruct )
717  {
718  pMan = Vec_PtrPop( vAigs );
719  Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
720  Vec_PtrWriteEntry( vAigs, 0, pMan );
721  }
722 
723 if ( fVerbose )
724 {
725 //ABC_PRT( "Synthesis time", Abc_Clock() - clk );
726 }
727  pPars->timeSynth = Abc_Clock() - clk;
728 
729 clk = Abc_Clock();
730  // perform choice computation
731  if ( pPars->fUseGia )
732  pMan = Cec_ComputeChoices( vAigs, pPars );
733  else
734  pMan = Dch_ComputeChoices( vAigs, pPars );
735 
736  // reconstruct the network
737  pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
738  Aig_ManStop( pTemp );
739  // duplicate the timing manager
740  pTemp = Vec_PtrEntry( vAigs, 0 );
741  if ( pTemp->pManTime )
742  {
743  extern void * Tim_ManDup( void * p, int fDiscrete );
744  pMan->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
745  }
746  // reset levels
747  Aig_ManChoiceLevel( pMan );
748  ABC_FREE( pMan->pName );
749  ABC_FREE( pMan->pSpec );
750  pMan->pName = Abc_UtilStrsav( pTemp->pName );
751  pMan->pSpec = Abc_UtilStrsav( pTemp->pSpec );
752 
753  // cleanup
754  Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
755  Aig_ManStop( pTemp );
756  Vec_PtrFree( vAigs );
757 
758 if ( fVerbose )
759 {
760 //ABC_PRT( "Choicing time ", Abc_Clock() - clk );
761 }
762  return pMan;
763 // return NULL;
764 }
765 */
766 
767 /**Function*************************************************************
768 
769  Synopsis [Reproduces script "compress2".]
770 
771  Description [Consumes the input AIG to reduce memory usage.]
772 
773  SideEffects []
774 
775  SeeAlso []
776 
777 ***********************************************************************/
778 Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
779 {
780 // extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
781  extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
782  int fVerbose = pPars->fVerbose;
783  Aig_Man_t * pMan, * pTemp;
784  Vec_Ptr_t * vAigs;
785  Vec_Ptr_t * vPios;
786  void * pManTime;
787  char * pName, * pSpec;
788  int i;
789  abctime clk;
790 
791 clk = Abc_Clock();
792  vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
793 pPars->timeSynth = Abc_Clock() - clk;
794  // swap the first and last network
795  // this should lead to the primary choice being "better" because of synthesis
796  // (it is also important when constructing choices)
797  pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
798  Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
799  Vec_PtrWriteEntry( vAigs, 0, pMan );
800 
801  // derive the total AIG
802  pMan = Dch_DeriveTotalAig( vAigs );
803  // cleanup
804  Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
805  Aig_ManStop( pTemp );
806  Vec_PtrFree( vAigs );
807 
808  // compute choices
809  pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
810  Aig_ManStop( pTemp );
811 
812  // save useful things
813  pManTime = pAig->pManTime; pAig->pManTime = NULL;
814  pName = Abc_UtilStrsav( pAig->pName );
815  pSpec = Abc_UtilStrsav( pAig->pSpec );
816 
817  // create guidence
818  vPios = Aig_ManOrderPios( pMan, pAig );
819  Aig_ManStop( pAig );
820 
821  // reconstruct the network
822  pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
823  Aig_ManStop( pTemp );
824  Vec_PtrFree( vPios );
825 
826  // reset levels
827  pMan->pManTime = pManTime;
828  Aig_ManChoiceLevel( pMan );
829 
830  // copy names
831  ABC_FREE( pMan->pName );
832  ABC_FREE( pMan->pSpec );
833  pMan->pName = pName;
834  pMan->pSpec = pSpec;
835  return pMan;
836 }
837 
838 /**Function*************************************************************
839 
840  Synopsis [Reproduces script "compress2".]
841 
842  Description [Consumes the input AIG to reduce memory usage.]
843 
844  SideEffects []
845 
846  SeeAlso []
847 
848 ***********************************************************************/
849 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
850 {
851  extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
852 // extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
853  extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
854 // int fVerbose = pPars->fVerbose;
855  Aig_Man_t * pMan, * pTemp;
856  Gia_Man_t * pGia;
857  Vec_Ptr_t * vPios;
858  void * pManTime;
859  char * pName, * pSpec;
860  abctime clk;
861 
862  // save useful things
863  pManTime = pAig->pManTime; pAig->pManTime = NULL;
864  pName = Abc_UtilStrsav( pAig->pName );
865  pSpec = Abc_UtilStrsav( pAig->pSpec );
866 
867  // perform synthesis
868 clk = Abc_Clock();
869  pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
870 pPars->timeSynth = Abc_Clock() - clk;
871 
872  // perform choice computation
873  if ( pPars->fUseGia )
874  pMan = Cec_ComputeChoices( pGia, pPars );
875  else
876  {
877  pMan = Gia_ManToAigSkip( pGia, 3 );
878  Gia_ManStop( pGia );
879  pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
880  Aig_ManStop( pTemp );
881  }
882 
883  // create guidence
884  vPios = Aig_ManOrderPios( pMan, pAig );
885  Aig_ManStop( pAig );
886 
887  // reconstruct the network
888  pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
889  Aig_ManStop( pTemp );
890  Vec_PtrFree( vPios );
891 
892  // reset levels
893  pMan->pManTime = pManTime;
894  Aig_ManChoiceLevel( pMan );
895 
896  // copy names
897  ABC_FREE( pMan->pName );
898  ABC_FREE( pMan->pSpec );
899  pMan->pName = pName;
900  pMan->pSpec = pSpec;
901  return pMan;
902 }
903 
904 
905 ////////////////////////////////////////////////////////////////////////
906 /// END OF FILE ///
907 ////////////////////////////////////////////////////////////////////////
908 
909 
910 ABC_NAMESPACE_IMPL_END
911 
Dar_ManRewriteDefault
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRewriteDefault(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: darScript.c:48
Dar_ManChoiceNewAig
Aig_Man_t * Dar_ManChoiceNewAig(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: darScript.c:778
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Dar_ManChoiceNew
Aig_Man_t * Dar_ManChoiceNew(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: darScript.c:849
Dar_ManCompress2
Aig_Man_t * Dar_ManCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition: darScript.c:235
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Dar_NewCompress
Aig_Man_t * Dar_NewCompress(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition: darScript.c:431
Dar_RefPar_t_::fUpdateLevel
int fUpdateLevel
Definition: dar.h:64
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Dar_ManRewrite
int Dar_ManRewrite(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
Definition: darCore.c:78
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Dch_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition: dch.h:43
Aig_ManChoiceConstructive
Aig_Man_t * Aig_ManChoiceConstructive(Vec_Ptr_t *vAigs, int fVerbose)
Definition: aigPart.c:1564
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Dar_ManCompress
Aig_Man_t * Dar_ManCompress(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition: darScript.c:162
Vec_PtrPop
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
Dar_NewCompress2
Aig_Man_t * Dar_NewCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose)
Definition: darScript.c:496
Aig_ManChoiceLevel
int Aig_ManChoiceLevel(Aig_Man_t *p)
Definition: aigDfs.c:581
Gia_ManFromAig
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
Definition: giaAig.c:73
Dar_RefPar_t_::fVerbose
int fVerbose
Definition: dar.h:66
Aig_ManDupDfsGuided
Aig_Man_t * Aig_ManDupDfsGuided(Aig_Man_t *p, Vec_Ptr_t *vPios)
Definition: aigDup.c:694
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Dar_ManRefactor
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Definition: darRefact.c:496
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ManOrderPios
Vec_Ptr_t * Aig_ManOrderPios(Aig_Man_t *p, Aig_Man_t *pOrder)
Definition: aigDup.c:626
Dar_NewChoiceSynthesis
Gia_Man_t * Dar_NewChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
Definition: darScript.c:632
Aig_Obj_t_
Definition: aig.h:69
Dar_ManDefaultRefParams
void Dar_ManDefaultRefParams(Dar_RefPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: darRefact.c:85
Gia_Man_t_::pManTime
void * pManTime
Definition: gia.h:165
Dch_DeriveTotalAig
Aig_Man_t * Dch_DeriveTotalAig(Vec_Ptr_t *vAigs)
MACRO DEFINITIONS ///.
Definition: dchAig.c:65
Cec_ComputeChoices
Aig_Man_t * Cec_ComputeChoices(Gia_Man_t *pGia, Dch_Pars_t *pPars)
Definition: cecChoice.c:385
Gia_ManChoiceMiter
Gia_Man_t * Gia_ManChoiceMiter(Vec_Ptr_t *vGias)
Definition: giaDup.c:2574
Dar_NewChoiceSynthesisGuard
int Dar_NewChoiceSynthesisGuard(Aig_Man_t *pAig)
Definition: darScript.c:611
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Dar_RefPar_t_::fUseZeros
int fUseZeros
Definition: dar.h:65
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Dar_ManChoice
Aig_Man_t * Dar_ManChoice(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Definition: darScript.c:378
Dar_ManRwsat
Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition: darScript.c:71
Aig_ManChoicePartitioned
Aig_Man_t * Aig_ManChoicePartitioned(Vec_Ptr_t *vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose)
Definition: aigPart.c:1247
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ManToAigSkip
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
Definition: giaAig.c:324
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Dar_RwrPar_t
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition: dar.h:42
Dar_RefPar_t_
Definition: dar.h:58
Dar_ManChoiceSynthesis
Vec_Ptr_t * Dar_ManChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition: darScript.c:345
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Dch_ComputeChoices
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: dchCore.c:89
Dar_ManBalance
Aig_Man_t * Dar_ManBalance(Aig_Man_t *p, int fUpdateLevel)
Definition: darBalance.c:554
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Dar_ManDefaultRwrParams
void Dar_ManDefaultRwrParams(Dar_RwrPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: darCore.c:51
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223