ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ifDsd.c
Go to the documentation of this file.
1
20
21#include <math.h>
22#include "if.h"
23#include "ifCount.h"
24#include "misc/extra/extra.h"
25#include "sat/bsat/satSolver.h"
26#include "aig/gia/gia.h"
27#include "bool/kit/kit.h"
28
29#ifdef ABC_USE_CUDD
30#include "bdd/extrab/extraBdd.h"
31#endif
32
33#ifdef ABC_USE_PTHREADS
34
35#ifdef _WIN32
36#include "../lib/pthread.h"
37#else
38#include <pthread.h>
39#include <unistd.h>
40#endif
41
42#endif
43
44ABC_NAMESPACE_IMPL_START
45
46
50
51#define DSD_VERSION "dsd1"
52
53// network types
54typedef enum {
55 IF_DSD_NONE = 0, // 0: unknown
56 IF_DSD_CONST0, // 1: constant
57 IF_DSD_VAR, // 2: variable
58 IF_DSD_AND, // 3: AND
59 IF_DSD_XOR, // 4: XOR
60 IF_DSD_MUX, // 5: MUX
61 IF_DSD_PRIME // 6: PRIME
62} If_DsdType_t;
63
64typedef struct If_DsdObj_t_ If_DsdObj_t;
65struct If_DsdObj_t_
66{
67 unsigned Id; // node ID
68 unsigned Type : 3; // node type
69 unsigned nSupp : 5; // variable
70 unsigned fMark : 1; // user mark
71 unsigned Count : 18; // variable
72 unsigned nFans : 5; // fanin count
73 unsigned pFans[0]; // fanins
74};
75
76struct If_DsdMan_t_
77{
78 char * pStore; // input/output file
79 int nVars; // max var number
80 int LutSize; // LUT size
81 int nWords; // word number
82 int nBins; // table size
83 unsigned * pBins; // hash table
84 Mem_Flex_t * pMem; // memory for nodes
85 Vec_Ptr_t vObjs; // objects
86 Vec_Int_t vNexts; // next pointers
87 Vec_Int_t vTruths; // truth IDs of prime nodes
88 Vec_Int_t * vTemp1; // temp
89 Vec_Int_t * vTemp2; // temp
90 word ** pTtElems; // elementary TTs
91 Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
92 Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
93 Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function
94 int * pSched[IF_MAX_FUNC_LUTSIZE+1]; // grey code schedules
95 int nTtBits; // the number of truth table bits
96 int nConfigWords; // the number of words for config data per node
97 Vec_Wrd_t * vConfigs; // permutations
98 Gia_Man_t * pTtGia; // GIA to represent truth tables
99 Vec_Int_t * vCover; // temporary memory
100 void * pSat; // SAT solver
101 char * pCellStr; // symbolic cell description
102 int nObjsPrev; // previous number of objects
103 int fNewAsUseless; // set new as useless
104 int nUniqueHits; // statistics
105 int nUniqueMisses; // statistics
106 abctime timeDsd; // statistics
107 abctime timeCanon; // statistics
108 abctime timeCheck; // statistics
109 abctime timeCheck2; // statistics
110 abctime timeVerify; // statistics
111};
112
113static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
114static inline int If_DsdObjTruthId( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return (pObj->Type == IF_DSD_PRIME && pObj->nFans > 2) ? Vec_IntEntry(&p->vTruths, pObj->Id) : -1; }
115static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem[pObj->nFans], If_DsdObjTruthId(p, pObj)); }
116static inline void If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); Vec_IntWriteEntry(&p->vTruths, pObj->Id, Id); }
117
118static inline void If_DsdObjClean( If_DsdObj_t * pObj ) { memset( pObj, 0, sizeof(If_DsdObj_t) ); }
119static inline int If_DsdObjId( If_DsdObj_t * pObj ) { return pObj->Id; }
120static inline int If_DsdObjType( If_DsdObj_t * pObj ) { return pObj->Type; }
121static inline int If_DsdObjIsVar( If_DsdObj_t * pObj ) { return (int)(pObj->Type == IF_DSD_VAR); }
122static inline int If_DsdObjSuppSize( If_DsdObj_t * pObj ) { return pObj->nSupp; }
123static inline int If_DsdObjFaninNum( If_DsdObj_t * pObj ) { return pObj->nFans; }
124static inline int If_DsdObjFaninC( If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); }
125static inline int If_DsdObjFaninLit( If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return pObj->pFans[i]; }
126
127static inline If_DsdObj_t * If_DsdVecObj( Vec_Ptr_t * p, int Id ) { return (If_DsdObj_t *)Vec_PtrEntry(p, Id); }
128static inline If_DsdObj_t * If_DsdVecConst0( Vec_Ptr_t * p ) { return If_DsdVecObj( p, 0 ); }
129static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v ) { return If_DsdVecObj( p, v+1 ); }
130static inline int If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->nSupp; }
131static inline int If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) ); }
132static inline int If_DsdVecObjRef( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->Count; }
133static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x3FFFF ) If_DsdVecObj( p, iObj )->Count++; }
134static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
135static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; }
136static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; }
137static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 0; }
138
139#define If_DsdVecForEachObj( vVec, pObj, i ) \
140 Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
141#define If_DsdVecForEachObjStart( vVec, pObj, i, Start ) \
142 Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, Start )
143#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \
144 for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ )
145#define If_DsdVecForEachNode( vVec, pObj, i ) \
146 Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, 2 )
147#define If_DsdObjForEachFanin( vVec, pObj, pFanin, i ) \
148 for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((pFanin) = If_DsdObjFanin(vVec, pObj, i)); i++ )
149#define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \
150 for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ )
151
152extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
153
157
169char * If_DsdManFileName( If_DsdMan_t * p )
170{
171 return p->pStore;
172}
173int If_DsdManVarNum( If_DsdMan_t * p )
174{
175 return p->nVars;
176}
177int If_DsdManObjNum( If_DsdMan_t * p )
178{
179 return Vec_PtrSize( &p->vObjs );
180}
181int If_DsdManLutSize( If_DsdMan_t * p )
182{
183 return p->LutSize;
184}
185int If_DsdManTtBitNum( If_DsdMan_t * p )
186{
187 return p->nTtBits;
188}
189int If_DsdManPermBitNum( If_DsdMan_t * p )
190{
191 return (Abc_Base2Log(p->nVars + 1) + 1) * p->nVars;
192}
193void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize )
194{
195 p->LutSize = nLutSize;
196}
197int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd )
198{
199 return If_DsdVecLitSuppSize( &p->vObjs, iDsd );
200}
201int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
202{
203 return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
204}
205int If_DsdManReadMark( If_DsdMan_t * p, int iDsd )
206{
207 return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
208}
209void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
210{
211 if ( p->nObjsPrev == 0 )
212 p->nObjsPrev = If_DsdManObjNum(p);
213 p->fNewAsUseless = 1;
214}
215word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd )
216{
217 return p->vConfigs ? Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Abc_Lit2Var(iDsd)) : NULL;
218}
219char * If_DsdManGetCellStr( If_DsdMan_t * p )
220{
221 return p->pCellStr;
222}
223
235static inline word ** If_ManDsdTtElems()
236{
237 static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
238 if ( pTtElems[0] == NULL )
239 {
240 int v;
241 for ( v = 0; v <= DAU_MAX_VAR; v++ )
242 pTtElems[v] = TtElems[v];
243 Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
244 }
245 return pTtElems;
246}
247If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
248{
249 int nWords = If_DsdObjWordNum( nFans );
250 If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
251 If_DsdObjClean( pObj );
252 pObj->Type = Type;
253 pObj->nFans = nFans;
254 pObj->Id = Vec_PtrSize( &p->vObjs );
255 pObj->fMark = p->fNewAsUseless;
256 pObj->Count = 0;
257 Vec_PtrPush( &p->vObjs, pObj );
258 Vec_IntPush( &p->vNexts, 0 );
259 Vec_IntPush( &p->vTruths, -1 );
260 assert( Vec_IntSize(&p->vNexts) == Vec_PtrSize(&p->vObjs) );
261 assert( Vec_IntSize(&p->vTruths) == Vec_PtrSize(&p->vObjs) );
262 return pObj;
263}
264If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
265{
266 If_DsdMan_t * p; int v;
267 char pFileName[100];
268 assert( nVars <= DAU_MAX_VAR );
269 sprintf( pFileName, "%02d.dsd", nVars );
270 p = ABC_CALLOC( If_DsdMan_t, 1 );
271 p->pStore = Abc_UtilStrsav( pFileName );
272 p->nVars = nVars;
273 p->LutSize = LutSize;
274 p->nWords = Abc_TtWordNum( nVars );
275 p->nBins = Abc_PrimeCudd( 100000 );
276 p->pBins = ABC_CALLOC( unsigned, p->nBins );
277 p->pMem = Mem_FlexStart();
278 p->nConfigWords = 1;
279 Vec_PtrGrow( &p->vObjs, 10000 );
280 Vec_IntGrow( &p->vNexts, 10000 );
281 Vec_IntGrow( &p->vTruths, 10000 );
282 If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
283 If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
284 p->vTemp1 = Vec_IntAlloc( 32 );
285 p->vTemp2 = Vec_IntAlloc( 32 );
286 p->pTtElems = If_ManDsdTtElems();
287 for ( v = 3; v <= nVars; v++ )
288 {
289 p->vTtMem[v] = Vec_MemAlloc( Abc_TtWordNum(v), 12 );
290 Vec_MemHashAlloc( p->vTtMem[v], 10000 );
291 p->vTtDecs[v] = Vec_PtrAlloc( 1000 );
292 }
293/*
294 p->pTtGia = Gia_ManStart( nVars );
295 Gia_ManHashAlloc( p->pTtGia );
296 for ( v = 0; v < nVars; v++ )
297 Gia_ManAppendCi( p->pTtGia );
298*/
299 for ( v = 2; v < nVars; v++ )
300 p->pSched[v] = Extra_GreyCodeSchedule( v );
301 if ( LutSize )
302 p->pSat = If_ManSatBuildXY( LutSize );
303 p->vCover = Vec_IntAlloc( 0 );
304 return p;
305}
306void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize )
307{
308 Vec_Int_t * vLevel;
309 int v, i, fCompl;
310 word * pTruth;
311 if ( p->vIsops[3] != NULL )
312 return;
313 if ( Vec_PtrSize(&p->vObjs) > 2 )
314 printf( "Warning: DSD manager is already started without ISOPs.\n" );
315 for ( v = 3; v <= nLutSize; v++ )
316 {
317 p->vIsops[v] = Vec_WecAlloc( 100 );
318 Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
319 {
320 vLevel = Vec_WecPushLevel( p->vIsops[v] );
321 fCompl = Kit_TruthIsop( (unsigned *)pTruth, v, p->vCover, 1 );
322 if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
323 {
324 Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
325 Vec_IntAppend( vLevel, p->vCover );
326 if ( fCompl )
327 vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
328 }
329 }
330 assert( Vec_WecSize(p->vIsops[v]) == Vec_MemEntryNum(p->vTtMem[v]) );
331 }
332}
333void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
334{
335 int v;
336// If_DsdManDumpDsd( p );
337 if ( fVerbose )
338 If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 );
339 if ( fVerbose )
340 {
341 char FileName[10];
342 for ( v = 3; v <= p->nVars; v++ )
343 {
344 sprintf( FileName, "dumpdsd%02d", v );
345 Vec_MemDumpTruthTables( p->vTtMem[v], FileName, v );
346 }
347 }
348 for ( v = 2; v < p->nVars; v++ )
349 ABC_FREE( p->pSched[v] );
350 for ( v = 3; v <= p->nVars; v++ )
351 {
352 Vec_MemHashFree( p->vTtMem[v] );
353 Vec_MemFree( p->vTtMem[v] );
354 Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) );
355 if ( p->vIsops[v] )
356 Vec_WecFree( p->vIsops[v] );
357 }
358 Vec_WrdFreeP( &p->vConfigs );
359 Vec_IntFreeP( &p->vTemp1 );
360 Vec_IntFreeP( &p->vTemp2 );
361 ABC_FREE( p->vObjs.pArray );
362 ABC_FREE( p->vNexts.pArray );
363 ABC_FREE( p->vTruths.pArray );
364 Mem_FlexStop( p->pMem, 0 );
365 Gia_ManStopP( &p->pTtGia );
366 Vec_IntFreeP( &p->vCover );
367 If_ManSatUnbuild( p->pSat );
368 ABC_FREE( p->pCellStr );
369 ABC_FREE( p->pStore );
370 ABC_FREE( p->pBins );
371 ABC_FREE( p );
372}
373void If_DsdManDumpDsd( If_DsdMan_t * p, int Support )
374{
375 char * pFileName = "tts_nondsd.txt";
376 If_DsdObj_t * pObj;
377 Vec_Int_t * vMap;
378 FILE * pFile = fopen( pFileName, "wb" );
379 int v, i;
380 if ( pFile == NULL )
381 {
382 printf( "Cannot open file \"%s\".\n", pFileName );
383 return;
384 }
385 for ( v = 3; v <= p->nVars; v++ )
386 {
387 vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem[v]) );
388 If_DsdVecForEachObj( &p->vObjs, pObj, i )
389 {
390 if ( Support && Support != If_DsdObjSuppSize(pObj) )
391 continue;
392 if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
393 continue;
394 if ( Vec_IntEntry(vMap, If_DsdObjTruthId(p, pObj)) )
395 continue;
396 Vec_IntWriteEntry(vMap, If_DsdObjTruthId(p, pObj), 1);
397 fprintf( pFile, "0x" );
398 Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : v );
399 fprintf( pFile, "\n" );
400 //printf( " " );
401 //Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
402 }
403 Vec_IntFree( vMap );
404 }
405 fclose( pFile );
406}
407void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
408{
409 extern word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits );
410 char * pFileName = "tts_all.txt";
411 If_DsdObj_t * pObj;
412 word * pRes; int i;
413 FILE * pFile = fopen( pFileName, "wb" );
414 if ( pFile == NULL )
415 {
416 printf( "Cannot open file \"%s\".\n", pFileName );
417 return;
418 }
419 If_DsdVecForEachObj( &p->vObjs, pObj, i )
420 {
421 if ( Support && Support != If_DsdObjSuppSize(pObj) )
422 continue;
423 pRes = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
424 fprintf( pFile, "0x" );
425 Abc_TtPrintHexRev( pFile, pRes, Support ? Abc_MaxInt(Support, 6) : p->nVars );
426 fprintf( pFile, "\n" );
427// printf( " " );
428// Dau_DsdPrintFromTruth( pRes, p->nVars );
429 }
430 fclose( pFile );
431}
432int If_DsdManHasMarks( If_DsdMan_t * p )
433{
434 If_DsdObj_t * pObj;
435 int i;
436 If_DsdVecForEachObj( &p->vObjs, pObj, i )
437 if ( pObj->fMark )
438 return 1;
439 return 0;
440}
441
453void If_DsdManHashProfile( If_DsdMan_t * p )
454{
455 If_DsdObj_t * pObj;
456 unsigned * pSpot;
457 int i, Counter;
458 for ( i = 0; i < p->nBins; i++ )
459 {
460 Counter = 0;
461 for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(&p->vNexts, pObj->Id), Counter++ )
462 pObj = If_DsdVecObj( &p->vObjs, *pSpot );
463// if ( Counter > 5 )
464// printf( "%d ", Counter );
465// if ( i > 10000 )
466// break;
467 }
468// printf( "\n" );
469}
470int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id )
471{
472 If_DsdObj_t * pObj;
473 int i, iFanin;
474 pObj = If_DsdVecObj( &p->vObjs, Id );
475 if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
476 return 0;
477 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
478 return 0;
479 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
480 return 1;
481 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
482 if ( If_DsdManCheckNonDec_rec( p, Abc_Lit2Var(iFanin) ) )
483 return 1;
484 return 0;
485}
486void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned char * pPermLits, int * pnSupp )
487{
488 char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
489 char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
490 If_DsdObj_t * pObj;
491 int i, iFanin;
492 fprintf( pFile, "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" );
493 pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsdLit) );
494 if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
495 { fprintf( pFile, "0" ); return; }
496 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
497 {
498 int iPermLit = pPermLits ? (int)pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
499 fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
500 return;
501 }
502 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
503 Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), If_DsdObjFaninNum(pObj) );
504 fprintf( pFile, "%c", OpenType[If_DsdObjType(pObj)] );
505 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
506 If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp );
507 fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] );
508}
509void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits, int fNewLine )
510{
511 int nSupp = 0;
512 fprintf( pFile, "%6d : ", iObjId );
513 fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(&p->vObjs, iObjId) );
514 fprintf( pFile, "%8d ", If_DsdVecObjRef(&p->vObjs, iObjId) );
515 fprintf( pFile, "%d ", If_DsdVecObjMark(&p->vObjs, iObjId) );
516 If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
517 if ( fNewLine )
518 fprintf( pFile, "\n" );
519 assert( nSupp == If_DsdVecObjSuppSize(&p->vObjs, iObjId) );
520}
521#define DSD_ARRAY_LIMIT 16
522void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p )
523{
524 Vec_Int_t * vDecs;
525 int i, k, v, nSuppSize, nDecMax = 0;
526 int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0};
527 int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0};
528 int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0};
529 int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}};
530 word * pTruth;
531 for ( v = 3; v <= p->nVars; v++ )
532 {
533 assert( Vec_MemEntryNum(p->vTtMem[v]) == Vec_PtrSize(p->vTtDecs[v]) );
534 // find max number of decompositions
535 Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
536 {
537 pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
538 nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
539 pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) );
540 nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) );
541 }
542 // fill up
543 Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
544 {
545 pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
546 nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
547 pCountsAll[nSuppSize]++;
548 pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs);
549 pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++;
550 // pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++;
551 /*
552 if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] )
553 {
554 fprintf( pFile, "0x" );
555 Abc_TtPrintHex( pTruth, nSuppSize );
556 Dau_DecPrintSets( vDecs, nSuppSize );
557 }
558 */
559 }
560 }
561 // print header
562 fprintf( pFile, " N : " );
563 fprintf( pFile, " Total " );
564 for ( k = 0; k <= DSD_ARRAY_LIMIT; k++ )
565 fprintf( pFile, "%6d", k );
566 fprintf( pFile, " " );
567 fprintf( pFile, " More" );
568 fprintf( pFile, " Ave" );
569 fprintf( pFile, " Max" );
570 fprintf( pFile, "\n" );
571 // print rows
572 for ( i = 0; i <= p->nVars; i++ )
573 {
574 fprintf( pFile, "%2d : ", i );
575 fprintf( pFile, "%6d ", pCountsAll[i] );
576 for ( k = 0; k <= DSD_ARRAY_LIMIT; k++ )
577// fprintf( pFile, "%6d", pCounts[i][k] );
578 fprintf( pFile, "%6.1f", 100.0*pCounts[i][k]/Abc_MaxInt(1,pCountsAll[i]) );
579 fprintf( pFile, " " );
580// fprintf( pFile, "%6d", pCounts[i][k] );
581 fprintf( pFile, "%6.1f", 100.0*pCounts[i][k]/Abc_MaxInt(1,pCountsAll[i]) );
582 fprintf( pFile, " " );
583 fprintf( pFile, "%6.1f", 1.0*pCountsSSizes[i]/Abc_MaxInt(1,pCountsAll[i]) );
584 fprintf( pFile, " " );
585 fprintf( pFile, "%6d", pDecMax[i] );
586 fprintf( pFile, "\n" );
587 }
588}
589void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p )
590{
591 char Buffer[100];
592 If_DsdObj_t * pObj;
593 Vec_Int_t * vOccurs;
594 int nOccurs, nOccursMax, nOccursAll;
595 int i, k, nSizeMax, Counter = 0;
596 // determine the largest fanin and fanout
597 nOccursMax = nOccursAll = 0;
598 If_DsdVecForEachNode( &p->vObjs, pObj, i )
599 {
600 nOccurs = pObj->Count;
601 nOccursAll += nOccurs;
602 nOccursMax = Abc_MaxInt( nOccursMax, nOccurs );
603 }
604 // allocate storage for fanin/fanout numbers
605 nSizeMax = 10 * (Abc_Base10Log(nOccursMax) + 1);
606 vOccurs = Vec_IntStart( nSizeMax );
607 // count the number of fanins and fanouts
608 If_DsdVecForEachNode( &p->vObjs, pObj, i )
609 {
610 nOccurs = pObj->Count;
611 if ( nOccurs < 10 )
612 Vec_IntAddToEntry( vOccurs, nOccurs, 1 );
613 else if ( nOccurs < 100 )
614 Vec_IntAddToEntry( vOccurs, 10 + nOccurs/10, 1 );
615 else if ( nOccurs < 1000 )
616 Vec_IntAddToEntry( vOccurs, 20 + nOccurs/100, 1 );
617 else if ( nOccurs < 10000 )
618 Vec_IntAddToEntry( vOccurs, 30 + nOccurs/1000, 1 );
619 else if ( nOccurs < 100000 )
620 Vec_IntAddToEntry( vOccurs, 40 + nOccurs/10000, 1 );
621 else if ( nOccurs < 1000000 )
622 Vec_IntAddToEntry( vOccurs, 50 + nOccurs/100000, 1 );
623 else if ( nOccurs < 10000000 )
624 Vec_IntAddToEntry( vOccurs, 60 + nOccurs/1000000, 1 );
625 }
626 fprintf( pFile, "The distribution of object occurrences:\n" );
627 for ( k = 0; k < nSizeMax; k++ )
628 {
629 if ( Vec_IntEntry(vOccurs, k) == 0 )
630 continue;
631 if ( k < 10 )
632 fprintf( pFile, "%15d : ", k );
633 else
634 {
635 sprintf( Buffer, "%d - %d", (int)pow((double)10, k/10) * (k%10), (int)pow((double)10, k/10) * (k%10+1) - 1 );
636 fprintf( pFile, "%15s : ", Buffer );
637 }
638 fprintf( pFile, "%12d ", Vec_IntEntry(vOccurs, k) );
639 Counter += Vec_IntEntry(vOccurs, k);
640 fprintf( pFile, "(%6.2f %%)", 100.0*Counter/Vec_PtrSize(&p->vObjs) );
641 fprintf( pFile, "\n" );
642 }
643 Vec_IntFree( vOccurs );
644 fprintf( pFile, "Fanins: Max = %d. Ave = %.2f.\n", nOccursMax, 1.0*nOccursAll/Vec_PtrSize(&p->vObjs) );
645}
646
647void If_DsdManPrintDistrib( If_DsdMan_t * p )
648{
649 If_DsdObj_t * pObj; int i;
650 int CountObj[IF_MAX_FUNC_LUTSIZE+2] = {0};
651 int CountObjNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
652 int CountObjNpn[IF_MAX_FUNC_LUTSIZE+2] = {0};
653 int CountStr[IF_MAX_FUNC_LUTSIZE+2] = {0};
654 int CountStrNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
655 int CountMarked[IF_MAX_FUNC_LUTSIZE+2] = {0};
656 for ( i = 3; i <= p->nVars; i++ )
657 {
658 CountObjNpn[i] = Vec_MemEntryNum(p->vTtMem[i]);
659 CountObjNpn[p->nVars+1] += Vec_MemEntryNum(p->vTtMem[i]);
660 }
661 If_DsdVecForEachObj( &p->vObjs, pObj, i )
662 {
663 CountObj[If_DsdObjFaninNum(pObj)]++, CountObj[p->nVars+1]++;
664 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
665 CountObjNon[If_DsdObjFaninNum(pObj)]++, CountObjNon[p->nVars+1]++;
666 CountStr[If_DsdObjSuppSize(pObj)]++, CountStr[p->nVars+1]++;
667 if ( If_DsdManCheckNonDec_rec(p, i) )
668 CountStrNon[If_DsdObjSuppSize(pObj)]++, CountStrNon[p->nVars+1]++;
669 if ( If_DsdVecObjMark(&p->vObjs, i) )
670 CountMarked[If_DsdObjSuppSize(pObj)]++, CountMarked[p->nVars+1]++;
671 }
672 printf( "***** DSD MANAGER STATISTICS *****\n" );
673 printf( "Support " );
674 printf( "Obj " );
675 printf( "ObjNDSD " );
676 printf( "NPNNDSD " );
677 printf( "Str " );
678 printf( "StrNDSD " );
679 printf( "Marked " );
680 printf( "\n" );
681 for ( i = 0; i <= p->nVars + 1; i++ )
682 {
683 if ( i == p->nVars + 1 )
684 printf( "All : " );
685 else
686 printf( "%3d : ", i );
687 printf( "%9d ", CountObj[i] );
688 printf( "%9d ", CountObjNon[i] );
689 printf( "%6.2f %% ", 100.0 * CountObjNon[i] / Abc_MaxInt(1, CountObj[i]) );
690 printf( "%9d ", CountObjNpn[i] );
691 printf( "%6.2f %% ", 100.0 * CountObjNpn[i] / Abc_MaxInt(1, CountObj[i]) );
692 printf( " " );
693 printf( "%9d ", CountStr[i] );
694 printf( "%9d ", CountStrNon[i] );
695 printf( "%6.2f %% ", 100.0 * CountStrNon[i] / Abc_MaxInt(1, CountStr[i]) );
696 printf( "%9d ", CountMarked[i] );
697 printf( "%6.2f %%", 100.0 * CountMarked[i] / Abc_MaxInt(1, CountStr[i]) );
698 printf( "\n" );
699 }
700}
701void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose )
702{
703 If_DsdObj_t * pObj;
704 Vec_Int_t * vStructs, * vCounts;
705 int CountUsed = 0, CountNonDsd = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0;
706 int i, v, * pPerm, DsdMax = 0, MemSizeTTs = 0, MemSizeDecs = 0;
707 FILE * pFile;
708 pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
709 if ( pFileName && pFile == NULL )
710 {
711 printf( "cannot open output file\n" );
712 return;
713 }
714 if ( fVerbose )
715 {
716 fprintf( pFile, "***** NOTATIONS USED BELOW *****\n" );
717 fprintf( pFile, "Support -- the support size\n" );
718 fprintf( pFile, "Obj -- the number of nodes in the DSD manager for each support size\n" );
719 fprintf( pFile, " (the constant node and the primary input node have no support)\n" );
720 fprintf( pFile, "ObjNDSD -- the number of prime nodes (that is, nodes whose function has no DSD)\n" );
721 fprintf( pFile, " (percentage is relative to the number of all nodes of that size)\n" );
722 fprintf( pFile, "NPNNDSD -- the number of different NPN classes of prime nodes\n" );
723 fprintf( pFile, " (Each NPN class may appear more than once. For example: F1 = 17(ab(cd))\n" );
724 fprintf( pFile, " and F2 = 17(ab[cd]) both have prime majority node (hex TT is 17),\n" );
725 fprintf( pFile, " but in one case the majority node is fed by AND, and in another by XOR.\n" );
726 fprintf( pFile, " These two majority nodes are different nodes in the DSD manager\n" );
727 fprintf( pFile, "Str -- the number of structures for each support size\n" );
728 fprintf( pFile, " (each structure is composed of one or more nodes)\n" );
729 fprintf( pFile, "StrNDSD -- the number of DSD structures containing at least one prime node\n" );
730 fprintf( pFile, "Marked -- the number of DSD structures matchable with the LUT structure (say, \"44\")\n" );
731 }
732 If_DsdVecForEachObj( &p->vObjs, pObj, i )
733 {
734 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
735 DsdMax = Abc_MaxInt( DsdMax, pObj->nFans );
736 CountPrime += If_DsdObjType(pObj) == IF_DSD_PRIME;
737 CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
738 CountUsed += ( If_DsdVecObjRef(&p->vObjs, pObj->Id) > 0 );
739 CountMarked += If_DsdVecObjMark( &p->vObjs, i );
740 }
741 for ( v = 3; v <= p->nVars; v++ )
742 {
743 CountNonDsd += Vec_MemEntryNum(p->vTtMem[v]);
744 MemSizeTTs += Vec_MemEntrySize(p->vTtMem[v]) * Vec_MemEntryNum(p->vTtMem[v]);
745 MemSizeDecs += (int)Vec_VecMemoryInt((Vec_Vec_t *)(p->vTtDecs[v]));
746 }
747 If_DsdManPrintDistrib( p );
748 printf( "Number of inputs = %d. LUT size = %d. Marks = %s. NewAsUseless = %s. Bookmark = %d.\n",
749 p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev );
750 if ( p->pCellStr )
751 printf( "Symbolic cell description: %s\n", p->pCellStr );
752 if ( p->pTtGia )
753 fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) );
754 fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses );
755 fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits );
756 fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
757 fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(MemSizeTTs+sizeof(int)*Vec_IntCap(&p->vTruths))/(1<<20) );
758 fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(&p->vNexts))/(1<<20) );
759 fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", 1.0*MemSizeDecs/(1<<20) );
760 fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(&p->vObjs)/(1<<20) );
761 if ( p->pTtGia )
762 fprintf( pFile, "Memory used for AIG = %8.2f MB.\n", 8.0*Gia_ManAndNum(p->pTtGia)/(1<<20) );
763 if ( p->timeDsd )
764 {
765 Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
766 Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck );
767 Abc_PrintTime( 1, "Time check ", p->timeCheck );
768 Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
769 Abc_PrintTime( 1, "Time verify", p->timeVerify );
770 }
771 if ( fOccurs )
772 If_DsdManPrintOccurs( stdout, p );
773// If_DsdManHashProfile( p );
774 if ( fTtDump )
775 If_DsdManDumpDsd( p, Support );
776 if ( fTtDump )
777 If_DsdManDumpAll( p, Support );
778// If_DsdManPrintDecs( stdout, p );
779 if ( !fVerbose )
780 return;
781 vStructs = Vec_IntAlloc( 1000 );
782 vCounts = Vec_IntAlloc( 1000 );
783 If_DsdVecForEachObj( &p->vObjs, pObj, i )
784 {
785 if ( Number && i % Number )
786 continue;
787 if ( Support && Support != If_DsdObjSuppSize(pObj) )
788 continue;
789 Vec_IntPush( vStructs, i );
790 Vec_IntPush( vCounts, -(int)pObj->Count );
791// If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
792 }
793// fprintf( pFile, "\n" );
794 pPerm = Abc_MergeSortCost( Vec_IntArray(vCounts), Vec_IntSize(vCounts) );
795 for ( i = 0; i < Abc_MinInt(Vec_IntSize(vCounts), 20); i++ )
796 {
797 printf( "%2d : ", i+1 );
798 pObj = If_DsdVecObj( &p->vObjs, Vec_IntEntry(vStructs, pPerm[i]) );
799 If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
800 }
801 ABC_FREE( pPerm );
802 Vec_IntFree( vStructs );
803 Vec_IntFree( vCounts );
804 if ( pFileName )
805 fclose( pFile );
806}
807
819int If_DsdManCheckNonTriv( If_DsdMan_t * p, int Id, int nVars, int iVarMax )
820{
821 If_DsdObj_t * pObj; int i, iFanin;
822 pObj = If_DsdVecObj( &p->vObjs, Id );
823 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
824 return 1;
825 if ( If_DsdObjFaninNum(pObj) == nVars )
826 return 0;
827 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
828 if ( Abc_Lit2Var(iFanin) == 1 && i == iVarMax )
829 return 0;
830 return 1;
831}
832
844int If_DsdObjCompare( If_DsdMan_t * pMan, Vec_Ptr_t * p, int iLit0, int iLit1 )
845{
846 If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
847 If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
848 int i, Res;
849 if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
850 return -1;
851 if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
852 return 1;
853 if ( If_DsdObjType(p0) < IF_DSD_AND )
854 return 0;
855 if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
856 return -1;
857 if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
858 return 1;
859 if ( If_DsdObjType(p0) == IF_DSD_PRIME )
860 {
861 if ( If_DsdObjTruthId(pMan, p0) < If_DsdObjTruthId(pMan, p1) )
862 return -1;
863 if ( If_DsdObjTruthId(pMan, p0) > If_DsdObjTruthId(pMan, p1) )
864 return 1;
865 }
866 for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
867 {
868 Res = If_DsdObjCompare( pMan, p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
869 if ( Res != 0 )
870 return Res;
871 }
872 if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
873 return -1;
874 if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
875 return 1;
876 assert( iLit0 == iLit1 );
877 return 0;
878}
879void If_DsdObjSort( If_DsdMan_t * pMan, Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
880{
881 int i, j, best_i;
882 for ( i = 0; i < nLits-1; i++ )
883 {
884 best_i = i;
885 for ( j = i+1; j < nLits; j++ )
886 if ( If_DsdObjCompare(pMan, p, pLits[best_i], pLits[j]) == 1 )
887 best_i = j;
888 if ( i == best_i )
889 continue;
890 ABC_SWAP( int, pLits[i], pLits[best_i] );
891 if ( pPerm )
892 ABC_SWAP( int, pPerm[i], pPerm[best_i] );
893 }
894}
895
907static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
908{
909 static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909,
910 3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281,
911 5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
912 int i;
913 unsigned uHash = Type * 7873 + nLits * 8147;
914 for ( i = 0; i < nLits; i++ )
915 uHash += pLits[i] * s_Primes[i & 0xF];
916 if ( Type == IF_DSD_PRIME )
917 uHash += truthId * s_Primes[i & 0xF];
918 return uHash % p->nBins;
919}
920unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
921{
922 If_DsdObj_t * pObj;
923 unsigned * pSpot = p->pBins + If_DsdObjHashKey(p, Type, pLits, nLits, truthId);
924 for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(&p->vNexts, pObj->Id) )
925 {
926 pObj = If_DsdVecObj( &p->vObjs, *pSpot );
927 if ( If_DsdObjType(pObj) == Type &&
928 If_DsdObjFaninNum(pObj) == nLits &&
929 !memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) &&
930 truthId == If_DsdObjTruthId(p, pObj) )
931 {
932 p->nUniqueHits++;
933 return pSpot;
934 }
935 }
936 p->nUniqueMisses++;
937 return pSpot;
938}
939static void If_DsdObjHashResize( If_DsdMan_t * p )
940{
941 If_DsdObj_t * pObj;
942 unsigned * pSpot;
943 int i, Prev = p->nUniqueMisses;
944 p->nBins = Abc_PrimeCudd( 2 * p->nBins );
945 p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
946 memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
947 Vec_IntFill( &p->vNexts, Vec_PtrSize(&p->vObjs), 0 );
948 If_DsdVecForEachNode( &p->vObjs, pObj, i )
949 {
950 pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
951 assert( *pSpot == 0 );
952 *pSpot = pObj->Id;
953 }
954 assert( p->nUniqueMisses - Prev == Vec_PtrSize(&p->vObjs) - 2 );
955 p->nUniqueMisses = Prev;
956}
957
958int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
959{
960 If_DsdObj_t * pObj, * pFanin;
961 int i, iPrev = -1;
962 // check structural canonicity
963 assert( Type != DAU_DSD_MUX || nLits == 3 );
964// assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
965 assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
966 // check that leaves are in good order
967 if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
968 {
969 for ( i = 0; i < nLits; i++ )
970 {
971 pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[i]) );
972 assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
973 assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
974 assert( iPrev == -1 || If_DsdObjCompare(p, &p->vObjs, iPrev, pLits[i]) <= 0 );
975 iPrev = pLits[i];
976 }
977 }
978 // create new node
979 pObj = If_DsdObjAlloc( p, Type, nLits );
980 if ( Type == DAU_DSD_PRIME )
981 If_DsdObjSetTruth( p, pObj, truthId );
982 assert( pObj->nSupp == 0 );
983 for ( i = 0; i < nLits; i++ )
984 {
985 pObj->pFans[i] = pLits[i];
986 pObj->nSupp += If_DsdVecLitSuppSize(&p->vObjs, pLits[i]);
987 }
988 // check decomposability
989 if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0, 0, 0) )
990 If_DsdVecObjSetMark( &p->vObjs, pObj->Id );
991 return pObj->Id;
992}
993int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
994{
995 int PrevSize = (Type == IF_DSD_PRIME) ? Vec_MemEntryNum( p->vTtMem[nLits] ) : -1;
996 int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
997 unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
998//abctime clk;
999 if ( *pSpot )
1000 return (int)*pSpot;
1001//clk = Abc_Clock();
1002 if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
1003 {
1004 Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
1005 assert( truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 );
1006 Vec_PtrPush( p->vTtDecs[nLits], vSets );
1007// Dau_DecPrintSets( vSets, nLits );
1008 }
1009 if ( p->vIsops[nLits] && truthId >= 0 && PrevSize != Vec_MemEntryNum(p->vTtMem[nLits]) )
1010 {
1011 Vec_Int_t * vLevel = Vec_WecPushLevel( p->vIsops[nLits] );
1012 int fCompl = Kit_TruthIsop( (unsigned *)pTruth, nLits, p->vCover, 1 );
1013 if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
1014 {
1015 Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
1016 Vec_IntAppend( vLevel, p->vCover );
1017 if ( fCompl )
1018 vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
1019 }
1020 assert( Vec_WecSize(p->vIsops[nLits]) == Vec_MemEntryNum(p->vTtMem[nLits]) );
1021 }
1022 if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 )
1023 {
1024// int nObjOld = Gia_ManAndNum(p->pTtGia);
1025 int Lit = Kit_TruthToGia( p->pTtGia, (unsigned *)pTruth, nLits, p->vCover, NULL, 1 );
1026// printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
1027 Gia_ManAppendCo( p->pTtGia, Lit );
1028 }
1029//p->timeCheck += Abc_Clock() - clk;
1030 *pSpot = Vec_PtrSize( &p->vObjs );
1031 objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
1032 if ( Vec_PtrSize(&p->vObjs) > p->nBins )
1033 If_DsdObjHashResize( p );
1034 return objId;
1035}
1036
1037
1049void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
1050{
1051 If_DsdObj_t * pObj;
1052 Vec_Int_t * vSets;
1053 word * pTruth;
1054 int i, v, Num;
1055 FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
1056 if ( pFile == NULL )
1057 {
1058 printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
1059 return;
1060 }
1061 fwrite( DSD_VERSION, 4, 1, pFile );
1062 Num = p->nVars;
1063 fwrite( &Num, 4, 1, pFile );
1064 Num = p->LutSize;
1065 fwrite( &Num, 4, 1, pFile );
1066 Num = Vec_PtrSize(&p->vObjs);
1067 fwrite( &Num, 4, 1, pFile );
1068 Vec_PtrForEachEntryStart( If_DsdObj_t *, &p->vObjs, pObj, i, 2 )
1069 {
1070 Num = If_DsdObjWordNum( pObj->nFans );
1071 fwrite( &Num, 4, 1, pFile );
1072 fwrite( pObj, sizeof(word)*Num, 1, pFile );
1073 if ( pObj->Type == IF_DSD_PRIME )
1074 fwrite( Vec_IntEntryP(&p->vTruths, i), 4, 1, pFile );
1075 }
1076 for ( v = 3; v <= p->nVars; v++ )
1077 {
1078 int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
1079 Num = Vec_MemEntryNum(p->vTtMem[v]);
1080 fwrite( &Num, 4, 1, pFile );
1081 Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
1082 fwrite( pTruth, nBytes, 1, pFile );
1083 Num = Vec_PtrSize(p->vTtDecs[v]);
1084 fwrite( &Num, 4, 1, pFile );
1085 Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vSets, i )
1086 {
1087 Num = Vec_IntSize(vSets);
1088 fwrite( &Num, 4, 1, pFile );
1089 fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
1090 }
1091 }
1092 Num = p->nConfigWords;
1093 fwrite( &Num, 4, 1, pFile );
1094 Num = p->nTtBits;
1095 fwrite( &Num, 4, 1, pFile );
1096 Num = p->vConfigs ? Vec_WrdSize(p->vConfigs) : 0;
1097 fwrite( &Num, 4, 1, pFile );
1098 if ( Num )
1099 fwrite( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
1100 Num = p->pCellStr ? strlen(p->pCellStr) : 0;
1101 fwrite( &Num, 4, 1, pFile );
1102 if ( Num )
1103 fwrite( p->pCellStr, sizeof(char)*Num, 1, pFile );
1104 fclose( pFile );
1105}
1106If_DsdMan_t * If_DsdManLoad( char * pFileName )
1107{
1108 If_DsdMan_t * p;
1109 If_DsdObj_t * pObj;
1110 Vec_Int_t * vSets;
1111 char pBuffer[10];
1112 unsigned * pSpot;
1113 word * pTruth;
1114 int i, v, Num, Num2, RetValue;
1115 FILE * pFile = fopen( pFileName, "rb" );
1116 if ( pFile == NULL )
1117 {
1118 printf( "Reading DSD manager file \"%s\" has failed.\n", pFileName );
1119 return NULL;
1120 }
1121 RetValue = fread( pBuffer, 4, 1, pFile );
1122 if ( strncmp(pBuffer, DSD_VERSION, strlen(DSD_VERSION)) )
1123 {
1124 printf( "Unrecognized format of file \"%s\".\n", pFileName );
1125 return NULL;
1126 }
1127 RetValue = fread( &Num, 4, 1, pFile );
1128 p = If_DsdManAlloc( Num, 0 );
1129 ABC_FREE( p->pStore );
1130 p->pStore = Abc_UtilStrsav( pFileName );
1131 RetValue = fread( &Num, 4, 1, pFile );
1132 p->LutSize = Num;
1133 p->pSat = If_ManSatBuildXY( p->LutSize );
1134 RetValue = fread( &Num, 4, 1, pFile );
1135 assert( Num >= 2 );
1136 Vec_PtrFillExtra( &p->vObjs, Num, NULL );
1137 Vec_IntFill( &p->vNexts, Num, 0 );
1138 Vec_IntFill( &p->vTruths, Num, -1 );
1139 p->nBins = Abc_PrimeCudd( 2*Num );
1140 p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
1141 memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
1142 for ( i = 2; i < Vec_PtrSize(&p->vObjs); i++ )
1143 {
1144 RetValue = fread( &Num, 4, 1, pFile );
1145 pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
1146 RetValue = fread( pObj, sizeof(word)*Num, 1, pFile );
1147 Vec_PtrWriteEntry( &p->vObjs, i, pObj );
1148 if ( pObj->Type == IF_DSD_PRIME )
1149 {
1150 RetValue = fread( &Num, 4, 1, pFile );
1151 Vec_IntWriteEntry( &p->vTruths, i, Num );
1152 }
1153 pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
1154 assert( *pSpot == 0 );
1155 *pSpot = pObj->Id;
1156 }
1157 assert( p->nUniqueMisses == Vec_PtrSize(&p->vObjs) - 2 );
1158 p->nUniqueMisses = 0;
1159 pTruth = ABC_ALLOC( word, p->nWords );
1160 for ( v = 3; v <= p->nVars; v++ )
1161 {
1162 int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
1163 RetValue = fread( &Num, 4, 1, pFile );
1164 for ( i = 0; i < Num; i++ )
1165 {
1166 RetValue = fread( pTruth, nBytes, 1, pFile );
1167 Vec_MemHashInsert( p->vTtMem[v], pTruth );
1168 }
1169 assert( Num == Vec_MemEntryNum(p->vTtMem[v]) );
1170 RetValue = fread( &Num2, 4, 1, pFile );
1171 for ( i = 0; i < Num2; i++ )
1172 {
1173 RetValue = fread( &Num, 4, 1, pFile );
1174 vSets = Vec_IntAlloc( Num );
1175 RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
1176 vSets->nSize = Num;
1177 Vec_PtrPush( p->vTtDecs[v], vSets );
1178 }
1179 assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) );
1180 }
1181 ABC_FREE( pTruth );
1182 RetValue = fread( &Num, 4, 1, pFile );
1183 p->nConfigWords = Num;
1184 RetValue = fread( &Num, 4, 1, pFile );
1185 p->nTtBits = Num;
1186 RetValue = fread( &Num, 4, 1, pFile );
1187 if ( RetValue && Num )
1188 {
1189 p->vConfigs = Vec_WrdStart( Num );
1190 RetValue = fread( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
1191 }
1192 RetValue = fread( &Num, 4, 1, pFile );
1193 if ( RetValue && Num )
1194 {
1195 p->pCellStr = ABC_CALLOC( char, Num + 1 );
1196 RetValue = fread( p->pCellStr, sizeof(char)*Num, 1, pFile );
1197 }
1198 fclose( pFile );
1199 return p;
1200}
1201void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
1202{
1203 If_DsdObj_t * pObj;
1204 Vec_Int_t * vMap;
1205 int pFanins[DAU_MAX_VAR];
1206 int i, k, iFanin, Id;
1207 if ( p->nVars < pNew->nVars )
1208 {
1209 printf( "The number of variables should be the same or smaller.\n" );
1210 return;
1211 }
1212 if ( p->LutSize != pNew->LutSize )
1213 {
1214 printf( "LUT size should be the same.\n" );
1215 return;
1216 }
1217 assert( p->nTtBits == pNew->nTtBits );
1218 assert( p->nConfigWords == pNew->nConfigWords );
1219 if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) )
1220 printf( "Warning! Old manager has %smarks while new manager has %smarks.\n",
1221 If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " );
1222 vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) );
1223 Vec_IntPush( vMap, 0 );
1224 Vec_IntPush( vMap, 1 );
1225 if ( p->vConfigs && pNew->vConfigs )
1226 Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * (Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs)), 0 );
1227 If_DsdVecForEachNode( &pNew->vObjs, pObj, i )
1228 {
1229 If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k )
1230 pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
1231 Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL );
1232 if ( pObj->fMark )
1233 If_DsdVecObjSetMark( &p->vObjs, Id );
1234 if ( p->vConfigs && pNew->vConfigs && p->nConfigWords * i < Vec_WrdSize(pNew->vConfigs) )
1235 {
1236 //Vec_WrdFillExtra( p->vConfigs, Id, Vec_WrdEntry(pNew->vConfigs, i) );
1237 word * pConfigNew = Vec_WrdEntryP(pNew->vConfigs, p->nConfigWords * i);
1238 word * pConfigOld = Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Id);
1239 memcpy( pConfigOld, pConfigNew, sizeof(word) * p->nConfigWords );
1240 }
1241 Vec_IntPush( vMap, Id );
1242 }
1243 assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
1244 Vec_IntFree( vMap );
1245 if ( p->vConfigs && pNew->vConfigs )
1246 Vec_WrdShrink( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs) );
1247}
1248void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose )
1249{
1250 If_DsdObj_t * pObj;
1251 int i;
1252 If_DsdVecForEachObj( &p->vObjs, pObj, i )
1253 pObj->Count = 0;
1254}
1255void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
1256{
1257 If_DsdObj_t * pObj;
1258 int i;
1259 ABC_FREE( p->pCellStr );
1260 Vec_WrdFreeP( &p->vConfigs );
1261 If_DsdVecForEachObj( &p->vObjs, pObj, i )
1262 pObj->fMark = 0;
1263}
1264void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose )
1265{
1266 If_DsdObj_t * pObj;
1267 int i;
1268 ABC_FREE( p->pCellStr );
1269 //Vec_WrdFreeP( &p->vConfigs );
1270 If_DsdVecForEachObj( &p->vObjs, pObj, i )
1271 pObj->fMark = !pObj->fMark;
1272}
1273void If_DsdManFilter_rec( If_DsdMan_t * pNew, If_DsdMan_t * p, int i, Vec_Int_t * vMap )
1274{
1275 If_DsdObj_t * pObj;
1276 int pFanins[DAU_MAX_VAR];
1277 int k, iFanin, Id;
1278 if ( Vec_IntEntry(vMap, i) >= 0 )
1279 return;
1280 // call recursively
1281 pObj = If_DsdVecObj( &p->vObjs, i );
1282 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
1283 If_DsdManFilter_rec( pNew, p, Abc_Lit2Var(iFanin), vMap );
1284 // duplicate this one
1285 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
1286 pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
1287 Id = If_DsdObjFindOrAdd( pNew, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(p, pObj) : NULL );
1288 if ( pObj->fMark )
1289 If_DsdVecObjSetMark( &pNew->vObjs, Id );
1290 If_DsdVecObj( &pNew->vObjs, Id )->Count = pObj->Count;
1291 // save the result
1292 Vec_IntWriteEntry( vMap, i, Id );
1293}
1294If_DsdMan_t * If_DsdManFilter( If_DsdMan_t * p, int Limit )
1295{
1296 If_DsdMan_t * pNew = If_DsdManAlloc( p->nVars, p->LutSize );
1297 If_DsdObj_t * pObj;
1298 Vec_Int_t * vMap;
1299 int i;
1300 vMap = Vec_IntStartFull( Vec_PtrSize(&p->vObjs) );
1301 Vec_IntWriteEntry( vMap, 0, 0 );
1302 Vec_IntWriteEntry( vMap, 1, 1 );
1303 If_DsdVecForEachNode( &p->vObjs, pObj, i )
1304 if ( (int)pObj->Count >= Limit )
1305 If_DsdManFilter_rec( pNew, p, i, vMap );
1306 Vec_IntFree( vMap );
1307 return pNew;
1308}
1309
1321void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts, int * pnSupp )
1322{
1323 int i, iFanin, iFirst;
1324 If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
1325 if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
1326 return;
1327 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1328 {
1329 (*pnSupp)++;
1330 return;
1331 }
1332 iFirst = *pnSupp;
1333 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1334 If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes, vFirsts, pnSupp );
1335 Vec_IntPush( vNodes, Id );
1336 Vec_IntPush( vFirsts, iFirst );
1337}
1338void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts )
1339{
1340 int nSupp = 0;
1341 Vec_IntClear( vNodes );
1342 Vec_IntClear( vFirsts );
1343 If_DsdManCollect_rec( p, Id, vNodes, vFirsts, &nSupp );
1344}
1345
1357void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned char * pPermLits, int * pnSupp )
1358{
1359 int i, iFanin, fCompl = Abc_LitIsCompl(iDsd);
1360 If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1361 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1362 {
1363 int iPermLit = pPermLits ? (int)pPermLits[*pnSupp] : Abc_Var2Lit(*pnSupp, 0);
1364 (*pnSupp)++;
1365 assert( (*pnSupp) <= p->nVars );
1366 Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
1367 return;
1368 }
1369 if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR )
1370 {
1371 word pTtTemp[DAU_MAX_WORD];
1372 if ( If_DsdObjType(pObj) == IF_DSD_AND )
1373 Abc_TtConst1( pRes, p->nWords );
1374 else
1375 Abc_TtConst0( pRes, p->nWords );
1376 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1377 {
1378 If_DsdManComputeTruth_rec( p, iFanin, pTtTemp, pPermLits, pnSupp );
1379 if ( If_DsdObjType(pObj) == IF_DSD_AND )
1380 Abc_TtAnd( pRes, pRes, pTtTemp, p->nWords, 0 );
1381 else
1382 Abc_TtXor( pRes, pRes, pTtTemp, p->nWords, 0 );
1383 }
1384 if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1385 return;
1386 }
1387 if ( If_DsdObjType(pObj) == IF_DSD_MUX ) // mux
1388 {
1389 word pTtTemp[3][DAU_MAX_WORD];
1390 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1391 If_DsdManComputeTruth_rec( p, iFanin, pTtTemp[i], pPermLits, pnSupp );
1392 assert( i == 3 );
1393 Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], p->nWords );
1394 if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1395 return;
1396 }
1397 if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) // function
1398 {
1399 word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
1400 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1401 If_DsdManComputeTruth_rec( p, iFanin, pFanins[i], pPermLits, pnSupp );
1402 Dau_DsdTruthCompose_rec( If_DsdObjTruth(p, pObj), pFanins, pRes, pObj->nFans, p->nWords );
1403 if ( fCompl ) Abc_TtNot( pRes, p->nWords );
1404 return;
1405 }
1406 assert( 0 );
1407
1408}
1409void If_DsdManComputeTruthPtr( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits, word * pRes )
1410{
1411 int nSupp = 0;
1412 If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1413 if ( iDsd == 0 )
1414 Abc_TtConst0( pRes, p->nWords );
1415 else if ( iDsd == 1 )
1416 Abc_TtConst1( pRes, p->nWords );
1417 else if ( pObj->Type == IF_DSD_VAR )
1418 {
1419 int iPermLit = pPermLits ? (int)pPermLits[nSupp] : Abc_Var2Lit(nSupp, 0);
1420 nSupp++;
1421 Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
1422 }
1423 else
1424 If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp );
1425 assert( nSupp == If_DsdVecLitSuppSize(&p->vObjs, iDsd) );
1426}
1427word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits )
1428{
1429 word * pRes = p->pTtElems[DAU_MAX_VAR];
1430 If_DsdManComputeTruthPtr( p, iDsd, pPermLits, pRes );
1431 return pRes;
1432}
1433
1445int If_DsdManCheckInv_rec( If_DsdMan_t * p, int iLit )
1446{
1447 If_DsdObj_t * pObj;
1448 int i, iFanin;
1449 pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLit) );
1450 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1451 return 1;
1452 if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_PRIME )
1453 return 0;
1454 if ( If_DsdObjType(pObj) == IF_DSD_XOR )
1455 {
1456 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1457 if ( If_DsdManCheckInv_rec(p, iFanin) )
1458 return 1;
1459 return 0;
1460 }
1461 if ( If_DsdObjType(pObj) == IF_DSD_MUX )
1462 return If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]);
1463 assert( 0 );
1464 return 0;
1465}
1466int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
1467{
1468 If_DsdObj_t * pObj;
1469 int i, iFanin;
1470 pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLit) );
1471 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1472 pPerm[0] = (unsigned char)Abc_LitNot((int)pPerm[0]);
1473 else if ( If_DsdObjType(pObj) == IF_DSD_XOR )
1474 {
1475 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1476 {
1477 if ( If_DsdManCheckInv_rec(p, iFanin) )
1478 {
1479 If_DsdManPushInv_rec( p, iFanin, pPerm );
1480 break;
1481 }
1482 pPerm += If_DsdVecLitSuppSize(&p->vObjs, iFanin);
1483 }
1484 }
1485 else if ( If_DsdObjType(pObj) == IF_DSD_MUX )
1486 {
1487 assert( If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]) );
1488 pPerm += If_DsdVecLitSuppSize(&p->vObjs, pObj->pFans[0]);
1489 If_DsdManPushInv_rec(p, pObj->pFans[1], pPerm);
1490 pPerm += If_DsdVecLitSuppSize(&p->vObjs, pObj->pFans[1]);
1491 If_DsdManPushInv_rec(p, pObj->pFans[2], pPerm);
1492 }
1493 else assert( 0 );
1494 return 1;
1495}
1496int If_DsdManPushInv( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
1497{
1498 if ( Abc_LitIsCompl(iLit) && If_DsdManCheckInv_rec(p, iLit) )
1499 return If_DsdManPushInv_rec( p, iLit, pPerm );
1500 return 0;
1501}
1502
1514int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
1515{
1516 int i, nSSize = 0;
1517 for ( i = 0; i < nLits; i++ )
1518 {
1519 pFirsts[i] = nSSize;
1520 nSSize += If_DsdVecLitSuppSize(&p->vObjs, pLits[i]);
1521 }
1522 return nSSize;
1523}
1524int If_DsdManComputeFirst( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pFirsts )
1525{
1526 return If_DsdManComputeFirstArray( p, (int *)pObj->pFans, pObj->nFans, pFirsts );
1527}
1528int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
1529{
1530 If_DsdObj_t * pObj, * pFanin;
1531 unsigned char pPermNew[DAU_MAX_VAR], * pPermStart = pPerm;
1532 int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
1533 int i, k, j, Id, iFanin, fCompl = 0, nSSize = 0;
1534 if ( Type == IF_DSD_AND || Type == IF_DSD_XOR )
1535 {
1536 for ( k = 0; k < nLits; k++ )
1537 {
1538 if ( Type == IF_DSD_XOR && Abc_LitIsCompl(pLits[k]) )
1539 {
1540 pLits[k] = Abc_LitNot(pLits[k]);
1541 fCompl ^= 1;
1542 }
1543 pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1544 if ( Type == If_DsdObjType(pObj) && (Type == IF_DSD_XOR || !Abc_LitIsCompl(pLits[k])) )
1545 {
1546 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
1547 {
1548 assert( Type == IF_DSD_AND || !Abc_LitIsCompl(iFanin) );
1549 pChildren[nChildren] = iFanin;
1550 pBegEnd[nChildren++] = (nSSize << 16) | (nSSize + If_DsdVecLitSuppSize(&p->vObjs, iFanin));
1551 nSSize += If_DsdVecLitSuppSize(&p->vObjs, iFanin);
1552 }
1553 }
1554 else
1555 {
1556 pChildren[nChildren] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1557 pBegEnd[nChildren++] = (nSSize << 16) | (nSSize + If_DsdObjSuppSize(pObj));
1558 nSSize += If_DsdObjSuppSize(pObj);
1559 }
1560 pPermStart += If_DsdObjSuppSize(pObj);
1561 }
1562 If_DsdObjSort( p, &p->vObjs, pChildren, nChildren, pBegEnd );
1563 // create permutation
1564 for ( j = i = 0; i < nChildren; i++ )
1565 for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
1566 pPermNew[j++] = pPerm[k];
1567 assert( j == nSSize );
1568 for ( j = 0; j < nSSize; j++ )
1569 pPerm[j] = pPermNew[j];
1570 }
1571 else if ( Type == IF_DSD_MUX )
1572 {
1573 int RetValue;
1574 assert( nLits == 3 );
1575 for ( k = 0; k < nLits; k++ )
1576 {
1577 pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1578 pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1579 pPermStart += pFanin->nSupp;
1580 }
1581 RetValue = If_DsdObjCompare( p, &p->vObjs, pLits[1], pLits[2] );
1582 if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) )
1583 {
1584 int nSupp0 = If_DsdVecLitSuppSize( &p->vObjs, pLits[0] );
1585 int nSupp1 = If_DsdVecLitSuppSize( &p->vObjs, pLits[1] );
1586 int nSupp2 = If_DsdVecLitSuppSize( &p->vObjs, pLits[2] );
1587 pLits[0] = Abc_LitNot(pLits[0]);
1588 ABC_SWAP( int, pLits[1], pLits[2] );
1589 for ( j = k = 0; k < nSupp0; k++ )
1590 pPermNew[j++] = pPerm[k];
1591 for ( k = 0; k < nSupp2; k++ )
1592 pPermNew[j++] = pPerm[nSupp0 + nSupp1 + k];
1593 for ( k = 0; k < nSupp1; k++ )
1594 pPermNew[j++] = pPerm[nSupp0 + k];
1595 for ( j = 0; j < nSupp0 + nSupp1 + nSupp2; j++ )
1596 pPerm[j] = pPermNew[j];
1597 }
1598 if ( Abc_LitIsCompl(pLits[1]) )
1599 {
1600 pLits[1] = Abc_LitNot(pLits[1]);
1601 pLits[2] = Abc_LitNot(pLits[2]);
1602 fCompl ^= 1;
1603 }
1604 pPermStart = pPerm;
1605 for ( k = 0; k < nLits; k++ )
1606 {
1607 pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(pLits[k]) );
1608 pChildren[nChildren++] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
1609 pPermStart += pFanin->nSupp;
1610 }
1611 }
1612 else if ( Type == IF_DSD_PRIME )
1613 {
1614 char pCanonPerm[DAU_MAX_VAR];
1615 int i, uCanonPhase, pFirsts[DAU_MAX_VAR];
1616 uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm );
1617 fCompl = ((uCanonPhase >> nLits) & 1);
1618 nSSize = If_DsdManComputeFirstArray( p, pLits, nLits, pFirsts );
1619 for ( j = i = 0; i < nLits; i++ )
1620 {
1621 int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) );
1622 pFanin = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iLitNew) );
1623 pPermStart = pPerm + pFirsts[(int)pCanonPerm[i]];
1624 pChildren[nChildren++] = Abc_LitNotCond( iLitNew, If_DsdManPushInv(p, iLitNew, pPermStart) );
1625 for ( k = 0; k < (int)pFanin->nSupp; k++ )
1626 pPermNew[j++] = pPermStart[k];
1627 }
1628 assert( j == nSSize );
1629 for ( j = 0; j < nSSize; j++ )
1630 pPerm[j] = pPermNew[j];
1631 Abc_TtStretch6( pTruth, nLits, p->nVars );
1632 }
1633 else assert( 0 );
1634 // create new graph
1635 Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, pTruth );
1636 return Abc_Var2Lit( Id, fCompl );
1637}
1638
1650static inline void If_DsdMergeMatches( char * pDsd, int * pMatches )
1651{
1652 int pNested[DAU_MAX_VAR];
1653 int i, nNested = 0;
1654 for ( i = 0; pDsd[i]; i++ )
1655 {
1656 pMatches[i] = 0;
1657 if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
1658 pNested[nNested++] = i;
1659 else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
1660 pMatches[pNested[--nNested]] = i;
1661 assert( nNested < DAU_MAX_VAR );
1662 }
1663 assert( nNested == 0 );
1664}
1665int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm, int * pnSupp )
1666{
1667 unsigned char * pPermStart = pPerm + *pnSupp;
1668 int iRes = -1, fCompl = 0;
1669 if ( **p == '!' )
1670 {
1671 fCompl = 1;
1672 (*p)++;
1673 }
1674 if ( **p >= 'a' && **p <= 'z' ) // var
1675 {
1676 pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
1677 return 2;
1678 }
1679 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
1680 {
1681 int Type = 0, nLits = 0, pLits[DAU_MAX_VAR];
1682 char * q = pStr + pMatches[ *p - pStr ];
1683 if ( **p == '(' )
1684 Type = DAU_DSD_AND;
1685 else if ( **p == '[' )
1686 Type = DAU_DSD_XOR;
1687 else if ( **p == '<' )
1688 Type = DAU_DSD_MUX;
1689 else if ( **p == '{' )
1690 Type = DAU_DSD_PRIME;
1691 else assert( 0 );
1692 assert( *q == **p + 1 + (**p != '(') );
1693 for ( (*p)++; *p < q; (*p)++ )
1694 pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
1695 assert( *p == q );
1696 iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth );
1697 return Abc_LitNotCond( iRes, fCompl );
1698 }
1699 if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
1700 {
1701 word pFunc[DAU_MAX_WORD];
1702 int nLits = 0, pLits[DAU_MAX_VAR];
1703 char * q;
1704 int i, nVarsF = Abc_TtReadHex( pFunc, *p );
1705 *p += Abc_TtHexDigitNum( nVarsF );
1706 q = pStr + pMatches[ *p - pStr ];
1707 assert( **p == '{' && *q == '}' );
1708 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
1709 pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
1710 assert( i == nVarsF );
1711 assert( *p == q );
1712 iRes = If_DsdManOperation( pMan, DAU_DSD_PRIME, pLits, nLits, pPermStart, pFunc );
1713 return Abc_LitNotCond( iRes, fCompl );
1714 }
1715 assert( 0 );
1716 return -1;
1717}
1718int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm, int * pnSupp )
1719{
1720 int iRes = -1, fCompl = 0;
1721 if ( *pDsd == '!' )
1722 pDsd++, fCompl = 1;
1723 if ( Dau_DsdIsConst0(pDsd) )
1724 iRes = 0;
1725 else if ( Dau_DsdIsConst1(pDsd) )
1726 iRes = 1;
1727 else if ( Dau_DsdIsVar(pDsd) )
1728 {
1729 pPerm[(*pnSupp)++] = Dau_DsdReadVar(pDsd);
1730 iRes = 2;
1731 }
1732 else
1733 {
1734 int pMatches[DAU_MAX_STR];
1735 If_DsdMergeMatches( pDsd, pMatches );
1736 iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm, pnSupp );
1737 }
1738 return Abc_LitNotCond( iRes, fCompl );
1739}
1740
1752// create signature of the support of the node
1753unsigned If_DsdSign_rec( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pnSupp )
1754{
1755 unsigned uSign = 0; int i;
1756 If_DsdObj_t * pFanin;
1757 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
1758 return (1 << (2*(*pnSupp)++));
1759 If_DsdObjForEachFanin( &p->vObjs, pObj, pFanin, i )
1760 uSign |= If_DsdSign_rec( p, pFanin, pnSupp );
1761 return uSign;
1762}
1763unsigned If_DsdSign( If_DsdMan_t * p, If_DsdObj_t * pObj, int iFan, int iFirst, int fShared )
1764{
1765 If_DsdObj_t * pFanin = If_DsdObjFanin( &p->vObjs, pObj, iFan );
1766 unsigned uSign = If_DsdSign_rec( p, pFanin, &iFirst );
1767 return fShared ? (uSign << 1) | uSign : uSign;
1768}
1769// collect supports of the node
1770void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
1771{
1772 If_DsdObj_t * pFanin; int i;
1773 If_DsdObjForEachFanin( &p->vObjs, pObj, pFanin, i )
1774 pSSizes[i] = If_DsdObjSuppSize(pFanin);
1775}
1776// checks if there is a way to package some fanins
1777unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1778{
1779 int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
1780 int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
1781 unsigned uRes;
1782 assert( pObj->nFans > 2 );
1783 assert( If_DsdObjSuppSize(pObj) > LutSize );
1784 If_DsdManGetSuppSizes( p, pObj, pSSizes );
1785 LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
1786 assert( LimitOut < LutSize );
1787 for ( i[0] = 0; i[0] < nFans; i[0]++ )
1788 for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1789 {
1790 SizeIn = pSSizes[i[0]] + pSSizes[i[1]];
1791 SizeOut = pObj->nSupp - SizeIn;
1792 if ( SizeIn > LutSize || SizeOut > LimitOut )
1793 continue;
1794 if ( !fDerive )
1795 return ~0;
1796 If_DsdManComputeFirst( p, pObj, pFirsts );
1797 uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1798 If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0);
1799 if ( uRes & uMaskNot )
1800 continue;
1801 return uRes;
1802 }
1803 if ( pObj->nFans == 3 )
1804 return 0;
1805 for ( i[0] = 0; i[0] < nFans; i[0]++ )
1806 for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1807 for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
1808 {
1809 SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]];
1810 SizeOut = pObj->nSupp - SizeIn;
1811 if ( SizeIn > LutSize || SizeOut > LimitOut )
1812 continue;
1813 if ( !fDerive )
1814 return ~0;
1815 If_DsdManComputeFirst( p, pObj, pFirsts );
1816 uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1817 If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
1818 If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0);
1819 if ( uRes & uMaskNot )
1820 continue;
1821 return uRes;
1822 }
1823 if ( pObj->nFans == 4 )
1824 return 0;
1825 for ( i[0] = 0; i[0] < nFans; i[0]++ )
1826 for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
1827 for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
1828 for ( i[3] = i[2]+1; i[3] < nFans; i[3]++ )
1829 {
1830 SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]] + pSSizes[i[3]];
1831 SizeOut = pObj->nSupp - SizeIn;
1832 if ( SizeIn > LutSize || SizeOut > LimitOut )
1833 continue;
1834 if ( !fDerive )
1835 return ~0;
1836 If_DsdManComputeFirst( p, pObj, pFirsts );
1837 uRes = If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
1838 If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
1839 If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0) |
1840 If_DsdSign(p, pObj, i[3], iFirst + pFirsts[i[3]], 0);
1841 if ( uRes & uMaskNot )
1842 continue;
1843 return uRes;
1844 }
1845 return 0;
1846}
1847// checks if there is a way to package some fanins
1848unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1849{
1850 int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
1851 unsigned uRes;
1852 assert( If_DsdObjFaninNum(pObj) == 3 );
1853 assert( If_DsdObjSuppSize(pObj) > LutSize );
1854 If_DsdManGetSuppSizes( p, pObj, pSSizes );
1855 LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
1856 assert( LimitOut < LutSize );
1857 // first input
1858 SizeIn = pSSizes[0] + pSSizes[1];
1859 SizeOut = pSSizes[0] + pSSizes[2] + 1;
1860 if ( SizeIn <= LutSize && SizeOut <= LimitOut )
1861 {
1862 if ( !fDerive )
1863 return ~0;
1864 If_DsdManComputeFirst( p, pObj, pFirsts );
1865 uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0);
1866 if ( (uRes & uMaskNot) == 0 )
1867 return uRes;
1868 }
1869 // second input
1870 SizeIn = pSSizes[0] + pSSizes[2];
1871 SizeOut = pSSizes[0] + pSSizes[1] + 1;
1872 if ( SizeIn <= LutSize && SizeOut <= LimitOut )
1873 {
1874 if ( !fDerive )
1875 return ~0;
1876 If_DsdManComputeFirst( p, pObj, pFirsts );
1877 uRes = If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0);
1878 if ( (uRes & uMaskNot) == 0 )
1879 return uRes;
1880 }
1881 return 0;
1882}
1883// checks if there is a way to package some fanins
1884unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, unsigned uMaskNot, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
1885{
1886 int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
1887 int truthId = If_DsdObjTruthId(p, pObj);
1888 int nFans = If_DsdObjFaninNum(pObj);
1889 Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs[pObj->nFans], truthId);
1890if ( fVerbose )
1891printf( "\n" );
1892if ( fVerbose )
1893Dau_DecPrintSets( vSets, nFans );
1894 assert( If_DsdObjFaninNum(pObj) > 2 );
1895 assert( If_DsdObjSuppSize(pObj) > LutSize );
1896 If_DsdManGetSuppSizes( p, pObj, pSSizes );
1897 LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
1898 assert( LimitOut < LutSize );
1899 Vec_IntForEachEntry( vSets, set, i )
1900 {
1901 SizeIn = SizeOut = 0;
1902 for ( v = 0; v < nFans; v++ )
1903 {
1904 int Value = ((set >> (v << 1)) & 3);
1905 if ( Value == 0 )
1906 SizeOut += pSSizes[v];
1907 else if ( Value == 1 )
1908 SizeIn += pSSizes[v];
1909 else if ( Value == 3 )
1910 {
1911 SizeIn += pSSizes[v];
1912 SizeOut += pSSizes[v];
1913 }
1914 else assert( 0 );
1915 if ( SizeIn > LutSize || SizeOut > LimitOut )
1916 break;
1917 }
1918 if ( v == nFans )
1919 {
1920 unsigned uRes = 0;
1921 if ( !fDerive )
1922 return ~0;
1923 If_DsdManComputeFirst( p, pObj, pFirsts );
1924 for ( v = 0; v < nFans; v++ )
1925 {
1926 int Value = ((set >> (v << 1)) & 3);
1927 if ( Value == 0 )
1928 {}
1929 else if ( Value == 1 )
1930 uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0);
1931 else if ( Value == 3 )
1932 uRes |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1);
1933 else assert( 0 );
1934 }
1935 if ( uRes & uMaskNot )
1936 continue;
1937 return uRes;
1938 }
1939 }
1940 return 0;
1941}
1942unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fVerbose )
1943{
1944 If_DsdObj_t * pObj, * pTemp;
1945 int i, Mask, iFirst;
1946 unsigned uRes;
1947 pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
1948 if ( fVerbose )
1949 If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
1950 if ( If_DsdObjSuppSize(pObj) <= LutSize )
1951 {
1952 if ( fVerbose )
1953 printf( " Trivial\n" );
1954 return ~0;
1955 }
1956 If_DsdManCollect( p, pObj->Id, p->vTemp1, p->vTemp2 );
1957 If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1958 if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
1959 {
1960 if ( fVerbose )
1961 printf( " Dec using node " );
1962 if ( fVerbose )
1963 If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
1964 iFirst = Vec_IntEntry(p->vTemp2, i);
1965 uRes = If_DsdSign_rec(p, pTemp, &iFirst);
1966 if ( uRes & uMaskNot )
1967 continue;
1968 return uRes;
1969 }
1970 If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1971 if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
1972 {
1973 if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
1974 {
1975 if ( fVerbose )
1976 printf( " " );
1977 if ( fVerbose )
1978 Abc_TtPrintBinary( (word *)&Mask, 4 );
1979 if ( fVerbose )
1980 printf( " Using multi-input AND/XOR node\n" );
1981 return Mask;
1982 }
1983 }
1984 If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1985 if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
1986 {
1987 if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
1988 {
1989 if ( fVerbose )
1990 printf( " " );
1991 if ( fVerbose )
1992 Abc_TtPrintBinary( (word *)&Mask, 4 );
1993 if ( fVerbose )
1994 printf( " Using multi-input MUX node\n" );
1995 return Mask;
1996 }
1997 }
1998 If_DsdVecForEachObjVec( p->vTemp1, &p->vObjs, pTemp, i )
1999 if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
2000 {
2001 if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), uMaskNot, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
2002 {
2003 if ( fVerbose )
2004 printf( " " );
2005 if ( fVerbose )
2006 Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
2007 if ( fVerbose )
2008 printf( " Using prime node\n" );
2009 return Mask;
2010 }
2011 }
2012 if ( fVerbose )
2013 printf( " UNDEC\n" );
2014// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
2015 return 0;
2016}
2017unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose )
2018{
2019 unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, uMaskNot, fVerbose );
2020 if ( uSet == 0 && fHighEffort )
2021 {
2022// abctime clk = Abc_Clock();
2023 int nVars = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
2024 word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
2025 uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
2026 if ( uSet )
2027 {
2028// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
2029// Dau_DecPrintSet( uSet, nVars, 1 );
2030 }
2031// p->timeCheck2 += Abc_Clock() - clk;
2032 }
2033 return uSet;
2034}
2035
2047unsigned If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
2048{
2049 return ~0;
2050}
2051
2063int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct )
2064{
2065 word pCopy[DAU_MAX_WORD], * pRes;
2066 char pDsd[DAU_MAX_STR];
2067 int iDsd, nSizeNonDec, nSupp = 0;
2068 int nWords = Abc_TtWordNum(nLeaves);
2069// abctime clk = 0;
2070 assert( nLeaves <= DAU_MAX_VAR );
2071 Abc_TtCopy( pCopy, pTruth, nWords, 0 );
2072//clk = Abc_Clock();
2073 nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
2074//p->timeDsd += Abc_Clock() - clk;
2075 if ( nSizeNonDec > 0 )
2076 Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
2077 memset( pPerm, 0xFF, (size_t)nLeaves );
2078//clk = Abc_Clock();
2079 iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
2080//p->timeCanon += Abc_Clock() - clk;
2081 assert( nSupp == nLeaves );
2082 // verify the result
2083//clk = Abc_Clock();
2084 pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
2085//p->timeVerify += Abc_Clock() - clk;
2086 if ( !Abc_TtEqual(pRes, pTruth, nWords) )
2087 {
2088// If_DsdManPrint( p, NULL );
2089 printf( "\n" );
2090 printf( "Verification failed!\n" );
2091 printf( "%s\n", pDsd );
2092 Dau_DsdPrintFromTruth( pTruth, nLeaves );
2093 Dau_DsdPrintFromTruth( pRes, nLeaves );
2094 If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
2095 printf( "\n" );
2096 }
2097 If_DsdVecObjIncRef( &p->vObjs, Abc_Lit2Var(iDsd) );
2098 assert( If_DsdVecLitSuppSize(&p->vObjs, iDsd) == nLeaves );
2099 return iDsd;
2100}
2101
2113void If_DsdManTest()
2114{
2115 Vec_Int_t * vSets;
2116 word t = 0x5277;
2117 t = Abc_Tt6Stretch( t, 4 );
2118// word t = 0xD9D900D900D900001010001000100000;
2119 vSets = Dau_DecFindSets( &t, 6 );
2120 Vec_IntFree( vSets );
2121}
2122
2123
2135int If_CutDsdBalancePinDelays_rec( If_DsdMan_t * p, int Id, int * pTimes, word * pRes, int * pnSupp, int nSuppAll, char * pPermLits )
2136{
2137 If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
2138 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
2139 {
2140 int iCutVar = Abc_Lit2Var(pPermLits[(*pnSupp)++]);
2141 *pRes = If_CutPinDelayInit(iCutVar);
2142 return pTimes[iCutVar];
2143 }
2144 if ( If_DsdObjType(pObj) == IF_DSD_MUX )
2145 {
2146 word pFaninRes[3], Res0, Res1;
2147 int i, iFanin, Delays[3];
2148 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2149 Delays[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2150 Res0 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[1], nSuppAll, 1 );
2151 Res1 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[2], nSuppAll, 1 );
2152 *pRes = If_CutPinDelayMax( Res0, Res1, nSuppAll, 1 );
2153 return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
2154 }
2155 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
2156 {
2157 word pFaninRes[IF_MAX_FUNC_LUTSIZE];
2158 int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE];
2159 Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
2160 assert( Vec_IntSize(vCover) > 0 );
2161 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2162 Delays[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2163 return If_CutSopBalancePinDelaysInt( vCover, Delays, pFaninRes, nSuppAll, pRes );
2164 }
2165 assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
2166 {
2167 word pFaninRes[IF_MAX_FUNC_LUTSIZE];
2168 int i, iFanin, Delay, Result = 0;
2169 int fXor = 0;//(If_DsdObjType(pObj) == IF_DSD_XOR);
2170 int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE];
2171 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2172 {
2173 Delay = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
2174 Result = If_LogCounterPinDelays( pCounter, &nCounter, pFaninRes, Delay, pFaninRes[i], nSuppAll, fXor );
2175 }
2176 assert( nCounter > 0 );
2177 if ( fXor )
2178 Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
2179 *pRes = If_LogPinDelaysMulti( pFaninRes, nCounter, nSuppAll, fXor );
2180 return Result;
2181 }
2182}
2183int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
2184{
2185 if ( pCut->nLeaves == 0 ) // const
2186 return 0;
2187 if ( pCut->nLeaves == 1 ) // variable
2188 {
2189 pPerm[0] = 0;
2190 return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
2191 }
2192 else
2193 {
2194 word Result = 0;
2195 int i, Delay, nSupp = 0, pTimes[IF_MAX_FUNC_LUTSIZE];
2196 for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2197 pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay;
2198 Delay = If_CutDsdBalancePinDelays_rec( p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)), pTimes, &Result, &nSupp, If_CutLeaveNum(pCut), If_CutDsdPerm(p, pCut) );
2199 assert( nSupp == If_CutLeaveNum(pCut) );
2200 If_CutPinDelayTranslate( Result, If_CutLeaveNum(pCut), pPerm );
2201 return Delay;
2202 }
2203}
2204
2205
2217int If_CutDsdPermLitMax( char * pPermLits, int nVars, int iVar )
2218{
2219 int i;
2220 assert( iVar >= 0 && iVar < nVars );
2221 for ( i = 0; i < nVars; i++ )
2222 if ( iVar == Abc_Lit2Var((int)pPermLits[i]) )
2223 return i;
2224 assert( 0 );
2225 return -1;
2226}
2227
2239int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSupp, Vec_Int_t * vAig, int * piLit, int nSuppAll, int * pArea, char * pPermLits )
2240{
2241 If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
2242 if ( If_DsdObjType(pObj) == IF_DSD_VAR )
2243 {
2244 int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] );
2245 if ( vAig )
2246 *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) );
2247 (*pnSupp)++;
2248 return pTimes[iCutVar];
2249 }
2250 if ( If_DsdObjType(pObj) == IF_DSD_MUX )
2251 {
2252 int i, iFanin, Delays[3], pFaninLits[3];
2253 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2254 {
2255 Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2256 if ( Delays[i] == -1 )
2257 return -1;
2258 if ( vAig )
2259 pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2260 }
2261 if ( vAig )
2262 *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll );
2263 else
2264 *pArea += 3;
2265 return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
2266 }
2267 if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
2268 {
2269 int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
2270 Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
2271 if ( Vec_IntSize(vCover) == 0 )
2272 return -1;
2273 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2274 {
2275 Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2276 if ( Delays[i] == -1 )
2277 return -1;
2278 if ( vAig )
2279 pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2280 }
2281 return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea );
2282 }
2283 assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
2284 {
2285 int i, iFanin, Delay, Result = 0;
2286 int fXor = 0;//(If_DsdObjType(pObj) == IF_DSD_XOR);
2287 int fXorFunc = (If_DsdObjType(pObj) == IF_DSD_XOR);
2288 int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
2289 If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
2290 {
2291 Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
2292 if ( Delay == -1 )
2293 return -1;
2294 if ( vAig )
2295 pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
2296 Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, vAig ? pFaninLits[i] : -1, vAig, nSuppAll, fXor, fXorFunc );
2297 }
2298 assert( nCounter > 0 );
2299 if ( fXor )
2300 Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
2301 if ( vAig )
2302 *piLit = If_LogCreateAndXorMulti( vAig, pFaninLits, nCounter, nSuppAll, fXorFunc );
2303 else
2304 *pArea += (pObj->nFans - 1) * (1 + 2 * fXor);
2305 return Result;
2306 }
2307}
2308int If_CutDsdBalanceEvalInt( If_DsdMan_t * p, int iDsd, int * pTimes, Vec_Int_t * vAig, int * pArea, char * pPermLits )
2309{
2310 int nSupp = 0, iLit = 0;
2311 int nSuppAll = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
2312 int Res = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iDsd), pTimes, &nSupp, vAig, &iLit, nSuppAll, pArea, pPermLits );
2313 if ( Res == -1 )
2314 return -1;
2315 assert( nSupp == nSuppAll );
2316 assert( vAig == NULL || Abc_Lit2Var(iLit) == nSupp + Abc_Lit2Var(Vec_IntSize(vAig)) - 1 );
2317 if ( vAig )
2318 Vec_IntPush( vAig, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(iDsd) );
2319 assert( vAig == NULL || (Vec_IntSize(vAig) & 1) );
2320 return Res;
2321}
2322int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
2323{
2324 int fUseCofs = 0;
2325 pCut->fUser = 1;
2326 if ( vAig )
2327 Vec_IntClear( vAig );
2328 if ( pCut->nLeaves == 0 ) // const
2329 {
2330 assert( Abc_Lit2Var(If_CutDsdLit(p, pCut)) == 0 );
2331 if ( vAig )
2332 Vec_IntPush( vAig, Abc_LitIsCompl(If_CutDsdLit(p, pCut)) );
2333 pCut->Cost = 0;
2334 return 0;
2335 }
2336 if ( pCut->nLeaves == 1 ) // variable
2337 {
2338 assert( Abc_Lit2Var(If_CutDsdLit(p, pCut)) == 1 );
2339 if ( vAig )
2340 Vec_IntPush( vAig, 0 );
2341 if ( vAig )
2342 Vec_IntPush( vAig, Abc_LitIsCompl(If_CutDsdLit(p, pCut)) );
2343 pCut->Cost = 0;
2344 return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
2345 }
2346 else
2347 {
2348 int fVerbose = 0;
2349 int i, pTimes[IF_MAX_FUNC_LUTSIZE];
2350 int Delay, Area = 0;
2351 char * pPermLits = If_CutDsdPerm(p, pCut);
2352 for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2353 pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay;
2354 Delay = If_CutDsdBalanceEvalInt( p->pIfDsdMan, Abc_LitNotCond(If_CutDsdLit(p, pCut), pCut->fCompl), pTimes, vAig, &Area, If_CutDsdPerm(p, pCut) );
2355 pCut->Cost = Area;
2356 // try cofactoring
2357 if ( fUseCofs )
2358 {
2359 // count how many times the max one appears
2360 int iMax = 0, nCountMax = 1;
2361 for ( i = 1; i < If_CutLeaveNum(pCut); i++ )
2362 if ( pTimes[i] > pTimes[iMax] )
2363 iMax = i, nCountMax = 1;
2364 else if ( pTimes[i] == pTimes[iMax] )
2365 nCountMax++;
2366 // decide when to try the decomposition
2367 if ( nCountMax == 1 && pTimes[iMax] + 2 < Delay && If_DsdManCheckNonTriv( p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)),
2368 If_CutLeaveNum(pCut), If_CutDsdPermLitMax(pPermLits, If_CutLeaveNum(pCut), iMax)) )
2369 {
2370// fVerbose = 1;
2371 Delay = pTimes[iMax] + 2;
2372 }
2373 }
2374 // report the result
2375 if ( fVerbose )
2376 {
2377/*
2378 int Max = 0, Two = 0;
2379 for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2380 Max = Abc_MaxInt( Max, pTimes[i] );
2381 for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2382 if ( pTimes[i] != Max )
2383 Two = Abc_MaxInt( Two, pTimes[i] );
2384 if ( Two + 2 < Max && Max + 3 < Delay )
2385*/
2386 {
2387 for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
2388 printf( "%3d ", pTimes[Abc_Lit2Var(pPermLits[i])] );
2389 for ( ; i < p->pPars->nLutSize; i++ )
2390 printf( " " );
2391 printf( "-> %3d ", Delay );
2392 If_DsdManPrintOne( stdout, p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(p, pCut)), NULL, 0 );
2393 printf( "\n" );
2394 }
2395 }
2396 return Delay;
2397 }
2398}
2399
2411void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose )
2412{
2413 ProgressBar * pProgress = NULL;
2414 sat_solver * pSat = NULL;
2415 If_DsdObj_t * pObj;
2416 Vec_Int_t * vLits;
2417 int i, Value, nVars;
2418 word * pTruth;
2419 if ( !fAdd || !LutSize )
2420 If_DsdVecForEachObj( &p->vObjs, pObj, i )
2421 pObj->fMark = 0;
2422 if ( LutSize == 0 )
2423 return;
2424 vLits = Vec_IntAlloc( 1000 );
2425 pSat = (sat_solver *)If_ManSatBuildXY( LutSize );
2426 pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2427 If_DsdVecForEachObj( &p->vObjs, pObj, i )
2428 {
2429 Extra_ProgressBarUpdate( pProgress, i, NULL );
2430 nVars = If_DsdObjSuppSize(pObj);
2431 if ( nVars <= LutSize )
2432 continue;
2433 if ( fAdd && !pObj->fMark )
2434 continue;
2435 pObj->fMark = 0;
2436 if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0, 0, 0) )
2437 continue;
2438 if ( fFast )
2439 Value = 0;
2440 else
2441 {
2442 pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2443 Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
2444 }
2445 if ( Value )
2446 continue;
2447 If_DsdVecObjSetMark( &p->vObjs, i );
2448 }
2449 Extra_ProgressBarStop( pProgress );
2450 If_ManSatUnbuild( pSat );
2451 Vec_IntFree( vLits );
2452 if ( fVerbose )
2453 If_DsdManPrintDistrib( p );
2454}
2455
2456
2457
2469void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose )
2470{
2471 int fVeryVerbose = 0;
2472 ProgressBar * pProgress = NULL;
2473 If_DsdObj_t * pObj;
2474 word * pTruth, * pConfig;
2475 int i, nVars, Value, LutSize;
2476 abctime clk = Abc_Clock();
2477 // parse the structure
2478 Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct );
2479 if ( pNtk == NULL )
2480 return;
2481 if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
2482 {
2483 printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2484 ABC_FREE( pNtk );
2485 return;
2486 }
2487 ABC_FREE( p->pCellStr );
2488 p->pCellStr = Abc_UtilStrsav( pStruct );
2489 if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
2490 printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2491 LutSize = Ifn_NtkLutSizeMax(pNtk);
2492 p->nTtBits = Ifn_NtkTtBits( pStruct );
2493 p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
2494 // print
2495 if ( fVerbose )
2496 {
2497 printf( "Considering programmable cell: " );
2498 Ifn_NtkPrint( pNtk );
2499 printf( "Largest LUT size = %d.\n", LutSize );
2500 }
2501 if ( p->nObjsPrev > 0 )
2502 printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2503 // clean the attributes
2504 If_DsdVecForEachObj( &p->vObjs, pObj, i )
2505 if ( i >= p->nObjsPrev )
2506 pObj->fMark = 0;
2507 if ( p->vConfigs == NULL )
2508 p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
2509 else
2510 Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
2511 pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2512 If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
2513 {
2514 if ( (i & 0xFF) == 0 )
2515 Extra_ProgressBarUpdate( pProgress, i, NULL );
2516 nVars = If_DsdObjSuppSize(pObj);
2517 //if ( nVars <= LutSize )
2518 // continue;
2519 pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2520 if ( fVeryVerbose )
2521 Dau_DsdPrintFromTruth( pTruth, nVars );
2522 if ( fVerbose )
2523 printf( "%6d : %2d ", i, nVars );
2524 pConfig = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * i );
2525 Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, pConfig );
2526 if ( fVeryVerbose )
2527 printf( "\n" );
2528 if ( Value == 0 )
2529 {
2530 If_DsdVecObjSetMark( &p->vObjs, i );
2531 memset( pConfig, 0, sizeof(word) * p->nConfigWords );
2532 }
2533 }
2534 p->nObjsPrev = 0;
2535 p->LutSize = 0;
2536 Extra_ProgressBarStop( pProgress );
2537 printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2538 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2539 if ( fVeryVerbose )
2540 If_DsdManPrintDistrib( p );
2541 ABC_FREE( pNtk );
2542}
2543
2544
2556#ifndef ABC_USE_PTHREADS
2557void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int nInputs, int fVerbose )
2558{
2559 Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
2560}
2561#else // pthreads are used
2562
2563
2564#define PAR_THR_MAX 100
2565typedef struct Ifn_ThData_t_
2566{
2567 Ifn_Ntk_t * pNtk; // network
2568 word pTruth[DAU_MAX_WORD];
2569 word pConfig[10]; // configuration data
2570 int nConfigWords;// configuration data word count
2571 int nVars; // support
2572 int Id; // object
2573 int nConfls; // conflicts
2574 int Result; // result
2575 int Status; // state
2576 abctime clkUsed; // total runtime
2577} Ifn_ThData_t;
2578void * Ifn_WorkerThread( void * pArg )
2579{
2580 Ifn_ThData_t * pThData = (Ifn_ThData_t *)pArg;
2581 volatile int * pPlace = &pThData->Status;
2582 abctime clk;
2583 while ( 1 )
2584 {
2585 while ( *pPlace == 0 );
2586 assert( pThData->Status == 1 );
2587 if ( pThData->Id == -1 )
2588 {
2589 pthread_exit( NULL );
2590 assert( 0 );
2591 return NULL;
2592 }
2593 clk = Abc_Clock();
2594 memset( pThData->pConfig, 0, sizeof(word) * pThData->nConfigWords );
2595 pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, pThData->pConfig );
2596 pThData->clkUsed += Abc_Clock() - clk;
2597 pThData->Status = 0;
2598// printf( "Finished object %d\n", pThData->Id );
2599 }
2600 assert( 0 );
2601 return NULL;
2602}
2603void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int nInputs, int fVerbose )
2604{
2605 int fVeryVerbose = 0;
2606 ProgressBar * pProgress = NULL;
2607 int i, k, nVars, LutSize;
2608 abctime clk = Abc_Clock();
2609 Ifn_Ntk_t * pNtk;
2610 If_DsdObj_t * pObj;
2611 if ( nProcs == 1 )
2612 {
2613 Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
2614 return;
2615 }
2616 if ( nProcs > PAR_THR_MAX )
2617 {
2618 printf( "The number of processes (%d) exceeds the precompiled limit (%d).\n", nProcs, PAR_THR_MAX );
2619 return;
2620 }
2621 // parse the structure
2622 pNtk = Ifn_NtkParse( pStruct );
2623 if ( pNtk == NULL )
2624 return;
2625 if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
2626 {
2627 printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2628 ABC_FREE( pNtk );
2629 return;
2630 }
2631 ABC_FREE( p->pCellStr );
2632 p->pCellStr = Abc_UtilStrsav( pStruct );
2633 if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
2634 printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
2635 // check the largest LUT
2636 LutSize = Ifn_NtkLutSizeMax(pNtk);
2637 p->nTtBits = Ifn_NtkTtBits( pStruct );
2638 p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
2639 assert( p->nConfigWords <= 10 );
2640 if ( fVerbose )
2641 {
2642 printf( "Considering programmable cell: " );
2643 Ifn_NtkPrint( pNtk );
2644 printf( "Largest LUT size = %d.\n", LutSize );
2645 }
2646 ABC_FREE( pNtk );
2647 if ( p->nObjsPrev > 0 )
2648 printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2649 // clean the attributes
2650 If_DsdVecForEachObj( &p->vObjs, pObj, i )
2651 if ( i >= p->nObjsPrev )
2652 pObj->fMark = 0;
2653 if ( p->vConfigs == NULL )
2654 p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
2655 else
2656 Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
2657 pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2658
2659 // perform concurrent solving
2660 {
2661 pthread_t WorkerThread[PAR_THR_MAX];
2662 Ifn_ThData_t ThData[PAR_THR_MAX];
2663 abctime clk, clkUsed = 0;
2664 int status, fRunning = 1, iCurrentObj = p->nObjsPrev;
2665 // start the threads
2666 for ( i = 0; i < nProcs; i++ )
2667 {
2668 ThData[i].pNtk = Ifn_NtkParse( pStruct );
2669 ThData[i].nVars = -1; // support
2670 ThData[i].Id = -1; // object
2671 ThData[i].nConfls = nConfls; // conflicts
2672 ThData[i].Result = -1; // result
2673 ThData[i].Status = 0; // state
2674 ThData[i].clkUsed = 0; // total runtime
2675 ThData[i].nConfigWords = p->nConfigWords;
2676 status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 );
2677 }
2678 // run the threads
2679 while ( fRunning || iCurrentObj < Vec_PtrSize(&p->vObjs) )
2680 {
2681 for ( i = 0; i < nProcs; i++ )
2682 {
2683 if ( ThData[i].Status )
2684 continue;
2685 assert( ThData[i].Status == 0 );
2686 if ( ThData[i].Id >= 0 )
2687 {
2688 //printf( "Closing obj %d with Thread %d:\n", ThData[i].Id, i );
2689 assert( ThData[i].Result == 0 || ThData[i].Result == 1 );
2690 if ( ThData[i].Result == 0 )
2691 If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
2692 else
2693 {
2694 word * pTtWords = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * ThData[i].Id );
2695 memcpy( pTtWords, ThData[i].pConfig, sizeof(word) * p->nConfigWords );
2696 }
2697 ThData[i].Id = -1;
2698 ThData[i].Result = -1;
2699 }
2700 for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ )
2701 {
2702 if ( (k & 0xFF) == 0 )
2703 Extra_ProgressBarUpdate( pProgress, k, NULL );
2704 pObj = If_DsdVecObj( &p->vObjs, k );
2705 nVars = If_DsdObjSuppSize(pObj);
2706 if ( nInputs && nVars < nInputs )
2707 continue;
2708 clk = Abc_Clock();
2709 If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth );
2710 clkUsed += Abc_Clock() - clk;
2711 ThData[i].nVars = nVars;
2712 ThData[i].Id = k;
2713 ThData[i].Result = -1;
2714 ThData[i].Status = 1;
2715 //printf( "Scheduling %d for Thread %d\n", ThData[i].Id, i );
2716 iCurrentObj = k+1;
2717 break;
2718 }
2719 }
2720 fRunning = 0;
2721 for ( i = 0; i < nProcs; i++ )
2722 if ( ThData[i].Status == 1 || (ThData[i].Status == 0 && ThData[i].Id >= 0) )
2723 fRunning = 1;
2724 //printf( "fRunning %d\n", fRunning );
2725 }
2726 // stop the threads
2727 for ( i = 0; i < nProcs; i++ )
2728 {
2729 assert( ThData[i].Status == 0 );
2730 ThData[i].Id = -1;
2731 ThData[i].Status = 1;
2732 ABC_FREE( ThData[i].pNtk );
2733 }
2734 if ( fVerbose )
2735 {
2736 printf( "Main : " );
2737 Abc_PrintTime( 1, "Time", clkUsed );
2738 for ( i = 0; i < nProcs; i++ )
2739 {
2740 printf( "Thread %d : ", i );
2741 Abc_PrintTime( 1, "Time", ThData[i].clkUsed );
2742 }
2743 }
2744 }
2745
2746 p->nObjsPrev = 0;
2747 p->LutSize = 0;
2748 Extra_ProgressBarStop( pProgress );
2749 printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2750 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2751 if ( fVeryVerbose )
2752 If_DsdManPrintDistrib( p );
2753}
2754
2755#endif // pthreads are used
2756
2768#ifdef ABC_USE_CUDD
2769
2770void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fThreshHeuristic, int fVerbose )
2771{
2772 extern int Extra_ThreshCheck( word * t, int nVars, int * pW );
2773 extern int Extra_ThreshHeuristic( word * t, int nVars, int * pW );
2774 int fVeryVerbose = 0;
2775 int pW[16];
2776 ProgressBar * pProgress = NULL;
2777 If_DsdObj_t * pObj;
2778 word * pTruth, Perm;
2779 int i, nVars, Value;
2780 abctime clk = Abc_Clock();
2781 assert( fUnate + fThresh + fThreshHeuristic <= 1 );
2782 if ( p->nObjsPrev > 0 )
2783 printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
2784 // clean the attributes
2785 If_DsdVecForEachObj( &p->vObjs, pObj, i )
2786 if ( i >= p->nObjsPrev )
2787 pObj->fMark = 0;
2788 if ( p->vConfigs == NULL )
2789 p->vConfigs = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
2790 else
2791 Vec_WrdFillExtra( p->vConfigs, Vec_PtrSize(&p->vObjs), 0 );
2792 pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
2793 If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
2794 {
2795 if ( (i & 0xFF) == 0 )
2796 Extra_ProgressBarUpdate( pProgress, i, NULL );
2797 nVars = If_DsdObjSuppSize(pObj);
2798 if ( nVars > 8 )
2799 continue;
2800 pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
2801 if ( fVeryVerbose )
2802 Dau_DsdPrintFromTruth( pTruth, nVars );
2803 if ( fVerbose )
2804 printf( "%6d : %2d ", i, nVars );
2805 if ( fUnate )
2806 Value = Abc_TtIsUnate( pTruth, nVars );
2807 else if ( fThresh )
2808 Value = Extra_ThreshCheck( pTruth, nVars, pW );
2809 else if ( fThreshHeuristic )
2810 Value = Extra_ThreshHeuristic( pTruth, nVars, pW );
2811 else
2812 Value = 0;
2813 Perm = 0;
2814 if ( fVeryVerbose )
2815 printf( "\n" );
2816 if ( Value )
2817 If_DsdVecObjSetMark( &p->vObjs, i );
2818 else
2819 Vec_WrdWriteEntry( p->vConfigs, i, Perm );
2820 }
2821 p->nObjsPrev = 0;
2822 p->LutSize = 0;
2823 Extra_ProgressBarStop( pProgress );
2824 printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
2825 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2826 if ( fVeryVerbose )
2827 If_DsdManPrintDistrib( p );
2828}
2829
2830#endif // ABC_USE_CUDD are used
2831
2835
2836
2837ABC_NAMESPACE_IMPL_END
2838
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Abc_MergeSortCost
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition utilSort.c:442
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
PAR_THR_MAX
#define PAR_THR_MAX
DECLARATIONS ///.
Definition bmcBmcG.c:31
sat_solver
#define sat_solver
Definition cecSatG2.c:34
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition dauNonDsd.c:390
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition dau.h:44
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition dauDsd.c:1912
Dau_DecFindSets
Vec_Int_t * Dau_DecFindSets(word *pInit, int nVars)
Definition dauNonDsd.c:516
Dau_DsdTruthCompose_rec
void Dau_DsdTruthCompose_rec(word *pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word *pRes, int nVars, int nWordsR)
Definition dauDsd.c:501
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition dauDsd.c:1968
DAU_DSD_XOR
@ DAU_DSD_XOR
Definition dau.h:56
DAU_DSD_PRIME
@ DAU_DSD_PRIME
Definition dau.h:58
DAU_DSD_MUX
@ DAU_DSD_MUX
Definition dau.h:57
DAU_DSD_AND
@ DAU_DSD_AND
Definition dau.h:55
DAU_MAX_STR
#define DAU_MAX_STR
Definition dau.h:43
Dau_DecPrintSets
void Dau_DecPrintSets(Vec_Int_t *vSets, int nVars)
Definition dauNonDsd.c:434
DAU_MAX_VAR
#define DAU_MAX_VAR
INCLUDES ///.
Definition dau.h:42
Dau_DecFindSets_int
Vec_Int_t * Dau_DecFindSets_int(word *pInit, int nVars, int *pSched[16])
Definition dauNonDsd.c:462
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition dauCanon.c:1036
p
Cube * p
Definition exorList.c:222
Extra_ThreshCheck
int Extra_ThreshCheck(word *t, int nVars, int *pW)
Definition extraBddThresh.c:570
Extra_ThreshHeuristic
int Extra_ThreshHeuristic(word *t, int nVars, int *pW)
Definition extraBddThresh.c:592
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition giaMan.c:224
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
If_DsdManDumpDsd
void If_DsdManDumpDsd(If_DsdMan_t *p, int Support)
Definition ifDsd.c:373
If_DsdManPrintOne
void If_DsdManPrintOne(FILE *pFile, If_DsdMan_t *p, int iObjId, unsigned char *pPermLits, int fNewLine)
Definition ifDsd.c:509
If_DsdManCheckNonTriv
int If_DsdManCheckNonTriv(If_DsdMan_t *p, int Id, int nVars, int iVarMax)
Definition ifDsd.c:819
If_DsdManFilter
If_DsdMan_t * If_DsdManFilter(If_DsdMan_t *p, int Limit)
Definition ifDsd.c:1294
If_DsdManTest
void If_DsdManTest()
Definition ifDsd.c:2113
If_CutDsdBalanceEval_rec
int If_CutDsdBalanceEval_rec(If_DsdMan_t *p, int Id, int *pTimes, int *pnSupp, Vec_Int_t *vAig, int *piLit, int nSuppAll, int *pArea, char *pPermLits)
Definition ifDsd.c:2239
If_DsdManCleanOccur
void If_DsdManCleanOccur(If_DsdMan_t *p, int fVerbose)
Definition ifDsd.c:1248
DSD_VERSION
#define DSD_VERSION
DECLARATIONS ///.
Definition ifDsd.c:51
If_DsdManCheckXY
unsigned If_DsdManCheckXY(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose)
Definition ifDsd.c:2017
If_DsdManSetNewAsUseless
void If_DsdManSetNewAsUseless(If_DsdMan_t *p)
Definition ifDsd.c:209
If_DsdManCheckMux
unsigned If_DsdManCheckMux(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition ifDsd.c:1848
If_DsdObjFindOrAdd
int If_DsdObjFindOrAdd(If_DsdMan_t *p, int Type, int *pLits, int nLits, word *pTruth)
Definition ifDsd.c:993
If_DsdObj_t
struct If_DsdObj_t_ If_DsdObj_t
Definition ifDsd.c:64
If_DsdManPrint
void If_DsdManPrint(If_DsdMan_t *p, char *pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose)
Definition ifDsd.c:701
If_DsdManCleanMarks
void If_DsdManCleanMarks(If_DsdMan_t *p, int fVerbose)
Definition ifDsd.c:1255
If_DsdManOperation
int If_DsdManOperation(If_DsdMan_t *p, int Type, int *pLits, int nLits, unsigned char *pPerm, word *pTruth)
Definition ifDsd.c:1528
If_DsdManLutSize
int If_DsdManLutSize(If_DsdMan_t *p)
Definition ifDsd.c:181
Id_DsdManTuneStr1
void Id_DsdManTuneStr1(If_DsdMan_t *p, char *pStruct, int nConfls, int fVerbose)
Definition ifDsd.c:2469
If_DsdSign_rec
unsigned If_DsdSign_rec(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pnSupp)
Definition ifDsd.c:1753
If_DsdManComputeFirstArray
int If_DsdManComputeFirstArray(If_DsdMan_t *p, int *pLits, int nLits, int *pFirsts)
Definition ifDsd.c:1514
If_DsdManPrint_rec
void If_DsdManPrint_rec(FILE *pFile, If_DsdMan_t *p, int iDsdLit, unsigned char *pPermLits, int *pnSupp)
Definition ifDsd.c:486
Id_DsdManTuneStr
void Id_DsdManTuneStr(If_DsdMan_t *p, char *pStruct, int nConfls, int nProcs, int nInputs, int fVerbose)
Definition ifDsd.c:2557
If_DsdManMerge
void If_DsdManMerge(If_DsdMan_t *p, If_DsdMan_t *pNew)
Definition ifDsd.c:1201
If_DsdManSuppSize
int If_DsdManSuppSize(If_DsdMan_t *p, int iDsd)
Definition ifDsd.c:197
If_DsdManCheckAndXor
unsigned If_DsdManCheckAndXor(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition ifDsd.c:1777
If_DsdManCheckPrime
unsigned If_DsdManCheckPrime(If_DsdMan_t *p, int iFirst, unsigned uMaskNot, If_DsdObj_t *pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose)
Definition ifDsd.c:1884
If_CutDsdBalanceEvalInt
int If_CutDsdBalanceEvalInt(If_DsdMan_t *p, int iDsd, int *pTimes, Vec_Int_t *vAig, int *pArea, char *pPermLits)
Definition ifDsd.c:2308
If_DsdManGetCellStr
char * If_DsdManGetCellStr(If_DsdMan_t *p)
Definition ifDsd.c:219
If_CutDsdBalancePinDelays_rec
int If_CutDsdBalancePinDelays_rec(If_DsdMan_t *p, int Id, int *pTimes, word *pRes, int *pnSupp, int nSuppAll, char *pPermLits)
Definition ifDsd.c:2135
If_DsdManAddDsd
int If_DsdManAddDsd(If_DsdMan_t *p, char *pDsd, word *pTruth, unsigned char *pPerm, int *pnSupp)
Definition ifDsd.c:1718
If_DsdObjHashLookup
unsigned * If_DsdObjHashLookup(If_DsdMan_t *p, int Type, int *pLits, int nLits, int truthId)
Definition ifDsd.c:920
If_DsdObjSort
void If_DsdObjSort(If_DsdMan_t *pMan, Vec_Ptr_t *p, int *pLits, int nLits, int *pPerm)
Definition ifDsd.c:879
If_DsdVecForEachObjVec
#define If_DsdVecForEachObjVec(vNodes, vVec, pObj, i)
Definition ifDsd.c:143
If_DsdManObjNum
int If_DsdManObjNum(If_DsdMan_t *p)
Definition ifDsd.c:177
If_DsdObjCreate
int If_DsdObjCreate(If_DsdMan_t *p, int Type, int *pLits, int nLits, int truthId)
Definition ifDsd.c:958
If_DsdManCheckNonDec_rec
int If_DsdManCheckNonDec_rec(If_DsdMan_t *p, int Id)
Definition ifDsd.c:470
If_DsdManInvertMarks
void If_DsdManInvertMarks(If_DsdMan_t *p, int fVerbose)
Definition ifDsd.c:1264
If_DsdManFilter_rec
void If_DsdManFilter_rec(If_DsdMan_t *pNew, If_DsdMan_t *p, int i, Vec_Int_t *vMap)
Definition ifDsd.c:1273
If_DsdManComputeTruth_rec
void If_DsdManComputeTruth_rec(If_DsdMan_t *p, int iDsd, word *pRes, unsigned char *pPermLits, int *pnSupp)
Definition ifDsd.c:1357
If_DsdManCompute
int If_DsdManCompute(If_DsdMan_t *p, word *pTruth, int nLeaves, unsigned char *pPerm, char *pLutStruct)
Definition ifDsd.c:2063
If_CutDsdPermLitMax
int If_CutDsdPermLitMax(char *pPermLits, int nVars, int iVar)
Definition ifDsd.c:2217
If_DsdManTune
void If_DsdManTune(If_DsdMan_t *p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose)
Definition ifDsd.c:2411
If_DsdType_t
If_DsdType_t
Definition ifDsd.c:54
IF_DSD_MUX
@ IF_DSD_MUX
Definition ifDsd.c:60
IF_DSD_AND
@ IF_DSD_AND
Definition ifDsd.c:58
IF_DSD_PRIME
@ IF_DSD_PRIME
Definition ifDsd.c:61
IF_DSD_CONST0
@ IF_DSD_CONST0
Definition ifDsd.c:56
IF_DSD_XOR
@ IF_DSD_XOR
Definition ifDsd.c:59
IF_DSD_NONE
@ IF_DSD_NONE
Definition ifDsd.c:55
IF_DSD_VAR
@ IF_DSD_VAR
Definition ifDsd.c:57
If_DsdManVarNum
int If_DsdManVarNum(If_DsdMan_t *p)
Definition ifDsd.c:173
If_DsdVecForEachObj
#define If_DsdVecForEachObj(vVec, pObj, i)
Definition ifDsd.c:139
If_DsdManPrintDistrib
void If_DsdManPrintDistrib(If_DsdMan_t *p)
Definition ifDsd.c:647
If_CutDsdBalanceEval
int If_CutDsdBalanceEval(If_Man_t *p, If_Cut_t *pCut, Vec_Int_t *vAig)
Definition ifDsd.c:2322
If_DsdVecForEachObjStart
#define If_DsdVecForEachObjStart(vVec, pObj, i, Start)
Definition ifDsd.c:141
If_DsdManGetFuncConfig
word * If_DsdManGetFuncConfig(If_DsdMan_t *p, int iDsd)
Definition ifDsd.c:215
If_DsdManSave
void If_DsdManSave(If_DsdMan_t *p, char *pFileName)
Definition ifDsd.c:1049
If_DsdSign
unsigned If_DsdSign(If_DsdMan_t *p, If_DsdObj_t *pObj, int iFan, int iFirst, int fShared)
Definition ifDsd.c:1763
If_DsdManPushInv
int If_DsdManPushInv(If_DsdMan_t *p, int iLit, unsigned char *pPerm)
Definition ifDsd.c:1496
If_DsdManCheckXYZ
unsigned If_DsdManCheckXYZ(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, int fVerbose)
Definition ifDsd.c:2047
If_DsdManAllocIsops
void If_DsdManAllocIsops(If_DsdMan_t *p, int nLutSize)
Definition ifDsd.c:306
If_DsdManPrintOccurs
void If_DsdManPrintOccurs(FILE *pFile, If_DsdMan_t *p)
Definition ifDsd.c:589
If_DsdObjForEachFaninLit
#define If_DsdObjForEachFaninLit(vVec, pObj, iLit, i)
Definition ifDsd.c:149
If_DsdManCheckXY_int
unsigned If_DsdManCheckXY_int(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fVerbose)
Definition ifDsd.c:1942
If_DsdManDumpAll
void If_DsdManDumpAll(If_DsdMan_t *p, int Support)
Definition ifDsd.c:407
If_DsdManGetSuppSizes
void If_DsdManGetSuppSizes(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pSSizes)
Definition ifDsd.c:1770
If_DsdManComputeTruthPtr
void If_DsdManComputeTruthPtr(If_DsdMan_t *p, int iDsd, unsigned char *pPermLits, word *pRes)
Definition ifDsd.c:1409
If_DsdManAddDsd_rec
int If_DsdManAddDsd_rec(char *pStr, char **p, int *pMatches, If_DsdMan_t *pMan, word *pTruth, unsigned char *pPerm, int *pnSupp)
Definition ifDsd.c:1665
If_DsdManPushInv_rec
int If_DsdManPushInv_rec(If_DsdMan_t *p, int iLit, unsigned char *pPerm)
Definition ifDsd.c:1466
Kit_TruthToGia
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
DSD_ARRAY_LIMIT
#define DSD_ARRAY_LIMIT
Definition ifDsd.c:521
If_DsdObjCompare
int If_DsdObjCompare(If_DsdMan_t *pMan, Vec_Ptr_t *p, int iLit0, int iLit1)
Definition ifDsd.c:844
If_DsdManReadMark
int If_DsdManReadMark(If_DsdMan_t *p, int iDsd)
Definition ifDsd.c:205
If_DsdManHasMarks
int If_DsdManHasMarks(If_DsdMan_t *p)
Definition ifDsd.c:432
If_DsdManPrintDecs
void If_DsdManPrintDecs(FILE *pFile, If_DsdMan_t *p)
Definition ifDsd.c:522
If_DsdVecForEachNode
#define If_DsdVecForEachNode(vVec, pObj, i)
Definition ifDsd.c:145
If_DsdManAlloc
If_DsdMan_t * If_DsdManAlloc(int nVars, int LutSize)
Definition ifDsd.c:264
If_DsdManCollect
void If_DsdManCollect(If_DsdMan_t *p, int Id, Vec_Int_t *vNodes, Vec_Int_t *vFirsts)
Definition ifDsd.c:1338
If_DsdManComputeTruth
word * If_DsdManComputeTruth(If_DsdMan_t *p, int iDsd, unsigned char *pPermLits)
Definition ifDsd.c:1427
If_DsdManComputeFirst
int If_DsdManComputeFirst(If_DsdMan_t *p, If_DsdObj_t *pObj, int *pFirsts)
Definition ifDsd.c:1524
If_DsdManCheckInv_rec
int If_DsdManCheckInv_rec(If_DsdMan_t *p, int iLit)
Definition ifDsd.c:1445
If_DsdManPermBitNum
int If_DsdManPermBitNum(If_DsdMan_t *p)
Definition ifDsd.c:189
If_DsdManCollect_rec
void If_DsdManCollect_rec(If_DsdMan_t *p, int Id, Vec_Int_t *vNodes, Vec_Int_t *vFirsts, int *pnSupp)
Definition ifDsd.c:1321
If_DsdManLoad
If_DsdMan_t * If_DsdManLoad(char *pFileName)
Definition ifDsd.c:1106
If_DsdManFree
void If_DsdManFree(If_DsdMan_t *p, int fVerbose)
Definition ifDsd.c:333
If_DsdManSetLutSize
void If_DsdManSetLutSize(If_DsdMan_t *p, int nLutSize)
Definition ifDsd.c:193
If_DsdObjAlloc
If_DsdObj_t * If_DsdObjAlloc(If_DsdMan_t *p, int Type, int nFans)
Definition ifDsd.c:247
If_DsdObjForEachFanin
#define If_DsdObjForEachFanin(vVec, pObj, pFanin, i)
Definition ifDsd.c:147
If_DsdManCheckDec
int If_DsdManCheckDec(If_DsdMan_t *p, int iDsd)
Definition ifDsd.c:201
If_DsdManTtBitNum
int If_DsdManTtBitNum(If_DsdMan_t *p)
Definition ifDsd.c:185
If_CutDsdBalancePinDelays
int If_CutDsdBalancePinDelays(If_Man_t *p, If_Cut_t *pCut, char *pPerm)
Definition ifDsd.c:2183
If_DsdManFileName
char * If_DsdManFileName(If_DsdMan_t *p)
FUNCTION DEFINITIONS ///.
Definition ifDsd.c:169
If_DsdManHashProfile
void If_DsdManHashProfile(If_DsdMan_t *p)
Definition ifDsd.c:453
Ifn_NtkInputNum
int Ifn_NtkInputNum(Ifn_Ntk_t *p)
Definition ifTune.c:167
If_DsdManCheckXY
unsigned If_DsdManCheckXY(If_DsdMan_t *p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose)
Definition ifDsd.c:2017
Ifn_NtkPrint
void Ifn_NtkPrint(Ifn_Ntk_t *p)
Definition ifTune.c:141
If_Cut_t
struct If_Cut_t_ If_Cut_t
Definition if.h:80
Ifn_NtkParse
Ifn_Ntk_t * Ifn_NtkParse(char *pStr)
Definition ifTune.c:440
If_ManSatCheckXYall
unsigned If_ManSatCheckXYall(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition ifSat.c:477
Ifn_NtkMatch
int Ifn_NtkMatch(Ifn_Ntk_t *p, word *pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word *pConfig)
Definition ifTune.c:1328
Id_DsdManTuneThresh
void Id_DsdManTuneThresh(If_DsdMan_t *p, int fUnate, int fThresh, int fThreshHeuristic, int fVerbose)
Ifn_NtkTtBits
int Ifn_NtkTtBits(char *pStr)
Definition ifTune.c:464
If_ManSatBuildXY
void * If_ManSatBuildXY(int nLutSize)
DECLARATIONS ///.
Definition ifSat.c:45
If_DsdMan_t
struct If_DsdMan_t_ If_DsdMan_t
Definition if.h:84
Ifn_NtkLutSizeMax
int Ifn_NtkLutSizeMax(Ifn_Ntk_t *p)
Definition ifTune.c:159
Ifn_Ntk_t
struct Ifn_Ntk_t_ Ifn_Ntk_t
Definition if.h:85
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition if.h:55
If_Man_t
struct If_Man_t_ If_Man_t
BASIC TYPES ///.
Definition if.h:77
If_CutSopBalanceEvalInt
int If_CutSopBalanceEvalInt(Vec_Int_t *vCover, int *pTimes, int *pFaninLits, Vec_Int_t *vAig, int *piRes, int nSuppAll, int *pArea)
Definition ifDelay.c:192
If_ManSatUnbuild
void If_ManSatUnbuild(void *p)
Definition ifSat.c:86
If_CutSopBalancePinDelaysInt
int If_CutSopBalancePinDelaysInt(Vec_Int_t *vCover, int *pTimes, word *pFaninRes, int nSuppAll, word *pRes)
Definition ifDelay.c:120
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Mem_FlexStart
Mem_Flex_t * Mem_FlexStart()
Definition mem.c:327
Mem_FlexEntryFetch
char * Mem_FlexEntryFetch(Mem_Flex_t *p, int nBytes)
Definition mem.c:388
Mem_FlexReadMemUsage
int Mem_FlexReadMemUsage(Mem_Flex_t *p)
Definition mem.c:461
Mem_FlexStop
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition mem.c:359
Mem_Flex_t
struct Mem_Flex_t_ Mem_Flex_t
Definition mem.h:34
If_Cut_t_::Cost
unsigned Cost
Definition if.h:310
If_Cut_t_::nLeaves
unsigned nLeaves
Definition if.h:316
If_Cut_t_::fCompl
unsigned fCompl
Definition if.h:311
If_Cut_t_::fUser
unsigned fUser
Definition if.h:312
If_DsdMan_t_
Definition ifDsd.c:77
If_DsdMan_t_::nUniqueHits
int nUniqueHits
Definition ifDsd.c:104
If_DsdMan_t_::vNexts
Vec_Int_t vNexts
Definition ifDsd.c:86
If_DsdMan_t_::nVars
int nVars
Definition ifDsd.c:79
If_DsdMan_t_::nWords
int nWords
Definition ifDsd.c:81
If_DsdMan_t_::vTtDecs
Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]
Definition ifDsd.c:92
If_DsdMan_t_::pTtElems
word ** pTtElems
Definition ifDsd.c:90
If_DsdMan_t_::nUniqueMisses
int nUniqueMisses
Definition ifDsd.c:105
If_DsdMan_t_::vConfigs
Vec_Wrd_t * vConfigs
Definition ifDsd.c:97
If_DsdMan_t_::pMem
Mem_Flex_t * pMem
Definition ifDsd.c:84
If_DsdMan_t_::timeDsd
abctime timeDsd
Definition ifDsd.c:106
If_DsdMan_t_::timeVerify
abctime timeVerify
Definition ifDsd.c:110
If_DsdMan_t_::vTemp1
Vec_Int_t * vTemp1
Definition ifDsd.c:88
If_DsdMan_t_::nConfigWords
int nConfigWords
Definition ifDsd.c:96
If_DsdMan_t_::pCellStr
char * pCellStr
Definition ifDsd.c:101
If_DsdMan_t_::vTruths
Vec_Int_t vTruths
Definition ifDsd.c:87
If_DsdMan_t_::nTtBits
int nTtBits
Definition ifDsd.c:95
If_DsdMan_t_::LutSize
int LutSize
Definition ifDsd.c:80
If_DsdMan_t_::vTemp2
Vec_Int_t * vTemp2
Definition ifDsd.c:89
If_DsdMan_t_::pTtGia
Gia_Man_t * pTtGia
Definition ifDsd.c:98
If_DsdMan_t_::vIsops
Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]
Definition ifDsd.c:93
If_DsdMan_t_::fNewAsUseless
int fNewAsUseless
Definition ifDsd.c:103
If_DsdMan_t_::timeCanon
abctime timeCanon
Definition ifDsd.c:107
If_DsdMan_t_::pSat
void * pSat
Definition ifDsd.c:100
If_DsdMan_t_::pStore
char * pStore
Definition ifDsd.c:78
If_DsdMan_t_::timeCheck
abctime timeCheck
Definition ifDsd.c:108
If_DsdMan_t_::vTtMem
Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]
Definition ifDsd.c:91
If_DsdMan_t_::vObjs
Vec_Ptr_t vObjs
Definition ifDsd.c:85
If_DsdMan_t_::timeCheck2
abctime timeCheck2
Definition ifDsd.c:109
If_DsdMan_t_::vCover
Vec_Int_t * vCover
Definition ifDsd.c:99
If_DsdMan_t_::pSched
int * pSched[IF_MAX_FUNC_LUTSIZE+1]
Definition ifDsd.c:94
If_DsdMan_t_::pBins
unsigned * pBins
Definition ifDsd.c:83
If_DsdMan_t_::nObjsPrev
int nObjsPrev
Definition ifDsd.c:102
If_DsdMan_t_::nBins
int nBins
Definition ifDsd.c:82
If_DsdObj_t_
Definition ifDsd.c:66
If_DsdObj_t_::nFans
unsigned nFans
Definition ifDsd.c:72
If_DsdObj_t_::fMark
unsigned fMark
Definition ifDsd.c:70
If_DsdObj_t_::pFans
unsigned pFans[0]
Definition ifDsd.c:73
If_DsdObj_t_::Count
unsigned Count
Definition ifDsd.c:71
If_DsdObj_t_::Type
unsigned Type
Definition ifDsd.c:68
If_DsdObj_t_::Id
unsigned Id
Definition ifDsd.c:67
If_DsdObj_t_::nSupp
unsigned nSupp
Definition ifDsd.c:69
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
strncmp
int strncmp()
memcpy
char * memcpy()
memset
char * memset()
strlen
int strlen()
memcmp
int memcmp()
sprintf
char * sprintf()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_MemForEachEntry
#define Vec_MemForEachEntry(p, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecMem.h:68
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
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_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42