From 342d2d9f5cd3f89289d84e2dc695516ec959e252 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Fri, 10 Feb 2017 17:26:45 -0800 Subject: New fixed point data type. Expose all options to command line. Expose search statistics to users. --- src/sat/satoko/solver_api.c | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src/sat/satoko/solver_api.c') 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 #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 -- cgit v1.2.3