abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaGiarf.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [gia.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 // combinational simulation manager
30 typedef struct Hcd_Man_t_ Hcd_Man_t;
31 struct Hcd_Man_t_
32 {
33  // parameters
34  Gia_Man_t * pGia; // the AIG to be used for simulation
35  int nBTLimit; // internal backtrack limit
36  int fVerbose; // internal verbose flag
37  // internal variables
38  unsigned * pSimInfo; // simulation info for each object
39  Vec_Ptr_t * vSimInfo; // pointers to the CI simulation info
40  Vec_Ptr_t * vSimPres; // pointers to the presense of simulation info
41  // temporaries
42  Vec_Int_t * vClassOld; // old class numbers
43  Vec_Int_t * vClassNew; // new class numbers
44  Vec_Int_t * vClassTemp; // temporary storage
45  Vec_Int_t * vRefinedC; // refined const reprs
46 };
47 
48 static inline unsigned Hcd_ObjSim( Hcd_Man_t * p, int Id ) { return p->pSimInfo[Id]; }
49 static inline unsigned * Hcd_ObjSimP( Hcd_Man_t * p, int Id ) { return p->pSimInfo + Id; }
50 static inline unsigned Hcd_ObjSetSim( Hcd_Man_t * p, int Id, unsigned n ) { return p->pSimInfo[Id] = n; }
51 
52 ////////////////////////////////////////////////////////////////////////
53 /// FUNCTION DEFINITIONS ///
54 ////////////////////////////////////////////////////////////////////////
55 
56 /**Function*************************************************************
57 
58  Synopsis [Starts the fraiging manager.]
59 
60  Description []
61 
62  SideEffects []
63 
64  SeeAlso []
65 
66 ***********************************************************************/
67 Hcd_Man_t * Gia_ManEquivStart( Gia_Man_t * pGia, int nBTLimit, int fVerbose )
68 {
69  Hcd_Man_t * p;
70  Gia_Obj_t * pObj;
71  int i;
72  p = ABC_CALLOC( Hcd_Man_t, 1 );
73  p->pGia = pGia;
74  p->nBTLimit = nBTLimit;
75  p->fVerbose = fVerbose;
76  p->pSimInfo = ABC_ALLOC( unsigned, Gia_ManObjNum(pGia) );
77  p->vClassOld = Vec_IntAlloc( 100 );
78  p->vClassNew = Vec_IntAlloc( 100 );
79  p->vClassTemp = Vec_IntAlloc( 100 );
80  p->vRefinedC = Vec_IntAlloc( 100 );
81  // collect simulation info
82  p->vSimInfo = Vec_PtrAlloc( 1000 );
83  Gia_ManForEachCi( pGia, pObj, i )
84  Vec_PtrPush( p->vSimInfo, Hcd_ObjSimP(p, Gia_ObjId(pGia,pObj)) );
85  p->vSimPres = Vec_PtrAllocSimInfo( Gia_ManCiNum(pGia), 1 );
86  return p;
87 }
88 
89 /**Function*************************************************************
90 
91  Synopsis [Starts the fraiging manager.]
92 
93  Description []
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
100 void Gia_ManEquivStop( Hcd_Man_t * p )
101 {
102  Vec_PtrFree( p->vSimInfo );
103  Vec_PtrFree( p->vSimPres );
104  Vec_IntFree( p->vClassOld );
105  Vec_IntFree( p->vClassNew );
106  Vec_IntFree( p->vClassTemp );
107  Vec_IntFree( p->vRefinedC );
108  ABC_FREE( p->pSimInfo );
109  ABC_FREE( p );
110 }
111 
112 
113 /**Function*************************************************************
114 
115  Synopsis [Compared two simulation infos.]
116 
117  Description []
118 
119  SideEffects []
120 
121  SeeAlso []
122 
123 ***********************************************************************/
124 static inline int Hcd_ManCompareEqual( unsigned s0, unsigned s1 )
125 {
126  if ( (s0 & 1) == (s1 & 1) )
127  return s0 == s1;
128  else
129  return s0 ==~s1;
130 }
131 
132 /**Function*************************************************************
133 
134  Synopsis [Compares one simulation info.]
135 
136  Description []
137 
138  SideEffects []
139 
140  SeeAlso []
141 
142 ***********************************************************************/
143 static inline int Hcd_ManCompareConst( unsigned s )
144 {
145  if ( s & 1 )
146  return s ==~0;
147  else
148  return s == 0;
149 }
150 
151 /**Function*************************************************************
152 
153  Synopsis [Creates one equivalence class.]
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 void Hcd_ManClassCreate( Gia_Man_t * pGia, Vec_Int_t * vClass )
163 {
164  int Repr = -1, EntPrev = -1, Ent, i;
165  assert( Vec_IntSize(vClass) > 0 );
166  Vec_IntForEachEntry( vClass, Ent, i )
167  {
168  if ( i == 0 )
169  {
170  Repr = Ent;
171  Gia_ObjSetRepr( pGia, Ent, -1 );
172  EntPrev = Ent;
173  }
174  else
175  {
176  Gia_ObjSetRepr( pGia, Ent, Repr );
177  Gia_ObjSetNext( pGia, EntPrev, Ent );
178  EntPrev = Ent;
179  }
180  }
181  Gia_ObjSetNext( pGia, EntPrev, 0 );
182 }
183 
184 /**Function*************************************************************
185 
186  Synopsis [Refines one equivalence class.]
187 
188  Description []
189 
190  SideEffects []
191 
192  SeeAlso []
193 
194 ***********************************************************************/
195 int Hcd_ManClassClassRemoveOne( Hcd_Man_t * p, int i )
196 {
197  int iRepr, Ent;
198  if ( Gia_ObjIsConst(p->pGia, i) )
199  {
200  Gia_ObjSetRepr( p->pGia, i, GIA_VOID );
201  return 1;
202  }
203  if ( !Gia_ObjIsClass(p->pGia, i) )
204  return 0;
205  assert( Gia_ObjIsClass(p->pGia, i) );
206  iRepr = Gia_ObjRepr( p->pGia, i );
207  if ( iRepr == GIA_VOID )
208  iRepr = i;
209  // collect nodes
210  Vec_IntClear( p->vClassOld );
211  Vec_IntClear( p->vClassNew );
212  Gia_ClassForEachObj( p->pGia, iRepr, Ent )
213  {
214  if ( Ent == i )
215  Vec_IntPush( p->vClassNew, Ent );
216  else
217  Vec_IntPush( p->vClassOld, Ent );
218  }
219  assert( Vec_IntSize( p->vClassNew ) == 1 );
220  Hcd_ManClassCreate( p->pGia, p->vClassOld );
221  Hcd_ManClassCreate( p->pGia, p->vClassNew );
222  assert( !Gia_ObjIsClass(p->pGia, i) );
223  return 1;
224 }
225 
226 /**Function*************************************************************
227 
228  Synopsis [Refines one equivalence class.]
229 
230  Description []
231 
232  SideEffects []
233 
234  SeeAlso []
235 
236 ***********************************************************************/
237 int Hcd_ManClassRefineOne( Hcd_Man_t * p, int i )
238 {
239  unsigned Sim0, Sim1;
240  int Ent;
241  Vec_IntClear( p->vClassOld );
242  Vec_IntClear( p->vClassNew );
243  Vec_IntPush( p->vClassOld, i );
244  Sim0 = Hcd_ObjSim(p, i);
245  Gia_ClassForEachObj1( p->pGia, i, Ent )
246  {
247  Sim1 = Hcd_ObjSim(p, Ent);
248  if ( Hcd_ManCompareEqual( Sim0, Sim1 ) )
249  Vec_IntPush( p->vClassOld, Ent );
250  else
251  Vec_IntPush( p->vClassNew, Ent );
252  }
253  if ( Vec_IntSize( p->vClassNew ) == 0 )
254  return 0;
255  Hcd_ManClassCreate( p->pGia, p->vClassOld );
256  Hcd_ManClassCreate( p->pGia, p->vClassNew );
257  if ( Vec_IntSize(p->vClassNew) > 1 )
258  return 1 + Hcd_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
259  return 1;
260 }
261 
262 /**Function*************************************************************
263 
264  Synopsis [Computes hash key of the simulation info.]
265 
266  Description []
267 
268  SideEffects []
269 
270  SeeAlso []
271 
272 ***********************************************************************/
273 int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
274 {
275  static int s_Primes[16] = {
276  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
277  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
278  unsigned uHash = 0;
279  int i;
280  if ( pSim[0] & 1 )
281  for ( i = 0; i < nWords; i++ )
282  uHash ^= ~pSim[i] * s_Primes[i & 0xf];
283  else
284  for ( i = 0; i < nWords; i++ )
285  uHash ^= pSim[i] * s_Primes[i & 0xf];
286  return (int)(uHash % nTableSize);
287 
288 }
289 
290 /**Function*************************************************************
291 
292  Synopsis [Rehashes the refined classes.]
293 
294  Description []
295 
296  SideEffects []
297 
298  SeeAlso []
299 
300 ***********************************************************************/
301 void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined )
302 {
303  int * pTable, nTableSize, Key, i, k;
304  nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
305  pTable = ABC_CALLOC( int, nTableSize );
306  Vec_IntForEachEntry( vRefined, i, k )
307  {
308  assert( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) );
309  Key = Hcd_ManHashKey( Hcd_ObjSimP(p, i), 1, nTableSize );
310  if ( pTable[Key] == 0 )
311  Gia_ObjSetRepr( p->pGia, i, GIA_VOID );
312  else
313  {
314  Gia_ObjSetNext( p->pGia, pTable[Key], i );
315  Gia_ObjSetRepr( p->pGia, i, Gia_ObjRepr(p->pGia, pTable[Key]) );
316  if ( Gia_ObjRepr(p->pGia, i) == GIA_VOID )
317  Gia_ObjSetRepr( p->pGia, i, pTable[Key] );
318  }
319  pTable[Key] = i;
320  }
321  ABC_FREE( pTable );
322 // Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
323  // refine classes in the table
324  Vec_IntForEachEntry( vRefined, i, k )
325  {
326  if ( Gia_ObjIsHead( p->pGia, i ) )
327  Hcd_ManClassRefineOne( p, i );
328  }
329  Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
330 }
331 
332 /**Function*************************************************************
333 
334  Synopsis [Refines equivalence classes after simulation.]
335 
336  Description []
337 
338  SideEffects []
339 
340  SeeAlso []
341 
342 ***********************************************************************/
343 void Hcd_ManClassesRefine( Hcd_Man_t * p )
344 {
345  Gia_Obj_t * pObj;
346  int i;
347  Vec_IntClear( p->vRefinedC );
348  Gia_ManForEachAnd( p->pGia, pObj, i )
349  {
350  if ( Gia_ObjIsTail(p->pGia, i) ) // add check for the class level
351  {
352  Hcd_ManClassRefineOne( p, Gia_ObjRepr(p->pGia, i) );
353  }
354  else if ( Gia_ObjIsConst(p->pGia, i) )
355  {
356  if ( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) )
357  Vec_IntPush( p->vRefinedC, i );
358  }
359  }
360  Hcd_ManClassesRehash( p, p->vRefinedC );
361 }
362 
363 /**Function*************************************************************
364 
365  Synopsis [Creates equivalence classes for the first time.]
366 
367  Description []
368 
369  SideEffects []
370 
371  SeeAlso []
372 
373 ***********************************************************************/
374 void Hcd_ManClassesCreate( Hcd_Man_t * p )
375 {
376  Gia_Obj_t * pObj;
377  int i;
378  assert( p->pGia->pReprs == NULL );
379  p->pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pGia) );
380  p->pGia->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pGia) );
381  Gia_ManForEachObj( p->pGia, pObj, i )
382  Gia_ObjSetRepr( p->pGia, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
383 }
384 
385 /**Function*************************************************************
386 
387  Synopsis [Initializes simulation info.]
388 
389  Description []
390 
391  SideEffects []
392 
393  SeeAlso []
394 
395 ***********************************************************************/
396 void Hcd_ManSimulationInit( Hcd_Man_t * p )
397 {
398  Gia_Obj_t * pObj;
399  int i;
400  Gia_ManForEachCi( p->pGia, pObj, i )
401  Hcd_ObjSetSim( p, i, (Gia_ManRandom(0) << 1) );
402 }
403 
404 /**Function*************************************************************
405 
406  Synopsis [Performs one round of simple combinational simulation.]
407 
408  Description []
409 
410  SideEffects []
411 
412  SeeAlso []
413 
414 ***********************************************************************/
415 void Hcd_ManSimulateSimple( Hcd_Man_t * p )
416 {
417  Gia_Obj_t * pObj;
418  unsigned Res0, Res1;
419  int i;
420  Gia_ManForEachAnd( p->pGia, pObj, i )
421  {
422  Res0 = Hcd_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
423  Res1 = Hcd_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
424  Hcd_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
425  (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
426  }
427 }
428 
429 
430 /**Function*************************************************************
431 
432  Synopsis [Resimulate and refine one equivalence class.]
433 
434  Description []
435 
436  SideEffects []
437 
438  SeeAlso []
439 
440 ***********************************************************************/
441 unsigned Gia_Resimulate_rec( Hcd_Man_t * p, int iObj )
442 {
443  Gia_Obj_t * pObj;
444  unsigned Res0, Res1;
445  if ( Gia_ObjIsTravIdCurrentId( p->pGia, iObj ) )
446  return Hcd_ObjSim( p, iObj );
447  Gia_ObjSetTravIdCurrentId( p->pGia, iObj );
448  pObj = Gia_ManObj(p->pGia, iObj);
449  if ( Gia_ObjIsCi(pObj) )
450  return Hcd_ObjSim( p, iObj );
451  assert( Gia_ObjIsAnd(pObj) );
452  Res0 = Gia_Resimulate_rec( p, Gia_ObjFaninId0(pObj, iObj) );
453  Res1 = Gia_Resimulate_rec( p, Gia_ObjFaninId1(pObj, iObj) );
454  return Hcd_ObjSetSim( p, iObj, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
455  (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
456 }
457 
458 /**Function*************************************************************
459 
460  Synopsis [Resimulate and refine one equivalence class.]
461 
462  Description [Assumes that the counter-example is assigned at the PIs.
463  The counter-example should have the first bit set to 0 at each PI.]
464 
465  SideEffects []
466 
467  SeeAlso []
468 
469 ***********************************************************************/
470 void Gia_ResimulateAndRefine( Hcd_Man_t * p, int i )
471 {
472  int RetValue, iObj;
473  Gia_ManIncrementTravId( p->pGia );
474  Gia_ClassForEachObj( p->pGia, i, iObj )
475  Gia_Resimulate_rec( p, iObj );
476  RetValue = Hcd_ManClassRefineOne( p, i );
477  if ( RetValue == 0 )
478  printf( "!!! no refinement !!!\n" );
479 // assert( RetValue );
480 }
481 
482 /**Function*************************************************************
483 
484  Synopsis [Returns temporary representative of the node.]
485 
486  Description [The temp repr is the first node among the nodes in the class that
487  (a) precedes the given node, and (b) whose level is lower than the given node.]
488 
489  SideEffects []
490 
491  SeeAlso []
492 
493 ***********************************************************************/
494 static inline Gia_Obj_t * Gia_ObjTempRepr( Gia_Man_t * p, int i, int Level )
495 {
496  int iRepr, iMember;
497  iRepr = Gia_ObjRepr( p, i );
498  if ( !Gia_ObjProved(p, i) )
499  return NULL;
500  if ( Gia_ObjFailed(p, i) )
501  return NULL;
502  if ( iRepr == GIA_VOID )
503  return NULL;
504  if ( iRepr == 0 )
505  return Gia_ManConst0( p );
506 // if ( p->pLevels[iRepr] < Level )
507 // return Gia_ManObj( p, iRepr );
508  Gia_ClassForEachObj( p, iRepr, iMember )
509  {
510  if ( Gia_ObjFailed(p, iMember) )
511  continue;
512  if ( iMember >= i )
513  return NULL;
514  if ( Gia_ObjLevelId(p, iMember) < Level )
515  return Gia_ManObj( p, iMember );
516  }
517  assert( 0 );
518  return NULL;
519 }
520 
521 /**Function*************************************************************
522 
523  Synopsis [Generates reduced AIG for the given level.]
524 
525  Description []
526 
527  SideEffects []
528 
529  SeeAlso []
530 
531 ***********************************************************************/
532 Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvRoots )
533 {
534  Gia_Man_t * pNew;
535  Gia_Obj_t * pObj, * pRepr;
536  Vec_Ptr_t * vRoots;
537  int i;
538  vRoots = Vec_PtrAlloc( 100 );
539  // copy unmarked nodes
540  pNew = Gia_ManStart( Gia_ManObjNum(p) );
541  pNew->pName = Abc_UtilStrsav( p->pName );
542  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
543  Gia_ManConst0(p)->Value = 0;
544  Gia_ManForEachCi( p, pObj, i )
545  pObj->Value = Gia_ManAppendCi(pNew);
546  Gia_ManHashAlloc( pNew );
547  Gia_ManForEachAnd( p, pObj, i )
548  {
549  if ( Gia_ObjLevelId(p, i) > Level )
550  continue;
551  if ( Gia_ObjLevelId(p, i) == Level )
552  Vec_PtrPush( vRoots, pObj );
553  if ( Gia_ObjLevelId(p, i) < Level && (pRepr = Gia_ObjTempRepr(p, i, Level)) )
554  {
555 // printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) );
556  assert( pRepr < pObj );
557  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
558  continue;
559  }
560  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
561  }
562  *pvRoots = vRoots;
563  // required by SAT solving
564  Gia_ManCreateRefs( pNew );
565  Gia_ManFillValue( pNew );
566  Gia_ManIncrementTravId( pNew ); // needed for MiniSat to record cexes
567 // Gia_ManSetPhase( pNew ); // needed if MiniSat is using polarity -- should not be enabled for TAS because fPhase is used to label
568  return pNew;
569 }
570 
571 /**Function*************************************************************
572 
573  Synopsis [Collects relevant classes.]
574 
575  Description []
576 
577  SideEffects []
578 
579  SeeAlso []
580 
581 ***********************************************************************/
582 Vec_Ptr_t * Gia_CollectRelatedClasses( Gia_Man_t * pGia, Vec_Ptr_t * vRoots )
583 {
584  Vec_Ptr_t * vClasses;
585  Gia_Obj_t * pRoot, * pRepr;
586  int i;
587  vClasses = Vec_PtrAlloc( 100 );
588  Gia_ManConst0( pGia )->fMark0 = 1;
589  Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pRoot, i )
590  {
591  pRepr = Gia_ObjReprObj( pGia, Gia_ObjId(pGia, pRoot) );
592  if ( pRepr == NULL || pRepr->fMark0 )
593  continue;
594  pRepr->fMark0 = 1;
595  Vec_PtrPush( vClasses, pRepr );
596  }
597  Gia_ManConst0( pGia )->fMark0 = 0;
598  Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
599  pRepr->fMark0 = 0;
600  return vClasses;
601 }
602 
603 /**Function*************************************************************
604 
605  Synopsis [Collects class members.]
606 
607  Description []
608 
609  SideEffects []
610 
611  SeeAlso []
612 
613 ***********************************************************************/
614 Gia_Obj_t * Gia_CollectClassMembers( Gia_Man_t * p, Gia_Obj_t * pRepr, Vec_Ptr_t * vMembers, int Level )
615 {
616  Gia_Obj_t * pTempRepr = NULL;
617  int iRepr, iMember;
618  iRepr = Gia_ObjId( p, pRepr );
619  Vec_PtrClear( vMembers );
620  Gia_ClassForEachObj( p, iRepr, iMember )
621  {
622  if ( Gia_ObjLevelId(p, iMember) == Level )
623  Vec_PtrPush( vMembers, Gia_ManObj( p, iMember ) );
624  if ( pTempRepr == NULL && Gia_ObjLevelId(p, iMember) < Level )
625  pTempRepr = Gia_ManObj( p, iMember );
626  }
627  return pTempRepr;
628 }
629 
630 
631 /**Function*************************************************************
632 
633  Synopsis [Packs patterns into array of simulation info.]
634 
635  Description []
636 
637  SideEffects []
638 
639  SeeAlso []
640 
641 *************************************`**********************************/
642 int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
643 {
644  unsigned * pInfo, * pPres;
645  int i;
646  for ( i = 0; i < nLits; i++ )
647  {
648  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
649  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
650  if ( Abc_InfoHasBit( pPres, iBit ) &&
651  Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
652  return 0;
653  }
654  for ( i = 0; i < nLits; i++ )
655  {
656  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
657  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
658  Abc_InfoSetBit( pPres, iBit );
659  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
660  Abc_InfoXorBit( pInfo, iBit );
661  }
662  return 1;
663 }
664 
665 /**Function*************************************************************
666 
667  Synopsis [Procedure to test the new SAT solver.]
668 
669  Description []
670 
671  SideEffects []
672 
673  SeeAlso []
674 
675 ***********************************************************************/
676 int Gia_GiarfStorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex )
677 {
678  int k;
679  for ( k = 1; k < 32; k++ )
680  if ( Gia_GiarfStorePatternTry( vSimInfo, vPres, k, (int *)Vec_IntArray(vCex), Vec_IntSize(vCex) ) )
681  break;
682  return (int)(k < 32);
683 }
684 
685 /**Function*************************************************************
686 
687  Synopsis [Inserts pattern into simulation info for the PIs.]
688 
689  Description []
690 
691  SideEffects []
692 
693  SeeAlso []
694 
695 ***********************************************************************/
696 void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k )
697 {
698  Gia_Obj_t * pObj;
699  unsigned * pInfo;
700  int Lit, i;
701  Vec_IntForEachEntry( vCex, Lit, i )
702  {
703  pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) );
704  pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) );
705  if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) )
706  Abc_InfoXorBit( pInfo, k );
707  }
708 }
709 
710 /**Function*************************************************************
711 
712  Synopsis [Inserts pattern into simulation info for the PIs.]
713 
714  Description []
715 
716  SideEffects []
717 
718  SeeAlso []
719 
720 ***********************************************************************/
721 void Gia_GiarfPrintClasses( Gia_Man_t * pGia )
722 {
723  int nFails = 0;
724  int nProves = 0;
725  int nTotal = 0;
726  int nBoth = 0;
727  int i;
728  for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
729  {
730  nFails += Gia_ObjFailed(pGia, i);
731  nProves += Gia_ObjProved(pGia, i);
732  nTotal += Gia_ObjReprObj(pGia, i) != NULL;
733  nBoth += Gia_ObjFailed(pGia, i) && Gia_ObjProved(pGia, i);
734  }
735  printf( "nFails = %7d. nProves = %7d. nBoth = %7d. nTotal = %7d.\n",
736  nFails, nProves, nBoth, nTotal );
737 }
738 
739 ABC_NAMESPACE_IMPL_END
740 
741 #include "proof/cec/cecInt.h"
742 
743 ABC_NAMESPACE_IMPL_START
744 
745 
746 /**Function*************************************************************
747 
748  Synopsis [Performs computation of AIGs with choices.]
749 
750  Description []
751 
752  SideEffects []
753 
754  SeeAlso []
755 
756 ***********************************************************************/
757 int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t * vOldRoots, int Level, int fUseMiniSat )
758 {
759  int fUse2Solver = 0;
760  Cec_ManSat_t * pSat;
761  Cec_ParSat_t Pars;
762  Tas_Man_t * pTas;
763  Vec_Int_t * vCex;
764  Vec_Ptr_t * vClasses, * vMembers, * vOldRootsNew;
765  Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr;
766  int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember;
767  int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0;
768  clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock();
769  if ( Vec_PtrSize(vOldRoots) == 0 )
770  return 0;
771  // start SAT solvers
772  Cec_ManSatSetDefaultParams( &Pars );
773  Pars.fPolarFlip = 0;
774  Pars.nBTLimit = p->nBTLimit;
775  pSat = Cec_ManSatCreate( pGiaLev, &Pars );
776  pTas = Tas_ManAlloc( pGiaLev, p->nBTLimit );
777  if ( fUseMiniSat )
778  vCex = Cec_ManSatReadCex( pSat );
779  else
780  vCex = Tas_ReadModel( pTas );
781  vMembers = Vec_PtrAlloc( 100 );
782  Vec_PtrCleanSimInfo( p->vSimPres, 0, 1 );
783  // resolve constants
784  Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
785  {
786  iRoot = Gia_ObjId( p->pGia, pRoot );
787  if ( !Gia_ObjIsConst( p->pGia, iRoot ) )
788  continue;
789  iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase );
790  assert( iRootNew != 1 );
791  if ( fUse2Solver )
792  {
793  nTsat++;
794  clk = clock();
795  status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
796  timeTsat += clock() - clk;
797  if ( status == -1 )
798  {
799  nMiniSat++;
800  clk = clock();
801  status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
802  timeMiniSat += clock() - clk;
803  if ( status == 0 )
804  {
805  Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
806  vCex = Cec_ManSatReadCex( pSat );
807  }
808  }
809  else if ( status == 0 )
810  vCex = Tas_ReadModel( pTas );
811  }
812  else if ( fUseMiniSat )
813  {
814  nMiniSat++;
815  clk = clock();
816  status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
817  timeMiniSat += clock() - clk;
818  if ( status == 0 )
819  Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
820  }
821  else
822  {
823  nTsat++;
824  clk = clock();
825  status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
826  timeTsat += clock() - clk;
827  }
828  if ( status == -1 ) // undec
829  {
830 // Gia_ObjSetFailed( p->pGia, iRoot );
831  nUndec++;
832 // Hcd_ManClassClassRemoveOne( p, iRoot );
833  Gia_ObjSetFailed( p->pGia, iRoot );
834  }
835  else if ( status == 1 ) // unsat
836  {
837  Gia_ObjSetProved( p->pGia, iRoot );
838 // printf( "proved constant %d\n", iRoot );
839  }
840  else // sat
841  {
842 // printf( "Disproved constant %d\n", iRoot );
843  Gia_ObjUnsetRepr( p->pGia, iRoot ); // do we need this?
844  nRecords++;
845  nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
846  }
847  }
848 
849  vClasses = Vec_PtrAlloc( 100 );
850  vOldRootsNew = Vec_PtrAlloc( 100 );
851  for ( nIter = 0; Vec_PtrSize(vOldRoots) > 0; nIter++ )
852  {
853 // printf( "Iter = %d (Size = %d)\n", nIter, Vec_PtrSize(vOldRoots) );
854  // resolve equivalences
855  Vec_PtrClear( vClasses );
856  Vec_PtrClear( vOldRootsNew );
857  Gia_ManConst0( p->pGia )->fMark0 = 1;
858  Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
859  {
860  iRoot = Gia_ObjId( p->pGia, pRoot );
861  if ( Gia_ObjIsHead( p->pGia, iRoot ) )
862  pRepr = pRoot;
863  else if ( Gia_ObjIsClass( p->pGia, iRoot ) )
864  pRepr = Gia_ObjReprObj( p->pGia, iRoot );
865  else
866  continue;
867  if ( pRepr->fMark0 )
868  continue;
869  pRepr->fMark0 = 1;
870  Vec_PtrPush( vClasses, pRepr );
871 // iRepr = Gia_ObjId( p->pGia, pRepr );
872 // fTwoMember = Gia_ClassIsPair(p->pGia, iRepr)
873  // derive temp repr and members on this level
874  pTempRepr = Gia_CollectClassMembers( p->pGia, pRepr, vMembers, Level );
875  if ( pTempRepr )
876  Vec_PtrPush( vMembers, pTempRepr );
877  if ( Vec_PtrSize(vMembers) < 2 )
878  continue;
879  // try proving the members
880  fOneFailed = 0;
881  pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers );
882  Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
883  {
884  iMemberPrev = Abc_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase );
885  iMember = Abc_LitNotCond( pMember->Value, !pMember->fPhase );
886  assert( iMemberPrev != iMember );
887  if ( fUse2Solver )
888  {
889  nTsat++;
890  clk = clock();
891  status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
892  timeTsat += clock() - clk;
893  if ( status == -1 )
894  {
895  nMiniSat++;
896  clk = clock();
897  status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
898  timeMiniSat += clock() - clk;
899  if ( status == 0 )
900  {
901  Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
902  vCex = Cec_ManSatReadCex( pSat );
903  }
904  }
905  else if ( status == 0 )
906  vCex = Tas_ReadModel( pTas );
907  }
908  else if ( fUseMiniSat )
909  {
910  nMiniSat++;
911  clk = clock();
912  status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
913  timeMiniSat += clock() - clk;
914  if ( status == 0 )
915  Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
916  }
917  else
918  {
919  nTsat++;
920  clk = clock();
921  status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
922  timeTsat += clock() - clk;
923  }
924  if ( status == -1 ) // undec
925  {
926 // Gia_ObjSetFailed( p->pGia, iRoot );
927  nUndec++;
928  if ( Gia_ObjLevel(p->pGia, pMemberPrev) > Gia_ObjLevel(p->pGia, pMember) )
929  {
930 // Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMemberPrev) );
931  Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
932  Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
933  }
934  else
935  {
936 // Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMember) );
937  Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
938  Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
939  }
940  }
941  else if ( status == 1 ) // unsat
942  {
943 // Gia_ObjSetProved( p->pGia, iRoot );
944  }
945  else // sat
946  {
947 // iRepr = Gia_ObjId( p->pGia, pRepr );
948 // if ( Gia_ClassIsPair(p->pGia, iRepr) )
949 // Gia_ClassUndoPair(p->pGia, iRepr);
950 // else
951  {
952  fOneFailed = 1;
953  nRecords++;
954  nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
955  Gia_GiarfInsertPattern( p, vCex, (k % 31) + 1 );
956  }
957  }
958  pMemberPrev = pMember;
959 // if ( fOneFailed )
960 // k += Vec_PtrSize(vMembers) / 4;
961  }
962  // if fail, quit this class
963  if ( fOneFailed )
964  {
965  nClassRefs++;
966  Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
967  if ( pMember != pTempRepr && !Gia_ObjFailed(p->pGia, Gia_ObjId(p->pGia, pMember)) )
968  Vec_PtrPush( vOldRootsNew, pMember );
969  clk = clock();
970  Gia_ResimulateAndRefine( p, Gia_ObjId(p->pGia, pRepr) );
971  timeSim += clock() - clk;
972  }
973  else
974  {
975  Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
976  Gia_ObjSetProved( p->pGia, Gia_ObjId(p->pGia, pMember) );
977 /*
978 // }
979 // else
980 // {
981  printf( "Proved equivalent: " );
982  Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
983  printf( "%d(L=%d) ", Gia_ObjId(p->pGia, pMember), p->pGia->pLevels[Gia_ObjId(p->pGia, pMember)] );
984  printf( "\n" );
985 */
986  }
987 
988  }
989  Vec_PtrClear( vOldRoots );
990  Vec_PtrForEachEntry( Gia_Obj_t *, vOldRootsNew, pMember, i )
991  Vec_PtrPush( vOldRoots, pMember );
992  // clean up
993  Gia_ManConst0( p->pGia )->fMark0 = 0;
994  Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
995  pRepr->fMark0 = 0;
996  }
997  Vec_PtrFree( vClasses );
998  Vec_PtrFree( vOldRootsNew );
999  printf( "nSaved = %d nRecords = %d nUndec = %d nClassRefs = %d nMiniSat = %d nTas = %d\n",
1000  nSaved, nRecords, nUndec, nClassRefs, nMiniSat, nTsat );
1001  ABC_PRT( "Tas ", timeTsat );
1002  ABC_PRT( "MiniSat", timeMiniSat );
1003  ABC_PRT( "Sim ", timeSim );
1004  ABC_PRT( "Total ", clock() - timeTotal );
1005 
1006  // resimulate
1007 // clk = clock();
1008  Hcd_ManSimulateSimple( p );
1009  Hcd_ManClassesRefine( p );
1010 // ABC_PRT( "Simulate/refine", clock() - clk );
1011 
1012  // verify the results
1013  Vec_PtrFree( vMembers );
1014  Tas_ManStop( pTas );
1015  Cec_ManSatStop( pSat );
1016  return nIter;
1017 }
1018 
1019 /**Function*************************************************************
1020 
1021  Synopsis [Performs computation of AIGs with choices.]
1022 
1023  Description []
1024 
1025  SideEffects []
1026 
1027  SeeAlso []
1028 
1029 ***********************************************************************/
1030 void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, int fVerbose )
1031 {
1032  Hcd_Man_t * p;
1033  Vec_Ptr_t * vRoots;
1034  Gia_Man_t * pGiaLev;
1035  int i, Lev, nLevels, nIters;
1036  clock_t clk;
1037  Gia_ManRandom( 1 );
1038  Gia_ManSetPhase( pGia );
1039  nLevels = Gia_ManLevelNum( pGia );
1040  Gia_ManIncrementTravId( pGia );
1041  // start the manager
1042  p = Gia_ManEquivStart( pGia, nBTLimit, fVerbose );
1043  // create trivial classes
1044  Hcd_ManClassesCreate( p );
1045  // refine
1046  for ( i = 0; i < 3; i++ )
1047  {
1048  clk = clock();
1049  Hcd_ManSimulationInit( p );
1050  Hcd_ManSimulateSimple( p );
1051  ABC_PRT( "Sim", clock() - clk );
1052  clk = clock();
1053  Hcd_ManClassesRefine( p );
1054  ABC_PRT( "Ref", clock() - clk );
1055  }
1056  // process in the levelized order
1057  for ( Lev = 1; Lev < nLevels; Lev++ )
1058  {
1059  clk = clock();
1060  printf( "LEVEL %3d (out of %3d) ", Lev, nLevels );
1061  pGiaLev = Gia_GenerateReducedLevel( pGia, Lev, &vRoots );
1062  nIters = Gia_ComputeEquivalencesLevel( p, pGiaLev, vRoots, Lev, fUseMiniSat );
1063  Gia_ManStop( pGiaLev );
1064  Vec_PtrFree( vRoots );
1065  printf( "Iters = %3d " );
1066  ABC_PRT( "Time", clock() - clk );
1067  }
1068  Gia_GiarfPrintClasses( pGia );
1069  // clean up
1070  Gia_ManEquivStop( p );
1071 }
1072 
1073 ////////////////////////////////////////////////////////////////////////
1074 /// END OF FILE ///
1075 ////////////////////////////////////////////////////////////////////////
1076 
1077 
1078 ABC_NAMESPACE_IMPL_END
1079 
Tas_ManAlloc
Tas_Man_t * Tas_ManAlloc(Gia_Man_t *pAig, int nBTLimit)
Definition: giaCTas.c:187
Gia_ObjLevelId
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Gia_ObjUnsetRepr
static void Gia_ObjUnsetRepr(Gia_Man_t *p, int Id)
Definition: gia.h:890
Gia_ComputeEquivalences
void Gia_ComputeEquivalences(Gia_Man_t *pGia, int nBTLimit, int fUseMiniSat, int fVerbose)
Definition: giaGiarf.c:1030
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Hcd_ManCompareConst
static int Hcd_ManCompareConst(unsigned s)
Definition: giaGiarf.c:143
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Gia_ComputeEquivalencesLevel
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Gia_ComputeEquivalencesLevel(Hcd_Man_t *p, Gia_Man_t *pGiaLev, Vec_Ptr_t *vOldRoots, int Level, int fUseMiniSat)
Definition: giaGiarf.c:757
Gia_ObjIsClass
static int Gia_ObjIsClass(Gia_Man_t *p, int Id)
Definition: gia.h:919
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Tas_Man_t_
Definition: giaCTas.c:82
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Hcd_Man_t_::vClassTemp
Vec_Int_t * vClassTemp
Definition: giaGiarf.c:44
Tas_ManStop
void Tas_ManStop(Tas_Man_t *p)
Definition: giaCTas.c:223
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_GiarfInsertPattern
void Gia_GiarfInsertPattern(Hcd_Man_t *p, Vec_Int_t *vCex, int k)
Definition: giaGiarf.c:696
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
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
Hcd_ManClassesRehash
void Hcd_ManClassesRehash(Hcd_Man_t *p, Vec_Int_t *vRefined)
Definition: giaGiarf.c:301
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ObjFromLit
static Gia_Obj_t * Gia_ObjFromLit(Gia_Man_t *p, int iLit)
Definition: gia.h:496
Hcd_Man_t_
Definition: giaGiarf.c:31
Hcd_Man_t_::vClassOld
Vec_Int_t * vClassOld
Definition: giaGiarf.c:42
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Hcd_Man_t_::vClassNew
Vec_Int_t * vClassNew
Definition: giaGiarf.c:43
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
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
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Hcd_ObjSimP
static unsigned * Hcd_ObjSimP(Hcd_Man_t *p, int Id)
Definition: giaGiarf.c:49
Hcd_Man_t_::vSimInfo
Vec_Ptr_t * vSimInfo
Definition: giaGiarf.c:39
Gia_GiarfStorePattern
int Gia_GiarfStorePattern(Vec_Ptr_t *vSimInfo, Vec_Ptr_t *vPres, Vec_Int_t *vCex)
Definition: giaGiarf.c:676
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Gia_CollectRelatedClasses
Vec_Ptr_t * Gia_CollectRelatedClasses(Gia_Man_t *pGia, Vec_Ptr_t *vRoots)
Definition: giaGiarf.c:582
nWords
int nWords
Definition: abcNpn.c:127
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
Hcd_Man_t_::nBTLimit
int nBTLimit
Definition: giaGiarf.c:35
Gia_Obj_t_
Definition: gia.h:75
Gia_ManEquivPrintClasses
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition: giaEquiv.c:304
Gia_GenerateReducedLevel
Gia_Man_t * Gia_GenerateReducedLevel(Gia_Man_t *p, int Level, Vec_Ptr_t **pvRoots)
Definition: giaGiarf.c:532
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Cec_ManSavePattern
void Cec_ManSavePattern(Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
Definition: cecSolve.c:1005
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ObjTempRepr
static Gia_Obj_t * Gia_ObjTempRepr(Gia_Man_t *p, int i, int Level)
Definition: giaGiarf.c:494
Hcd_Man_t_::fVerbose
int fVerbose
Definition: giaGiarf.c:36
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
Hcd_ManClassesCreate
void Hcd_ManClassesCreate(Hcd_Man_t *p)
Definition: giaGiarf.c:374
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Hcd_ManClassesRefine
void Hcd_ManClassesRefine(Hcd_Man_t *p)
Definition: giaGiarf.c:343
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
Hcd_Man_t_::vRefinedC
Vec_Int_t * vRefinedC
Definition: giaGiarf.c:45
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
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
Gia_Resimulate_rec
unsigned Gia_Resimulate_rec(Hcd_Man_t *p, int iObj)
Definition: giaGiarf.c:441
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_ManEquivStop
void Gia_ManEquivStop(Hcd_Man_t *p)
Definition: giaGiarf.c:100
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Hcd_ObjSim
static unsigned Hcd_ObjSim(Hcd_Man_t *p, int Id)
Definition: giaGiarf.c:48
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cec_ManSatReadCex
Vec_Int_t * Cec_ManSatReadCex(Cec_ManSat_t *p)
Definition: cecSolve.c:820
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Hcd_Man_t_::pGia
Gia_Man_t * pGia
Definition: giaGiarf.c:34
Hcd_ManClassRefineOne
int Hcd_ManClassRefineOne(Hcd_Man_t *p, int i)
Definition: giaGiarf.c:237
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Hcd_ManClassClassRemoveOne
int Hcd_ManClassClassRemoveOne(Hcd_Man_t *p, int i)
Definition: giaGiarf.c:195
Tas_ReadModel
Vec_Int_t * Tas_ReadModel(Tas_Man_t *p)
Definition: giaCTas.c:250
s1
static char s1[largest_string]
Definition: set.c:514
Hcd_ManSimulationInit
void Hcd_ManSimulationInit(Hcd_Man_t *p)
Definition: giaGiarf.c:396
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ClassForEachObj
#define Gia_ClassForEachObj(p, i, iObj)
Definition: gia.h:931
Hcd_Man_t_::vSimPres
Vec_Ptr_t * vSimPres
Definition: giaGiarf.c:40
Gia_ObjIsTravIdCurrentId
static int Gia_ObjIsTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:536
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
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Gia_ResimulateAndRefine
void Gia_ResimulateAndRefine(Hcd_Man_t *p, int i)
Definition: giaGiarf.c:470
Gia_GiarfStorePatternTry
int Gia_GiarfStorePatternTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition: giaGiarf.c:642
Cec_ManSatStop
void Cec_ManSatStop(Cec_ManSat_t *p)
Definition: cecMan.c:104
Cec_ManSat_t_
Definition: cecInt.h:75
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_ObjIsTail
static int Gia_ObjIsTail(Gia_Man_t *p, int Id)
Definition: gia.h:918
Hcd_Man_t_::pSimInfo
unsigned * pSimInfo
Definition: giaGiarf.c:38
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Hcd_ManHashKey
int Hcd_ManHashKey(unsigned *pSim, int nWords, int nTableSize)
Definition: giaGiarf.c:273
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cec_ManSatCheckNodeTwo
int Cec_ManSatCheckNodeTwo(Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
Definition: cecSolve.c:569
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Hcd_Man_t
typedefABC_NAMESPACE_IMPL_START struct Hcd_Man_t_ Hcd_Man_t
DECLARATIONS ///.
Definition: giaGiarf.c:30
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Hcd_ObjSetSim
static unsigned Hcd_ObjSetSim(Hcd_Man_t *p, int Id, unsigned n)
Definition: giaGiarf.c:50
Hcd_ManCompareEqual
static int Hcd_ManCompareEqual(unsigned s0, unsigned s1)
Definition: giaGiarf.c:124
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
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
Cec_ManSatCheckNode
int Cec_ManSatCheckNode(Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecSolve.c:470
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_GiarfPrintClasses
void Gia_GiarfPrintClasses(Gia_Man_t *pGia)
Definition: giaGiarf.c:721
Gia_ManEquivStart
Hcd_Man_t * Gia_ManEquivStart(Gia_Man_t *pGia, int nBTLimit, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: giaGiarf.c:67
Gia_ObjFailed
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
Gia_Man_t_::fVerbose
int fVerbose
Definition: gia.h:174
Gia_ObjProved
static int Gia_ObjProved(Gia_Man_t *p, int Id)
Definition: gia.h:896
Cec_ParSat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
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
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Tas_ManSolve
int Tas_ManSolve(Tas_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pObj2)
Definition: giaCTas.c:1366
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_Rpr_t_
Definition: gia.h:56
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
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
Hcd_ManSimulateSimple
void Hcd_ManSimulateSimple(Hcd_Man_t *p)
Definition: giaGiarf.c:415
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_ObjSetTravIdCurrentId
static void Gia_ObjSetTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:535
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Cec_ManSatCreate
Cec_ManSat_t * Cec_ManSatCreate(Gia_Man_t *pAig, Cec_ParSat_t *pPars)
DECLARATIONS ///.
Definition: cecMan.c:45
Cec_ManSatSetDefaultParams
void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ObjSetFailed
static void Gia_ObjSetFailed(Gia_Man_t *p, int Id)
Definition: gia.h:901
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
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Gia_CollectClassMembers
Gia_Obj_t * Gia_CollectClassMembers(Gia_Man_t *p, Gia_Obj_t *pRepr, Vec_Ptr_t *vMembers, int Level)
Definition: giaGiarf.c:614
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Hcd_ManClassCreate
void Hcd_ManClassCreate(Gia_Man_t *pGia, Vec_Int_t *vClass)
Definition: giaGiarf.c:162