1 /**CFile****************************************************************
2 
3   FileName    [pdrMan.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Property driven reachability.]
8 
9   Synopsis    [Manager procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - November 20, 2010.]
16 
17   Revision    [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "pdrInt.h"
22 #include "sat/bmc/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    [Structural analysis.]
38 
39   Description []
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Pdr_ManDeriveFlopPriorities3(Gia_Man_t * p,int fMuxCtrls)46 Vec_Int_t * Pdr_ManDeriveFlopPriorities3( Gia_Man_t * p, int fMuxCtrls )
47 {
48     int fDiscount = 0;
49     Vec_Wec_t * vLevels;
50     Vec_Int_t * vRes, * vLevel, * vCosts;
51     Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
52     int i, k, Entry, MaxEntry = 0;
53     Gia_ManCreateRefs(p);
54     // discount references
55     if ( fDiscount )
56     {
57         Gia_ManForEachAnd( p, pObj, i )
58         {
59             if ( !Gia_ObjIsMuxType(pObj) )
60                 continue;
61             pCtrl  = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
62             pData0 = Gia_Regular(pData0);
63             pData1 = Gia_Regular(pData1);
64             p->pRefs[Gia_ObjId(p, pCtrl)]--;
65             if ( pData0 == pData1 )
66                 p->pRefs[Gia_ObjId(p, pData0)]--;
67         }
68     }
69     // create flop costs
70     vCosts = Vec_IntAlloc( Gia_ManRegNum(p) );
71     Gia_ManForEachRo( p, pObj, i )
72     {
73         Vec_IntPush( vCosts, Gia_ObjRefNum(p, pObj) );
74         MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
75         //printf( "%d(%d) ", i, Gia_ObjRefNum(p, pObj) );
76     }
77     //printf( "\n" );
78     MaxEntry++;
79     // add costs due to MUX inputs
80     if ( fMuxCtrls )
81     {
82         int fVerbose = 0;
83         Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
84         Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
85         Gia_Obj_t * pCtrl, * pData1, * pData0;
86         int nCtrls = 0, nDatas = 0, nBoth = 0;
87         Gia_ManForEachAnd( p, pObj, i )
88         {
89             if ( !Gia_ObjIsMuxType(pObj) )
90                 continue;
91             pCtrl  = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
92             pCtrl  = Gia_Regular(pCtrl);
93             pData1 = Gia_Regular(pData1);
94             pData0 = Gia_Regular(pData0);
95             Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
96             Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
97             Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
98         }
99         Gia_ManForEachRo( p, pObj, i )
100             if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
101                 Vec_IntAddToEntry( vCosts, i, MaxEntry );
102             //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
103             //    Vec_IntAddToEntry( vCosts, i,   MaxEntry );
104         MaxEntry = 2*MaxEntry + 1;
105         // print out
106         if ( fVerbose )
107         {
108             Gia_ManForEachRo( p, pObj, i )
109             {
110                 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
111                     nCtrls++;
112                 if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
113                     nDatas++;
114                 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
115                     nBoth++;
116             }
117             printf( "%10s : Flops = %5d.  Ctrls = %5d.  Datas = %5d.  Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
118         }
119         Vec_BitFree( vCtrls );
120         Vec_BitFree( vDatas );
121     }
122     // create levelized structure
123     vLevels = Vec_WecStart( MaxEntry );
124     Vec_IntForEachEntry( vCosts, Entry, i )
125         Vec_WecPush( vLevels, Entry, i );
126     // collect in this order
127     MaxEntry = 0;
128     vRes = Vec_IntStart( Gia_ManRegNum(p) );
129     Vec_WecForEachLevel( vLevels, vLevel, i )
130         Vec_IntForEachEntry( vLevel, Entry, k )
131             Vec_IntWriteEntry( vRes, Entry, MaxEntry++ );
132         //printf( "%d ", Gia_ObjRefNum(p, Gia_ManCi(p, Gia_ManPiNum(p)+Entry)) );
133     //printf( "\n" );
134     assert( MaxEntry == Gia_ManRegNum(p) );
135     Vec_WecFree( vLevels );
136     Vec_IntFree( vCosts );
137     ABC_FREE( p->pRefs );
138 //Vec_IntPrint( vRes );
139     return vRes;
140 }
141 
142 /**Function*************************************************************
143 
144   Synopsis    [Structural analysis.]
145 
146   Description []
147 
148   SideEffects []
149 
150   SeeAlso     []
151 
152 ***********************************************************************/
Pdr_ManDeriveFlopPriorities2(Gia_Man_t * p,int fMuxCtrls)153 Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls )
154 {
155     int fDiscount = 0;
156     Vec_Int_t * vRes = NULL;
157     Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
158     int MaxEntry = 0;
159     int i, * pPerm;
160     // create flop costs
161     Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) );
162     Gia_ManCreateRefs(p);
163     // discount references
164     if ( fDiscount )
165     {
166         Gia_ManForEachAnd( p, pObj, i )
167         {
168             if ( !Gia_ObjIsMuxType(pObj) )
169                 continue;
170             pCtrl  = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
171             pData0 = Gia_Regular(pData0);
172             pData1 = Gia_Regular(pData1);
173             p->pRefs[Gia_ObjId(p, pCtrl)]--;
174             if ( pData0 == pData1 )
175                 p->pRefs[Gia_ObjId(p, pData0)]--;
176         }
177     }
178     Gia_ManForEachRo( p, pObj, i )
179     {
180         Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) );
181         MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
182     }
183     MaxEntry++;
184     ABC_FREE( p->pRefs );
185     // add costs due to MUX inputs
186     if ( fMuxCtrls )
187     {
188         int fVerbose = 0;
189         Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
190         Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
191         Gia_Obj_t * pCtrl, * pData1, * pData0;
192         int nCtrls = 0, nDatas = 0, nBoth = 0;
193         Gia_ManForEachAnd( p, pObj, i )
194         {
195             if ( !Gia_ObjIsMuxType(pObj) )
196                 continue;
197             pCtrl  = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
198             pCtrl  = Gia_Regular(pCtrl);
199             pData1 = Gia_Regular(pData1);
200             pData0 = Gia_Regular(pData0);
201             Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
202             Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
203             Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
204         }
205         Gia_ManForEachRo( p, pObj, i )
206             if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
207                 Vec_IntAddToEntry( vCosts, i, MaxEntry );
208             //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
209             //    Vec_IntAddToEntry( vCosts, i,   MaxEntry );
210         // print out
211         if ( fVerbose )
212         {
213             Gia_ManForEachRo( p, pObj, i )
214             {
215                 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
216                     nCtrls++;
217                 if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
218                     nDatas++;
219                 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
220                     nBoth++;
221             }
222             printf( "%10s : Flops = %5d.  Ctrls = %5d.  Datas = %5d.  Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
223         }
224         Vec_BitFree( vCtrls );
225         Vec_BitFree( vDatas );
226     }
227     // create ordering based on costs
228     pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
229     vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) );
230     Vec_IntFree( vCosts );
231     vCosts = Vec_IntInvert( vRes, -1 );
232     Vec_IntFree( vRes );
233 //Vec_IntPrint( vCosts );
234     return vCosts;
235 }
236 
237 /**Function*************************************************************
238 
239   Synopsis    [Creates manager.]
240 
241   Description []
242 
243   SideEffects []
244 
245   SeeAlso     []
246 
247 ***********************************************************************/
Pdr_ManStart(Aig_Man_t * pAig,Pdr_Par_t * pPars,Vec_Int_t * vPrioInit)248 Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
249 {
250     Pdr_Man_t * p;
251     p = ABC_CALLOC( Pdr_Man_t, 1 );
252     p->pPars    = pPars;
253     p->pAig     = pAig;
254     p->pGia     = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
255     p->vSolvers = Vec_PtrAlloc( 0 );
256     p->vClauses = Vec_VecAlloc( 0 );
257     p->pQueue   = NULL;
258     p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
259     p->vActVars = Vec_IntAlloc( 256 );
260     if ( !p->pPars->fMonoCnf )
261         p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
262     // internal use
263     p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig));
264     if ( vPrioInit )
265         p->vPrio = vPrioInit;
266     else if ( pPars->fFlopPrio )
267         p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
268 //    else if ( p->pPars->fNewXSim )
269 //        p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
270     else
271         p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
272     p->vLits    = Vec_IntAlloc( 100 );  // array of literals
273     p->vCiObjs  = Vec_IntAlloc( 100 );  // cone leaves
274     p->vCoObjs  = Vec_IntAlloc( 100 );  // cone roots
275     p->vCiVals  = Vec_IntAlloc( 100 );  // cone leaf values
276     p->vCoVals  = Vec_IntAlloc( 100 );  // cone root values
277     p->vNodes   = Vec_IntAlloc( 100 );  // cone nodes
278     p->vUndo    = Vec_IntAlloc( 100 );  // cone undos
279     p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
280     p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
281     p->vRes     = Vec_IntAlloc( 100 );  // final result
282     p->pCnfMan  = Cnf_ManStart();
283     // ternary simulation
284     p->pTxs3    = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
285     // additional AIG data-members
286     if ( pAig->pFanData == NULL )
287         Aig_ManFanoutStart( pAig );
288     if ( pAig->pTerSimData == NULL )
289         pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
290     // time spent on each outputs
291     if ( pPars->nTimeOutOne )
292     {
293         int i;
294         p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
295         for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
296             p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
297     }
298     if ( pPars->fSolveAll )
299     {
300         p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
301         p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
302         Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
303     }
304     return p;
305 }
306 
307 /**Function*************************************************************
308 
309   Synopsis    [Frees manager.]
310 
311   Description []
312 
313   SideEffects []
314 
315   SeeAlso     []
316 
317 ***********************************************************************/
Pdr_ManStop(Pdr_Man_t * p)318 void Pdr_ManStop( Pdr_Man_t * p )
319 {
320     Pdr_Set_t * pCla;
321     sat_solver * pSat;
322     int i, k;
323     Gia_ManStopP( &p->pGia );
324     Aig_ManCleanMarkAB( p->pAig );
325     if ( p->pPars->fVerbose )
326     {
327         Abc_Print( 1, "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Cex =%4d  Start =%4d\n",
328             p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
329         ABC_PRTP( "SAT solving", p->tSat,       p->tTotal );
330         ABC_PRTP( "  unsat    ", p->tSatUnsat,  p->tTotal );
331         ABC_PRTP( "  sat      ", p->tSatSat,    p->tTotal );
332         ABC_PRTP( "Generalize ", p->tGeneral,   p->tTotal );
333         ABC_PRTP( "Push clause", p->tPush,      p->tTotal );
334         ABC_PRTP( "Ternary sim", p->tTsim,      p->tTotal );
335         ABC_PRTP( "Containment", p->tContain,   p->tTotal );
336         ABC_PRTP( "CNF compute", p->tCnf,       p->tTotal );
337         ABC_PRTP( "Refinement ", p->tAbs,       p->tTotal );
338         ABC_PRTP( "TOTAL      ", p->tTotal,     p->tTotal );
339         fflush( stdout );
340     }
341 //    Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
342     Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
343         sat_solver_delete( pSat );
344     Vec_PtrFree( p->vSolvers );
345     Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
346         Pdr_SetDeref( pCla );
347     Vec_VecFree( p->vClauses );
348     Pdr_QueueStop( p );
349     ABC_FREE( p->pOrder );
350     Vec_IntFree( p->vActVars );
351     // static CNF
352     Cnf_DataFree( p->pCnf1 );
353     Vec_IntFreeP( &p->vVar2Reg );
354     // dynamic CNF
355     Cnf_DataFree( p->pCnf2 );
356     if ( p->pvId2Vars )
357     for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
358         ABC_FREE( p->pvId2Vars[i].pArray );
359     ABC_FREE( p->pvId2Vars );
360 //    Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
361     for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
362         Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
363     ABC_FREE( p->vVar2Ids.pArray );
364     Vec_WecFreeP( &p->vVLits );
365     // CNF manager
366     Cnf_ManStop( p->pCnfMan );
367     Vec_IntFreeP( &p->vAbsFlops );
368     Vec_IntFreeP( &p->vMapFf2Ppi );
369     Vec_IntFreeP( &p->vMapPpi2Ff );
370     // terminary simulation
371     if ( p->pPars->fNewXSim )
372         Txs3_ManStop( p->pTxs3 );
373     // internal use
374     Vec_IntFreeP( &p->vPrio   );  // priority flops
375     Vec_IntFree( p->vLits     );  // array of literals
376     Vec_IntFree( p->vCiObjs   );  // cone leaves
377     Vec_IntFree( p->vCoObjs   );  // cone roots
378     Vec_IntFree( p->vCiVals   );  // cone leaf values
379     Vec_IntFree( p->vCoVals   );  // cone root values
380     Vec_IntFree( p->vNodes    );  // cone nodes
381     Vec_IntFree( p->vUndo     );  // cone undos
382     Vec_IntFree( p->vVisits   );  // intermediate
383     Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
384     Vec_IntFree( p->vRes      );  // final result
385     Vec_PtrFreeP( &p->vInfCubes );
386     ABC_FREE( p->pTime4Outs );
387     if ( p->vCexes )
388         Vec_PtrFreeFree( p->vCexes );
389     // additional AIG data-members
390     if ( p->pAig->pFanData != NULL )
391         Aig_ManFanoutStop( p->pAig );
392     if ( p->pAig->pTerSimData != NULL )
393         ABC_FREE( p->pAig->pTerSimData );
394     ABC_FREE( p );
395 }
396 
397 /**Function*************************************************************
398 
399   Synopsis    [Derives counter-example.]
400 
401   Description []
402 
403   SideEffects []
404 
405   SeeAlso     []
406 
407 ***********************************************************************/
Pdr_ManDeriveCex(Pdr_Man_t * p)408 Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
409 {
410     Abc_Cex_t * pCex;
411     Pdr_Obl_t * pObl;
412     int i, f, Lit, nFrames = 0;
413     // count the number of frames
414     for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
415         nFrames++;
416     // create the counter-example
417     pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
418     pCex->iPo    = p->iOutCur;
419     pCex->iFrame = nFrames-1;
420     for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
421         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
422         {
423             Lit = pObl->pState->Lits[i];
424             if ( Abc_LitIsCompl(Lit) )
425                 continue;
426             if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
427                 continue;
428             assert( Abc_Lit2Var(Lit) < pCex->nPis );
429             Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
430         }
431     assert( f == nFrames );
432     if ( !Saig_ManVerifyCex(p->pAig, pCex) )
433         printf( "CEX for output %d is not valid.\n", p->iOutCur );
434     return pCex;
435 }
436 
437 /**Function*************************************************************
438 
439   Synopsis    [Derives counter-example when abstraction is used.]
440 
441   Description []
442 
443   SideEffects []
444 
445   SeeAlso     []
446 
447 ***********************************************************************/
Pdr_ManDeriveCexAbs(Pdr_Man_t * p)448 Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
449 {
450     extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
451 
452     Gia_Man_t * pAbs;
453     Abc_Cex_t * pCex, * pCexCare;
454     Pdr_Obl_t * pObl;
455     int i, f, Lit, Flop, nFrames = 0;
456     int nPis = Saig_ManPiNum(p->pAig);
457     int nFfRefined = 0;
458     if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
459         return Pdr_ManDeriveCex(p);
460     // restore previous map
461     Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
462     {
463         assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
464         Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
465     }
466     Vec_IntClear( p->vMapPpi2Ff );
467     // count the number of frames
468     for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
469     {
470         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
471         {
472             Lit = pObl->pState->Lits[i];
473             if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
474                 continue;
475             Flop = Abc_Lit2Var(Lit) - nPis;
476             if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
477                 continue;
478             Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
479             Vec_IntPush( p->vMapPpi2Ff, Flop );
480         }
481         nFrames++;
482     }
483     if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
484         return Pdr_ManDeriveCex(p);
485     if ( p->pPars->fUseSimpleRef )
486     {
487         // rely on ternary simulation to perform refinement
488         Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
489         {
490             assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
491             Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
492             nFfRefined++;
493         }
494     }
495     else
496     {
497         // create the counter-example
498         pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
499         pCex->iPo    = p->iOutCur;
500         pCex->iFrame = nFrames-1;
501         for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
502             for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
503             {
504                 Lit = pObl->pState->Lits[i];
505                 if ( Abc_LitIsCompl(Lit) )
506                     continue;
507                 if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
508                     Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
509                 else
510                 {
511                     int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
512                     assert( iPPI < pCex->nPis );
513                     Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
514                 }
515             }
516         assert( f == nFrames );
517         // perform CEX minimization
518         pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
519         pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
520         Gia_ManStop( pAbs );
521         assert( pCexCare->nPis == pCex->nPis );
522         Abc_CexFree( pCex );
523         // detect care PPIs
524         for ( f = 0; f < nFrames; f++ )
525         {
526             for ( i = nPis; i < pCexCare->nPis; i++ )
527                 if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
528                 {
529                     if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
530                         Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
531                 }
532         }
533         Abc_CexFree( pCexCare );
534         if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
535             return Pdr_ManDeriveCex(p);
536     }
537     //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
538     p->nCexesTotal++;
539     p->nCexes++;
540     return NULL;
541 }
542 
543 ////////////////////////////////////////////////////////////////////////
544 ///                       END OF FILE                                ///
545 ////////////////////////////////////////////////////////////////////////
546 
547 
548 ABC_NAMESPACE_IMPL_END
549 
550