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