abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sswClass.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sswClass.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Inductive prover with constraints.]
8 
9  Synopsis [Representation of candidate equivalence classes.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - September 1, 2008.]
16 
17  Revision [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 /*
27  The candidate equivalence classes are stored as a vector of pointers
28  to the array of pointers to the nodes in each class.
29  The first node of the class is its representative node.
30  The representative has the smallest topological order among the class nodes.
31  The nodes inside each class are ordered according to their topological order.
32  The classes are ordered according to the topo order of their representatives.
33 */
34 
35 // internal representation of candidate equivalence classes
36 struct Ssw_Cla_t_
37 {
38  // class information
39  Aig_Man_t * pAig; // original AIG manager
40  Aig_Obj_t *** pId2Class; // non-const classes by ID of repr node
41  int * pClassSizes; // sizes of each equivalence class
42  int fConstCorr;
43  // statistics
44  int nClasses; // the total number of non-const classes
45  int nCands1; // the total number of const candidates
46  int nLits; // the number of literals in all classes
47  // memory
48  Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
49  Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
50  // temporary data
51  Vec_Ptr_t * vClassOld; // old equivalence class after splitting
52  Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
53  Vec_Ptr_t * vRefined; // the nodes refined since the last iteration
54  // procedures used for class refinement
55  void * pManData;
56  unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node
57  int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant
58  int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
59 };
60 
61 ////////////////////////////////////////////////////////////////////////
62 /// DECLARATIONS ///
63 ////////////////////////////////////////////////////////////////////////
64 
65 static inline Aig_Obj_t * Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
66 static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
67 
68 // iterator through the equivalence classes
69 #define Ssw_ManForEachClass( p, ppClass, i ) \
70  for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
71  if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
72 // iterator through the nodes in one class
73 #define Ssw_ClassForEachNode( p, pRepr, pNode, i ) \
74  for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
75  if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
76 
77 ////////////////////////////////////////////////////////////////////////
78 /// FUNCTION DEFINITIONS ///
79 ////////////////////////////////////////////////////////////////////////
80 
81 /**Function*************************************************************
82 
83  Synopsis [Creates one equivalence class.]
84 
85  Description []
86 
87  SideEffects []
88 
89  SeeAlso []
90 
91 ***********************************************************************/
92 static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
93 {
94  assert( p->pId2Class[pRepr->Id] == NULL );
95  assert( pClass[0] == pRepr );
96  p->pId2Class[pRepr->Id] = pClass;
97  assert( p->pClassSizes[pRepr->Id] == 0 );
98  assert( nSize > 1 );
99  p->pClassSizes[pRepr->Id] = nSize;
100  p->nClasses++;
101  p->nLits += nSize - 1;
102 }
103 
104 /**Function*************************************************************
105 
106  Synopsis [Removes one equivalence class.]
107 
108  Description []
109 
110  SideEffects []
111 
112  SeeAlso []
113 
114 ***********************************************************************/
115 static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
116 {
117  Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
118  int nSize;
119  assert( pClass != NULL );
120  p->pId2Class[pRepr->Id] = NULL;
121  nSize = p->pClassSizes[pRepr->Id];
122  assert( nSize > 1 );
123  p->nClasses--;
124  p->nLits -= nSize - 1;
125  p->pClassSizes[pRepr->Id] = 0;
126  return pClass;
127 }
128 
129 /**Function*************************************************************
130 
131  Synopsis [Starts representation of equivalence classes.]
132 
133  Description []
134 
135  SideEffects []
136 
137  SeeAlso []
138 
139 ***********************************************************************/
140 Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
141 {
142  Ssw_Cla_t * p;
143  p = ABC_ALLOC( Ssw_Cla_t, 1 );
144  memset( p, 0, sizeof(Ssw_Cla_t) );
145  p->pAig = pAig;
146  p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
147  p->pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
148  p->vClassOld = Vec_PtrAlloc( 100 );
149  p->vClassNew = Vec_PtrAlloc( 100 );
150  p->vRefined = Vec_PtrAlloc( 1000 );
151  if ( pAig->pReprs == NULL )
152  Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
153  return p;
154 }
155 
156 /**Function*************************************************************
157 
158  Synopsis [Starts representation of equivalence classes.]
159 
160  Description []
161 
162  SideEffects []
163 
164  SeeAlso []
165 
166 ***********************************************************************/
167 void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
168  unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
169  int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
170  int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
171 {
172  p->pManData = pManData;
173  p->pFuncNodeHash = pFuncNodeHash;
174  p->pFuncNodeIsConst = pFuncNodeIsConst;
175  p->pFuncNodesAreEqual = pFuncNodesAreEqual;
176 }
177 
178 /**Function*************************************************************
179 
180  Synopsis [Stop representation of equivalence classes.]
181 
182  Description []
183 
184  SideEffects []
185 
186  SeeAlso []
187 
188 ***********************************************************************/
189 void Ssw_ClassesStop( Ssw_Cla_t * p )
190 {
191  if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
192  if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
193  Vec_PtrFree( p->vRefined );
194  ABC_FREE( p->pId2Class );
195  ABC_FREE( p->pClassSizes );
196  ABC_FREE( p->pMemClasses );
197  ABC_FREE( p );
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [Stop representation of equivalence classes.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
212 {
213  return p->pAig;
214 }
215 
216 /**Function*************************************************************
217 
218  Synopsis []
219 
220  Description []
221 
222  SideEffects []
223 
224  SeeAlso []
225 
226 ***********************************************************************/
227 Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
228 {
229  return p->vRefined;
230 }
231 
232 /**Function*************************************************************
233 
234  Synopsis []
235 
236  Description []
237 
238  SideEffects []
239 
240  SeeAlso []
241 
242 ***********************************************************************/
243 void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
244 {
245  Vec_PtrClear( p->vRefined );
246 }
247 
248 /**Function*************************************************************
249 
250  Synopsis [Stop representation of equivalence classes.]
251 
252  Description []
253 
254  SideEffects []
255 
256  SeeAlso []
257 
258 ***********************************************************************/
259 int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
260 {
261  return p->nCands1;
262 }
263 
264 /**Function*************************************************************
265 
266  Synopsis [Stop representation of equivalence classes.]
267 
268  Description []
269 
270  SideEffects []
271 
272  SeeAlso []
273 
274 ***********************************************************************/
275 int Ssw_ClassesClassNum( Ssw_Cla_t * p )
276 {
277  return p->nClasses;
278 }
279 
280 /**Function*************************************************************
281 
282  Synopsis [Stop representation of equivalence classes.]
283 
284  Description []
285 
286  SideEffects []
287 
288  SeeAlso []
289 
290 ***********************************************************************/
291 int Ssw_ClassesLitNum( Ssw_Cla_t * p )
292 {
293  return p->nLits;
294 }
295 
296 /**Function*************************************************************
297 
298  Synopsis [Stop representation of equivalence classes.]
299 
300  Description []
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
307 Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
308 {
309  if ( p->pId2Class[pRepr->Id] == NULL )
310  return NULL;
311  assert( p->pId2Class[pRepr->Id] != NULL );
312  assert( p->pClassSizes[pRepr->Id] > 1 );
313  *pnSize = p->pClassSizes[pRepr->Id];
314  return p->pId2Class[pRepr->Id];
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis [Stop representation of equivalence classes.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
329 {
330  int i;
331  Vec_PtrClear( vClass );
332  if ( p->pId2Class[pRepr->Id] == NULL )
333  return;
334  assert( p->pClassSizes[pRepr->Id] > 1 );
335  for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
336  Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
337 }
338 
339 /**Function*************************************************************
340 
341  Synopsis [Checks candidate equivalence classes.]
342 
343  Description []
344 
345  SideEffects []
346 
347  SeeAlso []
348 
349 ***********************************************************************/
350 void Ssw_ClassesCheck( Ssw_Cla_t * p )
351 {
352  Aig_Obj_t * pObj, * pPrev, ** ppClass;
353  int i, k, nLits, nClasses, nCands1;
354  nClasses = nLits = 0;
355  Ssw_ManForEachClass( p, ppClass, k )
356  {
357  pPrev = NULL;
358  assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
359  Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
360  {
361  if ( i == 0 )
362  assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
363  else
364  {
365  assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
366  assert( pPrev->Id < pObj->Id );
367  nLits++;
368  }
369  pPrev = pObj;
370  }
371  nClasses++;
372  }
373  nCands1 = 0;
374  Aig_ManForEachObj( p->pAig, pObj, i )
375  nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
376  assert( p->nLits == nLits );
377  assert( p->nCands1 == nCands1 );
378  assert( p->nClasses == nClasses );
379 }
380 
381 /**Function*************************************************************
382 
383  Synopsis [Prints simulation classes.]
384 
385  Description []
386 
387  SideEffects []
388 
389  SeeAlso []
390 
391 ***********************************************************************/
392 void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
393 {
394  Aig_Obj_t * pObj;
395  int i;
396  Abc_Print( 1, "{ " );
397  Ssw_ClassForEachNode( p, pRepr, pObj, i )
398  Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
399  Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
400  Abc_Print( 1, "}\n" );
401 }
402 
403 /**Function*************************************************************
404 
405  Synopsis [Prints simulation classes.]
406 
407  Description []
408 
409  SideEffects []
410 
411  SeeAlso []
412 
413 ***********************************************************************/
414 void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
415 {
416  Aig_Obj_t ** ppClass;
417  Aig_Obj_t * pObj;
418  int i;
419  Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
420  p->nCands1, p->nClasses, p->nCands1+p->nLits );
421  if ( !fVeryVerbose )
422  return;
423  Abc_Print( 1, "Constants { " );
424  Aig_ManForEachObj( p->pAig, pObj, i )
425  if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
426  Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
427  Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
428  Abc_Print( 1, "}\n" );
429  Ssw_ManForEachClass( p, ppClass, i )
430  {
431  Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
432  Ssw_ClassesPrintOne( p, ppClass[0] );
433  }
434  Abc_Print( 1, "\n" );
435 }
436 
437 /**Function*************************************************************
438 
439  Synopsis [Prints simulation classes.]
440 
441  Description []
442 
443  SideEffects []
444 
445  SeeAlso []
446 
447 ***********************************************************************/
448 void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
449 {
450  Aig_Obj_t * pRepr, * pTemp;
451  assert( p->pClassSizes[pObj->Id] == 0 );
452  assert( p->pId2Class[pObj->Id] == NULL );
453  pRepr = Aig_ObjRepr( p->pAig, pObj );
454  assert( pRepr != NULL );
455 // Vec_PtrPush( p->vRefined, pObj );
456  if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
457  {
458  assert( p->pClassSizes[pRepr->Id] == 0 );
459  assert( p->pId2Class[pRepr->Id] == NULL );
460  Aig_ObjSetRepr( p->pAig, pObj, NULL );
461  p->nCands1--;
462  return;
463  }
464 // Vec_PtrPush( p->vRefined, pRepr );
465  Aig_ObjSetRepr( p->pAig, pObj, NULL );
466  assert( p->pId2Class[pRepr->Id][0] == pRepr );
467  assert( p->pClassSizes[pRepr->Id] >= 2 );
468  if ( p->pClassSizes[pRepr->Id] == 2 )
469  {
470  p->pId2Class[pRepr->Id] = NULL;
471  p->nClasses--;
472  p->pClassSizes[pRepr->Id] = 0;
473  p->nLits--;
474  }
475  else
476  {
477  int i, k = 0;
478  // remove the entry from the class
479  Ssw_ClassForEachNode( p, pRepr, pTemp, i )
480  if ( pTemp != pObj )
481  p->pId2Class[pRepr->Id][k++] = pTemp;
482  assert( k + 1 == p->pClassSizes[pRepr->Id] );
483  // reduce the class
484  p->pClassSizes[pRepr->Id]--;
485  p->nLits--;
486  }
487 }
488 
489 /**Function*************************************************************
490 
491  Synopsis [Takes the set of const1 cands and rehashes them using sim info.]
492 
493  Description []
494 
495  SideEffects []
496 
497  SeeAlso []
498 
499 ***********************************************************************/
500 int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
501 {
502 // Aig_Man_t * pAig = p->pAig;
503  Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
504  Aig_Obj_t * pObj, * pTemp, * pRepr;
505  int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
506 
507  // allocate the hash table hashing simulation info into nodes
508  nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
509  ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
510  ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
511 
512  // sort through the candidates
513  nEntries = 0;
514  p->nCands1 = 0;
515  Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
516  {
517  assert( p->pClassSizes[pObj->Id] == 0 );
518  Aig_ObjSetRepr( p->pAig, pObj, NULL );
519  // check if the node belongs to the class of constant 1
520  if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
521  {
522  Ssw_ObjSetConst1Cand( p->pAig, pObj );
523  p->nCands1++;
524  continue;
525  }
526  if ( fConstCorr )
527  continue;
528  // hash the node by its simulation info
529  iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
530  // add the node to the class
531  if ( ppTable[iEntry] == NULL )
532  {
533  ppTable[iEntry] = pObj;
534  }
535  else
536  {
537  // set the representative of this node
538  pRepr = ppTable[iEntry];
539  Aig_ObjSetRepr( p->pAig, pObj, pRepr );
540  // add node to the table
541  if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
542  { // this will be the second entry
543  p->pClassSizes[pRepr->Id]++;
544  nEntries++;
545  }
546  // add the entry to the list
547  Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
548  Ssw_ObjSetNext( ppNexts, pRepr, pObj );
549  p->pClassSizes[pRepr->Id]++;
550  nEntries++;
551  }
552  }
553 
554  // copy the entries into storage in the topological order
555  nEntries2 = 0;
556  Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
557  {
558  nNodes = p->pClassSizes[pObj->Id];
559  // skip the nodes that are not representatives of non-trivial classes
560  if ( nNodes == 0 )
561  continue;
562  assert( nNodes > 1 );
563  // add the nodes to the class in the topological order
564  ppClassNew = p->pMemClassesFree + nEntries2;
565  ppClassNew[0] = pObj;
566  for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
567  pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
568  {
569  ppClassNew[nNodes-k] = pTemp;
570  }
571  // add the class of nodes
572  p->pClassSizes[pObj->Id] = 0;
573  Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
574  // increment the number of entries
575  nEntries2 += nNodes;
576  }
577  p->pMemClassesFree += nEntries2;
578  assert( nEntries == nEntries2 );
579  ABC_FREE( ppTable );
580  ABC_FREE( ppNexts );
581  // now it is time to refine the classes
582  return Ssw_ClassesRefine( p, 1 );
583 }
584 
585 /**Function*************************************************************
586 
587  Synopsis [Creates initial simulation classes.]
588 
589  Description [Assumes that simulation info is assigned.]
590 
591  SideEffects []
592 
593  SeeAlso []
594 
595 ***********************************************************************/
596 Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
597 {
598 // int nFrames = 4;
599 // int nWords = 1;
600 // int nIters = 16;
601 
602 // int nFrames = 32;
603 // int nWords = 4;
604 // int nIters = 0;
605 
606  int nFrames = Abc_MaxInt( nFramesK, 4 );
607  int nWords = 2;
608  int nIters = 16;
609  Ssw_Cla_t * p;
610  Ssw_Sml_t * pSml;
611  Vec_Ptr_t * vCands;
612  Aig_Obj_t * pObj;
613  int i, k, RetValue;
614  abctime clk;
615 
616  // start the classes
617  p = Ssw_ClassesStart( pAig );
618  p->fConstCorr = fConstCorr;
619 
620  // perform sequential simulation
621 clk = Abc_Clock();
622  pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
623 if ( fVerbose )
624 {
625  Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
626  1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
627  Abc_Print( 1, "Initial simulation of %d frames with %d words. ", nFrames, nWords );
628  ABC_PRT( "Time", Abc_Clock() - clk );
629 }
630 
631  // set comparison procedures
632 clk = Abc_Clock();
633  Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
634 
635  // collect nodes to be considered as candidates
636  vCands = Vec_PtrAlloc( 1000 );
637  Aig_ManForEachObj( p->pAig, pObj, i )
638  {
639  if ( fLatchCorr )
640  {
641  if ( !Saig_ObjIsLo(p->pAig, pObj) )
642  continue;
643  }
644  else
645  {
646  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
647  continue;
648  // skip the node with more that the given number of levels
649  if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
650  continue;
651  }
652  Vec_PtrPush( vCands, pObj );
653  }
654 
655  // this change will consider all PO drivers
656  if ( fOutputCorr )
657  {
658  Vec_PtrClear( vCands );
659  Aig_ManForEachObj( p->pAig, pObj, i )
660  pObj->fMarkB = 0;
661  Saig_ManForEachPo( p->pAig, pObj, i )
662  if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
663  Aig_ObjFanin0(pObj)->fMarkB = 1;
664  Aig_ManForEachObj( p->pAig, pObj, i )
665  if ( pObj->fMarkB )
666  Vec_PtrPush( vCands, pObj );
667  Aig_ManForEachObj( p->pAig, pObj, i )
668  pObj->fMarkB = 0;
669  }
670 
671  // allocate room for classes
672  p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
673  p->pMemClassesFree = p->pMemClasses;
674 
675  // now it is time to refine the classes
676  Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
677 if ( fVerbose )
678 {
679  Abc_Print( 1, "Collecting candidate equivalence classes. " );
680 ABC_PRT( "Time", Abc_Clock() - clk );
681 }
682 
683 clk = Abc_Clock();
684  // perform iterative refinement using simulation
685  for ( i = 1; i < nIters; i++ )
686  {
687  // collect const1 candidates
688  Vec_PtrClear( vCands );
689  Aig_ManForEachObj( p->pAig, pObj, k )
690  if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
691  Vec_PtrPush( vCands, pObj );
692  assert( Vec_PtrSize(vCands) == p->nCands1 );
693  // perform new round of simulation
694  Ssw_SmlResimulateSeq( pSml );
695  // check equivalence classes
696  RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
697  if ( RetValue == 0 )
698  break;
699  }
700  Ssw_SmlStop( pSml );
701  Vec_PtrFree( vCands );
702 if ( fVerbose )
703 {
704  Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
705  nFrames, nWords, i-1 );
706  ABC_PRT( "Time", Abc_Clock() - clk );
707 }
708  Ssw_ClassesCheck( p );
709 // Ssw_ClassesPrint( p, 0 );
710  return p;
711 }
712 
713 /**Function*************************************************************
714 
715  Synopsis [Creates initial simulation classes.]
716 
717  Description [Assumes that simulation info is assigned.]
718 
719  SideEffects []
720 
721  SeeAlso []
722 
723 ***********************************************************************/
724 Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
725 {
726  Ssw_Cla_t * p;
727  Aig_Obj_t * pObj;
728  int i;
729  // start the classes
730  p = Ssw_ClassesStart( pAig );
731  // go through the nodes
732  p->nCands1 = 0;
733  Aig_ManForEachObj( pAig, pObj, i )
734  {
735  if ( fLatchCorr )
736  {
737  if ( !Saig_ObjIsLo(pAig, pObj) )
738  continue;
739  }
740  else
741  {
742  if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
743  continue;
744  // skip the node with more that the given number of levels
745  if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
746  continue;
747  }
748  Ssw_ObjSetConst1Cand( pAig, pObj );
749  p->nCands1++;
750  }
751  // allocate room for classes
752  p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
753 // Ssw_ClassesPrint( p, 0 );
754  return p;
755 }
756 
757 /**Function*************************************************************
758 
759  Synopsis [Creates initial simulation classes.]
760 
761  Description [Assumes that simulation info is assigned.]
762 
763  SideEffects []
764 
765  SeeAlso []
766 
767 ***********************************************************************/
768 Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig )
769 {
770  Ssw_Cla_t * p;
771  Aig_Obj_t * pObj, * pRepr;
772  int * pClassSizes, nEntries, i;
773  // start the classes
774  p = Ssw_ClassesStart( pAig );
775  // allocate memory for classes
776  p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
777  // count classes
778  p->nCands1 = 0;
779  Aig_ManForEachObj( pAig, pObj, i )
780  {
781  if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
782  {
783  p->nCands1++;
784  continue;
785  }
786  if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
787  {
788  if ( p->pClassSizes[pRepr->Id]++ == 0 )
789  p->pClassSizes[pRepr->Id]++;
790  }
791  }
792  // add nodes
793  nEntries = 0;
794  p->nClasses = 0;
795  pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
796  Aig_ManForEachObj( pAig, pObj, i )
797  {
798  if ( p->pClassSizes[i] )
799  {
800  p->pId2Class[i] = p->pMemClasses + nEntries;
801  nEntries += p->pClassSizes[i];
802  p->pId2Class[i][pClassSizes[i]++] = pObj;
803  p->nClasses++;
804  continue;
805  }
806  if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
807  continue;
808  if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
809  p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
810  }
811  p->pMemClassesFree = p->pMemClasses + nEntries;
812  p->nLits = nEntries - p->nClasses;
813  assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
814  ABC_FREE( pClassSizes );
815 // Abc_Print( 1, "After converting:\n" );
816 // Ssw_ClassesPrint( p, 0 );
817  return p;
818 }
819 
820 /**Function*************************************************************
821 
822  Synopsis [Creates initial simulation classes.]
823 
824  Description [Assumes that simulation info is assigned.]
825 
826  SideEffects []
827 
828  SeeAlso []
829 
830 ***********************************************************************/
831 Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
832 {
833  Ssw_Cla_t * p;
834  Aig_Obj_t * pObj;
835  int i;
836  // start the classes
837  p = Ssw_ClassesStart( pAig );
838  // go through the nodes
839  p->nCands1 = 0;
840  Saig_ManForEachPo( pAig, pObj, i )
841  {
842  Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
843  p->nCands1++;
844  }
845  // allocate room for classes
846  p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
847 // Ssw_ClassesPrint( p, 0 );
848  return p;
849 }
850 
851 /**Function*************************************************************
852 
853  Synopsis [Creates classes from the temporary representation.]
854 
855  Description []
856 
857  SideEffects []
858 
859  SeeAlso []
860 
861 ***********************************************************************/
862 Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
863 {
864  Ssw_Cla_t * p;
865  Aig_Obj_t ** ppClassNew;
866  Aig_Obj_t * pObj, * pRepr, * pPrev;
867  int i, k, nTotalObjs, nEntries, Entry;
868  // start the classes
869  p = Ssw_ClassesStart( pAig );
870  // count the number of entries in the classes
871  nTotalObjs = 0;
872  for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
873  nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
874  // allocate memory for classes
875  p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
876  // create constant-1 class
877  if ( pvClasses[0] )
878  Vec_IntForEachEntry( pvClasses[0], Entry, i )
879  {
880  assert( (i == 0) == (Entry == 0) );
881  if ( i == 0 )
882  continue;
883  pObj = Aig_ManObj( pAig, Entry );
884  Ssw_ObjSetConst1Cand( pAig, pObj );
885  p->nCands1++;
886  }
887  // create classes
888  nEntries = 0;
889  for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
890  {
891  if ( pvClasses[i] == NULL )
892  continue;
893  // get room for storing the class
894  ppClassNew = p->pMemClasses + nEntries;
895  nEntries += Vec_IntSize( pvClasses[i] );
896  // store the nodes of the class
897  pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
898  ppClassNew[0] = pRepr;
899  Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
900  {
901  pObj = Aig_ManObj( pAig, Entry );
902  assert( pPrev->Id < pObj->Id );
903  pPrev = pObj;
904  ppClassNew[k] = pObj;
905  Aig_ObjSetRepr( pAig, pObj, pRepr );
906  }
907  // create new class
908  Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
909  }
910  // prepare room for new classes
911  p->pMemClassesFree = p->pMemClasses + nEntries;
912  Ssw_ClassesCheck( p );
913 // Ssw_ClassesPrint( p, 0 );
914  return p;
915 }
916 
917 /**Function*************************************************************
918 
919  Synopsis [Creates classes from the temporary representation.]
920 
921  Description []
922 
923  SideEffects []
924 
925  SeeAlso []
926 
927 ***********************************************************************/
928 Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
929 {
930  Ssw_Cla_t * p;
931  Aig_Obj_t ** ppClassNew;
932  Aig_Obj_t * pObj, * pRepr;
933  int i;
934  // start the classes
935  p = Ssw_ClassesStart( pMiter );
936  // allocate memory for classes
937  p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
938  // create classes
939  for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
940  {
941  pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
942  pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
943  assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
944  Aig_ObjSetRepr( pMiter, pObj, pRepr );
945  // get room for storing the class
946  ppClassNew = p->pMemClasses + i;
947  ppClassNew[0] = pRepr;
948  ppClassNew[1] = pObj;
949  // create new class
950  Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
951  }
952  // prepare room for new classes
953  p->pMemClassesFree = NULL;
954  Ssw_ClassesCheck( p );
955 // Ssw_ClassesPrint( p, 0 );
956  return p;
957 }
958 
959 /**Function*************************************************************
960 
961  Synopsis [Iteratively refines the classes after simulation.]
962 
963  Description [Returns the number of refinements performed.]
964 
965  SideEffects []
966 
967  SeeAlso []
968 
969 ***********************************************************************/
970 int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
971 {
972  Aig_Obj_t ** pClassOld, ** pClassNew;
973  Aig_Obj_t * pObj, * pReprNew;
974  int i;
975 
976  // split the class
977  Vec_PtrClear( p->vClassOld );
978  Vec_PtrClear( p->vClassNew );
979  Ssw_ClassForEachNode( p, pReprOld, pObj, i )
980  if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
981  Vec_PtrPush( p->vClassOld, pObj );
982  else
983  Vec_PtrPush( p->vClassNew, pObj );
984  // check if splitting happened
985  if ( Vec_PtrSize(p->vClassNew) == 0 )
986  return 0;
987  // remember that this class is refined
988 // Ssw_ClassForEachNode( p, pReprOld, pObj, i )
989 // Vec_PtrPush( p->vRefined, pObj );
990 
991  // get the new representative
992  pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
993  assert( Vec_PtrSize(p->vClassOld) > 0 );
994  assert( Vec_PtrSize(p->vClassNew) > 0 );
995 
996  // create old class
997  pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
998  Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
999  {
1000  pClassOld[i] = pObj;
1001  Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
1002  }
1003  // create new class
1004  pClassNew = pClassOld + i;
1005  Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1006  {
1007  pClassNew[i] = pObj;
1008  Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1009  }
1010 
1011  // put classes back
1012  if ( Vec_PtrSize(p->vClassOld) > 1 )
1013  Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
1014  if ( Vec_PtrSize(p->vClassNew) > 1 )
1015  Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
1016 
1017  // check if the class should be recursively refined
1018  if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
1019  return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1020  return 1;
1021 }
1022 
1023 /**Function*************************************************************
1024 
1025  Synopsis [Refines the classes after simulation.]
1026 
1027  Description []
1028 
1029  SideEffects []
1030 
1031  SeeAlso []
1032 
1033 ***********************************************************************/
1034 int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
1035 {
1036  Aig_Obj_t ** ppClass;
1037  int i, nRefis = 0;
1038  Ssw_ManForEachClass( p, ppClass, i )
1039  nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
1040  return nRefis;
1041 }
1042 
1043 /**Function*************************************************************
1044 
1045  Synopsis [Refines the classes after simulation.]
1046 
1047  Description []
1048 
1049  SideEffects []
1050 
1051  SeeAlso []
1052 
1053 ***********************************************************************/
1054 int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
1055 {
1056  Aig_Obj_t * pObj;
1057  int i, nRefis = 0;
1058  Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
1059  nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
1060  return nRefis;
1061 }
1062 
1063 /**Function*************************************************************
1064 
1065  Synopsis [Refine the group of constant 1 nodes.]
1066 
1067  Description []
1068 
1069  SideEffects []
1070 
1071  SeeAlso []
1072 
1073 ***********************************************************************/
1074 int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
1075 {
1076  Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1077  int i;
1078  if ( Vec_PtrSize(vRoots) == 0 )
1079  return 0;
1080  // collect the nodes to be refined
1081  Vec_PtrClear( p->vClassNew );
1082  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
1083  if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1084  Vec_PtrPush( p->vClassNew, pObj );
1085  // check if there is a new class
1086  if ( Vec_PtrSize(p->vClassNew) == 0 )
1087  return 0;
1088  p->nCands1 -= Vec_PtrSize(p->vClassNew);
1089  pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1090  Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1091  if ( Vec_PtrSize(p->vClassNew) == 1 )
1092  return 1;
1093  // create a new class composed of these nodes
1094  ppClassNew = p->pMemClassesFree;
1095  p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1096  Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1097  {
1098  ppClassNew[i] = pObj;
1099  Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1100  }
1101  Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1102  // refine them recursively
1103  if ( fRecursive )
1104  return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1105  return 1;
1106 }
1107 
1108 /**Function*************************************************************
1109 
1110  Synopsis [Refine the group of constant 1 nodes.]
1111 
1112  Description []
1113 
1114  SideEffects []
1115 
1116  SeeAlso []
1117 
1118 ***********************************************************************/
1119 int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
1120 {
1121  Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1122  int i;
1123  // collect the nodes to be refined
1124  Vec_PtrClear( p->vClassNew );
1125  for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
1126  if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
1127  {
1128  pObj = Aig_ManObj( p->pAig, i );
1129  if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1130  {
1131  Vec_PtrPush( p->vClassNew, pObj );
1132 // Vec_PtrPush( p->vRefined, pObj );
1133  }
1134  }
1135  // check if there is a new class
1136  if ( Vec_PtrSize(p->vClassNew) == 0 )
1137  return 0;
1138  if ( p->fConstCorr )
1139  {
1140  Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1141  Aig_ObjSetRepr( p->pAig, pObj, NULL );
1142  return 1;
1143  }
1144  p->nCands1 -= Vec_PtrSize(p->vClassNew);
1145  pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1146  Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1147  if ( Vec_PtrSize(p->vClassNew) == 1 )
1148  return 1;
1149  // create a new class composed of these nodes
1150  ppClassNew = p->pMemClassesFree;
1151  p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1152  Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1153  {
1154  ppClassNew[i] = pObj;
1155  Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1156  }
1157  Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1158  // refine them recursively
1159  if ( fRecursive )
1160  return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1161  return 1;
1162 }
1163 
1164 
1165 ////////////////////////////////////////////////////////////////////////
1166 /// END OF FILE ///
1167 ////////////////////////////////////////////////////////////////////////
1168 
1169 
1170 ABC_NAMESPACE_IMPL_END
memset
char * memset()
Ssw_SmlObjHashWord
unsigned Ssw_SmlObjHashWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: sswSim.c:63
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Ssw_ClassesRefineGroup
int Ssw_ClassesRefineGroup(Ssw_Cla_t *p, Vec_Ptr_t *vReprs, int fRecursive)
Definition: sswClass.c:1054
Ssw_ClassesClassNum
int Ssw_ClassesClassNum(Ssw_Cla_t *p)
Definition: sswClass.c:275
Aig_ObjRepr
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Ssw_SmlSimulateSeq
Ssw_Sml_t * Ssw_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords)
Definition: sswSim.c:1248
Ssw_Cla_t_::pId2Class
Aig_Obj_t *** pId2Class
Definition: sswClass.c:40
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ssw_ClassesCand1Num
int Ssw_ClassesCand1Num(Ssw_Cla_t *p)
Definition: sswClass.c:259
Ssw_Cla_t_::pFuncNodeHash
unsigned(* pFuncNodeHash)(void *, Aig_Obj_t *)
Definition: sswClass.c:56
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Ssw_ObjAddClass
static void Ssw_ObjAddClass(Ssw_Cla_t *p, Aig_Obj_t *pRepr, Aig_Obj_t **pClass, int nSize)
FUNCTION DEFINITIONS ///.
Definition: sswClass.c:92
Ssw_Cla_t_::nLits
int nLits
Definition: sswClass.c:46
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_Cla_t_::pFuncNodesAreEqual
int(* pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *)
Definition: sswClass.c:58
Ssw_ClassesRefineConst1Group
int Ssw_ClassesRefineConst1Group(Ssw_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
Definition: sswClass.c:1074
Ssw_ObjSetConst1Cand
static void Ssw_ObjSetConst1Cand(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: sswInt.h:176
Ssw_ClassesStop
void Ssw_ClassesStop(Ssw_Cla_t *p)
Definition: sswClass.c:189
Ssw_ClassesPrepareRehash
int Ssw_ClassesPrepareRehash(Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
Definition: sswClass.c:500
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Ssw_Cla_t_::nCands1
int nCands1
Definition: sswClass.c:45
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
Ssw_ManForEachClass
#define Ssw_ManForEachClass(p, ppClass, i)
Definition: sswClass.c:69
Ssw_ClassesRefine
int Ssw_ClassesRefine(Ssw_Cla_t *p, int fRecursive)
Definition: sswClass.c:1034
Ssw_ClassesPreparePairsSimple
Ssw_Cla_t * Ssw_ClassesPreparePairsSimple(Aig_Man_t *pMiter, Vec_Int_t *vPairs)
Definition: sswClass.c:928
Ssw_ClassesPrepareTargets
Ssw_Cla_t * Ssw_ClassesPrepareTargets(Aig_Man_t *pAig)
Definition: sswClass.c:831
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
Ssw_Cla_t_::pMemClassesFree
Aig_Obj_t ** pMemClassesFree
Definition: sswClass.c:49
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ssw_ClassesPreparePairs
Ssw_Cla_t * Ssw_ClassesPreparePairs(Aig_Man_t *pAig, Vec_Int_t **pvClasses)
Definition: sswClass.c:862
Ssw_Cla_t_::pManData
void * pManData
Definition: sswClass.c:55
Ssw_SmlObjIsConstWord
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:102
nWords
int nWords
Definition: abcNpn.c:127
Aig_SupportSize
int Aig_SupportSize(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigDfs.c:758
Ssw_Cla_t_::nClasses
int nClasses
Definition: sswClass.c:44
Ssw_ClassesRemoveNode
void Ssw_ClassesRemoveNode(Ssw_Cla_t *p, Aig_Obj_t *pObj)
Definition: sswClass.c:448
Aig_NodeMffcSupp
int Aig_NodeMffcSupp(Aig_Man_t *p, Aig_Obj_t *pNode, int LevelMin, Vec_Ptr_t *vSupp)
Definition: aigMffc.c:179
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Ssw_ClassesPrintOne
void Ssw_ClassesPrintOne(Ssw_Cla_t *p, Aig_Obj_t *pRepr)
Definition: sswClass.c:392
Ssw_Cla_t_::pClassSizes
int * pClassSizes
Definition: sswClass.c:41
Ssw_Cla_t_::pAig
Aig_Man_t * pAig
Definition: sswClass.c:39
Ssw_ClassesClearRefined
void Ssw_ClassesClearRefined(Ssw_Cla_t *p)
Definition: sswClass.c:243
Aig_ObjSetRepr
static void Aig_ObjSetRepr(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
Definition: aig.h:331
Ssw_Cla_t_::fConstCorr
int fConstCorr
Definition: sswClass.c:42
Aig_ManReprStart
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition: aigRepr.c:45
Ssw_ClassesPrepare
Ssw_Cla_t * Ssw_ClassesPrepare(Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
Definition: sswClass.c:596
Ssw_SmlObjsAreEqualWord
int Ssw_SmlObjsAreEqualWord(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: sswSim.c:124
Ssw_ClassesSetData
void Ssw_ClassesSetData(Ssw_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
Definition: sswClass.c:167
Ssw_ClassesPrint
void Ssw_ClassesPrint(Ssw_Cla_t *p, int fVeryVerbose)
Definition: sswClass.c:414
Ssw_ClassesRefineOneClass
int Ssw_ClassesRefineOneClass(Ssw_Cla_t *p, Aig_Obj_t *pReprOld, int fRecursive)
Definition: sswClass.c:970
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Ssw_ClassesCheck
void Ssw_ClassesCheck(Ssw_Cla_t *p)
Definition: sswClass.c:350
memcmp
int memcmp()
Aig_Obj_t_
Definition: aig.h:69
Ssw_Cla_t_
Definition: sswClass.c:36
Ssw_Cla_t_::vRefined
Vec_Ptr_t * vRefined
Definition: sswClass.c:53
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Ssw_Cla_t_::vClassNew
Vec_Ptr_t * vClassNew
Definition: sswClass.c:52
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Ssw_Cla_t_::vClassOld
Vec_Ptr_t * vClassOld
Definition: sswClass.c:51
Ssw_Cla_t_::pFuncNodeIsConst
int(* pFuncNodeIsConst)(void *, Aig_Obj_t *)
Definition: sswClass.c:57
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Ssw_SmlStop
void Ssw_SmlStop(Ssw_Sml_t *p)
Definition: sswSim.c:1211
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Ssw_ClassesPrepareFromReprs
Ssw_Cla_t * Ssw_ClassesPrepareFromReprs(Aig_Man_t *pAig)
Definition: sswClass.c:768
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
Ssw_ClassesPrepareSimple
Ssw_Cla_t * Ssw_ClassesPrepareSimple(Aig_Man_t *pAig, int fLatchCorr, int nMaxLevs)
Definition: sswClass.c:724
Ssw_ClassesReadClass
Aig_Obj_t ** Ssw_ClassesReadClass(Ssw_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
Definition: sswClass.c:307
Ssw_ObjSetNext
static void Ssw_ObjSetNext(Aig_Obj_t **ppNexts, Aig_Obj_t *pObj, Aig_Obj_t *pNext)
Definition: sswClass.c:66
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Ssw_ClassesStart
Ssw_Cla_t * Ssw_ClassesStart(Aig_Man_t *pAig)
Definition: sswClass.c:140
Ssw_Cla_t_::pMemClasses
Aig_Obj_t ** pMemClasses
Definition: sswClass.c:48
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ssw_ClassesCollectClass
void Ssw_ClassesCollectClass(Ssw_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vClass)
Definition: sswClass.c:328
Ssw_ClassForEachNode
#define Ssw_ClassForEachNode(p, pRepr, pNode, i)
Definition: sswClass.c:73
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Aig_ObjIsCand
static int Aig_ObjIsCand(Aig_Obj_t *pObj)
Definition: aig.h:284
Ssw_ObjIsConst1Cand
static int Ssw_ObjIsConst1Cand(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: sswInt.h:172
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Ssw_ObjNext
static Aig_Obj_t * Ssw_ObjNext(Aig_Obj_t **ppNexts, Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition: sswClass.c:65
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Ssw_SmlResimulateSeq
void Ssw_SmlResimulateSeq(Ssw_Sml_t *p)
Definition: sswSim.c:1269
Ssw_ObjRemoveClass
static Aig_Obj_t ** Ssw_ObjRemoveClass(Ssw_Cla_t *p, Aig_Obj_t *pRepr)
Definition: sswClass.c:115
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Ssw_ClassesGetRefined
Vec_Ptr_t * Ssw_ClassesGetRefined(Ssw_Cla_t *p)
Definition: sswClass.c:227
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Ssw_ClassesRefineConst1
int Ssw_ClassesRefineConst1(Ssw_Cla_t *p, int fRecursive)
Definition: sswClass.c:1119
Ssw_Sml_t_
DECLARATIONS ///.
Definition: sswSim.c:31
Ssw_ClassesLitNum
int Ssw_ClassesLitNum(Ssw_Cla_t *p)
Definition: sswClass.c:291
Ssw_ClassesReadAig
Aig_Man_t * Ssw_ClassesReadAig(Ssw_Cla_t *p)
Definition: sswClass.c:211
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223