abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecSplit.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecSplit.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Cofactoring for combinational miters.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <math.h>
22 #include "aig/gia/gia.h"
23 #include "aig/gia/giaAig.h"
24 #include "sat/cnf/cnf.h"
25 #include "sat/bsat/satSolver.h"
26 #include "misc/util/utilTruth.h"
27 //#include "bdd/cudd/cuddInt.h"
28 
29 #ifdef ABC_USE_PTHREADS
30 
31 #ifdef _WIN32
32 #include "../lib/pthread.h"
33 #else
34 #include <pthread.h>
35 #include <unistd.h>
36 #endif
37 
38 #endif
39 
40 ABC_NAMESPACE_IMPL_START
41 
42 
43 ////////////////////////////////////////////////////////////////////////
44 /// DECLARATIONS ///
45 ////////////////////////////////////////////////////////////////////////
46 
47 #ifndef ABC_USE_PTHREADS
48 
49 int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { return -1; }
50 
51 #else // pthreads are used
52 
53 ////////////////////////////////////////////////////////////////////////
54 /// FUNCTION DEFINITIONS ///
55 ////////////////////////////////////////////////////////////////////////
56 
57 #if 0 // BDD code
58 
59 /**Function*************************************************************
60 
61  Synopsis [Permute primary inputs.]
62 
63  Description []
64 
65  SideEffects []
66 
67  SeeAlso []
68 
69 ***********************************************************************/
70 DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip )
71 {
72  abctime clk = Abc_Clock();
73  DdManager * dd;
74  DdNode * bBdd, * bBdd0, * bBdd1;
75  Vec_Ptr_t * vNodes;
76  Gia_Obj_t * pObj;
77  int i;
78  vNodes = Vec_PtrStart( Gia_ManObjNum(p) );
79  dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
80 // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
81  bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
82  Vec_PtrWriteEntry( vNodes, 0, bBdd );
83  Gia_ManForEachPi( p, pObj, i )
84  {
85  bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
86  Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
87  }
88  Gia_ManForEachAnd( p, pObj, i )
89  {
90  bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
91  bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
92  bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
93  Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
94  if ( i % 10 == 0 )
95  printf( "%d ", i );
96 // if ( i == 3000 )
97 // break;
98  }
99  printf( "\n" );
100  Gia_ManForEachPo( p, pObj, i )
101  {
102  bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) ); Cudd_Ref( bBdd );
103  Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
104  }
105  if ( bBdd == Cudd_ReadLogicZero(dd) )
106  printf( "Equivalent!\n" );
107  else
108  printf( "Not tquivalent!\n" );
109  if ( pvNodes )
110  *pvNodes = vNodes;
111  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
112  return dd;
113 }
114 void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes )
115 {
116  DdNode * bBdd;
117  int i;
118  Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i )
119  if ( bBdd )
120  Cudd_RecursiveDeref( dd, bBdd );
121  if ( Cudd_CheckZeroRef(dd) > 0 )
122  printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) );
123  Cudd_PrintInfo( dd, stdout );
124  Cudd_Quit( dd );
125 }
126 void Gia_ManBuildBddTest( Gia_Man_t * p )
127 {
128  Vec_Ptr_t * vNodes;
129  DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 );
130  Gia_ManDerefBdd( dd, vNodes );
131 }
132 
133 #endif // BDD code
134 
135 /**Function*************************************************************
136 
137  Synopsis []
138 
139  Description []
140 
141  SideEffects []
142 
143  SeeAlso []
144 
145 ***********************************************************************/
146 void Cec_GiaSplitExplore( Gia_Man_t * p )
147 {
148  Gia_Obj_t * pObj, * pFan0, * pFan1;
149  int i, Counter = 0;
150  assert( p->pMuxes == NULL );
151  ABC_FREE( p->pRefs );
152  Gia_ManCreateRefs( p );
153  Gia_ManForEachAnd( p, pObj, i )
154  {
155  if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
156  continue;
157  if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 &&
158  Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 )
159  continue;
160  printf( "%5d : ", Counter++ );
161  printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) );
162  printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) );
163  }
164 }
165 
166 /**Function*************************************************************
167 
168  Synopsis [Find cofactoring variable.]
169 
170  Description []
171 
172  SideEffects []
173 
174  SeeAlso []
175 
176 ***********************************************************************/
177 int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
178 {
179  Vec_Int_t * vPerm;
180  Gia_Obj_t * pObj;
181  int i, * pOrder;
182  Gia_ManCreateRefs( p );
183  vPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
184  Gia_ManForEachPi( p, pObj, i )
185  Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
186  pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
187  Vec_IntFree( vPerm );
188  return pOrder;
189 }
190 Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
191 {
192  Gia_Man_t * pNew;
193  Vec_Int_t * vPerm;
194  int * pOrder = Gia_PermuteSpecialOrder( p );
195  vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
196  pNew = Gia_ManDupPerm( p, vPerm );
197  Vec_IntFree( vPerm );
198  return pNew;
199 }
200 
201 /**Function*************************************************************
202 
203  Synopsis [Find cofactoring variable.]
204 
205  Description []
206 
207  SideEffects []
208 
209  SeeAlso []
210 
211 ***********************************************************************/
212 int Gia_SplitCofVar2( Gia_Man_t * p, int * pnFanouts, int * pnCost )
213 {
214  Gia_Obj_t * pObj;
215  int i, iBest = -1, CostBest = -1;
216  if ( p->pRefs == NULL )
217  Gia_ManCreateRefs( p );
218  Gia_ManForEachPi( p, pObj, i )
219  if ( CostBest < Gia_ObjRefNum(p, pObj) )
220  iBest = i, CostBest = Gia_ObjRefNum(p, pObj);
221  assert( iBest >= 0 );
222  *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
223  *pnCost = -1;
224  return iBest;
225 }
226 int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost )
227 {
228  Gia_Man_t * pPart;
229  int Cost0, Cost1, CostBest = ABC_INFINITY;
230  int * pOrder, i, iBest = -1;
231  if ( LookAhead == 1 )
232  return Gia_SplitCofVar2( p, pnFanouts, pnCost );
233  pOrder = Gia_PermuteSpecialOrder( p );
234  LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
235  for ( i = 0; i < LookAhead; i++ )
236  {
237  pPart = Gia_ManDupCofactorVar( p, pOrder[i], 0 );
238  Cost0 = Gia_ManAndNum(pPart);
239  Gia_ManStop( pPart );
240 
241  pPart = Gia_ManDupCofactorVar( p, pOrder[i], 1 );
242  Cost1 = Gia_ManAndNum(pPart);
243  Gia_ManStop( pPart );
244 
245  if ( CostBest > Cost0 + Cost1 )
246  CostBest = Cost0 + Cost1, iBest = pOrder[i];
247 
248 /*
249  pPart = Gia_ManDupExist( p, pOrder[i] );
250  printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d %6d -> %6d\n",
251  i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
252  Cost0, Cost1, Cost0+Cost1, Gia_ManAndNum(p), Gia_ManAndNum(pPart) );
253  Gia_ManStop( pPart );
254 
255  printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n",
256  i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
257  Cost0, Cost1, Cost0+Cost1 );
258 */
259  }
260  ABC_FREE( pOrder );
261  assert( iBest >= 0 );
262  *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
263  *pnCost = CostBest;
264  return iBest;
265 }
266 
267 /**Function*************************************************************
268 
269  Synopsis []
270 
271  Description []
272 
273  SideEffects []
274 
275  SeeAlso []
276 
277 ***********************************************************************/
278 Abc_Cex_t * Cec_SplitDeriveModel( Gia_Man_t * p, Cnf_Dat_t * pCnf, sat_solver * pSat )
279 {
280  Abc_Cex_t * pCex;
281  Gia_Obj_t * pObj;
282  int i, iLit, * pModel;
283  pModel = ABC_CALLOC( int, Gia_ManPiNum(p) );
284  Gia_ManForEachPi( p, pObj, i )
285  pModel[i] = sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(p, pObj)]);
286  if ( p->vCofVars )
287  Vec_IntForEachEntry( p->vCofVars, iLit, i )
288  pModel[Abc_Lit2Var(iLit)] = !Abc_LitIsCompl(iLit);
289  pCex = Abc_CexCreate( 0, Gia_ManPiNum(p), pModel, 0, 0, 0 );
290  ABC_FREE( pModel );
291  return pCex;
292 }
293 
294 /**Function*************************************************************
295 
296  Synopsis []
297 
298  Description []
299 
300  SideEffects []
301 
302  SeeAlso []
303 
304 ***********************************************************************/
305 static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
306 {
307  Cnf_Dat_t * pCnf;
308  Aig_Man_t * pAig = Gia_ManToAigSimple( p );
309  pAig->nRegs = 0;
310  pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) );
311  Aig_ManStop( pAig );
312  return pCnf;
313 }
314 static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut )
315 {
316  sat_solver * pSat;
317  int i;
318  pSat = sat_solver_new();
319  sat_solver_setnvars( pSat, pCnf->nVars );
320  for ( i = 0; i < pCnf->nClauses; i++ )
321  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
322  {
323  // the problem is UNSAT
324  sat_solver_delete( pSat );
325  return NULL;
326  }
327  sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
328  return pSat;
329 }
330 static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
331 {
332  int status;
333  sat_solver * pSat = Cec_GiaDeriveSolver( p, pCnf, nTimeOut );
334  if ( pSat == NULL )
335  {
336  *pnVars = 0;
337  *pnConfs = 0;
338  return 1;
339  }
340  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
341  *pnVars = sat_solver_nvars( pSat );
342  *pnConfs = sat_solver_nconflicts( pSat );
343  if ( status == l_True )
344  p->pCexComb = Cec_SplitDeriveModel( p, pCnf, pSat );
345  sat_solver_delete( pSat );
346  if ( status == l_Undef )
347  return -1;
348  if ( status == l_False )
349  return 1;
350  return 0;
351 }
352 static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
353 {
354  Gia_Man_t * pNew;
355  int i;
356  Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i )
357  Gia_ManStop( pNew );
358  Vec_PtrFree( vStack );
359 }
360 
361 /**Function*************************************************************
362 
363  Synopsis []
364 
365  Description []
366 
367  SideEffects []
368 
369  SeeAlso []
370 
371 ***********************************************************************/
372 void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk )
373 {
374  printf( "%4d : ", nIter );
375  printf( "Depth =%3d ", Depth );
376  printf( "SatVar =%7d ", nVars );
377  printf( "SatConf =%7d ", nConfs );
378  printf( "%s ", fStatus ? (fStatus == 1 ? "UNSAT " : "UNDECIDED") : "SAT " );
379  printf( "Solved %8.4f %% ", 100*Prog );
380  Abc_PrintTime( 1, "Time", clk );
381  //ABC_PRTr( "Time", Abc_Clock()-clk );
382  fflush( stdout );
383 }
384 void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
385 {
386  Gia_Obj_t * pObj;
387  int i;
388  if ( p->pRefs == NULL )
389  Gia_ManCreateRefs( p );
390  Gia_ManForEachPi( p, pObj, i )
391  printf( "%d ", Gia_ObjRefNum(p, pObj) );
392  printf( "\n" );
393 }
394 
395 /**Function*************************************************************
396 
397  Synopsis []
398 
399  Description []
400 
401  SideEffects []
402 
403  SeeAlso []
404 
405 ***********************************************************************/
406 int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose )
407 {
408  abctime clkTotal = Abc_Clock();
409  Vec_Ptr_t * vStack;
410  Cnf_Dat_t * pCnf;
411  int nSatVars, nSatConfs;
412  int nIter, status, RetValue = -1;
413  double Progress = 0;
414  // check the problem
415  pCnf = Cec_GiaDeriveGiaRemapped( p );
416  status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
417  Cnf_DataFree( pCnf );
418  if ( fVerbose )
419  Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
420  if ( status == 0 )
421  {
422  printf( "The problem is SAT without cofactoring.\n" );
423  return 0;
424  }
425  if ( status == 1 )
426  {
427  printf( "The problem is UNSAT without cofactoring.\n" );
428  return 1;
429  }
430  assert( status == -1 );
431  // create local copy
432  vStack = Vec_PtrAlloc( 1000 );
433  Vec_PtrPush( vStack, Gia_ManDup(p) );
434  // start with the current problem
435  for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
436  {
437  // get the last AIG
438  Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
439  // determine cofactoring variable
440  int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
441  int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
442  // cofactor
443  Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
444  if ( pLast->vCofVars == NULL )
445  pLast->vCofVars = Vec_IntAlloc( 100 );
446  // print results
447  if ( fVeryVerbose )
448  {
449 // Cec_GiaSplitPrintRefs( pLast );
450  printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
451  iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
452 // Cec_GiaSplitPrintRefs( pPart );
453  }
454  // create variable
455  pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
456  Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
457  Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
458  // solve the problem
459  pCnf = Cec_GiaDeriveGiaRemapped( pPart );
460  status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
461  Cnf_DataFree( pCnf );
462  if ( status == 1 )
463  Progress += 1.0 / pow(2, Depth);
464  if ( fVerbose )
465  Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
466  if ( status == 0 ) // SAT
467  {
468  p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL;
469  Gia_ManStop( pLast );
470  Gia_ManStop( pPart );
471  RetValue = 0;
472  break;
473  }
474  if ( status == 1 ) // UNSAT
475  Gia_ManStop( pPart );
476  else // UNDEC
477  Vec_PtrPush( vStack, pPart );
478  // cofactor
479  pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
480  // create variable
481  pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
482  Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
483  Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 0) );
484  Gia_ManStop( pLast );
485  // solve the problem
486  pCnf = Cec_GiaDeriveGiaRemapped( pPart );
487  status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
488  Cnf_DataFree( pCnf );
489  if ( status == 1 )
490  Progress += 1.0 / pow(2, Depth);
491  if ( fVerbose )
492  Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
493  if ( status == 0 ) // SAT
494  {
495  p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL;
496  Gia_ManStop( pPart );
497  RetValue = 0;
498  break;
499  }
500  if ( status == 1 ) // UNSAT
501  Gia_ManStop( pPart );
502  else // UNDEC
503  Vec_PtrPush( vStack, pPart );
504  if ( nIterMax && nIter >= nIterMax )
505  break;
506  }
507  if ( Vec_PtrSize(vStack) == 0 )
508  RetValue = 1;
509  // finish
510  Cec_GiaSplitClean( vStack );
511  if ( RetValue == 0 )
512  printf( "Problem is SAT " );
513  else if ( RetValue == 1 )
514  printf( "Problem is UNSAT " );
515  else if ( RetValue == -1 )
516  printf( "Problem is UNDECIDED " );
517  else assert( 0 );
518  printf( "after %d case-splits. ", nIter );
519  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
520  fflush( stdout );
521  return RetValue;
522 }
523 
524 /**Function*************************************************************
525 
526  Synopsis []
527 
528  Description []
529 
530  SideEffects []
531 
532  SeeAlso []
533 
534 ***********************************************************************/
535 #define PAR_THR_MAX 100
536 typedef struct Par_ThData_t_
537 {
538  Gia_Man_t * p;
539  Cnf_Dat_t * pCnf;
540  int iThread;
541  int nTimeOut;
542  int fWorking;
543  int Result;
544  int nVars;
545  int nConfs;
546 } Par_ThData_t;
547 void * Cec_GiaSplitWorkerThread( void * pArg )
548 {
549  Par_ThData_t * pThData = (Par_ThData_t *)pArg;
550  volatile int * pPlace = &pThData->fWorking;
551  while ( 1 )
552  {
553  while ( *pPlace == 0 );
554  assert( pThData->fWorking );
555  if ( pThData->p == NULL )
556  {
557  pthread_exit( NULL );
558  assert( 0 );
559  return NULL;
560  }
561  pThData->Result = Cnf_GiaSolveOne( pThData->p, pThData->pCnf, pThData->nTimeOut, &pThData->nVars, &pThData->nConfs );
562  pThData->fWorking = 0;
563  }
564  assert( 0 );
565  return NULL;
566 }
567 int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose )
568 {
569  abctime clkTotal = Abc_Clock();
570  Par_ThData_t ThData[PAR_THR_MAX];
571  pthread_t WorkerThread[PAR_THR_MAX];
572  Vec_Ptr_t * vStack;
573  Cnf_Dat_t * pCnf;
574  double Progress = 0;
575  int i, status, nSatVars, nSatConfs;
576  int nIter = 0, RetValue = -1, fWorkToDo = 1;
577  Abc_CexFreeP( &p->pCexComb );
578  if ( fVerbose )
579  printf( "Solving CEC problem by cofactoring with the following parameters:\n" );
580  if ( fVerbose )
581  printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
582  fflush( stdout );
583  if ( nProcs == 1 )
584  return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose );
585  // subtract manager thread
586  nProcs--;
587  assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
588  // check the problem
589  pCnf = Cec_GiaDeriveGiaRemapped( p );
590  status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
591  Cnf_DataFree( pCnf );
592  if ( fVerbose && status != -1 )
593  Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
594  if ( status == 0 )
595  {
596  printf( "The problem is SAT without cofactoring.\n" );
597  return 0;
598  }
599  if ( status == 1 )
600  {
601  printf( "The problem is UNSAT without cofactoring.\n" );
602  return 1;
603  }
604  assert( status == -1 );
605  // create local copy
606  vStack = Vec_PtrAlloc( 1000 );
607  Vec_PtrPush( vStack, Gia_ManDup(p) );
608  // start threads
609  for ( i = 0; i < nProcs; i++ )
610  {
611  ThData[i].p = NULL;
612  ThData[i].pCnf = NULL;
613  ThData[i].iThread = i;
614  ThData[i].nTimeOut = nTimeOut;
615  ThData[i].fWorking = 0;
616  ThData[i].Result = -1;
617  ThData[i].nVars = -1;
618  ThData[i].nConfs = -1;
619  status = pthread_create( WorkerThread + i, NULL,Cec_GiaSplitWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
620  }
621  // look at the threads
622  while ( fWorkToDo )
623  {
624  fWorkToDo = (int)(Vec_PtrSize(vStack) > 0);
625  for ( i = 0; i < nProcs; i++ )
626  {
627  // check if this thread is working
628  if ( ThData[i].fWorking )
629  {
630  fWorkToDo = 1;
631  continue;
632  }
633  // check if this thread has recently finished
634  if ( ThData[i].p != NULL )
635  {
636  Gia_Man_t * pLast = ThData[i].p;
637  int Depth = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0;
638  if ( pLast->vCofVars == NULL )
639  pLast->vCofVars = Vec_IntAlloc( 100 );
640  if ( fVerbose )
641  Cec_GiaSplitPrint( i+1, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
642  if ( ThData[i].Result == 0 ) // SAT
643  {
644  p->pCexComb = pLast->pCexComb; pLast->pCexComb = NULL;
645  RetValue = 0;
646  goto finish;
647  }
648  if ( ThData[i].Result == -1 ) // UNDEC
649  {
650  // determine cofactoring variable
651  int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
652  // cofactor
653  Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
654  pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
655  Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
656  Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
657  Vec_PtrPush( vStack, pPart );
658  // print results
659  if ( fVeryVerbose )
660  {
661 // Cec_GiaSplitPrintRefs( pLast );
662  printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
663  iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
664 // Cec_GiaSplitPrintRefs( pPart );
665  }
666  // cofactor
667  pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
668  pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
669  Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
670  Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
671  Vec_PtrPush( vStack, pPart );
672  // keep working
673  fWorkToDo = 1;
674  nIter++;
675  }
676  else
677  Progress += 1.0 / pow(2, Depth);
678  Gia_ManStopP( &ThData[i].p );
679  if ( ThData[i].pCnf == NULL )
680  continue;
681  Cnf_DataFree( ThData[i].pCnf );
682  ThData[i].pCnf = NULL;
683  }
684  if ( Vec_PtrSize(vStack) == 0 )
685  continue;
686  // start a new thread
687  assert( ThData[i].p == NULL );
688  ThData[i].p = Vec_PtrPop( vStack );
689  ThData[i].pCnf = Cec_GiaDeriveGiaRemapped( ThData[i].p );
690  ThData[i].fWorking = 1;
691  }
692  if ( nIterMax && nIter >= nIterMax )
693  break;
694  }
695  if ( !fWorkToDo )
696  RetValue = 1;
697 finish:
698  // wait till threads finish
699  for ( i = 0; i < nProcs; i++ )
700  if ( ThData[i].fWorking )
701  i = 0;
702  // stop threads
703  for ( i = 0; i < nProcs; i++ )
704  {
705  assert( !ThData[i].fWorking );
706  // cleanup
707  Gia_ManStopP( &ThData[i].p );
708  if ( ThData[i].pCnf == NULL )
709  continue;
710  Cnf_DataFree( ThData[i].pCnf );
711  ThData[i].pCnf = NULL;
712  // stop
713  ThData[i].p = NULL;
714  ThData[i].fWorking = 1;
715  }
716  // finish
717  Cec_GiaSplitClean( vStack );
718  if ( RetValue == 0 )
719  printf( "Problem is SAT " );
720  else if ( RetValue == 1 )
721  printf( "Problem is UNSAT " );
722  else if ( RetValue == -1 )
723  printf( "Problem is UNDECIDED " );
724  else assert( 0 );
725  printf( "after %d case-splits. ", nIter );
726  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
727  fflush( stdout );
728  return RetValue;
729 }
730 int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose )
731 {
732  Abc_Cex_t * pCex = NULL;
733  Gia_Man_t * pOne;
734  Gia_Obj_t * pObj;
735  int i, RetValue1, fOneUndef = 0, RetValue = -1;
736  Abc_CexFreeP( &p->pCexComb );
737  Gia_ManForEachPo( p, pObj, i )
738  {
739  pOne = Gia_ManDupOutputGroup( p, i, i+1 );
740  if ( fVerbose )
741  printf( "\nSolving output %d:\n", i );
742  RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose );
743  Gia_ManStop( pOne );
744  // collect the result
745  if ( RetValue1 == 0 && RetValue == -1 )
746  {
747  pCex = pOne->pCexComb; pOne->pCexComb = NULL;
748  pCex->iPo = i;
749  RetValue = 0;
750  }
751  if ( RetValue1 == -1 )
752  fOneUndef = 1;
753  }
754  if ( RetValue == -1 )
755  RetValue = fOneUndef ? -1 : 1;
756  else
757  p->pCexComb = pCex;
758  return RetValue;
759 }
760 
761 /**Function*************************************************************
762 
763  Synopsis [Print stats about cofactoring variables.]
764 
765  Description []
766 
767  SideEffects []
768 
769  SeeAlso []
770 
771 ***********************************************************************/
772 void Cec_GiaPrintCofStats( Gia_Man_t * p )
773 {
774  Gia_Man_t * pCof0, * pCof1;
775  Gia_Obj_t * pObj, * pFan0, * pFan1, * pCtrl;
776  Vec_Int_t * vMarks;
777  int i, Count = 0;
778  vMarks = Vec_IntStart( Gia_ManObjNum(p) );
779  Gia_ManForEachAnd( p, pObj, i )
780  {
781  if ( !Gia_ObjIsMuxType(pObj) )
782  continue;
783  if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
784  continue;
785  pCtrl = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
786  pCtrl = Gia_Regular(pCtrl);
787  Vec_IntAddToEntry( vMarks, Gia_ObjId(p, pCtrl), 1 );
788  }
789  printf( "The AIG with %d candidate nodes (PI+AND) has %d unique MUX control drivers:\n",
790  Gia_ManCandNum(p), Vec_IntCountPositive(vMarks) );
791  Gia_ManLevelNum( p );
792  Gia_ManForEachCand( p, pObj, i )
793  {
794  if ( !Vec_IntEntry(vMarks, i) )
795  continue;
796  pCof0 = Gia_ManDupCofactorObj( p, i, 0 );
797  pCof1 = Gia_ManDupCofactorObj( p, i, 1 );
798  printf( "%6d : ", Count++ );
799  printf( "Obj = %6d ", i );
800  printf( "MUX refs = %5d ", Vec_IntEntry(vMarks, i) );
801  printf( "Level = %5d ", Gia_ObjLevelId(p, i) );
802  printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) );
803  printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) );
804  printf( "\n" );
805  Gia_ManStop( pCof0 );
806  Gia_ManStop( pCof1 );
807  }
808  Vec_IntFree( vMarks );
809 }
810 void Cec_GiaPrintCofStats2( Gia_Man_t * p )
811 {
812  Gia_Man_t * pCof0, * pCof1;
813  Gia_Obj_t * pObj;
814  int i;
815  Gia_ManLevelNum( p );
816  Gia_ManCreateRefs( p );
817  Gia_ManForEachPi( p, pObj, i )
818  {
819  pCof0 = Gia_ManDupCofactorVar( p, i, 0 );
820  pCof1 = Gia_ManDupCofactorVar( p, i, 1 );
821  printf( "PI %5d : ", i );
822  printf( "Refs = %5d ", Gia_ObjRefNum(p, pObj) );
823  printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) );
824  printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) );
825  printf( "\n" );
826  Gia_ManStop( pCof0 );
827  Gia_ManStop( pCof1 );
828  }
829 }
830 
831 #endif // pthreads are used
832 
833 ////////////////////////////////////////////////////////////////////////
834 /// END OF FILE ///
835 ////////////////////////////////////////////////////////////////////////
836 
837 
838 ABC_NAMESPACE_IMPL_END
839 
Vec_IntCountPositive
static int Vec_IntCountPositive(Vec_Int_t *p)
Definition: vecInt.h:1175
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_ObjLevelId
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
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
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Gia_ObjRecognizeExor
int Gia_ObjRecognizeExor(Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Definition: giaUtil.c:921
Abc_QuickSortCost
int * Abc_QuickSortCost(int *pCosts, int nSize, int fDecrease)
Definition: utilSort.c:719
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Gia_ManDupPerm
Gia_Man_t * Gia_ManDupPerm(Gia_Man_t *p, Vec_Int_t *vPiPerm)
Definition: giaDup.c:632
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Gia_ManDupCofactorObj
Gia_Man_t * Gia_ManDupCofactorObj(Gia_Man_t *p, int iObj, int Value)
Definition: giaDup.c:1319
Vec_IntAllocArray
static Vec_Int_t * Vec_IntAllocArray(int *pArray, int nSize)
Definition: bblif.c:214
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_ManDupOutputGroup
Gia_Man_t * Gia_ManDupOutputGroup(Gia_Man_t *p, int iOutStart, int iOutStop)
Definition: giaDup.c:203
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
Gia_Man_t_::pMuxes
unsigned * pMuxes
Definition: gia.h:104
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Gia_Man_t_::pCexComb
Abc_Cex_t * pCexComb
Definition: gia.h:135
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
l_True
#define l_True
Definition: SolverTypes.h:84
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Vec_PtrPop
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
Gia_Man_t_::pRefs
int * pRefs
Definition: gia.h:114
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cec_GiaSplitTest
ABC_NAMESPACE_IMPL_START int Cec_GiaSplitTest(Gia_Man_t *p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose)
DECLARATIONS ///.
Definition: cecSplit.c:49
Cudd_PrintInfo
int Cudd_PrintInfo(DdManager *dd, FILE *fp)
Definition: cuddAPI.c:2937
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
if
if(last==0)
Definition: sparse_int.h:34
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntAppend
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
Definition: extraZddTrunc.c:126
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManCandNum
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Gia_ManForEachCand
#define Gia_ManForEachCand(p, pObj, i)
Definition: gia.h:1008
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cudd_CheckZeroRef
int Cudd_CheckZeroRef(DdManager *manager)
Definition: cuddRef.c:466
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Gia_ManDupCofactorVar
Gia_Man_t * Gia_ManDupCofactorVar(Gia_Man_t *p, int iVar, int Value)
Definition: giaDup.c:1281
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_Man_t_::vCofVars
Vec_Int_t * vCofVars
Definition: gia.h:162
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Gia_Man_t_
Definition: gia.h:95
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
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
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
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
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_CexCreate
Abc_Cex_t * Abc_CexCreate(int nRegs, int nPis, int *pArray, int iFrame, int iPo, int fSkipRegs)
Definition: utilCex.c:110
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
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
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
inline
#define inline
Definition: kitPerm.c:28
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
Depth
static int Depth
Definition: dsdProc.c:56