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

Autotuner for 'satoko'.

This commit is contained in:
Alan Mishchenko 2017-02-08 18:57:16 -08:00
parent cf24a0eb0c
commit 77e2b1ff53
7 changed files with 702 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -523,6 +523,10 @@ SOURCE=.\src\base\cmd\cmdApi.c
# End Source File
# Begin Source File
SOURCE=.\src\base\cmd\cmdAuto.c
# End Source File
# Begin Source File
SOURCE=.\src\base\cmd\cmdFlag.c
# End Source File
# Begin Source File

8
src/aig/gia/giaSatoko.c
View File

@ -21,6 +21,7 @@
#include "gia.h"
#include "sat/cnf/cnf.h"
#include "sat/satoko/satoko.h"
#include "sat/satoko/solver.h"
ABC_NAMESPACE_IMPL_START
@ -68,17 +69,19 @@ satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
satoko_destroy( pSat );
return NULL;
}
void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
{
abctime clk = Abc_Clock();
satoko_t * pSat;
int status;
int status, Cost = 0;
pSat = Gia_ManCreateSatoko( p );
if ( pSat )
{
satoko_configure(pSat, opts);
status = satoko_solve( pSat );
Cost = (unsigned)pSat->stats.n_conflicts;
satoko_destroy( pSat );
}
else
@ -97,6 +100,7 @@ void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
Abc_Print( 1, "UNSATISFIABLE " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Cost;
}
void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
{

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

@ -16782,7 +16782,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
If_ManSetDefaultPars( pPars );
pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyuojiktncvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "K:CFAGRNTXYDEWSqaflepmrsdbgxyuojiktncvh" ) ) != EOF )
{
switch ( c )
{
@ -38135,9 +38135,9 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
Vec_Int_t * vPos;
int c, iOutNum = -1, nOutRange = 1, iPartNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fVerbose = 0;
int c, iOutNum = -1, nOutRange = 1, iPartNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fExtractAll = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWaevh" ) ) != EOF )
{
switch ( c )
{
@ -38199,6 +38199,9 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
fUseAllCis ^= 1;
break;
case 'e':
fExtractAll ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -38213,6 +38216,21 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Cone(): There is no AIG.\n" );
return 1;
}
if ( fExtractAll )
{
char Buffer[1000];
Gia_Obj_t * pObj;
int i, nDigits = Abc_Base10Log(Gia_ManPoNum(pAbc->pGia));
Gia_ManForEachPo( pAbc->pGia, pObj, i )
{
Gia_Man_t * pOne = Gia_ManDupDfsCone( pAbc->pGia, pObj );
sprintf( Buffer, "%s_%0*d.aig", Extra_FileNameGeneric(pAbc->pGia->pSpec), nDigits, i );
Gia_AigerWrite( pOne, Buffer, 0, 0 );
Gia_ManStop( pOne );
}
printf( "Dumped all outputs into individual AIGER files.\n" );
return 0;
}
if ( nLevelMax || nTimeWindow )
{
if ( nLevelMax && nTimeWindow )
@ -38260,7 +38278,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &cone [-ORPLW num] [-avh]\n" );
Abc_Print( -2, "usage: &cone [-ORPLW num] [-aevh]\n" );
Abc_Print( -2, "\t extracting multi-output sequential logic cones\n" );
Abc_Print( -2, "\t-O num : the index of first PO to extract [default = %d]\n", iOutNum );
Abc_Print( -2, "\t-R num : (optional) the number of outputs to extract [default = %d]\n", nOutRange );
@ -38268,6 +38286,7 @@ usage:
Abc_Print( -2, "\t-L num : (optional) extract cones with higher level [default = %d]\n", nLevelMax );
Abc_Print( -2, "\t-W num : (optional) extract cones falling into this window [default = %d]\n", nTimeWindow );
Abc_Print( -2, "\t-a : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
Abc_Print( -2, "\t-e : toggle writing all outputs into individual files [default = %s]\n", fExtractAll? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

114
src/base/cmd/cmd.c
View File

@ -60,6 +60,7 @@ static int CmdCommandSis ( Abc_Frame_t * pAbc, int argc, char ** argv
static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv );
extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -110,6 +111,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "mvsis", CmdCommandMvsis, 1 );
Cmd_CommandAdd( pAbc, "Various", "capo", CmdCommandCapo, 0 );
Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 );
Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 );
Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 );
}
@ -2457,6 +2459,118 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int CmdCommandAutoTuner( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Cmd_RunAutoTuner( char * pConfig, char * pFileList, int nCores );
FILE * pFile;
char * pFileConf = NULL;
char * pFileList = NULL;
char * pFileName;
int c, nCores = 3;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NCFvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nCores = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCores < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by a string (possibly in quotes).\n" );
goto usage;
}
pFileConf = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by a string (possibly in quotes).\n" );
goto usage;
}
pFileList = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pFileConf == NULL )
{
Abc_Print( -2, "File containing configuration for autotuning is not given.\n" );
return 1;
}
if ( pFileList == NULL )
{
Abc_Print( -2, "File contining list of files for autotuning is not given.\n" );
return 1;
}
// get the input file name
pFileName = pFileConf;
if ( (pFile = Io_FileOpen( pFileName, "open_path", "rb", 0 )) == NULL )
// if ( (pFile = fopen( pFileName, "rb" )) == NULL )
{
Abc_Print( -2, "Cannot open configuration file \"%s\". ", pFileName );
if (( pFileName = Extra_FileGetSimilarName( pFileName, ".c", ".s", ".scr", ".script", NULL ) ))
Abc_Print( -2, "Did you mean \"%s\"?", pFileName );
Abc_Print( -2, "\n" );
return 1;
}
fclose( pFile );
// get the input file name
pFileName = pFileList;
if ( (pFile = Io_FileOpen( pFileName, "open_path", "rb", 0 )) == NULL )
// if ( (pFile = fopen( pFileName, "rb" )) == NULL )
{
Abc_Print( -2, "Cannot open the file list \"%s\". ", pFileName );
if (( pFileName = Extra_FileGetSimilarName( pFileName, ".c", ".s", ".scr", ".script", NULL ) ))
Abc_Print( -2, "Did you mean \"%s\"?", pFileName );
Abc_Print( -2, "\n" );
return 1;
}
fclose( pFile );
// run commands
Cmd_RunAutoTuner( pFileConf, pFileList, nCores );
return 0;
usage:
Abc_Print( -2, "usage: autotuner [-N num] [-C file] [-F file] [-vh]\n" );
Abc_Print( -2, "\t runs command lines listed in <file> concurrently on <num> CPUs\n" );
Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controler [default = %d]\n", nCores );
Abc_Print( -2, "\t-C cmd : configuration file for autotuning\n" );
Abc_Print( -2, "\t-F cmd : list of files to be used for autotuning\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis [Print the version string.]

522
src/base/cmd/cmdAuto.c Normal file
View File

@ -0,0 +1,522 @@
/**CFile****************************************************************
FileName [cmdAuto.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Autotuner.]
Author [Alan Mishchenko, Bruno Schmitt]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cmdAuto.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/util/abc_global.h"
#include "misc/extra/extra.h"
#include "aig/gia/gia.h"
#include "sat/satoko/satoko.h"
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define CMD_AUTO_LINE_MAX 1000 // max number of chars in the string
#define CMD_AUTO_ARG_MAX 100 // max number of arguments in the call
extern int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Printing option structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cmd_RunAutoTunerPrintOptions( satoko_opts_t * pOpts )
{
printf( "-C %d ", pOpts->conf_limit );
printf( "-V %.3f ", pOpts->var_decay );
printf( "-W %.3f ", pOpts->clause_decay );
if ( pOpts->verbose )
printf( "-v", pOpts->verbose );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [The main evaluation procedure for an array of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cmd_RunAutoTunerEvalSimple( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts )
{
Gia_Man_t * pGia;
int i, TotalCost = 0;
//printf( "Tuning with options: " );
//Cmd_RunAutoTunerPrintOptions( pOpts );
Vec_PtrForEachEntry( Gia_Man_t *, vAigs, pGia, i )
TotalCost += Gia_ManCallSatokoOne( pGia, pOpts, -1 );
return TotalCost;
}
/**Function*************************************************************
Synopsis [The main evaluation procedure for the set of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
int Cmd_RunAutoTunerEval( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts, int nCores )
{
return Cmd_RunAutoTunerEvalSimple( vAigs, pOpts );
}
#else // pthreads are used
#define CMD_THR_MAX 100
typedef struct Cmd_AutoData_t_
{
Gia_Man_t * pGia;
satoko_opts_t * pOpts;
int iThread;
int nTimeOut;
int fWorking;
int Result;
} Cmd_AutoData_t;
void * Cmd_RunAutoTunerEvalWorkerThread( void * pArg )
{
Cmd_AutoData_t * pThData = (Cmd_AutoData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->pGia == NULL ) // kills itself when there is nothing to do
{
pthread_exit( NULL );
assert( 0 );
return NULL;
}
pThData->Result = Gia_ManCallSatokoOne( pThData->pGia, pThData->pOpts, -1 );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
int Cmd_RunAutoTunerEval( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts, int nProcs )
{
abctime clkTotal = Abc_Clock();
Cmd_AutoData_t ThData[CMD_THR_MAX];
pthread_t WorkerThread[CMD_THR_MAX];
int i, status, fWorkToDo = 1, TotalCost = 0;
Vec_Ptr_t * vStack;
if ( nProcs == 1 )
return Cmd_RunAutoTunerEvalSimple( vAigs, pOpts );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= CMD_THR_MAX );
// start threads
for ( i = 0; i < nProcs; i++ )
{
ThData[i].pGia = NULL;
ThData[i].pOpts = pOpts;
ThData[i].iThread = i;
ThData[i].nTimeOut = -1;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
status = pthread_create( WorkerThread + i, NULL,Cmd_RunAutoTunerEvalWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
vStack = Vec_PtrDup(vAigs);
while ( fWorkToDo )
{
fWorkToDo = (int)(Vec_PtrSize(vStack) > 0);
for ( i = 0; i < nProcs; i++ )
{
// check if this thread is working
if ( ThData[i].fWorking )
{
fWorkToDo = 1;
continue;
}
// check if this thread has recently finished
if ( ThData[i].pGia != NULL )
{
assert( ThData[i].Result >= 0 );
TotalCost += ThData[i].Result;
ThData[i].pGia = NULL;
}
if ( Vec_PtrSize(vStack) == 0 )
continue;
// give this thread a new job
assert( ThData[i].pGia == NULL );
ThData[i].pGia = (Gia_Man_t *)Vec_PtrPop( vStack );
ThData[i].fWorking = 1;
}
}
Vec_PtrFree( vStack );
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// stop
ThData[i].pGia = NULL;
ThData[i].fWorking = 1;
}
return TotalCost;
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis [Derives all possible param stucts according to the config file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Cmd_DeriveConvertIntoString( int argc, char ** argv )
{
char pBuffer[CMD_AUTO_LINE_MAX] = {0};
int i;
for ( i = 0; i < argc; i++ )
{
strcat( pBuffer, argv[i] );
strcat( pBuffer, " " );
}
return Abc_UtilStrsav(pBuffer);
}
satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv )
{
int c;
satoko_opts_t opts, * pOpts;
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CVWhv" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
return NULL;
}
opts.conf_limit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.conf_limit < 0 )
return NULL;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
return NULL;
}
opts.var_decay = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.var_decay < 0 )
return NULL;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
return NULL;
}
opts.clause_decay = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.clause_decay < 0 )
return NULL;
break;
case 'v':
opts.verbose ^= 1;
break;
default:
return NULL;
}
}
// return a copy of this parameter structure
pOpts = ABC_ALLOC( satoko_opts_t, 1 );
memcpy( pOpts, &opts, sizeof(satoko_opts_t) );
return pOpts;
}
void Cmf_CreateOptions_rec( Vec_Wec_t * vPars, int iPar, char Argv[CMD_AUTO_ARG_MAX][20], int Argc, Vec_Ptr_t * vOpts )
{
Vec_Int_t * vLine;
int Symb, Num, i;
assert( Argc <= CMD_AUTO_ARG_MAX );
if ( Vec_WecSize(vPars) == iPar )
{
satoko_opts_t * pOpts;
char * pArgv[CMD_AUTO_ARG_MAX];
for ( i = 0; i < Argc; i++ )
pArgv[i] = Argv[i];
pOpts = Cmd_DeriveOptionFromSettings( Argc, pArgv );
if ( pOpts == NULL )
printf( "Cannot parse command line options...\n" );
else
{
Vec_PtrPush( vOpts, pOpts );
Vec_PtrPush( vOpts, Cmd_DeriveConvertIntoString(Argc, pArgv) );
printf( "Adding settings %s\n", (char *)Vec_PtrEntryLast(vOpts) );
}
return;
}
vLine = Vec_WecEntry( vPars, iPar );
// consider binary option
if ( Vec_IntSize(vLine) == 2 )
{
Symb = Vec_IntEntry( vLine, 0 );
Num = Vec_IntEntry( vLine, 1 );
assert( Abc_Int2Float(Num) == -1.0 );
// create one setting without this option
Cmf_CreateOptions_rec( vPars, iPar+1, Argv, Argc, vOpts );
// create another setting with this option
sprintf( Argv[Argc], "-%c", Symb );
Cmf_CreateOptions_rec( vPars, iPar+1, Argv, Argc+1, vOpts );
return;
}
// consider numeric option
Vec_IntForEachEntryDouble( vLine, Symb, Num, i )
{
float NumF = Abc_Int2Float(Num);
// create setting with this option
assert( NumF >= 0 );
sprintf( Argv[Argc], "-%c", Symb );
if ( NumF == (float)(int)NumF )
sprintf( Argv[Argc+1], "%d", (int)NumF );
else
sprintf( Argv[Argc+1], "%.3f", NumF );
Cmf_CreateOptions_rec( vPars, iPar+1, Argv, Argc+2, vOpts );
}
}
Vec_Ptr_t * Cmf_CreateOptions( Vec_Wec_t * vPars )
{
char Argv[CMD_AUTO_ARG_MAX][20];
int Symb, Num, i, Argc = 0;
Vec_Ptr_t * vOpts = Vec_PtrAlloc( 100 );
Vec_Int_t * vLine = Vec_WecEntry( vPars, 0 );
printf( "Creating all possible settings to be used by the autotuner:\n" );
sprintf( Argv[Argc++], "autotuner" );
Vec_IntForEachEntryDouble( vLine, Symb, Num, i )
{
float NumF = Abc_Int2Float(Num);
sprintf( Argv[Argc++], "-%c", Symb );
if ( NumF < 0.0 )
continue;
if ( NumF == (float)(int)NumF )
sprintf( Argv[Argc++], "%d", (int)NumF );
else
sprintf( Argv[Argc++], "%.3f", NumF );
}
Cmf_CreateOptions_rec( vPars, 1, Argv, Argc, vOpts );
printf( "Finished creating %d settings.\n\n", Vec_PtrSize(vOpts)/2 );
return vOpts;
}
/**Function*************************************************************
Synopsis [Parses config file and derives AIGs listed in file list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cmf_IsSpace( char p ) { return p == ' ' || p == '\t' || p == '\n' || p == '\r'; }
static inline Cmf_IsLowerCaseChar( char p ) { return p >= 'a' && p <= 'z'; }
static inline Cmf_IsUpperCaseChar( char p ) { return p >= 'A' && p <= 'Z'; }
static inline Cmf_IsDigit( char p ) { return (p >= '0' && p <= '9') || p == '.'; }
Vec_Wec_t * Cmd_ReadParamChoices( char * pConfig )
{
Vec_Wec_t * vPars;
Vec_Int_t * vLine;
char * pThis, pBuffer[CMD_AUTO_LINE_MAX];
FILE * pFile = fopen( pConfig, "rb" );
if ( pFile == NULL )
{ printf( "File containing list of files \"%s\" cannot be opened.\n", pConfig ); return NULL; }
vPars = Vec_WecAlloc( 100 );
while ( fgets( pBuffer, CMD_AUTO_LINE_MAX, pFile ) != NULL )
{
// get the command from the file
if ( Cmf_IsSpace(pBuffer[0]) || pBuffer[0] == '#')
continue;
// skip trailing spaces
while ( Cmf_IsSpace(pBuffer[strlen(pBuffer)-1]) )
pBuffer[strlen(pBuffer)-1] = 0;
// read the line
vLine = Vec_WecPushLevel( vPars );
for ( pThis = pBuffer; *pThis; )
{
if ( Cmf_IsLowerCaseChar(*pThis) )
{
Vec_IntPushTwo( vLine, (int)*pThis, Abc_Float2Int((float)-1.0) );
pThis++;
while ( Cmf_IsSpace(*pThis) )
pThis++;
continue;
}
if ( Cmf_IsUpperCaseChar(*pThis) )
{
char Param = *pThis++;
if ( !Cmf_IsDigit(*pThis) )
{ printf( "Upper-case character (%c) should be followed by a number without space in line \"%s\".\n", Param, pBuffer ); return NULL; }
Vec_IntPushTwo( vLine, (int)Param, Abc_Float2Int(atof(pThis)) );
while ( Cmf_IsDigit(*pThis) )
pThis++;
while ( Cmf_IsSpace(*pThis) )
pThis++;
continue;
}
printf( "Expecting a leading lower-case or upper-case digit in line \"%s\".\n", pBuffer );
return NULL;
}
}
fclose( pFile );
return vPars;
}
Vec_Ptr_t * Cmd_ReadFiles( char * pFileList )
{
Gia_Man_t * pGia;
Vec_Ptr_t * vAigs;
char pBuffer[CMD_AUTO_LINE_MAX];
FILE * pFile = fopen( pFileList, "rb" );
if ( pFile == NULL )
{ printf( "File containing list of files \"%s\" cannot be opened.\n", pFileList ); return NULL; }
vAigs = Vec_PtrAlloc( 100 );
while ( fgets( pBuffer, CMD_AUTO_LINE_MAX, pFile ) != NULL )
{
// get the command from the file
if ( Cmf_IsSpace(pBuffer[0]) || pBuffer[0] == '#')
continue;
// skip trailing spaces
while ( Cmf_IsSpace(pBuffer[strlen(pBuffer)-1]) )
pBuffer[strlen(pBuffer)-1] = 0;
// read the file
pGia = Gia_AigerRead( pBuffer, 0, 0, 0 );
if ( pGia == NULL )
{
printf( "Cannot read AIG from file \"%s\".\n", pBuffer );
continue;
}
Vec_PtrPush( vAigs, pGia );
}
fclose( pFile );
return vAigs;
}
/**Function*************************************************************
Synopsis [Autotuner for SAT solver "satoko".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cmd_RunAutoTuner( char * pConfig, char * pFileList, int nCores )
{
abctime clk = Abc_Clock();
Vec_Wec_t * vPars = Cmd_ReadParamChoices( pConfig );
Vec_Ptr_t * vAigs = Cmd_ReadFiles( pFileList );
Vec_Ptr_t * vOpts = vPars ? Cmf_CreateOptions( vPars ) : NULL;
int i; char * pString, * pStringBest = NULL;
satoko_opts_t * pOpts, * pOptsBest = NULL;
int Result, ResultBest = 0x7FFFFFFF;
Gia_Man_t * pGia;
// iterate through all possible option settings
if ( vAigs && vOpts )
{
Vec_PtrForEachEntryDouble( satoko_opts_t *, char *, vOpts, pOpts, pString, i )
{
abctime clk = Abc_Clock();
printf( "Evaluating options %20s... ", pString );
Result = Cmd_RunAutoTunerEval( vAigs, pOpts, nCores );
printf( "Cost = %6d. ", Result );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( ResultBest > Result )
{
ResultBest = Result;
pStringBest = pString;
pOptsBest = pOpts;
}
}
printf( "The best options are: %20s ", pStringBest );
printf( "Best cost = %6d. ", ResultBest );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// cleanup
if ( vPars ) Vec_WecFree( vPars );
if ( vOpts ) Vec_PtrFreeFree( vOpts );
if ( vAigs )
{
Vec_PtrForEachEntry( Gia_Man_t *, vAigs, pGia, i )
Gia_ManStop( pGia );
Vec_PtrFree( vAigs );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/base/cmd/module.make
View File

@ -1,6 +1,7 @@
SRC += src/base/cmd/cmd.c \
src/base/cmd/cmdAlias.c \
src/base/cmd/cmdApi.c \
src/base/cmd/cmdAuto.c \
src/base/cmd/cmdFlag.c \
src/base/cmd/cmdHist.c \
src/base/cmd/cmdLoad.c \

54
src/misc/extra/extraUtilUtil.c
View File

@ -102,35 +102,45 @@ int Extra_UtilGetopt( int argc, char *argv[], const char *optstring )
globalUtilOptarg = NULL;
if (pScanStr == NULL || *pScanStr == '\0') {
if (globalUtilOptind == 0) globalUtilOptind++;
if (globalUtilOptind >= argc) return EOF;
place = argv[globalUtilOptind];
if (place[0] != '-' || place[1] == '\0') return EOF;
globalUtilOptind++;
if (place[1] == '-' && place[2] == '\0') return EOF;
pScanStr = place+1;
if (pScanStr == NULL || *pScanStr == '\0')
{
if (globalUtilOptind == 0)
globalUtilOptind++;
if (globalUtilOptind >= argc)
return EOF;
place = argv[globalUtilOptind];
if (place[0] != '-' || place[1] == '\0')
return EOF;
globalUtilOptind++;
if (place[1] == '-' && place[2] == '\0')
return EOF;
pScanStr = place+1;
}
c = *pScanStr++;
place = strchr(optstring, c);
if (place == NULL || c == ':') {
(void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
return '?';
}
if (*++place == ':') {
if (*pScanStr != '\0') {
globalUtilOptarg = pScanStr;
pScanStr = NULL;
} else {
if (globalUtilOptind >= argc) {
(void) fprintf(stderr, "%s: %c requires an argument\n",
argv[0], c);
(void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
return '?';
}
globalUtilOptarg = argv[globalUtilOptind];
globalUtilOptind++;
}
if (*++place == ':')
{
if (*pScanStr != '\0')
{
globalUtilOptarg = pScanStr;
pScanStr = NULL;
}
else
{
if (globalUtilOptind >= argc)
{
(void) fprintf(stderr, "%s: %c requires an argument\n",
argv[0], c);
return '?';
}
globalUtilOptarg = argv[globalUtilOptind];
globalUtilOptind++;
}
}
return c;
}