Skip to content

A
abc
Commit 883e21fe by Alan Mishchenko
Options

Improvements to DSD manager.

parent 329cdc35
Showing with 189 additions and 99 deletions
src/bool/kit/kitHop.c
...@@ -73,7 +73,7 @@ int Kit_GraphToGia( Gia_Man_t * pMan, Kit_Graph_t * pGraph, Vec_Int_t * vLeaves, ...@@ -73,7 +73,7 @@ int Kit_GraphToGia( Gia_Man_t * pMan, Kit_Graph_t * pGraph, Vec_Int_t * vLeaves,
int i; int i;
// collect the fanins // collect the fanins
Kit_GraphForEachLeaf( pGraph, pNode, i ) Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->iFunc = Vec_IntEntry( vLeaves, i ); pNode->iFunc = vLeaves ? Vec_IntEntry(vLeaves, i) : Gia_Obj2Lit(pMan, Gia_ManPi(pMan, i));
// perform strashing // perform strashing
return Kit_GraphToGiaInternal( pMan, pGraph, fHash ); return Kit_GraphToGiaInternal( pMan, pGraph, fHash );
} }
......
src/map/if/ifDsd.c
...@@ -22,6 +22,7 @@ ...@@ -22,6 +22,7 @@
#include "if.h" #include "if.h"
#include "misc/extra/extra.h" #include "misc/extra/extra.h"
#include "sat/bsat/satSolver.h" #include "sat/bsat/satSolver.h"
#include "aig/gia/gia.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -64,13 +65,16 @@ struct If_DsdMan_t_ ...@@ -64,13 +65,16 @@ struct If_DsdMan_t_
Mem_Flex_t * pMem; // memory for nodes Mem_Flex_t * pMem; // memory for nodes
Vec_Ptr_t * vObjs; // objects Vec_Ptr_t * vObjs; // objects
Vec_Int_t * vNexts; // next pointers Vec_Int_t * vNexts; // next pointers
Vec_Int_t * vTruths; // truth IDs of prime nodes
Vec_Int_t * vTemp1; // temp Vec_Int_t * vTemp1; // temp
Vec_Int_t * vTemp2; // temp Vec_Int_t * vTemp2; // temp
word ** pTtElems; // elementary TTs word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
Vec_Ptr_t * vTtDecs; // truth table decompositions Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules
Gia_Man_t * pTtGia; // GIA to represent truth tables
Vec_Int_t * vCover; // temporary memory
void * pSat; // SAT solver void * pSat; // SAT solver
int * pSched[16]; // grey code schedules
int nUniqueHits; // statistics int nUniqueHits; // statistics
int nUniqueMisses; // statistics int nUniqueMisses; // statistics
abctime timeDsd; // statistics abctime timeDsd; // statistics
...@@ -81,9 +85,9 @@ struct If_DsdMan_t_ ...@@ -81,9 +85,9 @@ struct If_DsdMan_t_
}; };
static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); } static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
static inline int If_DsdObjTruthId( If_DsdObj_t * pObj ) { return pObj->Type == IF_DSD_PRIME ? pObj->pFans[pObj->nFans] : -1; } static 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; }
static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem, If_DsdObjTruthId(pObj)); } static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem[pObj->nFans], If_DsdObjTruthId(p, pObj)); }
static inline void If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); pObj->pFans[pObj->nFans] = Id; } static 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); }
static inline void If_DsdObjClean( If_DsdObj_t * pObj ) { memset( pObj, 0, sizeof(If_DsdObj_t) ); } static inline void If_DsdObjClean( If_DsdObj_t * pObj ) { memset( pObj, 0, sizeof(If_DsdObj_t) ); }
static inline int If_DsdObjId( If_DsdObj_t * pObj ) { return pObj->Id; } static inline int If_DsdObjId( If_DsdObj_t * pObj ) { return pObj->Id; }
...@@ -117,6 +121,8 @@ static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) ...@@ -117,6 +121,8 @@ static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj )
#define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \ #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \
for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ ) for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ )
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -174,7 +180,7 @@ static inline word ** If_ManDsdTtElems() ...@@ -174,7 +180,7 @@ static inline word ** If_ManDsdTtElems()
} }
If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
{ {
int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) ); int nWords = If_DsdObjWordNum( nFans );
If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords ); If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
If_DsdObjClean( pObj ); If_DsdObjClean( pObj );
pObj->Type = Type; pObj->Type = Type;
...@@ -184,7 +190,9 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) ...@@ -184,7 +190,9 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
pObj->Count = 0; pObj->Count = 0;
Vec_PtrPush( p->vObjs, pObj ); Vec_PtrPush( p->vObjs, pObj );
Vec_IntPush( p->vNexts, 0 ); Vec_IntPush( p->vNexts, 0 );
Vec_IntPush( p->vTruths, -1 );
assert( Vec_IntSize(p->vNexts) == Vec_PtrSize(p->vObjs) ); assert( Vec_IntSize(p->vNexts) == Vec_PtrSize(p->vObjs) );
assert( Vec_IntSize(p->vTruths) == Vec_PtrSize(p->vObjs) );
return pObj; return pObj;
} }
If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
...@@ -202,14 +210,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) ...@@ -202,14 +210,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
p->pMem = Mem_FlexStart(); p->pMem = Mem_FlexStart();
p->vObjs = Vec_PtrAlloc( 10000 ); p->vObjs = Vec_PtrAlloc( 10000 );
p->vNexts = Vec_IntAlloc( 10000 ); p->vNexts = Vec_IntAlloc( 10000 );
p->vTruths = Vec_IntAlloc( 10000 );
If_DsdObjAlloc( p, IF_DSD_CONST0, 0 ); If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1; If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
p->vTemp1 = Vec_IntAlloc( 32 ); p->vTemp1 = Vec_IntAlloc( 32 );
p->vTemp2 = Vec_IntAlloc( 32 ); p->vTemp2 = Vec_IntAlloc( 32 );
p->pTtElems = If_ManDsdTtElems(); p->pTtElems = If_ManDsdTtElems();
p->vTtDecs = Vec_PtrAlloc( 1000 ); for ( v = 3; v <= nVars; v++ )
p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 ); {
Vec_MemHashAlloc( p->vTtMem, 10000 ); p->vTtMem[v] = Vec_MemAlloc( Abc_TtWordNum(v), 12 );
Vec_MemHashAlloc( p->vTtMem[v], 10000 );
p->vTtDecs[v] = Vec_PtrAlloc( 1000 );
}
/*
p->pTtGia = Gia_ManStart( nVars );
Gia_ManHashAlloc( p->pTtGia );
for ( v = 0; v < nVars; v++ )
Gia_ManAppendCi( p->pTtGia );
p->vCover = Vec_IntAlloc( 0 );
*/
for ( v = 2; v < nVars; v++ ) for ( v = 2; v < nVars; v++ )
p->pSched[v] = Extra_GreyCodeSchedule( v ); p->pSched[v] = Extra_GreyCodeSchedule( v );
if ( LutSize ) if ( LutSize )
...@@ -223,17 +242,30 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) ...@@ -223,17 +242,30 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 ); If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 );
if ( fVerbose ) if ( fVerbose )
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars ); {
char FileName[10];
for ( v = 3; v <= p->nVars; v++ )
{
sprintf( FileName, "dumpdsd%02d", v );
Vec_MemDumpTruthTables( p->vTtMem[v], FileName, v );
}
}
for ( v = 2; v < p->nVars; v++ ) for ( v = 2; v < p->nVars; v++ )
ABC_FREE( p->pSched[v] ); ABC_FREE( p->pSched[v] );
Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); for ( v = 3; v <= p->nVars; v++ )
Vec_MemHashFree( p->vTtMem ); {
Vec_MemFreeP( &p->vTtMem ); Vec_MemHashFree( p->vTtMem[v] );
Vec_MemFree( p->vTtMem[v] );
Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) );
}
Vec_IntFreeP( &p->vTemp1 ); Vec_IntFreeP( &p->vTemp1 );
Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vTemp2 );
Vec_IntFreeP( &p->vNexts ); Vec_IntFreeP( &p->vNexts );
Vec_IntFreeP( &p->vTruths );
Vec_PtrFreeP( &p->vObjs ); Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 ); Mem_FlexStop( p->pMem, 0 );
Gia_ManStopP( &p->pTtGia );
Vec_IntFreeP( &p->vCover );
If_ManSatUnbuild( p->pSat ); If_ManSatUnbuild( p->pSat );
ABC_FREE( p->pStore ); ABC_FREE( p->pStore );
ABC_FREE( p->pBins ); ABC_FREE( p->pBins );
...@@ -242,31 +274,35 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) ...@@ -242,31 +274,35 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
void If_DsdManDumpDsd( If_DsdMan_t * p, int Support ) void If_DsdManDumpDsd( If_DsdMan_t * p, int Support )
{ {
char * pFileName = "tts_nondsd.txt"; char * pFileName = "tts_nondsd.txt";
If_DsdObj_t * pObj; int i; If_DsdObj_t * pObj;
Vec_Int_t * vMap; Vec_Int_t * vMap;
FILE * pFile = fopen( pFileName, "wb" ); FILE * pFile = fopen( pFileName, "wb" );
int v, i;
if ( pFile == NULL ) if ( pFile == NULL )
{ {
printf( "Cannot open file \"%s\".\n", pFileName ); printf( "Cannot open file \"%s\".\n", pFileName );
return; return;
} }
vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) ); for ( v = 3; v <= p->nVars; v++ )
{
vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem[v]) );
If_DsdVecForEachObj( p->vObjs, pObj, i ) If_DsdVecForEachObj( p->vObjs, pObj, i )
{ {
if ( Support && Support != If_DsdObjSuppSize(pObj) ) if ( Support && Support != If_DsdObjSuppSize(pObj) )
continue; continue;
if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
continue; continue;
if ( Vec_IntEntry(vMap, If_DsdObjTruthId(pObj)) ) if ( Vec_IntEntry(vMap, If_DsdObjTruthId(p, pObj)) )
continue; continue;
Vec_IntWriteEntry(vMap, If_DsdObjTruthId(pObj), 1); Vec_IntWriteEntry(vMap, If_DsdObjTruthId(p, pObj), 1);
fprintf( pFile, "0x" ); fprintf( pFile, "0x" );
Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : p->nVars ); Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : v );
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
// printf( " " ); //printf( " " );
// Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); //Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
} }
Vec_IntFree( vMap ); Vec_IntFree( vMap );
}
fclose( pFile ); fclose( pFile );
} }
void If_DsdManDumpAll( If_DsdMan_t * p, int Support ) void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
...@@ -378,38 +414,41 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char ...@@ -378,38 +414,41 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p ) void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p )
{ {
Vec_Int_t * vDecs; Vec_Int_t * vDecs;
int i, k, nSuppSize, nDecMax = 0; int i, k, v, nSuppSize, nDecMax = 0;
int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0}; int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0};
int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0}; int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0};
int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0}; int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0};
int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}}; int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}};
word * pTruth; word * pTruth;
assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); for ( v = 3; v <= p->nVars; v++ )
{
assert( Vec_MemEntryNum(p->vTtMem[v]) == Vec_PtrSize(p->vTtDecs[v]) );
// find max number of decompositions // find max number of decompositions
Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i ) Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
{ {
pTruth = Vec_MemReadEntry( p->vTtMem, i ); pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) ); pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) );
nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) ); nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) );
} }
// fill up // fill up
Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i ) Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
{ {
pTruth = Vec_MemReadEntry( p->vTtMem, i ); pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
pCountsAll[nSuppSize]++; pCountsAll[nSuppSize]++;
pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs); pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs);
pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++; pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++;
// pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++; // pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++;
/* /*
if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] ) if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] )
{ {
fprintf( pFile, "0x" ); fprintf( pFile, "0x" );
Abc_TtPrintHex( pTruth, nSuppSize ); Abc_TtPrintHex( pTruth, nSuppSize );
Dau_DecPrintSets( vDecs, nSuppSize ); Dau_DecPrintSets( vDecs, nSuppSize );
} }
*/ */
}
} }
// print header // print header
fprintf( pFile, " N : " ); fprintf( pFile, " N : " );
...@@ -499,39 +538,64 @@ void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p ) ...@@ -499,39 +538,64 @@ void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p )
void If_DsdManPrintDistrib( If_DsdMan_t * p ) void If_DsdManPrintDistrib( If_DsdMan_t * p )
{ {
If_DsdObj_t * pObj; If_DsdObj_t * pObj; int i;
int CountAll[IF_MAX_FUNC_LUTSIZE] = {0}; int CountObj[IF_MAX_FUNC_LUTSIZE+2] = {0};
int CountNon[IF_MAX_FUNC_LUTSIZE] = {0}; int CountObjNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
int i, nVars, CountNonTotal = 0; int CountObjNpn[IF_MAX_FUNC_LUTSIZE+2] = {0};
If_DsdVecForEachObj( p->vObjs, pObj, i ) int CountStr[IF_MAX_FUNC_LUTSIZE+2] = {0};
int CountStrNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
int CountMarked[IF_MAX_FUNC_LUTSIZE+2] = {0};
for ( i = 3; i <= p->nVars; i++ )
{ {
nVars = If_DsdObjSuppSize(pObj); CountObjNpn[i] = Vec_MemEntryNum(p->vTtMem[i]);
CountAll[nVars]++; CountObjNpn[p->nVars+1] += Vec_MemEntryNum(p->vTtMem[i]);
if ( !If_DsdVecObjMark(p->vObjs, i) )
continue;
CountNon[nVars]++;
CountNonTotal++;
} }
for ( i = 0; i <= p->nVars; i++ ) If_DsdVecForEachObj( p->vObjs, pObj, i )
{ {
printf( "%3d : ", i ); CountObj[If_DsdObjFaninNum(pObj)]++, CountObj[p->nVars+1]++;
printf( "All = %8d ", CountAll[i] ); if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
printf( "Non = %8d ", CountNon[i] ); CountObjNon[If_DsdObjFaninNum(pObj)]++, CountObjNon[p->nVars+1]++;
printf( "(%6.2f %%)", 100.0 * CountNon[i] / CountAll[i] ); CountStr[If_DsdObjSuppSize(pObj)]++, CountStr[p->nVars+1]++;
if ( If_DsdManCheckNonDec_rec(p, i) )
CountStrNon[If_DsdObjSuppSize(pObj)]++, CountStrNon[p->nVars+1]++;
if ( If_DsdVecObjMark(p->vObjs, i) )
CountMarked[If_DsdObjSuppSize(pObj)]++, CountMarked[p->nVars+1]++;
}
printf( "***** DSD MANAGER STATISTICS *****\n" );
printf( "Support " );
printf( "Obj " );
printf( "ObjNDSD " );
printf( "NPNNDSD " );
printf( "Str " );
printf( "StrNDSD " );
printf( "Marked " );
printf( "\n" ); printf( "\n" );
} for ( i = 0; i <= p->nVars + 1; i++ )
{
if ( i == p->nVars + 1 )
printf( "All : " ); printf( "All : " );
printf( "All = %8d ", Vec_PtrSize(p->vObjs) ); else
printf( "Non = %8d ", CountNonTotal ); printf( "%3d : ", i );
printf( "(%6.2f %%)", 100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) ); printf( "%9d ", CountObj[i] );
printf( "%9d ", CountObjNon[i] );
printf( "%6.2f %% ", 100.0 * CountObjNon[i] / Abc_MaxInt(1, CountObj[i]) );
printf( "%9d ", CountObjNpn[i] );
printf( "%6.2f %% ", 100.0 * CountObjNpn[i] / Abc_MaxInt(1, CountObj[i]) );
printf( " " );
printf( "%9d ", CountStr[i] );
printf( "%9d ", CountStrNon[i] );
printf( "%6.2f %% ", 100.0 * CountStrNon[i] / Abc_MaxInt(1, CountStr[i]) );
printf( "%9d ", CountMarked[i] );
printf( "%6.2f %%", 100.0 * CountMarked[i] / Abc_MaxInt(1, CountStr[i]) );
printf( "\n" ); printf( "\n" );
}
} }
void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose ) void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose )
{ {
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
Vec_Int_t * vStructs, * vCounts; Vec_Int_t * vStructs, * vCounts;
int CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0; int CountUsed = 0, CountNonDsd = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0;
int i, * pPerm, DsdMax = 0; int i, v, * pPerm, DsdMax = 0, MemSizeTTs = 0, MemSizeDecs = 0;
FILE * pFile; FILE * pFile;
pFile = pFileName ? fopen( pFileName, "wb" ) : stdout; pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
if ( pFileName && pFile == NULL ) if ( pFileName && pFile == NULL )
...@@ -548,22 +612,24 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, ...@@ -548,22 +612,24 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 ); CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
CountMarked += If_DsdVecObjMark( p->vObjs, i ); CountMarked += If_DsdVecObjMark( p->vObjs, i );
} }
fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); for ( v = 3; v <= p->nVars; v++ )
fprintf( pFile, "Externally used objects = %8d\n", CountUsed ); {
fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) ); CountNonDsd += Vec_MemEntryNum(p->vTtMem[v]);
fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr ); MemSizeTTs += Vec_MemEntrySize(p->vTtMem[v]) * Vec_MemEntryNum(p->vTtMem[v]);
fprintf( pFile, "Prime objects = %8d\n", CountPrime ); MemSizeDecs += (int)Vec_VecMemoryInt((Vec_Vec_t *)(p->vTtDecs[v]));
fprintf( pFile, "Marked objects = %8d\n", CountMarked ); }
fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits ); If_DsdManPrintDistrib( p );
if ( p->pTtGia )
fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) );
fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses ); fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses );
fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits );
fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(Vec_MemEntrySize(p->vTtMem)+1)*Vec_MemEntryNum(p->vTtMem)/(1<<20) ); fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(MemSizeTTs+sizeof(int)*Vec_IntCap(p->vTruths))/(1<<20) );
fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(p->vNexts))/(1<<20) ); fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(p->vNexts))/(1<<20) );
fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", (float)Vec_VecMemoryInt((Vec_Vec_t *)p->vTtDecs)/(1<<20) ); fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", 1.0*MemSizeDecs/(1<<20) );
fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
If_DsdManPrintDistrib( p ); if ( p->pTtGia )
if ( fOccurs ) fprintf( pFile, "Memory used for AIG = %8.2f MB.\n", 8.0*Gia_ManAndNum(p->pTtGia)/(1<<20) );
If_DsdManPrintOccurs( stdout, p );
if ( p->timeDsd ) if ( p->timeDsd )
{ {
Abc_PrintTime( 1, "Time DSD ", p->timeDsd ); Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
...@@ -572,6 +638,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, ...@@ -572,6 +638,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
Abc_PrintTime( 1, "Time check2", p->timeCheck2 ); Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
Abc_PrintTime( 1, "Time verify", p->timeVerify ); Abc_PrintTime( 1, "Time verify", p->timeVerify );
} }
if ( fOccurs )
If_DsdManPrintOccurs( stdout, p );
// If_DsdManHashProfile( p ); // If_DsdManHashProfile( p );
if ( fTtDump ) if ( fTtDump )
If_DsdManDumpDsd( p, Support ); If_DsdManDumpDsd( p, Support );
...@@ -618,7 +686,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, ...@@ -618,7 +686,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) int If_DsdObjCompare( If_DsdMan_t * pMan, Vec_Ptr_t * p, int iLit0, int iLit1 )
{ {
If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0)); If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1)); If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
...@@ -635,14 +703,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) ...@@ -635,14 +703,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
return 1; return 1;
if ( If_DsdObjType(p0) == IF_DSD_PRIME ) if ( If_DsdObjType(p0) == IF_DSD_PRIME )
{ {
if ( If_DsdObjTruthId(p0) < If_DsdObjTruthId(p1) ) if ( If_DsdObjTruthId(pMan, p0) < If_DsdObjTruthId(pMan, p1) )
return -1; return -1;
if ( If_DsdObjTruthId(p0) > If_DsdObjTruthId(p1) ) if ( If_DsdObjTruthId(pMan, p0) > If_DsdObjTruthId(pMan, p1) )
return 1; return 1;
} }
for ( i = 0; i < If_DsdObjFaninNum(p0); i++ ) for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
{ {
Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) ); Res = If_DsdObjCompare( pMan, p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
if ( Res != 0 ) if ( Res != 0 )
return Res; return Res;
} }
...@@ -653,14 +721,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) ...@@ -653,14 +721,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
assert( iLit0 == iLit1 ); assert( iLit0 == iLit1 );
return 0; return 0;
} }
void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm ) void If_DsdObjSort( If_DsdMan_t * pMan, Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
{ {
int i, j, best_i; int i, j, best_i;
for ( i = 0; i < nLits-1; i++ ) for ( i = 0; i < nLits-1; i++ )
{ {
best_i = i; best_i = i;
for ( j = i+1; j < nLits; j++ ) for ( j = i+1; j < nLits; j++ )
if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 ) if ( If_DsdObjCompare(pMan, p, pLits[best_i], pLits[j]) == 1 )
best_i = j; best_i = j;
if ( i == best_i ) if ( i == best_i )
continue; continue;
...@@ -704,7 +772,7 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit ...@@ -704,7 +772,7 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit
if ( If_DsdObjType(pObj) == Type && if ( If_DsdObjType(pObj) == Type &&
If_DsdObjFaninNum(pObj) == nLits && If_DsdObjFaninNum(pObj) == nLits &&
!memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) && !memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) &&
truthId == If_DsdObjTruthId(pObj) ) truthId == If_DsdObjTruthId(p, pObj) )
{ {
p->nUniqueHits++; p->nUniqueHits++;
return pSpot; return pSpot;
...@@ -724,7 +792,7 @@ static void If_DsdObjHashResize( If_DsdMan_t * p ) ...@@ -724,7 +792,7 @@ static void If_DsdObjHashResize( If_DsdMan_t * p )
Vec_IntFill( p->vNexts, Vec_PtrSize(p->vObjs), 0 ); Vec_IntFill( p->vNexts, Vec_PtrSize(p->vObjs), 0 );
If_DsdVecForEachNode( p->vObjs, pObj, i ) If_DsdVecForEachNode( p->vObjs, pObj, i )
{ {
pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) ); pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
assert( *pSpot == 0 ); assert( *pSpot == 0 );
*pSpot = pObj->Id; *pSpot = pObj->Id;
} }
...@@ -748,7 +816,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut ...@@ -748,7 +816,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) ); pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) );
assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND ); assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR ); assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 ); assert( iPrev == -1 || If_DsdObjCompare(p, p->vObjs, iPrev, pLits[i]) <= 0 );
iPrev = pLits[i]; iPrev = pLits[i];
} }
} }
...@@ -775,20 +843,26 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut ...@@ -775,20 +843,26 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
} }
int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth ) int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
{ {
int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1; int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId ); unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
abctime clk; abctime clk;
if ( *pSpot ) if ( *pSpot )
return (int)*pSpot; return (int)*pSpot;
clk = Abc_Clock(); clk = Abc_Clock();
if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) ) if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
{ {
Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched ); Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
// printf( "%d ", Vec_IntSize(vSets) ); assert( truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 );
assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 ); Vec_PtrPush( p->vTtDecs[nLits], vSets );
Vec_PtrPush( p->vTtDecs, vSets );
// Dau_DecPrintSets( vSets, nLits ); // Dau_DecPrintSets( vSets, nLits );
} }
if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 )
{
int nObjOld = Gia_ManAndNum(p->pTtGia);
int Lit = Kit_TruthToGia( p->pTtGia, (unsigned *)pTruth, nLits, p->vCover, NULL, 1 );
// printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
Gia_ManAppendCo( p->pTtGia, Lit );
}
p->timeCheck += Abc_Clock() - clk; p->timeCheck += Abc_Clock() - clk;
*pSpot = Vec_PtrSize( p->vObjs ); *pSpot = Vec_PtrSize( p->vObjs );
objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId ); objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
...@@ -815,7 +889,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) ...@@ -815,7 +889,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
Vec_Int_t * vSets; Vec_Int_t * vSets;
char * pBuffer = "dsd0"; char * pBuffer = "dsd0";
word * pTruth; word * pTruth;
int i, Num; int i, v, Num;
FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" ); FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
if ( pFile == NULL ) if ( pFile == NULL )
{ {
...@@ -831,22 +905,28 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) ...@@ -831,22 +905,28 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
Vec_PtrForEachEntryStart( If_DsdObj_t *, p->vObjs, pObj, i, 2 ) Vec_PtrForEachEntryStart( If_DsdObj_t *, p->vObjs, pObj, i, 2 )
{ {
Num = If_DsdObjWordNum( pObj->nFans + (int)(pObj->Type == DAU_DSD_PRIME) ); Num = If_DsdObjWordNum( pObj->nFans );
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
fwrite( pObj, sizeof(word)*Num, 1, pFile ); fwrite( pObj, sizeof(word)*Num, 1, pFile );
if ( pObj->Type == IF_DSD_PRIME )
fwrite( Vec_IntEntryP(p->vTruths, i), 4, 1, pFile );
} }
Num = Vec_MemEntryNum(p->vTtMem); for ( v = 3; v <= p->nVars; v++ )
{
int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
Num = Vec_MemEntryNum(p->vTtMem[v]);
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
Vec_MemForEachEntry( p->vTtMem, pTruth, i ) Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile ); fwrite( pTruth, nBytes, 1, pFile );
Num = Vec_PtrSize(p->vTtDecs); Num = Vec_PtrSize(p->vTtDecs[v]);
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i ) Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vSets, i )
{ {
Num = Vec_IntSize(vSets); Num = Vec_IntSize(vSets);
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
} }
}
fclose( pFile ); fclose( pFile );
} }
If_DsdMan_t * If_DsdManLoad( char * pFileName ) If_DsdMan_t * If_DsdManLoad( char * pFileName )
...@@ -857,7 +937,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) ...@@ -857,7 +937,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
char pBuffer[10]; char pBuffer[10];
unsigned * pSpot; unsigned * pSpot;
word * pTruth; word * pTruth;
int i, Num, Num2, RetValue; int i, v, Num, Num2, RetValue;
FILE * pFile = fopen( pFileName, "rb" ); FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL ) if ( pFile == NULL )
{ {
...@@ -881,6 +961,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) ...@@ -881,6 +961,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
assert( Num >= 2 ); assert( Num >= 2 );
Vec_PtrFillExtra( p->vObjs, Num, NULL ); Vec_PtrFillExtra( p->vObjs, Num, NULL );
Vec_IntFill( p->vNexts, Num, 0 ); Vec_IntFill( p->vNexts, Num, 0 );
Vec_IntFill( p->vTruths, Num, -1 );
p->nBins = Abc_PrimeCudd( 2*Num ); p->nBins = Abc_PrimeCudd( 2*Num );
p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins ); p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
memset( p->pBins, 0, sizeof(unsigned) * p->nBins ); memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
...@@ -890,21 +971,28 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) ...@@ -890,21 +971,28 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num ); pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
RetValue = fread( pObj, sizeof(word)*Num, 1, pFile ); RetValue = fread( pObj, sizeof(word)*Num, 1, pFile );
Vec_PtrWriteEntry( p->vObjs, i, pObj ); Vec_PtrWriteEntry( p->vObjs, i, pObj );
pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) ); if ( pObj->Type == IF_DSD_PRIME )
{
RetValue = fread( &Num, 4, 1, pFile );
Vec_IntWriteEntry( p->vTruths, i, Num );
}
pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
assert( *pSpot == 0 ); assert( *pSpot == 0 );
*pSpot = pObj->Id; *pSpot = pObj->Id;
} }
assert( p->nUniqueMisses == Vec_PtrSize(p->vObjs) - 2 ); assert( p->nUniqueMisses == Vec_PtrSize(p->vObjs) - 2 );
p->nUniqueMisses = 0; p->nUniqueMisses = 0;
RetValue = fread( &Num, 4, 1, pFile );
pTruth = ABC_ALLOC( word, p->nWords ); pTruth = ABC_ALLOC( word, p->nWords );
for ( v = 3; v <= p->nVars; v++ )
{
int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
RetValue = fread( &Num, 4, 1, pFile );
for ( i = 0; i < Num; i++ ) for ( i = 0; i < Num; i++ )
{ {
RetValue = fread( pTruth, sizeof(word)*p->nWords, 1, pFile ); RetValue = fread( pTruth, nBytes, 1, pFile );
Vec_MemHashInsert( p->vTtMem, pTruth ); Vec_MemHashInsert( p->vTtMem[v], pTruth );
} }
ABC_FREE( pTruth ); assert( Num == Vec_MemEntryNum(p->vTtMem[v]) );
assert( Num == Vec_MemEntryNum(p->vTtMem) );
RetValue = fread( &Num2, 4, 1, pFile ); RetValue = fread( &Num2, 4, 1, pFile );
for ( i = 0; i < Num2; i++ ) for ( i = 0; i < Num2; i++ )
{ {
...@@ -912,9 +1000,11 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) ...@@ -912,9 +1000,11 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
vSets = Vec_IntAlloc( Num ); vSets = Vec_IntAlloc( Num );
RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
vSets->nSize = Num; vSets->nSize = Num;
Vec_PtrPush( p->vTtDecs, vSets ); Vec_PtrPush( p->vTtDecs[v], vSets );
}
assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) );
} }
assert( Num2 == Vec_PtrSize(p->vTtDecs) ); ABC_FREE( pTruth );
fclose( pFile ); fclose( pFile );
return p; return p;
} }
...@@ -1203,7 +1293,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig ...@@ -1203,7 +1293,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
} }
pPermStart += If_DsdObjSuppSize(pObj); pPermStart += If_DsdObjSuppSize(pObj);
} }
If_DsdObjSort( p->vObjs, pChildren, nChildren, pBegEnd ); If_DsdObjSort( p, p->vObjs, pChildren, nChildren, pBegEnd );
// create permutation // create permutation
for ( j = i = 0; i < nChildren; i++ ) for ( j = i = 0; i < nChildren; i++ )
for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ ) for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
...@@ -1222,7 +1312,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig ...@@ -1222,7 +1312,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) ); pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
pPermStart += pFanin->nSupp; pPermStart += pFanin->nSupp;
} }
RetValue = If_DsdObjCompare( p->vObjs, pLits[1], pLits[2] ); RetValue = If_DsdObjCompare( p, p->vObjs, pLits[1], pLits[2] );
if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) ) if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) )
{ {
int nSupp0 = If_DsdVecLitSuppSize( p->vObjs, pLits[0] ); int nSupp0 = If_DsdVecLitSuppSize( p->vObjs, pLits[0] );
...@@ -1513,9 +1603,9 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int ...@@ -1513,9 +1603,9 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int
unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{ {
int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
int truthId = If_DsdObjTruthId(pObj); int truthId = If_DsdObjTruthId(p, pObj);
int nFans = If_DsdObjFaninNum(pObj); int nFans = If_DsdObjFaninNum(pObj);
Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId); Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs[pObj->nFans], truthId);
if ( fVerbose ) if ( fVerbose )
printf( "\n" ); printf( "\n" );
if ( fVerbose ) if ( fVerbose )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment