abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaCTas.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 Tas_Par_t_ Tas_Par_t;
34 struct Tas_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  // activity
46  float VarDecay; // variable activity decay
47  int VarInc; // variable increment
48  // decision heuristics
49  int fUseActive; // use most active
50  int fUseHighest; // use node with the highest ID
51  int fUseLowest; // use node with the highest ID
52  int fUseMaxFF; // use node with the largest fanin fanout
53  // other
54  int fVerbose;
55 };
56 
57 typedef struct Tas_Cls_t_ Tas_Cls_t;
58 struct Tas_Cls_t_
59 {
60  int iNext[2]; // beginning of the queue
61  int nLits; // the number of literals
62  int pLits[0]; // clause literals
63 };
64 
65 typedef struct Tas_Sto_t_ Tas_Sto_t;
66 struct Tas_Sto_t_
67 {
68  int iCur; // current position
69  int nSize; // allocated size
70  int * pData; // clause information
71 };
72 
73 typedef struct Tas_Que_t_ Tas_Que_t;
74 struct Tas_Que_t_
75 {
76  int iHead; // beginning of the queue
77  int iTail; // end of the queue
78  int nSize; // allocated size
79  Gia_Obj_t ** pData; // nodes stored in the queue
80 };
81 
82 struct Tas_Man_t_
83 {
84  Tas_Par_t Pars; // parameters
85  Gia_Man_t * pAig; // AIG manager
86  Tas_Que_t pProp; // propagation queue
87  Tas_Que_t pJust; // justification queue
88  Tas_Que_t pClauses; // clause queue
89  Gia_Obj_t ** pIter; // iterator through clause vars
90  Vec_Int_t * vLevReas; // levels and decisions
91  Vec_Int_t * vModel; // satisfying assignment
92  Vec_Ptr_t * vTemp; // temporary storage
93  // watched clauses
94  Tas_Sto_t pStore; // storage for watched clauses
95  int * pWatches; // watched lists for each literal
96  Vec_Int_t * vWatchLits; // lits whose watched are assigned
97  int nClauses; // the counter of clauses
98  // activity
99  float * pActivity; // variable activity
100  Vec_Int_t * vActiveVars; // variables with activity
101  // SAT calls statistics
102  int nSatUnsat; // the number of proofs
103  int nSatSat; // the number of failure
104  int nSatUndec; // the number of timeouts
105  int nSatTotal; // the number of calls
106  // conflicts
107  int nConfUnsat; // conflicts in unsat problems
108  int nConfSat; // conflicts in sat problems
109  int nConfUndec; // conflicts in undec problems
110  // runtime stats
111  abctime timeSatUnsat; // unsat
112  abctime timeSatSat; // sat
113  abctime timeSatUndec; // undecided
114  abctime timeTotal; // total runtime
115 };
116 
117 static inline int Tas_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
118 static inline void Tas_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
119 static inline void Tas_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
120 static inline int Tas_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
121 static inline void Tas_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
122 static inline int Tas_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); }
123 static inline int Tas_VarFanin0Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
124 static inline int Tas_VarFanin1Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
125 static inline int Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Abc_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) ); }
126 static inline int Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Abc_LitIsCompl(Lit); }
127 
128 static inline int Tas_ClsHandle( Tas_Man_t * p, Tas_Cls_t * pClause ) { return ((int *)pClause) - p->pStore.pData; }
129 static inline Tas_Cls_t * Tas_ClsFromHandle( Tas_Man_t * p, int h ) { return (Tas_Cls_t *)(p->pStore.pData + h); }
130 
131 static inline int Tas_VarDecLevel( Tas_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
132 static inline Gia_Obj_t * Tas_VarReason0( Tas_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
133 static inline Gia_Obj_t * Tas_VarReason1( Tas_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
134 static inline int Tas_ClauseDecLevel( Tas_Man_t * p, int hClause ) { return Tas_VarDecLevel( p, p->pClauses.pData[hClause] ); }
135 
136 static inline int Tas_VarHasReasonCls( Tas_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value+1) == 0 && Vec_IntEntry(p->vLevReas, 3*pVar->Value+2) != 0; }
137 static inline Tas_Cls_t * Tas_VarReasonCls( Tas_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Tas_ClsFromHandle( p, Vec_IntEntry(p->vLevReas, 3*pVar->Value+2) ); }
138 
139 #define Tas_QueForEachEntry( Que, pObj, i ) \
140  for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
141 
142 #define Tas_ClauseForEachVar( p, hClause, pObj ) \
143  for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
144 #define Tas_ClauseForEachVar1( p, hClause, pObj ) \
145  for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
146 
147 ////////////////////////////////////////////////////////////////////////
148 /// FUNCTION DEFINITIONS ///
149 ////////////////////////////////////////////////////////////////////////
150 
151 /**Function*************************************************************
152 
153  Synopsis [Sets default values of the parameters.]
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 void Tas_SetDefaultParams( Tas_Par_t * pPars )
163 {
164  memset( pPars, 0, sizeof(Tas_Par_t) );
165  pPars->nBTLimit = 2000; // limit on the number of conflicts
166  pPars->nJustLimit = 2000; // limit on the size of justification queue
167  pPars->fUseActive = 0; // use node with the highest activity
168  pPars->fUseHighest = 1; // use node with the highest ID
169  pPars->fUseLowest = 0; // use node with the lowest ID
170  pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
171  pPars->fVerbose = 1; // print detailed statistics
172  pPars->VarDecay = (float)0.95; // variable decay
173  pPars->VarInc = 1.0; // variable increment
174 }
175 
176 /**Function*************************************************************
177 
178  Synopsis []
179 
180  Description []
181 
182  SideEffects []
183 
184  SeeAlso []
185 
186 ***********************************************************************/
187 Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit )
188 {
189  Tas_Man_t * p;
190  p = ABC_CALLOC( Tas_Man_t, 1 );
191  Tas_SetDefaultParams( &p->Pars );
192  p->pAig = pAig;
193  p->Pars.nBTLimit = nBTLimit;
194  p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
195  p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
196  p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
197  p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
198  p->pClauses.iHead = p->pClauses.iTail = 1;
199  p->vModel = Vec_IntAlloc( 1000 );
200  p->vLevReas = Vec_IntAlloc( 1000 );
201  p->vTemp = Vec_PtrAlloc( 1000 );
202  p->pStore.iCur = 16;
203  p->pStore.nSize = 10000;
204  p->pStore.pData = ABC_ALLOC( int, p->pStore.nSize );
205  p->pWatches = ABC_CALLOC( int, 2 * Gia_ManObjNum(pAig) );
206  p->vWatchLits = Vec_IntAlloc( 100 );
207  p->pActivity = ABC_CALLOC( float, Gia_ManObjNum(pAig) );
208  p->vActiveVars = Vec_IntAlloc( 100 );
209  return p;
210 }
211 
212 /**Function*************************************************************
213 
214  Synopsis []
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 void Tas_ManStop( Tas_Man_t * p )
224 {
225  Vec_IntFree( p->vActiveVars );
226  Vec_IntFree( p->vWatchLits );
227  Vec_IntFree( p->vLevReas );
228  Vec_IntFree( p->vModel );
229  Vec_PtrFree( p->vTemp );
230  ABC_FREE( p->pActivity );
231  ABC_FREE( p->pWatches );
232  ABC_FREE( p->pStore.pData );
233  ABC_FREE( p->pClauses.pData );
234  ABC_FREE( p->pProp.pData );
235  ABC_FREE( p->pJust.pData );
236  ABC_FREE( p );
237 }
238 
239 /**Function*************************************************************
240 
241  Synopsis [Returns satisfying assignment.]
242 
243  Description []
244 
245  SideEffects []
246 
247  SeeAlso []
248 
249 ***********************************************************************/
250 Vec_Int_t * Tas_ReadModel( Tas_Man_t * p )
251 {
252  return p->vModel;
253 }
254 
255 
256 
257 
258 /**Function*************************************************************
259 
260  Synopsis [Returns 1 if the solver is out of limits.]
261 
262  Description []
263 
264  SideEffects []
265 
266  SeeAlso []
267 
268 ***********************************************************************/
269 static inline int Tas_ManCheckLimits( Tas_Man_t * p )
270 {
271  return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
272 }
273 
274 /**Function*************************************************************
275 
276  Synopsis [Saves the satisfying assignment as an array of literals.]
277 
278  Description []
279 
280  SideEffects []
281 
282  SeeAlso []
283 
284 ***********************************************************************/
285 static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex )
286 {
287  Gia_Obj_t * pVar;
288  int i;
289  Vec_IntClear( vCex );
290  p->pProp.iHead = 0;
291 // printf( "\n" );
292  Tas_QueForEachEntry( p->pProp, pVar, i )
293  {
294  if ( Gia_ObjIsCi(pVar) )
295 // Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) );
296  Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) );
297 /*
298  printf( "%5d(%d) = ", Gia_ObjId(p->pAig, pVar), Tas_VarValue(pVar) );
299  if ( Gia_ObjIsCi(pVar) )
300  printf( "pi %d\n", Gia_ObjCioId(pVar) );
301  else
302  {
303  printf( "%5d %d & ", Gia_ObjFaninId0p(p->pAig, pVar), Gia_ObjFaninC0(pVar) );
304  printf( "%5d %d ", Gia_ObjFaninId1p(p->pAig, pVar), Gia_ObjFaninC1(pVar) );
305  printf( "\n" );
306  }
307 */
308  }
309 }
310 
311 /**Function*************************************************************
312 
313  Synopsis []
314 
315  Description []
316 
317  SideEffects []
318 
319  SeeAlso []
320 
321 ***********************************************************************/
322 static inline int Tas_QueIsEmpty( Tas_Que_t * p )
323 {
324  return p->iHead == p->iTail;
325 }
326 
327 /**Function*************************************************************
328 
329  Synopsis []
330 
331  Description []
332 
333  SideEffects []
334 
335  SeeAlso []
336 
337 ***********************************************************************/
338 static inline void Tas_QuePush( Tas_Que_t * p, Gia_Obj_t * pObj )
339 {
340  if ( p->iTail == p->nSize )
341  {
342  p->nSize *= 2;
343  p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
344  }
345  p->pData[p->iTail++] = pObj;
346 }
347 
348 /**Function*************************************************************
349 
350  Synopsis [Returns 1 if the object in the queue.]
351 
352  Description []
353 
354  SideEffects []
355 
356  SeeAlso []
357 
358 ***********************************************************************/
359 static inline int Tas_QueHasNode( Tas_Que_t * p, Gia_Obj_t * pObj )
360 {
361  Gia_Obj_t * pTemp;
362  int i;
363  Tas_QueForEachEntry( *p, pTemp, i )
364  if ( pTemp == pObj )
365  return 1;
366  return 0;
367 }
368 
369 /**Function*************************************************************
370 
371  Synopsis []
372 
373  Description []
374 
375  SideEffects []
376 
377  SeeAlso []
378 
379 ***********************************************************************/
380 static inline void Tas_QueStore( Tas_Que_t * p, int * piHeadOld, int * piTailOld )
381 {
382  int i;
383  *piHeadOld = p->iHead;
384  *piTailOld = p->iTail;
385  for ( i = *piHeadOld; i < *piTailOld; i++ )
386  Tas_QuePush( p, p->pData[i] );
387  p->iHead = *piTailOld;
388 }
389 
390 /**Function*************************************************************
391 
392  Synopsis []
393 
394  Description []
395 
396  SideEffects []
397 
398  SeeAlso []
399 
400 ***********************************************************************/
401 static inline void Tas_QueRestore( Tas_Que_t * p, int iHeadOld, int iTailOld )
402 {
403  p->iHead = iHeadOld;
404  p->iTail = iTailOld;
405 }
406 
407 /**Function*************************************************************
408 
409  Synopsis [Finalized the clause.]
410 
411  Description []
412 
413  SideEffects []
414 
415  SeeAlso []
416 
417 ***********************************************************************/
418 static inline int Tas_QueFinish( Tas_Que_t * p )
419 {
420  int iHeadOld = p->iHead;
421  assert( p->iHead < p->iTail );
422  Tas_QuePush( p, NULL );
423  p->iHead = p->iTail;
424  return iHeadOld;
425 }
426 
427 
428 /**Function*************************************************************
429 
430  Synopsis [Max number of fanins fanouts.]
431 
432  Description []
433 
434  SideEffects []
435 
436  SeeAlso []
437 
438 ***********************************************************************/
439 static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj )
440 {
441  int Count0, Count1;
442  assert( !Gia_IsComplement(pObj) );
443  assert( Gia_ObjIsAnd(pObj) );
444  Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
445  Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
446  return Abc_MaxInt( Count0, Count1 );
447 }
448 
449 
450 
451 /**Function*************************************************************
452 
453  Synopsis [Find variable with the highest activity.]
454 
455  Description []
456 
457  SideEffects []
458 
459  SeeAlso []
460 
461 ***********************************************************************/
462 static inline Gia_Obj_t * Tas_ManFindActive( Tas_Man_t * p )
463 {
464  Gia_Obj_t * pObj, * pObjMax = NULL;
465  float BestCost = 0.0;
466  int i, ObjId;
467  Tas_QueForEachEntry( p->pJust, pObj, i )
468  {
469  assert( Gia_ObjIsAnd(pObj) );
470  ObjId = Gia_ObjId( p->pAig, pObj );
471  if ( pObjMax == NULL ||
472  p->pActivity[Gia_ObjFaninId0(pObj,ObjId)] > BestCost ||
473  (p->pActivity[Gia_ObjFaninId0(pObj,ObjId)] == BestCost && pObjMax < Gia_ObjFanin0(pObj)) )
474  {
475  pObjMax = Gia_ObjFanin0(pObj);
476  BestCost = p->pActivity[Gia_ObjFaninId0(pObj,ObjId)];
477  }
478  if ( p->pActivity[Gia_ObjFaninId1(pObj,ObjId)] > BestCost ||
479  (p->pActivity[Gia_ObjFaninId1(pObj,ObjId)] == BestCost && pObjMax < Gia_ObjFanin1(pObj)) )
480  {
481  pObjMax = Gia_ObjFanin1(pObj);
482  BestCost = p->pActivity[Gia_ObjFaninId1(pObj,ObjId)];
483  }
484  }
485  return pObjMax;
486 }
487 
488 /**Function*************************************************************
489 
490  Synopsis [Find variable with the highest activity.]
491 
492  Description []
493 
494  SideEffects []
495 
496  SeeAlso []
497 
498 ***********************************************************************/
499 static inline Gia_Obj_t * Tas_ManDecideHighestFanin( Tas_Man_t * p )
500 {
501  Gia_Obj_t * pObj, * pObjMax = NULL;
502  int i, ObjId;
503  Tas_QueForEachEntry( p->pJust, pObj, i )
504  {
505  assert( Gia_ObjIsAnd(pObj) );
506  ObjId = Gia_ObjId( p->pAig, pObj );
507  if ( pObjMax == NULL || pObjMax < Gia_ObjFanin0(pObj) )
508  pObjMax = Gia_ObjFanin0(pObj);
509  if ( pObjMax < Gia_ObjFanin1(pObj) )
510  pObjMax = Gia_ObjFanin1(pObj);
511  }
512  return pObjMax;
513 }
514 
515 /**Function*************************************************************
516 
517  Synopsis [Find variable with the highest ID.]
518 
519  Description []
520 
521  SideEffects []
522 
523  SeeAlso []
524 
525 ***********************************************************************/
526 static inline Gia_Obj_t * Tas_ManDecideHighest( Tas_Man_t * p )
527 {
528  Gia_Obj_t * pObj, * pObjMax = NULL;
529  int i;
530  Tas_QueForEachEntry( p->pJust, pObj, i )
531  {
532 //printf( "%d %6.2f ", Gia_ObjId(p->pAig, pObj), p->pActivity[Gia_ObjId(p->pAig, pObj)] );
533  if ( pObjMax == NULL || pObjMax < pObj )
534  pObjMax = pObj;
535  }
536 //printf( "\n" );
537  return pObjMax;
538 }
539 
540 /**Function*************************************************************
541 
542  Synopsis [Find variable with the highest ID.]
543 
544  Description []
545 
546  SideEffects []
547 
548  SeeAlso []
549 
550 ***********************************************************************/
551 static inline Gia_Obj_t * Tas_ManDecideHighestA( Tas_Man_t * p )
552 {
553  Gia_Obj_t * pObj, * pObjMax = NULL;
554  int i;
555  Tas_QueForEachEntry( p->pJust, pObj, i )
556  {
557  if ( pObjMax == NULL ||
558  p->pActivity[Gia_ObjId(p->pAig, pObjMax)] < p->pActivity[Gia_ObjId(p->pAig, pObj)] )
559  pObjMax = pObj;
560  }
561  return pObjMax;
562 }
563 
564 /**Function*************************************************************
565 
566  Synopsis [Find variable with the lowest ID.]
567 
568  Description []
569 
570  SideEffects []
571 
572  SeeAlso []
573 
574 ***********************************************************************/
575 static inline Gia_Obj_t * Tas_ManDecideLowest( Tas_Man_t * p )
576 {
577  Gia_Obj_t * pObj, * pObjMin = NULL;
578  int i;
579  Tas_QueForEachEntry( p->pJust, pObj, i )
580  if ( pObjMin == NULL || pObjMin > pObj )
581  pObjMin = pObj;
582  return pObjMin;
583 }
584 
585 /**Function*************************************************************
586 
587  Synopsis [Find variable with the maximum number of fanin fanouts.]
588 
589  Description []
590 
591  SideEffects []
592 
593  SeeAlso []
594 
595 ***********************************************************************/
596 static inline Gia_Obj_t * Tas_ManDecideMaxFF( Tas_Man_t * p )
597 {
598  Gia_Obj_t * pObj, * pObjMax = NULL;
599  int i, iMaxFF = 0, iCurFF;
600  assert( p->pAig->pRefs != NULL );
601  Tas_QueForEachEntry( p->pJust, pObj, i )
602  {
603  iCurFF = Tas_VarFaninFanoutMax( p, pObj );
604  assert( iCurFF > 0 );
605  if ( iMaxFF < iCurFF )
606  {
607  iMaxFF = iCurFF;
608  pObjMax = pObj;
609  }
610  }
611  return pObjMax;
612 }
613 
614 
615 
616 /**Function*************************************************************
617 
618  Synopsis []
619 
620  Description []
621 
622  SideEffects []
623 
624  SeeAlso []
625 
626 ***********************************************************************/
627 static inline void Tas_ManCancelUntil( Tas_Man_t * p, int iBound )
628 {
629  Gia_Obj_t * pVar;
630  int i;
631  assert( iBound <= p->pProp.iTail );
632  p->pProp.iHead = iBound;
633  Tas_QueForEachEntry( p->pProp, pVar, i )
634  Tas_VarUnassign( pVar );
635  p->pProp.iTail = iBound;
636  Vec_IntShrink( p->vLevReas, 3*iBound );
637 }
638 
639 int s_Counter2 = 0;
640 int s_Counter3 = 0;
641 int s_Counter4 = 0;
642 
643 /**Function*************************************************************
644 
645  Synopsis [Assigns the variables a value.]
646 
647  Description [Returns 1 if conflict; 0 if no conflict.]
648 
649  SideEffects []
650 
651  SeeAlso []
652 
653 ***********************************************************************/
654 static inline void Tas_ManAssign( Tas_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
655 {
656  Gia_Obj_t * pObjR = Gia_Regular(pObj);
657  assert( Gia_ObjIsCand(pObjR) );
658  assert( !Tas_VarIsAssigned(pObjR) );
659  Tas_VarAssign( pObjR );
660  Tas_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
661  assert( pObjR->Value == ~0 );
662  pObjR->Value = p->pProp.iTail;
663  Tas_QuePush( &p->pProp, pObjR );
664  Vec_IntPush( p->vLevReas, Level );
665  if ( pRes0 == NULL && pRes1 != 0 ) // clause
666  {
667  Vec_IntPush( p->vLevReas, 0 );
668  Vec_IntPush( p->vLevReas, Tas_ClsHandle( p, (Tas_Cls_t *)pRes1 ) );
669  }
670  else
671  {
672  Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
673  Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
674  }
675  assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
676  s_Counter2++;
677 }
678 
679 
680 /**Function*************************************************************
681 
682  Synopsis [Returns clause size.]
683 
684  Description []
685 
686  SideEffects []
687 
688  SeeAlso []
689 
690 ***********************************************************************/
691 static inline int Tas_ManClauseSize( Tas_Man_t * p, int hClause )
692 {
693  Tas_Que_t * pQue = &(p->pClauses);
694  Gia_Obj_t ** pIter;
695  for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
696  return pIter - pQue->pData - hClause ;
697 }
698 
699 /**Function*************************************************************
700 
701  Synopsis [Prints conflict clause.]
702 
703  Description []
704 
705  SideEffects []
706 
707  SeeAlso []
708 
709 ***********************************************************************/
710 static inline void Tas_ManPrintClause( Tas_Man_t * p, int Level, int hClause )
711 {
712  Tas_Que_t * pQue = &(p->pClauses);
713  Gia_Obj_t * pObj;
714  int i;
715  assert( Tas_QueIsEmpty( pQue ) );
716  printf( "Level %2d : ", Level );
717  for ( i = hClause; (pObj = pQue->pData[i]); i++ )
718  printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Tas_VarValue(pObj), Tas_VarDecLevel(p, pObj) );
719  printf( "\n" );
720 }
721 
722 /**Function*************************************************************
723 
724  Synopsis [Prints conflict clause.]
725 
726  Description []
727 
728  SideEffects []
729 
730  SeeAlso []
731 
732 ***********************************************************************/
733 static inline void Tas_ManPrintClauseNew( Tas_Man_t * p, int Level, int hClause )
734 {
735  Tas_Que_t * pQue = &(p->pClauses);
736  Gia_Obj_t * pObj;
737  int i;
738  assert( Tas_QueIsEmpty( pQue ) );
739  printf( "Level %2d : ", Level );
740  for ( i = hClause; (pObj = pQue->pData[i]); i++ )
741  printf( "%c%d ", Tas_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
742  printf( "\n" );
743 }
744 
745 /**Function*************************************************************
746 
747  Synopsis [Returns conflict clause.]
748 
749  Description [Performs conflict analysis.]
750 
751  SideEffects []
752 
753  SeeAlso []
754 
755 ***********************************************************************/
756 static inline void Tas_ManDeriveReason( Tas_Man_t * p, int Level )
757 {
758  Tas_Que_t * pQue = &(p->pClauses);
759  Gia_Obj_t * pObj, * pReason;
760  int i, k, j, iLitLevel, iLitLevel2;//, Id;
761  assert( pQue->pData[pQue->iHead] == NULL );
762  assert( pQue->iHead + 1 < pQue->iTail );
763 /*
764  for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
765  {
766  pObj = pQue->pData[i];
767  assert( pObj->fPhase == 0 );
768  }
769 */
770  // compact literals
771  Vec_PtrClear( p->vTemp );
772  for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
773  {
774  pObj = pQue->pData[i];
775  if ( pObj->fPhase ) // unassigned - seen again
776  continue;
777  // assigned - seen first time
778  pObj->fPhase = 1;
779  Vec_PtrPush( p->vTemp, pObj );
780  // bump activity
781 // Id = Gia_ObjId( p->pAig, pObj );
782 // if ( p->pActivity[Id] == 0.0 )
783 // Vec_IntPush( p->vActiveVars, Id );
784 // p->pActivity[Id] += p->Pars.VarInc;
785  // check decision level
786  iLitLevel = Tas_VarDecLevel( p, pObj );
787  if ( iLitLevel < Level )
788  {
789  pQue->pData[k++] = pObj;
790  continue;
791  }
792  assert( iLitLevel == Level );
793  if ( Tas_VarHasReasonCls( p, pObj ) )
794  {
795  Tas_Cls_t * pCls = Tas_VarReasonCls( p, pObj );
796  pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[0]) );
797  assert( pReason == pObj );
798  for ( j = 1; j < pCls->nLits; j++ )
799  {
800  pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[j]) );
801  iLitLevel2 = Tas_VarDecLevel( p, pReason );
802  assert( Tas_VarIsAssigned( pReason ) );
803  assert( !Tas_LitIsTrue( pReason, pCls->pLits[j] ) );
804  Tas_QuePush( pQue, pReason );
805  }
806  }
807  else
808  {
809  pReason = Tas_VarReason0( p, pObj );
810  if ( pReason == pObj ) // no reason
811  {
812  assert( pQue->pData[pQue->iHead] == NULL || Level == 0 );
813  if ( pQue->pData[pQue->iHead] == NULL )
814  pQue->pData[pQue->iHead] = pObj;
815  else
816  Tas_QuePush( pQue, pObj );
817  continue;
818  }
819  Tas_QuePush( pQue, pReason );
820  pReason = Tas_VarReason1( p, pObj );
821  if ( pReason != pObj ) // second reason
822  Tas_QuePush( pQue, pReason );
823  }
824  }
825  assert( pQue->pData[pQue->iHead] != NULL );
826  if ( pQue->pData[pQue->iHead] == NULL )
827  printf( "Tas_ManDeriveReason(): Failed to derive the clause!!!\n" );
828  pQue->iTail = k;
829  // clear the marks
830  Vec_PtrForEachEntry( Gia_Obj_t *, p->vTemp, pObj, i )
831  pObj->fPhase = 0;
832 }
833 
834 /**Function*************************************************************
835 
836  Synopsis [Returns conflict clause.]
837 
838  Description [Performs conflict analysis.]
839 
840  SideEffects []
841 
842  SeeAlso []
843 
844 ***********************************************************************/
845 static inline int Tas_ManAnalyze( Tas_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
846 {
847  Tas_Que_t * pQue = &(p->pClauses);
848  assert( Tas_VarIsAssigned(pVar) );
849  assert( Tas_VarIsAssigned(pFan0) );
850  assert( pFan1 == NULL || Tas_VarIsAssigned(pFan1) );
851  assert( Tas_QueIsEmpty( pQue ) );
852  Tas_QuePush( pQue, NULL );
853  Tas_QuePush( pQue, pVar );
854  Tas_QuePush( pQue, pFan0 );
855  if ( pFan1 )
856  Tas_QuePush( pQue, pFan1 );
857  Tas_ManDeriveReason( p, Level );
858  return Tas_QueFinish( pQue );
859 }
860 
861 
862 /**Function*************************************************************
863 
864  Synopsis [Performs resolution of two clauses.]
865 
866  Description []
867 
868  SideEffects []
869 
870  SeeAlso []
871 
872 ***********************************************************************/
873 static inline int Tas_ManResolve( Tas_Man_t * p, int Level, int hClause0, int hClause1 )
874 {
875  Tas_Que_t * pQue = &(p->pClauses);
876  Gia_Obj_t * pObj;
877  int i, LevelMax = -1, LevelCur;
878  assert( pQue->pData[hClause0] != NULL );
879  assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
880 /*
881  for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
882  assert( pObj->fPhase == 0 );
883  for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
884  assert( pObj->fPhase == 0 );
885 */
886  assert( Tas_QueIsEmpty( pQue ) );
887  Tas_QuePush( pQue, NULL );
888  for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
889  {
890  if ( pObj->fPhase ) // unassigned - seen again
891  continue;
892  // assigned - seen first time
893  pObj->fPhase = 1;
894  Tas_QuePush( pQue, pObj );
895  LevelCur = Tas_VarDecLevel( p, pObj );
896  if ( LevelMax < LevelCur )
897  LevelMax = LevelCur;
898  }
899  for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
900  {
901  if ( pObj->fPhase ) // unassigned - seen again
902  continue;
903  // assigned - seen first time
904  pObj->fPhase = 1;
905  Tas_QuePush( pQue, pObj );
906  LevelCur = Tas_VarDecLevel( p, pObj );
907  if ( LevelMax < LevelCur )
908  LevelMax = LevelCur;
909  }
910  for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
911  pQue->pData[i]->fPhase = 0;
912  Tas_ManDeriveReason( p, LevelMax );
913  return Tas_QueFinish( pQue );
914 }
915 
916 
917 
918 /**Function*************************************************************
919 
920  Synopsis [Allocates clause of the given size.]
921 
922  Description []
923 
924  SideEffects []
925 
926  SeeAlso []
927 
928 ***********************************************************************/
929 static inline Tas_Cls_t * Tas_ManAllocCls( Tas_Man_t * p, int nSize )
930 {
931  Tas_Cls_t * pCls;
932  if ( p->pStore.iCur + nSize > p->pStore.nSize )
933  {
934  p->pStore.nSize *= 2;
935  p->pStore.pData = ABC_REALLOC( int, p->pStore.pData, p->pStore.nSize );
936  }
937  pCls = Tas_ClsFromHandle( p, p->pStore.iCur ); p->pStore.iCur += nSize;
938  memset( pCls, 0, sizeof(int) * nSize );
939  p->nClauses++;
940  return pCls;
941 }
942 
943 /**Function*************************************************************
944 
945  Synopsis [Adds one clause to the watcher list.]
946 
947  Description []
948 
949  SideEffects []
950 
951  SeeAlso []
952 
953 ***********************************************************************/
954 static inline void Tas_ManWatchClause( Tas_Man_t * p, Tas_Cls_t * pClause, int Lit )
955 {
956  assert( Abc_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) );
957  assert( pClause->nLits >= 2 );
958  assert( pClause->pLits[0] == Lit || pClause->pLits[1] == Lit );
959  if ( pClause->pLits[0] == Lit )
960  pClause->iNext[0] = p->pWatches[Abc_LitNot(Lit)];
961  else
962  pClause->iNext[1] = p->pWatches[Abc_LitNot(Lit)];
963  if ( p->pWatches[Abc_LitNot(Lit)] == 0 )
964  Vec_IntPush( p->vWatchLits, Abc_LitNot(Lit) );
965  p->pWatches[Abc_LitNot(Lit)] = Tas_ClsHandle( p, pClause );
966 }
967 
968 /**Function*************************************************************
969 
970  Synopsis [Creates clause of the given size.]
971 
972  Description []
973 
974  SideEffects []
975 
976  SeeAlso []
977 
978 ***********************************************************************/
979 static inline Tas_Cls_t * Tas_ManCreateCls( Tas_Man_t * p, int hClause )
980 {
981  Tas_Cls_t * pClause;
982  Tas_Que_t * pQue = &(p->pClauses);
983  Gia_Obj_t * pObj;
984  int i, nLits = 0;
985  assert( Tas_QueIsEmpty( pQue ) );
986  assert( pQue->pData[hClause] != NULL );
987  for ( i = hClause; (pObj = pQue->pData[i]); i++ )
988  nLits++;
989  if ( nLits == 1 )
990  return NULL;
991  // create this clause
992  pClause = Tas_ManAllocCls( p, nLits + 3 );
993  pClause->nLits = nLits;
994  for ( i = hClause; (pObj = pQue->pData[i]); i++ )
995  {
996  assert( Tas_VarIsAssigned( pObj ) );
997  pClause->pLits[i-hClause] = Abc_LitNot( Tas_VarToLit(p, pObj) );
998  }
999  // add the clause as watched one
1000  if ( nLits >= 2 )
1001  {
1002  Tas_ManWatchClause( p, pClause, pClause->pLits[0] );
1003  Tas_ManWatchClause( p, pClause, pClause->pLits[1] );
1004  }
1005  // increment activity
1006 // p->Pars.VarInc /= p->Pars.VarDecay;
1007  return pClause;
1008 }
1009 
1010 /**Function*************************************************************
1011 
1012  Synopsis [Creates clause of the given size.]
1013 
1014  Description []
1015 
1016  SideEffects []
1017 
1018  SeeAlso []
1019 
1020 ***********************************************************************/
1021 static inline int Tas_ManCreateFromCls( Tas_Man_t * p, Tas_Cls_t * pCls, int Level )
1022 {
1023  Tas_Que_t * pQue = &(p->pClauses);
1024  Gia_Obj_t * pObj;
1025  int i;
1026  assert( Tas_QueIsEmpty( pQue ) );
1027  Tas_QuePush( pQue, NULL );
1028  for ( i = 0; i < pCls->nLits; i++ )
1029  {
1030  pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[i]) );
1031  assert( Tas_VarIsAssigned(pObj) );
1032  assert( !Tas_LitIsTrue( pObj, pCls->pLits[i] ) );
1033  Tas_QuePush( pQue, pObj );
1034  }
1035  Tas_ManDeriveReason( p, Level );
1036  return Tas_QueFinish( pQue );
1037 }
1038 
1039 /**Function*************************************************************
1040 
1041  Synopsis [Propagate one assignment.]
1042 
1043  Description []
1044 
1045  SideEffects []
1046 
1047  SeeAlso []
1048 
1049 ***********************************************************************/
1050 static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
1051 {
1052  Gia_Obj_t * pObj;
1053  Tas_Cls_t * pCur;
1054  int * piPrev, iCur, iTemp;
1055  int i, LitF = Abc_LitNot(Lit);
1056  // iterate through the clauses
1057  piPrev = p->pWatches + Lit;
1058  for ( iCur = p->pWatches[Lit]; iCur; iCur = *piPrev )
1059  {
1060  pCur = Tas_ClsFromHandle( p, iCur );
1061  // make sure the false literal is in the second literal of the clause
1062  if ( pCur->pLits[0] == LitF )
1063  {
1064  pCur->pLits[0] = pCur->pLits[1];
1065  pCur->pLits[1] = LitF;
1066  iTemp = pCur->iNext[0];
1067  pCur->iNext[0] = pCur->iNext[1];
1068  pCur->iNext[1] = iTemp;
1069  }
1070  assert( pCur->pLits[1] == LitF );
1071 
1072  // if the first literal is true, the clause is satisfied
1073 // if ( pCur->pLits[0] == p->pAssigns[Abc_Lit2Var(pCur->pLits[0])] )
1074  pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
1075  if ( Tas_VarIsAssigned(pObj) && Tas_LitIsTrue( pObj, pCur->pLits[0] ) )
1076  {
1077  piPrev = &pCur->iNext[1];
1078  continue;
1079  }
1080 
1081  // look for a new literal to watch
1082  for ( i = 2; i < (int)pCur->nLits; i++ )
1083  {
1084  // skip the case when the literal is false
1085 // if ( Abc_LitNot(pCur->pLits[i]) == p->pAssigns[Abc_Lit2Var(pCur->pLits[i])] )
1086  pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
1087  if ( Tas_VarIsAssigned(pObj) && !Tas_LitIsTrue( pObj, pCur->pLits[i] ) )
1088  continue;
1089  // the literal is either true or unassigned - watch it
1090  pCur->pLits[1] = pCur->pLits[i];
1091  pCur->pLits[i] = LitF;
1092  // remove this clause from the watch list of Lit
1093  *piPrev = pCur->iNext[1];
1094  // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
1095  Tas_ManWatchClause( p, pCur, pCur->pLits[1] );
1096  break;
1097  }
1098  if ( i < (int)pCur->nLits ) // found new watch
1099  continue;
1100 
1101  // clause is unit - enqueue new implication
1102  pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
1103  if ( !Tas_VarIsAssigned(pObj) )
1104  {
1105 /*
1106  {
1107  int iLitLevel, iPlace;
1108  for ( i = 1; i < (int)pCur->nLits; i++ )
1109  {
1110  pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
1111  iLitLevel = Tas_VarDecLevel( p, pObj );
1112  iPlace = pObj->Value;
1113  printf( "Lit = %d. Level = %d. Place = %d.\n", pCur->pLits[i], iLitLevel, iPlace );
1114  i = i;
1115  }
1116  }
1117 */
1118  Tas_ManAssign( p, Gia_ObjFromLit(p->pAig, pCur->pLits[0]), Level, NULL, (Gia_Obj_t *)pCur );
1119  piPrev = &pCur->iNext[1];
1120  continue;
1121  }
1122  // conflict detected - return the conflict clause
1123  assert( !Tas_LitIsTrue( pObj, pCur->pLits[0] ) );
1124  return Tas_ManCreateFromCls( p, pCur, Level );
1125  }
1126  return 0;
1127 }
1128 
1129 
1130 
1131 /**Function*************************************************************
1132 
1133  Synopsis [Propagates a variable.]
1134 
1135  Description [Returns clause handle if conflict; 0 if no conflict.]
1136 
1137  SideEffects []
1138 
1139  SeeAlso []
1140 
1141 ***********************************************************************/
1142 static inline int Tas_ManPropagateOne( Tas_Man_t * p, Gia_Obj_t * pVar, int Level )
1143 {
1144  int Value0, Value1, hClause;
1145  assert( !Gia_IsComplement(pVar) );
1146  assert( Tas_VarIsAssigned(pVar) );
1147  s_Counter3++;
1148  if ( (hClause = Tas_ManPropagateWatch( p, Level, Tas_VarToLit(p, pVar) )) )
1149  return hClause;
1150  if ( Gia_ObjIsCi(pVar) )
1151  return 0;
1152 /*
1153  if ( pVar->iDiff0 == 570869 && pVar->iDiff1 == 546821 && Level == 3 )
1154  {
1155  Gia_Obj_t * pFan0 = Gia_ObjFanin0(pVar);
1156  Gia_Obj_t * pFan1 = Gia_ObjFanin1(pVar);
1157  int s = 0;
1158  }
1159 */
1160  assert( Gia_ObjIsAnd(pVar) );
1161  Value0 = Tas_VarFanin0Value(pVar);
1162  Value1 = Tas_VarFanin1Value(pVar);
1163  if ( Tas_VarValue(pVar) )
1164  { // value is 1
1165  if ( Value0 == 0 || Value1 == 0 ) // one is 0
1166  {
1167  if ( Value0 == 0 && Value1 != 0 )
1168  return Tas_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
1169  if ( Value0 != 0 && Value1 == 0 )
1170  return Tas_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
1171  assert( Value0 == 0 && Value1 == 0 );
1172  return Tas_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
1173  }
1174  if ( Value0 == 2 ) // first is unassigned
1175  Tas_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
1176  if ( Value1 == 2 ) // first is unassigned
1177  Tas_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
1178  return 0;
1179  }
1180  // value is 0
1181  if ( Value0 == 0 || Value1 == 0 ) // one is 0
1182  return 0;
1183  if ( Value0 == 1 && Value1 == 1 ) // both are 1
1184  return Tas_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
1185  if ( Value0 == 1 || Value1 == 1 ) // one is 1
1186  {
1187  if ( Value0 == 2 ) // first is unassigned
1188  Tas_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
1189  if ( Value1 == 2 ) // second is unassigned
1190  Tas_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
1191  return 0;
1192  }
1193  assert( Tas_VarIsJust(pVar) );
1194  assert( !Tas_QueHasNode( &p->pJust, pVar ) );
1195  Tas_QuePush( &p->pJust, pVar );
1196  return 0;
1197 }
1198 
1199 /**Function*************************************************************
1200 
1201  Synopsis [Propagates a variable.]
1202 
1203  Description [Returns 1 if conflict; 0 if no conflict.]
1204 
1205  SideEffects []
1206 
1207  SeeAlso []
1208 
1209 ***********************************************************************/
1210 static inline int Tas_ManPropagateTwo( Tas_Man_t * p, Gia_Obj_t * pVar, int Level )
1211 {
1212  int Value0, Value1;
1213  s_Counter4++;
1214  assert( !Gia_IsComplement(pVar) );
1215  assert( Gia_ObjIsAnd(pVar) );
1216  assert( Tas_VarIsAssigned(pVar) );
1217  assert( !Tas_VarValue(pVar) );
1218  Value0 = Tas_VarFanin0Value(pVar);
1219  Value1 = Tas_VarFanin1Value(pVar);
1220  // value is 0
1221  if ( Value0 == 0 || Value1 == 0 ) // one is 0
1222  return 0;
1223  if ( Value0 == 1 && Value1 == 1 ) // both are 1
1224  return Tas_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
1225  assert( Value0 == 1 || Value1 == 1 );
1226  if ( Value0 == 2 ) // first is unassigned
1227  Tas_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
1228  if ( Value1 == 2 ) // first is unassigned
1229  Tas_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
1230  return 0;
1231 }
1232 
1233 /**Function*************************************************************
1234 
1235  Synopsis [Propagates all variables.]
1236 
1237  Description [Returns 1 if conflict; 0 if no conflict.]
1238 
1239  SideEffects []
1240 
1241  SeeAlso []
1242 
1243 ***********************************************************************/
1244 int Tas_ManPropagate( Tas_Man_t * p, int Level )
1245 {
1246  int hClause;
1247  Gia_Obj_t * pVar;
1248  int i, k;//, nIter = 0;
1249  while ( 1 )
1250  {
1251 // nIter++;
1252  Tas_QueForEachEntry( p->pProp, pVar, i )
1253  {
1254  if ( (hClause = Tas_ManPropagateOne( p, pVar, Level )) )
1255  return hClause;
1256  }
1257  p->pProp.iHead = p->pProp.iTail;
1258  k = p->pJust.iHead;
1259  Tas_QueForEachEntry( p->pJust, pVar, i )
1260  {
1261  if ( Tas_VarIsJust( pVar ) )
1262  p->pJust.pData[k++] = pVar;
1263  else if ( (hClause = Tas_ManPropagateTwo( p, pVar, Level )) )
1264  return hClause;
1265  }
1266  if ( k == p->pJust.iTail )
1267  break;
1268  p->pJust.iTail = k;
1269  }
1270 // printf( "%d ", nIter );
1271  return 0;
1272 }
1273 
1274 /**Function*************************************************************
1275 
1276  Synopsis [Solve the problem recursively.]
1277 
1278  Description [Returns learnt clause if unsat, NULL if sat or undecided.]
1279 
1280  SideEffects []
1281 
1282  SeeAlso []
1283 
1284 ***********************************************************************/
1285 int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
1286 {
1287  Tas_Que_t * pQue = &(p->pClauses);
1288  Gia_Obj_t * pVar, * pDecVar = NULL;
1289  int hClause, hLearn0, hLearn1;
1290  int iPropHead, iJustHead, iJustTail;
1291  // propagate assignments
1292  assert( !Tas_QueIsEmpty(&p->pProp) );
1293  if ( (hClause = Tas_ManPropagate( p, Level )) )
1294  {
1295  Tas_ManCreateCls( p, hClause );
1296  return hClause;
1297  }
1298  // check for satisfying assignment
1299  assert( Tas_QueIsEmpty(&p->pProp) );
1300  if ( Tas_QueIsEmpty(&p->pJust) )
1301  return 0;
1302  // quit using resource limits
1303  p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
1304  if ( Tas_ManCheckLimits( p ) )
1305  return 0;
1306  // remember the state before branching
1307  iPropHead = p->pProp.iHead;
1308  Tas_QueStore( &p->pJust, &iJustHead, &iJustTail );
1309  // find the decision variable
1310  if ( p->Pars.fUseActive )
1311  pVar = NULL, pDecVar = Tas_ManFindActive( p );
1312  else if ( p->Pars.fUseHighest )
1313 // pVar = NULL, pDecVar = Tas_ManDecideHighestFanin( p );
1314  pVar = Tas_ManDecideHighest( p );
1315  else if ( p->Pars.fUseLowest )
1316  pVar = Tas_ManDecideLowest( p );
1317  else if ( p->Pars.fUseMaxFF )
1318  pVar = Tas_ManDecideMaxFF( p );
1319  else assert( 0 );
1320  // chose decision variable using fanout count
1321  if ( pVar != NULL )
1322  {
1323  assert( Tas_VarIsJust( pVar ) );
1324  if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
1325  pDecVar = Gia_Not(Gia_ObjChild0(pVar));
1326  else
1327  pDecVar = Gia_Not(Gia_ObjChild1(pVar));
1328 // pDecVar = Gia_NotCond( pDecVar, Gia_Regular(pDecVar)->fMark1 ^ !Gia_IsComplement(pDecVar) );
1329  }
1330  // decide on first fanin
1331  Tas_ManAssign( p, pDecVar, Level+1, NULL, NULL );
1332  if ( !(hLearn0 = Tas_ManSolve_rec( p, Level+1 )) )
1333  return 0;
1334  if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
1335  return hLearn0;
1336  Tas_ManCancelUntil( p, iPropHead );
1337  Tas_QueRestore( &p->pJust, iJustHead, iJustTail );
1338  // decide on second fanin
1339  Tas_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
1340  if ( !(hLearn1 = Tas_ManSolve_rec( p, Level+1 )) )
1341  return 0;
1342  if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
1343  return hLearn1;
1344  hClause = Tas_ManResolve( p, Level, hLearn0, hLearn1 );
1345  Tas_ManCreateCls( p, hClause );
1346 // Tas_ManPrintClauseNew( p, Level, hClause );
1347 // if ( Level > Tas_ClauseDecLevel(p, hClause) )
1348 // p->Pars.nBTThisNc++;
1349  p->Pars.nBTThis++;
1350  return hClause;
1351 }
1352 
1353 /**Function*************************************************************
1354 
1355  Synopsis [Looking for a satisfying assignment of the node.]
1356 
1357  Description [Assumes that each node has flag pObj->fMark0 set to 0.
1358  Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
1359  The node may be complemented. ]
1360 
1361  SideEffects []
1362 
1363  SeeAlso []
1364 
1365 ***********************************************************************/
1366 int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
1367 {
1368  int i, Entry, RetValue = 0;
1369  s_Counter2 = 0;
1370  Vec_IntClear( p->vModel );
1371  if ( pObj == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj == Gia_Not(pObj2) )
1372  return 1;
1373  if ( pObj == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
1374  return 0;
1375  assert( !p->pProp.iHead && !p->pProp.iTail );
1376  assert( !p->pJust.iHead && !p->pJust.iTail );
1377  assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1378  p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1379  Tas_ManAssign( p, pObj, 0, NULL, NULL );
1380  if ( pObj2 && !Tas_VarIsAssigned(Gia_Regular(pObj2)) )
1381  Tas_ManAssign( p, pObj2, 0, NULL, NULL );
1382  if ( !Tas_ManSolve_rec(p, 0) && !Tas_ManCheckLimits(p) )
1383  Tas_ManSaveModel( p, p->vModel );
1384  else
1385  RetValue = 1;
1386  Tas_ManCancelUntil( p, 0 );
1387  p->pJust.iHead = p->pJust.iTail = 0;
1388  p->pClauses.iHead = p->pClauses.iTail = 1;
1389  // clauses
1390  if ( p->nClauses > 0 )
1391  {
1392  p->pStore.iCur = 16;
1393  Vec_IntForEachEntry( p->vWatchLits, Entry, i )
1394  p->pWatches[Entry] = 0;
1395  Vec_IntClear( p->vWatchLits );
1396  p->nClauses = 0;
1397  }
1398  // activity
1399  Vec_IntForEachEntry( p->vActiveVars, Entry, i )
1400  p->pActivity[Entry] = 0.0;
1401  Vec_IntClear( p->vActiveVars );
1402  // statistics
1403  p->Pars.nBTTotal += p->Pars.nBTThis;
1404  p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1405  if ( Tas_ManCheckLimits( p ) )
1406  RetValue = -1;
1407  return RetValue;
1408 }
1409 
1410 /**Function*************************************************************
1411 
1412  Synopsis [Looking for a satisfying assignment of the node.]
1413 
1414  Description [Assumes that each node has flag pObj->fMark0 set to 0.
1415  Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
1416  The node may be complemented. ]
1417 
1418  SideEffects []
1419 
1420  SeeAlso []
1421 
1422 ***********************************************************************/
1423 int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
1424 {
1425  Gia_Obj_t * pObj;
1426  int i, Entry, RetValue = 0;
1427  s_Counter2 = 0;
1428  s_Counter3 = 0;
1429  s_Counter4 = 0;
1430  Vec_IntClear( p->vModel );
1431  Vec_PtrForEachEntry( Gia_Obj_t *, vObjs, pObj, i )
1432  if ( pObj == Gia_ManConst0(p->pAig) )
1433  return 1;
1434  assert( !p->pProp.iHead && !p->pProp.iTail );
1435  assert( !p->pJust.iHead && !p->pJust.iTail );
1436  assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1437  p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1438  Vec_PtrForEachEntry( Gia_Obj_t *, vObjs, pObj, i )
1439  if ( pObj != Gia_ManConst1(p->pAig) && !Tas_VarIsAssigned(Gia_Regular(pObj)) )
1440  Tas_ManAssign( p, pObj, 0, NULL, NULL );
1441  if ( !Tas_ManSolve_rec(p, 0) && !Tas_ManCheckLimits(p) )
1442  Tas_ManSaveModel( p, p->vModel );
1443  else
1444  RetValue = 1;
1445  Tas_ManCancelUntil( p, 0 );
1446  p->pJust.iHead = p->pJust.iTail = 0;
1447  p->pClauses.iHead = p->pClauses.iTail = 1;
1448  // clauses
1449  if ( p->nClauses > 0 )
1450  {
1451  p->pStore.iCur = 16;
1452  Vec_IntForEachEntry( p->vWatchLits, Entry, i )
1453  p->pWatches[Entry] = 0;
1454  Vec_IntClear( p->vWatchLits );
1455  p->nClauses = 0;
1456  }
1457  // activity
1458  Vec_IntForEachEntry( p->vActiveVars, Entry, i )
1459  p->pActivity[Entry] = 0.0;
1460  Vec_IntClear( p->vActiveVars );
1461  // statistics
1462  p->Pars.nBTTotal += p->Pars.nBTThis;
1463  p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1464  if ( Tas_ManCheckLimits( p ) )
1465  RetValue = -1;
1466 
1467 // printf( "%d ", Gia_ManObjNum(p->pAig) );
1468 // printf( "%d ", p->Pars.nBTThis );
1469 // printf( "%d ", p->Pars.nJustThis );
1470 // printf( "%d ", s_Counter2 );
1471 // printf( "%d ", s_Counter3 );
1472 // printf( "%d ", s_Counter4 );
1473  return RetValue;
1474 }
1475 
1476 /**Function*************************************************************
1477 
1478  Synopsis [Prints statistics of the manager.]
1479 
1480  Description []
1481 
1482  SideEffects []
1483 
1484  SeeAlso []
1485 
1486 ***********************************************************************/
1487 void Tas_ManSatPrintStats( Tas_Man_t * p )
1488 {
1489  printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
1490  printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
1491  printf( "Conf = %6d ", p->Pars.nBTLimit );
1492  printf( "JustMax = %5d ", p->Pars.nJustLimit );
1493  printf( "\n" );
1494  printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1495  p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
1496  ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
1497  printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1498  p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
1499  ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
1500  printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
1501  p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
1502  ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
1503  ABC_PRT( "Total time", p->timeTotal );
1504 }
1505 
1506 /**Function*************************************************************
1507 
1508  Synopsis [Procedure to test the new SAT solver.]
1509 
1510  Description []
1511 
1512  SideEffects []
1513 
1514  SeeAlso []
1515 
1516 ***********************************************************************/
1517 Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
1518 {
1519  extern void Gia_ManCollectTest( Gia_Man_t * pAig );
1520  extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1521  Tas_Man_t * p;
1522  Vec_Int_t * vCex, * vVisit, * vCexStore;
1523  Vec_Str_t * vStatus;
1524  Gia_Obj_t * pRoot;//, * pRootCopy;
1525 // Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
1526 
1527  int i, status;
1528  abctime clk, clkTotal = Abc_Clock();
1529  assert( Gia_ManRegNum(pAig) == 0 );
1530 // Gia_ManCollectTest( pAig );
1531  // prepare AIG
1532  Gia_ManCreateRefs( pAig );
1533  Gia_ManCleanMark0( pAig );
1534  Gia_ManCleanMark1( pAig );
1535  Gia_ManFillValue( pAig ); // maps nodes into trail ids
1536  Gia_ManCleanPhase( pAig ); // maps nodes into trail ids
1537  // create logic network
1538  p = Tas_ManAlloc( pAig, nConfs );
1539  p->pAig = pAig;
1540  // create resulting data-structures
1541  vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1542  vCexStore = Vec_IntAlloc( 10000 );
1543  vVisit = Vec_IntAlloc( 100 );
1544  vCex = Tas_ReadModel( p );
1545  // solve for each output
1546  Gia_ManForEachCo( pAig, pRoot, i )
1547  {
1548 // printf( "%d=", i );
1549 
1550  Vec_IntClear( vCex );
1551  if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
1552  {
1553  if ( Gia_ObjFaninC0(pRoot) )
1554  {
1555 // printf( "Constant 1 output of SRM!!!\n" );
1556  Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
1557  Vec_StrPush( vStatus, 0 );
1558  }
1559  else
1560  {
1561 // printf( "Constant 0 output of SRM!!!\n" );
1562  Vec_StrPush( vStatus, 1 );
1563  }
1564  continue;
1565  }
1566  clk = Abc_Clock();
1567 // p->Pars.fUseActive = 1;
1568  p->Pars.fUseHighest = 1;
1569  p->Pars.fUseLowest = 0;
1570  status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
1571 // printf( "\n" );
1572 /*
1573  if ( status == -1 )
1574  {
1575  p->Pars.fUseHighest = 0;
1576  p->Pars.fUseLowest = 1;
1577  status = Tas_ManSolve( p, Gia_ObjChild0(pRoot) );
1578  }
1579 */
1580  Vec_StrPush( vStatus, (char)status );
1581  if ( status == -1 )
1582  {
1583 // printf( "Unsolved %d.\n", i );
1584 
1585  p->nSatUndec++;
1586  p->nConfUndec += p->Pars.nBTThis;
1587  Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1588  p->timeSatUndec += Abc_Clock() - clk;
1589  continue;
1590  }
1591 
1592 // pRootCopy = Gia_ManCo( pAigCopy, i );
1593 // pRootCopy->iDiff0 = Gia_ObjId( pAigCopy, pRootCopy );
1594 // pRootCopy->fCompl0 = 0;
1595 
1596  if ( status == 1 )
1597  {
1598  p->nSatUnsat++;
1599  p->nConfUnsat += p->Pars.nBTThis;
1600  p->timeSatUnsat += Abc_Clock() - clk;
1601  continue;
1602  }
1603  p->nSatSat++;
1604  p->nConfSat += p->Pars.nBTThis;
1605 // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1606  Cec_ManSatAddToStore( vCexStore, vCex, i );
1607  p->timeSatSat += Abc_Clock() - clk;
1608 
1609 // printf( "%d ", Vec_IntSize(vCex) );
1610  }
1611 // pAigCopy = Gia_ManCleanup( pAigTemp = pAigCopy );
1612 // Gia_ManStop( pAigTemp );
1613 // Gia_DumpAiger( pAigCopy, "test", 0, 2 );
1614 // Gia_ManStop( pAigCopy );
1615 
1616  Vec_IntFree( vVisit );
1617  p->nSatTotal = Gia_ManPoNum(pAig);
1618  p->timeTotal = Abc_Clock() - clkTotal;
1619  if ( fVerbose )
1620  Tas_ManSatPrintStats( p );
1621 // printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
1622  Tas_ManStop( p );
1623  *pvStatus = vStatus;
1624 
1625 // printf( "Total number of cex literals = %d. (Ave = %d)\n",
1626 // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
1627 // (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
1628  return vCexStore;
1629 }
1630 
1631 /**Function*************************************************************
1632 
1633  Synopsis [Packs patterns into array of simulation info.]
1634 
1635  Description []
1636 
1637  SideEffects []
1638 
1639  SeeAlso []
1640 
1641 *************************************`**********************************/
1642 int Tas_StorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
1643 {
1644  unsigned * pInfo, * pPres;
1645  int i;
1646  for ( i = 0; i < nLits; i++ )
1647  {
1648  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
1649  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
1650  if ( Abc_InfoHasBit( pPres, iBit ) &&
1651  Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
1652  return 0;
1653  }
1654  for ( i = 0; i < nLits; i++ )
1655  {
1656  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
1657  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
1658  Abc_InfoSetBit( pPres, iBit );
1659  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
1660  Abc_InfoXorBit( pInfo, iBit );
1661  }
1662  return 1;
1663 }
1664 
1665 /**Function*************************************************************
1666 
1667  Synopsis [Procedure to test the new SAT solver.]
1668 
1669  Description []
1670 
1671  SideEffects []
1672 
1673  SeeAlso []
1674 
1675 ***********************************************************************/
1676 int Tas_StorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex )
1677 {
1678  int k;
1679  for ( k = 1; k < 32; k++ )
1680  if ( Tas_StorePatternTry( vSimInfo, vPres, k, (int *)Vec_IntArray(vCex), Vec_IntSize(vCex) ) )
1681  break;
1682  return (int)(k < 32);
1683 }
1684 
1685 /**Function*************************************************************
1686 
1687  Synopsis [Procedure to test the new SAT solver.]
1688 
1689  Description []
1690 
1691  SideEffects []
1692 
1693  SeeAlso []
1694 
1695 ***********************************************************************/
1696 void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Vec_Ptr_t * vOldRoots, Vec_Ptr_t * vSimInfo )
1697 {
1698  int nPatMax = 1000;
1699  int fVerbose = 1;
1700  extern void Gia_ManCollectTest( Gia_Man_t * pAig );
1701  extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1702  Tas_Man_t * p;
1703  Vec_Ptr_t * vPres;
1704  Vec_Int_t * vCex, * vVisit, * vCexStore;
1705  Vec_Str_t * vStatus;
1706  Gia_Obj_t * pRoot, * pOldRoot;
1707  int i, status;
1708  abctime clk, clkTotal = Abc_Clock();
1709  int Tried = 0, Stored = 0, Step = Gia_ManCoNum(pAig) / nPatMax;
1710  assert( Gia_ManRegNum(pAig) == 0 );
1711 // Gia_ManCollectTest( pAig );
1712  // prepare AIG
1713  Gia_ManCreateRefs( pAig );
1714  Gia_ManCleanMark0( pAig );
1715  Gia_ManCleanMark1( pAig );
1716  Gia_ManFillValue( pAig ); // maps nodes into trail ids
1717  Gia_ManCleanPhase( pAig ); // maps nodes into trail ids
1718  // create logic network
1719  p = Tas_ManAlloc( pAig, nConfs );
1720  p->pAig = pAig;
1721  // create resulting data-structures
1722  vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1723  vCexStore = Vec_IntAlloc( 10000 );
1724  vVisit = Vec_IntAlloc( 100 );
1725  vCex = Tas_ReadModel( p );
1726  // solve for each output
1727  vPres = Vec_PtrAllocSimInfo( Gia_ManCiNum(pAig), 1 );
1728  Vec_PtrCleanSimInfo( vPres, 0, 1 );
1729 
1730  Gia_ManForEachCo( pAig, pRoot, i )
1731  {
1732  assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) );
1733  Vec_IntClear( vCex );
1734  clk = Abc_Clock();
1735  p->Pars.fUseHighest = 1;
1736  p->Pars.fUseLowest = 0;
1737  status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
1738  Vec_StrPush( vStatus, (char)status );
1739  if ( status == -1 )
1740  {
1741  p->nSatUndec++;
1742  p->nConfUndec += p->Pars.nBTThis;
1743 // Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1744  p->timeSatUndec += Abc_Clock() - clk;
1745 
1746  i += Step;
1747  continue;
1748  }
1749  if ( status == 1 )
1750  {
1751  p->nSatUnsat++;
1752  p->nConfUnsat += p->Pars.nBTThis;
1753  p->timeSatUnsat += Abc_Clock() - clk;
1754  // record proved
1755  pOldRoot = (Gia_Obj_t *)Vec_PtrEntry( vOldRoots, i );
1756  assert( !Gia_ObjProved( pAigOld, Gia_ObjId(pAigOld, pOldRoot) ) );
1757  Gia_ObjSetProved( pAigOld, Gia_ObjId(pAigOld, pOldRoot) );
1758 
1759  i += Step;
1760  continue;
1761  }
1762  p->nSatSat++;
1763  p->nConfSat += p->Pars.nBTThis;
1764 // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1765 // Cec_ManSatAddToStore( vCexStore, vCex, i );
1766 
1767  // save pattern
1768  Tried++;
1769  Stored += Tas_StorePattern( vSimInfo, vPres, vCex );
1770  p->timeSatSat += Abc_Clock() - clk;
1771  i += Step;
1772  }
1773  printf( "Tried = %d Stored = %d\n", Tried, Stored );
1774  Vec_IntFree( vVisit );
1775  p->nSatTotal = Gia_ManPoNum(pAig);
1776  p->timeTotal = Abc_Clock() - clkTotal;
1777  if ( fVerbose )
1778  Tas_ManSatPrintStats( p );
1779  Tas_ManStop( p );
1780  Vec_PtrFree( vPres );
1781 }
1782 
1783 
1784 ////////////////////////////////////////////////////////////////////////
1785 /// END OF FILE ///
1786 ////////////////////////////////////////////////////////////////////////
1787 
1788 
1789 ABC_NAMESPACE_IMPL_END
1790 
memset
char * memset()
Tas_StorePatternTry
int Tas_StorePatternTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition: giaCTas.c:1642
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Gia_ManCleanPhase
void Gia_ManCleanPhase(Gia_Man_t *p)
Definition: giaUtil.c:431
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Tas_ManCreateFromCls
static int Tas_ManCreateFromCls(Tas_Man_t *p, Tas_Cls_t *pCls, int Level)
Definition: giaCTas.c:1021
Tas_Sto_t_::nSize
int nSize
Definition: giaCTas.c:69
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Tas_Man_t_::timeSatUndec
abctime timeSatUndec
Definition: giaCTas.c:113
Tas_ManResolve
static int Tas_ManResolve(Tas_Man_t *p, int Level, int hClause0, int hClause1)
Definition: giaCTas.c:873
Tas_Man_t_::pIter
Gia_Obj_t ** pIter
Definition: giaCTas.c:89
Tas_QueRestore
static void Tas_QueRestore(Tas_Que_t *p, int iHeadOld, int iTailOld)
Definition: giaCTas.c:401
Tas_Man_t_::pWatches
int * pWatches
Definition: giaCTas.c:95
Tas_Man_t_
Definition: giaCTas.c:82
Tas_Par_t_::fUseMaxFF
int fUseMaxFF
Definition: giaCTas.c:52
Tas_Par_t_::nJustThis
int nJustThis
Definition: giaCTas.c:42
Tas_ManDecideHighestFanin
static Gia_Obj_t * Tas_ManDecideHighestFanin(Tas_Man_t *p)
Definition: giaCTas.c:499
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Tas_VarReason1
static Gia_Obj_t * Tas_VarReason1(Tas_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCTas.c:133
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
Tas_ManDecideLowest
static Gia_Obj_t * Tas_ManDecideLowest(Tas_Man_t *p)
Definition: giaCTas.c:575
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Tas_Man_t_::timeTotal
abctime timeTotal
Definition: giaCTas.c:114
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ObjFromLit
static Gia_Obj_t * Gia_ObjFromLit(Gia_Man_t *p, int iLit)
Definition: gia.h:496
Tas_Par_t_::nJustTotal
int nJustTotal
Definition: giaCTas.c:44
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
Tas_ManPrintClause
static void Tas_ManPrintClause(Tas_Man_t *p, int Level, int hClause)
Definition: giaCTas.c:710
Tas_Man_t_::vActiveVars
Vec_Int_t * vActiveVars
Definition: giaCTas.c:100
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Tas_ManSaveModel
static void Tas_ManSaveModel(Tas_Man_t *p, Vec_Int_t *vCex)
Definition: giaCTas.c:285
Tas_Man_t_::pAig
Gia_Man_t * pAig
Definition: giaCTas.c:85
Tas_ManDeriveReason
static void Tas_ManDeriveReason(Tas_Man_t *p, int Level)
Definition: giaCTas.c:756
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Tas_Par_t_::nBTThisNc
int nBTThisNc
Definition: giaCTas.c:41
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
Tas_Man_t_::pProp
Tas_Que_t pProp
Definition: giaCTas.c:86
Tas_Cls_t_::iNext
int iNext[2]
Definition: giaCTas.c:60
Tas_VarFanin1Value
static int Tas_VarFanin1Value(Gia_Obj_t *pVar)
Definition: giaCTas.c:124
Tas_Que_t_::iHead
int iHead
Definition: giaCTas.c:76
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Tas_VarValue
static int Tas_VarValue(Gia_Obj_t *pVar)
Definition: giaCTas.c:120
Tas_ManAssign
static void Tas_ManAssign(Tas_Man_t *p, Gia_Obj_t *pObj, int Level, Gia_Obj_t *pRes0, Gia_Obj_t *pRes1)
Definition: giaCTas.c:654
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
Tas_Par_t_::VarInc
int VarInc
Definition: giaCTas.c:47
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Tas_Man_t_::pActivity
float * pActivity
Definition: giaCTas.c:99
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Tas_Par_t_::nBTThis
int nBTThis
Definition: giaCTas.c:40
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
Tas_Par_t_::VarDecay
float VarDecay
Definition: giaCTas.c:46
Tas_Man_t_::nSatTotal
int nSatTotal
Definition: giaCTas.c:105
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Tas_VarFanin0Value
static int Tas_VarFanin0Value(Gia_Obj_t *pVar)
Definition: giaCTas.c:123
Tas_ManAnalyze
static int Tas_ManAnalyze(Tas_Man_t *p, int Level, Gia_Obj_t *pVar, Gia_Obj_t *pFan0, Gia_Obj_t *pFan1)
Definition: giaCTas.c:845
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Tas_ManClauseSize
static int Tas_ManClauseSize(Tas_Man_t *p, int hClause)
Definition: giaCTas.c:691
Tas_ManSolveMiterNc2
void Tas_ManSolveMiterNc2(Gia_Man_t *pAig, int nConfs, Gia_Man_t *pAigOld, Vec_Ptr_t *vOldRoots, Vec_Ptr_t *vSimInfo)
Definition: giaCTas.c:1696
Tas_Cls_t_::nLits
int nLits
Definition: giaCTas.c:61
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
Gia_ManConst1
static Gia_Obj_t * Gia_ManConst1(Gia_Man_t *p)
Definition: gia.h:401
Tas_Par_t_::fUseHighest
int fUseHighest
Definition: giaCTas.c:50
Tas_ManPrintClauseNew
static void Tas_ManPrintClauseNew(Tas_Man_t *p, int Level, int hClause)
Definition: giaCTas.c:733
Tas_Par_t_::fVerbose
int fVerbose
Definition: giaCTas.c:54
Tas_VarToLit
static int Tas_VarToLit(Tas_Man_t *p, Gia_Obj_t *pObj)
Definition: giaCTas.c:125
Tas_ClauseDecLevel
static int Tas_ClauseDecLevel(Tas_Man_t *p, int hClause)
Definition: giaCTas.c:134
Tas_ManWatchClause
static void Tas_ManWatchClause(Tas_Man_t *p, Tas_Cls_t *pClause, int Lit)
Definition: giaCTas.c:954
Tas_ManPropagateOne
static int Tas_ManPropagateOne(Tas_Man_t *p, Gia_Obj_t *pVar, int Level)
Definition: giaCTas.c:1142
Tas_Par_t_::nJustLimit
int nJustLimit
Definition: giaCTas.c:38
Tas_Par_t_::nBTTotal
int nBTTotal
Definition: giaCTas.c:43
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
Tas_Man_t_::nConfUnsat
int nConfUnsat
Definition: giaCTas.c:107
Tas_Que_t_::pData
Gia_Obj_t ** pData
Definition: giaCTas.c:79
Tas_ManSolveMiterNc
Vec_Int_t * Tas_ManSolveMiterNc(Gia_Man_t *pAig, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCTas.c:1517
Tas_Man_t_::nConfSat
int nConfSat
Definition: giaCTas.c:108
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
Tas_QueHasNode
static int Tas_QueHasNode(Tas_Que_t *p, Gia_Obj_t *pObj)
Definition: giaCTas.c:359
Tas_ManStop
void Tas_ManStop(Tas_Man_t *p)
Definition: giaCTas.c:223
Tas_VarIsAssigned
static int Tas_VarIsAssigned(Gia_Obj_t *pVar)
Definition: giaCTas.c:117
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Tas_Sto_t_::iCur
int iCur
Definition: giaCTas.c:68
Tas_QueForEachEntry
#define Tas_QueForEachEntry(Que, pObj, i)
Definition: giaCTas.c:139
Tas_Sto_t_
Definition: giaCTas.c:66
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
s_Counter3
int s_Counter3
Definition: giaCTas.c:640
Tas_Man_t_::nClauses
int nClauses
Definition: giaCTas.c:97
Tas_Man_t_::nSatUnsat
int nSatUnsat
Definition: giaCTas.c:102
Tas_Man_t_::pStore
Tas_Sto_t pStore
Definition: giaCTas.c:94
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjSetProved
static void Gia_ObjSetProved(Gia_Man_t *p, int Id)
Definition: gia.h:897
Tas_Sto_t_::pData
int * pData
Definition: giaCTas.c:70
Tas_ManDecideMaxFF
static Gia_Obj_t * Tas_ManDecideMaxFF(Tas_Man_t *p)
Definition: giaCTas.c:596
Tas_Que_t_::nSize
int nSize
Definition: giaCTas.c:78
Tas_ManSolve
int Tas_ManSolve(Tas_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pObj2)
Definition: giaCTas.c:1366
Tas_VarHasReasonCls
static int Tas_VarHasReasonCls(Tas_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCTas.c:136
Tas_Man_t_::vLevReas
Vec_Int_t * vLevReas
Definition: giaCTas.c:90
Tas_QuePush
static void Tas_QuePush(Tas_Que_t *p, Gia_Obj_t *pObj)
Definition: giaCTas.c:338
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Tas_StorePattern
int Tas_StorePattern(Vec_Ptr_t *vSimInfo, Vec_Ptr_t *vPres, Vec_Int_t *vCex)
Definition: giaCTas.c:1676
Tas_LitIsTrue
static int Tas_LitIsTrue(Gia_Obj_t *pObj, int Lit)
Definition: giaCTas.c:126
Tas_Par_t_
Definition: giaCTas.c:34
Tas_SetDefaultParams
void Tas_SetDefaultParams(Tas_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: giaCTas.c:162
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Tas_Cls_t_
Definition: giaCTas.c:58
Tas_Man_t_::nSatSat
int nSatSat
Definition: giaCTas.c:103
Tas_Man_t_::timeSatSat
abctime timeSatSat
Definition: giaCTas.c:112
Tas_ManPropagate
int Tas_ManPropagate(Tas_Man_t *p, int Level)
Definition: giaCTas.c:1244
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
Tas_ManDecideHighest
static Gia_Obj_t * Tas_ManDecideHighest(Tas_Man_t *p)
Definition: giaCTas.c:526
Tas_ManDecideHighestA
static Gia_Obj_t * Tas_ManDecideHighestA(Tas_Man_t *p)
Definition: giaCTas.c:551
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Tas_VarUnassign
static void Tas_VarUnassign(Gia_Obj_t *pVar)
Definition: giaCTas.c:119
Tas_Que_t_
Definition: giaCTas.c:74
Tas_Par_t
typedefABC_NAMESPACE_IMPL_START struct Tas_Par_t_ Tas_Par_t
DECLARATIONS ///.
Definition: giaCTas.c:33
Tas_VarIsJust
static int Tas_VarIsJust(Gia_Obj_t *pVar)
Definition: giaCTas.c:122
Tas_Par_t_::nBTLimit
int nBTLimit
Definition: giaCTas.c:37
Tas_ManSolve_rec
int Tas_ManSolve_rec(Tas_Man_t *p, int Level)
Definition: giaCTas.c:1285
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Tas_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition: giaCTas.c:111
s_Counter4
int s_Counter4
Definition: giaCTas.c:641
Cec_ManSatAddToStore
void Cec_ManSatAddToStore(Vec_Int_t *vCexStore, Vec_Int_t *vCex, int Out)
Definition: cecSolve.c:952
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Tas_Par_t_::fUseLowest
int fUseLowest
Definition: giaCTas.c:51
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Tas_Man_t_::vWatchLits
Vec_Int_t * vWatchLits
Definition: giaCTas.c:96
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
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
Tas_ManAllocCls
static Tas_Cls_t * Tas_ManAllocCls(Tas_Man_t *p, int nSize)
Definition: giaCTas.c:929
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
Tas_ClsFromHandle
static Tas_Cls_t * Tas_ClsFromHandle(Tas_Man_t *p, int h)
Definition: giaCTas.c:129
Tas_ManSolveArray
int Tas_ManSolveArray(Tas_Man_t *p, Vec_Ptr_t *vObjs)
Definition: giaCTas.c:1423
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Tas_VarDecLevel
static int Tas_VarDecLevel(Tas_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCTas.c:131
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Tas_Par_t_::fUseActive
int fUseActive
Definition: giaCTas.c:49
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Tas_ManPropagateWatch
static int Tas_ManPropagateWatch(Tas_Man_t *p, int Level, int Lit)
Definition: giaCTas.c:1050
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Tas_ManFindActive
static Gia_Obj_t * Tas_ManFindActive(Tas_Man_t *p)
Definition: giaCTas.c:462
Tas_Man_t_::pClauses
Tas_Que_t pClauses
Definition: giaCTas.c:88
Tas_QueIsEmpty
static int Tas_QueIsEmpty(Tas_Que_t *p)
Definition: giaCTas.c:322
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Tas_Man_t_::pJust
Tas_Que_t pJust
Definition: giaCTas.c:87
Tas_ManCreateCls
static Tas_Cls_t * Tas_ManCreateCls(Tas_Man_t *p, int hClause)
Definition: giaCTas.c:979
Tas_Man_t_::nConfUndec
int nConfUndec
Definition: giaCTas.c:109
Gia_ObjProved
static int Gia_ObjProved(Gia_Man_t *p, int Id)
Definition: gia.h:896
s_Counter2
int s_Counter2
Definition: giaCTas.c:639
Tas_Que_t_::iTail
int iTail
Definition: giaCTas.c:77
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Tas_VarReasonCls
static Tas_Cls_t * Tas_VarReasonCls(Tas_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCTas.c:137
Tas_ManPropagateTwo
static int Tas_ManPropagateTwo(Tas_Man_t *p, Gia_Obj_t *pVar, int Level)
Definition: giaCTas.c:1210
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_ManCollectTest
void Gia_ManCollectTest(Gia_Man_t *p)
Definition: giaDfs.c:208
Tas_Cls_t_::pLits
int pLits[0]
Definition: giaCTas.c:62
Tas_ManSatPrintStats
void Tas_ManSatPrintStats(Tas_Man_t *p)
Definition: giaCTas.c:1487
Tas_ReadModel
Vec_Int_t * Tas_ReadModel(Tas_Man_t *p)
Definition: giaCTas.c:250
Tas_VarFaninFanoutMax
static int Tas_VarFaninFanoutMax(Tas_Man_t *p, Gia_Obj_t *pObj)
Definition: giaCTas.c:439
Tas_VarAssign
static void Tas_VarAssign(Gia_Obj_t *pVar)
Definition: giaCTas.c:118
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
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Tas_ManCancelUntil
static void Tas_ManCancelUntil(Tas_Man_t *p, int iBound)
Definition: giaCTas.c:627
Tas_ManAlloc
Tas_Man_t * Tas_ManAlloc(Gia_Man_t *pAig, int nBTLimit)
Definition: giaCTas.c:187
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
Tas_ManCheckLimits
static int Tas_ManCheckLimits(Tas_Man_t *p)
Definition: giaCTas.c:269
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Tas_Man_t_::vTemp
Vec_Ptr_t * vTemp
Definition: giaCTas.c:92
Tas_QueStore
static void Tas_QueStore(Tas_Que_t *p, int *piHeadOld, int *piTailOld)
Definition: giaCTas.c:380
Tas_VarReason0
static Gia_Obj_t * Tas_VarReason0(Tas_Man_t *p, Gia_Obj_t *pVar)
Definition: giaCTas.c:132
Tas_Man_t_::vModel
Vec_Int_t * vModel
Definition: giaCTas.c:91
Tas_ClsHandle
static int Tas_ClsHandle(Tas_Man_t *p, Tas_Cls_t *pClause)
Definition: giaCTas.c:128
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Tas_VarSetValue
static void Tas_VarSetValue(Gia_Obj_t *pVar, int v)
Definition: giaCTas.c:121
Tas_Man_t_::nSatUndec
int nSatUndec
Definition: giaCTas.c:104
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Tas_Man_t_::Pars
Tas_Par_t Pars
Definition: giaCTas.c:84
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Tas_QueFinish
static int Tas_QueFinish(Tas_Que_t *p)
Definition: giaCTas.c:418