1 /**CFile****************************************************************
2 
3   FileName    [abcRec2.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Network and node package.]
8 
9   Synopsis    [Record of semi-canonical AIG subgraphs.]
10 
11   Author      [Allan Yang, Alan Mishchenko]
12 
13   Affiliation [Fudan University in Shanghai, UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: abcRec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "map/if/if.h"
23 #include "bool/kit/kit.h"
24 #include "aig/gia/giaAig.h"
25 #include "misc/vec/vecMem.h"
26 #include "opt/dau/dau.h"
27 #include "misc/util/utilTruth.h"
28 
29 ABC_NAMESPACE_IMPL_START
30 
31 #define LMS_VAR_MAX    16  // LMS_VAR_MAX >= 6
32 #define LMS_MAX_WORD  (1<<(LMS_VAR_MAX-6))
33 //#define LMS_USE_OLD_FORM
34 
35 ////////////////////////////////////////////////////////////////////////
36 ///                        DECLARATIONS                              ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 /*
40     This LMS manager can be used in two modes:
41         - library constuction
42         - AIG level minimization
43     To switch from library construction to AIG level minimization
44     LSM manager should be restarted by dumping GIA (rec_dump3 <file>.aig)
45     and starting LMS manager again (rec_start3 <file>.aig).
46 */
47 
48 typedef struct Lms_Man_t_ Lms_Man_t;
49 struct Lms_Man_t_
50 {
51     // parameters
52     int               nVars;        // the number of variables
53     int               nWords;       // the number of TT words
54     int               nCuts;        // the max number of cuts to use
55     int               fFuncOnly;    // record only functions
56     int               fLibConstr;   // this manager is used for library construction
57     // internal data for library construction
58     Gia_Man_t *       pGia;         // the record
59     Vec_Mem_t *       vTtMem;       // truth table memory and hash table
60 //    Vec_Mem_t *       vTtMem2;      // truth table memory and hash table
61     Vec_Int_t *       vTruthIds;    // truth table IDs of each PO
62     // internal data for AIG level minimization (allocated the first time it is called)
63     Vec_Int_t *       vTruthPo;     // first PO where this canonicized truth table was seen
64     Vec_Wrd_t *       vDelays;      // pin-to-pin delays of each PO
65     Vec_Str_t *       vAreas;       // number of AND gates in each PO
66     Vec_Int_t *       vFreqs;       // subgraph usage frequencies
67     Vec_Int_t *       vTruthFreqs;  // truth table usage frequencies
68     // temporaries
69     Vec_Ptr_t *       vNodes;       // the temporary nodes
70     Vec_Ptr_t *       vLabelsP;     // temporary storage for HOP node labels
71     Vec_Int_t *       vLabels;      // temporary storage for AIG node labels
72     Vec_Str_t *       vSupps;       // used temporarily by TT dumping
73     word              pTemp1[LMS_MAX_WORD]; // copy of the truth table
74     word              pTemp2[LMS_MAX_WORD]; // copy of the truth table
75     // statistics
76     int               nTried;
77     int               nFilterSize;
78     int               nFilterRedund;
79     int               nFilterVolume;
80     int               nFilterTruth;
81     int               nFilterError;
82     int               nFilterSame;
83     int               nAdded;
84     int               nAddedFuncs;
85     int               nHoleInTheWall;
86     // runtime
87     abctime           timeTruth;
88     abctime           timeCanon;
89     abctime           timeBuild;
90     abctime           timeCheck;
91     abctime           timeInsert;
92     abctime           timeOther;
93     abctime           timeTotal;
94 };
95 
96 static Lms_Man_t * s_pMan3 = NULL;
97 
98 ////////////////////////////////////////////////////////////////////////
99 ///                     FUNCTION DEFINITIONS                         ///
100 ////////////////////////////////////////////////////////////////////////
101 
102 /**Function*************************************************************
103 
104   Synopsis    [Compute delay/area profiles of POs.]
105 
106   Description []
107 
108   SideEffects []
109 
110   SeeAlso     []
111 
112 ***********************************************************************/
Lms_DelayGet(word D,int v)113 static inline int  Lms_DelayGet( word D, int v )           { assert(v >= 0 && v < LMS_VAR_MAX); return (int)((D >> (v << 2)) & 0xF);                             }
Lms_DelaySet(word * pD,int v,int d)114 static inline void Lms_DelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < LMS_VAR_MAX); assert(d >= 0 && d < LMS_VAR_MAX); *pD |= ((word)d << (v << 2)); }
Lms_DelayInit(int v)115 static inline word Lms_DelayInit( int v )                  { assert(v >= 0 && v < LMS_VAR_MAX); return (word)1 << (v << 2);                                      }
Lms_DelayMax(word D1,word D2,int nVars)116 static inline word Lms_DelayMax( word D1, word D2, int nVars )
117 {
118     int v, Max;
119     word D = 0;
120     for ( v = 0; v < nVars; v++ )
121         if ( (Max = Abc_MaxInt(Lms_DelayGet(D1, v), Lms_DelayGet(D2, v))) )
122             Lms_DelaySet( &D, v, Abc_MinInt(Max + 1, 15) );
123     return D;
124 }
Lms_DelayDecrement(word D1,int nVars)125 static inline word Lms_DelayDecrement( word D1, int nVars )
126 {
127     int v;
128     word D = 0;
129     for ( v = 0; v < nVars; v++ )
130         if ( Lms_DelayGet(D1, v) )
131             Lms_DelaySet( &D, v, Lms_DelayGet(D1, v) - 1 );
132     return D;
133 }
Lms_DelayEqual(word D1,word D2,int nVars)134 static inline int Lms_DelayEqual( word D1, word D2, int nVars ) // returns 1 if D1 has the same delays than D2
135 {
136     int v;
137     for ( v = 0; v < nVars; v++ )
138         if ( Lms_DelayGet(D1, v) != Lms_DelayGet(D2, v) )
139             return 0;
140     return 1;
141 }
Lms_DelayDom(word D1,word D2,int nVars)142 static inline int Lms_DelayDom( word D1, word D2, int nVars ) // returns 1 if D1 has the same or smaller delays than D2
143 {
144     int v;
145     for ( v = 0; v < nVars; v++ )
146         if ( Lms_DelayGet(D1, v) > Lms_DelayGet(D2, v) )
147             return 0;
148     return 1;
149 }
Lms_DelayPrint(word D,int nVars)150 static inline void Lms_DelayPrint( word D, int nVars )
151 {
152     int v;
153     printf( "Delay profile = {" );
154     for ( v = 0; v < nVars; v++ )
155         printf( " %d", Lms_DelayGet(D, v) );
156     printf( " }\n" );
157 }
Lms_GiaDelays(Gia_Man_t * p)158 Vec_Wrd_t * Lms_GiaDelays( Gia_Man_t * p )
159 {
160     Vec_Wrd_t * vDelays, * vResult;
161     Gia_Obj_t * pObj;
162     int i;
163     // compute delay profiles of all objects
164     vDelays = Vec_WrdAlloc( Gia_ManObjNum(p) );
165     Vec_WrdPush( vDelays, 0 ); // const 0
166     Gia_ManForEachObj1( p, pObj, i )
167     {
168         if ( Gia_ObjIsAnd(pObj) )
169             Vec_WrdPush( vDelays, Lms_DelayMax( Vec_WrdEntry(vDelays, Gia_ObjFaninId0(pObj, i)), Vec_WrdEntry(vDelays, Gia_ObjFaninId1(pObj, i)), Gia_ManCiNum(p) ) );
170         else if ( Gia_ObjIsCo(pObj) )
171             Vec_WrdPush( vDelays, Lms_DelayDecrement( Vec_WrdEntry(vDelays, Gia_ObjFaninId0(pObj, i)), Gia_ManCiNum(p) ) );
172         else if ( Gia_ObjIsCi(pObj) )
173             Vec_WrdPush( vDelays, Lms_DelayInit( Gia_ObjCioId(pObj) ) );
174         else assert( 0 );
175     }
176     // collect delay profiles of COs only
177     vResult = Vec_WrdAlloc( Gia_ManCoNum(p) );
178     Gia_ManForEachCo( p, pObj, i )
179         Vec_WrdPush( vResult, Vec_WrdEntry(vDelays, Gia_ObjId(p, pObj)) );
180     Vec_WrdFree( vDelays );
181     return vResult;
182 }
Lms_ObjAreaMark_rec(Gia_Obj_t * pObj)183 void Lms_ObjAreaMark_rec( Gia_Obj_t * pObj )
184 {
185     if ( pObj->fMark0 || Gia_ObjIsCi(pObj) )
186         return;
187     pObj->fMark0 = 1;
188     Lms_ObjAreaMark_rec( Gia_ObjFanin0(pObj) );
189     Lms_ObjAreaMark_rec( Gia_ObjFanin1(pObj) );
190 }
Lms_ObjAreaUnmark_rec(Gia_Obj_t * pObj)191 int  Lms_ObjAreaUnmark_rec( Gia_Obj_t * pObj )
192 {
193     if ( !pObj->fMark0 || Gia_ObjIsCi(pObj) )
194         return 0;
195     pObj->fMark0 = 0;
196     return 1 + Lms_ObjAreaUnmark_rec( Gia_ObjFanin0(pObj) )
197              + Lms_ObjAreaUnmark_rec( Gia_ObjFanin1(pObj) );
198 }
Lms_ObjArea(Gia_Obj_t * pObj)199 int Lms_ObjArea( Gia_Obj_t * pObj )
200 {
201     assert( Gia_ObjIsAnd(pObj) );
202     Lms_ObjAreaMark_rec( pObj );
203     return Lms_ObjAreaUnmark_rec( pObj );
204 }
Lms_GiaAreas(Gia_Man_t * p)205 Vec_Str_t * Lms_GiaAreas( Gia_Man_t * p )
206 {
207     Vec_Str_t * vAreas;
208     Gia_Obj_t * pObj;
209     int i;
210     vAreas = Vec_StrAlloc( Gia_ManCoNum(p) );
211     Gia_ManForEachCo( p, pObj, i )
212         Vec_StrPush( vAreas, (char)(Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) ? Lms_ObjArea(Gia_ObjFanin0(pObj)) : 0) );
213     return vAreas;
214 }
Lms_GiaSuppSizes(Gia_Man_t * p)215 Vec_Str_t * Lms_GiaSuppSizes( Gia_Man_t * p )
216 {
217     Vec_Str_t * vResult;
218     Vec_Str_t * vSupps;
219     Gia_Obj_t * pObj;
220     int i;
221     vSupps = Vec_StrAlloc( Gia_ManObjNum(p) );
222     Vec_StrPush( vSupps, 0 );
223     Gia_ManForEachObj1( p, pObj, i )
224     {
225         if ( Gia_ObjIsAnd(pObj) )
226             Vec_StrPush( vSupps, (char)Abc_MaxInt( Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)), Vec_StrEntry(vSupps, Gia_ObjFaninId1(pObj, i)) ) );
227         else if ( Gia_ObjIsCo(pObj) )
228             Vec_StrPush( vSupps, Vec_StrEntry(vSupps, Gia_ObjFaninId0(pObj, i)) );
229         else if ( Gia_ObjIsCi(pObj) )
230             Vec_StrPush( vSupps, (char)(Gia_ObjCioId(pObj)+1) );
231         else assert( 0 );
232     }
233     assert( Vec_StrSize(vSupps) == Gia_ManObjNum(p) );
234     vResult = Vec_StrAlloc( Gia_ManCoNum(p) );
235     Gia_ManForEachCo( p, pObj, i )
236         Vec_StrPush( vResult, Vec_StrEntry(vSupps, Gia_ObjId(p, pObj)) );
237     Vec_StrFree( vSupps );
238     return vResult;
239 }
Lms_GiaProfilesPrint(Gia_Man_t * p)240 void Lms_GiaProfilesPrint( Gia_Man_t * p )
241 {
242     Gia_Obj_t * pObj;
243     int i;
244     Vec_Wrd_t * vDelays;
245     Vec_Str_t * vAreas;
246     vDelays = Lms_GiaDelays( p );
247     vAreas = Lms_GiaAreas( p );
248     Gia_ManForEachPo( p, pObj, i )
249     {
250         printf( "%6d : ", i );
251         printf( "A = %2d  ", Vec_StrEntry(vAreas, i) );
252         Lms_DelayPrint( Vec_WrdEntry(vDelays, i), Gia_ManPiNum(p) );
253 //        Lms_GiaPrintSubgraph( p, pObj );
254 //        printf( "\n" );
255     }
256     Vec_WrdFree( vDelays );
257     Vec_StrFree( vAreas );
258 }
259 
260 /**Function*************************************************************
261 
262   Synopsis    [Prints one GIA subgraph.]
263 
264   Description []
265 
266   SideEffects []
267 
268   SeeAlso     []
269 
270 ***********************************************************************/
Lms_GiaPrintSubgraph_rec(Gia_Man_t * p,Gia_Obj_t * pObj)271 void Lms_GiaPrintSubgraph_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
272 {
273     if ( !pObj->fMark0 || Gia_ObjIsCi(pObj) )
274         return;
275     pObj->fMark0 = 0;
276     assert( Gia_ObjIsAnd(pObj) );
277     Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin0(pObj) );
278     Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin1(pObj) );
279     Gia_ObjPrint( p, pObj );
280 }
Lms_GiaPrintSubgraph(Gia_Man_t * p,Gia_Obj_t * pObj)281 void Lms_GiaPrintSubgraph( Gia_Man_t * p, Gia_Obj_t * pObj )
282 {
283     assert( Gia_ObjIsCo(pObj) );
284     if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
285     {
286         Lms_ObjAreaMark_rec( Gia_ObjFanin0(pObj) );
287         Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin0(pObj) );
288     }
289     else
290         Gia_ObjPrint( p, Gia_ObjFanin0(pObj) );
291     Gia_ObjPrint( p, pObj );
292 }
293 
294 /**Function*************************************************************
295 
296   Synopsis    []
297 
298   Description []
299 
300   SideEffects []
301 
302   SeeAlso     []
303 
304 ***********************************************************************/
Lms_ManStart(Gia_Man_t * pGia,int nVars,int nCuts,int fFuncOnly,int fVerbose)305 Lms_Man_t * Lms_ManStart( Gia_Man_t * pGia, int nVars, int nCuts, int fFuncOnly, int fVerbose )
306 {
307     Lms_Man_t * p;
308     abctime clk, clk2 = Abc_Clock();
309     // if GIA is given, use the number of variables from GIA
310     nVars = pGia ? Gia_ManCiNum(pGia) : nVars;
311     assert( nVars >= 6 && nVars <= LMS_VAR_MAX );
312     // allocate manager
313     p = ABC_CALLOC( Lms_Man_t, 1 );
314     // parameters
315     p->nVars = nVars;
316     p->nCuts = nCuts;
317     p->nWords = Abc_Truth6WordNum( nVars );
318     p->fFuncOnly = fFuncOnly;
319     // internal data for library construction
320     p->vTtMem = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
321 //    p->vTtMem2 = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
322     Vec_MemHashAlloc( p->vTtMem, 10000 );
323 //    Vec_MemHashAlloc( p->vTtMem2, 10000 );
324     if ( fFuncOnly )
325         return p;
326     p->vTruthIds = Vec_IntAlloc( 10000 );
327     if ( pGia == NULL )
328     {
329         int i;
330         p->pGia = Gia_ManStart( 10000 );
331         p->pGia->pName = Abc_UtilStrsav( "record" );
332         for ( i = 0; i < nVars; i++ )
333             Gia_ManAppendCi( p->pGia );
334     }
335     else
336     {
337         Gia_Obj_t * pObj;
338         word * pTruth;
339         int i, Index, Prev = -1;
340         p->pGia = pGia;
341         // populate the manager with subgraphs present in GIA
342         p->nAdded = Gia_ManCoNum( p->pGia );
343         Gia_ManForEachCo( p->pGia, pObj, i )
344         {
345             clk = Abc_Clock();
346             pTruth = Gia_ObjComputeTruthTable( p->pGia, pObj );
347             p->timeTruth += Abc_Clock() - clk;
348             clk = Abc_Clock();
349             Index = Vec_MemHashInsert( p->vTtMem, pTruth );
350             p->timeInsert += Abc_Clock() - clk;
351             assert( Index == Prev || Index == Prev + 1 ); // GIA subgraphs should be ordered
352             Vec_IntPush( p->vTruthIds, Index );
353             Prev = Index;
354         }
355     }
356     // temporaries
357     p->vNodes    = Vec_PtrAlloc( 1000 );
358     p->vLabelsP  = Vec_PtrAlloc( 1000 );
359     p->vLabels   = Vec_IntAlloc( 1000 );
360 p->timeTotal += Abc_Clock() - clk2;
361     return p;
362 }
Lms_ManStop(Lms_Man_t * p)363 void Lms_ManStop( Lms_Man_t * p )
364 {
365     // temporaries
366     Vec_IntFreeP( &p->vLabels );
367     Vec_PtrFreeP( &p->vLabelsP );
368     Vec_PtrFreeP( &p->vNodes );
369     // internal data for AIG level minimization
370     Vec_IntFreeP( &p->vTruthPo );
371     Vec_WrdFreeP( &p->vDelays );
372     Vec_StrFreeP( &p->vAreas );
373     Vec_IntFreeP( &p->vFreqs );
374     Vec_IntFreeP( &p->vTruthFreqs );
375     // internal data for library construction
376     Vec_IntFreeP( &p->vTruthIds );
377     Vec_MemHashFree( p->vTtMem );
378 //    Vec_MemHashFree( p->vTtMem2 );
379     Vec_MemFree( p->vTtMem );
380 //    Vec_MemFree( p->vTtMem2 );
381     Gia_ManStopP( &p->pGia );
382     ABC_FREE( p );
383 }
Lms_ManPrepare(Lms_Man_t * p)384 void Lms_ManPrepare( Lms_Man_t * p )
385 {
386     // compute the first PO for each semi-canonical form
387     int i, Entry;
388     assert( !p->fLibConstr );
389     assert( p->vTruthPo == NULL );
390     p->vTruthPo = Vec_IntStartFull( Vec_MemEntryNum(p->vTtMem)+1 );
391     assert( Vec_IntFindMin(p->vTruthIds) >= 0 );
392     assert( Vec_IntFindMax(p->vTruthIds) < Vec_MemEntryNum(p->vTtMem) );
393     Vec_IntForEachEntry( p->vTruthIds, Entry, i )
394         if ( Vec_IntEntry(p->vTruthPo, Entry) == -1 )
395             Vec_IntWriteEntry( p->vTruthPo, Entry, i );
396     Vec_IntWriteEntry( p->vTruthPo, Vec_MemEntryNum(p->vTtMem), Gia_ManCoNum(p->pGia) );
397     // compute delay/area and init frequency
398     assert( p->vDelays == NULL );
399     assert( p->vAreas == NULL );
400     assert( p->vFreqs == NULL );
401     p->vDelays = Lms_GiaDelays( p->pGia );
402     p->vAreas  = Lms_GiaAreas( p->pGia );
403     p->vFreqs  = Vec_IntStart( Gia_ManCoNum(p->pGia) );
404 }
Lms_ManPrintFuncStats(Lms_Man_t * p)405 void Lms_ManPrintFuncStats( Lms_Man_t * p )
406 {
407     Vec_Str_t * vSupps;
408     int Counters[LMS_VAR_MAX+1] = {0}, CountersS[LMS_VAR_MAX+1] = {0};
409     int i, Entry, Next;
410     if ( p->pGia == NULL )
411         return;
412     if ( p->fLibConstr )
413         return;
414     if ( p->vTruthPo == NULL )
415         Lms_ManPrepare( p );
416     vSupps = Lms_GiaSuppSizes( p->pGia );
417     Vec_IntForEachEntry( p->vTruthPo, Entry, i )
418     {
419         if ( i == Vec_IntSize(p->vTruthPo) - 1 )
420             break;
421         Next = Vec_IntEntry( p->vTruthPo, i+1 );
422         Counters[(int)Vec_StrEntry(vSupps, Entry)]++;
423         CountersS[(int)Vec_StrEntry(vSupps, Entry)] += Next - Entry;
424     }
425     for ( i = 0; i <= LMS_VAR_MAX; i++ )
426         if ( Counters[i] )
427             printf( "Inputs = %2d.  Funcs = %8d.  Subgrs = %8d.  Ratio = %6.2f.\n", i, Counters[i], CountersS[i], 1.0*CountersS[i]/Counters[i] );
428     Vec_StrFree( vSupps );
429 }
Lms_ManPrintFreqStats(Lms_Man_t * p)430 void Lms_ManPrintFreqStats( Lms_Man_t * p )
431 {
432     int CountDsdNpn[3]  = {0};  // full/part/none
433     int CountDsdAll[3]  = {0};  // full/part/none
434     int CountStepNpn[3] = {0};  // full/1step/complex
435     int CountStepAll[3] = {0};  // full/1step/complex
436     char pBuffer[1000];
437     int nSuppSize;
438     int nNonDecSize;
439     word * pTruth;
440     int i, Freq, Status;
441     printf( "Cuts  = %10d. ",            p->nTried );
442 //    printf( "Funcs = %10d (%6.2f %%). ", Vec_MemEntryNum(p->vTtMem2), 100.0*Vec_MemEntryNum(p->vTtMem2)/p->nTried );
443     printf( "Class = %10d (%6.2f %%). ", Vec_MemEntryNum(p->vTtMem),  100.0*Vec_MemEntryNum(p->vTtMem)/p->nTried );
444     printf( "\n" );
445 //    return;
446 
447     Vec_IntForEachEntry( p->vTruthFreqs, Freq, i )
448     {
449         pTruth = Vec_MemReadEntry(p->vTtMem, i);
450 /*
451         printf( "%6d -- %6d : ", i, Freq );
452         Kit_DsdWriteFromTruth( pBuffer, (unsigned *)pTruth, p->nVars );
453         printf( "%s\n", pBuffer );
454 */
455         nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
456         nNonDecSize = Dau_DsdDecompose( pTruth, p->nVars, 0, 0, pBuffer );
457         if ( nNonDecSize == 0 )
458         {
459             CountDsdNpn[0]++;
460             CountDsdAll[0] += Freq;
461         }
462         else if ( nNonDecSize < nSuppSize )
463         {
464             CountDsdNpn[1]++;
465             CountDsdAll[1] += Freq;
466         }
467         else // non-dec
468         {
469             CountDsdNpn[2]++;
470             CountDsdAll[2] += Freq;
471         }
472 
473         if ( nNonDecSize == 0 )
474         {
475             CountStepNpn[0]++;
476             CountStepAll[0] += Freq;
477             continue;
478         }
479 
480         // check the non dec core
481         Status = Dau_DsdCheck1Step( NULL, pTruth, nNonDecSize, NULL );
482         if ( Status >= 0 )
483         {
484             CountStepNpn[1]++;
485             CountStepAll[1] += Freq;
486         }
487         else
488         {
489             assert( Status == -2 );
490             CountStepNpn[2]++;
491             CountStepAll[2] += Freq;
492         }
493     }
494 
495     // print the results
496     printf( "NPN: " );
497     printf( "Full = %6.2f %%  ", 100.0 * CountDsdNpn[0] / Vec_MemEntryNum(p->vTtMem) );
498     printf( "Part = %6.2f %%  ", 100.0 * CountDsdNpn[1] / Vec_MemEntryNum(p->vTtMem) );
499     printf( "None = %6.2f %%  ", 100.0 * CountDsdNpn[2] / Vec_MemEntryNum(p->vTtMem) );
500 //    printf( "\n" );
501     printf( "   " );
502     // print the results
503     printf( "All: " );
504     printf( "Full = %6.2f %%  ", 100.0 * CountDsdAll[0] / p->nTried );
505     printf( "Part = %6.2f %%  ", 100.0 * CountDsdAll[1] / p->nTried );
506     printf( "None = %6.2f %%  ", 100.0 * CountDsdAll[2] / p->nTried );
507     printf( "\n" );
508 
509     // print the results
510     printf( "NPN: " );
511     printf( "Full = %6.2f %%  ", 100.0 * CountStepNpn[0] / Vec_MemEntryNum(p->vTtMem) );
512     printf( "1stp = %6.2f %%  ", 100.0 * CountStepNpn[1] / Vec_MemEntryNum(p->vTtMem) );
513     printf( "Comp = %6.2f %%  ", 100.0 * CountStepNpn[2] / Vec_MemEntryNum(p->vTtMem) );
514 //    printf( "\n" );
515     printf( "   " );
516     // print the results
517     printf( "All: " );
518     printf( "Full = %6.2f %%  ", 100.0 * CountStepAll[0] / p->nTried );
519     printf( "1stp = %6.2f %%  ", 100.0 * CountStepAll[1] / p->nTried );
520     printf( "Comp = %6.2f %%  ", 100.0 * CountStepAll[2] / p->nTried );
521     printf( "\n" );
522 
523 }
Lms_ManPrint(Lms_Man_t * p)524 void Lms_ManPrint( Lms_Man_t * p )
525 {
526 //    Gia_ManPrintStats( p->pGia, 0, 0 );
527     printf( "Library with %d vars has %d classes and %d AIG subgraphs with %d AND nodes.\n",
528         p->nVars, Vec_MemEntryNum(p->vTtMem), p->nAdded, p->pGia ? Gia_ManAndNum(p->pGia) : 0 );
529 
530 //    Lms_ManPrintFreqStats( p );
531     Lms_ManPrintFuncStats( p );
532 
533     p->nAddedFuncs = Vec_MemEntryNum(p->vTtMem);
534     printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,         !p->nTried? 0 : 100.0*p->nTried/p->nTried );
535     printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,    !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
536     printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund,  !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
537     printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume,  !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
538     printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,   !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
539     printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,   !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
540     printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,    !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
541     printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,         !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
542     printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,    !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
543     if ( p->nHoleInTheWall )
544     printf( "Cuts whose logic structure has a hole       = %10d. (%6.2f %%)\n", p->nHoleInTheWall, !p->nTried? 0 : 100.0*p->nHoleInTheWall/p->nTried );
545 
546     p->timeOther = p->timeTotal - p->timeTruth - p->timeCanon - p->timeBuild - p->timeCheck - p->timeInsert;
547     ABC_PRTP( "Runtime: Truth ", p->timeTruth,  p->timeTotal );
548     ABC_PRTP( "Runtime: Canon ", p->timeCanon,  p->timeTotal );
549     ABC_PRTP( "Runtime: Build ", p->timeBuild,  p->timeTotal );
550     ABC_PRTP( "Runtime: Check ", p->timeCheck,  p->timeTotal );
551     ABC_PRTP( "Runtime: Insert", p->timeInsert, p->timeTotal );
552     ABC_PRTP( "Runtime: Other ", p->timeOther,  p->timeTotal );
553     ABC_PRTP( "Runtime: TOTAL ", p->timeTotal,  p->timeTotal );
554 }
555 
556 /**Function*************************************************************
557 
558   Synopsis    [Recanonicizes the library and add it to the current library.]
559 
560   Description []
561 
562   SideEffects []
563 
564   SeeAlso     []
565 
566 ***********************************************************************/
Abc_NtkRecLibMerge3(Gia_Man_t * pLib)567 void Abc_NtkRecLibMerge3( Gia_Man_t * pLib )
568 {
569     int fCheck = 0;
570     Lms_Man_t * p = s_pMan3;
571     Gia_Man_t * pGia = p->pGia;
572     Vec_Str_t * vSupps;
573     char pCanonPerm[LMS_VAR_MAX];
574     unsigned uCanonPhase;
575     word * pTruth;
576     int i, k, Index, iFanin0, iFanin1, nLeaves;
577     Gia_Obj_t * pObjPo, * pDriver, * pTemp = NULL;
578     abctime clk, clk2 = Abc_Clock();
579 
580     if ( Gia_ManCiNum(pLib) != Gia_ManCiNum(pGia) )
581     {
582         printf( "The number of Library inputs (%d) differs from the number of Gia inputs (%d).\n", Gia_ManCiNum(pLib), Gia_ManCiNum(pGia) );
583         return;
584     }
585     assert( Gia_ManCiNum(pLib) == Gia_ManCiNum(pGia) );
586 
587     // create hash table if not available
588     if ( Vec_IntSize(&pGia->vHTable) == 0 )
589         Gia_ManHashStart( pGia );
590 
591     // add AIG subgraphs
592     vSupps = Lms_GiaSuppSizes( pLib );
593     Gia_ManForEachCo( pLib, pObjPo, k )
594     {
595         // get support size
596         nLeaves = Vec_StrEntry(vSupps, k);
597         assert( nLeaves > 1 );
598 
599         // compute the truth table
600 clk = Abc_Clock();
601         pTruth = Gia_ObjComputeTruthTable( pLib, Gia_ObjFanin0(pObjPo) );
602 p->timeTruth += Abc_Clock() - clk;
603         // semi-canonicize
604 clk = Abc_Clock();
605         memcpy( p->pTemp1, pTruth, p->nWords * sizeof(word) );
606 #ifdef LMS_USE_OLD_FORM
607         uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
608 #else
609         uCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
610 #endif
611         Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
612 p->timeCanon += Abc_Clock() - clk;
613         // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
614         if ( nLeaves == 2 && Abc_TtSupportSize(pTruth, 2) != 2 )
615             continue;
616 
617 clk = Abc_Clock();
618         // map cut leaves into elementary variables of GIA
619         for ( i = 0; i < nLeaves; i++ )
620             Gia_ManCi( pLib, pCanonPerm[i] )->Value = Abc_Var2Lit( Gia_ObjId(pGia, Gia_ManPi(pGia, i)), (uCanonPhase >> i) & 1 );
621         // build internal nodes
622         assert( Vec_IntSize(pLib->vTtNodes) > 0 );
623         Gia_ManForEachObjVec( pLib->vTtNodes, pLib, pTemp, i )
624         {
625             iFanin0 = Abc_LitNotCond( Gia_ObjFanin0(pTemp)->Value, Gia_ObjFaninC0(pTemp) );
626             iFanin1 = Abc_LitNotCond( Gia_ObjFanin1(pTemp)->Value, Gia_ObjFaninC1(pTemp) );
627             pTemp->Value = Gia_ManHashAnd( pGia, iFanin0, iFanin1 );
628         }
629 p->timeBuild += Abc_Clock() - clk;
630 
631         // check if this node is already driving a PO
632         assert( Gia_ObjIsAnd(pTemp) );
633         pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pTemp->Value));
634         if ( pDriver->fMark1 )
635         {
636             p->nFilterSame++;
637             continue;
638         }
639         pDriver->fMark1 = 1;
640         // create output
641         Gia_ManAppendCo( pGia, Abc_LitNotCond( pTemp->Value, (uCanonPhase >> nLeaves) & 1 ) );
642 
643         // verify truth table
644         if ( fCheck )
645         {
646 clk = Abc_Clock();
647         pTemp = Gia_ManCo(pGia, Gia_ManCoNum(pGia)-1);
648         pTruth = Gia_ObjComputeTruthTable( pGia, Gia_ManCo(pGia, Gia_ManCoNum(pGia)-1) );
649 p->timeCheck += Abc_Clock() - clk;
650         if ( memcmp( p->pTemp1, pTruth, p->nWords * sizeof(word) ) != 0 )
651         {
652 
653             Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
654             Kit_DsdPrintFromTruth( (unsigned *)p->pTemp1, nLeaves ); printf( "\n" );
655             printf( "Truth table verification has failed.\n" );
656 
657             // drive PO with constant
658             Gia_ManPatchCoDriver( pGia, Gia_ManCoNum(pGia)-1, 0 );
659             // save truth table ID
660             Vec_IntPush( p->vTruthIds, -1 );
661             p->nFilterTruth++;
662             continue;
663         }
664         }
665 
666 clk = Abc_Clock();
667         // add the resulting truth table to the hash table
668         Index = Vec_MemHashInsert( p->vTtMem, p->pTemp1 );
669         // save truth table ID
670         Vec_IntPush( p->vTruthIds, Index );
671         assert( Gia_ManCoNum(pGia) == Vec_IntSize(p->vTruthIds) );
672         p->nAdded++;
673 p->timeInsert += Abc_Clock() - clk;
674     }
675     Vec_StrFree( vSupps );
676 p->timeTotal += Abc_Clock() - clk2;
677 }
678 
679 
680 /**Function*************************************************************
681 
682   Synopsis    [Evaluates one cut during library construction.]
683 
684   Description []
685 
686   SideEffects []
687 
688   SeeAlso     []
689 
690 ***********************************************************************/
Abc_NtkRecAddCut3(If_Man_t * pIfMan,If_Obj_t * pRoot,If_Cut_t * pCut)691 int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
692 {
693     Lms_Man_t * p = s_pMan3;
694     char pCanonPerm[LMS_VAR_MAX];
695     unsigned uCanonPhase;
696     int i, Index, iFanin0, iFanin1, fHole;
697     int nLeaves = If_CutLeaveNum(pCut);
698     Vec_Ptr_t * vNodes = p->vNodes;
699     Gia_Man_t * pGia = p->pGia;
700     Gia_Obj_t * pDriver;
701     If_Obj_t * pIfObj = NULL;
702     word * pTruth;
703     abctime clk;
704     p->nTried++;
705 
706     // skip small cuts
707     assert( p->nVars == (int)pCut->nLimit );
708     if ( nLeaves < 2 || (nLeaves == 2 && Abc_TtSupportSize(If_CutTruthW(pIfMan, pCut), 2) != 2) )
709     {
710         p->nFilterSize++;
711         return 1;
712     }
713 
714 //    if ( p->vTtMem2 )
715 //        Vec_MemHashInsert( p->vTtMem2, If_CutTruthW(pCut) );
716 
717     // semi-canonicize truth table
718 clk = Abc_Clock();
719     memcpy( p->pTemp1, If_CutTruthW(pIfMan, pCut), p->nWords * sizeof(word) );
720 #ifdef LMS_USE_OLD_FORM
721     uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
722 #else
723     uCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
724 #endif
725     Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
726 p->timeCanon += Abc_Clock() - clk;
727     // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
728 
729     if ( p->pGia == NULL )
730     {
731 clk = Abc_Clock();
732         // add the resulting truth table to the hash table
733         Index = Vec_MemHashInsert( p->vTtMem, p->pTemp1 );
734 /*
735         if ( p->vTruthFreqs == NULL )
736             p->vTruthFreqs = Vec_IntAlloc( 1000 );
737         assert( Index <= Vec_IntSize(p->vTruthFreqs)  );
738         if ( Index < Vec_IntSize(p->vTruthFreqs) )
739             Vec_IntAddToEntry( p->vTruthFreqs, Index, 1 );
740         else
741             Vec_IntPush( p->vTruthFreqs, 1 );
742 */
743         p->nAdded++;
744 p->timeInsert += Abc_Clock() - clk;
745         return 1;
746     }
747 
748     // collect internal nodes and skip redundant cuts
749 clk = Abc_Clock();
750     If_CutTraverse( pIfMan, pRoot, pCut, vNodes );
751 p->timeTruth += Abc_Clock() - clk;
752     if ( Vec_PtrSize(vNodes) > 253 )
753     {
754         p->nFilterSize++;
755         return 1;
756     }
757 
758 clk = Abc_Clock();
759     // map cut leaves into elementary variables of GIA
760     for ( i = 0; i < nLeaves; i++ )
761         If_ManObj( pIfMan, pCut->pLeaves[(int)pCanonPerm[i]] )->iCopy = Abc_Var2Lit( Gia_ObjId(pGia, Gia_ManPi(pGia, i)), (uCanonPhase >> i) & 1 );
762     // build internal nodes
763     fHole = 0;
764     assert( Vec_PtrSize(vNodes) > 0 );
765     Vec_PtrForEachEntryStart( If_Obj_t *, vNodes, pIfObj, i, nLeaves )
766     {
767         if ( If_ObjIsCi(pIfObj) )
768         {
769             pIfObj->iCopy = 0;
770             fHole = 1;
771             continue;
772         }
773         iFanin0 = Abc_LitNotCond( If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj) );
774         iFanin1 = Abc_LitNotCond( If_ObjFanin1(pIfObj)->iCopy, If_ObjFaninC1(pIfObj) );
775         pIfObj->iCopy = Gia_ManHashAnd( pGia, iFanin0, iFanin1 );
776     }
777     p->nHoleInTheWall += fHole;
778 p->timeBuild += Abc_Clock() - clk;
779 
780     // check if this node is already driving a PO
781     assert( If_ObjIsAnd(pIfObj) );
782     pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pIfObj->iCopy));
783     if ( pDriver->fMark1 )
784     {
785         p->nFilterSame++;
786         return 1;
787     }
788     pDriver->fMark1 = 1;
789     // create output
790     Gia_ManAppendCo( pGia, Abc_LitNotCond( pIfObj->iCopy, (uCanonPhase >> nLeaves) & 1 ) );
791 
792     // verify truth table
793 clk = Abc_Clock();
794     pTruth = Gia_ObjComputeTruthTable( pGia, Gia_ManCo(pGia, Gia_ManCoNum(pGia)-1) );
795 p->timeCheck += Abc_Clock() - clk;
796     if ( memcmp( p->pTemp1, pTruth, p->nWords * sizeof(word) ) != 0 )
797     {
798 /*
799         Kit_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
800         Kit_DsdPrintFromTruth( (unsigned *)p->pTemp1, nLeaves ); printf( "\n" );
801         printf( "Truth table verification has failed.\n" );
802 */
803         // drive PO with constant
804         Gia_ManPatchCoDriver( pGia, Gia_ManCoNum(pGia)-1, 0 );
805         // save truth table ID
806         Vec_IntPush( p->vTruthIds, -1 );
807         p->nFilterTruth++;
808         return 1;
809     }
810 
811 clk = Abc_Clock();
812     // add the resulting truth table to the hash table
813     Index = Vec_MemHashInsert( p->vTtMem, p->pTemp1 );
814     // save truth table ID
815     Vec_IntPush( p->vTruthIds, Index );
816     assert( Gia_ManCoNum(pGia) == Vec_IntSize(p->vTruthIds) );
817     p->nAdded++;
818 p->timeInsert += Abc_Clock() - clk;
819     return 1;
820 }
821 
822 /**Function*************************************************************
823 
824   Synopsis    [Top level procedure for library construction.]
825 
826   Description []
827 
828   SideEffects []
829 
830   SeeAlso     []
831 
832 ***********************************************************************/
Abc_NtkRecAdd3(Abc_Ntk_t * pNtk,int fUseSOPB)833 void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB )
834 {
835     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
836     If_Par_t Pars, * pPars = &Pars;
837     Abc_Ntk_t * pNtkNew;
838     int clk = Abc_Clock();
839     if ( Abc_NtkGetChoiceNum( pNtk ) )
840         printf( "Performing recoding structures with choices.\n" );
841     // remember that the manager was used for library construction
842     s_pMan3->fLibConstr = 1;
843     // create hash table if not available
844     if ( s_pMan3->pGia && Vec_IntSize(&s_pMan3->pGia->vHTable) == 0 )
845         Gia_ManHashStart( s_pMan3->pGia );
846 
847     // set defaults
848     memset( pPars, 0, sizeof(If_Par_t) );
849     // user-controlable paramters
850     pPars->nLutSize    =  s_pMan3->nVars;
851     pPars->nCutsMax    =  s_pMan3->nCuts;
852     pPars->DelayTarget = -1;
853     pPars->Epsilon     =  (float)0.005;
854     pPars->fArea       =  1;
855     // internal parameters
856     if ( fUseSOPB )
857     {
858         pPars->fTruth      =  1;
859         pPars->fCutMin     =  0;
860         pPars->fUsePerm    =  1;
861         pPars->fDelayOpt   =  1;
862     }
863     else
864     {
865         pPars->fTruth      =  1;
866         pPars->fCutMin     =  1;
867         pPars->fUsePerm    =  0;
868         pPars->fDelayOpt   =  0;
869     }
870     pPars->fSkipCutFilter = 0;
871     pPars->pFuncCost   =  NULL;
872     pPars->pFuncUser   =  Abc_NtkRecAddCut3;
873     // perform recording
874     pNtkNew = Abc_NtkIf( pNtk, pPars );
875     Abc_NtkDelete( pNtkNew );
876 s_pMan3->timeTotal += Abc_Clock() - clk;
877 }
878 
879  /**Function*************************************************************
880 
881   Synopsis    [Returns min AIG level at the output fo the cut using the library.]
882 
883   Description []
884 
885   SideEffects []
886 
887   SeeAlso     []
888 
889 ***********************************************************************/
If_CutComputeDelay(If_Man_t * p,If_Cut_t * pCut,char * pCanonPerm,word DelayProfile)890 static inline int If_CutComputeDelay( If_Man_t * p, If_Cut_t * pCut, char * pCanonPerm, word DelayProfile )
891 {
892     If_Obj_t* pLeaf;
893     int nLeaves = If_CutLeaveNum(pCut);
894     int i, delayTemp, delayMax = -ABC_INFINITY;
895     for ( i = 0; i < nLeaves; i++ )
896     {
897         pLeaf     = If_ManObj(p, (pCut)->pLeaves[(int)pCanonPerm[i]]);
898         delayTemp = If_ObjCutBest(pLeaf)->Delay + Lms_DelayGet(DelayProfile, i);
899         delayMax  = Abc_MaxInt( delayMax, delayTemp );
900     }
901     return delayMax;
902 }
If_CutFindBestStruct(If_Man_t * pIfMan,If_Cut_t * pCut,char * pCanonPerm,unsigned * puCanonPhase,int * pBestPo)903 static inline int If_CutFindBestStruct( If_Man_t * pIfMan, If_Cut_t * pCut, char * pCanonPerm, unsigned * puCanonPhase, int * pBestPo )
904 {
905     Lms_Man_t * p = s_pMan3;
906     int i, * pTruthId, iFirstPo, iFirstPoNext, iBestPo;
907     int BestDelay = ABC_INFINITY, BestArea = ABC_INFINITY, Delay, Area;
908     int uSupport, nLeaves = If_CutLeaveNum( pCut );
909     char * pPerm = If_CutPerm( pCut );
910     word DelayProfile;
911     abctime clk;
912     pCut->fUser = 1;
913     // compute support
914     uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
915     if ( uSupport == 0 )
916     {
917         pCut->Cost = 1;
918         for ( i = 0; i < nLeaves; i++ )
919             pPerm[i] = IF_BIG_CHAR;
920         return 0;
921     }
922     if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
923     {
924         assert( Abc_TtSuppOnlyOne(uSupport) );
925         pCut->Cost = 1;
926         for ( i = 0; i < nLeaves; i++ )
927             pPerm[i] = IF_BIG_CHAR;
928         pPerm[Abc_TtSuppFindFirst(uSupport)] = 0;
929         return If_ObjCutBest(If_ManObj(pIfMan, pCut->pLeaves[Abc_TtSuppFindFirst(uSupport)]))->Delay;
930     }
931     assert( Gia_WordCountOnes(uSupport) == nLeaves );
932 
933     // semicanonicize the function
934 clk = Abc_Clock();
935     memcpy( p->pTemp1, If_CutTruthW(pIfMan, pCut), p->nWords * sizeof(word) );
936 #ifdef LMS_USE_OLD_FORM
937     *puCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
938 #else
939     *puCanonPhase = Abc_TtCanonicize( p->pTemp1, nLeaves, pCanonPerm );
940 #endif
941     Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
942 p->timeCanon += Abc_Clock() - clk;
943 
944     // get TT ID for the given class
945     pTruthId = Vec_MemHashLookup( p->vTtMem, p->pTemp1 );
946     if ( *pTruthId == -1 )
947     {
948         pCut->Cost = IF_COST_MAX;
949         pCut->fUseless = 1;
950         return ABC_INFINITY;
951     }
952 
953     // note that array p->vTruthPo contains the first PO for the given truth table
954     // other POs belonging to the same equivalence class follow immediately after this one
955     // to iterate through the POs, we need to perform the following steps
956 
957     // find the first PO of this class
958     iFirstPo = Vec_IntEntry( p->vTruthPo, *pTruthId );
959     // find the first PO of the next class
960     iFirstPoNext = Vec_IntEntry( p->vTruthPo, *pTruthId+1 );
961     // iterate through the subgraphs of this class
962     iBestPo = -1;
963     for ( i = iFirstPo; i < iFirstPoNext; i++ )
964     {
965         Delay = If_CutComputeDelay( pIfMan, pCut, pCanonPerm, Vec_WrdEntry(p->vDelays, i) );
966         Area  = Vec_StrEntry(p->vAreas, i);
967         if ( iBestPo == -1 || BestDelay > Delay || (BestDelay == Delay && BestArea > Area) )
968         {
969             iBestPo = i;
970             BestDelay = Delay;
971             BestArea = Area;
972         }
973     }
974     if ( pBestPo )
975         *pBestPo = iBestPo;
976 
977     // mark as user cut.
978     DelayProfile = Vec_WrdEntry(p->vDelays, iBestPo);
979     pCut->Cost = Vec_StrEntry(p->vAreas, iBestPo);
980     for ( i = 0; i < nLeaves; i++ )
981         pPerm[(int)pCanonPerm[i]] = Lms_DelayGet(DelayProfile, i);
982     if ( 0 )
983     {
984         int Max = 0, Two = 0, pTimes[16];
985         for ( i = 0; i < nLeaves; i++ )
986             pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(pIfMan, pCut, i))->Delay;
987         for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
988             Max = Abc_MaxInt( Max, pTimes[i] );
989         for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
990             if ( pTimes[i] != Max )
991                 Two = Abc_MaxInt( Two, pTimes[i] );
992         if ( Two + 2 < Max && Max + 3 < BestDelay )
993         {
994             for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
995                 printf( "%3d ", pTimes[i] );
996             for ( ; i < pIfMan->pPars->nLutSize; i++ )
997                 printf( "    " );
998             printf( "-> %3d   ", BestDelay );
999             Dau_DsdPrintFromTruth( If_CutTruthW(pIfMan, pCut), If_CutLeaveNum(pCut) );
1000         }
1001     }
1002     return BestDelay;
1003 }
If_CutDelayRecCost3(If_Man_t * pIfMan,If_Cut_t * pCut,If_Obj_t * pObj)1004 int If_CutDelayRecCost3( If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pObj )
1005 {
1006     Lms_Man_t * p = s_pMan3;
1007     char pCanonPerm[LMS_VAR_MAX];
1008     unsigned uCanonPhase = 0;
1009     // make sure the cut functions match the library
1010     assert( p->nVars == (int)pCut->nLimit );
1011     // if this assertion fires, it means that LMS manager was used for library construction
1012     // in this case, GIA has to be written out and the manager restarted as described above
1013     assert( !p->fLibConstr );
1014     if ( p->vTruthPo == NULL )
1015         Lms_ManPrepare( p );
1016     // return the delay of the best structure
1017     return If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, NULL );
1018 }
1019 
1020 /**Function*************************************************************
1021 
1022   Synopsis    [Reexpresses the best structure of the cut in the HOP manager.]
1023 
1024   Description []
1025 
1026   SideEffects []
1027 
1028   SeeAlso     []
1029 
1030 ***********************************************************************/
Abc_RecToHop3(Hop_Man_t * pMan,If_Man_t * pIfMan,If_Cut_t * pCut,If_Obj_t * pIfObj)1031 Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj )
1032 {
1033     Lms_Man_t * p = s_pMan3;
1034     char pCanonPerm[LMS_VAR_MAX];
1035     unsigned uCanonPhase = 0;
1036     Hop_Obj_t * pFan0, * pFan1, * pHopObj;
1037     Gia_Man_t * pGia = p->pGia;
1038     Gia_Obj_t * pGiaPo, * pGiaTemp = NULL;
1039     int i, uSupport, BestPo = -1, nLeaves = If_CutLeaveNum(pCut);
1040     assert( pIfMan->pPars->fCutMin == 1 );
1041 
1042     // compute support
1043     uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
1044     if ( uSupport == 0 )
1045         return Hop_NotCond( Hop_ManConst0(pMan), If_CutTruthIsCompl(pCut) );
1046     if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
1047     {
1048         assert( Abc_TtSuppOnlyOne(uSupport) );
1049         return Hop_NotCond( Hop_IthVar(pMan, Abc_TtSuppFindFirst(uSupport)), If_CutTruthIsCompl(pCut) );
1050     }
1051     assert( Gia_WordCountOnes(uSupport) == nLeaves );
1052 
1053     // get the best output for this node
1054     If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
1055     assert( BestPo >= 0 );
1056     pGiaPo = Gia_ManCo( pGia, BestPo );
1057     // collect internal nodes into pGia->vTtNodes
1058     if ( pGia->vTtNodes == NULL )
1059         pGia->vTtNodes = Vec_IntAlloc( 256 );
1060     assert( Gia_ObjIsAnd( Gia_ObjFanin0(pGiaPo) ) );
1061     Gia_ObjCollectInternal( pGia, Gia_ObjFanin0(pGiaPo) );
1062     assert( Vec_IntSize(pGia->vTtNodes) > 0 );
1063 
1064     // collect HOP nodes for leaves
1065     Vec_PtrClear( p->vLabelsP );
1066     for ( i = 0; i < nLeaves; i++ )
1067         Vec_PtrPush( p->vLabelsP, Hop_NotCond(Hop_IthVar(pMan, pCanonPerm[i]), (uCanonPhase >> i) & 1) );
1068 
1069     // compute HOP nodes for internal nodes
1070     Gia_ManForEachObjVec( pGia->vTtNodes, pGia, pGiaTemp, i )
1071     {
1072         pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
1073         if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
1074             pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
1075         else
1076             pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
1077         pFan0 = Hop_NotCond(pFan0, Gia_ObjFaninC0(pGiaTemp));
1078         if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
1079             pFan1 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
1080         else
1081             pFan1 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
1082         pFan1 = Hop_NotCond(pFan1, Gia_ObjFaninC1(pGiaTemp));
1083 
1084         pHopObj = Hop_And(pMan, pFan0, pFan1);
1085         Vec_PtrPush(p->vLabelsP, pHopObj);
1086     }
1087     // get the final result
1088     assert( Gia_ObjIsAnd(pGiaTemp) );
1089     pHopObj = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
1090     // complement the result if needed
1091     return Hop_NotCond( pHopObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );
1092 }
1093 
1094 /**Function*************************************************************
1095 
1096   Synopsis    [Reexpresses the best structure of the cut in the GIA manager.]
1097 
1098   Description []
1099 
1100   SideEffects []
1101 
1102   SeeAlso     []
1103 
1104 ***********************************************************************/
Abc_RecToGia3(Gia_Man_t * pMan,If_Man_t * pIfMan,If_Cut_t * pCut,Vec_Int_t * vLeaves,int fHash)1105 int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int_t * vLeaves, int fHash )
1106 {
1107     Lms_Man_t * p = s_pMan3;
1108     char pCanonPerm[LMS_VAR_MAX];
1109     unsigned uCanonPhase = 0;
1110     int iFan0, iFan1, iGiaObj;
1111     Gia_Man_t * pGia = p->pGia;
1112     Gia_Obj_t * pGiaPo, * pGiaTemp = NULL;
1113     int i, uSupport, BestPo = -1, nLeaves = If_CutLeaveNum(pCut);
1114     assert( pIfMan->pPars->fCutMin == 1 );
1115     assert( nLeaves == Vec_IntSize(vLeaves) );
1116 
1117     // compute support
1118     uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
1119     if ( uSupport == 0 )
1120         return Abc_LitNotCond( 0, If_CutTruthIsCompl(pCut) );
1121     if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
1122     {
1123         assert( Abc_TtSuppOnlyOne(uSupport) );
1124         return Abc_LitNotCond( Vec_IntEntry(vLeaves, Abc_TtSuppFindFirst(uSupport)), If_CutTruthIsCompl(pCut) );
1125     }
1126     assert( Gia_WordCountOnes(uSupport) == nLeaves );
1127 
1128     // get the best output for this node
1129     If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
1130     assert( BestPo >= 0 );
1131     pGiaPo = Gia_ManCo( pGia, BestPo );
1132 
1133     // collect internal nodes into pGia->vTtNodes
1134     if ( pGia->vTtNodes == NULL )
1135         pGia->vTtNodes = Vec_IntAlloc( 256 );
1136     assert( Gia_ObjIsAnd( Gia_ObjFanin0(pGiaPo) ) );
1137     Gia_ObjCollectInternal( pGia, Gia_ObjFanin0(pGiaPo) );
1138     assert( Vec_IntSize(pGia->vTtNodes) > 0 );
1139 
1140     // collect GIA nodes for leaves
1141     Vec_IntClear( p->vLabels );
1142     for (i = 0; i < nLeaves; i++)
1143         Vec_IntPush( p->vLabels, Abc_LitNotCond(Vec_IntEntry(vLeaves, pCanonPerm[i]), (uCanonPhase >> i) & 1) );
1144 
1145     // compute HOP nodes for internal nodes
1146     Gia_ManForEachObjVec( pGia->vTtNodes, pGia, pGiaTemp, i )
1147     {
1148         pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
1149         if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
1150             iFan0 = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
1151         else
1152             iFan0 = Vec_IntEntry(p->vLabels, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
1153         iFan0 = Abc_LitNotCond(iFan0, Gia_ObjFaninC0(pGiaTemp));
1154         if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
1155             iFan1 = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
1156         else
1157             iFan1 = Vec_IntEntry(p->vLabels, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
1158         iFan1 = Abc_LitNotCond(iFan1, Gia_ObjFaninC1(pGiaTemp));
1159         if ( fHash )
1160             iGiaObj = Gia_ManHashAnd(pMan, iFan0, iFan1);
1161         else
1162             iGiaObj = Gia_ManAppendAnd(pMan, iFan0, iFan1);
1163         Vec_IntPush(p->vLabels, iGiaObj);
1164     }
1165     // get the final result
1166     assert( Gia_ObjIsAnd(pGiaTemp) );
1167     iGiaObj = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
1168     // complement the result if needed
1169     return Abc_LitNotCond( iGiaObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) ^ pCut->fCompl );
1170 }
1171 
1172 
1173 /**Function*************************************************************
1174 
1175   Synopsis    [Reduces GIA to contain only useful COs and internal nodes.]
1176 
1177   Description [During library construction, redundant nodes are added.
1178   Some COs are found to be useless because their TT does not match the
1179   (semi-canonicized TT) of the cut, etc.  This procedure reduces GIA
1180   to contains only useful (non-redundant, non-dominated) COs and the
1181   corresponding internal nodes. This procedure replaces GIA by a new GIA
1182   and creates new vTruthIds. The COs with the same truth table have
1183   adjacent IDs. This procedure does not change the truth tables.]
1184 
1185   SideEffects []
1186 
1187   SeeAlso     []
1188 
1189 ***********************************************************************/
1190 // count how many times TT occurs
Lms_GiaCountTruths(Lms_Man_t * p)1191 Vec_Int_t * Lms_GiaCountTruths( Lms_Man_t * p )
1192 {
1193     Vec_Int_t * vCounts = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) );
1194     int i, Entry;
1195     Vec_IntForEachEntry( p->vTruthIds, Entry, i )
1196         if ( Entry >= 0 )
1197             Vec_IntAddToEntry( vCounts, Entry, 1 );
1198     return vCounts;
1199 }
1200 // collect PO indexes worth visiting
Lms_GiaCollectUsefulCos(Lms_Man_t * p)1201 Vec_Int_t * Lms_GiaCollectUsefulCos( Lms_Man_t * p )
1202 {
1203     Vec_Int_t * vBegins = Vec_IntAlloc( Vec_MemEntryNum(p->vTtMem) );
1204     Vec_Int_t * vUseful = Vec_IntStartFull( Gia_ManCoNum(p->pGia) + Vec_MemEntryNum(p->vTtMem) );
1205     Vec_Int_t * vCounts = Lms_GiaCountTruths( p );
1206     int i, Entry, * pPlace, SumTotal = 0;
1207     // mark up the place for POs
1208     Vec_IntForEachEntry( vCounts, Entry, i )
1209     {
1210         assert( Entry > 0 );
1211         Vec_IntPush( vBegins, SumTotal );
1212         SumTotal += Entry + 1;
1213 //        printf( "%d ", Entry );
1214     }
1215     Vec_IntPush( vBegins, SumTotal );
1216     // fill out POs in their places
1217     Vec_IntFill( vCounts, Vec_IntSize(vCounts), 0 );
1218     Vec_IntForEachEntry( p->vTruthIds, Entry, i )
1219     {
1220         if ( Entry < 0 )
1221             continue;
1222         pPlace = Vec_IntEntryP( vUseful, Vec_IntEntry(vBegins, Entry) + Vec_IntEntry(vCounts, Entry) );
1223         assert( *pPlace == -1 );
1224         *pPlace = i;
1225         Vec_IntAddToEntry( vCounts, Entry, 1 );
1226     }
1227     Vec_IntFree( vBegins );
1228     Vec_IntFree( vCounts );
1229     return vUseful;
1230 }
1231 // collect non-dominated COs
Lms_GiaFindNonRedundantCos(Lms_Man_t * p)1232 Vec_Int_t * Lms_GiaFindNonRedundantCos( Lms_Man_t * p )
1233 {
1234     Vec_Int_t * vRemain;
1235     Vec_Int_t * vUseful;
1236     Vec_Wrd_t * vDelays;
1237     int i, k, EntryI, EntryK;
1238     word D1, D2;
1239     vDelays = Lms_GiaDelays( p->pGia );
1240     vUseful = Lms_GiaCollectUsefulCos( p );
1241     Vec_IntForEachEntry( vUseful, EntryI, i )
1242     {
1243         if ( EntryI < 0 )
1244             continue;
1245         D1 = Vec_WrdEntry(vDelays, EntryI);
1246         assert( D1 > 0 );
1247         Vec_IntForEachEntryStart( vUseful, EntryK, k, i+1 )
1248         {
1249             if ( EntryK == -1 )
1250                 break;
1251             if ( EntryK == -2 )
1252                 continue;
1253             D2 = Vec_WrdEntry(vDelays, EntryK);
1254             assert( D2 > 0 );
1255             if ( Lms_DelayDom(D1, D2, Gia_ManCiNum(p->pGia)) ) // D1 dominate D2
1256             {
1257                 Vec_IntWriteEntry( vUseful, k, -2 );
1258                 continue;
1259             }
1260             if ( Lms_DelayDom(D2, D1, Gia_ManCiNum(p->pGia)) ) // D2 dominate D1
1261             {
1262                 Vec_IntWriteEntry( vUseful, i, -2 );
1263                 break;
1264             }
1265         }
1266     }
1267 
1268     vRemain = Vec_IntAlloc( 1000 );
1269     Vec_IntForEachEntry( vUseful, EntryI, i )
1270         if ( EntryI >= 0 )
1271             Vec_IntPush( vRemain, EntryI );
1272     Vec_IntFree( vUseful );
1273     Vec_WrdFree( vDelays );
1274     return vRemain;
1275 }
1276 // replace GIA and vTruthIds by filtered ones
Lms_GiaNormalize(Lms_Man_t * p)1277 void Lms_GiaNormalize( Lms_Man_t * p )
1278 {
1279     Gia_Man_t * pGiaNew;
1280     Gia_Obj_t * pObj;
1281     Vec_Int_t * vRemain;
1282     Vec_Int_t * vTruthIdsNew;
1283     int i, Entry, Prev = -1, Next;
1284     // collect non-redundant COs
1285     vRemain = Lms_GiaFindNonRedundantCos( p );
1286     // change these to be useful literals
1287     vTruthIdsNew = Vec_IntAlloc( Vec_IntSize(vRemain) );
1288     Vec_IntForEachEntry( vRemain, Entry, i )
1289     {
1290         pObj = Gia_ManCo(p->pGia, Entry);
1291         assert( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) );
1292         Vec_IntWriteEntry( vRemain, i, Gia_ObjFaninLit0p(p->pGia, pObj) );
1293         // create new truth IDs
1294         Next = Vec_IntEntry(p->vTruthIds, Gia_ObjCioId(pObj));
1295         assert( Prev <= Next );
1296         Vec_IntPush( vTruthIdsNew, Next );
1297         Prev = Next;
1298     }
1299     // create a new GIA
1300     Gia_ManForEachObj( p->pGia, pObj, i )
1301         assert( pObj->fMark0 == 0 );
1302     for ( i = 0; i < Gia_ManCoNum(p->pGia); i++ )
1303         Gia_ManPatchCoDriver( p->pGia, i, 0 );
1304     Vec_IntForEachEntry( vRemain, Entry, i )
1305         Gia_ManAppendCo( p->pGia, Entry );
1306 //    pGiaNew = Gia_ManCleanup( p->pGia );
1307     pGiaNew = Gia_ManCleanupOutputs( p->pGia, Gia_ManCoNum(p->pGia) - Vec_IntSize(vRemain) );
1308     Gia_ManStop( p->pGia );
1309     p->pGia = pGiaNew;
1310     Vec_IntFree( vRemain );
1311     // update truth IDs
1312     Vec_IntFree( p->vTruthIds );
1313     p->vTruthIds = vTruthIdsNew;
1314 //    Vec_IntPrint( vTruthIdsNew );
1315 }
1316 
1317 /**Function*************************************************************
1318 
1319   Synopsis    []
1320 
1321   Description []
1322 
1323   SideEffects []
1324 
1325   SeeAlso     []
1326 
1327 ***********************************************************************/
Abc_NtkRecTruthCompare(int * p1,int * p2)1328 int Abc_NtkRecTruthCompare( int * p1, int * p2 )
1329 {
1330     int Diff = Vec_StrEntry( s_pMan3->vSupps, *p1 ) - Vec_StrEntry( s_pMan3->vSupps, *p2 );
1331     if ( Diff )
1332         return Diff;
1333     return memcmp( Vec_MemReadEntry(s_pMan3->vTtMem, *p1), Vec_MemReadEntry(s_pMan3->vTtMem, *p2), sizeof(word) * s_pMan3->nWords );
1334 }
Abc_NtkRecDumpTt3(char * pFileName,int fBinary)1335 void Abc_NtkRecDumpTt3( char * pFileName, int fBinary )
1336 {
1337     FILE * pFile;
1338     char pBuffer[1000];
1339     Lms_Man_t * p = s_pMan3;
1340     Vec_Int_t * vEntries;
1341     word * pTruth;
1342     int i, Entry, nVars = p->nVars;
1343     int nEntries = Vec_MemEntryNum(p->vTtMem);
1344     if ( nEntries == 0 )
1345     {
1346         printf( "There is not truth tables.\n" );
1347         return;
1348     }
1349     pFile = fopen( pFileName, "wb" );
1350     if ( pFile == NULL )
1351     {
1352         printf( "The file cannot be opened.\n" );
1353         return;
1354     }
1355     p->vSupps = Vec_StrAlloc( nEntries );
1356     Vec_MemForEachEntry( p->vTtMem, pTruth, i )
1357         Vec_StrPush( p->vSupps, (char)Abc_TtSupportSize(pTruth, nVars) );
1358     vEntries = Vec_IntStartNatural( nEntries );
1359     qsort( (void *)Vec_IntArray(vEntries), (size_t)nEntries, sizeof(int), (int(*)(const void *,const void *))Abc_NtkRecTruthCompare );
1360     Vec_StrFreeP( &p->vSupps );
1361     // write the file
1362     Vec_IntForEachEntry( vEntries, Entry, i )
1363     {
1364         pTruth = Vec_MemReadEntry(p->vTtMem, Entry);
1365         if ( fBinary )
1366         {
1367             fwrite( pTruth, 1, sizeof(word) * p->nWords, pFile );
1368             continue;
1369         }
1370         Extra_PrintHex( pFile, (unsigned *)pTruth, nVars );
1371         fprintf( pFile, "  " );
1372 //        Kit_DsdWriteFromTruth( pBuffer, (unsigned *)pTruth, nVars );
1373         Dau_DsdDecompose( pTruth, p->nVars, 0, (int)(nVars <= 10), pBuffer );
1374         fprintf( pFile, "%s\n", pBuffer );
1375     }
1376     fclose( pFile );
1377     Vec_IntFree( vEntries );
1378 }
1379 
1380 /**Function*************************************************************
1381 
1382   Synopsis    []
1383 
1384   Description []
1385 
1386   SideEffects []
1387 
1388   SeeAlso     []
1389 
1390 ***********************************************************************/
Abc_NtkRecInputNum3()1391 int Abc_NtkRecInputNum3()
1392 {
1393     return Gia_ManCiNum(s_pMan3->pGia);
1394 }
Abc_NtkRecIsRunning3()1395 int Abc_NtkRecIsRunning3()
1396 {
1397     return s_pMan3 != NULL;
1398 }
Abc_NtkRecGetGia3()1399 Gia_Man_t * Abc_NtkRecGetGia3()
1400 {
1401     abctime clk = Abc_Clock();
1402     printf( "Before normalizing: Library has %d classes and %d AIG subgraphs with %d AND nodes.\n",
1403         Vec_MemEntryNum(s_pMan3->vTtMem), Gia_ManPoNum(s_pMan3->pGia), Gia_ManAndNum(s_pMan3->pGia) );
1404     Lms_GiaNormalize( s_pMan3 );
1405     printf( "After normalizing:  Library has %d classes and %d AIG subgraphs with %d AND nodes.\n",
1406         Vec_MemEntryNum(s_pMan3->vTtMem), Gia_ManPoNum(s_pMan3->pGia), Gia_ManAndNum(s_pMan3->pGia) );
1407     Abc_PrintTime( 1, "Normalization runtime", Abc_Clock() - clk );
1408     s_pMan3->fLibConstr = 0;
1409     return s_pMan3->pGia;
1410 }
Abc_NtkRecPs3(int fPrintLib)1411 void Abc_NtkRecPs3(int fPrintLib)
1412 {
1413     Lms_ManPrint( s_pMan3 );
1414 }
Abc_NtkRecStart3(Gia_Man_t * p,int nVars,int nCuts,int fFuncOnly,int fVerbose)1415 void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose )
1416 {
1417     assert( s_pMan3 == NULL );
1418     s_pMan3 = Lms_ManStart( p, nVars, nCuts, fFuncOnly, fVerbose );
1419 }
1420 
Abc_NtkRecStop3()1421 void Abc_NtkRecStop3()
1422 {
1423     assert( s_pMan3 != NULL );
1424     Lms_ManStop( s_pMan3 );
1425     s_pMan3 = NULL;
1426 }
1427 
1428 ////////////////////////////////////////////////////////////////////////
1429 ///                       END OF FILE                                ///
1430 ////////////////////////////////////////////////////////////////////////
1431 
1432 
1433 ABC_NAMESPACE_IMPL_END
1434