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

Merged in boschmitt/abc (pull request #51) 

Modifications to satoko.
This commit is contained in:
Alan Mishchenko 2017-02-11 01:41:19 +00:00
parent 1bdbea6612 d69735309d
commit f7a1fe88fb
7 changed files with 363 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -23326,7 +23326,11 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != 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 )
{
@ -23341,6 +23345,184 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
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':
@ -23379,9 +23561,37 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
}
usage:
Abc_Print( -2, "usage: satoko [-CILDE num] [-hv]<file>.cnf\n" );
#ifdef SATOKO_ACT_VAR_FIXED
Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRSTU num] [-hv]<file>.cnf\n" );
#else
Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRS num] [-hv]<file>.cnf\n" );
#endif
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
Abc_Print( -2, "\t-P num : limit on the number of propagations [default = %d]\n", opts.conf_limit );
Abc_Print( -2, "\n\tConstants used for restart heuristic:\n");
Abc_Print( -2, "\t-D num : Constant value used by restart heuristics in forcing restarts [default = %f]\n", opts.f_rst );
Abc_Print( -2, "\t-E num : Constant value used by restart heuristics in blocking restarts [default = %f]\n", opts.b_rst );
Abc_Print( -2, "\t-F num : Lower bound n.of conflicts for start blocking restarts [default = %d]\n", opts.fst_block_rst );
Abc_Print( -2, "\t-G num : Size of the moving avarege queue for LBD (force restart) [default = %d]\n", opts.sz_lbd_bqueue );
Abc_Print( -2, "\t-H num : Size of the moving avarege queue for Trail size (block restart) [default = %d]\n", opts.sz_trail_bqueue );
Abc_Print( -2, "\n\tConstants used for clause database reduction heuristic:\n");
Abc_Print( -2, "\t-I num : N.of conflicts before first clause databese reduction [default = %d]\n", opts.n_conf_fst_reduce );
Abc_Print( -2, "\t-J num : Increment to reduce [default = %d]\n", opts.inc_reduce );
Abc_Print( -2, "\t-K num : Special increment to reduce [default = %d]\n", opts.inc_special_reduce );
Abc_Print( -2, "\t-L num : Protecs clauses from deletion for one turn if its LBD is lower [default = %d]\n", opts.lbd_freeze_clause );
Abc_Print( -2, "\t-M num : Percentage of learned clauses to remove [default = %d]\n", ( int )( 100 * opts.learnt_ratio ) );
Abc_Print( -2, "\t-N num : Max percentage of garbage in clause database [default = %d]\n", ( int )( 100 * opts.garbage_max_ratio ) );
Abc_Print( -2, "\n\tConstants used for binary resolution (clause minimization):\n");
Abc_Print( -2, "\t-O num : Max clause size for binary resolution [default = %d]\n", opts.clause_max_sz_bin_resol );
Abc_Print( -2, "\t-Q num : Min clause LBD for binary resolution [default = %d]\n", opts.clause_min_lbd_bin_resol );
Abc_Print( -2, "\n\tConstants used for branching (VSIDS heuristic):\n");
Abc_Print( -2, "\t-R num : Clause activity decay factor (when using float clause activity) [default = %f]\n", opts.clause_decay );
Abc_Print( -2, "\t-S num : Varibale activity decay factor [default = %f]\n", opts.var_decay );
#ifdef SATOKO_ACT_VAR_FIXED
Abc_Print( -2, "\t-T num : Variable activity limit valeu [default = 0x%08X]\n", opts.var_act_limit );
Abc_Print( -2, "\t-U num : Variable activity re-scale factor [default = 0x%08X]\n", opts.var_act_rescale );
#endif
Abc_Print( -2, "\n\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -38223,7 +38433,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fExtractAll )
{
char Buffer[1000];
Gia_Obj_t * pObj;
Gia_Obj_t * pObj;
int i, nDigits = Abc_Base10Log(Gia_ManPoNum(pAbc->pGia));
Gia_ManForEachPo( pAbc->pGia, pObj, i )
{

38
src/sat/satoko/act_var.h
View File

@ -16,7 +16,7 @@
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
#if defined SATOKO_ACT_VAR_DBLE || defined SATOKO_ACT_VAR_FLOAT
#if defined SATOKO_ACT_VAR_DBLE
/** Re-scale the activity value for all variables.
*/
static inline void var_act_rescale(solver_t *s)
@ -25,8 +25,8 @@ static inline void var_act_rescale(solver_t *s)
act_t *activity = vec_act_data(s->activity);
for (i = 0; i < vec_act_size(s->activity); i++)
activity[i] *= VAR_ACT_RESCALE;
s->var_act_inc *= VAR_ACT_RESCALE;
activity[i] *= s->opts.var_act_rescale;
s->var_act_inc *= s->opts.var_act_rescale;
}
/** Increment the activity value of one variable ('var')
@ -36,7 +36,7 @@ static inline void var_act_bump(solver_t *s, unsigned var)
act_t *activity = vec_act_data(s->activity);
activity[var] += s->var_act_inc;
if (activity[var] > VAR_ACT_LIMIT)
if (activity[var] > s->opts.var_act_limit)
var_act_rescale(s);
if (heap_in_heap(s->var_order, var))
heap_decrease(s->var_order, var);
@ -49,6 +49,34 @@ static inline void var_act_decay(solver_t *s)
s->var_act_inc *= (1 / s->opts.var_decay);
}
#elif defined(SATOKO_ACT_VAR_FIXED)
static inline void var_act_rescale(solver_t *s)
{
unsigned i;
act_t *activity = (act_t *)vec_act_data(s->activity);
for (i = 0; i < vec_act_size(s->activity); i++)
activity[i] = fixed_mult(activity[i], VAR_ACT_RESCALE);
s->var_act_inc = fixed_mult(s->var_act_inc, VAR_ACT_RESCALE);
}
static inline void var_act_bump(solver_t *s, unsigned var)
{
act_t *activity = (act_t *)vec_act_data(s->activity);
activity[var] = fixed_add(activity[var], s->var_act_inc);
if (activity[var] > VAR_ACT_LIMIT)
var_act_rescale(s);
if (heap_in_heap(s->var_order, var))
heap_decrease(s->var_order, var);
}
static inline void var_act_decay(solver_t *s)
{
s->var_act_inc = fixed_mult(s->var_act_inc, dble2fixed(1 / s->opts.var_decay));
}
#else
static inline void var_act_rescale(solver_t *s)
@ -77,7 +105,7 @@ static inline void var_act_decay(solver_t *s)
s->var_act_inc += (s->var_act_inc >> 4);
}
#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FLOAT */
#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FIXED */
ABC_NAMESPACE_HEADER_END
#endif /* satoko__act_var_h */

27
src/sat/satoko/satoko.h
View File

@ -32,7 +32,7 @@ typedef struct satoko_opts satoko_opts_t;
struct satoko_opts {
/* Limits */
long conf_limit; /* Limit on the n.of conflicts */
long prop_limit; /* Limit on the n.of implications */
long prop_limit; /* Limit on the n.of propagations */
/* Constants used for restart heuristic */
double f_rst; /* Used to force a restart */
@ -42,7 +42,7 @@ struct satoko_opts {
unsigned sz_trail_bqueue; /* Size of the moving avarege queue for Trail size (block restart) */
/* Constants used for clause database reduction heuristic */
unsigned n_conf_fst_reduce; /* N.of conflicts before first reduction */
unsigned n_conf_fst_reduce; /* N.of conflicts before first clause databese reduction */
unsigned inc_reduce; /* Increment to reduce */
unsigned inc_special_reduce; /* Special increment to reduce */
unsigned lbd_freeze_clause;
@ -50,7 +50,9 @@ struct satoko_opts {
/* VSIDS heuristic */
float clause_decay;
act_t var_decay;
double var_decay;
act_t var_act_limit;
act_t var_act_rescale;
/* Binary resolution */
unsigned clause_max_sz_bin_resol;
@ -59,6 +61,21 @@ struct satoko_opts {
char verbose;
};
typedef struct satoko_stats satoko_stats_t;
struct satoko_stats {
unsigned n_starts;
unsigned n_reduce_db;
long n_decisions;
long n_propagations;
long n_inspects;
long n_conflicts;
long n_original_lits;
long n_learnt_lits;
};
//===------------------------------------------------------------------------===
extern satoko_t *satoko_create(void);
extern void satoko_destroy(satoko_t *);
@ -81,7 +98,9 @@ extern int satoko_solve(satoko_t *);
* - The return value is either the size of the array or -1 in case the final
* conflict cluase was not generated.
*/
extern int satoko_final_conflict(satoko_t *, unsigned *);
extern int satoko_final_conflict(satoko_t *, unsigned *);
extern satoko_stats_t satoko_stats(satoko_t *);
ABC_NAMESPACE_HEADER_END
#endif /* satoko__satoko_h */

13
src/sat/satoko/solver.h
View File

@ -38,19 +38,6 @@ enum {
#define UNDEF 0xFFFFFFFF
struct satoko_stats {
unsigned n_starts;
unsigned n_reduce_db;
long n_decisions;
long n_propagations;
long n_inspects;
long n_conflicts;
long n_original_lits;
long n_learnt_lits;
};
typedef struct solver_t_ solver_t;
struct solver_t_ {
/* User data */

11
src/sat/satoko/solver_api.c
View File

@ -12,8 +12,8 @@
#include <math.h>
#include "act_var.h"
#include "utils/misc.h"
#include "solver.h"
#include "utils/misc.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_IMPL_START
@ -167,7 +167,9 @@ void satoko_default_opts(satoko_opts_t *opts)
opts->lbd_freeze_clause = 30;
opts->learnt_ratio = 0.5;
/* VSIDS heuristic */
opts->var_decay = (act_t) 0.95;
opts->var_act_limit = VAR_ACT_LIMIT;
opts->var_act_rescale = VAR_ACT_RESCALE;
opts->var_decay = VAR_ACT_DECAY;
opts->clause_decay = (clause_act_t) 0.995;
/* Binary resolution */
opts->clause_max_sz_bin_resol = 30;
@ -308,4 +310,9 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
}
satoko_stats_t satoko_stats(satoko_t *s)
{
return s->stats;
}
ABC_NAMESPACE_IMPL_END

32
src/sat/satoko/types.h
View File

@ -9,21 +9,22 @@
#ifndef satoko__types_h
#define satoko__types_h
#include "utils/fixed.h"
#include "utils/vec/vec_dble.h"
#include "utils/vec/vec_flt.h"
#include "utils/vec/vec_uint.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
// #define SATOKO_ACT_VAR_DBLE
// #define SATOKO_ACT_VAR_FLOAT
#define SATOKO_ACT_VAR_DBLE
// #define SATOKO_ACT_VAR_FIXED
// #define SATOKO_ACT_CLAUSE_FLOAT
#ifdef SATOKO_ACT_VAR_DBLE
#define VAR_ACT_INIT_INC 1.0
#define VAR_ACT_LIMIT (double)1e100
#define VAR_ACT_RESCALE (double)1e-100
#define VAR_ACT_DECAY (double)0.95
typedef double act_t;
typedef vec_dble_t vec_act_t ;
#define vec_act_alloc(size) vec_dble_alloc(size)
@ -32,18 +33,19 @@ ABC_NAMESPACE_HEADER_START
#define vec_act_data(vec) vec_dble_data(vec)
#define vec_act_at(vec, idx) vec_dble_at(vec, idx)
#define vec_act_push_back(vec, value) vec_dble_push_back(vec, value)
#elif defined(SATOKO_ACT_VAR_FLOAT)
#define VAR_ACT_INIT_INC 1.0
#define VAR_ACT_LIMIT (float)1e20
#define VAR_ACT_RESCALE (float)1e-20
typedef float act_t;
typedef vec_flt_t vec_act_t ;
#define vec_act_alloc(size) vec_flt_alloc(size)
#define vec_act_free(vec) vec_flt_free(vec)
#define vec_act_size(vec) vec_flt_size(vec)
#define vec_act_data(vec) vec_flt_data(vec)
#define vec_act_at(vec, idx) vec_flt_at(vec, idx)
#define vec_act_push_back(vec, value) vec_flt_push_back(vec, value)
#elif defined(SATOKO_ACT_VAR_FIXED)
#define VAR_ACT_INIT_INC FIXED_ONE
#define VAR_ACT_LIMIT (fixed_t)0xDFFFFFFF
#define VAR_ACT_RESCALE (fixed_t)0x00000012
#define VAR_ACT_DECAY (double)0.96
typedef fixed_t act_t;
typedef vec_uint_t vec_act_t;
#define vec_act_alloc(size) vec_uint_alloc(size)
#define vec_act_free(vec) vec_uint_free(vec)
#define vec_act_size(vec) vec_uint_size(vec)
#define vec_act_data(vec) vec_uint_data(vec)
#define vec_act_at(vec, idx) vec_uint_at(vec, idx)
#define vec_act_push_back(vec, value) vec_uint_push_back(vec, value)
#else
#define VAR_ACT_INIT_INC (1 << 5)
typedef unsigned act_t;

67
src/sat/satoko/utils/fixed.h Normal file
View File

@ -0,0 +1,67 @@
//===--- sort.h -------------------------------------------------------------===
//
// satoko: Satisfiability solver
//
// This file is distributed under the BSD 2-Clause License.
// See LICENSE for details.
//
//===------------------------------------------------------------------------===
#ifndef satoko__utils__fixed_h
#define satoko__utils__fixed_h
#include "misc.h"
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
typedef unsigned fixed_t;
static const int FIXED_W_BITS = 16; /* */
static const int FIXED_F_BITS = 32 - FIXED_W_BITS;
static const int FIXED_F_MASK = (1 << FIXED_F_BITS) - 1;
static const fixed_t FIXED_MAX = 0xFFFFFFFF;
static const fixed_t FIXED_MIN = 0x00000000;
static const fixed_t FIXED_ONE = (1 << FIXED_F_BITS);
/* Conversion functions */
static inline fixed_t uint2fixed(unsigned a) { return a * FIXED_ONE; }
static inline unsigned fixed2uint(fixed_t a)
{
return (a + (FIXED_ONE >> 1)) / FIXED_ONE;
}
static inline float fixed2float(fixed_t a) { return (float)a / FIXED_ONE; }
static inline fixed_t float2fixed(float a)
{
float temp = a * FIXED_ONE;
temp += (temp >= 0) ? 0.5f : -0.5f;
return (fixed_t)temp;
}
static inline double fixed2dble(fixed_t a) { return (double)a / FIXED_ONE; }
static inline fixed_t dble2fixed(double a)
{
double temp = a * FIXED_ONE;
temp += (temp >= 0) ? 0.5f : -0.5f;
return (fixed_t)temp;
}
static inline fixed_t fixed_add(fixed_t a, fixed_t b) { return (a + b); }
static inline fixed_t fixed_mult(fixed_t a, fixed_t b)
{
unsigned hi_a = (a >> FIXED_F_BITS), lo_a = (a & FIXED_F_MASK);
unsigned hi_b = (b >> FIXED_F_BITS), lo_b = (b & FIXED_F_MASK);
unsigned lo_ab = lo_a * lo_b;
unsigned ab_ab = (hi_a * lo_b) + (lo_a * hi_b);
unsigned hi_ret = (hi_a * hi_b) + (ab_ab >> FIXED_F_BITS);
unsigned lo_ret = lo_ab + (ab_ab << FIXED_W_BITS);
/* Carry */
if (lo_ret < lo_ab)
hi_ret++;
return (hi_ret << FIXED_F_BITS) | (lo_ret >> FIXED_W_BITS);
}
ABC_NAMESPACE_HEADER_END
#endif /* satoko__utils__fixed_h */