Skip to content

A
abc
Commit 5d717256 by Alan Mishchenko
Options

Updates to the autotuner.

parent d4b491d8
Showing with 197 additions and 234 deletions
src/base/abci/abc.c
......@@ -23320,222 +23320,22 @@ usage:
***********************************************************************/
int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
{
abctime clk;
int c;
satoko_opts_t opts;
extern satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv );
// create default options
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" );
goto usage;
}
opts.conf_limit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.conf_limit < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
opts.prop_limit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.prop_limit < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" );
goto usage;
}
opts.f_rst = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.f_rst < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" );
goto usage;
}
opts.b_rst = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.b_rst < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100;
globalUtilOptind++;
if ( opts.learnt_ratio < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100;
globalUtilOptind++;
if ( opts.garbage_max_ratio < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
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" );
goto usage;
}
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" );
goto usage;
}
opts.clause_decay = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.clause_decay < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" );
goto usage;
}
opts.var_decay = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.var_decay < 0 )
goto usage;
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" );
goto usage;
}
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" );
goto usage;
}
opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16);
globalUtilOptind++;
break;
#endif
case 'h':
goto usage;
case 'v':
opts.verbose ^= 1;
break;
default:
goto usage;
}
}
// override default options
popts = Cmd_DeriveOptionFromSettings( argc, argv );
if ( popts == NULL )
goto usage;
memcpy( &opts, popts, sizeof(satoko_opts_t) );
ABC_FREE( popts );
if ( argc == globalUtilOptind + 1 )
{
abctime clk;
char * pFileName = argv[globalUtilOptind];
satoko_t * p;
int status;
src/base/cmd/cmdAuto.c
......@@ -241,7 +241,11 @@ satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv )
satoko_opts_t opts, * pOpts;
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CVWhv" ) ) != EOF )
#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 )
{
......@@ -256,31 +260,190 @@ satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv )
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 '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;
}
......
src/sat/satoko/types.h
......@@ -18,7 +18,7 @@ ABC_NAMESPACE_HEADER_START
#define SATOKO_ACT_VAR_DBLE
// #define SATOKO_ACT_VAR_FIXED
// #define SATOKO_ACT_CLAUSE_FLOAT
#define SATOKO_ACT_CLAUSE_FLOAT
#ifdef SATOKO_ACT_VAR_DBLE
#define VAR_ACT_INIT_INC 1.0
......
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