Skip to content

A
abc
Commit ee727912 by Alan Mishchenko
Options

Improvements to Boolean matching.

parent 69699da9
Showing with 30 additions and 14 deletions
abcexe.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -67,7 +67,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe
......
abclib.dsp
......@@ -41,7 +41,7 @@ RSC=rc.exe
# PROP Intermediate_Dir "ReleaseLib"
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -64,7 +64,7 @@ LIB32=link.exe -lib
# PROP Intermediate_Dir "DebugLib"
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe
......
src/base/abci/abc.c
......@@ -15409,9 +15409,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "DSD manager is not available.\n" );
return 1;
}
if ( pPars->nLutSize > If_DsdManLutSize(pDsdMan) )
if ( pPars->nLutSize > If_DsdManVarNum(pDsdMan) )
{
Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManLutSize(pDsdMan) );
Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManVarNum(pDsdMan) );
return 1;
}
pPars->fCutMin = 1;
......@@ -31280,9 +31280,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "DSD manager is not available.\n" );
return 1;
}
if ( pPars->nLutSize > If_DsdManLutSize(pDsdMan) )
if ( pPars->nLutSize > If_DsdManVarNum(pDsdMan) )
{
Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManLutSize(pDsdMan) );
Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManVarNum(pDsdMan) );
return 1;
}
pPars->fCutMin = 1;
src/map/if/ifDsd.c
......@@ -89,6 +89,7 @@ struct If_DsdMan_t_
Gia_Man_t * pTtGia; // GIA to represent truth tables
Vec_Int_t * vCover; // temporary memory
void * pSat; // SAT solver
int nObjsPrev; // previous number of objects
int fNewAsUseless; // set new as useless
int nUniqueHits; // statistics
int nUniqueMisses; // statistics
......@@ -127,13 +128,15 @@ static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj )
#define If_DsdVecForEachObj( vVec, pObj, i ) \
Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \
#define If_DsdVecForEachObjStart( vVec, pObj, i, Start ) \
Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, Start )
#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ )
#define If_DsdVecForEachNode( vVec, pObj, i ) \
Vec_PtrForEachEntryStart( If_DsdObj_t *, vVec, pObj, i, 2 )
#define If_DsdObjForEachFanin( vVec, pObj, pFanin, i ) \
for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((pFanin) = If_DsdObjFanin(vVec, pObj, i)); i++ )
#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++ )
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
......@@ -183,6 +186,7 @@ int If_DsdManReadMark( If_DsdMan_t * p, int iDsd )
}
void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
{
p->nObjsPrev = If_DsdManObjNum(p);
p->fNewAsUseless = 1;
}
......@@ -2379,6 +2383,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
abctime clk = Abc_Clock();
// parse the structure
Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct );
if ( pNtk == NULL )
return;
if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
{
printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
......@@ -2395,11 +2401,14 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
Ifn_NtkPrint( pNtk );
printf( "Largest LUT size = %d.\n", LutSize );
}
if ( p->nObjsPrev > 0 )
printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
// clean the attributes
If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = 0;
if ( i >= p->nObjsPrev )
pObj->fMark = 0;
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
If_DsdVecForEachObj( &p->vObjs, pObj, i )
If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
nVars = If_DsdObjSuppSize(pObj);
......@@ -2416,6 +2425,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
if ( Value == 0 )
If_DsdVecObjSetMark( &p->vObjs, i );
}
p->nObjsPrev = 0;
Extra_ProgressBarStop( pProgress );
printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
......@@ -2519,9 +2529,12 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
printf( "Largest LUT size = %d.\n", LutSize );
}
ABC_FREE( pNtk );
if ( p->nObjsPrev > 0 )
printf( "Starting the tuning process from object %d (out of %d).\n", p->nObjsPrev, Vec_PtrSize(&p->vObjs) );
// clean the attributes
If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = 0;
if ( i >= p->nObjsPrev )
pObj->fMark = 0;
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
// perform concurrent solving
......@@ -2529,7 +2542,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
pthread_t WorkerThread[PAR_THR_MAX];
Ifn_ThData_t ThData[PAR_THR_MAX];
abctime clk, clkUsed = 0;
int status, fRunning = 1, iCurrentObj = 0;
int status, fRunning = 1, iCurrentObj = p->nObjsPrev;
// start the threads
for ( i = 0; i < nProcs; i++ )
{
......@@ -2605,6 +2618,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
}
}
p->nObjsPrev = 0;
Extra_ProgressBarStop( pProgress );
printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
......
src/map/if/ifTune.c
......@@ -807,6 +807,8 @@ void Ifn_NtkRead()
// char * pStr = "g=<abc>;h=<ade>;i={fgh};";
char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
if ( p == NULL )
return;
Ifn_NtkPrint( p );
Dau_DsdPrintFromTruth( pTruth, nVars );
// get the given function
......
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