1 /**CFile****************************************************************
2
3 FileName [aig.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [AIG package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - April 28, 2007.]
16
17 Revision [$Id: aig.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__aig__aig_h
22 #define ABC__aig__aig__aig_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/util/utilCex.h"
36
37 ////////////////////////////////////////////////////////////////////////
38 /// PARAMETERS ///
39 ////////////////////////////////////////////////////////////////////////
40
41
42
43 ABC_NAMESPACE_HEADER_START
44
45
46 ////////////////////////////////////////////////////////////////////////
47 /// BASIC TYPES ///
48 ////////////////////////////////////////////////////////////////////////
49
50 typedef struct Aig_Man_t_ Aig_Man_t;
51 typedef struct Aig_Obj_t_ Aig_Obj_t;
52 typedef struct Aig_MmFixed_t_ Aig_MmFixed_t;
53 typedef struct Aig_MmFlex_t_ Aig_MmFlex_t;
54 typedef struct Aig_MmStep_t_ Aig_MmStep_t;
55
56 // object types
57 typedef enum {
58 AIG_OBJ_NONE, // 0: non-existent object
59 AIG_OBJ_CONST1, // 1: constant 1
60 AIG_OBJ_CI, // 2: combinational input
61 AIG_OBJ_CO, // 3: combinational output
62 AIG_OBJ_BUF, // 4: buffer node
63 AIG_OBJ_AND, // 5: AND node
64 AIG_OBJ_EXOR, // 6: EXOR node
65 AIG_OBJ_VOID // 7: unused object
66 } Aig_Type_t;
67
68 // the AIG node
69 struct Aig_Obj_t_ // 8 words
70 {
71 union {
72 Aig_Obj_t * pNext; // strashing table
73 int CioId; // 0-based number of CI/CO
74 };
75 Aig_Obj_t * pFanin0; // fanin
76 Aig_Obj_t * pFanin1; // fanin
77 unsigned int Type : 3; // object type
78 unsigned int fPhase : 1; // value under 000...0 pattern
79 unsigned int fMarkA : 1; // multipurpose mask
80 unsigned int fMarkB : 1; // multipurpose mask
81 unsigned int nRefs : 26; // reference count
82 unsigned Level : 24; // the level of this node
83 unsigned nCuts : 8; // the number of cuts
84 int TravId; // unique ID of last traversal involving the node
85 int Id; // unique ID of the node
86 union { // temporary store for user's data
87 void * pData;
88 int iData;
89 float dData;
90 };
91 };
92
93 // the AIG manager
94 struct Aig_Man_t_
95 {
96 char * pName; // the design name
97 char * pSpec; // the input file name
98 // AIG nodes
99 Vec_Ptr_t * vCis; // the array of PIs
100 Vec_Ptr_t * vCos; // the array of POs
101 Vec_Ptr_t * vObjs; // the array of all nodes (optional)
102 Vec_Ptr_t * vBufs; // the array of buffers
103 Aig_Obj_t * pConst1; // the constant 1 node
104 Aig_Obj_t Ghost; // the ghost node
105 int nRegs; // the number of registers (registers are last POs)
106 int nTruePis; // the number of true primary inputs
107 int nTruePos; // the number of true primary outputs
108 int nAsserts; // the number of asserts among POs (asserts are first POs)
109 int nConstrs; // the number of constraints (model checking only)
110 int nBarBufs; // the number of barrier buffers
111 // AIG node counters
112 int nObjs[AIG_OBJ_VOID];// the number of objects by type
113 int nDeleted; // the number of deleted objects
114 // structural hash table
115 Aig_Obj_t ** pTable; // structural hash table
116 int nTableSize; // structural hash table size
117 // representation of fanouts
118 int * pFanData; // the database to store fanout information
119 int nFansAlloc; // the size of fanout representation
120 Vec_Vec_t * vLevels; // used to update timing information
121 int nBufReplaces; // the number of times replacement led to a buffer
122 int nBufFixes; // the number of times buffers were propagated
123 int nBufMax; // the maximum number of buffers during computation
124 // topological order
125 unsigned * pOrderData;
126 int nOrderAlloc;
127 int iPrev;
128 int iNext;
129 int nAndTotal;
130 int nAndPrev;
131 // representatives
132 Aig_Obj_t ** pEquivs; // linked list of equivalent nodes (when choices are used)
133 Aig_Obj_t ** pReprs; // representatives of each node
134 int nReprsAlloc; // the number of allocated representatives
135 // various data members
136 Aig_MmFixed_t * pMemObjs; // memory manager for objects
137 Vec_Int_t * vLevelR; // the reverse level of the nodes
138 int nLevelMax; // maximum number of levels
139 void * pData; // the temporary data
140 void * pData2; // the temporary data
141 int nTravIds; // the current traversal ID
142 int fCatchExor; // enables EXOR nodes
143 int fAddStrash; // performs additional strashing
144 Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes
145 void (*pImpFunc) (void*, void*); // implication checking precedure
146 void * pImpData; // implication checking data
147 void * pManTime; // the timing manager
148 void * pManCuts;
149 int * pFastSim;
150 unsigned * pTerSimData; // ternary simulation data
151 Vec_Ptr_t * vMapped;
152 Vec_Int_t * vFlopNums;
153 Vec_Int_t * vFlopReprs;
154 Abc_Cex_t * pSeqModel;
155 Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
156 Aig_Man_t * pManExdc;
157 Vec_Ptr_t * vOnehots;
158 int fCreatePios;
159 Vec_Int_t * vEquPairs;
160 Vec_Vec_t * vClockDoms;
161 Vec_Int_t * vProbs; // probability of node being 1
162 Vec_Int_t * vCiNumsOrig; // original CI names
163 int nComplEdges; // complemented edges
164 abctime Time2Quit;
165 // timing statistics
166 abctime time1;
167 abctime time2;
168 //-- jlong -- begin
169 Vec_Ptr_t * unfold2_type_I;
170 Vec_Ptr_t * unfold2_type_II;
171 //-- jlong -- end
172 };
173
174 // cut computation
175 typedef struct Aig_ManCut_t_ Aig_ManCut_t;
176 typedef struct Aig_Cut_t_ Aig_Cut_t;
177
178 // the cut used to represent node in the AIG
179 struct Aig_Cut_t_
180 {
181 Aig_Cut_t * pNext; // the next cut in the table
182 int Cost; // the cost of the cut
183 unsigned uSign; // cut signature
184 int iNode; // the node, for which it is the cut
185 short nCutSize; // the number of bytes in the cut
186 char nLeafMax; // the maximum number of fanins
187 char nFanins; // the current number of fanins
188 int pFanins[0]; // the fanins (followed by the truth table)
189 };
190
191 // the CNF computation manager
192 struct Aig_ManCut_t_
193 {
194 // AIG manager
195 Aig_Man_t * pAig; // the input AIG manager
196 Aig_Cut_t ** pCuts; // the cuts for each node in the output manager
197 // parameters
198 int nCutsMax; // the max number of cuts at the node
199 int nLeafMax; // the max number of leaves of a cut
200 int fTruth; // enables truth table computation
201 int fVerbose; // enables verbose output
202 // internal variables
203 int nCutSize; // the number of bytes needed to store one cut
204 int nTruthWords; // the number of truth table words
205 Aig_MmFixed_t * pMemCuts; // memory manager for cuts
206 unsigned * puTemp[4]; // used for the truth table computation
207 };
208
Aig_ObjCuts(Aig_ManCut_t * p,Aig_Obj_t * pObj)209 static inline Aig_Cut_t * Aig_ObjCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; }
Aig_ObjSetCuts(Aig_ManCut_t * p,Aig_Obj_t * pObj,Aig_Cut_t * pCuts)210 static inline void Aig_ObjSetCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; }
211
Aig_CutLeaveNum(Aig_Cut_t * pCut)212 static inline int Aig_CutLeaveNum( Aig_Cut_t * pCut ) { return pCut->nFanins; }
Aig_CutLeaves(Aig_Cut_t * pCut)213 static inline int * Aig_CutLeaves( Aig_Cut_t * pCut ) { return pCut->pFanins; }
Aig_CutTruth(Aig_Cut_t * pCut)214 static inline unsigned * Aig_CutTruth( Aig_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); }
Aig_CutNext(Aig_Cut_t * pCut)215 static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return (Aig_Cut_t *)(((char *)pCut) + pCut->nCutSize); }
216
217 // iterator over cuts of the node
218 #define Aig_ObjForEachCut( p, pObj, pCut, i ) \
219 for ( i = 0, pCut = Aig_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Aig_CutNext(pCut) )
220 // iterator over leaves of the cut
221 #define Aig_CutForEachLeaf( p, pCut, pLeaf, i ) \
222 for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
223
224 ////////////////////////////////////////////////////////////////////////
225 /// MACRO DEFINITIONS ///
226 ////////////////////////////////////////////////////////////////////////
227
Aig_ObjCutSign(unsigned ObjId)228 static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
Aig_WordCountOnes(unsigned uWord)229 static inline int Aig_WordCountOnes( unsigned uWord )
230 {
231 uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
232 uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
233 uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
234 uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
235 return (uWord & 0x0000FFFF) + (uWord>>16);
236 }
Aig_WordFindFirstBit(unsigned uWord)237 static inline int Aig_WordFindFirstBit( unsigned uWord )
238 {
239 int i;
240 for ( i = 0; i < 32; i++ )
241 if ( uWord & (1 << i) )
242 return i;
243 return -1;
244 }
245
Aig_Regular(Aig_Obj_t * p)246 static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
Aig_Not(Aig_Obj_t * p)247 static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
Aig_NotCond(Aig_Obj_t * p,int c)248 static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
Aig_IsComplement(Aig_Obj_t * p)249 static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
250
Aig_ManCiNum(Aig_Man_t * p)251 static inline int Aig_ManCiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_CI]; }
Aig_ManCoNum(Aig_Man_t * p)252 static inline int Aig_ManCoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_CO]; }
Aig_ManBufNum(Aig_Man_t * p)253 static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
Aig_ManAndNum(Aig_Man_t * p)254 static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
Aig_ManExorNum(Aig_Man_t * p)255 static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
Aig_ManNodeNum(Aig_Man_t * p)256 static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
Aig_ManGetCost(Aig_Man_t * p)257 static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
Aig_ManObjNum(Aig_Man_t * p)258 static inline int Aig_ManObjNum( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs) - p->nDeleted; }
Aig_ManObjNumMax(Aig_Man_t * p)259 static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
Aig_ManRegNum(Aig_Man_t * p)260 static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
Aig_ManConstrNum(Aig_Man_t * p)261 static inline int Aig_ManConstrNum( Aig_Man_t * p ) { return p->nConstrs; }
262
Aig_ManConst0(Aig_Man_t * p)263 static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
Aig_ManConst1(Aig_Man_t * p)264 static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
Aig_ManGhost(Aig_Man_t * p)265 static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
Aig_ManCi(Aig_Man_t * p,int i)266 static inline Aig_Obj_t * Aig_ManCi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i); }
Aig_ManCo(Aig_Man_t * p,int i)267 static inline Aig_Obj_t * Aig_ManCo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i); }
Aig_ManLo(Aig_Man_t * p,int i)268 static inline Aig_Obj_t * Aig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i); }
Aig_ManLi(Aig_Man_t * p,int i)269 static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i); }
Aig_ManObj(Aig_Man_t * p,int i)270 static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
271
Aig_ObjType(Aig_Obj_t * pObj)272 static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; }
Aig_ObjIsNone(Aig_Obj_t * pObj)273 static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; }
Aig_ObjIsConst1(Aig_Obj_t * pObj)274 static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
Aig_ObjIsCi(Aig_Obj_t * pObj)275 static inline int Aig_ObjIsCi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI; }
Aig_ObjIsCo(Aig_Obj_t * pObj)276 static inline int Aig_ObjIsCo( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CO; }
Aig_ObjIsBuf(Aig_Obj_t * pObj)277 static inline int Aig_ObjIsBuf( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_BUF; }
Aig_ObjIsAnd(Aig_Obj_t * pObj)278 static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND; }
Aig_ObjIsExor(Aig_Obj_t * pObj)279 static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; }
Aig_ObjIsNode(Aig_Obj_t * pObj)280 static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
Aig_ObjIsTerm(Aig_Obj_t * pObj)281 static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI || pObj->Type == AIG_OBJ_CO || pObj->Type == AIG_OBJ_CONST1; }
Aig_ObjIsHash(Aig_Obj_t * pObj)282 static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
Aig_ObjIsChoice(Aig_Man_t * p,Aig_Obj_t * pObj)283 static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; }
Aig_ObjIsCand(Aig_Obj_t * pObj)284 static inline int Aig_ObjIsCand( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI || pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
Aig_ObjCioId(Aig_Obj_t * pObj)285 static inline int Aig_ObjCioId( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return pObj->CioId; }
Aig_ObjId(Aig_Obj_t * pObj)286 static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; }
287
Aig_ObjIsMarkA(Aig_Obj_t * pObj)288 static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; }
Aig_ObjSetMarkA(Aig_Obj_t * pObj)289 static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; }
Aig_ObjClearMarkA(Aig_Obj_t * pObj)290 static inline void Aig_ObjClearMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 0; }
291
Aig_ObjSetTravId(Aig_Obj_t * pObj,int TravId)292 static inline void Aig_ObjSetTravId( Aig_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; }
Aig_ObjSetTravIdCurrent(Aig_Man_t * p,Aig_Obj_t * pObj)293 static inline void Aig_ObjSetTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj ) { pObj->TravId = p->nTravIds; }
Aig_ObjSetTravIdPrevious(Aig_Man_t * p,Aig_Obj_t * pObj)294 static inline void Aig_ObjSetTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; }
Aig_ObjIsTravIdCurrent(Aig_Man_t * p,Aig_Obj_t * pObj)295 static inline int Aig_ObjIsTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds); }
Aig_ObjIsTravIdPrevious(Aig_Man_t * p,Aig_Obj_t * pObj)296 static inline int Aig_ObjIsTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds - 1); }
297
Aig_ObjPhase(Aig_Obj_t * pObj)298 static inline int Aig_ObjPhase( Aig_Obj_t * pObj ) { return pObj->fPhase; }
Aig_ObjPhaseReal(Aig_Obj_t * pObj)299 static inline int Aig_ObjPhaseReal( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 1; }
Aig_ObjRefs(Aig_Obj_t * pObj)300 static inline int Aig_ObjRefs( Aig_Obj_t * pObj ) { return pObj->nRefs; }
Aig_ObjRef(Aig_Obj_t * pObj)301 static inline void Aig_ObjRef( Aig_Obj_t * pObj ) { pObj->nRefs++; }
Aig_ObjDeref(Aig_Obj_t * pObj)302 static inline void Aig_ObjDeref( Aig_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; }
Aig_ObjClearRef(Aig_Obj_t * pObj)303 static inline void Aig_ObjClearRef( Aig_Obj_t * pObj ) { pObj->nRefs = 0; }
Aig_ObjFaninId0(Aig_Obj_t * pObj)304 static inline int Aig_ObjFaninId0( Aig_Obj_t * pObj ) { return pObj->pFanin0? Aig_Regular(pObj->pFanin0)->Id : -1; }
Aig_ObjFaninId1(Aig_Obj_t * pObj)305 static inline int Aig_ObjFaninId1( Aig_Obj_t * pObj ) { return pObj->pFanin1? Aig_Regular(pObj->pFanin1)->Id : -1; }
Aig_ObjFaninC0(Aig_Obj_t * pObj)306 static inline int Aig_ObjFaninC0( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin0); }
Aig_ObjFaninC1(Aig_Obj_t * pObj)307 static inline int Aig_ObjFaninC1( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin1); }
Aig_ObjFanin0(Aig_Obj_t * pObj)308 static inline Aig_Obj_t * Aig_ObjFanin0( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin0); }
Aig_ObjFanin1(Aig_Obj_t * pObj)309 static inline Aig_Obj_t * Aig_ObjFanin1( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin1); }
Aig_ObjChild0(Aig_Obj_t * pObj)310 static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj->pFanin0; }
Aig_ObjChild1(Aig_Obj_t * pObj)311 static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; }
Aig_ObjChild0Copy(Aig_Obj_t * pObj)312 static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
Aig_ObjChild1Copy(Aig_Obj_t * pObj)313 static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
Aig_ObjChild0Next(Aig_Obj_t * pObj)314 static inline Aig_Obj_t * Aig_ObjChild0Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pNext, Aig_ObjFaninC0(pObj)) : NULL; }
Aig_ObjChild1Next(Aig_Obj_t * pObj)315 static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pNext, Aig_ObjFaninC1(pObj)) : NULL; }
Aig_ObjChild0Flip(Aig_Obj_t * pObj)316 static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); }
Aig_ObjChild1Flip(Aig_Obj_t * pObj)317 static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); }
Aig_ObjCopy(Aig_Obj_t * pObj)318 static inline Aig_Obj_t * Aig_ObjCopy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return (Aig_Obj_t *)pObj->pData; }
Aig_ObjSetCopy(Aig_Obj_t * pObj,Aig_Obj_t * pCopy)319 static inline void Aig_ObjSetCopy( Aig_Obj_t * pObj, Aig_Obj_t * pCopy ) { assert( !Aig_IsComplement(pObj) ); pObj->pData = pCopy; }
Aig_ObjRealCopy(Aig_Obj_t * pObj)320 static inline Aig_Obj_t * Aig_ObjRealCopy( Aig_Obj_t * pObj ) { return Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj));}
Aig_ObjToLit(Aig_Obj_t * pObj)321 static inline int Aig_ObjToLit( Aig_Obj_t * pObj ) { return Abc_Var2Lit( Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj) ); }
Aig_ObjFromLit(Aig_Man_t * p,int iLit)322 static inline Aig_Obj_t * Aig_ObjFromLit( Aig_Man_t * p,int iLit){ return Aig_NotCond( Aig_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
Aig_ObjLevel(Aig_Obj_t * pObj)323 static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; }
Aig_ObjLevelNew(Aig_Obj_t * pObj)324 static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + Abc_MaxInt(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
Aig_ObjSetLevel(Aig_Obj_t * pObj,int i)325 static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i; }
Aig_ObjClean(Aig_Obj_t * pObj)326 static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
Aig_ObjFanout0(Aig_Man_t * p,Aig_Obj_t * pObj)327 static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
Aig_ObjEquiv(Aig_Man_t * p,Aig_Obj_t * pObj)328 static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; }
Aig_ObjSetEquiv(Aig_Man_t * p,Aig_Obj_t * pObj,Aig_Obj_t * pEqu)329 static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEqu ) { assert(p->pEquivs); p->pEquivs[pObj->Id] = pEqu; }
Aig_ObjRepr(Aig_Man_t * p,Aig_Obj_t * pObj)330 static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; }
Aig_ObjSetRepr(Aig_Man_t * p,Aig_Obj_t * pObj,Aig_Obj_t * pRepr)331 static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; }
Aig_ObjWhatFanin(Aig_Obj_t * pObj,Aig_Obj_t * pFanin)332 static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
333 {
334 if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
335 if ( Aig_ObjFanin1(pObj) == pFanin ) return 1;
336 assert(0); return -1;
337 }
Aig_ObjFanoutC(Aig_Obj_t * pObj,Aig_Obj_t * pFanout)338 static inline int Aig_ObjFanoutC( Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
339 {
340 if ( Aig_ObjFanin0(pFanout) == pObj ) return Aig_ObjFaninC0(pObj);
341 if ( Aig_ObjFanin1(pFanout) == pObj ) return Aig_ObjFaninC1(pObj);
342 assert(0); return -1;
343 }
344
345 // create the ghost of the new node
Aig_ObjCreateGhost(Aig_Man_t * p,Aig_Obj_t * p0,Aig_Obj_t * p1,Aig_Type_t Type)346 static inline Aig_Obj_t * Aig_ObjCreateGhost( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type )
347 {
348 Aig_Obj_t * pGhost;
349 assert( Type != AIG_OBJ_AND || !Aig_ObjIsConst1(Aig_Regular(p0)) );
350 assert( p1 == NULL || !Aig_ObjIsConst1(Aig_Regular(p1)) );
351 assert( Type == AIG_OBJ_CI || Aig_Regular(p0) != Aig_Regular(p1) );
352 pGhost = Aig_ManGhost(p);
353 pGhost->Type = Type;
354 if ( p1 == NULL || Aig_Regular(p0)->Id < Aig_Regular(p1)->Id )
355 {
356 pGhost->pFanin0 = p0;
357 pGhost->pFanin1 = p1;
358 }
359 else
360 {
361 pGhost->pFanin0 = p1;
362 pGhost->pFanin1 = p0;
363 }
364 return pGhost;
365 }
366
367 // internal memory manager
Aig_ManFetchMemory(Aig_Man_t * p)368 static inline Aig_Obj_t * Aig_ManFetchMemory( Aig_Man_t * p )
369 {
370 extern char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p );
371 Aig_Obj_t * pTemp;
372 pTemp = (Aig_Obj_t *)Aig_MmFixedEntryFetch( p->pMemObjs );
373 memset( pTemp, 0, sizeof(Aig_Obj_t) );
374 pTemp->Id = Vec_PtrSize(p->vObjs);
375 Vec_PtrPush( p->vObjs, pTemp );
376 return pTemp;
377 }
Aig_ManRecycleMemory(Aig_Man_t * p,Aig_Obj_t * pEntry)378 static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
379 {
380 extern void Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry );
381 assert( pEntry->nRefs == 0 );
382 pEntry->Type = AIG_OBJ_NONE; // distinquishes a dead node from a live node
383 Aig_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
384 p->nDeleted++;
385 }
386
387
388 ////////////////////////////////////////////////////////////////////////
389 /// ITERATORS ///
390 ////////////////////////////////////////////////////////////////////////
391
392 // iterator over the combinational inputs
393 #define Aig_ManForEachCi( p, pObj, i ) \
394 Vec_PtrForEachEntry( Aig_Obj_t *, p->vCis, pObj, i )
395 #define Aig_ManForEachCiReverse( p, pObj, i ) \
396 Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vCis, pObj, i )
397 // iterator over the combinational outputs
398 #define Aig_ManForEachCo( p, pObj, i ) \
399 Vec_PtrForEachEntry( Aig_Obj_t *, p->vCos, pObj, i )
400 #define Aig_ManForEachCoReverse( p, pObj, i ) \
401 Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vCos, pObj, i )
402 // iterators over all objects, including those currently not used
403 #define Aig_ManForEachObj( p, pObj, i ) \
404 Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
405 #define Aig_ManForEachObjReverse( p, pObj, i ) \
406 Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
407 // iterators over the objects whose IDs are stored in an array
408 #define Aig_ManForEachObjVec( vIds, p, pObj, i ) \
409 for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
410 #define Aig_ManForEachObjVecReverse( vIds, p, pObj, i ) \
411 for ( i = Vec_IntSize(vIds) - 1; i >= 0 && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i-- )
412 // iterators over all nodes
413 #define Aig_ManForEachNode( p, pObj, i ) \
414 Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
415 #define Aig_ManForEachNodeReverse( p, pObj, i ) \
416 Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
417 // iterator over all nodes
418 #define Aig_ManForEachExor( p, pObj, i ) \
419 Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
420 #define Aig_ManForEachExorReverse( p, pObj, i ) \
421 Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
422
423 // these two procedures are only here for the use inside the iterator
Aig_ObjFanout0Int(Aig_Man_t * p,int ObjId)424 static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; }
Aig_ObjFanoutNext(Aig_Man_t * p,int iFan)425 static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iFan/2 < p->nFansAlloc); return p->pFanData[5*(iFan >> 1) + 3 + (iFan & 1)]; }
426 // iterator over the fanouts
427 #define Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) \
428 for ( assert(p->pFanData), i = 0; (i < (int)(pObj)->nRefs) && \
429 (((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \
430 (((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ )
431
432
433 ////////////////////////////////////////////////////////////////////////
434 /// SEQUENTIAL ITERATORS ///
435 ////////////////////////////////////////////////////////////////////////
436
437 // iterator over the primary inputs
438 #define Aig_ManForEachPiSeq( p, pObj, i ) \
439 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
440 // iterator over the latch outputs
441 #define Aig_ManForEachLoSeq( p, pObj, i ) \
442 Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vCis, pObj, i, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
443 // iterator over the primary outputs
444 #define Aig_ManForEachPoSeq( p, pObj, i ) \
445 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Aig_ManCoNum(p)-Aig_ManRegNum(p) )
446 // iterator over the latch inputs
447 #define Aig_ManForEachLiSeq( p, pObj, i ) \
448 Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vCos, pObj, i, Aig_ManCoNum(p)-Aig_ManRegNum(p) )
449 // iterator over the latch input and outputs
450 #define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k ) \
451 for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1) \
452 && (((pObjLo)=Aig_ManLo(p, k)), 1); k++ )
453
454 ////////////////////////////////////////////////////////////////////////
455 /// FUNCTION DECLARATIONS ///
456 ////////////////////////////////////////////////////////////////////////
457
458 /*=== aigCheck.c ========================================================*/
459 extern ABC_DLL int Aig_ManCheck( Aig_Man_t * p );
460 extern void Aig_ManCheckMarkA( Aig_Man_t * p );
461 extern void Aig_ManCheckPhase( Aig_Man_t * p );
462 /*=== aigCuts.c ========================================================*/
463 extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
464 extern void Aig_ManCutStop( Aig_ManCut_t * p );
465 /*=== aigDfs.c ==========================================================*/
466 extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p );
467 extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly );
468 extern Vec_Ptr_t * Aig_ManDfsAll( Aig_Man_t * p );
469 extern Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly );
470 extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
471 extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
472 extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
473 extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p );
474 extern int Aig_ManLevelNum( Aig_Man_t * p );
475 extern int Aig_ManChoiceLevel( Aig_Man_t * p );
476 extern int Aig_DagSize( Aig_Obj_t * pObj );
477 extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
478 extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
479 extern void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp );
480 extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
481 extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
482 extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
483 extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
484 extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
485 /*=== aigDup.c ==========================================================*/
486 extern Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
487 extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
488 extern Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints );
489 extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
490 extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vCos );
491 extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
492 extern Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value );
493 extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p );
494 extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
495 extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
496 extern Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder );
497 extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios );
498 extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p );
499 extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
500 extern Aig_Man_t * Aig_ManDupFlopsOnly( Aig_Man_t * p );
501 extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
502 extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p );
503 extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
504 extern Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
505 extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
506 extern Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
507 extern Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray );
508 extern Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * pMan, Vec_Ptr_t * vArray );
509 /*=== aigFanout.c ==========================================================*/
510 extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
511 extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
512 extern void Aig_ManFanoutStart( Aig_Man_t * p );
513 extern void Aig_ManFanoutStop( Aig_Man_t * p );
514 /*=== aigFrames.c ==========================================================*/
515 extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap );
516 /*=== aigMan.c ==========================================================*/
517 extern Aig_Man_t * Aig_ManStart( int nNodesMax );
518 extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
519 extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
520 extern void Aig_ManStop( Aig_Man_t * p );
521 extern void Aig_ManStopP( Aig_Man_t ** p );
522 extern int Aig_ManCleanup( Aig_Man_t * p );
523 extern int Aig_ManAntiCleanup( Aig_Man_t * p );
524 extern int Aig_ManCiCleanup( Aig_Man_t * p );
525 extern int Aig_ManCoCleanup( Aig_Man_t * p );
526 extern void Aig_ManPrintStats( Aig_Man_t * p );
527 extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
528 extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
529 extern void Aig_ManFlipFirstPo( Aig_Man_t * p );
530 extern void * Aig_ManReleaseData( Aig_Man_t * p );
531 /*=== aigMem.c ==========================================================*/
532 extern void Aig_ManStartMemory( Aig_Man_t * p );
533 extern void Aig_ManStopMemory( Aig_Man_t * p );
534 /*=== aigMffc.c ==========================================================*/
535 extern int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
536 extern int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin, float * pPower, float * pProbs );
537 extern int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
538 extern int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower );
539 extern int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
540 extern int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
541 /*=== aigObj.c ==========================================================*/
542 extern Aig_Obj_t * Aig_ObjCreateCi( Aig_Man_t * p );
543 extern Aig_Obj_t * Aig_ObjCreateCo( Aig_Man_t * p, Aig_Obj_t * pDriver );
544 extern Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost );
545 extern void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj_t * pFan1 );
546 extern void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
547 extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
548 extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
549 extern void Aig_ObjDeletePo( Aig_Man_t * p, Aig_Obj_t * pObj );
550 extern void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
551 extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
552 extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel );
553 /*=== aigOper.c =========================================================*/
554 extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i );
555 extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
556 extern Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
557 extern Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
558 extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
559 extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
560 extern Aig_Obj_t * Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC );
561 extern Aig_Obj_t * Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type );
562 extern Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs );
563 extern Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 );
564 extern Aig_Obj_t * Aig_CreateAnd( Aig_Man_t * p, int nVars );
565 extern Aig_Obj_t * Aig_CreateOr( Aig_Man_t * p, int nVars );
566 extern Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars );
567 /*=== aigOrder.c =========================================================*/
568 extern void Aig_ManOrderStart( Aig_Man_t * p );
569 extern void Aig_ManOrderStop( Aig_Man_t * p );
570 extern void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId );
571 extern void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId );
572 extern void Aig_ObjOrderAdvance( Aig_Man_t * p );
573 /*=== aigPart.c =========================================================*/
574 extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p );
575 extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p );
576 extern Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p );
577 extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
578 extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
579 extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
580 extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart );
581 extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
582 extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
583 extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
584 /*=== aigPartReg.c =========================================================*/
585 extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
586 extern void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize );
587 extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
588 extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
589 extern Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
590 /*=== aigRepr.c =========================================================*/
591 extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
592 extern void Aig_ManReprStop( Aig_Man_t * p );
593 extern void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
594 extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
595 extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
596 extern Aig_Man_t * Aig_ManDupReprBasic( Aig_Man_t * p );
597 extern int Aig_ManCountReprs( Aig_Man_t * p );
598 extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
599 extern int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
600 extern void Aig_ManMarkValidChoices( Aig_Man_t * p );
601 extern int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack );
602 /*=== aigRet.c ========================================================*/
603 extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
604 /*=== aigRetF.c ========================================================*/
605 extern Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax );
606 /*=== aigScl.c ==========================================================*/
607 extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
608 extern int Aig_ManSeqCleanup( Aig_Man_t * p );
609 extern int Aig_ManSeqCleanupBasic( Aig_Man_t * p );
610 extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
611 extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
612 extern void Aig_ManComputeSccs( Aig_Man_t * p );
613 extern Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
614 /*=== aigShow.c ========================================================*/
615 extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
616 /*=== aigTable.c ========================================================*/
617 extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
618 extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 );
619 extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
620 extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
621 extern int Aig_TableCountEntries( Aig_Man_t * p );
622 extern void Aig_TableProfile( Aig_Man_t * p );
623 extern void Aig_TableClear( Aig_Man_t * p );
624 /*=== aigTiming.c ========================================================*/
625 extern void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
626 extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
627 extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease );
628 extern void Aig_ManStopReverseLevels( Aig_Man_t * p );
629 extern void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
630 extern void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
631 extern void Aig_ManVerifyLevel( Aig_Man_t * p );
632 extern void Aig_ManVerifyReverseLevel( Aig_Man_t * p );
633 /*=== aigTruth.c ========================================================*/
634 extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
635 /*=== aigTsim.c ========================================================*/
636 extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
637 /*=== aigUtil.c =========================================================*/
638 extern void Aig_ManIncrementTravId( Aig_Man_t * p );
639 extern char * Aig_TimeStamp();
640 extern int Aig_ManHasNoGaps( Aig_Man_t * p );
641 extern int Aig_ManLevels( Aig_Man_t * p );
642 extern void Aig_ManResetRefs( Aig_Man_t * p );
643 extern void Aig_ManCleanMarkA( Aig_Man_t * p );
644 extern void Aig_ManCleanMarkB( Aig_Man_t * p );
645 extern void Aig_ManCleanMarkAB( Aig_Man_t * p );
646 extern void Aig_ManCleanData( Aig_Man_t * p );
647 extern void Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
648 extern void Aig_ManCleanNext( Aig_Man_t * p );
649 extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
650 extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj );
651 extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
652 extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
653 extern Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj );
654 extern int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
655 extern void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
656 extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
657 extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
658 extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
659 extern void Aig_ManDump( Aig_Man_t * p );
660 extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
661 extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
662 extern void Aig_ManSetCioIds( Aig_Man_t * p );
663 extern void Aig_ManCleanCioIds( Aig_Man_t * p );
664 extern int Aig_ManChoiceNum( Aig_Man_t * p );
665 extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
666 extern unsigned Aig_ManRandom( int fReset );
667 extern word Aig_ManRandom64( int fReset );
668 extern void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
669 extern void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
670 extern void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
671 extern void Aig_ManSetPhase( Aig_Man_t * pAig );
672 extern Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig );
673 extern void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
674 extern void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
675 extern void Aig_ManInvertConstraints( Aig_Man_t * pAig );
676
677 /*=== aigWin.c =========================================================*/
678 extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
679
680 /*=== aigMem.c ===========================================================*/
681 // fixed-size-block memory manager
682 extern Aig_MmFixed_t * Aig_MmFixedStart( int nEntrySize, int nEntriesMax );
683 extern void Aig_MmFixedStop( Aig_MmFixed_t * p, int fVerbose );
684 extern char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p );
685 extern void Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry );
686 extern void Aig_MmFixedRestart( Aig_MmFixed_t * p );
687 extern int Aig_MmFixedReadMemUsage( Aig_MmFixed_t * p );
688 extern int Aig_MmFixedReadMaxEntriesUsed( Aig_MmFixed_t * p );
689 // flexible-size-block memory manager
690 extern Aig_MmFlex_t * Aig_MmFlexStart();
691 extern void Aig_MmFlexStop( Aig_MmFlex_t * p, int fVerbose );
692 extern char * Aig_MmFlexEntryFetch( Aig_MmFlex_t * p, int nBytes );
693 extern void Aig_MmFlexRestart( Aig_MmFlex_t * p );
694 extern int Aig_MmFlexReadMemUsage( Aig_MmFlex_t * p );
695 // hierarchical memory manager
696 extern Aig_MmStep_t * Aig_MmStepStart( int nSteps );
697 extern void Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose );
698 extern char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
699 extern void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
700 extern int Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
701
702
703
704 ABC_NAMESPACE_HEADER_END
705
706
707
708 #endif
709
710 ////////////////////////////////////////////////////////////////////////
711 /// END OF FILE ///
712 ////////////////////////////////////////////////////////////////////////
713
714