abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaCSatOld.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 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 typedef struct Cbs0_Par_t_ Cbs0_Par_t;
31 struct Cbs0_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  // current parameters
37  int nBTThis; // number of conflicts
38  int nJustThis; // max size of the frontier
39  int nBTTotal; // total number of conflicts
40  int nJustTotal; // total size of the frontier
41  // decision heuristics
42  int fUseHighest; // use node with the highest ID
43  int fUseLowest; // use node with the highest ID
44  int fUseMaxFF; // use node with the largest fanin fanout
45  // other
46  int fVerbose;
47 };
48 
49 typedef struct Cbs0_Que_t_ Cbs0_Que_t;
50 struct Cbs0_Que_t_
51 {
52  int iHead; // beginning of the queue
53  int iTail; // end of the queue
54  int nSize; // allocated size
55  Gia_Obj_t ** pData; // nodes stored in the queue
56 };
57 
58 typedef struct Cbs0_Man_t_ Cbs0_Man_t;
59 struct Cbs0_Man_t_
60 {
61  Cbs0_Par_t Pars; // parameters
62  Gia_Man_t * pAig; // AIG manager
63  Cbs0_Que_t pProp; // propagation queue
64  Cbs0_Que_t pJust; // justification queue
65  Vec_Int_t * vModel; // satisfying assignment
66  // SAT calls statistics
67  int nSatUnsat; // the number of proofs
68  int nSatSat; // the number of failure
69  int nSatUndec; // the number of timeouts
70  int nSatTotal; // the number of calls
71  // conflicts
72  int nConfUnsat; // conflicts in unsat problems
73  int nConfSat; // conflicts in sat problems
74  int nConfUndec; // conflicts in undec problems
75  // runtime stats
76  abctime timeSatUnsat; // unsat
77  abctime timeSatSat; // sat
78  abctime timeSatUndec; // undecided
79  abctime timeTotal; // total runtime
80 };
81 
82 static inline int Cbs0_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
83 static inline void Cbs0_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
84 static inline void Cbs0_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; }
85 static inline int Cbs0_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
86 static inline void Cbs0_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
87 static inline int Cbs0_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)); }
88 static inline int Cbs0_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
89 static inline int Cbs0_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
90 
91 #define Cbs0_QueForEachEntry( Que, pObj, i ) \
92  for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
93 
94 ////////////////////////////////////////////////////////////////////////
95 /// FUNCTION DEFINITIONS ///
96 ////////////////////////////////////////////////////////////////////////
97 
98 /**Function*************************************************************
99 
100  Synopsis [Sets default values of the parameters.]
101 
102  Description []
103 
104  SideEffects []
105 
106  SeeAlso []
107 
108 ***********************************************************************/
109 void Cbs0_SetDefaultParams( Cbs0_Par_t * pPars )
110 {
111  memset( pPars, 0, sizeof(Cbs0_Par_t) );
112  pPars->nBTLimit = 1000; // limit on the number of conflicts
113  pPars->nJustLimit = 100; // limit on the size of justification queue
114  pPars->fUseHighest = 1; // use node with the highest ID
115  pPars->fUseLowest = 0; // use node with the highest ID
116  pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
117  pPars->fVerbose = 1; // print detailed statistics
118 }
119 
120 /**Function*************************************************************
121 
122  Synopsis []
123 
124  Description []
125 
126  SideEffects []
127 
128  SeeAlso []
129 
130 ***********************************************************************/
131 Cbs0_Man_t * Cbs0_ManAlloc()
132 {
133  Cbs0_Man_t * p;
134  p = ABC_CALLOC( Cbs0_Man_t, 1 );
135  p->pProp.nSize = p->pJust.nSize = 10000;
136  p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
137  p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
138  p->vModel = Vec_IntAlloc( 1000 );
139  Cbs0_SetDefaultParams( &p->Pars );
140  return p;
141 }
142 
143 /**Function*************************************************************
144 
145  Synopsis []
146 
147  Description []
148 
149  SideEffects []
150 
151  SeeAlso []
152 
153 ***********************************************************************/
154 void Cbs0_ManStop( Cbs0_Man_t * p )
155 {
156  Vec_IntFree( p->vModel );
157  ABC_FREE( p->pProp.pData );
158  ABC_FREE( p->pJust.pData );
159  ABC_FREE( p );
160 }
161 
162 /**Function*************************************************************
163 
164  Synopsis [Returns satisfying assignment.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 Vec_Int_t * Cbs0_ReadModel( Cbs0_Man_t * p )
174 {
175  return p->vModel;
176 }
177 
178 
179 
180 
181 /**Function*************************************************************
182 
183  Synopsis [Returns 1 if the solver is out of limits.]
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 static inline int Cbs0_ManCheckLimits( Cbs0_Man_t * p )
193 {
194  return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis [Saves the satisfying assignment as an array of literals.]
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
209 {
210  Gia_Obj_t * pVar;
211  int i;
212  Vec_IntClear( vCex );
213  p->pProp.iHead = 0;
214  Cbs0_QueForEachEntry( p->pProp, pVar, i )
215  if ( Gia_ObjIsCi(pVar) )
216 // Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
217  Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
218 }
219 
220 /**Function*************************************************************
221 
222  Synopsis []
223 
224  Description []
225 
226  SideEffects []
227 
228  SeeAlso []
229 
230 ***********************************************************************/
231 static inline int Cbs0_QueIsEmpty( Cbs0_Que_t * p )
232 {
233  return p->iHead == p->iTail;
234 }
235 
236 /**Function*************************************************************
237 
238  Synopsis []
239 
240  Description []
241 
242  SideEffects []
243 
244  SeeAlso []
245 
246 ***********************************************************************/
247 static inline void Cbs0_QuePush( Cbs0_Que_t * p, Gia_Obj_t * pObj )
248 {
249  if ( p->iTail == p->nSize )
250  {
251  p->nSize *= 2;
252  p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
253  }
254  p->pData[p->iTail++] = pObj;
255 }
256 
257 /**Function*************************************************************
258 
259  Synopsis [Returns 1 if the object in the queue.]
260 
261  Description []
262 
263  SideEffects []
264 
265  SeeAlso []
266 
267 ***********************************************************************/
268 static inline int Cbs0_QueHasNode( Cbs0_Que_t * p, Gia_Obj_t * pObj )
269 {
270  Gia_Obj_t * pTemp;
271  int i;
272  Cbs0_QueForEachEntry( *p, pTemp, i )
273  if ( pTemp == pObj )
274  return 1;
275  return 0;
276 }
277 
278 /**Function*************************************************************
279 
280  Synopsis []
281 
282  Description []
283 
284  SideEffects []
285 
286  SeeAlso []
287 
288 ***********************************************************************/
289 static inline void Cbs0_QueStore( Cbs0_Que_t * p, int * piHeadOld, int * piTailOld )
290 {
291  int i;
292  *piHeadOld = p->iHead;
293  *piTailOld = p->iTail;
294  for ( i = *piHeadOld; i < *piTailOld; i++ )
295  Cbs0_QuePush( p, p->pData[i] );
296  p->iHead = *piTailOld;
297 }
298 
299 /**Function*************************************************************
300 
301  Synopsis []
302 
303  Description []
304 
305  SideEffects []
306 
307  SeeAlso []
308 
309 ***********************************************************************/
310 static inline void Cbs0_QueRestore( Cbs0_Que_t * p, int iHeadOld, int iTailOld )
311 {
312  p->iHead = iHeadOld;
313  p->iTail = iTailOld;
314 }
315 
316 
317 /**Function*************************************************************
318 
319  Synopsis [Max number of fanins fanouts.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
329 {
330  int Count0, Count1;
331  assert( !Gia_IsComplement(pObj) );
332  assert( Gia_ObjIsAnd(pObj) );
333  Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
334  Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
335  return Abc_MaxInt( Count0, Count1 );
336 }
337 
338 /**Function*************************************************************
339 
340  Synopsis [Find variable with the highest ID.]
341 
342  Description []
343 
344  SideEffects []
345 
346  SeeAlso []
347 
348 ***********************************************************************/
349 static inline Gia_Obj_t * Cbs0_ManDecideHighest( Cbs0_Man_t * p )
350 {
351  Gia_Obj_t * pObj, * pObjMax = NULL;
352  int i;
353  Cbs0_QueForEachEntry( p->pJust, pObj, i )
354  if ( pObjMax == NULL || pObjMax < pObj )
355  pObjMax = pObj;
356  return pObjMax;
357 }
358 
359 /**Function*************************************************************
360 
361  Synopsis [Find variable with the lowest ID.]
362 
363  Description []
364 
365  SideEffects []
366 
367  SeeAlso []
368 
369 ***********************************************************************/
370 static inline Gia_Obj_t * Cbs0_ManDecideLowest( Cbs0_Man_t * p )
371 {
372  Gia_Obj_t * pObj, * pObjMin = NULL;
373  int i;
374  Cbs0_QueForEachEntry( p->pJust, pObj, i )
375  if ( pObjMin == NULL || pObjMin > pObj )
376  pObjMin = pObj;
377  return pObjMin;
378 }
379 
380 /**Function*************************************************************
381 
382  Synopsis [Find variable with the maximum number of fanin fanouts.]
383 
384  Description []
385 
386  SideEffects []
387 
388  SeeAlso []
389 
390 ***********************************************************************/
391 static inline Gia_Obj_t * Cbs0_ManDecideMaxFF( Cbs0_Man_t * p )
392 {
393  Gia_Obj_t * pObj, * pObjMax = NULL;
394  int i, iMaxFF = 0, iCurFF;
395  assert( p->pAig->pRefs != NULL );
396  Cbs0_QueForEachEntry( p->pJust, pObj, i )
397  {
398  iCurFF = Cbs0_VarFaninFanoutMax( p, pObj );
399  assert( iCurFF > 0 );
400  if ( iMaxFF < iCurFF )
401  {
402  iMaxFF = iCurFF;
403  pObjMax = pObj;
404  }
405  }
406  return pObjMax;
407 }
408 
409 
410 
411 /**Function*************************************************************
412 
413  Synopsis []
414 
415  Description []
416 
417  SideEffects []
418 
419  SeeAlso []
420 
421 ***********************************************************************/
422 static inline void Cbs0_ManCancelUntil( Cbs0_Man_t * p, int iBound )
423 {
424  Gia_Obj_t * pVar;
425  int i;
426  assert( iBound <= p->pProp.iTail );
427  p->pProp.iHead = iBound;
428  Cbs0_QueForEachEntry( p->pProp, pVar, i )
429  Cbs0_VarUnassign( pVar );
430  p->pProp.iTail = iBound;
431 }
432 
433 /**Function*************************************************************
434 
435  Synopsis [Assigns the variables a value.]
436 
437  Description [Returns 1 if conflict; 0 if no conflict.]
438 
439  SideEffects []
440 
441  SeeAlso []
442 
443 ***********************************************************************/
444 static inline void Cbs0_ManAssign( Cbs0_Man_t * p, Gia_Obj_t * pObj )
445 {
446  Gia_Obj_t * pObjR = Gia_Regular(pObj);
447  assert( Gia_ObjIsCand(pObjR) );
448  assert( !Cbs0_VarIsAssigned(pObjR) );
449  Cbs0_VarAssign( pObjR );
450  Cbs0_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
451  Cbs0_QuePush( &p->pProp, pObjR );
452 }
453 
454 /**Function*************************************************************
455 
456  Synopsis [Propagates a variable.]
457 
458  Description [Returns 1 if conflict; 0 if no conflict.]
459 
460  SideEffects []
461 
462  SeeAlso []
463 
464 ***********************************************************************/
465 static inline int Cbs0_ManPropagateOne( Cbs0_Man_t * p, Gia_Obj_t * pVar )
466 {
467  int Value0, Value1;
468  assert( !Gia_IsComplement(pVar) );
469  assert( Cbs0_VarIsAssigned(pVar) );
470  if ( Gia_ObjIsCi(pVar) )
471  return 0;
472  assert( Gia_ObjIsAnd(pVar) );
473  Value0 = Cbs0_VarFanin0Value(pVar);
474  Value1 = Cbs0_VarFanin1Value(pVar);
475  if ( Cbs0_VarValue(pVar) )
476  { // value is 1
477  if ( Value0 == 0 || Value1 == 0 ) // one is 0
478  return 1;
479  if ( Value0 == 2 ) // first is unassigned
480  Cbs0_ManAssign( p, Gia_ObjChild0(pVar) );
481  if ( Value1 == 2 ) // first is unassigned
482  Cbs0_ManAssign( p, Gia_ObjChild1(pVar) );
483  return 0;
484  }
485  // value is 0
486  if ( Value0 == 0 || Value1 == 0 ) // one is 0
487  return 0;
488  if ( Value0 == 1 && Value1 == 1 ) // both are 1
489  return 1;
490  if ( Value0 == 1 || Value1 == 1 ) // one is 1
491  {
492  if ( Value0 == 2 ) // first is unassigned
493  Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
494  if ( Value1 == 2 ) // first is unassigned
495  Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
496  return 0;
497  }
498  assert( Cbs0_VarIsJust(pVar) );
499  assert( !Cbs0_QueHasNode( &p->pJust, pVar ) );
500  Cbs0_QuePush( &p->pJust, pVar );
501  return 0;
502 }
503 
504 /**Function*************************************************************
505 
506  Synopsis [Propagates a variable.]
507 
508  Description [Returns 1 if conflict; 0 if no conflict.]
509 
510  SideEffects []
511 
512  SeeAlso []
513 
514 ***********************************************************************/
515 static inline int Cbs0_ManPropagateTwo( Cbs0_Man_t * p, Gia_Obj_t * pVar )
516 {
517  int Value0, Value1;
518  assert( !Gia_IsComplement(pVar) );
519  assert( Gia_ObjIsAnd(pVar) );
520  assert( Cbs0_VarIsAssigned(pVar) );
521  assert( !Cbs0_VarValue(pVar) );
522  Value0 = Cbs0_VarFanin0Value(pVar);
523  Value1 = Cbs0_VarFanin1Value(pVar);
524  // value is 0
525  if ( Value0 == 0 || Value1 == 0 ) // one is 0
526  return 0;
527  if ( Value0 == 1 && Value1 == 1 ) // both are 1
528  return 1;
529  assert( Value0 == 1 || Value1 == 1 );
530  if ( Value0 == 2 ) // first is unassigned
531  Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
532  if ( Value1 == 2 ) // first is unassigned
533  Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
534  return 0;
535 }
536 
537 /**Function*************************************************************
538 
539  Synopsis [Propagates all variables.]
540 
541  Description [Returns 1 if conflict; 0 if no conflict.]
542 
543  SideEffects []
544 
545  SeeAlso []
546 
547 ***********************************************************************/
548 int Cbs0_ManPropagate( Cbs0_Man_t * p )
549 {
550  Gia_Obj_t * pVar;
551  int i, k;
552  while ( 1 )
553  {
554  Cbs0_QueForEachEntry( p->pProp, pVar, i )
555  {
556  if ( Cbs0_ManPropagateOne( p, pVar ) )
557  return 1;
558  }
559  p->pProp.iHead = p->pProp.iTail;
560  k = p->pJust.iHead;
561  Cbs0_QueForEachEntry( p->pJust, pVar, i )
562  {
563  if ( Cbs0_VarIsJust( pVar ) )
564  p->pJust.pData[k++] = pVar;
565  else if ( Cbs0_ManPropagateTwo( p, pVar ) )
566  return 1;
567  }
568  if ( k == p->pJust.iTail )
569  break;
570  p->pJust.iTail = k;
571  }
572  return 0;
573 }
574 
575 /**Function*************************************************************
576 
577  Synopsis [Solve the problem recursively.]
578 
579  Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
580 
581  SideEffects []
582 
583  SeeAlso []
584 
585 ***********************************************************************/
586 int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
587 {
588  Gia_Obj_t * pVar, * pDecVar;
589  int iPropHead, iJustHead, iJustTail;
590  // propagate assignments
591  assert( !Cbs0_QueIsEmpty(&p->pProp) );
592  if ( Cbs0_ManPropagate( p ) )
593  return 1;
594  // check for satisfying assignment
595  assert( Cbs0_QueIsEmpty(&p->pProp) );
596  if ( Cbs0_QueIsEmpty(&p->pJust) )
597  return 0;
598  // quit using resource limits
599  p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
600  if ( Cbs0_ManCheckLimits( p ) )
601  return 0;
602  // remember the state before branching
603  iPropHead = p->pProp.iHead;
604  Cbs0_QueStore( &p->pJust, &iJustHead, &iJustTail );
605  // find the decision variable
606  if ( p->Pars.fUseHighest )
607  pVar = Cbs0_ManDecideHighest( p );
608  else if ( p->Pars.fUseLowest )
609  pVar = Cbs0_ManDecideLowest( p );
610  else if ( p->Pars.fUseMaxFF )
611  pVar = Cbs0_ManDecideMaxFF( p );
612  else assert( 0 );
613  assert( Cbs0_VarIsJust( pVar ) );
614  // chose decision variable using fanout count
615  if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
616  pDecVar = Gia_Not(Gia_ObjChild0(pVar));
617  else
618  pDecVar = Gia_Not(Gia_ObjChild1(pVar));
619  // decide on first fanin
620  Cbs0_ManAssign( p, pDecVar );
621  if ( !Cbs0_ManSolve_rec( p ) )
622  return 0;
623  Cbs0_ManCancelUntil( p, iPropHead );
624  Cbs0_QueRestore( &p->pJust, iJustHead, iJustTail );
625  // decide on second fanin
626  Cbs0_ManAssign( p, Gia_Not(pDecVar) );
627  if ( !Cbs0_ManSolve_rec( p ) )
628  return 0;
629  p->Pars.nBTThis++;
630  return 1;
631 }
632 
633 /**Function*************************************************************
634 
635  Synopsis [Looking for a satisfying assignment of the node.]
636 
637  Description [Assumes that each node has flag pObj->fMark0 set to 0.
638  Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
639  The node may be complemented. ]
640 
641  SideEffects []
642 
643  SeeAlso []
644 
645 ***********************************************************************/
646 int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
647 {
648  int RetValue;
649  assert( !p->pProp.iHead && !p->pProp.iTail );
650  assert( !p->pJust.iHead && !p->pJust.iTail );
651  p->Pars.nBTThis = p->Pars.nJustThis = 0;
652  Cbs0_ManAssign( p, pObj );
653  RetValue = Cbs0_ManSolve_rec( p );
654  if ( RetValue == 0 && !Cbs0_ManCheckLimits(p) )
655  Cbs0_ManSaveModel( p, p->vModel );
656  Cbs0_ManCancelUntil( p, 0 );
657  p->pJust.iHead = p->pJust.iTail = 0;
658  p->Pars.nBTTotal += p->Pars.nBTThis;
659  p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
660  if ( Cbs0_ManCheckLimits( p ) )
661  RetValue = -1;
662 // printf( "Outcome = %2d. Confs = %6d. Decision level max = %3d.\n",
663 // RetValue, p->Pars.nBTThis, p->DecLevelMax );
664  return RetValue;
665 }
666 
667 /**Function*************************************************************
668 
669  Synopsis [Prints statistics of the manager.]
670 
671  Description []
672 
673  SideEffects []
674 
675  SeeAlso []
676 
677 ***********************************************************************/
678 void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
679 {
680  printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
681  printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
682  printf( "Conf = %6d ", p->Pars.nBTLimit );
683  printf( "JustMax = %5d ", p->Pars.nJustLimit );
684  printf( "\n" );
685  printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
686  p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
687  ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
688  printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
689  p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
690  ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
691  printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
692  p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
693  ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
694  ABC_PRT( "Total time", p->timeTotal );
695 }
696 
697 /**Function*************************************************************
698 
699  Synopsis [Procedure to test the new SAT solver.]
700 
701  Description []
702 
703  SideEffects []
704 
705  SeeAlso []
706 
707 ***********************************************************************/
708 Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
709 {
710  extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
711  Cbs0_Man_t * p;
712  Vec_Int_t * vCex, * vVisit, * vCexStore;
713  Vec_Str_t * vStatus;
714  Gia_Obj_t * pRoot;
715  int i, status;
716  abctime clk, clkTotal = Abc_Clock();
717  assert( Gia_ManRegNum(pAig) == 0 );
718  // prepare AIG
719  Gia_ManCreateRefs( pAig );
720  Gia_ManCleanMark0( pAig );
721  Gia_ManCleanMark1( pAig );
722  // create logic network
723  p = Cbs0_ManAlloc();
724  p->Pars.nBTLimit = nConfs;
725  p->pAig = pAig;
726  // create resulting data-structures
727  vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
728  vCexStore = Vec_IntAlloc( 10000 );
729  vVisit = Vec_IntAlloc( 100 );
730  vCex = Cbs0_ReadModel( p );
731  // solve for each output
732  Gia_ManForEachCo( pAig, pRoot, i )
733  {
734  Vec_IntClear( vCex );
735  if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
736  {
737  if ( Gia_ObjFaninC0(pRoot) )
738  {
739  printf( "Constant 1 output of SRM!!!\n" );
740  Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
741  Vec_StrPush( vStatus, 0 );
742  }
743  else
744  {
745 // printf( "Constant 0 output of SRM!!!\n" );
746  Vec_StrPush( vStatus, 1 );
747  }
748  continue;
749  }
750  clk = Abc_Clock();
751  p->Pars.fUseHighest = 1;
752  p->Pars.fUseLowest = 0;
753  status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
754 /*
755  if ( status == -1 )
756  {
757  p->Pars.fUseHighest = 0;
758  p->Pars.fUseLowest = 1;
759  status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
760  }
761 */
762  Vec_StrPush( vStatus, (char)status );
763  if ( status == -1 )
764  {
765  p->nSatUndec++;
766  p->nConfUndec += p->Pars.nBTThis;
767  Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
768  p->timeSatUndec += Abc_Clock() - clk;
769  continue;
770  }
771  if ( status == 1 )
772  {
773  p->nSatUnsat++;
774  p->nConfUnsat += p->Pars.nBTThis;
775  p->timeSatUnsat += Abc_Clock() - clk;
776  continue;
777  }
778  p->nSatSat++;
779  p->nConfSat += p->Pars.nBTThis;
780 // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
781  Cec_ManSatAddToStore( vCexStore, vCex, i );
782  p->timeSatSat += Abc_Clock() - clk;
783  }
784  Vec_IntFree( vVisit );
785  p->nSatTotal = Gia_ManPoNum(pAig);
786  p->timeTotal = Abc_Clock() - clkTotal;
787  if ( fVerbose )
788  Cbs0_ManSatPrintStats( p );
789  Cbs0_ManStop( p );
790  *pvStatus = vStatus;
791 // printf( "Total number of cex literals = %d. (Ave = %d)\n",
792 // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
793 // (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
794  return vCexStore;
795 }
796 
797 
798 ////////////////////////////////////////////////////////////////////////
799 /// END OF FILE ///
800 ////////////////////////////////////////////////////////////////////////
801 
802 
803 ABC_NAMESPACE_IMPL_END
804 
memset
char * memset()
Cbs0_Man_t_::nConfSat
int nConfSat
Definition: giaCSatOld.c:73
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Cbs0_Par_t_::fUseMaxFF
int fUseMaxFF
Definition: giaCSatOld.c:44
Cbs0_Man_t_::nSatUnsat
int nSatUnsat
Definition: giaCSatOld.c:67
Cbs0_Man_t_::nConfUnsat
int nConfUnsat
Definition: giaCSatOld.c:72
Cbs0_VarIsJust
static int Cbs0_VarIsJust(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:87
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Cbs0_Man_t_::timeSatUndec
abctime timeSatUndec
Definition: giaCSatOld.c:78
Cbs0_QueForEachEntry
#define Cbs0_QueForEachEntry(Que, pObj, i)
Definition: giaCSatOld.c:91
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
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Cbs0_Que_t_::iTail
int iTail
Definition: giaCSatOld.c:53
Gia_ObjIsCand
static int Gia_ObjIsCand(Gia_Obj_t *pObj)
Definition: gia.h:429
Cbs0_VarSetValue
static void Cbs0_VarSetValue(Gia_Obj_t *pVar, int v)
Definition: giaCSatOld.c:86
Cbs0_VarValue
static int Cbs0_VarValue(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:85
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
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
Cbs0_ManStop
void Cbs0_ManStop(Cbs0_Man_t *p)
Definition: giaCSatOld.c:154
Cbs0_Que_t_::pData
Gia_Obj_t ** pData
Definition: giaCSatOld.c:55
Cbs0_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition: giaCSatOld.c:76
Cbs0_VarFanin0Value
static int Cbs0_VarFanin0Value(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:88
Cbs0_ManCheckLimits
static int Cbs0_ManCheckLimits(Cbs0_Man_t *p)
Definition: giaCSatOld.c:192
Gia_ObjRefNum
static int Gia_ObjRefNum(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:521
Cbs0_ManDecideHighest
static Gia_Obj_t * Cbs0_ManDecideHighest(Cbs0_Man_t *p)
Definition: giaCSatOld.c:349
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cbs0_QueRestore
static void Cbs0_QueRestore(Cbs0_Que_t *p, int iHeadOld, int iTailOld)
Definition: giaCSatOld.c:310
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
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
Cbs0_ManCancelUntil
static void Cbs0_ManCancelUntil(Cbs0_Man_t *p, int iBound)
Definition: giaCSatOld.c:422
Cbs0_ManSaveModel
static void Cbs0_ManSaveModel(Cbs0_Man_t *p, Vec_Int_t *vCex)
Definition: giaCSatOld.c:208
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
Cbs0_SetDefaultParams
void Cbs0_SetDefaultParams(Cbs0_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: giaCSatOld.c:109
Cbs0_Man_t_::nSatTotal
int nSatTotal
Definition: giaCSatOld.c:70
Cbs0_ManSolve_rec
int Cbs0_ManSolve_rec(Cbs0_Man_t *p)
Definition: giaCSatOld.c:586
Cbs0_ManSolve
int Cbs0_ManSolve(Cbs0_Man_t *p, Gia_Obj_t *pObj)
Definition: giaCSatOld.c:646
Gia_Not
static Gia_Obj_t * Gia_Not(Gia_Obj_t *p)
Definition: gia.h:378
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Cbs0_ManDecideMaxFF
static Gia_Obj_t * Cbs0_ManDecideMaxFF(Cbs0_Man_t *p)
Definition: giaCSatOld.c:391
Cbs0_QueIsEmpty
static int Cbs0_QueIsEmpty(Cbs0_Que_t *p)
Definition: giaCSatOld.c:231
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Cbs0_Par_t_::nBTLimit
int nBTLimit
Definition: giaCSatOld.c:34
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cbs0_ManPropagateOne
static int Cbs0_ManPropagateOne(Cbs0_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCSatOld.c:465
Cbs0_Par_t_::fUseHighest
int fUseHighest
Definition: giaCSatOld.c:42
Cbs0_QuePush
static void Cbs0_QuePush(Cbs0_Que_t *p, Gia_Obj_t *pObj)
Definition: giaCSatOld.c:247
Cbs0_Man_t_::nSatUndec
int nSatUndec
Definition: giaCSatOld.c:69
Cbs0_Man_t_::pJust
Cbs0_Que_t pJust
Definition: giaCSatOld.c:64
Cbs0_ManDecideLowest
static Gia_Obj_t * Cbs0_ManDecideLowest(Cbs0_Man_t *p)
Definition: giaCSatOld.c:370
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cbs0_VarUnassign
static void Cbs0_VarUnassign(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:84
Cbs0_Que_t_::iHead
int iHead
Definition: giaCSatOld.c:52
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cbs0_Man_t_::nConfUndec
int nConfUndec
Definition: giaCSatOld.c:74
Cbs0_ManPropagate
int Cbs0_ManPropagate(Cbs0_Man_t *p)
Definition: giaCSatOld.c:548
Cbs0_Par_t_::nJustLimit
int nJustLimit
Definition: giaCSatOld.c:35
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cbs0_Par_t_::nBTTotal
int nBTTotal
Definition: giaCSatOld.c:39
Cec_ManSatAddToStore
void Cec_ManSatAddToStore(Vec_Int_t *vCexStore, Vec_Int_t *vCex, int Out)
Definition: cecSolve.c:952
Cbs0_Man_t_::Pars
Cbs0_Par_t Pars
Definition: giaCSatOld.c:61
Cbs0_ReadModel
Vec_Int_t * Cbs0_ReadModel(Cbs0_Man_t *p)
Definition: giaCSatOld.c:173
Cbs0_Que_t_::nSize
int nSize
Definition: giaCSatOld.c:54
Cbs0_Par_t_::fUseLowest
int fUseLowest
Definition: giaCSatOld.c:43
Cbs0_ManPropagateTwo
static int Cbs0_ManPropagateTwo(Cbs0_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCSatOld.c:515
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Cbs0_Man_t_::pProp
Cbs0_Que_t pProp
Definition: giaCSatOld.c:63
Vec_Str_t_
Definition: bblif.c:47
Cbs0_ManAlloc
Cbs0_Man_t * Cbs0_ManAlloc()
Definition: giaCSatOld.c:131
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
Cbs0_Par_t_::nJustThis
int nJustThis
Definition: giaCSatOld.c:38
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Cbs_ManSolveMiter
Vec_Int_t * Cbs_ManSolveMiter(Gia_Man_t *pAig, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCSatOld.c:708
Cbs0_Man_t_::timeTotal
abctime timeTotal
Definition: giaCSatOld.c:79
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Cbs0_Par_t_
Definition: giaCSatOld.c:31
Cbs0_ManAssign
static void Cbs0_ManAssign(Cbs0_Man_t *p, Gia_Obj_t *pObj)
Definition: giaCSatOld.c:444
Cbs0_QueStore
static void Cbs0_QueStore(Cbs0_Que_t *p, int *piHeadOld, int *piTailOld)
Definition: giaCSatOld.c:289
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Cbs0_Man_t_
Definition: giaCSatOld.c:59
Cbs0_Par_t_::nJustTotal
int nJustTotal
Definition: giaCSatOld.c:40
assert
#define assert(ex)
Definition: util_old.h:213
Cbs0_Par_t_::nBTThis
int nBTThis
Definition: giaCSatOld.c:37
Cbs0_QueHasNode
static int Cbs0_QueHasNode(Cbs0_Que_t *p, Gia_Obj_t *pObj)
Definition: giaCSatOld.c:268
Cbs0_VarFanin1Value
static int Cbs0_VarFanin1Value(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:89
Cbs0_VarIsAssigned
static int Cbs0_VarIsAssigned(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:82
Cbs0_Man_t_::vModel
Vec_Int_t * vModel
Definition: giaCSatOld.c:65
Cbs0_Par_t_::fVerbose
int fVerbose
Definition: giaCSatOld.c:46
Cbs0_VarFaninFanoutMax
static int Cbs0_VarFaninFanoutMax(Cbs0_Man_t *p, Gia_Obj_t *pObj)
Definition: giaCSatOld.c:328
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Cbs0_Man_t_::pAig
Gia_Man_t * pAig
Definition: giaCSatOld.c:62
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
Cbs0_ManSatPrintStats
void Cbs0_ManSatPrintStats(Cbs0_Man_t *p)
Definition: giaCSatOld.c:678
Cbs0_Par_t
typedefABC_NAMESPACE_IMPL_START struct Cbs0_Par_t_ Cbs0_Par_t
DECLARATIONS ///.
Definition: giaCSatOld.c:30
Cbs0_Man_t_::nSatSat
int nSatSat
Definition: giaCSatOld.c:68
Cbs0_VarAssign
static void Cbs0_VarAssign(Gia_Obj_t *pVar)
Definition: giaCSatOld.c:83
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Cbs0_Man_t_::timeSatSat
abctime timeSatSat
Definition: giaCSatOld.c:77
Cbs0_Que_t_
Definition: giaCSatOld.c:50
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