Autotuner for 'satoko'.

7 files changed, 702 insertions, 28 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 5f0bfc7a..321a6d71 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -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
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c
index 5506c7e4..fc8e5c28 100644
--- a/src/aig/gia/giaSatoko.c
+++ b/src/aig/gia/giaSatoko.c
@@ -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 )
 {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1ecc5e68..38a555d8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index ab037139..ec4a0c86 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -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.]
diff --git a/src/base/cmd/cmdAuto.c b/src/base/cmd/cmdAuto.c
new file mode 100644
index 00000000..28b209fa
--- /dev/null
+++ b/src/base/cmd/cmdAuto.c
@@ -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
+
diff --git a/src/base/cmd/module.make b/src/base/cmd/module.make
index b09ffa81..1042fbb0 100644
--- a/src/base/cmd/module.make
+++ b/src/base/cmd/module.make
@@ -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 \
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index 253d9e3c..2f0f4559 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -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;
 }