abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
pdrUtil.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [pdrUtil.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Property driven reachability.]
8 
9  Synopsis [Various utilities.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 20, 2010.]
16 
17  Revision [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "pdrInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis []
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 Pdr_Set_t * Pdr_SetAlloc( int nSize )
47 {
48  Pdr_Set_t * p;
49  assert( nSize >= 0 && nSize < (1<<30) );
50  p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
51  return p;
52 }
53 
54 /**Function*************************************************************
55 
56  Synopsis []
57 
58  Description []
59 
60  SideEffects []
61 
62  SeeAlso []
63 
64 ***********************************************************************/
65 Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
66 {
67  Pdr_Set_t * p;
68  int i;
69  assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) );
70  p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
71  p->nLits = Vec_IntSize(vLits);
72  p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
73  p->nRefs = 1;
74  p->Sign = 0;
75  for ( i = 0; i < p->nLits; i++ )
76  {
77  p->Lits[i] = Vec_IntEntry(vLits, i);
78  p->Sign |= ((word)1 << (p->Lits[i] % 63));
79  }
80  Vec_IntSelectSort( p->Lits, p->nLits );
81  // remember PI literals
82  for ( i = p->nLits; i < p->nTotal; i++ )
83  p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
84  return p;
85 }
86 
87 /**Function*************************************************************
88 
89  Synopsis []
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
99 {
100  Pdr_Set_t * p;
101  int i, k = 0;
102  assert( iRemove >= 0 && iRemove < pSet->nLits );
103  p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
104  p->nLits = pSet->nLits - 1;
105  p->nTotal = pSet->nTotal - 1;
106  p->nRefs = 1;
107  p->Sign = 0;
108  for ( i = 0; i < pSet->nTotal; i++ )
109  {
110  if ( i == iRemove )
111  continue;
112  p->Lits[k++] = pSet->Lits[i];
113  if ( i >= pSet->nLits )
114  continue;
115  p->Sign |= ((word)1 << (pSet->Lits[i] % 63));
116  }
117  assert( k == p->nTotal );
118  return p;
119 }
120 
121 /**Function*************************************************************
122 
123  Synopsis []
124 
125  Description []
126 
127  SideEffects []
128 
129  SeeAlso []
130 
131 ***********************************************************************/
132 Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
133 {
134  Pdr_Set_t * p;
135  int i, k = 0;
136  assert( nLits >= 0 && nLits <= pSet->nLits );
137  p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
138  p->nLits = nLits;
139  p->nTotal = nLits + pSet->nTotal - pSet->nLits;
140  p->nRefs = 1;
141  p->Sign = 0;
142  for ( i = 0; i < nLits; i++ )
143  {
144  assert( pLits[i] >= 0 );
145  p->Lits[k++] = pLits[i];
146  p->Sign |= ((word)1 << (pLits[i] % 63));
147  }
148  Vec_IntSelectSort( p->Lits, p->nLits );
149  for ( i = pSet->nLits; i < pSet->nTotal; i++ )
150  p->Lits[k++] = pSet->Lits[i];
151  assert( k == p->nTotal );
152  return p;
153 }
154 
155 /**Function*************************************************************
156 
157  Synopsis []
158 
159  Description []
160 
161  SideEffects []
162 
163  SeeAlso []
164 
165 ***********************************************************************/
166 Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
167 {
168  Pdr_Set_t * p;
169  int i;
170  p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
171  p->nLits = pSet->nLits;
172  p->nTotal = pSet->nTotal;
173  p->nRefs = 1;
174  p->Sign = pSet->Sign;
175  for ( i = 0; i < pSet->nTotal; i++ )
176  p->Lits[i] = pSet->Lits[i];
177  return p;
178 }
179 
180 /**Function*************************************************************
181 
182  Synopsis []
183 
184  Description []
185 
186  SideEffects []
187 
188  SeeAlso []
189 
190 ***********************************************************************/
191 Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p )
192 {
193  p->nRefs++;
194  return p;
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis []
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 void Pdr_SetDeref( Pdr_Set_t * p )
209 {
210  if ( --p->nRefs == 0 )
211  ABC_FREE( p );
212 }
213 
214 /**Function*************************************************************
215 
216  Synopsis []
217 
218  Description []
219 
220  SideEffects []
221 
222  SeeAlso []
223 
224 ***********************************************************************/
225 void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
226 {
227  char * pBuff;
228  int i, k, Entry;
229  pBuff = ABC_ALLOC( char, nRegs + 1 );
230  for ( i = 0; i < nRegs; i++ )
231  pBuff[i] = '-';
232  pBuff[i] = 0;
233  for ( i = 0; i < p->nLits; i++ )
234  {
235  if ( p->Lits[i] == -1 )
236  continue;
237  pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
238  }
239  if ( vFlopCounts )
240  {
241  // skip some literals
242  k = 0;
243  Vec_IntForEachEntry( vFlopCounts, Entry, i )
244  if ( Entry )
245  pBuff[k++] = pBuff[i];
246  pBuff[k] = 0;
247  }
248  fprintf( pFile, "%s", pBuff );
249  ABC_FREE( pBuff );
250 }
251 
252 /**Function*************************************************************
253 
254  Synopsis [Return 1 if pOld set-theoretically contains pNew.]
255 
256  Description []
257 
258  SideEffects []
259 
260  SeeAlso []
261 
262 ***********************************************************************/
263 int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
264 {
265  int * pOldInt, * pNewInt;
266  assert( pOld->nLits > 0 );
267  assert( pNew->nLits > 0 );
268  if ( pOld->nLits < pNew->nLits )
269  return 0;
270  if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
271  return 0;
272  pOldInt = pOld->Lits + pOld->nLits - 1;
273  pNewInt = pNew->Lits + pNew->nLits - 1;
274  while ( pNew->Lits <= pNewInt )
275  {
276  if ( pOld->Lits > pOldInt )
277  return 0;
278  assert( *pNewInt != -1 );
279  assert( *pOldInt != -1 );
280  if ( *pNewInt == *pOldInt )
281  pNewInt--, pOldInt--;
282  else if ( *pNewInt < *pOldInt )
283  pOldInt--;
284  else
285  return 0;
286  }
287  return 1;
288 }
289 
290 /**Function*************************************************************
291 
292  Synopsis [Return 1 if pOld set-theoretically contains pNew.]
293 
294  Description []
295 
296  SideEffects []
297 
298  SeeAlso []
299 
300 ***********************************************************************/
301 int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
302 {
303  int * pOldInt, * pNewInt;
304  assert( pOld->nLits > 0 );
305  assert( pNew->nLits > 0 );
306  pOldInt = pOld->Lits + pOld->nLits - 1;
307  pNewInt = pNew->Lits + pNew->nLits - 1;
308  while ( pNew->Lits <= pNewInt )
309  {
310  assert( *pOldInt != -1 );
311  if ( *pNewInt == -1 )
312  {
313  pNewInt--;
314  continue;
315  }
316  if ( pOld->Lits > pOldInt )
317  return 0;
318  assert( *pNewInt != -1 );
319  assert( *pOldInt != -1 );
320  if ( *pNewInt == *pOldInt )
321  pNewInt--, pOldInt--;
322  else if ( *pNewInt < *pOldInt )
323  pOldInt--;
324  else
325  return 0;
326  }
327  return 1;
328 }
329 
330 /**Function*************************************************************
331 
332  Synopsis [Return 1 if the state cube contains init state (000...0).]
333 
334  Description []
335 
336  SideEffects []
337 
338  SeeAlso []
339 
340 ***********************************************************************/
341 int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
342 {
343  int i;
344  for ( i = 0; i < pCube->nLits; i++ )
345  {
346  assert( pCube->Lits[i] != -1 );
347  if ( i == iRemove )
348  continue;
349  if ( lit_sign( pCube->Lits[i] ) == 0 )
350  return 0;
351  }
352  return 1;
353 }
354 
355 /**Function*************************************************************
356 
357  Synopsis []
358 
359  Description []
360 
361  SideEffects []
362 
363  SeeAlso []
364 
365 ***********************************************************************/
366 int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
367 {
368  Pdr_Set_t * p1 = *pp1;
369  Pdr_Set_t * p2 = *pp2;
370  int i;
371  for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
372  {
373  if ( p1->Lits[i] > p2->Lits[i] )
374  return -1;
375  if ( p1->Lits[i] < p2->Lits[i] )
376  return 1;
377  }
378  if ( i == p1->nLits && i < p2->nLits )
379  return -1;
380  if ( i < p1->nLits && i == p2->nLits )
381  return 1;
382  return 0;
383 }
384 
385 /**Function*************************************************************
386 
387  Synopsis []
388 
389  Description []
390 
391  SideEffects []
392 
393  SeeAlso []
394 
395 ***********************************************************************/
396 Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
397 {
398  Pdr_Obl_t * p;
399  p = ABC_ALLOC( Pdr_Obl_t, 1 );
400  p->iFrame = k;
401  p->prio = prio;
402  p->nRefs = 1;
403  p->pState = pState;
404  p->pNext = pNext;
405  p->pLink = NULL;
406  return p;
407 }
408 
409 /**Function*************************************************************
410 
411  Synopsis []
412 
413  Description []
414 
415  SideEffects []
416 
417  SeeAlso []
418 
419 ***********************************************************************/
420 Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
421 {
422  p->nRefs++;
423  return p;
424 }
425 
426 /**Function*************************************************************
427 
428  Synopsis []
429 
430  Description []
431 
432  SideEffects []
433 
434  SeeAlso []
435 
436 ***********************************************************************/
437 void Pdr_OblDeref( Pdr_Obl_t * p )
438 {
439  if ( --p->nRefs == 0 )
440  {
441  if ( p->pNext )
442  Pdr_OblDeref( p->pNext );
443  Pdr_SetDeref( p->pState );
444  ABC_FREE( p );
445  }
446 }
447 
448 /**Function*************************************************************
449 
450  Synopsis []
451 
452  Description []
453 
454  SideEffects []
455 
456  SeeAlso []
457 
458 ***********************************************************************/
459 int Pdr_QueueIsEmpty( Pdr_Man_t * p )
460 {
461  return p->pQueue == NULL;
462 }
463 
464 /**Function*************************************************************
465 
466  Synopsis []
467 
468  Description []
469 
470  SideEffects []
471 
472  SeeAlso []
473 
474 ***********************************************************************/
475 Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
476 {
477  return p->pQueue;
478 }
479 
480 /**Function*************************************************************
481 
482  Synopsis []
483 
484  Description []
485 
486  SideEffects []
487 
488  SeeAlso []
489 
490 ***********************************************************************/
491 Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
492 {
493  Pdr_Obl_t * pRes = p->pQueue;
494  if ( p->pQueue == NULL )
495  return NULL;
496  p->pQueue = p->pQueue->pLink;
497  Pdr_OblDeref( pRes );
498  p->nQueCur--;
499  return pRes;
500 }
501 
502 /**Function*************************************************************
503 
504  Synopsis []
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 void Pdr_QueueClean( Pdr_Man_t * p )
514 {
515  Pdr_Obl_t * pThis;
516  while ( (pThis = Pdr_QueuePop(p)) )
517  Pdr_OblDeref( pThis );
518  pThis = NULL;
519 }
520 
521 /**Function*************************************************************
522 
523  Synopsis []
524 
525  Description []
526 
527  SideEffects []
528 
529  SeeAlso []
530 
531 ***********************************************************************/
532 void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
533 {
534  Pdr_Obl_t * pTemp, ** ppPrev;
535  p->nObligs++;
536  p->nQueCur++;
537  p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
538  Pdr_OblRef( pObl );
539  if ( p->pQueue == NULL )
540  {
541  p->pQueue = pObl;
542  return;
543  }
544  for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
545  if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
546  break;
547  *ppPrev = pObl;
548  pObl->pLink = pTemp;
549 }
550 
551 /**Function*************************************************************
552 
553  Synopsis []
554 
555  Description []
556 
557  SideEffects []
558 
559  SeeAlso []
560 
561 ***********************************************************************/
562 void Pdr_QueuePrint( Pdr_Man_t * p )
563 {
564  Pdr_Obl_t * pObl;
565  for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
566  Abc_Print( 1, "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
567 }
568 
569 /**Function*************************************************************
570 
571  Synopsis []
572 
573  Description []
574 
575  SideEffects []
576 
577  SeeAlso []
578 
579 ***********************************************************************/
580 void Pdr_QueueStop( Pdr_Man_t * p )
581 {
582  Pdr_Obl_t * pObl;
583  while ( !Pdr_QueueIsEmpty(p) )
584  {
585  pObl = Pdr_QueuePop(p);
586  Pdr_OblDeref( pObl );
587  }
588  p->pQueue = NULL;
589  p->nQueCur = 0;
590 }
591 
592 
593 #define PDR_VAL0 1
594 #define PDR_VAL1 2
595 #define PDR_VALX 3
596 
597 /**Function*************************************************************
598 
599  Synopsis [Returns value (0 or 1) or X if unassigned.]
600 
601  Description []
602 
603  SideEffects []
604 
605  SeeAlso []
606 
607 ***********************************************************************/
608 static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
609 {
610  if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
611  return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0;
612  return PDR_VALX;
613 }
614 
615 /**Function*************************************************************
616 
617  Synopsis [Recursively searched for a satisfying assignment.]
618 
619  Description []
620 
621  SideEffects []
622 
623  SeeAlso []
624 
625 ***********************************************************************/
626 int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur )
627 {
628  int Value0, Value1;
629  if ( Aig_ObjIsConst1(pNode) )
630  return 1;
631  if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
632  return ((int)pNode->fMarkA == Value);
633  Aig_ObjSetTravIdCurrent(pAig, pNode);
634  pNode->fMarkA = Value;
635  if ( Aig_ObjIsCi(pNode) )
636  {
637 // if ( vSuppLits )
638 // Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
639  if ( Saig_ObjIsLo(pAig, pNode) )
640  {
641 // pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
642  pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value );
643  pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
644  }
645  return 1;
646  }
647  assert( Aig_ObjIsNode(pNode) );
648  // propagation
649  if ( Value )
650  {
651  if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) )
652  return 0;
653  return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur);
654  }
655  // justification
656  Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
657  if ( Value0 == PDR_VAL0 )
658  return 1;
659  Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
660  if ( Value1 == PDR_VAL0 )
661  return 1;
662  if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 )
663  return 0;
664  if ( Value0 == PDR_VAL1 )
665  return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
666  if ( Value1 == PDR_VAL1 )
667  return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
668  assert( Value0 == PDR_VALX && Value1 == PDR_VALX );
669  // decision making
670 // if ( rand() % 10 == Heur )
671  if ( Aig_ObjId(pNode) % 4 == Heur )
672  return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
673  else
674  return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
675 }
676 
677 /**Function*************************************************************
678 
679  Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]
680 
681  Description []
682 
683  SideEffects []
684 
685  SeeAlso []
686 
687 ***********************************************************************/
688 int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
689 {
690  Aig_Obj_t * pNode;
691  int i, v, fCompl;
692 // return 0;
693  for ( i = 0; i < 4; i++ )
694  {
695  // derive new assignment
696  p->pCubeJust->nLits = 0;
697  p->pCubeJust->Sign = 0;
698  Aig_ManIncrementTravId( p->pAig );
699  for ( v = 0; v < pCube->nLits; v++ )
700  {
701  if ( pCube->Lits[v] == -1 )
702  continue;
703  pNode = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) );
704  fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode);
705  if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) )
706  break;
707  }
708  if ( v < pCube->nLits )
709  continue;
710  // figure this out!!!
711  if ( p->pCubeJust->nLits == 0 )
712  continue;
713  // successfully derived new assignment
714  Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits );
715  // check assignment against this cube
716  if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) )
717  continue;
718 //printf( "\n" );
719 //Pdr_SetPrint( stdout, pCube, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
720 //Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
721  // check assignment against the clauses
722  if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) )
723  continue;
724  // find good assignment
725  return 1;
726  }
727  return 0;
728 }
729 
730 
731 ////////////////////////////////////////////////////////////////////////
732 /// END OF FILE ///
733 ////////////////////////////////////////////////////////////////////////
734 
735 
736 ABC_NAMESPACE_IMPL_END
737 
Pdr_SetRef
Pdr_Set_t * Pdr_SetRef(Pdr_Set_t *p)
Definition: pdrUtil.c:191
Pdr_Man_t_::pQueue
Pdr_Obl_t * pQueue
Definition: pdrInt.h:85
Pdr_Man_t_::pAig
Aig_Man_t * pAig
Definition: pdrInt.h:70
Pdr_Man_t_::nObligs
int nObligs
Definition: pdrInt.h:106
Pdr_QueueHead
Pdr_Obl_t * Pdr_QueueHead(Pdr_Man_t *p)
Definition: pdrUtil.c:475
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Pdr_Obl_t_::prio
int prio
Definition: pdrInt.h:58
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
Pdr_SetCompare
int Pdr_SetCompare(Pdr_Set_t **pp1, Pdr_Set_t **pp2)
Definition: pdrUtil.c:366
Pdr_Obl_t_::pState
Pdr_Set_t * pState
Definition: pdrInt.h:60
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Pdr_Obl_t_::nRefs
int nRefs
Definition: pdrInt.h:59
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Pdr_SetCreateFrom
Pdr_Set_t * Pdr_SetCreateFrom(Pdr_Set_t *pSet, int iRemove)
Definition: pdrUtil.c:98
Pdr_Obl_t_
Definition: pdrInt.h:55
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Pdr_SetCreate
Pdr_Set_t * Pdr_SetCreate(Vec_Int_t *vLits, Vec_Int_t *vPiLits)
Definition: pdrUtil.c:65
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Pdr_Obl_t_::pNext
Pdr_Obl_t * pNext
Definition: pdrInt.h:61
Pdr_SetCreateSubset
Pdr_Set_t * Pdr_SetCreateSubset(Pdr_Set_t *pSet, int *pLits, int nLits)
Definition: pdrUtil.c:132
Pdr_Man_t_::pCubeJust
Pdr_Set_t * pCubeJust
Definition: pdrInt.h:102
Pdr_SetAlloc
ABC_NAMESPACE_IMPL_START Pdr_Set_t * Pdr_SetAlloc(int nSize)
DECLARATIONS ///.
Definition: pdrUtil.c:46
Pdr_QueuePrint
void Pdr_QueuePrint(Pdr_Man_t *p)
Definition: pdrUtil.c:562
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Pdr_Man_t_
Definition: pdrInt.h:66
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Pdr_SetPrint
void Pdr_SetPrint(FILE *pFile, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
Definition: pdrUtil.c:225
Pdr_Man_t_::nQueMax
int nQueMax
Definition: pdrInt.h:118
Pdr_SetDup
Pdr_Set_t * Pdr_SetDup(Pdr_Set_t *pSet)
Definition: pdrUtil.c:166
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Pdr_SetDeref
void Pdr_SetDeref(Pdr_Set_t *p)
Definition: pdrUtil.c:208
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Pdr_Obl_t_::iFrame
int iFrame
Definition: pdrInt.h:57
Pdr_ObjSatValue
static int Pdr_ObjSatValue(Aig_Man_t *pAig, Aig_Obj_t *pNode, int fCompl)
Definition: pdrUtil.c:608
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Pdr_Obl_t_::pLink
Pdr_Obl_t * pLink
Definition: pdrInt.h:62
Vec_IntSelectSort
static void Vec_IntSelectSort(int *pArray, int nSize)
Definition: vecInt.h:1740
Pdr_QueueStop
void Pdr_QueueStop(Pdr_Man_t *p)
Definition: pdrUtil.c:580
Pdr_NtkFindSatAssign_rec
int Pdr_NtkFindSatAssign_rec(Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Pdr_Set_t *pCube, int Heur)
Definition: pdrUtil.c:626
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Pdr_QueueIsEmpty
int Pdr_QueueIsEmpty(Pdr_Man_t *p)
Definition: pdrUtil.c:459
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Saig_ManLi
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Pdr_Set_t
typedefABC_NAMESPACE_HEADER_START struct Pdr_Set_t_ Pdr_Set_t
INCLUDES ///.
Definition: pdrInt.h:44
PDR_VALX
#define PDR_VALX
Definition: pdrUtil.c:595
Pdr_QueuePop
Pdr_Obl_t * Pdr_QueuePop(Pdr_Man_t *p)
Definition: pdrUtil.c:491
Aig_Obj_t_
Definition: aig.h:69
PDR_VAL1
#define PDR_VAL1
Definition: pdrUtil.c:594
Pdr_ManCubeJust
int Pdr_ManCubeJust(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition: pdrUtil.c:688
Pdr_QueuePush
void Pdr_QueuePush(Pdr_Man_t *p, Pdr_Obl_t *pObl)
Definition: pdrUtil.c:532
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Pdr_OblRef
Pdr_Obl_t * Pdr_OblRef(Pdr_Obl_t *p)
Definition: pdrUtil.c:420
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Pdr_ManCheckContainment
int Pdr_ManCheckContainment(Pdr_Man_t *p, int k, Pdr_Set_t *pSet)
Definition: pdrCore.c:241
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Pdr_OblDeref
void Pdr_OblDeref(Pdr_Obl_t *p)
Definition: pdrUtil.c:437
Pdr_QueueClean
void Pdr_QueueClean(Pdr_Man_t *p)
Definition: pdrUtil.c:513
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Pdr_SetIsInit
int Pdr_SetIsInit(Pdr_Set_t *pCube, int iRemove)
Definition: pdrUtil.c:341
PDR_VAL0
#define PDR_VAL0
Definition: pdrUtil.c:593
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Pdr_SetContains
int Pdr_SetContains(Pdr_Set_t *pOld, Pdr_Set_t *pNew)
Definition: pdrUtil.c:263
Pdr_OblStart
Pdr_Obl_t * Pdr_OblStart(int k, int prio, Pdr_Set_t *pState, Pdr_Obl_t *pNext)
Definition: pdrUtil.c:396
Pdr_Man_t_::nQueCur
int nQueCur
Definition: pdrInt.h:117
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Pdr_SetContainsSimple
int Pdr_SetContainsSimple(Pdr_Set_t *pOld, Pdr_Set_t *pNew)
Definition: pdrUtil.c:301
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285