luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding conflict limit and timeout to &simap.

This commit is contained in:
Alan Mishchenko 2025-03-10 17:54:30 -07:00
parent 40ea8a7598
commit 2c45f9dce2
2 changed files with 48 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/aig/gia/giaSatLut.c
View File

@ -1233,7 +1233,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut, int fVerbose )
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose )
{
extern Vec_Int_t * Exa4_ManParse( char *pFileName );
int fVerboseSolver = 0;
@ -1245,10 +1245,18 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut
char * pKadical = "kadical";
#endif
char Command[1000], * pCommand = (char *)&Command;
if ( TimeOut )
sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else
sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
if ( nBTLimit ) {
if ( TimeOut )
sprintf( pCommand, "%s -c %d -t %d %s %s > %s", pKadical, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else
sprintf( pCommand, "%s -c %d %s %s > %s", pKadical, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
}
else {
if ( TimeOut )
sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else
sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
}
#ifdef __wasm
if ( 1 )
#else
@ -1266,7 +1274,7 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut
else if ( vRes == NULL && TimeOut == 0 )
printf( "The problem has no solution. " );
else if ( vRes == NULL )
printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut );
Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
}
return vRes;
@ -1527,7 +1535,7 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
fclose( pFile );
return 1;
}
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose )
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose )
{
char * pFileNameI = (char *)"__temp__.cnf";
char * pFileNameO = (char *)"__temp__.out";
@ -1540,11 +1548,12 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose
return 0;
}
if ( fVerbose )
printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d.\n", nVars, Vec_StrCountEntry(vStr, '\n'), nBound );
printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n",
nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout );
//char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 );
//Gia_ManDumpCnf( pFileName, vStr, nVars );
Vec_StrFree( vStr );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, 0, 1 );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 );
unlink( pFileNameI );
//unlink( pFileNameO );
if ( vRes == NULL )

50
src/base/abci/abc.c
View File

@ -44383,27 +44383,13 @@ usage:
int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Mio_IntallSimpleLibrary();
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose );
int c, nBTLimit = 0, nBound = 0, fVerbose = 0;
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose );
int c, nBTLimit = 0, nBound = 0, nTimeout = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CBvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "BCTvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBTLimit < 0 )
{
Abc_Print( -1, "Conflict limit should be a positive integer.\n" );
goto usage;
}
break;
case 'B':
if ( globalUtilOptind >= argc )
{
@ -44418,6 +44404,29 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBTLimit < 0 )
{
Abc_Print( -1, "Conflict limit should be a positive integer.\n" );
goto usage;
}
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
goto usage;
}
nTimeout = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'v':
fVerbose ^= 1;
break;
@ -44432,15 +44441,16 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Mio_IntallSimpleLibrary();
if ( !Gia_ManSimpleMapping( pAbc->pGia, nBTLimit, nBound, fVerbose ) )
if ( !Gia_ManSimpleMapping( pAbc->pGia, nBound, nBTLimit, nTimeout, fVerbose ) )
printf( "Simple mapping has failed.\n" );
return 0;
usage:
Abc_Print( -2, "usage: &simap [-CB num] [-vh]\n" );
Abc_Print( -2, "usage: &simap [-BCT num] [-vh]\n" );
Abc_Print( -2, "\t performs simple mapping of the AIG\n" );
Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-B num : the bound on the solution size [default = %d]\n", nBound );
Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-T num : runtime limit in seconds [default = %d]\n", nTimeout );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
return 1;