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 ***********************************************************************/
Pdr_SetAlloc(int nSize)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 ***********************************************************************/
Pdr_SetCreate(Vec_Int_t * vLits,Vec_Int_t * vPiLits)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 ***********************************************************************/
Pdr_SetCreateFrom(Pdr_Set_t * pSet,int iRemove)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 ***********************************************************************/
Pdr_SetCreateSubset(Pdr_Set_t * pSet,int * pLits,int nLits)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 ***********************************************************************/
Pdr_SetDup(Pdr_Set_t * pSet)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 ***********************************************************************/
Pdr_SetRef(Pdr_Set_t * p)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 ***********************************************************************/
Pdr_SetDeref(Pdr_Set_t * p)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 ***********************************************************************/
Pdr_SetPrint(FILE * pFile,Pdr_Set_t * p,int nRegs,Vec_Int_t * vFlopCounts)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[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(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 []
255
256 Description []
257
258 SideEffects []
259
260 SeeAlso []
261
262 ***********************************************************************/
ZPdr_SetPrint(Pdr_Set_t * p)263 void ZPdr_SetPrint( Pdr_Set_t * p )
264 {
265 int i;
266 for ( i = 0; i < p->nLits; i++)
267 printf ("%d ", p->Lits[i]);
268 printf ("\n");
269
270 }
271
272 /**Function*************************************************************
273
274 Synopsis [Return the intersection of p1 and p2.]
275
276 Description []
277
278 SideEffects []
279
280 SeeAlso []
281
282 ***********************************************************************/
ZPdr_SetIntersection(Pdr_Set_t * p1,Pdr_Set_t * p2,Hash_Int_t * keep)283 Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep )
284 {
285 Pdr_Set_t * pIntersection;
286 Vec_Int_t * vCommonLits, * vPiLits;
287 int i, j, nLits;
288 nLits = p1->nLits;
289 if ( p2->nLits < nLits )
290 nLits = p2->nLits;
291 vCommonLits = Vec_IntAlloc( nLits );
292 vPiLits = Vec_IntAlloc( 1 );
293 for ( i = 0, j = 0; i < p1->nLits && j < p2->nLits; )
294 {
295 if ( p1->Lits[i] > p2->Lits[j] )
296 {
297 if ( Hash_IntExists( keep, p2->Lits[j] ) )
298 {
299 //about to drop a literal that should not be dropped
300 Vec_IntFree( vCommonLits );
301 Vec_IntFree( vPiLits );
302 return NULL;
303 }
304 j++;
305 }
306 else if ( p1->Lits[i] < p2->Lits[j] )
307 {
308 if ( Hash_IntExists( keep, p1->Lits[i] ) )
309 {
310 //about to drop a literal that should not be dropped
311 Vec_IntFree( vCommonLits );
312 Vec_IntFree( vPiLits );
313 return NULL;
314 }
315 i++;
316 }
317 else
318 {
319 Vec_IntPush( vCommonLits, p1->Lits[i] );
320 i++;
321 j++;
322 }
323 }
324 pIntersection = Pdr_SetCreate( vCommonLits, vPiLits );
325 Vec_IntFree( vCommonLits );
326 Vec_IntFree( vPiLits );
327 return pIntersection;
328 }
329
330
331 /**Function*************************************************************
332
333 Synopsis []
334
335 Description []
336
337 SideEffects []
338
339 SeeAlso []
340
341 ***********************************************************************/
Pdr_SetPrintStr(Vec_Str_t * vStr,Pdr_Set_t * p,int nRegs,Vec_Int_t * vFlopCounts)342 void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
343 {
344 char * pBuff;
345 int i, k = 0, Entry;
346 pBuff = ABC_ALLOC( char, nRegs + 1 );
347 for ( i = 0; i < nRegs; i++ )
348 pBuff[i] = '-';
349 pBuff[i] = 0;
350 for ( i = 0; i < p->nLits; i++ )
351 {
352 if ( p->Lits[i] == -1 )
353 continue;
354 pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
355 }
356 if ( vFlopCounts )
357 {
358 // skip some literals
359 Vec_IntForEachEntry( vFlopCounts, Entry, i )
360 if ( Entry )
361 pBuff[k++] = pBuff[i];
362 pBuff[k] = 0;
363 }
364 Vec_StrPushBuffer( vStr, pBuff, k );
365 Vec_StrPush( vStr, ' ' );
366 Vec_StrPush( vStr, '1' );
367 Vec_StrPush( vStr, '\n' );
368 ABC_FREE( pBuff );
369 }
370
371 /**Function*************************************************************
372
373 Synopsis [Return 1 if pOld set-theoretically contains pNew.]
374
375 Description []
376
377 SideEffects []
378
379 SeeAlso []
380
381 ***********************************************************************/
Pdr_SetContains(Pdr_Set_t * pOld,Pdr_Set_t * pNew)382 int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
383 {
384 int * pOldInt, * pNewInt;
385 assert( pOld->nLits > 0 );
386 assert( pNew->nLits > 0 );
387 if ( pOld->nLits < pNew->nLits )
388 return 0;
389 if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
390 return 0;
391 pOldInt = pOld->Lits + pOld->nLits - 1;
392 pNewInt = pNew->Lits + pNew->nLits - 1;
393 while ( pNew->Lits <= pNewInt )
394 {
395 if ( pOld->Lits > pOldInt )
396 return 0;
397 assert( *pNewInt != -1 );
398 assert( *pOldInt != -1 );
399 if ( *pNewInt == *pOldInt )
400 pNewInt--, pOldInt--;
401 else if ( *pNewInt < *pOldInt )
402 pOldInt--;
403 else
404 return 0;
405 }
406 return 1;
407 }
408
409 /**Function*************************************************************
410
411 Synopsis [Return 1 if pOld set-theoretically contains pNew.]
412
413 Description []
414
415 SideEffects []
416
417 SeeAlso []
418
419 ***********************************************************************/
Pdr_SetContainsSimple(Pdr_Set_t * pOld,Pdr_Set_t * pNew)420 int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
421 {
422 int * pOldInt, * pNewInt;
423 assert( pOld->nLits > 0 );
424 assert( pNew->nLits > 0 );
425 pOldInt = pOld->Lits + pOld->nLits - 1;
426 pNewInt = pNew->Lits + pNew->nLits - 1;
427 while ( pNew->Lits <= pNewInt )
428 {
429 assert( *pOldInt != -1 );
430 if ( *pNewInt == -1 )
431 {
432 pNewInt--;
433 continue;
434 }
435 if ( pOld->Lits > pOldInt )
436 return 0;
437 assert( *pNewInt != -1 );
438 assert( *pOldInt != -1 );
439 if ( *pNewInt == *pOldInt )
440 pNewInt--, pOldInt--;
441 else if ( *pNewInt < *pOldInt )
442 pOldInt--;
443 else
444 return 0;
445 }
446 return 1;
447 }
448
449 /**Function*************************************************************
450
451 Synopsis [Return 1 if the state cube contains init state (000...0).]
452
453 Description []
454
455 SideEffects []
456
457 SeeAlso []
458
459 ***********************************************************************/
Pdr_SetIsInit(Pdr_Set_t * pCube,int iRemove)460 int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
461 {
462 int i;
463 for ( i = 0; i < pCube->nLits; i++ )
464 {
465 assert( pCube->Lits[i] != -1 );
466 if ( i == iRemove )
467 continue;
468 if ( Abc_LitIsCompl( pCube->Lits[i] ) == 0 )
469 return 0;
470 }
471 return 1;
472 }
473
474 /**Function*************************************************************
475
476 Synopsis []
477
478 Description []
479
480 SideEffects []
481
482 SeeAlso []
483
484 ***********************************************************************/
Pdr_SetCompare(Pdr_Set_t ** pp1,Pdr_Set_t ** pp2)485 int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
486 {
487 Pdr_Set_t * p1 = *pp1;
488 Pdr_Set_t * p2 = *pp2;
489 int i;
490 for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
491 {
492 if ( p1->Lits[i] > p2->Lits[i] )
493 return -1;
494 if ( p1->Lits[i] < p2->Lits[i] )
495 return 1;
496 }
497 if ( i == p1->nLits && i < p2->nLits )
498 return -1;
499 if ( i < p1->nLits && i == p2->nLits )
500 return 1;
501 return 0;
502 }
503
504 /**Function*************************************************************
505
506 Synopsis []
507
508 Description []
509
510 SideEffects []
511
512 SeeAlso []
513
514 ***********************************************************************/
Pdr_OblStart(int k,int prio,Pdr_Set_t * pState,Pdr_Obl_t * pNext)515 Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
516 {
517 Pdr_Obl_t * p;
518 p = ABC_ALLOC( Pdr_Obl_t, 1 );
519 p->iFrame = k;
520 p->prio = prio;
521 p->nRefs = 1;
522 p->pState = pState;
523 p->pNext = pNext;
524 p->pLink = NULL;
525 return p;
526 }
527
528 /**Function*************************************************************
529
530 Synopsis []
531
532 Description []
533
534 SideEffects []
535
536 SeeAlso []
537
538 ***********************************************************************/
Pdr_OblRef(Pdr_Obl_t * p)539 Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
540 {
541 p->nRefs++;
542 return p;
543 }
544
545 /**Function*************************************************************
546
547 Synopsis []
548
549 Description []
550
551 SideEffects []
552
553 SeeAlso []
554
555 ***********************************************************************/
Pdr_OblDeref(Pdr_Obl_t * p)556 void Pdr_OblDeref( Pdr_Obl_t * p )
557 {
558 if ( --p->nRefs == 0 )
559 {
560 if ( p->pNext )
561 Pdr_OblDeref( p->pNext );
562 Pdr_SetDeref( p->pState );
563 ABC_FREE( p );
564 }
565 }
566
567 /**Function*************************************************************
568
569 Synopsis []
570
571 Description []
572
573 SideEffects []
574
575 SeeAlso []
576
577 ***********************************************************************/
Pdr_QueueIsEmpty(Pdr_Man_t * p)578 int Pdr_QueueIsEmpty( Pdr_Man_t * p )
579 {
580 return p->pQueue == NULL;
581 }
582
583 /**Function*************************************************************
584
585 Synopsis []
586
587 Description []
588
589 SideEffects []
590
591 SeeAlso []
592
593 ***********************************************************************/
Pdr_QueueHead(Pdr_Man_t * p)594 Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
595 {
596 return p->pQueue;
597 }
598
599 /**Function*************************************************************
600
601 Synopsis []
602
603 Description []
604
605 SideEffects []
606
607 SeeAlso []
608
609 ***********************************************************************/
Pdr_QueuePop(Pdr_Man_t * p)610 Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
611 {
612 Pdr_Obl_t * pRes = p->pQueue;
613 if ( p->pQueue == NULL )
614 return NULL;
615 p->pQueue = p->pQueue->pLink;
616 Pdr_OblDeref( pRes );
617 p->nQueCur--;
618 return pRes;
619 }
620
621 /**Function*************************************************************
622
623 Synopsis []
624
625 Description []
626
627 SideEffects []
628
629 SeeAlso []
630
631 ***********************************************************************/
Pdr_QueueClean(Pdr_Man_t * p)632 void Pdr_QueueClean( Pdr_Man_t * p )
633 {
634 Pdr_Obl_t * pThis;
635 while ( (pThis = Pdr_QueuePop(p)) )
636 Pdr_OblDeref( pThis );
637 pThis = NULL;
638 }
639
640 /**Function*************************************************************
641
642 Synopsis []
643
644 Description []
645
646 SideEffects []
647
648 SeeAlso []
649
650 ***********************************************************************/
Pdr_QueuePush(Pdr_Man_t * p,Pdr_Obl_t * pObl)651 void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
652 {
653 Pdr_Obl_t * pTemp, ** ppPrev;
654 p->nObligs++;
655 p->nQueCur++;
656 p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
657 Pdr_OblRef( pObl );
658 if ( p->pQueue == NULL )
659 {
660 p->pQueue = pObl;
661 return;
662 }
663 for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
664 if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
665 break;
666 *ppPrev = pObl;
667 pObl->pLink = pTemp;
668 }
669
670 /**Function*************************************************************
671
672 Synopsis []
673
674 Description []
675
676 SideEffects []
677
678 SeeAlso []
679
680 ***********************************************************************/
Pdr_QueuePrint(Pdr_Man_t * p)681 void Pdr_QueuePrint( Pdr_Man_t * p )
682 {
683 Pdr_Obl_t * pObl;
684 for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
685 Abc_Print( 1, "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
686 }
687
688 /**Function*************************************************************
689
690 Synopsis []
691
692 Description []
693
694 SideEffects []
695
696 SeeAlso []
697
698 ***********************************************************************/
Pdr_QueueStop(Pdr_Man_t * p)699 void Pdr_QueueStop( Pdr_Man_t * p )
700 {
701 Pdr_Obl_t * pObl;
702 while ( !Pdr_QueueIsEmpty(p) )
703 {
704 pObl = Pdr_QueuePop(p);
705 Pdr_OblDeref( pObl );
706 }
707 p->pQueue = NULL;
708 p->nQueCur = 0;
709 }
710
711
712 #define PDR_VAL0 1
713 #define PDR_VAL1 2
714 #define PDR_VALX 3
715
716 /**Function*************************************************************
717
718 Synopsis [Returns value (0 or 1) or X if unassigned.]
719
720 Description []
721
722 SideEffects []
723
724 SeeAlso []
725
726 ***********************************************************************/
Pdr_ObjSatValue(Aig_Man_t * pAig,Aig_Obj_t * pNode,int fCompl)727 static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
728 {
729 if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
730 return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0;
731 return PDR_VALX;
732 }
733
734 /**Function*************************************************************
735
736 Synopsis [Recursively searched for a satisfying assignment.]
737
738 Description []
739
740 SideEffects []
741
742 SeeAlso []
743
744 ***********************************************************************/
Pdr_NtkFindSatAssign_rec(Aig_Man_t * pAig,Aig_Obj_t * pNode,int Value,Pdr_Set_t * pCube,int Heur)745 int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur )
746 {
747 int Value0, Value1;
748 if ( Aig_ObjIsConst1(pNode) )
749 return 1;
750 if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
751 return ((int)pNode->fMarkA == Value);
752 Aig_ObjSetTravIdCurrent(pAig, pNode);
753 pNode->fMarkA = Value;
754 if ( Aig_ObjIsCi(pNode) )
755 {
756 if ( Saig_ObjIsLo(pAig, pNode) )
757 {
758 // pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
759 pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value );
760 pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
761 }
762 return 1;
763 }
764 assert( Aig_ObjIsNode(pNode) );
765 // propagation
766 if ( Value )
767 {
768 if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) )
769 return 0;
770 return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur);
771 }
772 // justification
773 Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
774 if ( Value0 == PDR_VAL0 )
775 return 1;
776 Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
777 if ( Value1 == PDR_VAL0 )
778 return 1;
779 if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 )
780 return 0;
781 if ( Value0 == PDR_VAL1 )
782 return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
783 if ( Value1 == PDR_VAL1 )
784 return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
785 assert( Value0 == PDR_VALX && Value1 == PDR_VALX );
786 // decision making
787 // if ( rand() % 10 == Heur )
788 if ( Aig_ObjId(pNode) % 4 == Heur )
789 return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
790 else
791 return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
792 }
793
794 ////////////////////////////////////////////////////////////////////////
795 /// END OF FILE ///
796 ////////////////////////////////////////////////////////////////////////
797
798
799 ABC_NAMESPACE_IMPL_END
800
801