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 ***********************************************************************/
Saig_ManCexMinGetCos(Aig_Man_t * pAig,Abc_Cex_t * pCex,Vec_Int_t * vLeaves,Vec_Int_t * vRoots)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 ***********************************************************************/
Saig_ManCexMinCollectFrameTerms_rec(Aig_Man_t * pAig,Aig_Obj_t * pObj,Vec_Int_t * vFrameCisOne)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 ***********************************************************************/
Saig_ManCexMinCollectFrameTerms(Aig_Man_t * pAig,Abc_Cex_t * pCex)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 ***********************************************************************/
Saig_ManCexMinDerivePhasePriority_rec(Aig_Man_t * pAig,Aig_Obj_t * pObj)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 ***********************************************************************/
Saig_ManCexMinVerifyPhase(Aig_Man_t * pAig,Abc_Cex_t * pCex,int f)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 ***********************************************************************/
Saig_ManCexMinDerivePhasePriority(Aig_Man_t * pAig,Abc_Cex_t * pCex,Vec_Vec_t * vFrameCis,Vec_Vec_t * vFramePPs,int f,Vec_Int_t * vRoots)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 ***********************************************************************/
Saig_ManCexMinCollectPhasePriority_(Aig_Man_t * pAig,Abc_Cex_t * pCex,Vec_Vec_t * vFrameCis)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 ***********************************************************************/
Saig_ManCexMinCollectPhasePriority(Aig_Man_t * pAig,Abc_Cex_t * pCex,Vec_Vec_t * vFrameCis)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 ***********************************************************************/
Saig_ManCexMinCollectReason_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Int_t * vReason,int fPiReason)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 ***********************************************************************/
Saig_ManCexMinCollectReason(Aig_Man_t * pAig,Abc_Cex_t * pCex,Vec_Vec_t * vFrameCis,Vec_Vec_t * vFramePPs,int fPiReason)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 ***********************************************************************/
Saig_ManCexMinComputeReason(Aig_Man_t * pAig,Abc_Cex_t * pCex,int fPiReason)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 ***********************************************************************/
Saig_ManCexMinDupWithCubes(Aig_Man_t * pAig,Vec_Vec_t * vReg2Value)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 ***********************************************************************/
Saig_ManCexMinPerform(Aig_Man_t * pAig,Abc_Cex_t * pCex)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
579