abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaEquiv.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaEquiv.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Manipulation of equivalence classes.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaEquiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "proof/cec/cec.h"
23 #include "sat/bmc/bmc.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Returns 1 if AIG is not in the required topo order.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
47 {
48  Gia_Obj_t * pRepr;
49  if ( pObj->Value == 0 )
50  return 1;
51  pObj->Value = 0;
52  assert( Gia_ObjIsAnd(pObj) );
53  if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) )
54  return 0;
55  if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
56  return 0;
57  pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL;
58  return pRepr == NULL || pRepr->Value == 0;
59 }
60 
61 /**Function*************************************************************
62 
63  Synopsis [Returns 0 if AIG is not in the required topo order.]
64 
65  Description [AIG should be in such an order that the representative
66  is always traversed before the node.]
67 
68  SideEffects []
69 
70  SeeAlso []
71 
72 ***********************************************************************/
73 int Gia_ManCheckTopoOrder( Gia_Man_t * p )
74 {
75  Gia_Obj_t * pObj;
76  int i, RetValue = 1;
77  Gia_ManFillValue( p );
78  Gia_ManConst0(p)->Value = 0;
79  Gia_ManForEachCi( p, pObj, i )
80  pObj->Value = 0;
81  Gia_ManForEachCo( p, pObj, i )
82  RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) );
83  return RetValue;
84 }
85 
86 /**Function*************************************************************
87 
88  Synopsis [Given representatives, derives pointers to the next objects.]
89 
90  Description []
91 
92  SideEffects []
93 
94  SeeAlso []
95 
96 ***********************************************************************/
97 int * Gia_ManDeriveNexts( Gia_Man_t * p )
98 {
99  unsigned * pNexts, * pTails;
100  int i;
101  assert( p->pReprs != NULL );
102  assert( p->pNexts == NULL );
103  pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
104  pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
105  for ( i = 0; i < Gia_ManObjNum(p); i++ )
106  pTails[i] = i;
107  for ( i = 0; i < Gia_ManObjNum(p); i++ )
108  {
109  if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
110  continue;
111  pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
112  pTails[p->pReprs[i].iRepr] = i;
113  }
114  ABC_FREE( pTails );
115  return (int *)pNexts;
116 }
117 
118 /**Function*************************************************************
119 
120  Synopsis [Given points to the next objects, derives representatives.]
121 
122  Description []
123 
124  SideEffects []
125 
126  SeeAlso []
127 
128 ***********************************************************************/
129 void Gia_ManDeriveReprs( Gia_Man_t * p )
130 {
131  int i, iObj;
132  assert( p->pReprs == NULL );
133  assert( p->pNexts != NULL );
134  p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
135  for ( i = 0; i < Gia_ManObjNum(p); i++ )
136  Gia_ObjSetRepr( p, i, GIA_VOID );
137  for ( i = 0; i < Gia_ManObjNum(p); i++ )
138  {
139  if ( p->pNexts[i] == 0 )
140  continue;
141  if ( p->pReprs[i].iRepr != GIA_VOID )
142  continue;
143  // next is set, repr is not set
144  for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
145  p->pReprs[iObj].iRepr = i;
146  }
147 }
148 
149 /**Function*************************************************************
150 
151  Synopsis []
152 
153  Description []
154 
155  SideEffects []
156 
157  SeeAlso []
158 
159 ***********************************************************************/
160 int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
161 {
162  int i, nLits = 0;
163  for ( i = 0; i < Gia_ManObjNum(p); i++ )
164  nLits += (Gia_ObjRepr(p, i) != GIA_VOID);
165  return nLits;
166 }
167 
168 /**Function*************************************************************
169 
170  Synopsis []
171 
172  Description []
173 
174  SideEffects []
175 
176  SeeAlso []
177 
178 ***********************************************************************/
179 int Gia_ManEquivCountClasses( Gia_Man_t * p )
180 {
181  int i, Counter = 0;
182  if ( p->pReprs == NULL )
183  return 0;
184  for ( i = 1; i < Gia_ManObjNum(p); i++ )
185  Counter += Gia_ObjIsHead(p, i);
186  return Counter;
187 }
188 
189 /**Function*************************************************************
190 
191  Synopsis []
192 
193  Description []
194 
195  SideEffects []
196 
197  SeeAlso []
198 
199 ***********************************************************************/
200 int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
201 {
202  int nLitsReal = Gia_ManEquivCountLitsAll( p );
203  if ( nLitsReal != nLits )
204  Abc_Print( 1, "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
205  return 1;
206 }
207 
208 /**Function*************************************************************
209 
210  Synopsis []
211 
212  Description []
213 
214  SideEffects []
215 
216  SeeAlso []
217 
218 ***********************************************************************/
219 void Gia_ManPrintStatsClasses( Gia_Man_t * p )
220 {
221  int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
222  for ( i = 1; i < Gia_ManObjNum(p); i++ )
223  {
224  if ( Gia_ObjIsHead(p, i) )
225  Counter++;
226  else if ( Gia_ObjIsConst(p, i) )
227  Counter0++;
228  else if ( Gia_ObjIsNone(p, i) )
229  CounterX++;
230  if ( Gia_ObjProved(p, i) )
231  Proved++;
232  }
233  CounterX -= Gia_ManCoNum(p);
234  nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
235 
236 // Abc_Print( 1, "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
237 // Abc_Print( 1, "and =%5d ", Gia_ManAndNum(p) );
238 // Abc_Print( 1, "lev =%3d ", Gia_ManLevelNum(p) );
239  Abc_Print( 1, "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
240 }
241 
242 /**Function*************************************************************
243 
244  Synopsis []
245 
246  Description []
247 
248  SideEffects []
249 
250  SeeAlso []
251 
252 ***********************************************************************/
253 int Gia_ManEquivCountLits( Gia_Man_t * p )
254 {
255  int i, Counter = 0, Counter0 = 0, CounterX = 0;
256  if ( p->pReprs == NULL || p->pNexts == NULL )
257  return 0;
258  for ( i = 1; i < Gia_ManObjNum(p); i++ )
259  {
260  if ( Gia_ObjIsHead(p, i) )
261  Counter++;
262  else if ( Gia_ObjIsConst(p, i) )
263  Counter0++;
264  else if ( Gia_ObjIsNone(p, i) )
265  CounterX++;
266  }
267  CounterX -= Gia_ManCoNum(p);
268  return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
269 }
270 
271 /**Function*************************************************************
272 
273  Synopsis []
274 
275  Description []
276 
277  SideEffects []
278 
279  SeeAlso []
280 
281 ***********************************************************************/
282 int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
283 {
284  int Ent, nLits = 1;
285  Gia_ClassForEachObj1( p, i, Ent )
286  {
287  assert( Gia_ObjRepr(p, Ent) == i );
288  nLits++;
289  }
290  return nLits;
291 }
292 void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
293 {
294  int Ent;
295  Abc_Print( 1, "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
296  Gia_ClassForEachObj( p, i, Ent )
297  {
298  Abc_Print( 1," %d", Ent );
299  if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
300  Abc_Print( 1," <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
301  }
302  Abc_Print( 1, " }\n" );
303 }
304 void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
305 {
306  int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
307  for ( i = 1; i < Gia_ManObjNum(p); i++ )
308  {
309  if ( Gia_ObjIsHead(p, i) )
310  Counter++;
311  else if ( Gia_ObjIsConst(p, i) )
312  Counter0++;
313  else if ( Gia_ObjIsNone(p, i) )
314  CounterX++;
315  if ( Gia_ObjProved(p, i) )
316  Proved++;
317  }
318  CounterX -= Gia_ManCoNum(p);
319  nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
320  Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
321  Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
322  assert( Gia_ManEquivCheckLits( p, nLits ) );
323  if ( fVerbose )
324  {
325 // int Ent;
326  Abc_Print( 1, "Const0 = " );
327  Gia_ManForEachConst( p, i )
328  Abc_Print( 1, "%d ", i );
329  Abc_Print( 1, "\n" );
330  Counter = 0;
331  Gia_ManForEachClass( p, i )
332  Gia_ManEquivPrintOne( p, i, ++Counter );
333 /*
334  Gia_ManLevelNum( p );
335  Gia_ManForEachClass( p, i )
336  if ( i % 100 == 0 )
337  {
338 // Abc_Print( 1, "%d ", Gia_ManEquivCountOne(p, i) );
339  Gia_ClassForEachObj( p, i, Ent )
340  {
341  Abc_Print( 1, "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
342  }
343  Abc_Print( 1, "\n" );
344  }
345 */
346  }
347 }
348 
349 /**Function*************************************************************
350 
351  Synopsis [Returns representative node.]
352 
353  Description []
354 
355  SideEffects []
356 
357  SeeAlso []
358 
359 ***********************************************************************/
360 static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
361 {
362  if ( fUseAll )
363  {
364  if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
365  return NULL;
366  }
367  else
368  {
369  if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
370  return NULL;
371  }
372 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
373  if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
374  return NULL;
375  return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
376 }
377 
378 /**Function*************************************************************
379 
380  Synopsis [Duplicates the AIG in the DFS order.]
381 
382  Description []
383 
384  SideEffects []
385 
386  SeeAlso []
387 
388 ***********************************************************************/
389 void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
390 {
391  Gia_Obj_t * pRepr;
392  if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
393  {
394  Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
395  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
396  return;
397  }
398  if ( ~pObj->Value )
399  return;
400  assert( Gia_ObjIsAnd(pObj) );
401  Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
402  Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
403  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Reduces AIG using equivalence classes.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
418 {
419  Gia_Man_t * pNew;
420  Gia_Obj_t * pObj;
421  int i;
422  if ( !p->pReprs )
423  {
424  Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
425  return NULL;
426  }
427  if ( fDualOut && (Gia_ManPoNum(p) & 1) )
428  {
429  Abc_Print( 1, "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
430  return NULL;
431  }
432  // check if there are any equivalences defined
433  Gia_ManForEachObj( p, pObj, i )
434  if ( Gia_ObjReprObj(p, i) != NULL )
435  break;
436  if ( i == Gia_ManObjNum(p) )
437  {
438 // Abc_Print( 1, "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
439  return NULL;
440  }
441 /*
442  if ( !Gia_ManCheckTopoOrder( p ) )
443  {
444  Abc_Print( 1, "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
445  return NULL;
446  }
447 */
448  if ( !fSkipPhase )
449  Gia_ManSetPhase( p );
450  if ( fDualOut )
451  Gia_ManEquivSetColors( p, fVerbose );
452  pNew = Gia_ManStart( Gia_ManObjNum(p) );
453  pNew->pName = Abc_UtilStrsav( p->pName );
454  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
455  Gia_ManFillValue( p );
456  Gia_ManConst0(p)->Value = 0;
457  Gia_ManForEachCi( p, pObj, i )
458  pObj->Value = Gia_ManAppendCi(pNew);
459  Gia_ManHashAlloc( pNew );
460  Gia_ManForEachCo( p, pObj, i )
461  Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
462  Gia_ManForEachCo( p, pObj, i )
463  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
464  Gia_ManHashStop( pNew );
465  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
466  return pNew;
467 }
468 
469 /**Function*************************************************************
470 
471  Synopsis [Reduces AIG using equivalence classes.]
472 
473  Description []
474 
475  SideEffects []
476 
477  SeeAlso []
478 
479 ***********************************************************************/
480 void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
481 {
482  Gia_Obj_t * pObj0, * pObj1;
483  int i;
484  assert( (Gia_ManPoNum(p) & 1) == 0 );
485  Gia_ManForEachPo( p, pObj0, i )
486  {
487  pObj1 = Gia_ManPo( p, ++i );
488  if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) )
489  continue;
490  pObj0->iDiff0 = Gia_ObjId(p, pObj0);
491  pObj0->fCompl0 = 0;
492  pObj1->iDiff0 = Gia_ObjId(p, pObj1);
493  pObj1->fCompl0 = 0;
494  }
495 }
496 
497 /**Function*************************************************************
498 
499  Synopsis [Removes pointers to the unmarked nodes..]
500 
501  Description []
502 
503  SideEffects []
504 
505  SeeAlso []
506 
507 ***********************************************************************/
508 void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
509 {
510  Gia_Obj_t * pObj, * pObjNew;
511  int i;
512  Gia_ManForEachObj( p, pObj, i )
513  {
514  if ( !~pObj->Value )
515  continue;
516  pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
517  if ( pObjNew->fMark0 )
518  pObj->Value = ~0;
519  }
520 }
521 
522 /**Function*************************************************************
523 
524  Synopsis [Removes pointers to the unmarked nodes..]
525 
526  Description []
527 
528  SideEffects []
529 
530  SeeAlso []
531 
532 ***********************************************************************/
533 void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal )
534 {
535  Vec_Int_t * vClass;
536  Gia_Obj_t * pObj, * pObjNew;
537  int i, k, iNode, iRepr, iPrev;
538  // start representatives
539  pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) );
540  for ( i = 0; i < Gia_ManObjNum(pFinal); i++ )
541  Gia_ObjSetRepr( pFinal, i, GIA_VOID );
542  // iterate over constant candidates
543  Gia_ManForEachConst( p, i )
544  {
545  pObj = Gia_ManObj( p, i );
546  if ( !~pObj->Value )
547  continue;
548  pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
549  if ( Abc_Lit2Var(pObjNew->Value) == 0 )
550  continue;
551  Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 );
552  }
553  // iterate over class candidates
554  vClass = Vec_IntAlloc( 100 );
555  Gia_ManForEachClass( p, i )
556  {
557  Vec_IntClear( vClass );
558  Gia_ClassForEachObj( p, i, k )
559  {
560  pObj = Gia_ManObj( p, k );
561  if ( !~pObj->Value )
562  continue;
563  pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
564  Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) );
565  }
566  if ( Vec_IntSize( vClass ) < 2 )
567  continue;
568  Vec_IntSort( vClass, 0 );
569  iRepr = iPrev = Vec_IntEntry( vClass, 0 );
570  Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
571  {
572  Gia_ObjSetRepr( pFinal, iNode, iRepr );
573  assert( iPrev < iNode );
574  iPrev = iNode;
575  }
576  }
577  Vec_IntFree( vClass );
578  pFinal->pNexts = Gia_ManDeriveNexts( pFinal );
579 }
580 
581 /**Function*************************************************************
582 
583  Synopsis [Removes pointers to the unmarked nodes..]
584 
585  Description []
586 
587  SideEffects []
588 
589  SeeAlso []
590 
591 ***********************************************************************/
592 Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
593 {
594  Gia_Man_t * pNew;
595  Vec_Int_t * vClass;
596  int i, k, iNode, iRepr, iPrev;
597  pNew = Gia_ManDupDfs( p );
598  // start representatives
599  pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
600  for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
601  Gia_ObjSetRepr( pNew, i, GIA_VOID );
602  // iterate over constant candidates
603  Gia_ManForEachConst( p, i )
604  Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
605  // iterate over class candidates
606  vClass = Vec_IntAlloc( 100 );
607  Gia_ManForEachClass( p, i )
608  {
609  Vec_IntClear( vClass );
610  Gia_ClassForEachObj( p, i, k )
611  Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
612  assert( Vec_IntSize( vClass ) > 1 );
613  Vec_IntSort( vClass, 0 );
614  iRepr = iPrev = Vec_IntEntry( vClass, 0 );
615  Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
616  {
617  Gia_ObjSetRepr( pNew, iNode, iRepr );
618  assert( iPrev < iNode );
619  iPrev = iNode;
620  }
621  }
622  Vec_IntFree( vClass );
623  pNew->pNexts = Gia_ManDeriveNexts( pNew );
624  return pNew;
625 }
626 
627 /**Function*************************************************************
628 
629  Synopsis [Reduces AIG while remapping equivalence classes.]
630 
631  Description [Drops the pairs of outputs if they are proved equivalent.]
632 
633  SideEffects []
634 
635  SeeAlso []
636 
637 ***********************************************************************/
638 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
639 {
640  Gia_Man_t * pNew, * pFinal;
641  pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
642  if ( pNew == NULL )
643  return NULL;
644  if ( fMiterPairs )
645  Gia_ManEquivFixOutputPairs( pNew );
646  if ( fSeq )
647  Gia_ManSeqMarkUsed( pNew );
648  else
649  Gia_ManCombMarkUsed( pNew );
650  Gia_ManEquivUpdatePointers( p, pNew );
651  pFinal = Gia_ManDupMarked( pNew );
652  Gia_ManEquivDeriveReprs( p, pNew, pFinal );
653  Gia_ManStop( pNew );
654  pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
655  Gia_ManStop( pNew );
656  return pFinal;
657 }
658 
659 /**Function*************************************************************
660 
661  Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
662 
663  Description []
664 
665  SideEffects []
666 
667  SeeAlso []
668 
669 ***********************************************************************/
670 int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
671 {
672  if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) )
673  return 0;
674  if ( Gia_ObjIsRo(p, pObj) )
675  return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds );
676  assert( Gia_ObjIsAnd(pObj) );
677  return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds )
678  + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds );
679 }
680 
681 /**Function*************************************************************
682 
683  Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
684 
685  Description []
686 
687  SideEffects []
688 
689  SeeAlso []
690 
691 ***********************************************************************/
692 int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
693 {
694  Gia_Obj_t * pObj;
695  int i, nNodes[2], nDiffs[2];
696  assert( (Gia_ManPoNum(p) & 1) == 0 );
697  Gia_ObjSetColors( p, 0 );
698  Gia_ManForEachPi( p, pObj, i )
699  Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
700  nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
701  Gia_ManForEachPo( p, pObj, i )
702  nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
703 // Gia_ManForEachObj( p, pObj, i )
704 // if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
705 // assert( Gia_ObjColors(p, i) );
706  nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
707  nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
708  if ( fVerbose )
709  {
710  Abc_Print( 1, "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
711  Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
712  Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
713  }
714  return (nDiffs[0] + nDiffs[1]) / 2;
715 }
716 
717 /**Function*************************************************************
718 
719  Synopsis [Duplicates the AIG in the DFS order.]
720 
721  Description []
722 
723  SideEffects []
724 
725  SeeAlso []
726 
727 ***********************************************************************/
728 static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
729 {
730  Gia_Obj_t * pRepr;
731  unsigned iLitNew;
732  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
733  if ( pRepr == NULL )
734  return;
735 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
736  if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
737  return;
738  iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
739  if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
740  {
741  if ( vTrace )
742  Vec_IntPush( vTrace, 1 );
743  if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
744  {
745  if ( vMap )
746  Vec_IntPush( vMap, Gia_ObjId(p, pObj) );
747  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
748  }
749  }
750  else
751  {
752  if ( vTrace )
753  Vec_IntPush( vTrace, 0 );
754  }
755  if ( fSpeculate )
756  pObj->Value = iLitNew;
757 }
758 
759 /**Function*************************************************************
760 
761  Synopsis [Duplicates the AIG in the DFS order.]
762 
763  Description []
764 
765  SideEffects []
766 
767  SeeAlso []
768 
769 ***********************************************************************/
770 void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
771 {
772  if ( ~pObj->Value )
773  return;
774  assert( Gia_ObjIsAnd(pObj) );
775  Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
776  Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
777  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
778  Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
779 }
780 
781 /**Function*************************************************************
782 
783  Synopsis [Reduces AIG using equivalence classes.]
784 
785  Description []
786 
787  SideEffects []
788 
789  SeeAlso []
790 
791 ***********************************************************************/
792 Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap )
793 {
794  Vec_Int_t * vXorLits;
795  Gia_Man_t * pNew, * pTemp;
796  Gia_Obj_t * pObj;
797  int i, iLitNew;
798  if ( !p->pReprs )
799  {
800  Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
801  return NULL;
802  }
803  Vec_IntClear( vTrace );
804  vXorLits = Vec_IntAlloc( 1000 );
805  Gia_ManSetPhase( p );
806  Gia_ManFillValue( p );
807  pNew = Gia_ManStart( Gia_ManObjNum(p) );
808  pNew->pName = Abc_UtilStrsav( p->pName );
809  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
810  Gia_ManHashAlloc( pNew );
811  Gia_ManConst0(p)->Value = 0;
812  Gia_ManForEachCi( p, pObj, i )
813  pObj->Value = Gia_ManAppendCi(pNew);
814  Gia_ManForEachRo( p, pObj, i )
815  Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap );
816  Gia_ManForEachCo( p, pObj, i )
817  Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap );
818  Gia_ManForEachPo( p, pObj, i )
819  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
820  Vec_IntForEachEntry( vXorLits, iLitNew, i )
821  Gia_ManAppendCo( pNew, iLitNew );
822  if ( Vec_IntSize(vXorLits) == 0 )
823  {
824  Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
825  Gia_ManAppendCo( pNew, 0 );
826  }
827  Gia_ManForEachRi( p, pObj, i )
828  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
829  Gia_ManHashStop( pNew );
830  Vec_IntFree( vXorLits );
831  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
832  pNew = Gia_ManCleanup( pTemp = pNew );
833  Gia_ManStop( pTemp );
834  return pNew;
835 }
836 
837 /**Function*************************************************************
838 
839  Synopsis [Reduces AIG using equivalence classes.]
840 
841  Description []
842 
843  SideEffects []
844 
845  SeeAlso []
846 
847 ***********************************************************************/
848 Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose )
849 {
850  Gia_Man_t * pNew, * pTemp;
851  Gia_Obj_t * pObj;
852  Vec_Int_t * vXorLits;
853  int i, iLitNew;
854  Vec_Int_t * vTrace = NULL, * vGuide = NULL;
855  if ( !p->pReprs )
856  {
857  Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
858  return NULL;
859  }
860  if ( fDualOut && (Gia_ManPoNum(p) & 1) )
861  {
862  Abc_Print( 1, "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
863  return NULL;
864  }
865  if ( fSkipSome )
866  {
867  vGuide = Vec_IntAlloc( 100 );
868  pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL );
869  Gia_ManStop( pTemp );
870  assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) );
871  vTrace = Vec_IntAlloc( 100 );
872  }
873  vXorLits = Vec_IntAlloc( 1000 );
874  Gia_ManSetPhase( p );
875  Gia_ManFillValue( p );
876  if ( fDualOut )
877  Gia_ManEquivSetColors( p, fVerbose );
878  pNew = Gia_ManStart( Gia_ManObjNum(p) );
879  pNew->pName = Abc_UtilStrsav( p->pName );
880  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
881  Gia_ManHashAlloc( pNew );
882  Gia_ManConst0(p)->Value = 0;
883  Gia_ManForEachCi( p, pObj, i )
884  pObj->Value = Gia_ManAppendCi(pNew);
885  Gia_ManForEachRo( p, pObj, i )
886  Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
887  Gia_ManForEachCo( p, pObj, i )
888  Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
889  if ( !fSynthesis )
890  {
891  Gia_ManForEachPo( p, pObj, i )
892  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
893  }
894  Vec_IntForEachEntry( vXorLits, iLitNew, i )
895  Gia_ManAppendCo( pNew, iLitNew );
896  if ( Vec_IntSize(vXorLits) == 0 )
897  {
898  Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
899  Gia_ManAppendCo( pNew, 0 );
900  }
901  Gia_ManForEachRi( p, pObj, i )
902  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
903  Gia_ManHashStop( pNew );
904  Vec_IntFree( vXorLits );
905  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
906  pNew = Gia_ManCleanup( pTemp = pNew );
907  Gia_ManStop( pTemp );
908 
909  // update using trace
910  if ( fSkipSome )
911  {
912  // count the number of non-zero entries
913  int iLit, nAddPos = 0;
914  Vec_IntForEachEntry( vGuide, iLit, i )
915  if ( iLit )
916  nAddPos++;
917  if ( nAddPos )
918  assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nAddPos );
919  }
920  Vec_IntFreeP( &vTrace );
921  Vec_IntFreeP( &vGuide );
922  return pNew;
923 }
924 
925 /**Function*************************************************************
926 
927  Synopsis [Duplicates the AIG in the DFS order.]
928 
929  Description []
930 
931  SideEffects []
932 
933  SeeAlso []
934 
935 ***********************************************************************/
936 void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
937 {
938  Gia_Obj_t * pRepr;
939  int iLitNew;
940  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
941  if ( pRepr == NULL )
942  return;
943 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
944  if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
945  return;
946  iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
947  if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
948  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
949  Gia_ObjSetCopyF( p, f, pObj, iLitNew );
950 }
951 
952 /**Function*************************************************************
953 
954  Synopsis [Duplicates the AIG in the DFS order.]
955 
956  Description []
957 
958  SideEffects []
959 
960  SeeAlso []
961 
962 ***********************************************************************/
963 void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
964 {
965  if ( ~Gia_ObjCopyF(p, f, pObj) )
966  return;
967  assert( Gia_ObjIsAnd(pObj) );
968  Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
969  Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
970  Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
971  Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
972 }
973 
974 /**Function*************************************************************
975 
976  Synopsis [Creates initialized SRM with the given number of frames.]
977 
978  Description []
979 
980  SideEffects []
981 
982  SeeAlso []
983 
984 ***********************************************************************/
985 Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut )
986 {
987  Gia_Man_t * pNew, * pTemp;
988  Gia_Obj_t * pObj, * pObjRi, * pObjRo;
989  Vec_Int_t * vXorLits;
990  int f, i, iLitNew;
991  if ( !p->pReprs )
992  {
993  Abc_Print( 1, "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
994  return NULL;
995  }
996  if ( Gia_ManRegNum(p) == 0 )
997  {
998  Abc_Print( 1, "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
999  return NULL;
1000  }
1001  if ( Gia_ManRegNum(p) != pInit->nRegs )
1002  {
1003  Abc_Print( 1, "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
1004  return NULL;
1005  }
1006  if ( fDualOut && (Gia_ManPoNum(p) & 1) )
1007  {
1008  Abc_Print( 1, "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
1009  return NULL;
1010  }
1011 
1012 /*
1013  if ( !Gia_ManCheckTopoOrder( p ) )
1014  {
1015  Abc_Print( 1, "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
1016  return NULL;
1017  }
1018 */
1019  assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
1020  Vec_IntFill( &p->vCopies, nFrames * Gia_ManObjNum(p), -1 );
1021  vXorLits = Vec_IntAlloc( 1000 );
1022  Gia_ManSetPhase( p );
1023  if ( fDualOut )
1024  Gia_ManEquivSetColors( p, 0 );
1025  pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
1026  pNew->pName = Abc_UtilStrsav( p->pName );
1027  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1028  Gia_ManHashAlloc( pNew );
1029  Gia_ManForEachRo( p, pObj, i )
1030  Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
1031  for ( f = 0; f < nFrames; f++ )
1032  {
1033  Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
1034  Gia_ManForEachPi( p, pObj, i )
1035  Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
1036  Gia_ManForEachRo( p, pObj, i )
1037  Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
1038  Gia_ManForEachCo( p, pObj, i )
1039  {
1040  Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
1041  Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
1042  }
1043  if ( f == nFrames - 1 )
1044  break;
1045  Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
1046  Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
1047  }
1048  Vec_IntForEachEntry( vXorLits, iLitNew, i )
1049  Gia_ManAppendCo( pNew, iLitNew );
1050  if ( Vec_IntSize(vXorLits) == 0 )
1051  {
1052 // Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1053  Gia_ManAppendCo( pNew, 0 );
1054  }
1055  Vec_IntErase( &p->vCopies );
1056  Vec_IntFree( vXorLits );
1057  Gia_ManHashStop( pNew );
1058  pNew = Gia_ManCleanup( pTemp = pNew );
1059  Gia_ManStop( pTemp );
1060  return pNew;
1061 }
1062 
1063 /**Function*************************************************************
1064 
1065  Synopsis [Creates initialized SRM with the given number of frames.]
1066 
1067  Description [Uses as many frames as needed to create the number of
1068  output not less than the number of equivalence literals.]
1069 
1070  SideEffects []
1071 
1072  SeeAlso []
1073 
1074 ***********************************************************************/
1075 Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
1076 {
1077  Gia_Man_t * pFrames;
1078  int f, nLits;
1079  nLits = Gia_ManEquivCountLits( p );
1080  for ( f = 1; ; f++ )
1081  {
1082  pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
1083  if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
1084  (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
1085  break;
1086  if ( f == nFramesMax )
1087  break;
1088  if ( Gia_ManAndNum(pFrames) > 500000 )
1089  {
1090  Gia_ManStop( pFrames );
1091  return NULL;
1092  }
1093  Gia_ManStop( pFrames );
1094  pFrames = NULL;
1095  }
1096  if ( f == nFramesMax )
1097  Abc_Print( 1, "Stopped unrolling after %d frames.\n", nFramesMax );
1098  if ( pnFrames )
1099  *pnFrames = f;
1100  return pFrames;
1101 }
1102 
1103 /**Function*************************************************************
1104 
1105  Synopsis [Transforms equiv classes by removing the AB nodes.]
1106 
1107  Description []
1108 
1109  SideEffects []
1110 
1111  SeeAlso []
1112 
1113 ***********************************************************************/
1114 void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
1115 {
1116  extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass );
1117  Vec_Int_t * vClass, * vClassNew;
1118  int iRepr, iNode, Ent, k;
1119  int nRemovedLits = 0, nRemovedClas = 0;
1120  int nTotalLits = 0, nTotalClas = 0;
1121  Gia_Obj_t * pObj;
1122  int i;
1123  assert( p->pReprs && p->pNexts );
1124  vClass = Vec_IntAlloc( 100 );
1125  vClassNew = Vec_IntAlloc( 100 );
1126  Gia_ManForEachObj( p, pObj, i )
1127  if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
1128  assert( Gia_ObjColors(p, i) );
1129  Gia_ManForEachClassReverse( p, iRepr )
1130  {
1131  nTotalClas++;
1132  Vec_IntClear( vClass );
1133  Vec_IntClear( vClassNew );
1134  Gia_ClassForEachObj( p, iRepr, iNode )
1135  {
1136  nTotalLits++;
1137  Vec_IntPush( vClass, iNode );
1138  assert( Gia_ObjColors(p, iNode) );
1139  if ( Gia_ObjColors(p, iNode) != 3 )
1140  Vec_IntPush( vClassNew, iNode );
1141  else
1142  nRemovedLits++;
1143  }
1144  Vec_IntForEachEntry( vClass, Ent, k )
1145  {
1146  p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0;
1147  p->pReprs[Ent].iRepr = GIA_VOID;
1148  p->pNexts[Ent] = 0;
1149  }
1150  if ( Vec_IntSize(vClassNew) < 2 )
1151  {
1152  nRemovedClas++;
1153  continue;
1154  }
1155  Cec_ManSimClassCreate( p, vClassNew );
1156  }
1157  Vec_IntFree( vClass );
1158  Vec_IntFree( vClassNew );
1159  if ( fVerbose )
1160  Abc_Print( 1, "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
1161  nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
1162 }
1163 
1164 /**Function*************************************************************
1165 
1166  Synopsis [Marks proved equivalences.]
1167 
1168  Description []
1169 
1170  SideEffects []
1171 
1172  SeeAlso []
1173 
1174 ***********************************************************************/
1175 void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose )
1176 {
1177  Gia_Man_t * pMiter, * pTemp;
1178  Gia_Obj_t * pObj;
1179  int i, iLit, nAddPos, nLits = 0;
1180  int nLitsAll, Counter = 0;
1181  nLitsAll = Gia_ManEquivCountLitsAll( p );
1182  if ( nLitsAll == 0 )
1183  {
1184  Abc_Print( 1, "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
1185  return;
1186  }
1187  // read AIGER file
1188  pMiter = Gia_AigerRead( pFileName, 0, 0 );
1189  if ( pMiter == NULL )
1190  {
1191  Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
1192  return;
1193  }
1194  if ( fSkipSome )
1195  {
1196  Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
1197  pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL );
1198  Gia_ManStop( pTemp );
1199  assert( Vec_IntSize(vTrace) == nLitsAll );
1200  // count the number of non-zero entries
1201  nAddPos = 0;
1202  Vec_IntForEachEntry( vTrace, iLit, i )
1203  if ( iLit )
1204  nAddPos++;
1205  // check the number
1206  if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos )
1207  {
1208  Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
1209  Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos );
1210  Gia_ManStop( pMiter );
1211  Vec_IntFreeP( &vTrace );
1212  return;
1213  }
1214  // mark corresponding POs as solved
1215  nLits = iLit = Counter = 0;
1216  for ( i = 0; i < Gia_ManObjNum(p); i++ )
1217  {
1218  if ( Gia_ObjRepr(p, i) == GIA_VOID )
1219  continue;
1220  if ( Vec_IntEntry( vTrace, nLits++ ) == 0 )
1221  continue;
1222  pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + iLit++ );
1223  if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1224  {
1225  Gia_ObjSetProved(p, i);
1226  Counter++;
1227  }
1228  }
1229  assert( nLits == nLitsAll );
1230  assert( iLit == nAddPos );
1231  Vec_IntFreeP( &vTrace );
1232  }
1233  else
1234  {
1235  if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
1236  {
1237  Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
1238  Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
1239  Gia_ManStop( pMiter );
1240  return;
1241  }
1242  // mark corresponding POs as solved
1243  nLits = 0;
1244  for ( i = 0; i < Gia_ManObjNum(p); i++ )
1245  {
1246  if ( Gia_ObjRepr(p, i) == GIA_VOID )
1247  continue;
1248  pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
1249  if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1250  {
1251  Gia_ObjSetProved(p, i);
1252  Counter++;
1253  }
1254  }
1255  assert( nLits == nLitsAll );
1256  }
1257  if ( fVerbose )
1258  Abc_Print( 1, "Set %d equivalences as proved.\n", Counter );
1259  Gia_ManStop( pMiter );
1260 }
1261 
1262 /**Function*************************************************************
1263 
1264  Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.]
1265 
1266  Description []
1267 
1268  SideEffects []
1269 
1270  SeeAlso []
1271 
1272 ***********************************************************************/
1273 void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose )
1274 {
1275  Gia_Man_t * pSrm;
1276  Vec_Int_t * vTrace, * vMap;
1277  int i, iObjId, Entry, Prev = -1;
1278  // check if there are equivalences
1279  if ( p->pReprs == NULL || p->pNexts == NULL )
1280  {
1281  Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" );
1282  return;
1283  }
1284  // check if PO indexes are available
1285  if ( vPoIds == NULL )
1286  {
1287  Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" );
1288  return;
1289  }
1290  if ( Vec_IntSize(vPoIds) == 0 )
1291  return;
1292  // create SRM with mapping into POs
1293  vMap = Vec_IntAlloc( 1000 );
1294  vTrace = Vec_IntAlloc( 1000 );
1295  pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap );
1296  Vec_IntFree( vTrace );
1297  // the resulting array (vMap) maps PO indexes of the SRM into object IDs
1298  assert( Gia_ManPoNum(pSrm) == Gia_ManPoNum(p) + Vec_IntSize(vMap) );
1299  Gia_ManStop( pSrm );
1300  if ( fVerbose )
1301  printf( "Design POs = %d. SRM POs = %d. Spec POs = %d. Disproved POs = %d.\n",
1302  Gia_ManPoNum(p), Gia_ManPoNum(p) + Vec_IntSize(vMap), Vec_IntSize(vMap), Vec_IntSize(vPoIds) );
1303  // check if disproved POs satisfy the range
1304  Vec_IntSort( vPoIds, 0 );
1305  Vec_IntForEachEntry( vPoIds, Entry, i )
1306  {
1307  if ( Entry < 0 || Entry >= Gia_ManPoNum(p) + Vec_IntSize(vMap) )
1308  {
1309  Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry );
1310  Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", 0, Gia_ManPoNum(p) + Vec_IntSize(vMap)-1 );
1311  Vec_IntFree( vMap );
1312  return;
1313  }
1314  if ( Entry < Gia_ManPoNum(p) )
1315  Abc_Print( 0, "Gia_ManEquivFilter(): One of the original POs (%d) have failed.\n", Entry );
1316  if ( Prev == Entry )
1317  {
1318  Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry );
1319  Vec_IntFree( vMap );
1320  return;
1321  }
1322  Prev = Entry;
1323  }
1324  // perform the reduction of the equivalence classes
1325  Vec_IntForEachEntry( vPoIds, Entry, i )
1326  {
1327  if ( Entry < Gia_ManPoNum(p) )
1328  continue;
1329  iObjId = Vec_IntEntry( vMap, Entry - Gia_ManPoNum(p) );
1330  Gia_ObjUnsetRepr( p, iObjId );
1331 // Gia_ObjSetNext( p, iObjId, 0 );
1332  }
1333  Vec_IntFree( vMap );
1334  ABC_FREE( p->pNexts );
1335  p->pNexts = Gia_ManDeriveNexts( p );
1336 }
1337 
1338 /**Function*************************************************************
1339 
1340  Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.]
1341 
1342  Description []
1343 
1344  SideEffects []
1345 
1346  SeeAlso []
1347 
1348 ***********************************************************************/
1349 void Gia_ManEquivFilterTest( Gia_Man_t * p )
1350 {
1351  Vec_Int_t * vPoIds;
1352  int i;
1353  vPoIds = Vec_IntAlloc( 1000 );
1354  for ( i = 0; i < 10; i++ )
1355  {
1356  Vec_IntPush( vPoIds, Gia_ManPoNum(p) + 2 * i + 2 );
1357  printf( "%d ", Gia_ManPoNum(p) + 2*i + 2 );
1358  }
1359  printf( "\n" );
1360  Gia_ManEquivFilter( p, vPoIds, 1 );
1361  Vec_IntFree( vPoIds );
1362 }
1363 
1364 /**Function*************************************************************
1365 
1366  Synopsis [Transforms equiv classes by setting a good representative.]
1367 
1368  Description []
1369 
1370  SideEffects []
1371 
1372  SeeAlso []
1373 
1374 ***********************************************************************/
1375 void Gia_ManEquivImprove( Gia_Man_t * p )
1376 {
1377  Vec_Int_t * vClass;
1378  int i, k, iNode, iRepr;
1379  int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
1380  assert( p->pReprs != NULL && p->pNexts != NULL );
1381  Gia_ManLevelNum( p );
1382  Gia_ManCreateRefs( p );
1383  // iterate over class candidates
1384  vClass = Vec_IntAlloc( 100 );
1385  Gia_ManForEachClass( p, i )
1386  {
1387  Vec_IntClear( vClass );
1388  iReprBest = -1;
1389  iLevelBest = iMffcBest = ABC_INFINITY;
1390  Gia_ClassForEachObj( p, i, k )
1391  {
1392  iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
1393  iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
1394  if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
1395  {
1396  iReprBest = k;
1397  iLevelBest = iLevelCur;
1398  iMffcBest = iMffcCur;
1399  }
1400  Vec_IntPush( vClass, k );
1401  }
1402  assert( Vec_IntSize( vClass ) > 1 );
1403  assert( iReprBest > 0 );
1404  if ( i == iReprBest )
1405  continue;
1406 /*
1407  Abc_Print( 1, "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
1408  i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
1409  Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
1410 */
1411  iRepr = iReprBest;
1412  Gia_ObjSetRepr( p, iRepr, GIA_VOID );
1413  Gia_ObjSetProved( p, i );
1414  Gia_ObjUnsetProved( p, iRepr );
1415  Vec_IntForEachEntry( vClass, iNode, k )
1416  if ( iNode != iRepr )
1417  Gia_ObjSetRepr( p, iNode, iRepr );
1418  }
1419  Vec_IntFree( vClass );
1420  ABC_FREE( p->pNexts );
1421 // p->pNexts = Gia_ManDeriveNexts( p );
1422 }
1423 
1424 
1425 /**Function*************************************************************
1426 
1427  Synopsis [Returns 1 if pOld is in the TFI of pNode.]
1428 
1429  Description []
1430 
1431  SideEffects []
1432 
1433  SeeAlso []
1434 
1435 ***********************************************************************/
1436 int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
1437 {
1438  // check the trivial cases
1439  if ( pNode == NULL )
1440  return 0;
1441  if ( Gia_ObjIsCi(pNode) )
1442  return 0;
1443 // if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
1444 // return 0;
1445  if ( pNode == pOld )
1446  return 1;
1447  // skip the visited node
1448  if ( pNode->fMark0 )
1449  return 0;
1450  pNode->fMark0 = 1;
1451  Vec_PtrPush( vVisited, pNode );
1452  // check the children
1453  if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
1454  return 1;
1455  if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
1456  return 1;
1457  // check equivalent nodes
1458  return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
1459 }
1460 
1461 /**Function*************************************************************
1462 
1463  Synopsis [Returns 1 if pOld is in the TFI of pNode.]
1464 
1465  Description []
1466 
1467  SideEffects []
1468 
1469  SeeAlso []
1470 
1471 ***********************************************************************/
1472 int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1473 {
1474  Vec_Ptr_t * vVisited;
1475  Gia_Obj_t * pObj;
1476  int RetValue, i;
1477  assert( !Gia_IsComplement(pOld) );
1478  assert( !Gia_IsComplement(pNode) );
1479  vVisited = Vec_PtrAlloc( 100 );
1480  RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
1481  Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
1482  pObj->fMark0 = 0;
1483  Vec_PtrFree( vVisited );
1484  return RetValue;
1485 }
1486 
1487 
1488 /**Function*************************************************************
1489 
1490  Synopsis [Adds the next entry while making choices.]
1491 
1492  Description []
1493 
1494  SideEffects []
1495 
1496  SeeAlso []
1497 
1498 ***********************************************************************/
1499 void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1500 {
1501  if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
1502  {
1503  Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
1504  return;
1505  }
1506  Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
1507 }
1508 
1509 /**Function*************************************************************
1510 
1511  Synopsis [Duplicates the AIG in the DFS order.]
1512 
1513  Description []
1514 
1515  SideEffects []
1516 
1517  SeeAlso []
1518 
1519 ***********************************************************************/
1520 void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1521 {
1522  Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
1523  if ( ~pObj->Value )
1524  return;
1525  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1526  {
1527  if ( Gia_ObjIsConst0(pRepr) )
1528  {
1529  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1530  return;
1531  }
1532  Gia_ManEquivToChoices_rec( pNew, p, pRepr );
1533  assert( Gia_ObjIsAnd(pObj) );
1534  Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1535  Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1536  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1537  if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
1538  {
1539  assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
1540  return;
1541  }
1542  if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
1543  return;
1544  assert( pRepr->Value < pObj->Value );
1545  pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
1546  pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
1547  if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
1548  {
1549 // assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
1550  if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew )
1551  return;
1552  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1553  return;
1554  }
1555  if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
1556  {
1557  assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
1558  Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
1559  Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
1560  }
1561  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1562  return;
1563  }
1564  assert( Gia_ObjIsAnd(pObj) );
1565  Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1566  Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1567  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1568 }
1569 
1570 /**Function*************************************************************
1571 
1572  Synopsis [Removes choices, which contain fanouts.]
1573 
1574  Description []
1575 
1576  SideEffects []
1577 
1578  SeeAlso []
1579 
1580 ***********************************************************************/
1581 void Gia_ManRemoveBadChoices( Gia_Man_t * p )
1582 {
1583  Gia_Obj_t * pObj;
1584  int i, iObj, iPrev, Counter = 0;
1585  // mark nodes with fanout
1586  Gia_ManForEachObj( p, pObj, i )
1587  {
1588  pObj->fMark0 = 0;
1589  if ( Gia_ObjIsAnd(pObj) )
1590  {
1591  Gia_ObjFanin0(pObj)->fMark0 = 1;
1592  Gia_ObjFanin1(pObj)->fMark0 = 1;
1593  }
1594  else if ( Gia_ObjIsCo(pObj) )
1595  Gia_ObjFanin0(pObj)->fMark0 = 1;
1596  }
1597  // go through the classes and remove
1598  Gia_ManForEachClass( p, i )
1599  {
1600  for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
1601  {
1602  if ( !Gia_ManObj(p, iObj)->fMark0 )
1603  {
1604  iPrev = iObj;
1605  continue;
1606  }
1607  Gia_ObjSetRepr( p, iObj, GIA_VOID );
1608  Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
1609  Gia_ObjSetNext( p, iObj, 0 );
1610  Counter++;
1611  }
1612  }
1613  // remove the marks
1614  Gia_ManCleanMark0( p );
1615 // Abc_Print( 1, "Removed %d bad choices.\n", Counter );
1616 }
1617 
1618 /**Function*************************************************************
1619 
1620  Synopsis [Reduces AIG using equivalence classes.]
1621 
1622  Description []
1623 
1624  SideEffects []
1625 
1626  SeeAlso []
1627 
1628 ***********************************************************************/
1629 Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
1630 {
1631  Vec_Int_t * vNodes;
1632  Gia_Man_t * pNew, * pTemp;
1633  Gia_Obj_t * pObj, * pRepr;
1634  int i;
1635 //Gia_ManEquivPrintClasses( p, 0, 0 );
1636  assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
1637  Gia_ManSetPhase( p );
1638  pNew = Gia_ManStart( Gia_ManObjNum(p) );
1639  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1640  pNew->pName = Abc_UtilStrsav( p->pName );
1641  pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
1642  pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
1643  for ( i = 0; i < Gia_ManObjNum(p); i++ )
1644  Gia_ObjSetRepr( pNew, i, GIA_VOID );
1645  Gia_ManFillValue( p );
1646  Gia_ManConst0(p)->Value = 0;
1647  Gia_ManForEachCi( p, pObj, i )
1648  pObj->Value = Gia_ManAppendCi(pNew);
1649  Gia_ManForEachRo( p, pObj, i )
1650  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1651  {
1652  assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
1653  pObj->Value = pRepr->Value;
1654  }
1655  Gia_ManHashAlloc( pNew );
1656  Gia_ManForEachCo( p, pObj, i )
1657  Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1658  vNodes = Gia_ManGetDangling( p );
1659  Gia_ManForEachObjVec( vNodes, p, pObj, i )
1660  Gia_ManEquivToChoices_rec( pNew, p, pObj );
1661  Vec_IntFree( vNodes );
1662  Gia_ManForEachCo( p, pObj, i )
1663  if ( i % nSnapshots == 0 )
1664  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1665  Gia_ManHashStop( pNew );
1666  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1667  Gia_ManRemoveBadChoices( pNew );
1668 //Gia_ManEquivPrintClasses( pNew, 0, 0 );
1669  pNew = Gia_ManCleanup( pTemp = pNew );
1670  Gia_ManStop( pTemp );
1671 //Gia_ManEquivPrintClasses( pNew, 0, 0 );
1672  return pNew;
1673 }
1674 
1675 /**Function*************************************************************
1676 
1677  Synopsis [Counts the number of choice nodes]
1678 
1679  Description []
1680 
1681  SideEffects []
1682 
1683  SeeAlso []
1684 
1685 ***********************************************************************/
1686 int Gia_ManCountChoiceNodes( Gia_Man_t * p )
1687 {
1688  Gia_Obj_t * pObj;
1689  int i, Counter = 0;
1690  if ( p->pReprs == NULL || p->pNexts == NULL )
1691  return 0;
1692  Gia_ManForEachObj( p, pObj, i )
1693  Counter += Gia_ObjIsHead( p, i );
1694  return Counter;
1695 }
1696 
1697 /**Function*************************************************************
1698 
1699  Synopsis [Counts the number of choices]
1700 
1701  Description []
1702 
1703  SideEffects []
1704 
1705  SeeAlso []
1706 
1707 ***********************************************************************/
1708 int Gia_ManCountChoices( Gia_Man_t * p )
1709 {
1710  Gia_Obj_t * pObj;
1711  int i, Counter = 0;
1712  if ( p->pReprs == NULL || p->pNexts == NULL )
1713  return 0;
1714  Gia_ManForEachObj( p, pObj, i )
1715  Counter += (int)(Gia_ObjNext( p, i ) > 0);
1716  return Counter;
1717 }
1718 
1719 ABC_NAMESPACE_IMPL_END
1720 
1721 #include "aig/aig/aig.h"
1722 #include "aig/saig/saig.h"
1723 #include "proof/cec/cec.h"
1724 #include "giaAig.h"
1725 
1726 ABC_NAMESPACE_IMPL_START
1727 
1728 
1729 /**Function*************************************************************
1730 
1731  Synopsis [Returns 1 if AIG has dangling nodes.]
1732 
1733  Description []
1734 
1735  SideEffects []
1736 
1737  SeeAlso []
1738 
1739 ***********************************************************************/
1740 int Gia_ManHasNoEquivs( Gia_Man_t * p )
1741 {
1742  Gia_Obj_t * pObj;
1743  int i;
1744  if ( p->pReprs == NULL )
1745  return 1;
1746  Gia_ManForEachObj( p, pObj, i )
1747  if ( Gia_ObjReprObj(p, i) != NULL )
1748  break;
1749  return i == Gia_ManObjNum(p);
1750 }
1751 
1752 /**Function*************************************************************
1753 
1754  Synopsis [Implements iteration during speculation.]
1755 
1756  Description []
1757 
1758  SideEffects []
1759 
1760  SeeAlso []
1761 
1762 ***********************************************************************/
1763 int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
1764 {
1765 // extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
1766  Aig_Man_t * pTemp;
1767  Gia_Man_t * pSrm, * pReduce, * pAux;
1768  int nIter, nStart = 0;
1769  if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
1770  {
1771  Abc_Print( 1, "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
1772  return 0;
1773  }
1774  // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
1775  Gia_ManCleanMark0( pGia );
1776  Gia_ManPrintStats( pGia, NULL );
1777  for ( nIter = 0; ; nIter++ )
1778  {
1779  if ( Gia_ManHasNoEquivs(pGia) )
1780  {
1781  Abc_Print( 1, "Gia_CommandSpecI: No equivalences left.\n" );
1782  break;
1783  }
1784  Abc_Print( 1, "ITER %3d : ", nIter );
1785 // if ( fVerbose )
1786 // Abc_Print( 1, "Starting BMC from frame %d.\n", nStart );
1787 // if ( fVerbose )
1788 // Gia_ManPrintStats( pGia, 0 );
1789  Gia_ManPrintStatsClasses( pGia );
1790  // perform speculative reduction
1791 // if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
1792  if ( !Cec_ManCheckNonTrivialCands(pGia) )
1793  {
1794  Abc_Print( 1, "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
1795  break;
1796  }
1797  pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
1798  // bmc2 -F 100 -C 25000
1799  {
1800  Abc_Cex_t * pCex;
1801  int nFrames = nFramesInit; // different from default
1802  int nNodeDelta = 2000;
1803  int nBTLimit = nBTLimitInit; // different from default
1804  int nBTLimitAll = 2000000;
1805  pTemp = Gia_ManToAig( pSrm, 0 );
1806 // Aig_ManPrintStats( pTemp );
1807  Gia_ManStop( pSrm );
1808  Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0 );
1809  pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
1810  Aig_ManStop( pTemp );
1811  if ( pCex == NULL )
1812  {
1813  Abc_Print( 1, "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
1814  break;
1815  }
1816  if ( fStart )
1817  nStart = pCex->iFrame;
1818  // perform simulation
1819  {
1820  Cec_ParSim_t Pars, * pPars = &Pars;
1821  Cec_ManSimSetDefaultParams( pPars );
1822  pPars->fCheckMiter = fCheckMiter;
1823  if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
1824  {
1825  ABC_FREE( pCex );
1826  break;
1827  }
1828  ABC_FREE( pCex );
1829  }
1830  }
1831  // write equivalence classes
1832  Gia_AigerWrite( pGia, "gore.aig", 0, 0 );
1833  // reduce the model
1834  pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
1835  if ( pReduce )
1836  {
1837  pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
1838  Gia_ManStop( pAux );
1839  Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
1840 // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
1841 // Gia_ManPrintStatsShort( pReduce );
1842  Gia_ManStop( pReduce );
1843  }
1844  }
1845  return 1;
1846 }
1847 
1848 
1849 
1850 
1851 /**Function*************************************************************
1852 
1853  Synopsis [Reduces AIG using equivalence classes.]
1854 
1855  Description []
1856 
1857  SideEffects []
1858 
1859  SeeAlso []
1860 
1861 ***********************************************************************/
1862 int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB )
1863 {
1864  Gia_Man_t * pGia1, * pGia2, * pMiter;
1865  Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj;
1866  int i, iObj, iNext, Counter = 0;
1867  if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
1868  {
1869  Abc_Print( 1, "Equivalences are not defined.\n" );
1870  return 0;
1871  }
1872  pGia1 = Gia_AigerRead( pName1, 0, 0 );
1873  if ( pGia1 == NULL )
1874  {
1875  Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
1876  return 0;
1877  }
1878  pGia2 = Gia_AigerRead( pName2, 0, 0 );
1879  if ( pGia2 == NULL )
1880  {
1881  Gia_ManStop( pGia2 );
1882  Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
1883  return 0;
1884  }
1885  pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
1886  if ( pMiter == NULL )
1887  {
1888  Gia_ManStop( pGia1 );
1889  Gia_ManStop( pGia2 );
1890  Abc_Print( 1, "Cannot create sequential miter.\n" );
1891  return 0;
1892  }
1893  // make sure the miter is isomorphic
1894  if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
1895  {
1896  Gia_ManStop( pGia1 );
1897  Gia_ManStop( pGia2 );
1898  Gia_ManStop( pMiter );
1899  Abc_Print( 1, "The number of objects in different.\n" );
1900  return 0;
1901  }
1902  if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
1903  {
1904  Gia_ManStop( pGia1 );
1905  Gia_ManStop( pGia2 );
1906  Gia_ManStop( pMiter );
1907  Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
1908  return 0;
1909  }
1910  // transfer copies
1911  Gia_ManCleanMark0( pGia );
1912  Gia_ManForEachObj( pGia1, pObj1, i )
1913  {
1914  if ( pObj1->Value == ~0 )
1915  continue;
1916  pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
1917  pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
1918  pObj->fMark0 = 1;
1919  }
1920  Gia_ManCleanMark1( pGia );
1921  Gia_ManForEachObj( pGia2, pObj2, i )
1922  {
1923  if ( pObj2->Value == ~0 )
1924  continue;
1925  pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
1926  pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
1927  pObj->fMark1 = 1;
1928  }
1929 
1930  // filter equivalences
1931  Gia_ManForEachConst( pGia, i )
1932  {
1933  Gia_ObjUnsetRepr( pGia, i );
1934  assert( pGia->pNexts[i] == 0 );
1935  }
1936  Gia_ManForEachClass( pGia, i )
1937  {
1938  // find the first colorA and colorB
1939  int ClassA = -1, ClassB = -1;
1940  Gia_ClassForEachObj( pGia, i, iObj )
1941  {
1942  pObj = Gia_ManObj( pGia, iObj );
1943  if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 )
1944  {
1945  if ( fLatchA && !Gia_ObjIsRo(pGia, pObj) )
1946  continue;
1947  ClassA = iObj;
1948  }
1949  if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 )
1950  {
1951  if ( fLatchB && !Gia_ObjIsRo(pGia, pObj) )
1952  continue;
1953  ClassB = iObj;
1954  }
1955  }
1956  // undo equivalence classes
1957  for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
1958  iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
1959  {
1960  Gia_ObjUnsetRepr( pGia, iObj );
1961  Gia_ObjSetNext( pGia, iObj, 0 );
1962  }
1963  assert( !Gia_ObjIsHead(pGia, i) );
1964  if ( ClassA > 0 && ClassB > 0 )
1965  {
1966  if ( ClassA > ClassB )
1967  {
1968  ClassA ^= ClassB;
1969  ClassB ^= ClassA;
1970  ClassA ^= ClassB;
1971  }
1972  assert( ClassA < ClassB );
1973  Gia_ObjSetNext( pGia, ClassA, ClassB );
1974  Gia_ObjSetRepr( pGia, ClassB, ClassA );
1975  Counter++;
1976  assert( Gia_ObjIsHead(pGia, ClassA) );
1977  }
1978  }
1979  Abc_Print( 1, "The number of two-node classes after filtering = %d.\n", Counter );
1980 //Gia_ManEquivPrintClasses( pGia, 1, 0 );
1981 
1982  Gia_ManCleanMark0( pGia );
1983  Gia_ManCleanMark1( pGia );
1984  return 1;
1985 }
1986 
1987 
1988 /**Function*************************************************************
1989 
1990  Synopsis [Reduces AIG using equivalence classes.]
1991 
1992  Description []
1993 
1994  SideEffects []
1995 
1996  SeeAlso []
1997 
1998 ***********************************************************************/
1999 int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 )
2000 {
2001  Vec_Int_t * vNodes;
2002  Gia_Man_t * pGia1, * pGia2, * pMiter;
2003  Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj = NULL;
2004  int i, k, iObj, iNext, iPrev, iRepr;
2005  int iLitsOld, iLitsNew;
2006  if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2007  {
2008  Abc_Print( 1, "Equivalences are not defined.\n" );
2009  return 0;
2010  }
2011  pGia1 = Gia_AigerRead( pName1, 0, 0 );
2012  if ( pGia1 == NULL )
2013  {
2014  Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
2015  return 0;
2016  }
2017  pGia2 = Gia_AigerRead( pName2, 0, 0 );
2018  if ( pGia2 == NULL )
2019  {
2020  Gia_ManStop( pGia2 );
2021  Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
2022  return 0;
2023  }
2024  pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
2025  if ( pMiter == NULL )
2026  {
2027  Gia_ManStop( pGia1 );
2028  Gia_ManStop( pGia2 );
2029  Abc_Print( 1, "Cannot create sequential miter.\n" );
2030  return 0;
2031  }
2032  // make sure the miter is isomorphic
2033  if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
2034  {
2035  Gia_ManStop( pGia1 );
2036  Gia_ManStop( pGia2 );
2037  Gia_ManStop( pMiter );
2038  Abc_Print( 1, "The number of objects in different.\n" );
2039  return 0;
2040  }
2041  if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
2042  {
2043  Gia_ManStop( pGia1 );
2044  Gia_ManStop( pGia2 );
2045  Gia_ManStop( pMiter );
2046  Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
2047  return 0;
2048  }
2049  // transfer copies
2050  Gia_ManCleanMark0( pGia );
2051  Gia_ManForEachObj( pGia1, pObj1, i )
2052  {
2053  if ( pObj1->Value == ~0 )
2054  continue;
2055  pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
2056  pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2057  pObj->fMark0 = 1;
2058  }
2059  Gia_ManCleanMark1( pGia );
2060  Gia_ManForEachObj( pGia2, pObj2, i )
2061  {
2062  if ( pObj2->Value == ~0 )
2063  continue;
2064  pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
2065  pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2066  pObj->fMark1 = 1;
2067  }
2068 
2069  // filter equivalences
2070  iLitsOld = iLitsNew = 0;
2071  Gia_ManForEachConst( pGia, i )
2072  {
2073  iLitsOld++;
2074  pObj = Gia_ManObj( pGia, i );
2075  assert( pGia->pNexts[i] == 0 );
2076  assert( pObj->fMark0 || pObj->fMark1 );
2077  if ( pObj->fMark0 && pObj->fMark1 ) // belongs to both A and B
2078  Gia_ObjUnsetRepr( pGia, i );
2079  else
2080  iLitsNew++;
2081  }
2082  // filter equivalences
2083  vNodes = Vec_IntAlloc( 100 );
2084  Gia_ManForEachClass( pGia, i )
2085  {
2086  int fSeenA = 0, fSeenB = 0;
2087  assert( pObj->fMark0 || pObj->fMark1 );
2088  Vec_IntClear( vNodes );
2089  Gia_ClassForEachObj( pGia, i, iObj )
2090  {
2091  pObj = Gia_ManObj( pGia, iObj );
2092  if ( pObj->fMark0 && !pObj->fMark1 )
2093  {
2094  fSeenA = 1;
2095  Vec_IntPush( vNodes, iObj );
2096  }
2097  if ( !pObj->fMark0 && pObj->fMark1 )
2098  {
2099  fSeenB = 1;
2100  Vec_IntPush( vNodes, iObj );
2101  }
2102  iLitsOld++;
2103  }
2104  iLitsOld--;
2105  // undo equivalence classes
2106  for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2107  iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2108  {
2109  Gia_ObjUnsetRepr( pGia, iObj );
2110  Gia_ObjSetNext( pGia, iObj, 0 );
2111  }
2112  assert( !Gia_ObjIsHead(pGia, i) );
2113  if ( fSeenA && fSeenB && Vec_IntSize(vNodes) > 1 )
2114  {
2115  // create new class
2116  iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2117  Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2118  {
2119  Gia_ObjSetRepr( pGia, iObj, iRepr );
2120  Gia_ObjSetNext( pGia, iPrev, iObj );
2121  iPrev = iObj;
2122  iLitsNew++;
2123  }
2124  assert( Gia_ObjNext(pGia, iPrev) == 0 );
2125  }
2126  }
2127  Vec_IntFree( vNodes );
2128  Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2129 //Gia_ManEquivPrintClasses( pGia, 1, 0 );
2130 
2131  Gia_ManCleanMark0( pGia );
2132  Gia_ManCleanMark1( pGia );
2133  return 1;
2134 }
2135 
2136 /**Function*************************************************************
2137 
2138  Synopsis []
2139 
2140  Description []
2141 
2142  SideEffects []
2143 
2144  SeeAlso []
2145 
2146 ***********************************************************************/
2147 void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers )
2148 {
2149  Gia_Obj_t * pObjR;
2150  Vec_Int_t * vNodes, * vFfIds;
2151  int i, k, iObj, iNext, iPrev, iRepr;
2152  int iLitsOld = 0, iLitsNew = 0;
2153  assert( fFlopsOnly ^ fFlopsWith );
2154  vNodes = Vec_IntAlloc( 100 );
2155  // select nodes "flop" node IDs
2156  vFfIds = Vec_IntStart( Gia_ManObjNum(pGia) );
2157  if ( fUseRiDrivers )
2158  {
2159  Gia_ManForEachRi( pGia, pObjR, i )
2160  Vec_IntWriteEntry( vFfIds, Gia_ObjFaninId0p(pGia, pObjR), 1 );
2161  }
2162  else
2163  {
2164  Gia_ManForEachRo( pGia, pObjR, i )
2165  Vec_IntWriteEntry( vFfIds, Gia_ObjId(pGia, pObjR), 1 );
2166  }
2167  // remove all non-flop constants
2168  Gia_ManForEachConst( pGia, i )
2169  {
2170  iLitsOld++;
2171  assert( pGia->pNexts[i] == 0 );
2172  if ( !Vec_IntEntry(vFfIds, i) )
2173  Gia_ObjUnsetRepr( pGia, i );
2174  else
2175  iLitsNew++;
2176  }
2177  // clear the classes
2178  if ( fFlopsOnly )
2179  {
2180  Gia_ManForEachClass( pGia, i )
2181  {
2182  Vec_IntClear( vNodes );
2183  Gia_ClassForEachObj( pGia, i, iObj )
2184  {
2185  if ( Vec_IntEntry(vFfIds, iObj) )
2186  Vec_IntPush( vNodes, iObj );
2187  iLitsOld++;
2188  }
2189  iLitsOld--;
2190  // undo equivalence classes
2191  for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2192  iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2193  {
2194  Gia_ObjUnsetRepr( pGia, iObj );
2195  Gia_ObjSetNext( pGia, iObj, 0 );
2196  }
2197  assert( !Gia_ObjIsHead(pGia, i) );
2198  if ( Vec_IntSize(vNodes) > 1 )
2199  {
2200  // create new class
2201  iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2202  Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2203  {
2204  Gia_ObjSetRepr( pGia, iObj, iRepr );
2205  Gia_ObjSetNext( pGia, iPrev, iObj );
2206  iPrev = iObj;
2207  iLitsNew++;
2208  }
2209  assert( Gia_ObjNext(pGia, iPrev) == 0 );
2210  }
2211  }
2212  }
2213  else
2214  {
2215  Gia_ManForEachClass( pGia, i )
2216  {
2217  int fSeenFlop = 0;
2218  Gia_ClassForEachObj( pGia, i, iObj )
2219  {
2220  if ( Vec_IntEntry(vFfIds, iObj) )
2221  fSeenFlop = 1;
2222  iLitsOld++;
2223  iLitsNew++;
2224  }
2225  iLitsOld--;
2226  iLitsNew--;
2227  if ( fSeenFlop )
2228  continue;
2229  // undo equivalence classes
2230  for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2231  iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2232  {
2233  Gia_ObjUnsetRepr( pGia, iObj );
2234  Gia_ObjSetNext( pGia, iObj, 0 );
2235  iLitsNew--;
2236  }
2237  iLitsNew++;
2238  assert( !Gia_ObjIsHead(pGia, i) );
2239  }
2240  }
2241  Vec_IntFree( vNodes );
2242  Vec_IntFree( vFfIds );
2243  Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2244 }
2245 
2246 ////////////////////////////////////////////////////////////////////////
2247 /// END OF FILE ///
2248 ////////////////////////////////////////////////////////////////////////
2249 
2250 
2251 ABC_NAMESPACE_IMPL_END
Gia_ManDupMarked
Gia_Man_t * Gia_ManDupMarked(Gia_Man_t *p)
Definition: giaDup.c:975
Gia_ManEquivToChoices
Gia_Man_t * Gia_ManEquivToChoices(Gia_Man_t *p, int nSnapshots)
Definition: giaEquiv.c:1629
Gia_ObjCheckTfi_rec
int Gia_ObjCheckTfi_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode, Vec_Ptr_t *vVisited)
Definition: giaEquiv.c:1436
Gia_ObjSetCopyF
static void Gia_ObjSetCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj, int iLit)
Definition: gia.h:486
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Gia_Obj_t_::iDiff0
unsigned iDiff0
Definition: gia.h:77
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_ObjUnsetRepr
static void Gia_ObjUnsetRepr(Gia_Man_t *p, int Id)
Definition: gia.h:890
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_ManForEachClassReverse
#define Gia_ManForEachClassReverse(p, i)
Definition: gia.h:929
Gia_ObjPhaseReal
static int Gia_ObjPhaseReal(Gia_Obj_t *pObj)
Definition: gia.h:416
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_AigerRead
Gia_Man_t * Gia_AigerRead(char *pFileName, int fSkipStrash, int fCheck)
Definition: giaAiger.c:821
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ManCheckTopoOrder_rec
ABC_NAMESPACE_IMPL_START int Gia_ManCheckTopoOrder_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
DECLARATIONS ///.
Definition: giaEquiv.c:46
Gia_ManCountChoiceNodes
int Gia_ManCountChoiceNodes(Gia_Man_t *p)
Definition: giaEquiv.c:1686
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManEquivRepr
static Gia_Obj_t * Gia_ManEquivRepr(Gia_Man_t *p, Gia_Obj_t *pObj, int fUseAll, int fDualOut)
Definition: giaEquiv.c:360
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Gia_ManEquivPrintOne
void Gia_ManEquivPrintOne(Gia_Man_t *p, int i, int Counter)
Definition: giaEquiv.c:292
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ManSpecReduce
Gia_Man_t * Gia_ManSpecReduce(Gia_Man_t *p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose)
Definition: giaEquiv.c:848
Gia_ObjFanin1CopyF
static int Gia_ObjFanin1CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:492
Gia_ManFilterEquivsUsingLatches
void Gia_ManFilterEquivsUsingLatches(Gia_Man_t *pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers)
Definition: giaEquiv.c:2147
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_ObjFaninLit0p
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
Gia_ManDeriveNexts
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition: giaEquiv.c:97
Gia_ManSpecReduceInitFrames
Gia_Man_t * Gia_ManSpecReduceInitFrames(Gia_Man_t *p, Abc_Cex_t *pInit, int nFramesMax, int *pnFrames, int fDualOut, int nMinOutputs)
Definition: giaEquiv.c:1075
Gia_ManEquivImprove
void Gia_ManEquivImprove(Gia_Man_t *p)
Definition: giaEquiv.c:1375
Gia_ManSeqMarkUsed
int Gia_ManSeqMarkUsed(Gia_Man_t *p)
Definition: giaScl.c:156
Gia_ManEquivDeriveReprs
void Gia_ManEquivDeriveReprs(Gia_Man_t *p, Gia_Man_t *pNew, Gia_Man_t *pFinal)
Definition: giaEquiv.c:533
Gia_ManGetDangling
Vec_Int_t * Gia_ManGetDangling(Gia_Man_t *p)
Definition: giaUtil.c:1224
Gia_ManAddNextEntry_rec
void Gia_ManAddNextEntry_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition: giaEquiv.c:1499
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManEquivTransform
void Gia_ManEquivTransform(Gia_Man_t *p, int fVerbose)
Definition: giaEquiv.c:1114
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Gia_Man_t_::pObjs
Gia_Obj_t * pObjs
Definition: gia.h:103
Gia_ManSpecReduceInit
Gia_Man_t * Gia_ManSpecReduceInit(Gia_Man_t *p, Abc_Cex_t *pInit, int nFrames, int fDualOut)
Definition: giaEquiv.c:985
Gia_Rpr_t_::fColorA
unsigned fColorA
Definition: gia.h:61
Gia_ObjIsHead
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Gia_ManEquivReduce_rec
void Gia_ManEquivReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int fUseAll, int fDualOut)
Definition: giaEquiv.c:389
Saig_BmcPerform
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
Definition: bmcBmc2.c:761
Gia_ManEquivRemapDfs
Gia_Man_t * Gia_ManEquivRemapDfs(Gia_Man_t *p)
Definition: giaEquiv.c:592
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_IntErase
static void Vec_IntErase(Vec_Int_t *p)
Definition: vecInt.h:266
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_ManDeriveReprs
void Gia_ManDeriveReprs(Gia_Man_t *p)
Definition: giaEquiv.c:129
Gia_Rpr_t_::iRepr
unsigned iRepr
Definition: gia.h:58
Gia_ManEquivPrintClasses
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition: giaEquiv.c:304
Gia_ManEquivSetColor_rec
int Gia_ManEquivSetColor_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fOdds)
Definition: giaEquiv.c:670
Gia_Rpr_t_::fColorB
unsigned fColorB
Definition: gia.h:62
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
Gia_ManEquivReduceAndRemap
Gia_Man_t * Gia_ManEquivReduceAndRemap(Gia_Man_t *p, int fSeq, int fMiterPairs)
Definition: giaEquiv.c:638
Gia_ManEquivFilter
void Gia_ManEquivFilter(Gia_Man_t *p, Vec_Int_t *vPoIds, int fVerbose)
Definition: giaEquiv.c:1273
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
Gia_Obj_t_
Definition: gia.h:75
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
Cec_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: cec.h:67
Gia_ManFilterEquivsUsingParts
int Gia_ManFilterEquivsUsingParts(Gia_Man_t *pGia, char *pName1, char *pName2)
Definition: giaEquiv.c:1999
Gia_ObjDiffColors2
static int Gia_ObjDiffColors2(Gia_Man_t *p, int i, int j)
Definition: gia.h:909
Gia_ManPrintStatsClasses
void Gia_ManPrintStatsClasses(Gia_Man_t *p)
Definition: giaEquiv.c:219
Cec_ManSimSetDefaultParams
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Gia_ManCountChoices
int Gia_ManCountChoices(Gia_Man_t *p)
Definition: giaEquiv.c:1708
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Gia_ManCombMarkUsed
int Gia_ManCombMarkUsed(Gia_Man_t *p)
Definition: giaScl.c:60
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ManEquivCountClasses
int Gia_ManEquivCountClasses(Gia_Man_t *p)
Definition: giaEquiv.c:179
Cec_ManSeqResimulateCounter
int Cec_ManSeqResimulateCounter(Gia_Man_t *pAig, Cec_ParSim_t *pPars, Abc_Cex_t *pCex)
Definition: cecSeq.c:215
Gia_ObjSetProved
static void Gia_ObjSetProved(Gia_Man_t *p, int Id)
Definition: gia.h:897
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Gia_ManForEachConst
#define Gia_ManForEachConst(p, i)
Definition: gia.h:925
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ManDupDfs
Gia_Man_t * Gia_ManDupDfs(Gia_Man_t *p)
Definition: giaDup.c:1238
Gia_ObjIsConst
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
memcmp
int memcmp()
Gia_ManHasNoEquivs
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Gia_ManHasNoEquivs(Gia_Man_t *p)
Definition: giaEquiv.c:1740
Gia_ManSeqStructSweep
Gia_Man_t * Gia_ManSeqStructSweep(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition: giaScl.c:258
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
Gia_CommandSpecI
int Gia_CommandSpecI(Gia_Man_t *pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose)
Definition: giaEquiv.c:1763
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Gia_ManCandNum
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_ManEquivFilterTest
void Gia_ManEquivFilterTest(Gia_Man_t *p)
Definition: giaEquiv.c:1349
Gia_ObjNextObj
static Gia_Obj_t * Gia_ObjNextObj(Gia_Man_t *p, int Id)
Definition: gia.h:911
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ManEquivCountOne
int Gia_ManEquivCountOne(Gia_Man_t *p, int i)
Definition: giaEquiv.c:282
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Cec_ManSimClassCreate
void Cec_ManSimClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition: cecClass.c:234
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ManRemoveBadChoices
void Gia_ManRemoveBadChoices(Gia_Man_t *p)
Definition: giaEquiv.c:1581
Gia_ClassForEachObj
#define Gia_ClassForEachObj(p, i, iObj)
Definition: gia.h:931
Gia_ObjColors
static int Gia_ObjColors(Gia_Man_t *p, int Id)
Definition: gia.h:904
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ObjSetNext
static void Gia_ObjSetNext(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:913
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Gia_ManEquivToChoices_rec
void Gia_ManEquivToChoices_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaEquiv.c:1520
Gia_ObjSetColors
static void Gia_ObjSetColors(Gia_Man_t *p, int Id)
Definition: gia.h:906
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_ManFilterEquivsForSpeculation
int Gia_ManFilterEquivsForSpeculation(Gia_Man_t *pGia, char *pName1, char *pName2, int fLatchA, int fLatchB)
Definition: giaEquiv.c:1862
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Gia_ManSpecReduceTrace
Gia_Man_t * Gia_ManSpecReduceTrace(Gia_Man_t *p, Vec_Int_t *vTrace, Vec_Int_t *vMap)
Definition: giaEquiv.c:792
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ManSpecReduceInit_rec
void Gia_ManSpecReduceInit_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int f, int fDualOut)
Definition: giaEquiv.c:963
Cec_ManCheckNonTrivialCands
int Cec_ManCheckNonTrivialCands(Gia_Man_t *pAig)
Definition: cecSeq.c:295
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ObjVisitColor
static int Gia_ObjVisitColor(Gia_Man_t *p, int Id, int c)
Definition: gia.h:907
Gia_ManEquivCheckLits
int Gia_ManEquivCheckLits(Gia_Man_t *p, int nLits)
Definition: giaEquiv.c:200
Gia_ManEquivFixOutputPairs
void Gia_ManEquivFixOutputPairs(Gia_Man_t *p)
Definition: giaEquiv.c:480
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
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ObjIsNone
static int Gia_ObjIsNone(Gia_Man_t *p, int Id)
Definition: gia.h:917
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManForEachClass
#define Gia_ManForEachClass(p, i)
Definition: gia.h:927
Gia_ManSpecBuildInit
void Gia_ManSpecBuildInit(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int f, int fDualOut)
Definition: giaEquiv.c:936
Gia_ManCheckTopoOrder
int Gia_ManCheckTopoOrder(Gia_Man_t *p)
Definition: giaEquiv.c:73
Gia_Rpr_t_::fFailed
unsigned fFailed
Definition: gia.h:60
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_ObjProved
static int Gia_ObjProved(Gia_Man_t *p, int Id)
Definition: gia.h:896
Gia_NodeMffcSize
int Gia_NodeMffcSize(Gia_Man_t *p, Gia_Obj_t *pNode)
Definition: giaUtil.c:1132
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
Gia_ManSpecBuild
static void Gia_ManSpecBuild(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int fDualOut, int fSpeculate, Vec_Int_t *vTrace, Vec_Int_t *vGuide, Vec_Int_t *vMap)
Definition: giaEquiv.c:728
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManEquivUpdatePointers
void Gia_ManEquivUpdatePointers(Gia_Man_t *p, Gia_Man_t *pNew)
Definition: giaEquiv.c:508
Gia_ManEquivCountLits
int Gia_ManEquivCountLits(Gia_Man_t *p)
Definition: giaEquiv.c:253
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Cec_ParSim_t_
Definition: cec.h:59
Gia_ObjCheckTfi
int Gia_ObjCheckTfi(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition: giaEquiv.c:1472
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_Obj_t_::fCompl0
unsigned fCompl0
Definition: gia.h:78
Gia_Rpr_t_::fProved
unsigned fProved
Definition: gia.h:59
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManEquivCountLitsAll
int Gia_ManEquivCountLitsAll(Gia_Man_t *p)
Definition: giaEquiv.c:160
Gia_ManSpecReduce_rec
void Gia_ManSpecReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int fDualOut, int fSpeculate, Vec_Int_t *vTrace, Vec_Int_t *vGuide, Vec_Int_t *vMap)
Definition: giaEquiv.c:770
Gia_Rpr_t_
Definition: gia.h:56
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_ObjUnsetProved
static void Gia_ObjUnsetProved(Gia_Man_t *p, int Id)
Definition: gia.h:898
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFanin0CopyF
static int Gia_ObjFanin0CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:491
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManEquivReduce
Gia_Man_t * Gia_ManEquivReduce(Gia_Man_t *p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose)
Definition: giaEquiv.c:417
Gia_ManEquivMark
void Gia_ManEquivMark(Gia_Man_t *p, char *pFileName, int fSkipSome, int fVerbose)
Definition: giaEquiv.c:1175
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ObjRepr
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
Gia_ManEquivSetColors
int Gia_ManEquivSetColors(Gia_Man_t *p, int fVerbose)
Definition: giaEquiv.c:692
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t_::vCopies
Vec_Int_t vCopies
Definition: gia.h:138
Gia_ObjCopyF
static int Gia_ObjCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:485
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387