summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c30
-rw-r--r--src/map/if/if.h3
-rw-r--r--src/map/if/ifDsd.c48
3 files changed, 53 insertions, 28 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e2913543..5666f56e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15535,9 +15535,9 @@ usage:
***********************************************************************/
int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c, Number = 0, fOccurs = 0, fVerbose = 0;
+ int c, Number = 0, Support = 0, fOccurs = 0, fTtDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Novh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NSotvh" ) ) != EOF )
{
switch ( c )
{
@@ -15552,9 +15552,23 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Number < 0 )
goto usage;
break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ Support = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Support < 0 )
+ goto usage;
+ break;
case 'o':
fOccurs ^= 1;
break;
+ case 't':
+ fTtDump ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -15569,15 +15583,17 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The DSD manager is not started.\n" );
return 0;
}
- If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, Number, fOccurs, fVerbose );
+ If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, Number, Support, fOccurs, fTtDump, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: dsd_ps [-N num] [-ovh]\n" );
+ Abc_Print( -2, "usage: dsd_ps [-NS num] [-ovh]\n" );
Abc_Print( -2, "\t prints statistics of DSD manager\n" );
- Abc_Print( -2, "\t-N num : show structures whose ID divides by N [default = %d]\n", Number );
+ Abc_Print( -2, "\t-N num : show structures whose ID divides by N [default = %d]\n", Number );
+ Abc_Print( -2, "\t-S num : show structures whose support size is S [default = %d]\n", Support );
Abc_Print( -2, "\t-o : toggles printing occurence distribution [default = %s]\n", fOccurs? "yes": "no" );
- Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-t : toggles dumping truth tables [default = %s]\n", fTtDump? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -15715,7 +15731,7 @@ int Abc_CommandDsdMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: dsd_merge [-h] <file>\n" );
- Abc_Print( -2, "\t mermges DSD manager from file with the current one\n");
+ Abc_Print( -2, "\t merges DSD manager from file with the current one\n");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : file name to read\n");
return 1;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index c422505b..52847e2d 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -518,8 +518,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int
char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
/*=== ifDsd.c =============================================================*/
extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize );
-extern void If_DsdManDump( If_DsdMan_t * p );
-extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int fOccurs, int fVerbose );
+extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose );
extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index e50a3743..a42187fa 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -219,9 +219,9 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
{
int v;
-// If_DsdManDump( p );
+// If_DsdManDumpDsd( p );
if ( fVerbose )
- If_DsdManPrint( p, NULL, 0, 0, 0 );
+ If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 );
if ( fVerbose )
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
for ( v = 2; v < p->nVars; v++ )
@@ -239,39 +239,43 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
ABC_FREE( p->pBins );
ABC_FREE( p );
}
-void If_DsdManDump( If_DsdMan_t * p )
+void If_DsdManDumpDsd( If_DsdMan_t * p, int Support )
{
- char * pFileName = "nondsd_tts.txt";
- FILE * pFile;
- If_DsdObj_t * pObj;
- int i;
- pFile = fopen( pFileName, "wb" );
+ char * pFileName = "tts_nondsd.txt";
+ If_DsdObj_t * pObj; int i;
+ Vec_Int_t * vMap;
+ FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\".\n", pFileName );
return;
}
+ vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) );
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
+ if ( Support && Support != If_DsdObjSuppSize(pObj) )
+ continue;
if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
continue;
+ if ( Vec_IntEntry(vMap, If_DsdObjTruthId(pObj)) )
+ continue;
+ Vec_IntWriteEntry(vMap, If_DsdObjTruthId(pObj), 1);
fprintf( pFile, "0x" );
- Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars );
+ Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : p->nVars );
fprintf( pFile, "\n" );
// printf( " " );
// Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
}
+ Vec_IntFree( vMap );
fclose( pFile );
}
-void If_DsdManDumpAll( If_DsdMan_t * p )
+void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
{
extern word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits );
- char * pFileName = "dsd_tts.txt";
- FILE * pFile;
+ char * pFileName = "tts_all.txt";
If_DsdObj_t * pObj;
- word * pRes;
- int i;
- pFile = fopen( pFileName, "wb" );
+ word * pRes; int i;
+ FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\".\n", pFileName );
@@ -279,9 +283,11 @@ void If_DsdManDumpAll( If_DsdMan_t * p )
}
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
+ if ( Support && Support != If_DsdObjSuppSize(pObj) )
+ continue;
pRes = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
fprintf( pFile, "0x" );
- Abc_TtPrintHexRev( pFile, pRes, p->nVars );
+ Abc_TtPrintHexRev( pFile, pRes, Support ? Abc_MaxInt(Support, 6) : p->nVars );
fprintf( pFile, "\n" );
// printf( " " );
// Dau_DsdPrintFromTruth( pRes, p->nVars );
@@ -455,7 +461,7 @@ void If_DsdManPrintDistrib( If_DsdMan_t * p )
printf( "(%6.2f %%)", 100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) );
printf( "\n" );
}
-void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int fOccurs, 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;
int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0;
@@ -497,14 +503,18 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int fOccurs,
Abc_PrintTime( 1, "Time verify", p->timeVerify );
}
// If_DsdManHashProfile( p );
-// If_DsdManDump( p );
-// If_DsdManDumpAll( p );
+ if ( fTtDump )
+ If_DsdManDumpDsd( p, Support );
+ if ( fTtDump )
+ If_DsdManDumpAll( p, Support );
if ( !fVerbose )
return;
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
if ( Number && i % Number )
continue;
+ if ( Support && Support != If_DsdObjSuppSize(pObj) )
+ continue;
If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
}
fprintf( pFile, "\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-22 16:34:23 +0000