1 /**CFile****************************************************************
2
3 FileName [gia.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: gia.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__gia__gia_h
22 #define ABC__aig__gia__gia_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include <stdio.h>
30 #include <stdlib.h>
31 #include <string.h>
32 #include <assert.h>
33
34 #include "misc/vec/vec.h"
35 #include "misc/vec/vecWec.h"
36 #include "misc/util/utilCex.h"
37
38 ////////////////////////////////////////////////////////////////////////
39 /// PARAMETERS ///
40 ////////////////////////////////////////////////////////////////////////
41
42
43 ABC_NAMESPACE_HEADER_START
44
45 #define GIA_NONE 0x1FFFFFFF
46 #define GIA_VOID 0x0FFFFFFF
47
48 ////////////////////////////////////////////////////////////////////////
49 /// BASIC TYPES ///
50 ////////////////////////////////////////////////////////////////////////
51
52 typedef struct Gia_MmFixed_t_ Gia_MmFixed_t;
53 typedef struct Gia_MmFlex_t_ Gia_MmFlex_t;
54 typedef struct Gia_MmStep_t_ Gia_MmStep_t;
55 typedef struct Gia_Dat_t_ Gia_Dat_t;
56
57 typedef struct Gia_Rpr_t_ Gia_Rpr_t;
58 struct Gia_Rpr_t_
59 {
60 unsigned iRepr : 28; // representative node
61 unsigned fProved : 1; // marks the proved equivalence
62 unsigned fFailed : 1; // marks the failed equivalence
63 unsigned fColorA : 1; // marks cone of A
64 unsigned fColorB : 1; // marks cone of B
65 };
66
67 typedef struct Gia_Plc_t_ Gia_Plc_t;
68 struct Gia_Plc_t_
69 {
70 unsigned fFixed : 1; // the placement of this object is fixed
71 unsigned xCoord : 15; // x-ooordinate of the placement
72 unsigned fUndef : 1; // the placement of this object is not assigned
73 unsigned yCoord : 15; // y-ooordinate of the placement
74 };
75
76 typedef struct Gia_Obj_t_ Gia_Obj_t;
77 struct Gia_Obj_t_
78 {
79 unsigned iDiff0 : 29; // the diff of the first fanin
80 unsigned fCompl0: 1; // the complemented attribute
81 unsigned fMark0 : 1; // first user-controlled mark
82 unsigned fTerm : 1; // terminal node (CI/CO)
83
84 unsigned iDiff1 : 29; // the diff of the second fanin
85 unsigned fCompl1: 1; // the complemented attribute
86 unsigned fMark1 : 1; // second user-controlled mark
87 unsigned fPhase : 1; // value under 000 pattern
88
89 unsigned Value; // application-specific value
90 };
91 // Value is currently used to store several types of information
92 // - pointer to the next node in the hash table during structural hashing
93 // - pointer to the node copy during duplication
94
95 // new AIG manager
96 typedef struct Gia_Man_t_ Gia_Man_t;
97 struct Gia_Man_t_
98 {
99 char * pName; // name of the AIG
100 char * pSpec; // name of the input file
101 int nRegs; // number of registers
102 int nRegsAlloc; // number of allocated registers
103 int nObjs; // number of objects
104 int nObjsAlloc; // number of allocated objects
105 Gia_Obj_t * pObjs; // the array of objects
106 unsigned * pMuxes; // control signals of MUXes
107 int nXors; // the number of XORs
108 int nMuxes; // the number of MUXes
109 int nBufs; // the number of buffers
110 Vec_Int_t * vCis; // the vector of CIs (PIs + LOs)
111 Vec_Int_t * vCos; // the vector of COs (POs + LIs)
112 Vec_Int_t vHash; // hash links
113 Vec_Int_t vHTable; // hash table
114 int fAddStrash; // performs additional structural hashing
115 int fSweeper; // sweeper is running
116 int fGiaSimple; // simple mode (no const-propagation and strashing)
117 Vec_Int_t vRefs; // the reference count
118 int * pRefs; // the reference count
119 int * pLutRefs; // the reference count
120 Vec_Int_t * vLevels; // levels of the nodes
121 int nLevels; // the mamixum level
122 int nConstrs; // the number of constraints
123 int nTravIds; // the current traversal ID
124 int nFront; // frontier size
125 int * pReprsOld; // representatives (for CIs and ANDs)
126 Gia_Rpr_t * pReprs; // representatives (for CIs and ANDs)
127 int * pNexts; // next nodes in the equivalence classes
128 int * pSibls; // next nodes in the choice nodes
129 int * pIso; // pairs of structurally isomorphic nodes
130 int nTerLoop; // the state where loop begins
131 int nTerStates; // the total number of ternary states
132 int * pFanData; // the database to store fanout information
133 int nFansAlloc; // the size of fanout representation
134 Vec_Int_t * vFanoutNums; // static fanout
135 Vec_Int_t * vFanout; // static fanout
136 Vec_Int_t * vMapping; // mapping for each node
137 Vec_Wec_t * vMapping2; // mapping for each node
138 Vec_Wec_t * vFanouts2; // mapping fanouts
139 Vec_Int_t * vCellMapping; // mapping for each node
140 void * pSatlutWinman; // windowing for SAT-based mapping
141 Vec_Int_t * vPacking; // packing information
142 Vec_Int_t * vConfigs; // cell configurations
143 char * pCellStr; // cell description
144 Vec_Int_t * vLutConfigs; // LUT configurations
145 Vec_Int_t * vEdgeDelay; // special edge information
146 Vec_Int_t * vEdgeDelayR; // special edge information
147 Vec_Int_t * vEdge1; // special edge information
148 Vec_Int_t * vEdge2; // special edge information
149 Abc_Cex_t * pCexComb; // combinational counter-example
150 Abc_Cex_t * pCexSeq; // sequential counter-example
151 Vec_Ptr_t * vSeqModelVec; // sequential counter-examples
152 Vec_Int_t vCopies; // intermediate copies
153 Vec_Int_t vCopies2; // intermediate copies
154 Vec_Int_t * vVar2Obj; // mapping of variables into objects
155 Vec_Int_t * vTruths; // used for truth table computation
156 Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
157 Vec_Int_t * vGateClasses; // classes of gates for abstraction
158 Vec_Int_t * vObjClasses; // classes of objects for abstraction
159 Vec_Int_t * vInitClasses; // classes of flops for retiming/merging/etc
160 Vec_Int_t * vRegClasses; // classes of registers for sequential synthesis
161 Vec_Int_t * vRegInits; // initial state
162 Vec_Int_t * vDoms; // dominators
163 Vec_Int_t * vBarBufs; // barrier buffers
164 Vec_Int_t * vXors; // temporary XORs
165 unsigned char* pSwitching; // switching activity for each object
166 Gia_Plc_t * pPlacement; // placement of the objects
167 Gia_Man_t * pAigExtra; // combinational logic of holes
168 Vec_Flt_t * vInArrs; // PI arrival times
169 Vec_Flt_t * vOutReqs; // PO required times
170 Vec_Int_t * vCiArrs; // CI arrival times
171 Vec_Int_t * vCoReqs; // CO required times
172 Vec_Int_t * vCoArrs; // CO arrival times
173 Vec_Int_t * vCoAttrs; // CO attributes
174 int And2Delay; // delay of the AND gate
175 float DefInArrs; // default PI arrival times
176 float DefOutReqs; // default PO required times
177 Vec_Int_t * vSwitching; // switching activity
178 int * pTravIds; // separate traversal ID representation
179 int nTravIdsAlloc; // the number of trav IDs allocated
180 Vec_Ptr_t * vNamesIn; // the input names
181 Vec_Ptr_t * vNamesOut; // the output names
182 Vec_Int_t * vUserPiIds; // numbers assigned to PIs by the user
183 Vec_Int_t * vUserPoIds; // numbers assigned to POs by the user
184 Vec_Int_t * vUserFfIds; // numbers assigned to FFs by the user
185 Vec_Int_t * vCiNumsOrig; // original CI names
186 Vec_Int_t * vCoNumsOrig; // original CO names
187 Vec_Int_t * vIdsOrig; // original object IDs
188 Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
189 Vec_Int_t * vCofVars; // cofactoring variables
190 Vec_Vec_t * vClockDoms; // clock domains
191 Vec_Flt_t * vTiming; // arrival/required/slack
192 void * pManTime; // the timing manager
193 void * pLutLib; // LUT library
194 word nHashHit; // hash table hit
195 word nHashMiss; // hash table miss
196 void * pData; // various user data
197 unsigned * pData2; // various user data
198 int iData; // various user data
199 int iData2; // various user data
200 int nAnd2Delay; // AND2 delay scaled to match delay numbers used
201 int fVerbose; // verbose reports
202 int MappedArea; // area after mapping
203 int MappedDelay; // delay after mapping
204 // bit-parallel simulation
205 int fBuiltInSim;
206 int iPatsPi;
207 int nSimWords;
208 int iPastPiMax;
209 int nSimWordsMax;
210 Vec_Wrd_t * vSims;
211 Vec_Wrd_t * vSimsPi;
212 Vec_Wrd_t * vSimsPo;
213 Vec_Int_t * vClassOld;
214 Vec_Int_t * vClassNew;
215 // incremental simulation
216 int fIncrSim;
217 int iNextPi;
218 int iTimeStamp;
219 Vec_Int_t * vTimeStamps;
220 // truth table computation for small functions
221 int nTtVars; // truth table variables
222 int nTtWords; // truth table words
223 Vec_Int_t * vTtNums; // object numbers
224 Vec_Int_t * vTtNodes; // internal nodes
225 Vec_Ptr_t * vTtInputs; // truth tables for constant and primary inputs
226 Vec_Wrd_t * vTtMemory; // truth tables for internal nodes
227 // balancing
228 Vec_Int_t * vSuper; // supergate
229 Vec_Int_t * vStore; // node storage
230 // existential quantification
231 int iSuppPi; // the number of support variables
232 int nSuppWords; // the number of support words
233 Vec_Wrd_t * vSuppWords; // support information
234 Vec_Int_t vCopiesTwo; // intermediate copies
235 Vec_Int_t vSuppVars; // used variables
236 Gia_Dat_t * pUData;
237 };
238
239
240 typedef struct Gps_Par_t_ Gps_Par_t;
241 struct Gps_Par_t_
242 {
243 int fTents;
244 int fSwitch;
245 int fCut;
246 int fNpn;
247 int fLutProf;
248 int fMuxXor;
249 int fMiter;
250 int fSkipMap;
251 int fSlacks;
252 int fNoColor;
253 char * pDumpFile;
254 };
255
256 typedef struct Emb_Par_t_ Emb_Par_t;
257 struct Emb_Par_t_
258 {
259 int nDims; // the number of dimension
260 int nSols; // the number of solutions (typically, 2)
261 int nIters; // the number of iterations of FORCE
262 int fRefine; // use refinement by FORCE
263 int fCluster; // use clustered representation
264 int fDump; // dump Gnuplot file
265 int fDumpLarge; // dump Gnuplot file for large benchmarks
266 int fShowImage; // shows image if Gnuplot is installed
267 int fVerbose; // verbose flag
268 };
269
270
271 // frames parameters
272 typedef struct Gia_ParFra_t_ Gia_ParFra_t;
273 struct Gia_ParFra_t_
274 {
275 int nFrames; // the number of frames to unroll
276 int fInit; // initialize the timeframes
277 int fSaveLastLit; // adds POs for outputs of each frame
278 int fDisableSt; // disables strashing
279 int fOrPos; // ORs respective POs in each timeframe
280 int fVerbose; // enables verbose output
281 };
282
283
284 // simulation parameters
285 typedef struct Gia_ParSim_t_ Gia_ParSim_t;
286 struct Gia_ParSim_t_
287 {
288 // user-controlled parameters
289 int nWords; // the number of machine words
290 int nIters; // the number of timeframes
291 int RandSeed; // seed to generate random numbers
292 int TimeLimit; // time limit in seconds
293 int fCheckMiter; // check if miter outputs are non-zero
294 int fVerbose; // enables verbose output
295 int iOutFail; // index of the failed output
296 };
297
298 typedef struct Gia_ManSim_t_ Gia_ManSim_t;
299 struct Gia_ManSim_t_
300 {
301 Gia_Man_t * pAig;
302 Gia_ParSim_t * pPars;
303 int nWords;
304 Vec_Int_t * vCis2Ids;
305 Vec_Int_t * vConsts;
306 // simulation information
307 unsigned * pDataSim; // simulation data
308 unsigned * pDataSimCis; // simulation data for CIs
309 unsigned * pDataSimCos; // simulation data for COs
310 };
311
312 typedef struct Jf_Par_t_ Jf_Par_t;
313 struct Jf_Par_t_
314 {
315 int nLutSize;
316 int nCutNum;
317 int nProcNum;
318 int nRounds;
319 int nRoundsEla;
320 int nRelaxRatio;
321 int nCoarseLimit;
322 int nAreaTuner;
323 int nReqTimeFlex;
324 int nVerbLimit;
325 int nDelayLut1;
326 int nDelayLut2;
327 int nFastEdges;
328 int DelayTarget;
329 int fAreaOnly;
330 int fPinPerm;
331 int fPinQuick;
332 int fPinFilter;
333 int fOptEdge;
334 int fUseMux7;
335 int fPower;
336 int fCoarsen;
337 int fCutMin;
338 int fFuncDsd;
339 int fGenCnf;
340 int fCnfObjIds;
341 int fAddOrCla;
342 int fCnfMapping;
343 int fPureAig;
344 int fDoAverage;
345 int fCutHashing;
346 int fCutSimple;
347 int fCutGroup;
348 int fVerbose;
349 int fVeryVerbose;
350 int nLutSizeMax;
351 int nCutNumMax;
352 int nProcNumMax;
353 int nLutSizeMux;
354 word Delay;
355 word Area;
356 word Edge;
357 word Clause;
358 word Mux7;
359 word WordMapDelay;
360 word WordMapArea;
361 word WordMapDelayTarget;
362 int MapDelay;
363 float MapArea;
364 float MapAreaF;
365 float MapDelayTarget;
366 float Epsilon;
367 float * pTimesArr;
368 float * pTimesReq;
369 };
370
Gia_ObjCutSign(unsigned ObjId)371 static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
Gia_WordHasOneBit(unsigned uWord)372 static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; }
Gia_WordHasOnePair(unsigned uWord)373 static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); }
Gia_WordCountOnes(unsigned uWord)374 static inline int Gia_WordCountOnes( unsigned uWord )
375 {
376 uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
377 uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
378 uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
379 uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
380 return (uWord & 0x0000FFFF) + (uWord>>16);
381 }
Gia_WordFindFirstBit(unsigned uWord)382 static inline int Gia_WordFindFirstBit( unsigned uWord )
383 {
384 int i;
385 for ( i = 0; i < 32; i++ )
386 if ( uWord & (1 << i) )
387 return i;
388 return -1;
389 }
390
Gia_ManTruthIsConst0(unsigned * pIn,int nVars)391 static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars )
392 {
393 int w;
394 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
395 if ( pIn[w] )
396 return 0;
397 return 1;
398 }
Gia_ManTruthIsConst1(unsigned * pIn,int nVars)399 static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars )
400 {
401 int w;
402 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
403 if ( pIn[w] != ~(unsigned)0 )
404 return 0;
405 return 1;
406 }
Gia_ManTruthCopy(unsigned * pOut,unsigned * pIn,int nVars)407 static inline void Gia_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
408 {
409 int w;
410 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
411 pOut[w] = pIn[w];
412 }
Gia_ManTruthClear(unsigned * pOut,int nVars)413 static inline void Gia_ManTruthClear( unsigned * pOut, int nVars )
414 {
415 int w;
416 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
417 pOut[w] = 0;
418 }
Gia_ManTruthFill(unsigned * pOut,int nVars)419 static inline void Gia_ManTruthFill( unsigned * pOut, int nVars )
420 {
421 int w;
422 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
423 pOut[w] = ~(unsigned)0;
424 }
Gia_ManTruthNot(unsigned * pOut,unsigned * pIn,int nVars)425 static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars )
426 {
427 int w;
428 for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
429 pOut[w] = ~pIn[w];
430 }
431
Gia_ManConst0Lit()432 static inline int Gia_ManConst0Lit() { return 0; }
Gia_ManConst1Lit()433 static inline int Gia_ManConst1Lit() { return 1; }
Gia_ManIsConst0Lit(int iLit)434 static inline int Gia_ManIsConst0Lit( int iLit ) { return (iLit == 0); }
Gia_ManIsConst1Lit(int iLit)435 static inline int Gia_ManIsConst1Lit( int iLit ) { return (iLit == 1); }
Gia_ManIsConstLit(int iLit)436 static inline int Gia_ManIsConstLit( int iLit ) { return (iLit <= 1); }
437
Gia_Regular(Gia_Obj_t * p)438 static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
Gia_Not(Gia_Obj_t * p)439 static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
Gia_NotCond(Gia_Obj_t * p,int c)440 static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
Gia_IsComplement(Gia_Obj_t * p)441 static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
442
Gia_ManName(Gia_Man_t * p)443 static inline char * Gia_ManName( Gia_Man_t * p ) { return p->pName; }
Gia_ManCiNum(Gia_Man_t * p)444 static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); }
Gia_ManCoNum(Gia_Man_t * p)445 static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); }
Gia_ManPiNum(Gia_Man_t * p)446 static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; }
Gia_ManPoNum(Gia_Man_t * p)447 static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos) - p->nRegs; }
Gia_ManRegNum(Gia_Man_t * p)448 static inline int Gia_ManRegNum( Gia_Man_t * p ) { return p->nRegs; }
Gia_ManObjNum(Gia_Man_t * p)449 static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; }
Gia_ManAndNum(Gia_Man_t * p)450 static inline int Gia_ManAndNum( Gia_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1; }
Gia_ManXorNum(Gia_Man_t * p)451 static inline int Gia_ManXorNum( Gia_Man_t * p ) { return p->nXors; }
Gia_ManMuxNum(Gia_Man_t * p)452 static inline int Gia_ManMuxNum( Gia_Man_t * p ) { return p->nMuxes; }
Gia_ManBufNum(Gia_Man_t * p)453 static inline int Gia_ManBufNum( Gia_Man_t * p ) { return p->nBufs; }
Gia_ManAndNotBufNum(Gia_Man_t * p)454 static inline int Gia_ManAndNotBufNum( Gia_Man_t * p ){ return Gia_ManAndNum(p) - Gia_ManBufNum(p); }
Gia_ManCandNum(Gia_Man_t * p)455 static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); }
Gia_ManConstrNum(Gia_Man_t * p)456 static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; }
Gia_ManFlipVerbose(Gia_Man_t * p)457 static inline void Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1; }
Gia_ManHasChoices(Gia_Man_t * p)458 static inline int Gia_ManHasChoices( Gia_Man_t * p ) { return p->pSibls != NULL; }
Gia_ManChoiceNum(Gia_Man_t * p)459 static inline int Gia_ManChoiceNum( Gia_Man_t * p ) { int c = 0; if (p->pSibls) { int i; for (i = 0; i < p->nObjs; i++) c += (int)(p->pSibls[i] > 0); } return c; }
460
Gia_ManConst0(Gia_Man_t * p)461 static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; }
Gia_ManConst1(Gia_Man_t * p)462 static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); }
Gia_ManObj(Gia_Man_t * p,int v)463 static inline Gia_Obj_t * Gia_ManObj( Gia_Man_t * p, int v ) { assert( v >= 0 && v < p->nObjs ); return p->pObjs + v; }
Gia_ManCi(Gia_Man_t * p,int v)464 static inline Gia_Obj_t * Gia_ManCi( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) ); }
Gia_ManCo(Gia_Man_t * p,int v)465 static inline Gia_Obj_t * Gia_ManCo( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) ); }
Gia_ManPi(Gia_Man_t * p,int v)466 static inline Gia_Obj_t * Gia_ManPi( Gia_Man_t * p, int v ) { assert( v < Gia_ManPiNum(p) ); return Gia_ManCi( p, v ); }
Gia_ManPo(Gia_Man_t * p,int v)467 static inline Gia_Obj_t * Gia_ManPo( Gia_Man_t * p, int v ) { assert( v < Gia_ManPoNum(p) ); return Gia_ManCo( p, v ); }
Gia_ManRo(Gia_Man_t * p,int v)468 static inline Gia_Obj_t * Gia_ManRo( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); }
Gia_ManRi(Gia_Man_t * p,int v)469 static inline Gia_Obj_t * Gia_ManRi( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); }
470
Gia_ObjId(Gia_Man_t * p,Gia_Obj_t * pObj)471 static inline int Gia_ObjId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pObjs <= pObj && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
Gia_ObjCioId(Gia_Obj_t * pObj)472 static inline int Gia_ObjCioId( Gia_Obj_t * pObj ) { assert( pObj->fTerm ); return pObj->iDiff1; }
Gia_ObjSetCioId(Gia_Obj_t * pObj,int v)473 static inline void Gia_ObjSetCioId( Gia_Obj_t * pObj, int v ) { assert( pObj->fTerm ); pObj->iDiff1 = v; }
Gia_ObjValue(Gia_Obj_t * pObj)474 static inline int Gia_ObjValue( Gia_Obj_t * pObj ) { return pObj->Value; }
Gia_ObjSetValue(Gia_Obj_t * pObj,int i)475 static inline void Gia_ObjSetValue( Gia_Obj_t * pObj, int i ) { pObj->Value = i; }
Gia_ObjPhase(Gia_Obj_t * pObj)476 static inline int Gia_ObjPhase( Gia_Obj_t * pObj ) { return pObj->fPhase; }
Gia_ObjPhaseReal(Gia_Obj_t * pObj)477 static inline int Gia_ObjPhaseReal( Gia_Obj_t * pObj ) { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj); }
478
Gia_ObjIsTerm(Gia_Obj_t * pObj)479 static inline int Gia_ObjIsTerm( Gia_Obj_t * pObj ) { return pObj->fTerm; }
Gia_ObjIsAndOrConst0(Gia_Obj_t * pObj)480 static inline int Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj ) { return!pObj->fTerm; }
Gia_ObjIsCi(Gia_Obj_t * pObj)481 static inline int Gia_ObjIsCi( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 == GIA_NONE; }
Gia_ObjIsCo(Gia_Obj_t * pObj)482 static inline int Gia_ObjIsCo( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 != GIA_NONE; }
Gia_ObjIsAnd(Gia_Obj_t * pObj)483 static inline int Gia_ObjIsAnd( Gia_Obj_t * pObj ) { return!pObj->fTerm && pObj->iDiff0 != GIA_NONE; }
Gia_ObjIsXor(Gia_Obj_t * pObj)484 static inline int Gia_ObjIsXor( Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 < pObj->iDiff1; }
Gia_ObjIsMuxId(Gia_Man_t * p,int iObj)485 static inline int Gia_ObjIsMuxId( Gia_Man_t * p, int iObj ) { return p->pMuxes && p->pMuxes[iObj] > 0; }
Gia_ObjIsMux(Gia_Man_t * p,Gia_Obj_t * pObj)486 static inline int Gia_ObjIsMux( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsMuxId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjIsAndReal(Gia_Man_t * p,Gia_Obj_t * pObj)487 static inline int Gia_ObjIsAndReal( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 > pObj->iDiff1 && !Gia_ObjIsMux(p, pObj); }
Gia_ObjIsBuf(Gia_Obj_t * pObj)488 static inline int Gia_ObjIsBuf( Gia_Obj_t * pObj ) { return pObj->iDiff0 == pObj->iDiff1 && pObj->iDiff0 != GIA_NONE && !pObj->fTerm; }
Gia_ObjIsAndNotBuf(Gia_Obj_t * pObj)489 static inline int Gia_ObjIsAndNotBuf( Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 != pObj->iDiff1; }
Gia_ObjIsCand(Gia_Obj_t * pObj)490 static inline int Gia_ObjIsCand( Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); }
Gia_ObjIsConst0(Gia_Obj_t * pObj)491 static inline int Gia_ObjIsConst0( Gia_Obj_t * pObj ) { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE; }
Gia_ManObjIsConst0(Gia_Man_t * p,Gia_Obj_t * pObj)492 static inline int Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs; }
493
Gia_Obj2Lit(Gia_Man_t * p,Gia_Obj_t * pObj)494 static inline int Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); }
Gia_Lit2Obj(Gia_Man_t * p,int iLit)495 static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); }
Gia_ManCiLit(Gia_Man_t * p,int CiId)496 static inline int Gia_ManCiLit( Gia_Man_t * p, int CiId ) { return Gia_Obj2Lit( p, Gia_ManCi(p, CiId) ); }
497
Gia_ManIdToCioId(Gia_Man_t * p,int Id)498 static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); }
Gia_ManCiIdToId(Gia_Man_t * p,int CiId)499 static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); }
Gia_ManCoIdToId(Gia_Man_t * p,int CoId)500 static inline int Gia_ManCoIdToId( Gia_Man_t * p, int CoId ) { return Gia_ObjId( p, Gia_ManCo(p, CoId) ); }
501
Gia_ObjIsPi(Gia_Man_t * p,Gia_Obj_t * pObj)502 static inline int Gia_ObjIsPi( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManPiNum(p); }
Gia_ObjIsPo(Gia_Man_t * p,Gia_Obj_t * pObj)503 static inline int Gia_ObjIsPo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) < Gia_ManPoNum(p); }
Gia_ObjIsRo(Gia_Man_t * p,Gia_Obj_t * pObj)504 static inline int Gia_ObjIsRo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPiNum(p); }
Gia_ObjIsRi(Gia_Man_t * p,Gia_Obj_t * pObj)505 static inline int Gia_ObjIsRi( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPoNum(p); }
506
Gia_ObjRoToRi(Gia_Man_t * p,Gia_Obj_t * pObj)507 static inline Gia_Obj_t * Gia_ObjRoToRi( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsRo(p, pObj) ); return Gia_ManCo(p, Gia_ManCoNum(p) - Gia_ManCiNum(p) + Gia_ObjCioId(pObj)); }
Gia_ObjRiToRo(Gia_Man_t * p,Gia_Obj_t * pObj)508 static inline Gia_Obj_t * Gia_ObjRiToRo( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsRi(p, pObj) ); return Gia_ManCi(p, Gia_ManCiNum(p) - Gia_ManCoNum(p) + Gia_ObjCioId(pObj)); }
Gia_ObjRoToRiId(Gia_Man_t * p,int ObjId)509 static inline int Gia_ObjRoToRiId( Gia_Man_t * p, int ObjId ) { return Gia_ObjId( p, Gia_ObjRoToRi( p, Gia_ManObj(p, ObjId) ) ); }
Gia_ObjRiToRoId(Gia_Man_t * p,int ObjId)510 static inline int Gia_ObjRiToRoId( Gia_Man_t * p, int ObjId ) { return Gia_ObjId( p, Gia_ObjRiToRo( p, Gia_ManObj(p, ObjId) ) ); }
511
Gia_ObjDiff0(Gia_Obj_t * pObj)512 static inline int Gia_ObjDiff0( Gia_Obj_t * pObj ) { return pObj->iDiff0; }
Gia_ObjDiff1(Gia_Obj_t * pObj)513 static inline int Gia_ObjDiff1( Gia_Obj_t * pObj ) { return pObj->iDiff1; }
Gia_ObjFaninC0(Gia_Obj_t * pObj)514 static inline int Gia_ObjFaninC0( Gia_Obj_t * pObj ) { return pObj->fCompl0; }
Gia_ObjFaninC1(Gia_Obj_t * pObj)515 static inline int Gia_ObjFaninC1( Gia_Obj_t * pObj ) { return pObj->fCompl1; }
Gia_ObjFaninC2(Gia_Man_t * p,Gia_Obj_t * pObj)516 static inline int Gia_ObjFaninC2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes && Abc_LitIsCompl(p->pMuxes[Gia_ObjId(p, pObj)]); }
Gia_ObjFanin0(Gia_Obj_t * pObj)517 static inline Gia_Obj_t * Gia_ObjFanin0( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff0; }
Gia_ObjFanin1(Gia_Obj_t * pObj)518 static inline Gia_Obj_t * Gia_ObjFanin1( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff1; }
Gia_ObjFanin2(Gia_Man_t * p,Gia_Obj_t * pObj)519 static inline Gia_Obj_t * Gia_ObjFanin2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes ? Gia_ManObj(p, Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)])) : NULL; }
Gia_ObjChild0(Gia_Obj_t * pObj)520 static inline Gia_Obj_t * Gia_ObjChild0( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); }
Gia_ObjChild1(Gia_Obj_t * pObj)521 static inline Gia_Obj_t * Gia_ObjChild1( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); }
Gia_ObjChild2(Gia_Man_t * p,Gia_Obj_t * pObj)522 static inline Gia_Obj_t * Gia_ObjChild2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin2(p, pObj), Gia_ObjFaninC2(p, pObj) ); }
Gia_ObjFaninId0(Gia_Obj_t * pObj,int ObjId)523 static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff0; }
Gia_ObjFaninId1(Gia_Obj_t * pObj,int ObjId)524 static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; }
Gia_ObjFaninId2(Gia_Man_t * p,int ObjId)525 static inline int Gia_ObjFaninId2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? Abc_Lit2Var(p->pMuxes[ObjId]) : -1; }
Gia_ObjFaninId0p(Gia_Man_t * p,Gia_Obj_t * pObj)526 static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); }
Gia_ObjFaninId1p(Gia_Man_t * p,Gia_Obj_t * pObj)527 static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); }
Gia_ObjFaninId2p(Gia_Man_t * p,Gia_Obj_t * pObj)528 static inline int Gia_ObjFaninId2p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)]) : -1; }
Gia_ObjFaninLit0(Gia_Obj_t * pObj,int ObjId)529 static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
Gia_ObjFaninLit1(Gia_Obj_t * pObj,int ObjId)530 static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
Gia_ObjFaninLit2(Gia_Man_t * p,int ObjId)531 static inline int Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1; }
Gia_ObjFaninLit0p(Gia_Man_t * p,Gia_Obj_t * pObj)532 static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); }
Gia_ObjFaninLit1p(Gia_Man_t * p,Gia_Obj_t * pObj)533 static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); }
Gia_ObjFaninLit2p(Gia_Man_t * p,Gia_Obj_t * pObj)534 static inline int Gia_ObjFaninLit2p( Gia_Man_t * p, Gia_Obj_t * pObj) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? p->pMuxes[Gia_ObjId(p, pObj)] : -1; }
Gia_ObjFlipFaninC0(Gia_Obj_t * pObj)535 static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; }
Gia_ObjFaninNum(Gia_Man_t * p,Gia_Obj_t * pObj)536 static inline int Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; }
Gia_ObjWhatFanin(Gia_Man_t * p,Gia_Obj_t * pObj,Gia_Obj_t * pFanin)537 static inline int Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; }
538
Gia_ManPoIsConst(Gia_Man_t * p,int iPoIndex)539 static inline int Gia_ManPoIsConst( Gia_Man_t * p, int iPoIndex ) { return Gia_ObjFaninId0p(p, Gia_ManPo(p, iPoIndex)) == 0; }
Gia_ManPoIsConst0(Gia_Man_t * p,int iPoIndex)540 static inline int Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
Gia_ManPoIsConst1(Gia_Man_t * p,int iPoIndex)541 static inline int Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
542
Gia_ObjCopy(Gia_Man_t * p,Gia_Obj_t * pObj)543 static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) ); }
Gia_ObjLitCopy(Gia_Man_t * p,int iLit)544 static inline int Gia_ObjLitCopy( Gia_Man_t * p, int iLit ) { return Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit))->Value, Abc_LitIsCompl(iLit)); }
545
Gia_ObjFanin0Copy(Gia_Obj_t * pObj)546 static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); }
Gia_ObjFanin1Copy(Gia_Obj_t * pObj)547 static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); }
Gia_ObjFanin2Copy(Gia_Man_t * p,Gia_Obj_t * pObj)548 static inline int Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); }
549
Gia_ObjCopyF(Gia_Man_t * p,int f,Gia_Obj_t * pObj)550 static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Vec_IntEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)); }
Gia_ObjSetCopyF(Gia_Man_t * p,int f,Gia_Obj_t * pObj,int iLit)551 static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit); }
Gia_ObjCopyArray(Gia_Man_t * p,int iObj)552 static inline int Gia_ObjCopyArray( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); }
Gia_ObjSetCopyArray(Gia_Man_t * p,int iObj,int iLit)553 static inline void Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); }
Gia_ManCleanCopyArray(Gia_Man_t * p)554 static inline void Gia_ManCleanCopyArray( Gia_Man_t * p ) { Vec_IntFill( &p->vCopies, Gia_ManObjNum(p), -1 ); }
555
Gia_ObjCopy2Array(Gia_Man_t * p,int iObj)556 static inline int Gia_ObjCopy2Array( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies2, iObj); }
Gia_ObjSetCopy2Array(Gia_Man_t * p,int iObj,int iLit)557 static inline void Gia_ObjSetCopy2Array( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies2, iObj, iLit); }
Gia_ManCleanCopy2Array(Gia_Man_t * p)558 static inline void Gia_ManCleanCopy2Array( Gia_Man_t * p ) { Vec_IntFill( &p->vCopies2, Gia_ManObjNum(p), -1 ); }
559
Gia_ObjFanin0CopyF(Gia_Man_t * p,int f,Gia_Obj_t * pObj)560 static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
Gia_ObjFanin1CopyF(Gia_Man_t * p,int f,Gia_Obj_t * pObj)561 static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
Gia_ObjFanin0CopyArray(Gia_Man_t * p,Gia_Obj_t * pObj)562 static inline int Gia_ObjFanin0CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p,pObj)), Gia_ObjFaninC0(pObj)); }
Gia_ObjFanin1CopyArray(Gia_Man_t * p,Gia_Obj_t * pObj)563 static inline int Gia_ObjFanin1CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId1p(p,pObj)), Gia_ObjFaninC1(pObj)); }
564
Gia_ObjFromLit(Gia_Man_t * p,int iLit)565 static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
Gia_ObjToLit(Gia_Man_t * p,Gia_Obj_t * pObj)566 static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
Gia_ObjPhaseRealLit(Gia_Man_t * p,int iLit)567 static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); }
568
Gia_ObjLevelId(Gia_Man_t * p,int Id)569 static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); }
Gia_ObjLevel(Gia_Man_t * p,Gia_Obj_t * pObj)570 static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); }
Gia_ObjSetLevelId(Gia_Man_t * p,int Id,int l)571 static inline void Gia_ObjSetLevelId( Gia_Man_t * p, int Id, int l ) { Vec_IntSetEntry(p->vLevels, Id, l); }
Gia_ObjSetLevel(Gia_Man_t * p,Gia_Obj_t * pObj,int l)572 static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Gia_ObjSetLevelId( p, Gia_ObjId(p,pObj), l ); }
Gia_ObjSetCoLevel(Gia_Man_t * p,Gia_Obj_t * pObj)573 static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); }
Gia_ObjSetBufLevel(Gia_Man_t * p,Gia_Obj_t * pObj)574 static inline void Gia_ObjSetBufLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); }
Gia_ObjSetAndLevel(Gia_Man_t * p,Gia_Obj_t * pObj)575 static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
Gia_ObjSetXorLevel(Gia_Man_t * p,Gia_Obj_t * pObj)576 static inline void Gia_ObjSetXorLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsXor(pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
Gia_ObjSetMuxLevel(Gia_Man_t * p,Gia_Obj_t * pObj)577 static inline void Gia_ObjSetMuxLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsMux(p,pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt( Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))), Gia_ObjLevel(p,Gia_ObjFanin2(p,pObj))) ); }
Gia_ObjSetGateLevel(Gia_Man_t * p,Gia_Obj_t * pObj)578 static inline void Gia_ObjSetGateLevel( Gia_Man_t * p, Gia_Obj_t * pObj ){ if ( !p->fGiaSimple && Gia_ObjIsBuf(pObj) ) Gia_ObjSetBufLevel(p, pObj); else if ( Gia_ObjIsMux(p,pObj) ) Gia_ObjSetMuxLevel(p, pObj); else if ( Gia_ObjIsXor(pObj) ) Gia_ObjSetXorLevel(p, pObj); else if ( Gia_ObjIsAnd(pObj) ) Gia_ObjSetAndLevel(p, pObj); }
579
Gia_ObjHasNumId(Gia_Man_t * p,int Id)580 static inline int Gia_ObjHasNumId( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vTtNums, Id) > -ABC_INFINITY; }
Gia_ObjNumId(Gia_Man_t * p,int Id)581 static inline int Gia_ObjNumId( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vTtNums, Id); }
Gia_ObjNum(Gia_Man_t * p,Gia_Obj_t * pObj)582 static inline int Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vTtNums, Gia_ObjId(p,pObj)); }
Gia_ObjSetNumId(Gia_Man_t * p,int Id,int n)583 static inline void Gia_ObjSetNumId( Gia_Man_t * p, int Id, int n ) { Vec_IntWriteEntry(p->vTtNums, Id, n); }
Gia_ObjSetNum(Gia_Man_t * p,Gia_Obj_t * pObj,int n)584 static inline void Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { Vec_IntWriteEntry(p->vTtNums, Gia_ObjId(p,pObj), n); }
Gia_ObjResetNumId(Gia_Man_t * p,int Id)585 static inline void Gia_ObjResetNumId( Gia_Man_t * p, int Id ) { Vec_IntWriteEntry(p->vTtNums, Id, -ABC_INFINITY); }
586
Gia_ObjRefNumId(Gia_Man_t * p,int Id)587 static inline int Gia_ObjRefNumId( Gia_Man_t * p, int Id ) { return p->pRefs[Id]; }
Gia_ObjRefIncId(Gia_Man_t * p,int Id)588 static inline int Gia_ObjRefIncId( Gia_Man_t * p, int Id ) { return p->pRefs[Id]++; }
Gia_ObjRefDecId(Gia_Man_t * p,int Id)589 static inline int Gia_ObjRefDecId( Gia_Man_t * p, int Id ) { return --p->pRefs[Id]; }
Gia_ObjRefNum(Gia_Man_t * p,Gia_Obj_t * pObj)590 static inline int Gia_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjRefNumId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjRefInc(Gia_Man_t * p,Gia_Obj_t * pObj)591 static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjRefIncId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjRefDec(Gia_Man_t * p,Gia_Obj_t * pObj)592 static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjRefDecId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjRefFanin0Inc(Gia_Man_t * p,Gia_Obj_t * pObj)593 static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); }
Gia_ObjRefFanin1Inc(Gia_Man_t * p,Gia_Obj_t * pObj)594 static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); }
Gia_ObjRefFanin2Inc(Gia_Man_t * p,Gia_Obj_t * pObj)595 static inline void Gia_ObjRefFanin2Inc(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefInc(p, Gia_ObjFanin2(p, pObj)); }
Gia_ObjRefFanin0Dec(Gia_Man_t * p,Gia_Obj_t * pObj)596 static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); }
Gia_ObjRefFanin1Dec(Gia_Man_t * p,Gia_Obj_t * pObj)597 static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); }
Gia_ObjRefFanin2Dec(Gia_Man_t * p,Gia_Obj_t * pObj)598 static inline void Gia_ObjRefFanin2Dec(Gia_Man_t * p, Gia_Obj_t * pObj) { Gia_ObjRefDec(p, Gia_ObjFanin2(p, pObj)); }
599
Gia_ObjLutRefNumId(Gia_Man_t * p,int Id)600 static inline int Gia_ObjLutRefNumId( Gia_Man_t * p, int Id ) { assert(p->pLutRefs); return p->pLutRefs[Id]; }
Gia_ObjLutRefIncId(Gia_Man_t * p,int Id)601 static inline int Gia_ObjLutRefIncId( Gia_Man_t * p, int Id ) { assert(p->pLutRefs); return p->pLutRefs[Id]++; }
Gia_ObjLutRefDecId(Gia_Man_t * p,int Id)602 static inline int Gia_ObjLutRefDecId( Gia_Man_t * p, int Id ) { assert(p->pLutRefs); return --p->pLutRefs[Id]; }
Gia_ObjLutRefNum(Gia_Man_t * p,Gia_Obj_t * pObj)603 static inline int Gia_ObjLutRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLutRefs); return p->pLutRefs[Gia_ObjId(p, pObj)]; }
Gia_ObjLutRefInc(Gia_Man_t * p,Gia_Obj_t * pObj)604 static inline int Gia_ObjLutRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLutRefs); return p->pLutRefs[Gia_ObjId(p, pObj)]++; }
Gia_ObjLutRefDec(Gia_Man_t * p,Gia_Obj_t * pObj)605 static inline int Gia_ObjLutRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLutRefs); return --p->pLutRefs[Gia_ObjId(p, pObj)]; }
606
Gia_ObjSetTravIdCurrent(Gia_Man_t * p,Gia_Obj_t * pObj)607 static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; }
Gia_ObjSetTravIdPrevious(Gia_Man_t * p,Gia_Obj_t * pObj)608 static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; }
Gia_ObjIsTravIdCurrent(Gia_Man_t * p,Gia_Obj_t * pObj)609 static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); }
Gia_ObjIsTravIdPrevious(Gia_Man_t * p,Gia_Obj_t * pObj)610 static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); }
Gia_ObjSetTravIdCurrentId(Gia_Man_t * p,int Id)611 static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; }
Gia_ObjSetTravIdPreviousId(Gia_Man_t * p,int Id)612 static inline void Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1; }
Gia_ObjIsTravIdCurrentId(Gia_Man_t * p,int Id)613 static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); }
Gia_ObjIsTravIdPreviousId(Gia_Man_t * p,int Id)614 static inline int Gia_ObjIsTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds - 1); }
615
Gia_ManTimeClean(Gia_Man_t * p)616 static inline void Gia_ManTimeClean( Gia_Man_t * p ) { int i; assert( p->vTiming != NULL ); Vec_FltFill(p->vTiming, 3*Gia_ManObjNum(p), 0); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Vec_FltWriteEntry( p->vTiming, 3*i+1, (float)(ABC_INFINITY) ); }
Gia_ManTimeStart(Gia_Man_t * p)617 static inline void Gia_ManTimeStart( Gia_Man_t * p ) { assert( p->vTiming == NULL ); p->vTiming = Vec_FltAlloc(0); Gia_ManTimeClean( p ); }
Gia_ManTimeStop(Gia_Man_t * p)618 static inline void Gia_ManTimeStop( Gia_Man_t * p ) { assert( p->vTiming != NULL ); Vec_FltFreeP(&p->vTiming); }
Gia_ObjTimeArrival(Gia_Man_t * p,int Id)619 static inline float Gia_ObjTimeArrival( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+0); }
Gia_ObjTimeRequired(Gia_Man_t * p,int Id)620 static inline float Gia_ObjTimeRequired( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+1); }
Gia_ObjTimeSlack(Gia_Man_t * p,int Id)621 static inline float Gia_ObjTimeSlack( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+2); }
Gia_ObjTimeArrivalObj(Gia_Man_t * p,Gia_Obj_t * pObj)622 static inline float Gia_ObjTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeArrival( p, Gia_ObjId(p, pObj) ); }
Gia_ObjTimeRequiredObj(Gia_Man_t * p,Gia_Obj_t * pObj)623 static inline float Gia_ObjTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeRequired( p, Gia_ObjId(p, pObj) ); }
Gia_ObjTimeSlackObj(Gia_Man_t * p,Gia_Obj_t * pObj)624 static inline float Gia_ObjTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeSlack( p, Gia_ObjId(p, pObj) ); }
Gia_ObjSetTimeArrival(Gia_Man_t * p,int Id,float t)625 static inline void Gia_ObjSetTimeArrival( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+0, t ); }
Gia_ObjSetTimeRequired(Gia_Man_t * p,int Id,float t)626 static inline void Gia_ObjSetTimeRequired( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+1, t ); }
Gia_ObjSetTimeSlack(Gia_Man_t * p,int Id,float t)627 static inline void Gia_ObjSetTimeSlack( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+2, t ); }
Gia_ObjSetTimeArrivalObj(Gia_Man_t * p,Gia_Obj_t * pObj,float t)628 static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeArrival( p, Gia_ObjId(p, pObj), t ); }
Gia_ObjSetTimeRequiredObj(Gia_Man_t * p,Gia_Obj_t * pObj,float t)629 static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); }
Gia_ObjSetTimeSlackObj(Gia_Man_t * p,Gia_Obj_t * pObj,float t)630 static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); }
631
Gia_ObjSimWords(Gia_Man_t * p)632 static inline int Gia_ObjSimWords( Gia_Man_t * p ) { return Vec_WrdSize( p->vSimsPi ) / Gia_ManPiNum( p ); }
Gia_ObjSimPi(Gia_Man_t * p,int PiId)633 static inline word * Gia_ObjSimPi( Gia_Man_t * p, int PiId ) { return Vec_WrdEntryP( p->vSimsPi, PiId * Gia_ObjSimWords(p) ); }
Gia_ObjSim(Gia_Man_t * p,int Id)634 static inline word * Gia_ObjSim( Gia_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vSims, Id * Gia_ObjSimWords(p) ); }
Gia_ObjSimObj(Gia_Man_t * p,Gia_Obj_t * pObj)635 static inline word * Gia_ObjSimObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjSim( p, Gia_ObjId(p, pObj) ); }
636
637 // AIG construction
638 extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
Gia_ManAppendObj(Gia_Man_t * p)639 static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
640 {
641 if ( p->nObjs == p->nObjsAlloc )
642 {
643 int nObjNew = Abc_MinInt( 2 * p->nObjsAlloc, (1 << 29) );
644 if ( p->nObjs == (1 << 29) )
645 printf( "Hard limit on the number of nodes (2^29) is reached. Quitting...\n" ), exit(1);
646 assert( p->nObjs < nObjNew );
647 if ( p->fVerbose )
648 printf("Extending GIA object storage: %d -> %d.\n", p->nObjsAlloc, nObjNew );
649 assert( p->nObjsAlloc > 0 );
650 p->pObjs = ABC_REALLOC( Gia_Obj_t, p->pObjs, nObjNew );
651 memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gia_Obj_t) * (nObjNew - p->nObjsAlloc) );
652 if ( p->pMuxes )
653 {
654 p->pMuxes = ABC_REALLOC( unsigned, p->pMuxes, nObjNew );
655 memset( p->pMuxes + p->nObjsAlloc, 0, sizeof(unsigned) * (nObjNew - p->nObjsAlloc) );
656 }
657 p->nObjsAlloc = nObjNew;
658 }
659 if ( Vec_IntSize(&p->vHTable) ) Vec_IntPush( &p->vHash, 0 );
660 return Gia_ManObj( p, p->nObjs++ );
661 }
Gia_ManAppendCi(Gia_Man_t * p)662 static inline int Gia_ManAppendCi( Gia_Man_t * p )
663 {
664 Gia_Obj_t * pObj = Gia_ManAppendObj( p );
665 pObj->fTerm = 1;
666 pObj->iDiff0 = GIA_NONE;
667 pObj->iDiff1 = Vec_IntSize( p->vCis );
668 Vec_IntPush( p->vCis, Gia_ObjId(p, pObj) );
669 return Gia_ObjId( p, pObj ) << 1;
670 }
671
672 extern void Gia_ManQuantSetSuppAnd( Gia_Man_t * p, Gia_Obj_t * pObj );
673 extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj );
674
Gia_ManAppendAnd(Gia_Man_t * p,int iLit0,int iLit1)675 static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
676 {
677 Gia_Obj_t * pObj = Gia_ManAppendObj( p );
678 assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
679 assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
680 assert( p->fGiaSimple || Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
681 if ( iLit0 < iLit1 )
682 {
683 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
684 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit0));
685 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
686 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit1));
687 }
688 else
689 {
690 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
691 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit0));
692 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
693 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit1));
694 }
695 if ( p->pFanData )
696 {
697 Gia_ObjAddFanout( p, Gia_ObjFanin0(pObj), pObj );
698 Gia_ObjAddFanout( p, Gia_ObjFanin1(pObj), pObj );
699 }
700 if ( p->fSweeper )
701 {
702 Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
703 Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
704 if ( pFan0->fMark0 ) pFan0->fMark1 = 1; else pFan0->fMark0 = 1;
705 if ( pFan1->fMark0 ) pFan1->fMark1 = 1; else pFan1->fMark0 = 1;
706 pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
707 }
708 if ( p->fBuiltInSim )
709 {
710 Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
711 Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
712 pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
713 Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) );
714 }
715 if ( p->vSuppWords )
716 Gia_ManQuantSetSuppAnd( p, pObj );
717 return Gia_ObjId( p, pObj ) << 1;
718 }
Gia_ManAppendXorReal(Gia_Man_t * p,int iLit0,int iLit1)719 static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
720 {
721 Gia_Obj_t * pObj = Gia_ManAppendObj( p );
722 assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
723 assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
724 assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
725 //assert( !Abc_LitIsCompl(iLit0) );
726 //assert( !Abc_LitIsCompl(iLit1) );
727 if ( Abc_Lit2Var(iLit0) > Abc_Lit2Var(iLit1) )
728 {
729 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
730 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit0));
731 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
732 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit1));
733 }
734 else
735 {
736 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
737 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit0));
738 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
739 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit1));
740 }
741 p->nXors++;
742 return Gia_ObjId( p, pObj ) << 1;
743 }
Gia_ManAppendMuxReal(Gia_Man_t * p,int iLitC,int iLit1,int iLit0)744 static inline int Gia_ManAppendMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
745 {
746 Gia_Obj_t * pObj = Gia_ManAppendObj( p );
747 assert( p->pMuxes != NULL );
748 assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
749 assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
750 assert( iLitC >= 0 && Abc_Lit2Var(iLitC) < Gia_ManObjNum(p) );
751 assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
752 assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit0) );
753 assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit1) );
754 assert( !Vec_IntSize(&p->vHTable) || !Abc_LitIsCompl(iLit1) );
755 if ( Abc_Lit2Var(iLit0) < Abc_Lit2Var(iLit1) )
756 {
757 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
758 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit0));
759 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
760 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit1));
761 p->pMuxes[Gia_ObjId(p, pObj)] = iLitC;
762 }
763 else
764 {
765 pObj->iDiff1 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0));
766 pObj->fCompl1 = (unsigned)(Abc_LitIsCompl(iLit0));
767 pObj->iDiff0 = (unsigned)(Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1));
768 pObj->fCompl0 = (unsigned)(Abc_LitIsCompl(iLit1));
769 p->pMuxes[Gia_ObjId(p, pObj)] = Abc_LitNot(iLitC);
770 }
771 p->nMuxes++;
772 return Gia_ObjId( p, pObj ) << 1;
773 }
Gia_ManAppendBuf(Gia_Man_t * p,int iLit)774 static inline int Gia_ManAppendBuf( Gia_Man_t * p, int iLit )
775 {
776 Gia_Obj_t * pObj = Gia_ManAppendObj( p );
777 assert( iLit >= 0 && Abc_Lit2Var(iLit) < Gia_ManObjNum(p) );
778 pObj->iDiff0 = pObj->iDiff1 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit);
779 pObj->fCompl0 = pObj->fCompl1 = Abc_LitIsCompl(iLit);
780 p->nBufs++;
781 return Gia_ObjId( p, pObj ) << 1;
782 }
Gia_ManAppendCo(Gia_Man_t * p,int iLit0)783 static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )
784 {
785 Gia_Obj_t * pObj;
786 assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
787 assert( !Gia_ObjIsCo(Gia_ManObj(p, Abc_Lit2Var(iLit0))) );
788 pObj = Gia_ManAppendObj( p );
789 pObj->fTerm = 1;
790 pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
791 pObj->fCompl0 = Abc_LitIsCompl(iLit0);
792 pObj->iDiff1 = Vec_IntSize( p->vCos );
793 Vec_IntPush( p->vCos, Gia_ObjId(p, pObj) );
794 if ( p->pFanData )
795 Gia_ObjAddFanout( p, Gia_ObjFanin0(pObj), pObj );
796 return Gia_ObjId( p, pObj ) << 1;
797 }
Gia_ManAppendOr(Gia_Man_t * p,int iLit0,int iLit1)798 static inline int Gia_ManAppendOr( Gia_Man_t * p, int iLit0, int iLit1 )
799 {
800 return Abc_LitNot(Gia_ManAppendAnd( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
801 }
Gia_ManAppendMux(Gia_Man_t * p,int iCtrl,int iData1,int iData0)802 static inline int Gia_ManAppendMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
803 {
804 int iTemp0 = Gia_ManAppendAnd( p, Abc_LitNot(iCtrl), iData0 );
805 int iTemp1 = Gia_ManAppendAnd( p, iCtrl, iData1 );
806 return Abc_LitNotCond( Gia_ManAppendAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
807 }
Gia_ManAppendMaj(Gia_Man_t * p,int iData0,int iData1,int iData2)808 static inline int Gia_ManAppendMaj( Gia_Man_t * p, int iData0, int iData1, int iData2 )
809 {
810 int iTemp0 = Gia_ManAppendOr( p, iData1, iData2 );
811 int iTemp1 = Gia_ManAppendAnd( p, iData0, iTemp0 );
812 int iTemp2 = Gia_ManAppendAnd( p, iData1, iData2 );
813 return Gia_ManAppendOr( p, iTemp1, iTemp2 );
814 }
Gia_ManAppendXor(Gia_Man_t * p,int iLit0,int iLit1)815 static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 )
816 {
817 return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 );
818 }
819
Gia_ManAppendAnd2(Gia_Man_t * p,int iLit0,int iLit1)820 static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )
821 {
822 if ( !p->fGiaSimple )
823 {
824 if ( iLit0 < 2 )
825 return iLit0 ? iLit1 : 0;
826 if ( iLit1 < 2 )
827 return iLit1 ? iLit0 : 0;
828 if ( iLit0 == iLit1 )
829 return iLit1;
830 if ( iLit0 == Abc_LitNot(iLit1) )
831 return 0;
832 }
833 return Gia_ManAppendAnd( p, iLit0, iLit1 );
834 }
Gia_ManAppendOr2(Gia_Man_t * p,int iLit0,int iLit1)835 static inline int Gia_ManAppendOr2( Gia_Man_t * p, int iLit0, int iLit1 )
836 {
837 return Abc_LitNot(Gia_ManAppendAnd2( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
838 }
Gia_ManAppendMux2(Gia_Man_t * p,int iCtrl,int iData1,int iData0)839 static inline int Gia_ManAppendMux2( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
840 {
841 int iTemp0 = Gia_ManAppendAnd2( p, Abc_LitNot(iCtrl), iData0 );
842 int iTemp1 = Gia_ManAppendAnd2( p, iCtrl, iData1 );
843 return Abc_LitNotCond( Gia_ManAppendAnd2( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
844 }
Gia_ManAppendMaj2(Gia_Man_t * p,int iData0,int iData1,int iData2)845 static inline int Gia_ManAppendMaj2( Gia_Man_t * p, int iData0, int iData1, int iData2 )
846 {
847 int iTemp0 = Gia_ManAppendOr2( p, iData1, iData2 );
848 int iTemp1 = Gia_ManAppendAnd2( p, iData0, iTemp0 );
849 int iTemp2 = Gia_ManAppendAnd2( p, iData1, iData2 );
850 return Gia_ManAppendOr2( p, iTemp1, iTemp2 );
851 }
Gia_ManAppendXor2(Gia_Man_t * p,int iLit0,int iLit1)852 static inline int Gia_ManAppendXor2( Gia_Man_t * p, int iLit0, int iLit1 )
853 {
854 return Gia_ManAppendMux2( p, iLit0, Abc_LitNot(iLit1), iLit1 );
855 }
856
Gia_ManAppendXorReal2(Gia_Man_t * p,int iLit0,int iLit1)857 static inline int Gia_ManAppendXorReal2( Gia_Man_t * p, int iLit0, int iLit1 )
858 {
859 if ( !p->fGiaSimple )
860 {
861 if ( iLit0 < 2 )
862 return iLit0 ? Abc_LitNot(iLit1) : iLit1;
863 if ( iLit1 < 2 )
864 return iLit1 ? Abc_LitNot(iLit0) : iLit0;
865 if ( iLit0 == iLit1 )
866 return 0;
867 if ( iLit0 == Abc_LitNot(iLit1) )
868 return 1;
869 }
870 return Gia_ManAppendXorReal( p, iLit0, iLit1 );
871 }
872
Gia_ManPatchCoDriver(Gia_Man_t * p,int iCoIndex,int iLit0)873 static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 )
874 {
875 Gia_Obj_t * pObjCo = Gia_ManCo( p, iCoIndex );
876 assert( Gia_ObjId(p, pObjCo) > Abc_Lit2Var(iLit0) );
877 pObjCo->iDiff0 = Gia_ObjId(p, pObjCo) - Abc_Lit2Var(iLit0);
878 pObjCo->fCompl0 = Abc_LitIsCompl(iLit0);
879 }
880
881 #define GIA_ZER 1
882 #define GIA_ONE 2
883 #define GIA_UND 3
884
Gia_XsimNotCond(int Value,int fCompl)885 static inline int Gia_XsimNotCond( int Value, int fCompl )
886 {
887 if ( Value == GIA_UND )
888 return GIA_UND;
889 if ( Value == GIA_ZER + fCompl )
890 return GIA_ZER;
891 return GIA_ONE;
892 }
Gia_XsimAndCond(int Value0,int fCompl0,int Value1,int fCompl1)893 static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCompl1 )
894 {
895 if ( Value0 == GIA_ZER + fCompl0 || Value1 == GIA_ZER + fCompl1 )
896 return GIA_ZER;
897 if ( Value0 == GIA_UND || Value1 == GIA_UND )
898 return GIA_UND;
899 return GIA_ONE;
900 }
901
902
Gia_ObjTerSimSetC(Gia_Obj_t * pObj)903 static inline void Gia_ObjTerSimSetC( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 0; }
Gia_ObjTerSimSet0(Gia_Obj_t * pObj)904 static inline void Gia_ObjTerSimSet0( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 0; }
Gia_ObjTerSimSet1(Gia_Obj_t * pObj)905 static inline void Gia_ObjTerSimSet1( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 1; }
Gia_ObjTerSimSetX(Gia_Obj_t * pObj)906 static inline void Gia_ObjTerSimSetX( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 1; }
907
Gia_ObjTerSimGetC(Gia_Obj_t * pObj)908 static inline int Gia_ObjTerSimGetC( Gia_Obj_t * pObj ) { return !pObj->fMark0 && !pObj->fMark1; }
Gia_ObjTerSimGet0(Gia_Obj_t * pObj)909 static inline int Gia_ObjTerSimGet0( Gia_Obj_t * pObj ) { return pObj->fMark0 && !pObj->fMark1; }
Gia_ObjTerSimGet1(Gia_Obj_t * pObj)910 static inline int Gia_ObjTerSimGet1( Gia_Obj_t * pObj ) { return !pObj->fMark0 && pObj->fMark1; }
Gia_ObjTerSimGetX(Gia_Obj_t * pObj)911 static inline int Gia_ObjTerSimGetX( Gia_Obj_t * pObj ) { return pObj->fMark0 && pObj->fMark1; }
912
Gia_ObjTerSimGet0Fanin0(Gia_Obj_t * pObj)913 static inline int Gia_ObjTerSimGet0Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
Gia_ObjTerSimGet1Fanin0(Gia_Obj_t * pObj)914 static inline int Gia_ObjTerSimGet1Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
915
Gia_ObjTerSimGet0Fanin1(Gia_Obj_t * pObj)916 static inline int Gia_ObjTerSimGet0Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
Gia_ObjTerSimGet1Fanin1(Gia_Obj_t * pObj)917 static inline int Gia_ObjTerSimGet1Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
918
Gia_ObjTerSimAnd(Gia_Obj_t * pObj)919 static inline void Gia_ObjTerSimAnd( Gia_Obj_t * pObj )
920 {
921 assert( Gia_ObjIsAnd(pObj) );
922 assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
923 assert( !Gia_ObjTerSimGetC( Gia_ObjFanin1(pObj) ) );
924 if ( Gia_ObjTerSimGet0Fanin0(pObj) || Gia_ObjTerSimGet0Fanin1(pObj) )
925 Gia_ObjTerSimSet0( pObj );
926 else if ( Gia_ObjTerSimGet1Fanin0(pObj) && Gia_ObjTerSimGet1Fanin1(pObj) )
927 Gia_ObjTerSimSet1( pObj );
928 else
929 Gia_ObjTerSimSetX( pObj );
930 }
Gia_ObjTerSimCo(Gia_Obj_t * pObj)931 static inline void Gia_ObjTerSimCo( Gia_Obj_t * pObj )
932 {
933 assert( Gia_ObjIsCo(pObj) );
934 assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
935 if ( Gia_ObjTerSimGet0Fanin0(pObj) )
936 Gia_ObjTerSimSet0( pObj );
937 else if ( Gia_ObjTerSimGet1Fanin0(pObj) )
938 Gia_ObjTerSimSet1( pObj );
939 else
940 Gia_ObjTerSimSetX( pObj );
941 }
Gia_ObjTerSimRo(Gia_Man_t * p,Gia_Obj_t * pObj)942 static inline void Gia_ObjTerSimRo( Gia_Man_t * p, Gia_Obj_t * pObj )
943 {
944 Gia_Obj_t * pTemp = Gia_ObjRoToRi(p, pObj);
945 assert( Gia_ObjIsRo(p, pObj) );
946 assert( !Gia_ObjTerSimGetC( pTemp ) );
947 pObj->fMark0 = pTemp->fMark0;
948 pObj->fMark1 = pTemp->fMark1;
949 }
950
Gia_ObjTerSimPrint(Gia_Obj_t * pObj)951 static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
952 {
953 if ( Gia_ObjTerSimGet0(pObj) )
954 printf( "0" );
955 else if ( Gia_ObjTerSimGet1(pObj) )
956 printf( "1" );
957 else if ( Gia_ObjTerSimGetX(pObj) )
958 printf( "X" );
959 }
960
Gia_AigerReadInt(unsigned char * pPos)961 static inline int Gia_AigerReadInt( unsigned char * pPos )
962 {
963 int i, Value = 0;
964 for ( i = 0; i < 4; i++ )
965 Value = (Value << 8) | *pPos++;
966 return Value;
967 }
Gia_AigerWriteInt(unsigned char * pPos,int Value)968 static inline void Gia_AigerWriteInt( unsigned char * pPos, int Value )
969 {
970 int i;
971 for ( i = 3; i >= 0; i-- )
972 *pPos++ = (Value >> (8*i)) & 255;
973 }
Gia_AigerReadUnsigned(unsigned char ** ppPos)974 static inline unsigned Gia_AigerReadUnsigned( unsigned char ** ppPos )
975 {
976 unsigned x = 0, i = 0;
977 unsigned char ch;
978 while ((ch = *(*ppPos)++) & 0x80)
979 x |= (ch & 0x7f) << (7 * i++);
980 return x | (ch << (7 * i));
981 }
Gia_AigerWriteUnsigned(Vec_Str_t * vStr,unsigned x)982 static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x )
983 {
984 unsigned char ch;
985 while (x & ~0x7f)
986 {
987 ch = (x & 0x7f) | 0x80;
988 Vec_StrPush( vStr, ch );
989 x >>= 7;
990 }
991 ch = x;
992 Vec_StrPush( vStr, ch );
993 }
Gia_AigerWriteUnsignedFile(FILE * pFile,unsigned x)994 static inline void Gia_AigerWriteUnsignedFile( FILE * pFile, unsigned x )
995 {
996 unsigned char ch;
997 while (x & ~0x7f)
998 {
999 ch = (x & 0x7f) | 0x80;
1000 fputc( ch, pFile );
1001 x >>= 7;
1002 }
1003 ch = x;
1004 fputc( ch, pFile );
1005 }
Gia_AigerWriteUnsignedBuffer(unsigned char * pBuffer,int Pos,unsigned x)1006 static inline int Gia_AigerWriteUnsignedBuffer( unsigned char * pBuffer, int Pos, unsigned x )
1007 {
1008 unsigned char ch;
1009 while (x & ~0x7f)
1010 {
1011 ch = (x & 0x7f) | 0x80;
1012 pBuffer[Pos++] = ch;
1013 x >>= 7;
1014 }
1015 ch = x;
1016 pBuffer[Pos++] = ch;
1017 return Pos;
1018 }
1019
Gia_ObjReprObj(Gia_Man_t * p,int Id)1020 static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
Gia_ObjRepr(Gia_Man_t * p,int Id)1021 static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
Gia_ObjSetRepr(Gia_Man_t * p,int Id,int Num)1022 static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num; }
Gia_ObjSetReprRev(Gia_Man_t * p,int Id,int Num)1023 static inline void Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ assert( Num == GIA_VOID || Num > Id ); p->pReprs[Id].iRepr = Num; }
Gia_ObjUnsetRepr(Gia_Man_t * p,int Id)1024 static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; }
Gia_ObjHasRepr(Gia_Man_t * p,int Id)1025 static inline int Gia_ObjHasRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr != GIA_VOID; }
Gia_ObjReprSelf(Gia_Man_t * p,int Id)1026 static inline int Gia_ObjReprSelf( Gia_Man_t * p, int Id ) { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id; }
Gia_ObjSibl(Gia_Man_t * p,int Id)1027 static inline int Gia_ObjSibl( Gia_Man_t * p, int Id ) { return p->pSibls ? p->pSibls[Id] : 0; }
Gia_ObjSiblObj(Gia_Man_t * p,int Id)1028 static inline Gia_Obj_t * Gia_ObjSiblObj( Gia_Man_t * p, int Id ) { return (p->pSibls && p->pSibls[Id]) ? Gia_ManObj(p, p->pSibls[Id]) : NULL; }
1029
Gia_ObjProved(Gia_Man_t * p,int Id)1030 static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
Gia_ObjSetProved(Gia_Man_t * p,int Id)1031 static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
Gia_ObjUnsetProved(Gia_Man_t * p,int Id)1032 static inline void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; }
1033
Gia_ObjFailed(Gia_Man_t * p,int Id)1034 static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; }
Gia_ObjSetFailed(Gia_Man_t * p,int Id)1035 static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; }
1036
Gia_ObjColor(Gia_Man_t * p,int Id,int c)1037 static inline int Gia_ObjColor( Gia_Man_t * p, int Id, int c ) { return c? p->pReprs[Id].fColorB : p->pReprs[Id].fColorA; }
Gia_ObjColors(Gia_Man_t * p,int Id)1038 static inline int Gia_ObjColors( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fColorB * 2 + p->pReprs[Id].fColorA; }
Gia_ObjSetColor(Gia_Man_t * p,int Id,int c)1039 static inline void Gia_ObjSetColor( Gia_Man_t * p, int Id, int c ) { if (c) p->pReprs[Id].fColorB = 1; else p->pReprs[Id].fColorA = 1; }
Gia_ObjSetColors(Gia_Man_t * p,int Id)1040 static inline void Gia_ObjSetColors( Gia_Man_t * p, int Id ) { p->pReprs[Id].fColorB = p->pReprs[Id].fColorA = 1; }
Gia_ObjVisitColor(Gia_Man_t * p,int Id,int c)1041 static inline int Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c ) { int x; if (c) { x = p->pReprs[Id].fColorB; p->pReprs[Id].fColorB = 1; } else { x = p->pReprs[Id].fColorA; p->pReprs[Id].fColorA = 1; } return x; }
Gia_ObjDiffColors(Gia_Man_t * p,int i,int j)1042 static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
Gia_ObjDiffColors2(Gia_Man_t * p,int i,int j)1043 static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
1044
Gia_ObjNextObj(Gia_Man_t * p,int Id)1045 static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id ) { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );}
Gia_ObjNext(Gia_Man_t * p,int Id)1046 static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; }
Gia_ObjSetNext(Gia_Man_t * p,int Id,int Num)1047 static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
1048
Gia_ObjIsConst(Gia_Man_t * p,int Id)1049 static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
Gia_ObjIsHead(Gia_Man_t * p,int Id)1050 static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; }
Gia_ObjIsNone(Gia_Man_t * p,int Id)1051 static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) <= 0; }
Gia_ObjIsTail(Gia_Man_t * p,int Id)1052 static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) <= 0; }
Gia_ObjIsClass(Gia_Man_t * p,int Id)1053 static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; }
Gia_ObjHasSameRepr(Gia_Man_t * p,int i,int k)1054 static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; }
Gia_ObjIsFailedPair(Gia_Man_t * p,int i,int k)1055 static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); }
Gia_ClassIsPair(Gia_Man_t * p,int i)1056 static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) <= 0; }
Gia_ClassUndoPair(Gia_Man_t * p,int i)1057 static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); }
1058
1059 #define Gia_ManForEachConst( p, i ) \
1060 for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
1061 #define Gia_ManForEachClass( p, i ) \
1062 for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else
1063 #define Gia_ManForEachClass0( p, i ) \
1064 for ( i = 0; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else
1065 #define Gia_ManForEachClassReverse( p, i ) \
1066 for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else
1067 #define Gia_ClassForEachObj( p, i, iObj ) \
1068 for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj > 0; iObj = Gia_ObjNext(p, iObj) )
1069 #define Gia_ClassForEachObj1( p, i, iObj ) \
1070 for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
1071
1072
Gia_ObjFoffsetId(Gia_Man_t * p,int Id)1073 static inline int Gia_ObjFoffsetId( Gia_Man_t * p, int Id ) { return Vec_IntEntry( p->vFanout, Id ); }
Gia_ObjFoffset(Gia_Man_t * p,Gia_Obj_t * pObj)1074 static inline int Gia_ObjFoffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFoffsetId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjFanoutNumId(Gia_Man_t * p,int Id)1075 static inline int Gia_ObjFanoutNumId( Gia_Man_t * p, int Id ) { return Vec_IntEntry( p->vFanoutNums, Id ); }
Gia_ObjFanoutNum(Gia_Man_t * p,Gia_Obj_t * pObj)1076 static inline int Gia_ObjFanoutNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFanoutNumId( p, Gia_ObjId(p, pObj) ); }
Gia_ObjFanoutId(Gia_Man_t * p,int Id,int i)1077 static inline int Gia_ObjFanoutId( Gia_Man_t * p, int Id, int i ) { return Vec_IntEntry( p->vFanout, Gia_ObjFoffsetId(p, Id) + i ); }
Gia_ObjFanout0(Gia_Man_t * p,Gia_Obj_t * pObj)1078 static inline Gia_Obj_t * Gia_ObjFanout0( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Gia_ObjFanoutId(p, Gia_ObjId(p, pObj), 0) ); }
Gia_ObjFanout(Gia_Man_t * p,Gia_Obj_t * pObj,int i)1079 static inline Gia_Obj_t * Gia_ObjFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int i ) { return Gia_ManObj( p, Gia_ObjFanoutId(p, Gia_ObjId(p, pObj), i) ); }
Gia_ObjSetFanout(Gia_Man_t * p,Gia_Obj_t * pObj,int i,Gia_Obj_t * pFan)1080 static inline void Gia_ObjSetFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int i, Gia_Obj_t * pFan ) { Vec_IntWriteEntry( p->vFanout, Gia_ObjFoffset(p, pObj) + i, Gia_ObjId(p, pFan) ); }
Gia_ObjSetFanoutInt(Gia_Man_t * p,Gia_Obj_t * pObj,int i,int x)1081 static inline void Gia_ObjSetFanoutInt( Gia_Man_t * p, Gia_Obj_t * pObj, int i, int x ) { Vec_IntWriteEntry( p->vFanout, Gia_ObjFoffset(p, pObj) + i, x ); }
1082
1083 #define Gia_ObjForEachFanoutStatic( p, pObj, pFanout, i ) \
1084 for ( i = 0; (i < Gia_ObjFanoutNum(p, pObj)) && (((pFanout) = Gia_ObjFanout(p, pObj, i)), 1); i++ )
1085 #define Gia_ObjForEachFanoutStaticId( p, Id, FanId, i ) \
1086 for ( i = 0; (i < Gia_ObjFanoutNumId(p, Id)) && (((FanId) = Gia_ObjFanoutId(p, Id, i)), 1); i++ )
1087
Gia_ManHasMapping(Gia_Man_t * p)1088 static inline int Gia_ManHasMapping( Gia_Man_t * p ) { return p->vMapping != NULL; }
Gia_ObjIsLut(Gia_Man_t * p,int Id)1089 static inline int Gia_ObjIsLut( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vMapping, Id) != 0; }
Gia_ObjLutSize(Gia_Man_t * p,int Id)1090 static inline int Gia_ObjLutSize( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vMapping, Vec_IntEntry(p->vMapping, Id)); }
Gia_ObjLutFanins(Gia_Man_t * p,int Id)1091 static inline int * Gia_ObjLutFanins( Gia_Man_t * p, int Id ) { return Vec_IntEntryP(p->vMapping, Vec_IntEntry(p->vMapping, Id)) + 1; }
Gia_ObjLutFanin(Gia_Man_t * p,int Id,int i)1092 static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { return Gia_ObjLutFanins(p, Id)[i]; }
Gia_ObjLutMuxId(Gia_Man_t * p,int Id)1093 static inline int Gia_ObjLutMuxId( Gia_Man_t * p, int Id ) { return Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)]; }
Gia_ObjLutIsMux(Gia_Man_t * p,int Id)1094 static inline int Gia_ObjLutIsMux( Gia_Man_t * p, int Id ) { return (int)(Gia_ObjLutMuxId(p, Id) < 0); }
1095
Gia_ManHasMapping2(Gia_Man_t * p)1096 static inline int Gia_ManHasMapping2( Gia_Man_t * p ) { return p->vMapping2 != NULL; }
Gia_ObjIsLut2(Gia_Man_t * p,int Id)1097 static inline int Gia_ObjIsLut2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)) != 0; }
Gia_ObjLutSize2(Gia_Man_t * p,int Id)1098 static inline int Gia_ObjLutSize2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)); }
Gia_ObjLutFanins2(Gia_Man_t * p,int Id)1099 static inline Vec_Int_t * Gia_ObjLutFanins2( Gia_Man_t * p, int Id ) { return Vec_WecEntry(p->vMapping2, Id); }
Gia_ObjLutFanin2(Gia_Man_t * p,int Id,int i)1100 static inline int Gia_ObjLutFanin2( Gia_Man_t * p, int Id, int i ) { return Vec_IntEntry(Vec_WecEntry(p->vMapping2, Id), i); }
Gia_ObjLutFanoutNum2(Gia_Man_t * p,int Id)1101 static inline int Gia_ObjLutFanoutNum2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts2, Id)); }
Gia_ObjLutFanout2(Gia_Man_t * p,int Id,int i)1102 static inline int Gia_ObjLutFanout2( Gia_Man_t * p, int Id, int i ) { return Vec_IntEntry(Vec_WecEntry(p->vFanouts2, Id), i); }
1103
Gia_ManHasCellMapping(Gia_Man_t * p)1104 static inline int Gia_ManHasCellMapping( Gia_Man_t * p ) { return p->vCellMapping != NULL; }
Gia_ObjIsCell(Gia_Man_t * p,int iLit)1105 static inline int Gia_ObjIsCell( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) != 0; }
Gia_ObjIsCellInv(Gia_Man_t * p,int iLit)1106 static inline int Gia_ObjIsCellInv( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) == -1; }
Gia_ObjIsCellBuf(Gia_Man_t * p,int iLit)1107 static inline int Gia_ObjIsCellBuf( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) == -2; }
Gia_ObjCellSize(Gia_Man_t * p,int iLit)1108 static inline int Gia_ObjCellSize( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, Vec_IntEntry(p->vCellMapping, iLit)); }
Gia_ObjCellFanins(Gia_Man_t * p,int iLit)1109 static inline int * Gia_ObjCellFanins( Gia_Man_t * p, int iLit ) { return Vec_IntEntryP(p->vCellMapping, Vec_IntEntry(p->vCellMapping, iLit))+1; }
Gia_ObjCellFanin(Gia_Man_t * p,int iLit,int i)1110 static inline int Gia_ObjCellFanin( Gia_Man_t * p, int iLit, int i ){ return Gia_ObjCellFanins(p, iLit)[i]; }
Gia_ObjCellId(Gia_Man_t * p,int iLit)1111 static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { return Gia_ObjCellFanins(p, iLit)[Gia_ObjCellSize(p, iLit)]; }
1112
1113 #define Gia_ManForEachLut( p, i ) \
1114 for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut(p, i) ) {} else
1115 #define Gia_ManForEachLutReverse( p, i ) \
1116 for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsLut(p, i) ) {} else
1117 #define Gia_LutForEachFanin( p, i, iFan, k ) \
1118 for ( k = 0; k < Gia_ObjLutSize(p,i) && ((iFan = Gia_ObjLutFanins(p,i)[k]),1); k++ )
1119 #define Gia_LutForEachFaninObj( p, i, pFanin, k ) \
1120 for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ )
1121
1122 #define Gia_ManForEachLut2( p, i ) \
1123 for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut2(p, i) ) {} else
1124 #define Gia_ManForEachLut2Reverse( p, i ) \
1125 for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsLut2(p, i) ) {} else
1126 #define Gia_ManForEachLut2Vec( vIds, p, vVec, iObj, i ) \
1127 for ( i = 0; i < Vec_IntSize(vIds) && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i++ )
1128 #define Gia_ManForEachLut2VecReverse( vIds, p, vVec, iObj, i ) \
1129 for ( i = Vec_IntSize(vIds)-1; i >= 0 && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i-- )
1130 #define Gia_LutForEachFanin2( p, i, iFan, k ) \
1131 for ( k = 0; k < Gia_ObjLutSize2(p,i) && ((iFan = Gia_ObjLutFanin2(p,i,k)),1); k++ )
1132 #define Gia_LutForEachFanout2( p, i, iFan, k ) \
1133 for ( k = 0; k < Gia_ObjLutFanoutNum2(p,i) && ((iFan = Gia_ObjLutFanout2(p,i,k)),1); k++ )
1134
1135 #define Gia_ManForEachCell( p, i ) \
1136 for ( i = 2; i < 2*Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsCell(p, i) ) {} else
1137 #define Gia_CellForEachFanin( p, i, iFanLit, k ) \
1138 for ( k = 0; k < Gia_ObjCellSize(p,i) && ((iFanLit = Gia_ObjCellFanins(p,i)[k]),1); k++ )
1139
1140 ////////////////////////////////////////////////////////////////////////
1141 /// MACRO DEFINITIONS ///
1142 ////////////////////////////////////////////////////////////////////////
1143
1144 #define Gia_ManForEachObj( p, pObj, i ) \
1145 for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )
1146 #define Gia_ManForEachObj1( p, pObj, i ) \
1147 for ( i = 1; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )
1148 #define Gia_ManForEachObjVec( vVec, p, pObj, i ) \
1149 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
1150 #define Gia_ManForEachObjVecReverse( vVec, p, pObj, i ) \
1151 for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
1152 #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \
1153 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Abc_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Abc_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
1154 #define Gia_ManForEachObjReverse( p, pObj, i ) \
1155 for ( i = p->nObjs - 1; (i >= 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
1156 #define Gia_ManForEachObjReverse1( p, pObj, i ) \
1157 for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
1158 #define Gia_ManForEachBuf( p, pObj, i ) \
1159 for ( i = Gia_ManBufNum(p) ? 0 : p->nObjs; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsBuf(pObj) ) {} else
1160 #define Gia_ManForEachBufId( p, i ) \
1161 for ( i = 0; (i < p->nObjs); i++ ) if ( !Gia_ObjIsBuf(Gia_ManObj(p, i)) ) {} else
1162 #define Gia_ManForEachAnd( p, pObj, i ) \
1163 for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else
1164 #define Gia_ManForEachAndId( p, i ) \
1165 for ( i = 0; (i < p->nObjs); i++ ) if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) {} else
1166 #define Gia_ManForEachMuxId( p, i ) \
1167 for ( i = 0; (i < p->nObjs); i++ ) if ( !Gia_ObjIsMuxId(p, i) ) {} else
1168 #define Gia_ManForEachCand( p, pObj, i ) \
1169 for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsCand(pObj) ) {} else
1170 #define Gia_ManForEachAndReverse( p, pObj, i ) \
1171 for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else
1172 #define Gia_ManForEachAndReverseId( p, i ) \
1173 for ( i = p->nObjs - 1; (i > 0); i-- ) if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) {} else
1174 #define Gia_ManForEachMux( p, pObj, i ) \
1175 for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsMuxId(p, i) ) {} else
1176 #define Gia_ManForEachCi( p, pObj, i ) \
1177 for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
1178 #define Gia_ManForEachCiId( p, Id, i ) \
1179 for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ )
1180 #define Gia_ManForEachCiVec( vVec, p, pObj, i ) \
1181 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManCi(p, Vec_IntEntry(vVec,i))); i++ )
1182 #define Gia_ManForEachCiReverse( p, pObj, i ) \
1183 for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- )
1184 #define Gia_ManForEachCo( p, pObj, i ) \
1185 for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ )
1186 #define Gia_ManForEachCoVec( vVec, p, pObj, i ) \
1187 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManCo(p, Vec_IntEntry(vVec,i))); i++ )
1188 #define Gia_ManForEachCoId( p, Id, i ) \
1189 for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((Id) = Gia_ObjId(p, Gia_ManCo(p, i))); i++ )
1190 #define Gia_ManForEachCoReverse( p, pObj, i ) \
1191 for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- )
1192 #define Gia_ManForEachCoDriver( p, pObj, i ) \
1193 for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ObjFanin0(Gia_ManCo(p, i))); i++ )
1194 #define Gia_ManForEachCoDriverId( p, DriverId, i ) \
1195 for ( i = 0; (i < Vec_IntSize(p->vCos)) && (((DriverId) = Gia_ObjFaninId0p(p, Gia_ManCo(p, i))), 1); i++ )
1196 #define Gia_ManForEachPi( p, pObj, i ) \
1197 for ( i = 0; (i < Gia_ManPiNum(p)) && ((pObj) = Gia_ManCi(p, i)); i++ )
1198 #define Gia_ManForEachPo( p, pObj, i ) \
1199 for ( i = 0; (i < Gia_ManPoNum(p)) && ((pObj) = Gia_ManCo(p, i)); i++ )
1200 #define Gia_ManForEachRo( p, pObj, i ) \
1201 for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObj) = Gia_ManCi(p, Gia_ManPiNum(p)+i)); i++ )
1202 #define Gia_ManForEachRi( p, pObj, i ) \
1203 for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObj) = Gia_ManCo(p, Gia_ManPoNum(p)+i)); i++ )
1204 #define Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) \
1205 for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObjRi) = Gia_ManCo(p, Gia_ManPoNum(p)+i)) && ((pObjRo) = Gia_ManCi(p, Gia_ManPiNum(p)+i)); i++ )
1206
1207 ////////////////////////////////////////////////////////////////////////
1208 /// FUNCTION DECLARATIONS ///
1209 ////////////////////////////////////////////////////////////////////////
1210
1211 /*=== giaAiger.c ===========================================================*/
1212 extern int Gia_FileSize( char * pFileName );
1213 extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck );
1214 extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck );
1215 extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine );
1216 extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
1217 extern Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );
1218 extern Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
1219 extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName );
1220 /*=== giaBalance.c ===========================================================*/
1221 extern Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fStrict, int fVerbose );
1222 extern Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
1223 extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose );
1224 extern Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
1225 extern Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
1226 /*=== giaBidec.c ===========================================================*/
1227 extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
1228 extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
1229 /*=== giaCex.c ============================================================*/
1230 extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
1231 extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
1232 extern int Gia_ManSetFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
1233 extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex );
1234 extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
1235 extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
1236 extern Abc_Cex_t * Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex );
1237 extern Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex );
1238 /*=== giaCsatOld.c ============================================================*/
1239 extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
1240 /*=== giaCsat.c ============================================================*/
1241 typedef struct Cbs_Man_t_ Cbs_Man_t;
1242 extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia );
1243 extern void Cbs_ManStop( Cbs_Man_t * p );
1244 extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
1245 extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
1246 extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
1247 extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
1248 extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p );
1249 /*=== giaCTas.c ============================================================*/
1250 extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
1251 /*=== giaCof.c =============================================================*/
1252 extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
1253 extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar );
1254 extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose );
1255 extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
1256 /*=== giaDfs.c ============================================================*/
1257 extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
1258 extern void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes );
1259 extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves );
1260 extern Vec_Int_t * Gia_ManCollectAndsAll( Gia_Man_t * p );
1261 extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes );
1262 extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
1263 extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
1264 extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p );
1265 extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p );
1266 extern void Gia_ManCollectTfi( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes );
1267 extern void Gia_ManCollectTfo( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes );
1268 /*=== giaDup.c ============================================================*/
1269 extern void Gia_ManDupRemapLiterals( Vec_Int_t * vLits, Gia_Man_t * p );
1270 extern void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p );
1271 extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p );
1272 extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p );
1273 extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
1274 extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
1275 extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
1276 extern Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft );
1277 extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p );
1278 extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
1279 extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
1280 extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
1281 extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
1282 extern Gia_Man_t * Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 );
1283 extern Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p );
1284 extern Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis );
1285 extern Gia_Man_t * Gia_ManDupZero( Gia_Man_t * p );
1286 extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
1287 extern Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm );
1288 extern Gia_Man_t * Gia_ManDupPermFlopGap( Gia_Man_t * p, Vec_Int_t * vFfPerm );
1289 extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo );
1290 extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo );
1291 extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo );
1292 extern Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs );
1293 extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p );
1294 extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
1295 extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p );
1296 extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
1297 extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
1298 extern Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo );
1299 extern Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value );
1300 extern Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value );
1301 extern Gia_Man_t * Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 );
1302 extern Gia_Man_t * Gia_ManDupBlock( Gia_Man_t * p, int nBlock );
1303 extern Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar );
1304 extern Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar );
1305 extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
1306 extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
1307 extern Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds );
1308 extern int Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds );
1309 extern int Gia_ManDupConeBackObjs( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vObjs );
1310 extern Gia_Man_t * Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pObj );
1311 extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
1312 extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
1313 extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
1314 extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
1315 extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
1316 extern Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra );
1317 extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
1318 extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
1319 extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
1320 extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
1321 extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose );
1322 extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
1323 extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
1324 extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p );
1325 extern Gia_Man_t * Gia_ManTransformToDual( Gia_Man_t * p );
1326 extern Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p );
1327 extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
1328 extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
1329 extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
1330 extern Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis );
1331 extern Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
1332 extern Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
1333 extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p );
1334 extern Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p );
1335 extern Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
1336 extern Gia_Man_t * Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax );
1337 extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose );
1338 extern Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p );
1339 extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
1340 extern int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
1341 /*=== giaEdge.c ==========================================================*/
1342 extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray );
1343 extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p );
1344 extern void Gia_ManConvertPackingToEdges( Gia_Man_t * p );
1345 extern int Gia_ObjCheckEdge( Gia_Man_t * p, int iObj, int iNext );
1346 extern int Gia_ManEvalEdgeDelay( Gia_Man_t * p );
1347 extern int Gia_ManEvalEdgeCount( Gia_Man_t * p );
1348 extern int Gia_ManComputeEdgeDelay( Gia_Man_t * p, int fUseTwo );
1349 extern int Gia_ManComputeEdgeDelay2( Gia_Man_t * p );
1350 extern void Gia_ManUpdateMapping( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Wec_t * vWin );
1351 extern int Gia_ManEvalWindow( Gia_Man_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Wec_t * vWin, Vec_Int_t * vTemp, int fUseTwo );
1352 /*=== giaEnable.c ==========================================================*/
1353 extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
1354 extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
1355 extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
1356 /*=== giaEquiv.c ==========================================================*/
1357 extern void Gia_ManOrigIdsInit( Gia_Man_t * p );
1358 extern void Gia_ManOrigIdsStart( Gia_Man_t * p );
1359 extern void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
1360 extern Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
1361 extern Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose );
1362 extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
1363 extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
1364 extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
1365 extern void Gia_ManDeriveReprs( Gia_Man_t * p );
1366 extern int Gia_ManEquivCountLits( Gia_Man_t * p );
1367 extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p );
1368 extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
1369 extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
1370 extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
1371 extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose );
1372 extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
1373 extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
1374 extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );
1375 extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut );
1376 extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
1377 extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
1378 extern void Gia_ManEquivImprove( Gia_Man_t * p );
1379 extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
1380 extern int Gia_ManCountChoiceNodes( Gia_Man_t * p );
1381 extern int Gia_ManCountChoices( Gia_Man_t * p );
1382 extern int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB );
1383 extern int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 );
1384 extern void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers );
1385 /*=== giaExist.c =========================================================*/
1386 extern void Gia_ManQuantSetSuppStart( Gia_Man_t * p );
1387 extern void Gia_ManQuantSetSuppZero( Gia_Man_t * p );
1388 extern void Gia_ManQuantSetSuppCi( Gia_Man_t * p, Gia_Obj_t * pObj );
1389 extern void Gia_ManQuantUpdateCiSupp( Gia_Man_t * p, int iObj );
1390 extern int Gia_ManQuantExist( Gia_Man_t * p, int iLit, int(*pFuncCiToKeep)(void *, int), void * pData );
1391 /*=== giaFanout.c =========================================================*/
1392 extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
1393 extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
1394 extern void Gia_ManFanoutStart( Gia_Man_t * p );
1395 extern void Gia_ManFanoutStop( Gia_Man_t * p );
1396 extern void Gia_ManStaticFanoutStart( Gia_Man_t * p );
1397 extern void Gia_ManStaticFanoutStop( Gia_Man_t * p );
1398 /*=== giaForce.c =========================================================*/
1399 extern void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose );
1400 /*=== giaFrames.c =========================================================*/
1401 extern Gia_Man_t * Gia_ManUnrollDup( Gia_Man_t * p, Vec_Int_t * vLimit );
1402 extern Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames );
1403 extern void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
1404 extern void * Gia_ManUnrollAdd( void * pMan, int fMax );
1405 extern void Gia_ManUnrollStop( void * pMan );
1406 extern int Gia_ManUnrollLastLit( void * pMan );
1407 extern void Gia_ManFraSetDefaultParams( Gia_ParFra_t * p );
1408 extern Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
1409 extern Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose );
1410 /*=== giaFront.c ==========================================================*/
1411 extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p );
1412 extern void Gia_ManFrontTest( Gia_Man_t * p );
1413 /*=== giaFx.c ==========================================================*/
1414 extern Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
1415 /*=== giaHash.c ===========================================================*/
1416 extern void Gia_ManHashAlloc( Gia_Man_t * p );
1417 extern void Gia_ManHashStart( Gia_Man_t * p );
1418 extern void Gia_ManHashStop( Gia_Man_t * p );
1419 extern int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 );
1420 extern int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 );
1421 extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 );
1422 extern int Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 );
1423 extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 );
1424 extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
1425 extern int Gia_ManHashMaj( Gia_Man_t * p, int iData0, int iData1, int iData2 );
1426 extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
1427 extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
1428 extern void Gia_ManHashProfile( Gia_Man_t * p );
1429 extern int Gia_ManHashLookupInt( Gia_Man_t * p, int iLit0, int iLit1 );
1430 extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
1431 extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
1432 extern int Gia_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits );
1433 extern int Gia_ManHashDualMiter( Gia_Man_t * p, Vec_Int_t * vOuts );
1434 /*=== giaIf.c ===========================================================*/
1435 extern void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile );
1436 extern void Gia_ManPrintPackingStats( Gia_Man_t * p );
1437 extern void Gia_ManPrintLutStats( Gia_Man_t * p );
1438 extern int Gia_ManLutFaninCount( Gia_Man_t * p );
1439 extern int Gia_ManLutSizeMax( Gia_Man_t * p );
1440 extern int Gia_ManLutNum( Gia_Man_t * p );
1441 extern int Gia_ManLutLevel( Gia_Man_t * p, int ** ppLevels );
1442 extern void Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels );
1443 extern void Gia_ManSetRefsMapped( Gia_Man_t * p );
1444 extern void Gia_ManSetLutRefs( Gia_Man_t * p );
1445 extern void Gia_ManSetIfParsDefault( void * pIfPars );
1446 extern void Gia_ManMappingVerify( Gia_Man_t * p );
1447 extern void Gia_ManTransferMapping( Gia_Man_t * p, Gia_Man_t * pGia );
1448 extern void Gia_ManTransferPacking( Gia_Man_t * p, Gia_Man_t * pGia );
1449 extern void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia );
1450 extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
1451 extern Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
1452 extern Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nLutSize, int nCutNum, int nRelaxRatio, int fVerbose );
1453 extern Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p );
1454 /*=== giaJf.c ===========================================================*/
1455 extern void Jf_ManSetDefaultPars( Jf_Par_t * pPars );
1456 extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
1457 extern Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds );
1458 /*=== giaIso.c ===========================================================*/
1459 extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
1460 extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
1461 extern Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fBetterQual, int fDualOut, int fVerbose, int fVeryVerbose );
1462 /*=== giaLf.c ===========================================================*/
1463 extern void Lf_ManSetDefaultPars( Jf_Par_t * pPars );
1464 extern Gia_Man_t * Lf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
1465 extern Gia_Man_t * Gia_ManPerformLfMapping( Gia_Man_t * p, Jf_Par_t * pPars, int fNormalized );
1466 /*=== giaLogic.c ===========================================================*/
1467 extern void Gia_ManTestDistance( Gia_Man_t * p );
1468 extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
1469 /*=== giaMan.c ===========================================================*/
1470 extern Gia_Man_t * Gia_ManStart( int nObjsMax );
1471 extern void Gia_ManStop( Gia_Man_t * p );
1472 extern void Gia_ManStopP( Gia_Man_t ** p );
1473 extern double Gia_ManMemory( Gia_Man_t * p );
1474 extern void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars );
1475 extern void Gia_ManPrintStatsShort( Gia_Man_t * p );
1476 extern void Gia_ManPrintMiterStatus( Gia_Man_t * p );
1477 extern void Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose );
1478 extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
1479 extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
1480 extern void Gia_ManPrintNpnClasses( Gia_Man_t * p );
1481 extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs );
1482 /*=== giaMem.c ===========================================================*/
1483 extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
1484 extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
1485 extern char * Gia_MmFixedEntryFetch( Gia_MmFixed_t * p );
1486 extern void Gia_MmFixedEntryRecycle( Gia_MmFixed_t * p, char * pEntry );
1487 extern void Gia_MmFixedRestart( Gia_MmFixed_t * p );
1488 extern int Gia_MmFixedReadMemUsage( Gia_MmFixed_t * p );
1489 extern int Gia_MmFixedReadMaxEntriesUsed( Gia_MmFixed_t * p );
1490 extern Gia_MmFlex_t * Gia_MmFlexStart();
1491 extern void Gia_MmFlexStop( Gia_MmFlex_t * p, int fVerbose );
1492 extern char * Gia_MmFlexEntryFetch( Gia_MmFlex_t * p, int nBytes );
1493 extern void Gia_MmFlexRestart( Gia_MmFlex_t * p );
1494 extern int Gia_MmFlexReadMemUsage( Gia_MmFlex_t * p );
1495 extern Gia_MmStep_t * Gia_MmStepStart( int nSteps );
1496 extern void Gia_MmStepStop( Gia_MmStep_t * p, int fVerbose );
1497 extern char * Gia_MmStepEntryFetch( Gia_MmStep_t * p, int nBytes );
1498 extern void Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEntry, int nBytes );
1499 extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
1500 /*=== giaMf.c ===========================================================*/
1501 extern void Mf_ManSetDefaultPars( Jf_Par_t * pPars );
1502 extern Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
1503 extern void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose );
1504 /*=== giaMini.c ===========================================================*/
1505 extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName );
1506 extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
1507 extern Gia_Man_t * Gia_ManReadMiniLut( char * pFileName );
1508 extern void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName );
1509 /*=== giaMuxes.c ===========================================================*/
1510 extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
1511 extern void Gia_ManPrintMuxStats( Gia_Man_t * p );
1512 extern Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit );
1513 extern Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p, int fSkipBufs );
1514 /*=== giaPat.c ===========================================================*/
1515 extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
1516 /*=== giaRetime.c ===========================================================*/
1517 extern Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose );
1518 /*=== giaSat.c ============================================================*/
1519 extern int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax );
1520 /*=== giaScl.c ============================================================*/
1521 extern int Gia_ManSeqMarkUsed( Gia_Man_t * p );
1522 extern int Gia_ManCombMarkUsed( Gia_Man_t * p );
1523 extern Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p );
1524 extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs );
1525 extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p );
1526 extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
1527 /*=== giaShow.c ===========================================================*/
1528 extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, int fPath );
1529 /*=== giaShrink.c ===========================================================*/
1530 extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose );
1531 extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose );
1532 /*=== giaSopb.c ============================================================*/
1533 extern Gia_Man_t * Gia_ManExtractWindow( Gia_Man_t * p, int LevelMax, int nTimeWindow, int fVerbose );
1534 extern Gia_Man_t * Gia_ManPerformSopBalanceWin( Gia_Man_t * p, int LevelMax, int nTimeWindow, int nCutNum, int nRelaxRatio, int fVerbose );
1535 extern Gia_Man_t * Gia_ManPerformDsdBalanceWin( Gia_Man_t * p, int LevelMax, int nTimeWindow, int nLutSize, int nCutNum, int nRelaxRatio, int fVerbose );
1536 /*=== giaSort.c ============================================================*/
1537 extern int * Gia_SortFloats( float * pArray, int * pPerm, int nSize );
1538 /*=== giaSim.c ============================================================*/
1539 extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
1540 extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
1541 extern unsigned * Gia_SimDataExt( Gia_ManSim_t * p, int i );
1542 extern unsigned * Gia_SimDataCiExt( Gia_ManSim_t * p, int i );
1543 extern unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i );
1544 extern void Gia_ManSimInfoInit( Gia_ManSim_t * p );
1545 extern void Gia_ManSimInfoTransfer( Gia_ManSim_t * p );
1546 extern void Gia_ManSimulateRound( Gia_ManSim_t * p );
1547 extern void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs );
1548 extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj );
1549 extern int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 );
1550 extern int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
1551 extern void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 );
1552 extern void Gia_ManBuiltInSimResimulate( Gia_Man_t * p );
1553 extern int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat );
1554 extern void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs );
1555 extern void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits );
1556 extern int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 );
1557 extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
1558 /*=== giaSpeedup.c ============================================================*/
1559 extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
1560 extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
1561 extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
1562 /*=== giaSplit.c ============================================================*/
1563 extern void Gia_ManComputeOneWinStart( Gia_Man_t * p, int nAnds, int fReverse );
1564 extern int Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds );
1565 /*=== giaStg.c ============================================================*/
1566 extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates );
1567 extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose );
1568 /*=== giaSupp.c ============================================================*/
1569 typedef struct Gia_ManMin_t_ Gia_ManMin_t;
1570 extern Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia );
1571 extern void Gia_ManSuppStop( Gia_ManMin_t * p );
1572 extern int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 );
1573 typedef struct Gia_Man2Min_t_ Gia_Man2Min_t;
1574 extern Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia );
1575 extern void Gia_Man2SuppStop( Gia_Man2Min_t * p );
1576 extern int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 );
1577 /*=== giaSweep.c ============================================================*/
1578 extern Gia_Man_t * Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars );
1579 extern Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs );
1580 extern void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p );
1581 /*=== giaSweeper.c ============================================================*/
1582 extern Gia_Man_t * Gia_SweeperStart( Gia_Man_t * p );
1583 extern void Gia_SweeperStop( Gia_Man_t * p );
1584 extern int Gia_SweeperIsRunning( Gia_Man_t * p );
1585 extern void Gia_SweeperPrintStats( Gia_Man_t * p );
1586 extern void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax );
1587 extern void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds );
1588 extern Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p );
1589 extern int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
1590 extern int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
1591 extern int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew );
1592 extern int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId );
1593 extern Vec_Int_t * Gia_SweeperCollectValidProbeIds( Gia_Man_t * p );
1594 extern int Gia_SweeperCondPop( Gia_Man_t * p );
1595 extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId );
1596 extern Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p );
1597 extern int Gia_SweeperCondCheckUnsat( Gia_Man_t * p );
1598 extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, int ProbeId2 );
1599 extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames );
1600 extern void Gia_SweeperLogicDump( Gia_Man_t * p, Vec_Int_t * vProbeIds, int fDumpConds, char * pFileName );
1601 extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime );
1602 extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc );
1603 extern int Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerify, int fVerbose );
1604 extern int Gia_SweeperRun( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int fVerbose );
1605 /*=== giaSwitch.c ============================================================*/
1606 extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
1607 extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
1608 extern Vec_Int_t * Gia_ManComputeSwitchProbs( Gia_Man_t * pGia, int nFrames, int nPref, int fProbOne );
1609 extern Vec_Flt_t * Gia_ManPrintOutputProb( Gia_Man_t * p );
1610 /*=== giaTim.c ===========================================================*/
1611 extern int Gia_ManBoxNum( Gia_Man_t * p );
1612 extern int Gia_ManRegBoxNum( Gia_Man_t * p );
1613 extern int Gia_ManNonRegBoxNum( Gia_Man_t * p );
1614 extern int Gia_ManBlackBoxNum( Gia_Man_t * p );
1615 extern int Gia_ManBoxCiNum( Gia_Man_t * p );
1616 extern int Gia_ManBoxCoNum( Gia_Man_t * p );
1617 extern int Gia_ManClockDomainNum( Gia_Man_t * p );
1618 extern int Gia_ManIsSeqWithBoxes( Gia_Man_t * p );
1619 extern int Gia_ManIsNormalized( Gia_Man_t * p );
1620 extern Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p );
1621 extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p, int fHashMapping );
1622 extern Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p );
1623 extern Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p );
1624 extern int Gia_ManLevelWithBoxes( Gia_Man_t * p );
1625 extern int Gia_ManLutLevelWithBoxes( Gia_Man_t * p );
1626 extern void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
1627 extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff );
1628 extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
1629 extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft );
1630 extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq );
1631 extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec );
1632 /*=== giaTruth.c ===========================================================*/
1633 extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths );
1634 extern word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp );
1635 extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
1636 extern word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp );
1637 extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
1638 extern word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
1639 extern void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax );
1640 extern void Gia_ObjComputeTruthTableStop( Gia_Man_t * p );
1641 extern word * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves );
1642 /*=== giaTsim.c ============================================================*/
1643 extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
1644 /*=== giaUtil.c ===========================================================*/
1645 extern unsigned Gia_ManRandom( int fReset );
1646 extern word Gia_ManRandomW( int fReset );
1647 extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
1648 extern char * Gia_TimeStamp();
1649 extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
1650 extern void Gia_ManIncrementTravId( Gia_Man_t * p );
1651 extern void Gia_ManCleanMark01( Gia_Man_t * p );
1652 extern void Gia_ManSetMark0( Gia_Man_t * p );
1653 extern void Gia_ManCleanMark0( Gia_Man_t * p );
1654 extern void Gia_ManCheckMark0( Gia_Man_t * p );
1655 extern void Gia_ManSetMark1( Gia_Man_t * p );
1656 extern void Gia_ManCleanMark1( Gia_Man_t * p );
1657 extern void Gia_ManCheckMark1( Gia_Man_t * p );
1658 extern void Gia_ManCleanValue( Gia_Man_t * p );
1659 extern void Gia_ManCleanLevels( Gia_Man_t * p, int Size );
1660 extern void Gia_ManCleanTruth( Gia_Man_t * p );
1661 extern void Gia_ManFillValue( Gia_Man_t * p );
1662 extern void Gia_ObjSetPhase( Gia_Man_t * p, Gia_Obj_t * pObj );
1663 extern void Gia_ManSetPhase( Gia_Man_t * p );
1664 extern void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues );
1665 extern void Gia_ManSetPhase1( Gia_Man_t * p );
1666 extern void Gia_ManCleanPhase( Gia_Man_t * p );
1667 extern int Gia_ManCheckCoPhase( Gia_Man_t * p );
1668 extern int Gia_ManLevelNum( Gia_Man_t * p );
1669 extern Vec_Int_t * Gia_ManGetCiLevels( Gia_Man_t * p );
1670 extern int Gia_ManSetLevels( Gia_Man_t * p, Vec_Int_t * vCiLevels );
1671 extern Vec_Int_t * Gia_ManReverseLevel( Gia_Man_t * p );
1672 extern Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p );
1673 extern void Gia_ManCreateValueRefs( Gia_Man_t * p );
1674 extern void Gia_ManCreateRefs( Gia_Man_t * p );
1675 extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p );
1676 extern int Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
1677 extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
1678 extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode );
1679 extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
1680 extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
1681 extern int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE );
1682 extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
1683 extern int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp );
1684 extern int Gia_ManHasDangling( Gia_Man_t * p );
1685 extern int Gia_ManMarkDangling( Gia_Man_t * p );
1686 extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
1687 extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
1688 extern void Gia_ManPrint( Gia_Man_t * p );
1689 extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
1690 extern void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes );
1691 extern void Gia_ManPrintConeMulti( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
1692 extern void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj );
1693 extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
1694 extern void Gia_ManInvertPos( Gia_Man_t * pAig );
1695 extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
1696 extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
1697 extern void Gia_ManSwapPos( Gia_Man_t * p, int i );
1698 extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p );
1699 extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
1700 extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p );
1701 extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 );
1702 extern int Gia_ManCountPisWithFanout( Gia_Man_t * p );
1703 extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
1704 extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
1705
1706 /*=== giaCTas.c ===========================================================*/
1707 typedef struct Tas_Man_t_ Tas_Man_t;
1708 extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
1709 extern void Tas_ManStop( Tas_Man_t * p );
1710 extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
1711 extern void Tas_ManSatPrintStats( Tas_Man_t * p );
1712 extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
1713 extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
1714
1715
1716 ABC_NAMESPACE_HEADER_END
1717
1718
1719 #endif
1720
1721 ////////////////////////////////////////////////////////////////////////
1722 /// END OF FILE ///
1723 ////////////////////////////////////////////////////////////////////////
1724
1725