abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb1Reach.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb1Reach.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Reachability analysis.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb1Reach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Derives global BDD for the node.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd )
46 {
47  DdNode * bBdd0, * bBdd1, * bFunc;
48  Vec_Ptr_t * vNodes;
49  Aig_Obj_t * pObj = NULL;
50  int i;
51  abctime TimeStop;
52  if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
53  return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
54  TimeStop = dd->TimeStop; dd->TimeStop = 0;
55  vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 );
56  assert( Vec_PtrSize(vNodes) > 0 );
57  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
58  {
59  if ( !Aig_ObjIsNode(pObj) )
60  continue;
61  bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
62  bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
63  pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
64  }
65  bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc );
66  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
67  {
68  if ( !Aig_ObjIsNode(pObj) )
69  continue;
70  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
71  }
72  Vec_PtrFree( vNodes );
73  if ( Aig_ObjIsCo(pNode) )
74  bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
75  Cudd_Deref( bFunc );
76  dd->TimeStop = TimeStop;
77  return bFunc;
78 }
79 
80 /**Function*************************************************************
81 
82  Synopsis [Derives BDD for the group.]
83 
84  Description []
85 
86  SideEffects []
87 
88  SeeAlso []
89 
90 ***********************************************************************/
91 DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
92 {
93  Aig_Obj_t * pObj;
94  DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp;
95  int i, k;
96  Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd );
97  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
98  pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
99  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
100  {
101  bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
102  bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
103 // pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget );
104  pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 );
105  if ( pObj->pData == NULL )
106  {
107  Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
108  if ( pObj->pData )
109  Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
110  return NULL;
111  }
112  Cudd_Ref( (DdNode *)pObj->pData );
113  }
114  bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
115  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
116  {
117  if ( Aig_ObjIsCo(pObj) )
118  bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
119  else
120  bBdd0 = (DdNode *)pObj->pData;
121  bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
122  bXor = Cudd_bddXor( p->dd, bBdd0, bBdd1 ); Cudd_Ref( bXor );
123 // bRes = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget );
124  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) );
125  if ( bRes == NULL )
126  {
127  Cudd_RecursiveDeref( p->dd, bTemp );
128  Cudd_RecursiveDeref( p->dd, bXor );
129  Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
130  if ( pObj->pData )
131  Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
132  return NULL;
133  }
134  Cudd_Ref( bRes );
135  Cudd_RecursiveDeref( p->dd, bTemp );
136  Cudd_RecursiveDeref( p->dd, bXor );
137  }
138  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
139  Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
140  Cudd_Deref( bRes );
141  return bRes;
142 }
143 
144 /**Function*************************************************************
145 
146  Synopsis [Derives quantification cube.]
147 
148  Description []
149 
150  SideEffects []
151 
152  SeeAlso []
153 
154 ***********************************************************************/
155 DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace, int fBackward )
156 {
157  Aig_Obj_t * pObj;
158  DdNode * bRes, * bTemp, * bVar;
159  int i, iGroupFirst, iGroupLast;
160  abctime TimeStop;
161  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
162  bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
163  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
164  {
165  if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
166  continue;
167  iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
168  iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
169  assert( iGroupFirst <= iGroupLast );
170  if ( iGroupFirst < iGroupLast )
171  continue;
172  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
173  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
174  Cudd_RecursiveDeref( p->dd, bTemp );
175  }
176  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
177  {
178  if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
179  continue;
180  iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
181  iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
182  assert( iGroupFirst <= iGroupLast );
183  if ( iGroupFirst < iGroupLast )
184  continue;
185  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
186  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
187  Cudd_RecursiveDeref( p->dd, bTemp );
188  }
189  Cudd_Deref( bRes );
190  p->dd->TimeStop = TimeStop;
191  return bRes;
192 }
193 
194 /**Function*************************************************************
195 
196  Synopsis [Derives quantification cube.]
197 
198  Description []
199 
200  SideEffects []
201 
202  SeeAlso []
203 
204 ***********************************************************************/
205 DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
206 {
207  Aig_Obj_t * pObj;
208  DdNode * bRes, * bTemp, * bVar;
209  int i, iGroupLast;
210  abctime TimeStop;
211  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
212  bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
213  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
214  {
215  iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
216  assert( iGroupLast >= iGrpPlace );
217  if ( iGroupLast > iGrpPlace )
218  continue;
219  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
220  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
221  Cudd_RecursiveDeref( p->dd, bTemp );
222  }
223  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
224  {
225  iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
226  assert( iGroupLast >= iGrpPlace );
227  if ( iGroupLast > iGrpPlace )
228  continue;
229  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
230  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
231  Cudd_RecursiveDeref( p->dd, bTemp );
232  }
233  Cudd_Deref( bRes );
234  p->dd->TimeStop = TimeStop;
235  return bRes;
236 }
237 
238 /**Function*************************************************************
239 
240  Synopsis [Derives quantification cube.]
241 
242  Description []
243 
244  SideEffects []
245 
246  SeeAlso []
247 
248 ***********************************************************************/
249 DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
250 {
251  Aig_Obj_t * pObj;
252  DdNode * bRes, * bTemp, * bVar;
253  int i, iGroupFirst;
254  abctime TimeStop;
255  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
256  bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
257  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
258  {
259  if ( Saig_ObjIsPi(p->pAig, pObj) )
260  continue;
261  iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
262  assert( iGroupFirst <= iGrpPlace );
263  if ( iGroupFirst < iGrpPlace )
264  continue;
265  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
266  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
267  Cudd_RecursiveDeref( p->dd, bTemp );
268  }
269  Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
270  {
271  if ( Saig_ObjIsPi(p->pAig, pObj) )
272  continue;
273  iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
274  assert( iGroupFirst <= iGrpPlace );
275  if ( iGroupFirst < iGrpPlace )
276  continue;
277  bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
278  bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
279  Cudd_RecursiveDeref( p->dd, bTemp );
280  }
281  Cudd_Deref( bRes );
282  p->dd->TimeStop = TimeStop;
283  return bRes;
284 }
285 
286 /**Function*************************************************************
287 
288  Synopsis []
289 
290  Description []
291 
292  SideEffects []
293 
294  SeeAlso []
295 
296 ***********************************************************************/
297 DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
298 {
299  Aig_Obj_t * pObj;
300  DdNode * bRes, * bVar, * bTemp;
301  int i, iVar;
302  abctime TimeStop;
303  TimeStop = dd->TimeStop; dd->TimeStop = 0;
304  bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
305  Saig_ManForEachLo( p->pAig, pObj, i )
306  {
307  iVar = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj));
308  bVar = Cudd_bddIthVar( dd, iVar );
309  bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
310  Cudd_RecursiveDeref( dd, bTemp );
311  }
312  Cudd_Deref( bRes );
313  dd->TimeStop = TimeStop;
314  return bRes;
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis []
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit, int fBackward )
329 {
330  int fCheckSupport = 0;
331  Llb_Grp_t * pGroup;
332  DdNode * bImage, * bGroup, * bCube, * bTemp;
333  int k, Index;
334  bImage = bInit; Cudd_Ref( bImage );
335  for ( k = 1; k < p->pMatrix->nCols-1; k++ )
336  {
337  if ( fBackward )
338  Index = p->pMatrix->nCols - 1 - k;
339  else
340  Index = k;
341 
342  // compute group BDD
343  pGroup = p->pMatrix->pColGrps[Index];
344  bGroup = Llb_ManConstructGroupBdd( p, pGroup );
345  if ( bGroup == NULL )
346  {
347  Cudd_RecursiveDeref( p->dd, bImage );
348  return NULL;
349  }
350  Cudd_Ref( bGroup );
351  // quantify variables appearing only in this group
352  bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, Index, fBackward ); Cudd_Ref( bCube );
353  bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );
354  if ( bGroup == NULL )
355  {
356  Cudd_RecursiveDeref( p->dd, bTemp );
357  Cudd_RecursiveDeref( p->dd, bCube );
358  return NULL;
359  }
360  Cudd_Ref( bGroup );
361  Cudd_RecursiveDeref( p->dd, bTemp );
362  Cudd_RecursiveDeref( p->dd, bCube );
363  // perform partial product
364  if ( fBackward )
365  bCube = Llb_ManConstructQuantCubeBwd( p, pGroup, Index );
366  else
367  bCube = Llb_ManConstructQuantCubeFwd( p, pGroup, Index );
368  Cudd_Ref( bCube );
369 // bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );
370  bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );
371  if ( bImage == NULL )
372  {
373  Cudd_RecursiveDeref( p->dd, bTemp );
374  Cudd_RecursiveDeref( p->dd, bGroup );
375  Cudd_RecursiveDeref( p->dd, bCube );
376  return NULL;
377  }
378  Cudd_Ref( bImage );
379  Cudd_RecursiveDeref( p->dd, bTemp );
380  Cudd_RecursiveDeref( p->dd, bGroup );
381  Cudd_RecursiveDeref( p->dd, bCube );
382  }
383 
384  // make sure image depends on next state vars
385  if ( fCheckSupport )
386  {
387  bCube = Cudd_Support( p->dd, bImage ); Cudd_Ref( bCube );
388  for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) )
389  {
390  int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index );
391  Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId );
392  if ( !Saig_ObjIsLi(p->pAig, pObj) )
393  printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId );
394  }
395  Cudd_RecursiveDeref( p->dd, bCube );
396  }
397  Cudd_Deref( bImage );
398  return bImage;
399 }
400 
401 /**Function*************************************************************
402 
403  Synopsis []
404 
405  Description []
406 
407  SideEffects []
408 
409  SeeAlso []
410 
411 ***********************************************************************/
412 DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars )
413 {
414  DdNode * bConstr, * bFunc, * bTemp;
415  Aig_Obj_t * pObj;
416  int i, Entry;
417  abctime TimeStop;
418  if ( vHints == NULL )
419  return Cudd_ReadOne( p->dd );
420  TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
421  assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) );
422  // assign const and PI nodes to the original AIG
423  Aig_ManCleanData( p->pAig );
424  Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
425  Saig_ManForEachPi( p->pAig, pObj, i )
426  pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
427  Saig_ManForEachLo( p->pAig, pObj, i )
428  {
429  if ( fUseNsVars )
430  Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) );
431  else
432  Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) );
433  pObj->pData = Cudd_bddIthVar( p->dd, Entry );
434  }
435  // transfer them to the global AIG
436  Aig_ManCleanData( p->pAigGlo );
437  Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
438  Aig_ManForEachCi( p->pAigGlo, pObj, i )
439  pObj->pData = Aig_ManCi(p->pAig, i)->pData;
440  // derive consraints
441  bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr );
442  Vec_IntForEachEntry( vHints, Entry, i )
443  {
444  if ( Entry != 0 && Entry != 1 )
445  continue;
446  bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd ); Cudd_Ref( bFunc );
447  bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint
448  // make the product
449  bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc ); Cudd_Ref( bConstr );
450  Cudd_RecursiveDeref( p->dd, bTemp );
451  Cudd_RecursiveDeref( p->dd, bFunc );
452  }
453  Cudd_Deref( bConstr );
454  p->dd->TimeStop = TimeStop;
455  return bConstr;
456 }
457 
458 /**Function*************************************************************
459 
460  Synopsis [Perform reachability with hints and returns reached states in ppGlo.]
461 
462  Description []
463 
464  SideEffects []
465 
466  SeeAlso []
467 
468 ***********************************************************************/
469 Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p )
470 {
471  Abc_Cex_t * pCex;
472  Aig_Obj_t * pObj;
473  DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
474  int i, v, RetValue, nPiOffset;
475  char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
476  assert( Vec_PtrSize(p->vRings) > 0 );
477 
478  p->dd->TimeStop = 0;
479  p->ddR->TimeStop = 0;
480 
481 /*
482  Saig_ManForEachLo( p->pAig, pObj, i )
483  printf( "%d ", pObj->Id );
484  printf( "\n" );
485  Saig_ManForEachLi( p->pAig, pObj, i )
486  printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
487  printf( "\n" );
488 */
489  // allocate room for the counter-example
490  pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
491  pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
492  pCex->iPo = -1;
493 
494  // get the last cube
495  bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
496  RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
497  Cudd_RecursiveDeref( p->ddR, bOneCube );
498  assert( RetValue );
499 
500  // write PIs of counter-example
501  nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
502  Saig_ManForEachPi( p->pAig, pObj, i )
503  if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
504  Abc_InfoSetBit( pCex->pData, nPiOffset + i );
505 
506  // write state in terms of NS variables
507  if ( Vec_PtrSize(p->vRings) > 1 )
508  {
509  bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
510  }
511  // perform backward analysis
512  Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
513  {
514  if ( v == Vec_PtrSize(p->vRings) - 1 )
515  continue;
516 //Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
517 //Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
518  // compute the next states
519  bImage = Llb_ManComputeImage( p, bState, 1 );
520  assert( bImage != NULL );
521  Cudd_Ref( bImage );
522  Cudd_RecursiveDeref( p->dd, bState );
523 //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
524 
525  // move reached states into ring manager
526  bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
527  Cudd_RecursiveDeref( p->dd, bTemp );
528 //Extra_bddPrintSupport( p->ddR, bImage ); printf( "\n" );
529 
530  // intersect with the previous set
531  bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
532  Cudd_RecursiveDeref( p->ddR, bImage );
533 
534  // find any assignment of the BDD
535  RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
536  Cudd_RecursiveDeref( p->ddR, bOneCube );
537  assert( RetValue );
538 /*
539  for ( i = 0; i < p->ddR->size; i++ )
540  printf( "%d ", pValues[i] );
541  printf( "\n" );
542 */
543  // write PIs of counter-example
544  nPiOffset -= Saig_ManPiNum(p->pAig);
545  Saig_ManForEachPi( p->pAig, pObj, i )
546  if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
547  Abc_InfoSetBit( pCex->pData, nPiOffset + i );
548 
549  // check that we get the init state
550  if ( v == 0 )
551  {
552  Saig_ManForEachLo( p->pAig, pObj, i )
553  assert( pValues[i] == 0 );
554  break;
555  }
556 
557  // write state in terms of NS variables
558  bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
559  }
560  assert( nPiOffset == Saig_ManRegNum(p->pAig) );
561  // update the output number
562 //Abc_CexPrint( pCex );
563  RetValue = Saig_ManFindFailedPoCex( p->pAigGlo, pCex );
564  assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAigGlo) ); // invalid CEX!!!
565  pCex->iPo = RetValue;
566  // cleanup
567  ABC_FREE( pValues );
568  return pCex;
569 }
570 
571 /**Function*************************************************************
572 
573  Synopsis [Perform reachability with hints and returns reached states in ppGlo.]
574 
575  Description []
576 
577  SideEffects []
578 
579  SeeAlso []
580 
581 ***********************************************************************/
582 int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
583 {
584  int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
585  int * pCs2Glo = Vec_IntArray( p->vCs2Glo );
586  int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
587  DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
588  DdNode * bConstrCs, * bConstrNs;
589  abctime clk2, clk = Abc_Clock();
590  int nIters, nBddSize = 0;
591 // int nThreshold = 10000;
592 
593  // compute time to stop
594  p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
595 
596  // define variable limits
597  Llb_ManPrepareVarLimits( p );
598 
599  // start the managers
600  assert( p->dd == NULL );
601  assert( p->ddG == NULL );
602  assert( p->ddR == NULL );
603  p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
604  p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
605  if ( pddGlo && *pddGlo )
606  p->ddG = *pddGlo, *pddGlo = NULL;
607  else
608  p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
609 
610  if ( p->pPars->fReorder )
611  {
612  Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
613  Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
614  Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
615  }
616  else
617  {
618  Cudd_AutodynDisable( p->dd );
619  Cudd_AutodynDisable( p->ddG );
620  Cudd_AutodynDisable( p->ddR );
621  }
622 
623  // set the stop time parameter
624  p->dd->TimeStop = p->pPars->TimeTarget;
625  p->ddG->TimeStop = p->pPars->TimeTarget;
626  p->ddR->TimeStop = p->pPars->TimeTarget;
627 
628  // create bad state in the ring manager
629  p->ddR->bFunc = Llb_BddComputeBad( p->pAigGlo, p->ddR, p->pPars->TimeTarget );
630  if ( p->ddR->bFunc == NULL )
631  {
632  if ( !p->pPars->fSilent )
633  printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
634  p->pPars->iFrame = -1;
635  return -1;
636  }
637  Cudd_Ref( p->ddR->bFunc );
638 
639  // derive constraints
640  bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 ); Cudd_Ref( bConstrCs );
641  bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 ); Cudd_Ref( bConstrNs );
642 //Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" );
643 //Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" );
644 
645  // perform reachability analysis
646  // compute the starting set of states
647  if ( p->ddG->bFunc )
648  {
649  bReached = p->ddG->bFunc; p->ddG->bFunc = NULL;
650  bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs ); Cudd_Ref( bCurrent );
651  }
652  else
653  {
654  bReached = Llb_ManComputeInitState( p, p->ddG ); Cudd_Ref( bReached );
655  bCurrent = Llb_ManComputeInitState( p, p->dd ); Cudd_Ref( bCurrent );
656  }
657 //Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" );
658 //Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
659 
660 //Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
661  for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
662  {
663  clk2 = Abc_Clock();
664  // check the runtime limit
665  if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
666  {
667  if ( !p->pPars->fSilent )
668  printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
669  p->pPars->iFrame = nIters - 1;
670  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
671  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
672  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
673  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
674  return -1;
675  }
676 
677  // save the onion ring
678  bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo );
679  if ( bTemp == NULL )
680  {
681  if ( !p->pPars->fSilent )
682  printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
683  p->pPars->iFrame = nIters - 1;
684  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
685  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
686  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
687  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
688  return -1;
689  }
690  Cudd_Ref( bTemp );
691  Vec_PtrPush( p->vRings, bTemp );
692 
693  // check it for bad states
694  if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
695  {
696  assert( p->pAigGlo->pSeqModel == NULL );
697  if ( !p->pPars->fBackward )
698  p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p );
699  if ( !p->pPars->fSilent )
700  {
701  if ( !p->pPars->fBackward )
702  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters );
703  else
704  Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters );
705  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
706  }
707  p->pPars->iFrame = nIters - 1;
708  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
709  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
710  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
711  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
712  return 0;
713  }
714 
715  // restrict reachable states using constraints
716  if ( vHints )
717  {
718  bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent );
719  Cudd_RecursiveDeref( p->dd, bTemp );
720  }
721 
722  // quantify variables appearing only in the init state
723  bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 ); Cudd_Ref( bCube );
724  bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent );
725  Cudd_RecursiveDeref( p->dd, bTemp );
726  Cudd_RecursiveDeref( p->dd, bCube );
727 
728  // compute the next states
729  bNext = Llb_ManComputeImage( p, bCurrent, 0 );
730  if ( bNext == NULL )
731  {
732  if ( !p->pPars->fSilent )
733  printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
734  p->pPars->iFrame = nIters - 1;
735  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
736  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
737  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
738  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
739  return -1;
740  }
741  Cudd_Ref( bNext );
742  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
743 
744  // restrict reachable states using constraints
745  if ( vHints )
746  {
747  bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs ); Cudd_Ref( bNext );
748  Cudd_RecursiveDeref( p->dd, bTemp );
749  }
750 //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
751 
752  // remap these states into the current state vars
753 // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); Cudd_Ref( bNext );
754 // Cudd_RecursiveDeref( p->dd, bTemp );
755 // bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );
756  bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );
757  if ( bNext == NULL )
758  {
759  if ( !p->pPars->fSilent )
760  printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
761  p->pPars->iFrame = nIters - 1;
762  Cudd_RecursiveDeref( p->dd, bTemp );
763  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
764  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
765  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
766  return -1;
767  }
768  Cudd_Ref( bNext );
769  Cudd_RecursiveDeref( p->dd, bTemp );
770 
771 
772  // check if there are any new states
773  if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
774  {
775  Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
776  break;
777  }
778 
779  // check the BDD size
780  nBddSize = Cudd_DagSize(bNext);
781  if ( nBddSize > p->pPars->nBddMax )
782  {
783  Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
784  break;
785  }
786 
787  // get the new states
788  bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
789  if ( bCurrent == NULL )
790  {
791  Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
792  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
793  break;
794  }
795  Cudd_Ref( bCurrent );
796  // minimize the new states with the reached states
797 // bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
798 // bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
799 // Cudd_RecursiveDeref( p->ddG, bTemp );
800 //printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) );
801 
802  // remap these states into the current state vars
803 // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); Cudd_Ref( bCurrent );
804 // Cudd_RecursiveDeref( p->ddG, bTemp );
805 // bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );
806  bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );
807  if ( bCurrent == NULL )
808  {
809  if ( !p->pPars->fSilent )
810  printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
811  p->pPars->iFrame = nIters - 1;
812  Cudd_RecursiveDeref( p->ddG, bTemp );
813  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
814  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
815  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
816  return -1;
817  }
818  Cudd_Ref( bCurrent );
819  Cudd_RecursiveDeref( p->ddG, bTemp );
820 
821 
822  // add to the reached states
823  bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );
824  if ( bReached == NULL )
825  {
826  Cudd_RecursiveDeref( p->ddG, bTemp ); bTemp = NULL;
827  Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
828  break;
829  }
830  Cudd_Ref( bReached );
831  Cudd_RecursiveDeref( p->ddG, bTemp );
832  Cudd_RecursiveDeref( p->ddG, bNext );
833  bNext = NULL;
834 
835  if ( p->pPars->fVerbose )
836  {
837  fprintf( stdout, "F =%5d : ", nIters );
838  fprintf( stdout, "Im =%6d ", nBddSize );
839  fprintf( stdout, "(%4d %3d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
840  fprintf( stdout, "Rea =%6d ", Cudd_DagSize(bReached) );
841  fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
842  Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
843  }
844 /*
845  if ( p->pPars->fVerbose )
846  {
847  double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
848 // Extra_bddPrint( p->ddG, bReached );printf( "\n" );
849  fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
850  fflush( stdout );
851  }
852 */
853  }
854  Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
855  Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
856  if ( bReached == NULL )
857  {
858  p->pPars->iFrame = nIters - 1;
859  return 0; // reachable
860  }
861 // assert( bCurrent == NULL );
862  if ( bCurrent )
863  Cudd_RecursiveDeref( p->dd, bCurrent );
864  // report the stats
865  if ( p->pPars->fVerbose )
866  {
867  double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
868  if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
869  fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
870  else
871  fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
872  fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
873  fflush( stdout );
874  }
875  if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
876  {
877  if ( !p->pPars->fSilent )
878  printf( "Verified only for states reachable in %d frames. ", nIters );
879  p->pPars->iFrame = p->pPars->nIterMax;
880  Cudd_RecursiveDeref( p->ddG, bReached );
881  return -1; // undecided
882  }
883  if ( pddGlo )
884  {
885  assert( p->ddG->bFunc == NULL );
886  p->ddG->bFunc = bReached; bReached = NULL;
887  assert( *pddGlo == NULL );
888  *pddGlo = p->ddG; p->ddG = NULL;
889  }
890  else
891  Cudd_RecursiveDeref( p->ddG, bReached );
892  if ( !p->pPars->fSilent )
893  printf( "The miter is proved unreachable after %d iterations. ", nIters );
894  p->pPars->iFrame = nIters - 1;
895  return 1; // unreachable
896 }
897 
898 ////////////////////////////////////////////////////////////////////////
899 /// END OF FILE ///
900 ////////////////////////////////////////////////////////////////////////
901 
902 
903 ABC_NAMESPACE_IMPL_END
904 
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
DdManager::TimeStop
abctime TimeStop
Definition: cuddInt.h:489
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
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
Cudd_bddPickOneCube
int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string)
Definition: cuddUtil.c:1221
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_ReadReorderings
int Cudd_ReadReorderings(DdManager *dd)
Definition: cuddAPI.c:1696
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Llb_Grp_t_::vNodes
Vec_Ptr_t * vNodes
Definition: llbInt.h:99
Llb_ManReachDeriveCex
Abc_Cex_t * Llb_ManReachDeriveCex(Llb_Man_t *p)
Definition: llb1Reach.c:469
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Llb_BddComputeBad
ABC_NAMESPACE_IMPL_START DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition: llb2Bad.c:45
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
Llb_ManReachability
int Llb_ManReachability(Llb_Man_t *p, Vec_Int_t *vHints, DdManager **pddGlo)
Definition: llb1Reach.c:582
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Llb_ManComputeInitState
DdNode * Llb_ManComputeInitState(Llb_Man_t *p, DdManager *dd)
Definition: llb1Reach.c:297
Llb_ManPrepareVarLimits
void Llb_ManPrepareVarLimits(Llb_Man_t *p)
Definition: llb1Man.c:88
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Aig_ManDfsNodes
Vec_Ptr_t * Aig_ManDfsNodes(Aig_Man_t *p, Aig_Obj_t **ppNodes, int nNodes)
Definition: aigDfs.c:333
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Llb_CoreComputeCube
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition: llb2Core.c:68
Aig_Obj_t_
Definition: aig.h:69
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Llb_ManConstructGroupBdd
DdNode * Llb_ManConstructGroupBdd(Llb_Man_t *p, Llb_Grp_t *pGroup)
Definition: llb1Reach.c:91
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Llb_ManConstructQuantCubeFwd
DdNode * Llb_ManConstructQuantCubeFwd(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace)
Definition: llb1Reach.c:205
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Llb_ManConstructOutBdd
ABC_NAMESPACE_IMPL_START DdNode * Llb_ManConstructOutBdd(Aig_Man_t *pAig, Aig_Obj_t *pNode, DdManager *dd)
DECLARATIONS ///.
Definition: llb1Reach.c:45
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
Llb_ManConstructQuantCubeIntern
DdNode * Llb_ManConstructQuantCubeIntern(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace, int fBackward)
Definition: llb1Reach.c:155
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Llb_ManConstructQuantCubeBwd
DdNode * Llb_ManConstructQuantCubeBwd(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace)
Definition: llb1Reach.c:249
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition: vecPtr.h:59
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Llb_ManCreateConstraints
DdNode * Llb_ManCreateConstraints(Llb_Man_t *p, Vec_Int_t *vHints, int fUseNsVars)
Definition: llb1Reach.c:412
assert
#define assert(ex)
Definition: util_old.h:213
Llb_ManComputeImage
DdNode * Llb_ManComputeImage(Llb_Man_t *p, DdNode *bInit, int fBackward)
Definition: llb1Reach.c:328
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Llb_Grp_t_
Definition: llbInt.h:94
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Cudd_bddIntersect
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:282
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Llb_Man_t
typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t
INCLUDES ///.
Definition: llbInt.h:46
Cudd_ReadGarbageCollections
int Cudd_ReadGarbageCollections(DdManager *dd)
Definition: cuddAPI.c:1741
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Llb_Grp_t_::vOuts
Vec_Ptr_t * vOuts
Definition: llbInt.h:98
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:434
Llb_Grp_t_::vIns
Vec_Ptr_t * vIns
Definition: llbInt.h:97
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91