diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-11 13:28:22 -0800 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-11 13:28:22 -0800 |
commit | ab2d3acac99620aef7d5b1c48eb59ee33bb2b584 (patch) | |
tree | 69d1da6aee0c60de07bd9384c77fcea029915fe4 /src/sat/satoko/solver_api.c | |
parent | 8333cb807fbe6773df8285591e75f35d519b6e81 (diff) | |
download | abc-ab2d3acac99620aef7d5b1c48eb59ee33bb2b584.tar.gz abc-ab2d3acac99620aef7d5b1c48eb59ee33bb2b584.tar.bz2 abc-ab2d3acac99620aef7d5b1c48eb59ee33bb2b584.zip |
New implementation of a software floating point implementation (sdbl) for consistency across different platforms and compilers.
Removing useless files and compile time options related to variable activity data type (it can only be sdbl).
Diffstat (limited to 'src/sat/satoko/solver_api.c')
-rw-r--r-- | src/sat/satoko/solver_api.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index ccab7685..f3f3d781 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -169,7 +169,7 @@ void satoko_default_opts(satoko_opts_t *opts) /* VSIDS heuristic */ opts->var_act_limit = VAR_ACT_LIMIT; opts->var_act_rescale = VAR_ACT_RESCALE; - opts->var_decay = VAR_ACT_DECAY; + opts->var_decay = 0.95; opts->clause_decay = (clause_act_t) 0.995; /* Binary resolution */ opts->clause_max_sz_bin_resol = 30; @@ -222,7 +222,9 @@ void satoko_add_variable(solver_t *s, char sign) vec_wl_push(s->bin_watches); vec_wl_push(s->watches); vec_wl_push(s->watches); - vec_act_push_back(s->activity, 0); + /* Variable activity are initialized with the lowest possible value + * which in satoko double implementation (SDBL) is the constant 1 */ + vec_act_push_back(s->activity, SDBL_CONST1); vec_uint_push_back(s->levels, 0); vec_char_push_back(s->assigns, VAR_UNASSING); vec_char_push_back(s->polarity, sign); |