New implementation of a software floating point implementation (sdbl) for consistency across different platforms and compilers.

Removing useless files and compile time options related to variable activity data type (it can only be sdbl).

11 files changed, 412 insertions, 469 deletions

diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h
index 1465e5ee..ade5e569 100644
--- a/src/sat/satoko/act_clause.h
+++ b/src/sat/satoko/act_clause.h
@@ -15,40 +15,6 @@
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-#ifdef SATOKO_ACT_CLAUSE_FLOAT
-
-/** Re-scale the activity value for all clauses.
- */
-static inline void clause_act_rescale(solver_t *s)
-{
-    unsigned i, cref;
-    struct clause *clause;
-
-    vec_uint_foreach(s->learnts, cref, i) {
-        clause = clause_read(s, cref);
-        clause->data[clause->size].act *= (float)1e-20;
-    }
-    s->clause_act_inc  *= (float)1e-20;
-}
-
-/** Increment the activity value of one clause ('clause')
- */
-static inline void clause_act_bump(solver_t *s, struct clause *clause)
-{
-    clause->data[clause->size].act += s->clause_act_inc;
-    if (clause->data[clause->size].act > 1e20)
-        clause_act_rescale(s);
-}
-
-/** Increment the value by which clauses activity values are incremented
- */
-static inline void clause_act_decay(solver_t *s)
-{
-    s->clause_act_inc *= (1 / s->opts.clause_decay);
-}
-
-#else /* SATOKO_ACT_CLAUSE_FLOAT */
-
 static inline void clause_act_rescale(solver_t *s)
 {
     unsigned i, cref;
@@ -73,7 +39,5 @@ static inline void clause_act_decay(solver_t *s)
     s->clause_act_inc += (s->clause_act_inc >> 10);
 }
 
-#endif /* SATOKO_ACT_CLAUSE_FLOAT */
-
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__act_clause_h */
diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h
index b1fdb756..6b0ff98a 100644
--- a/src/sat/satoko/act_var.h
+++ b/src/sat/satoko/act_var.h
@@ -12,11 +12,11 @@
 #include "solver.h"
 #include "types.h"
 #include "utils/heap.h"
+#include "utils/sdbl.h"
 
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-#if defined SATOKO_ACT_VAR_DBLE
 /** Re-scale the activity value for all variables.
  */
 static inline void var_act_rescale(solver_t *s)
@@ -24,9 +24,9 @@ static inline void var_act_rescale(solver_t *s)
     unsigned i;
     act_t *activity = vec_act_data(s->activity);
 
-    for (i = 0; i < vec_act_size(s->activity); i++)
-        activity[i] *= s->opts.var_act_rescale;
-    s->var_act_inc *= s->opts.var_act_rescale;
+    for (i = 0; i < vec_sdbl_size(s->activity); i++)
+        activity[i] = sdbl_div(activity[i], s->opts.var_act_rescale);
+    s->var_act_inc = sdbl_div(s->var_act_inc, s->opts.var_act_rescale);
 }
 
 /** Increment the activity value of one variable ('var')
@@ -35,7 +35,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;
+    activity[var] = sdbl_add(activity[var], s->var_act_inc);
     if (activity[var] > s->opts.var_act_limit)
         var_act_rescale(s);
     if (heap_in_heap(s->var_order, var))
@@ -46,66 +46,8 @@ static inline void var_act_bump(solver_t *s, unsigned var)
  */
 static inline void var_act_decay(solver_t *s)
 {
-    s->var_act_inc *= (1 / s->opts.var_decay);
+    s->var_act_inc = sdbl_mult(s->var_act_inc, double2sdbl(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)
-{
-    unsigned i;
-    act_t *activity = vec_act_data(s->activity);
-
-    for (i = 0; i < vec_act_size(s->activity); i++)
-        activity[i] >>= 19;
-    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)
-{
-    act_t *activity = vec_act_data(s->activity);
-
-    activity[var] += s->var_act_inc;
-    if (activity[var] & 0xF0000000)
-        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 += (s->var_act_inc >> 4);
-}
-
-#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 363fe2fd..e3134b77 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -49,10 +49,11 @@ struct satoko_opts {
     float learnt_ratio;          /* Percentage of learned clauses to remove */
 
     /* VSIDS heuristic */
-    float clause_decay;
     double var_decay;
+    float clause_decay;
+    unsigned var_act_rescale;
     act_t var_act_limit;
-    act_t var_act_rescale;
+
 
     /* Binary resolution */
     unsigned clause_max_sz_bin_resol;
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index a46b0c9d..849d738a 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -24,7 +24,7 @@
 #include "utils/mem.h"
 #include "utils/misc.h"
 #include "utils/vec/vec_char.h"
-#include "utils/vec/vec_dble.h"
+#include "utils/vec/vec_sdbl.h"
 #include "utils/vec/vec_uint.h"
 
 #include "misc/util/abc_global.h"
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index ccab7685..f3f3d781 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -169,7 +169,7 @@ void satoko_default_opts(satoko_opts_t *opts)
     /* VSIDS heuristic */
     opts->var_act_limit = VAR_ACT_LIMIT;
     opts->var_act_rescale = VAR_ACT_RESCALE;
-    opts->var_decay = VAR_ACT_DECAY;
+    opts->var_decay = 0.95;
     opts->clause_decay = (clause_act_t) 0.995;
     /* Binary resolution */
     opts->clause_max_sz_bin_resol = 30;
@@ -222,7 +222,9 @@ void satoko_add_variable(solver_t *s, char sign)
     vec_wl_push(s->bin_watches);
     vec_wl_push(s->watches);
     vec_wl_push(s->watches);
-    vec_act_push_back(s->activity, 0);
+    /* Variable activity are initialized with the lowest possible value
+     * which in satoko double implementation (SDBL) is the constant 1 */
+    vec_act_push_back(s->activity, SDBL_CONST1);
     vec_uint_push_back(s->levels, 0);
     vec_char_push_back(s->assigns, VAR_UNASSING);
     vec_char_push_back(s->polarity, sign);
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h
index 5d5d4b98..d51aed4c 100644
--- a/src/sat/satoko/types.h
+++ b/src/sat/satoko/types.h
@@ -9,62 +9,29 @@
 #ifndef satoko__types_h
 #define satoko__types_h
 
-#include "utils/fixed.h"
-#include "utils/vec/vec_dble.h"
-#include "utils/vec/vec_uint.h"
+#include "utils/sdbl.h"
+#include "utils/vec/vec_sdbl.h"
 
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-#define SATOKO_ACT_VAR_DBLE
-// #define SATOKO_ACT_VAR_FIXED
-#define SATOKO_ACT_CLAUSE_FLOAT
+/* In Satoko ABC version this file is useless */
 
-#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)
-    #define vec_act_free(vec) vec_dble_free(vec)
-    #define vec_act_size(vec) vec_dble_size(vec)
-    #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_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;
-    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)
-#endif /* SATOKO_ACT_VAR_DBLE */
+#define VAR_ACT_INIT_INC SDBL_CONST1
+#define VAR_ACT_LIMIT ABC_CONST(0x014c924d692ca61b)
+#define VAR_ACT_RESCALE 200
+typedef sdbl_t act_t;
+typedef vec_sdbl_t vec_act_t ;
+#define vec_act_alloc(size) vec_sdbl_alloc(size)
+#define vec_act_free(vec) vec_sdbl_free(vec)
+#define vec_act_size(vec) vec_sdbl_size(vec)
+#define vec_act_data(vec) vec_sdbl_data(vec)
+#define vec_act_at(vec, idx) vec_sdbl_at(vec, idx)
+#define vec_act_push_back(vec, value) vec_sdbl_push_back(vec, value)
 
-#ifdef SATOKO_ACT_CLAUSE_FLOAT
-    #define CLAUSE_ACT_INIT_INC 1.0
-    typedef float clause_act_t;
-#else
-    #define CLAUSE_ACT_INIT_INC (1 << 11)
-    typedef unsigned clause_act_t;
-#endif /* SATOKO_ACT_CLAUSE_FLOAT */
+
+#define CLAUSE_ACT_INIT_INC (1 << 11)
+typedef unsigned clause_act_t;
 
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__types_h */
diff --git a/src/sat/satoko/utils/fixed.h b/src/sat/satoko/utils/fixed.h
deleted file mode 100644
index bddd1bb4..00000000
--- a/src/sat/satoko/utils/fixed.h
+++ /dev/null
@@ -1,67 +0,0 @@
-//===--- 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 = 16;//32 - FIXED_W_BITS;
-static const int FIXED_F_MASK = 0xFFFF; //(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 = 0x10000;//(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 */
diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h
index e1611e95..8b1d8f4b 100644
--- a/src/sat/satoko/utils/heap.h
+++ b/src/sat/satoko/utils/heap.h
@@ -11,7 +11,7 @@
 
 #include "mem.h"
 #include "../types.h"
-#include "vec/vec_dble.h"
+#include "vec/vec_sdbl.h"
 #include "vec/vec_int.h"
 #include "vec/vec_uint.h"
 
diff --git a/src/sat/satoko/utils/sdbl.h b/src/sat/satoko/utils/sdbl.h
new file mode 100644
index 00000000..9f90ba02
--- /dev/null
+++ b/src/sat/satoko/utils/sdbl.h
@@ -0,0 +1,133 @@
+//===--- sdbl.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+// by Alan Mishchenko
+#ifndef satoko__utils__sdbl_h
+#define satoko__utils__sdbl_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+/*
+    The sdbl_t floating-point number is represented as a 64-bit unsigned int.
+    The number is (2^expt)*mnt, where expt is a 16-bit exponent and mnt is a
+    48-bit mantissa.  The decimal point is located between the MSB of mnt,
+    which is always 1, and the remaining 15 digits of mnt.
+
+    Currently, only positive numbers are represented.
+
+    The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111]
+    that is, the smallest possible number is 1.0 and the largest possible
+    number is 2^(---16 ones---).(1.---47 ones---)
+
+    Comparison of numbers can be done by comparing the underlying unsigned ints.
+
+    Only addition, multiplication, and division by 2^n are currently implemented.
+*/
+
+typedef word sdbl_t;
+
+static sdbl_t SDBL_CONST1 = ABC_CONST(0x0000800000000000);
+static sdbl_t SDBL_MAX = ~(sdbl_t)(0);
+
+union ui64_dbl { word ui64; double dbl; };
+
+static inline word sdbl_exp(sdbl_t a) { return a >> 48;         }
+static inline word sdbl_mnt(sdbl_t a) { return (a << 16) >> 16; }
+
+static inline double sdbl2double(sdbl_t a) {
+    union ui64_dbl temp;
+    assert(sdbl_exp(a) < 1023);
+    temp.ui64 = ((sdbl_exp(a) + 1023) << 52) | (((a << 17) >> 17) << 5);
+    return temp.dbl;
+}
+
+static inline sdbl_t double2sdbl(double value)
+{
+    union ui64_dbl temp;
+    sdbl_t expt, mnt;
+    assert(value >= 1.0);
+    temp.dbl = value;
+    expt = (temp.ui64 >> 52) - 1023;
+    mnt = SDBL_CONST1 | ((temp.ui64 << 12) >> 17);
+    return (expt << 48) + mnt;
+}
+
+static inline sdbl_t sdbl_add(sdbl_t a, sdbl_t b)
+{
+    sdbl_t expt, mnt;
+    if (a < b) {
+        a ^= b;
+        b ^= a;
+        a ^= b;
+    }
+    assert(a >= b);
+    expt = sdbl_exp(a);
+    mnt = sdbl_mnt(a) + (sdbl_mnt(b) >> (sdbl_exp(a) - sdbl_exp(b)));
+    /* Check for carry */
+    if (mnt >> 48) {
+        expt++;
+        mnt >>= 1;
+    }
+    if (expt >> 16) /* overflow */
+        return SDBL_MAX;
+    return (expt << 48) + mnt;
+}
+
+static inline sdbl_t sdbl_mult(sdbl_t a, sdbl_t b)
+{
+    sdbl_t expt, mnt;
+    sdbl_t a_mnt, a_mnt_hi, a_mnt_lo;
+    sdbl_t b_mnt, b_mnt_hi, b_mnt_lo;
+    if (a < b) {
+        a ^= b;
+        b ^= a;
+        a ^= b;
+    }
+    assert( a >= b );
+    a_mnt  = sdbl_mnt(a);
+    b_mnt  = sdbl_mnt(b);
+    a_mnt_hi = a_mnt>>32;
+    b_mnt_hi = b_mnt>>32;
+    a_mnt_lo = (a_mnt<<32)>>32;
+    b_mnt_lo = (b_mnt<<32)>>32;
+    mnt = ((a_mnt_hi * b_mnt_hi) << 17) +
+          ((a_mnt_lo * b_mnt_lo) >> 47) +
+          ((a_mnt_lo * b_mnt_hi) >> 15) +
+          ((a_mnt_hi * b_mnt_lo) >> 15);
+    expt = sdbl_exp(a) + sdbl_exp(b);
+    /* Check for carry */
+    if (mnt >> 48) {
+        expt++;
+        mnt >>= 1;
+    }
+    if (expt >> 16) /* overflow */
+        return SDBL_MAX;
+    return (expt << 48) + mnt;
+}
+
+static inline sdbl_t sdbl_div(sdbl_t a, unsigned deg2)
+{
+    if (sdbl_exp(a) >= (word)deg2)
+        return ((sdbl_exp(a) - deg2) << 48) + sdbl_mnt(a);
+    return SDBL_CONST1;
+}
+
+static inline void sdbl_test()
+{
+    sdbl_t ten100_ = ABC_CONST(0x014c924d692ca61b);
+    printf("%f\n", sdbl2double(ten100_));
+    printf("%016lX\n", double2sdbl(1 /0.95));
+    printf("%016lX\n", SDBL_CONST1);
+    printf("%f\n", sdbl2double(SDBL_CONST1));
+    printf("%f\n", sdbl2double(ABC_CONST(0x000086BCA1AF286B)));
+
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif /* satoko__utils__sdbl_h */
diff --git a/src/sat/satoko/utils/vec/vec_dble.h b/src/sat/satoko/utils/vec/vec_dble.h
deleted file mode 100755
index 50281c2a..00000000
--- a/src/sat/satoko/utils/vec/vec_dble.h
+++ /dev/null
@@ -1,246 +0,0 @@
-//===--- vec_int.h ----------------------------------------------------------===
-//
-//                     satoko: Satisfiability solver
-//
-// This file is distributed under the BSD 2-Clause License.
-// See LICENSE for details.
-//
-//===------------------------------------------------------------------------===
-#ifndef satoko__utils__vec__vec_dble_h
-#define satoko__utils__vec__vec_dble_h
-
-#include <assert.h>
-#include <stdio.h>
-#include <string.h>
-
-#include "../mem.h"
-
-#include "misc/util/abc_global.h"
-ABC_NAMESPACE_HEADER_START
-
-typedef struct vec_dble_t_ vec_dble_t;
-struct vec_dble_t_ {
-    unsigned cap;
-    unsigned size;
-    double *data;
-};
-
-//===------------------------------------------------------------------------===
-// Vector Macros
-//===------------------------------------------------------------------------===
-#define vec_dble_foreach(vec, entry, i) \
-    for (i = 0; (i < vec->size) && (((entry) = vec_dble_at(vec, i)), 1); i++)
-
-#define vec_dble_foreach_start(vec, entry, i, start) \
-    for (i = start; (i < vec_dble_size(vec)) && (((entry) = vec_dble_at(vec, i)), 1); i++)
-
-#define vec_dble_foreach_stop(vec, entry, i, stop) \
-    for (i = 0; (i < stop) && (((entry) = vec_dble_at(vec, i)), 1); i++)
-
-//===------------------------------------------------------------------------===
-// Vector API
-//===------------------------------------------------------------------------===
-static inline vec_dble_t *vec_dble_alloc(unsigned cap)
-{
-    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
-
-    if (cap > 0 && cap < 16)
-        cap = 16;
-    p->size = 0;
-    p->cap = cap;
-    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
-    return p;
-}
-
-static inline vec_dble_t *vec_dble_alloc_exact(unsigned cap)
-{
-    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
-
-    p->size = 0;
-    p->cap = cap;
-    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
-    return p;
-}
-
-static inline vec_dble_t *vec_dble_init(unsigned size, double value)
-{
-    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
-
-    p->cap = size;
-    p->size = size;
-    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
-    memset(p->data, value, sizeof(double) * p->size);
-    return p;
-}
-
-static inline void vec_dble_free(vec_dble_t *p)
-{
-    if (p->data != NULL)
-        satoko_free(p->data);
-    satoko_free(p);
-}
-
-static inline unsigned vec_dble_size(vec_dble_t *p)
-{
-    return p->size;
-}
-
-static inline void vec_dble_resize(vec_dble_t *p, unsigned new_size)
-{
-    p->size = new_size;
-    if (p->cap >= new_size)
-        return;
-    p->data = satoko_realloc(double, p->data, new_size);
-    assert(p->data != NULL);
-    p->cap = new_size;
-}
-
-static inline void vec_dble_reserve(vec_dble_t *p, unsigned new_cap)
-{
-    if (p->cap >= new_cap)
-        return;
-    p->data = satoko_realloc(double, p->data, new_cap);
-    assert(p->data != NULL);
-    p->cap = new_cap;
-}
-
-static inline unsigned vec_dble_capacity(vec_dble_t *p)
-{
-    return p->cap;
-}
-
-static inline int vec_dble_empty(vec_dble_t *p)
-{
-    return p->size ? 0 : 1;
-}
-
-static inline void vec_dble_erase(vec_dble_t *p)
-{
-    satoko_free(p->data);
-    p->size = 0;
-    p->cap = 0;
-}
-
-static inline double vec_dble_at(vec_dble_t *p, unsigned i)
-{
-    assert(i >= 0 && i < p->size);
-    return p->data[i];
-}
-
-static inline double *vec_dble_at_ptr(vec_dble_t *p, unsigned i)
-{
-    assert(i >= 0 && i < p->size);
-    return p->data + i;
-}
-
-static inline double *vec_dble_data(vec_dble_t *p)
-{
-    assert(p);
-    return p->data;
-}
-
-static inline void vec_dble_duplicate(vec_dble_t *dest, const vec_dble_t *src)
-{
-    assert(dest != NULL && src != NULL);
-    vec_dble_resize(dest, src->cap);
-    memcpy(dest->data, src->data, sizeof(double) * src->cap);
-    dest->size = src->size;
-}
-
-static inline void vec_dble_copy(vec_dble_t *dest, const vec_dble_t *src)
-{
-    assert(dest != NULL && src != NULL);
-    vec_dble_resize(dest, src->size);
-    memcpy(dest->data, src->data, sizeof(double) * src->size);
-    dest->size = src->size;
-}
-
-static inline void vec_dble_push_back(vec_dble_t *p, double value)
-{
-    if (p->size == p->cap) {
-        if (p->cap < 16)
-            vec_dble_reserve(p, 16);
-        else
-            vec_dble_reserve(p, 2 * p->cap);
-    }
-    p->data[p->size] = value;
-    p->size++;
-}
-
-static inline void vec_dble_assign(vec_dble_t *p, unsigned i, double value)
-{
-    assert((i >= 0) && (i < vec_dble_size(p)));
-    p->data[i] = value;
-}
-
-static inline void vec_dble_insert(vec_dble_t *p, unsigned i, double value)
-{
-    assert((i >= 0) && (i < vec_dble_size(p)));
-    vec_dble_push_back(p, 0);
-    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(double));
-    p->data[i] = value;
-}
-
-static inline void vec_dble_drop(vec_dble_t *p, unsigned i)
-{
-    assert((i >= 0) && (i < vec_dble_size(p)));
-    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(double));
-    p->size -= 1;
-}
-
-static inline void vec_dble_clear(vec_dble_t *p)
-{
-    p->size = 0;
-}
-
-static inline int vec_dble_asc_compare(const void *p1, const void *p2)
-{
-    const double *pp1 = (const double *) p1;
-    const double *pp2 = (const double *) p2;
-
-    if (*pp1 < *pp2)
-        return -1;
-    if (*pp1 > *pp2)
-        return 1;
-    return 0;
-}
-
-static inline int vec_dble_desc_compare(const void* p1, const void* p2)
-{
-    const double *pp1 = (const double *) p1;
-    const double *pp2 = (const double *) p2;
-
-    if (*pp1 > *pp2)
-        return -1;
-    if (*pp1 < *pp2)
-        return 1;
-    return 0;
-}
-
-static inline void vec_dble_sort(vec_dble_t* p, int ascending)
-{
-    if (ascending)
-        qsort((void *) p->data, p->size, sizeof(double),
-              (int (*)(const void*, const void*)) vec_dble_asc_compare);
-    else
-        qsort((void *) p->data, p->size, sizeof(double),
-              (int (*)(const void*, const void*)) vec_dble_desc_compare);
-}
-
-static inline long vec_dble_memory(vec_dble_t *p)
-{
-    return p == NULL ? 0 : sizeof(double) * p->cap + sizeof(vec_dble_t);
-}
-
-static inline void vec_dble_print(vec_dble_t *p)
-{
-    unsigned i;
-    assert(p != NULL);
-    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
-    for (i = 0; i < p->size; i++)
-        fprintf(stdout, " %f", p->data[i]);
-    fprintf(stdout, " }\n");
-}
-
-ABC_NAMESPACE_HEADER_END
-#endif /* satoko__utils__vec__vec_dble_h */
diff --git a/src/sat/satoko/utils/vec/vec_sdbl.h b/src/sat/satoko/utils/vec/vec_sdbl.h
new file mode 100755
index 00000000..aefd687a
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_sdbl.h
@@ -0,0 +1,247 @@
+//===--- vec_int.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_sdbl_h
+#define satoko__utils__vec__vec_sdbl_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+#include "../sdbl.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_sdbl_t_ vec_sdbl_t;
+struct vec_sdbl_t_ {
+    unsigned cap;
+    unsigned size;
+    sdbl_t *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_sdbl_foreach(vec, entry, i) \
+    for (i = 0; (i < vec->size) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
+
+#define vec_sdbl_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_sdbl_size(vec)) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
+
+#define vec_sdbl_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_sdbl_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_sdbl_t *vec_sdbl_alloc(unsigned cap)
+{
+    vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_sdbl_t *vec_sdbl_alloc_exact(unsigned cap)
+{
+    vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1);
+
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_sdbl_t *vec_sdbl_init(unsigned size, sdbl_t value)
+{
+    vec_sdbl_t* p = satoko_alloc(vec_sdbl_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(sdbl_t, p->cap) : NULL;
+    memset(p->data, value, sizeof(sdbl_t) * p->size);
+    return p;
+}
+
+static inline void vec_sdbl_free(vec_sdbl_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_sdbl_size(vec_sdbl_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_sdbl_resize(vec_sdbl_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(sdbl_t, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_sdbl_reserve(vec_sdbl_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(sdbl_t, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_sdbl_capacity(vec_sdbl_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_sdbl_empty(vec_sdbl_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_sdbl_erase(vec_sdbl_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline sdbl_t vec_sdbl_at(vec_sdbl_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data[i];
+}
+
+static inline sdbl_t *vec_sdbl_at_ptr(vec_sdbl_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data + i;
+}
+
+static inline sdbl_t *vec_sdbl_data(vec_sdbl_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_sdbl_duplicate(vec_sdbl_t *dest, const vec_sdbl_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_sdbl_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(sdbl_t) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_sdbl_copy(vec_sdbl_t *dest, const vec_sdbl_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_sdbl_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(sdbl_t) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_sdbl_push_back(vec_sdbl_t *p, sdbl_t value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_sdbl_reserve(p, 16);
+        else
+            vec_sdbl_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline void vec_sdbl_assign(vec_sdbl_t *p, unsigned i, sdbl_t value)
+{
+    assert((i >= 0) && (i < vec_sdbl_size(p)));
+    p->data[i] = value;
+}
+
+static inline void vec_sdbl_insert(vec_sdbl_t *p, unsigned i, sdbl_t value)
+{
+    assert((i >= 0) && (i < vec_sdbl_size(p)));
+    vec_sdbl_push_back(p, 0);
+    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(sdbl_t));
+    p->data[i] = value;
+}
+
+static inline void vec_sdbl_drop(vec_sdbl_t *p, unsigned i)
+{
+    assert((i >= 0) && (i < vec_sdbl_size(p)));
+    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(sdbl_t));
+    p->size -= 1;
+}
+
+static inline void vec_sdbl_clear(vec_sdbl_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_sdbl_asc_compare(const void *p1, const void *p2)
+{
+    const sdbl_t *pp1 = (const sdbl_t *) p1;
+    const sdbl_t *pp2 = (const sdbl_t *) p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_sdbl_desc_compare(const void* p1, const void* p2)
+{
+    const sdbl_t *pp1 = (const sdbl_t *) p1;
+    const sdbl_t *pp2 = (const sdbl_t *) p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_sdbl_sort(vec_sdbl_t* p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(sdbl_t),
+              (int (*)(const void*, const void*)) vec_sdbl_asc_compare);
+    else
+        qsort((void *) p->data, p->size, sizeof(sdbl_t),
+              (int (*)(const void*, const void*)) vec_sdbl_desc_compare);
+}
+
+static inline long vec_sdbl_memory(vec_sdbl_t *p)
+{
+    return p == NULL ? 0 : sizeof(sdbl_t) * p->cap + sizeof(vec_sdbl_t);
+}
+
+static inline void vec_sdbl_print(vec_sdbl_t *p)
+{
+    unsigned i;
+    assert(p != NULL);
+    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+    for (i = 0; i < p->size; i++)
+        fprintf(stdout, " %f", sdbl2double(p->data[i]));
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_sdbl_h */