abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaFalse.c
Go to the documentation of this file.
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 }
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 );
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 }
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 }
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 
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_ObjLevelId
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Vec_WecLevelSize
static int Vec_WecLevelSize(Vec_Wec_t *p, int i)
Definition: vecWec.h:197
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition: vecWec.h:42
Gia_ManCollectPath_rec
void Gia_ManCollectPath_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPath)
Definition: giaFalse.c:134
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_ManCollectNodesCis
Vec_Int_t * Gia_ManCollectNodesCis(Gia_Man_t *p, int *pNodes, int nNodes)
Definition: giaDfs.c:178
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Vec_WecFree
static void Vec_WecFree(Vec_Wec_t *p)
Definition: vecWec.h:345
Vec_QueTopPriority
static float Vec_QueTopPriority(Vec_Que_t *p)
Definition: vecQue.h:143
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Vec_FltFree
static void Vec_FltFree(Vec_Flt_t *p)
Definition: vecFlt.h:218
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_WecStart
static Vec_Wec_t * Vec_WecStart(int nSize)
Definition: vecWec.h:98
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_Que_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Que_t_ Vec_Que_t
INCLUDES ///.
Definition: vecQue.h:40
Gia_ManFalseRebuildPath
Gia_Man_t * Gia_ManFalseRebuildPath(Gia_Man_t *p, Vec_Int_t *vHooks, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:326
Vec_FltAlloc
static Vec_Flt_t * Vec_FltAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecFlt.h:78
l_True
#define l_True
Definition: SolverTypes.h:84
sat_solver_add_xor
static int sat_solver_add_xor(sat_solver *pSat, int iVarA, int iVarB, int iVarC, int fCompl)
Definition: satSolver.h:346
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Vec_WecSizeUsed
static int Vec_WecSizeUsed(Vec_Wec_t *p)
Definition: vecWec.h:210
Vec_QuePop
static int Vec_QuePop(Vec_Que_t *p)
Definition: vecQue.h:234
Gia_Man_t_::nLevels
int nLevels
Definition: gia.h:116
Gia_ManCheckOne
Gia_Man_t * Gia_ManCheckOne(Gia_Man_t *p, int iOut, int iObj, int nTimeOut, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:357
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Gia_ManFalseRebuildOne
ABC_NAMESPACE_IMPL_START void Gia_ManFalseRebuildOne(Gia_Man_t *pNew, Gia_Man_t *p, Vec_Int_t *vHook, int fVerbose, int fVeryVerbose)
DECLARATIONS ///.
Definition: giaFalse.c:48
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Vec_FltPush
static void Vec_FltPush(Vec_Flt_t *p, float Entry)
Definition: vecFlt.h:528
Gia_Obj_t_
Definition: gia.h:75
sat_solver_final
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManCheckFalse
Gia_Man_t * Gia_ManCheckFalse(Gia_Man_t *p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:497
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManCheckFalseAll
Gia_Man_t * Gia_ManCheckFalseAll(Gia_Man_t *p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:467
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Gia_ObjPrint
void Gia_ObjPrint(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1258
Gia_ManCollectPath
Vec_Int_t * Gia_ManCollectPath(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaFalse.c:149
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_WecEntry
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
Vec_IntEntryLast
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
Gia_ManCo
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_FltArrayP
static float ** Vec_FltArrayP(Vec_Flt_t *p)
Definition: vecFlt.h:278
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Vec_Flt_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Flt_t_ Vec_Flt_t
INCLUDES ///.
Definition: vecFlt.h:42
Gia_ManCheckFalse2
Gia_Man_t * Gia_ManCheckFalse2(Gia_Man_t *p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:279
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Vec_QueFree
static void Vec_QueFree(Vec_Que_t *p)
Definition: vecQue.h:83
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_ManCheckFalseOne
void Gia_ManCheckFalseOne(Gia_Man_t *p, int iOut, int nTimeOut, Vec_Wec_t *vHooks, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:167
Vec_IntPrint
static void Vec_IntPrint(Vec_Int_t *vVec)
Definition: vecInt.h:1803
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_QueAlloc
static Vec_Que_t * Vec_QueAlloc(int nCap)
MACRO DEFINITIONS ///.
Definition: vecQue.h:71
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Vec_QuePush
static void Vec_QuePush(Vec_Que_t *p, int v)
Definition: vecQue.h:221
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManFalseRebuild
Gia_Man_t * Gia_ManFalseRebuild(Gia_Man_t *p, Vec_Wec_t *vHooks, int fVerbose, int fVeryVerbose)
Definition: giaFalse.c:88
Vec_QueSetPriority
static void Vec_QueSetPriority(Vec_Que_t *p, float **pCosts)
Definition: vecQue.h:95
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
sat_solver_add_and
static int sat_solver_add_and(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl)
Definition: satSolver.h:324
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387