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
Hcd_ObjSim(Hcd_Man_t * p,int Id)48 static inline unsigned Hcd_ObjSim( Hcd_Man_t * p, int Id ) { return p->pSimInfo[Id]; }
Hcd_ObjSimP(Hcd_Man_t * p,int Id)49 static inline unsigned * Hcd_ObjSimP( Hcd_Man_t * p, int Id ) { return p->pSimInfo + Id; }
Hcd_ObjSetSim(Hcd_Man_t * p,int Id,unsigned n)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 ***********************************************************************/
Gia_ManEquivStart(Gia_Man_t * pGia,int nBTLimit,int fVerbose)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 ***********************************************************************/
Gia_ManEquivStop(Hcd_Man_t * p)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 ***********************************************************************/
Hcd_ManCompareEqual(unsigned s0,unsigned s1)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 ***********************************************************************/
Hcd_ManCompareConst(unsigned s)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 ***********************************************************************/
Hcd_ManClassCreate(Gia_Man_t * pGia,Vec_Int_t * vClass)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 ***********************************************************************/
Hcd_ManClassClassRemoveOne(Hcd_Man_t * p,int i)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 ***********************************************************************/
Hcd_ManClassRefineOne(Hcd_Man_t * p,int i)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 ***********************************************************************/
Hcd_ManHashKey(unsigned * pSim,int nWords,int nTableSize)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 ***********************************************************************/
Hcd_ManClassesRehash(Hcd_Man_t * p,Vec_Int_t * vRefined)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 ***********************************************************************/
Hcd_ManClassesRefine(Hcd_Man_t * p)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 ***********************************************************************/
Hcd_ManClassesCreate(Hcd_Man_t * p)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 ***********************************************************************/
Hcd_ManSimulationInit(Hcd_Man_t * p)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 ***********************************************************************/
Hcd_ManSimulateSimple(Hcd_Man_t * p)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 ***********************************************************************/
Gia_Resimulate_rec(Hcd_Man_t * p,int iObj)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 ***********************************************************************/
Gia_ResimulateAndRefine(Hcd_Man_t * p,int i)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 ***********************************************************************/
Gia_ObjTempRepr(Gia_Man_t * p,int i,int Level)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 ***********************************************************************/
Gia_GenerateReducedLevel(Gia_Man_t * p,int Level,Vec_Ptr_t ** pvRoots)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 ***********************************************************************/
Gia_CollectRelatedClasses(Gia_Man_t * pGia,Vec_Ptr_t * vRoots)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 ***********************************************************************/
Gia_CollectClassMembers(Gia_Man_t * p,Gia_Obj_t * pRepr,Vec_Ptr_t * vMembers,int Level)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 *************************************`**********************************/
Gia_GiarfStorePatternTry(Vec_Ptr_t * vInfo,Vec_Ptr_t * vPres,int iBit,int * pLits,int nLits)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 ***********************************************************************/
Gia_GiarfStorePattern(Vec_Ptr_t * vSimInfo,Vec_Ptr_t * vPres,Vec_Int_t * vCex)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 ***********************************************************************/
Gia_GiarfInsertPattern(Hcd_Man_t * p,Vec_Int_t * vCex,int k)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 ***********************************************************************/
Gia_GiarfPrintClasses(Gia_Man_t * pGia)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 ***********************************************************************/
Gia_ComputeEquivalencesLevel(Hcd_Man_t * p,Gia_Man_t * pGiaLev,Vec_Ptr_t * vOldRoots,int Level,int fUseMiniSat)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 ***********************************************************************/
Gia_ComputeEquivalences(Gia_Man_t * pGia,int nBTLimit,int fUseMiniSat,int fVerbose)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
1080