ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaCSat3.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30typedef struct Cbs3_Par_t_ Cbs3_Par_t;
31struct Cbs3_Par_t_
32{
33 // conflict limits
34 int nBTLimit; // limit on the number of conflicts
35 int nJustLimit; // limit on the size of justification queue
36 int nRestLimit; // limit on the number of restarts
37 // current parameters
38 int nBTThis; // number of conflicts
39 int nJustThis; // max size of the frontier
40 int nBTTotal; // total number of conflicts
41 int nJustTotal; // total size of the frontier
42 // other
43 int fVerbose;
44};
45
46typedef struct Cbs3_Que_t_ Cbs3_Que_t;
47struct Cbs3_Que_t_
48{
49 int iHead; // beginning of the queue
50 int iTail; // end of the queue
51 int nSize; // allocated size
52 int * pData; // nodes stored in the queue
53};
54
55typedef struct Cbs3_Man_t_ Cbs3_Man_t;
56struct Cbs3_Man_t_
57{
58 Cbs3_Par_t Pars; // parameters
59 Gia_Man_t * pAig; // AIG manager
60 Cbs3_Que_t pProp; // propagation queue
61 Cbs3_Que_t pJust; // justification queue
62 Cbs3_Que_t pClauses; // clause queue
63 Vec_Int_t * vModel; // satisfying assignment
64 Vec_Int_t * vTemp; // temporary storage
65 // circuit structure
66 int nVars;
67 int nVarsAlloc;
68 int var_inc;
69 Vec_Int_t vMap;
70 Vec_Int_t vRef;
71 Vec_Int_t vFans;
72 Vec_Wec_t vImps;
73 // internal data
74 Vec_Str_t vAssign;
75 Vec_Str_t vMark;
76 Vec_Int_t vLevReason;
77 Vec_Int_t vActs;
78 Vec_Int_t vWatches;
79 Vec_Int_t vWatchUpds;
80 // SAT calls statistics
81 int nSatUnsat; // the number of proofs
82 int nSatSat; // the number of failure
83 int nSatUndec; // the number of timeouts
84 int nSatTotal; // the number of calls
85 // conflicts
86 int nConfUnsat; // conflicts in unsat problems
87 int nConfSat; // conflicts in sat problems
88 int nConfUndec; // conflicts in undec problems
89 // runtime stats
90 abctime timeJFront;
91 abctime timeSatLoad; // SAT solver loading time
92 abctime timeSatUnsat; // unsat
93 abctime timeSatSat; // sat
94 abctime timeSatUndec; // undecided
95 abctime timeTotal; // total runtime
96 // other statistics
97 int nPropCalls[3];
98 int nFails[2];
99 int nClauseConf;
100 int nDecs;
101};
102
103static inline int Cbs3_VarUnused( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; }
104static inline void Cbs3_VarSetUnused( Cbs3_Man_t * p, int iVar ) { Vec_IntWriteEntry(&p->vLevReason, 3*iVar, -1); }
105
106static inline int Cbs3_VarMark0( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vMark, iVar); }
107static inline void Cbs3_VarSetMark0( Cbs3_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vMark, iVar, (char)Value); }
108
109static inline int Cbs3_VarIsAssigned( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar) < 2; }
110static inline void Cbs3_VarUnassign( Cbs3_Man_t * p, int iVar ) { assert( Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)(2+Vec_StrEntry(&p->vAssign, iVar))); Cbs3_VarSetUnused(p, iVar); }
111
112static inline int Cbs3_VarValue( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar); }
113static inline void Cbs3_VarSetValue( Cbs3_Man_t * p, int iVar, int v ) { assert( !Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)v); }
114
115static inline int Cbs3_VarLit0( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) ); }
116static inline int Cbs3_VarLit1( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 1) ); }
117static inline int Cbs3_VarIsPi( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) ) == 0; }
118static inline int Cbs3_VarIsJust( Cbs3_Man_t * p, int iVar ) { int * pLits = Vec_IntEntryP(&p->vFans, Abc_Var2Lit(iVar, 0)); return pLits[0] > 0 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) >= 2 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[1])) >= 2; }
119
120static inline int Cbs3_VarDecLevel( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar); }
121static inline int Cbs3_VarReason0( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+1); }
122static inline int Cbs3_VarReason1( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+2); }
123static inline int * Cbs3_VarReasonP( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntryP(&p->vLevReason, 3*iVar+1); }
124static inline int Cbs3_ClauseDecLevel( Cbs3_Man_t * p, int hClause ) { return Cbs3_VarDecLevel( p, p->pClauses.pData[hClause] ); }
125
126static inline int Cbs3_ClauseSize( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData[hClause]; }
127static inline int * Cbs3_ClauseLits( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+1; }
128static inline int Cbs3_ClauseLit( Cbs3_Man_t * p, int hClause, int i ) { return p->pClauses.pData[hClause+1+i]; }
129static inline int * Cbs3_ClauseNext1p( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+Cbs3_ClauseSize(p, hClause)+2; }
130
131static inline void Cbs3_ClauseSetSize( Cbs3_Man_t * p, int hClause, int x ) { p->pClauses.pData[hClause] = x; }
132static inline void Cbs3_ClauseSetLit( Cbs3_Man_t * p, int hClause, int i, int x ) { p->pClauses.pData[hClause+i+1] = x; }
133static inline void Cbs3_ClauseSetNext( Cbs3_Man_t * p, int hClause, int n, int x ){ p->pClauses.pData[hClause+Cbs3_ClauseSize(p, hClause)+1+n] = x; }
134
135
136#define Cbs3_QueForEachEntry( Que, iObj, i ) \
137 for ( i = (Que).iHead; (i < (Que).iTail) && ((iObj) = (Que).pData[i]); i++ )
138
139#define Cbs3_ClauseForEachEntry( p, hClause, iObj, i ) \
140 for ( i = 1; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
141#define Cbs3_ClauseForEachEntry1( p, hClause, iObj, i ) \
142 for ( i = 2; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
143
147
159void Cbs3_SetDefaultParams( Cbs3_Par_t * pPars )
160{
161 memset( pPars, 0, sizeof(Cbs3_Par_t) );
162 pPars->nBTLimit = 1000; // limit on the number of conflicts
163 pPars->nJustLimit = 500; // limit on the size of justification queue
164 pPars->nRestLimit = 10; // limit on the number of restarts
165 pPars->fVerbose = 1; // print detailed statistics
166}
167void Cbs3_ManSetConflictNum( Cbs3_Man_t * p, int Num )
168{
169 p->Pars.nBTLimit = Num;
170}
171
183Cbs3_Man_t * Cbs3_ManAlloc( Gia_Man_t * pGia )
184{
185 Cbs3_Man_t * p;
186 p = ABC_CALLOC( Cbs3_Man_t, 1 );
187 p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
188 p->pProp.pData = ABC_ALLOC( int, p->pProp.nSize );
189 p->pJust.pData = ABC_ALLOC( int, p->pJust.nSize );
190 p->pClauses.pData = ABC_ALLOC( int, p->pClauses.nSize );
191 p->pClauses.iHead = p->pClauses.iTail = 1;
192 p->vModel = Vec_IntAlloc( 1000 );
193 p->vTemp = Vec_IntAlloc( 1000 );
194 p->pAig = pGia;
195 Cbs3_SetDefaultParams( &p->Pars );
196 // circuit structure
197 Vec_IntPush( &p->vMap, -1 );
198 Vec_IntPush( &p->vRef, -1 );
199 Vec_IntPushTwo( &p->vFans, -1, -1 );
200 Vec_WecPushLevel( &p->vImps );
201 Vec_WecPushLevel( &p->vImps );
202 p->nVars = 1;
203 // internal data
204 p->nVarsAlloc = 1000;
205 Vec_StrFill( &p->vAssign, p->nVarsAlloc, 2 );
206 Vec_StrFill( &p->vMark, p->nVarsAlloc, 0 );
207 Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
208 Vec_IntFill( &p->vActs, p->nVarsAlloc, 0 );
209 Vec_IntFill( &p->vWatches, 2*p->nVarsAlloc, 0 );
210 Vec_IntGrow( &p->vWatchUpds, 1000 );
211 return p;
212}
213static inline void Cbs3_ManReset( Cbs3_Man_t * p )
214{
215 assert( p->nVars == Vec_IntSize(&p->vMap) );
216 Vec_IntShrink( &p->vMap, 1 );
217 Vec_IntShrink( &p->vRef, 1 );
218 Vec_IntShrink( &p->vFans, 2 );
219 Vec_WecShrink( &p->vImps, 2 );
220 p->nVars = 1;
221}
222static inline void Cbs3_ManGrow( Cbs3_Man_t * p )
223{
224 if ( p->nVarsAlloc < p->nVars )
225 {
226 p->nVarsAlloc = 2*p->nVars;
227 Vec_StrFill( &p->vAssign, p->nVarsAlloc, 2 );
228 Vec_StrFill( &p->vMark, p->nVarsAlloc, 0 );
229 Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
230 Vec_IntFill( &p->vActs, p->nVarsAlloc, 0 );
231 Vec_IntFill( &p->vWatches, 2*p->nVarsAlloc, 0 );
232 }
233}
234
246void Cbs3_ManStop( Cbs3_Man_t * p )
247{
248 // circuit structure
249 Vec_IntErase( &p->vMap );
250 Vec_IntErase( &p->vRef );
251 Vec_IntErase( &p->vFans );
252 Vec_WecErase( &p->vImps );
253 // internal data
254 Vec_StrErase( &p->vAssign );
255 Vec_StrErase( &p->vMark );
256 Vec_IntErase( &p->vLevReason );
257 Vec_IntErase( &p->vActs );
258 Vec_IntErase( &p->vWatches );
259 Vec_IntErase( &p->vWatchUpds );
260 Vec_IntFree( p->vModel );
261 Vec_IntFree( p->vTemp );
262 ABC_FREE( p->pClauses.pData );
263 ABC_FREE( p->pProp.pData );
264 ABC_FREE( p->pJust.pData );
265 ABC_FREE( p );
266}
267int Cbs3_ManMemory( Cbs3_Man_t * p )
268{
269 int nMem = sizeof(Cbs3_Man_t);
270 nMem += (int)Vec_IntMemory( &p->vMap );
271 nMem += (int)Vec_IntMemory( &p->vRef );
272 nMem += (int)Vec_IntMemory( &p->vFans );
273 nMem += (int)Vec_WecMemory( &p->vImps );
274 nMem += (int)Vec_StrMemory( &p->vAssign );
275 nMem += (int)Vec_StrMemory( &p->vMark );
276 nMem += (int)Vec_IntMemory( &p->vActs );
277 nMem += (int)Vec_IntMemory( &p->vWatches );
278 nMem += (int)Vec_IntMemory( &p->vWatchUpds );
279 nMem += (int)Vec_IntMemory( p->vModel );
280 nMem += (int)Vec_IntMemory( p->vTemp );
281 nMem += 4*p->pClauses.nSize;
282 nMem += 4*p->pProp.nSize;
283 nMem += 4*p->pJust.nSize;
284 return nMem;
285}
286
298Vec_Int_t * Cbs3_ReadModel( Cbs3_Man_t * p )
299{
300 return p->vModel;
301}
302
303
315//#define USE_ACTIVITY
316
317#ifdef USE_ACTIVITY
318static inline void Cbs3_ActReset( Cbs3_Man_t * p )
319{
320 int i, * pAct = Vec_IntArray(&p->vActs);
321 for ( i = 0; i < p->nVars; i++ )
322 pAct[i] = (1 << 10);
323 p->var_inc = (1 << 5);
324}
325static inline void Cbs3_ActRescale( Cbs3_Man_t * p )
326{
327 int i, * pAct = Vec_IntArray(&p->vActs);
328 for ( i = 0; i < p->nVars; i++ )
329 pAct[i] >>= 19;
330 p->var_inc >>= 19;
331 p->var_inc = Abc_MaxInt( (unsigned)p->var_inc, (1<<5) );
332}
333static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar )
334{
335 int * pAct = Vec_IntArray(&p->vActs);
336 pAct[iVar] += p->var_inc;
337 if ((unsigned)pAct[iVar] & 0x80000000)
338 Cbs3_ActRescale(p);
339}
340static inline void Cbs3_ActDecay( Cbs3_Man_t * p )
341{
342 p->var_inc += (p->var_inc >> 4);
343}
344#else
345static inline void Cbs3_ActReset( Cbs3_Man_t * p ) {}
346static inline void Cbs3_ActRescale( Cbs3_Man_t * p ) {}
347static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar ) {}
348static inline void Cbs3_ActDecay( Cbs3_Man_t * p ) {}
349#endif
350
351
363static inline int Cbs3_ManCheckLimits( Cbs3_Man_t * p )
364{
365 p->nFails[0] += p->Pars.nJustThis > p->Pars.nJustLimit;
366 p->nFails[1] += p->Pars.nBTThis > p->Pars.nBTLimit;
367 return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
368}
369
381static inline void Cbs3_ManSaveModel( Cbs3_Man_t * p, Vec_Int_t * vCex )
382{
383 int i, iLit;
384 Vec_IntClear( vCex );
385 p->pProp.iHead = 0;
386 Cbs3_QueForEachEntry( p->pProp, iLit, i )
387 if ( Cbs3_VarIsPi(p, Abc_Lit2Var(iLit)) )
388 Vec_IntPush( vCex, Abc_Lit2LitV(Vec_IntArray(&p->vMap), iLit)-2 );
389}
390static inline void Cbs3_ManSaveModelAll( Cbs3_Man_t * p, Vec_Int_t * vCex )
391{
392 int i, iLit;
393 Vec_IntClear( vCex );
394 p->pProp.iHead = 0;
395 Cbs3_QueForEachEntry( p->pProp, iLit, i )
396 {
397 int iVar = Abc_Lit2Var(iLit);
398 Vec_IntPush( vCex, Abc_Var2Lit(iVar, !Cbs3_VarValue(p, iVar)) );
399 }
400}
401
413static inline int Cbs3_QueIsEmpty( Cbs3_Que_t * p )
414{
415 return p->iHead == p->iTail;
416}
417static inline int Cbs3_QueSize( Cbs3_Que_t * p )
418{
419 return p->iTail - p->iHead;
420}
421
433static inline void Cbs3_QuePush( Cbs3_Que_t * p, int iObj )
434{
435 if ( p->iTail == p->nSize )
436 {
437 p->nSize *= 2;
438 p->pData = ABC_REALLOC( int, p->pData, p->nSize );
439 }
440 p->pData[p->iTail++] = iObj;
441}
442static inline void Cbs3_QueGrow( Cbs3_Que_t * p, int Plus )
443{
444 if ( p->iTail + Plus > p->nSize )
445 {
446 p->nSize *= 2;
447 p->pData = ABC_REALLOC( int, p->pData, p->nSize );
448 }
449 assert( p->iTail + Plus <= p->nSize );
450}
451
463static inline int Cbs3_QueHasNode( Cbs3_Que_t * p, int iObj )
464{
465 int i, iTemp;
466 Cbs3_QueForEachEntry( *p, iTemp, i )
467 if ( iTemp == iObj )
468 return 1;
469 return 0;
470}
471
483static inline void Cbs3_QueStore( Cbs3_Que_t * p, int * piHeadOld, int * piTailOld )
484{
485 int i;
486 *piHeadOld = p->iHead;
487 *piTailOld = p->iTail;
488 for ( i = *piHeadOld; i < *piTailOld; i++ )
489 Cbs3_QuePush( p, p->pData[i] );
490 p->iHead = *piTailOld;
491}
492
504static inline void Cbs3_QueRestore( Cbs3_Que_t * p, int iHeadOld, int iTailOld )
505{
506 p->iHead = iHeadOld;
507 p->iTail = iTailOld;
508}
509
521static inline int Cbs3_ManDecide( Cbs3_Man_t * p )
522{
523 int i, iObj, iObjMax = 0;
524#ifdef USE_ACTIVITY
525 Cbs3_QueForEachEntry( p->pJust, iObj, i )
526 if ( iObjMax == 0 ||
527 Vec_IntEntry(&p->vActs, iObjMax) < Vec_IntEntry(&p->vActs, iObj) ||
528 (Vec_IntEntry(&p->vActs, iObjMax) == Vec_IntEntry(&p->vActs, iObj) && Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj)) )
529 iObjMax = iObj;
530#else
531 Cbs3_QueForEachEntry( p->pJust, iObj, i )
532// if ( iObjMax == 0 || iObjMax < iObj )
533 if ( iObjMax == 0 || Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj) )
534 iObjMax = iObj;
535#endif
536 return iObjMax;
537}
538
539
551static inline void Cbs3_ManCancelUntil( Cbs3_Man_t * p, int iBound )
552{
553 int i, iLit;
554 assert( iBound <= p->pProp.iTail );
555 p->pProp.iHead = iBound;
556 Cbs3_QueForEachEntry( p->pProp, iLit, i )
557 Cbs3_VarUnassign( p, Abc_Lit2Var(iLit) );
558 p->pProp.iTail = iBound;
559}
560
572static inline void Cbs3_ManAssign( Cbs3_Man_t * p, int iLit, int Level, int iRes0, int iRes1 )
573{
574 int iObj = Abc_Lit2Var(iLit);
575 assert( Cbs3_VarUnused(p, iObj) );
576 assert( !Cbs3_VarIsAssigned(p, iObj) );
577 Cbs3_VarSetValue( p, iObj, !Abc_LitIsCompl(iLit) );
578 Cbs3_QuePush( &p->pProp, iLit );
579 Vec_IntWriteEntry( &p->vLevReason, 3*iObj, Level );
580 Vec_IntWriteEntry( &p->vLevReason, 3*iObj+1, iRes0 );
581 Vec_IntWriteEntry( &p->vLevReason, 3*iObj+2, iRes1 );
582}
583
584
585
586
598static inline void Cbs3_ManPrintClause( Cbs3_Man_t * p, int Level, int hClause )
599{
600 int i, iLit;
601 assert( Cbs3_QueIsEmpty( &p->pClauses ) );
602 printf( "Level %2d : ", Level );
603 Cbs3_ClauseForEachEntry( p, hClause, iLit, i )
604 printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) );
605// printf( "%d=%d(%d) ", iObj, Cbs3_VarValue(p, Abc_Lit2Var(iLit)), Cbs3_VarDecLevel(p, Abc_Lit2Var(iLit)) );
606 printf( "\n" );
607}
608static inline void Cbs3_ManPrintCube( Cbs3_Man_t * p, int Level, int hClause )
609{
610 int i, iObj;
611 assert( Cbs3_QueIsEmpty( &p->pClauses ) );
612 printf( "Level %2d : ", Level );
613 Cbs3_ClauseForEachEntry( p, hClause, iObj, i )
614 printf( "%c%d ", Cbs3_VarValue(p, iObj)? '+':'-', iObj );
615 printf( "\n" );
616}
617
629static inline void Cbs3_ManCleanWatch( Cbs3_Man_t * p )
630{
631 int i, iLit;
632 Vec_IntForEachEntry( &p->vWatchUpds, iLit, i )
633 Vec_IntWriteEntry( &p->vWatches, iLit, 0 );
634 Vec_IntClear( &p->vWatchUpds );
635 //Vec_IntForEachEntry( &p->vWatches, iLit, i )
636 // assert( iLit == 0 );
637}
638static inline void Cbs3_ManWatchClause( Cbs3_Man_t * p, int hClause, int Lit )
639{
640 int * pLits = Cbs3_ClauseLits( p, hClause );
641 int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) );
642 if ( *pPlace == 0 )
643 Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) );
644/*
645 if ( pClause->pLits[0] == Lit )
646 pClause->pNext0 = p->pWatches[lit_neg(Lit)];
647 else
648 {
649 assert( pClause->pLits[1] == Lit );
650 pClause->pNext1 = p->pWatches[lit_neg(Lit)];
651 }
652 p->pWatches[lit_neg(Lit)] = pClause;
653*/
654 assert( Lit == pLits[0] || Lit == pLits[1] );
655 Cbs3_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace );
656 *pPlace = hClause;
657}
658static inline int Cbs3_QueFinish( Cbs3_Man_t * p, int Level )
659{
660 Cbs3_Que_t * pQue = &(p->pClauses);
661 int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
662 assert( pQue->iHead+1 < pQue->iTail );
663 Cbs3_ClauseSetSize( p, pQue->iHead, Size );
664 hClauseC = pQue->iHead = pQue->iTail;
665 //printf( "Adding cube: " ); Cbs3_ManPrintCube(p, Level, hClause);
666 if ( Size == 1 )
667 return hClause;
668 // create watched clause
669 pQue->iHead = hClause;
670 Cbs3_QueForEachEntry( p->pClauses, iObj, i )
671 {
672 if ( i == hClauseC )
673 break;
674 else if ( i == hClause ) // nlits
675 Cbs3_QuePush( pQue, iObj );
676 else // literals
677 Cbs3_QuePush( pQue, Abc_Var2Lit(iObj, Cbs3_VarValue(p, iObj)) ); // complement
678 }
679 Cbs3_QuePush( pQue, 0 ); // next0
680 Cbs3_QuePush( pQue, 0 ); // next1
681 pQue->iHead = pQue->iTail;
682 Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 0) );
683 Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 1) );
684 //printf( "Adding clause %d: ", hClauseC ); Cbs3_ManPrintClause(p, Level, hClauseC);
685 Cbs3_ActDecay( p );
686 return hClause;
687}
688
700static inline int Cbs3_ManDeriveReason( Cbs3_Man_t * p, int Level )
701{
702 Cbs3_Que_t * pQue = &(p->pClauses);
703 int i, k, iObj, iLitLevel, * pReason;
704 assert( pQue->pData[pQue->iHead] == 0 );
705 assert( pQue->pData[pQue->iHead+1] == 0 );
706 assert( pQue->iHead + 2 < pQue->iTail );
707 //for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
708 // assert( !Cbs3_VarMark0(p, pQue->pData[i]) );
709 // compact literals
710 Vec_IntClear( p->vTemp );
711 for ( i = k = pQue->iHead + 2; i < pQue->iTail; i++ )
712 {
713 iObj = pQue->pData[i];
714 if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
715 continue;
716 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
717 // Vec_IntPush( &p->vActStore, iObj );
718 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
719 // assigned - seen first time
720 Cbs3_VarSetMark0(p, iObj, 1);
721 Cbs3_ActBumpVar(p, iObj);
722 Vec_IntPush( p->vTemp, iObj );
723 // check decision level
724 iLitLevel = Cbs3_VarDecLevel( p, iObj );
725 if ( iLitLevel < Level )
726 {
727 pQue->pData[k++] = iObj;
728 continue;
729 }
730 assert( iLitLevel == Level );
731 pReason = Cbs3_VarReasonP( p, iObj );
732 if ( pReason[0] == 0 && pReason[1] == 0 ) // no reason
733 {
734 assert( pQue->pData[pQue->iHead+1] == 0 );
735 pQue->pData[pQue->iHead+1] = iObj;
736 }
737 else if ( pReason[0] != 0 ) // circuit reason
738 {
739 Cbs3_QuePush( pQue, pReason[0] );
740 if ( pReason[1] )
741 Cbs3_QuePush( pQue, pReason[1] );
742 }
743 else // clause reason
744 {
745 int i, * pLits, nLits = Cbs3_ClauseSize( p, pReason[1] );
746 assert( pReason[1] );
747 Cbs3_QueGrow( pQue, nLits );
748 pLits = Cbs3_ClauseLits( p, pReason[1] );
749 assert( iObj == Abc_Lit2Var(pLits[0]) );
750 for ( i = 1; i < nLits; i++ )
751 Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
752 }
753 }
754 assert( pQue->pData[pQue->iHead] == 0 );
755 assert( pQue->pData[pQue->iHead+1] != 0 );
756 pQue->iTail = k;
757 // clear the marks
758 Vec_IntForEachEntry( p->vTemp, iObj, i )
759 Cbs3_VarSetMark0(p, iObj, 0);
760 return Cbs3_QueFinish( p, Level );
761}
762static inline int Cbs3_ManAnalyze( Cbs3_Man_t * p, int Level, int iVar, int iFan0, int iFan1 )
763{
764 Cbs3_Que_t * pQue = &(p->pClauses);
765 assert( Cbs3_VarIsAssigned(p, iVar) );
766 assert( Cbs3_QueIsEmpty( pQue ) );
767 Cbs3_QuePush( pQue, 0 );
768 Cbs3_QuePush( pQue, 0 );
769 if ( iFan0 ) // circuit conflict
770 {
771 assert( Cbs3_VarIsAssigned(p, iFan0) );
772 assert( iFan1 == 0 || Cbs3_VarIsAssigned(p, iFan1) );
773 Cbs3_QuePush( pQue, iVar );
774 Cbs3_QuePush( pQue, iFan0 );
775 if ( iFan1 )
776 Cbs3_QuePush( pQue, iFan1 );
777 }
778 else // clause conflict
779 {
780 int i, * pLits, nLits = Cbs3_ClauseSize( p, iFan1 );
781 assert( iFan1 );
782 Cbs3_QueGrow( pQue, nLits );
783 pLits = Cbs3_ClauseLits( p, iFan1 );
784 assert( iVar == Abc_Lit2Var(pLits[0]) );
785 assert( Cbs3_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) );
786 for ( i = 0; i < nLits; i++ )
787 Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
788 }
789 return Cbs3_ManDeriveReason( p, Level );
790}
791
792
804static inline int Cbs3_ManPropagateClauses( Cbs3_Man_t * p, int Level, int Lit )
805{
806 int i, Value, Cur, LitF = Abc_LitNot(Lit);
807 int * pPrev = Vec_IntEntryP( &p->vWatches, Lit );
808 //for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
809 for ( Cur = *pPrev; Cur; Cur = *pPrev )
810 {
811 int nLits = Cbs3_ClauseSize( p, Cur );
812 int * pLits = Cbs3_ClauseLits( p, Cur );
813 p->nPropCalls[1]++;
814//printf( " Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level );
815 // make sure the false literal is in the second literal of the clause
816 //if ( pCur->pLits[0] == LitF )
817 if ( pLits[0] == LitF )
818 {
819 //pCur->pLits[0] = pCur->pLits[1];
820 pLits[0] = pLits[1];
821 //pCur->pLits[1] = LitF;
822 pLits[1] = LitF;
823 //pTemp = pCur->pNext0;
824 //pCur->pNext0 = pCur->pNext1;
825 //pCur->pNext1 = pTemp;
826 ABC_SWAP( int, pLits[nLits], pLits[nLits+1] );
827 }
828 //assert( pCur->pLits[1] == LitF );
829 assert( pLits[1] == LitF );
830
831 // if the first literal is true, the clause is satisfied
832 //if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
833 if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) == !Abc_LitIsCompl(pLits[0]) )
834 {
835 //ppPrev = &pCur->pNext1;
836 pPrev = Cbs3_ClauseNext1p(p, Cur);
837 continue;
838 }
839
840 // look for a new literal to watch
841 for ( i = 2; i < nLits; i++ )
842 {
843 // skip the case when the literal is false
844 //if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
845 if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[i])) == Abc_LitIsCompl(pLits[i]) )
846 continue;
847 // the literal is either true or unassigned - watch it
848 //pCur->pLits[1] = pCur->pLits[i];
849 //pCur->pLits[i] = LitF;
850 pLits[1] = pLits[i];
851 pLits[i] = LitF;
852 // remove this clause from the watch list of Lit
853 //*ppPrev = pCur->pNext1;
854 *pPrev = *Cbs3_ClauseNext1p(p, Cur);
855 // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
856 //Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
857 Cbs3_ManWatchClause( p, Cur, Cbs3_ClauseLit(p, Cur, 1) );
858 break;
859 }
860 if ( i < nLits ) // found new watch
861 continue;
862
863 // clause is unit - enqueue new implication
864 //if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
865 //{
866 // ppPrev = &pCur->pNext1;
867 // continue;
868 //}
869
870 // clause is unit - enqueue new implication
871 Value = Cbs3_VarValue(p, Abc_Lit2Var(pLits[0]));
872 if ( Value >= 2 ) // unassigned
873 {
874 Cbs3_ManAssign( p, pLits[0], Level, 0, Cur );
875 pPrev = Cbs3_ClauseNext1p(p, Cur);
876 continue;
877 }
878
879 // conflict detected - return the conflict clause
880 //return pCur;
881 if ( Value == Abc_LitIsCompl(pLits[0]) )
882 {
883 p->nClauseConf++;
884 return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur );
885 }
886 }
887 return 0;
888}
889
890
902static inline int Cbs3_ManResolve( Cbs3_Man_t * p, int Level, int hClause0, int hClause1 )
903{
904 Cbs3_Que_t * pQue = &(p->pClauses);
905 int i, iObj, LevelMax = -1, LevelCur;
906 assert( pQue->pData[hClause0+1] != 0 );
907 assert( pQue->pData[hClause0+1] == pQue->pData[hClause1+1] );
908 //Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
909 // assert( !Cbs3_VarMark0(p, iObj) );
910 //Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
911 // assert( !Cbs3_VarMark0(p, iObj) );
912 assert( Cbs3_QueIsEmpty( pQue ) );
913 Cbs3_QuePush( pQue, 0 );
914 Cbs3_QuePush( pQue, 0 );
915// for ( i = hClause0 + 1; (iObj = pQue->pData[i]); i++ )
916 Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
917 {
918 if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
919 continue;
920 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
921 // Vec_IntPush( &p->vActStore, iObj );
922 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
923 // assigned - seen first time
924 Cbs3_VarSetMark0(p, iObj, 1);
925 Cbs3_ActBumpVar(p, iObj);
926 Cbs3_QuePush( pQue, iObj );
927 LevelCur = Cbs3_VarDecLevel( p, iObj );
928 if ( LevelMax < LevelCur )
929 LevelMax = LevelCur;
930 }
931// for ( i = hClause1 + 1; (iObj = pQue->pData[i]); i++ )
932 Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
933 {
934 if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
935 continue;
936 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
937 // Vec_IntPush( &p->vActStore, iObj );
938 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
939 // assigned - seen first time
940 Cbs3_VarSetMark0(p, iObj, 1);
941 Cbs3_ActBumpVar(p, iObj);
942 Cbs3_QuePush( pQue, iObj );
943 LevelCur = Cbs3_VarDecLevel( p, iObj );
944 if ( LevelMax < LevelCur )
945 LevelMax = LevelCur;
946 }
947 for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
948 Cbs3_VarSetMark0(p, pQue->pData[i], 0);
949 return Cbs3_ManDeriveReason( p, LevelMax );
950}
951
963void Cbs3_ManUpdateJFrontier( Cbs3_Man_t * p )
964{
965 //abctime clk = Abc_Clock();
966 int iVar, iLit, i, k = p->pJust.iTail;
967 Cbs3_QueGrow( &p->pJust, Cbs3_QueSize(&p->pJust) + Cbs3_QueSize(&p->pProp) );
968 Cbs3_QueForEachEntry( p->pJust, iVar, i )
969 if ( Cbs3_VarIsJust(p, iVar) )
970 p->pJust.pData[k++] = iVar;
971 Cbs3_QueForEachEntry( p->pProp, iLit, i )
972 if ( Cbs3_VarIsJust(p, Abc_Lit2Var(iLit)) )
973 p->pJust.pData[k++] = Abc_Lit2Var(iLit);
974 p->pJust.iHead = p->pJust.iTail;
975 p->pJust.iTail = k;
976 //p->timeJFront += Abc_Clock() - clk;
977}
978int Cbs3_ManPropagateNew( Cbs3_Man_t * p, int Level )
979{
980 int i, k, iLit, hClause, nLits, * pLits;
981 p->nPropCalls[0]++;
982 Cbs3_QueForEachEntry( p->pProp, iLit, i )
983 {
984 if ( (hClause = Cbs3_ManPropagateClauses(p, Level, iLit)) )
985 return hClause;
986 p->nPropCalls[2]++;
987 nLits = Vec_IntSize(Vec_WecEntry(&p->vImps, iLit));
988 pLits = Vec_IntArray(Vec_WecEntry(&p->vImps, iLit));
989 for ( k = 0; k < nLits; k += 2 )
990 {
991 int Value0 = Cbs3_VarValue(p, Abc_Lit2Var(pLits[k]));
992 int Value1 = pLits[k+1] ? Cbs3_VarValue(p, Abc_Lit2Var(pLits[k+1])) : -1;
993 if ( Value1 == -1 || Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
994 {
995 if ( Value0 >= 2 ) // pLits[k] is unassigned
996 Cbs3_ManAssign( p, pLits[k], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k+1]) );
997 else if ( Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
998 return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
999 }
1000 if ( Value1 != -1 && Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
1001 {
1002 if ( Value1 >= 2 ) // pLits[k+1] is unassigned
1003 Cbs3_ManAssign( p, pLits[k+1], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]) );
1004 else if ( Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
1005 return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
1006 }
1007 }
1008 }
1009 Cbs3_ManUpdateJFrontier( p );
1010 // finalize propagation queue
1011 p->pProp.iHead = p->pProp.iTail;
1012 return 0;
1013}
1014
1026int Cbs3_ManSolve2_rec( Cbs3_Man_t * p, int Level )
1027{
1028 Cbs3_Que_t * pQue = &(p->pClauses);
1029 int iPropHead, iJustHead, iJustTail;
1030 int hClause, hLearn0, hLearn1, iVar, iDecLit;
1031 int nRef0, nRef1;
1032 // propagate assignments
1033 assert( !Cbs3_QueIsEmpty(&p->pProp) );
1034 //if ( (hClause = Cbs3_ManPropagate( p, Level )) )
1035 if ( (hClause = Cbs3_ManPropagateNew( p, Level )) )
1036 return hClause;
1037 // check for satisfying assignment
1038 assert( Cbs3_QueIsEmpty(&p->pProp) );
1039 if ( Cbs3_QueIsEmpty(&p->pJust) )
1040 return 0;
1041 // quit using resource limits
1042 p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
1043 if ( Cbs3_ManCheckLimits( p ) )
1044 return 0;
1045 // remember the state before branching
1046 iPropHead = p->pProp.iHead;
1047 iJustHead = p->pJust.iHead;
1048 iJustTail = p->pJust.iTail;
1049 // find the decision variable
1050 p->nDecs++;
1051 iVar = Cbs3_ManDecide( p );
1052 assert( !Cbs3_VarIsPi(p, iVar) );
1053 assert( Cbs3_VarIsJust(p, iVar) );
1054 // chose decision variable using fanout count
1055 nRef0 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit0(p, iVar)));
1056 nRef1 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit1(p, iVar)));
1057// if ( nRef0 >= nRef1 || (nRef0 == nRef1) && (Abc_Random(0) & 1) )
1058 if ( nRef0 >= nRef1 )
1059 iDecLit = Abc_LitNot(Cbs3_VarLit0(p, iVar));
1060 else
1061 iDecLit = Abc_LitNot(Cbs3_VarLit1(p, iVar));
1062 // decide on first fanin
1063 Cbs3_ManAssign( p, iDecLit, Level+1, 0, 0 );
1064 if ( !(hLearn0 = Cbs3_ManSolve2_rec( p, Level+1 )) )
1065 return 0;
1066 if ( pQue->pData[hLearn0+1] != Abc_Lit2Var(iDecLit) )
1067 return hLearn0;
1068 Cbs3_ManCancelUntil( p, iPropHead );
1069 Cbs3_QueRestore( &p->pJust, iJustHead, iJustTail );
1070 // decide on second fanin
1071 Cbs3_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 );
1072 if ( !(hLearn1 = Cbs3_ManSolve2_rec( p, Level+1 )) )
1073 return 0;
1074 if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) )
1075 return hLearn1;
1076 hClause = Cbs3_ManResolve( p, Level, hLearn0, hLearn1 );
1077 p->Pars.nBTThis++;
1078 return hClause;
1079}
1080
1092static inline int Cbs3_ManSolveInt( Cbs3_Man_t * p, int iLit )
1093{
1094 int RetValue = 0;
1095 assert( !p->pProp.iHead && !p->pProp.iTail );
1096 assert( !p->pJust.iHead && !p->pJust.iTail );
1097 p->Pars.nBTThis = p->Pars.nJustThis = 0;
1098 Cbs3_ManAssign( p, iLit, 0, 0, 0 );
1099 if ( !Cbs3_ManSolve2_rec(p, 0) && !Cbs3_ManCheckLimits(p) )
1100 Cbs3_ManSaveModel( p, p->vModel );
1101 else
1102 RetValue = 1;
1103 Cbs3_ManCancelUntil( p, 0 );
1104 p->pJust.iHead = p->pJust.iTail = 0;
1105 p->Pars.nBTTotal += p->Pars.nBTThis;
1106 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1107 if ( Cbs3_ManCheckLimits( p ) )
1108 RetValue = -1;
1109 return RetValue;
1110}
1111int Cbs3_ManSolve( Cbs3_Man_t * p, int iLit, int nRestarts )
1112{
1113 int i, RetValue = -1;
1114 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1115 for ( i = 0; i < nRestarts; i++ )
1116 if ( (RetValue = Cbs3_ManSolveInt(p, iLit)) != -1 )
1117 break;
1118 Cbs3_ManCleanWatch( p );
1119 p->pClauses.iHead = p->pClauses.iTail = 1;
1120 return RetValue;
1121}
1122
1134void Cbs3_ManSatPrintStats( Cbs3_Man_t * p )
1135{
1136 printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
1137 printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
1138 printf( "Conf = %6d ", p->Pars.nBTLimit );
1139 printf( "Restart = %2d ", p->Pars.nRestLimit );
1140 printf( "JustMax = %5d ", p->Pars.nJustLimit );
1141 printf( "\n" );
1142 printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1143 p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
1144 ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
1145 printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1146 p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
1147 ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
1148 printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
1149 p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
1150 ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
1151 ABC_PRT( "Total time", p->timeTotal );
1152}
1153
1154
1166static inline int Cbs3_ManAddVar( Cbs3_Man_t * p, int iGiaObj )
1167{
1168 assert( Vec_IntSize(&p->vMap) == p->nVars );
1169 Vec_IntPush( &p->vMap, iGiaObj );
1170 Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
1171 Vec_IntPushTwo( &p->vFans, 0, 0 );
1172 Vec_WecPushLevel(&p->vImps);
1173 Vec_WecPushLevel(&p->vImps);
1174 return Abc_Var2Lit( p->nVars++, 0 );
1175}
1176static inline void Cbs3_ManAddConstr( Cbs3_Man_t * p, int x, int x0, int x1 )
1177{
1178 Vec_WecPushTwo( &p->vImps, x , x0, 0 ); // ~x + x0
1179 Vec_WecPushTwo( &p->vImps, x , x1, 0 ); // ~x + x1
1180 Vec_WecPushTwo( &p->vImps, 1^x0, 1^x , 0 ); // ~x + x0
1181 Vec_WecPushTwo( &p->vImps, 1^x1, 1^x , 0 ); // ~x + x1
1182 Vec_WecPushTwo( &p->vImps, 1^x , 1^x0, 1^x1 ); // x + ~x0 + ~x1
1183 Vec_WecPushTwo( &p->vImps, x0, x , 1^x1 ); // x + ~x0 + ~x1
1184 Vec_WecPushTwo( &p->vImps, x1, x , 1^x0 ); // x + ~x0 + ~x1
1185}
1186static inline void Cbs3_ManAddAnd( Cbs3_Man_t * p, int x, int x0, int x1 )
1187{
1188 assert( x > 0 && x0 > 0 && x1 > 0 );
1189 Vec_IntWriteEntry( &p->vFans, x, x0 );
1190 Vec_IntWriteEntry( &p->vFans, x+1, x1 );
1191 Cbs3_ManAddConstr( p, x, x0, x1 );
1192}
1193static inline int Cbs3_ManToSolver1_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
1194{
1195 Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
1196 if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
1197 return pObj->Value;
1198 pObj->Value = Cbs3_ManAddVar( pSol, iObj );
1199 if ( Gia_ObjIsCi(pObj) || Depth == 0 )
1200 return pObj->Value;
1201 assert( Gia_ObjIsAnd(pObj) );
1202 Lit0 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
1203 Lit1 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
1204 Cbs3_ManAddAnd( pSol, pObj->Value, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj) );
1205 return pObj->Value;
1206}
1207static inline int Cbs3_ManToSolver1( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
1208{
1209 //abctime clk = Abc_Clock();
1210 assert( Gia_ObjIsCo(pRoot) );
1211 Cbs3_ManReset( pSol );
1212 Gia_ManIncrementTravId( p );
1213 Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
1214 Cbs3_ManGrow( pSol );
1215 Cbs3_ActReset( pSol );
1216 //pSol->timeSatLoad += Abc_Clock() - clk;
1217 return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
1218}
1219
1231static inline void Cbs3_ManPrepare( Cbs3_Man_t * p )
1232{
1233 int x, x0, x1;
1234 Vec_WecInit( &p->vImps, Abc_Var2Lit(p->nVars, 0) );
1235 Vec_IntForEachEntryDoubleStart( &p->vFans, x0, x1, x, 2 )
1236 if ( x0 ) Cbs3_ManAddConstr( p, x, x0, x1 );
1237}
1238static inline int Cbs3_ManAddNode( Cbs3_Man_t * p, int iGiaObj, int iLit0, int iLit1 )
1239{
1240 assert( Vec_IntSize(&p->vMap) == p->nVars );
1241 Vec_IntPush( &p->vMap, iGiaObj );
1242 Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
1243 Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
1244 return Abc_Var2Lit( p->nVars++, 0 );
1245}
1246static inline int Cbs3_ManToSolver2_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
1247{
1248 Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
1249 if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
1250 return pObj->Value;
1251 if ( Gia_ObjIsCi(pObj) || Depth == 0 )
1252 return pObj->Value = Cbs3_ManAddNode(pSol, iObj, 0, 0);
1253 assert( Gia_ObjIsAnd(pObj) );
1254 Lit0 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
1255 Lit1 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
1256 return pObj->Value = Cbs3_ManAddNode(pSol, iObj, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj));
1257}
1258static inline int Cbs3_ManToSolver2( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
1259{
1260 //abctime clk = Abc_Clock();
1261 assert( Gia_ObjIsCo(pRoot) );
1262 Cbs3_ManReset( pSol );
1263 Gia_ManIncrementTravId( p );
1264 Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
1265 Cbs3_ManGrow( pSol );
1266 Cbs3_ManPrepare( pSol );
1267 Cbs3_ActReset( pSol );
1268 //pSol->timeSatLoad += Abc_Clock() - clk;
1269 return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
1270}
1271
1272
1284Vec_Int_t * Cbs3_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, int nRestarts, Vec_Str_t ** pvStatus, int fVerbose )
1285{
1286 extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1287 Cbs3_Man_t * p;
1288 Vec_Int_t * vCex, * vVisit, * vCexStore;
1289 Vec_Str_t * vStatus;
1290 Gia_Obj_t * pRoot;
1291 int i, status; // 1 = unsat, 0 = sat, -1 = undec
1292 abctime clk, clkTotal = Abc_Clock();
1293 //assert( Gia_ManRegNum(pAig) == 0 );
1294 Gia_ManCreateRefs( pAig );
1295 //Gia_ManLevelNum( pAig );
1296 // create logic network
1297 p = Cbs3_ManAlloc( pAig );
1298 p->Pars.nBTLimit = nConfs;
1299 p->Pars.nRestLimit = nRestarts;
1300 // create resulting data-structures
1301 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1302 vCexStore = Vec_IntAlloc( 10000 );
1303 vVisit = Vec_IntAlloc( 100 );
1304 vCex = Cbs3_ReadModel( p );
1305 // solve for each output
1306 Gia_ManForEachCo( pAig, pRoot, i )
1307 {
1308 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
1309 {
1310 Vec_IntClear( vCex );
1311 Vec_StrPush( vStatus, (char)(!Gia_ObjFaninC0(pRoot)) );
1312 if ( Gia_ObjFaninC0(pRoot) ) // const1
1313 Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
1314 continue;
1315 }
1316 clk = Abc_Clock();
1317 status = Cbs3_ManToSolver2( p, pAig, pRoot, p->Pars.nRestLimit, 10000 );
1318 Vec_StrPush( vStatus, (char)status );
1319 if ( status == -1 )
1320 {
1321 p->nSatUndec++;
1322 p->nConfUndec += p->Pars.nBTThis;
1323 Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1324 p->timeSatUndec += Abc_Clock() - clk;
1325 continue;
1326 }
1327 if ( status == 1 )
1328 {
1329 p->nSatUnsat++;
1330 p->nConfUnsat += p->Pars.nBTThis;
1331 p->timeSatUnsat += Abc_Clock() - clk;
1332 continue;
1333 }
1334 p->nSatSat++;
1335 p->nConfSat += p->Pars.nBTThis;
1336 //Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1337 Cec_ManSatAddToStore( vCexStore, vCex, i );
1338 p->timeSatSat += Abc_Clock() - clk;
1339 }
1340 Vec_IntFree( vVisit );
1341 p->nSatTotal = Gia_ManPoNum(pAig);
1342 p->timeTotal = Abc_Clock() - clkTotal;
1343 if ( fVerbose )
1344 Cbs3_ManSatPrintStats( p );
1345 if ( fVerbose )
1346 {
1347 printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
1348 printf( "Mem usage %.2f MB.\n", 1.0*Cbs3_ManMemory(p)/(1<<20) );
1349 //Abc_PrintTime( 1, "JFront", p->timeJFront );
1350 //Abc_PrintTime( 1, "Loading", p->timeSatLoad );
1351 //printf( "Decisions = %d.\n", p->nDecs );
1352 }
1353 Cbs3_ManStop( p );
1354 *pvStatus = vStatus;
1355 return vCexStore;
1356}
1357
1358
1362
1363
1364ABC_NAMESPACE_IMPL_END
1365
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
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
Cbs3_Que_t
struct Cbs3_Que_t_ Cbs3_Que_t
Definition giaCSat3.c:46
Cbs3_ClauseForEachEntry1
#define Cbs3_ClauseForEachEntry1(p, hClause, iObj, i)
Definition giaCSat3.c:141
Cbs3_ManSolveMiterNc
Vec_Int_t * Cbs3_ManSolveMiterNc(Gia_Man_t *pAig, int nConfs, int nRestarts, Vec_Str_t **pvStatus, int fVerbose)
Definition giaCSat3.c:1284
Cbs3_ClauseForEachEntry
#define Cbs3_ClauseForEachEntry(p, hClause, iObj, i)
Definition giaCSat3.c:139
Cbs3_ManStop
void Cbs3_ManStop(Cbs3_Man_t *p)
Definition giaCSat3.c:246
Cbs3_Par_t
typedefABC_NAMESPACE_IMPL_START struct Cbs3_Par_t_ Cbs3_Par_t
DECLARATIONS ///.
Definition giaCSat3.c:30
Cbs3_ManUpdateJFrontier
void Cbs3_ManUpdateJFrontier(Cbs3_Man_t *p)
Definition giaCSat3.c:963
Cbs3_QueForEachEntry
#define Cbs3_QueForEachEntry(Que, iObj, i)
Definition giaCSat3.c:136
Cbs3_ReadModel
Vec_Int_t * Cbs3_ReadModel(Cbs3_Man_t *p)
Definition giaCSat3.c:298
Cbs3_ManSatPrintStats
void Cbs3_ManSatPrintStats(Cbs3_Man_t *p)
Definition giaCSat3.c:1134
Cbs3_ManAlloc
Cbs3_Man_t * Cbs3_ManAlloc(Gia_Man_t *pGia)
Definition giaCSat3.c:183
Cbs3_ManSolve
int Cbs3_ManSolve(Cbs3_Man_t *p, int iLit, int nRestarts)
Definition giaCSat3.c:1111
Cbs3_SetDefaultParams
void Cbs3_SetDefaultParams(Cbs3_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition giaCSat3.c:159
Cbs3_ManPropagateNew
int Cbs3_ManPropagateNew(Cbs3_Man_t *p, int Level)
Definition giaCSat3.c:978
Cbs3_ManSolve2_rec
int Cbs3_ManSolve2_rec(Cbs3_Man_t *p, int Level)
Definition giaCSat3.c:1026
Cbs3_ManSetConflictNum
void Cbs3_ManSetConflictNum(Cbs3_Man_t *p, int Num)
Definition giaCSat3.c:167
Cbs3_ManMemory
int Cbs3_ManMemory(Cbs3_Man_t *p)
Definition giaCSat3.c:267
Cbs3_Man_t
struct Cbs3_Man_t_ Cbs3_Man_t
Definition giaCSat3.c:55
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
inline
#define inline
Definition kitPerm.c:28
if
if(last==0)
Definition sparse_int.h:34
Cbs3_Man_t_
Definition giaCSat3.c:57
Cbs3_Man_t_::nConfUndec
int nConfUndec
Definition giaCSat3.c:88
Cbs3_Man_t_::timeSatLoad
abctime timeSatLoad
Definition giaCSat3.c:91
Cbs3_Man_t_::nVars
int nVars
Definition giaCSat3.c:66
Cbs3_Man_t_::vMark
Vec_Str_t vMark
Definition giaCSat3.c:75
Cbs3_Man_t_::nVarsAlloc
int nVarsAlloc
Definition giaCSat3.c:67
Cbs3_Man_t_::nSatUndec
int nSatUndec
Definition giaCSat3.c:83
Cbs3_Man_t_::timeTotal
abctime timeTotal
Definition giaCSat3.c:95
Cbs3_Man_t_::vMap
Vec_Int_t vMap
Definition giaCSat3.c:69
Cbs3_Man_t_::nSatUnsat
int nSatUnsat
Definition giaCSat3.c:81
Cbs3_Man_t_::pClauses
Cbs3_Que_t pClauses
Definition giaCSat3.c:62
Cbs3_Man_t_::nSatSat
int nSatSat
Definition giaCSat3.c:82
Cbs3_Man_t_::timeJFront
abctime timeJFront
Definition giaCSat3.c:90
Cbs3_Man_t_::var_inc
int var_inc
Definition giaCSat3.c:68
Cbs3_Man_t_::timeSatSat
abctime timeSatSat
Definition giaCSat3.c:93
Cbs3_Man_t_::nFails
int nFails[2]
Definition giaCSat3.c:98
Cbs3_Man_t_::nConfSat
int nConfSat
Definition giaCSat3.c:87
Cbs3_Man_t_::vFans
Vec_Int_t vFans
Definition giaCSat3.c:71
Cbs3_Man_t_::nPropCalls
int nPropCalls[3]
Definition giaCSat3.c:97
Cbs3_Man_t_::vLevReason
Vec_Int_t vLevReason
Definition giaCSat3.c:76
Cbs3_Man_t_::vActs
Vec_Int_t vActs
Definition giaCSat3.c:77
Cbs3_Man_t_::vRef
Vec_Int_t vRef
Definition giaCSat3.c:70
Cbs3_Man_t_::vWatches
Vec_Int_t vWatches
Definition giaCSat3.c:78
Cbs3_Man_t_::vTemp
Vec_Int_t * vTemp
Definition giaCSat3.c:64
Cbs3_Man_t_::vModel
Vec_Int_t * vModel
Definition giaCSat3.c:63
Cbs3_Man_t_::nClauseConf
int nClauseConf
Definition giaCSat3.c:99
Cbs3_Man_t_::Pars
Cbs3_Par_t Pars
Definition giaCSat3.c:58
Cbs3_Man_t_::nConfUnsat
int nConfUnsat
Definition giaCSat3.c:86
Cbs3_Man_t_::pJust
Cbs3_Que_t pJust
Definition giaCSat3.c:61
Cbs3_Man_t_::pProp
Cbs3_Que_t pProp
Definition giaCSat3.c:60
Cbs3_Man_t_::timeSatUndec
abctime timeSatUndec
Definition giaCSat3.c:94
Cbs3_Man_t_::nDecs
int nDecs
Definition giaCSat3.c:100
Cbs3_Man_t_::vAssign
Vec_Str_t vAssign
Definition giaCSat3.c:74
Cbs3_Man_t_::nSatTotal
int nSatTotal
Definition giaCSat3.c:84
Cbs3_Man_t_::pAig
Gia_Man_t * pAig
Definition giaCSat3.c:59
Cbs3_Man_t_::vImps
Vec_Wec_t vImps
Definition giaCSat3.c:72
Cbs3_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition giaCSat3.c:92
Cbs3_Man_t_::vWatchUpds
Vec_Int_t vWatchUpds
Definition giaCSat3.c:79
Cbs3_Par_t_
Definition giaCSat3.c:32
Cbs3_Par_t_::nBTThis
int nBTThis
Definition giaCSat3.c:38
Cbs3_Par_t_::nBTLimit
int nBTLimit
Definition giaCSat3.c:34
Cbs3_Par_t_::nBTTotal
int nBTTotal
Definition giaCSat3.c:40
Cbs3_Par_t_::nJustLimit
int nJustLimit
Definition giaCSat3.c:35
Cbs3_Par_t_::nJustTotal
int nJustTotal
Definition giaCSat3.c:41
Cbs3_Par_t_::nRestLimit
int nRestLimit
Definition giaCSat3.c:36
Cbs3_Par_t_::nJustThis
int nJustThis
Definition giaCSat3.c:39
Cbs3_Par_t_::fVerbose
int fVerbose
Definition giaCSat3.c:43
Cbs3_Que_t_
Definition giaCSat3.c:48
Cbs3_Que_t_::nSize
int nSize
Definition giaCSat3.c:51
Cbs3_Que_t_::pData
int * pData
Definition giaCSat3.c:52
Cbs3_Que_t_::iTail
int iTail
Definition giaCSat3.c:50
Cbs3_Que_t_::iHead
int iHead
Definition giaCSat3.c:49
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryDoubleStart
#define Vec_IntForEachEntryDoubleStart(vVec, Entry1, Entry2, i, Start)
Definition vecInt.h:74
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42