ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaSimBase.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/util/utilTruth.h"
23#include "misc/extra/extra.h"
24//#include <immintrin.h>
25#include "aig/miniaig/miniaig.h"
26
27ABC_NAMESPACE_IMPL_START
28
29
33
34
35typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t;
48
49
50typedef struct Gia_SimAbsMan_t_ Gia_SimAbsMan_t;
51struct Gia_SimAbsMan_t_
52{
53 // problem formulation
54 Gia_Man_t * pGia; // AIG manager
55 word * pSet[2]; // offset/onset truth tables
56 int nCands; // candidate count
57 int nWords; // word count
58 Vec_Wrd_t * vSims; // candidate simulation info
59 Vec_Int_t * vResub; // the result
60 int fVerbose; // verbose
61 // intermediate result
62 Vec_Int_t * vValues; // function values in each pattern
63 Vec_Int_t * vPatPairs; // used minterms
64 int nWordsTable; // words of table data
65 word * pTableTemp; // temporary table pattern
66 Vec_Wrd_t * vCoverTable; // columns = minterms; rows = classes
67 Vec_Int_t * vTtMints; // truth table minterms
68};
69
73
85void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn )
86{
87 int i, Id;
88 assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) );
89 assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) );
90 Gia_ManForEachCiId( p, Id, i )
91 memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords );
92}
93static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
94{
95 word pComps[2] = { 0, ~(word)0 };
96 word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
97 word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
98 word * pSims = Vec_WrdArray(vSims);
99 word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i);
100 word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i);
101 word * pSims2 = pSims + nWords*i; int w;
102 if ( Gia_ObjIsXor(pObj) )
103 for ( w = 0; w < nWords; w++ )
104 pSims2[w] = (pSims0[w] ^ Diff0) ^ (pSims1[w] ^ Diff1);
105 else
106 for ( w = 0; w < nWords; w++ )
107 pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
108}
109static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
110{
111 word pComps[2] = { 0, ~(word)0 };
112 word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
113 word * pSims = Vec_WrdArray(vSims);
114 word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i);
115 word * pSims2 = pSims + nWords*i; int w;
116 for ( w = 0; w < nWords; w++ )
117 pSims2[w] = (pSims0[w] ^ Diff0);
118}
119static inline void Gia_ManSimPatSimNot( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
120{
121 word * pSims = Vec_WrdArray(vSims) + nWords*i; int w;
122 for ( w = 0; w < nWords; w++ )
123 pSims[w] = ~pSims[w];
124}
125Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
126{
127 Gia_Obj_t * pObj;
128 int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
129 Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
130 assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
131 Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi );
132 Gia_ManForEachAnd( pGia, pObj, i )
133 Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims );
134 Gia_ManForEachCo( pGia, pObj, i )
135 Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
136 return vSims;
137}
138Vec_Wrd_t * Gia_ManSimPatSimOut( Gia_Man_t * pGia, Vec_Wrd_t * vSimsPi, int fOuts )
139{
140 Gia_Obj_t * pObj;
141 int i, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(pGia);
142 Vec_Wrd_t * vSimsCo = fOuts ? Vec_WrdStart( Gia_ManCoNum(pGia) * nWords ) : NULL;
143 Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
144 assert( Vec_WrdSize(vSimsPi) % Gia_ManCiNum(pGia) == 0 );
145 Gia_ManSimPatAssignInputs( pGia, nWords, vSims, vSimsPi );
146 Gia_ManForEachAnd( pGia, pObj, i )
147 Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims );
148 Gia_ManForEachCo( pGia, pObj, i )
149 Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
150 if ( !fOuts )
151 return vSims;
152 Gia_ManForEachCo( pGia, pObj, i )
153 memcpy( Vec_WrdEntryP(vSimsCo, i*nWords), Vec_WrdEntryP(vSims, Gia_ObjId(pGia, pObj)*nWords), sizeof(word)*nWords );
154 Vec_WrdFree( vSims );
155 return vSimsCo;
156}
157static inline void Gia_ManSimPatSimAnd3( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC )
158{
159 word pComps[2] = { ~(word)0, 0 };
160 word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
161 word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
162 word * pSims0 = Vec_WrdArray(vSims) + nWords*Gia_ObjFaninId0(pObj, i);
163 word * pSims1 = Vec_WrdArray(vSims) + nWords*Gia_ObjFaninId1(pObj, i);
164 word * pSims2 = Vec_WrdArray(vSims) + nWords*i;
165 word * pSimsC0 = Vec_WrdArray(vSimsC) + nWords*Gia_ObjFaninId0(pObj, i);
166 word * pSimsC1 = Vec_WrdArray(vSimsC) + nWords*Gia_ObjFaninId1(pObj, i);
167 word * pSimsC2 = Vec_WrdArray(vSimsC) + nWords*i; int w;
168 if ( Gia_ObjIsXor(pObj) )
169 for ( w = 0; w < nWords; w++ )
170 {
171 pSimsC0[w] |= pSimsC2[w];
172 pSimsC1[w] |= pSimsC2[w];
173 }
174 else
175 for ( w = 0; w < nWords; w++ )
176 {
177 pSimsC0[w] |= (pSims2[w] | (pSims0[w] ^ Diff0)) & pSimsC2[w];
178 pSimsC1[w] |= (pSims2[w] | (pSims1[w] ^ Diff1)) & pSimsC2[w];
179 }
180}
181Vec_Wrd_t * Gia_ManSimPatSimIn( Gia_Man_t * pGia, Vec_Wrd_t * vSims, int fIns, Vec_Int_t * vAnds )
182{
183 Gia_Obj_t * pObj;
184 int i, Id, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
185 Vec_Wrd_t * vSimsCi = fIns ? Vec_WrdStart( Gia_ManCiNum(pGia) * nWords ) : NULL;
186 Vec_Wrd_t * vSimsC = Vec_WrdStart( Vec_WrdSize(vSims) );
187 assert( Vec_WrdSize(vSims) % Gia_ManObjNum(pGia) == 0 );
188 if ( vAnds )
189 Vec_IntForEachEntry( vAnds, Id, i )
190 memset( Vec_WrdEntryP(vSimsC, Id*nWords), 0xFF, sizeof(word)*nWords );
191 else
192 Gia_ManForEachCoDriverId( pGia, Id, i )
193 memset( Vec_WrdEntryP(vSimsC, Id*nWords), 0xFF, sizeof(word)*nWords );
194 Gia_ManForEachAndReverse( pGia, pObj, i )
195 Gia_ManSimPatSimAnd3( pGia, i, pObj, nWords, vSims, vSimsC );
196 if ( !fIns )
197 return vSimsC;
198 Gia_ManForEachCi( pGia, pObj, i )
199 memcpy( Vec_WrdEntryP(vSimsCi, i*nWords), Vec_WrdEntryP(vSimsC, Gia_ObjId(pGia, pObj)*nWords), sizeof(word)*nWords );
200 Vec_WrdFree( vSimsC );
201 return vSimsCi;
202}
203void Gia_ManSimPatSimInTest( Gia_Man_t * pGia )
204{
205 int nWords = 10;
206 Vec_Wrd_t * vSimsCi = Vec_WrdStartRandom( Gia_ManCiNum(pGia) * nWords );
207 Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( pGia, vSimsCi, 0 );
208 Vec_Wrd_t * vSims2 = Gia_ManSimPatSimIn( pGia, vSims, 0, NULL );
209 int nOnes = Abc_TtCountOnesVec( Vec_WrdArray(vSims2), Vec_WrdSize(vSims2) );
210 int nTotal = 64*nWords*Gia_ManCandNum(pGia);
211 printf( "Ratio = %6.2f %%\n", 100.0*nOnes/nTotal );
212 Vec_WrdFree( vSims );
213 Vec_WrdFree( vSims2 );
214 Vec_WrdFree( vSimsCi );
215}
216static inline void Gia_ManSimPatSimAnd4( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC )
217{
218 word pComps[2] = { ~(word)0, 0 };
219 word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
220 word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
221 word * pSims0 = Vec_WrdArray(vSims) + nWords*Gia_ObjFaninId0(pObj, i);
222 word * pSims1 = Vec_WrdArray(vSims) + nWords*Gia_ObjFaninId1(pObj, i);
223 word * pSimsC0 = Vec_WrdArray(vSimsC) + nWords*Gia_ObjFaninId0(pObj, i);
224 word * pSimsC1 = Vec_WrdArray(vSimsC) + nWords*Gia_ObjFaninId1(pObj, i);
225 word * pSimsC2 = Vec_WrdArray(vSimsC) + nWords*i; int w;
226 if ( Gia_ObjIsXor(pObj) )
227 for ( w = 0; w < nWords; w++ )
228 pSimsC2[w] = pSimsC0[w] & pSimsC1[w];
229 else
230 for ( w = 0; w < nWords; w++ )
231 pSimsC2[w] = (pSimsC0[w] & pSimsC1[w]) | ((pSims0[w] ^ Diff0) & pSimsC0[w]) | ((pSims1[w] ^ Diff1) & pSimsC1[w]);
232}
233Vec_Wrd_t * Gia_ManSimPatSimC( Gia_Man_t * pGia, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsCiC )
234{
235 Gia_Obj_t * pObj;
236 int i, Id, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
237 Vec_Wrd_t * vSimsC = Vec_WrdStart( Vec_WrdSize(vSims) );
238 assert( Vec_WrdSize(vSims) % Gia_ManObjNum(pGia) == 0 );
239 memset( Vec_WrdEntryP(vSimsC, 0), 0xFF, sizeof(word)*nWords );
240 Gia_ManForEachCiId( pGia, Id, i )
241 memmove( Vec_WrdEntryP(vSimsC, Id*nWords), Vec_WrdEntryP(vSimsCiC, i*nWords), sizeof(word)*nWords );
242 Gia_ManForEachAnd( pGia, pObj, i )
243 Gia_ManSimPatSimAnd4( pGia, i, pObj, nWords, vSims, vSimsC );
244 return vSimsC;
245}
246void Gia_ManSimPatSimCTest( Gia_Man_t * pGia )
247{
248 int nWords = 10;
249 Vec_Wrd_t * vSimsCi = Vec_WrdStartRandom( Gia_ManCiNum(pGia) * nWords );
250 Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( pGia, vSimsCi, 0 );
251 Vec_Wrd_t * vSims2 = Gia_ManSimPatSimIn( pGia, vSims, 0, NULL );
252 Vec_Wrd_t * vSimsCi2 = Gia_ManSimPatSimIn( pGia, vSims, 1, NULL );
253 Vec_Wrd_t * vSims3 = Gia_ManSimPatSimC( pGia, vSims, vSimsCi2 );
254 int nOnes2 = Abc_TtCountOnesVec( Vec_WrdArray(vSims2), Vec_WrdSize(vSims2) );
255 int nOnes3 = Abc_TtCountOnesVec( Vec_WrdArray(vSims3), Vec_WrdSize(vSims3) );
256 int nTotal = 64*nWords*Gia_ManCandNum(pGia);
257 printf( "Ratio = %6.2f %% Ratio = %6.2f %%\n", 100.0*nOnes2/nTotal, 100.0*nOnes3/nTotal );
258 Vec_WrdFree( vSims );
259 Vec_WrdFree( vSims2 );
260 Vec_WrdFree( vSims3 );
261 Vec_WrdFree( vSimsCi );
262 Vec_WrdFree( vSimsCi2 );
263}
264void Gia_ManSimPatResim( Gia_Man_t * pGia, Vec_Int_t * vObjs, int nWords, Vec_Wrd_t * vSims )
265{
266 Gia_Obj_t * pObj; int i;
267 Gia_ManForEachObjVec( vObjs, pGia, pObj, i )
268 if ( i == 0 )
269 Gia_ManSimPatSimNot( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
270 else if ( Gia_ObjIsAnd(pObj) )
271 Gia_ManSimPatSimAnd( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
272 else if ( !Gia_ObjIsCo(pObj) ) assert(0);
273}
274void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
275{
276 Vec_WrdDumpHex( pFileName, vSimsIn, nWords, 0 );
277}
278
279
291Vec_Wrd_t * Gia_ManDeriveNodeFuncs( Gia_Man_t * p )
292{
293 int nWords = Abc_Truth6WordNum( Gia_ManCiNum(p) );
294 Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) );
295 Gia_Obj_t * pObj; int i;
296 Gia_ManForEachCi( p, pObj, i )
297 assert( Gia_ObjId(p, pObj) == i+1 );
298 Vec_Ptr_t * vTruths = Vec_PtrAllocTruthTables( Gia_ManCiNum(p) );
299 Gia_ManForEachCi( p, pObj, i )
300 Abc_TtCopy( Vec_WrdEntryP(vSims, nWords*(i+1)), (word *)Vec_PtrEntry(vTruths, i), nWords, 0 );
301 Vec_PtrFree( vTruths );
302 Gia_ManForEachAnd( p, pObj, i )
303 Gia_ManSimPatSimAnd( p, i, pObj, nWords, vSims );
304 return vSims;
305}
306word * Gia_ManDeriveFuncs( Gia_Man_t * p )
307{
308 int nVars2 = (Gia_ManCiNum(p) + 6)/2;
309 int nVars3 = Gia_ManCiNum(p) - nVars2;
310 int nWords = Abc_Truth6WordNum( Gia_ManCiNum(p) );
311 int nWords2 = Abc_Truth6WordNum( nVars2 );
312 word * pRes = ABC_ALLOC( word, Gia_ManCoNum(p) * nWords );
313 Vec_Wrd_t * vSims = Vec_WrdStart( nWords2 * Gia_ManObjNum(p) );
314 Vec_Ptr_t * vTruths = Vec_PtrAllocTruthTables( nVars2 );
315 Gia_Obj_t * pObj; int i, v, m;
316 Gia_ManForEachCi( p, pObj, i )
317 assert( Gia_ObjId(p, pObj) == i+1 );
318 for ( i = 0; i < nVars2; i++ )
319 Abc_TtCopy( Vec_WrdEntryP(vSims, nWords2*(i+1)), (word *)Vec_PtrEntry(vTruths, i), nWords2, 0 );
320 Vec_PtrFree( vTruths );
321 for ( m = 0; m < (1 << nVars3); m++ )
322 {
323 for ( v = 0; v < nVars3; v++ )
324 Abc_TtConst( Vec_WrdEntryP(vSims, nWords2*(nVars2+v+1)), nWords2, (m >> v) & 1 );
325 Gia_ManForEachAnd( p, pObj, i )
326 Gia_ManSimPatSimAnd( p, i, pObj, nWords2, vSims );
327 Gia_ManForEachCo( p, pObj, i )
328 Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords2, vSims );
329 Gia_ManForEachCo( p, pObj, i )
330 Abc_TtCopy( pRes + i*nWords + m*nWords2, Vec_WrdEntryP(vSims, nWords2*Gia_ObjId(p, pObj)), nWords2, 0 );
331 }
332 Vec_WrdFree( vSims );
333 return pRes;
334}
335Gia_Man_t * Gia_ManPerformMuxDec( Gia_Man_t * p )
336{
337 extern int Gia_ManFindMuxTree_rec( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData, int Shift );
338 extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
339 int nWords = Abc_Truth6WordNum( Gia_ManCiNum(p) );
340 int nCofs = 1 << (Gia_ManCiNum(p) - 6);
341 word * pRes = Gia_ManDeriveFuncs( p );
342 Vec_Int_t * vMemory = Vec_IntAlloc( 1 << 16 );
343 Vec_Int_t * vLeaves = Vec_IntAlloc( 6 );
344 Vec_Int_t * vCtrls = Vec_IntAlloc( nCofs );
345 Vec_Int_t * vDatas = Vec_IntAlloc( Gia_ManCoNum(p) );
346 Gia_Man_t * pNew, * pTemp; int i, o;
347 pNew = Gia_ManStart( Gia_ManObjNum(p) );
348 pNew->pName = Abc_UtilStrsav( p->pName );
349 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
350 Gia_ManConst0(p)->Value = 0;
351 for ( i = 0; i < Gia_ManCiNum(p); i++ )
352 Vec_IntPush( i < 6 ? vLeaves : vCtrls, Gia_ManAppendCi(pNew) );
353 Gia_ManHashAlloc( pNew );
354 for ( o = 0; o < Gia_ManCoNum(p); o++ )
355 {
356 Vec_IntClear( vDatas );
357 for ( i = 0; i < nWords; i++ )
358 Vec_IntPush( vDatas, Kit_TruthToGia(pNew, (unsigned *)(pRes+o*nWords+i), 6, vMemory, vLeaves, 1) );
359 Gia_ManAppendCo( pNew, Gia_ManFindMuxTree_rec(pNew, Vec_IntArray(vCtrls), Vec_IntSize(vCtrls), vDatas, 0) );
360 }
361 Gia_ManHashStop( pNew );
362 ABC_FREE( pRes );
363 Vec_IntFree( vMemory );
364 Vec_IntFree( vLeaves );
365 Vec_IntFree( vCtrls );
366 Vec_IntFree( vDatas );
367 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
368 pNew = Gia_ManCleanup( pTemp = pNew );
369 Gia_ManStop( pTemp );
370 Gia_ManTransferTiming( pNew, p );
371 return pNew;
372}
373
385int Gia_ManComputeTfos_rec( Gia_Man_t * p, int iObj, int iRoot, Vec_Int_t * vNode )
386{
387 Gia_Obj_t * pObj;
388 if ( Gia_ObjIsTravIdPreviousId(p, iObj) )
389 return 1;
390 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
391 return 0;
392 pObj = Gia_ManObj( p, iObj );
393 if ( !Gia_ObjIsAnd(pObj) )
394 return 0;
395 if ( Gia_ManComputeTfos_rec( p, Gia_ObjFaninId0(pObj, iObj), iRoot, vNode ) |
396 Gia_ManComputeTfos_rec( p, Gia_ObjFaninId1(pObj, iObj), iRoot, vNode ) )
397 {
398 Gia_ObjSetTravIdPreviousId(p, iObj);
399 Vec_IntPush( vNode, iObj );
400 return 1;
401 }
402 Gia_ObjSetTravIdCurrentId(p, iObj);
403 return 0;
404}
405Vec_Wec_t * Gia_ManComputeTfos( Gia_Man_t * p )
406{
407 Vec_Wec_t * vNodes = Vec_WecStart( Gia_ManCiNum(p) );
408 Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
409 int i, o, IdCi, IdCo;
410 Gia_ManForEachCiId( p, IdCi, i )
411 {
412 Vec_Int_t * vNode = Vec_WecEntry( vNodes, i );
413 Gia_ManIncrementTravId( p );
414 Gia_ManIncrementTravId( p );
415 Gia_ObjSetTravIdPreviousId(p, IdCi);
416 Vec_IntPush( vNode, IdCi );
417 Vec_IntClear( vTemp );
418 Gia_ManForEachCoId( p, IdCo, o )
419 if ( Gia_ManComputeTfos_rec( p, Gia_ObjFaninId0(Gia_ManObj(p, IdCo), IdCo), IdCi, vNode ) )
420 Vec_IntPush( vTemp, Gia_ManObjNum(p) + (o >> 1) );
421 Vec_IntUniqify( vTemp );
422 Vec_IntAppend( vNode, vTemp );
423 }
424 Vec_IntFree( vTemp );
425 Vec_WecSort( vNodes, 1 );
426 //Vec_WecPrint( vNodes, 0 );
427 //Gia_AigerWrite( p, "dump.aig", 0, 0, 0 );
428 return vNodes;
429}
430int Gia_ManFindDividerVar( Gia_Man_t * p, int fVerbose )
431{
432 int iVar, Target = 1 << 28;
433 for ( iVar = 6; iVar < Gia_ManCiNum(p); iVar++ )
434 if ( (1 << (iVar-3)) * Gia_ManObjNum(p) > Target )
435 break;
436 if ( iVar == Gia_ManCiNum(p) )
437 iVar = Gia_ManCiNum(p) - 1;
438 if ( fVerbose )
439 printf( "Split var = %d. Rounds = %d. Bytes per node = %d. Total = %.2f MB.\n", iVar, 1 << (Gia_ManCiNum(p) - iVar), 1 << (iVar-3), 1.0*(1 << (iVar-3)) * Gia_ManObjNum(p)/(1<<20) );
440 return iVar;
441}
442int Gia_ManComparePair( Gia_Man_t * p, Vec_Wrd_t * vSims, int iOut, int nWords2 )
443{
444 Gia_Obj_t * pObj0 = Gia_ManCo( p, 2*iOut+0 );
445 Gia_Obj_t * pObj1 = Gia_ManCo( p, 2*iOut+1 );
446 word * pSim0 = Vec_WrdEntryP( vSims, nWords2*Gia_ObjId(p, pObj0) );
447 word * pSim1 = Vec_WrdEntryP( vSims, nWords2*Gia_ObjId(p, pObj1) );
448 Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj0), pObj0, nWords2, vSims );
449 Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj1), pObj1, nWords2, vSims );
450 return Abc_TtEqual( pSim0, pSim1, nWords2 );
451}
452int Gia_ManCheckSimEquiv( Gia_Man_t * p, int fVerbose )
453{
454 abctime clk = Abc_Clock(); int fWarning = 0;
455 //int nVars2 = (Gia_ManCiNum(p) + 6)/2;
456 int nVars2 = Gia_ManFindDividerVar( p, fVerbose );
457 int nVars3 = Gia_ManCiNum(p) - nVars2;
458 int nWords2 = Abc_Truth6WordNum( nVars2 );
459 Vec_Wrd_t * vSims = Vec_WrdStart( nWords2 * Gia_ManObjNum(p) );
460 Vec_Wec_t * vNodes = Gia_ManComputeTfos( p );
461 Vec_Ptr_t * vTruths = Vec_PtrAllocTruthTables( nVars2 );
462 Gia_Obj_t * pObj; Vec_Int_t * vNode; int i, m, iObj;
463 Vec_WecForEachLevelStop( vNodes, vNode, i, nVars2 )
464 Abc_TtCopy( Vec_WrdEntryP(vSims, nWords2*Vec_IntEntry(vNode,0)), (word *)Vec_PtrEntry(vTruths, i), nWords2, 0 );
465 Vec_PtrFree( vTruths );
466 Gia_ManForEachAnd( p, pObj, i )
467 Gia_ManSimPatSimAnd( p, i, pObj, nWords2, vSims );
468 for ( i = 0; i < Gia_ManCoNum(p)/2; i++ )
469 {
470 if ( !Gia_ManComparePair( p, vSims, i, nWords2 ) )
471 {
472 printf( "Miter is asserted for output %d.\n", i );
473 Vec_WecFree( vNodes );
474 Vec_WrdFree( vSims );
475 return 0;
476 }
477 }
478 for ( m = 0; m < (1 << nVars3); m++ )
479 {
480 int iVar = m ? Abc_TtSuppFindFirst( m ^ (m >> 1) ^ (m-1) ^ ((m-1) >> 1) ) : 0;
481 vNode = Vec_WecEntry( vNodes, nVars2+iVar );
482 Abc_TtNot( Vec_WrdEntryP(vSims, nWords2*Vec_IntEntry(vNode,0)), nWords2 );
483 Vec_IntForEachEntryStart( vNode, iObj, i, 1 )
484 {
485 if ( iObj < Gia_ManObjNum(p) )
486 {
487 pObj = Gia_ManObj( p, iObj );
488 assert( Gia_ObjIsAnd(pObj) );
489 Gia_ManSimPatSimAnd( p, iObj, pObj, nWords2, vSims );
490 }
491 else if ( !Gia_ManComparePair( p, vSims, iObj - Gia_ManObjNum(p), nWords2 ) )
492 {
493 printf( "Miter is asserted for output %d.\n", iObj - Gia_ManObjNum(p) );
494 Vec_WecFree( vNodes );
495 Vec_WrdFree( vSims );
496 return 0;
497 }
498 }
499 //for ( i = 0; i < Gia_ManObjNum(p); i++ )
500 // printf( "%3d : ", i), Extra_PrintHex2( stdout, (unsigned *)Vec_WrdEntryP(vSims, i), 6 ), printf( "\n" );
501 if ( !fWarning && Abc_Clock() > clk + 5*CLOCKS_PER_SEC )
502 printf( "The computation is expected to take about %.2f sec.\n", 5.0*(1 << nVars3)/m ), fWarning = 1;
503 //if ( (m & 0x3F) == 0x3F )
504 if ( fVerbose && (m & 0xFF) == 0xFF )
505 printf( "Finished %6d (out of %6d)...\n", m, 1 << nVars3 );
506 }
507 Vec_WecFree( vNodes );
508 Vec_WrdFree( vSims );
509 return 1;
510}
511
523void Gia_ManSimPatAssignInputs2( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn )
524{
525 int i, Id;
526 assert( Vec_WrdSize(vSims) == 2 * nWords * Gia_ManObjNum(p) );
527 assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) );
528 Gia_ManForEachCiId( p, Id, i )
529 {
530 Abc_TtCopy( Vec_WrdEntryP(vSims, 2*Id*nWords+0), Vec_WrdEntryP(vSimsIn, i*nWords), nWords, 0 );
531 Abc_TtCopy( Vec_WrdEntryP(vSims, 2*Id*nWords+1), Vec_WrdEntryP(vSimsIn, i*nWords), nWords, 1 );
532 }
533}
534static inline void Gia_ManSimPatSimAnd2( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
535{
536 word * pSims = Vec_WrdArray(vSims);
537 word * pSims0 = pSims + nWords*Gia_ObjFaninLit0(pObj, i);
538 word * pSims1 = pSims + nWords*Gia_ObjFaninLit1(pObj, i);
539 word * pSims2 = pSims + nWords*(2*i+0);
540 word * pSims3 = pSims + nWords*(2*i+1); int w;
541 assert( !Gia_ObjIsXor(pObj) );
542// if ( Gia_ObjIsXor(pObj) )
543// for ( w = 0; w < nWords; w++ )
544// pSims2[w] = pSims0[w] ^ pSims1[w];
545// else
546 for ( w = 0; w < nWords; w++ )
547 {
548 pSims2[w] = pSims0[w] & pSims1[w];
549 pSims3[w] = ~pSims2[w];
550 }
551 //_mm256_storeu_ps( (float *)pSims2, _mm256_and_ps(_mm256_loadu_ps((float *)pSims0), _mm256_loadu_ps((float *)pSims1)) );
552}
553static inline void Gia_ManSimPatSimPo2( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
554{
555 word * pSims = Vec_WrdArray(vSims);
556 word * pSims0 = pSims + nWords*Gia_ObjFaninLit0(pObj, i);
557 word * pSims2 = pSims + nWords*i; int w;
558 for ( w = 0; w < nWords; w++ )
559 pSims2[w] = pSims0[w];
560}
561Vec_Wrd_t * Gia_ManSimPatSim2( Gia_Man_t * pGia )
562{
563 Gia_Obj_t * pObj;
564 int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
565 Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords * 2 );
566 assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
567 Gia_ManSimPatAssignInputs2( pGia, nWords, vSims, pGia->vSimsPi );
568 Gia_ManForEachAnd( pGia, pObj, i )
569 Gia_ManSimPatSimAnd2( pGia, i, pObj, nWords, vSims );
570 Gia_ManForEachCo( pGia, pObj, i )
571 Gia_ManSimPatSimPo2( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
572 return vSims;
573}
574
586void Gia_ManSimPatValuesDerive( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vValues )
587{
588 int i, Id;
589 assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) );
590 assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) );
591 Gia_ManForEachCoId( p, Id, i )
592 memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords );
593}
594Vec_Wrd_t * Gia_ManSimPatValues( Gia_Man_t * p )
595{
596 int i, Id, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
597 Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
598 Vec_Wrd_t * vValues = Vec_WrdStart( Gia_ManCoNum(p) * nWords );
599 assert( Vec_WrdSize(p->vSimsPi) == nWords * Gia_ManCiNum(p) );
600 assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) );
601 assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) );
602 Gia_ManForEachCoId( p, Id, i )
603 memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords );
604 Vec_WrdFree( vSims );
605 return vValues;
606}
607
608
620Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse )
621{
622 int nWordsBase = Vec_WrdSize(vBase) / nInputs;
623 int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w;
624 Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) );
625 assert( Vec_WrdSize(vBase) % nInputs == 0 );
626 assert( Vec_WrdSize(vAddOn) % nInputs == 0 );
627 assert( nWordsUse <= nWordsAddOn );
628 for ( i = 0; i < nInputs; i++ )
629 {
630 word * pSimsB = nWordsBase ? Vec_WrdEntryP( vBase, i * nWordsBase ) : NULL;
631 word * pSimsA = nWordsAddOn ? Vec_WrdEntryP( vAddOn, i * nWordsAddOn ) : NULL;
632 for ( w = 0; w < nWordsBase; w++ )
633 Vec_WrdPush( vSimsIn, pSimsB[w] );
634 for ( w = 0; w < nWordsUse; w++ )
635 Vec_WrdPush( vSimsIn, pSimsA[w] );
636 }
637 assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) || Vec_WrdSize(vSimsIn) < 16 );
638 return vSimsIn;
639}
640int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits )
641{
642 word * pSimsI, * pSimsC; int i, k;
643 for ( i = 0; i < iPat; i++ )
644 {
645 for ( k = 0; k < nLits; k++ )
646 {
647 int iVar = Abc_Lit2Var( pLits[k] );
648 pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar );
649 pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
650 if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) )
651 break;
652 }
653 if ( k == nLits )
654 break;
655 }
656 for ( k = 0; k < nLits; k++ )
657 {
658 int iVar = Abc_Lit2Var( pLits[k] );
659 pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar );
660 pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
661 if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) )
662 Abc_TtXorBit( pSimsI, i );
663 Abc_TtSetBit( pSimsC, i );
664 assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) );
665 }
666 return (int)(i == iPat);
667}
668Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes, int nUnDecs )
669{
670 int c, iCur = 0, iPat = 0;
671 int nWordsMax = Abc_Bit6WordNum( nCexes );
672 Vec_Wrd_t * vSimsIn = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWordsMax );
673 Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax );
674 Vec_Wrd_t * vSimsRes = NULL;
675 for ( c = 0; c < nCexes + nUnDecs; c++ )
676 {
677 int Out = Vec_IntEntry( vCexStore, iCur++ );
678 int Size = Vec_IntEntry( vCexStore, iCur++ );
679 if ( Size == -1 )
680 continue;
681 iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
682 iCur += Size;
683 assert( iPat <= nCexes + nUnDecs );
684 Out = 0;
685 }
686 assert( iCur == Vec_IntSize(vCexStore) );
687 vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) );
688 printf( "Compressed %d CEXes into %d patterns and added %d words to available %d words.\n",
689 nCexes, iPat, Abc_Bit6WordNum(iPat+1), Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p) );
690 Vec_WrdFree( vSimsIn );
691 Vec_WrdFree( vSimsCare );
692 return vSimsRes;
693}
694
706int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 )
707{
708 Gia_Obj_t * pObj;
709 int i, nUnique;
710 Vec_Mem_t * vStore;
711 vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
712 Vec_MemHashAlloc( vStore, 1 << 12 );
713 Gia_ManForEachCand( p, pObj, i )
714 {
715 word * pSim = Vec_WrdEntryP(vSims, i*nWords);
716 if ( pnC0 && Abc_TtIsConst0(pSim, nWords) )
717 (*pnC0)++;
718 if ( pnC1 && Abc_TtIsConst1(pSim, nWords) )
719 (*pnC1)++;
720 Vec_MemHashInsert( vStore, pSim );
721 }
722 nUnique = Vec_MemEntryNum( vStore );
723 Vec_MemHashFree( vStore );
724 Vec_MemFree( vStore );
725 return nUnique;
726}
727Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims )
728{
729 Gia_Man_t * pNew;
730 Gia_Obj_t * pObj;
731 int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p);
732 pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) );
733 Gia_ManHashStart( pNew );
734 Gia_ManConst0(p)->Value = 0;
735 Gia_ManForEachCi( p, pObj, i )
736 pObj->Value = Gia_ManAppendCi( pNew );
737 Gia_ManForEachAnd( p, pObj, i )
738 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
739 Gia_ManForEachAnd( p, pObj, i )
740 {
741 word * pSim = Vec_WrdEntryP(vSims, i*nWords);
742 if ( Abc_TtIsConst0(pSim, nWords) )
743 Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) );
744 if ( Abc_TtIsConst1(pSim, nWords) )
745 Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) );
746 }
747 Gia_ManHashStop( pNew );
748 return pNew;
749}
750
751
752
764void Gia_ManSimProfile( Gia_Man_t * pGia )
765{
766 Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
767 int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
768 int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
769 printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n",
770 64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
771 Vec_WrdFree( vSims );
772}
773void Gia_ManPatSatImprove( Gia_Man_t * p, int nWords0, int fVerbose )
774{
775 extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
776 int i, Status, Counts[3] = {0};
777 Gia_Man_t * pGia;
778 Vec_Wrd_t * vSimsIn = NULL;
779 Vec_Str_t * vStatus = NULL;
780 Vec_Int_t * vCexStore = NULL;
781 Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
782 //Gia_ManSimProfile( p );
783 pGia = Gia_ManSimPatGenMiter( p, vSims );
784 vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 );
785 Gia_ManStop( pGia );
786 Vec_StrForEachEntry( vStatus, Status, i )
787 {
788 assert( Status >= -1 && Status <= 1 );
789 Counts[Status+1]++;
790 }
791 if ( fVerbose )
792 printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
793 if ( Counts[1] == 0 )
794 printf( "There are no counter-examples. No need for more simulation.\n" );
795 else
796 {
797 vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1], Counts[0] );
798 Vec_WrdFreeP( &p->vSimsPi );
799 p->vSimsPi = vSimsIn;
800 //Gia_ManSimProfile( p );
801 }
802 Vec_StrFree( vStatus );
803 Vec_IntFree( vCexStore );
804 Vec_WrdFree( vSims );
805}
806
807
808
809
821Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia )
822{
823 Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 );
824 p->pGia = pGia;
825 p->nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
826 p->pFunc[0] = ABC_CALLOC( word, p->nWords );
827 p->pFunc[1] = ABC_CALLOC( word, p->nWords );
828 p->pFunc[2] = ABC_CALLOC( word, p->nWords );
829 p->vTfo = Vec_IntAlloc( 1000 );
830 p->vCands = Vec_IntAlloc( 1000 );
831 p->vFanins = Vec_IntAlloc( 10 );
832 p->vFanins2 = Vec_IntAlloc( 10 );
833 p->vSimsObj = Gia_ManSimPatSim( pGia );
834 p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) );
835 assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) );
836 Gia_ManStaticFanoutStart( pGia );
837 return p;
838}
839void Gia_SimRsbFree( Gia_SimRsbMan_t * p )
840{
841 Gia_ManStaticFanoutStop( p->pGia );
842 Vec_IntFree( p->vTfo );
843 Vec_IntFree( p->vCands );
844 Vec_IntFree( p->vFanins );
845 Vec_IntFree( p->vFanins2 );
846 Vec_WrdFree( p->vSimsObj );
847 Vec_WrdFree( p->vSimsObj2 );
848 ABC_FREE( p->pFunc[0] );
849 ABC_FREE( p->pFunc[1] );
850 ABC_FREE( p->pFunc[2] );
851 ABC_FREE( p );
852}
853
865void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo )
866{
867 int i, iFan;
868 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
869 return;
870 Gia_ObjSetTravIdCurrentId(p, iObj);
871 Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i )
872 if ( iFanout == -1 || iFan == iFanout )
873 Gia_SimRsbTfo_rec( p, iFan, -1, vTfo );
874 Vec_IntPush( vTfo, iObj );
875}
876Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout )
877{
878 assert( iObj > 0 );
879 Vec_IntClear( p->vTfo );
880 Gia_ManIncrementTravId( p->pGia );
881 Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo );
882 assert( Vec_IntEntryLast(p->vTfo) == iObj );
883 Vec_IntPop( p->vTfo );
884 Vec_IntReverseOrder( p->vTfo );
885 Vec_IntSort( p->vTfo, 0 );
886 return p->vTfo;
887}
888
900word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet )
901{
902 int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) );
903 word * pTruth = ABC_CALLOC( word, nTruthWords );
904 word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
905 word * pFanins[16] = {NULL}; int s, b, iMint, i, iFanin;
906 assert( Vec_IntSize(vFanins) <= 16 );
907 Vec_IntForEachEntry( vFanins, iFanin, i )
908 pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin );
909 for ( s = 0; s < 64*p->nWords; s++ )
910 {
911 if ( !Abc_TtGetBit(p->pFunc[2], s) || Abc_TtGetBit(pFunc, s) != fOnSet )
912 continue;
913 iMint = 0;
914 for ( b = 0; b < Vec_IntSize(vFanins); b++ )
915 if ( Abc_TtGetBit(pFanins[b], s) )
916 iMint |= 1 << b;
917 Abc_TtSetBit( pTruth, iMint );
918 }
919 return pTruth;
920}
921int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins )
922{
923 word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 );
924 word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 );
925 int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 );
926 ABC_FREE( pTruth0 );
927 ABC_FREE( pTruth1 );
928 return Res;
929}
930
942static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 )
943{
944 word pComps[2] = { 0, ~(word)0 };
945 word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
946 word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
947 Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims;
948 Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims;
949 word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) );
950 word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) );
951 word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w;
952 if ( Gia_ObjIsXor(pObj) )
953 for ( w = 0; w < nWords; w++ )
954 pSims2[w] = (pSims0[w] ^ Diff0) ^ (pSims1[w] ^ Diff1);
955 else
956 for ( w = 0; w < nWords; w++ )
957 pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
958}
959word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo )
960{
961 word * pSims = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
962 word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj ); int iNode, i;
963 Abc_TtCopy( pSims2, pSims, p->nWords, 1 );
964 Abc_TtClear( p->pFunc[2], p->nWords );
965 Vec_IntForEachEntry( vTfo, iNode, i )
966 {
967 Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode);
968 if ( Gia_ObjIsAnd(pNode) )
969 Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 );
970 else if ( Gia_ObjIsCo(pNode) )
971 {
972 word * pSimsA = Vec_WrdEntryP( p->vSimsObj, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
973 word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
974 Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords );
975 }
976 else assert( 0 );
977 }
978 return p->pFunc[2];
979}
980
981
993void Gia_ObjSimCollect( Gia_SimRsbMan_t * p )
994{
995 int i, k, iTemp, iFanout;
996 Vec_IntClear( p->vFanins2 );
997 assert( Vec_IntSize(p->vFanins) > 0 );
998 Vec_IntForEachEntry( p->vFanins, iTemp, i )
999 {
1000 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp );
1001 if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) )
1002 Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) );
1003 if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) )
1004 Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) );
1005 Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k )
1006 if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) )
1007 Vec_IntPush( p->vFanins2, iFanout );
1008 }
1009}
1010Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands )
1011{
1012 assert( iObj > 0 );
1013 assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) );
1014 Vec_IntClear( p->vCands );
1015 Vec_IntFill( p->vFanins, 1, iObj );
1016 while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands )
1017 {
1018 int i, iTemp;
1019 Vec_IntForEachEntry( p->vFanins, iTemp, i )
1020 Gia_ObjSetTravIdCurrentId( p->pGia, iTemp );
1021 Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2
1022 Vec_IntAppend( p->vCands, p->vFanins2 );
1023 ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 );
1024 }
1025 assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands );
1026 if ( Vec_IntSize(p->vCands) > nCands )
1027 Vec_IntShrink( p->vCands, nCands );
1028 return p->vCands;
1029}
1030
1042int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs )
1043{
1044 int i, iCand, RetValue = 0;
1045 Vec_Int_t * vTfo = Gia_SimRsbTfo( p, iObj, -1 );
1046 word * pCareSet = Gia_SimRsbCareSet( p, iObj, vTfo );
1047 word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
1048 Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands );
1049 Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 );
1050 Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 );
1051
1052/*
1053printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) );
1054Vec_IntPrint( vTfo );
1055Vec_IntPrint( vCands );
1056Extra_PrintBinary( stdout, (unsigned *)pCareSet, 64 ); printf( "\n" );
1057Extra_PrintBinary( stdout, (unsigned *)pFunc, 64 ); printf( "\n" );
1058Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 ); printf( "\n" );
1059Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 ); printf( "\n" );
1060*/
1061 Vec_IntForEachEntry( vCands, iCand, i )
1062 {
1063 word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand );
1064 if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) &&
1065 !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) )
1066 { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
1067 if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) &&
1068 !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) )
1069 { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
1070 }
1071 return RetValue;
1072}
1073
1074int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose )
1075{
1076 abctime clk = Abc_Clock();
1077 Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0;
1078 Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia );
1079 assert( pGia->vSimsPi != NULL );
1080 Gia_ManLevelNum( pGia );
1081 Gia_ManForEachAnd( pGia, pObj, iObj )
1082 //if ( iObj == 6 )
1083 nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs );
1084 printf( "Can resubstitute %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d) ",
1085 nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs );
1086 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1087 Gia_SimRsbFree( p );
1088 return nCount;
1089}
1090
1091
1092
1093
1105void Gia_ManSimRelAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsIn, Vec_Wrd_t * vSimsIn )
1106{
1107 int i, m, Id, nMints = nWords / nWordsIn;
1108 assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) );
1109 assert( Vec_WrdSize(vSimsIn) == nWordsIn * Gia_ManCiNum(p) );
1110 Gia_ManForEachCiId( p, Id, i )
1111 for ( m = 0; m < nMints; m++ )
1112 memcpy( Vec_WrdEntryP(vSims, Id * nWords + nWordsIn * m),
1113 Vec_WrdEntryP(vSimsIn, i * nWordsIn), sizeof(word) * nWordsIn );
1114}
1115int Gia_ManSimRelCompare( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, int iPat, int iMint )
1116{
1117 int i, Id;
1118 Gia_ManForEachCoId( p, Id, i )
1119 {
1120 word * pSim = Vec_WrdEntryP( vSims, nWords * Id + iMint * nWordsOut );
1121 word * pSimOut = Vec_WrdEntryP( vSimsOut, nWordsOut * i );
1122/*
1123 int k;
1124 for ( k = 0; k < 64*nWordsOut; k++ )
1125 printf( "%d", Abc_TtGetBit( pSim, k ) );
1126 printf( "\n" );
1127 for ( k = 0; k < 64*nWordsOut; k++ )
1128 printf( "%d", Abc_TtGetBit( pSimOut, k ) );
1129 printf( "\n\n" );
1130*/
1131 if ( Abc_TtGetBit(pSim, iPat) != Abc_TtGetBit(pSimOut, iPat) )
1132 return 0;
1133 }
1134 return 1;
1135}
1136int Gia_ManSimRelCollectOutputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, Vec_Wrd_t * vRel )
1137{
1138 int i, m, nMints = nWords / nWordsOut, Count = 0;
1139 assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) );
1140 assert( Vec_WrdSize(vSimsOut) == nWordsOut * Gia_ManCoNum(p) );
1141 assert( Vec_WrdSize(vRel) == nWordsOut * nMints );
1142 for ( i = 0; i < 64 * nWordsOut; i++ )
1143 {
1144 int CountMints = 0;
1145 for ( m = 0; m < nMints; m++ )
1146 if ( Gia_ManSimRelCompare(p, nWords, vSims, nWordsOut, vSimsOut, i, m) )
1147 Abc_TtSetBit( Vec_WrdArray(vRel), i*nMints+m ), CountMints++;
1148 Count += CountMints == 0;
1149 }
1150 if ( Count )
1151 printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWordsOut );
1152 return Count;
1153}
1154Vec_Wrd_t * Gia_ManSimRel( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vVals )
1155{
1156 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
1157 int nMints = 1 << Vec_IntSize(vObjs), i, m, iObj;
1158 Gia_Obj_t * pObj;
1159 Vec_Wrd_t * vRel = Vec_WrdStart( nWords * nMints );
1160 Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords * nMints );
1161 Gia_ManSimRelAssignInputs( p, nWords * nMints, vSims, nWords, p->vSimsPi );
1162 Vec_IntForEachEntry( vObjs, iObj, i )
1163 for ( m = 0; m < nMints; m++ )
1164 if ( (m >> i) & 1 )
1165 memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0xFF, sizeof(word)*nWords );
1166 else
1167 memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0x00, sizeof(word)*nWords );
1168 Gia_ManCleanPhase( p );
1169 Gia_ManForEachObjVec( vObjs, p, pObj, i )
1170 pObj->fPhase = 1;
1171 Gia_ManForEachAnd( p, pObj, i )
1172 if ( !pObj->fPhase )
1173 Gia_ManSimPatSimAnd( p, i, pObj, nWords * nMints, vSims );
1174 Gia_ManForEachCo( p, pObj, i )
1175 if ( !pObj->fPhase )
1176 Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords * nMints, vSims );
1177 Gia_ManForEachObjVec( vObjs, p, pObj, i )
1178 pObj->fPhase = 0;
1179 if ( Gia_ManSimRelCollectOutputs( p, nWords * nMints, vSims, nWords, vVals, vRel ) )
1180 Vec_WrdFreeP( &vRel );
1181 Vec_WrdFree( vSims );
1182 return vRel;
1183}
1184
1196void Gia_ManSimRelCheckFuncs( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts, Vec_Wrd_t * vFuncs )
1197{
1198 int i, k, m, Values[32], nErrors = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
1199 assert( Vec_WrdSize(vFuncs) == 2 * nOuts * nWords );
1200 assert( nOuts <= 32 );
1201 for ( i = 0; i < 64 * nWords; i++ )
1202 {
1203 for ( k = 0; k < nOuts; k++ )
1204 {
1205 int Value0 = Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i );
1206 int Value1 = Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
1207 if ( Value0 && !Value1 )
1208 Values[k] = 1;
1209 else if ( !Value0 && Value1 )
1210 Values[k] = 2;
1211 else if ( !Value0 && !Value1 )
1212 Values[k] = 3;
1213 else assert( 0 );
1214 }
1215 for ( m = 0; m < nMints; m++ )
1216 {
1217 for ( k = 0; k < nOuts; k++ )
1218 if ( ((Values[k] >> ((m >> k) & 1)) & 1) == 0 )
1219 break;
1220 if ( k < nOuts )
1221 continue;
1222 if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
1223 continue;
1224 if ( nErrors++ == 0 )
1225 printf( "For pattern %d, minterm %d produced by function is not in the relation.\n", i, m );
1226 }
1227 }
1228 if ( nErrors )
1229 printf( "Total number of similar errors = %d.\n", nErrors );
1230 else
1231 printf( "The function agrees with the relation.\n" );
1232}
1233Vec_Wrd_t * Gia_ManSimRelDeriveFuncs( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts )
1234{
1235 int i, k, m, Count = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
1236 Vec_Wrd_t * vFuncs = Vec_WrdStart( 2 * nOuts * nWords );
1237 assert( Vec_WrdSize(vRel) % nMints == 0 );
1238 for ( i = 0; i < 64 * nWords; i++ )
1239 {
1240 for ( m = 0; m < nMints; m++ )
1241 if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
1242 break;
1243 Count += m == nMints;
1244 for ( k = 0; k < nOuts; k++ )
1245 if ( (m >> k) & 1 )
1246 Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
1247 else
1248 Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i );
1249 }
1250 if ( Count )
1251 printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWords );
1252 else
1253 printf( "The relation was successfully determized without don't-cares for %d patterns.\n", 64 * nWords );
1254 Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs );
1255 return vFuncs;
1256}
1257Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts )
1258{
1259 int i, k, m, nDCs[32] = {0}, Count = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
1260 Vec_Wrd_t * vFuncs = Vec_WrdStart( 2 * nOuts * nWords );
1261 assert( Vec_WrdSize(vRel) % nMints == 0 );
1262 assert( nOuts <= 32 );
1263 for ( i = 0; i < 64 * nWords; i++ )
1264 {
1265 for ( m = 0; m < nMints; m++ )
1266 if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
1267 break;
1268 Count += m == nMints;
1269 for ( k = 0; k < nOuts; k++ )
1270 {
1271 if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+(m^(1<<k)) ) )
1272 {
1273 nDCs[k]++;
1274 continue;
1275 }
1276 if ( (m >> k) & 1 )
1277 Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
1278 else
1279 Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i );
1280 }
1281 if ( 0 )
1282 {
1283 for ( m = 0; m < nMints; m++ )
1284 printf( "%d", Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) );
1285 printf( " " );
1286 for ( k = 0; k < nOuts; k++ )
1287 {
1288 if ( Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i ) )
1289 printf( "0" );
1290 else if ( Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i ) )
1291 printf( "1" );
1292 else
1293 printf( "-" );
1294 }
1295 printf( "\n" );
1296 }
1297 }
1298 if ( Count )
1299 printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWords );
1300 else
1301 {
1302 printf( "The relation was successfully determized with don't-cares for %d patterns.\n", 64 * nWords );
1303 for ( k = 0; k < nOuts; k++ )
1304 {
1305 int nOffs = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), nWords );
1306 int nOns = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), nWords );
1307 printf( "%4d : Off = %6d On = %6d Dc = %6d (%6.2f %%)\n", k, nOffs, nOns, nDCs[k], 100.0*nDCs[k]/(64*nWords) );
1308 }
1309 printf( "\n" );
1310 }
1311 Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs );
1312 return vFuncs;
1313}
1314
1326void Gia_ManSimRelPrint( Gia_Man_t * p, Vec_Wrd_t * vRel, Vec_Int_t * vOutMints )
1327{
1328 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
1329 int nMints = Vec_WrdSize(vRel) / nWords;
1330 int i, m, Count;
1331/*
1332 for ( i = 0; i < 64 * nWords; i++ )
1333 {
1334 int k;
1335 for ( k = 0; k < Gia_ManCiNum(p); k++ )
1336 printf( "%d", Abc_TtGetBit( Vec_WrdEntryP(p->vSimsPi, k), i ) );
1337 printf( " " );
1338 Count = 0;
1339 for ( m = 0; m < nMints; m++ )
1340 {
1341 printf( "%d", Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) );
1342 Count += Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m );
1343 }
1344 printf( " Count = %2d ", Count );
1345 if ( vOutMints )
1346 {
1347 printf( " %3d ", Vec_IntEntry(vOutMints, i) );
1348 if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+Vec_IntEntry(vOutMints, i) ) )
1349 printf( "yes" );
1350 else
1351 printf( "no" );
1352 }
1353 printf( "\n" );
1354 }
1355*/
1356/*
1357 for ( i = 0; i < 64 * nWords; i++ )
1358 {
1359 Count = 0;
1360 for ( m = 0; m < nMints; m++ )
1361 Count += Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m );
1362 printf( "%d ", Count );
1363 }
1364 printf( "\n" );
1365*/
1366 for ( i = 0; i < 64 * nWords; i++ )
1367 {
1368 Count = 0;
1369 for ( m = 0; m < nMints; m++ )
1370 {
1371 printf( "%d", Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) );
1372 Count += Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m );
1373 }
1374 printf( " Count = %2d \n", Count );
1375 }
1376}
1377Vec_Int_t * Gia_ManSimPatStart( int nItems )
1378{
1379 Vec_Int_t * vValues = Vec_IntAlloc( nItems );
1380 Vec_IntPush( vValues, 17 );
1381 Vec_IntPush( vValues, 39 );
1382 Vec_IntPush( vValues, 56 );
1383 Vec_IntPush( vValues, 221 );
1384 return vValues;
1385}
1386void Gia_ManSimRelTest( Gia_Man_t * p )
1387{
1388 //int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
1389 Vec_Int_t * vObjs = Gia_ManSimPatStart( 4 ); // can be CI/AND/CO
1390 Vec_Wrd_t * vVals = Gia_ManSimPatValues( p );
1391 Vec_Wrd_t * vRel = Gia_ManSimRel( p, vObjs, vVals );
1392 assert( p->vSimsPi != NULL );
1393 Gia_ManSimRelPrint( p, vRel, NULL );
1394 Vec_IntFree( vObjs );
1395 Vec_WrdFree( vVals );
1396 Vec_WrdFree( vRel );
1397}
1398
1399
1400
1412Vec_Int_t * Gia_Sim5CollectValues( word * pOffSet, word * pOnSet, int nWords )
1413{
1414 Vec_Int_t * vBits = Vec_IntAlloc( 64*nWords ); int i, Count[2] = {0};
1415 for ( i = 0; i < 64*nWords; i++ )
1416 if ( Abc_TtGetBit( pOffSet, i ) )
1417 Vec_IntPush( vBits, 0 ), Count[0]++;
1418 else if ( Abc_TtGetBit( pOnSet, i ) )
1419 Vec_IntPush( vBits, 1 ), Count[1]++;
1420 else
1421 Vec_IntPush( vBits, -1 );
1422 //printf( "Offset = %d. Onset = %d. Dcset = %d.\n", Count[0], Count[1], 64*nWords - Count[0] - Count[1] );
1423 return vBits;
1424}
1425Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vResub, int fVerbose )
1426{
1427 Gia_SimAbsMan_t * p = ABC_CALLOC( Gia_SimAbsMan_t, 1 );
1428 p->pGia = pGia;
1429 p->pSet[0] = pOffSet;
1430 p->pSet[1] = pOnSet;
1431 p->nCands = Vec_WrdSize(vSims)/nWords;
1432 p->nWords = nWords;
1433 p->vSims = vSims;
1434 p->vResub = vResub;
1435 p->fVerbose = fVerbose;
1436 p->vValues = Gia_Sim5CollectValues( pOffSet, pOnSet, nWords );
1437 p->vPatPairs = Vec_IntAlloc( 100 );
1438 p->vCoverTable = Vec_WrdAlloc( 10000 );
1439 p->vTtMints = Vec_IntAlloc( 100 );
1440 assert( Vec_WrdSize(vSims) % nWords == 0 );
1441 return p;
1442}
1443void Gia_SimAbsFree( Gia_SimAbsMan_t * p )
1444{
1445 Vec_IntFree( p->vValues );
1446 Vec_IntFree( p->vPatPairs );
1447 Vec_WrdFree( p->vCoverTable );
1448 Vec_IntFree( p->vTtMints );
1449 ABC_FREE( p );
1450}
1451
1452
1464void Gia_SimAbsCheckSolution( Gia_SimAbsMan_t * p )
1465{
1466 int x, y, z, w, fFound = 0;
1467 assert( Vec_WrdSize(p->vCoverTable) == p->nWordsTable * (p->nCands+1) );
1468
1469 Abc_TtClear( p->pTableTemp, p->nWordsTable );
1470 for ( x = 0; x < Vec_IntSize(p->vPatPairs)/2; x++ )
1471 Abc_TtXorBit( p->pTableTemp, x );
1472
1473 for ( x = 0; x < p->nCands; x++ )
1474 {
1475 word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x );
1476 for ( w = 0; w < p->nWordsTable; w++ )
1477 if ( p->pTableTemp[w] != pSimTableX[w] )
1478 break;
1479 if ( w == p->nWordsTable )
1480 {
1481 printf( "Found solution { %d }\n", x );
1482 fFound = 1;
1483 }
1484 }
1485 if ( fFound )
1486 return;
1487
1488 for ( x = 0; x < p->nCands; x++ )
1489 for ( y = 0; y < x; y++ )
1490 {
1491 word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x );
1492 word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y );
1493 for ( w = 0; w < p->nWordsTable; w++ )
1494 if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w]) )
1495 break;
1496 if ( w == p->nWordsTable )
1497 {
1498 printf( "Found solution { %d %d }\n", y, x );
1499 fFound = 1;
1500 }
1501 }
1502 if ( fFound )
1503 return;
1504
1505 for ( x = 0; x < p->nCands; x++ )
1506 for ( y = 0; y < x; y++ )
1507 for ( z = 0; z < y; z++ )
1508 {
1509 word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x );
1510 word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y );
1511 word * pSimTableZ = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * z );
1512 for ( w = 0; w < p->nWordsTable; w++ )
1513 if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w] | pSimTableZ[w]) )
1514 break;
1515 if ( w == p->nWordsTable )
1516 printf( "Found solution { %d %d %d }\n", z, y, x );
1517 }
1518}
1519
1520void Gia_SimAbsSolve( Gia_SimAbsMan_t * p )
1521{
1522 abctime clk = Abc_Clock();
1523 int i, k, iPat, iPat2;
1524/*
1525 Vec_Int_t * vSimPats = Vec_IntDup( p->vPatPairs );
1526 Vec_IntUniqify( vSimPats );
1527 printf( "Selected %d pattern pairs contain %d unique patterns.\n", Vec_IntSize(p->vPatPairs)/2, Vec_IntSize(vSimPats) );
1528 Vec_IntFree( vSimPats );
1529*/
1530 // set up the covering problem
1531 p->nWordsTable = Abc_Bit6WordNum( Vec_IntSize(p->vPatPairs)/2 );
1532 Vec_WrdFill( p->vCoverTable, p->nWordsTable * (p->nCands + 1), 0 );
1533 p->pTableTemp = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * p->nCands );
1534 for ( i = 0; i < p->nCands; i++ )
1535 {
1536 word * pSimCand = Vec_WrdEntryP( p->vSims, p->nWords * i );
1537 word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i );
1538 //printf( "%4d : ", i );
1539 //Extra_PrintBinary( stdout, (word *)pSimCand, p->nCands ); printf( "\n" );
1540 Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, k )
1541 {
1542 assert( Vec_IntEntry(p->vValues, iPat) == 0 );
1543 assert( Vec_IntEntry(p->vValues, iPat2) == 1 );
1544 if ( Abc_TtGetBit(pSimCand, iPat) != Abc_TtGetBit(pSimCand, iPat2) )
1545 Abc_TtXorBit(pSimTable, k/2);
1546 }
1547 assert( k == Vec_IntSize(p->vPatPairs) );
1548 }
1549
1550 if ( 0 )
1551 {
1552 printf( " " );
1553 for ( i = 0; i < p->nCands; i++ )
1554 printf( "%d", i % 10 );
1555 printf( "\n" );
1556
1557 Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, i )
1558 {
1559 printf( "%4d ", i/2 );
1560 printf( "%4d ", iPat );
1561 printf( "%4d ", iPat2 );
1562 for ( k = 0; k < p->nCands; k++ )
1563 {
1564 word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * k );
1565 printf( "%c", Abc_TtGetBit(pSimTable, i/2) ? '*' : ' ' );
1566 }
1567 printf( "\n" );
1568 }
1569 }
1570
1571 //Gia_SimAbsCheckSolution(p);
1572
1573 Vec_IntClear( p->vResub );
1574 Abc_TtClear( p->pTableTemp, p->nWordsTable );
1575 for ( i = 0; i < Vec_IntSize(p->vPatPairs)/2; i++ )
1576 Abc_TtXorBit( p->pTableTemp, i );
1577
1578 while ( !Abc_TtIsConst0(p->pTableTemp, p->nWordsTable) )
1579 {
1580 word * pSimTable;
1581 int iArgMax = -1, CostThis, CostMax = -1;
1582 // compute the cost of each column
1583 for ( i = 0; i < p->nCands; i++ )
1584 {
1585 pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i );
1586 CostThis = Abc_TtCountOnesVecMask( pSimTable, p->pTableTemp, p->nWordsTable, 0 );
1587 if ( CostMax >= CostThis )
1588 continue;
1589 CostMax = CostThis;
1590 iArgMax = i;
1591 }
1592 // find the best column
1593 Vec_IntPush( p->vResub, iArgMax );
1594 // delete values of this column
1595 pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * iArgMax );
1596 Abc_TtSharp( p->pTableTemp, p->pTableTemp, pSimTable, p->nWordsTable );
1597 }
1598 if ( p->fVerbose )
1599 {
1600 printf( "Solution %2d for covering problem [%5d x %5d]: ", Vec_IntSize(p->vResub), Vec_IntSize(p->vPatPairs)/2, p->nCands );
1601 Vec_IntForEachEntry( p->vResub, iPat, i )
1602 printf( "%6d ", iPat );
1603 for ( ; i < 12; i++ )
1604 printf( " " );
1605 printf( " " );
1606 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1607 }
1608}
1609int Gia_SimAbsRefine( Gia_SimAbsMan_t * p )
1610{
1611 int i, b, Value, iPat, iMint, iObj, Count = 0;
1612 word ** pFanins = ABC_ALLOC( word *, Vec_IntSize(p->vResub) );
1613 assert( Vec_IntSize(p->vResub) > 0 );
1614 Vec_IntForEachEntry( p->vResub, iObj, b )
1615 pFanins[b] = Vec_WrdEntryP( p->vSims, p->nWords * iObj );
1616 Vec_IntFill( p->vTtMints, 1 << Vec_IntSize(p->vResub), -1 );
1617 Vec_IntForEachEntry( p->vValues, Value, i )
1618 {
1619 if ( Value == -1 )
1620 continue;
1621 iMint = 0;
1622 for ( b = 0; b < Vec_IntSize(p->vResub); b++ )
1623 if ( Abc_TtGetBit(pFanins[b], i) )
1624 iMint |= 1 << b;
1625 iPat = Vec_IntEntry( p->vTtMints, iMint );
1626 if ( iPat == -1 )
1627 {
1628 Vec_IntWriteEntry( p->vTtMints, iMint, i );
1629 continue;
1630 }
1631 assert( Abc_TtGetBit(p->pSet[Value], i) );
1632 if ( Abc_TtGetBit(p->pSet[Value], iPat) )
1633 continue;
1634 assert( Abc_TtGetBit(p->pSet[!Value], iPat) );
1635 Vec_IntPushTwo( p->vPatPairs, Value ? iPat : i, Value ? i : iPat );
1636 //printf( "iPat1 = %d iPat2 = %d Mint = %d\n", Value ? iPat : i, Value ? i : iPat, iMint );
1637 Count++;
1638 if ( Count == 64 )
1639 {
1640 ABC_FREE( pFanins );
1641 return 1;
1642 }
1643 }
1644 //printf( "Refinement added %d minterm pairs.\n", Count );
1645 ABC_FREE( pFanins );
1646 return Count != 0;
1647}
1648Vec_Int_t * Gia_SimAbsFind( Vec_Int_t * vValues, int Value )
1649{
1650 Vec_Int_t * vSubset = Vec_IntAlloc( 100 ); int i, Entry;
1651 Vec_IntForEachEntry( vValues, Entry, i )
1652 if ( Entry == Value )
1653 Vec_IntPush( vSubset, i );
1654 return vSubset;
1655}
1656void Gia_SimAbsInit( Gia_SimAbsMan_t * p )
1657{
1658 int n, nPairsInit = 64;
1659 Vec_Int_t * vValue0 = Gia_SimAbsFind( p->vValues, 0 );
1660 Vec_Int_t * vValue1 = Gia_SimAbsFind( p->vValues, 1 );
1661 Vec_IntClear( p->vPatPairs );
1662 printf( "There are %d offset and %d onset minterms (%d pairs) and %d divisors.\n",
1663 Vec_IntSize(vValue0), Vec_IntSize(vValue1), Vec_IntSize(vValue0)*Vec_IntSize(vValue1), p->nCands );
1664 Abc_Random( 1 );
1665 assert( Vec_IntSize(vValue0) > 0 );
1666 assert( Vec_IntSize(vValue1) > 0 );
1667 for ( n = 0; n < nPairsInit; n++ )
1668 Vec_IntPushTwo( p->vPatPairs,
1669 Vec_IntEntry(vValue0, Abc_Random(0) % Vec_IntSize(vValue0)),
1670 Vec_IntEntry(vValue1, Abc_Random(0) % Vec_IntSize(vValue1)) );
1671 Vec_IntFree( vValue0 );
1672 Vec_IntFree( vValue1 );
1673}
1674
1686Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSimsCands, int nWords, int fVerbose )
1687{
1688 abctime clk = Abc_Clock();
1689 Vec_Int_t * vResub = Vec_IntAlloc( 10 );
1690 Gia_SimAbsMan_t * p = Gia_SimAbsAlloc( pGia, pOffSet, pOnSet, vSimsCands, nWords, vResub, fVerbose );
1691 Gia_SimAbsInit( p );
1692 while ( 1 )
1693 {
1694 Gia_SimAbsSolve( p );
1695 if ( !Gia_SimAbsRefine( p ) )
1696 break;
1697 }
1698 Gia_SimAbsFree( p );
1699 Abc_PrintTime( 1, "Resubstitution time", Abc_Clock() - clk );
1700 return vResub;
1701}
1702
1703
1704
1716
1717typedef struct Gia_RsbMan_t_ Gia_RsbMan_t;
1734Gia_RsbMan_t * Gia_RsbAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Wrd_t * vSimsT, int nWordsT, Vec_Int_t * vCands )
1735{
1736 int i, iObj;
1737 Gia_RsbMan_t * p = ABC_CALLOC( Gia_RsbMan_t, 1 );
1738 assert( nWords <= 1024 );
1739 assert( Vec_WrdSize(vSims) == 64 * nWords * nWordsT );
1740 assert( Vec_WrdSize(vSims) == Vec_WrdSize(vSimsT) );
1741 p->pGia = pGia;
1742 p->pOffSet = pOffSet;
1743 p->pOnSet = pOnSet;
1744 p->nWords = nWords;
1745 p->nWordsT = nWordsT;
1746 p->vSims = vSims;
1747 p->vSimsT = vSimsT;
1748 p->vCands = vCands;
1749 p->vObjs = Vec_IntAlloc( 100 );
1750 p->vObjs2 = Vec_IntAlloc( 100 );
1751 p->vSets[0] = Vec_WecAlloc( 1024 );
1752 p->vSets[1] = Vec_WecAlloc( 1024 );
1753 p->pSet[0] = ABC_CALLOC( word, nWordsT );
1754 p->pSet[1] = ABC_CALLOC( word, nWordsT );
1755 p->pSet[2] = ABC_CALLOC( word, nWordsT );
1756 p->vActive = Vec_IntAlloc( 100 );
1757 Vec_IntForEachEntry( vCands, iObj, i )
1758 {
1759 assert( iObj < nWordsT * 64 );
1760 Abc_TtSetBit( p->pSet[0], iObj );
1761 }
1762 Vec_WecPushLevel( p->vSets[0] );
1763 Vec_WecPushLevel( p->vSets[1] );
1764 for ( i = 0; i < 64*nWords; i++ )
1765 {
1766 int Value0 = Abc_TtGetBit( pOffSet, i );
1767 int Value1 = Abc_TtGetBit( pOnSet, i );
1768 if ( Value0 && !Value1 )
1769 Vec_WecPush( p->vSets[0], 0, i );
1770 else if ( !Value0 && Value1 )
1771 Vec_WecPush( p->vSets[1], 0, i );
1772 else assert( !Value0 || !Value1 );
1773 }
1774 assert( Vec_WecSize(p->vSets[0]) == 1 );
1775 assert( Vec_WecSize(p->vSets[1]) == 1 );
1776 Abc_Random( 1 );
1777 //Extra_PrintBinary2( stdout, (unsigned*)pOffSet, 64*nWords ); printf( "\n" );
1778 //Extra_PrintBinary2( stdout, (unsigned*)pOnSet, 64*nWords ); printf( "\n" );
1779 return p;
1780}
1781void Gia_RsbFree( Gia_RsbMan_t * p )
1782{
1783 Vec_IntFree( p->vActive );
1784 Vec_IntFree( p->vObjs );
1785 Vec_IntFree( p->vObjs2 );
1786 Vec_WecFree( p->vSets[0] );
1787 Vec_WecFree( p->vSets[1] );
1788 ABC_FREE( p->pSet[0] );
1789 ABC_FREE( p->pSet[1] );
1790 ABC_FREE( p->pSet[2] );
1791 ABC_FREE( p );
1792}
1793
1794
1795int Gia_RsbCost( Gia_RsbMan_t * p )
1796{
1797 Vec_Int_t * vLevel[2]; int i, Cost = 0;
1798 Vec_WecForEachLevelTwo( p->vSets[0], p->vSets[1], vLevel[0], vLevel[1], i )
1799 Cost += Vec_IntSize(vLevel[0]) * Vec_IntSize(vLevel[1]);
1800 return Cost;
1801}
1802void Gia_RsbPrint( Gia_RsbMan_t * p )
1803{
1804 Vec_Int_t * vLevel[2];
1805 int n, i, nLeaves = 1 << Vec_IntSize(p->vObjs);
1806 assert( Vec_WecSize(p->vSets[0]) == nLeaves );
1807 assert( Vec_WecSize(p->vSets[1]) == nLeaves );
1808 printf( "Database for %d objects and cost %d:\n", Vec_IntSize(p->vObjs), Gia_RsbCost(p) );
1809 Vec_WecForEachLevelTwo( p->vSets[0], p->vSets[1], vLevel[0], vLevel[1], i )
1810 {
1811 for ( n = 0; n < 2; n++ )
1812 {
1813 printf( "%5d : ", i );
1814 Extra_PrintBinary2( stdout, (unsigned*)&i, Vec_IntSize(p->vObjs) ); printf( " %d ", n );
1815 Vec_IntPrint( vLevel[n] );
1816 }
1817 }
1818}
1819void Gia_RsbUpdateAdd( Gia_RsbMan_t * p, int iObj )
1820{
1821 int n, i, nLeaves = 1 << Vec_IntSize(p->vObjs);
1822 assert( Vec_WecSize(p->vSets[0]) == nLeaves );
1823 assert( Vec_WecSize(p->vSets[1]) == nLeaves );
1824 for ( i = 0; i < nLeaves; i++ )
1825 {
1826 for ( n = 0; n < 2; n++ )
1827 {
1828 Vec_Int_t * vLevelN = Vec_WecPushLevel(p->vSets[n]);
1829 Vec_Int_t * vLevel = Vec_WecEntry(p->vSets[n], i);
1830 int iMint, j, k = 0;
1831 Vec_IntForEachEntry( vLevel, iMint, j )
1832 {
1833 if ( Abc_TtGetBit(Vec_WrdEntryP(p->vSims, p->nWords*iObj), iMint) )
1834 Vec_IntPush( vLevelN, iMint );
1835 else
1836 Vec_IntWriteEntry( vLevel, k++, iMint );
1837 }
1838 Vec_IntShrink( vLevel, k );
1839 }
1840 }
1841 Vec_IntPush( p->vObjs, iObj );
1842 assert( Vec_WecSize(p->vSets[0]) == 2*nLeaves );
1843 assert( Vec_WecSize(p->vSets[1]) == 2*nLeaves );
1844}
1845void Gia_RsbUpdateRemove( Gia_RsbMan_t * p, int Index )
1846{
1847 Vec_Int_t * vLevel[2], * vTemp[2][2];
1848 int k = 0, m, m2, nLeaves = 1 << Vec_IntSize(p->vObjs);
1849 assert( Index < Vec_IntSize(p->vObjs) );
1850 assert( Vec_WecSize(p->vSets[0]) == nLeaves );
1851 assert( Vec_WecSize(p->vSets[1]) == nLeaves );
1852 for ( m = 0; m < nLeaves; m++ )
1853 {
1854 if ( m & (1 << Index) )
1855 continue;
1856 m2 = m ^ (1 << Index);
1857 vTemp[0][0] = Vec_WecEntry(p->vSets[0], m);
1858 vTemp[0][1] = Vec_WecEntry(p->vSets[1], m);
1859 vTemp[1][0] = Vec_WecEntry(p->vSets[0], m2);
1860 vTemp[1][1] = Vec_WecEntry(p->vSets[1], m2);
1861 Vec_IntAppend( vTemp[0][0], vTemp[1][0] );
1862 Vec_IntAppend( vTemp[0][1], vTemp[1][1] );
1863 Vec_IntClear( vTemp[1][0] );
1864 Vec_IntClear( vTemp[1][1] );
1865 }
1866 Vec_IntDrop( p->vObjs, Index );
1867 Vec_WecForEachLevelTwo( p->vSets[0], p->vSets[1], vLevel[0], vLevel[1], m )
1868 {
1869 if ( m & (1 << Index) )
1870 continue;
1871 ABC_SWAP( Vec_Int_t, Vec_WecArray(p->vSets[0])[k], Vec_WecArray(p->vSets[0])[m] );
1872 ABC_SWAP( Vec_Int_t, Vec_WecArray(p->vSets[1])[k], Vec_WecArray(p->vSets[1])[m] );
1873 k++;
1874 }
1875 assert( k == nLeaves/2 );
1876 Vec_WecShrink( p->vSets[0], k );
1877 Vec_WecShrink( p->vSets[1], k );
1878}
1879int Gia_RsbRemovalCost( Gia_RsbMan_t * p, int Index )
1880{
1881 Vec_Int_t * vTemp[2][2];
1882 //unsigned Mask = Abc_InfoMask( Index );
1883 int m, m2, Cost = 0, nLeaves = 1 << Vec_IntSize(p->vObjs);
1884 assert( Vec_WecSize(p->vSets[0]) == (1 << Vec_IntSize(p->vObjs)) );
1885 assert( Vec_WecSize(p->vSets[1]) == (1 << Vec_IntSize(p->vObjs)) );
1886 for ( m = 0; m < nLeaves; m++ )
1887 {
1888 if ( m & (1 << Index) )
1889 continue;
1890 m2 = m ^ (1 << Index);
1891 vTemp[0][0] = Vec_WecEntry(p->vSets[0], m);
1892 vTemp[0][1] = Vec_WecEntry(p->vSets[1], m);
1893 vTemp[1][0] = Vec_WecEntry(p->vSets[0], m2);
1894 vTemp[1][1] = Vec_WecEntry(p->vSets[1], m2);
1895 Cost += (Vec_IntSize(vTemp[0][0]) + Vec_IntSize(vTemp[1][0])) * (Vec_IntSize(vTemp[0][1]) + Vec_IntSize(vTemp[1][1]));
1896 }
1897 return Cost;
1898}
1899int Gia_RsbFindNodeToRemove( Gia_RsbMan_t * p, int * pMinCost )
1900{
1901 int i, iObj, iMin = -1, CostMin = ABC_INFINITY;
1902 Vec_IntForEachEntry( p->vObjs, iObj, i )
1903 {
1904 int Cost = Gia_RsbRemovalCost( p, i );
1905 if ( CostMin > Cost )
1906 {
1907 CostMin = Cost;
1908 iMin = i;
1909 }
1910 }
1911 if ( pMinCost )
1912 *pMinCost = CostMin;
1913 return iMin;
1914}
1915
1916void Gia_RsbFindMints( Gia_RsbMan_t * p, int * pMint0, int * pMint1 )
1917{
1918 int iSetI = Abc_Random(0) % Vec_IntSize(p->vActive);
1919 int iSet = Vec_IntEntry( p->vActive, iSetI );
1920 Vec_Int_t * vArray0 = Vec_WecEntry(p->vSets[0], iSet);
1921 Vec_Int_t * vArray1 = Vec_WecEntry(p->vSets[1], iSet);
1922 int iMint0i = Abc_Random(0) % Vec_IntSize(vArray0);
1923 int iMint1i = Abc_Random(0) % Vec_IntSize(vArray1);
1924 int iMint0 = Vec_IntEntry( vArray0, iMint0i );
1925 int iMint1 = Vec_IntEntry( vArray1, iMint1i );
1926 *pMint0 = iMint0;
1927 *pMint1 = iMint1;
1928}
1929int Gia_RsbFindNode( Gia_RsbMan_t * p )
1930{
1931 int i, iObj, nNodes, nNodesNew = -1, nNodesOld = -1, Mint0, Mint1, Shift;
1932 Abc_TtCopy( p->pSet[1], p->pSet[0], p->nWordsT, 0 );
1933 Vec_IntForEachEntry( p->vObjs, iObj, i )
1934 {
1935 assert( Abc_TtGetBit(p->pSet[1], iObj) );
1936 Abc_TtXorBit(p->pSet[1], iObj);
1937 }
1938 Abc_TtCopy( p->pSet[2], p->pSet[1], p->nWordsT, 0 );
1939 Gia_RsbFindMints( p, &Mint0, &Mint1 );
1940 nNodes = Abc_TtAndXorSum( p->pSet[1], Vec_WrdEntryP(p->vSimsT, p->nWordsT*Mint0), Vec_WrdEntryP(p->vSimsT, p->nWordsT*Mint1), p->nWordsT );
1941 for ( i = 0; i < 5 && nNodes > 1; i++ )
1942 {
1943 nNodesOld = nNodes;
1944 Abc_TtCopy( p->pSet[2], p->pSet[1], p->nWordsT, 0 );
1945 Gia_RsbFindMints( p, &Mint0, &Mint1 );
1946 nNodesNew = Abc_TtAndXorSum( p->pSet[1], Vec_WrdEntryP(p->vSimsT, p->nWordsT*Mint0), Vec_WrdEntryP(p->vSimsT, p->nWordsT*Mint1), p->nWordsT );
1947 assert( nNodesNew <= nNodes );
1948 if ( nNodesNew < nNodes )
1949 i = 0;
1950 nNodes = nNodesNew;
1951 }
1952 Shift = Abc_Random(0) % (64*p->nWordsT);
1953 for ( i = 0; i < 64*p->nWordsT; i++ )
1954 {
1955 int Index = (i+Shift) % (64*p->nWordsT);
1956 if ( Abc_TtGetBit( p->pSet[2], Index ) )
1957 return Index;
1958 }
1959 assert( 0 );
1960 return -1;
1961}
1962int Gia_RsbCollectValid( Gia_RsbMan_t * p )
1963{
1964 Vec_Int_t * vLevel[2]; int i;
1965 Vec_IntClear( p->vActive );
1966 assert( Vec_WecSize(p->vSets[0]) == Vec_WecSize(p->vSets[1]) );
1967 Vec_WecForEachLevelTwo( p->vSets[0], p->vSets[1], vLevel[0], vLevel[1], i )
1968 if ( Vec_IntSize(vLevel[0]) && Vec_IntSize(vLevel[1]) )
1969 Vec_IntPush( p->vActive, i );
1970 if ( Vec_IntSize(p->vActive) == 0 )
1971 return 0;
1972 return 1;
1973}
1974Vec_Int_t * Gia_RsbSolve( Gia_RsbMan_t * p )
1975{
1976 int i, iMin;
1977 Vec_IntClear( p->vObjs );
1978 while ( Gia_RsbCollectValid(p) )
1979 Gia_RsbUpdateAdd( p, Gia_RsbFindNode(p) );
1980 for ( i = 0; i < 100; i++ )
1981 {
1982 int k, nUndo = 1 + Abc_Random(0) % Vec_IntSize(p->vObjs);
1983 for ( k = 0; k < nUndo; k++ )
1984 {
1985 iMin = Gia_RsbFindNodeToRemove( p, NULL );// &MinCost );
1986 Gia_RsbUpdateRemove( p, iMin );
1987 }
1988 while ( Gia_RsbCollectValid(p) )
1989 Gia_RsbUpdateAdd( p, Gia_RsbFindNode(p) );
1990 if ( Vec_IntSize(p->vObjs2) == 0 || Vec_IntSize(p->vObjs2) > Vec_IntSize(p->vObjs) )
1991 {
1992 Vec_IntClear( p->vObjs2 );
1993 Vec_IntAppend( p->vObjs2, p->vObjs );
1994 }
1995 }
1996 //Gia_RsbPrint( p );
1997 return Vec_IntDup( p->vObjs2 );
1998}
1999Vec_Int_t * Gia_RsbSetFind( word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Wrd_t * vSimsT, int nWordsT, Vec_Int_t * vCands )
2000{
2001 Gia_RsbMan_t * p = Gia_RsbAlloc( NULL, pOffSet, pOnSet, vSims, nWords, vSimsT, nWordsT, vCands );
2002 Vec_Int_t * vObjs = Gia_RsbSolve( p );
2003 Gia_RsbFree( p );
2004 Vec_IntSort( vObjs, 0 );
2005 return vObjs;
2006}
2007
2019Vec_Int_t * Gia_SimQualityOne( Gia_Man_t * p, Vec_Int_t * vPat, int fPoOnly )
2020{
2021 int i, Id, Value, nWords = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
2022 Vec_Wrd_t * vTemp, * vSims, * vSimsPi = Vec_WrdStart( Gia_ManCiNum(p) * nWords );
2023 Vec_Int_t * vRes;
2024 assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
2025 Vec_IntForEachEntry( vPat, Value, i )
2026 {
2027 word * pSim = Vec_WrdEntryP( vSimsPi, i*nWords );
2028 if ( Value )
2029 Abc_TtFill( pSim, nWords );
2030 Abc_TtXorBit( pSim, i+1 );
2031 }
2032 vTemp = p->vSimsPi;
2033 p->vSimsPi = vSimsPi;
2034 vSims = Gia_ManSimPatSim( p );
2035 p->vSimsPi = vTemp;
2036 if ( fPoOnly )
2037 {
2038 vRes = Vec_IntStart( Gia_ManCoNum(p) );
2039 Gia_ManForEachCoId( p, Id, i )
2040 {
2041 word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
2042 if ( pSim[0] & 1 )
2043 Abc_TtNot( pSim, nWords );
2044 Vec_IntWriteEntry( vRes, i, Abc_TtCountOnesVec(pSim, nWords) );
2045 }
2046 assert( Vec_IntSize(vRes) == Gia_ManCoNum(p) );
2047 }
2048 else
2049 {
2050 vRes = Vec_IntStart( Gia_ManObjNum(p) );
2051 Gia_ManForEachAndId( p, Id )
2052 {
2053 word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
2054 if ( pSim[0] & 1 )
2055 Abc_TtNot( pSim, nWords );
2056 Vec_IntWriteEntry( vRes, Id, Abc_TtCountOnesVec(pSim, nWords) );
2057 }
2058 assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
2059 }
2060 Vec_WrdFree( vSims );
2061 Vec_WrdFree( vSimsPi );
2062 return vRes;
2063}
2064void Gia_SimQualityTest( Gia_Man_t * p )
2065{
2066 Vec_Int_t * vPat, * vRes;
2067 int k, m, nMints = (1 << Gia_ManCiNum(p));
2068 assert( Gia_ManCiNum(p) <= 10 );
2069 for ( m = 0; m < nMints; m++ )
2070 {
2071 printf( "%d : ", m );
2072 Extra_PrintBinary( stdout, (unsigned*)&m, Gia_ManCiNum(p) );
2073 printf( " " );
2074 vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
2075 for ( k = 0; k < Gia_ManCiNum(p); k++ )
2076 Vec_IntPush( vPat, (m >> k) & 1 );
2077 vRes = Gia_SimQualityOne( p, vPat, 1 );
2078 printf( "%d ", Vec_IntSum(vRes) );
2079 Vec_IntFree( vRes );
2080 Vec_IntFree( vPat );
2081 printf( "\n" );
2082 }
2083}
2084Vec_Int_t * Gia_SimGenerateStats( Gia_Man_t * p )
2085{
2086 Vec_Int_t * vTotal = Vec_IntStart( Gia_ManObjNum(p) );
2087 Vec_Int_t * vRes, * vPat;
2088 int i, k, Value;
2089 Abc_Random(1);
2090 for ( i = 0; i < 1000; i++ )
2091 {
2092 vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
2093 for ( k = 0; k < Gia_ManCiNum(p); k++ )
2094 Vec_IntPush( vPat, Abc_Random(0) & 1 );
2095 vRes = Gia_SimQualityOne( p, vPat, 0 );
2096 assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
2097 Vec_IntForEachEntry( vRes, Value, k )
2098 Vec_IntAddToEntry( vTotal, k, Value );
2099 Vec_IntFree( vRes );
2100 Vec_IntFree( vPat );
2101 }
2102 //Vec_IntPrint( vTotal );
2103 return vTotal;
2104}
2105double Gia_SimComputeScore( Gia_Man_t * p, Vec_Int_t * vTotal, Vec_Int_t * vThis )
2106{
2107 double TotalScore = 0;
2108 int i, Total, This;
2109 assert( Vec_IntSize(vTotal) == Vec_IntSize(vThis) );
2110 Vec_IntForEachEntryTwo( vTotal, vThis, Total, This, i )
2111 {
2112 if ( Total == 0 )
2113 Total = 1;
2114 TotalScore += 1000.0*This/Total;
2115 }
2116 return TotalScore == 0 ? 1.0 : TotalScore/Gia_ManAndNum(p);
2117}
2118int Gia_SimQualityPatternsMax( Gia_Man_t * p, Vec_Int_t * vPat, int Iter, int fVerbose, Vec_Int_t * vStats )
2119{
2120 int k, MaxIn = -1;
2121 Vec_Int_t * vTries = Vec_IntAlloc( 100 );
2122 Vec_Int_t * vRes = Gia_SimQualityOne( p, vPat, 0 );
2123 double Value, InitValue, MaxValue = InitValue = Gia_SimComputeScore( p, vStats, vRes );
2124 Vec_IntFree( vRes );
2125
2126 if ( fVerbose )
2127 printf( "Iter %5d : Init = %6.3f ", Iter, InitValue );
2128
2129 for ( k = 0; k < Gia_ManCiNum(p); k++ )
2130 {
2131 Vec_IntArray(vPat)[k] ^= 1;
2132 //Vec_IntPrint( vPat );
2133
2134 vRes = Gia_SimQualityOne( p, vPat, 0 );
2135 Value = Gia_SimComputeScore( p, vStats, vRes );
2136 if ( MaxValue <= Value )
2137 {
2138 if ( MaxValue < Value )
2139 Vec_IntClear( vTries );
2140 Vec_IntPush( vTries, k );
2141 MaxValue = Value;
2142 MaxIn = k;
2143 }
2144 Vec_IntFree( vRes );
2145
2146 Vec_IntArray(vPat)[k] ^= 1;
2147 }
2148 MaxIn = Vec_IntSize(vTries) ? Vec_IntEntry( vTries, rand()%Vec_IntSize(vTries) ) : -1;
2149 if ( fVerbose )
2150 {
2151 printf( "Final = %6.3f Ratio = %4.2f Tries = %5d ", MaxValue, MaxValue/InitValue, Vec_IntSize(vTries) );
2152 printf( "Choosing %5d\r", MaxIn );
2153 }
2154 Vec_IntFree( vTries );
2155 return MaxIn;
2156}
2157Vec_Int_t * Gia_ManPatCollectOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords )
2158{
2159 Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) ); int k;
2160 for ( k = 0; k < Gia_ManCiNum(p); k++ )
2161 Vec_IntPush( vPat, Abc_TtGetBit( Vec_WrdEntryP(vPatterns, k*nWords), n ) );
2162 return vPat;
2163}
2164void Gia_ManPatUpdateOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords, Vec_Int_t * vPat )
2165{
2166 int k, Value;
2167 Vec_IntForEachEntry( vPat, Value, k )
2168 {
2169 word * pSim = Vec_WrdEntryP( vPatterns, k*nWords );
2170 if ( Abc_TtGetBit(pSim, n) != Value )
2171 Abc_TtXorBit( pSim, n );
2172 }
2173}
2174void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose )
2175{
2176 int n, k, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
2177 double InitValue, InitTotal = 0, FinalValue, FinalTotal = 0;
2178 Vec_Int_t * vPat, * vRes, * vStats = Gia_SimGenerateStats( p );
2179 Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
2180 Abc_Random(1);
2181 for ( n = 0; n < 64*nWords; n++ )
2182 {
2183 abctime clk = Abc_Clock();
2184// if ( n == 32 )
2185// break;
2186
2187 vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
2188 vRes = Gia_SimQualityOne( p, vPat, 0 );
2189 InitValue = Gia_SimComputeScore(p, vStats, vRes);
2190 InitTotal += InitValue;
2191 Vec_IntFree( vRes );
2192
2193 for ( k = 0; k < 100; k++ )
2194 {
2195 int MaxIn = Gia_SimQualityPatternsMax( p, vPat, k, fVerbose, vStats );
2196 if ( MaxIn == -1 )
2197 break;
2198 assert( MaxIn >= 0 && MaxIn < Gia_ManCiNum(p) );
2199 Vec_IntArray(vPat)[MaxIn] ^= 1;
2200 }
2201 //Vec_IntPrint( vPat );
2202
2203 vRes = Gia_SimQualityOne( p, vPat, 0 );
2204 FinalValue = Gia_SimComputeScore(p, vStats, vRes);
2205 FinalTotal += FinalValue;
2206 Vec_IntFree( vRes );
2207
2208 if ( fVerbose )
2209 {
2210 printf( "Pat %5d : Tries = %5d InitValue = %6.3f FinalValue = %6.3f Ratio = %4.2f ",
2211 n, k, InitValue, FinalValue, FinalValue/InitValue );
2212 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2213 }
2214
2215 Gia_ManPatUpdateOne( p, vPatterns, n, nWords, vPat );
2216 Vec_IntFree( vPat );
2217 }
2218 Vec_IntFree( vStats );
2219 if ( fVerbose )
2220 printf( "\n" );
2221 printf( "Improved %d patterns with average init value %.2f and average final value %.2f.\n",
2222 64*nWords, 1.0*InitTotal/(64*nWords), 1.0*FinalTotal/(64*nWords) );
2223 p->vSimsPi = vPatterns;
2224}
2225
2237Vec_Int_t * Gia_SimCollectRare( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int RareLimit )
2238{
2239 Vec_Int_t * vRareCounts = Vec_IntAlloc( 100 ); // (node, rare_count) pairs
2240 int Id, nWords = Vec_WrdSize(vPatterns) / Gia_ManCiNum(p), TotalBits = 64*nWords;
2241 Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
2242 assert( Vec_WrdSize(vPatterns) % Gia_ManCiNum(p) == 0 );
2243 p->vSimsPi = vPatterns;
2244 vSims = Gia_ManSimPatSim( p );
2245 p->vSimsPi = vTemp;
2246 Gia_ManForEachAndId( p, Id )
2247 {
2248 word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
2249 int Count = Abc_TtCountOnesVec( pSim, nWords );
2250 int fRareOne = Count < TotalBits/2; // fRareOne is 1 if rare value is 1
2251 int CountRare = fRareOne ? Count : TotalBits - Count;
2252 assert( CountRare <= TotalBits/2 );
2253 if ( CountRare <= RareLimit )
2254 Vec_IntPushTwo( vRareCounts, Abc_Var2Lit(Id, fRareOne), CountRare );
2255 }
2256 Vec_WrdFree( vSims );
2257 return vRareCounts;
2258}
2259Vec_Flt_t * Gia_SimQualityImpact( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vRareCounts )
2260{
2261 Vec_Flt_t * vQuoIncs = Vec_FltStart( Gia_ManCiNum(p) );
2262 int nWordsNew = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
2263 Vec_Wrd_t * vSimsPiNew = Vec_WrdStart( Gia_ManCiNum(p) * nWordsNew );
2264 Vec_Wrd_t * vTemp, * vSims;
2265 int i, k, Value, RareLit, RareCount;
2266 assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
2267 Vec_IntForEachEntry( vPat, Value, i )
2268 {
2269 word * pSim = Vec_WrdEntryP( vSimsPiNew, i*nWordsNew );
2270 if ( Value )
2271 Abc_TtFill( pSim, nWordsNew );
2272 Abc_TtXorBit( pSim, i+1 );
2273 }
2274 vTemp = p->vSimsPi;
2275 p->vSimsPi = vSimsPiNew;
2276 vSims = Gia_ManSimPatSim( p );
2277 p->vSimsPi = vTemp;
2278 Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
2279 {
2280 float Incrm = (float)1.0/(RareCount+1);
2281 int RareObj = Abc_Lit2Var(RareLit);
2282 int RareVal = Abc_LitIsCompl(RareLit);
2283 word * pSim = Vec_WrdEntryP( vSims, RareObj*nWordsNew );
2284 int OrigVal = pSim[0] & 1;
2285 if ( OrigVal )
2286 Abc_TtNot( pSim, nWordsNew );
2287 for ( k = 0; k < Gia_ManCiNum(p); k++ )
2288 if ( Abc_TtGetBit(pSim, k+1) ) // value changed
2289 Vec_FltAddToEntry( vQuoIncs, k, OrigVal != RareVal ? Incrm : -Incrm );
2290 }
2291 Vec_WrdFree( vSims );
2292 Vec_WrdFree( vSimsPiNew );
2293 return vQuoIncs;
2294}
2295Vec_Int_t * Gia_SimCollectBest( Vec_Flt_t * vQuo )
2296{
2297 Vec_Int_t * vRes; int i;
2298 float Value, ValueMax = Vec_FltFindMax( vQuo );
2299 if ( ValueMax <= 0 )
2300 return NULL;
2301 vRes = Vec_IntAlloc( 100 ); // variables with max quo
2302 Vec_FltForEachEntry( vQuo, Value, i )
2303 if ( Value == ValueMax )
2304 Vec_IntPush( vRes, i );
2305 return vRes;
2306}
2307float Gia_ManPatGetQuo( Gia_Man_t * p, Vec_Int_t * vRareCounts, Vec_Wrd_t * vSims, int n, int nWords )
2308{
2309 float Quality = 0;
2310 int RareLit, RareCount, i;
2311 assert( Vec_WrdSize(vSims) == Gia_ManObjNum(p) );
2312 Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
2313 {
2314 float Incrm = (float)1.0/(RareCount+1);
2315 int RareObj = Abc_Lit2Var(RareLit);
2316 int RareVal = Abc_LitIsCompl(RareLit);
2317 word * pSim = Vec_WrdEntryP( vSims, RareObj*nWords );
2318 if ( Abc_TtGetBit(pSim, n) == RareVal )
2319 Quality += Incrm;
2320 }
2321 return Quality;
2322}
2323float Gia_ManPatGetTotalQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords )
2324{
2325 float Total = 0; int n;
2326 Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
2327 Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
2328 p->vSimsPi = vPatterns;
2329 vSims = Gia_ManSimPatSim( p );
2330 p->vSimsPi = vTemp;
2331 for ( n = 0; n < 64*nWords; n++ )
2332 Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
2333 Vec_IntFree( vRareCounts );
2334 Vec_WrdFree( vSims );
2335 return Total;
2336}
2337float Gia_ManPatGetOneQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords, int n )
2338{
2339 float Total = 0;
2340 Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
2341 Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
2342 p->vSimsPi = vPatterns;
2343 vSims = Gia_ManSimPatSim( p );
2344 p->vSimsPi = vTemp;
2345 Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
2346 Vec_IntFree( vRareCounts );
2347 Vec_WrdFree( vSims );
2348 return Total;
2349}
2350void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose )
2351{
2352 abctime clk = Abc_Clock();
2353 float FinalTotal, InitTotal;
2354 int n, nRares = 0, nChanges = 0, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
2355 Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
2356 InitTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
2357 for ( n = 0; n < 64*nWords; n++ )
2358 {
2359 abctime clk = Abc_Clock();
2360 Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
2361 Vec_Int_t * vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
2362 Vec_Flt_t * vQuoIncs = Gia_SimQualityImpact( p, vPat, vRareCounts );
2363 Vec_Int_t * vBest = Gia_SimCollectBest( vQuoIncs );
2364 if ( fVerbose )
2365 {
2366 float PatQuo = Gia_ManPatGetOneQuo( p, RareLimit, vPatterns, nWords, n );
2367 printf( "Pat %5d : Rare = %4d Cands = %3d Value = %8.3f Change = %8.3f ",
2368 n, Vec_IntSize(vRareCounts)/2, vBest ? Vec_IntSize(vBest) : 0,
2369 PatQuo, vBest ? Vec_FltEntry(vQuoIncs, Vec_IntEntry(vBest,0)) : 0 );
2370 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2371 }
2372 if ( vBest != NULL )
2373 {
2374 int VarBest = Vec_IntEntry( vBest, rand()%Vec_IntSize(vBest) );
2375 Abc_TtXorBit( Vec_WrdEntryP(vPatterns, VarBest*nWords), n );
2376 nChanges++;
2377 }
2378 nRares = Vec_IntSize(vRareCounts)/2;
2379 Vec_IntFree( vRareCounts );
2380 Vec_IntFree( vPat );
2381 Vec_FltFree( vQuoIncs );
2382 Vec_IntFreeP( &vBest );
2383 }
2384 if ( fVerbose )
2385 printf( "\n" );
2386 FinalTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
2387 p->vSimsPi = vPatterns;
2388
2389 printf( "Improved %d out of %d patterns using %d rare nodes: %.2f -> %.2f. ",
2390 nChanges, 64*nWords, nRares, InitTotal, FinalTotal );
2391 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2392}
2393
2405void Gia_ManSimTest( Gia_Man_t * pGia )
2406{
2407 int n, nWords = 4;
2408 Vec_Wrd_t * vSim1, * vSim2;
2409 Vec_Wrd_t * vSim0 = Vec_WrdStartRandom( Gia_ManCiNum(pGia) * nWords );
2410 abctime clk = Abc_Clock();
2411
2412 pGia->vSimsPi = vSim0;
2413 for ( n = 0; n < 20; n++ )
2414 {
2415 vSim1 = Gia_ManSimPatSim( pGia );
2416 Vec_WrdFree( vSim1 );
2417 }
2418 Abc_PrintTime( 1, "Time1", Abc_Clock() - clk );
2419
2420 clk = Abc_Clock();
2421 for ( n = 0; n < 20; n++ )
2422 {
2423 vSim2 = Gia_ManSimPatSim2( pGia );
2424 Vec_WrdFree( vSim2 );
2425 }
2426 Abc_PrintTime( 1, "Time2", Abc_Clock() - clk );
2427
2428 pGia->vSimsPi = NULL;
2429 Vec_WrdFree( vSim0 );
2430}
2431
2443void Gia_ManSimGen( Gia_Man_t * pGia )
2444{
2445 int nWords = 4;
2446 Gia_Obj_t * pObj;
2447 Vec_Wrd_t * vSim0 = Vec_WrdStartRandom( Gia_ManCiNum(pGia) * nWords );
2448 FILE * pFile = fopen( "comp_sim.c", "wb" );
2449 int i, k, Id;
2450 fprintf( pFile, "#include <stdio.h>\n" );
2451 fprintf( pFile, "#include <stdlib.h>\n" );
2452 fprintf( pFile, "#include <time.h>\n" );
2453 fprintf( pFile, "int main()\n" );
2454 fprintf( pFile, "{\n" );
2455 fprintf( pFile, " clock_t clkThis = clock();\n" );
2456 fprintf( pFile, " unsigned long Res = 0;\n" );
2457 fprintf( pFile, " int i;\n" );
2458 fprintf( pFile, " srand(time(NULL));\n" );
2459 fprintf( pFile, " for ( i = 0; i < 2000; i++ )\n" );
2460 fprintf( pFile, " {\n" );
2461 for ( k = 0; k < nWords; k++ )
2462 fprintf( pFile, " unsigned long s%07d_%d = 0x%08x%08x;\n", 0, k, 0, 0 );
2463 Gia_ManForEachCiId( pGia, Id, i )
2464 {
2465 //word * pSim = Vec_WrdEntryP(vSim0, i*nWords);
2466 //unsigned * pSimU = (unsigned *)pSim;
2467 for ( k = 0; k < nWords; k++ )
2468 fprintf( pFile, " unsigned long s%07d_%d = ((unsigned long)rand() << 48) | ((unsigned long)rand() << 32) | ((unsigned long)rand() << 16) | (unsigned long)rand();\n", Id, k );
2469 }
2470 Gia_ManForEachAnd( pGia, pObj, Id )
2471 {
2472 for ( k = 0; k < nWords; k++ )
2473 fprintf( pFile, " unsigned long s%07d_%d = %cs%07d_%d & %cs%07d_%d;\n", Id, k,
2474 Gia_ObjFaninC0(pObj) ? '~' : ' ', Gia_ObjFaninId0(pObj, Id), k,
2475 Gia_ObjFaninC1(pObj) ? ' ' : '~', Gia_ObjFaninId1(pObj, Id), k );
2476 }
2477 Gia_ManForEachCoId( pGia, Id, i )
2478 {
2479 pObj = Gia_ManObj(pGia, Id);
2480 for ( k = 0; k < nWords; k++ )
2481 fprintf( pFile, " Res ^= %cs%07d_%d;\n", Gia_ObjFaninC0(pObj) ? '~' : ' ', Gia_ObjFaninId0(pObj, Id), k );
2482 }
2483 Vec_WrdFree( vSim0 );
2484 fprintf( pFile, " }\n" );
2485 fprintf( pFile, " printf( \"Res = 0x%%08x \", (unsigned)Res );\n" );
2486 fprintf( pFile, " printf( \"Time = %%6.2f sec\\n\", (float)(clock() - clkThis)/CLOCKS_PER_SEC );\n" );
2487 fprintf( pFile, " return 1;\n" );
2488 fprintf( pFile, "}\n" );
2489 fclose( pFile );
2490}
2491
2492
2504int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int TimeLimit, int fVerbose )
2505{
2506 Vec_Wrd_t * vSim0, * vSim1, * vSim2;
2507 abctime clk = Abc_Clock();
2508 int n, i, RetValue = 1;
2509 int TimeStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0; // in CPU ticks
2510 printf( "Simulating %d round with %d machine words.\n", nRounds, nWords );
2511 Abc_RandomW(0);
2512 for ( n = 0; RetValue && n < nRounds; n++ )
2513 {
2514 if ( TimeStop && Abc_Clock() > TimeStop )
2515 {
2516 printf( "Computation timed out after %d seconds and %d rounds.\n", TimeLimit, n );
2517 break;
2518 }
2519 vSim0 = Vec_WrdStartRandom( Gia_ManCiNum(p0) * nWords );
2520 p0->vSimsPi = vSim0;
2521 p1->vSimsPi = vSim0;
2522 vSim1 = Gia_ManSimPatSim( p0 );
2523 vSim2 = Gia_ManSimPatSim( p1 );
2524 for ( i = 0; i < Gia_ManCoNum(p0); i++ )
2525 {
2526 word * pSim1 = Vec_WrdEntryP(vSim1, Gia_ObjId(p0, Gia_ManCo(p0, i))*nWords);
2527 word * pSim2 = Vec_WrdEntryP(vSim2, Gia_ObjId(p1, Gia_ManCo(p1, i))*nWords);
2528 if ( memcmp(pSim1, pSim2, sizeof(word)*nWords) )
2529 {
2530 printf( "Output %d failed simulation at round %d. ", i, n );
2531 RetValue = 0;
2532 break;
2533 }
2534 }
2535 Vec_WrdFree( vSim1 );
2536 Vec_WrdFree( vSim2 );
2537 Vec_WrdFree( vSim0 );
2538 p0->vSimsPi = NULL;
2539 p1->vSimsPi = NULL;
2540 }
2541 if ( RetValue == 1 )
2542 printf( "Simulation did not detect a bug. " );
2543 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2544 return RetValue;
2545}
2546
2558void Gia_ManSim2ArrayOne( Vec_Wrd_t * vSimsPi, Vec_Int_t * vRes )
2559{
2560 word * pInfo = Vec_WrdArray(vSimsPi); int w, i;
2561 word * pCare = pInfo + Vec_WrdSize(vSimsPi);
2562 Vec_IntClear( vRes );
2563 for ( w = 0; w < Vec_WrdSize(vSimsPi); w++ )
2564 if ( pCare[w] )
2565 for ( i = 0; i < 64; i++ )
2566 if ( Abc_TtGetBit(pCare, w*64+i) )
2567 Vec_IntPush( vRes, Abc_Var2Lit(w*64+i, Abc_TtGetBit(pInfo, w*64+i)) );
2568 Vec_IntPush( vRes, Vec_WrdSize(vSimsPi) );
2569}
2570Vec_Wec_t * Gia_ManSim2Array( Vec_Ptr_t * vSims )
2571{
2572 Vec_Wec_t * vRes = Vec_WecStart( Vec_PtrSize(vSims) );
2573 Vec_Int_t * vLevel; int i;
2574 Vec_WecForEachLevel( vRes, vLevel, i )
2575 Gia_ManSim2ArrayOne( (Vec_Wrd_t *)Vec_PtrEntry(vSims, i), vLevel );
2576 return vRes;
2577}
2578
2579Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes )
2580{
2581 int i, iLit, nWords = Vec_IntEntryLast(vRes);
2582 Vec_Wrd_t * vSimsPi = Vec_WrdStart( 2*nWords );
2583 word * pInfo = Vec_WrdArray(vSimsPi);
2584 word * pCare = pInfo + nWords;
2585 Vec_IntPop( vRes );
2586 Vec_IntForEachEntry( vRes, iLit, i )
2587 {
2588 Abc_TtXorBit( pCare, Abc_Lit2Var(iLit) );
2589 if ( Abc_LitIsCompl(iLit) )
2590 Abc_TtXorBit( pInfo, Abc_Lit2Var(iLit) );
2591 }
2592 Vec_IntPush( vRes, nWords );
2593 Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
2594 return vSimsPi;
2595}
2596Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes )
2597{
2598 Vec_Ptr_t * vSims = Vec_PtrAlloc( Vec_WecSize(vRes) );
2599 Vec_Int_t * vLevel; int i;
2600 Vec_WecForEachLevel( vRes, vLevel, i )
2601 Vec_PtrPush( vSims, Gia_ManArray2SimOne(vLevel) );
2602 return vSims;
2603}
2604
2605void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi )
2606{
2607 Vec_Ptr_t * vTemp = Vec_PtrAlloc( 2 );
2608 Vec_PtrPushTwo( vTemp, vSimsPi, vSimsPi );
2609 {
2610 Vec_Wec_t * vRes = Gia_ManSim2Array( vTemp );
2611 Vec_WecDumpBin( "temp.sims", vRes, 1 );
2612 {
2613 Vec_Wec_t * vRes = Vec_WecReadBin( "temp.sims", 1 );
2614 Vec_Ptr_t * vTemp2 = Gia_ManArray2Sim( vRes );
2615 Vec_Wrd_t * vSimsPi2 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 0 );
2616 Vec_Wrd_t * vSimsPi3 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 1 );
2617
2618 Abc_TtAnd( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi)+Vec_WrdSize(vSimsPi), Vec_WrdSize(vSimsPi), 0 );
2619
2620 vSimsPi->nSize *= 2;
2621 vSimsPi2->nSize *= 2;
2622 vSimsPi3->nSize *= 2;
2623 Vec_WrdDumpHex( "test1.hex", vSimsPi, 1, 1 );
2624 Vec_WrdDumpHex( "test2.hex", vSimsPi2, 1, 1 );
2625 Vec_WrdDumpHex( "test3.hex", vSimsPi3, 1, 1 );
2626 vSimsPi->nSize /= 2;
2627 vSimsPi2->nSize /= 2;
2628 vSimsPi3->nSize /= 2;
2629
2630 if ( Vec_WrdEqual( vSimsPi, vSimsPi2 ) )
2631 printf( "Success.\n" );
2632 else
2633 printf( "Failure.\n" );
2634 if ( Vec_WrdEqual( vSimsPi, vSimsPi3 ) )
2635 printf( "Success.\n" );
2636 else
2637 printf( "Failure.\n" );
2638 Vec_WrdFree( vSimsPi2 );
2639 Vec_WrdFree( vSimsPi3 );
2640 Vec_PtrFree( vTemp2 );
2641 Vec_WecFree( vRes );
2642 }
2643 Vec_WecFree( vRes );
2644 }
2645 Vec_PtrFree( vTemp );
2646}
2647
2648
2660void Gia_ManPtrWrdDumpBin( char * pFileName, Vec_Ptr_t * p, int fVerbose )
2661{
2662 Vec_Wrd_t * vLevel;
2663 int i, nSize, RetValue;
2664 FILE * pFile = fopen( pFileName, "wb" );
2665 if ( pFile == NULL )
2666 {
2667 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2668 return;
2669 }
2670 nSize = Vec_PtrSize(p);
2671 RetValue = fwrite( &nSize, 1, sizeof(int), pFile );
2672 Vec_PtrForEachEntry( Vec_Wrd_t *, p, vLevel, i )
2673 {
2674 nSize = Vec_WrdSize(vLevel);
2675 RetValue += fwrite( &nSize, 1, sizeof(int), pFile );
2676 RetValue += fwrite( Vec_WrdArray(vLevel), 1, sizeof(word)*nSize, pFile );
2677 }
2678 fclose( pFile );
2679 if ( fVerbose )
2680 printf( "Written %d arrays into file \"%s\".\n", Vec_PtrSize(p), pFileName );
2681}
2682Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose )
2683{
2684 Vec_Ptr_t * p = NULL; Vec_Wrd_t * vLevel; int i, nSize, RetValue;
2685 FILE * pFile = fopen( pFileName, "rb" );
2686 if ( pFile == NULL )
2687 {
2688 printf( "Cannot open file \"%s\" for reading.\n", pFileName );
2689 return NULL;
2690 }
2691 fseek( pFile, 0, SEEK_END );
2692 nSize = ftell( pFile );
2693 if ( nSize == 0 )
2694 {
2695 printf( "The input file is empty.\n" );
2696 fclose( pFile );
2697 return NULL;
2698 }
2699 if ( nSize % (int)sizeof(int) > 0 )
2700 {
2701 printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", nSize % (int)sizeof(int) );
2702 fclose( pFile );
2703 return NULL;
2704 }
2705 rewind( pFile );
2706 RetValue = fread( &nSize, 1, sizeof(int), pFile );
2707 assert( RetValue == 4 );
2708 p = Vec_PtrAlloc( nSize );
2709 for ( i = 0; i < nSize; i++ )
2710 Vec_PtrPush( p, Vec_WrdAlloc(100) );
2711 Vec_PtrForEachEntry( Vec_Wrd_t *, p, vLevel, i )
2712 {
2713 RetValue = fread( &nSize, 1, sizeof(int), pFile );
2714 assert( RetValue == 4 );
2715 Vec_WrdFill( vLevel, nSize, 0 );
2716 RetValue = fread( Vec_WrdArray(vLevel), 1, sizeof(word)*nSize, pFile );
2717 assert( RetValue == 8*nSize );
2718 }
2719 fclose( pFile );
2720 if ( fVerbose )
2721 printf( "Read %d arrays from file \"%s\".\n", Vec_PtrSize(p), pFileName );
2722 return p;
2723}
2724
2736Vec_Int_t * Gia_ManProcessBuffs( Gia_Man_t * pHie, Vec_Wrd_t * vSimsH, int nWords, Vec_Mem_t * vStore, Vec_Int_t * vLabels )
2737{
2738 Vec_Int_t * vPoSigs = Vec_IntAlloc( Gia_ManBufNum(pHie) );
2739 Vec_Int_t * vMap;
2740 Vec_Wec_t * vNodes = Vec_WecStart( Gia_ManBufNum(pHie) );
2741 Gia_Obj_t * pObj; int i, Sig, Value;
2742 Gia_ManForEachBuf( pHie, pObj, i )
2743 {
2744 word * pSim = Vec_WrdEntryP(vSimsH, Gia_ObjId(pHie, pObj)*nWords);
2745 int fCompl = pSim[0] & 1;
2746 if ( fCompl )
2747 Abc_TtNot( pSim, nWords );
2748 Vec_IntPush( vPoSigs, Vec_MemHashInsert(vStore, pSim) );
2749 if ( fCompl )
2750 Abc_TtNot( pSim, nWords );
2751 }
2752 Vec_IntPrint( vPoSigs );
2753 vMap = Vec_IntStartFull( Vec_MemEntryNum(vStore) );
2754 Vec_IntForEachEntry( vPoSigs, Sig, i )
2755 {
2756 assert( Vec_IntEntry(vMap, Sig) == -1 );
2757 Vec_IntWriteEntry( vMap, Sig, i );
2758 }
2759 Vec_IntForEachEntry( vLabels, Sig, i )
2760 {
2761 if ( Sig < 0 )
2762 continue;
2763 Value = Vec_IntEntry(vMap, Sig);
2764 if ( Value == -1 )
2765 continue;
2766 assert( Value >= 0 && Value < Gia_ManBufNum(pHie) );
2767 Vec_WecPush( vNodes, Value, i );
2768 }
2769 Vec_WecPrint( vNodes, 0 );
2770 Vec_WecFree( vNodes );
2771 Vec_IntFree( vMap );
2772 Vec_IntFree( vPoSigs );
2773 return NULL;
2774}
2775
2787void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld )
2788{
2789 Gia_Obj_t * pObj; int i;
2790 Gia_ManSetPhase( pNew );
2791 Gia_ManSetPhase( pOld );
2792 Gia_ManForEachCo( pNew, pObj, i )
2793 if ( pObj->fPhase ^ Gia_ManCo(pOld, i)->fPhase )
2794 {
2795 printf( "Updating out %d.\n", i );
2796 Gia_ObjFlipFaninC0( pObj );
2797 }
2798}
2799
2811void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fVerbose )
2812{
2813 abctime clk = Abc_Clock();
2814 Vec_Wrd_t * vSims = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords );
2815 Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat );
2816 Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie );
2817 Vec_Int_t * vLabels = Vec_IntStartFull( Gia_ManObjNum(pFlat) );
2818 Gia_Obj_t * pObj; int fCompl, Value, * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
2819 Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
2820 pFlat->vSimsPi = NULL;
2821 pHie->vSimsPi = NULL;
2822 Vec_WrdFree( vSims );
2823
2824 printf( "Comparing two AIGs using %d simulation words.\n", nWords );
2825 printf( "Hierarchical: " ); Gia_ManPrintStats( pHie, NULL );
2826 printf( "Flat: " ); Gia_ManPrintStats( pFlat, NULL );
2827
2828 Vec_MemHashAlloc( vStore, 1 << 12 );
2829 Gia_ManForEachCand( pFlat, pObj, i )
2830 {
2831 word * pSim = Vec_WrdEntryP(vSims0, i*nWords);
2832 nC0s += Abc_TtIsConst0(pSim, nWords);
2833 nC1s += Abc_TtIsConst1(pSim, nWords);
2834 fCompl = pSim[0] & 1;
2835 if ( fCompl )
2836 Abc_TtNot( pSim, nWords );
2837 Value = Vec_MemHashInsert( vStore, pSim );
2838 if ( fCompl )
2839 Abc_TtNot( pSim, nWords );
2840 Vec_IntWriteEntry( vLabels, i, Value );
2841 }
2842 nUnique = Vec_MemEntryNum( vStore );
2843 printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n",
2844 64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pFlat), Gia_ManCandNum(pFlat), nC0s, nC1s );
2845
2846 assert( Gia_ManCiNum(pFlat) == Gia_ManCiNum(pHie) );
2847 Gia_ManForEachCand( pHie, pObj, i )
2848 {
2849 word * pSim = Vec_WrdEntryP(vSims1, i*nWords);
2850 pSpot = Vec_MemHashLookup( vStore, pSim );
2851 Abc_TtNot( pSim, nWords );
2852 pSpot2 = Vec_MemHashLookup( vStore, pSim );
2853 Abc_TtNot( pSim, nWords );
2854 nBoundary += Gia_ObjIsBuf(pObj);
2855 if ( *pSpot != -1 || *pSpot2 != -1 )
2856 {
2857 nMatched++;
2858 continue;
2859 }
2860 //Extra_PrintBinary( stdout, (unsigned *)pSim, 64*nWords ); printf("\n");
2861 nFound[1] += Gia_ObjIsBuf(pObj);
2862 nFound[2]++;
2863 //if ( Gia_ObjIsBuf(pObj) )
2864 // printf( "%d(%d) ", i, nBoundary-1 );
2865 }
2866 Gia_ManProcessBuffs( pHie, vSims1, nWords, vStore, vLabels );
2867 Vec_MemHashFree( vStore );
2868 Vec_MemFree( vStore );
2869 Vec_WrdFree( vSims0 );
2870 Vec_WrdFree( vSims1 );
2871 Vec_IntFree( vLabels );
2872
2873 printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary. ",
2874 nMatched, 100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)),
2875 nFound[2], 100.0*nFound[2]/Abc_MaxInt(1, Gia_ManCandNum(pHie)),
2876 nFound[1], 100.0*nFound[1]/Abc_MaxInt(1, nBoundary) );
2877 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2878}
2879
2891Vec_Wec_t * Gia_ManRelTfos( Gia_Man_t * p, Vec_Int_t * vObjs )
2892{
2893 Gia_Obj_t * pObj;
2894 Vec_Wec_t * vNodes = Vec_WecStart( Vec_IntSize(vObjs)+1 );
2895 Vec_Int_t * vSigns = Vec_IntStart( Gia_ManObjNum(p) );
2896 int n, k, i, iObj, * pSigns = Vec_IntArray(vSigns);
2897 assert( Vec_IntSize(vObjs) < 32 );
2898 Vec_IntForEachEntry( vObjs, iObj, i )
2899 pSigns[iObj] |= 1 << i;
2900 Gia_ManForEachAnd( p, pObj, i )
2901 {
2902 if ( pSigns[i] == 0 )
2903 for ( n = 0; n < 2; n++ )
2904 pSigns[i] |= pSigns[Gia_ObjFaninId(pObj, i, n)];
2905 if ( pSigns[i] == 0 )
2906 continue;
2907 Vec_WecPush( vNodes, Vec_IntSize(vObjs), i );
2908 for ( k = 0; k < Vec_IntSize(vObjs); k++ )
2909 if ( (pSigns[i] >> k) & 1 )
2910 Vec_WecPush( vNodes, k, i );
2911 }
2912 Vec_IntFree( vSigns );
2913 return vNodes;
2914}
2915Vec_Wrd_t * Gia_ManRelDerive( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
2916{
2917 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
2918 int i, m, iVar, iMint = 0, nMints = 1 << Vec_IntSize(vObjs);
2919 Vec_Wrd_t * vCopy = Vec_WrdDup(vSims); Vec_Int_t * vLevel;
2920 Vec_Wrd_t * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
2921 Vec_Wec_t * vNodes = Gia_ManRelTfos( p, vObjs );
2922 Vec_WecPrint( vNodes, 0 );
2923 Gia_ManForEachAnd( p, pObj, i )
2924 assert( pObj->fPhase == 0 );
2925 Gia_ManForEachObjVec( vObjs, p, pObj, i )
2926 pObj->fPhase = 1;
2927 vLevel = Vec_WecEntry( vNodes, Vec_IntSize(vObjs) );
2928 Gia_ManForEachObjVec( vLevel, p, pObj, i )
2929 if ( pObj->fPhase )
2930 Abc_TtClear( Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords), nWords );
2931 else
2932 Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
2933 for ( m = 0; m < nMints; m++ )
2934 {
2935 Gia_ManForEachCo( p, pObj, i )
2936 {
2937 word * pSimO = Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords);
2938 word * pSimF = Vec_WrdEntryP(vCopy, Gia_ObjFaninId0p(p, pObj)*nWords);
2939 word * pSimR = Vec_WrdEntryP(vRel, (iMint*Gia_ManCoNum(p) + i)*nWords);
2940 Abc_TtXor( pSimR, pSimF, pSimO, nWords, Gia_ObjFaninC0(pObj) );
2941 }
2942 if ( m == nMints-1 )
2943 break;
2944 iVar = Abc_TtSuppFindFirst( (m+1) ^ ((m+1) >> 1) ^ (m) ^ ((m) >> 1) );
2945 vLevel = Vec_WecEntry( vNodes, iVar );
2946 assert( Vec_IntEntry(vLevel, 0) == Vec_IntEntry(vObjs, iVar) );
2947 Abc_TtNot( Vec_WrdEntryP(vCopy, Vec_IntEntry(vObjs, iVar)*nWords), nWords );
2948 Gia_ManForEachObjVec( vLevel, p, pObj, i )
2949 if ( !pObj->fPhase )
2950 Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
2951 iMint ^= 1 << iVar;
2952 }
2953 Gia_ManForEachObjVec( vObjs, p, pObj, i )
2954 pObj->fPhase = 0;
2955 Vec_WrdFree( vCopy );
2956 Vec_WecFree( vNodes );
2957 return vRel;
2958}
2959Vec_Wrd_t * Gia_ManRelDerive2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
2960{
2961 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
2962 int i, Id, m, Index, nMints = 1 << Vec_IntSize(vObjs);
2963 Vec_Wrd_t * vPos, * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
2964 for ( m = 0; m < nMints; m++ )
2965 {
2966 Gia_Man_t * pNew = Gia_ManDup( p );
2967 Gia_ManForEachAnd( pNew, pObj, i )
2968 {
2969 if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId0(pObj, i))) >= 0 )
2970 pObj->iDiff0 = i, pObj->fCompl0 ^= (m >> Index) & 1;
2971 if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId1(pObj, i))) >= 0 )
2972 pObj->iDiff1 = i, pObj->fCompl1 ^= (m >> Index) & 1;
2973 }
2974 vPos = Gia_ManSimPatSimOut( pNew, p->vSimsPi, 1 );
2975 Gia_ManForEachCoId( p, Id, i )
2976 Abc_TtXor( Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p) + i)*nWords), Vec_WrdEntryP(vPos, i*nWords), Vec_WrdEntryP(vSims, Id*nWords), nWords, 0 );
2977 Vec_WrdFree( vPos );
2978 Gia_ManStop( pNew );
2979 }
2980 return vRel;
2981}
2982void Gia_ManRelPrint( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
2983{
2984 int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
2985 int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
2986 printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
2987 for ( w = 0; w < 64*nWords; w++ )
2988 {
2989 Gia_ManForEachCiId( p, Id, i )
2990 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
2991 printf( " " );
2992 Vec_IntForEachEntry( vObjs, Id, i )
2993 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
2994 printf( " " );
2995 Gia_ManForEachCoId( p, Id, i )
2996 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
2997 printf( " " );
2998 for ( m = 0; m < nMints; m++ )
2999 {
3000 printf( " " );
3001 for ( i = 0; i < Vec_IntSize(vObjs); i++ )
3002 printf( "%d", (m >> i) & 1 );
3003 printf( "=" );
3004 Gia_ManForEachCoId( p, Id, i )
3005 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w) );
3006 }
3007 printf( "\n" );
3008 }
3009}
3010void Gia_ManRelPrint2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
3011{
3012 int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3013 int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
3014 int nWordsM = Abc_Truth6WordNum(Vec_IntSize(vObjs));
3015 Vec_Wrd_t * vRes = Vec_WrdStart( 64*nWords * nWordsM );
3016 printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
3017 for ( w = 0; w < 64*nWords; w++ )
3018 {
3019 int iMint = 0;
3020 int nValid = 0;
3021 Gia_ManForEachCiId( p, Id, i )
3022 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
3023 printf( " " );
3024 Vec_IntForEachEntry( vObjs, Id, i )
3025 {
3026 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
3027 if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) )
3028 iMint |= 1 << i;
3029 }
3030 printf( " " );
3031 Gia_ManForEachCoId( p, Id, i )
3032 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
3033 printf( " " );
3034 for ( m = 0; m < nMints; m++ )
3035 {
3036 int Count = 0;
3037 Gia_ManForEachCoId( p, Id, i )
3038 Count += Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w);
3039 printf( "%d", Count == 0 );
3040 nValid += Count > 0;
3041 if ( Count == 0 )
3042 Abc_TtSetBit( Vec_WrdEntryP(vRes, w*nWordsM), m );
3043 }
3044 printf( " " );
3045 for ( m = 0; m < nMints; m++ )
3046 printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), m) );
3047 printf( " " );
3048 assert( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint) );
3049 for ( i = 0; i < Vec_IntSize(vObjs); i++ )
3050 if ( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint ^ (1 << i)) )
3051 printf( "-" );
3052 else
3053 printf( "%d", (iMint >> i) & 1 );
3054 printf( " %d", nMints-nValid );
3055 printf( "\n" );
3056 }
3057 Vec_WrdFree( vRes );
3058}
3059Vec_Int_t * Gia_ManRelInitObjs()
3060{
3061 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3062 /*
3063 Vec_IntPush( vRes, 33 );
3064 Vec_IntPush( vRes, 52 );
3065 Vec_IntPush( vRes, 53 );
3066 Vec_IntPush( vRes, 65 );
3067 Vec_IntPush( vRes, 79 );
3068 Vec_IntPush( vRes, 81 );
3069 */
3070 /*
3071 Vec_IntPush( vRes, 60 );
3072 Vec_IntPush( vRes, 61 );
3073 Vec_IntPush( vRes, 71 );
3074 Vec_IntPush( vRes, 72 );
3075 */
3076 /*
3077 Vec_IntPush( vRes, 65 );
3078 Vec_IntPush( vRes, 79 );
3079 Vec_IntPush( vRes, 81 );
3080 */
3081 Vec_IntPush( vRes, 52 );
3082 Vec_IntPush( vRes, 54 );
3083 Vec_IntPrint( vRes );
3084 return vRes;
3085}
3086void Gia_ManRelDeriveTest2( Gia_Man_t * p )
3087{
3088 Vec_Int_t * vObjs = Gia_ManRelInitObjs();
3089 Vec_Wrd_t * vSims, * vRel, * vRel2; int nWords;
3090 Vec_WrdFreeP( &p->vSimsPi );
3091 p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
3092 nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3093 vSims = Gia_ManSimPatSim( p );
3094 vRel = Gia_ManRelDerive( p, vObjs, vSims );
3095 vRel2 = Gia_ManRelDerive2( p, vObjs, vSims );
3096 //assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) );
3097 Gia_ManRelPrint2( p, vObjs, vSims, vRel );
3098 Vec_WrdFree( vRel2 );
3099 Vec_WrdFree( vRel );
3100 Vec_WrdFree( vSims );
3101 Vec_IntFree( vObjs );
3102}
3103
3115Vec_Int_t * Gia_ManRelInitIns()
3116{
3117 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3118 Vec_IntPush( vRes, 12 );
3119 Vec_IntPush( vRes, 18 );
3120 Vec_IntPush( vRes, 21 );
3121 Vec_IntPush( vRes, 34 );
3122 Vec_IntPush( vRes, 45 );
3123 Vec_IntPush( vRes, 59 );
3124 return vRes;
3125}
3126Vec_Int_t * Gia_ManRelInitOuts()
3127{
3128 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3129 Vec_IntPush( vRes, 65 );
3130 Vec_IntPush( vRes, 66 );
3131 return vRes;
3132}
3133Vec_Int_t * Gia_ManRelInitMffc( Gia_Man_t * p, Vec_Int_t * vOuts )
3134{
3135 Gia_Obj_t * pObj; int i;
3136 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
3137 Vec_IntSort( vOuts, 0 );
3138 Gia_ManIncrementTravId( p );
3139 Gia_ManForEachObjVec( vOuts, p, pObj, i )
3140 Gia_ObjSetTravIdCurrent( p, pObj );
3141 Gia_ManIncrementTravId( p );
3142 Gia_ManForEachCo( p, pObj, i )
3143 if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
3144 Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
3145 Gia_ManForEachAndReverse( p, pObj, i )
3146 if ( Gia_ObjIsTravIdPrevious(p, pObj) )
3147 continue;
3148 else if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3149 {
3150 if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
3151 Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
3152 if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin1(pObj)) )
3153 Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin1(pObj) );
3154 }
3155 Gia_ManForEachAnd( p, pObj, i )
3156 if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
3157 Vec_IntPush( vRes, i );
3158 printf( "MFFC: " );
3159 Vec_IntPrint( vRes );
3160 return vRes;
3161}
3162Vec_Int_t * Gia_ManRelInitDivs( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vOuts )
3163{
3164 Gia_Obj_t * pObj; int i;
3165 Vec_Int_t * vMffc = Gia_ManRelInitMffc( p, vOuts );
3166 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
3167 Vec_IntSort( vIns, 0 );
3168
3169 Gia_ManIncrementTravId( p );
3170 Gia_ManForEachObjVec( vMffc, p, pObj, i )
3171 Gia_ObjSetTravIdCurrent( p, pObj );
3172 Vec_IntFree( vMffc );
3173
3174 Vec_IntPush( vRes, 0 );
3175 Vec_IntAppend( vRes, vIns );
3176
3177 Gia_ManIncrementTravId( p );
3178 Gia_ManForEachObjVec( vIns, p, pObj, i )
3179 Gia_ObjSetTravIdCurrent( p, pObj );
3180
3181 Gia_ManForEachAnd( p, pObj, i )
3182 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3183 continue;
3184 else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
3185 {
3186 if ( !Gia_ObjIsTravIdPrevious(p, pObj) )
3187 Vec_IntPush( vRes, i );
3188 Gia_ObjSetTravIdCurrent( p, pObj );
3189 }
3190 printf( "Divisors: " );
3191 Vec_IntPrint( vRes );
3192 return vRes;
3193}
3194
3195Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts )
3196{
3197 Vec_Int_t * vRes = Vec_IntStartFull( 1 << Vec_IntSize(vIns) );
3198 int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3199 for ( w = 0; w < 64*nWords; w++ )
3200 {
3201 int i, iObj, iMint = 0, iMint2 = 0;
3202 Vec_IntForEachEntry( vIns, iObj, i )
3203 if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
3204 iMint |= 1 << i;
3205 if ( Vec_IntEntry(vRes, iMint) >= 0 )
3206 continue;
3207 Vec_IntForEachEntry( vOuts, iObj, i )
3208 if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
3209 iMint2 |= 1 << i;
3210 Vec_IntWriteEntry( vRes, iMint, iMint2 );
3211 }
3212 return vRes;
3213}
3214
3215void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs )
3216{
3217 extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide );
3218
3219 int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1);
3220 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
3221 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
3222 int Entry0 = Vec_IntEntry( vRel, 0 );
3223
3224 word Value, Phase = 0;
3225 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3226 Vec_IntForEachEntry( vDivs, iObj, i )
3227 if ( Vec_WrdEntry(vSims, iObj*nWords) & 1 )
3228 Phase |= 1 << i;
3229
3230 assert( Entry0 >= 0 );
3231 printf( "Entry0 = %d\n", Entry0 );
3232 Entry0 ^= 1;
3233// for ( m = 0; m < nMints; m++ )
3234 Vec_IntForEachEntry( vRel, Entry, m )
3235 {
3236 if ( Entry == -1 )
3237 continue;
3238 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, iMint), Entry0 ^ Entry );
3239
3240 Value = 0;
3241 Vec_IntForEachEntry( vDivs, iObj, i )
3242 if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), m) )
3243 Abc_TtSetBit( &Value, i );
3244 Vec_WrdEntryP(vSimsOut, iMint)[0] = Value ^ Phase;
3245
3246 iMint++;
3247 }
3248 assert( iMint == nMints );
3249 printf( "Created %d minterms.\n", iMint );
3250 Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0, NULL );
3251 Vec_WrdFree( vSimsIn );
3252 Vec_WrdFree( vSimsOut );
3253}
3254void Gia_ManRelDeriveTest( Gia_Man_t * p )
3255{
3256 Vec_Int_t * vIns = Gia_ManRelInitIns();
3257 Vec_Int_t * vOuts = Gia_ManRelInitOuts();
3258 Vec_Wrd_t * vSims; Vec_Int_t * vRel, * vDivs; int nWords;
3259 Vec_WrdFreeP( &p->vSimsPi );
3260 p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
3261 nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3262 vSims = Gia_ManSimPatSim( p );
3263 vRel = Gia_ManRelDeriveSimple( p, vSims, vIns, vOuts );
3264 vDivs = Gia_ManRelInitDivs( p, vIns, vOuts );
3265 //printf( "Neg = %d\n", Vec_IntCountEntry(vRel, -1) );
3266
3267 Gia_ManRelSolve( p, vSims, vIns, vOuts, vRel, vDivs );
3268
3269 Vec_IntFree( vDivs );
3270 Vec_IntPrint( vRel );
3271 Vec_IntFree( vRel );
3272 Vec_WrdFree( vSims );
3273 Vec_IntFree( vIns );
3274 Vec_IntFree( vOuts );
3275}
3276
3277
3289int Gia_ManRelOutsTfo_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vTfo )
3290{
3291 if ( Gia_ObjIsTravIdPrevious(p, pObj) )
3292 return 1;
3293 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3294 return 0;
3295 if ( pObj->fPhase )
3296 {
3297 Gia_ObjSetTravIdPrevious(p, pObj);
3298 return 1;
3299 }
3300 if ( Gia_ObjIsAnd(pObj) )
3301 {
3302 int Val0 = Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin0(pObj), vTfo );
3303 int Val1 = Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin1(pObj), vTfo );
3304 if ( Val0 || Val1 )
3305 {
3306 Gia_ObjSetTravIdPrevious(p, pObj);
3307 Vec_IntPush( vTfo, Gia_ObjId(p, pObj) );
3308 return 1;
3309 }
3310 }
3311 Gia_ObjSetTravIdCurrent(p, pObj);
3312 return 0;
3313}
3314Vec_Int_t * Gia_ManRelOutsTfo( Gia_Man_t * p, Vec_Int_t * vOuts )
3315{
3316 Gia_Obj_t * pObj; int i;
3317 Vec_Int_t * vTfo = Vec_IntAlloc( 100 );
3318 Gia_ManIncrementTravId( p );
3319 Gia_ManIncrementTravId( p );
3320 Gia_ObjSetTravIdCurrentId( p, 0 );
3321 Gia_ManCleanPhase( p );
3322 Gia_ManForEachObjVec( vOuts, p, pObj, i )
3323 pObj->fPhase = 1;
3324 Gia_ManForEachCo( p, pObj, i )
3325 if ( Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin0(pObj), vTfo ) )
3326 Vec_IntPush( vTfo, Gia_ObjId(p, pObj) );
3327 Gia_ManForEachObjVec( vOuts, p, pObj, i )
3328 pObj->fPhase = 0;
3329 //Vec_IntPrint( vTfo );
3330 return vTfo;
3331}
3332void Gia_ManSimPatSimTfo( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vTfo )
3333{
3334 Gia_Obj_t * pObj;
3335 int i, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3336 Gia_ManForEachObjVec( vTfo, p, pObj, i )
3337 if ( Gia_ObjIsAnd(pObj) )
3338 Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vSims );
3339 else
3340 Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords, vSims );
3341}
3342void Gia_ManSimPatSimMiter( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2, word * pSims, int nWords )
3343{
3344 Gia_Obj_t * pObj; int i;
3345 Gia_ManForEachCo( p, pObj, i )
3346 Abc_TtOrXor( pSims, Vec_WrdEntryP(vSims, Gia_ObjId(p, pObj)*nWords), Vec_WrdEntryP(vSims2, Gia_ObjId(p, pObj)*nWords), nWords );
3347 Abc_TtNot( pSims, nWords );
3348}
3349Vec_Wrd_t * Gia_ManRelDeriveRel( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t * vSims )
3350{
3351 extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
3352 int i, o, iObj, nMintsO = 1 << Vec_IntSize(vOuts);
3353 int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
3354 Vec_Wrd_t * vSims2 = Vec_WrdDup( vSims );
3355 Vec_Wrd_t * vRel = Vec_WrdStart( nWords * 64 );
3356 Vec_Wrd_t * vRel2 = Vec_WrdStart( nWords * 64 );
3357 Vec_Int_t * vTfo = Gia_ManRelOutsTfo( p, vOuts );
3358 assert( 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs) + nMintsO <= 64 );
3359 assert( Vec_WrdSize(p->vSimsPi) % Gia_ManCiNum(p) == 0 );
3360 Vec_IntForEachEntry( vIns, iObj, o )
3361 memcpy( Vec_WrdEntryP(vRel, nWords*o), Vec_WrdEntryP(vSims, iObj*nWords), sizeof(word)*nWords );
3362 Vec_IntForEachEntry( vDivs, iObj, o )
3363 memcpy( Vec_WrdEntryP(vRel, nWords*(Vec_IntSize(vIns)+o)), Vec_WrdEntryP(vSims, iObj*nWords), sizeof(word)*nWords );
3364 for ( o = 0; o < nMintsO; o++ )
3365 {
3366 word * pRes = Vec_WrdEntryP(vRel, nWords*(Vec_IntSize(vIns)+Vec_IntSize(vDivs)+o));
3367 Vec_IntForEachEntry( vOuts, iObj, i )
3368 memset( Vec_WrdEntryP(vSims2, iObj*nWords), ((o >> i) & 1) ? 0xFF : 0x00, sizeof(word)*nWords );
3369 Gia_ManSimPatSimTfo( p, vSims2, vTfo );
3370 Gia_ManSimPatSimMiter( p, vSims, vSims2, pRes, nWords );
3371 }
3372 Extra_BitMatrixTransposeP( vRel, nWords, vRel2, 1 );
3373 Vec_IntFree( vTfo );
3374 Vec_WrdFree( vSims2 );
3375 Vec_WrdFree( vRel );
3376 return vRel2;
3377}
3378void Gia_ManRelDeriveSims( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel, Vec_Wrd_t ** pvSimsIn, Vec_Wrd_t ** pvSimsOut )
3379{
3380 Vec_Wrd_t * vVals = Vec_WrdStartFull( 1 << Vec_IntSize(vIns) );
3381 Vec_Wrd_t * vSets = Vec_WrdStartFull( 1 << Vec_IntSize(vIns) );
3382 int m, nMints = 1 << Gia_ManCiNum(p), nCares = 0;
3383 int nMintsI = 1 << Vec_IntSize(vIns);
3384 int nShift = Vec_IntSize(vIns) + Vec_IntSize(vDivs);
3385 int MaskI = Abc_Tt6Mask( Vec_IntSize(vIns) );
3386 int MaskD = Abc_Tt6Mask( nShift );
3387 for ( m = 0; m < nMints; m++ )
3388 {
3389 word Sign = Vec_WrdEntry( vRel, m );
3390 *Vec_WrdEntryP( vVals, (int)Sign & MaskI ) = (int)Sign & MaskD;
3391 *Vec_WrdEntryP( vSets, (int)Sign & MaskI ) &= Sign >> nShift;
3392 }
3393 for ( m = 0; m < nMintsI; m++ )
3394 if ( ~Vec_WrdEntry(vSets, m) )
3395 nCares++;
3396 assert( *pvSimsIn == NULL );
3397 assert( *pvSimsOut == NULL );
3398 *pvSimsIn = Vec_WrdAlloc( nCares );
3399 *pvSimsOut = Vec_WrdAlloc( nCares );
3400 for ( m = 0; m < nMintsI; m++ )
3401 if ( ~Vec_WrdEntry(vSets, m) )
3402 {
3403 Vec_WrdPush( *pvSimsIn, Vec_WrdEntry(vVals, m) << 1 );
3404 Vec_WrdPush( *pvSimsOut, Vec_WrdEntry(vSets, m) );
3405 }
3406 assert( Vec_WrdSize(*pvSimsIn) == nCares );
3407 Vec_WrdFree( vSets );
3408 Vec_WrdFree( vVals );
3409}
3410
3411int Gia_ManRelCheck_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
3412{
3413 if ( Gia_ObjIsTravIdPrevious(p, pObj) )
3414 return 1;
3415 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3416 return 0;
3417 if ( pObj->fPhase )
3418 {
3419 Gia_ObjSetTravIdPrevious(p, pObj);
3420 return 1;
3421 }
3422 if ( Gia_ObjIsAnd(pObj) )
3423 {
3424 int Val0 = Gia_ManRelCheck_rec( p, Gia_ObjFanin0(pObj) );
3425 int Val1 = Gia_ManRelCheck_rec( p, Gia_ObjFanin1(pObj) );
3426 if ( Val0 && Val1 )
3427 {
3428 Gia_ObjSetTravIdPrevious(p, pObj);
3429 return 1;
3430 }
3431 }
3432 Gia_ObjSetTravIdCurrent(p, pObj);
3433 return 0;
3434}
3435int Gia_ManRelCheck( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts )
3436{
3437 Gia_Obj_t * pObj; int i, Res = 1;
3438 Gia_ManIncrementTravId( p );
3439 Gia_ManIncrementTravId( p );
3440 Gia_ObjSetTravIdCurrentId( p, 0 );
3441 Gia_ManCleanPhase( p );
3442 Gia_ManForEachObjVec( vIns, p, pObj, i )
3443 pObj->fPhase = 1;
3444 Gia_ManForEachObjVec( vDivs, p, pObj, i )
3445 if ( !Gia_ManRelCheck_rec( p, pObj ) )
3446 Res = 0;
3447 Gia_ManForEachObjVec( vOuts, p, pObj, i )
3448 if ( !Gia_ManRelCheck_rec( p, pObj ) )
3449 Res = 0;
3450 Gia_ManForEachObjVec( vIns, p, pObj, i )
3451 pObj->fPhase = 0;
3452 return Res;
3453}
3454void Gia_ManRelCompute( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t ** pvSimsIn, Vec_Wrd_t ** pvSimsOut )
3455{
3456 Vec_Wrd_t * vSims, * vRel;
3457 //Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3458
3459 Vec_WrdFreeP( &p->vSimsPi );
3460 p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
3461
3462 if ( !Gia_ManRelCheck( p, vIns, vDivs, vOuts ) )
3463 printf( "Window is NOT consistent.\n" );
3464 else
3465 printf( "Window is consistent.\n" );
3466
3467 vSims = Gia_ManSimPatSim( p );
3468 vRel = Gia_ManRelDeriveRel( p, vIns, vDivs, vOuts, vSims );
3469
3470 Gia_ManRelDeriveSims( p, vIns, vDivs, vOuts, vSims, vRel, pvSimsIn, pvSimsOut );
3471
3472 Vec_WrdFree( vRel );
3473 Vec_WrdFree( vSims );
3474 Vec_WrdFreeP( &p->vSimsPi );
3475}
3476
3488/*
3489Vec_Int_t * Gia_ManRelInitIns1()
3490{
3491 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3492 Vec_IntPush( vRes, 22 );
3493 Vec_IntPush( vRes, 41 );
3494 Vec_IntPush( vRes, 45 );
3495 Vec_IntPush( vRes, 59 );
3496 return vRes;
3497}
3498Vec_Int_t * Gia_ManRelInitDivs1()
3499{
3500 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3501 Vec_IntPush( vRes, 46 );
3502 Vec_IntPush( vRes, 47 );
3503 Vec_IntPush( vRes, 48 );
3504 return vRes;
3505}
3506Vec_Int_t * Gia_ManRelInitOuts1()
3507{
3508 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3509 Vec_IntPush( vRes, 65 );
3510 Vec_IntPush( vRes, 66 );
3511 return vRes;
3512}
3513*/
3514
3515Vec_Int_t * Gia_ManRelInitIns1()
3516{
3517 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3518 Vec_IntPush( vRes, 22 );
3519 Vec_IntPush( vRes, 25 );
3520 Vec_IntPush( vRes, 42 );
3521 Vec_IntPush( vRes, 59 );
3522 return vRes;
3523}
3524Vec_Int_t * Gia_ManRelInitDivs1()
3525{
3526 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3527 Vec_IntPush( vRes, 43 );
3528 Vec_IntPush( vRes, 44 );
3529 Vec_IntPush( vRes, 45 );
3530 Vec_IntPush( vRes, 46 );
3531 return vRes;
3532}
3533Vec_Int_t * Gia_ManRelInitOuts1()
3534{
3535 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3536 Vec_IntPush( vRes, 60 );
3537 Vec_IntPush( vRes, 61 );
3538 return vRes;
3539}
3540
3541/*
3542Vec_Int_t * Gia_ManRelInitIns1()
3543{
3544 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3545 Vec_IntPush( vRes, 22 );
3546 Vec_IntPush( vRes, 25 );
3547 Vec_IntPush( vRes, 42 );
3548 Vec_IntPush( vRes, 50 );
3549 Vec_IntPush( vRes, 67 );
3550 return vRes;
3551}
3552Vec_Int_t * Gia_ManRelInitDivs1()
3553{
3554 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3555 Vec_IntPush( vRes, 43 );
3556 Vec_IntPush( vRes, 44 );
3557 Vec_IntPush( vRes, 45 );
3558 Vec_IntPush( vRes, 46 );
3559 return vRes;
3560}
3561Vec_Int_t * Gia_ManRelInitOuts1()
3562{
3563 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3564 Vec_IntPush( vRes, 73 );
3565 Vec_IntPush( vRes, 74 );
3566 return vRes;
3567}
3568*/
3569
3570/*
3571Vec_Int_t * Gia_ManRelInitIns1()
3572{
3573 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3574 Vec_IntPush( vRes, 43 );
3575 Vec_IntPush( vRes, 46 );
3576 //Vec_IntPush( vRes, 49 );
3577 Vec_IntPush( vRes, 50 );
3578 Vec_IntPush( vRes, 67 );
3579 Vec_IntPush( vRes, 75 );
3580 return vRes;
3581}
3582Vec_Int_t * Gia_ManRelInitDivs1()
3583{
3584 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3585 return vRes;
3586}
3587Vec_Int_t * Gia_ManRelInitOuts1()
3588{
3589 Vec_Int_t * vRes = Vec_IntAlloc( 10 );
3590 Vec_IntPush( vRes, 73 );
3591 Vec_IntPush( vRes, 86 );
3592 Vec_IntPush( vRes, 88 );
3593 return vRes;
3594}
3595*/
3596
3597void Gia_ManRelDeriveTest1( Gia_Man_t * p )
3598{
3599 extern void Exa6_WriteFile2( char * pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut );
3600
3601 word Entry; int i;
3602 Vec_Int_t * vIns = Gia_ManRelInitIns1();
3603 Vec_Int_t * vDivs = Gia_ManRelInitDivs1();
3604 Vec_Int_t * vOuts = Gia_ManRelInitOuts1();
3605
3606 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3607 Gia_ManRelCompute( p, vIns, vDivs, vOuts, &vSimsDiv, &vSimsOut );
3608
3609 printf( "Inputs:\n" );
3610 Vec_WrdForEachEntry( vSimsDiv, Entry, i )
3611 Abc_TtPrintBits( &Entry, 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs) );
3612 printf( "Outputs:\n" );
3613 Vec_WrdForEachEntry( vSimsOut, Entry, i )
3614 Abc_TtPrintBits( &Entry, 1 << Vec_IntSize(vOuts) );
3615 printf( "\n" );
3616
3617 Exa6_WriteFile2( "mul44_i5_n0_t3_s11.rel", Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), vSimsDiv, vSimsOut );
3618
3619 Vec_WrdFree( vSimsDiv );
3620 Vec_WrdFree( vSimsOut );
3621
3622 Vec_IntFree( vIns );
3623 Vec_IntFree( vDivs );
3624 Vec_IntFree( vOuts );
3625}
3626
3627
3639Gia_Man_t * Gia_ManChangeTest3( Gia_Man_t * p )
3640{
3641 extern void Exa6_WriteFile2( char * pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut );
3642 extern void Exa_ManExactPrint( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nDivs, int nOuts );
3643 extern Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char * pFileName );
3644 extern Gia_Man_t * Gia_ManDupMini( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Mini_Aig_t * pMini );
3645
3646 Gia_Man_t * pNew = NULL;
3647 Mini_Aig_t * pMini = NULL;
3648 Vec_Int_t * vIns = Gia_ManRelInitIns1();
3649 Vec_Int_t * vDivs = Gia_ManRelInitDivs1();
3650 Vec_Int_t * vOuts = Gia_ManRelInitOuts1();
3651 int nNodes = 4;
3652
3653 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3654 Gia_ManRelCompute( p, vIns, vDivs, vOuts, &vSimsDiv, &vSimsOut );
3655 Exa_ManExactPrint( vSimsDiv, vSimsOut, 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs), Vec_IntSize(vOuts) );
3656 //Exa6_WriteFile2( "mul44_i%d_n%d_t%d_s%d.rel", Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), nNodes );
3657 pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), nNodes, 1, 1, NULL );
3658 if ( pMini )
3659 {
3660 pNew = Gia_ManDupMini( p, vIns, vDivs, vOuts, pMini );
3661 Mini_AigStop( pMini );
3662 }
3663 Vec_WrdFree( vSimsDiv );
3664 Vec_WrdFree( vSimsOut );
3665
3666 Vec_IntFree( vIns );
3667 Vec_IntFree( vDivs );
3668 Vec_IntFree( vOuts );
3669 return pNew;
3670}
3671
3672
3673
3685Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
3686{
3687 Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
3688 Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
3689 int n, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
3690 int i, nLimit = Gia_ManCiNum(p) < 6 ? 1 << Gia_ManCiNum(p) : 64*nWords;
3691 Vec_Str_t * vOut = Vec_StrAlloc( nLimit*(Gia_ManCoNum(p) + 3)+1 );
3692 assert( Vec_WrdSize(vSims) == nWords * Gia_ManCoNum(p) );
3693 for ( n = 0; n < nLimit; n++ )
3694 {
3695 for ( i = 0; i < Gia_ManCoNum(p); i++ )
3696 Vec_StrPush( vOut, (char)('0' + Abc_TtGetBit(Vec_WrdEntryP(vSims, i*nWords), n)) );
3697 Vec_StrPush( vOut, ' ' );
3698 Vec_StrPush( vOut, '1' );
3699 Vec_StrPush( vOut, '\n' );
3700 }
3701 Vec_StrPush( vOut, '\0' );
3702 Vec_WrdFree( vSims );
3703 Vec_WrdFree( vSimsPi );
3704 return vOut;
3705}
3706
3718void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q )
3719{
3720 Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
3721 Vec_Wrd_t * vSimsP = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
3722 Vec_Wrd_t * vSimsQ = Gia_ManSimPatSimOut( q, vSimsPi, 0 );
3723 int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0;
3724 Gia_Obj_t * pObjP, * pObjQ;
3725 Gia_ManSetPhase( p );
3726 Gia_ManSetPhase( q );
3727 Gia_ManForEachObj( p, pObjP, i ) {
3728 word * pSim = Vec_WrdEntryP( vSimsP, i * nWords );
3729 if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
3730 }
3731 Gia_ManForEachObj( q, pObjQ, i ) {
3732 word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords );
3733 if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
3734 }
3735 Gia_ManForEachAnd( q, pObjQ, i ) {
3736 word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords );
3737 int fFirst = 1;
3738 Gia_ManForEachObj( p, pObjP, k ) {
3739 word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords );
3740 if ( !Abc_TtEqual(pSimQ, pSimP, nWords) )
3741 continue;
3742 if ( fFirst ) {
3743 printf( "%5d :", i );
3744 fFirst = 0;
3745 Count++;
3746 }
3747 printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase );
3748 }
3749 if ( !fFirst )
3750 printf( "\n");
3751 }
3752 printf( "Found %d equivalent nodes.\n", Count );
3753 Vec_WrdFree( vSimsP );
3754 Vec_WrdFree( vSimsQ );
3755 Vec_WrdFree( vSimsPi );
3756}
3757
3758
3762
3763
3764ABC_NAMESPACE_IMPL_END
3765
nWords
int nWords
Definition abcNpn.c:127
Abc_RandomW
word Abc_RandomW(int fReset)
Definition utilSort.c:1022
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Abc_Random
unsigned Abc_Random(int fReset)
Definition utilSort.c:1004
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Exa_ManExactPrint
void Exa_ManExactPrint(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nDivs, int nOuts)
Definition bmcMaj.c:3935
Exa_ManExactSynthesis6Int
Mini_Aig_t * Exa_ManExactSynthesis6Int(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char *pFileName)
Definition bmcMaj.c:3945
Exa4_ManGenTest
Mini_Aig_t * Exa4_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char *pGuide)
Definition bmcMaj.c:2395
Exa6_WriteFile2
void Exa6_WriteFile2(char *pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:3263
Gia_ManDupMini
Gia_Man_t * Gia_ManDupMini(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Mini_Aig_t *pMini)
Definition bmcMaj.c:3368
p
Cube * p
Definition exorList.c:222
Extra_PrintBinary2
void Extra_PrintBinary2(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:523
Cbs2_ManSolveMiterNc
Vec_Int_t * Cbs2_ManSolveMiterNc(Gia_Man_t *pAig, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition giaCSat2.c:1559
Extra_BitMatrixTransposeP
ABC_NAMESPACE_IMPL_START void Extra_BitMatrixTransposeP(Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
DECLARATIONS ///.
Definition extraUtilMisc.c:2652
Kit_TruthToGia
ABC_NAMESPACE_IMPL_START int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition kitHop.c:80
Gia_ManFindMuxTree_rec
int Gia_ManFindMuxTree_rec(Gia_Man_t *pNew, int *pCtrl, int nCtrl, Vec_Int_t *vData, int Shift)
Definition giaMuxes.c:1146
Gia_ManPtrWrdReadBin
Vec_Ptr_t * Gia_ManPtrWrdReadBin(char *pFileName, int fVerbose)
Definition giaSimBase.c:2682
Gia_ManSimPatSimOut
Vec_Wrd_t * Gia_ManSimPatSimOut(Gia_Man_t *pGia, Vec_Wrd_t *vSimsPi, int fOuts)
Definition giaSimBase.c:138
Gia_ManSimPatAssignInputs
void Gia_ManSimPatAssignInputs(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, Vec_Wrd_t *vSimsIn)
FUNCTION DEFINITIONS ///.
Definition giaSimBase.c:85
Gia_ObjSimCollect
void Gia_ObjSimCollect(Gia_SimRsbMan_t *p)
Definition giaSimBase.c:993
Gia_RsbUpdateAdd
void Gia_RsbUpdateAdd(Gia_RsbMan_t *p, int iObj)
Definition giaSimBase.c:1819
Gia_ManSimTest
void Gia_ManSimTest(Gia_Man_t *pGia)
Definition giaSimBase.c:2405
Gia_ManPatGetOneQuo
float Gia_ManPatGetOneQuo(Gia_Man_t *p, int RareLimit, Vec_Wrd_t *vPatterns, int nWords, int n)
Definition giaSimBase.c:2337
Gia_SimAbsPerformOne
Vec_Int_t * Gia_SimAbsPerformOne(Gia_Man_t *pGia, word *pOffSet, word *pOnSet, Vec_Wrd_t *vSimsCands, int nWords, int fVerbose)
Definition giaSimBase.c:1686
Gia_SimQualityOne
Vec_Int_t * Gia_SimQualityOne(Gia_Man_t *p, Vec_Int_t *vPat, int fPoOnly)
Definition giaSimBase.c:2019
Gia_ManRelOutsTfo
Vec_Int_t * Gia_ManRelOutsTfo(Gia_Man_t *p, Vec_Int_t *vOuts)
Definition giaSimBase.c:3314
Gia_ManSimRsb
int Gia_ManSimRsb(Gia_Man_t *pGia, int nCands, int fVerbose)
Definition giaSimBase.c:1074
Gia_SimQualityPatternsMax
int Gia_SimQualityPatternsMax(Gia_Man_t *p, Vec_Int_t *vPat, int Iter, int fVerbose, Vec_Int_t *vStats)
Definition giaSimBase.c:2118
Gia_SimCollectRare
Vec_Int_t * Gia_SimCollectRare(Gia_Man_t *p, Vec_Wrd_t *vPatterns, int RareLimit)
Definition giaSimBase.c:2237
Gia_RsbFindMints
void Gia_RsbFindMints(Gia_RsbMan_t *p, int *pMint0, int *pMint1)
Definition giaSimBase.c:1916
Gia_ManSimPatHashPatterns
int Gia_ManSimPatHashPatterns(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, int *pnC0, int *pnC1)
Definition giaSimBase.c:706
Gia_ManRelInitOuts
Vec_Int_t * Gia_ManRelInitOuts()
Definition giaSimBase.c:3126
Gia_ManSimRelCollectOutputs
int Gia_ManSimRelCollectOutputs(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, int nWordsOut, Vec_Wrd_t *vSimsOut, Vec_Wrd_t *vRel)
Definition giaSimBase.c:1136
Gia_ManRelDeriveRel
Vec_Wrd_t * Gia_ManRelDeriveRel(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Vec_Wrd_t *vSims)
Definition giaSimBase.c:3349
Gia_ManRelInitOuts1
Vec_Int_t * Gia_ManRelInitOuts1()
Definition giaSimBase.c:3533
Gia_ManSim2ArrayOne
void Gia_ManSim2ArrayOne(Vec_Wrd_t *vSimsPi, Vec_Int_t *vRes)
Definition giaSimBase.c:2558
Gia_ManRelPrint2
void Gia_ManRelPrint2(Gia_Man_t *p, Vec_Int_t *vObjs, Vec_Wrd_t *vSims, Vec_Wrd_t *vRel)
Definition giaSimBase.c:3010
Gia_ManPatDistImprove
void Gia_ManPatDistImprove(Gia_Man_t *p, int fVerbose)
Definition giaSimBase.c:2174
Gia_SimRsbFunc
word * Gia_SimRsbFunc(Gia_SimRsbMan_t *p, int iObj, Vec_Int_t *vFanins, int fOnSet)
Definition giaSimBase.c:900
Gia_SimAbsRefine
int Gia_SimAbsRefine(Gia_SimAbsMan_t *p)
Definition giaSimBase.c:1609
Gia_ManSimTwo
int Gia_ManSimTwo(Gia_Man_t *p0, Gia_Man_t *p1, int nWords, int nRounds, int TimeLimit, int fVerbose)
Definition giaSimBase.c:2504
Gia_ManRelDeriveTest
void Gia_ManRelDeriveTest(Gia_Man_t *p)
Definition giaSimBase.c:3254
Gia_ManSimBitPackOne
int Gia_ManSimBitPackOne(int nWords, Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsCare, int iPat, int *pLits, int nLits)
Definition giaSimBase.c:640
Gia_ManPatCollectOne
Vec_Int_t * Gia_ManPatCollectOne(Gia_Man_t *p, Vec_Wrd_t *vPatterns, int n, int nWords)
Definition giaSimBase.c:2157
Gia_ManComputeTfos
Vec_Wec_t * Gia_ManComputeTfos(Gia_Man_t *p)
Definition giaSimBase.c:405
Gia_ManProcessBuffs
Vec_Int_t * Gia_ManProcessBuffs(Gia_Man_t *pHie, Vec_Wrd_t *vSimsH, int nWords, Vec_Mem_t *vStore, Vec_Int_t *vLabels)
Definition giaSimBase.c:2736
Gia_ManRelDeriveSimple
Vec_Int_t * Gia_ManRelDeriveSimple(Gia_Man_t *p, Vec_Wrd_t *vSims, Vec_Int_t *vIns, Vec_Int_t *vOuts)
Definition giaSimBase.c:3195
Gia_ManSim2Array
Vec_Wec_t * Gia_ManSim2Array(Vec_Ptr_t *vSims)
Definition giaSimBase.c:2570
Gia_SimRsbAlloc
Gia_SimRsbMan_t * Gia_SimRsbAlloc(Gia_Man_t *pGia)
Definition giaSimBase.c:821
Gia_ManComputeRange
Vec_Str_t * Gia_ManComputeRange(Gia_Man_t *p)
Definition giaSimBase.c:3685
Gia_ManCheckSimEquiv
int Gia_ManCheckSimEquiv(Gia_Man_t *p, int fVerbose)
Definition giaSimBase.c:452
Gia_ManSimPatSimIn
Vec_Wrd_t * Gia_ManSimPatSimIn(Gia_Man_t *pGia, Vec_Wrd_t *vSims, int fIns, Vec_Int_t *vAnds)
Definition giaSimBase.c:181
Gia_ManComparePrint
void Gia_ManComparePrint(Gia_Man_t *p, Gia_Man_t *q)
Definition giaSimBase.c:3718
Gia_ManCompareSims
void Gia_ManCompareSims(Gia_Man_t *pHie, Gia_Man_t *pFlat, int nWords, int fVerbose)
Definition giaSimBase.c:2811
Gia_ManSimRelAssignInputs
void Gia_ManSimRelAssignInputs(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, int nWordsIn, Vec_Wrd_t *vSimsIn)
Definition giaSimBase.c:1105
Gia_RsbRemovalCost
int Gia_RsbRemovalCost(Gia_RsbMan_t *p, int Index)
Definition giaSimBase.c:1879
Gia_ManRelSolve
void Gia_ManRelSolve(Gia_Man_t *p, Vec_Wrd_t *vSims, Vec_Int_t *vIns, Vec_Int_t *vOuts, Vec_Int_t *vRel, Vec_Int_t *vDivs)
Definition giaSimBase.c:3215
Gia_RsbUpdateRemove
void Gia_RsbUpdateRemove(Gia_RsbMan_t *p, int Index)
Definition giaSimBase.c:1845
Gia_ManSimCombine
Vec_Wrd_t * Gia_ManSimCombine(int nInputs, Vec_Wrd_t *vBase, Vec_Wrd_t *vAddOn, int nWordsUse)
Definition giaSimBase.c:620
Gia_ManRelDeriveTest2
void Gia_ManRelDeriveTest2(Gia_Man_t *p)
Definition giaSimBase.c:3086
Gia_ManSimRelDeriveFuncs
Vec_Wrd_t * Gia_ManSimRelDeriveFuncs(Gia_Man_t *p, Vec_Wrd_t *vRel, int nOuts)
Definition giaSimBase.c:1233
Gia_ManPatSatImprove
void Gia_ManPatSatImprove(Gia_Man_t *p, int nWords0, int fVerbose)
Definition giaSimBase.c:773
Gia_ManComparePair
int Gia_ManComparePair(Gia_Man_t *p, Vec_Wrd_t *vSims, int iOut, int nWords2)
Definition giaSimBase.c:442
Gia_ManSimPatSimTfo
void Gia_ManSimPatSimTfo(Gia_Man_t *p, Vec_Wrd_t *vSims, Vec_Int_t *vTfo)
Definition giaSimBase.c:3332
Gia_SimGenerateStats
Vec_Int_t * Gia_SimGenerateStats(Gia_Man_t *p)
Definition giaSimBase.c:2084
Gia_ManSimPatAssignInputs2
void Gia_ManSimPatAssignInputs2(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, Vec_Wrd_t *vSimsIn)
Definition giaSimBase.c:523
Gia_ManSimPatSimC
Vec_Wrd_t * Gia_ManSimPatSimC(Gia_Man_t *pGia, Vec_Wrd_t *vSims, Vec_Wrd_t *vSimsCiC)
Definition giaSimBase.c:233
Gia_SimRsbFree
void Gia_SimRsbFree(Gia_SimRsbMan_t *p)
Definition giaSimBase.c:839
Gia_SimAbsSolve
void Gia_SimAbsSolve(Gia_SimAbsMan_t *p)
Definition giaSimBase.c:1520
Gia_SimAbsFind
Vec_Int_t * Gia_SimAbsFind(Vec_Int_t *vValues, int Value)
Definition giaSimBase.c:1648
Gia_ManSimPatSim
Vec_Wrd_t * Gia_ManSimPatSim(Gia_Man_t *pGia)
Definition giaSimBase.c:125
Gia_ManSimProfile
void Gia_ManSimProfile(Gia_Man_t *pGia)
Definition giaSimBase.c:764
Gia_ManPatGetQuo
float Gia_ManPatGetQuo(Gia_Man_t *p, Vec_Int_t *vRareCounts, Vec_Wrd_t *vSims, int n, int nWords)
Definition giaSimBase.c:2307
Gia_ManRelCheck_rec
int Gia_ManRelCheck_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaSimBase.c:3411
Gia_SimAbsAlloc
Gia_SimAbsMan_t * Gia_SimAbsAlloc(Gia_Man_t *pGia, word *pOffSet, word *pOnSet, Vec_Wrd_t *vSims, int nWords, Vec_Int_t *vResub, int fVerbose)
Definition giaSimBase.c:1425
Gia_ManRelCheck
int Gia_ManRelCheck(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts)
Definition giaSimBase.c:3435
Gia_ManRelDerive2
Vec_Wrd_t * Gia_ManRelDerive2(Gia_Man_t *p, Vec_Int_t *vObjs, Vec_Wrd_t *vSims)
Definition giaSimBase.c:2959
Gia_ManRelPrint
void Gia_ManRelPrint(Gia_Man_t *p, Vec_Int_t *vObjs, Vec_Wrd_t *vSims, Vec_Wrd_t *vRel)
Definition giaSimBase.c:2982
Gia_ManRelInitObjs
Vec_Int_t * Gia_ManRelInitObjs()
Definition giaSimBase.c:3059
Gia_SimAbsMan_t
struct Gia_SimAbsMan_t_ Gia_SimAbsMan_t
Definition giaSimBase.c:50
Gia_ManRelInitDivs1
Vec_Int_t * Gia_ManRelInitDivs1()
Definition giaSimBase.c:3524
Gia_ManRelInitMffc
Vec_Int_t * Gia_ManRelInitMffc(Gia_Man_t *p, Vec_Int_t *vOuts)
Definition giaSimBase.c:3133
Gia_RsbFindNodeToRemove
int Gia_RsbFindNodeToRemove(Gia_RsbMan_t *p, int *pMinCost)
Definition giaSimBase.c:1899
Gia_SimRsbCareSet
word * Gia_SimRsbCareSet(Gia_SimRsbMan_t *p, int iObj, Vec_Int_t *vTfo)
Definition giaSimBase.c:959
Gia_RsbAlloc
Gia_RsbMan_t * Gia_RsbAlloc(Gia_Man_t *pGia, word *pOffSet, word *pOnSet, Vec_Wrd_t *vSims, int nWords, Vec_Wrd_t *vSimsT, int nWordsT, Vec_Int_t *vCands)
Definition giaSimBase.c:1734
Gia_SimAbsInit
void Gia_SimAbsInit(Gia_SimAbsMan_t *p)
Definition giaSimBase.c:1656
Gia_ManRelDeriveSims
void Gia_ManRelDeriveSims(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Vec_Wrd_t *vSims, Vec_Wrd_t *vRel, Vec_Wrd_t **pvSimsIn, Vec_Wrd_t **pvSimsOut)
Definition giaSimBase.c:3378
Gia_SimCollectBest
Vec_Int_t * Gia_SimCollectBest(Vec_Flt_t *vQuo)
Definition giaSimBase.c:2295
Gia_ManDeriveNodeFuncs
Vec_Wrd_t * Gia_ManDeriveNodeFuncs(Gia_Man_t *p)
Definition giaSimBase.c:291
Gia_ManRelInitIns
Vec_Int_t * Gia_ManRelInitIns()
Definition giaSimBase.c:3115
Gia_ManPatRareImprove
void Gia_ManPatRareImprove(Gia_Man_t *p, int RareLimit, int fVerbose)
Definition giaSimBase.c:2350
Gia_ManSimGen
void Gia_ManSimGen(Gia_Man_t *pGia)
Definition giaSimBase.c:2443
Gia_RsbSolve
Vec_Int_t * Gia_RsbSolve(Gia_RsbMan_t *p)
Definition giaSimBase.c:1974
Gia_RsbFindNode
int Gia_RsbFindNode(Gia_RsbMan_t *p)
Definition giaSimBase.c:1929
Gia_ManRelInitIns1
Vec_Int_t * Gia_ManRelInitIns1()
Definition giaSimBase.c:3515
Gia_SimAbsCheckSolution
void Gia_SimAbsCheckSolution(Gia_SimAbsMan_t *p)
Definition giaSimBase.c:1464
Gia_ManPtrWrdDumpBin
void Gia_ManPtrWrdDumpBin(char *pFileName, Vec_Ptr_t *p, int fVerbose)
Definition giaSimBase.c:2660
Gia_ManSimPatStart
Vec_Int_t * Gia_ManSimPatStart(int nItems)
Definition giaSimBase.c:1377
Gia_ManFindDividerVar
int Gia_ManFindDividerVar(Gia_Man_t *p, int fVerbose)
Definition giaSimBase.c:430
Gia_SimRsbTfo_rec
void Gia_SimRsbTfo_rec(Gia_Man_t *p, int iObj, int iFanout, Vec_Int_t *vTfo)
Definition giaSimBase.c:865
Gia_ManSimRelPrint
void Gia_ManSimRelPrint(Gia_Man_t *p, Vec_Wrd_t *vRel, Vec_Int_t *vOutMints)
Definition giaSimBase.c:1326
Gia_ManRelDeriveTest1
void Gia_ManRelDeriveTest1(Gia_Man_t *p)
Definition giaSimBase.c:3597
Gia_RsbPrint
void Gia_RsbPrint(Gia_RsbMan_t *p)
Definition giaSimBase.c:1802
Gia_ManSimPatSimMiter
void Gia_ManSimPatSimMiter(Gia_Man_t *p, Vec_Wrd_t *vSims, Vec_Wrd_t *vSims2, word *pSims, int nWords)
Definition giaSimBase.c:3342
Gia_ObjSimRsb
int Gia_ObjSimRsb(Gia_SimRsbMan_t *p, int iObj, int nCands, int fVerbose, int *pnBufs, int *pnInvs)
Definition giaSimBase.c:1042
Gia_SimRsbMan_t
typedefABC_NAMESPACE_IMPL_START struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t
DECLARATIONS ///.
Definition giaSimBase.c:35
Gia_ManArray2Sim
Vec_Ptr_t * Gia_ManArray2Sim(Vec_Wec_t *vRes)
Definition giaSimBase.c:2596
Gia_ManSimPatValues
Vec_Wrd_t * Gia_ManSimPatValues(Gia_Man_t *p)
Definition giaSimBase.c:594
Gia_SimQualityImpact
Vec_Flt_t * Gia_SimQualityImpact(Gia_Man_t *p, Vec_Int_t *vPat, Vec_Int_t *vRareCounts)
Definition giaSimBase.c:2259
Gia_RsbMan_t
struct Gia_RsbMan_t_ Gia_RsbMan_t
Definition giaSimBase.c:1717
Gia_ManArray2SimOne
Vec_Wrd_t * Gia_ManArray2SimOne(Vec_Int_t *vRes)
Definition giaSimBase.c:2579
Gia_ManSimRelCompare
int Gia_ManSimRelCompare(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, int nWordsOut, Vec_Wrd_t *vSimsOut, int iPat, int iMint)
Definition giaSimBase.c:1115
Gia_Sim5CollectValues
Vec_Int_t * Gia_Sim5CollectValues(word *pOffSet, word *pOnSet, int nWords)
Definition giaSimBase.c:1412
Gia_ManSimPatSimInTest
void Gia_ManSimPatSimInTest(Gia_Man_t *pGia)
Definition giaSimBase.c:203
Gia_ManSimPatWrite
void Gia_ManSimPatWrite(char *pFileName, Vec_Wrd_t *vSimsIn, int nWords)
Definition giaSimBase.c:274
Gia_ManSimPatSimCTest
void Gia_ManSimPatSimCTest(Gia_Man_t *pGia)
Definition giaSimBase.c:246
Gia_ManSimRelTest
void Gia_ManSimRelTest(Gia_Man_t *p)
Definition giaSimBase.c:1386
Gia_ManChangeTest3
Gia_Man_t * Gia_ManChangeTest3(Gia_Man_t *p)
Definition giaSimBase.c:3639
Gia_ManSimPatGenMiter
Gia_Man_t * Gia_ManSimPatGenMiter(Gia_Man_t *p, Vec_Wrd_t *vSims)
Definition giaSimBase.c:727
Gia_ManSimRel
Vec_Wrd_t * Gia_ManSimRel(Gia_Man_t *p, Vec_Int_t *vObjs, Vec_Wrd_t *vVals)
Definition giaSimBase.c:1154
Gia_RsbFree
void Gia_RsbFree(Gia_RsbMan_t *p)
Definition giaSimBase.c:1781
Gia_SimComputeScore
double Gia_SimComputeScore(Gia_Man_t *p, Vec_Int_t *vTotal, Vec_Int_t *vThis)
Definition giaSimBase.c:2105
Gia_ManSimArrayTest
void Gia_ManSimArrayTest(Vec_Wrd_t *vSimsPi)
Definition giaSimBase.c:2605
Gia_SimRsbResubVerify
int Gia_SimRsbResubVerify(Gia_SimRsbMan_t *p, int iObj, Vec_Int_t *vFanins)
Definition giaSimBase.c:921
Gia_ManSimPatValuesDerive
void Gia_ManSimPatValuesDerive(Gia_Man_t *p, int nWords, Vec_Wrd_t *vSims, Vec_Wrd_t *vValues)
Definition giaSimBase.c:586
Gia_ManSimPatSim2
Vec_Wrd_t * Gia_ManSimPatSim2(Gia_Man_t *pGia)
Definition giaSimBase.c:561
Gia_ManUpdateCoPhase
void Gia_ManUpdateCoPhase(Gia_Man_t *pNew, Gia_Man_t *pOld)
Definition giaSimBase.c:2787
Gia_SimAbsFree
void Gia_SimAbsFree(Gia_SimAbsMan_t *p)
Definition giaSimBase.c:1443
Gia_RsbCost
int Gia_RsbCost(Gia_RsbMan_t *p)
Definition giaSimBase.c:1795
Gia_SimRsbTfo
Vec_Int_t * Gia_SimRsbTfo(Gia_SimRsbMan_t *p, int iObj, int iFanout)
Definition giaSimBase.c:876
Gia_ManRelTfos
Vec_Wec_t * Gia_ManRelTfos(Gia_Man_t *p, Vec_Int_t *vObjs)
Definition giaSimBase.c:2891
Gia_ManRelDerive
Vec_Wrd_t * Gia_ManRelDerive(Gia_Man_t *p, Vec_Int_t *vObjs, Vec_Wrd_t *vSims)
Definition giaSimBase.c:2915
Gia_ManRelOutsTfo_rec
int Gia_ManRelOutsTfo_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vTfo)
Definition giaSimBase.c:3289
Gia_ObjSimCands
Vec_Int_t * Gia_ObjSimCands(Gia_SimRsbMan_t *p, int iObj, int nCands)
Definition giaSimBase.c:1010
Gia_ManPerformMuxDec
Gia_Man_t * Gia_ManPerformMuxDec(Gia_Man_t *p)
Definition giaSimBase.c:335
Gia_RsbCollectValid
int Gia_RsbCollectValid(Gia_RsbMan_t *p)
Definition giaSimBase.c:1962
Gia_SimQualityTest
void Gia_SimQualityTest(Gia_Man_t *p)
Definition giaSimBase.c:2064
Gia_ManRelCompute
void Gia_ManRelCompute(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Vec_Wrd_t **pvSimsIn, Vec_Wrd_t **pvSimsOut)
Definition giaSimBase.c:3454
Gia_RsbSetFind
Vec_Int_t * Gia_RsbSetFind(word *pOffSet, word *pOnSet, Vec_Wrd_t *vSims, int nWords, Vec_Wrd_t *vSimsT, int nWordsT, Vec_Int_t *vCands)
Definition giaSimBase.c:1999
Gia_ManRelInitDivs
Vec_Int_t * Gia_ManRelInitDivs(Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vOuts)
Definition giaSimBase.c:3162
Gia_ManSimPatResim
void Gia_ManSimPatResim(Gia_Man_t *pGia, Vec_Int_t *vObjs, int nWords, Vec_Wrd_t *vSims)
Definition giaSimBase.c:264
Gia_ManComputeTfos_rec
int Gia_ManComputeTfos_rec(Gia_Man_t *p, int iObj, int iRoot, Vec_Int_t *vNode)
Definition giaSimBase.c:385
Gia_ManSimRelDeriveFuncs2
Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2(Gia_Man_t *p, Vec_Wrd_t *vRel, int nOuts)
Definition giaSimBase.c:1257
Gia_ManPatUpdateOne
void Gia_ManPatUpdateOne(Gia_Man_t *p, Vec_Wrd_t *vPatterns, int n, int nWords, Vec_Int_t *vPat)
Definition giaSimBase.c:2164
Gia_ManDeriveFuncs
word * Gia_ManDeriveFuncs(Gia_Man_t *p)
Definition giaSimBase.c:306
Gia_ManPatGetTotalQuo
float Gia_ManPatGetTotalQuo(Gia_Man_t *p, int RareLimit, Vec_Wrd_t *vPatterns, int nWords)
Definition giaSimBase.c:2323
Gia_ManSimRelCheckFuncs
void Gia_ManSimRelCheckFuncs(Gia_Man_t *p, Vec_Wrd_t *vRel, int nOuts, Vec_Wrd_t *vFuncs)
Definition giaSimBase.c:1196
Gia_ManSimBitPacking
Vec_Wrd_t * Gia_ManSimBitPacking(Gia_Man_t *p, Vec_Int_t *vCexStore, int nCexes, int nUnDecs)
Definition giaSimBase.c:668
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_ManStaticFanoutStart
void Gia_ManStaticFanoutStart(Gia_Man_t *p)
Definition giaFanout.c:238
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition giaHash.c:125
Gia_ManStaticFanoutStop
void Gia_ManStaticFanoutStop(Gia_Man_t *p)
Definition giaFanout.c:393
Gia_ManForEachBuf
#define Gia_ManForEachBuf(p, pObj, i)
Definition gia.h:1210
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachCoId
#define Gia_ManForEachCoId(p, Id, i)
Definition gia.h:1240
Gia_ManForEachCand
#define Gia_ManForEachCand(p, pObj, i)
Definition gia.h:1220
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManForEachCoDriverId
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManCleanPhase
void Gia_ManCleanPhase(Gia_Man_t *p)
Definition giaUtil.c:472
Gia_ManTransferTiming
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2370
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ObjForEachFanoutStaticId
#define Gia_ObjForEachFanoutStaticId(p, Id, FanId, i)
Definition gia.h:1127
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
Gia_ManForEachAndId
#define Gia_ManForEachAndId(p, i)
Definition gia.h:1216
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Mini_Aig_t
struct Mini_Aig_t_ Mini_Aig_t
BASIC TYPES ///.
Definition miniaig.h:48
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::vSimsPi
Vec_Wrd_t * vSimsPi
Definition gia.h:215
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::iDiff1
unsigned iDiff1
Definition gia.h:84
Gia_Obj_t_::fCompl1
unsigned fCompl1
Definition gia.h:85
Gia_Obj_t_::fCompl0
unsigned fCompl0
Definition gia.h:80
Gia_Obj_t_::iDiff0
unsigned iDiff0
Definition gia.h:79
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_RsbMan_t_
Definition giaSimBase.c:1719
Gia_RsbMan_t_::nWords
int nWords
Definition giaSimBase.c:1723
Gia_RsbMan_t_::pSet
word * pSet[3]
Definition giaSimBase.c:1731
Gia_RsbMan_t_::vActive
Vec_Int_t * vActive
Definition giaSimBase.c:1732
Gia_RsbMan_t_::vCands
Vec_Int_t * vCands
Definition giaSimBase.c:1727
Gia_RsbMan_t_::pOffSet
word * pOffSet
Definition giaSimBase.c:1721
Gia_RsbMan_t_::vSims
Vec_Wrd_t * vSims
Definition giaSimBase.c:1725
Gia_RsbMan_t_::vObjs
Vec_Int_t * vObjs
Definition giaSimBase.c:1728
Gia_RsbMan_t_::vObjs2
Vec_Int_t * vObjs2
Definition giaSimBase.c:1729
Gia_RsbMan_t_::nWordsT
int nWordsT
Definition giaSimBase.c:1724
Gia_RsbMan_t_::vSets
Vec_Wec_t * vSets[2]
Definition giaSimBase.c:1730
Gia_RsbMan_t_::pOnSet
word * pOnSet
Definition giaSimBase.c:1722
Gia_RsbMan_t_::pGia
Gia_Man_t * pGia
Definition giaSimBase.c:1720
Gia_RsbMan_t_::vSimsT
Vec_Wrd_t * vSimsT
Definition giaSimBase.c:1726
Gia_SimAbsMan_t_
Definition giaSimBase.c:52
Gia_SimAbsMan_t_::pSet
word * pSet[2]
Definition giaSimBase.c:55
Gia_SimAbsMan_t_::pGia
Gia_Man_t * pGia
Definition giaSimBase.c:54
Gia_SimAbsMan_t_::vPatPairs
Vec_Int_t * vPatPairs
Definition giaSimBase.c:63
Gia_SimAbsMan_t_::fVerbose
int fVerbose
Definition giaSimBase.c:60
Gia_SimAbsMan_t_::nWordsTable
int nWordsTable
Definition giaSimBase.c:64
Gia_SimAbsMan_t_::vResub
Vec_Int_t * vResub
Definition giaSimBase.c:59
Gia_SimAbsMan_t_::nWords
int nWords
Definition giaSimBase.c:57
Gia_SimAbsMan_t_::vValues
Vec_Int_t * vValues
Definition giaSimBase.c:62
Gia_SimAbsMan_t_::vTtMints
Vec_Int_t * vTtMints
Definition giaSimBase.c:67
Gia_SimAbsMan_t_::vSims
Vec_Wrd_t * vSims
Definition giaSimBase.c:58
Gia_SimAbsMan_t_::nCands
int nCands
Definition giaSimBase.c:56
Gia_SimAbsMan_t_::pTableTemp
word * pTableTemp
Definition giaSimBase.c:65
Gia_SimAbsMan_t_::vCoverTable
Vec_Wrd_t * vCoverTable
Definition giaSimBase.c:66
Gia_SimRsbMan_t_
Definition giaSimBase.c:37
Gia_SimRsbMan_t_::vTfo
Vec_Int_t * vTfo
Definition giaSimBase.c:39
Gia_SimRsbMan_t_::pGia
Gia_Man_t * pGia
Definition giaSimBase.c:38
Gia_SimRsbMan_t_::vFanins
Vec_Int_t * vFanins
Definition giaSimBase.c:41
Gia_SimRsbMan_t_::vSimsObj
Vec_Wrd_t * vSimsObj
Definition giaSimBase.c:43
Gia_SimRsbMan_t_::nWords
int nWords
Definition giaSimBase.c:45
Gia_SimRsbMan_t_::vSimsObj2
Vec_Wrd_t * vSimsObj2
Definition giaSimBase.c:44
Gia_SimRsbMan_t_::vFanins2
Vec_Int_t * vFanins2
Definition giaSimBase.c:42
Gia_SimRsbMan_t_::pFunc
word * pFunc[3]
Definition giaSimBase.c:46
Gia_SimRsbMan_t_::vCands
Vec_Int_t * vCands
Definition giaSimBase.c:40
Vec_Mem_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
memset
char * memset()
memcmp
int memcmp()
memmove
char * memmove()
rewind
VOID_HACK rewind()
Vec_FltForEachEntry
#define Vec_FltForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecFlt.h:54
Vec_Flt_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Flt_t_ Vec_Flt_t
INCLUDES ///.
Definition vecFlt.h:42
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryTwo
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition vecInt.h:66
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_StrForEachEntry
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecStr.h:54
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_WecForEachLevelTwo
#define Vec_WecForEachLevelTwo(vGlob1, vGlob2, vVec1, vVec2, i)
Definition vecWec.h:69
Vec_WecForEachLevelStop
#define Vec_WecForEachLevelStop(vGlob, vVec, i, LevelStop)
Definition vecWec.h:61
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42
SEEK_END
#define SEEK_END
Definition zconf.h:392