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