abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
int2Bmc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [int2Bmc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Interpolation engine.]
8 
9  Synopsis [BMC used inside IMC.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - Dec 1, 2013.]
16 
17  Revision [$Id: int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "int2Int.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 
35 /**Function*************************************************************
36 
37  Synopsis [Trasnforms AIG to transition into the init state.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose )
47 {
48  Gia_Man_t * pNew, * pTemp;
49  Gia_Obj_t * pObj, * pObjRi, * pObjRo;
50  int i, iCtrl;
51  assert( Gia_ManRegNum(p) > 0 );
52  pNew = Gia_ManStart( 10000 );
53  pNew->pName = Abc_UtilStrsav( p->pName );
54  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
55  Gia_ManConst0(p)->Value = 0;
56  Gia_ManForEachCi( p, pObj, i )
57  {
58  if ( i == Gia_ManPiNum(p) )
59  iCtrl = Gia_ManAppendCi( pNew );
60  pObj->Value = Gia_ManAppendCi( pNew );
61  }
62  Gia_ManHashAlloc( pNew );
63  Gia_ManForEachAnd( p, pObj, i )
64  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
65  Gia_ManForEachPo( p, pObj, i )
66  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
67  Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
68  Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
69  Gia_ManHashStop( pNew );
70  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
71  // remove dangling
72  pNew = Gia_ManCleanup( pTemp = pNew );
73  if ( fVerbose )
74  printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
75  Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
76  Gia_ManStop( pTemp );
77  return pNew;
78 }
79 
80 
81 /**Function*************************************************************
82 
83  Synopsis [Returns 1 if AIG has transition into init state.]
84 
85  Description []
86 
87  SideEffects []
88 
89  SeeAlso []
90 
91 ***********************************************************************/
93 {
94  sat_solver * pSat;
95  Cnf_Dat_t * pCnf;
96  Gia_Man_t * pNew;
97  Gia_Obj_t * pObj;
98  Vec_Int_t * vLits;
99  int i, Lit, RetValue = 0;
100  assert( Gia_ManRegNum(p) > 0 );
101  pNew = Jf_ManDeriveCnf( p, 0 );
102  pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
103  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
104  if ( pSat != NULL )
105  {
106  vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
107  Gia_ManForEachRi( pNew, pObj, i )
108  {
109  Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
110  Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
111  Vec_IntPush( vLits, Abc_LitNot(Lit) );
112  }
113  if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
114  RetValue = 1;
115  Vec_IntFree( vLits );
116  sat_solver_delete( pSat );
117  }
118  Cnf_DataFree( pCnf );
119  Gia_ManStop( pNew );
120  return RetValue;
121 }
122 
123 
124 /**Function*************************************************************
125 
126  Synopsis [Creates the BMC instance in the SAT solver.]
127 
128  Description [The PIs are mapped in the natural order. The flop inputs
129  are the last Gia_ManRegNum(p) variables of resulting SAT solver.]
130 
131  SideEffects []
132 
133  SeeAlso []
134 
135 ***********************************************************************/
136 Gia_Man_t * Int2_ManFrameInit( Gia_Man_t * p, int nFrames, int fVerbose )
137 {
138  Gia_Man_t * pFrames, * pTemp;
139  Gia_Obj_t * pObj;
140  int i, f;
141  pFrames = Gia_ManStart( 10000 );
142  pFrames->pName = Abc_UtilStrsav( p->pName );
143  pFrames->pSpec = Abc_UtilStrsav( p->pSpec );
144  Gia_ManConst0(p)->Value = 0;
145  // perform structural hashing
146  Gia_ManHashAlloc( pFrames );
147  for ( f = 0; f < nFrames; f++ )
148  {
149  Gia_ManForEachPi( p, pObj, i )
150  pObj->Value = Gia_ManAppendCi( pFrames );
151  Gia_ManForEachRo( p, pObj, i )
152  pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0;
153  Gia_ManForEachAnd( p, pObj, i )
154  pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
155  Gia_ManForEachRi( p, pObj, i )
156  pObj->Value = Gia_ObjFanin0Copy(pObj);
157  }
158  Gia_ManHashStop( pFrames );
159  // create flop inputs
160  Gia_ManForEachRi( p, pObj, i )
161  pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
162  // remove dangling
163  pFrames = Gia_ManCleanup( pTemp = pFrames );
164  if ( fVerbose )
165  printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
166  Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
167  Gia_ManStop( pTemp );
168  return pFrames;
169 }
171 {
172  Gia_Man_t * pFrames, * pTemp;
173  Cnf_Dat_t * pCnf;
174  sat_solver * pSat;
175  // unfold for the given number of timeframes
176  pFrames = Int2_ManFrameInit( p, nFrames, 1 );
177  assert( Gia_ManRegNum(pFrames) == 0 );
178  // derive CNF for the timeframes
179  pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp );
180  pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
181  // create SAT solver
182  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
183  if ( pSat != NULL )
184  {
185  Gia_Obj_t * pObj;
186  int i, nVars = sat_solver_nvars( pSat );
187  sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
188  // add clauses for the POs
189  Gia_ManForEachCo( pFrames, pObj, i )
190  sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
191  }
192  Cnf_DataFree( pCnf );
193  Gia_ManStop( pFrames );
194  return pSat;
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis []
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 static inline int Int2_ManCheckFrames( Int2_Man_t * p, int iFrame, int iObj )
209 {
210  Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
211  return Vec_IntEntry(vMapFrame, iObj);
212 }
213 static inline void Int2_ManWriteFrames( Int2_Man_t * p, int iFrame, int iObj, int iRes )
214 {
215  Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
216  assert( Vec_IntEntry(vMapFrame, iObj) == -1 );
217  Vec_IntWriteEntry( vMapFrame, iObj, iRes );
218 }
219 void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos )
220 {
221  Gia_Obj_t * pObj;
222  int i, Entry, iLit;
223  // create storage room for unfolded IDs
224  for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
225  Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
226  assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
227  // create constant 0 node
228  if ( f == 0 )
229  {
230  iLit = 1;
231  Int2_ManWriteFrames( p, iFrame, iObj, 0 );
232  sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
233  }
234  // start the stack
235  Vec_IntClear( p->vStack );
236  Vec_IntForEachEntry( vPrefCos, Entry, i )
237  {
238  pObj = Gia_ManCo( p->pGia, Entry );
239  Vec_IntPush( p->vStack, iFrame );
240  Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
241  }
242  // construct unfolded AIG
243  while ( Vec_IntSize(p->vStack) > 0 )
244  {
245  int iObj = Vec_IntPop(p->vStack);
246  int iFrame = Vec_IntPop(p->vStack);
247  if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
248  continue;
249  pObj = Gia_ManObj( p->pGia, iObj );
250  if ( Gia_ObjIsPi(p->pGia, pObj) )
251  Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
252  else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
253  Int2_ManWriteFrames( p, iFrame, iObj, 0 );
254  else if ( Gia_ObjIsRo(p->pGia, iObj) )
255  {
256  int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
257  int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
258  if ( iLit >= 0 )
259  Int2_ManWriteFrames( p, iFrame, iObj, iLit );
260  else
261  {
262  Vec_IntPush( p->vStack, iFrame );
263  Vec_IntPush( p->vStack, iObj );
264  Vec_IntPush( p->vStack, iFrame-1 );
265  Vec_IntPush( p->vStack, iObjF );
266  }
267  }
268  else if ( Gia_ObjIsCo(pObj) )
269  {
270  int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
271  int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
272  if ( iLit >= 0 )
273  Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
274  else
275  {
276  Vec_IntPush( p->vStack, iFrame );
277  Vec_IntPush( p->vStack, iObj );
278  Vec_IntPush( p->vStack, iFrame );
279  Vec_IntPush( p->vStack, iObjF );
280  }
281  }
282  else if ( Gia_ObjIsAnd(pObj) )
283  {
284  int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
285  int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
286  int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
287  int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
288  if ( iLit0 >= 0 && iLit1 >= 0 )
289  {
290  Entry = Gia_ManObjNum(pFrames);
291  iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
292  Int2_ManWriteFrames( p, iFrame, iObj, iLit );
293  if ( Entry < Gia_ManObjNum(pFrames) )
294  {
295  assert( !Abc_LitIsCompl(iLit) );
296  sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 );
297  }
298  }
299  else
300  {
301  Vec_IntPush( p->vStack, iFrame );
302  Vec_IntPush( p->vStack, iObj );
303  if ( iLit0 < 0 )
304  {
305  Vec_IntPush( p->vStack, iFrame );
306  Vec_IntPush( p->vStack, iObjF0 );
307  }
308  if ( iLit1 < 0 )
309  {
310  Vec_IntPush( p->vStack, iFrame );
311  Vec_IntPush( p->vStack, iObjF1 );
312  }
313  }
314  }
315  else assert( 0 );
316  }
317 }
319 {
320  int status;
321  if ( vCube == NULL )
322  {
323  Gia_Obj_t * pObj;
324  int i, iLit;
325  Gia_ManForEachPo( p->pGia, pObj, i )
326  {
327  iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
328  if ( iLit == 0 )
329  continue;
330  if ( iLit == 1 )
331  return 0;
332  status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
333  if ( status == l_False )
334  continue;
335  if ( status == l_True )
336  return 0;
337  return -1;
338  }
339  return 1;
340  }
341  status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
342  if ( status == l_False )
343  return 1;
344  if ( status == l_True )
345  return 0;
346  return -1;
347 }
348 
349 ////////////////////////////////////////////////////////////////////////
350 /// END OF FILE ///
351 ////////////////////////////////////////////////////////////////////////
352 
353 
355 
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static void Int2_ManWriteFrames(Int2_Man_t *p, int iFrame, int iObj, int iRes)
Definition: int2Bmc.c:213
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
void Int2_ManCreateFrames(Int2_Man_t *p, int iFrame, Vec_Int_t *vPrefCos)
Definition: int2Bmc.c:219
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
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
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
int * pVarNums
Definition: cnf.h:63
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define l_True
Definition: SolverTypes.h:84
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition: giaJf.c:1746
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: cnf.h:56
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_Man_t * Int2_ManFrameInit(Gia_Man_t *p, int nFrames, int fVerbose)
Definition: int2Bmc.c:136
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
int Int2_ManCheckInit(Gia_Man_t *p)
MACRO DEFINITIONS ///.
Definition: int2Bmc.c:92
typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_ Int2_Man_t
INCLUDES ///.
Definition: int2Int.h:45
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
int Int2_ManCheckBmc(Int2_Man_t *p, Vec_Int_t *vCube)
Definition: int2Bmc.c:318
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
void * pData
Definition: gia.h:169
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
char * pSpec
Definition: gia.h:98
static int Vec_IntPop(Vec_Int_t *p)
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Int2_ManCheckFrames(Int2_Man_t *p, int iFrame, int iObj)
Definition: int2Bmc.c:208
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
sat_solver * Int2_ManSetupBmcSolver(Gia_Man_t *p, int nFrames)
Definition: int2Bmc.c:170
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Definition: gia.h:95
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
ABC_NAMESPACE_IMPL_START Gia_Man_t * Int2_ManDupInit(Gia_Man_t *p, int fVerbose)
DECLARATIONS ///.
Definition: int2Bmc.c:46
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static int sat_solver_add_and(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl)
Definition: satSolver.h:324
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387