diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 01:41:19 +0000 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 01:41:19 +0000 |
| commit | f7a1fe88fb43ea326af3625fc33a914b22e96336 (patch) | |
| tree | e686fac902b425b80c49d83494b4e8fe670ea662 /src/sat/satoko/solver_api.c | |
| parent | 1bdbea66120292d821fc594b9a6637135bde6244 (diff) | |
| parent | d69735309d3281bbc824f0c9b5c2420d7f2a4bd3 (diff) | |
| download | abc-f7a1fe88fb43ea326af3625fc33a914b22e96336.tar.gz abc-f7a1fe88fb43ea326af3625fc33a914b22e96336.tar.bz2 abc-f7a1fe88fb43ea326af3625fc33a914b22e96336.zip | |
Merged in boschmitt/abc (pull request #51)
Modifications to satoko.
Diffstat (limited to 'src/sat/satoko/solver_api.c')
| -rw-r--r-- | src/sat/satoko/solver_api.c | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 980cc160..ccab7685 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -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 |