abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaEra2.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [gia.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #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 
128 static inline Gia_PtrAre_t Gia_Int2Ptr( unsigned n ) { Gia_PtrAreInt_t g; g.iInt = n; return g.iGia; }
129 static inline unsigned Gia_Ptr2Int( Gia_PtrAre_t n ) { Gia_PtrAreInt_t g; g.iGia = n; return g.iInt & 0x7fffffff; }
130 
131 static inline int Gia_ObjHasBranch0( Gia_ObjAre_t * q ) { return !q->nStas0 && (q->F[0].nPage || q->F[0].nItem); }
132 static inline int Gia_ObjHasBranch1( Gia_ObjAre_t * q ) { return !q->nStas1 && (q->F[1].nPage || q->F[1].nItem); }
133 static inline int Gia_ObjHasBranch2( Gia_ObjAre_t * q ) { return !q->nStas2 && (q->F[2].nPage || q->F[2].nItem); }
134 
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)); }
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); }
137 static inline Gia_ObjAre_t * Gia_ManAreObjInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreObj( p, Gia_Int2Ptr(n) ); }
138 static inline Gia_StaAre_t * Gia_ManAreStaInt( Gia_ManAre_t * p, int n ) { return Gia_ManAreSta( p, Gia_Int2Ptr(n) ); }
139 static inline Gia_ObjAre_t * Gia_ManAreObjLast( Gia_ManAre_t * p ) { return Gia_ManAreObjInt( p, p->nObjs-1 ); }
140 static inline Gia_StaAre_t * Gia_ManAreStaLast( Gia_ManAre_t * p ) { return Gia_ManAreStaInt( p, p->nStas-1 ); }
141 
142 static inline Gia_ObjAre_t * Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[0] ); }
143 static inline Gia_ObjAre_t * Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[1] ); }
144 static inline Gia_ObjAre_t * Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[2] ); }
145 
146 static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, iReg << 1 ); }
147 static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 ); }
148 
149 static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, iReg << 1 ); }
150 static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 ); }
151 
152 static inline Gia_StaAre_t * Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iPrev); }
153 static inline Gia_StaAre_t * Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iNext); }
154 static inline int Gia_StaIsGood( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return ((unsigned *)pS) != p->ppStas[0]; }
155 
156 static inline void Gia_StaSetUnused( Gia_StaAre_t * pS ) { pS->iPrev.fMark = 1; }
157 static inline int Gia_StaIsUnused( Gia_StaAre_t * pS ) { return pS->iPrev.fMark; }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
Gia_WordHasOneBit
static int Gia_WordHasOneBit(unsigned uWord)
Definition: gia.h:311
memset
char * memset()
Gia_StaAre_t_::iNext
Gia_PtrAre_t iNext
Definition: giaEra2.c:76
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ObjHasBranch1
static int Gia_ObjHasBranch1(Gia_ObjAre_t *q)
Definition: giaEra2.c:132
Gia_ObjNextObj1
static Gia_ObjAre_t * Gia_ObjNextObj1(Gia_ManAre_t *p, Gia_ObjAre_t *q)
Definition: giaEra2.c:143
Gia_ManDeriveCiTfo
Vec_Vec_t * Gia_ManDeriveCiTfo(Gia_Man_t *p)
Definition: giaEra2.c:312
Gia_ManAre_t_::iOutFail
int iOutFail
Definition: giaEra2.c:114
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_StaAreDashNum
static int Gia_StaAreDashNum(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:397
Gia_ManAre_t_::vCubesA
Vec_Int_t * vCubesA
Definition: giaEra2.c:105
Gia_Ptr2Int
static unsigned Gia_Ptr2Int(Gia_PtrAre_t n)
Definition: giaEra2.c:129
Gia_ManAreRycycleSta
static void Gia_ManAreRycycleSta(Gia_ManAre_t *p, Gia_StaAre_t *pSta)
Definition: giaEra2.c:607
Gia_ManDeriveCiTfo_rec
int Gia_ManDeriveCiTfo_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vRes)
Definition: giaEra2.c:252
Gia_ManAre_t_::vSatNumCis
Vec_Int_t * vSatNumCis
Definition: giaEra2.c:109
Gia_ManAreRebalance
static void Gia_ManAreRebalance(Gia_ManAre_t *p, Gia_PtrAre_t *pRoot)
Definition: giaEra2.c:903
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManArePrintUsed
static int Gia_ManArePrintUsed(Gia_ManAre_t *p)
Definition: giaEra2.c:835
Gia_ObjAre_t_::nStas0
unsigned nStas0
Definition: giaEra2.c:65
Gia_ManAre_t_::Root
Gia_PtrAre_t Root
Definition: giaEra2.c:102
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_StaAreEqual
static int Gia_StaAreEqual(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:337
Gia_ManAre_t_::vCofVars
Vec_Int_t * vCofVars
Definition: giaEra2.c:111
Gia_ManArePerform
int Gia_ManArePerform(Gia_Man_t *pAig, int nStatesMax, int fMiter, int fVerbose)
Definition: giaEra2.c:1710
Gia_ManAreCreateObj
static Gia_ObjAre_t * Gia_ManAreCreateObj(Gia_ManAre_t *p)
Definition: giaEra2.c:541
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Gia_ObjAre_t_::iVar
unsigned iVar
Definition: giaEra2.c:64
Gia_ManAreForEachCubeList2
#define Gia_ManAreForEachCubeList2(p, iList, pCube, iCube)
Definition: giaEra2.c:162
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Gia_ManAre_t_::vCiLits
Vec_Vec_t * vCiLits
Definition: giaEra2.c:104
Gia_ManAre_t_::nObjPages
int nObjPages
Definition: giaEra2.c:97
Gia_ObjAre_t_
Definition: giaEra2.c:62
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Gia_ManAreDeriveCexSat
void Gia_ManAreDeriveCexSat(Gia_ManAre_t *p, Gia_StaAre_t *pCur, Gia_StaAre_t *pNext, int iOutFailed)
Definition: giaEra2.c:1852
Gia_ManAre_t_::nStaPages
int nStaPages
Definition: giaEra2.c:98
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManAre_t_::vCubesB
Vec_Int_t * vCubesB
Definition: giaEra2.c:106
Gia_ManAreCubeCheckList
static int Gia_ManAreCubeCheckList(Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, Gia_StaAre_t *pSta)
Definition: giaEra2.c:971
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_ManAre_t_::fStopped
int fStopped
Definition: giaEra2.c:92
Gia_ManAreCubeAddToList
static void Gia_ManAreCubeAddToList(Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1040
Gia_ManAreListCountUsed
static int Gia_ManAreListCountUsed(Gia_ManAre_t *p)
Definition: giaEra2.c:776
Gia_PtrAre_t_::nPage
unsigned nPage
Definition: giaEra2.c:49
Gia_WordFindFirstBit
static int Gia_WordFindFirstBit(unsigned uWord)
Definition: gia.h:321
Gia_ManAreObj
static Gia_ObjAre_t * Gia_ManAreObj(Gia_ManAre_t *p, Gia_PtrAre_t n)
Definition: giaEra2.c:135
MAX_VARS_NUM
#define MAX_VARS_NUM
Definition: giaEra2.c:41
Gia_StaAreContain
static int Gia_StaAreContain(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:377
Gia_StaAre_t_
Definition: giaEra2.c:73
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Gia_WordCountOnes
static int Gia_WordCountOnes(unsigned uWord)
Definition: gia.h:313
l_True
#define l_True
Definition: SolverTypes.h:84
Gia_ManArePrintListUsed
static int Gia_ManArePrintListUsed(Gia_ManAre_t *p, Gia_PtrAre_t Root)
Definition: giaEra2.c:793
Gia_ManAre_t_::nObjs
int nObjs
Definition: giaEra2.c:99
Gia_StaIsGood
static int Gia_StaIsGood(Gia_ManAre_t *p, Gia_StaAre_t *pS)
Definition: giaEra2.c:154
Gia_ManAre_t_::nDisjs3
int nDisjs3
Definition: giaEra2.c:122
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManCheckPOs_rec
int Gia_ManCheckPOs_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaEra2.c:1452
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Gia_ManAreFindBestVar
int Gia_ManAreFindBestVar(Gia_ManAre_t *p, Gia_PtrAre_t List)
Definition: giaEra2.c:853
Gia_Int2Ptr
static Gia_PtrAre_t Gia_Int2Ptr(unsigned n)
Definition: giaEra2.c:128
Gia_ManAreCreateStaNew
static Gia_StaAre_t * Gia_ManAreCreateStaNew(Gia_ManAre_t *p)
Definition: giaEra2.c:633
Gia_ManAre_t_::pNew
Gia_Man_t * pNew
Definition: giaEra2.c:85
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManAre_t_::nDisjs
int nDisjs
Definition: giaEra2.c:120
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_ManAre_t_::pAig
Gia_Man_t * pAig
Definition: giaEra2.c:84
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Gia_ManAre_t_::nSize
int nSize
Definition: giaEra2.c:96
Gia_StaAre_t_::iPrev
Gia_PtrAre_t iPrev
Definition: giaEra2.c:75
Gia_ManAreStaInt
static Gia_StaAre_t * Gia_ManAreStaInt(Gia_ManAre_t *p, int n)
Definition: giaEra2.c:138
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Gia_ManAreForEachCubeStore
#define Gia_ManAreForEachCubeStore(p, pCube, i)
Definition: giaEra2.c:166
Gia_ManAreDeriveCexSatStop
void Gia_ManAreDeriveCexSatStop(Gia_ManAre_t *p)
Definition: giaEra2.c:1827
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManAreListCountUsed_rec
int Gia_ManAreListCountUsed_rec(Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)
Definition: giaEra2.c:754
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_VecDupInt
static Vec_Vec_t * Vec_VecDupInt(Vec_Vec_t *p)
Definition: vecVec.h:395
Gia_StaIsUsed
static int Gia_StaIsUsed(Gia_StaAre_t *pS)
Definition: giaEra2.c:158
Gia_ManAreCubeCheckTree_rec
int Gia_ManAreCubeCheckTree_rec(Gia_ManAre_t *p, Gia_ObjAre_t *pObj, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1065
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManAre_t_::iStaCur
int iStaCur
Definition: giaEra2.c:101
Gia_ManAreDeriveNexts
int Gia_ManAreDeriveNexts(Gia_ManAre_t *p, Gia_PtrAre_t Sta)
Definition: giaEra2.c:1618
Gia_StaSetValue1
static void Gia_StaSetValue1(Gia_StaAre_t *p, int iReg)
Definition: giaEra2.c:150
Gia_ObjNextObj2
static Gia_ObjAre_t * Gia_ObjNextObj2(Gia_ManAre_t *p, Gia_ObjAre_t *q)
Definition: giaEra2.c:144
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_ManAreDeriveCex
Abc_Cex_t * Gia_ManAreDeriveCex(Gia_ManAre_t *p, Gia_StaAre_t *pLast)
Definition: giaEra2.c:1919
Gia_ManAreForEachCubeVec
#define Gia_ManAreForEachCubeVec(vVec, p, pCube, i)
Definition: giaEra2.c:168
Gia_StaSetValue0
static void Gia_StaSetValue0(Gia_StaAre_t *p, int iReg)
Definition: giaEra2.c:149
MAX_CALL_NUM
#define MAX_CALL_NUM
DECLARATIONS ///.
Definition: giaEra2.c:38
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ManCountMintermsInCube
void Gia_ManCountMintermsInCube(Gia_StaAre_t *pCube, int nVars, unsigned *pStore)
FUNCTION DEFINITIONS ///.
Definition: giaEra2.c:186
Gia_ManAreCubeCollectList
static int Gia_ManAreCubeCollectList(Gia_ManAre_t *p, Gia_PtrAre_t *pRoot, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1179
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ManAreCreate
Gia_ManAre_t * Gia_ManAreCreate(Gia_Man_t *pAig)
Definition: giaEra2.c:481
Gia_ManAre_t_::nDisjs2
int nDisjs2
Definition: giaEra2.c:121
ABC_PRTr
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
Gia_StaAre_t
struct Gia_StaAre_t_ Gia_StaAre_t
Definition: giaEra2.c:72
Gia_ManAreDepth
int Gia_ManAreDepth(Gia_ManAre_t *p, int iState)
Definition: giaEra2.c:714
Gia_StaAreDisjointVar
static int Gia_StaAreDisjointVar(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:450
Gia_ManAre_t_::ppObjs
unsigned ** ppObjs
Definition: giaEra2.c:86
Gia_ManAre_t_::nCompares
int nCompares
Definition: giaEra2.c:118
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Gia_ManAre_t_::pSat
void * pSat
Definition: giaEra2.c:108
Gia_ManAreCubeCollectTree_rec
int Gia_ManAreCubeCollectTree_rec(Gia_ManAre_t *p, Gia_ObjAre_t *pObj, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1223
Gia_PtrAre_t_::fMark
unsigned fMark
Definition: giaEra2.c:50
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManAre_t_::nStas
int nStas
Definition: giaEra2.c:100
Gia_ManAreDeriveCexSatStart
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Gia_ManAreDeriveCexSatStart(Gia_ManAre_t *p)
Definition: giaEra2.c:1799
if
if(last==0)
Definition: sparse_int.h:34
Gia_StaAreDisjoint
static int Gia_StaAreDisjoint(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:357
Gia_ManAreMostUsedPi
static Gia_Obj_t * Gia_ManAreMostUsedPi(Gia_ManAre_t *p)
Definition: giaEra2.c:1418
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManAre_t_::timeCube
int timeCube
Definition: giaEra2.c:125
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_StaHasValue0
static int Gia_StaHasValue0(Gia_StaAre_t *p, int iReg)
Definition: giaEra2.c:146
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ManAreFree
void Gia_ManAreFree(Gia_ManAre_t *p)
Definition: giaEra2.c:510
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ManAreCubeCheckTree
int Gia_ManAreCubeCheckTree(Gia_ManAre_t *p, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1260
MAX_CUBE_NUM
#define MAX_CUBE_NUM
Definition: giaEra2.c:42
Gia_ManAre_t_::nRecCalls
int nRecCalls
Definition: giaEra2.c:119
Vec_VecEntryInt
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_PtrAreInt_t_::iGia
Gia_PtrAre_t iGia
Definition: giaEra2.c:56
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gia_StaHasValue1
static int Gia_StaHasValue1(Gia_StaAre_t *p, int iReg)
Definition: giaEra2.c:147
Gia_ObjAre_t_::F
Gia_PtrAre_t F[3]
Definition: giaEra2.c:68
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_ObjHasBranch0
static int Gia_ObjHasBranch0(Gia_ObjAre_t *q)
Definition: giaEra2.c:131
Gia_ManAreForEachCubeList
#define Gia_ManAreForEachCubeList(p, pList, pCube)
Definition: giaEra2.c:160
Gia_ManAreCreateStaInit
static Gia_StaAre_t * Gia_ManAreCreateStaInit(Gia_ManAre_t *p)
Definition: giaEra2.c:660
Gia_PtrAreInt_t_
Definition: giaEra2.c:54
Gia_ManAre_t_::fMiter
int fMiter
Definition: giaEra2.c:91
Gia_StaSetUnused
static void Gia_StaSetUnused(Gia_StaAre_t *pS)
Definition: giaEra2.c:156
Gia_ManAreCubeProcess
static int Gia_ManAreCubeProcess(Gia_ManAre_t *p, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1357
Gia_StaIsUnused
static int Gia_StaIsUnused(Gia_StaAre_t *pS)
Definition: giaEra2.c:157
Gia_PtrAre_t_::nItem
unsigned nItem
Definition: giaEra2.c:48
Gia_ManAre_t_::fTree
int fTree
Definition: giaEra2.c:93
MAX_ITEM_NUM
#define MAX_ITEM_NUM
Definition: giaEra2.c:39
Gia_StaAre_t_::pData
unsigned pData[0]
Definition: giaEra2.c:77
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_ManAre_t_::nEquals
int nEquals
Definition: giaEra2.c:117
Gia_PtrAre_t_
Definition: giaEra2.c:46
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Gia_ManAreDeriveNexts_rec
int Gia_ManAreDeriveNexts_rec(Gia_ManAre_t *p, Gia_PtrAre_t Sta)
Definition: giaEra2.c:1541
Gia_ManAreCubeAddToTree_rec
void Gia_ManAreCubeAddToTree_rec(Gia_ManAre_t *p, Gia_ObjAre_t *pObj, Gia_StaAre_t *pSta)
Definition: giaEra2.c:1102
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ManAre_t_::vSatNumCos
Vec_Int_t * vSatNumCos
Definition: giaEra2.c:110
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ObjAre_t_::nStas1
unsigned nStas1
Definition: giaEra2.c:66
Gia_PtrAreInt_t_::iInt
unsigned iInt
Definition: giaEra2.c:57
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManDeriveCiTfoOne
Vec_Int_t * Gia_ManDeriveCiTfoOne(Gia_Man_t *p, Gia_Obj_t *pPivot)
Definition: giaEra2.c:280
Gia_ManCheckPOs
static int Gia_ManCheckPOs(Gia_ManAre_t *p)
Definition: giaEra2.c:1475
Gia_ManCountMinterms
int Gia_ManCountMinterms(Gia_ManAre_t *p)
Definition: giaEra2.c:223
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ManAre_t_::timeAig
int timeAig
Definition: giaEra2.c:124
Gia_ManAre_t_::vCiTfos
Vec_Vec_t * vCiTfos
Definition: giaEra2.c:103
Gia_ManAre_t_::ppStas
unsigned ** ppStas
Definition: giaEra2.c:87
MAX_PAGE_NUM
#define MAX_PAGE_NUM
Definition: giaEra2.c:40
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManCheckPOstatus
static int Gia_ManCheckPOstatus(Gia_ManAre_t *p)
Definition: giaEra2.c:1505
Minisat::Var
int Var
Definition: SolverTypes.h:42
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Cnf_DataCollectCiSatNums
Vec_Int_t * Cnf_DataCollectCiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
Definition: cnfUtil.c:200
Gia_ManAreListCountListUsed
static int Gia_ManAreListCountListUsed(Gia_ManAre_t *p, Gia_PtrAre_t Root)
Definition: giaEra2.c:734
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ObjAre_t_::nStas2
unsigned nStas2
Definition: giaEra2.c:67
Gia_ManAre_t_::nChecks
int nChecks
Definition: giaEra2.c:116
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_ObjHasBranch2
static int Gia_ObjHasBranch2(Gia_ObjAre_t *q)
Definition: giaEra2.c:133
sat_solver_t
Definition: satSolver.h:91
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Gia_ManAre_t_::pTarget
Gia_StaAre_t * pTarget
Definition: giaEra2.c:113
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManAreMostUsedPi_rec
void Gia_ManAreMostUsedPi_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaEra2.c:1392
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManAreStaLast
static Gia_StaAre_t * Gia_ManAreStaLast(Gia_ManAre_t *p)
Definition: giaEra2.c:140
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_ManAre_t_
Definition: giaEra2.c:82
Gia_ManArePrintUsed_rec
int Gia_ManArePrintUsed_rec(Gia_ManAre_t *p, Gia_PtrAre_t Root, int fTree)
Definition: giaEra2.c:813
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_ManArePrintReport
void Gia_ManArePrintReport(Gia_ManAre_t *p, abctime Time, int fFinal)
Definition: giaEra2.c:1683
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_ManAreCompress
static void Gia_ManAreCompress(Gia_ManAre_t *p, Gia_PtrAre_t *pRoot)
Definition: giaEra2.c:940
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_StaPrev
static Gia_StaAre_t * Gia_StaPrev(Gia_ManAre_t *p, Gia_StaAre_t *pS)
Definition: giaEra2.c:152
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManAre_t_::nWords
int nWords
Definition: giaEra2.c:95
Gia_ObjNextObj0
static Gia_ObjAre_t * Gia_ObjNextObj0(Gia_ManAre_t *p, Gia_ObjAre_t *q)
Definition: giaEra2.c:142
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_StaNext
static Gia_StaAre_t * Gia_StaNext(Gia_ManAre_t *p, Gia_StaAre_t *pS)
Definition: giaEra2.c:153
Gia_ManArePrintCube
void Gia_ManArePrintCube(Gia_ManAre_t *p, Gia_StaAre_t *pSta)
Definition: giaEra2.c:681
Gia_ManAreObjInt
static Gia_ObjAre_t * Gia_ManAreObjInt(Gia_ManAre_t *p, int n)
Definition: giaEra2.c:137
Cnf_DataCollectCoSatNums
Vec_Int_t * Cnf_DataCollectCoSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
Definition: cnfUtil.c:222
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManAreSta
static Gia_StaAre_t * Gia_ManAreSta(Gia_ManAre_t *p, Gia_PtrAre_t n)
Definition: giaEra2.c:136
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManAreCreateSta
static Gia_StaAre_t * Gia_ManAreCreateSta(Gia_ManAre_t *p)
Definition: giaEra2.c:568
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ManAreObjLast
static Gia_ObjAre_t * Gia_ManAreObjLast(Gia_ManAre_t *p)
Definition: giaEra2.c:139
Gia_ManAre_t_::vAssumps
Vec_Int_t * vAssumps
Definition: giaEra2.c:112
Gia_StaAreSharpVar
static int Gia_StaAreSharpVar(Gia_StaAre_t *p1, Gia_StaAre_t *p2, int nWords)
Definition: giaEra2.c:418
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387