1 /**CFile****************************************************************
2 
3   FileName    [giaFalse.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Scalable AIG package.]
8 
9   Synopsis    [Detection and elimination of false paths.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: giaFalse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "misc/vec/vecQue.h"
23 #include "misc/vec/vecWec.h"
24 #include "sat/bsat/satStore.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                        DECLARATIONS                              ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 ///                     FUNCTION DEFINITIONS                         ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39   Synopsis    [Reconstruct the AIG after detecting false paths.]
40 
41   Description []
42 
43   SideEffects []
44 
45   SeeAlso     []
46 
47 ***********************************************************************/
Gia_ManFalseRebuildOne(Gia_Man_t * pNew,Gia_Man_t * p,Vec_Int_t * vHook,int fVerbose,int fVeryVerbose)48 void Gia_ManFalseRebuildOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vHook, int fVerbose, int fVeryVerbose )
49 {
50     Gia_Obj_t * pObj, * pObj1, * pPrev = NULL;
51     int i, CtrlValue = 0, iPrevValue = -1;
52     pObj = Gia_ManObj( p, Vec_IntEntry(vHook, 0) );
53     if ( Vec_IntSize(vHook) == 1 )
54     {
55         pObj->Value = 0; // what if stuck at 1???
56         return;
57     }
58     assert( Vec_IntSize(vHook) >= 2 );
59     // find controlling value
60     pObj1 = Gia_ManObj( p, Vec_IntEntry(vHook, 1) );
61     if ( Gia_ObjFanin0(pObj1) == pObj )
62         CtrlValue = Gia_ObjFaninC0(pObj1);
63     else if ( Gia_ObjFanin1(pObj1) == pObj )
64         CtrlValue = Gia_ObjFaninC1(pObj1);
65     else assert( 0 );
66 //    printf( "%d ", CtrlValue );
67     // rewrite the path
68     Gia_ManForEachObjVec( vHook, p, pObj, i )
69     {
70         int iObjValue = pObj->Value;
71         pObj->Value = i ? Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)) : CtrlValue;
72         if ( pPrev )
73             pPrev->Value = iPrevValue;
74         iPrevValue = iObjValue;
75         pPrev = pObj;
76     }
77     if ( fVeryVerbose )
78     {
79         printf( "Eliminated path: " );
80         Vec_IntPrint( vHook );
81         Gia_ManForEachObjVec( vHook, p, pObj, i )
82         {
83             printf( "Level %3d : ", Gia_ObjLevel(p, pObj) );
84             Gia_ObjPrint( p, pObj );
85         }
86     }
87 }
Gia_ManFalseRebuild(Gia_Man_t * p,Vec_Wec_t * vHooks,int fVerbose,int fVeryVerbose)88 Gia_Man_t * Gia_ManFalseRebuild( Gia_Man_t * p, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
89 {
90     Gia_Man_t * pNew, * pTemp;
91     Gia_Obj_t * pObj;
92     int i, Counter = 0;
93     pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) / 3 );
94     pNew->pName = Abc_UtilStrsav( p->pName );
95     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
96     Gia_ManConst0(p)->Value = 0;
97     Gia_ManHashAlloc( pNew );
98     Gia_ManForEachObj1( p, pObj, i )
99     {
100         if ( Gia_ObjIsAnd(pObj) )
101         {
102             if ( Vec_WecLevelSize(vHooks, i) > 0 )
103             {
104                 if ( fVeryVerbose )
105                     printf( "Path %d : ", Counter++ );
106                 Gia_ManFalseRebuildOne( pNew, p, Vec_WecEntry(vHooks, i), fVerbose, fVeryVerbose );
107             }
108             else
109                 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
110         }
111         else if ( Gia_ObjIsCi(pObj) )
112             pObj->Value = Gia_ManAppendCi( pNew );
113         else if ( Gia_ObjIsCo(pObj) )
114             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
115     }
116     Gia_ManHashStop( pNew );
117     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
118     pNew = Gia_ManCleanup( pTemp = pNew );
119     Gia_ManStop( pTemp );
120     return pNew;
121 }
122 
123 /**Function*************************************************************
124 
125   Synopsis    [Derive critical path by following minimum slacks.]
126 
127   Description []
128 
129   SideEffects []
130 
131   SeeAlso     []
132 
133 ***********************************************************************/
Gia_ManCollectPath_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vPath)134 void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPath )
135 {
136     if ( Gia_ObjIsAnd(pObj) )
137     {
138         if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) > Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) )
139             Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
140         else if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) )
141             Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath );
142 //        else if ( rand() & 1 )
143 //            Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
144         else
145             Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath );
146     }
147     Vec_IntPush( vPath, Gia_ObjId(p, pObj) );
148 }
Gia_ManCollectPath(Gia_Man_t * p,Gia_Obj_t * pObj)149 Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj )
150 {
151     Vec_Int_t * vPath = Vec_IntAlloc( p->nLevels );
152     Gia_ManCollectPath_rec( p, Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj, vPath );
153     return vPath;
154 }
155 
156 /**Function*************************************************************
157 
158   Synopsis    []
159 
160   Description []
161 
162   SideEffects []
163 
164   SeeAlso     []
165 
166 ***********************************************************************/
Gia_ManCheckFalseOne(Gia_Man_t * p,int iOut,int nTimeOut,Vec_Wec_t * vHooks,int fVerbose,int fVeryVerbose)167 void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
168 {
169     sat_solver * pSat;
170     Gia_Obj_t * pObj, * pFanin;
171     Gia_Obj_t * pPivot = Gia_ManCo( p, iOut );
172     Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels );
173     Vec_Int_t * vPath = Gia_ManCollectPath( p, pPivot );
174     int nLits = 0, * pLits = NULL;
175     int i, Shift[2], status;
176     abctime clkStart = Abc_Clock();
177     // collect objects and assign SAT variables
178     int iFanin = Gia_ObjFaninId0p( p, pPivot );
179     Vec_Int_t * vObjs = Gia_ManCollectNodesCis( p, &iFanin, 1 );
180     Gia_ManForEachObjVec( vObjs, p, pObj, i )
181         pObj->Value = Vec_IntSize(vObjs) - 1 - i;
182     assert( Gia_ObjIsCo(pPivot) );
183     // create SAT solver
184     pSat = sat_solver_new();
185     sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
186     sat_solver_setnvars( pSat, 3 * Vec_IntSize(vPath) + 2 * Vec_IntSize(vObjs) );
187     Shift[0] = 3 * Vec_IntSize(vPath);
188     Shift[1] = 3 * Vec_IntSize(vPath) + Vec_IntSize(vObjs);
189     // add CNF for the cone
190     Gia_ManForEachObjVec( vObjs, p, pObj, i )
191     {
192         if ( !Gia_ObjIsAnd(pObj) )
193             continue;
194         sat_solver_add_and( pSat, pObj->Value + Shift[0],
195             Gia_ObjFanin0(pObj)->Value + Shift[0], Gia_ObjFanin1(pObj)->Value + Shift[0],
196             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
197         sat_solver_add_and( pSat, pObj->Value + Shift[1],
198             Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1],
199             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
200     }
201     // add CNF for the path
202     Gia_ManForEachObjVec( vPath, p, pObj, i )
203     {
204         if ( Gia_ObjIsAnd(pObj) )
205         {
206             assert( i > 0 );
207             pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
208             if ( pFanin == Gia_ObjFanin0(pObj) )
209             {
210                 sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
211                     i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0],
212                     Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
213                 sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
214                     i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1],
215                     Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
216             }
217             else if ( pFanin == Gia_ObjFanin1(pObj) )
218             {
219                 sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
220                     Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath),
221                     Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
222                 sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
223                     Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath),
224                     Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
225             }
226             else assert( 0 );
227             sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
228         }
229         else if ( Gia_ObjIsCi(pObj) )
230             sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 );
231         else assert( 0 );
232         Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
233     }
234     // call the SAT solver
235     status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)nTimeOut, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
236     if ( status == l_False )
237     {
238         int iBeg, iEnd;
239         nLits = sat_solver_final( pSat, &pLits );
240         iBeg  = Abc_Lit2Var(pLits[nLits-1]);
241         iEnd  = Abc_Lit2Var(pLits[0]);
242         if ( iEnd - iBeg < 20 )
243         {
244             // check if nodes on the path are already used
245             for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
246                 if ( Vec_WecLevelSize(vHooks, Vec_IntEntry(vPath, i)) > 0 )
247                     break;
248             if ( i > iEnd )
249             {
250                 Vec_Int_t * vHook = Vec_WecEntry(vHooks, Vec_IntEntry(vPath, iEnd));
251                 for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
252                     Vec_IntPush( vHook, Vec_IntEntry(vPath, i) );
253             }
254         }
255     }
256     if ( fVerbose )
257     {
258         printf( "PO %6d : Level = %3d  ", iOut, Gia_ObjLevel(p, pPivot) );
259         if ( status == l_Undef )
260             printf( "Timeout reached after %d seconds. ", nTimeOut );
261         else if ( status == l_True )
262             printf( "There is no false path. " );
263         else
264         {
265             printf( "False path contains %d nodes (out of %d):  ", nLits, Vec_IntSize(vPath) );
266             printf( "top = %d  ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[0])) );
267             if ( fVeryVerbose )
268                 for ( i = 0; i < nLits; i++ )
269                     printf( "%d ", Abc_Lit2Var(pLits[i]) );
270             printf( "  " );
271         }
272         Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
273     }
274     sat_solver_delete( pSat );
275     Vec_IntFree( vObjs );
276     Vec_IntFree( vPath );
277     Vec_IntFree( vLits );
278 }
Gia_ManCheckFalse2(Gia_Man_t * p,int nSlackMax,int nTimeOut,int fVerbose,int fVeryVerbose)279 Gia_Man_t * Gia_ManCheckFalse2( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
280 {
281     Gia_Man_t * pNew;
282     Vec_Wec_t * vHooks;
283     Vec_Que_t * vPrio;
284     Vec_Flt_t * vWeights;
285     Gia_Obj_t * pObj;
286     int i;
287 //    srand( 111 );
288     Gia_ManLevelNum( p );
289     // create PO weights
290     vWeights = Vec_FltAlloc( Gia_ManCoNum(p) );
291     Gia_ManForEachCo( p, pObj, i )
292         Vec_FltPush( vWeights, Gia_ObjLevel(p, pObj) );
293     // put POs into the queue
294     vPrio = Vec_QueAlloc( Gia_ManCoNum(p) );
295     Vec_QueSetPriority( vPrio, Vec_FltArrayP(vWeights) );
296     Gia_ManForEachCo( p, pObj, i )
297         Vec_QuePush( vPrio, i );
298     // work on each PO in the queue
299     vHooks = Vec_WecStart( Gia_ManObjNum(p) );
300     while ( Vec_QueTopPriority(vPrio) >= p->nLevels - nSlackMax )
301         Gia_ManCheckFalseOne( p, Vec_QuePop(vPrio), nTimeOut, vHooks, fVerbose, fVeryVerbose );
302     if ( fVerbose )
303     printf( "Collected %d non-overlapping false paths.\n", Vec_WecSizeUsed(vHooks) );
304     // reconstruct the AIG
305     pNew = Gia_ManFalseRebuild( p, vHooks, fVerbose, fVeryVerbose );
306     // cleanup
307     Vec_WecFree( vHooks );
308     Vec_FltFree( vWeights );
309     Vec_QueFree( vPrio );
310     return pNew;
311 }
312 
313 
314 
315 /**Function*************************************************************
316 
317   Synopsis    []
318 
319   Description []
320 
321   SideEffects []
322 
323   SeeAlso     []
324 
325 ***********************************************************************/
Gia_ManFalseRebuildPath(Gia_Man_t * p,Vec_Int_t * vHooks,int fVerbose,int fVeryVerbose)326 Gia_Man_t * Gia_ManFalseRebuildPath( Gia_Man_t * p, Vec_Int_t * vHooks, int fVerbose, int fVeryVerbose )
327 {
328     Gia_Man_t * pNew, * pTemp;
329     Gia_Obj_t * pObj;
330     int i, iPathEnd = Vec_IntEntryLast(vHooks);
331     pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) / 3 );
332     pNew->pName = Abc_UtilStrsav( p->pName );
333     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
334     Gia_ManFillValue(p);
335     Gia_ManConst0(p)->Value = 0;
336     Gia_ManHashAlloc( pNew );
337     Gia_ManForEachObj1( p, pObj, i )
338     {
339         if ( Gia_ObjIsAnd(pObj) )
340         {
341             if ( iPathEnd == i )
342                 Gia_ManFalseRebuildOne( pNew, p, vHooks, fVerbose, fVeryVerbose );
343             else
344                 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
345         }
346         else if ( Gia_ObjIsCi(pObj) )
347             pObj->Value = Gia_ManAppendCi( pNew );
348         else if ( Gia_ObjIsCo(pObj) )
349             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
350     }
351     Gia_ManHashStop( pNew );
352     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
353     pNew = Gia_ManCleanup( pTemp = pNew );
354     Gia_ManStop( pTemp );
355     return pNew;
356 }
Gia_ManCheckOne(Gia_Man_t * p,int iOut,int iObj,int nTimeOut,int fVerbose,int fVeryVerbose)357 Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, int fVerbose, int fVeryVerbose )
358 {
359     sat_solver * pSat;
360     Gia_Man_t * pNew;
361     Gia_Obj_t * pObj, * pFanin;
362     Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels );
363     Vec_Int_t * vPath = Gia_ManCollectPath( p, Gia_ManObj(p, iObj) );
364     int nLits = 0, * pLits = NULL;
365     int i, Shift[2], status;
366     abctime clkStart = Abc_Clock();
367     // collect objects and assign SAT variables
368     Vec_Int_t * vObjs = Gia_ManCollectNodesCis( p, &iObj, 1 );
369     Gia_ManForEachObjVec( vObjs, p, pObj, i )
370         pObj->Value = Vec_IntSize(vObjs) - 1 - i;
371     // create SAT solver
372     pSat = sat_solver_new();
373     sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
374     sat_solver_setnvars( pSat, 3 * Vec_IntSize(vPath) + 2 * Vec_IntSize(vObjs) );
375     Shift[0] = 3 * Vec_IntSize(vPath);
376     Shift[1] = 3 * Vec_IntSize(vPath) + Vec_IntSize(vObjs);
377     // add CNF for the cone
378     Gia_ManForEachObjVec( vObjs, p, pObj, i )
379     {
380         if ( !Gia_ObjIsAnd(pObj) )
381             continue;
382         sat_solver_add_and( pSat, pObj->Value + Shift[0],
383             Gia_ObjFanin0(pObj)->Value + Shift[0], Gia_ObjFanin1(pObj)->Value + Shift[0],
384             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
385         sat_solver_add_and( pSat, pObj->Value + Shift[1],
386             Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1],
387             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
388     }
389     // add CNF for the path
390     Gia_ManForEachObjVec( vPath, p, pObj, i )
391     {
392         if ( !Gia_ObjIsAnd(pObj) )
393             continue;
394         assert( i > 0 );
395         pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
396         if ( pFanin == Gia_ObjFanin0(pObj) )
397         {
398             sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
399                 i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0],
400                 Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
401             sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
402                 i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1],
403                 Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
404         }
405         else if ( pFanin == Gia_ObjFanin1(pObj) )
406         {
407             sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
408                 Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath),
409                 Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
410             sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
411                 Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath),
412                 Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
413         }
414         else assert( 0 );
415         sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
416         Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
417     }
418     // call the SAT solver
419     status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)nTimeOut, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
420     Vec_IntClear( vLits );
421     if ( status == l_False )
422     {
423         int iBeg, iEnd;
424         nLits = sat_solver_final( pSat, &pLits );
425         iBeg  = Abc_Lit2Var(pLits[nLits-1]);
426         iEnd  = Abc_Lit2Var(pLits[0]);
427         assert( iBeg <= iEnd );
428         // collect path
429         for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
430 //        for ( i = 0; i < Vec_IntSize(vPath); i++ )
431             Vec_IntPush( vLits, Vec_IntEntry(vPath, i) );
432     }
433     if ( fVerbose )
434     {
435         printf( "PO %6d : Level = %3d  ", iOut, Gia_ObjLevelId(p, iObj) );
436         if ( status == l_Undef )
437             printf( "Timeout reached after %d seconds. ", nTimeOut );
438         else if ( status == l_True )
439             printf( "There is no false path. " );
440         else
441         {
442             printf( "False path contains %d nodes (out of %d):  ", Vec_IntSize(vLits), Vec_IntSize(vPath) );
443             if ( fVeryVerbose )
444                 for ( i = nLits-1; i >= 0; i-- )
445                     printf( "%d ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[i])) );
446             printf( "  " );
447         }
448         Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
449     }
450     sat_solver_delete( pSat );
451     Vec_IntFree( vObjs );
452     Vec_IntFree( vPath );
453     // update the AIG
454     pNew = Vec_IntSize(vLits) ? Gia_ManFalseRebuildPath( p, vLits, fVerbose, fVeryVerbose ) : NULL;
455     Vec_IntFree( vLits );
456 /*
457     if ( pNew )
458     {
459         Gia_Man_t * pTemp = Gia_ManDupDfsNode( p, Gia_ManObj(p, iObj) );
460         Gia_AigerWrite( pTemp, "false.aig", 0, 0, 0 );
461         Abc_Print( 1, "Dumping cone with %d nodes into file \"%s\".\n", Gia_ManAndNum(pTemp), "false.aig" );
462         Gia_ManStop( pTemp );
463     }
464 */
465     return pNew;
466 }
Gia_ManCheckFalseAll(Gia_Man_t * p,int nSlackMax,int nTimeOut,int fVerbose,int fVeryVerbose)467 Gia_Man_t * Gia_ManCheckFalseAll( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
468 {
469     int Tried = 0, Changed = 0;
470     p = Gia_ManDup( p );
471     while ( 1 )
472     {
473         Gia_Man_t * pNew;
474         Gia_Obj_t * pObj;
475         int i, LevelMax, Changed0 = Changed;
476         LevelMax = Gia_ManLevelNum( p );
477         Gia_ManForEachAnd( p, pObj, i )
478         {
479             if ( Gia_ObjLevel(p, pObj) > nSlackMax )
480                 continue;
481             Tried++;
482             pNew = Gia_ManCheckOne( p, -1, i, nTimeOut, fVerbose, fVeryVerbose );
483             if ( pNew == NULL )
484                 continue;
485             Changed++;
486             Gia_ManStop( p );
487             p = pNew;
488             LevelMax = Gia_ManLevelNum( p );
489         }
490         if ( Changed0 == Changed )
491             break;
492     }
493 //    if ( fVerbose )
494         printf( "Performed %d attempts and %d changes.\n", Tried, Changed );
495     return p;
496 }
Gia_ManCheckFalse(Gia_Man_t * p,int nSlackMax,int nTimeOut,int fVerbose,int fVeryVerbose)497 Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
498 {
499     int Tried = 0, Changed = 0;
500     Vec_Int_t * vTried;
501 //    srand( 111 );
502     p = Gia_ManDup( p );
503     vTried = Vec_IntStart( Gia_ManCoNum(p) );
504     while ( 1 )
505     {
506         Gia_Man_t * pNew;
507         Gia_Obj_t * pObj;
508         int i, LevelMax, Changed0 = Changed;
509         LevelMax = Gia_ManLevelNum( p );
510         Gia_ManForEachCo( p, pObj, i )
511         {
512             if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
513                 continue;
514             if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < LevelMax - nSlackMax )
515                 continue;
516             if ( Vec_IntEntry( vTried, i ) )
517                 continue;
518             Tried++;
519             pNew = Gia_ManCheckOne( p, i, Gia_ObjFaninId0p(p, pObj), nTimeOut, fVerbose, fVeryVerbose );
520 /*
521             if ( i != 126 && pNew )
522             {
523                 Gia_ManStop( pNew );
524                 pNew = NULL;
525             }
526 */
527             if ( pNew == NULL )
528             {
529                 Vec_IntWriteEntry( vTried, i, 1 );
530                 continue;
531             }
532             Changed++;
533             Gia_ManStop( p );
534             p = pNew;
535             LevelMax = Gia_ManLevelNum( p );
536         }
537         if ( Changed0 == Changed )
538             break;
539     }
540 //    if ( fVerbose )
541         printf( "Performed %d attempts and %d changes.\n", Tried, Changed );
542     Vec_IntFree( vTried );
543     return p;
544 }
545 
546 ////////////////////////////////////////////////////////////////////////
547 ///                       END OF FILE                                ///
548 ////////////////////////////////////////////////////////////////////////
549 
550 
551 ABC_NAMESPACE_IMPL_END
552 
553