abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcCexMin1.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcCexMin1.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [CEX minimization.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcCexMin1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig/ioa/ioa.h"
22 #include "bmc.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Find the roots to begin traversal.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Int_t * vLeaves, Vec_Int_t * vRoots )
47 {
48  Aig_Obj_t * pObj;
49  int i;
50  Vec_IntClear( vRoots );
51  if ( vLeaves == NULL )
52  {
53  pObj = Aig_ManCo( pAig, pCex->iPo );
54  Vec_IntPush( vRoots, Aig_ObjId(pObj) );
55  return;
56  }
57  Aig_ManForEachObjVec( vLeaves, pAig, pObj, i )
58  if ( Saig_ObjIsLo(pAig, pObj) )
59  Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
60 }
61 
62 /**Function*************************************************************
63 
64  Synopsis [Collects CI of the given timeframe.]
65 
66  Description []
67 
68  SideEffects []
69 
70  SeeAlso []
71 
72 ***********************************************************************/
73 void Saig_ManCexMinCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFrameCisOne )
74 {
75  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
76  return;
77  Aig_ObjSetTravIdCurrent(pAig, pObj);
78  if ( Aig_ObjIsCo(pObj) )
79  Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
80  else if ( Aig_ObjIsNode(pObj) )
81  {
82  Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
83  Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFrameCisOne );
84  }
85  else if ( Aig_ObjIsCi(pObj) )
86  Vec_IntPush( vFrameCisOne, Aig_ObjId(pObj) );
87 }
88 
89 /**Function*************************************************************
90 
91  Synopsis [Collects CIs of all timeframes.]
92 
93  Description []
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
100 Vec_Vec_t * Saig_ManCexMinCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex )
101 {
102  Vec_Vec_t * vFrameCis;
103  Vec_Int_t * vRoots, * vLeaves;
104  Aig_Obj_t * pObj;
105  int i, f;
106  // create terminals
107  vRoots = Vec_IntAlloc( 1000 );
108  vFrameCis = Vec_VecStart( pCex->iFrame+1 );
109  for ( f = pCex->iFrame; f >= 0; f-- )
110  {
111  // create roots
112  vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
113  Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
114  // collect nodes starting from the roots
115  Aig_ManIncrementTravId( pAig );
116  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
117  Saig_ManCexMinCollectFrameTerms_rec( pAig, pObj, Vec_VecEntryInt(vFrameCis, f) );
118  }
119  Vec_IntFree( vRoots );
120  return vFrameCis;
121 }
122 
123 
124 
125 /**Function*************************************************************
126 
127  Synopsis [Recursively sets phase and priority.]
128 
129  Description []
130 
131  SideEffects []
132 
133  SeeAlso []
134 
135 ***********************************************************************/
136 void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj )
137 {
138  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
139  return;
140  Aig_ObjSetTravIdCurrent(pAig, pObj);
141  if ( Aig_ObjIsCo(pObj) )
142  {
143  Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
144  assert( Aig_ObjFanin0(pObj)->iData >= 0 );
145  pObj->iData = Aig_ObjFanin0(pObj)->iData ^ Aig_ObjFaninC0(pObj);
146  }
147  else if ( Aig_ObjIsNode(pObj) )
148  {
149  int fPhase0, fPhase1, iPrio0, iPrio1;
150  Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
151  Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) );
152  assert( Aig_ObjFanin0(pObj)->iData >= 0 );
153  assert( Aig_ObjFanin1(pObj)->iData >= 0 );
154  fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
155  fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
156  iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
157  iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
158  if ( fPhase0 && fPhase1 ) // both are one
159  pObj->iData = Abc_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
160  else if ( !fPhase0 && fPhase1 )
161  pObj->iData = Abc_Var2Lit( iPrio0, 0 );
162  else if ( fPhase0 && !fPhase1 )
163  pObj->iData = Abc_Var2Lit( iPrio1, 0 );
164  else // both are zero
165  pObj->iData = Abc_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
166  }
167 }
168 
169 /**Function*************************************************************
170 
171  Synopsis [Verify phase.]
172 
173  Description []
174 
175  SideEffects []
176 
177  SeeAlso []
178 
179 ***********************************************************************/
180 void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f )
181 {
182  Aig_Obj_t * pObj;
183  int i;
184  Aig_ManConst1(pAig)->fPhase = 1;
185  Saig_ManForEachPi( pAig, pObj, i )
186  pObj->fPhase = Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
187  if ( f == 0 )
188  {
189  Saig_ManForEachLo( pAig, pObj, i )
190  pObj->fPhase = 0;
191  }
192  else
193  {
194  Saig_ManForEachLo( pAig, pObj, i )
195  pObj->fPhase = Saig_ObjLoToLi(pAig, pObj)->fPhase;
196  }
197  Aig_ManForEachNode( pAig, pObj, i )
198  pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase) &
199  (Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase);
200  Aig_ManForEachCo( pAig, pObj, i )
201  pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase);
202 }
203 
204 /**Function*************************************************************
205 
206  Synopsis [Collects phase and priority of all timeframes.]
207 
208  Description []
209 
210  SideEffects []
211 
212  SeeAlso []
213 
214 ***********************************************************************/
215 void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int f, Vec_Int_t * vRoots )
216 {
217  Vec_Int_t * vFramePPsOne, * vFrameCisOne, * vLeaves;
218  Aig_Obj_t * pObj;
219  int i;
220  // set PP for the CIs
221  vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
222  vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
223  Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
224  {
225  pObj->iData = Vec_IntEntry( vFramePPsOne, i );
226  assert( pObj->iData >= 0 );
227  }
228 // if ( f == 0 )
229 // Saig_ManCexMinVerifyPhase( pAig, pCex, f );
230 
231  // create roots
232  vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
233  Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
234  // derive for the nodes starting from the roots
235  Aig_ManIncrementTravId( pAig );
236  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
237  {
238  Saig_ManCexMinDerivePhasePriority_rec( pAig, pObj );
239 // if ( f == 0 )
240 // assert( (pObj->iData & 1) == pObj->fPhase );
241  }
242 }
243 
244 /**Function*************************************************************
245 
246  Synopsis [Collects phase and priority of all timeframes.]
247 
248  Description []
249 
250  SideEffects []
251 
252  SeeAlso []
253 
254 ***********************************************************************/
255 Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
256 {
257  Vec_Vec_t * vFramePPs;
258  Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
259  Aig_Obj_t * pObj;
260  int i, f, nPrioOffset;
261 
262  // initialize phase and priority
263  Aig_ManForEachObj( pAig, pObj, i )
264  pObj->iData = -1;
265 
266  // set the constant node to higher priority than the flops
267  vFramePPs = Vec_VecStart( pCex->iFrame+1 );
268  nPrioOffset = (pCex->iFrame + 1) * pCex->nPis;
269  Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
270  vRoots = Vec_IntAlloc( 1000 );
271  for ( f = 0; f <= pCex->iFrame; f++ )
272  {
273  int nPiCount = 0;
274  // fill in PP for the CIs
275  vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
276  vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
277  assert( Vec_IntSize(vFramePPsOne) == 0 );
278  Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
279  {
280  assert( Aig_ObjIsCi(pObj) );
281  if ( Saig_ObjIsPi(pAig, pObj) )
282  Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
283  else if ( f == 0 )
284  Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
285  else
286  Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
287  }
288  // compute the PP info
289  Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
290  }
291  Vec_IntFree( vRoots );
292  // check the output
293  pObj = Aig_ManCo( pAig, pCex->iPo );
294  assert( Abc_LitIsCompl(pObj->iData) );
295  return vFramePPs;
296 }
297 
298 /**Function*************************************************************
299 
300  Synopsis [Collects phase and priority of all timeframes.]
301 
302  Description []
303 
304  SideEffects []
305 
306  SeeAlso []
307 
308 ***********************************************************************/
309 Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
310 {
311  Vec_Vec_t * vFramePPs;
312  Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
313  Aig_Obj_t * pObj;
314  int i, f, nPrioOffset;
315 
316  // initialize phase and priority
317  Aig_ManForEachObj( pAig, pObj, i )
318  pObj->iData = -1;
319 
320  // set the constant node to higher priority than the flops
321  vFramePPs = Vec_VecStart( pCex->iFrame+1 );
322  nPrioOffset = pCex->nRegs;
323  Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
324  vRoots = Vec_IntAlloc( 1000 );
325  for ( f = 0; f <= pCex->iFrame; f++ )
326  {
327  int nPiCount = 0;
328  // fill in PP for the CIs
329  vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
330  vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
331  assert( Vec_IntSize(vFramePPsOne) == 0 );
332  Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
333  {
334  assert( Aig_ObjIsCi(pObj) );
335  if ( Saig_ObjIsPi(pAig, pObj) )
336  Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
337  else if ( f == 0 )
338  Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
339  else
340  Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
341  }
342  // compute the PP info
343  Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
344  }
345  Vec_IntFree( vRoots );
346  // check the output
347  pObj = Aig_ManCo( pAig, pCex->iPo );
348  assert( Abc_LitIsCompl(pObj->iData) );
349  return vFramePPs;
350 }
351 
352 
353 /**Function*************************************************************
354 
355  Synopsis [Returns reasons for the property to fail.]
356 
357  Description []
358 
359  SideEffects []
360 
361  SeeAlso []
362 
363 ***********************************************************************/
364 void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vReason, int fPiReason )
365 {
366  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
367  return;
368  Aig_ObjSetTravIdCurrent(p, pObj);
369  if ( Aig_ObjIsCi(pObj) )
370  {
371  if ( fPiReason && Saig_ObjIsPi(p, pObj) )
372  Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjCioId(pObj), !Abc_LitIsCompl(pObj->iData) ) );
373  else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
374  Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) );
375  return;
376  }
377  if ( Aig_ObjIsCo(pObj) )
378  {
379  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
380  return;
381  }
382  if ( Aig_ObjIsConst1(pObj) )
383  return;
384  assert( Aig_ObjIsNode(pObj) );
385  if ( Abc_LitIsCompl(pObj->iData) ) // value 1
386  {
387  int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
388  int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
389  assert( fPhase0 && fPhase1 );
390  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
391  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
392  }
393  else
394  {
395  int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
396  int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
397  assert( !fPhase0 || !fPhase1 );
398  if ( !fPhase0 && fPhase1 )
399  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
400  else if ( fPhase0 && !fPhase1 )
401  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
402  else
403  {
404  int iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
405  int iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
406  if ( iPrio0 >= iPrio1 )
407  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
408  else
409  Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
410  }
411  }
412 }
413 
414 
415 /**Function*************************************************************
416 
417  Synopsis [Collects phase and priority of all timeframes.]
418 
419  Description []
420 
421  SideEffects []
422 
423  SeeAlso []
424 
425 ***********************************************************************/
426 Vec_Vec_t * Saig_ManCexMinCollectReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int fPiReason )
427 {
428  Vec_Vec_t * vFrameReas;
429  Vec_Int_t * vRoots, * vLeaves;
430  Aig_Obj_t * pObj;
431  int i, f;
432  // select reason for the property to fail
433  vFrameReas = Vec_VecStart( pCex->iFrame+1 );
434  vRoots = Vec_IntAlloc( 1000 );
435  for ( f = pCex->iFrame; f >= 0; f-- )
436  {
437  // set phase and polarity
438  Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
439  // create roots
440  vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
441  Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
442  // collect nodes starting from the roots
443  Aig_ManIncrementTravId( pAig );
444  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
445  Saig_ManCexMinCollectReason_rec( pAig, pObj, Vec_VecEntryInt(vFrameReas, f), fPiReason );
446 //printf( "%d(%d) ", Vec_VecLevelSize(vFrameCis, f), Vec_VecLevelSize(vFrameReas, f) );
447  }
448 //printf( "\n" );
449  Vec_IntFree( vRoots );
450  return vFrameReas;
451 }
452 
453 /**Function*************************************************************
454 
455  Synopsis []
456 
457  Description []
458 
459  SideEffects []
460 
461  SeeAlso []
462 
463 ***********************************************************************/
464 Vec_Vec_t * Saig_ManCexMinComputeReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, int fPiReason )
465 {
466  Vec_Vec_t * vFrameCis, * vFramePPs, * vFrameReas;
467  // sanity checks
468  assert( pCex->nPis == Saig_ManPiNum(pAig) );
469  assert( pCex->nRegs == Saig_ManRegNum(pAig) );
470  assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
471  // derive frame terms
472  vFrameCis = Saig_ManCexMinCollectFrameTerms( pAig, pCex );
473  // derive phase and priority
474  vFramePPs = Saig_ManCexMinCollectPhasePriority( pAig, pCex, vFrameCis );
475  // derive reasons for property failure
476  vFrameReas = Saig_ManCexMinCollectReason( pAig, pCex, vFrameCis, vFramePPs, fPiReason );
477  Vec_VecFree( vFramePPs );
478  Vec_VecFree( vFrameCis );
479  return vFrameReas;
480 }
481 
482 
483 /**Function*************************************************************
484 
485  Synopsis [Duplicate with literals.]
486 
487  Description []
488 
489  SideEffects []
490 
491  SeeAlso []
492 
493 ***********************************************************************/
494 Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
495 {
496  Vec_Int_t * vLevel;
497  Aig_Man_t * pAigNew;
498  Aig_Obj_t * pObj, * pMiter;
499  int i, k, Lit;
500  assert( pAig->nConstrs == 0 );
501  // start the new manager
502  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) );
503  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
504  // map the constant node
505  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
506  // create variables for PIs
507  Aig_ManForEachCi( pAig, pObj, i )
508  pObj->pData = Aig_ObjCreateCi( pAigNew );
509  // add internal nodes of this frame
510  Aig_ManForEachNode( pAig, pObj, i )
511  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
512  // create POs for cubes
513  Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
514  {
515  if ( i == 0 )
516  continue;
517  pMiter = Aig_ManConst1( pAigNew );
518  Vec_IntForEachEntry( vLevel, Lit, k )
519  {
520  assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) );
521  pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
522  pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
523  }
524  Aig_ObjCreateCo( pAigNew, pMiter );
525  }
526  // transfer to register outputs
527  Saig_ManForEachLi( pAig, pObj, i )
528  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
529  // finalize
530  Aig_ManCleanup( pAigNew );
531  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
532  return pAigNew;
533 }
534 
535 
536 /**Function*************************************************************
537 
538  Synopsis []
539 
540  Description []
541 
542  SideEffects []
543 
544  SeeAlso []
545 
546 ***********************************************************************/
547 Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
548 {
549  int fReasonPi = 0;
550 
551  Abc_Cex_t * pCexMin = NULL;
552  Aig_Man_t * pManNew = NULL;
553  Vec_Vec_t * vFrameReas;
554  vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
555  printf( "Reason size = %d. Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );
556 
557  // try reducing the frames
558  if ( !fReasonPi )
559  {
560  char * pFileName = "aigcube.aig";
561  pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
562  Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
563  Aig_ManStop( pManNew );
564  printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
565  }
566 
567  // find reduced counter-example
568  Vec_VecFree( vFrameReas );
569  return pCexMin;
570 }
571 
572 ////////////////////////////////////////////////////////////////////////
573 /// END OF FILE ///
574 ////////////////////////////////////////////////////////////////////////
575 
576 
577 ABC_NAMESPACE_IMPL_END
578 
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Saig_ManCexMinPerform
Abc_Cex_t * Saig_ManCexMinPerform(Aig_Man_t *pAig, Abc_Cex_t *pCex)
Definition: bmcCexMin1.c:547
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
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
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Saig_ManCexMinCollectFrameTerms
Vec_Vec_t * Saig_ManCexMinCollectFrameTerms(Aig_Man_t *pAig, Abc_Cex_t *pCex)
Definition: bmcCexMin1.c:100
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Vec_VecForEachLevelInt
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition: vecVec.h:71
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Saig_ObjRegId
static int Saig_ObjRegId(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:88
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Saig_ManCexMinCollectFrameTerms_rec
void Saig_ManCexMinCollectFrameTerms_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vFrameCisOne)
Definition: bmcCexMin1.c:73
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Saig_ManCexMinVerifyPhase
void Saig_ManCexMinVerifyPhase(Aig_Man_t *pAig, Abc_Cex_t *pCex, int f)
Definition: bmcCexMin1.c:180
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_ManCexMinCollectPhasePriority_
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_(Aig_Man_t *pAig, Abc_Cex_t *pCex, Vec_Vec_t *vFrameCis)
Definition: bmcCexMin1.c:255
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Saig_ManCexMinDerivePhasePriority_rec
void Saig_ManCexMinDerivePhasePriority_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: bmcCexMin1.c:136
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Saig_ManCexMinCollectReason
Vec_Vec_t * Saig_ManCexMinCollectReason(Aig_Man_t *pAig, Abc_Cex_t *pCex, Vec_Vec_t *vFrameCis, Vec_Vec_t *vFramePPs, int fPiReason)
Definition: bmcCexMin1.c:426
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Saig_ManLi
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Saig_ManCexMinCollectPhasePriority
Vec_Vec_t * Saig_ManCexMinCollectPhasePriority(Aig_Man_t *pAig, Abc_Cex_t *pCex, Vec_Vec_t *vFrameCis)
Definition: bmcCexMin1.c:309
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Vec_VecStart
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
Saig_ManCexMinCollectReason_rec
void Saig_ManCexMinCollectReason_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vReason, int fPiReason)
Definition: bmcCexMin1.c:364
Saig_ManCexMinDupWithCubes
Aig_Man_t * Saig_ManCexMinDupWithCubes(Aig_Man_t *pAig, Vec_Vec_t *vReg2Value)
Definition: bmcCexMin1.c:494
Ioa_WriteAiger
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Vec_VecEntryInt
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_Obj_t_::iData
int iData
Definition: aig.h:88
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManCexMinDerivePhasePriority
void Saig_ManCexMinDerivePhasePriority(Aig_Man_t *pAig, Abc_Cex_t *pCex, Vec_Vec_t *vFrameCis, Vec_Vec_t *vFramePPs, int f, Vec_Int_t *vRoots)
Definition: bmcCexMin1.c:215
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_VecSizeSize
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Vec_VecSize
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
Saig_ManCexMinComputeReason
Vec_Vec_t * Saig_ManCexMinComputeReason(Aig_Man_t *pAig, Abc_Cex_t *pCex, int fPiReason)
Definition: bmcCexMin1.c:464
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Saig_ManCexMinGetCos
ABC_NAMESPACE_IMPL_START void Saig_ManCexMinGetCos(Aig_Man_t *pAig, Abc_Cex_t *pCex, Vec_Int_t *vLeaves, Vec_Int_t *vRoots)
DECLARATIONS ///.
Definition: bmcCexMin1.c:46
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91