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 #include "giaAig.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 /*
27 Limitations of this package:
28 - no more than (1<<31)-1 state cubes and internal nodes
29 - no more than MAX_VARS_NUM state variables
30 - no more than MAX_CALL_NUM transitions from a state
31 - cube list rebalancing happens when cube count reaches MAX_CUBE_NUM
32 */
33
34 ////////////////////////////////////////////////////////////////////////
35 /// DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 #define MAX_CALL_NUM (1000000) // the max number of recursive calls
39 #define MAX_ITEM_NUM (1<<20) // the number of items on a page
40 #define MAX_PAGE_NUM (1<<11) // the max number of memory pages
41 #define MAX_VARS_NUM (1<<14) // the max number of state vars allowed
42 #define MAX_CUBE_NUM 63 // the max number of cubes before rebalancing
43
44 // pointer to the tree node or state cube
45 typedef struct Gia_PtrAre_t_ Gia_PtrAre_t;
46 struct Gia_PtrAre_t_
47 {
48 unsigned nItem : 20; // item number (related to MAX_ITEM_NUM)
49 unsigned nPage : 11; // page number (related to MAX_PAGE_NUM)
50 unsigned fMark : 1; // user mark
51 };
52
53 typedef union Gia_PtrAreInt_t_ Gia_PtrAreInt_t;
54 union Gia_PtrAreInt_t_
55 {
56 Gia_PtrAre_t iGia;
57 unsigned iInt;
58 };
59
60 // tree nodes
61 typedef struct Gia_ObjAre_t_ Gia_ObjAre_t;
62 struct Gia_ObjAre_t_
63 {
64 unsigned iVar : 14; // variable (related to MAX_VARS_NUM)
65 unsigned nStas0 : 6; // cube counter (related to MAX_CUBE_NUM)
66 unsigned nStas1 : 6; // cube counter (related to MAX_CUBE_NUM)
67 unsigned nStas2 : 6; // cube counter (related to MAX_CUBE_NUM)
68 Gia_PtrAre_t F[3]; // branches
69 };
70
71 // state cube
72 typedef struct Gia_StaAre_t_ Gia_StaAre_t;
73 struct Gia_StaAre_t_
74 {
75 Gia_PtrAre_t iPrev; // previous state
76 Gia_PtrAre_t iNext; // next cube in the list
77 unsigned pData[0]; // state bits
78 };
79
80 // explicit state reachability manager
81 typedef struct Gia_ManAre_t_ Gia_ManAre_t;
82 struct Gia_ManAre_t_
83 {
84 Gia_Man_t * pAig; // user's AIG manager
85 Gia_Man_t * pNew; // temporary AIG manager
86 unsigned ** ppObjs; // storage for objects (MAX_PAGE_NUM pages)
87 unsigned ** ppStas; // storage for states (MAX_PAGE_NUM pages)
88 // unsigned * pfUseless; // to label useless cubes
89 // int nUselessAlloc; // the number of useless alloced
90 // internal flags
91 int fMiter; // stops when a bug is discovered
92 int fStopped; // set high when reachability is stopped
93 int fTree; // working in the tree mode
94 // internal parametesr
95 int nWords; // the size of bit info in words
96 int nSize; // the size of state structure in words
97 int nObjPages; // the number of pages used for objects
98 int nStaPages; // the number of pages used for states
99 int nObjs; // the number of objects
100 int nStas; // the number of states
101 int iStaCur; // the next state to be explored
102 Gia_PtrAre_t Root; // root of the tree
103 Vec_Vec_t * vCiTfos; // storage for nodes in the CI TFOs
104 Vec_Vec_t * vCiLits; // storage for literals of these nodes
105 Vec_Int_t * vCubesA; // checked cubes
106 Vec_Int_t * vCubesB; // unchecked cubes
107 // deriving counter-example
108 void * pSat; // SAT solver
109 Vec_Int_t * vSatNumCis; // SAT variables for CIs
110 Vec_Int_t * vSatNumCos; // SAT variables for COs
111 Vec_Int_t * vCofVars; // variables used to cofactor
112 Vec_Int_t * vAssumps; // temporary storage for assumptions
113 Gia_StaAre_t * pTarget; // state that needs to be reached
114 int iOutFail; // the number of the failed output
115 // statistics
116 int nChecks; // the number of timea cube was checked
117 int nEquals; // total number of equal
118 int nCompares; // the number of compares
119 int nRecCalls; // the number of rec calls
120 int nDisjs; // the number of disjoint cube pairs
121 int nDisjs2; // the number of disjoint cube pairs
122 int nDisjs3; // the number of disjoint cube pairs
123 // time
124 int timeAig; // AIG cofactoring time
125 int timeCube; // cube checking time
126 };
127
Gia_Int2Ptr(unsigned n)128 static inline Gia_PtrAre_t Gia_Int2Ptr( unsigned n ) { Gia_PtrAreInt_t g; g.iInt = n; return g.iGia; }
Gia_Ptr2Int(Gia_PtrAre_t n)129 static inline unsigned Gia_Ptr2Int( Gia_PtrAre_t n ) { Gia_PtrAreInt_t g; g.iGia = n; return g.iInt & 0x7fffffff; }
130
Gia_ObjHasBranch0(Gia_ObjAre_t * q)131 static inline int Gia_ObjHasBranch0( Gia_ObjAre_t * q ) { return !q->nStas0 && (q->F[0].nPage || q->F[0].nItem); }
Gia_ObjHasBranch1(Gia_ObjAre_t * q)132 static inline int Gia_ObjHasBranch1( Gia_ObjAre_t * q ) { return !q->nStas1 && (q->F[1].nPage || q->F[1].nItem); }
Gia_ObjHasBranch2(Gia_ObjAre_t * q)133 static inline int Gia_ObjHasBranch2( Gia_ObjAre_t * q ) { return !q->nStas2 && (q->F[2].nPage || q->F[2].nItem); }
134
Gia_ManAreObj(Gia_ManAre_t * p,Gia_PtrAre_t n)135 static inline Gia_ObjAre_t * Gia_ManAreObj( Gia_ManAre_t * p, Gia_PtrAre_t n ) { return (Gia_ObjAre_t *)(p->ppObjs[n.nPage] + (n.nItem << 2)); }
Gia_ManAreSta(Gia_ManAre_t * p,Gia_PtrAre_t n)136 static inline Gia_StaAre_t * Gia_ManAreSta( Gia_ManAre_t * p, Gia_PtrAre_t n ) { return (Gia_StaAre_t *)(p->ppStas[n.nPage] + n.nItem * p->nSize); }
Gia_ManAreObjInt(Gia_ManAre_t * p,int n)137 static inline Gia_ObjAre_t * Gia_ManAreObjInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreObj( p, Gia_Int2Ptr(n) ); }
Gia_ManAreStaInt(Gia_ManAre_t * p,int n)138 static inline Gia_StaAre_t * Gia_ManAreStaInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreSta( p, Gia_Int2Ptr(n) ); }
Gia_ManAreObjLast(Gia_ManAre_t * p)139 static inline Gia_ObjAre_t * Gia_ManAreObjLast( Gia_ManAre_t * p ) { return Gia_ManAreObjInt( p, p->nObjs-1 ); }
Gia_ManAreStaLast(Gia_ManAre_t * p)140 static inline Gia_StaAre_t * Gia_ManAreStaLast( Gia_ManAre_t * p ) { return Gia_ManAreStaInt( p, p->nStas-1 ); }
141
Gia_ObjNextObj0(Gia_ManAre_t * p,Gia_ObjAre_t * q)142 static inline Gia_ObjAre_t * Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[0] ); }
Gia_ObjNextObj1(Gia_ManAre_t * p,Gia_ObjAre_t * q)143 static inline Gia_ObjAre_t * Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[1] ); }
Gia_ObjNextObj2(Gia_ManAre_t * p,Gia_ObjAre_t * q)144 static inline Gia_ObjAre_t * Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[2] ); }
145
Gia_StaHasValue0(Gia_StaAre_t * p,int iReg)146 static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, iReg << 1 ); }
Gia_StaHasValue1(Gia_StaAre_t * p,int iReg)147 static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 ); }
148
Gia_StaSetValue0(Gia_StaAre_t * p,int iReg)149 static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, iReg << 1 ); }
Gia_StaSetValue1(Gia_StaAre_t * p,int iReg)150 static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 ); }
151
Gia_StaPrev(Gia_ManAre_t * p,Gia_StaAre_t * pS)152 static inline Gia_StaAre_t * Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iPrev); }
Gia_StaNext(Gia_ManAre_t * p,Gia_StaAre_t * pS)153 static inline Gia_StaAre_t * Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iNext); }
Gia_StaIsGood(Gia_ManAre_t * p,Gia_StaAre_t * pS)154 static inline int Gia_StaIsGood( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return ((unsigned *)pS) != p->ppStas[0]; }
155
Gia_StaSetUnused(Gia_StaAre_t * pS)156 static inline void Gia_StaSetUnused( Gia_StaAre_t * pS ) { pS->iPrev.fMark = 1; }
Gia_StaIsUnused(Gia_StaAre_t * pS)157 static inline int Gia_StaIsUnused( Gia_StaAre_t * pS ) { return pS->iPrev.fMark; }
Gia_StaIsUsed(Gia_StaAre_t * pS)158 static inline int Gia_StaIsUsed( Gia_StaAre_t * pS ) { return !pS->iPrev.fMark; }
159
160 #define Gia_ManAreForEachCubeList( p, pList, pCube ) \
161 for ( pCube = pList; Gia_StaIsGood(p, pCube); pCube = Gia_StaNext(p, pCube) )
162 #define Gia_ManAreForEachCubeList2( p, iList, pCube, iCube ) \
163 for ( iCube = Gia_Ptr2Int(iList), pCube = Gia_ManAreSta(p, iList); \
164 Gia_StaIsGood(p, pCube); \
165 iCube = Gia_Ptr2Int(pCube->iNext), pCube = Gia_StaNext(p, pCube) )
166 #define Gia_ManAreForEachCubeStore( p, pCube, i ) \
167 for ( i = 1; i < p->nStas && (pCube = Gia_ManAreStaInt(p, i)); i++ )
168 #define Gia_ManAreForEachCubeVec( vVec, p, pCube, i ) \
169 for ( i = 0; i < Vec_IntSize(vVec) && (pCube = Gia_ManAreStaInt(p, Vec_IntEntry(vVec,i))); i++ )
170
171 ////////////////////////////////////////////////////////////////////////
172 /// FUNCTION DEFINITIONS ///
173 ////////////////////////////////////////////////////////////////////////
174
175 /**Function*************************************************************
176
177 Synopsis [Count state minterms contained in a cube.]
178
179 Description []
180
181 SideEffects []
182
183 SeeAlso []
184
185 ***********************************************************************/
Gia_ManCountMintermsInCube(Gia_StaAre_t * pCube,int nVars,unsigned * pStore)186 void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pStore )
187 {
188 unsigned Mint, Mask = 0;
189 int i, m, nMints, nDashes = 0, Dashes[32];
190 // count the number of dashes
191 for ( i = 0; i < nVars; i++ )
192 {
193 if ( Gia_StaHasValue0( pCube, i ) )
194 continue;
195 if ( Gia_StaHasValue1( pCube, i ) )
196 Mask |= (1 << i);
197 else
198 Dashes[nDashes++] = i;
199 }
200 // fill in the miterms
201 nMints = (1 << nDashes);
202 for ( m = 0; m < nMints; m++ )
203 {
204 Mint = Mask;
205 for ( i = 0; i < nVars; i++ )
206 if ( m & (1 << i) )
207 Mint |= (1 << Dashes[i]);
208 Abc_InfoSetBit( pStore, Mint );
209 }
210 }
211
212 /**Function*************************************************************
213
214 Synopsis [Count state minterms contains in the used cubes.]
215
216 Description []
217
218 SideEffects []
219
220 SeeAlso []
221
222 ***********************************************************************/
Gia_ManCountMinterms(Gia_ManAre_t * p)223 int Gia_ManCountMinterms( Gia_ManAre_t * p )
224 {
225 Gia_StaAre_t * pCube;
226 unsigned * pMemory;
227 int i, nMemSize, Counter = 0;
228 if ( Gia_ManRegNum(p->pAig) > 30 )
229 return -1;
230 nMemSize = Abc_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
231 pMemory = ABC_CALLOC( unsigned, nMemSize );
232 Gia_ManAreForEachCubeStore( p, pCube, i )
233 if ( Gia_StaIsUsed(pCube) )
234 Gia_ManCountMintermsInCube( pCube, Gia_ManRegNum(p->pAig), pMemory );
235 for ( i = 0; i < nMemSize; i++ )
236 Counter += Gia_WordCountOnes( pMemory[i] );
237 ABC_FREE( pMemory );
238 return Counter;
239 }
240
241 /**Function*************************************************************
242
243 Synopsis [Derives the TFO of one CI.]
244
245 Description []
246
247 SideEffects []
248
249 SeeAlso []
250
251 ***********************************************************************/
Gia_ManDeriveCiTfo_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vRes)252 int Gia_ManDeriveCiTfo_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRes )
253 {
254 if ( Gia_ObjIsCi(pObj) )
255 return pObj->fMark0;
256 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
257 return pObj->fMark0;
258 Gia_ObjSetTravIdCurrent(p, pObj);
259 assert( Gia_ObjIsAnd(pObj) );
260 Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes );
261 Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin1(pObj), vRes );
262 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 | Gia_ObjFanin1(pObj)->fMark0;
263 if ( pObj->fMark0 )
264 Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
265 return pObj->fMark0;
266 }
267
268
269 /**Function*************************************************************
270
271 Synopsis [Derives the TFO of one CI.]
272
273 Description []
274
275 SideEffects []
276
277 SeeAlso []
278
279 ***********************************************************************/
Gia_ManDeriveCiTfoOne(Gia_Man_t * p,Gia_Obj_t * pPivot)280 Vec_Int_t * Gia_ManDeriveCiTfoOne( Gia_Man_t * p, Gia_Obj_t * pPivot )
281 {
282 Vec_Int_t * vRes;
283 Gia_Obj_t * pObj;
284 int i;
285 assert( pPivot->fMark0 == 0 );
286 pPivot->fMark0 = 1;
287 vRes = Vec_IntAlloc( 100 );
288 Vec_IntPush( vRes, Gia_ObjId(p, pPivot) );
289 Gia_ManIncrementTravId( p );
290 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
291 Gia_ManForEachCo( p, pObj, i )
292 {
293 Gia_ManDeriveCiTfo_rec( p, Gia_ObjFanin0(pObj), vRes );
294 if ( Gia_ObjFanin0(pObj)->fMark0 )
295 Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
296 }
297 pPivot->fMark0 = 0;
298 return vRes;
299 }
300
301 /**Function*************************************************************
302
303 Synopsis [Derives the TFO of each CI.]
304
305 Description []
306
307 SideEffects []
308
309 SeeAlso []
310
311 ***********************************************************************/
Gia_ManDeriveCiTfo(Gia_Man_t * p)312 Vec_Vec_t * Gia_ManDeriveCiTfo( Gia_Man_t * p )
313 {
314 Vec_Ptr_t * vRes;
315 Gia_Obj_t * pPivot;
316 int i;
317 Gia_ManCleanMark0( p );
318 Gia_ManIncrementTravId( p );
319 vRes = Vec_PtrAlloc( Gia_ManCiNum(p) );
320 Gia_ManForEachCi( p, pPivot, i )
321 Vec_PtrPush( vRes, Gia_ManDeriveCiTfoOne(p, pPivot) );
322 Gia_ManCleanMark0( p );
323 return (Vec_Vec_t *)vRes;
324 }
325
326 /**Function*************************************************************
327
328 Synopsis [Returns 1 if states are equal.]
329
330 Description []
331
332 SideEffects []
333
334 SeeAlso []
335
336 ***********************************************************************/
Gia_StaAreEqual(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)337 static inline int Gia_StaAreEqual( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
338 {
339 int w;
340 for ( w = 0; w < nWords; w++ )
341 if ( p1->pData[w] != p2->pData[w] )
342 return 0;
343 return 1;
344 }
345
346 /**Function*************************************************************
347
348 Synopsis [Returns 1 if states are disjoint.]
349
350 Description []
351
352 SideEffects []
353
354 SeeAlso []
355
356 ***********************************************************************/
Gia_StaAreDisjoint(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)357 static inline int Gia_StaAreDisjoint( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
358 {
359 int w;
360 for ( w = 0; w < nWords; w++ )
361 if ( ((p1->pData[w] ^ p2->pData[w]) >> 1) & (p1->pData[w] ^ p2->pData[w]) & 0x55555555 )
362 return 1;
363 return 0;
364 }
365
366 /**Function*************************************************************
367
368 Synopsis [Returns 1 if cube p1 contains cube p2.]
369
370 Description []
371
372 SideEffects []
373
374 SeeAlso []
375
376 ***********************************************************************/
Gia_StaAreContain(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)377 static inline int Gia_StaAreContain( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
378 {
379 int w;
380 for ( w = 0; w < nWords; w++ )
381 if ( (p1->pData[w] | p2->pData[w]) != p2->pData[w] )
382 return 0;
383 return 1;
384 }
385
386 /**Function*************************************************************
387
388 Synopsis [Returns the number of dashes in p1 that are non-dashes in p2.]
389
390 Description []
391
392 SideEffects []
393
394 SeeAlso []
395
396 ***********************************************************************/
Gia_StaAreDashNum(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)397 static inline int Gia_StaAreDashNum( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
398 {
399 int w, Counter = 0;
400 for ( w = 0; w < nWords; w++ )
401 Counter += Gia_WordCountOnes( (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555 );
402 return Counter;
403 }
404
405 /**Function*************************************************************
406
407 Synopsis [Returns the number of a variable for sharping the cube.]
408
409 Description [Counts the number of variables that have dash in p1 and
410 non-dash in p2. If there is exactly one such variable, returns its index.
411 Otherwise returns -1.]
412
413 SideEffects []
414
415 SeeAlso []
416
417 ***********************************************************************/
Gia_StaAreSharpVar(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)418 static inline int Gia_StaAreSharpVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
419 {
420 unsigned Word;
421 int w, iVar = -1;
422 for ( w = 0; w < nWords; w++ )
423 {
424 Word = (~(p1->pData[w] ^ (p1->pData[w] >> 1))) & (p2->pData[w] ^ (p2->pData[w] >> 1)) & 0x55555555;
425 if ( Word == 0 )
426 continue;
427 if ( !Gia_WordHasOneBit(Word) )
428 return -1;
429 // has exactly one bit
430 if ( iVar >= 0 )
431 return -1;
432 // the first variable of this type
433 iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2;
434 }
435 return iVar;
436 }
437
438 /**Function*************************************************************
439
440 Synopsis [Returns the number of a variable for merging the cubes.]
441
442 Description [If there is exactly one such variable, returns its index.
443 Otherwise returns -1.]
444
445 SideEffects []
446
447 SeeAlso []
448
449 ***********************************************************************/
Gia_StaAreDisjointVar(Gia_StaAre_t * p1,Gia_StaAre_t * p2,int nWords)450 static inline int Gia_StaAreDisjointVar( Gia_StaAre_t * p1, Gia_StaAre_t * p2, int nWords )
451 {
452 unsigned Word;
453 int w, iVar = -1;
454 for ( w = 0; w < nWords; w++ )
455 {
456 Word = (p1->pData[w] ^ p2->pData[w]) & ((p1->pData[w] ^ p2->pData[w]) >> 1) & 0x55555555;
457 if ( Word == 0 )
458 continue;
459 if ( !Gia_WordHasOneBit(Word) )
460 return -1;
461 // has exactly one bit
462 if ( iVar >= 0 )
463 return -1;
464 // the first variable of this type
465 iVar = 16 * w + Gia_WordFindFirstBit( Word ) / 2;
466 }
467 return iVar;
468 }
469
470 /**Function*************************************************************
471
472 Synopsis [Creates reachability manager.]
473
474 Description []
475
476 SideEffects []
477
478 SeeAlso []
479
480 ***********************************************************************/
Gia_ManAreCreate(Gia_Man_t * pAig)481 Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig )
482 {
483 Gia_ManAre_t * p;
484 assert( sizeof(Gia_ObjAre_t) == 16 );
485 p = ABC_CALLOC( Gia_ManAre_t, 1 );
486 p->pAig = pAig;
487 p->nWords = Abc_BitWordNum( 2 * Gia_ManRegNum(pAig) );
488 p->nSize = sizeof(Gia_StaAre_t)/4 + p->nWords;
489 p->ppObjs = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
490 p->ppStas = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
491 p->vCiTfos = Gia_ManDeriveCiTfo( pAig );
492 p->vCiLits = Vec_VecDupInt( p->vCiTfos );
493 p->vCubesA = Vec_IntAlloc( 100 );
494 p->vCubesB = Vec_IntAlloc( 100 );
495 p->iOutFail = -1;
496 return p;
497 }
498
499 /**Function*************************************************************
500
501 Synopsis [Deletes reachability manager.]
502
503 Description []
504
505 SideEffects []
506
507 SeeAlso []
508
509 ***********************************************************************/
Gia_ManAreFree(Gia_ManAre_t * p)510 void Gia_ManAreFree( Gia_ManAre_t * p )
511 {
512 int i;
513 Gia_ManStop( p->pAig );
514 if ( p->pNew )
515 Gia_ManStop( p->pNew );
516 Vec_IntFree( p->vCubesA );
517 Vec_IntFree( p->vCubesB );
518 Vec_VecFree( p->vCiTfos );
519 Vec_VecFree( p->vCiLits );
520 for ( i = 0; i < p->nObjPages; i++ )
521 ABC_FREE( p->ppObjs[i] );
522 ABC_FREE( p->ppObjs );
523 for ( i = 0; i < p->nStaPages; i++ )
524 ABC_FREE( p->ppStas[i] );
525 ABC_FREE( p->ppStas );
526 // ABC_FREE( p->pfUseless );
527 ABC_FREE( p );
528 }
529
530 /**Function*************************************************************
531
532 Synopsis [Returns new object.]
533
534 Description []
535
536 SideEffects []
537
538 SeeAlso []
539
540 ***********************************************************************/
Gia_ManAreCreateObj(Gia_ManAre_t * p)541 static inline Gia_ObjAre_t * Gia_ManAreCreateObj( Gia_ManAre_t * p )
542 {
543 if ( p->nObjs == p->nObjPages * MAX_ITEM_NUM )
544 {
545 if ( p->nObjPages == MAX_PAGE_NUM )
546 {
547 printf( "ERA manager has run out of memory after allocating 2B internal nodes.\n" );
548 return NULL;
549 }
550 p->ppObjs[p->nObjPages++] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * 4 );
551 if ( p->nObjs == 0 )
552 p->nObjs = 1;
553 }
554 return Gia_ManAreObjInt( p, p->nObjs++ );
555 }
556
557 /**Function*************************************************************
558
559 Synopsis [Returns new state.]
560
561 Description []
562
563 SideEffects []
564
565 SeeAlso []
566
567 ***********************************************************************/
Gia_ManAreCreateSta(Gia_ManAre_t * p)568 static inline Gia_StaAre_t * Gia_ManAreCreateSta( Gia_ManAre_t * p )
569 {
570 if ( p->nStas == p->nStaPages * MAX_ITEM_NUM )
571 {
572 if ( p->nStaPages == MAX_PAGE_NUM )
573 {
574 printf( "ERA manager has run out of memory after allocating 2B state cubes.\n" );
575 return NULL;
576 }
577 if ( p->ppStas[p->nStaPages] == NULL )
578 p->ppStas[p->nStaPages] = ABC_CALLOC( unsigned, MAX_ITEM_NUM * p->nSize );
579 p->nStaPages++;
580 if ( p->nStas == 0 )
581 {
582 p->nStas = 1;
583 // p->nUselessAlloc = (1 << 18);
584 // p->pfUseless = ABC_CALLOC( unsigned, p->nUselessAlloc );
585 }
586 // if ( p->nStas == p->nUselessAlloc * 32 )
587 // {
588 // p->nUselessAlloc *= 2;
589 // p->pfUseless = ABC_REALLOC( unsigned, p->pfUseless, p->nUselessAlloc );
590 // memset( p->pfUseless + p->nUselessAlloc/2, 0, sizeof(unsigned) * p->nUselessAlloc/2 );
591 // }
592 }
593 return Gia_ManAreStaInt( p, p->nStas++ );
594 }
595
596 /**Function*************************************************************
597
598 Synopsis [Recycles new state.]
599
600 Description []
601
602 SideEffects []
603
604 SeeAlso []
605
606 ***********************************************************************/
Gia_ManAreRycycleSta(Gia_ManAre_t * p,Gia_StaAre_t * pSta)607 static inline void Gia_ManAreRycycleSta( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
608 {
609 memset( pSta, 0, p->nSize << 2 );
610 if ( pSta == Gia_ManAreStaLast(p) )
611 {
612 p->nStas--;
613 if ( p->nStas == (p->nStaPages-1) * MAX_ITEM_NUM )
614 p->nStaPages--;
615 }
616 else
617 {
618 // Gia_StaSetUnused( pSta );
619 }
620 }
621
622 /**Function*************************************************************
623
624 Synopsis [Creates new state state from the latch values.]
625
626 Description []
627
628 SideEffects []
629
630 SeeAlso []
631
632 ***********************************************************************/
Gia_ManAreCreateStaNew(Gia_ManAre_t * p)633 static inline Gia_StaAre_t * Gia_ManAreCreateStaNew( Gia_ManAre_t * p )
634 {
635 Gia_StaAre_t * pSta;
636 Gia_Obj_t * pObj;
637 int i;
638 pSta = Gia_ManAreCreateSta( p );
639 Gia_ManForEachRi( p->pAig, pObj, i )
640 {
641 if ( pObj->Value == 0 )
642 Gia_StaSetValue0( pSta, i );
643 else if ( pObj->Value == 1 )
644 Gia_StaSetValue1( pSta, i );
645 }
646 return pSta;
647 }
648
649 /**Function*************************************************************
650
651 Synopsis [Creates new state state with latch init values.]
652
653 Description []
654
655 SideEffects []
656
657 SeeAlso []
658
659 ***********************************************************************/
Gia_ManAreCreateStaInit(Gia_ManAre_t * p)660 static inline Gia_StaAre_t * Gia_ManAreCreateStaInit( Gia_ManAre_t * p )
661 {
662 Gia_Obj_t * pObj;
663 int i;
664 Gia_ManForEachRi( p->pAig, pObj, i )
665 pObj->Value = 0;
666 return Gia_ManAreCreateStaNew( p );
667 }
668
669
670 /**Function*************************************************************
671
672 Synopsis [Prints the state cube.]
673
674 Description []
675
676 SideEffects []
677
678 SeeAlso []
679
680 ***********************************************************************/
Gia_ManArePrintCube(Gia_ManAre_t * p,Gia_StaAre_t * pSta)681 void Gia_ManArePrintCube( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
682 {
683 Gia_Obj_t * pObj;
684 int i, Count0 = 0, Count1 = 0, Count2 = 0;
685 printf( "%4d %4d : ", p->iStaCur, p->nStas-1 );
686 printf( "Prev %4d ", Gia_Ptr2Int(pSta->iPrev) );
687 printf( "%p ", pSta );
688 Gia_ManForEachRi( p->pAig, pObj, i )
689 {
690 if ( Gia_StaHasValue0(pSta, i) )
691 printf( "0" ), Count0++;
692 else if ( Gia_StaHasValue1(pSta, i) )
693 printf( "1" ), Count1++;
694 else
695 printf( "-" ), Count2++;
696 }
697 printf( " 0 =%3d", Count0 );
698 printf( " 1 =%3d", Count1 );
699 printf( " - =%3d", Count2 );
700 printf( "\n" );
701 }
702
703 /**Function*************************************************************
704
705 Synopsis [Counts the depth of state transitions leading ot this state.]
706
707 Description []
708
709 SideEffects []
710
711 SeeAlso []
712
713 ***********************************************************************/
Gia_ManAreDepth(Gia_ManAre_t * p,int iState)714 int Gia_ManAreDepth( Gia_ManAre_t * p, int iState )
715 {
716 Gia_StaAre_t * pSta;
717 int Counter = 0;
718 for ( pSta = Gia_ManAreStaInt(p, iState); Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) )
719 Counter++;
720 return Counter;
721 }
722
723 /**Function*************************************************************
724
725 Synopsis [Counts the number of cubes in the list.]
726
727 Description []
728
729 SideEffects []
730
731 SeeAlso []
732
733 ***********************************************************************/
Gia_ManAreListCountListUsed(Gia_ManAre_t * p,Gia_PtrAre_t Root)734 static inline int Gia_ManAreListCountListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root )
735 {
736 Gia_StaAre_t * pCube;
737 int Counter = 0;
738 Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
739 Counter += Gia_StaIsUsed(pCube);
740 return Counter;
741 }
742
743 /**Function*************************************************************
744
745 Synopsis [Counts the number of used cubes in the tree.]
746
747 Description []
748
749 SideEffects []
750
751 SeeAlso []
752
753 ***********************************************************************/
Gia_ManAreListCountUsed_rec(Gia_ManAre_t * p,Gia_PtrAre_t Root,int fTree)754 int Gia_ManAreListCountUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree )
755 {
756 Gia_ObjAre_t * pObj;
757 if ( !fTree )
758 return Gia_ManAreListCountListUsed( p, Root );
759 pObj = Gia_ManAreObj(p, Root);
760 return Gia_ManAreListCountUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) +
761 Gia_ManAreListCountUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) +
762 Gia_ManAreListCountUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) );
763 }
764
765 /**Function*************************************************************
766
767 Synopsis [Counts the number of used cubes in the tree.]
768
769 Description []
770
771 SideEffects []
772
773 SeeAlso []
774
775 ***********************************************************************/
Gia_ManAreListCountUsed(Gia_ManAre_t * p)776 static inline int Gia_ManAreListCountUsed( Gia_ManAre_t * p )
777 {
778 return Gia_ManAreListCountUsed_rec( p, p->Root, p->fTree );
779 }
780
781
782 /**Function*************************************************************
783
784 Synopsis [Prints used cubes in the list.]
785
786 Description []
787
788 SideEffects []
789
790 SeeAlso []
791
792 ***********************************************************************/
Gia_ManArePrintListUsed(Gia_ManAre_t * p,Gia_PtrAre_t Root)793 static inline int Gia_ManArePrintListUsed( Gia_ManAre_t * p, Gia_PtrAre_t Root )
794 {
795 Gia_StaAre_t * pCube;
796 Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, Root), pCube )
797 if ( Gia_StaIsUsed(pCube) )
798 Gia_ManArePrintCube( p, pCube );
799 return 1;
800 }
801
802 /**Function*************************************************************
803
804 Synopsis [Prints used cubes in the tree.]
805
806 Description []
807
808 SideEffects []
809
810 SeeAlso []
811
812 ***********************************************************************/
Gia_ManArePrintUsed_rec(Gia_ManAre_t * p,Gia_PtrAre_t Root,int fTree)813 int Gia_ManArePrintUsed_rec( Gia_ManAre_t * p, Gia_PtrAre_t Root, int fTree )
814 {
815 Gia_ObjAre_t * pObj;
816 if ( !fTree )
817 return Gia_ManArePrintListUsed( p, Root );
818 pObj = Gia_ManAreObj(p, Root);
819 return Gia_ManArePrintUsed_rec( p, pObj->F[0], Gia_ObjHasBranch0(pObj) ) +
820 Gia_ManArePrintUsed_rec( p, pObj->F[1], Gia_ObjHasBranch1(pObj) ) +
821 Gia_ManArePrintUsed_rec( p, pObj->F[2], Gia_ObjHasBranch2(pObj) );
822 }
823
824 /**Function*************************************************************
825
826 Synopsis [Prints used cubes in the tree.]
827
828 Description []
829
830 SideEffects []
831
832 SeeAlso []
833
834 ***********************************************************************/
Gia_ManArePrintUsed(Gia_ManAre_t * p)835 static inline int Gia_ManArePrintUsed( Gia_ManAre_t * p )
836 {
837 return Gia_ManArePrintUsed_rec( p, p->Root, p->fTree );
838 }
839
840
841 /**Function*************************************************************
842
843 Synopsis [Best var has max weight.]
844
845 Description [Weight is defined as the number of 0/1-lits minus the
846 absolute value of the diff between the number of 0-lits and 1-lits.]
847
848 SideEffects []
849
850 SeeAlso []
851
852 ***********************************************************************/
Gia_ManAreFindBestVar(Gia_ManAre_t * p,Gia_PtrAre_t List)853 int Gia_ManAreFindBestVar( Gia_ManAre_t * p, Gia_PtrAre_t List )
854 {
855 Gia_StaAre_t * pCube;
856 int Count0, Count1, Count2;
857 int iVarThis, iVarBest = -1, WeightThis, WeightBest = -1;
858 for ( iVarThis = 0; iVarThis < Gia_ManRegNum(p->pAig); iVarThis++ )
859 {
860 Count0 = Count1 = Count2 = 0;
861 Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, List), pCube )
862 {
863 if ( Gia_StaIsUnused(pCube) )
864 continue;
865 if ( Gia_StaHasValue0(pCube, iVarThis) )
866 Count0++;
867 else if ( Gia_StaHasValue1(pCube, iVarThis) )
868 Count1++;
869 else
870 Count2++;
871 }
872 // printf( "%4d : %5d %5d %5d Weight = %5d\n", iVarThis, Count0, Count1, Count2,
873 // Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0) );
874 if ( (!Count0 && !Count1) || (!Count0 && !Count2) || (!Count1 && !Count2) )
875 continue;
876 WeightThis = Count0 + Count1 - (Count0 > Count1 ? Count0 - Count1 : Count1 - Count0);
877 if ( WeightBest < WeightThis )
878 {
879 WeightBest = WeightThis;
880 iVarBest = iVarThis;
881 }
882 }
883 if ( iVarBest == -1 )
884 {
885 Gia_ManArePrintListUsed( p, List );
886 printf( "Error: Best variable not found!!!\n" );
887 }
888 assert( iVarBest != -1 );
889 return iVarBest;
890 }
891
892 /**Function*************************************************************
893
894 Synopsis [Rebalances the tree when cubes exceed the limit.]
895
896 Description []
897
898 SideEffects []
899
900 SeeAlso []
901
902 ***********************************************************************/
Gia_ManAreRebalance(Gia_ManAre_t * p,Gia_PtrAre_t * pRoot)903 static inline void Gia_ManAreRebalance( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot )
904 {
905 Gia_ObjAre_t * pNode;
906 Gia_StaAre_t * pCube;
907 Gia_PtrAre_t iCube, iNext;
908 assert( pRoot->nItem || pRoot->nPage );
909 pNode = Gia_ManAreCreateObj( p );
910 pNode->iVar = Gia_ManAreFindBestVar( p, *pRoot );
911 for ( iCube = *pRoot, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext;
912 Gia_StaIsGood(p, pCube);
913 iCube = iNext, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext )
914 {
915 if ( Gia_StaIsUnused(pCube) )
916 continue;
917 if ( Gia_StaHasValue0(pCube, pNode->iVar) )
918 pCube->iNext = pNode->F[0], pNode->F[0] = iCube, pNode->nStas0++;
919 else if ( Gia_StaHasValue1(pCube, pNode->iVar) )
920 pCube->iNext = pNode->F[1], pNode->F[1] = iCube, pNode->nStas1++;
921 else
922 pCube->iNext = pNode->F[2], pNode->F[2] = iCube, pNode->nStas2++;
923 }
924 *pRoot = Gia_Int2Ptr(p->nObjs - 1);
925 assert( pNode == Gia_ManAreObj(p, *pRoot) );
926 p->fTree = 1;
927 }
928
929 /**Function*************************************************************
930
931 Synopsis [Compresses the list by removing unused cubes.]
932
933 Description []
934
935 SideEffects []
936
937 SeeAlso []
938
939 ***********************************************************************/
Gia_ManAreCompress(Gia_ManAre_t * p,Gia_PtrAre_t * pRoot)940 static inline void Gia_ManAreCompress( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot )
941 {
942 Gia_StaAre_t * pCube;
943 Gia_PtrAre_t iList = *pRoot;
944 Gia_PtrAre_t iCube, iNext;
945 assert( pRoot->nItem || pRoot->nPage );
946 pRoot->nItem = 0;
947 pRoot->nPage = 0;
948 for ( iCube = iList, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext;
949 Gia_StaIsGood(p, pCube);
950 iCube = iNext, pCube = Gia_ManAreSta(p, iCube), iNext = pCube->iNext )
951 {
952 if ( Gia_StaIsUnused(pCube) )
953 continue;
954 pCube->iNext = *pRoot;
955 *pRoot = iCube;
956 }
957 }
958
959
960 /**Function*************************************************************
961
962 Synopsis [Checks if the state exists in the list.]
963
964 Description [The state may be sharped.]
965
966 SideEffects []
967
968 SeeAlso []
969
970 ***********************************************************************/
Gia_ManAreCubeCheckList(Gia_ManAre_t * p,Gia_PtrAre_t * pRoot,Gia_StaAre_t * pSta)971 static inline int Gia_ManAreCubeCheckList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
972 {
973 int fVerbose = 0;
974 Gia_StaAre_t * pCube;
975 int iVar;
976 if ( fVerbose )
977 {
978 printf( "Trying cube: " );
979 Gia_ManArePrintCube( p, pSta );
980 }
981 Gia_ManAreForEachCubeList( p, Gia_ManAreSta(p, *pRoot), pCube )
982 {
983 p->nChecks++;
984 if ( Gia_StaIsUnused( pCube ) )
985 continue;
986 if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
987 continue;
988 if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
989 {
990 if ( fVerbose )
991 {
992 printf( "Contained in " );
993 Gia_ManArePrintCube( p, pCube );
994 }
995 Gia_ManAreRycycleSta( p, pSta );
996 return 0;
997 }
998 if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
999 {
1000 if ( fVerbose )
1001 {
1002 printf( "Contains " );
1003 Gia_ManArePrintCube( p, pCube );
1004 }
1005 Gia_StaSetUnused( pCube );
1006 continue;
1007 }
1008 iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
1009 if ( iVar == -1 )
1010 continue;
1011 if ( fVerbose )
1012 {
1013 printf( "Sharped by " );
1014 Gia_ManArePrintCube( p, pCube );
1015 Gia_ManArePrintCube( p, pSta );
1016 }
1017 // printf( "%d %d\n", Gia_StaAreDashNum( pSta, pCube, p->nWords ), Gia_StaAreSharpVar( pSta, pCube, p->nWords ) );
1018 assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) );
1019 assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) );
1020 if ( Gia_StaHasValue0(pCube, iVar) )
1021 Gia_StaSetValue1( pSta, iVar );
1022 else
1023 Gia_StaSetValue0( pSta, iVar );
1024 // return Gia_ManAreCubeCheckList( p, pRoot, pSta );
1025 }
1026 return 1;
1027 }
1028
1029 /**Function*************************************************************
1030
1031 Synopsis [Adds new state to the list.]
1032
1033 Description []
1034
1035 SideEffects []
1036
1037 SeeAlso []
1038
1039 ***********************************************************************/
Gia_ManAreCubeAddToList(Gia_ManAre_t * p,Gia_PtrAre_t * pRoot,Gia_StaAre_t * pSta)1040 static inline void Gia_ManAreCubeAddToList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
1041 {
1042 int fVerbose = 0;
1043 pSta->iNext = *pRoot;
1044 *pRoot = Gia_Int2Ptr( p->nStas - 1 );
1045 assert( pSta == Gia_ManAreSta(p, *pRoot) );
1046 if ( fVerbose )
1047 {
1048 printf( "Adding cube: " );
1049 Gia_ManArePrintCube( p, pSta );
1050 //printf( "\n" );
1051 }
1052 }
1053
1054 /**Function*************************************************************
1055
1056 Synopsis [Checks if the cube like this exists in the tree.]
1057
1058 Description []
1059
1060 SideEffects []
1061
1062 SeeAlso []
1063
1064 ***********************************************************************/
Gia_ManAreCubeCheckTree_rec(Gia_ManAre_t * p,Gia_ObjAre_t * pObj,Gia_StaAre_t * pSta)1065 int Gia_ManAreCubeCheckTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
1066 {
1067 int RetValue;
1068 if ( Gia_StaHasValue0(pSta, pObj->iVar) )
1069 {
1070 if ( Gia_ObjHasBranch0(pObj) )
1071 RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
1072 else
1073 RetValue = Gia_ManAreCubeCheckList( p, pObj->F, pSta );
1074 if ( RetValue == 0 )
1075 return 0;
1076 }
1077 else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
1078 {
1079 if ( Gia_ObjHasBranch1(pObj) )
1080 RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
1081 else
1082 RetValue = Gia_ManAreCubeCheckList( p, pObj->F + 1, pSta );
1083 if ( RetValue == 0 )
1084 return 0;
1085 }
1086 if ( Gia_ObjHasBranch2(pObj) )
1087 return Gia_ManAreCubeCheckTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
1088 return Gia_ManAreCubeCheckList( p, pObj->F + 2, pSta );
1089 }
1090
1091 /**Function*************************************************************
1092
1093 Synopsis [Adds new cube to the tree.]
1094
1095 Description []
1096
1097 SideEffects []
1098
1099 SeeAlso []
1100
1101 ***********************************************************************/
Gia_ManAreCubeAddToTree_rec(Gia_ManAre_t * p,Gia_ObjAre_t * pObj,Gia_StaAre_t * pSta)1102 void Gia_ManAreCubeAddToTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
1103 {
1104 if ( Gia_StaHasValue0(pSta, pObj->iVar) )
1105 {
1106 if ( Gia_ObjHasBranch0(pObj) )
1107 Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
1108 else
1109 {
1110 Gia_ManAreCubeAddToList( p, pObj->F, pSta );
1111 if ( ++pObj->nStas0 == MAX_CUBE_NUM )
1112 {
1113 pObj->nStas0 = Gia_ManAreListCountListUsed( p, pObj->F[0] );
1114 if ( pObj->nStas0 < MAX_CUBE_NUM/2 )
1115 Gia_ManAreCompress( p, pObj->F );
1116 else
1117 {
1118 Gia_ManAreRebalance( p, pObj->F );
1119 pObj->nStas0 = 0;
1120 }
1121 }
1122 }
1123 }
1124 else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
1125 {
1126 if ( Gia_ObjHasBranch1(pObj) )
1127 Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
1128 else
1129 {
1130 Gia_ManAreCubeAddToList( p, pObj->F+1, pSta );
1131 if ( ++pObj->nStas1 == MAX_CUBE_NUM )
1132 {
1133 pObj->nStas1 = Gia_ManAreListCountListUsed( p, pObj->F[1] );
1134 if ( pObj->nStas1 < MAX_CUBE_NUM/2 )
1135 Gia_ManAreCompress( p, pObj->F+1 );
1136 else
1137 {
1138 Gia_ManAreRebalance( p, pObj->F+1 );
1139 pObj->nStas1 = 0;
1140 }
1141 }
1142 }
1143 }
1144 else
1145 {
1146 if ( Gia_ObjHasBranch2(pObj) )
1147 Gia_ManAreCubeAddToTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
1148 else
1149 {
1150 Gia_ManAreCubeAddToList( p, pObj->F+2, pSta );
1151 if ( ++pObj->nStas2 == MAX_CUBE_NUM )
1152 {
1153 pObj->nStas2 = Gia_ManAreListCountListUsed( p, pObj->F[2] );
1154 if ( pObj->nStas2 < MAX_CUBE_NUM/2 )
1155 Gia_ManAreCompress( p, pObj->F+2 );
1156 else
1157 {
1158 Gia_ManAreRebalance( p, pObj->F+2 );
1159 pObj->nStas2 = 0;
1160 }
1161 }
1162 }
1163 }
1164 }
1165
1166
1167
1168 /**Function*************************************************************
1169
1170 Synopsis [Collects overlapping cubes in the list.]
1171
1172 Description []
1173
1174 SideEffects []
1175
1176 SeeAlso []
1177
1178 ***********************************************************************/
Gia_ManAreCubeCollectList(Gia_ManAre_t * p,Gia_PtrAre_t * pRoot,Gia_StaAre_t * pSta)1179 static inline int Gia_ManAreCubeCollectList( Gia_ManAre_t * p, Gia_PtrAre_t * pRoot, Gia_StaAre_t * pSta )
1180 {
1181 Gia_StaAre_t * pCube;
1182 int iCube;
1183 Gia_ManAreForEachCubeList2( p, *pRoot, pCube, iCube )
1184 {
1185 if ( Gia_StaIsUnused( pCube ) )
1186 continue;
1187 if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
1188 {
1189 /*
1190 int iVar;
1191 p->nDisjs++;
1192 iVar = Gia_StaAreDisjointVar( pSta, pCube, p->nWords );
1193 if ( iVar >= 0 )
1194 {
1195 p->nDisjs2++;
1196 if ( iCube > p->iStaCur )
1197 p->nDisjs3++;
1198 }
1199 */
1200 continue;
1201 }
1202 // p->nCompares++;
1203 // p->nEquals += Gia_StaAreEqual( pSta, pCube, p->nWords );
1204 if ( iCube <= p->iStaCur )
1205 Vec_IntPush( p->vCubesA, iCube );
1206 else
1207 Vec_IntPush( p->vCubesB, iCube );
1208 }
1209 return 1;
1210 }
1211
1212 /**Function*************************************************************
1213
1214 Synopsis [Collects overlapping cubes in the tree.]
1215
1216 Description []
1217
1218 SideEffects []
1219
1220 SeeAlso []
1221
1222 ***********************************************************************/
Gia_ManAreCubeCollectTree_rec(Gia_ManAre_t * p,Gia_ObjAre_t * pObj,Gia_StaAre_t * pSta)1223 int Gia_ManAreCubeCollectTree_rec( Gia_ManAre_t * p, Gia_ObjAre_t * pObj, Gia_StaAre_t * pSta )
1224 {
1225 int RetValue;
1226 if ( Gia_StaHasValue0(pSta, pObj->iVar) )
1227 {
1228 if ( Gia_ObjHasBranch0(pObj) )
1229 RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj0(p, pObj), pSta );
1230 else
1231 RetValue = Gia_ManAreCubeCollectList( p, pObj->F, pSta );
1232 if ( RetValue == 0 )
1233 return 0;
1234 }
1235 else if ( Gia_StaHasValue1(pSta, pObj->iVar) )
1236 {
1237 if ( Gia_ObjHasBranch1(pObj) )
1238 RetValue = Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj1(p, pObj), pSta );
1239 else
1240 RetValue = Gia_ManAreCubeCollectList( p, pObj->F + 1, pSta );
1241 if ( RetValue == 0 )
1242 return 0;
1243 }
1244 if ( Gia_ObjHasBranch2(pObj) )
1245 return Gia_ManAreCubeCollectTree_rec( p, Gia_ObjNextObj2(p, pObj), pSta );
1246 return Gia_ManAreCubeCollectList( p, pObj->F + 2, pSta );
1247 }
1248
1249 /**Function*************************************************************
1250
1251 Synopsis [Checks if the cube like this exists in the tree.]
1252
1253 Description []
1254
1255 SideEffects []
1256
1257 SeeAlso []
1258
1259 ***********************************************************************/
Gia_ManAreCubeCheckTree(Gia_ManAre_t * p,Gia_StaAre_t * pSta)1260 int Gia_ManAreCubeCheckTree( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
1261 {
1262 Gia_StaAre_t * pCube;
1263 int i, iVar;
1264 assert( p->fTree );
1265 Vec_IntClear( p->vCubesA );
1266 Vec_IntClear( p->vCubesB );
1267 Gia_ManAreCubeCollectTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
1268 // if ( p->nStas > 3000 )
1269 // printf( "%d %d \n", Vec_IntSize(p->vCubesA), Vec_IntSize(p->vCubesB) );
1270 // Vec_IntSort( p->vCubesA, 0 );
1271 // Vec_IntSort( p->vCubesB, 0 );
1272 Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i )
1273 {
1274 if ( Gia_StaIsUnused( pCube ) )
1275 continue;
1276 if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
1277 continue;
1278 if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
1279 {
1280 Gia_ManAreRycycleSta( p, pSta );
1281 return 0;
1282 }
1283 if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
1284 {
1285 Gia_StaSetUnused( pCube );
1286 continue;
1287 }
1288 iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
1289 if ( iVar == -1 )
1290 continue;
1291 assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) );
1292 assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) );
1293 if ( Gia_StaHasValue0(pCube, iVar) )
1294 Gia_StaSetValue1( pSta, iVar );
1295 else
1296 Gia_StaSetValue0( pSta, iVar );
1297 return Gia_ManAreCubeCheckTree( p, pSta );
1298 }
1299 Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i )
1300 {
1301 if ( Gia_StaIsUnused( pCube ) )
1302 continue;
1303 if ( Gia_StaAreDisjoint( pSta, pCube, p->nWords ) )
1304 continue;
1305 if ( Gia_StaAreContain( pCube, pSta, p->nWords ) )
1306 {
1307 Gia_ManAreRycycleSta( p, pSta );
1308 return 0;
1309 }
1310 if ( Gia_StaAreContain( pSta, pCube, p->nWords ) )
1311 {
1312 Gia_StaSetUnused( pCube );
1313 continue;
1314 }
1315 iVar = Gia_StaAreSharpVar( pSta, pCube, p->nWords );
1316 if ( iVar == -1 )
1317 continue;
1318 assert( !Gia_StaHasValue0(pSta, iVar) && !Gia_StaHasValue1(pSta, iVar) );
1319 assert( Gia_StaHasValue0(pCube, iVar) ^ Gia_StaHasValue1(pCube, iVar) );
1320 if ( Gia_StaHasValue0(pCube, iVar) )
1321 Gia_StaSetValue1( pSta, iVar );
1322 else
1323 Gia_StaSetValue0( pSta, iVar );
1324 return Gia_ManAreCubeCheckTree( p, pSta );
1325 }
1326 /*
1327 if ( p->nStas > 3000 )
1328 {
1329 printf( "Trying cube: " );
1330 Gia_ManArePrintCube( p, pSta );
1331 Gia_ManAreForEachCubeVec( p->vCubesA, p, pCube, i )
1332 {
1333 printf( "aaaaaaaaaaaa %5d ", Vec_IntEntry(p->vCubesA,i) );
1334 Gia_ManArePrintCube( p, pCube );
1335 }
1336 Gia_ManAreForEachCubeVec( p->vCubesB, p, pCube, i )
1337 {
1338 printf( "bbbbbbbbbbbb %5d ", Vec_IntEntry(p->vCubesB,i) );
1339 Gia_ManArePrintCube( p, pCube );
1340 }
1341 }
1342 */
1343 return 1;
1344 }
1345
1346 /**Function*************************************************************
1347
1348 Synopsis [Processes the new cube.]
1349
1350 Description []
1351
1352 SideEffects []
1353
1354 SeeAlso []
1355
1356 ***********************************************************************/
Gia_ManAreCubeProcess(Gia_ManAre_t * p,Gia_StaAre_t * pSta)1357 static inline int Gia_ManAreCubeProcess( Gia_ManAre_t * p, Gia_StaAre_t * pSta )
1358 {
1359 int RetValue;
1360 p->nChecks = 0;
1361 if ( !p->fTree && p->nStas == MAX_CUBE_NUM )
1362 Gia_ManAreRebalance( p, &p->Root );
1363 if ( p->fTree )
1364 {
1365 // RetValue = Gia_ManAreCubeCheckTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
1366 RetValue = Gia_ManAreCubeCheckTree( p, pSta );
1367 if ( RetValue )
1368 Gia_ManAreCubeAddToTree_rec( p, Gia_ManAreObj(p, p->Root), pSta );
1369 }
1370 else
1371 {
1372 RetValue = Gia_ManAreCubeCheckList( p, &p->Root, pSta );
1373 if ( RetValue )
1374 Gia_ManAreCubeAddToList( p, &p->Root, pSta );
1375 }
1376 // printf( "%d ", p->nChecks );
1377 return RetValue;
1378 }
1379
1380
1381 /**Function*************************************************************
1382
1383 Synopsis [Returns the most used CI, or NULL if condition is met.]
1384
1385 Description []
1386
1387 SideEffects []
1388
1389 SeeAlso []
1390
1391 ***********************************************************************/
Gia_ManAreMostUsedPi_rec(Gia_Man_t * p,Gia_Obj_t * pObj)1392 void Gia_ManAreMostUsedPi_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1393 {
1394 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1395 return;
1396 Gia_ObjSetTravIdCurrent(p, pObj);
1397 if ( Gia_ObjIsCi(pObj) )
1398 {
1399 pObj->Value++;
1400 return;
1401 }
1402 assert( Gia_ObjIsAnd(pObj) );
1403 Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin0(pObj) );
1404 Gia_ManAreMostUsedPi_rec( p, Gia_ObjFanin1(pObj) );
1405 }
1406
1407 /**Function*************************************************************
1408
1409 Synopsis [Returns the most used CI, or NULL if condition is met.]
1410
1411 Description []
1412
1413 SideEffects []
1414
1415 SeeAlso []
1416
1417 ***********************************************************************/
Gia_ManAreMostUsedPi(Gia_ManAre_t * p)1418 static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p )
1419 {
1420 Gia_Obj_t * pObj, * pObjMax = NULL;
1421 int i;
1422 // clean CI counters
1423 Gia_ManForEachCi( p->pNew, pObj, i )
1424 pObj->Value = 0;
1425 // traverse from each register output
1426 Gia_ManForEachRi( p->pAig, pObj, i )
1427 {
1428 if ( pObj->Value <= 1 )
1429 continue;
1430 Gia_ManIncrementTravId( p->pNew );
1431 Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Abc_Lit2Var(pObj->Value)) );
1432 }
1433 // check the CI counters
1434 Gia_ManForEachCi( p->pNew, pObj, i )
1435 if ( pObjMax == NULL || pObjMax->Value < pObj->Value )
1436 pObjMax = pObj;
1437 // return the result
1438 return pObjMax->Value > 1 ? pObjMax : NULL;
1439 }
1440
1441 /**Function*************************************************************
1442
1443 Synopsis [Counts maximum support of primary outputs.]
1444
1445 Description []
1446
1447 SideEffects []
1448
1449 SeeAlso []
1450
1451 ***********************************************************************/
Gia_ManCheckPOs_rec(Gia_Man_t * p,Gia_Obj_t * pObj)1452 int Gia_ManCheckPOs_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1453 {
1454 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1455 return 0;
1456 Gia_ObjSetTravIdCurrent(p, pObj);
1457 if ( Gia_ObjIsCi(pObj) )
1458 return 1;
1459 assert( Gia_ObjIsAnd(pObj) );
1460 return Gia_ManCheckPOs_rec( p, Gia_ObjFanin0(pObj) ) +
1461 Gia_ManCheckPOs_rec( p, Gia_ObjFanin1(pObj) );
1462 }
1463
1464 /**Function*************************************************************
1465
1466 Synopsis [Counts maximum support of primary outputs.]
1467
1468 Description []
1469
1470 SideEffects []
1471
1472 SeeAlso []
1473
1474 ***********************************************************************/
Gia_ManCheckPOs(Gia_ManAre_t * p)1475 static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
1476 {
1477 Gia_Obj_t * pObj, * pObjNew;
1478 int i, CountCur, CountMax = 0;
1479 Gia_ManForEachPo( p->pAig, pObj, i )
1480 {
1481 pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
1482 if ( Gia_ObjIsConst0(pObjNew) )
1483 CountCur = 0;
1484 else
1485 {
1486 Gia_ManIncrementTravId( p->pNew );
1487 CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew );
1488 }
1489 CountMax = Abc_MaxInt( CountMax, CountCur );
1490 }
1491 return CountMax;
1492 }
1493
1494 /**Function*************************************************************
1495
1496 Synopsis [Returns the status of the primary outputs.]
1497
1498 Description []
1499
1500 SideEffects []
1501
1502 SeeAlso []
1503
1504 ***********************************************************************/
Gia_ManCheckPOstatus(Gia_ManAre_t * p)1505 static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p )
1506 {
1507 Gia_Obj_t * pObj, * pObjNew;
1508 int i;
1509 Gia_ManForEachPo( p->pAig, pObj, i )
1510 {
1511 pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
1512 if ( Gia_ObjIsConst0(pObjNew) )
1513 {
1514 if ( Abc_LitIsCompl(pObj->Value) )
1515 {
1516 p->iOutFail = i;
1517 return 1;
1518 }
1519 }
1520 else
1521 {
1522 p->iOutFail = i;
1523 // printf( "To fix later: PO may be assertable.\n" );
1524 return 1;
1525 }
1526 }
1527 return 0;
1528 }
1529
1530 /**Function*************************************************************
1531
1532 Synopsis [Derives next state cubes.]
1533
1534 Description []
1535
1536 SideEffects []
1537
1538 SeeAlso []
1539
1540 ***********************************************************************/
Gia_ManAreDeriveNexts_rec(Gia_ManAre_t * p,Gia_PtrAre_t Sta)1541 int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
1542 {
1543 Gia_Obj_t * pPivot;
1544 Vec_Int_t * vLits, * vTfos;
1545 Gia_Obj_t * pObj;
1546 int i;
1547 abctime clk;
1548 if ( ++p->nRecCalls == MAX_CALL_NUM )
1549 return 0;
1550 if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL )
1551 {
1552 Gia_StaAre_t * pNew;
1553 clk = Abc_Clock();
1554 pNew = Gia_ManAreCreateStaNew( p );
1555 pNew->iPrev = Sta;
1556 p->fStopped = (p->fMiter && (Gia_ManCheckPOstatus(p) & 1));
1557 if ( p->fStopped )
1558 {
1559 assert( p->pTarget == NULL );
1560 p->pTarget = pNew;
1561 return 1;
1562 }
1563 Gia_ManAreCubeProcess( p, pNew );
1564 p->timeCube += Abc_Clock() - clk;
1565 return p->fStopped;
1566 }
1567 // remember values in the cone and perform update
1568 vTfos = Vec_VecEntryInt( p->vCiTfos, Gia_ObjCioId(pPivot) );
1569 vLits = Vec_VecEntryInt( p->vCiLits, Gia_ObjCioId(pPivot) );
1570 assert( Vec_IntSize(vTfos) == Vec_IntSize(vLits) );
1571 Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
1572 {
1573 Vec_IntWriteEntry( vLits, i, pObj->Value );
1574 if ( Gia_ObjIsAnd(pObj) )
1575 pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1576 else if ( Gia_ObjIsCo(pObj) )
1577 pObj->Value = Gia_ObjFanin0Copy(pObj);
1578 else
1579 {
1580 assert( Gia_ObjIsCi(pObj) );
1581 pObj->Value = 0;
1582 }
1583 }
1584 if ( Gia_ManAreDeriveNexts_rec( p, Sta ) )
1585 return 1;
1586 // compute different values
1587 Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
1588 {
1589 if ( Gia_ObjIsAnd(pObj) )
1590 pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1591 else if ( Gia_ObjIsCo(pObj) )
1592 pObj->Value = Gia_ObjFanin0Copy(pObj);
1593 else
1594 {
1595 assert( Gia_ObjIsCi(pObj) );
1596 pObj->Value = 1;
1597 }
1598 }
1599 if ( Gia_ManAreDeriveNexts_rec( p, Sta ) )
1600 return 1;
1601 // reset the original values
1602 Gia_ManForEachObjVec( vTfos, p->pAig, pObj, i )
1603 pObj->Value = Vec_IntEntry( vLits, i );
1604 return 0;
1605 }
1606
1607 /**Function*************************************************************
1608
1609 Synopsis [Derives next state cubes.]
1610
1611 Description []
1612
1613 SideEffects []
1614
1615 SeeAlso []
1616
1617 ***********************************************************************/
Gia_ManAreDeriveNexts(Gia_ManAre_t * p,Gia_PtrAre_t Sta)1618 int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
1619 {
1620 Gia_StaAre_t * pSta;
1621 Gia_Obj_t * pObj;
1622 int i, RetValue;
1623 abctime clk = Abc_Clock();
1624 pSta = Gia_ManAreSta( p, Sta );
1625 if ( Gia_StaIsUnused(pSta) )
1626 return 0;
1627 // recycle the manager
1628 if ( p->pNew && Gia_ManObjNum(p->pNew) > 1000000 )
1629 {
1630 Gia_ManStop( p->pNew );
1631 p->pNew = NULL;
1632 }
1633 // allocate the manager
1634 if ( p->pNew == NULL )
1635 {
1636 p->pNew = Gia_ManStart( 10 * Gia_ManObjNum(p->pAig) );
1637 Gia_ManIncrementTravId( p->pNew );
1638 Gia_ManHashAlloc( p->pNew );
1639 Gia_ManConst0(p->pAig)->Value = 0;
1640 Gia_ManForEachCi( p->pAig, pObj, i )
1641 pObj->Value = Gia_ManAppendCi(p->pNew);
1642 }
1643 Gia_ManForEachRo( p->pAig, pObj, i )
1644 {
1645 if ( Gia_StaHasValue0( pSta, i ) )
1646 pObj->Value = 0;
1647 else if ( Gia_StaHasValue1( pSta, i ) )
1648 pObj->Value = 1;
1649 else // don't-care literal
1650 pObj->Value = Abc_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
1651 }
1652 Gia_ManForEachAnd( p->pAig, pObj, i )
1653 pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1654 Gia_ManForEachCo( p->pAig, pObj, i )
1655 pObj->Value = Gia_ObjFanin0Copy(pObj);
1656
1657 // perform case-splitting
1658 p->nRecCalls = 0;
1659 RetValue = Gia_ManAreDeriveNexts_rec( p, Sta );
1660 if ( p->nRecCalls >= MAX_CALL_NUM )
1661 {
1662 printf( "Exceeded the limit on the number of transitions from a state cube (%d).\n", MAX_CALL_NUM );
1663 p->fStopped = 1;
1664 }
1665 // printf( "%d ", p->nRecCalls );
1666 //printf( "%d ", Gia_ManObjNum(p->pNew) );
1667 p->timeAig += Abc_Clock() - clk;
1668 return RetValue;
1669 }
1670
1671
1672 /**Function*************************************************************
1673
1674 Synopsis [Prints the report]
1675
1676 Description []
1677
1678 SideEffects []
1679
1680 SeeAlso []
1681
1682 ***********************************************************************/
Gia_ManArePrintReport(Gia_ManAre_t * p,abctime Time,int fFinal)1683 void Gia_ManArePrintReport( Gia_ManAre_t * p, abctime Time, int fFinal )
1684 {
1685 printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f MB. ",
1686 p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur),
1687 (sizeof(Gia_ManAre_t) + 4.0*Gia_ManRegNum(p->pAig) + 8.0*MAX_PAGE_NUM +
1688 4.0*p->nStaPages*p->nSize*MAX_ITEM_NUM + 16.0*p->nObjPages*MAX_ITEM_NUM)/(1<<20) );
1689 if ( fFinal )
1690 {
1691 ABC_PRT( "Time", Abc_Clock() - Time );
1692 }
1693 else
1694 {
1695 ABC_PRTr( "Time", Abc_Clock() - Time );
1696 }
1697 }
1698
1699 /**Function*************************************************************
1700
1701 Synopsis [Performs explicit reachability.]
1702
1703 Description []
1704
1705 SideEffects []
1706
1707 SeeAlso []
1708
1709 ***********************************************************************/
Gia_ManArePerform(Gia_Man_t * pAig,int nStatesMax,int fMiter,int fVerbose)1710 int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose )
1711 {
1712 // extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose );
1713 extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast );
1714 Gia_ManAre_t * p;
1715 abctime clk = Abc_Clock();
1716 int RetValue = 1;
1717 if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM )
1718 {
1719 printf( "Currently can only handle circuit with up to %d registers.\n", MAX_VARS_NUM );
1720 return -1;
1721 }
1722 ABC_FREE( pAig->pCexSeq );
1723 // p = Gia_ManAreCreate( Gia_ManCompress2(pAig, 0, 0) );
1724 p = Gia_ManAreCreate( Gia_ManDup(pAig) );
1725 p->fMiter = fMiter;
1726 Gia_ManAreCubeProcess( p, Gia_ManAreCreateStaInit(p) );
1727 for ( p->iStaCur = 1; p->iStaCur < p->nStas; p->iStaCur++ )
1728 {
1729 // printf( "Explored state %d. Total cubes %d.\n", p->iStaCur, p->nStas-1 );
1730 if ( Gia_ManAreDeriveNexts( p, Gia_Int2Ptr(p->iStaCur) ) || p->nStas > nStatesMax )
1731 pAig->pCexSeq = Gia_ManAreDeriveCex( p, p->pTarget );
1732 if ( p->fStopped )
1733 {
1734 RetValue = -1;
1735 break;
1736 }
1737 if ( fVerbose )//&& p->iStaCur % 5000 == 0 )
1738 Gia_ManArePrintReport( p, clk, 0 );
1739 }
1740 Gia_ManArePrintReport( p, clk, 1 );
1741 printf( "%s after finding %d state cubes (%d not contained) with depth %d. ",
1742 p->fStopped ? "Stopped" : "Completed",
1743 p->nStas, Gia_ManAreListCountUsed(p),
1744 Gia_ManAreDepth(p, p->iStaCur-1) );
1745 ABC_PRT( "Time", Abc_Clock() - clk );
1746 if ( pAig->pCexSeq != NULL )
1747 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n",
1748 p->iStaCur, pAig->pName, Gia_ManAreDepth(p, p->iStaCur)-1 );
1749 if ( fVerbose )
1750 {
1751 ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube, Abc_Clock() - clk );
1752 ABC_PRTP( "Containment", p->timeCube, Abc_Clock() - clk );
1753 ABC_PRTP( "Other ", Abc_Clock() - clk - p->timeAig, Abc_Clock() - clk );
1754 ABC_PRTP( "TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1755 }
1756 if ( Gia_ManRegNum(pAig) <= 30 )
1757 {
1758 clk = Abc_Clock();
1759 printf( "The number of unique state minterms in computed state cubes is %d. ", Gia_ManCountMinterms(p) );
1760 ABC_PRT( "Time", Abc_Clock() - clk );
1761 }
1762 // printf( "Compares = %d. Equals = %d. Disj = %d. Disj2 = %d. Disj3 = %d.\n",
1763 // p->nCompares, p->nEquals, p->nDisjs, p->nDisjs2, p->nDisjs3 );
1764 // Gia_ManAreFindBestVar( p, Gia_ManAreSta(p, p->Root) );
1765 // Gia_ManArePrintUsed( p );
1766 Gia_ManAreFree( p );
1767 // verify
1768 if ( pAig->pCexSeq )
1769 {
1770 if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
1771 printf( "Generated counter-example is INVALID. \n" );
1772 else
1773 printf( "Generated counter-example verified correctly. \n" );
1774 return 0;
1775 }
1776 return RetValue;
1777 }
1778
1779 ABC_NAMESPACE_IMPL_END
1780
1781 #include "giaAig.h"
1782 #include "sat/cnf/cnf.h"
1783 #include "sat/bsat/satSolver.h"
1784
1785 ABC_NAMESPACE_IMPL_START
1786
1787
1788 /**Function*************************************************************
1789
1790 Synopsis []
1791
1792 Description []
1793
1794 SideEffects []
1795
1796 SeeAlso []
1797
1798 ***********************************************************************/
Gia_ManAreDeriveCexSatStart(Gia_ManAre_t * p)1799 void Gia_ManAreDeriveCexSatStart( Gia_ManAre_t * p )
1800 {
1801 Aig_Man_t * pAig2;
1802 Cnf_Dat_t * pCnf;
1803 assert( p->pSat == NULL );
1804 pAig2 = Gia_ManToAig( p->pAig, 0 );
1805 Aig_ManSetRegNum( pAig2, 0 );
1806 pCnf = Cnf_Derive( pAig2, Gia_ManCoNum(p->pAig) );
1807 p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
1808 p->vSatNumCis = Cnf_DataCollectCiSatNums( pCnf, pAig2 );
1809 p->vSatNumCos = Cnf_DataCollectCoSatNums( pCnf, pAig2 );
1810 Cnf_DataFree( pCnf );
1811 Aig_ManStop( pAig2 );
1812 p->vAssumps = Vec_IntAlloc( 100 );
1813 p->vCofVars = Vec_IntAlloc( 100 );
1814 }
1815
1816 /**Function*************************************************************
1817
1818 Synopsis []
1819
1820 Description []
1821
1822 SideEffects []
1823
1824 SeeAlso []
1825
1826 ***********************************************************************/
Gia_ManAreDeriveCexSatStop(Gia_ManAre_t * p)1827 void Gia_ManAreDeriveCexSatStop( Gia_ManAre_t * p )
1828 {
1829 assert( p->pSat != NULL );
1830 assert( p->pTarget != NULL );
1831 sat_solver_delete( (sat_solver *)p->pSat );
1832 Vec_IntFree( p->vSatNumCis );
1833 Vec_IntFree( p->vSatNumCos );
1834 Vec_IntFree( p->vAssumps );
1835 Vec_IntFree( p->vCofVars );
1836 p->pTarget = NULL;
1837 p->pSat = NULL;
1838 }
1839
1840 /**Function*************************************************************
1841
1842 Synopsis [Computes satisfying assignment in one timeframe.]
1843
1844 Description [Returns the vector of integers represeting PIO ids
1845 of the primary inputs that should be 1 in the counter-example.]
1846
1847 SideEffects []
1848
1849 SeeAlso []
1850
1851 ***********************************************************************/
Gia_ManAreDeriveCexSat(Gia_ManAre_t * p,Gia_StaAre_t * pCur,Gia_StaAre_t * pNext,int iOutFailed)1852 void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t * pNext, int iOutFailed )
1853 {
1854 int i, status;
1855 // make assuptions
1856 Vec_IntClear( p->vAssumps );
1857 for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
1858 {
1859 if ( Gia_StaHasValue0(pCur, i) )
1860 Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
1861 else if ( Gia_StaHasValue1(pCur, i) )
1862 Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
1863 }
1864 if ( pNext )
1865 for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
1866 {
1867 if ( Gia_StaHasValue0(pNext, i) )
1868 Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
1869 else if ( Gia_StaHasValue1(pNext, i) )
1870 Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
1871 }
1872 if ( iOutFailed >= 0 )
1873 {
1874 assert( iOutFailed < Gia_ManPoNum(p->pAig) );
1875 Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
1876 }
1877 // solve SAT
1878 status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps),
1879 (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1880 if ( status != l_True )
1881 {
1882 printf( "SAT problem is not satisfiable. Failure...\n" );
1883 return;
1884 }
1885 assert( status == l_True );
1886 // check the model
1887 Vec_IntClear( p->vCofVars );
1888 for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
1889 {
1890 if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, i) ) )
1891 Vec_IntPush( p->vCofVars, i );
1892 }
1893 // write the current state
1894 for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
1895 {
1896 if ( Gia_StaHasValue0(pCur, i) )
1897 assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 );
1898 else if ( Gia_StaHasValue1(pCur, i) )
1899 assert( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 1 );
1900 // set don't-care value
1901 if ( sat_solver_var_value( (sat_solver *)p->pSat, Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i) ) == 0 )
1902 Gia_StaSetValue0( pCur, i );
1903 else
1904 Gia_StaSetValue1( pCur, i );
1905 }
1906 }
1907
1908 /**Function*************************************************************
1909
1910 Synopsis [Returns the status of the cone.]
1911
1912 Description []
1913
1914 SideEffects []
1915
1916 SeeAlso []
1917
1918 ***********************************************************************/
Gia_ManAreDeriveCex(Gia_ManAre_t * p,Gia_StaAre_t * pLast)1919 Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
1920 {
1921 Abc_Cex_t * pCex;
1922 Vec_Ptr_t * vStates;
1923 Gia_StaAre_t * pSta, * pPrev;
1924 int Var, i, v;
1925 assert( p->iOutFail >= 0 );
1926 Gia_ManAreDeriveCexSatStart( p );
1927 // compute the trace
1928 vStates = Vec_PtrAlloc( 1000 );
1929 for ( pSta = pLast; Gia_StaIsGood(p, pSta); pSta = Gia_StaPrev(p, pSta) )
1930 if ( pSta != pLast )
1931 Vec_PtrPush( vStates, pSta );
1932 assert( Vec_PtrSize(vStates) >= 1 );
1933 // start the counter-example
1934 pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
1935 pCex->iFrame = Vec_PtrSize(vStates)-1;
1936 pCex->iPo = p->iOutFail;
1937 // compute states
1938 pPrev = NULL;
1939 Vec_PtrForEachEntry( Gia_StaAre_t *, vStates, pSta, i )
1940 {
1941 Gia_ManAreDeriveCexSat( p, pSta, pPrev, (i == 0) ? p->iOutFail : -1 );
1942 pPrev = pSta;
1943 // create the counter-example
1944 Vec_IntForEachEntry( p->vCofVars, Var, v )
1945 {
1946 assert( Var < Gia_ManPiNum(p->pAig) );
1947 Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
1948 }
1949 }
1950 // free temporary things
1951 Vec_PtrFree( vStates );
1952 Gia_ManAreDeriveCexSatStop( p );
1953 return pCex;
1954 }
1955
1956
1957 ////////////////////////////////////////////////////////////////////////
1958 /// END OF FILE ///
1959 ////////////////////////////////////////////////////////////////////////
1960
1961
1962 ABC_NAMESPACE_IMPL_END
1963
1964