1 /**CFile****************************************************************
2
3 FileName [giaCSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [A simple circuit-based solver.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 //#define gia_assert(exp) ((void)0)
27 //#define gia_assert(exp) (assert(exp))
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 typedef struct Cbs_Par_t_ Cbs_Par_t;
34 struct Cbs_Par_t_
35 {
36 // conflict limits
37 int nBTLimit; // limit on the number of conflicts
38 int nJustLimit; // limit on the size of justification queue
39 // current parameters
40 int nBTThis; // number of conflicts
41 int nBTThisNc; // number of conflicts
42 int nJustThis; // max size of the frontier
43 int nBTTotal; // total number of conflicts
44 int nJustTotal; // total size of the frontier
45 // decision heuristics
46 int fUseHighest; // use node with the highest ID
47 int fUseLowest; // use node with the highest ID
48 int fUseMaxFF; // use node with the largest fanin fanout
49 // other
50 int fVerbose;
51 };
52
53 typedef struct Cbs_Que_t_ Cbs_Que_t;
54 struct Cbs_Que_t_
55 {
56 int iHead; // beginning of the queue
57 int iTail; // end of the queue
58 int nSize; // allocated size
59 Gia_Obj_t ** pData; // nodes stored in the queue
60 };
61
62 //typedef struct Cbs_Man_t_ Cbs_Man_t;
63 struct Cbs_Man_t_
64 {
65 Cbs_Par_t Pars; // parameters
66 Gia_Man_t * pAig; // AIG manager
67 Cbs_Que_t pProp; // propagation queue
68 Cbs_Que_t pJust; // justification queue
69 Cbs_Que_t pClauses; // clause queue
70 Gia_Obj_t ** pIter; // iterator through clause vars
71 Vec_Int_t * vLevReas; // levels and decisions
72 Vec_Int_t * vModel; // satisfying assignment
73 Vec_Ptr_t * vTemp; // temporary storage
74 // SAT calls statistics
75 int nSatUnsat; // the number of proofs
76 int nSatSat; // the number of failure
77 int nSatUndec; // the number of timeouts
78 int nSatTotal; // the number of calls
79 // conflicts
80 int nConfUnsat; // conflicts in unsat problems
81 int nConfSat; // conflicts in sat problems
82 int nConfUndec; // conflicts in undec problems
83 // runtime stats
84 abctime timeSatUnsat; // unsat
85 abctime timeSatSat; // sat
86 abctime timeSatUndec; // undecided
87 abctime timeTotal; // total runtime
88 };
89
Cbs_VarIsAssigned(Gia_Obj_t * pVar)90 static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
Cbs_VarAssign(Gia_Obj_t * pVar)91 static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
Cbs_VarUnassign(Gia_Obj_t * pVar)92 static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
Cbs_VarValue(Gia_Obj_t * pVar)93 static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
Cbs_VarSetValue(Gia_Obj_t * pVar,int v)94 static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
Cbs_VarIsJust(Gia_Obj_t * pVar)95 static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); }
Cbs_VarFanin0Value(Gia_Obj_t * pVar)96 static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
Cbs_VarFanin1Value(Gia_Obj_t * pVar)97 static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
98
Cbs_VarDecLevel(Cbs_Man_t * p,Gia_Obj_t * pVar)99 static inline int Cbs_VarDecLevel( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
Cbs_VarReason0(Cbs_Man_t * p,Gia_Obj_t * pVar)100 static inline Gia_Obj_t * Cbs_VarReason0( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
Cbs_VarReason1(Cbs_Man_t * p,Gia_Obj_t * pVar)101 static inline Gia_Obj_t * Cbs_VarReason1( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
Cbs_ClauseDecLevel(Cbs_Man_t * p,int hClause)102 static inline int Cbs_ClauseDecLevel( Cbs_Man_t * p, int hClause ) { return Cbs_VarDecLevel( p, p->pClauses.pData[hClause] ); }
103
104 #define Cbs_QueForEachEntry( Que, pObj, i ) \
105 for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
106
107 #define Cbs_ClauseForEachVar( p, hClause, pObj ) \
108 for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
109 #define Cbs_ClauseForEachVar1( p, hClause, pObj ) \
110 for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
111
112 ////////////////////////////////////////////////////////////////////////
113 /// FUNCTION DEFINITIONS ///
114 ////////////////////////////////////////////////////////////////////////
115
116 /**Function*************************************************************
117
118 Synopsis [Sets default values of the parameters.]
119
120 Description []
121
122 SideEffects []
123
124 SeeAlso []
125
126 ***********************************************************************/
Cbs_SetDefaultParams(Cbs_Par_t * pPars)127 void Cbs_SetDefaultParams( Cbs_Par_t * pPars )
128 {
129 memset( pPars, 0, sizeof(Cbs_Par_t) );
130 pPars->nBTLimit = 1000; // limit on the number of conflicts
131 pPars->nJustLimit = 100; // limit on the size of justification queue
132 pPars->fUseHighest = 1; // use node with the highest ID
133 pPars->fUseLowest = 0; // use node with the highest ID
134 pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
135 pPars->fVerbose = 1; // print detailed statistics
136 }
Cbs_ManSetConflictNum(Cbs_Man_t * p,int Num)137 void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num )
138 {
139 p->Pars.nBTLimit = Num;
140 }
141
142 /**Function*************************************************************
143
144 Synopsis []
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152 ***********************************************************************/
Cbs_ManAlloc(Gia_Man_t * pGia)153 Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia )
154 {
155 Cbs_Man_t * p;
156 p = ABC_CALLOC( Cbs_Man_t, 1 );
157 p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
158 p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
159 p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
160 p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
161 p->pClauses.iHead = p->pClauses.iTail = 1;
162 p->vModel = Vec_IntAlloc( 1000 );
163 p->vLevReas = Vec_IntAlloc( 1000 );
164 p->vTemp = Vec_PtrAlloc( 1000 );
165 p->pAig = pGia;
166 Cbs_SetDefaultParams( &p->Pars );
167 return p;
168 }
169
170 /**Function*************************************************************
171
172 Synopsis []
173
174 Description []
175
176 SideEffects []
177
178 SeeAlso []
179
180 ***********************************************************************/
Cbs_ManStop(Cbs_Man_t * p)181 void Cbs_ManStop( Cbs_Man_t * p )
182 {
183 Vec_IntFree( p->vLevReas );
184 Vec_IntFree( p->vModel );
185 Vec_PtrFree( p->vTemp );
186 ABC_FREE( p->pClauses.pData );
187 ABC_FREE( p->pProp.pData );
188 ABC_FREE( p->pJust.pData );
189 ABC_FREE( p );
190 }
191
192 /**Function*************************************************************
193
194 Synopsis [Returns satisfying assignment.]
195
196 Description []
197
198 SideEffects []
199
200 SeeAlso []
201
202 ***********************************************************************/
Cbs_ReadModel(Cbs_Man_t * p)203 Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p )
204 {
205 return p->vModel;
206 }
207
208
209
210
211 /**Function*************************************************************
212
213 Synopsis [Returns 1 if the solver is out of limits.]
214
215 Description []
216
217 SideEffects []
218
219 SeeAlso []
220
221 ***********************************************************************/
Cbs_ManCheckLimits(Cbs_Man_t * p)222 static inline int Cbs_ManCheckLimits( Cbs_Man_t * p )
223 {
224 return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
225 }
226
227 /**Function*************************************************************
228
229 Synopsis [Saves the satisfying assignment as an array of literals.]
230
231 Description []
232
233 SideEffects []
234
235 SeeAlso []
236
237 ***********************************************************************/
Cbs_ManSaveModel(Cbs_Man_t * p,Vec_Int_t * vCex)238 static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
239 {
240 Gia_Obj_t * pVar;
241 int i;
242 Vec_IntClear( vCex );
243 p->pProp.iHead = 0;
244 Cbs_QueForEachEntry( p->pProp, pVar, i )
245 if ( Gia_ObjIsCi(pVar) )
246 // Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
247 Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
248 }
Cbs_ManSaveModelAll(Cbs_Man_t * p,Vec_Int_t * vCex)249 static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex )
250 {
251 Gia_Obj_t * pVar;
252 int i;
253 Vec_IntClear( vCex );
254 p->pProp.iHead = 0;
255 Cbs_QueForEachEntry( p->pProp, pVar, i )
256 Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
257 }
258
259 /**Function*************************************************************
260
261 Synopsis []
262
263 Description []
264
265 SideEffects []
266
267 SeeAlso []
268
269 ***********************************************************************/
Cbs_QueIsEmpty(Cbs_Que_t * p)270 static inline int Cbs_QueIsEmpty( Cbs_Que_t * p )
271 {
272 return p->iHead == p->iTail;
273 }
274
275 /**Function*************************************************************
276
277 Synopsis []
278
279 Description []
280
281 SideEffects []
282
283 SeeAlso []
284
285 ***********************************************************************/
Cbs_QuePush(Cbs_Que_t * p,Gia_Obj_t * pObj)286 static inline void Cbs_QuePush( Cbs_Que_t * p, Gia_Obj_t * pObj )
287 {
288 assert( !Gia_IsComplement(pObj) );
289 if ( p->iTail == p->nSize )
290 {
291 p->nSize *= 2;
292 p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
293 }
294 p->pData[p->iTail++] = pObj;
295 }
296
297 /**Function*************************************************************
298
299 Synopsis [Returns 1 if the object in the queue.]
300
301 Description []
302
303 SideEffects []
304
305 SeeAlso []
306
307 ***********************************************************************/
Cbs_QueHasNode(Cbs_Que_t * p,Gia_Obj_t * pObj)308 static inline int Cbs_QueHasNode( Cbs_Que_t * p, Gia_Obj_t * pObj )
309 {
310 Gia_Obj_t * pTemp;
311 int i;
312 Cbs_QueForEachEntry( *p, pTemp, i )
313 if ( pTemp == pObj )
314 return 1;
315 return 0;
316 }
317
318 /**Function*************************************************************
319
320 Synopsis []
321
322 Description []
323
324 SideEffects []
325
326 SeeAlso []
327
328 ***********************************************************************/
Cbs_QueStore(Cbs_Que_t * p,int * piHeadOld,int * piTailOld)329 static inline void Cbs_QueStore( Cbs_Que_t * p, int * piHeadOld, int * piTailOld )
330 {
331 int i;
332 *piHeadOld = p->iHead;
333 *piTailOld = p->iTail;
334 for ( i = *piHeadOld; i < *piTailOld; i++ )
335 Cbs_QuePush( p, p->pData[i] );
336 p->iHead = *piTailOld;
337 }
338
339 /**Function*************************************************************
340
341 Synopsis []
342
343 Description []
344
345 SideEffects []
346
347 SeeAlso []
348
349 ***********************************************************************/
Cbs_QueRestore(Cbs_Que_t * p,int iHeadOld,int iTailOld)350 static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld )
351 {
352 p->iHead = iHeadOld;
353 p->iTail = iTailOld;
354 }
355
356 /**Function*************************************************************
357
358 Synopsis [Finalized the clause.]
359
360 Description []
361
362 SideEffects []
363
364 SeeAlso []
365
366 ***********************************************************************/
Cbs_QueFinish(Cbs_Que_t * p)367 static inline int Cbs_QueFinish( Cbs_Que_t * p )
368 {
369 int iHeadOld = p->iHead;
370 assert( p->iHead < p->iTail );
371 Cbs_QuePush( p, NULL );
372 p->iHead = p->iTail;
373 return iHeadOld;
374 }
375
376
377 /**Function*************************************************************
378
379 Synopsis [Max number of fanins fanouts.]
380
381 Description []
382
383 SideEffects []
384
385 SeeAlso []
386
387 ***********************************************************************/
Cbs_VarFaninFanoutMax(Cbs_Man_t * p,Gia_Obj_t * pObj)388 static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj )
389 {
390 int Count0, Count1;
391 assert( !Gia_IsComplement(pObj) );
392 assert( Gia_ObjIsAnd(pObj) );
393 Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
394 Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
395 return Abc_MaxInt( Count0, Count1 );
396 }
397
398 /**Function*************************************************************
399
400 Synopsis [Find variable with the highest ID.]
401
402 Description []
403
404 SideEffects []
405
406 SeeAlso []
407
408 ***********************************************************************/
Cbs_ManDecideHighest(Cbs_Man_t * p)409 static inline Gia_Obj_t * Cbs_ManDecideHighest( Cbs_Man_t * p )
410 {
411 Gia_Obj_t * pObj, * pObjMax = NULL;
412 int i;
413 Cbs_QueForEachEntry( p->pJust, pObj, i )
414 if ( pObjMax == NULL || pObjMax < pObj )
415 pObjMax = pObj;
416 return pObjMax;
417 }
418
419 /**Function*************************************************************
420
421 Synopsis [Find variable with the lowest ID.]
422
423 Description []
424
425 SideEffects []
426
427 SeeAlso []
428
429 ***********************************************************************/
Cbs_ManDecideLowest(Cbs_Man_t * p)430 static inline Gia_Obj_t * Cbs_ManDecideLowest( Cbs_Man_t * p )
431 {
432 Gia_Obj_t * pObj, * pObjMin = NULL;
433 int i;
434 Cbs_QueForEachEntry( p->pJust, pObj, i )
435 if ( pObjMin == NULL || pObjMin > pObj )
436 pObjMin = pObj;
437 return pObjMin;
438 }
439
440 /**Function*************************************************************
441
442 Synopsis [Find variable with the maximum number of fanin fanouts.]
443
444 Description []
445
446 SideEffects []
447
448 SeeAlso []
449
450 ***********************************************************************/
Cbs_ManDecideMaxFF(Cbs_Man_t * p)451 static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p )
452 {
453 Gia_Obj_t * pObj, * pObjMax = NULL;
454 int i, iMaxFF = 0, iCurFF;
455 assert( p->pAig->pRefs != NULL );
456 Cbs_QueForEachEntry( p->pJust, pObj, i )
457 {
458 iCurFF = Cbs_VarFaninFanoutMax( p, pObj );
459 assert( iCurFF > 0 );
460 if ( iMaxFF < iCurFF )
461 {
462 iMaxFF = iCurFF;
463 pObjMax = pObj;
464 }
465 }
466 return pObjMax;
467 }
468
469
470
471 /**Function*************************************************************
472
473 Synopsis []
474
475 Description []
476
477 SideEffects []
478
479 SeeAlso []
480
481 ***********************************************************************/
Cbs_ManCancelUntil(Cbs_Man_t * p,int iBound)482 static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
483 {
484 Gia_Obj_t * pVar;
485 int i;
486 assert( iBound <= p->pProp.iTail );
487 p->pProp.iHead = iBound;
488 Cbs_QueForEachEntry( p->pProp, pVar, i )
489 Cbs_VarUnassign( pVar );
490 p->pProp.iTail = iBound;
491 Vec_IntShrink( p->vLevReas, 3*iBound );
492 }
493
494 int s_Counter = 0;
495
496 /**Function*************************************************************
497
498 Synopsis [Assigns the variables a value.]
499
500 Description [Returns 1 if conflict; 0 if no conflict.]
501
502 SideEffects []
503
504 SeeAlso []
505
506 ***********************************************************************/
Cbs_ManAssign(Cbs_Man_t * p,Gia_Obj_t * pObj,int Level,Gia_Obj_t * pRes0,Gia_Obj_t * pRes1)507 static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
508 {
509 Gia_Obj_t * pObjR = Gia_Regular(pObj);
510 assert( Gia_ObjIsCand(pObjR) );
511 assert( !Cbs_VarIsAssigned(pObjR) );
512 Cbs_VarAssign( pObjR );
513 Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
514 assert( pObjR->Value == ~0 );
515 pObjR->Value = p->pProp.iTail;
516 Cbs_QuePush( &p->pProp, pObjR );
517 Vec_IntPush( p->vLevReas, Level );
518 Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
519 Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
520 assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
521 // s_Counter++;
522 // s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
523 }
524
525
526 /**Function*************************************************************
527
528 Synopsis [Returns clause size.]
529
530 Description []
531
532 SideEffects []
533
534 SeeAlso []
535
536 ***********************************************************************/
Cbs_ManClauseSize(Cbs_Man_t * p,int hClause)537 static inline int Cbs_ManClauseSize( Cbs_Man_t * p, int hClause )
538 {
539 Cbs_Que_t * pQue = &(p->pClauses);
540 Gia_Obj_t ** pIter;
541 for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
542 return pIter - pQue->pData - hClause ;
543 }
544
545 /**Function*************************************************************
546
547 Synopsis [Prints conflict clause.]
548
549 Description []
550
551 SideEffects []
552
553 SeeAlso []
554
555 ***********************************************************************/
Cbs_ManPrintClause(Cbs_Man_t * p,int Level,int hClause)556 static inline void Cbs_ManPrintClause( Cbs_Man_t * p, int Level, int hClause )
557 {
558 Cbs_Que_t * pQue = &(p->pClauses);
559 Gia_Obj_t * pObj;
560 int i;
561 assert( Cbs_QueIsEmpty( pQue ) );
562 printf( "Level %2d : ", Level );
563 for ( i = hClause; (pObj = pQue->pData[i]); i++ )
564 printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs_VarValue(pObj), Cbs_VarDecLevel(p, pObj) );
565 printf( "\n" );
566 }
567
568 /**Function*************************************************************
569
570 Synopsis [Prints conflict clause.]
571
572 Description []
573
574 SideEffects []
575
576 SeeAlso []
577
578 ***********************************************************************/
Cbs_ManPrintClauseNew(Cbs_Man_t * p,int Level,int hClause)579 static inline void Cbs_ManPrintClauseNew( Cbs_Man_t * p, int Level, int hClause )
580 {
581 Cbs_Que_t * pQue = &(p->pClauses);
582 Gia_Obj_t * pObj;
583 int i;
584 assert( Cbs_QueIsEmpty( pQue ) );
585 printf( "Level %2d : ", Level );
586 for ( i = hClause; (pObj = pQue->pData[i]); i++ )
587 printf( "%c%d ", Cbs_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
588 printf( "\n" );
589 }
590
591 /**Function*************************************************************
592
593 Synopsis [Returns conflict clause.]
594
595 Description [Performs conflict analysis.]
596
597 SideEffects []
598
599 SeeAlso []
600
601 ***********************************************************************/
Cbs_ManDeriveReason(Cbs_Man_t * p,int Level)602 static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
603 {
604 Cbs_Que_t * pQue = &(p->pClauses);
605 Gia_Obj_t * pObj, * pReason;
606 int i, k, iLitLevel;
607 assert( pQue->pData[pQue->iHead] == NULL );
608 assert( pQue->iHead + 1 < pQue->iTail );
609 /*
610 for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
611 {
612 pObj = pQue->pData[i];
613 assert( pObj->fMark0 == 1 );
614 }
615 */
616 // compact literals
617 Vec_PtrClear( p->vTemp );
618 for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
619 {
620 pObj = pQue->pData[i];
621 if ( !pObj->fMark0 ) // unassigned - seen again
622 continue;
623 // assigned - seen first time
624 pObj->fMark0 = 0;
625 Vec_PtrPush( p->vTemp, pObj );
626 // check decision level
627 iLitLevel = Cbs_VarDecLevel( p, pObj );
628 if ( iLitLevel < Level )
629 {
630 pQue->pData[k++] = pObj;
631 continue;
632 }
633 assert( iLitLevel == Level );
634 pReason = Cbs_VarReason0( p, pObj );
635 if ( pReason == pObj ) // no reason
636 {
637 //assert( pQue->pData[pQue->iHead] == NULL );
638 pQue->pData[pQue->iHead] = pObj;
639 continue;
640 }
641 Cbs_QuePush( pQue, pReason );
642 pReason = Cbs_VarReason1( p, pObj );
643 if ( pReason != pObj ) // second reason
644 Cbs_QuePush( pQue, pReason );
645 }
646 assert( pQue->pData[pQue->iHead] != NULL );
647 pQue->iTail = k;
648 // clear the marks
649 Vec_PtrForEachEntry( Gia_Obj_t *, p->vTemp, pObj, i )
650 pObj->fMark0 = 1;
651 }
652
653 /**Function*************************************************************
654
655 Synopsis [Returns conflict clause.]
656
657 Description [Performs conflict analysis.]
658
659 SideEffects []
660
661 SeeAlso []
662
663 ***********************************************************************/
Cbs_ManAnalyze(Cbs_Man_t * p,int Level,Gia_Obj_t * pVar,Gia_Obj_t * pFan0,Gia_Obj_t * pFan1)664 static inline int Cbs_ManAnalyze( Cbs_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
665 {
666 Cbs_Que_t * pQue = &(p->pClauses);
667 assert( Cbs_VarIsAssigned(pVar) );
668 assert( Cbs_VarIsAssigned(pFan0) );
669 assert( pFan1 == NULL || Cbs_VarIsAssigned(pFan1) );
670 assert( Cbs_QueIsEmpty( pQue ) );
671 Cbs_QuePush( pQue, NULL );
672 Cbs_QuePush( pQue, pVar );
673 Cbs_QuePush( pQue, pFan0 );
674 if ( pFan1 )
675 Cbs_QuePush( pQue, pFan1 );
676 Cbs_ManDeriveReason( p, Level );
677 return Cbs_QueFinish( pQue );
678 }
679
680
681 /**Function*************************************************************
682
683 Synopsis [Performs resolution of two clauses.]
684
685 Description []
686
687 SideEffects []
688
689 SeeAlso []
690
691 ***********************************************************************/
Cbs_ManResolve(Cbs_Man_t * p,int Level,int hClause0,int hClause1)692 static inline int Cbs_ManResolve( Cbs_Man_t * p, int Level, int hClause0, int hClause1 )
693 {
694 Cbs_Que_t * pQue = &(p->pClauses);
695 Gia_Obj_t * pObj;
696 int i, LevelMax = -1, LevelCur;
697 assert( pQue->pData[hClause0] != NULL );
698 assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
699 /*
700 for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
701 assert( pObj->fMark0 == 1 );
702 for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
703 assert( pObj->fMark0 == 1 );
704 */
705 assert( Cbs_QueIsEmpty( pQue ) );
706 Cbs_QuePush( pQue, NULL );
707 for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
708 {
709 if ( !pObj->fMark0 ) // unassigned - seen again
710 continue;
711 // assigned - seen first time
712 pObj->fMark0 = 0;
713 Cbs_QuePush( pQue, pObj );
714 LevelCur = Cbs_VarDecLevel( p, pObj );
715 if ( LevelMax < LevelCur )
716 LevelMax = LevelCur;
717 }
718 for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
719 {
720 if ( !pObj->fMark0 ) // unassigned - seen again
721 continue;
722 // assigned - seen first time
723 pObj->fMark0 = 0;
724 Cbs_QuePush( pQue, pObj );
725 LevelCur = Cbs_VarDecLevel( p, pObj );
726 if ( LevelMax < LevelCur )
727 LevelMax = LevelCur;
728 }
729 for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
730 pQue->pData[i]->fMark0 = 1;
731 Cbs_ManDeriveReason( p, LevelMax );
732 return Cbs_QueFinish( pQue );
733 }
734
735 /**Function*************************************************************
736
737 Synopsis [Propagates a variable.]
738
739 Description [Returns clause handle if conflict; 0 if no conflict.]
740
741 SideEffects []
742
743 SeeAlso []
744
745 ***********************************************************************/
Cbs_ManPropagateOne(Cbs_Man_t * p,Gia_Obj_t * pVar,int Level)746 static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
747 {
748 int Value0, Value1;
749 assert( !Gia_IsComplement(pVar) );
750 assert( Cbs_VarIsAssigned(pVar) );
751 if ( Gia_ObjIsCi(pVar) )
752 return 0;
753 assert( Gia_ObjIsAnd(pVar) );
754 Value0 = Cbs_VarFanin0Value(pVar);
755 Value1 = Cbs_VarFanin1Value(pVar);
756 if ( Cbs_VarValue(pVar) )
757 { // value is 1
758 if ( Value0 == 0 || Value1 == 0 ) // one is 0
759 {
760 if ( Value0 == 0 && Value1 != 0 )
761 return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
762 if ( Value0 != 0 && Value1 == 0 )
763 return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
764 assert( Value0 == 0 && Value1 == 0 );
765 return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
766 }
767 if ( Value0 == 2 ) // first is unassigned
768 Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
769 if ( Value1 == 2 ) // first is unassigned
770 Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
771 return 0;
772 }
773 // value is 0
774 if ( Value0 == 0 || Value1 == 0 ) // one is 0
775 return 0;
776 if ( Value0 == 1 && Value1 == 1 ) // both are 1
777 return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
778 if ( Value0 == 1 || Value1 == 1 ) // one is 1
779 {
780 if ( Value0 == 2 ) // first is unassigned
781 Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
782 if ( Value1 == 2 ) // second is unassigned
783 Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
784 return 0;
785 }
786 assert( Cbs_VarIsJust(pVar) );
787 assert( !Cbs_QueHasNode( &p->pJust, pVar ) );
788 Cbs_QuePush( &p->pJust, pVar );
789 return 0;
790 }
791
792 /**Function*************************************************************
793
794 Synopsis [Propagates a variable.]
795
796 Description [Returns 1 if conflict; 0 if no conflict.]
797
798 SideEffects []
799
800 SeeAlso []
801
802 ***********************************************************************/
Cbs_ManPropagateTwo(Cbs_Man_t * p,Gia_Obj_t * pVar,int Level)803 static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
804 {
805 int Value0, Value1;
806 assert( !Gia_IsComplement(pVar) );
807 assert( Gia_ObjIsAnd(pVar) );
808 assert( Cbs_VarIsAssigned(pVar) );
809 assert( !Cbs_VarValue(pVar) );
810 Value0 = Cbs_VarFanin0Value(pVar);
811 Value1 = Cbs_VarFanin1Value(pVar);
812 // value is 0
813 if ( Value0 == 0 || Value1 == 0 ) // one is 0
814 return 0;
815 if ( Value0 == 1 && Value1 == 1 ) // both are 1
816 return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
817 assert( Value0 == 1 || Value1 == 1 );
818 if ( Value0 == 2 ) // first is unassigned
819 Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
820 if ( Value1 == 2 ) // first is unassigned
821 Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
822 return 0;
823 }
824
825 /**Function*************************************************************
826
827 Synopsis [Propagates all variables.]
828
829 Description [Returns 1 if conflict; 0 if no conflict.]
830
831 SideEffects []
832
833 SeeAlso []
834
835 ***********************************************************************/
Cbs_ManPropagate(Cbs_Man_t * p,int Level)836 int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
837 {
838 int hClause;
839 Gia_Obj_t * pVar;
840 int i, k;
841 while ( 1 )
842 {
843 Cbs_QueForEachEntry( p->pProp, pVar, i )
844 {
845 if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
846 return hClause;
847 }
848 p->pProp.iHead = p->pProp.iTail;
849 k = p->pJust.iHead;
850 Cbs_QueForEachEntry( p->pJust, pVar, i )
851 {
852 if ( Cbs_VarIsJust( pVar ) )
853 p->pJust.pData[k++] = pVar;
854 else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
855 return hClause;
856 }
857 if ( k == p->pJust.iTail )
858 break;
859 p->pJust.iTail = k;
860 }
861 return 0;
862 }
863
864 /**Function*************************************************************
865
866 Synopsis [Solve the problem recursively.]
867
868 Description [Returns learnt clause if unsat, NULL if sat or undecided.]
869
870 SideEffects []
871
872 SeeAlso []
873
874 ***********************************************************************/
Cbs_ManSolve_rec(Cbs_Man_t * p,int Level)875 int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
876 {
877 Cbs_Que_t * pQue = &(p->pClauses);
878 Gia_Obj_t * pVar = NULL, * pDecVar;
879 int hClause, hLearn0, hLearn1;
880 int iPropHead, iJustHead, iJustTail;
881 // propagate assignments
882 assert( !Cbs_QueIsEmpty(&p->pProp) );
883 if ( (hClause = Cbs_ManPropagate( p, Level )) )
884 return hClause;
885 // check for satisfying assignment
886 assert( Cbs_QueIsEmpty(&p->pProp) );
887 if ( Cbs_QueIsEmpty(&p->pJust) )
888 return 0;
889 // quit using resource limits
890 p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
891 if ( Cbs_ManCheckLimits( p ) )
892 return 0;
893 // remember the state before branching
894 iPropHead = p->pProp.iHead;
895 Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
896 // find the decision variable
897 if ( p->Pars.fUseHighest )
898 pVar = Cbs_ManDecideHighest( p );
899 else if ( p->Pars.fUseLowest )
900 pVar = Cbs_ManDecideLowest( p );
901 else if ( p->Pars.fUseMaxFF )
902 pVar = Cbs_ManDecideMaxFF( p );
903 else assert( 0 );
904 assert( Cbs_VarIsJust( pVar ) );
905 // chose decision variable using fanout count
906 if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
907 pDecVar = Gia_Not(Gia_ObjChild0(pVar));
908 else
909 pDecVar = Gia_Not(Gia_ObjChild1(pVar));
910 // pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
911 // pDecVar = Gia_Not(pDecVar);
912 // decide on first fanin
913 Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
914 if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
915 return 0;
916 if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
917 return hLearn0;
918 Cbs_ManCancelUntil( p, iPropHead );
919 Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
920 // decide on second fanin
921 Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
922 if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
923 return 0;
924 if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
925 return hLearn1;
926 hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 );
927 // Cbs_ManPrintClauseNew( p, Level, hClause );
928 // if ( Level > Cbs_ClauseDecLevel(p, hClause) )
929 // p->Pars.nBTThisNc++;
930 p->Pars.nBTThis++;
931 return hClause;
932 }
933
934 /**Function*************************************************************
935
936 Synopsis [Looking for a satisfying assignment of the node.]
937
938 Description [Assumes that each node has flag pObj->fMark0 set to 0.
939 Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
940 The node may be complemented. ]
941
942 SideEffects [The two procedures differ in the CEX format.]
943
944 SeeAlso []
945
946 ***********************************************************************/
Cbs_ManSolve(Cbs_Man_t * p,Gia_Obj_t * pObj)947 int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
948 {
949 int RetValue = 0;
950 s_Counter = 0;
951 assert( !p->pProp.iHead && !p->pProp.iTail );
952 assert( !p->pJust.iHead && !p->pJust.iTail );
953 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
954 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
955 Cbs_ManAssign( p, pObj, 0, NULL, NULL );
956 if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
957 Cbs_ManSaveModel( p, p->vModel );
958 else
959 RetValue = 1;
960 Cbs_ManCancelUntil( p, 0 );
961 p->pJust.iHead = p->pJust.iTail = 0;
962 p->pClauses.iHead = p->pClauses.iTail = 1;
963 p->Pars.nBTTotal += p->Pars.nBTThis;
964 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
965 if ( Cbs_ManCheckLimits( p ) )
966 RetValue = -1;
967 // printf( "%d ", s_Counter );
968 return RetValue;
969 }
Cbs_ManSolve2(Cbs_Man_t * p,Gia_Obj_t * pObj,Gia_Obj_t * pObj2)970 int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
971 {
972 int RetValue = 0;
973 s_Counter = 0;
974 assert( !p->pProp.iHead && !p->pProp.iTail );
975 assert( !p->pJust.iHead && !p->pJust.iTail );
976 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
977 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
978 Cbs_ManAssign( p, pObj, 0, NULL, NULL );
979 if ( pObj2 )
980 Cbs_ManAssign( p, pObj2, 0, NULL, NULL );
981 if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
982 Cbs_ManSaveModelAll( p, p->vModel );
983 else
984 RetValue = 1;
985 Cbs_ManCancelUntil( p, 0 );
986 p->pJust.iHead = p->pJust.iTail = 0;
987 p->pClauses.iHead = p->pClauses.iTail = 1;
988 p->Pars.nBTTotal += p->Pars.nBTThis;
989 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
990 if ( Cbs_ManCheckLimits( p ) )
991 RetValue = -1;
992 // printf( "%d ", s_Counter );
993 return RetValue;
994 }
995
996 /**Function*************************************************************
997
998 Synopsis [Prints statistics of the manager.]
999
1000 Description []
1001
1002 SideEffects []
1003
1004 SeeAlso []
1005
1006 ***********************************************************************/
Cbs_ManSatPrintStats(Cbs_Man_t * p)1007 void Cbs_ManSatPrintStats( Cbs_Man_t * p )
1008 {
1009 printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
1010 printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
1011 printf( "Conf = %6d ", p->Pars.nBTLimit );
1012 printf( "JustMax = %5d ", p->Pars.nJustLimit );
1013 printf( "\n" );
1014 printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1015 p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
1016 ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
1017 printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1018 p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
1019 ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
1020 printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
1021 p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
1022 ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
1023 ABC_PRT( "Total time", p->timeTotal );
1024 }
1025
1026 /**Function*************************************************************
1027
1028 Synopsis [Procedure to test the new SAT solver.]
1029
1030 Description []
1031
1032 SideEffects []
1033
1034 SeeAlso []
1035
1036 ***********************************************************************/
Cbs_ManSolveMiterNc(Gia_Man_t * pAig,int nConfs,Vec_Str_t ** pvStatus,int fVerbose)1037 Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
1038 {
1039 extern void Gia_ManCollectTest( Gia_Man_t * pAig );
1040 extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1041 Cbs_Man_t * p;
1042 Vec_Int_t * vCex, * vVisit, * vCexStore;
1043 Vec_Str_t * vStatus;
1044 Gia_Obj_t * pRoot;
1045 int i, status;
1046 abctime clk, clkTotal = Abc_Clock();
1047 assert( Gia_ManRegNum(pAig) == 0 );
1048 // Gia_ManCollectTest( pAig );
1049 // prepare AIG
1050 Gia_ManCreateRefs( pAig );
1051 Gia_ManCleanMark0( pAig );
1052 Gia_ManCleanMark1( pAig );
1053 Gia_ManFillValue( pAig ); // maps nodes into trail ids
1054 Gia_ManSetPhase( pAig ); // maps nodes into trail ids
1055 // create logic network
1056 p = Cbs_ManAlloc( pAig );
1057 p->Pars.nBTLimit = nConfs;
1058 // create resulting data-structures
1059 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1060 vCexStore = Vec_IntAlloc( 10000 );
1061 vVisit = Vec_IntAlloc( 100 );
1062 vCex = Cbs_ReadModel( p );
1063 // solve for each output
1064 Gia_ManForEachCo( pAig, pRoot, i )
1065 {
1066 // printf( "\n" );
1067
1068 Vec_IntClear( vCex );
1069 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
1070 {
1071 if ( Gia_ObjFaninC0(pRoot) )
1072 {
1073 // printf( "Constant 1 output of SRM!!!\n" );
1074 Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
1075 Vec_StrPush( vStatus, 0 );
1076 }
1077 else
1078 {
1079 // printf( "Constant 0 output of SRM!!!\n" );
1080 Vec_StrPush( vStatus, 1 );
1081 }
1082 continue;
1083 }
1084 clk = Abc_Clock();
1085 p->Pars.fUseHighest = 1;
1086 p->Pars.fUseLowest = 0;
1087 status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
1088 // printf( "\n" );
1089 /*
1090 if ( status == -1 )
1091 {
1092 p->Pars.fUseHighest = 0;
1093 p->Pars.fUseLowest = 1;
1094 status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
1095 }
1096 */
1097 Vec_StrPush( vStatus, (char)status );
1098 if ( status == -1 )
1099 {
1100 p->nSatUndec++;
1101 p->nConfUndec += p->Pars.nBTThis;
1102 Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1103 p->timeSatUndec += Abc_Clock() - clk;
1104 continue;
1105 }
1106 if ( status == 1 )
1107 {
1108 p->nSatUnsat++;
1109 p->nConfUnsat += p->Pars.nBTThis;
1110 p->timeSatUnsat += Abc_Clock() - clk;
1111 continue;
1112 }
1113 p->nSatSat++;
1114 p->nConfSat += p->Pars.nBTThis;
1115 // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1116 Cec_ManSatAddToStore( vCexStore, vCex, i );
1117 p->timeSatSat += Abc_Clock() - clk;
1118 }
1119 Vec_IntFree( vVisit );
1120 p->nSatTotal = Gia_ManPoNum(pAig);
1121 p->timeTotal = Abc_Clock() - clkTotal;
1122 if ( fVerbose )
1123 Cbs_ManSatPrintStats( p );
1124 // printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
1125 Cbs_ManStop( p );
1126 *pvStatus = vStatus;
1127
1128 // printf( "Total number of cex literals = %d. (Ave = %d)\n",
1129 // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
1130 // (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
1131 return vCexStore;
1132 }
1133
1134
1135 ////////////////////////////////////////////////////////////////////////
1136 /// END OF FILE ///
1137 ////////////////////////////////////////////////////////////////////////
1138
1139
1140 ABC_NAMESPACE_IMPL_END
1141
1142