abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb4Nonlin.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb2Nonlin.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Non-linear quantification scheduling.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb2Nonlin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.h"
22 #include "base/abc/abc.h"
23 #include "aig/gia/giaAig.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Llb_Mnx_t_ Llb_Mnx_t;
33 struct Llb_Mnx_t_
34 {
35  // user info
36  Aig_Man_t * pAig; // AIG manager
37  Gia_ParLlb_t * pPars; // parameters
38 
39  // intermediate BDDs
40  DdManager * dd; // BDD manager
41  DdNode * bBad; // bad states in terms of CIs
42  DdNode * bReached; // reached states
43  DdNode * bCurrent; // from states
44  DdNode * bNext; // to states
45  Vec_Ptr_t * vRings; // onion rings in ddR
46  Vec_Ptr_t * vRoots; // BDDs for partitions
47 
48  // structural info
49  Vec_Int_t * vOrder; // for each object ID, its BDD variable number or -1
50  Vec_Int_t * vVars2Q; // 1 if variable is quantifiable; 0 othervise
51 
52  abctime timeImage;
53  abctime timeRemap;
54  abctime timeReo;
55  abctime timeOther;
56  abctime timeTotal;
57 };
58 
59 //extern int timeBuild, timeAndEx, timeOther;
60 //extern int nSuppMax;
61 
62 ////////////////////////////////////////////////////////////////////////
63 /// FUNCTION DEFINITIONS ///
64 ////////////////////////////////////////////////////////////////////////
65 
66 /**Function*************************************************************
67 
68  Synopsis [Computes bad in working manager.]
69 
70  Description []
71 
72  SideEffects []
73 
74  SeeAlso []
75 
76 ***********************************************************************/
77 DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
78 {
79  Vec_Ptr_t * vNodes;
80  DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult, * bCube;
81  Aig_Obj_t * pObj;
82  int i;
83  Aig_ManCleanData( pAig );
84  // assign elementary variables
85  Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
86  Aig_ManForEachCi( pAig, pObj, i )
87  pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
88  // compute internal nodes
89  vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), Saig_ManPoNum(pAig) );
90  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
91  {
92  if ( !Aig_ObjIsNode(pObj) )
93  continue;
94  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
95  bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
96  bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
97  if ( bBdd == NULL )
98  {
99  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
100  if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
101  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
102  Vec_PtrFree( vNodes );
103  return NULL;
104  }
105  Cudd_Ref( bBdd );
106  pObj->pData = bBdd;
107  }
108  // quantify PIs of each PO
109  bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult );
110  Saig_ManForEachPo( pAig, pObj, i )
111  {
112  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
113  bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 );
114  if ( bResult == NULL )
115  {
116  Cudd_RecursiveDeref( dd, bTemp );
117  break;
118  }
119  Cudd_Ref( bResult );
120  Cudd_RecursiveDeref( dd, bTemp );
121  }
122  // deref
123  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
124  if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
125  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
126  Vec_PtrFree( vNodes );
127  if ( bResult )
128  {
129  bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
130  Saig_ManForEachPi( pAig, pObj, i )
131  {
132  bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData );
133  if ( bCube == NULL )
134  {
135  Cudd_RecursiveDeref( dd, bTemp );
136  Cudd_RecursiveDeref( dd, bResult );
137  bResult = NULL;
138  break;
139  }
140  Cudd_Ref( bCube );
141  Cudd_RecursiveDeref( dd, bTemp );
142  }
143  if ( bResult != NULL )
144  {
145  bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube ); Cudd_Ref( bResult );
146  Cudd_RecursiveDeref( dd, bTemp );
147  Cudd_RecursiveDeref( dd, bCube );
148  Cudd_Deref( bResult );
149  }
150  }
151 //if ( bResult )
152 //printf( "Bad state = %d.\n", Cudd_DagSize(bResult) );
153  return bResult;
154 }
155 
156 /**Function*************************************************************
157 
158  Synopsis [Derives BDDs for the partitions.]
159 
160  Description []
161 
162  SideEffects []
163 
164  SeeAlso []
165 
166 ***********************************************************************/
167 Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
168 {
169  Vec_Ptr_t * vRoots;
170  Aig_Obj_t * pObj;
171  DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
172  int i;
173  Aig_ManCleanData( pAig );
174  // assign elementary variables
175  Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
176  Aig_ManForEachCi( pAig, pObj, i )
177  pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
178  Aig_ManForEachNode( pAig, pObj, i )
179  if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
180  {
181  pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
182  Cudd_Ref( (DdNode *)pObj->pData );
183  }
184  Saig_ManForEachLi( pAig, pObj, i )
185  pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
186  // compute intermediate BDDs
187  vRoots = Vec_PtrAlloc( 100 );
188  Aig_ManForEachNode( pAig, pObj, i )
189  {
190  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
191  bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
192  bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
193  if ( bBdd == NULL )
194  goto finish;
195  Cudd_Ref( bBdd );
196  if ( pObj->pData == NULL )
197  {
198  pObj->pData = bBdd;
199  continue;
200  }
201  // create new partition
202  bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );
203  if ( bPart == NULL )
204  goto finish;
205  Cudd_Ref( bPart );
206  Cudd_RecursiveDeref( dd, bBdd );
207  Vec_PtrPush( vRoots, bPart );
208 //printf( "%d ", Cudd_DagSize(bPart) );
209  }
210  // compute register output BDDs
211  Saig_ManForEachLi( pAig, pObj, i )
212  {
213  bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
214  bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );
215  if ( bPart == NULL )
216  goto finish;
217  Cudd_Ref( bPart );
218  Vec_PtrPush( vRoots, bPart );
219 //printf( "%d ", Cudd_DagSize(bPart) );
220  }
221 //printf( "\n" );
222  Aig_ManForEachNode( pAig, pObj, i )
223  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
224  return vRoots;
225  // early termination
226 finish:
227  Aig_ManForEachNode( pAig, pObj, i )
228  if ( pObj->pData )
229  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
230  Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
231  Cudd_RecursiveDeref( dd, bPart );
232  Vec_PtrFree( vRoots );
233  return NULL;
234 }
235 
236 /**Function*************************************************************
237 
238  Synopsis [Find simple variable ordering.]
239 
240  Description []
241 
242  SideEffects []
243 
244  SeeAlso []
245 
246 ***********************************************************************/
247 Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
248 {
249  Vec_Int_t * vOrder;
250  Aig_Obj_t * pObj;
251  int i, Counter = 0;
252  vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
253  Aig_ManForEachCi( pAig, pObj, i )
254  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
255  Saig_ManForEachLi( pAig, pObj, i )
256  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
257  return vOrder;
258 }
259 
260 /**Function*************************************************************
261 
262  Synopsis [Find good static variable ordering.]
263 
264  Description []
265 
266  SideEffects []
267 
268  SeeAlso []
269 
270 ***********************************************************************/
271 void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
272 {
273  Aig_Obj_t * pFanin0, * pFanin1;
274  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
275  return;
276  Aig_ObjSetTravIdCurrent( pAig, pObj );
277  assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
278  if ( Aig_ObjIsCi(pObj) )
279  {
280 // if ( Saig_ObjIsLo(pAig, pObj) )
281 // Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
282  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
283  return;
284  }
285  // try fanins with higher level first
286  pFanin0 = Aig_ObjFanin0(pObj);
287  pFanin1 = Aig_ObjFanin1(pObj);
288 // if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
289  if ( pFanin0->Level > pFanin1->Level )
290  {
291  Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
292  Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
293  }
294  else
295  {
296  Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
297  Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
298  }
299  if ( pObj->fMarkA )
300  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
301 }
302 
303 /**Function*************************************************************
304 
305  Synopsis [Collect nodes with the given fanout count.]
306 
307  Description []
308 
309  SideEffects []
310 
311  SeeAlso []
312 
313 ***********************************************************************/
314 Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
315 {
316  Vec_Int_t * vNodes;
317  Aig_Obj_t * pObj;
318  int i;
319  Aig_ManCleanMarkA( pAig );
320  Aig_ManForEachNode( pAig, pObj, i )
321  if ( Aig_ObjRefs(pObj) >= nFans )
322  pObj->fMarkA = 1;
323  // unmark flop drivers
324  Saig_ManForEachLi( pAig, pObj, i )
325  Aig_ObjFanin0(pObj)->fMarkA = 0;
326  // collect mapping
327  vNodes = Vec_IntAlloc( 100 );
328  Aig_ManForEachNode( pAig, pObj, i )
329  if ( pObj->fMarkA )
330  Vec_IntPush( vNodes, Aig_ObjId(pObj) );
331  Aig_ManCleanMarkA( pAig );
332  return vNodes;
333 }
334 
335 /**Function*************************************************************
336 
337  Synopsis [Find good static variable ordering.]
338 
339  Description []
340 
341  SideEffects []
342 
343  SeeAlso []
344 
345 ***********************************************************************/
346 Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
347 {
348  Vec_Int_t * vNodes = NULL;
349  Vec_Int_t * vOrder;
350  Aig_Obj_t * pObj;
351  int i, Counter = 0;
352 /*
353  // mark internal nodes to be used
354  Aig_ManCleanMarkA( pAig );
355  vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
356  Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
357  pObj->fMarkA = 1;
358 printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
359 */
360  // collect nodes in the order
361  vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
362  Aig_ManIncrementTravId( pAig );
363  Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
364  Saig_ManForEachLi( pAig, pObj, i )
365  {
366  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
367  Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
368  }
369  Aig_ManForEachCi( pAig, pObj, i )
370  if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
371  {
372 // if ( Saig_ObjIsLo(pAig, pObj) )
373 // Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
374  Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
375  }
376  assert( Counter <= Aig_ManCiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
377  Aig_ManCleanMarkA( pAig );
378  Vec_IntFreeP( &vNodes );
379  return vOrder;
380 }
381 
382 
383 /**Function*************************************************************
384 
385  Synopsis [Creates quantifiable varaibles for both types of traversal.]
386 
387  Description []
388 
389  SideEffects []
390 
391  SeeAlso []
392 
393 ***********************************************************************/
394 Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fBackward )
395 {
396  Vec_Int_t * vVars2Q;
397  Aig_Obj_t * pObjLi, * pObjLo;
398  int i;
399  vVars2Q = Vec_IntAlloc( 0 );
400  Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
401  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
402  Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, fBackward ? pObjLo : pObjLi), 0 );
403  return vVars2Q;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Compute initial state in terms of current state variables.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
418 {
419  DdNode ** pVarsX, ** pVarsY;
420  Aig_Obj_t * pObjLo, * pObjLi;
421  int i;
422  pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
423  pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
424  Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
425  {
426  assert( Llb_ObjBddVar(vOrder, pObjLo) >= 0 );
427  assert( Llb_ObjBddVar(vOrder, pObjLi) >= 0 );
428  pVarsX[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLo) );
429  pVarsY[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) );
430  }
431  Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) );
432  ABC_FREE( pVarsX );
433  ABC_FREE( pVarsY );
434 }
435 
436 /**Function*************************************************************
437 
438  Synopsis [Compute initial state in terms of current state variables.]
439 
440  Description []
441 
442  SideEffects []
443 
444  SeeAlso []
445 
446 ***********************************************************************/
447 DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fBackward )
448 {
449  Aig_Obj_t * pObjLi, * pObjLo;
450  DdNode * bRes, * bVar, * bTemp;
451  int i;
452  abctime TimeStop;
453  TimeStop = dd->TimeStop; dd->TimeStop = 0;
454  bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
455  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
456  {
457  bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo) );
458  bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
459  Cudd_RecursiveDeref( dd, bTemp );
460  }
461  Cudd_Deref( bRes );
462  dd->TimeStop = TimeStop;
463  return bRes;
464 }
465 
466 /**Function*************************************************************
467 
468  Synopsis [Compute initial state in terms of current state variables.]
469 
470  Description []
471 
472  SideEffects []
473 
474  SeeAlso []
475 
476 ***********************************************************************/
477 DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues, int Flag )
478 {
479  Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp;
480  DdNode * bRes, * bVar, * bTemp;
481  int i;
482  abctime TimeStop;
483  TimeStop = dd->TimeStop; dd->TimeStop = 0;
484  bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
485  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
486  {
487  if ( Flag )
488  pObjTemp = pObjLo, pObjLo = pObjLi, pObjLi = pObjTemp;
489  // get the correspoding flop input variable
490  bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) );
491  if ( pValues[Llb_ObjBddVar(vOrder, pObjLo)] != 1 )
492  bVar = Cudd_Not(bVar);
493  // create cube
494  bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
495  Cudd_RecursiveDeref( dd, bTemp );
496  }
497  Cudd_Deref( bRes );
498  dd->TimeStop = TimeStop;
499  return bRes;
500 }
501 
502 /**Function*************************************************************
503 
504  Synopsis [Compute initial state in terms of current state variables.]
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 void Llb_Nonlin4RecordState( Aig_Man_t * pAig, Vec_Int_t * vOrder, unsigned * pState, char * pValues, int fBackward )
514 {
515  Aig_Obj_t * pObjLo, * pObjLi;
516  int i;
517  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
518  if ( pValues[Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo)] == 1 )
519  Abc_InfoSetBit( pState, i );
520 }
521 
522 /**Function*************************************************************
523 
524  Synopsis [Multiply every partition by the cube.]
525 
526  Description []
527 
528  SideEffects []
529 
530  SeeAlso []
531 
532 ***********************************************************************/
533 Vec_Ptr_t * Llb_Nonlin4Multiply( DdManager * dd, DdNode * bCube, Vec_Ptr_t * vParts )
534 {
535  Vec_Ptr_t * vNew;
536  DdNode * bTemp, * bFunc;
537  int i;
538  vNew = Vec_PtrAlloc( Vec_PtrSize(vParts) );
539  Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
540  {
541  bTemp = Cudd_bddAnd( dd, bFunc, bCube ); Cudd_Ref( bTemp );
542  Vec_PtrPush( vNew, bTemp );
543  }
544  return vNew;
545 }
546 
547 /**Function*************************************************************
548 
549  Synopsis [Multiply every partition by the cube.]
550 
551  Description []
552 
553  SideEffects []
554 
555  SeeAlso []
556 
557 ***********************************************************************/
558 void Llb_Nonlin4Deref( DdManager * dd, Vec_Ptr_t * vParts )
559 {
560  DdNode * bFunc;
561  int i;
562  Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
563  Cudd_RecursiveDeref( dd, bFunc );
564  Vec_PtrFree( vParts );
565 }
566 
567 /**Function*************************************************************
568 
569  Synopsis [Derives counter-example by backward reachability.]
570 
571  Description []
572 
573  SideEffects []
574 
575  SeeAlso []
576 
577 ***********************************************************************/
578 Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose )
579 {
580  Vec_Int_t * vVars2Q;
581  Vec_Ptr_t * vStates, * vRootsNew;
582  Aig_Obj_t * pObj;
583  DdNode * bState = NULL, * bImage, * bOneCube, * bRing;
584  int i, v, RetValue;//, clk = Abc_Clock();
585  char * pValues;
586  assert( Vec_PtrSize(p->vRings) > 0 );
587  // disable the timeout
588  p->dd->TimeStop = 0;
589 
590  // start the state set
591  vStates = Vec_PtrAllocSimInfo( Vec_PtrSize(p->vRings), Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
592  Vec_PtrCleanSimInfo( vStates, 0, Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
593  if ( fBackward )
594  Vec_PtrReverseOrder( vStates );
595 
596  // get the last cube
597  pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
598  bOneCube = Cudd_bddIntersect( p->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad ); Cudd_Ref( bOneCube );
599  RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
600  Cudd_RecursiveDeref( p->dd, bOneCube );
601  assert( RetValue );
602 
603  // record the cube
604  Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntryLast(vStates), pValues, fBackward );
605 
606  // write state in terms of NS variables
607  if ( Vec_PtrSize(p->vRings) > 1 )
608  {
609  bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState );
610  }
611  // perform backward analysis
612  vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, !fBackward );
613  Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
614  {
615  if ( v == Vec_PtrSize(p->vRings) - 1 )
616  continue;
617 
618  // preprocess partitions
619  vRootsNew = Llb_Nonlin4Multiply( p->dd, bState, p->vRoots );
620  Cudd_RecursiveDeref( p->dd, bState );
621 
622  // compute the next states
623  bImage = Llb_Nonlin4Image( p->dd, vRootsNew, NULL, vVars2Q ); Cudd_Ref( bImage );
624  Llb_Nonlin4Deref( p->dd, vRootsNew );
625 
626  // intersect with the previous set
627  bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube );
628  Cudd_RecursiveDeref( p->dd, bImage );
629 
630  // find any assignment of the BDD
631  RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
632  Cudd_RecursiveDeref( p->dd, bOneCube );
633  assert( RetValue );
634 
635  // record the cube
636  Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntry(vStates, v), pValues, fBackward );
637 
638  // check that we get the init state
639  if ( v == 0 )
640  {
641  Saig_ManForEachLo( p->pAig, pObj, i )
642  assert( fBackward || pValues[Llb_ObjBddVar(p->vOrder, pObj)] == 0 );
643  break;
644  }
645 
646  // write state in terms of NS variables
647  bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState );
648  }
649  Vec_IntFree( vVars2Q );
650  ABC_FREE( pValues );
651  if ( fBackward )
652  Vec_PtrReverseOrder( vStates );
653 // if ( fVerbose )
654 // Abc_PrintTime( 1, "BDD-based cex generation time", Abc_Clock() - clk );
655  return vStates;
656 }
657 
658 
659 /**Function*************************************************************
660 
661  Synopsis [Perform reachability with hints.]
662 
663  Description []
664 
665  SideEffects []
666 
667  SeeAlso []
668 
669 ***********************************************************************/
670 int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
671 {
672  DdNode * bAux;
673  int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0;
674  abctime clkTemp, clkIter, clk = Abc_Clock();
675  assert( Aig_ManRegNum(p->pAig) > 0 );
676 
677  if ( p->pPars->fBackward )
678  {
679  // create bad state in the ring manager
680  if ( !p->pPars->fSkipOutCheck )
681  {
682  p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bBad );
683  }
684  // create init state
685  if ( p->pPars->fCluster )
686  p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL;
687  else
688  {
689  p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );
690  if ( p->bCurrent == NULL )
691  {
692  if ( !p->pPars->fSilent )
693  printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
694  p->pPars->iFrame = -1;
695  return -1;
696  }
697  Cudd_Ref( p->bCurrent );
698  }
699  // remap into the next states
700  p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent );
701  if ( p->bCurrent == NULL )
702  {
703  if ( !p->pPars->fSilent )
704  printf( "Reached timeout (%d seconds) during remapping bad states.\n", p->pPars->TimeLimit );
705  Cudd_RecursiveDeref( p->dd, bAux );
706  p->pPars->iFrame = -1;
707  return -1;
708  }
709  Cudd_Ref( p->bCurrent );
710  Cudd_RecursiveDeref( p->dd, bAux );
711  }
712  else
713  {
714  // create bad state in the ring manager
715  if ( !p->pPars->fSkipOutCheck )
716  {
717  if ( p->pPars->fCluster )
718  p->bBad = p->dd->bFunc, p->dd->bFunc = NULL;
719  else
720  {
721  p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );
722  if ( p->bBad == NULL )
723  {
724  if ( !p->pPars->fSilent )
725  printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
726  p->pPars->iFrame = -1;
727  return -1;
728  }
729  Cudd_Ref( p->bBad );
730  }
731  }
732  else if ( p->dd->bFunc )
733  Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL;
734  // compute the starting set of states
735  p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bCurrent );
736  }
737  // perform iterations
738  p->bReached = p->bCurrent; Cudd_Ref( p->bReached );
739  for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
740  {
741  clkIter = Abc_Clock();
742  // check the runtime limit
743  if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
744  {
745  if ( !p->pPars->fSilent )
746  printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
747  p->pPars->iFrame = nIters - 1;
748  return -1;
749  }
750 
751  // save the onion ring
752  Vec_PtrPush( p->vRings, p->bCurrent ); Cudd_Ref( p->bCurrent );
753 
754  // check it for bad states
755  if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) )
756  {
757  Vec_Ptr_t * vStates;
758  assert( p->pAig->pSeqModel == NULL );
759  vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose );
760  p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose );
761  Vec_PtrFreeP( &vStates );
762  if ( !p->pPars->fSilent )
763  {
764  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAig->pSeqModel->iPo, p->pAig->pName, nIters );
765  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
766  }
767  p->pPars->iFrame = nIters - 1;
768  return 0;
769  }
770 
771  // compute the next states
772  clkTemp = Abc_Clock();
773  p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q );
774  if ( p->bNext == NULL )
775  {
776  if ( !p->pPars->fSilent )
777  printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit );
778  p->pPars->iFrame = nIters - 1;
779  return -1;
780  }
781  Cudd_Ref( p->bNext );
782  p->timeImage += Abc_Clock() - clkTemp;
783 
784  // remap into current states
785  clkTemp = Abc_Clock();
786  p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext );
787  if ( p->bNext == NULL )
788  {
789  if ( !p->pPars->fSilent )
790  printf( "Reached timeout (%d seconds) during remapping next states.\n", p->pPars->TimeLimit );
791  Cudd_RecursiveDeref( p->dd, bAux );
792  p->pPars->iFrame = nIters - 1;
793  return -1;
794  }
795  Cudd_Ref( p->bNext );
796  Cudd_RecursiveDeref( p->dd, bAux );
797  p->timeRemap += Abc_Clock() - clkTemp;
798 
799  // collect statistics
800  if ( p->pPars->fVerbose )
801  {
802  nBddSizeFr = Cudd_DagSize( p->bCurrent );
803  nBddSizeTo = Cudd_DagSize( bAux );
804  nBddSizeTo2 = Cudd_DagSize( p->bNext );
805  }
806  Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL;
807 
808  // derive new states
809  p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) );
810  if ( p->bCurrent == NULL )
811  {
812  if ( !p->pPars->fSilent )
813  printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
814  p->pPars->iFrame = nIters - 1;
815  return -1;
816  }
817  Cudd_Ref( p->bCurrent );
818  Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
819  if ( Cudd_IsConstant(p->bCurrent) )
820  break;
821 /*
822  // reduce BDD size using constrain // Cudd_bddRestrict
823  p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );
824  Cudd_Ref( p->bCurrent );
825 printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
826  Cudd_RecursiveDeref( p->dd, bAux );
827 */
828 
829  // add to the reached set
830  p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );
831  if ( p->bReached == NULL )
832  {
833  if ( !p->pPars->fSilent )
834  printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
835  p->pPars->iFrame = nIters - 1;
836  Cudd_RecursiveDeref( p->dd, bAux );
837  return -1;
838  }
839  Cudd_Ref( p->bReached );
840  Cudd_RecursiveDeref( p->dd, bAux );
841 
842 
843  // report the results
844  if ( p->pPars->fVerbose )
845  {
846  printf( "I =%5d : ", nIters );
847  printf( "Fr =%7d ", nBddSizeFr );
848  printf( "ImNs =%7d ", nBddSizeTo );
849  printf( "ImCs =%7d ", nBddSizeTo2 );
850  printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
851  printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
852  Abc_PrintTime( 1, "T", Abc_Clock() - clkIter );
853  }
854 /*
855  if ( pPars->fVerbose )
856  {
857  double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) );
858 // Extra_bddPrint( p->dd, bReached );printf( "\n" );
859  printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
860  fflush( stdout );
861  }
862 */
863  if ( nIters == p->pPars->nIterMax - 1 )
864  {
865  if ( !p->pPars->fSilent )
866  printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
867  p->pPars->iFrame = nIters;
868  return -1;
869  }
870  }
871 
872  // report the stats
873  if ( p->pPars->fVerbose )
874  {
875  double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) );
876  if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) )
877  printf( "Reachability analysis completed after %d frames.\n", nIters );
878  else
879  printf( "Reachability analysis is stopped after %d frames.\n", nIters );
880  printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
881  fflush( stdout );
882  }
883  if ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) )
884  {
885  if ( !p->pPars->fSilent )
886  printf( "Verified only for states reachable in %d frames. ", nIters );
887  p->pPars->iFrame = p->pPars->nIterMax;
888  return -1; // undecided
889  }
890  // report
891  if ( !p->pPars->fSilent )
892  printf( "The miter is proved unreachable after %d iterations. ", nIters );
893  if ( !p->pPars->fSilent )
894  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
895  p->pPars->iFrame = nIters - 1;
896  return 1; // unreachable
897 }
898 
899 /**Function*************************************************************
900 
901  Synopsis [Reorders BDDs in the working manager.]
902 
903  Description []
904 
905  SideEffects []
906 
907  SeeAlso []
908 
909 ***********************************************************************/
910 void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose )
911 {
912  abctime clk = Abc_Clock();
913  if ( fVerbose )
914  Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
915  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
916  if ( fVerbose )
917  Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
918  if ( fTwice )
919  {
920  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
921  if ( fVerbose )
922  Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
923  }
924  if ( fVerbose )
925  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
926 }
927 
928 /**Function*************************************************************
929 
930  Synopsis []
931 
932  Description []
933 
934  SideEffects []
935 
936  SeeAlso []
937 
938 ***********************************************************************/
939 Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
940 {
941  Llb_Mnx_t * p;
942 
943  p = ABC_CALLOC( Llb_Mnx_t, 1 );
944  p->pAig = pAig;
945  p->pPars = pPars;
946 
947  // compute time to stop
948  p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
949 
950  if ( pPars->fCluster )
951  {
952 // Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
953 // Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
954  Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose );
955  // set the stop time parameter
956  p->dd->TimeStop = p->pPars->TimeTarget;
957  }
958  else
959  {
960 // p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig );
961  p->vOrder = Llb_Nonlin4CreateOrder( pAig );
962  p->dd = Cudd_Init( Vec_IntCountPositive(p->vOrder) + 1, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
963  Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
964  Cudd_SetMaxGrowth( p->dd, 1.05 );
965  // set the stop time parameter
966  p->dd->TimeStop = p->pPars->TimeTarget;
967  p->vRoots = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
968  }
969 
970  Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
971  p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, p->pPars->fBackward );
972  p->vRings = Vec_PtrAlloc( 100 );
973 
974  if ( pPars->fReorder )
975  Llb_Nonlin4Reorder( p->dd, 0, 1 );
976  return p;
977 }
978 
979 /**Function*************************************************************
980 
981  Synopsis []
982 
983  Description []
984 
985  SideEffects []
986 
987  SeeAlso []
988 
989 ***********************************************************************/
990 void Llb_MnxStop( Llb_Mnx_t * p )
991 {
992  DdNode * bTemp;
993  int i;
994  if ( p->pPars->fVerbose )
995  {
996  p->timeReo = Cudd_ReadReorderingTime(p->dd);
997  p->timeOther = p->timeTotal - p->timeImage - p->timeRemap;
998  ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
999  ABC_PRTP( "Remap ", p->timeRemap, p->timeTotal );
1000  ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
1001  ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
1002  ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
1003  }
1004  // remove BDDs
1005  if ( p->bBad )
1006  Cudd_RecursiveDeref( p->dd, p->bBad );
1007  if ( p->bReached )
1008  Cudd_RecursiveDeref( p->dd, p->bReached );
1009  if ( p->bCurrent )
1010  Cudd_RecursiveDeref( p->dd, p->bCurrent );
1011  if ( p->bNext )
1012  Cudd_RecursiveDeref( p->dd, p->bNext );
1013  if ( p->vRings )
1014  Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
1015  Cudd_RecursiveDeref( p->dd, bTemp );
1016  if ( p->vRoots )
1017  Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
1018  Cudd_RecursiveDeref( p->dd, bTemp );
1019  // remove arrays
1020  Vec_PtrFreeP( &p->vRings );
1021  Vec_PtrFreeP( &p->vRoots );
1022 //Cudd_PrintInfo( p->dd, stdout );
1023  Extra_StopManager( p->dd );
1024  Vec_IntFreeP( &p->vOrder );
1025  Vec_IntFreeP( &p->vVars2Q );
1026  ABC_FREE( p );
1027 }
1028 
1029 
1030 /**Function*************************************************************
1031 
1032  Synopsis []
1033 
1034  Description []
1035 
1036  SideEffects []
1037 
1038  SeeAlso []
1039 
1040 ***********************************************************************/
1041 void Llb_MnxCheckNextStateVars( Llb_Mnx_t * p )
1042 {
1043  Aig_Obj_t * pObj;
1044  int i, Counter0 = 0, Counter1 = 0;
1045  Saig_ManForEachLi( p->pAig, pObj, i )
1046  if ( Saig_ObjIsLo(p->pAig, Aig_ObjFanin0(pObj)) )
1047  {
1048  if ( Aig_ObjFaninC0(pObj) )
1049  Counter0++;
1050  else
1051  Counter1++;
1052  }
1053  printf( "Total = %d. Direct LO = %d. Compl LO = %d.\n", Aig_ManRegNum(p->pAig), Counter1, Counter0 );
1054 }
1055 
1056 /**Function*************************************************************
1057 
1058  Synopsis [Finds balanced cut.]
1059 
1060  Description []
1061 
1062  SideEffects []
1063 
1064  SeeAlso []
1065 
1066 ***********************************************************************/
1067 int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
1068 {
1069  Llb_Mnx_t * pMnn;
1070  int RetValue = -1;
1071  if ( pPars->fVerbose )
1072  Aig_ManPrintStats( pAig );
1073  if ( pPars->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) )
1074  {
1075  printf( "The number of objects is more than 2^15. Clustering cannot be used.\n" );
1076  return RetValue;
1077  }
1078  {
1079  abctime clk = Abc_Clock();
1080  pMnn = Llb_MnxStart( pAig, pPars );
1081 //Llb_MnxCheckNextStateVars( pMnn );
1082  if ( !pPars->fSkipReach )
1083  RetValue = Llb_Nonlin4Reachability( pMnn );
1084  pMnn->timeTotal = Abc_Clock() - clk;
1085  Llb_MnxStop( pMnn );
1086  }
1087  return RetValue;
1088 }
1089 
1090 
1091 /**Function*************************************************************
1092 
1093  Synopsis [Takes an AIG and returns an AIG representing reachable states.]
1094 
1095  Description []
1096 
1097  SideEffects []
1098 
1099  SeeAlso []
1100 
1101 ***********************************************************************/
1102 Aig_Man_t * Llb_ReachableStates( Aig_Man_t * pAig )
1103 {
1104  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
1105  Vec_Int_t * vPermute;
1106  Vec_Ptr_t * vNames;
1107  Gia_ParLlb_t Pars, * pPars = &Pars;
1108  DdManager * dd;
1109  DdNode * bReached;
1110  Llb_Mnx_t * pMnn;
1111  Abc_Ntk_t * pNtk, * pNtkMuxes;
1112  Aig_Obj_t * pObj;
1113  int i, RetValue;
1114  abctime clk = Abc_Clock();
1115 
1116  // create parameters
1117  Llb_ManSetDefaultParams( pPars );
1118  pPars->fSkipOutCheck = 1;
1119  pPars->fCluster = 0;
1120  pPars->fReorder = 0;
1121  pPars->fSilent = 1;
1122  pPars->nBddMax = 100;
1123  pPars->nClusterMax = 500;
1124 
1125  // run reachability
1126  pMnn = Llb_MnxStart( pAig, pPars );
1127  RetValue = Llb_Nonlin4Reachability( pMnn );
1128  assert( RetValue == 1 );
1129 
1130  // print BDD
1131 // Extra_bddPrint( pMnn->dd, pMnn->bReached );
1132 // Extra_bddPrintSupport( pMnn->dd, pMnn->bReached );
1133 // printf( "\n" );
1134 
1135  // collect flop output variables
1136  vPermute = Vec_IntStartFull( Cudd_ReadSize(pMnn->dd) );
1137  Saig_ManForEachLo( pAig, pObj, i )
1138  Vec_IntWriteEntry( vPermute, Llb_ObjBddVar(pMnn->vOrder, pObj), i );
1139 
1140  // transfer the reached state BDD into the new manager
1141  dd = Cudd_Init( Saig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
1142  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
1143  bReached = Extra_TransferPermute( pMnn->dd, dd, pMnn->bReached, Vec_IntArray(vPermute) ); Cudd_Ref( bReached );
1144  Vec_IntFree( vPermute );
1145  assert( Cudd_ReadSize(dd) == Saig_ManRegNum(pAig) );
1146 
1147  // quit reachability engine
1148  pMnn->timeTotal = Abc_Clock() - clk;
1149  Llb_MnxStop( pMnn );
1150 
1151  // derive the network
1152  vNames = Abc_NodeGetFakeNames( Saig_ManRegNum(pAig) );
1153  pNtk = Abc_NtkDeriveFromBdd( dd, bReached, "reached", vNames );
1154  Abc_NodeFreeNames( vNames );
1155  Cudd_RecursiveDeref( dd, bReached );
1156  Cudd_Quit( dd );
1157 
1158  // convert
1159  pNtkMuxes = Abc_NtkBddToMuxes( pNtk );
1160  Abc_NtkDelete( pNtk );
1161  pNtk = Abc_NtkStrash( pNtkMuxes, 0, 1, 0 );
1162  Abc_NtkDelete( pNtkMuxes );
1163  pAig = Abc_NtkToDar( pNtk, 0, 0 );
1164  Abc_NtkDelete( pNtk );
1165  return pAig;
1166 }
1167 Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p )
1168 {
1169  Gia_Man_t * pNew;
1170  Aig_Man_t * pAig, * pReached;
1171  pAig = Gia_ManToAigSimple( p );
1172  pReached = Llb_ReachableStates( pAig );
1173  Aig_ManStop( pAig );
1174  pNew = Gia_ManFromAigSimple( pReached );
1175  Aig_ManStop( pReached );
1176  return pNew;
1177 }
1178 
1179 ////////////////////////////////////////////////////////////////////////
1180 /// END OF FILE ///
1181 ////////////////////////////////////////////////////////////////////////
1182 
1183 
1184 ABC_NAMESPACE_IMPL_END
1185 
Vec_IntCountPositive
static int Vec_IntCountPositive(Vec_Int_t *p)
Definition: vecInt.h:1175
Llb4_Nonlin4TransformCex
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Llb4_Nonlin4TransformCex(Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
DECLARATIONS ///.
Definition: llb4Cex.c:47
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Llb_Nonlin4CollectHighRefNodes
Vec_Int_t * Llb_Nonlin4CollectHighRefNodes(Aig_Man_t *pAig, int nFans)
Definition: llb4Nonlin.c:314
Vec_PtrReverseOrder
static void Vec_PtrReverseOrder(Vec_Ptr_t *p)
Definition: vecPtr.h:785
Llb_Mnx_t
typedefABC_NAMESPACE_IMPL_START struct Llb_Mnx_t_ Llb_Mnx_t
DECLARATIONS ///.
Definition: llb4Nonlin.c:32
Llb_Mnx_t_::bCurrent
DdNode * bCurrent
Definition: llb4Nonlin.c:43
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
Llb_MnxStart
Llb_Mnx_t * Llb_MnxStart(Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition: llb4Nonlin.c:939
Llb4_Nonlin4Sweep
void Llb4_Nonlin4Sweep(Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
Definition: llb4Sweep.c:520
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Llb_Nonlin4CreateOrder_rec
void Llb_Nonlin4CreateOrder_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter)
Definition: llb4Nonlin.c:271
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
Llb_ManSetDefaultParams
void Llb_ManSetDefaultParams(Gia_ParLlb_t *pPars)
MACRO DEFINITIONS ///.
Definition: llb1Core.c:46
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
Llb_Mnx_t_::bReached
DdNode * bReached
Definition: llb4Nonlin.c:42
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Llb_Nonlin4SetupVarMap
void Llb_Nonlin4SetupVarMap(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder)
Definition: llb4Nonlin.c:417
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Llb_Nonlin4Multiply
Vec_Ptr_t * Llb_Nonlin4Multiply(DdManager *dd, DdNode *bCube, Vec_Ptr_t *vParts)
Definition: llb4Nonlin.c:533
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
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
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Cudd_ReadReorderings
int Cudd_ReadReorderings(DdManager *dd)
Definition: cuddAPI.c:1696
Llb_Mnx_t_
Definition: llb4Nonlin.c:33
Abc_Ntk_t_
Definition: abc.h:153
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition: abcStrash.c:265
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
Llb_Mnx_t_::pAig
Aig_Man_t * pAig
Definition: llb4Nonlin.c:36
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_Mnx_t_::timeOther
abctime timeOther
Definition: llb4Nonlin.c:55
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Cudd_SetVarMap
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:416
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
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
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Gia_ParLlb_t
typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t
INCLUDES ///.
Definition: llb.h:41
Gia_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition: giaAig.c:171
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Llb_Nonlin4Reorder
void Llb_Nonlin4Reorder(DdManager *dd, int fTwice, int fVerbose)
Definition: llb4Nonlin.c:910
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
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
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Llb_MnxCheckNextStateVars
void Llb_MnxCheckNextStateVars(Llb_Mnx_t *p)
Definition: llb4Nonlin.c:1041
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Llb_Mnx_t_::vOrder
Vec_Int_t * vOrder
Definition: llb4Nonlin.c:49
Cudd_ReadReorderingTime
long Cudd_ReadReorderingTime(DdManager *dd)
Definition: cuddAPI.c:1718
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Llb_Mnx_t_::bBad
DdNode * bBad
Definition: llb4Nonlin.c:41
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Abc_NodeFreeNames
ABC_DLL void Abc_NodeFreeNames(Vec_Ptr_t *vNames)
Definition: abcNames.c:257
Llb_Mnx_t_::vVars2Q
Vec_Int_t * vVars2Q
Definition: llb4Nonlin.c:50
Llb_Nonlin4ComputeCube
DdNode * Llb_Nonlin4ComputeCube(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, char *pValues, int Flag)
Definition: llb4Nonlin.c:477
Llb_Mnx_t_::timeReo
abctime timeReo
Definition: llb4Nonlin.c:54
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Llb_Mnx_t_::timeRemap
abctime timeRemap
Definition: llb4Nonlin.c:53
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Cudd_bddVarMap
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:373
Llb_Nonlin4CreateVars2Q
Vec_Int_t * Llb_Nonlin4CreateVars2Q(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fBackward)
Definition: llb4Nonlin.c:394
Llb_Nonlin4ComputeBad
DdNode * Llb_Nonlin4ComputeBad(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder)
FUNCTION DEFINITIONS ///.
Definition: llb4Nonlin.c:77
Abc_NtkDeriveFromBdd
ABC_DLL Abc_Ntk_t * Abc_NtkDeriveFromBdd(void *dd, void *bFunc, char *pNamePo, Vec_Ptr_t *vNamesPi)
FUNCTION DEFINITIONS ///.
Definition: abcNtbdd.c:56
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Llb_Nonlin4DeriveCex
Vec_Ptr_t * Llb_Nonlin4DeriveCex(Llb_Mnx_t *p, int fBackward, int fVerbose)
Definition: llb4Nonlin.c:578
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition: abcDar.c:233
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_ManDfsNodes
Vec_Ptr_t * Aig_ManDfsNodes(Aig_Man_t *p, Aig_Obj_t **ppNodes, int nNodes)
Definition: aigDfs.c:333
Abc_NodeGetFakeNames
ABC_DLL Vec_Ptr_t * Abc_NodeGetFakeNames(int nNames)
Definition: abcNames.c:221
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
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
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_Nonlin4Reachability
int Llb_Nonlin4Reachability(Llb_Mnx_t *p)
Definition: llb4Nonlin.c:670
Llb_Nonlin4ComputeInitState
DdNode * Llb_Nonlin4ComputeInitState(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fBackward)
Definition: llb4Nonlin.c:447
Llb_Mnx_t_::timeTotal
abctime timeTotal
Definition: llb4Nonlin.c:56
Llb_Nonlin4RecordState
void Llb_Nonlin4RecordState(Aig_Man_t *pAig, Vec_Int_t *vOrder, unsigned *pState, char *pValues, int fBackward)
Definition: llb4Nonlin.c:513
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Llb_Nonlin4CreateOrder
Vec_Int_t * Llb_Nonlin4CreateOrder(Aig_Man_t *pAig)
Definition: llb4Nonlin.c:346
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Llb_ReachableStatesGia
Gia_Man_t * Llb_ReachableStatesGia(Gia_Man_t *p)
Definition: llb4Nonlin.c:1167
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Llb_Mnx_t_::vRoots
Vec_Ptr_t * vRoots
Definition: llb4Nonlin.c:46
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Llb_Nonlin4Image
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Definition: llb4Image.c:752
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
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_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Llb_ReachableStates
Aig_Man_t * Llb_ReachableStates(Aig_Man_t *pAig)
Definition: llb4Nonlin.c:1102
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_ObjBddVar
static int Llb_ObjBddVar(Vec_Int_t *vOrder, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: llbInt.h:109
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
Llb_MnxStop
void Llb_MnxStop(Llb_Mnx_t *p)
Definition: llb4Nonlin.c:990
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_Nonlin4Deref
void Llb_Nonlin4Deref(DdManager *dd, Vec_Ptr_t *vParts)
Definition: llb4Nonlin.c:558
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Llb_Mnx_t_::vRings
Vec_Ptr_t * vRings
Definition: llb4Nonlin.c:45
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Llb_Nonlin4CreateOrderSimple
Vec_Int_t * Llb_Nonlin4CreateOrderSimple(Aig_Man_t *pAig)
Definition: llb4Nonlin.c:247
Abc_NtkBddToMuxes
ABC_DLL Abc_Ntk_t * Abc_NtkBddToMuxes(Abc_Ntk_t *pNtk)
Definition: abcNtbdd.c:125
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
Llb_Mnx_t_::timeImage
abctime timeImage
Definition: llb4Nonlin.c:52
Cudd_SetMaxGrowth
void Cudd_SetMaxGrowth(DdManager *dd, double mg)
Definition: cuddAPI.c:2013
Vec_PtrFreeP
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
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
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Llb_Mnx_t_::pPars
Gia_ParLlb_t * pPars
Definition: llb4Nonlin.c:37
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
Llb_Nonlin4DerivePartitions
Vec_Ptr_t * Llb_Nonlin4DerivePartitions(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder)
Definition: llb4Nonlin.c:167
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Llb_Mnx_t_::bNext
DdNode * bNext
Definition: llb4Nonlin.c:44
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Llb_Mnx_t_::dd
DdManager * dd
Definition: llb4Nonlin.c:40
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Llb_Nonlin4CoreReach
int Llb_Nonlin4CoreReach(Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition: llb4Nonlin.c:1067
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
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
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Cudd_ReadGarbageCollections
int Cudd_ReadGarbageCollections(DdManager *dd)
Definition: cuddAPI.c:1741
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
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