New fixed point data type.

Expose all options to command line.
Expose search statistics to users.

6 files changed, 149 insertions, 39 deletions

diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h
index aa8a76ab..b1fdb756 100644
--- a/src/sat/satoko/act_var.h
+++ b/src/sat/satoko/act_var.h
@@ -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 */
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index fb07c6f9..363fe2fd 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -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 */
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index fe1d1ef5..a46b0c9d 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -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 */
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
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h
index ee9363bc..7865ab0e 100644
--- a/src/sat/satoko/types.h
+++ b/src/sat/satoko/types.h
@@ -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;
diff --git a/src/sat/satoko/utils/fixed.h b/src/sat/satoko/utils/fixed.h
new file mode 100644
index 00000000..91fc9b79
--- /dev/null
+++ b/src/sat/satoko/utils/fixed.h
@@ -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 */