abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
darLib.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [darLib.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware AIG rewriting.]
8 
9  Synopsis [Library of AIG subgraphs used for rewriting.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: darLib.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "darInt.h"
22 #include "aig/gia/gia.h"
23 #include "dar.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Dar_Lib_t_ Dar_Lib_t;
33 typedef struct Dar_LibObj_t_ Dar_LibObj_t;
34 typedef struct Dar_LibDat_t_ Dar_LibDat_t;
35 
36 struct Dar_LibObj_t_ // library object (2 words)
37 {
38  unsigned Fan0 : 16; // the first fanin
39  unsigned Fan1 : 16; // the second fanin
40  unsigned fCompl0 : 1; // the first compl attribute
41  unsigned fCompl1 : 1; // the second compl attribute
42  unsigned fPhase : 1; // the phase of the node
43  unsigned fTerm : 1; // indicates a PI
44  unsigned Num : 28; // internal use
45 };
46 
47 struct Dar_LibDat_t_ // library object data
48 {
49  union {
50  Aig_Obj_t * pFunc; // the corresponding AIG node if it exists
51  int iGunc; }; // the corresponding AIG node if it exists
52  int Level; // level of this node after it is constructured
53  int TravId; // traversal ID of the library object data
54  float dProb; // probability of the node being 1
55  unsigned char fMffc; // set to one if node is part of MFFC
56  unsigned char nLats[3]; // the number of latches on the input/output stem
57 };
58 
59 struct Dar_Lib_t_ // library
60 {
61  // objects
62  Dar_LibObj_t * pObjs; // the set of library objects
63  int nObjs; // the number of objects used
64  int iObj; // the current object
65  // structures by class
66  int nSubgr[222]; // the number of subgraphs by class
67  int * pSubgr[222]; // the subgraphs for each class
68  int * pSubgrMem; // memory for subgraph pointers
69  int nSubgrTotal; // the total number of subgraph
70  // structure priorities
71  int * pPriosMem; // memory for priority of structures
72  int * pPrios[222]; // pointers to the priority numbers
73  // structure places in the priorities
74  int * pPlaceMem; // memory for places of structures in the priority lists
75  int * pPlace[222]; // pointers to the places numbers
76  // structure scores
77  int * pScoreMem; // memory for scores of structures
78  int * pScore[222]; // pointers to the scores numbers
79  // nodes by class
80  int nNodes[222]; // the number of nodes by class
81  int * pNodes[222]; // the nodes for each class
82  int * pNodesMem; // memory for nodes pointers
83  int nNodesTotal; // the total number of nodes
84  // prepared library
85  int nSubgraphs;
86  int nNodes0Max;
87  // nodes by class
88  int nNodes0[222]; // the number of nodes by class
89  int * pNodes0[222]; // the nodes for each class
90  int * pNodes0Mem; // memory for nodes pointers
91  int nNodes0Total; // the total number of nodes
92  // structures by class
93  int nSubgr0[222]; // the number of subgraphs by class
94  int * pSubgr0[222]; // the subgraphs for each class
95  int * pSubgr0Mem; // memory for subgraph pointers
96  int nSubgr0Total; // the total number of subgraph
97  // object data
98  Dar_LibDat_t * pDatas;
99  int nDatas;
100  // information about NPN classes
101  char ** pPerms4;
102  unsigned short * puCanons;
103  char * pPhases;
104  char * pPerms;
105  unsigned char * pMap;
106 };
107 
108 static Dar_Lib_t * s_DarLib = NULL;
109 
110 static inline Dar_LibObj_t * Dar_LibObj( Dar_Lib_t * p, int Id ) { return p->pObjs + Id; }
111 static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pObj->Num < (0xFFFF & ~pObj->Num) ? pObj->Num : (0xFFFF & ~pObj->Num); }
112 
113 ////////////////////////////////////////////////////////////////////////
114 /// FUNCTION DEFINITIONS ///
115 ////////////////////////////////////////////////////////////////////////
116 
117 /**Function*************************************************************
118 
119  Synopsis [Starts the library.]
120 
121  Description []
122 
123  SideEffects []
124 
125  SeeAlso []
126 
127 ***********************************************************************/
128 Dar_Lib_t * Dar_LibAlloc( int nObjs )
129 {
130  unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
131  Dar_Lib_t * p;
132  int i;//, clk = Abc_Clock();
133  p = ABC_ALLOC( Dar_Lib_t, 1 );
134  memset( p, 0, sizeof(Dar_Lib_t) );
135  // allocate objects
136  p->nObjs = nObjs;
137  p->pObjs = ABC_ALLOC( Dar_LibObj_t, nObjs );
138  memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
139  // allocate canonical data
140  p->pPerms4 = Dar_Permutations( 4 );
141  Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
142  // start the elementary objects
143  p->iObj = 4;
144  for ( i = 0; i < 4; i++ )
145  {
146  p->pObjs[i].fTerm = 1;
147  p->pObjs[i].Num = uTruths[i];
148  }
149 // ABC_PRT( "Library start", Abc_Clock() - clk );
150  return p;
151 }
152 
153 /**Function*************************************************************
154 
155  Synopsis [Frees the library.]
156 
157  Description []
158 
159  SideEffects []
160 
161  SeeAlso []
162 
163 ***********************************************************************/
164 void Dar_LibFree( Dar_Lib_t * p )
165 {
166  ABC_FREE( p->pObjs );
167  ABC_FREE( p->pDatas );
168  ABC_FREE( p->pNodesMem );
169  ABC_FREE( p->pNodes0Mem );
170  ABC_FREE( p->pSubgrMem );
171  ABC_FREE( p->pSubgr0Mem );
172  ABC_FREE( p->pPriosMem );
173  ABC_FREE( p->pPlaceMem );
174  ABC_FREE( p->pScoreMem );
175  ABC_FREE( p->pPerms4 );
176  ABC_FREE( p->puCanons );
177  ABC_FREE( p->pPhases );
178  ABC_FREE( p->pPerms );
179  ABC_FREE( p->pMap );
180  ABC_FREE( p );
181 }
182 
183 /**Function*************************************************************
184 
185  Synopsis [Returns canonical truth tables.]
186 
187  Description []
188 
189  SideEffects []
190 
191  SeeAlso []
192 
193 ***********************************************************************/
194 int Dar_LibReturnClass( unsigned uTruth )
195 {
196  return s_DarLib->pMap[uTruth & 0xffff];
197 }
198 
199 
200 /**Function*************************************************************
201 
202  Synopsis [Returns canonical truth tables.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 void Dar_LibReturnCanonicals( unsigned * pCanons )
212 {
213  int Visits[222] = {0};
214  int i, k;
215  // find canonical truth tables
216  for ( i = k = 0; i < (1<<16); i++ )
217  if ( !Visits[s_DarLib->pMap[i]] )
218  {
219  Visits[s_DarLib->pMap[i]] = 1;
220  pCanons[k++] = ((i<<16) | i);
221  }
222  assert( k == 222 );
223 }
224 
225 /**Function*************************************************************
226 
227  Synopsis [Adds one AND to the library.]
228 
229  Description []
230 
231  SideEffects []
232 
233  SeeAlso []
234 
235 ***********************************************************************/
236 void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 )
237 {
238  Dar_LibObj_t * pFan0 = Dar_LibObj( p, Id0 );
239  Dar_LibObj_t * pFan1 = Dar_LibObj( p, Id1 );
240  Dar_LibObj_t * pObj = p->pObjs + p->iObj++;
241  pObj->Fan0 = Id0;
242  pObj->Fan1 = Id1;
243  pObj->fCompl0 = fCompl0;
244  pObj->fCompl1 = fCompl1;
245  pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
246  pObj->Num = 0xFFFF & (fCompl0? ~pFan0->Num : pFan0->Num) & (fCompl1? ~pFan1->Num : pFan1->Num);
247 }
248 
249 /**Function*************************************************************
250 
251  Synopsis [Adds one AND to the library.]
252 
253  Description []
254 
255  SideEffects []
256 
257  SeeAlso []
258 
259 ***********************************************************************/
260 void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
261 {
262  if ( pObj->fTerm || (int)pObj->Num == Class )
263  return;
264  pObj->Num = Class;
265  Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
266  Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
267  if ( fCollect )
268  p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
269  else
270  p->nNodes[Class]++;
271 }
272 
273 /**Function*************************************************************
274 
275  Synopsis [Adds one AND to the library.]
276 
277  Description []
278 
279  SideEffects []
280 
281  SeeAlso []
282 
283 ***********************************************************************/
284 void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
285 {
286  int fTraining = 0;
287  Dar_LibObj_t * pObj;
288  int nNodesTotal, uTruth, Class, Out, i, k;
289  assert( p->iObj == p->nObjs );
290 
291  // count the number of representatives of each class
292  for ( i = 0; i < 222; i++ )
293  p->nSubgr[i] = p->nNodes[i] = 0;
294  Vec_IntForEachEntry( vOuts, Out, i )
295  {
296  pObj = Dar_LibObj( p, Out );
297  uTruth = Dar_LibObjTruth( pObj );
298  Class = p->pMap[uTruth];
299  p->nSubgr[Class]++;
300  }
301  // allocate memory for the roots of each class
302  p->pSubgrMem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
303  p->pSubgr0Mem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
304  p->nSubgrTotal = 0;
305  for ( i = 0; i < 222; i++ )
306  {
307  p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
308  p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
309  p->nSubgrTotal += p->nSubgr[i];
310  p->nSubgr[i] = 0;
311  }
312  assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
313  // add the outputs to storage
314  Vec_IntForEachEntry( vOuts, Out, i )
315  {
316  pObj = Dar_LibObj( p, Out );
317  uTruth = Dar_LibObjTruth( pObj );
318  Class = p->pMap[uTruth];
319  p->pSubgr[Class][ p->nSubgr[Class]++ ] = Out;
320  }
321 
322  if ( fTraining )
323  {
324  // allocate memory for the priority of roots of each class
325  p->pPriosMem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
326  p->nSubgrTotal = 0;
327  for ( i = 0; i < 222; i++ )
328  {
329  p->pPrios[i] = p->pPriosMem + p->nSubgrTotal;
330  p->nSubgrTotal += p->nSubgr[i];
331  for ( k = 0; k < p->nSubgr[i]; k++ )
332  p->pPrios[i][k] = k;
333 
334  }
335  assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
336 
337  // allocate memory for the priority of roots of each class
338  p->pPlaceMem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
339  p->nSubgrTotal = 0;
340  for ( i = 0; i < 222; i++ )
341  {
342  p->pPlace[i] = p->pPlaceMem + p->nSubgrTotal;
343  p->nSubgrTotal += p->nSubgr[i];
344  for ( k = 0; k < p->nSubgr[i]; k++ )
345  p->pPlace[i][k] = k;
346 
347  }
348  assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
349 
350  // allocate memory for the priority of roots of each class
351  p->pScoreMem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
352  p->nSubgrTotal = 0;
353  for ( i = 0; i < 222; i++ )
354  {
355  p->pScore[i] = p->pScoreMem + p->nSubgrTotal;
356  p->nSubgrTotal += p->nSubgr[i];
357  for ( k = 0; k < p->nSubgr[i]; k++ )
358  p->pScore[i][k] = 0;
359 
360  }
361  assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
362  }
363  else
364  {
365  int Counter = 0;
366  // allocate memory for the priority of roots of each class
367  p->pPriosMem = ABC_ALLOC( int, Vec_IntSize(vOuts) );
368  p->nSubgrTotal = 0;
369  for ( i = 0; i < 222; i++ )
370  {
371  p->pPrios[i] = p->pPriosMem + p->nSubgrTotal;
372  p->nSubgrTotal += p->nSubgr[i];
373  for ( k = 0; k < p->nSubgr[i]; k++ )
374  p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++);
375 
376  }
377  assert( p->nSubgrTotal == Vec_IntSize(vOuts) );
378  assert( Counter == Vec_IntSize(vPrios) );
379  }
380 
381  // create traversal IDs
382  for ( i = 0; i < p->iObj; i++ )
383  Dar_LibObj(p, i)->Num = 0xff;
384  // count nodes in each class
385  for ( i = 0; i < 222; i++ )
386  for ( k = 0; k < p->nSubgr[i]; k++ )
387  Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
388  // count the total number of nodes
389  p->nNodesTotal = 0;
390  for ( i = 0; i < 222; i++ )
391  p->nNodesTotal += p->nNodes[i];
392  // allocate memory for the nodes of each class
393  p->pNodesMem = ABC_ALLOC( int, p->nNodesTotal );
394  p->pNodes0Mem = ABC_ALLOC( int, p->nNodesTotal );
395  p->nNodesTotal = 0;
396  for ( i = 0; i < 222; i++ )
397  {
398  p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
399  p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
400  p->nNodesTotal += p->nNodes[i];
401  p->nNodes[i] = 0;
402  }
403  // create traversal IDs
404  for ( i = 0; i < p->iObj; i++ )
405  Dar_LibObj(p, i)->Num = 0xff;
406  // add the nodes to storage
407  nNodesTotal = 0;
408  for ( i = 0; i < 222; i++ )
409  {
410  for ( k = 0; k < p->nSubgr[i]; k++ )
411  Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
412  nNodesTotal += p->nNodes[i];
413 //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
414  }
415  assert( nNodesTotal == p->nNodesTotal );
416  // prepare the number of the PI nodes
417  for ( i = 0; i < 4; i++ )
418  Dar_LibObj(p, i)->Num = i;
419 }
420 
421 /**Function*************************************************************
422 
423  Synopsis [Starts the library.]
424 
425  Description []
426 
427  SideEffects []
428 
429  SeeAlso []
430 
431 ***********************************************************************/
432 void Dar_LibCreateData( Dar_Lib_t * p, int nDatas )
433 {
434  if ( p->nDatas == nDatas )
435  return;
436  ABC_FREE( p->pDatas );
437  // allocate datas
438  p->nDatas = nDatas;
439  p->pDatas = ABC_ALLOC( Dar_LibDat_t, nDatas );
440  memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Adds one AND to the library.]
446 
447  Description []
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
455 {
456  if ( pObj->fTerm || (int)pObj->Num == Class )
457  return;
458  pObj->Num = Class;
459  Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
460  Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
461  if ( fCollect )
462  p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
463  else
464  p->nNodes0[Class]++;
465 }
466 
467 /**Function*************************************************************
468 
469  Synopsis [Starts the library.]
470 
471  Description []
472 
473  SideEffects []
474 
475  SeeAlso []
476 
477 ***********************************************************************/
478 void Dar_LibPrepare( int nSubgraphs )
479 {
480  Dar_Lib_t * p = s_DarLib;
481  int i, k, nNodes0Total;
482  if ( p->nSubgraphs == nSubgraphs )
483  return;
484 
485  // favor special classes:
486  // 1 : F = (!d*!c*!b*!a)
487  // 4 : F = (!d*!c*!(b*a))
488  // 12 : F = (!d*!(c*!(!b*!a)))
489  // 20 : F = (!d*!(c*b*a))
490 
491  // set the subgraph counters
492  p->nSubgr0Total = 0;
493  for ( i = 0; i < 222; i++ )
494  {
495 // if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes
496  if ( i == 1 ) // special classes
497  p->nSubgr0[i] = p->nSubgr[i];
498  else
499  p->nSubgr0[i] = Abc_MinInt( p->nSubgr[i], nSubgraphs );
500  p->nSubgr0Total += p->nSubgr0[i];
501  for ( k = 0; k < p->nSubgr0[i]; k++ )
502  p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
503  }
504 
505  // count the number of nodes
506  // clean node counters
507  for ( i = 0; i < 222; i++ )
508  p->nNodes0[i] = 0;
509  // create traversal IDs
510  for ( i = 0; i < p->iObj; i++ )
511  Dar_LibObj(p, i)->Num = 0xff;
512  // count nodes in each class
513  // count the total number of nodes and the largest class
514  p->nNodes0Total = 0;
515  p->nNodes0Max = 0;
516  for ( i = 0; i < 222; i++ )
517  {
518  for ( k = 0; k < p->nSubgr0[i]; k++ )
519  Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
520  p->nNodes0Total += p->nNodes0[i];
521  p->nNodes0Max = Abc_MaxInt( p->nNodes0Max, p->nNodes0[i] );
522  }
523 
524  // clean node counters
525  for ( i = 0; i < 222; i++ )
526  p->nNodes0[i] = 0;
527  // create traversal IDs
528  for ( i = 0; i < p->iObj; i++ )
529  Dar_LibObj(p, i)->Num = 0xff;
530  // add the nodes to storage
531  nNodes0Total = 0;
532  for ( i = 0; i < 222; i++ )
533  {
534  for ( k = 0; k < p->nSubgr0[i]; k++ )
535  Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
536  nNodes0Total += p->nNodes0[i];
537  }
538  assert( nNodes0Total == p->nNodes0Total );
539  // prepare the number of the PI nodes
540  for ( i = 0; i < 4; i++ )
541  Dar_LibObj(p, i)->Num = i;
542 
543  // realloc the datas
544  Dar_LibCreateData( p, p->nNodes0Max + 32 );
545  // allocated more because Dar_LibBuildBest() sometimes requires more entries
546 }
547 
548 /**Function*************************************************************
549 
550  Synopsis [Reads library from array.]
551 
552  Description []
553 
554  SideEffects []
555 
556  SeeAlso []
557 
558 ***********************************************************************/
559 Dar_Lib_t * Dar_LibRead()
560 {
561  Vec_Int_t * vObjs, * vOuts, * vPrios;
562  Dar_Lib_t * p;
563  int i;
564  // read nodes and outputs
565  vObjs = Dar_LibReadNodes();
566  vOuts = Dar_LibReadOuts();
567  vPrios = Dar_LibReadPrios();
568  // create library
569  p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
570  // create nodes
571  for ( i = 0; i < vObjs->nSize; i += 2 )
572  Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
573  vObjs->pArray[i] & 1, vObjs->pArray[i+1] & 1 );
574  // create outputs
575  Dar_LibSetup( p, vOuts, vPrios );
576  Vec_IntFree( vObjs );
577  Vec_IntFree( vOuts );
578  Vec_IntFree( vPrios );
579  return p;
580 }
581 
582 /**Function*************************************************************
583 
584  Synopsis [Starts the library.]
585 
586  Description []
587 
588  SideEffects []
589 
590  SeeAlso []
591 
592 ***********************************************************************/
593 void Dar_LibStart()
594 {
595 // abctime clk = Abc_Clock();
596  if ( s_DarLib != NULL )
597  return;
598  assert( s_DarLib == NULL );
599  s_DarLib = Dar_LibRead();
600 // printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
601 // ABC_PRT( "Time", Abc_Clock() - clk );
602 }
603 
604 /**Function*************************************************************
605 
606  Synopsis [Stops the library.]
607 
608  Description []
609 
610  SideEffects []
611 
612  SeeAlso []
613 
614 ***********************************************************************/
615 void Dar_LibStop()
616 {
617  assert( s_DarLib != NULL );
618  Dar_LibFree( s_DarLib );
619  s_DarLib = NULL;
620 }
621 
622 /**Function*************************************************************
623 
624  Synopsis [Updates the score of the class and adjusts the priority of this class.]
625 
626  Description []
627 
628  SideEffects []
629 
630  SeeAlso []
631 
632 ***********************************************************************/
633 void Dar_LibIncrementScore( int Class, int Out, int Gain )
634 {
635  int * pPrios = s_DarLib->pPrios[Class]; // pPrios[i] = Out
636  int * pPlace = s_DarLib->pPlace[Class]; // pPlace[Out] = i
637  int * pScore = s_DarLib->pScore[Class]; // score of Out
638  int Out2;
639  assert( Class >= 0 && Class < 222 );
640  assert( Out >= 0 && Out < s_DarLib->nSubgr[Class] );
641  assert( pPlace[pPrios[Out]] == Out );
642  // increment the score
643  pScore[Out] += Gain;
644  // move the out in the order
645  while ( pPlace[Out] > 0 && pScore[Out] > pScore[ pPrios[pPlace[Out]-1] ] )
646  {
647  // get the previous output in the priority list
648  Out2 = pPrios[pPlace[Out]-1];
649  // swap Out and Out2
650  pPlace[Out]--;
651  pPlace[Out2]++;
652  pPrios[pPlace[Out]] = Out;
653  pPrios[pPlace[Out2]] = Out2;
654  }
655 }
656 
657 /**Function*************************************************************
658 
659  Synopsis [Prints out the priorities into the file.]
660 
661  Description []
662 
663  SideEffects []
664 
665  SeeAlso []
666 
667 ***********************************************************************/
668 void Dar_LibDumpPriorities()
669 {
670  int i, k, Out, Out2, Counter = 0, Printed = 0;
671  printf( "\nOutput priorities (total = %d):\n", s_DarLib->nSubgrTotal );
672  for ( i = 0; i < 222; i++ )
673  {
674 // printf( "Class%d: ", i );
675  for ( k = 0; k < s_DarLib->nSubgr[i]; k++ )
676  {
677  Out = s_DarLib->pPrios[i][k];
678  Out2 = k == 0 ? Out : s_DarLib->pPrios[i][k-1];
679  assert( s_DarLib->pScore[i][Out2] >= s_DarLib->pScore[i][Out] );
680 // printf( "%d(%d), ", Out, s_DarLib->pScore[i][Out] );
681  printf( "%d, ", Out );
682  Printed++;
683  if ( ++Counter == 15 )
684  {
685  printf( "\n" );
686  Counter = 0;
687  }
688  }
689  }
690  printf( "\n" );
691  assert( Printed == s_DarLib->nSubgrTotal );
692 }
693 
694 
695 /**Function*************************************************************
696 
697  Synopsis [Matches the cut with its canonical form.]
698 
699  Description []
700 
701  SideEffects []
702 
703  SeeAlso []
704 
705 ***********************************************************************/
706 int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut )
707 {
708  Aig_Obj_t * pFanin;
709  unsigned uPhase;
710  char * pPerm;
711  int i;
712  assert( pCut->nLeaves == 4 );
713  // get the fanin permutation
714  uPhase = s_DarLib->pPhases[pCut->uTruth];
715  pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[pCut->uTruth] ];
716  // collect fanins with the corresponding permutation/phase
717  for ( i = 0; i < (int)pCut->nLeaves; i++ )
718  {
719  pFanin = Aig_ManObj( p->pAig, pCut->pLeaves[ (int)pPerm[i] ] );
720  if ( pFanin == NULL )
721  {
722  p->nCutsBad++;
723  return 0;
724  }
725  pFanin = Aig_NotCond(pFanin, ((uPhase >> i) & 1) );
726  s_DarLib->pDatas[i].pFunc = pFanin;
727  s_DarLib->pDatas[i].Level = Aig_Regular(pFanin)->Level;
728  // copy the propability of node being one
729  if ( p->pPars->fPower )
730  {
731  float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pFanin)) ) );
732  s_DarLib->pDatas[i].dProb = Aig_IsComplement(pFanin)? 1.0-Prob : Prob;
733  }
734  }
735  p->nCutsGood++;
736  return 1;
737 }
738 
739 
740 
741 /**Function*************************************************************
742 
743  Synopsis [Marks the MFFC of the node.]
744 
745  Description []
746 
747  SideEffects []
748 
749  SeeAlso []
750 
751 ***********************************************************************/
752 int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * pPower )
753 {
754  int i, nNodes;
755  // mark the cut leaves
756  for ( i = 0; i < nLeaves; i++ )
757  Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
758  // label MFFC with current ID
759  nNodes = Aig_NodeMffcLabel( p, pRoot, pPower );
760  // unmark the cut leaves
761  for ( i = 0; i < nLeaves; i++ )
762  Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
763  return nNodes;
764 }
765 
766 /**Function*************************************************************
767 
768  Synopsis [Evaluates one cut.]
769 
770  Description [Returns the best gain.]
771 
772  SideEffects []
773 
774  SeeAlso []
775 
776 ***********************************************************************/
777 void Dar_LibObjPrint_rec( Dar_LibObj_t * pObj )
778 {
779  if ( pObj->fTerm )
780  {
781  printf( "%c", 'a' + (int)(pObj - s_DarLib->pObjs) );
782  return;
783  }
784  printf( "(" );
785  Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan0) );
786  if ( pObj->fCompl0 )
787  printf( "\'" );
788  Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan1) );
789  if ( pObj->fCompl0 )
790  printf( "\'" );
791  printf( ")" );
792 }
793 
794 
795 /**Function*************************************************************
796 
797  Synopsis [Assigns numbers to the nodes of one class.]
798 
799  Description []
800 
801  SideEffects []
802 
803  SeeAlso []
804 
805 ***********************************************************************/
806 void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
807 {
808  Dar_LibObj_t * pObj;
809  Dar_LibDat_t * pData, * pData0, * pData1;
810  Aig_Obj_t * pFanin0, * pFanin1;
811  int i;
812  for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
813  {
814  // get one class node, assign its temporary number and set its data
815  pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
816  pObj->Num = 4 + i;
817  assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
818  pData = s_DarLib->pDatas + pObj->Num;
819  pData->fMffc = 0;
820  pData->pFunc = NULL;
821  pData->TravId = 0xFFFF;
822 
823  // explore the fanins
824  assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
825  assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
826  pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
827  pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
828  pData->Level = 1 + Abc_MaxInt(pData0->Level, pData1->Level);
829  if ( pData0->pFunc == NULL || pData1->pFunc == NULL )
830  continue;
831  pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
832  pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 );
833  if ( Aig_Regular(pFanin0) == pRoot || Aig_Regular(pFanin1) == pRoot )
834  continue;
835  pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 );
836  if ( pData->pFunc )
837  {
838  // update the level to be more accurate
839  pData->Level = Aig_Regular(pData->pFunc)->Level;
840  // mark the node if it is part of MFFC
841  pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc));
842  // assign the probability
843  if ( p->pPars->fPower )
844  {
845  float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) );
846  pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob;
847  }
848  }
849  }
850 }
851 
852 /**Function*************************************************************
853 
854  Synopsis [Evaluates one cut.]
855 
856  Description [Returns the best gain.]
857 
858  SideEffects []
859 
860  SeeAlso []
861 
862 ***********************************************************************/
863 int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower )
864 {
865  Dar_LibDat_t * pData;
866  float Power0, Power1;
867  int Area;
868  if ( pPower )
869  *pPower = (float)0.0;
870  pData = s_DarLib->pDatas + pObj->Num;
871  if ( pData->TravId == Out )
872  return 0;
873  pData->TravId = Out;
874  if ( pObj->fTerm )
875  {
876  if ( pPower )
877  *pPower = pData->dProb;
878  return 0;
879  }
880  assert( pObj->Num > 3 );
881  if ( pData->Level > Required )
882  return 0xff;
883  if ( pData->pFunc && !pData->fMffc )
884  {
885  if ( pPower )
886  *pPower = pData->dProb;
887  return 0;
888  }
889  // this is a new node - get a bound on the area of its branches
890  nNodesSaved--;
891  Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1, pPower? &Power0 : NULL );
892  if ( Area > nNodesSaved )
893  return 0xff;
894  Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1, pPower? &Power1 : NULL );
895  if ( Area > nNodesSaved )
896  return 0xff;
897  if ( pPower )
898  {
899  Dar_LibDat_t * pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
900  Dar_LibDat_t * pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
901  pData->dProb = (pObj->fCompl0? 1.0 - pData0->dProb : pData0->dProb)*
902  (pObj->fCompl1? 1.0 - pData1->dProb : pData1->dProb);
903  *pPower = Power0 + 2.0 * pData0->dProb * (1.0 - pData0->dProb) +
904  Power1 + 2.0 * pData1->dProb * (1.0 - pData1->dProb);
905  }
906  return Area + 1;
907 }
908 
909 /**Function*************************************************************
910 
911  Synopsis [Evaluates one cut.]
912 
913  Description [Returns the best gain.]
914 
915  SideEffects []
916 
917  SeeAlso []
918 
919 ***********************************************************************/
920 void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required, int * pnMffcSize )
921 {
922  int fTraining = 0;
923  float PowerSaved, PowerAdded;
924  Dar_LibObj_t * pObj;
925  int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
926  abctime clk = Abc_Clock();
927  if ( pCut->nLeaves != 4 )
928  return;
929  // check if the cut exits and assigns leaves and their levels
930  if ( !Dar_LibCutMatch(p, pCut) )
931  return;
932  // mark MFFC of the node
933  nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL );
934  // evaluate the cut
935  Class = s_DarLib->pMap[pCut->uTruth];
936  Dar_LibEvalAssignNums( p, Class, pRoot );
937  // profile outputs by their savings
938  p->nTotalSubgs += s_DarLib->nSubgr0[Class];
939  p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
940  for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
941  {
942  pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
943  if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
944  continue;
945  nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL );
946  nNodesGained = nNodesSaved - nNodesAdded;
947  if ( p->pPars->fPower && PowerSaved < PowerAdded )
948  continue;
949  if ( fTraining && nNodesGained >= 0 )
950  Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
951  if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
952  continue;
953  if ( nNodesGained < p->GainBest ||
954  (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
955  continue;
956  // remember this possibility
957  Vec_PtrClear( p->vLeavesBest );
958  for ( k = 0; k < (int)pCut->nLeaves; k++ )
959  Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
960  p->OutBest = s_DarLib->pSubgr0[Class][Out];
961  p->OutNumBest = Out;
962  p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
963  p->GainBest = nNodesGained;
964  p->ClassBest = Class;
965  assert( p->LevelBest <= Required );
966  *pnMffcSize = nNodesSaved;
967  }
968 clk = Abc_Clock() - clk;
969 p->ClassTimes[Class] += clk;
970 p->timeEval += clk;
971 }
972 
973 /**Function*************************************************************
974 
975  Synopsis [Clears the fields of the nodes used in this cut.]
976 
977  Description []
978 
979  SideEffects []
980 
981  SeeAlso []
982 
983 ***********************************************************************/
984 void Dar_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter )
985 {
986  if ( pObj->fTerm )
987  return;
988  pObj->Num = (*pCounter)++;
989  s_DarLib->pDatas[ pObj->Num ].pFunc = NULL;
990  Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter );
991  Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter );
992 }
993 
994 /**Function*************************************************************
995 
996  Synopsis [Reconstructs the best cut.]
997 
998  Description []
999 
1000  SideEffects []
1001 
1002  SeeAlso []
1003 
1004 ***********************************************************************/
1005 Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
1006 {
1007  Aig_Obj_t * pFanin0, * pFanin1;
1008  Dar_LibDat_t * pData = s_DarLib->pDatas + pObj->Num;
1009  if ( pData->pFunc )
1010  return pData->pFunc;
1011  pFanin0 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) );
1012  pFanin1 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) );
1013  pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
1014  pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
1015  pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
1016 // assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level );
1017  return pData->pFunc;
1018 }
1019 
1020 /**Function*************************************************************
1021 
1022  Synopsis [Reconstructs the best cut.]
1023 
1024  Description []
1025 
1026  SideEffects []
1027 
1028  SeeAlso []
1029 
1030 ***********************************************************************/
1031 Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p )
1032 {
1033  int i, Counter = 4;
1034  for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
1035  s_DarLib->pDatas[i].pFunc = (Aig_Obj_t *)Vec_PtrEntry( p->vLeavesBest, i );
1036  Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
1037  return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
1038 }
1039 
1040 
1041 
1042 
1043 
1044 
1045 /**Function*************************************************************
1046 
1047  Synopsis [Matches the cut with its canonical form.]
1048 
1049  Description []
1050 
1051  SideEffects []
1052 
1053  SeeAlso []
1054 
1055 ***********************************************************************/
1056 int Dar2_LibCutMatch( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth )
1057 {
1058  unsigned uPhase;
1059  char * pPerm;
1060  int i;
1061  assert( Vec_IntSize(vCutLits) == 4 );
1062  // get the fanin permutation
1063  uPhase = s_DarLib->pPhases[uTruth];
1064  pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[uTruth] ];
1065  // collect fanins with the corresponding permutation/phase
1066  for ( i = 0; i < Vec_IntSize(vCutLits); i++ )
1067  {
1068 // pFanin = Gia_ManObj( p, pCut->pLeaves[ (int)pPerm[i] ] );
1069 // pFanin = Gia_ManObj( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) );
1070 // pFanin = Gia_ObjFromLit( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) );
1071  s_DarLib->pDatas[i].iGunc = Abc_LitNotCond( Vec_IntEntry(vCutLits, (int)pPerm[i]), ((uPhase >> i) & 1) );
1072  s_DarLib->pDatas[i].Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, s_DarLib->pDatas[i].iGunc)) );
1073  }
1074  return 1;
1075 }
1076 
1077 /**Function*************************************************************
1078 
1079  Synopsis [Assigns numbers to the nodes of one class.]
1080 
1081  Description []
1082 
1083  SideEffects []
1084 
1085  SeeAlso []
1086 
1087 ***********************************************************************/
1088 void Dar2_LibEvalAssignNums( Gia_Man_t * p, int Class )
1089 {
1090  Dar_LibObj_t * pObj;
1091  Dar_LibDat_t * pData, * pData0, * pData1;
1092  int iFanin0, iFanin1, i, iLit;
1093  for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
1094  {
1095  // get one class node, assign its temporary number and set its data
1096  pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
1097  pObj->Num = 4 + i;
1098  assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
1099  pData = s_DarLib->pDatas + pObj->Num;
1100  pData->fMffc = 0;
1101  pData->iGunc = -1;
1102  pData->TravId = 0xFFFF;
1103 
1104  // explore the fanins
1105  assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
1106  assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
1107  pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
1108  pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
1109  pData->Level = 1 + Abc_MaxInt(pData0->Level, pData1->Level);
1110  if ( pData0->iGunc == -1 || pData1->iGunc == -1 )
1111  continue;
1112  iFanin0 = Abc_LitNotCond( pData0->iGunc, pObj->fCompl0 );
1113  iFanin1 = Abc_LitNotCond( pData1->iGunc, pObj->fCompl1 );
1114  // compute the resulting literal
1115  if ( iFanin0 == 0 || iFanin1 == 0 || iFanin0 == Abc_LitNot(iFanin1) )
1116  iLit = 0;
1117  else if ( iFanin0 == 1 || iFanin0 == iFanin1 )
1118  iLit = iFanin1;
1119  else if ( iFanin1 == 1 )
1120  iLit = iFanin0;
1121  else
1122  {
1123  iLit = Gia_ManHashLookup( p, Gia_ObjFromLit(p, iFanin0), Gia_ObjFromLit(p, iFanin1) );
1124  if ( iLit == 0 )
1125  iLit = -1;
1126  }
1127  pData->iGunc = iLit;
1128  if ( pData->iGunc >= 0 )
1129  {
1130  // update the level to be more accurate
1131  pData->Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, pData->iGunc)) );
1132  // mark the node if it is part of MFFC
1133 // pData->fMffc = Gia_ObjIsTravIdCurrentArray(p, Gia_Regular(pData->pGunc));
1134  }
1135  }
1136 }
1137 
1138 /**Function*************************************************************
1139 
1140  Synopsis [Evaluates one cut.]
1141 
1142  Description [Returns the best gain.]
1143 
1144  SideEffects []
1145 
1146  SeeAlso []
1147 
1148 ***********************************************************************/
1149 int Dar2_LibEval_rec( Dar_LibObj_t * pObj, int Out )
1150 {
1151  Dar_LibDat_t * pData;
1152  int Area;
1153  pData = s_DarLib->pDatas + pObj->Num;
1154  if ( pData->TravId == Out )
1155  return 0;
1156  pData->TravId = Out;
1157  if ( pObj->fTerm )
1158  return 0;
1159  assert( pObj->Num > 3 );
1160  if ( pData->iGunc >= 0 )//&& !pData->fMffc )
1161  return 0;
1162  // this is a new node - get a bound on the area of its branches
1163 // nNodesSaved--;
1164  Area = Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out );
1165 // if ( Area > nNodesSaved )
1166 // return 0xff;
1167  Area += Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out );
1168 // if ( Area > nNodesSaved )
1169 // return 0xff;
1170  return Area + 1;
1171 }
1172 
1173 /**Function*************************************************************
1174 
1175  Synopsis [Evaluates one cut.]
1176 
1177  Description [Returns the best gain.]
1178 
1179  SideEffects []
1180 
1181  SeeAlso []
1182 
1183 ***********************************************************************/
1184 int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 )
1185 {
1186  int p_OutBest = -1;
1187  int p_OutNumBest = -1;
1188  int p_LevelBest = 1000000;
1189  int p_GainBest = -1000000;
1190  int p_ClassBest = -1;
1191 // int fTraining = 0;
1192  Dar_LibObj_t * pObj;
1193  int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
1194 // abctime clk = Abc_Clock();
1195  assert( Vec_IntSize(vCutLits) == 4 );
1196  assert( (uTruth >> 16) == 0 );
1197  // check if the cut exits and assigns leaves and their levels
1198  if ( !Dar2_LibCutMatch(p, vCutLits, uTruth) )
1199  return -1;
1200  // mark MFFC of the node
1201 // nNodesSaved = Dar2_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL );
1202  nNodesSaved = 0;
1203  // evaluate the cut
1204  Class = s_DarLib->pMap[uTruth];
1205  Dar2_LibEvalAssignNums( p, Class );
1206  // profile outputs by their savings
1207 // p->nTotalSubgs += s_DarLib->nSubgr0[Class];
1208 // p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
1209  for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
1210  {
1211  pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
1212 // nNodesAdded = Dar2_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL );
1213  nNodesAdded = Dar2_LibEval_rec( pObj, Out );
1214  nNodesGained = nNodesSaved - nNodesAdded;
1215  if ( fKeepLevel )
1216  {
1217  if ( s_DarLib->pDatas[pObj->Num].Level > p_LevelBest ||
1218  (s_DarLib->pDatas[pObj->Num].Level == p_LevelBest && nNodesGained <= p_GainBest) )
1219  continue;
1220  }
1221  else
1222  {
1223  if ( nNodesGained < p_GainBest ||
1224  (nNodesGained == p_GainBest && s_DarLib->pDatas[pObj->Num].Level >= p_LevelBest) )
1225  continue;
1226  }
1227  // remember this possibility
1228  Vec_IntClear( vLeavesBest2 );
1229  for ( k = 0; k < Vec_IntSize(vCutLits); k++ )
1230  Vec_IntPush( vLeavesBest2, s_DarLib->pDatas[k].iGunc );
1231  p_OutBest = s_DarLib->pSubgr0[Class][Out];
1232  p_OutNumBest = Out;
1233  p_LevelBest = s_DarLib->pDatas[pObj->Num].Level;
1234  p_GainBest = nNodesGained;
1235  p_ClassBest = Class;
1236 // assert( p_LevelBest <= Required );
1237  }
1238 //clk = Abc_Clock() - clk;
1239 //p->ClassTimes[Class] += clk;
1240 //p->timeEval += clk;
1241  assert( p_OutBest != -1 );
1242  return p_OutBest;
1243 }
1244 
1245 /**Function*************************************************************
1246 
1247  Synopsis [Clears the fields of the nodes used i this cut.]
1248 
1249  Description []
1250 
1251  SideEffects []
1252 
1253  SeeAlso []
1254 
1255 ***********************************************************************/
1256 void Dar2_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter )
1257 {
1258  if ( pObj->fTerm )
1259  return;
1260  pObj->Num = (*pCounter)++;
1261  s_DarLib->pDatas[ pObj->Num ].iGunc = -1;
1262  Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter );
1263  Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter );
1264 }
1265 
1266 /**Function*************************************************************
1267 
1268  Synopsis [Reconstructs the best cut.]
1269 
1270  Description []
1271 
1272  SideEffects []
1273 
1274  SeeAlso []
1275 
1276 ***********************************************************************/
1277 int Dar2_LibBuildBest_rec( Gia_Man_t * p, Dar_LibObj_t * pObj )
1278 {
1279  Gia_Obj_t * pNode;
1280  Dar_LibDat_t * pData;
1281  int iFanin0, iFanin1;
1282  pData = s_DarLib->pDatas + pObj->Num;
1283  if ( pData->iGunc >= 0 )
1284  return pData->iGunc;
1285  iFanin0 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) );
1286  iFanin1 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) );
1287  iFanin0 = Abc_LitNotCond( iFanin0, pObj->fCompl0 );
1288  iFanin1 = Abc_LitNotCond( iFanin1, pObj->fCompl1 );
1289  pData->iGunc = Gia_ManHashAnd( p, iFanin0, iFanin1 );
1290  pNode = Gia_ManObj( p, Abc_Lit2Var(pData->iGunc) );
1291  if ( Gia_ObjIsAnd( pNode ) )
1292  Gia_ObjSetAndLevel( p, pNode );
1293  Gia_ObjSetPhase( p, pNode );
1294  return pData->iGunc;
1295 }
1296 
1297 /**Function*************************************************************
1298 
1299  Synopsis [Reconstructs the best cut.]
1300 
1301  Description []
1302 
1303  SideEffects []
1304 
1305  SeeAlso []
1306 
1307 ***********************************************************************/
1308 int Dar2_LibBuildBest( Gia_Man_t * p, Vec_Int_t * vLeavesBest2, int OutBest )
1309 {
1310  int i, iLeaf, Counter = 4;
1311  assert( Vec_IntSize(vLeavesBest2) == 4 );
1312  Vec_IntForEachEntry( vLeavesBest2, iLeaf, i )
1313  s_DarLib->pDatas[i].iGunc = iLeaf;
1314  Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, OutBest), &Counter );
1315  return Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, OutBest) );
1316 }
1317 
1318 /**Function*************************************************************
1319 
1320  Synopsis [Evaluate and build the new node.]
1321 
1322  Description []
1323 
1324  SideEffects []
1325 
1326  SeeAlso []
1327 
1328 ***********************************************************************/
1329 int Dar_LibEvalBuild( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 )
1330 {
1331  int OutBest = Dar2_LibEval( p, vCutLits, uTruth, fKeepLevel, vLeavesBest2 );
1332  return Dar2_LibBuildBest( p, vLeavesBest2, OutBest );
1333 }
1334 
1335 ////////////////////////////////////////////////////////////////////////
1336 /// END OF FILE ///
1337 ////////////////////////////////////////////////////////////////////////
1338 
1339 
1340 ABC_NAMESPACE_IMPL_END
1341 
Dar2_LibEvalAssignNums
void Dar2_LibEvalAssignNums(Gia_Man_t *p, int Class)
Definition: darLib.c:1088
memset
char * memset()
Dar_Lib_t_::pScore
int * pScore[222]
Definition: darLib.c:78
Dar_Lib_t
typedefABC_NAMESPACE_IMPL_START struct Dar_Lib_t_ Dar_Lib_t
DECLARATIONS ///.
Definition: darLib.c:32
Dar_LibObjPrint_rec
void Dar_LibObjPrint_rec(Dar_LibObj_t *pObj)
Definition: darLib.c:777
Aig_NodeMffcLabel
int Aig_NodeMffcLabel(Aig_Man_t *p, Aig_Obj_t *pNode, float *pPower)
Definition: aigMffc.c:211
Dar_LibReadNodes
Vec_Int_t * Dar_LibReadNodes()
Definition: darData.c:11094
Dar_LibDat_t_::Level
int Level
Definition: darLib.c:52
Dar_LibObj_t_::fTerm
unsigned fTerm
Definition: darLib.c:43
Dar_Lib_t_::pPlace
int * pPlace[222]
Definition: darLib.c:75
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Dar_LibSetup
void Dar_LibSetup(Dar_Lib_t *p, Vec_Int_t *vOuts, Vec_Int_t *vPrios)
Definition: darLib.c:284
Dar_LibStart
void Dar_LibStart()
MACRO DEFINITIONS ///.
Definition: darLib.c:593
Dar_LibObj_t_
Definition: darLib.c:36
Dar_Lib_t_::nNodes0
int nNodes0[222]
Definition: darLib.c:88
Dar_LibDat_t_::TravId
int TravId
Definition: darLib.c:53
Dar_LibBuildBest_rec
Aig_Obj_t * Dar_LibBuildBest_rec(Dar_Man_t *p, Dar_LibObj_t *pObj)
Definition: darLib.c:1005
Dar_LibCreateData
void Dar_LibCreateData(Dar_Lib_t *p, int nDatas)
Definition: darLib.c:432
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Dar_Truth4VarNPN
void Dar_Truth4VarNPN(unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)
Definition: darPrec.c:293
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dar_Lib_t_::pNodes0Mem
int * pNodes0Mem
Definition: darLib.c:90
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Dar_LibDat_t_
Definition: darLib.c:47
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Dar_LibDat_t_::iGunc
int iGunc
Definition: darLib.c:51
Gia_ObjFromLit
static Gia_Obj_t * Gia_ObjFromLit(Gia_Man_t *p, int iLit)
Definition: gia.h:496
Dar_LibObj
static Dar_LibObj_t * Dar_LibObj(Dar_Lib_t *p, int Id)
Definition: darLib.c:110
Dar_Lib_t_::puCanons
unsigned short * puCanons
Definition: darLib.c:102
Dar_Lib_t_::nNodes
int nNodes[222]
Definition: darLib.c:80
Dar_Lib_t_::pNodes0
int * pNodes0[222]
Definition: darLib.c:89
Dar_Cut_t_::uTruth
unsigned uTruth
Definition: darInt.h:58
Dar_LibReadOuts
Vec_Int_t * Dar_LibReadOuts()
Definition: darData.c:11115
Dar_Lib_t_::pMap
unsigned char * pMap
Definition: darLib.c:105
Dar_Lib_t_::nNodes0Total
int nNodes0Total
Definition: darLib.c:91
Dar_Lib_t_::pDatas
Dar_LibDat_t * pDatas
Definition: darLib.c:98
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Dar2_LibBuildBest_rec
int Dar2_LibBuildBest_rec(Gia_Man_t *p, Dar_LibObj_t *pObj)
Definition: darLib.c:1277
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Dar_LibSetup0_rec
void Dar_LibSetup0_rec(Dar_Lib_t *p, Dar_LibObj_t *pObj, int Class, int fCollect)
Definition: darLib.c:454
Dar_Lib_t_::nSubgr0
int nSubgr0[222]
Definition: darLib.c:93
Dar_Lib_t_::iObj
int iObj
Definition: darLib.c:64
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Dar_Lib_t_::pPlaceMem
int * pPlaceMem
Definition: darLib.c:74
Dar_Lib_t_::pPerms
char * pPerms
Definition: darLib.c:104
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
for
for(p=first;p->value< newval;p=p->next)
Gia_Obj_t_
Definition: gia.h:75
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Dar_Lib_t_::nNodes0Max
int nNodes0Max
Definition: darLib.c:86
Dar_LibObj_t_::Fan0
unsigned Fan0
Definition: darLib.c:38
Dar_LibDat_t_::fMffc
unsigned char fMffc
Definition: darLib.c:55
Dar_LibDumpPriorities
void Dar_LibDumpPriorities()
Definition: darLib.c:668
Dar_LibObj_t_::Fan1
unsigned Fan1
Definition: darLib.c:39
Dar_LibReturnCanonicals
void Dar_LibReturnCanonicals(unsigned *pCanons)
Definition: darLib.c:211
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Dar_Man_t
typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
INCLUDES ///.
Definition: darInt.h:51
Dar_Lib_t_::pScoreMem
int * pScoreMem
Definition: darLib.c:77
Dar_Cut_t_::pLeaves
int pLeaves[4]
Definition: darInt.h:63
Dar_LibEval_rec
int Dar_LibEval_rec(Dar_LibObj_t *pObj, int Out, int nNodesSaved, int Required, float *pPower)
Definition: darLib.c:863
Dar_Lib_t_::pNodesMem
int * pNodesMem
Definition: darLib.c:82
Dar_Lib_t_::nObjs
int nObjs
Definition: darLib.c:63
Dar_LibSetup_rec
void Dar_LibSetup_rec(Dar_Lib_t *p, Dar_LibObj_t *pObj, int Class, int fCollect)
Definition: darLib.c:260
Dar_LibCutMarkMffc
int Dar_LibCutMarkMffc(Aig_Man_t *p, Aig_Obj_t *pRoot, int nLeaves, float *pPower)
Definition: darLib.c:752
Dar_LibAddNode
void Dar_LibAddNode(Dar_Lib_t *p, int Id0, int Id1, int fCompl0, int fCompl1)
Definition: darLib.c:236
Dar_LibObj_t_::Num
unsigned Num
Definition: darLib.c:44
Gia_ObjSetPhase
void Gia_ObjSetPhase(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:346
Dar_Lib_t_::pObjs
Dar_LibObj_t * pObjs
Definition: darLib.c:62
Dar_Lib_t_::nDatas
int nDatas
Definition: darLib.c:99
Gia_ObjSetAndLevel
static void Gia_ObjSetAndLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:506
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Dar_LibEval
void Dar_LibEval(Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required, int *pnMffcSize)
Definition: darLib.c:920
Dar_LibReturnClass
int Dar_LibReturnClass(unsigned uTruth)
Definition: darLib.c:194
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Dar_LibDat_t_::dProb
float dProb
Definition: darLib.c:54
Dar2_LibEval_rec
int Dar2_LibEval_rec(Dar_LibObj_t *pObj, int Out)
Definition: darLib.c:1149
Dar_LibObj_t_::fCompl0
unsigned fCompl0
Definition: darLib.c:40
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Dar_LibBuildClear_rec
void Dar_LibBuildClear_rec(Dar_LibObj_t *pObj, int *pCounter)
Definition: darLib.c:984
Dar_Lib_t_::pSubgrMem
int * pSubgrMem
Definition: darLib.c:68
Counter
static int Counter
Definition: extraBddMisc.c:1877
Dar_Lib_t_::nSubgr
int nSubgr[222]
Definition: darLib.c:66
Dar_Lib_t_::nSubgrTotal
int nSubgrTotal
Definition: darLib.c:69
Aig_TableLookupTwo
Aig_Obj_t * Aig_TableLookupTwo(Aig_Man_t *p, Aig_Obj_t *pFanin0, Aig_Obj_t *pFanin1)
Definition: aigTable.c:146
Dar_LibIncrementScore
void Dar_LibIncrementScore(int Class, int Out, int Gain)
Definition: darLib.c:633
Dar_Cut_t_
Definition: darInt.h:55
Dar_Cut_t_::nLeaves
unsigned nLeaves
Definition: darInt.h:62
Dar_Lib_t_::pSubgr0
int * pSubgr0[222]
Definition: darLib.c:94
Dar_LibEvalBuild
int Dar_LibEvalBuild(Gia_Man_t *p, Vec_Int_t *vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t *vLeavesBest2)
DECLARATIONS ///.
Definition: darLib.c:1329
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Dar_Lib_t_::nNodesTotal
int nNodesTotal
Definition: darLib.c:83
Dar_LibCutMatch
int Dar_LibCutMatch(Dar_Man_t *p, Dar_Cut_t *pCut)
Definition: darLib.c:706
Dar_Permutations
char ** Dar_Permutations(int n)
Definition: darPrec.c:144
Dar_Lib_t_::pPerms4
char ** pPerms4
Definition: darLib.c:101
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_Lib_t_::pSubgr0Mem
int * pSubgr0Mem
Definition: darLib.c:95
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Dar_LibObj_t_::fCompl1
unsigned fCompl1
Definition: darLib.c:41
Dar_Lib_t_::nSubgr0Total
int nSubgr0Total
Definition: darLib.c:96
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Dar_Lib_t_::nSubgraphs
int nSubgraphs
Definition: darLib.c:85
Gia_ManHashLookup
int Gia_ManHashLookup(Gia_Man_t *p, Gia_Obj_t *p0, Gia_Obj_t *p1)
Definition: giaHash.c:79
Dar_LibEvalAssignNums
void Dar_LibEvalAssignNums(Dar_Man_t *p, int Class, Aig_Obj_t *pRoot)
Definition: darLib.c:806
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Dar_LibDat_t_::nLats
unsigned char nLats[3]
Definition: darLib.c:56
s_DarLib
static Dar_Lib_t * s_DarLib
Definition: darLib.c:108
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Abc_Int2Float
static float Abc_Int2Float(int Num)
Definition: abc_global.h:250
Dar_LibObj_t_::fPhase
unsigned fPhase
Definition: darLib.c:42
Dar_LibStop
void Dar_LibStop()
Definition: darLib.c:615
Dar_Lib_t_::pSubgr
int * pSubgr[222]
Definition: darLib.c:67
Dar_Lib_t_::pPhases
char * pPhases
Definition: darLib.c:103
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Dar2_LibEval
int Dar2_LibEval(Gia_Man_t *p, Vec_Int_t *vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t *vLeavesBest2)
Definition: darLib.c:1184
Dar2_LibCutMatch
int Dar2_LibCutMatch(Gia_Man_t *p, Vec_Int_t *vCutLits, unsigned uTruth)
Definition: darLib.c:1056
Dar_LibPrepare
void Dar_LibPrepare(int nSubgraphs)
Definition: darLib.c:478
Dar_Lib_t_
Definition: darLib.c:59
Dar_LibAlloc
Dar_Lib_t * Dar_LibAlloc(int nObjs)
FUNCTION DEFINITIONS ///.
Definition: darLib.c:128
Dar_LibObjTruth
static int Dar_LibObjTruth(Dar_LibObj_t *pObj)
Definition: darLib.c:111
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Dar_LibReadPrios
Vec_Int_t * Dar_LibReadPrios()
Definition: darData.c:11136
Dar_LibDat_t_::pFunc
Aig_Obj_t * pFunc
Definition: darLib.c:50
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Dar_LibFree
void Dar_LibFree(Dar_Lib_t *p)
Definition: darLib.c:164
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Dar_Lib_t_::pPriosMem
int * pPriosMem
Definition: darLib.c:71
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Dar2_LibBuildClear_rec
void Dar2_LibBuildClear_rec(Dar_LibObj_t *pObj, int *pCounter)
Definition: darLib.c:1256
Dar_Lib_t_::pPrios
int * pPrios[222]
Definition: darLib.c:72
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition: aig.h:81
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Dar2_LibBuildBest
int Dar2_LibBuildBest(Gia_Man_t *p, Vec_Int_t *vLeavesBest2, int OutBest)
Definition: darLib.c:1308
Dar_Lib_t_::pNodes
int * pNodes[222]
Definition: darLib.c:81
Dar_LibBuildBest
Aig_Obj_t * Dar_LibBuildBest(Dar_Man_t *p)
Definition: darLib.c:1031
Dar_LibRead
Dar_Lib_t * Dar_LibRead()
Definition: darLib.c:559