1 /**CFile****************************************************************
2
3 FileName [bmcCexCare.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis [Computing care set of the counter-example.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22 #include "aig/gia/giaAig.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 [Takes CEX and its care-set. Returns care-set of all objects.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Bmc_CexCareExtendToObjects(Gia_Man_t * p,Abc_Cex_t * pCex,Abc_Cex_t * pCexCare)46 Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
47 {
48 Abc_Cex_t * pNew;
49 Gia_Obj_t * pObj;
50 int i, k;
51 assert( pCex->nPis == pCexCare->nPis );
52 assert( pCex->nRegs == pCexCare->nRegs );
53 assert( pCex->nBits == pCexCare->nBits );
54 // start the counter-example
55 pNew = Abc_CexAlloc( pCex->nRegs, Gia_ManObjNum(p), pCex->iFrame + 1 );
56 pNew->iFrame = pCex->iFrame;
57 pNew->iPo = pCex->iPo;
58 // initialize terminary simulation
59 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
60 Gia_ManForEachRi( p, pObj, k )
61 Gia_ObjTerSimSet0( pObj );
62 for ( i = 0; i <= pCex->iFrame; i++ )
63 {
64 Gia_ManForEachPi( p, pObj, k )
65 {
66 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
67 Gia_ObjTerSimSetX( pObj );
68 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
69 Gia_ObjTerSimSet1( pObj );
70 else
71 Gia_ObjTerSimSet0( pObj );
72 }
73 Gia_ManForEachRo( p, pObj, k )
74 Gia_ObjTerSimRo( p, pObj );
75 Gia_ManForEachAnd( p, pObj, k )
76 Gia_ObjTerSimAnd( pObj );
77 Gia_ManForEachCo( p, pObj, k )
78 Gia_ObjTerSimCo( pObj );
79 // add cares to the exdended counter-example
80 Gia_ManForEachObj( p, pObj, k )
81 if ( !Gia_ObjTerSimGetX(pObj) )
82 Abc_InfoSetBit( pNew->pData, pNew->nRegs + pNew->nPis * i + k );
83 }
84 pObj = Gia_ManPo( p, pCex->iPo );
85 assert( Gia_ObjTerSimGet1(pObj) );
86 return pNew;
87 }
88
89 /**Function*************************************************************
90
91 Synopsis [Forward propagation.]
92
93 Description []
94
95 SideEffects []
96
97 SeeAlso []
98
99 ***********************************************************************/
Bmc_CexCarePropagateFwdOne(Gia_Man_t * p,Abc_Cex_t * pCex,int f,Vec_Int_t * vPriosIn)100 void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Vec_Int_t * vPriosIn )
101 {
102 Gia_Obj_t * pObj;
103 int Prio, Prio0, Prio1;
104 int i, Phase0, Phase1;
105 assert( Vec_IntSize(vPriosIn) == pCex->nPis * (pCex->iFrame + 1) );
106 Gia_ManForEachPi( p, pObj, i )
107 pObj->Value = Vec_IntEntry( vPriosIn, f * pCex->nPis + i );
108 Gia_ManForEachAnd( p, pObj, i )
109 {
110 Prio0 = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value);
111 Prio1 = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value);
112 Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
113 Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
114 if ( Phase0 && Phase1 )
115 Prio = Abc_MinInt(Prio0, Prio1);
116 else if ( Phase0 )
117 Prio = Prio1;
118 else if ( Phase1 )
119 Prio = Prio0;
120 else // if ( !Phase0 && !Phase1 )
121 Prio = Abc_MaxInt(Prio0, Prio1);
122 pObj->Value = Abc_Var2Lit( Prio, Phase0 && Phase1 );
123 pObj->fPhase = 0;
124 }
125 Gia_ManForEachCo( p, pObj, i )
126 pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
127 }
Bmc_CexCarePropagateFwd(Gia_Man_t * p,Abc_Cex_t * pCex,Vec_Int_t * vPriosIn,Vec_Int_t * vPriosFf)128 void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPriosIn, Vec_Int_t * vPriosFf )
129 {
130 Gia_Obj_t * pObjRo, * pObjRi;
131 int i, f, ValueMax = Abc_Var2Lit( pCex->nPis * (pCex->iFrame + 1), 0 );
132 Gia_ManConst0( p )->Value = ValueMax;
133 Gia_ManForEachRi( p, pObjRi, i )
134 pObjRi->Value = ValueMax;
135 Vec_IntClear( vPriosFf );
136 for ( f = 0; f <= pCex->iFrame; f++ )
137 {
138 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
139 Vec_IntPush( vPriosFf, (pObjRo->Value = pObjRi->Value) );
140 Bmc_CexCarePropagateFwdOne( p, pCex, f, vPriosIn );
141 }
142 }
143
144 /**Function*************************************************************
145
146 Synopsis [Backward propagation.]
147
148 Description []
149
150 SideEffects []
151
152 SeeAlso []
153
154 ***********************************************************************/
Bmc_CexCarePropagateBwdOne(Gia_Man_t * p,Abc_Cex_t * pCex,int f,Abc_Cex_t * pCexMin)155 void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin )
156 {
157 Gia_Obj_t * pObj, * pFan0, * pFan1;
158 int i, Phase0, Phase1;
159 Gia_ManForEachCi( p, pObj, i )
160 pObj->fPhase = 0;
161 Gia_ManForEachCo( p, pObj, i )
162 if ( pObj->fPhase )
163 Gia_ObjFanin0(pObj)->fPhase = 1;
164 Gia_ManForEachAndReverse( p, pObj, i )
165 {
166 if ( !pObj->fPhase )
167 continue;
168 pFan0 = Gia_ObjFanin0(pObj);
169 pFan1 = Gia_ObjFanin1(pObj);
170 Phase0 = Abc_LitIsCompl(pFan0->Value) ^ Gia_ObjFaninC0(pObj);
171 Phase1 = Abc_LitIsCompl(pFan1->Value) ^ Gia_ObjFaninC1(pObj);
172 if ( Phase0 && Phase1 )
173 {
174 pFan0->fPhase = 1;
175 pFan1->fPhase = 1;
176 }
177 else if ( Phase0 )
178 pFan1->fPhase = 1;
179 else if ( Phase1 )
180 pFan0->fPhase = 1;
181 else // if ( !Phase0 && !Phase1 )
182 {
183 if ( pFan0->fPhase || pFan1->fPhase )
184 continue;
185 if ( Gia_ObjIsPi(p, pFan0) )
186 pFan0->fPhase = 1;
187 else if ( Gia_ObjIsPi(p, pFan1) )
188 pFan1->fPhase = 1;
189 // else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
190 // pFan0->fPhase = 1;
191 // else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
192 // pFan1->fPhase = 1;
193 else
194 {
195 if ( Abc_Lit2Var(pFan0->Value) > Abc_Lit2Var(pFan1->Value) )
196 pFan0->fPhase = 1;
197 else
198 pFan1->fPhase = 1;
199 }
200 }
201 }
202 Gia_ManForEachPi( p, pObj, i )
203 if ( pObj->fPhase )
204 Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i );
205 }
Bmc_CexCarePropagateBwd(Gia_Man_t * p,Abc_Cex_t * pCex,Vec_Int_t * vPriosIn,Vec_Int_t * vPriosFf)206 Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPriosIn, Vec_Int_t * vPriosFf )
207 {
208 Abc_Cex_t * pCexMin;
209 Gia_Obj_t * pObjRo, * pObjRi;
210 int f, i;
211 pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
212 pCexMin->iPo = pCex->iPo;
213 pCexMin->iFrame = pCex->iFrame;
214 Gia_ManForEachCo( p, pObjRi, i )
215 pObjRi->fPhase = 0;
216 for ( f = pCex->iFrame; f >= 0; f-- )
217 {
218 Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame);
219 Gia_ManForEachRo( p, pObjRo, i )
220 pObjRo->Value = Vec_IntEntry( vPriosFf, f * pCex->nRegs + i );
221 Bmc_CexCarePropagateFwdOne( p, pCex, f, vPriosIn );
222 Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin );
223 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
224 pObjRi->fPhase = pObjRo->fPhase;
225 }
226 return pCexMin;
227 }
228
229 /**Function*************************************************************
230
231 Synopsis [Computes the care set of the counter-example.]
232
233 Description []
234
235 SideEffects []
236
237 SeeAlso []
238
239 ***********************************************************************/
Bmc_CexCareTotal(Abc_Cex_t ** pCexes,int nCexes)240 Abc_Cex_t * Bmc_CexCareTotal( Abc_Cex_t ** pCexes, int nCexes )
241 {
242 int i, k, nWords = Abc_BitWordNum( pCexes[0]->nBits );
243 Abc_Cex_t * pCexMin = Abc_CexAlloc( pCexes[0]->nRegs, pCexes[0]->nPis, pCexes[0]->iFrame + 1 );
244 pCexMin->iPo = pCexes[0]->iPo;
245 pCexMin->iFrame = pCexes[0]->iFrame;
246 for ( i = 0; i < nWords; i++ )
247 {
248 pCexMin->pData[i] = pCexes[0]->pData[i];
249 for ( k = 1; k < nCexes; k++ )
250 pCexMin->pData[i] &= pCexes[k]->pData[i];
251 }
252 return pCexMin;
253 }
Bmc_CexCareMinimizeAig(Gia_Man_t * p,int nRealPis,Abc_Cex_t * pCex,int nTryCexes,int fCheck,int fVerbose)254 Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
255 {
256 //int nTryCexes = 4; // belongs to range [1;4]
257 Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
258 int k, f, i, nOnesBest, nOnesCur, Counter = 0;
259 Vec_Int_t * vPriosIn, * vPriosFf;
260 if ( pCex->nPis != Gia_ManPiNum(p) )
261 {
262 printf( "Given CEX does to have same number of inputs as the AIG.\n" );
263 return NULL;
264 }
265 if ( pCex->nRegs != Gia_ManRegNum(p) )
266 {
267 printf( "Given CEX does to have same number of flops as the AIG.\n" );
268 return NULL;
269 }
270 if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
271 {
272 printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
273 return NULL;
274 }
275 assert( pCex->nPis == Gia_ManPiNum(p) );
276 assert( pCex->nRegs == Gia_ManRegNum(p) );
277 assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
278 if ( fVerbose )
279 {
280 printf( "Original : " );
281 Bmc_CexPrint( pCex, nRealPis, 0 );
282 }
283 vPriosIn = Vec_IntAlloc( pCex->nPis * (pCex->iFrame + 1) );
284 vPriosFf = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
285 for ( k = 0; k < nTryCexes; k++ )
286 {
287 Counter = 0;
288 Vec_IntFill( vPriosIn, pCex->nPis * (pCex->iFrame + 1), 0 );
289 /*
290 if ( k == 0 )
291 {
292 for ( f = 0; f <= pCex->iFrame; f++ )
293 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
294 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
295 for ( f = 0; f <= pCex->iFrame; f++ )
296 for ( i = 0; i < nRealPis; i++ )
297 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
298 }
299 else if ( k == 1 )
300 {
301 for ( f = pCex->iFrame; f >= 0; f-- )
302 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
303 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
304 for ( f = pCex->iFrame; f >= 0; f-- )
305 for ( i = 0; i < nRealPis; i++ )
306 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
307 }
308 else if ( k == 2 )
309 {
310 for ( f = 0; f <= pCex->iFrame; f++ )
311 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
312 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
313 for ( f = 0; f <= pCex->iFrame; f++ )
314 for ( i = nRealPis - 1; i >= 0; i-- )
315 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
316 }
317 else if ( k == 3 )
318 {
319 for ( f = pCex->iFrame; f >= 0; f-- )
320 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
321 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
322 for ( f = pCex->iFrame; f >= 0; f-- )
323 for ( i = nRealPis - 1; i >= 0; i-- )
324 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
325 }
326 else assert( 0 );
327 */
328 if ( k == 0 )
329 {
330 for ( f = pCex->iFrame; f >= 0; f-- )
331 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
332 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
333 for ( f = pCex->iFrame; f >= 0; f-- )
334 for ( i = nRealPis - 1; i >= 0; i-- )
335 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
336 }
337 else if ( k == 1 )
338 {
339 for ( f = pCex->iFrame; f >= 0; f-- )
340 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
341 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
342 for ( f = pCex->iFrame; f >= 0; f-- )
343 for ( i = 0; i < nRealPis; i++ )
344 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
345 }
346 else if ( k == 2 )
347 {
348 for ( f = pCex->iFrame; f >= 0; f-- )
349 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
350 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
351 for ( f = pCex->iFrame; f >= 0; f-- )
352 for ( i = nRealPis - 1; i >= 0; i-- )
353 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
354 }
355 else if ( k == 3 )
356 {
357 for ( f = pCex->iFrame; f >= 0; f-- )
358 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
359 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
360 for ( f = pCex->iFrame; f >= 0; f-- )
361 for ( i = 0; i < nRealPis; i++ )
362 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
363 }
364 else assert( 0 );
365
366 assert( Counter == pCex->nPis * (pCex->iFrame + 1) );
367 Bmc_CexCarePropagateFwd( p, pCex, vPriosIn, vPriosFf );
368 assert( Vec_IntSize(vPriosFf) == pCex->nRegs * (pCex->iFrame + 1) );
369 if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
370 {
371 printf( "Counter-example is invalid.\n" );
372 Vec_IntFree( vPriosIn );
373 Vec_IntFree( vPriosFf );
374 return NULL;
375 }
376 pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPriosIn, vPriosFf );
377 if ( fVerbose )
378 {
379 if ( k == 0 )
380 printf( "PI- PPI-: " );
381 else if ( k == 1 )
382 printf( "PI+ PPI-: " );
383 else if ( k == 2 )
384 printf( "PI- PPI+: " );
385 else if ( k == 3 )
386 printf( "PI+ PPI+: " );
387 else assert( 0 );
388 Bmc_CexPrint( pCexMin[k], nRealPis, 0 );
389 }
390 }
391 Vec_IntFree( vPriosIn );
392 Vec_IntFree( vPriosFf );
393 // select the best one
394 pCexBest = pCexMin[0];
395 nOnesBest = Abc_CexCountOnes(pCexMin[0]);
396 for ( k = 1; k < nTryCexes; k++ )
397 {
398 if ( pCexMin[k] == NULL )
399 continue;
400 nOnesCur = Abc_CexCountOnes(pCexMin[k]);
401 if ( nOnesBest > nOnesCur )
402 {
403 nOnesBest = nOnesCur;
404 pCexBest = pCexMin[k];
405 }
406 }
407 if ( fVerbose )
408 {
409 //Abc_Cex_t * pTotal = Bmc_CexCareTotal( pCexMin, nTryCexes );
410 printf( "Final : " );
411 Bmc_CexPrint( pCexBest, nRealPis, 0 );
412 //printf( "Total : " );
413 //Bmc_CexPrint( pTotal, nRealPis, 0 );
414 //Abc_CexFreeP( &pTotal );
415 }
416 for ( k = 0; k < nTryCexes; k++ )
417 if ( pCexMin[k] && pCexBest != pCexMin[k] )
418 Abc_CexFreeP( &pCexMin[k] );
419 // verify and return
420 if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
421 printf( "Counter-example verification has failed.\n" );
422 else if ( fCheck )
423 printf( "Counter-example verification succeeded.\n" );
424 return pCexBest;
425 }
Bmc_CexCareMinimize(Aig_Man_t * p,int nRealPis,Abc_Cex_t * pCex,int nTryCexes,int fCheck,int fVerbose)426 Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
427 {
428 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
429 Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, nTryCexes, fCheck, fVerbose );
430 Gia_ManStop( pGia );
431 return pCexMin;
432 }
Bmc_CexCareSatBasedMinimize(Aig_Man_t * p,int nRealPis,Abc_Cex_t * pCex,int fHighEffort,int fCheck,int fVerbose)433 Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose )
434 {
435 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
436 Abc_Cex_t * pCexMin = Bmc_CexCareSatBasedMinimizeAig( pGia, pCex, fHighEffort, fVerbose );
437 if ( pCexMin == NULL )
438 {
439 Gia_ManStop( pGia );
440 return NULL;
441 }
442 // unfortunately, cannot verify - ternary simulation does not work
443 Gia_ManStop( pGia );
444 return pCexMin;
445 }
446
447 /**Function*************************************************************
448
449 Synopsis [Verifies the care set of the counter-example.]
450
451 Description []
452
453 SideEffects []
454
455 SeeAlso []
456
457 ***********************************************************************/
Bmc_CexCareVerify(Aig_Man_t * p,Abc_Cex_t * pCex,Abc_Cex_t * pCexMin,int fVerbose)458 void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
459 {
460 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
461 if ( fVerbose )
462 {
463 printf( "Original : " );
464 Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
465 printf( "Minimized: " );
466 Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
467 }
468 if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
469 printf( "Counter-example verification has failed.\n" );
470 else
471 printf( "Counter-example verification succeeded.\n" );
472 Gia_ManStop( pGia );
473 }
474 /*
475 {
476 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
477 Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, 4, pAbc->pCex, 1, 1 );
478 Aig_ManStop( pAig );
479 Abc_CexFree( pCex );
480 }
481 */
482
483 ////////////////////////////////////////////////////////////////////////
484 /// END OF FILE ///
485 ////////////////////////////////////////////////////////////////////////
486
487
488 ABC_NAMESPACE_IMPL_END
489
490