ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaShrink7.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/vec/vecHash.h"
23#include "misc/util/utilTruth.h"
24
25
27
31
32// operation manager
33typedef struct Unm_Man_t_ Unm_Man_t;
35{
36 Gia_Man_t * pGia; // user's AIG
37 Gia_Man_t * pNew; // constructed AIG
38 Hash_IntMan_t * pHash; // hash table
39 int nNewSize; // expected size of new manager
40 Vec_Int_t * vUsed; // used nodes
41 Vec_Int_t * vId2Used; // mapping of obj IDs into used node IDs
42 Vec_Wrd_t * vTruths; // truth tables
43 Vec_Int_t * vLeaves; // temporary storage for leaves
44 abctime clkStart; // starting the clock
45};
46
47extern word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Wrd_t * vTruths );
48
52
65{
66 Unm_Man_t * p;
67 p = ABC_CALLOC( Unm_Man_t, 1 );
68 p->clkStart = Abc_Clock();
69 p->nNewSize = 3 * Gia_ManObjNum(pGia) / 2;
70 p->pGia = pGia;
71 p->pNew = Gia_ManStart( p->nNewSize );
72 p->pNew->pName = Abc_UtilStrsav( pGia->pName );
73 p->pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
74 Gia_ManHashAlloc( p->pNew );
75 Gia_ManCleanLevels( p->pNew, p->nNewSize );
76 // allocate traversal IDs
77 p->pNew->nObjs = p->nNewSize;
79 p->pNew->nObjs = 1;
80 // start hashing
81 p->pHash = Hash_IntManStart( 1000 );
82 // truth tables
83 p->vLeaves = Vec_IntStart( 10 );
84 return p;
85}
87{
88 Gia_Man_t * pTemp = p->pNew; p->pNew = NULL;
89 Gia_ManHashStop( pTemp );
90 Vec_IntFreeP( &pTemp->vLevels );
91 Gia_ManSetRegNum( pTemp, Gia_ManRegNum(p->pGia) );
92 // truth tables
93 Vec_WrdFreeP( &p->vTruths );
94 Vec_IntFreeP( &p->vLeaves );
95 Vec_IntFreeP( &p->vUsed );
96 Vec_IntFreeP( &p->vId2Used );
97 // free data structures
98 Hash_IntManStop( p->pHash );
99 ABC_FREE( p );
100
101 Gia_ManStop( pTemp );
102 pTemp = NULL;
103
104 return pTemp;
105}
106
118int Unm_ManPrintPairStats( Hash_IntMan_t * pHash, int nTotal0, int nPairs0, int nPairs1, int fUseLit )
119{
120 int i, Num, nRefs, nPairs = 0, nTotal = 0, Counter[21] = {0};
121 Num = Hash_IntManEntryNum( pHash );
122 for ( i = 1; i <= Num; i++ )
123 {
124 nRefs = Abc_MinInt( 20, Hash_IntObjData2(pHash, i) );
125 nTotal += nRefs;
126 Counter[nRefs]++;
127 nPairs += (nRefs > 1);
128/*
129 if ( fUseLit )
130 printf( "(%c%c, %c%c) %d\n",
131 Abc_LitIsCompl(Hash_IntObjData0(pHash, i)-2) ? '!' : ' ',
132 'a' + Abc_Lit2Var(Hash_IntObjData0(pHash, i)-2),
133 Abc_LitIsCompl(Hash_IntObjData1(pHash, i)-2) ? '!' : ' ',
134 'a' + Abc_Lit2Var(Hash_IntObjData1(pHash, i)-2), nRefs );
135 else
136 printf( "( %c, %c) %d\n",
137 'a' + Hash_IntObjData0(pHash, i)-1,
138 'a' + Hash_IntObjData1(pHash, i)-1, nRefs );
139*/
140// printf( "(%4d, %4d) %d\n", Hash_IntObjData0(pHash, i), Hash_IntObjData1(pHash, i), nRefs );
141
142 }
143 printf( "Statistics for pairs appearing less than 20 times:\n" );
144 for ( i = 0; i < 21; i++ )
145 if ( Counter[i] > 0 )
146 printf( "%3d : %7d %7.2f %%\n", i, Counter[i], 100.0 * Counter[i] * i / Abc_MaxInt(nTotal, 1) );
147 printf( "Pairs: Total = %8d Init = %8d %7.2f %% Final = %8d %7.2f %% Real = %8d %7.2f %%\n", nTotal0,
148 nPairs0, 100.0 * nPairs0 / Abc_MaxInt(nTotal0, 1),
149 nPairs, 100.0 * nPairs / Abc_MaxInt(nTotal0, 1),
150 nPairs1, 100.0 * nPairs1 / Abc_MaxInt(nTotal0, 1) );
151 return nPairs;
152}
154{
155 Gia_Obj_t * pObj;
156 Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
157 Vec_Int_t * vNum2Obj = Vec_IntStart( 1 );
158 Hash_IntMan_t * pHash = Hash_IntManStart( 1000 );
159 int nTotal = 0, nPairs0 = 0, nPairs = 0;
160 int i, k, j, FanK, FanJ, Num, nRefs;
161 Gia_ManSetRefsMapped( p->pGia );
162 Gia_ManForEachLut( p->pGia, i )
163 {
164 nTotal += Gia_ObjLutSize(p->pGia, i) * (Gia_ObjLutSize(p->pGia, i) - 1) / 2;
165 pObj = Gia_ManObj( p->pGia, i );
166 // collect leaves of this gate
167 Vec_IntClear( p->vLeaves );
168 Gia_LutForEachFanin( p->pGia, i, Num, k )
169 if ( Gia_ObjRefNumId(p->pGia, Num) > 1 )
170 Vec_IntPush( p->vLeaves, Num );
171 if ( Vec_IntSize(p->vLeaves) < 2 )
172 continue;
173 nPairs0 += Vec_IntSize(p->vLeaves) * (Vec_IntSize(p->vLeaves) - 1) / 2;
174 // enumerate pairs
175 Vec_IntForEachEntry( p->vLeaves, FanK, k )
176 Vec_IntForEachEntryStart( p->vLeaves, FanJ, j, k+1 )
177 {
178 if ( FanK > FanJ )
179 ABC_SWAP( int, FanK, FanJ );
180 Num = Hash_Int2ManInsert( pHash, FanK, FanJ, 0 );
181 nRefs = Hash_Int2ObjInc(pHash, Num);
182 if ( nRefs == 0 )
183 {
184 assert( Num == Hash_IntManEntryNum(pHash) );
185 assert( Num == Vec_IntSize(vNum2Obj) );
186 Vec_IntPush( vNum2Obj, i );
187 continue;
188 }
189 if ( nRefs == 1 )
190 {
191 assert( Num < Vec_IntSize(vNum2Obj) );
192 Vec_IntPush( vPairs, Vec_IntEntry(vNum2Obj, Num) );
193 Vec_IntPush( vPairs, FanK );
194 Vec_IntPush( vPairs, FanJ);
195 }
196 Vec_IntPush( vPairs, i );
197 Vec_IntPush( vPairs, FanK );
198 Vec_IntPush( vPairs, FanJ );
199 }
200 }
201 Vec_IntFree( vNum2Obj );
202 if ( fVerbose )
203 nPairs = Unm_ManPrintPairStats( pHash, nTotal, nPairs0, Vec_IntSize(vPairs) / 3, 0 );
204 Hash_IntManStop( pHash );
205 return vPairs;
206}
207// finds used nodes
209{
210 Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
211 Vec_Str_t * vMarks = Vec_StrStart( nObjs ); int i;
212 for ( i = 0; i < Vec_IntSize(vPairs); i += 3 )
213 Vec_StrWriteEntry( vMarks, Vec_IntEntry(vPairs, i), 1 );
214 for ( i = 0; i < nObjs; i++ )
215 if ( Vec_StrEntry( vMarks, i ) )
216 Vec_IntPush( vNodes, i );
217 Vec_StrFree( vMarks );
218 printf( "The number of used nodes = %d\n", Vec_IntSize(vNodes) );
219 return vNodes;
220}
221// computes truth table for selected nodes
223{
224 Vec_Wrd_t * vTruthsTemp, * vTruths;
225 int i, k, iObj, iNode;
226 word uTruth;
227 vTruths = Vec_WrdAlloc( Vec_IntSize(p->vUsed) );
228 vTruthsTemp = Vec_WrdStart( Gia_ManObjNum(p->pGia) );
229 Vec_IntForEachEntry( p->vUsed, iObj, i )
230 {
231 assert( Gia_ObjIsLut(p->pGia, iObj) );
232 // collect leaves of this gate
233 Vec_IntClear( p->vLeaves );
234 Gia_LutForEachFanin( p->pGia, iObj, iNode, k )
235 Vec_IntPush( p->vLeaves, iNode );
236 assert( Vec_IntSize(p->vLeaves) <= 6 );
237 // compute truth table
238 uTruth = Shr_ManComputeTruth6( p->pGia, Gia_ManObj(p->pGia, iObj), p->vLeaves, vTruthsTemp );
239 Vec_WrdPush( vTruths, uTruth );
240// if ( i % 100 == 0 )
241// Kit_DsdPrintFromTruth( (unsigned *)&uTruth, 6 ), printf( "\n" );
242 }
243 Vec_WrdFreeP( &vTruthsTemp );
244 return vTruths;
245}
246
258Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbose )
259{
260 word uTruth; int nNonUnique = 0;
261 int i, k, j, s, iObj, iNode, iUsed, FanK, FanJ, Res, Num, nRefs;
262 Vec_Int_t * vNum2Obj = Vec_IntStart( 1 );
263 Vec_Int_t * vPairs2 = Vec_IntAlloc( 1000 );
264 assert( Hash_IntManEntryNum(p->pHash) == 0 );
265 for ( i = 0; i < Vec_IntSize(vPairs); i += 3 )
266 {
267 iObj = Vec_IntEntry( vPairs, i );
268 assert( Gia_ObjIsLut(p->pGia, iObj) );
269 // collect leaves of this gate
270 Vec_IntClear( p->vLeaves );
271 Gia_LutForEachFanin( p->pGia, iObj, iNode, s )
272 Vec_IntPush( p->vLeaves, iNode );
273 assert( Vec_IntSize(p->vLeaves) <= 6 );
274 FanK = Vec_IntEntry(vPairs, i+1);
275 FanJ = Vec_IntEntry(vPairs, i+2);
276 k = Vec_IntFind( p->vLeaves, FanK );
277 j = Vec_IntFind( p->vLeaves, FanJ );
278 assert( FanK < FanJ );
279 iUsed = Vec_IntEntry( p->vId2Used, iObj );
280 uTruth = Vec_WrdEntry( p->vTruths, iUsed );
281 Res = Abc_TtCheckDsdAnd( uTruth, k, j, NULL );
282 if ( Res == -1 )
283 continue;
284 // derive literals
285 FanK = Abc_Var2Lit( FanK, ((Res >> 0) & 1) );
286 FanJ = Abc_Var2Lit( FanJ, ((Res >> 1) & 1) );
287 if ( Res == 4 )
288 ABC_SWAP( int, FanK, FanJ );
289 Num = Hash_Int2ManInsert( p->pHash, FanK, FanJ, 0 );
290 nRefs = Hash_Int2ObjInc(p->pHash, Num);
291 if ( nRefs == 0 )
292 {
293 assert( Num == Hash_IntManEntryNum(p->pHash) );
294 assert( Num == Vec_IntSize(vNum2Obj) );
295 Vec_IntPush( vNum2Obj, iObj );
296 continue;
297 }
298 if ( nRefs == 1 )
299 {
300 assert( Num < Vec_IntSize(vNum2Obj) );
301 Vec_IntPush( vPairs2, Vec_IntEntry(vNum2Obj, Num) );
302 Vec_IntPush( vPairs2, FanK );
303 Vec_IntPush( vPairs2, FanJ );
304 nNonUnique++;
305 }
306 Vec_IntPush( vPairs2, iObj );
307 Vec_IntPush( vPairs2, FanK );
308 Vec_IntPush( vPairs2, FanJ );
309 }
310 Vec_IntFree( vNum2Obj );
311 if ( fVerbose )
312 Unm_ManPrintPairStats( p->pHash, Vec_IntSize(vPairs)/3, Hash_IntManEntryNum(p->pHash), Vec_IntSize(vPairs2)/3, 1 );
313// Hash_IntManStop( pHash );
314 return vPairs2;
315}
316
329{
330 Vec_Int_t * vPairs, * vPairs2;
331 // find the duplicated pairs
332 vPairs = Unm_ManComputePairs( p, 1 );
333 // find the used nodes
334 p->vUsed = Unm_ManFindUsedNodes( vPairs, Gia_ManObjNum(p->pGia) );
335 p->vId2Used = Vec_IntInvert( p->vUsed, -1 );
336 Vec_IntFillExtra( p->vId2Used, Gia_ManObjNum(p->pGia), -1 );
337 // compute truth tables for used nodes
338 p->vTruths = Unm_ManComputeTruths( p );
339 // derive new pairs
340 vPairs2 = Unm_ManCollectDecomp( p, vPairs, 1 );
341 Vec_IntFreeP( &vPairs );
342 Vec_IntFreeP( &vPairs2 );
343}
344
345
358{
359 Unm_Man_t * p;
360 p = Unm_ManAlloc( pGia );
361 Unm_ManWork( p );
362
363 Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
364 return Unm_ManFree( p );
365}
366
370
371
373
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Cube * p
Definition exorList.c:222
Vec_Int_t * Unm_ManCollectDecomp(Unm_Man_t *p, Vec_Int_t *vPairs, int fVerbose)
Definition giaShrink7.c:258
Gia_Man_t * Unm_ManFree(Unm_Man_t *p)
Definition giaShrink7.c:86
word Shr_ManComputeTruth6(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves, Vec_Wrd_t *vTruths)
Definition giaShrink6.c:335
Vec_Int_t * Unm_ManFindUsedNodes(Vec_Int_t *vPairs, int nObjs)
Definition giaShrink7.c:208
Vec_Int_t * Unm_ManComputePairs(Unm_Man_t *p, int fVerbose)
Definition giaShrink7.c:153
typedefABC_NAMESPACE_IMPL_START struct Unm_Man_t_ Unm_Man_t
DECLARATIONS ///.
Definition giaShrink7.c:33
Vec_Wrd_t * Unm_ManComputeTruths(Unm_Man_t *p)
Definition giaShrink7.c:222
int Unm_ManPrintPairStats(Hash_IntMan_t *pHash, int nTotal0, int nPairs0, int nPairs1, int fUseLit)
Definition giaShrink7.c:118
Gia_Man_t * Unm_ManTest(Gia_Man_t *pGia)
Definition giaShrink7.c:357
void Unm_ManWork(Unm_Man_t *p)
Definition giaShrink7.c:328
Unm_Man_t * Unm_ManAlloc(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition giaShrink7.c:64
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
void Gia_ManSetRefsMapped(Gia_Man_t *p)
Definition giaIf.c:271
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
#define Gia_ManForEachLut(p, i)
Definition gia.h:1157
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition gia.h:1161
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition giaUtil.c:511
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Vec_Int_t * vLevels
Definition gia.h:120
char * pSpec
Definition gia.h:100
char * pName
Definition gia.h:99
Hash_IntMan_t * pHash
Definition giaShrink7.c:38
abctime clkStart
Definition giaShrink7.c:44
Gia_Man_t * pNew
Definition giaShrink7.c:37
Vec_Int_t * vId2Used
Definition giaShrink7.c:41
Vec_Wrd_t * vTruths
Definition giaShrink7.c:42
Vec_Int_t * vUsed
Definition giaShrink7.c:40
Gia_Man_t * pGia
Definition giaShrink7.c:36
Vec_Int_t * vLeaves
Definition giaShrink7.c:43
#define assert(ex)
Definition util_old.h:213
struct Hash_IntMan_t_ Hash_IntMan_t
Definition vecHash.h:51
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42