diff options
| author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-10 17:26:45 -0800 |
|---|---|---|
| committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-10 17:26:45 -0800 |
| commit | 342d2d9f5cd3f89289d84e2dc695516ec959e252 (patch) | |
| tree | 08aba0251e73be1b223c6f13bbbeca7b7dbe6528 /src/sat/satoko/solver_api.c | |
| parent | d335ee096e902844b9a94076e8ce5855f74d9bde (diff) | |
| download | abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.tar.gz abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.tar.bz2 abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.zip | |
New fixed point data type.
Expose all options to command line.
Expose search statistics to users.
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 |