ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaCSatP.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "giaCSatP.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
27//#define gia_assert(exp) ((void)0)
28//#define gia_assert(exp) (assert(exp))
29
33
34
35static inline int CbsP_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
36static inline void CbsP_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
37static inline void CbsP_VarUnassign( CbsP_Man_t * pMan, Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pMan->vValue->pArray[Gia_ObjId(pMan->pAig,pVar)] = ~0; }
38static inline int CbsP_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
39static inline void CbsP_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
40static inline int CbsP_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !CbsP_VarIsAssigned(Gia_ObjFanin0(pVar)) && !CbsP_VarIsAssigned(Gia_ObjFanin1(pVar)); }
41static inline int CbsP_VarFanin0Value( Gia_Obj_t * pVar ) { return !CbsP_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (CbsP_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
42static inline int CbsP_VarFanin1Value( Gia_Obj_t * pVar ) { return !CbsP_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (CbsP_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
43
44static inline int CbsP_VarDecLevel( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*Value); }
45static inline Gia_Obj_t * CbsP_VarReason0( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*Value+1); }
46static inline Gia_Obj_t * CbsP_VarReason1( CbsP_Man_t * p, Gia_Obj_t * pVar ) { int Value = p->vValue->pArray[Gia_ObjId(p->pAig,pVar)]; assert( Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*Value+2); }
47static inline int CbsP_ClauseDecLevel( CbsP_Man_t * p, int hClause ) { return CbsP_VarDecLevel( p, p->pClauses.pData[hClause] ); }
48
49#define CbsP_QueForEachEntry( Que, pObj, i ) \
50 for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
51
52#define CbsP_ClauseForEachVar( p, hClause, pObj ) \
53 for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
54#define CbsP_ClauseForEachVar1( p, hClause, pObj ) \
55 for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
56
60
72void CbsP_SetDefaultParams( CbsP_Par_t * pPars )
73{
74 memset( pPars, 0, sizeof(CbsP_Par_t) );
75 pPars->nBTLimit = 1000; // limit on the number of conflicts
76 pPars->nJustLimit = 100; // limit on the size of justification queue
77 pPars->fUseHighest = 1; // use node with the highest ID
78 pPars->fUseLowest = 0; // use node with the highest ID
79 pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
80 pPars->fVerbose = 1; // print detailed statistics
81
82 pPars->fUseProved = 1;
83
84
85 pPars->nJscanThis = 0;
86 pPars->nRscanThis = 0;
87 pPars->maxJscanUndec = 0;
88 pPars->maxRscanUndec = 0;
89 pPars->maxJscanSolved = 0;
90 pPars->maxRscanSolved = 0;
91
92
93 pPars->accJscanSat = 0;
94 pPars->accJscanUnsat = 0;
95 pPars->accJscanUndec = 0;
96 pPars->accRscanSat = 0;
97 pPars->accRscanUnsat = 0;
98 pPars->accRscanUndec = 0;
99 pPars->nSat = 0;
100 pPars->nUnsat = 0;
101 pPars->nUndec = 0;
102
103 pPars->nJscanLimit = 100;
104 pPars->nRscanLimit = 100;
105 pPars->nPropLimit = 500;
106}
107void CbsP_ManSetConflictNum( CbsP_Man_t * p, int Num )
108{
109 p->Pars.nBTLimit = Num;
110}
111
112static inline void CbsP_UpdateRecord( CbsP_Par_t * pPars, int res ){
113 if( CBS_UNDEC == res ){
114 pPars->nUndec ++ ;
115 if( pPars-> maxJscanUndec < pPars->nJscanThis )
116 pPars-> maxJscanUndec = pPars->nJscanThis;
117 if( pPars-> maxRscanUndec < pPars->nRscanThis )
118 pPars-> maxRscanUndec = pPars->nRscanThis;
119 if( pPars-> maxPropUndec < pPars->nPropThis )
120 pPars-> maxPropUndec = pPars->nPropThis;
121
122 pPars->accJscanUndec += pPars->nJscanThis;
123 pPars->accRscanUndec += pPars->nRscanThis;
124 pPars-> accPropUndec += pPars->nPropThis;
125 } else {
126 if( pPars->maxJscanSolved < pPars->nJscanThis )
127 pPars->maxJscanSolved = pPars->nJscanThis;
128 if( pPars->maxRscanSolved < pPars->nRscanThis )
129 pPars->maxRscanSolved = pPars->nRscanThis;
130 if( pPars-> maxPropSolved < pPars->nPropThis )
131 pPars-> maxPropSolved = pPars->nPropThis;
132 if( CBS_SAT == res ){
133 pPars->nSat ++ ;
134 pPars->accJscanSat += pPars->nJscanThis;
135 pPars->accRscanSat += pPars->nRscanThis;
136 pPars-> accPropSat += pPars->nPropThis;
137 } else
138 if( CBS_UNSAT == res ){
139 pPars->nUnsat ++ ;
140 pPars->accJscanUnsat += pPars->nJscanThis;
141 pPars->accRscanUnsat += pPars->nRscanThis;
142 pPars-> accPropUnsat += pPars->nPropThis;
143 }
144 }
145
146}
147
148void CbsP_PrintRecord( CbsP_Par_t * pPars ){
149 printf("max of solved: jscan# %13d rscan %13d prop %13d\n" , pPars->maxJscanSolved, pPars->maxRscanSolved , pPars->maxPropSolved );
150 printf("max of undec: jscan# %13d rscan %13d prop %13d\n" , pPars->maxJscanUndec , pPars->maxRscanUndec , pPars->maxPropUndec );
151 printf("acc of sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat , pPars->accRscanSat , pPars->accPropSat );
152 printf("acc of unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat , pPars->accRscanUnsat , pPars->accPropUnsat );
153 printf("acc of undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec , pPars->accRscanUndec , pPars->accPropUndec );
154 if( pPars->nSat )
155 printf("avg of sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat / pPars->nSat , pPars->accRscanSat / pPars->nSat , pPars->accPropSat / pPars->nSat );
156 if( pPars->nUnsat )
157 printf("avg of unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat / pPars->nUnsat , pPars->accRscanUnsat / pPars->nUnsat , pPars->accPropUnsat / pPars->nUnsat );
158 if( pPars->nUndec )
159 printf("avg of undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec / pPars->nUndec , pPars->accRscanUndec / pPars->nUndec , pPars->accPropUndec / pPars->nUndec );
160}
161
173CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia )
174{
175 CbsP_Man_t * p;
176 p = ABC_CALLOC( CbsP_Man_t, 1 );
177 p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
178 p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
179 p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
180 p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
181 p->pClauses.iHead = p->pClauses.iTail = 1;
182 p->vModel = Vec_IntAlloc( 1000 );
183 p->vLevReas = Vec_IntAlloc( 1000 );
184 p->vTemp = Vec_PtrAlloc( 1000 );
185 p->pAig = pGia;
186 p->vValue = Vec_IntAlloc( Gia_ManObjNum(pGia) );
187 Vec_IntFill( p->vValue, Gia_ManObjNum(pGia), ~0 );
188 //memset( p->vValue->pArray, (unsigned) ~0, sizeof(int) * Gia_ManObjNum(pGia) );
189 CbsP_SetDefaultParams( &p->Pars );
190 return p;
191}
192
204void CbsP_ManStop( CbsP_Man_t * p )
205{
206 Vec_IntFree( p->vLevReas );
207 Vec_IntFree( p->vModel );
208 Vec_PtrFree( p->vTemp );
209 Vec_IntFree( p->vValue );
210 ABC_FREE( p->pClauses.pData );
211 ABC_FREE( p->pProp.pData );
212 ABC_FREE( p->pJust.pData );
213 ABC_FREE( p );
214}
215
227Vec_Int_t * CbsP_ReadModel( CbsP_Man_t * p )
228{
229 return p->vModel;
230}
231
232
233
234
246
247static inline int CbsP_ManCheckPropLimits( CbsP_Man_t * p )
248{
249 return p->Pars.nPropThis > p->Pars.nPropLimit;
250}
251static inline int CbsP_ManCheckLimits( CbsP_Man_t * p )
252{
253 return CbsP_ManCheckPropLimits(p) || p->Pars.nJscanThis > p->Pars.nJscanLimit || p->Pars.nRscanThis > p->Pars.nRscanLimit || p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
254}
255
267static inline void CbsP_ManSaveModel( CbsP_Man_t * p, Vec_Int_t * vCex )
268{
269 Gia_Obj_t * pVar;
270 int i;
271 Vec_IntClear( vCex );
272 p->pProp.iHead = 0;
273 CbsP_QueForEachEntry( p->pProp, pVar, i )
274 if ( Gia_ObjIsCi(pVar) )
275 Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !CbsP_VarValue(pVar)) );
276// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !CbsP_VarValue(pVar)) );
277}
278static inline void CbsP_ManSaveModelAll( CbsP_Man_t * p, Vec_Int_t * vCex )
279{
280 Gia_Obj_t * pVar;
281 int i;
282 Vec_IntClear( vCex );
283 p->pProp.iHead = 0;
284 CbsP_QueForEachEntry( p->pProp, pVar, i )
285 Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !CbsP_VarValue(pVar)) );
286}
287
299static inline int CbsP_QueIsEmpty( CbsP_Que_t * p )
300{
301 return p->iHead == p->iTail;
302}
303
315static inline void CbsP_QuePush( CbsP_Que_t * p, Gia_Obj_t * pObj )
316{
317 assert( !Gia_IsComplement(pObj) );
318 if ( p->iTail == p->nSize )
319 {
320 p->nSize *= 2;
321 p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
322 }
323 p->pData[p->iTail++] = pObj;
324}
325
337static inline int CbsP_QueHasNode( CbsP_Que_t * p, Gia_Obj_t * pObj )
338{
339 Gia_Obj_t * pTemp;
340 int i;
341 CbsP_QueForEachEntry( *p, pTemp, i )
342 if ( pTemp == pObj )
343 return 1;
344 return 0;
345}
346
358static inline void CbsP_QueStore( CbsP_Que_t * p, int * piHeadOld, int * piTailOld )
359{
360 int i;
361 *piHeadOld = p->iHead;
362 *piTailOld = p->iTail;
363 for ( i = *piHeadOld; i < *piTailOld; i++ )
364 CbsP_QuePush( p, p->pData[i] );
365 p->iHead = *piTailOld;
366}
367
379static inline void CbsP_QueRestore( CbsP_Que_t * p, int iHeadOld, int iTailOld )
380{
381 p->iHead = iHeadOld;
382 p->iTail = iTailOld;
383}
384
396static inline int CbsP_QueFinish( CbsP_Que_t * p )
397{
398 int iHeadOld = p->iHead;
399 assert( p->iHead < p->iTail );
400 CbsP_QuePush( p, NULL );
401 p->iHead = p->iTail;
402 return iHeadOld;
403}
404
405
417static inline int CbsP_VarFaninFanoutMax( CbsP_Man_t * p, Gia_Obj_t * pObj )
418{
419 int Count0, Count1;
420 assert( !Gia_IsComplement(pObj) );
421 assert( Gia_ObjIsAnd(pObj) );
422 Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
423 Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
424 return Abc_MaxInt( Count0, Count1 );
425}
426
438static inline Gia_Obj_t * CbsP_ManDecideHighest( CbsP_Man_t * p )
439{
440 Gia_Obj_t * pObj, * pObjMax = NULL;
441 int i;
442 CbsP_QueForEachEntry( p->pJust, pObj, i )
443 if ( pObjMax == NULL || pObjMax < pObj )
444 pObjMax = pObj;
445 return pObjMax;
446}
447
459static inline Gia_Obj_t * CbsP_ManDecideLowest( CbsP_Man_t * p )
460{
461 Gia_Obj_t * pObj, * pObjMin = NULL;
462 int i;
463 CbsP_QueForEachEntry( p->pJust, pObj, i )
464 if ( pObjMin == NULL || pObjMin > pObj )
465 pObjMin = pObj;
466 return pObjMin;
467}
468
480static inline Gia_Obj_t * CbsP_ManDecideMaxFF( CbsP_Man_t * p )
481{
482 Gia_Obj_t * pObj, * pObjMax = NULL;
483 int i, iMaxFF = 0, iCurFF;
484 assert( p->pAig->pRefs != NULL );
485 CbsP_QueForEachEntry( p->pJust, pObj, i )
486 {
487 iCurFF = CbsP_VarFaninFanoutMax( p, pObj );
488 assert( iCurFF > 0 );
489 if ( iMaxFF < iCurFF )
490 {
491 iMaxFF = iCurFF;
492 pObjMax = pObj;
493 }
494 }
495 return pObjMax;
496}
497
498
499
511static inline void CbsP_ManCancelUntil( CbsP_Man_t * p, int iBound )
512{
513 Gia_Obj_t * pVar;
514 int i;
515 assert( iBound <= p->pProp.iTail );
516 p->pProp.iHead = iBound;
517 CbsP_QueForEachEntry( p->pProp, pVar, i )
518 CbsP_VarUnassign( p, pVar );
519 p->pProp.iTail = iBound;
520 Vec_IntShrink( p->vLevReas, 3*iBound );
521}
522
523//int s_Counter = 0;
524
536static inline void CbsP_ManAssign( CbsP_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
537{
538 Gia_Obj_t * pObjR = Gia_Regular(pObj);
539 assert( Gia_ObjIsCand(pObjR) );
540 assert( !CbsP_VarIsAssigned(pObjR) );
541 CbsP_VarAssign( pObjR );
542 CbsP_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
543 assert( p->vValue->pArray[Gia_ObjId(p->pAig,pObjR)] == ~0 );
544 p->vValue->pArray[Gia_ObjId(p->pAig,pObjR)] = p->pProp.iTail;
545 CbsP_QuePush( &p->pProp, pObjR );
546 Vec_IntPush( p->vLevReas, Level );
547 Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
548 Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
549 assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
550 if( pRes0 )
551 p->Pars.nPropThis ++ ;
552// s_Counter++;
553// s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
554}
555
556
568static inline int CbsP_ManClauseSize( CbsP_Man_t * p, int hClause )
569{
570 CbsP_Que_t * pQue = &(p->pClauses);
571 Gia_Obj_t ** pIter;
572 for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
573 return pIter - pQue->pData - hClause ;
574}
575
587static inline void CbsP_ManPrintClause( CbsP_Man_t * p, int Level, int hClause )
588{
589 CbsP_Que_t * pQue = &(p->pClauses);
590 Gia_Obj_t * pObj;
591 int i;
592 assert( CbsP_QueIsEmpty( pQue ) );
593 printf( "Level %2d : ", Level );
594 for ( i = hClause; (pObj = pQue->pData[i]); i++ )
595 printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), CbsP_VarValue(pObj), CbsP_VarDecLevel(p, pObj) );
596 printf( "\n" );
597}
598
610static inline void CbsP_ManPrintClauseNew( CbsP_Man_t * p, int Level, int hClause )
611{
612 CbsP_Que_t * pQue = &(p->pClauses);
613 Gia_Obj_t * pObj;
614 int i;
615 assert( CbsP_QueIsEmpty( pQue ) );
616 printf( "Level %2d : ", Level );
617 for ( i = hClause; (pObj = pQue->pData[i]); i++ )
618 printf( "%c%d ", CbsP_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
619 printf( "\n" );
620}
621
633static inline void CbsP_ManDeriveReason( CbsP_Man_t * p, int Level )
634{
635 CbsP_Que_t * pQue = &(p->pClauses);
636 Gia_Obj_t * pObj, * pReason;
637 int i, k, iLitLevel;
638 assert( pQue->pData[pQue->iHead] == NULL );
639 assert( pQue->iHead + 1 < pQue->iTail );
640/*
641 for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
642 {
643 pObj = pQue->pData[i];
644 assert( pObj->fMark0 == 1 );
645 }
646*/
647 // compact literals
648 Vec_PtrClear( p->vTemp );
649 for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
650 {
651 pObj = pQue->pData[i];
652 if ( !pObj->fMark0 ) // unassigned - seen again
653 continue;
654 // assigned - seen first time
655 pObj->fMark0 = 0;
656 Vec_PtrPush( p->vTemp, pObj );
657 // check decision level
658 iLitLevel = CbsP_VarDecLevel( p, pObj );
659 if ( iLitLevel < Level )
660 {
661 pQue->pData[k++] = pObj;
662 continue;
663 }
664 assert( iLitLevel == Level );
665 pReason = CbsP_VarReason0( p, pObj );
666 if ( pReason == pObj ) // no reason
667 {
668 //assert( pQue->pData[pQue->iHead] == NULL );
669 pQue->pData[pQue->iHead] = pObj;
670 continue;
671 }
672 CbsP_QuePush( pQue, pReason );
673 pReason = CbsP_VarReason1( p, pObj );
674 if ( pReason != pObj ) // second reason
675 CbsP_QuePush( pQue, pReason );
676 }
677 assert( pQue->pData[pQue->iHead] != NULL );
678 pQue->iTail = k;
679 // clear the marks
680 Vec_PtrForEachEntry( Gia_Obj_t *, p->vTemp, pObj, i )
681 pObj->fMark0 = 1;
682}
683
695static inline int CbsP_ManAnalyze( CbsP_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
696{
697 CbsP_Que_t * pQue = &(p->pClauses);
698 assert( CbsP_VarIsAssigned(pVar) );
699 assert( CbsP_VarIsAssigned(pFan0) );
700 assert( pFan1 == NULL || CbsP_VarIsAssigned(pFan1) );
701 assert( CbsP_QueIsEmpty( pQue ) );
702 CbsP_QuePush( pQue, NULL );
703 CbsP_QuePush( pQue, pVar );
704 CbsP_QuePush( pQue, pFan0 );
705 if ( pFan1 )
706 CbsP_QuePush( pQue, pFan1 );
707 CbsP_ManDeriveReason( p, Level );
708 return CbsP_QueFinish( pQue );
709}
710
711
723static inline int CbsP_ManResolve( CbsP_Man_t * p, int Level, int hClause0, int hClause1 )
724{
725 CbsP_Que_t * pQue = &(p->pClauses);
726 Gia_Obj_t * pObj;
727 int i, LevelMax = -1, LevelCur;
728 assert( pQue->pData[hClause0] != NULL );
729 assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
730/*
731 for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
732 assert( pObj->fMark0 == 1 );
733 for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
734 assert( pObj->fMark0 == 1 );
735*/
736 assert( CbsP_QueIsEmpty( pQue ) );
737 CbsP_QuePush( pQue, NULL );
738 for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
739 {
740 if ( !pObj->fMark0 ) // unassigned - seen again
741 continue;
742 // assigned - seen first time
743 pObj->fMark0 = 0;
744 CbsP_QuePush( pQue, pObj );
745 p->Pars.nRscanThis ++ ;
746 LevelCur = CbsP_VarDecLevel( p, pObj );
747 if ( LevelMax < LevelCur )
748 LevelMax = LevelCur;
749 }
750 for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
751 {
752 if ( !pObj->fMark0 ) // unassigned - seen again
753 continue;
754 // assigned - seen first time
755 pObj->fMark0 = 0;
756 CbsP_QuePush( pQue, pObj );
757 p->Pars.nRscanThis ++ ;
758 LevelCur = CbsP_VarDecLevel( p, pObj );
759 if ( LevelMax < LevelCur )
760 LevelMax = LevelCur;
761 }
762 for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
763 pQue->pData[i]->fMark0 = 1;
764 CbsP_ManDeriveReason( p, LevelMax );
765 return CbsP_QueFinish( pQue );
766}
767
779static inline int CbsP_ManPropagateOne( CbsP_Man_t * p, Gia_Obj_t * pVar, int Level )
780{
781 int Value0, Value1;
782 assert( !Gia_IsComplement(pVar) );
783 assert( CbsP_VarIsAssigned(pVar) );
784 if ( Gia_ObjIsCi(pVar) )
785 return 0;
786 assert( Gia_ObjIsAnd(pVar) );
787 Value0 = CbsP_VarFanin0Value(pVar);
788 Value1 = CbsP_VarFanin1Value(pVar);
789 if ( CbsP_VarValue(pVar) )
790 { // value is 1
791 if ( Value0 == 0 || Value1 == 0 ) // one is 0
792 {
793 if ( Value0 == 0 && Value1 != 0 )
794 return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
795 if ( Value0 != 0 && Value1 == 0 )
796 return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
797 assert( Value0 == 0 && Value1 == 0 );
798 return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
799 }
800 if ( Value0 == 2 ) // first is unassigned
801 CbsP_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
802 if ( Value1 == 2 ) // first is unassigned
803 CbsP_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
804 return 0;
805 }
806 // value is 0
807 if ( Value0 == 0 || Value1 == 0 ) // one is 0
808 return 0;
809 if ( Value0 == 1 && Value1 == 1 ) // both are 1
810 return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
811 if ( Value0 == 1 || Value1 == 1 ) // one is 1
812 {
813 if ( Value0 == 2 ) // first is unassigned
814 CbsP_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
815 if ( Value1 == 2 ) // second is unassigned
816 CbsP_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
817 return 0;
818 }
819 assert( CbsP_VarIsJust(pVar) );
820 assert( !CbsP_QueHasNode( &p->pJust, pVar ) );
821 CbsP_QuePush( &p->pJust, pVar );
822 return 0;
823}
824
836static inline int CbsP_ManPropagateTwo( CbsP_Man_t * p, Gia_Obj_t * pVar, int Level )
837{
838 int Value0, Value1;
839 assert( !Gia_IsComplement(pVar) );
840 assert( Gia_ObjIsAnd(pVar) );
841 assert( CbsP_VarIsAssigned(pVar) );
842 assert( !CbsP_VarValue(pVar) );
843 Value0 = CbsP_VarFanin0Value(pVar);
844 Value1 = CbsP_VarFanin1Value(pVar);
845 // value is 0
846 if ( Value0 == 0 || Value1 == 0 ) // one is 0
847 return 0;
848 if ( Value0 == 1 && Value1 == 1 ) // both are 1
849 return CbsP_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
850 assert( Value0 == 1 || Value1 == 1 );
851 if ( Value0 == 2 ) // first is unassigned
852 CbsP_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
853 if ( Value1 == 2 ) // first is unassigned
854 CbsP_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
855 return 0;
856}
857
869int CbsP_ManPropagate( CbsP_Man_t * p, int Level )
870{
871 int hClause;
872 Gia_Obj_t * pVar;
873 int i, k;
874 while ( 1 )
875 {
876 CbsP_QueForEachEntry( p->pProp, pVar, i )
877 {
878 if ( (hClause = CbsP_ManPropagateOne( p, pVar, Level )) )
879 return hClause;
880 if( CbsP_ManCheckPropLimits(p) )
881 return 0;
882 }
883 p->pProp.iHead = p->pProp.iTail;
884 k = p->pJust.iHead;
885 CbsP_QueForEachEntry( p->pJust, pVar, i )
886 {
887 if ( CbsP_VarIsJust( pVar ) )
888 p->pJust.pData[k++] = pVar;
889 else if ( (hClause = CbsP_ManPropagateTwo( p, pVar, Level )) )
890 return hClause;
891 if( CbsP_ManCheckPropLimits(p) )
892 return 0;
893 }
894 if ( k == p->pJust.iTail )
895 break;
896 p->pJust.iTail = k;
897 }
898 return 0;
899}
900
912int CbsP_ManSolve_rec( CbsP_Man_t * p, int Level )
913{
914 CbsP_Que_t * pQue = &(p->pClauses);
915 Gia_Obj_t * pVar = NULL, * pDecVar;
916 int hClause, hLearn0, hLearn1;
917 int iPropHead, iJustHead, iJustTail;
918 // propagate assignments
919 assert( !CbsP_QueIsEmpty(&p->pProp) );
920 if ( (hClause = CbsP_ManPropagate( p, Level )) )
921 return hClause;
922
923 // quit using resource limits
924 if ( CbsP_ManCheckLimits( p ) )
925 return 0;
926 // check for satisfying assignment
927 assert( CbsP_QueIsEmpty(&p->pProp) );
928 if ( CbsP_QueIsEmpty(&p->pJust) )
929 return 0;
930 p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
931 // remember the state before branching
932 iPropHead = p->pProp.iHead;
933 CbsP_QueStore( &p->pJust, &iJustHead, &iJustTail );
934 p->Pars.nJscanThis += iJustTail - iJustHead;
935 if ( CbsP_ManCheckLimits( p ) )
936 return 0;
937 // find the decision variable
938 if ( p->Pars.fUseHighest )
939 pVar = CbsP_ManDecideHighest( p );
940 else if ( p->Pars.fUseLowest )
941 pVar = CbsP_ManDecideLowest( p );
942 else if ( p->Pars.fUseMaxFF )
943 pVar = CbsP_ManDecideMaxFF( p );
944 else assert( 0 );
945 assert( CbsP_VarIsJust( pVar ) );
946 // chose decision variable using fanout count
947
948 if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
949 pDecVar = Gia_Not(Gia_ObjChild0(pVar));
950 else
951 pDecVar = Gia_Not(Gia_ObjChild1(pVar));
952
953// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
954// pDecVar = Gia_Not(pDecVar);
955 // decide on first fanin
956 CbsP_ManAssign( p, pDecVar, Level+1, NULL, NULL );
957 if ( !(hLearn0 = CbsP_ManSolve_rec( p, Level+1 )) )
958 return 0;
959 if ( CbsP_ManCheckLimits( p ) )
960 return 0;
961 if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
962 return hLearn0;
963 CbsP_ManCancelUntil( p, iPropHead );
964 CbsP_QueRestore( &p->pJust, iJustHead, iJustTail );
965 // decide on second fanin
966 CbsP_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
967 if ( !(hLearn1 = CbsP_ManSolve_rec( p, Level+1 )) )
968 return 0;
969 if ( CbsP_ManCheckLimits( p ) )
970 return 0;
971 if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
972 return hLearn1;
973 hClause = CbsP_ManResolve( p, Level, hLearn0, hLearn1 );
974// CbsP_ManPrintClauseNew( p, Level, hClause );
975// if ( Level > CbsP_ClauseDecLevel(p, hClause) )
976// p->Pars.nBTThisNc++;
977 p->Pars.nBTThis++;
978 return hClause;
979}
980
994int CbsP_ManSolve( CbsP_Man_t * p, Gia_Obj_t * pObj )
995{
996 int RetValue = 0;
997// s_Counter = 0;
998 assert( !p->pProp.iHead && !p->pProp.iTail );
999 assert( !p->pJust.iHead && !p->pJust.iTail );
1000 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1001 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1002 CbsP_ManAssign( p, pObj, 0, NULL, NULL );
1003 if ( !CbsP_ManSolve_rec(p, 0) && !CbsP_ManCheckLimits(p) )
1004 CbsP_ManSaveModel( p, p->vModel );
1005 else
1006 RetValue = 1;
1007 CbsP_ManCancelUntil( p, 0 );
1008 p->pJust.iHead = p->pJust.iTail = 0;
1009 p->pClauses.iHead = p->pClauses.iTail = 1;
1010 p->Pars.nBTTotal += p->Pars.nBTThis;
1011 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1012 if ( CbsP_ManCheckLimits( p ) )
1013 RetValue = -1;
1014// printf( "%d ", s_Counter );
1015 return RetValue;
1016}
1017int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
1018{
1019 abctime clk = Abc_Clock();
1020 int RetValue = 0;
1021// s_Counter = 0;
1022 assert( !p->pProp.iHead && !p->pProp.iTail );
1023 assert( !p->pJust.iHead && !p->pJust.iTail );
1024 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1025 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1026 p->Pars.nJscanThis = p->Pars.nRscanThis = p->Pars.nPropThis = 0;
1027 CbsP_ManAssign( p, pObj, 0, NULL, NULL );
1028 if ( pObj2 )
1029 CbsP_ManAssign( p, pObj2, 0, NULL, NULL );
1030 if ( !CbsP_ManSolve_rec(p, 0) && !CbsP_ManCheckLimits(p) )
1031 CbsP_ManSaveModel( p, p->vModel );
1032 else
1033 RetValue = 1;
1034 CbsP_ManCancelUntil( p, 0 );
1035
1036 p->pJust.iHead = p->pJust.iTail = 0;
1037 p->pClauses.iHead = p->pClauses.iTail = 1;
1038 p->Pars.nBTTotal += p->Pars.nBTThis;
1039 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1040 if ( CbsP_ManCheckLimits( p ) )
1041 RetValue = -1;
1042
1043 if( CBS_SAT == RetValue ){
1044 p->nSatSat ++;
1045 p->timeSatSat += Abc_Clock() - clk;
1046 p->nConfSat += p->Pars.nBTThis;
1047 } else
1048 if( CBS_UNSAT == RetValue ){
1049 p->nSatUnsat ++;
1050 p->timeSatUnsat += Abc_Clock() - clk;
1051 p->nConfUnsat += p->Pars.nBTThis;
1052 } else {
1053 p->nSatUndec ++;
1054 p->timeSatUndec += Abc_Clock() - clk;
1055 p->nConfUndec += p->Pars.nBTThis;
1056 }
1057// printf( "%d ", s_Counter );
1058 CbsP_UpdateRecord(&p->Pars,RetValue);
1059 return RetValue;
1060}
1061
1073void CbsP_ManSatPrintStats( CbsP_Man_t * p )
1074{
1075 printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
1076 printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
1077 printf( "Conf = %6d ", p->Pars.nBTLimit );
1078 printf( "JustMax = %5d ", p->Pars.nJustLimit );
1079 printf( "\n" );
1080 printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1081 p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
1082 ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
1083 printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1084 p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
1085 ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
1086 printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
1087 p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
1088 ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
1089 ABC_PRT( "Total time", p->timeTotal );
1090}
1091
1103Vec_Int_t * CbsP_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose )
1104{
1105 extern void Gia_ManCollectTest( Gia_Man_t * pAig );
1106 extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1107 CbsP_Man_t * p;
1108 Vec_Int_t * vCex, * vVisit, * vCexStore;
1109 Vec_Str_t * vStatus;
1110 Gia_Obj_t * pRoot;
1111 int i, status;
1112 abctime clk, clkTotal = Abc_Clock();
1113 assert( Gia_ManRegNum(pAig) == 0 );
1114// Gia_ManCollectTest( pAig );
1115 // prepare AIG
1116 Gia_ManCreateRefs( pAig );
1117 Gia_ManCleanMark0( pAig );
1118 Gia_ManCleanMark1( pAig );
1119 Gia_ManFillValue( pAig ); // maps nodes into trail ids
1120 Gia_ManSetPhase( pAig ); // maps nodes into trail ids
1121 // create logic network
1122 p = CbsP_ManAlloc( pAig );
1123 p->Pars.nBTLimit = nConfs;
1124 // create resulting data-structures
1125 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1126 vCexStore = Vec_IntAlloc( 10000 );
1127 vVisit = Vec_IntAlloc( 100 );
1128 vCex = CbsP_ReadModel( p );
1129 // solve for each output
1130 Gia_ManForEachCo( pAig, pRoot, i )
1131 {
1132// printf( "\n" );
1133
1134 Vec_IntClear( vCex );
1135 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
1136 {
1137 if ( Gia_ObjFaninC0(pRoot) )
1138 {
1139// printf( "Constant 1 output of SRM!!!\n" );
1140 Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
1141 Vec_StrPush( vStatus, 0 );
1142 }
1143 else
1144 {
1145// printf( "Constant 0 output of SRM!!!\n" );
1146 Vec_StrPush( vStatus, 1 );
1147 }
1148 continue;
1149 }
1150 clk = Abc_Clock();
1151 p->Pars.fUseHighest = 1;
1152 p->Pars.fUseLowest = 0;
1153 status = CbsP_ManSolve( p, Gia_ObjChild0(pRoot) );
1154// printf( "\n" );
1155/*
1156 if ( status == -1 )
1157 {
1158 p->Pars.fUseHighest = 0;
1159 p->Pars.fUseLowest = 1;
1160 status = CbsP_ManSolve( p, Gia_ObjChild0(pRoot) );
1161 }
1162*/
1163 Vec_StrPush( vStatus, (char)status );
1164 if ( status == -1 )
1165 {
1166 p->nSatUndec++;
1167 p->nConfUndec += p->Pars.nBTThis;
1168 Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1169 p->timeSatUndec += Abc_Clock() - clk;
1170 continue;
1171 }
1172 if ( status == 1 )
1173 {
1174 if ( f0Proved )
1175 Gia_ManPatchCoDriver( pAig, i, 0 );
1176 p->nSatUnsat++;
1177 p->nConfUnsat += p->Pars.nBTThis;
1178 p->timeSatUnsat += Abc_Clock() - clk;
1179 continue;
1180 }
1181 p->nSatSat++;
1182 p->nConfSat += p->Pars.nBTThis;
1183// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1184 Cec_ManSatAddToStore( vCexStore, vCex, i );
1185 p->timeSatSat += Abc_Clock() - clk;
1186 }
1187 Vec_IntFree( vVisit );
1188 p->nSatTotal = Gia_ManPoNum(pAig);
1189 p->timeTotal = Abc_Clock() - clkTotal;
1190 if ( fVerbose )
1191 CbsP_ManSatPrintStats( p );
1192// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
1193 CbsP_ManStop( p );
1194 *pvStatus = vStatus;
1195
1196// printf( "Total number of cex literals = %d. (Ave = %d)\n",
1197// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
1198// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
1199 return vCexStore;
1200}
1201
1202
1206
1207
1208ABC_NAMESPACE_IMPL_END
1209
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Cec_ManSatAddToStore
void Cec_ManSatAddToStore(Vec_Int_t *vCexStore, Vec_Int_t *vCex, int Out)
Definition cecSolve.c:996
p
Cube * p
Definition exorList.c:222
CbsP_ManSolve_rec
int CbsP_ManSolve_rec(CbsP_Man_t *p, int Level)
Definition giaCSatP.c:912
CbsP_ManAlloc
CbsP_Man_t * CbsP_ManAlloc(Gia_Man_t *pGia)
Definition giaCSatP.c:173
CbsP_PrintRecord
void CbsP_PrintRecord(CbsP_Par_t *pPars)
Definition giaCSatP.c:148
CbsP_ManStop
void CbsP_ManStop(CbsP_Man_t *p)
Definition giaCSatP.c:204
CbsP_SetDefaultParams
void CbsP_SetDefaultParams(CbsP_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition giaCSatP.c:72
CbsP_ManSatPrintStats
void CbsP_ManSatPrintStats(CbsP_Man_t *p)
Definition giaCSatP.c:1073
CbsP_QueForEachEntry
#define CbsP_QueForEachEntry(Que, pObj, i)
Definition giaCSatP.c:49
CbsP_ReadModel
Vec_Int_t * CbsP_ReadModel(CbsP_Man_t *p)
Definition giaCSatP.c:227
CbsP_ManPropagate
int CbsP_ManPropagate(CbsP_Man_t *p, int Level)
Definition giaCSatP.c:869
CbsP_ManSolve
int CbsP_ManSolve(CbsP_Man_t *p, Gia_Obj_t *pObj)
Definition giaCSatP.c:994
CbsP_ManSetConflictNum
void CbsP_ManSetConflictNum(CbsP_Man_t *p, int Num)
Definition giaCSatP.c:107
CbsP_ManSolve2
int CbsP_ManSolve2(CbsP_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pObj2)
Definition giaCSatP.c:1017
CbsP_ManSolveMiterNc
Vec_Int_t * CbsP_ManSolveMiterNc(Gia_Man_t *pAig, int nConfs, Vec_Str_t **pvStatus, int f0Proved, int fVerbose)
Definition giaCSatP.c:1103
CBS_UNSAT
#define CBS_UNSAT
Definition giaCSatP.h:110
CbsP_Man_t
struct CbsP_Man_t_ CbsP_Man_t
Definition giaCSatP.h:75
CBS_UNDEC
#define CBS_UNDEC
Definition giaCSatP.h:112
CbsP_Que_t
struct CbsP_Que_t_ CbsP_Que_t
Definition giaCSatP.h:66
CbsP_Par_t
typedefABC_NAMESPACE_HEADER_START struct CbsP_Par_t_ CbsP_Par_t
INCLUDES ///.
Definition giaCSatP.h:19
CBS_SAT
#define CBS_SAT
Definition giaCSatP.h:111
Gia_ManCollectTest
void Gia_ManCollectTest(Gia_Man_t *p)
Definition giaDfs.c:232
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition giaUtil.c:313
CbsP_Man_t_::vValue
Vec_Int_t * vValue
Definition giaCSatP.h:85
CbsP_Man_t_::pAig
Gia_Man_t * pAig
Definition giaCSatP.h:79
CbsP_Que_t_::iTail
int iTail
Definition giaCSatP.h:70
CbsP_Que_t_::iHead
int iHead
Definition giaCSatP.h:69
CbsP_Que_t_::pData
Gia_Obj_t ** pData
Definition giaCSatP.h:72
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55