abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absOut.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [absOut.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Abstraction package.]
8 
9  Synopsis [Abstraction refinement outside of abstraction engines.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "abs.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Derive a new counter-example.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
46 {
47  Abc_Cex_t * pCex;
48  int i, f, iPiNum;
49  assert( pCexAbs->iPo == 0 );
50  // start the counter-example
51  pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
52  pCex->iFrame = pCexAbs->iFrame;
53  pCex->iPo = pCexAbs->iPo;
54  // copy the bit data
55  for ( f = 0; f <= pCexAbs->iFrame; f++ )
56  for ( i = 0; i < Vec_IntSize(vPis); i++ )
57  {
58  if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
59  {
60  iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
61  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
62  }
63  }
64  // verify the counter example
65  if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
66  {
67  Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
68  Abc_CexFree( pCex );
69  pCex = NULL;
70  }
71  else
72  {
73  Abc_Print( 1, "Counter-example verification is successful.\n" );
74  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
75  }
76  return pCex;
77 }
78 
79 /**Function*************************************************************
80 
81  Synopsis [Refines gate-level abstraction using the counter-example.]
82 
83  Description []
84 
85  SideEffects []
86 
87  SeeAlso []
88 
89 ***********************************************************************/
90 int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
91 {
92  extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
93  int fAddOneLayer = 1;
94  Abc_Cex_t * pCexNew = NULL;
95  Gia_Man_t * pAbs;
96  Aig_Man_t * pAig;
97  Abc_Cex_t * pCare;
98  Vec_Int_t * vPis, * vPPis;
99  int f, i, iObjId;
100  abctime clk = Abc_Clock();
101  int nOnes = 0, Counter = 0;
102  if ( p->vGateClasses == NULL )
103  {
104  Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
105  return -1;
106  }
107  // derive abstraction
108  pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
109  Gia_ManStop( pAbs );
110  pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
111  if ( Gia_ManPiNum(pAbs) != pCex->nPis )
112  {
113  Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
114  Gia_ManStop( pAbs );
115  return -1;
116  }
117  if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
118  {
119  Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
120 // Gia_ManStop( pAbs );
121 // return -1;
122  }
123 // else
124 // Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
125  // get inputs
126  Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
127  assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
128  // add missing logic
129  if ( fAddOneLayer )
130  {
131  Gia_Obj_t * pObj;
132  // check if this is a real counter-example
134  for ( f = 0; f <= pCex->iFrame; f++ )
135  {
136  Gia_ManForEachPi( pAbs, pObj, i )
137  {
138  if ( i >= Vec_IntSize(vPis) ) // PPIs
139  Gia_ObjTerSimSetX( pObj );
140  else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
141  Gia_ObjTerSimSet1( pObj );
142  else
143  Gia_ObjTerSimSet0( pObj );
144  }
145  Gia_ManForEachRo( pAbs, pObj, i )
146  {
147  if ( f == 0 )
148  Gia_ObjTerSimSet0( pObj );
149  else
150  Gia_ObjTerSimRo( pAbs, pObj );
151  }
152  Gia_ManForEachAnd( pAbs, pObj, i )
153  Gia_ObjTerSimAnd( pObj );
154  Gia_ManForEachCo( pAbs, pObj, i )
155  Gia_ObjTerSimCo( pObj );
156  }
157  pObj = Gia_ManPo( pAbs, 0 );
158  if ( Gia_ObjTerSimGet1(pObj) )
159  {
160  pCexNew = Gia_ManCexRemap( p, pCex, vPis );
161  Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
162  }
163 // else
164 // Abc_Print( 1, "CEX is not real.\n" );
165  Gia_ManForEachObj( pAbs, pObj, i )
166  Gia_ObjTerSimSetC( pObj );
167  if ( pCexNew == NULL )
168  {
169  // grow one layer
170  Vec_IntForEachEntry( vPPis, iObjId, i )
171  {
172  assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
173  Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
174  }
175  if ( fVerbose )
176  {
177  Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
178  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
179  }
180  }
181  }
182  else
183  {
184  // minimize the CEX
185  pAig = Gia_ManToAigSimple( pAbs );
186  pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
187  Aig_ManStop( pAig );
188  if ( pCare == NULL )
189  Abc_Print( 1, "Counter-example minimization has failed.\n" );
190  // add new objects to the map
191  iObjId = -1;
192  for ( f = 0; f <= pCare->iFrame; f++ )
193  for ( i = 0; i < pCare->nPis; i++ )
194  if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
195  {
196  nOnes++;
197  assert( i >= Vec_IntSize(vPis) );
198  iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
199  assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
200  if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
201  continue;
202  assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
203  Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
204  // Abc_Print( 1, "Adding object %d.\n", iObjId );
205  // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
206  Counter++;
207  }
208  Abc_CexFree( pCare );
209  if ( fVerbose )
210  {
211  Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
212  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
213  }
214  // consider the case of SAT
215  if ( iObjId == -1 )
216  {
217  pCexNew = Gia_ManCexRemap( p, pCex, vPis );
218  Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
219  }
220  }
221  Vec_IntFree( vPis );
222  Vec_IntFree( vPPis );
223  Gia_ManStop( pAbs );
224  if ( pCexNew )
225  {
226  ABC_FREE( p->pCexSeq );
227  p->pCexSeq = pCexNew;
228  return 0;
229  }
230  // extract abstraction to include min-cut
231  if ( fMinCut )
232  Nwk_ManDeriveMinCut( p, fVerbose );
233  return -1;
234 }
235 
236 
237 
238 
239 
240 /**Function*************************************************************
241 
242  Synopsis [Resimulates the counter-example and returns flop values.]
243 
244  Description []
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
252 {
253  Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) );
254  Gia_Obj_t * pObj, * pObjRi, * pObjRo;
255  int RetValue, i, k, iBit = 0;
256  assert( iFrame >= 0 && iFrame <= p->iFrame );
257  Gia_ManCleanMark0(pAig);
258  Gia_ManForEachRo( pAig, pObj, i )
259  pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
260  for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ )
261  {
262  if ( i == iFrame )
263  {
264  Gia_ManForEachRo( pAig, pObjRo, k )
265  Vec_IntPush( vInit, pObjRo->fMark0 );
266  }
267  Gia_ManForEachPi( pAig, pObj, k )
268  pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
269  Gia_ManForEachAnd( pAig, pObj, k )
270  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
271  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
272  Gia_ManForEachCo( pAig, pObj, k )
273  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
274  if ( i == p->iFrame )
275  break;
276  Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
277  pObjRo->fMark0 = pObjRi->fMark0;
278  }
279  assert( iBit == p->nBits );
280  RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
281  if ( RetValue != 1 )
282  Vec_IntFreeP( &vInit );
283  Gia_ManCleanMark0(pAig);
284  return vInit;
285 }
286 
287 /**Function*************************************************************
288 
289  Synopsis [Verify counter-example starting in the given timeframe.]
290 
291  Description []
292 
293  SideEffects []
294 
295  SeeAlso []
296 
297 ***********************************************************************/
298 void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
299 {
300  Gia_Obj_t * pObj, * pObjRi, * pObjRo;
301  int RetValue, i, k, iBit = 0;
302  assert( iFrame >= 0 && iFrame <= p->iFrame );
303  Gia_ManCleanMark0(pAig);
304  Gia_ManForEachRo( pAig, pObj, i )
305  pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
306  for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ )
307  {
308  Gia_ManForEachPi( pAig, pObj, k )
309  pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
310  Gia_ManForEachAnd( pAig, pObj, k )
311  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
312  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
313  Gia_ManForEachCo( pAig, pObj, k )
314  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
315  if ( i == p->iFrame )
316  break;
317  Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
318  pObjRo->fMark0 = pObjRi->fMark0;
319  }
320  assert( iBit == p->nBits );
321  RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
322  Gia_ManCleanMark0(pAig);
323  if ( RetValue == 1 )
324  printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" );
325  else
326  printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" );
327 }
328 
329 /**Function*************************************************************
330 
331  Synopsis []
332 
333  Description []
334 
335  SideEffects []
336 
337  SeeAlso []
338 
339 ***********************************************************************/
341 {
342  Vec_Bit_t * vInitNew;
343  Gia_Man_t * pNew;
344  Gia_Obj_t * pObj;
345  int i, iFlopId;
346  assert( Vec_IntSize(vInit) == Vec_IntSize(vFlops) );
347  vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
348  Gia_ManForEachObjVec( vFlops, p, pObj, i )
349  {
350  assert( Gia_ObjIsRo(p, pObj) );
351  if ( Vec_IntEntry(vInit, i) == 0 )
352  continue;
353  iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
354  assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) );
355  Vec_BitWriteEntry( vInitNew, iFlopId, 1 );
356  }
357  pNew = Gia_ManDupFlip( p, Vec_BitArray(vInitNew) );
358  Vec_BitFree( vInitNew );
359  return pNew;
360 }
361 
362 /**Function*************************************************************
363 
364  Synopsis []
365 
366  Description []
367 
368  SideEffects []
369 
370  SeeAlso []
371 
372 ***********************************************************************/
373 int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose )
374 {
375  Gia_Man_t * pAbs, * pNew;
376  Vec_Int_t * vFlops, * vInit;
377  Vec_Int_t * vCopy;
378 // abctime clk = Abc_Clock();
379  int RetValue;
380  ABC_FREE( p->pCexSeq );
381  if ( p->vGateClasses == NULL )
382  {
383  Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" );
384  return -1;
385  }
386  vCopy = Vec_IntDup( p->vGateClasses );
387  Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra );
388  // derive abstraction
389  pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
390  Gia_ManStop( pAbs );
391  pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
392  if ( Gia_ManPiNum(pAbs) != pCex->nPis )
393  {
394  Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" );
395  Gia_ManStop( pAbs );
396  Vec_IntFree( vCopy );
397  return -1;
398  }
399  // get the state in frame iFrameStart
400  vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart );
401  if ( vInit == NULL )
402  {
403  Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" );
404  Gia_ManStop( pAbs );
405  Vec_IntFree( vCopy );
406  return -1;
407  }
408  if ( fVerbose )
409  Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" );
410  // get inputs
411  Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL );
412 // assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
413  Gia_ManStop( pAbs );
414 //Vec_IntPrint( vFlops );
415 //Vec_IntPrint( vInit );
416  // transform the manager to have new init state
417  pNew = Gia_ManTransformFlops( p, vFlops, vInit );
418  Vec_IntFree( vFlops );
419  Vec_IntFree( vInit );
420  // verify abstraction
421  {
422  Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses );
423  Gia_ManCheckCex( pAbs, pCex, iFrameStart );
424  Gia_ManStop( pAbs );
425  }
426  // transfer abstraction
427  assert( pNew->vGateClasses == NULL );
428  pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
429  // perform abstraction for the new AIG
430  {
431  Abs_Par_t Pars, * pPars = &Pars;
432  Abs_ParSetDefaults( pPars );
433  pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra;
434  pPars->fVerbose = fVerbose;
435  RetValue = Gia_ManPerformGla( pNew, pPars );
436  if ( RetValue == 0 ) // spurious SAT
437  {
438  Vec_IntFreeP( &pNew->vGateClasses );
439  pNew->vGateClasses = Vec_IntDup( vCopy );
440  }
441  }
442  // move the abstraction map
443  Vec_IntFreeP( &p->vGateClasses );
444  p->vGateClasses = pNew->vGateClasses;
445  pNew->vGateClasses = NULL;
446  // cleanup
447  Gia_ManStop( pNew );
448  Vec_IntFree( vCopy );
449  return -1;
450 }
451 
452 ////////////////////////////////////////////////////////////////////////
453 /// END OF FILE ///
454 ////////////////////////////////////////////////////////////////////////
455 
456 
458 
static void Gia_ObjTerSimCo(Gia_Obj_t *pObj)
Definition: gia.h:797
static void Gia_ObjTerSimRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:808
static void Gia_ObjTerSimSet0(Gia_Obj_t *pObj)
Definition: gia.h:770
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
void Gia_ManGlaCollect(Gia_Man_t *p, Vec_Int_t *vGateClasses, Vec_Int_t **pvPis, Vec_Int_t **pvPPis, Vec_Int_t **pvFlops, Vec_Int_t **pvNodes)
Definition: absDup.c:158
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition: absDup.c:220
int Gia_ManPerformGla(Gia_Man_t *p, Abs_Par_t *pPars)
Definition: absGla.c:1500
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
static abctime Abc_Clock()
Definition: abc_global.h:279
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: gia.h:75
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
static int * Vec_BitArray(Vec_Bit_t *p)
Definition: vecBit.h:223
void Abs_ParSetDefaults(Abs_Par_t *p)
DECLARATIONS ///.
Definition: absUtil.c:44
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_Man_t * Gia_ManTransformFlops(Gia_Man_t *p, Vec_Int_t *vFlops, Vec_Int_t *vInit)
Definition: absOut.c:340
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Abc_Cex_t * Saig_ManCbaFindCexCareBits(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition: absOldCex.c:718
Vec_Int_t * vGateClasses
Definition: gia.h:141
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Counter
Vec_Int_t * Gia_ManGetStateAndCheckCex(Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
Definition: absOut.c:251
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
void Gia_ManCheckCex(Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
Definition: absOut.c:298
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Gia_ManCexRemap(Gia_Man_t *p, Abc_Cex_t *pCexAbs, Vec_Int_t *vPis)
DECLARATIONS ///.
Definition: absOut.c:45
int Gia_ManGlaRefine(Gia_Man_t *p, Abc_Cex_t *pCex, int fMinCut, int fVerbose)
Definition: absOut.c:90
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Gia_ObjTerSimGet1(Gia_Obj_t *pObj)
Definition: gia.h:776
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned fMark0
Definition: gia.h:79
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition: giaDup.c:460
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static void Gia_ObjTerSimSetC(Gia_Obj_t *pObj)
Definition: gia.h:769
static void Gia_ObjTerSimSet1(Gia_Obj_t *pObj)
Definition: gia.h:771
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
static void Vec_BitFree(Vec_Bit_t *p)
Definition: vecBit.h:167
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_ManNewRefine(Gia_Man_t *p, Abc_Cex_t *pCex, int iFrameStart, int iFrameExtra, int fVerbose)
Definition: absOut.c:373
static void Gia_ObjTerSimSetX(Gia_Obj_t *pObj)
Definition: gia.h:772
void Nwk_ManDeriveMinCut(Gia_Man_t *p, int fVerbose)
Definition: nwkAig.c:218
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition: abs.h:46
static void Gia_ObjTerSimAnd(Gia_Obj_t *pObj)
Definition: gia.h:785
Abc_Cex_t * pCexSeq
Definition: gia.h:136
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387