- Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default))

- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.

1 files changed, 14 insertions, 15 deletions

diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h
index 161e9d9a..aa8a76ab 100644
--- a/src/sat/satoko/act_var.h
+++ b/src/sat/satoko/act_var.h
@@ -16,27 +16,27 @@
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-#ifdef SATOKO_ACT_VAR_DBLE
+#if defined SATOKO_ACT_VAR_DBLE || defined SATOKO_ACT_VAR_FLOAT
 /** Re-scale the activity value for all variables.
  */
 static inline void var_act_rescale(solver_t *s)
 {
     unsigned i;
-    double *activity = vec_dble_data(s->activity);
+    act_t *activity = vec_act_data(s->activity);
 
-    for (i = 0; i < vec_dble_size(s->activity); i++)
-        activity[i] *= 1e-100;
-    s->var_act_inc *= 1e-100;
+    for (i = 0; i < vec_act_size(s->activity); i++)
+        activity[i] *= VAR_ACT_RESCALE;
+    s->var_act_inc *= VAR_ACT_RESCALE;
 }
 
 /** Increment the activity value of one variable ('var')
  */
 static inline void var_act_bump(solver_t *s, unsigned var)
 {
-    double *activity = vec_dble_data(s->activity);
+    act_t *activity = vec_act_data(s->activity);
 
     activity[var] += s->var_act_inc;
-    if (activity[var] > 1e100)
+    if (activity[var] > VAR_ACT_LIMIT)
         var_act_rescale(s);
     if (heap_in_heap(s->var_order, var))
         heap_decrease(s->var_order, var);
@@ -49,25 +49,24 @@ static inline void var_act_decay(solver_t *s)
     s->var_act_inc *= (1 / s->opts.var_decay);
 }
 
-#else /* SATOKO_ACT_VAR_DBLE */
+#else
 
 static inline void var_act_rescale(solver_t *s)
 {
     unsigned i;
-    unsigned *activity = vec_uint_data(s->activity);
+    act_t *activity = vec_act_data(s->activity);
 
-    for (i = 0; i < vec_uint_size(s->activity); i++)
+    for (i = 0; i < vec_act_size(s->activity); i++)
         activity[i] >>= 19;
-    s->var_act_inc >>= 19;
-    s->var_act_inc = mkt_uint_max(s->var_act_inc, (1 << 5));
+    s->var_act_inc = stk_uint_max((s->var_act_inc >> 19), (1 << 5));
 }
 
 static inline void var_act_bump(solver_t *s, unsigned var)
 {
-    unsigned *activity = vec_uint_data(s->activity);
+    act_t *activity = vec_act_data(s->activity);
 
     activity[var] += s->var_act_inc;
-    if (activity[var] & 0x80000000)
+    if (activity[var] & 0xF0000000)
         var_act_rescale(s);
     if (heap_in_heap(s->var_order, var))
         heap_decrease(s->var_order, var);
@@ -78,7 +77,7 @@ static inline void var_act_decay(solver_t *s)
     s->var_act_inc += (s->var_act_inc >> 4);
 }
 
-#endif /* SATOKO_ACT_VAR_DBLE */
+#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FLOAT */
 
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__act_var_h */