cmdAuto.c File Reference

#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"

Include dependency graph for cmdAuto.c:

Go to the source code of this file.

Macros
#define	CMD_AUTO_LINE_MAX   1000
	DECLARATIONS ///.
#define	CMD_AUTO_ARG_MAX   100

Functions
int	Gia_ManSatokoCallOne (Gia_Man_t *p, satoko_opts_t *opts, int iOutput)
void	Cmd_RunAutoTunerPrintOptions (satoko_opts_t *pOpts)
	FUNCTION DEFINITIONS ///.
int	Cmd_RunAutoTunerEvalSimple (Vec_Ptr_t *vAigs, satoko_opts_t *pOpts)
int	Cmd_RunAutoTunerEval (Vec_Ptr_t *vAigs, satoko_opts_t *pOpts, int nCores)
char *	Cmd_DeriveConvertIntoString (int argc, char **argv)
satoko_opts_t *	Cmd_DeriveOptionFromSettings (int argc, char **argv)
void	Cmf_CreateOptions_rec (Vec_Wec_t *vPars, int iPar, char Argv[CMD_AUTO_ARG_MAX][20], int Argc, Vec_Ptr_t *vOpts)
Vec_Ptr_t *	Cmf_CreateOptions (Vec_Wec_t *vPars)
Vec_Wec_t *	Cmd_ReadParamChoices (char *pConfig)
Vec_Ptr_t *	Cmd_ReadFiles (char *pFileList)
void	Cmd_RunAutoTuner (char *pConfig, char *pFileList, int nCores)

Macro Definition Documentation

CMD_AUTO_ARG_MAX

#define CMD_AUTO_ARG_MAX   100

Definition at line 48 of file cmdAuto.c.

CMD_AUTO_LINE_MAX

#define CMD_AUTO_LINE_MAX   1000

DECLARATIONS ///.

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

]

Definition at line 47 of file cmdAuto.c.

Function Documentation

Cmd_DeriveConvertIntoString()

char * Cmd_DeriveConvertIntoString	(	int	argc,
		char **	argv )

Function*************************************************************

Synopsis [Derives all possible param stucts according to the config file.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file cmdAuto.c.

{
    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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_DeriveOptionFromSettings()

satoko_opts_t * Cmd_DeriveOptionFromSettings	(	int	argc,
		char **	argv )

Definition at line 238 of file cmdAuto.c.

{
    int c;
    satoko_opts_t opts, * pOpts;
    satoko_default_opts(&opts);
    Extra_UtilGetoptReset();
#ifdef SATOKO_ACT_VAR_FIXED
    while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRSTUhv" ) ) != EOF )
#else
    while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRShv" ) ) != EOF )
#endif
    {
        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 'P':
                if ( globalUtilOptind >= argc )
                {
                    Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
                    return NULL;
                }
                opts.prop_limit = atoi(argv[globalUtilOptind]);
                globalUtilOptind++;
                if ( opts.prop_limit < 0 )
                    return NULL;
                break;
         case 'D':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.f_rst = atof(argv[globalUtilOptind]);
               globalUtilOptind++;
               if ( opts.f_rst < 0 )
                   return NULL;
               break;
         case 'E':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.b_rst = atof(argv[globalUtilOptind]);
               globalUtilOptind++;
               if ( opts.b_rst < 0 )
                   return NULL;
               break;
         case 'F':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.fst_block_rst = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'G':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.sz_lbd_bqueue = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'H':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.sz_trail_bqueue = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'I':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.n_conf_fst_reduce = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'J':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.inc_reduce = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'K':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.inc_special_reduce = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'L':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.lbd_freeze_clause = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'M':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100;
               globalUtilOptind++;
               if ( opts.learnt_ratio < 0 )
                   return NULL;
               break;
         case 'N':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100;
               globalUtilOptind++;
               if ( opts.garbage_max_ratio < 0 )
                   return NULL;
               break;
         case 'O':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.clause_max_sz_bin_resol = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'Q':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
                   return NULL;
               }
               opts.clause_min_lbd_bin_resol = (unsigned)atoi(argv[globalUtilOptind]);
               globalUtilOptind++;
               break;
         case 'R':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-R\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.clause_decay = atof(argv[globalUtilOptind]);
               globalUtilOptind++;
               if ( opts.clause_decay < 0 )
                   return NULL;
               break;
         case 'S':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.var_decay = atof(argv[globalUtilOptind]);
               globalUtilOptind++;
               if ( opts.var_decay < 0 )
                   return NULL;
               break;
#ifdef SATOKO_ACT_VAR_FIXED
         case 'T':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-T\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.var_act_limit = (unsigned)strtol(argv[globalUtilOptind], NULL, 16);
               globalUtilOptind++;
               break;
         case 'U':
               if ( globalUtilOptind >= argc )
               {
                   Abc_Print( -1, "Command line switch \"-U\" should be followed by an float.\n" );
                   return NULL;
               }
               opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16);
               globalUtilOptind++;
               break;
#endif
        case 'h':
            return NULL;
        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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_ReadFiles()

Vec_Ptr_t * Cmd_ReadFiles

(

char *

pFileList

)

Definition at line 595 of file cmdAuto.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_ReadParamChoices()

Vec_Wec_t * Cmd_ReadParamChoices

(

char *

pConfig

)

Definition at line 547 of file cmdAuto.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_RunAutoTuner()

void Cmd_RunAutoTuner	(	char *	pConfig,
		char *	pFileList,
		int	nCores )

Function*************************************************************

Synopsis [Autotuner for SAT solver "satoko".]

Description []

SideEffects []

SeeAlso []

Definition at line 636 of file cmdAuto.c.

{
    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 settings: %20s...  \n", 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 settings are: %20s    \n", pStringBest );
        printf( "Best cost = %6d.  ", ResultBest );
        Abc_PrintTime( 1, "Total 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 );
    }
}

Here is the call graph for this function:

Cmd_RunAutoTunerEval()

int Cmd_RunAutoTunerEval	(	Vec_Ptr_t *	vAigs,
		satoko_opts_t *	pOpts,
		int	nCores )

Function*************************************************************

Synopsis [The main evaluation procedure for the set of AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file cmdAuto.c.

{
    return Cmd_RunAutoTunerEvalSimple( vAigs, pOpts );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_RunAutoTunerEvalSimple()

int Cmd_RunAutoTunerEvalSimple	(	Vec_Ptr_t *	vAigs,
		satoko_opts_t *	pOpts )

Function*************************************************************

Synopsis [The main evaluation procedure for an array of AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file cmdAuto.c.

{
    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_ManSatokoCallOne( pGia, pOpts, -1 );
    return TotalCost;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmd_RunAutoTunerPrintOptions()

void Cmd_RunAutoTunerPrintOptions

(

satoko_opts_t *

pOpts

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Printing option structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 67 of file cmdAuto.c.

{
    printf( "-C %d  ",   (int)pOpts->conf_limit );
    printf( "-V %.3f  ", (float)pOpts->var_decay );
    printf( "-W %.3f  ", (float)pOpts->clause_decay );
    if ( pOpts->verbose )
        printf( "-v" );
    printf( "\n" );
}

Cmf_CreateOptions()

Vec_Ptr_t * Cmf_CreateOptions

(

Vec_Wec_t *

vPars

)

Definition at line 506 of file cmdAuto.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cmf_CreateOptions_rec()

void Cmf_CreateOptions_rec	(	Vec_Wec_t *	vPars,
		int	iPar,
		char	Argv[CMD_AUTO_ARG_MAX][20],
		int	Argc,
		Vec_Ptr_t *	vOpts )

Definition at line 456 of file cmdAuto.c.

{
    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 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManSatokoCallOne()

int Gia_ManSatokoCallOne ( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )

extern

Definition at line 199 of file giaSatoko.c.

{
    abctime clk = Abc_Clock();
    satoko_t * pSat;
    int status = SATOKO_UNSAT, Cost = 0;
    pSat = Gia_ManSatokoCreate( p, opts );
    if ( pSat )
    {
        status = satoko_solve( pSat );
        Cost = satoko_stats(pSat)->n_conflicts;
        satoko_destroy( pSat );
    }
    Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk );
    return Cost;
}

Here is the call graph for this function:

Here is the caller graph for this function: