11 files changed, 1782 insertions, 0 deletions

diff --git a/src/sat/satoko/utils/b_queue.h b/src/sat/satoko/utils/b_queue.h
new file mode 100644
index 00000000..b9b62676
--- /dev/null
+++ b/src/sat/satoko/utils/b_queue.h
@@ -0,0 +1,81 @@
+//===--- b_queue.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__b_queue_h
+#define satoko__utils__b_queue_h
+
+#include "mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/* Bounded Queue */
+typedef struct b_queue_t_ b_queue_t;
+struct b_queue_t_ {
+    unsigned size;
+    unsigned cap;
+    unsigned i_first;
+    unsigned i_empty;
+    unsigned long sum;
+    unsigned *data;
+};
+
+//===------------------------------------------------------------------------===
+// Bounded Queue API
+//===------------------------------------------------------------------------===
+static inline b_queue_t *b_queue_alloc(unsigned cap)
+{
+    b_queue_t *p = satoko_calloc(b_queue_t, 1);
+    p->cap = cap;
+    p->data = satoko_calloc(unsigned, cap);
+    return p;
+}
+
+static inline void b_queue_free(b_queue_t *p)
+{
+    satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline void b_queue_push(b_queue_t *p, unsigned Value)
+{
+    if (p->size == p->cap) {
+        assert(p->i_first == p->i_empty);
+        p->sum -= p->data[p->i_first];
+        p->i_first = (p->i_first + 1) % p->cap;
+    } else
+        p->size++;
+
+    p->sum += Value;
+    p->data[p->i_empty] = Value;
+    if ((++p->i_empty) == p->cap) {
+        p->i_empty = 0;
+        p->i_first = 0;
+    }
+}
+
+static inline unsigned b_queue_avg(b_queue_t *p)
+{
+    return (unsigned)(p->sum / ((unsigned long) p->size));
+}
+
+static inline unsigned b_queue_is_valid(b_queue_t *p)
+{
+    return (p->cap == p->size);
+}
+
+static inline void b_queue_clean(b_queue_t *p)
+{
+    p->i_first = 0;
+    p->i_empty = 0;
+    p->size = 0;
+    p->sum = 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__b_queue_h */
diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h
new file mode 100644
index 00000000..391b8a7e
--- /dev/null
+++ b/src/sat/satoko/utils/heap.h
@@ -0,0 +1,178 @@
+//===--- heap.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__heap_h
+#define satoko__utils__heap_h
+
+#include "mem.h"
+#include "../types.h"
+#include "vec/vec_sdbl.h"
+#include "vec/vec_int.h"
+#include "vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct heap_t_ heap_t;
+struct heap_t_ {
+    vec_int_t *indices;
+    vec_uint_t *data;
+    vec_act_t *weights;
+};
+//===------------------------------------------------------------------------===
+// Heap internal functions
+//===------------------------------------------------------------------------===
+static inline unsigned left(unsigned i) { return 2 * i + 1; }
+static inline unsigned right(unsigned i) { return (i + 1) * 2; }
+static inline unsigned parent(unsigned i) { return (i - 1) >> 1; }
+
+static inline int compare(heap_t *p, unsigned x, unsigned y)
+{
+    return vec_act_at(p->weights, x) > vec_act_at(p->weights, y);
+}
+
+static inline void heap_percolate_up(heap_t *h, unsigned i)
+{
+    unsigned x = vec_uint_at(h->data, i);
+    unsigned p = parent(i);
+
+    while (i != 0 && compare(h, x, vec_uint_at(h->data, p))) {
+        vec_uint_assign(h->data, i, vec_uint_at(h->data, p));
+        vec_int_assign(h->indices, vec_uint_at(h->data, p), (int) i);
+        i = p;
+        p = parent(p);
+    }
+    vec_uint_assign(h->data, i, x);
+    vec_int_assign(h->indices, x, (int) i);
+}
+
+static inline void heap_percolate_down(heap_t *h, unsigned i)
+{
+    unsigned x = vec_uint_at(h->data, i);
+
+    while (left(i) < vec_uint_size(h->data)) {
+        unsigned child = right(i) < vec_uint_size(h->data) &&
+                     compare(h, vec_uint_at(h->data, right(i)), vec_uint_at(h->data, left(i)))
+                   ? right(i)
+                   : left(i);
+
+        if (!compare(h, vec_uint_at(h->data, child), x))
+            break;
+
+        vec_uint_assign(h->data, i, vec_uint_at(h->data, child));
+        vec_int_assign(h->indices, vec_uint_at(h->data, i), (int) i);
+        i = child;
+    }
+    vec_uint_assign(h->data, i, x);
+    vec_int_assign(h->indices, x, (int) i);
+}
+
+//===------------------------------------------------------------------------===
+// Heap API
+//===------------------------------------------------------------------------===
+static inline heap_t *heap_alloc(vec_act_t *weights)
+{
+    heap_t *p = satoko_alloc(heap_t, 1);
+    p->weights = weights;
+    p->indices = vec_int_alloc(0);
+    p->data = vec_uint_alloc(0);
+    return p;
+}
+
+static inline void heap_free(heap_t *p)
+{
+    vec_int_free(p->indices);
+    vec_uint_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned heap_size(heap_t *p)
+{
+    return vec_uint_size(p->data);
+}
+
+static inline int heap_in_heap(heap_t *p, unsigned entry)
+{
+    return (entry < vec_int_size(p->indices)) &&
+           (vec_int_at(p->indices, entry) >= 0);
+}
+
+static inline void heap_increase(heap_t *p, unsigned entry)
+{
+    assert(heap_in_heap(p, entry));
+    heap_percolate_down(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_decrease(heap_t *p, unsigned entry)
+{
+    assert(heap_in_heap(p, entry));
+    heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_insert(heap_t *p, unsigned entry)
+{
+    if (vec_int_size(p->indices) < entry + 1) {
+        unsigned old_size = vec_int_size(p->indices);
+        unsigned i;
+        int e;
+        vec_int_resize(p->indices, entry + 1);
+        vec_int_foreach_start(p->indices, e, i, old_size)
+            vec_int_assign(p->indices, i, -1);
+    }
+    assert(!heap_in_heap(p, entry));
+    vec_int_assign(p->indices, entry, (int) vec_uint_size(p->data));
+    vec_uint_push_back(p->data, entry);
+    heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_update(heap_t *p, unsigned i)
+{
+    if (!heap_in_heap(p, i))
+        heap_insert(p, i);
+    else {
+        heap_percolate_up(p, (unsigned) vec_int_at(p->indices, i));
+        heap_percolate_down(p, (unsigned) vec_int_at(p->indices, i));
+    }
+}
+
+static inline void heap_build(heap_t *p, vec_uint_t *entries)
+{
+    int i;
+    unsigned j, entry;
+
+    vec_uint_foreach(p->data, entry, j)
+        vec_int_assign(p->indices, entry, -1);
+    vec_uint_clear(p->data);
+    vec_uint_foreach(entries, entry, j) {
+        vec_int_assign(p->indices, entry, (int) j);
+        vec_uint_push_back(p->data, entry);
+    }
+    for ((i = vec_uint_size(p->data) / 2 - 1); i >= 0; i--)
+        heap_percolate_down(p, (unsigned) i);
+}
+
+static inline void heap_clear(heap_t *p)
+{
+    vec_int_clear(p->indices);
+    vec_uint_clear(p->data);
+}
+
+static inline unsigned heap_remove_min(heap_t *p)
+{
+    unsigned x = vec_uint_at(p->data, 0);
+    vec_uint_assign(p->data, 0, vec_uint_at(p->data, vec_uint_size(p->data) - 1));
+    vec_int_assign(p->indices, vec_uint_at(p->data, 0), 0);
+    vec_int_assign(p->indices, x, -1);
+    vec_uint_pop_back(p->data);
+    if (vec_uint_size(p->data) > 1)
+        heap_percolate_down(p, 0);
+    return x;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__heap_h */
diff --git a/src/sat/satoko/utils/mem.h b/src/sat/satoko/utils/mem.h
new file mode 100755
index 00000000..5ff9873d
--- /dev/null
+++ b/src/sat/satoko/utils/mem.h
@@ -0,0 +1,23 @@
+//===--- mem.h --------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__mem_h
+#define satoko__utils__mem_h
+
+#include <stdlib.h>
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define satoko_alloc(type, n_elements) ((type *) malloc((n_elements) * sizeof(type)))
+#define satoko_calloc(type, n_elements) ((type *) calloc((n_elements), sizeof(type)))
+#define satoko_realloc(type, ptr, n_elements) ((type *) realloc(ptr, (n_elements) * sizeof(type)))
+#define satoko_free(p) do { free(p); p = NULL; } while(0)
+
+ABC_NAMESPACE_HEADER_END
+#endif
diff --git a/src/sat/satoko/utils/misc.h b/src/sat/satoko/utils/misc.h
new file mode 100755
index 00000000..7205a096
--- /dev/null
+++ b/src/sat/satoko/utils/misc.h
@@ -0,0 +1,35 @@
+//===--- misc.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__misc_h
+#define satoko__utils__misc_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define stk_swap(type, a, b)  { type t = a; a = b; b = t; }
+
+static inline unsigned stk_uint_max(unsigned a, unsigned b)
+{
+    return a > b ?  a : b;
+}
+
+static inline int stk_uint_compare(const void *p1, const void *p2)
+{
+    const unsigned pp1 = *(const unsigned *)p1;
+    const unsigned pp2 = *(const unsigned *)p2;
+
+    if (pp1 < pp2)
+        return -1;
+    if (pp1 > pp2)
+        return 1;
+    return 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__misc_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/sort.h b/src/sat/satoko/utils/sort.h
new file mode 100644
index 00000000..285f4b91
--- /dev/null
+++ b/src/sat/satoko/utils/sort.h
@@ -0,0 +1,65 @@
+//===--- sort.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__sort_h
+#define satoko__utils__sort_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+static inline void select_sort(void **data, unsigned size,
+                   int (*comp_fn)(const void *, const void *))
+{
+    unsigned i, j, i_best;
+    void *temp;
+
+    for (i = 0; i < (size - 1); i++) {
+        i_best = i;
+        for (j = i + 1; j < size; j++) {
+            if (comp_fn(data[j], data[i_best]))
+                i_best = j;
+        }
+        temp = data[i];
+        data[i] = data[i_best];
+        data[i_best] = temp;
+    }
+}
+
+static void satoko_sort(void **data, unsigned size,
+            int (*comp_fn)(const void *, const void *))
+{
+    if (size <= 15)
+        select_sort(data, size, comp_fn);
+    else {
+        void *pivot = data[size / 2];
+        void *temp;
+        unsigned j = size;
+        int i = -1;
+
+        for (;;) {
+            do {
+                i++;
+            } while (comp_fn(data[i], pivot));
+            do {
+                j--;
+            } while (comp_fn(pivot, data[j]));
+
+            if ((unsigned) i >= j)
+                break;
+
+            temp = data[i];
+            data[i] = data[j];
+            data[j] = temp;
+        }
+        satoko_sort(data, (unsigned) i, comp_fn);
+        satoko_sort(data + i, (size - (unsigned) i), comp_fn);
+    }
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__sort_h */
diff --git a/src/sat/satoko/utils/vec/vec_char.h b/src/sat/satoko/utils/vec/vec_char.h
new file mode 100644
index 00000000..7d5732ec
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_char.h
@@ -0,0 +1,260 @@
+//===--- vec_char.h ---------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_char_h
+#define satoko__utils__vec__vec_char_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_char_t_ vec_char_t;
+struct vec_char_t_ {
+    unsigned cap;
+    unsigned size;
+    char *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_char_foreach(vec, entry, i) \
+    for (i = 0; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_char_t * vec_char_alloc(unsigned cap)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_char_t * vec_char_alloc_exact(unsigned cap)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    cap = 0;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(char, p->cap ) : NULL;
+    return p;
+}
+
+static inline vec_char_t * vec_char_init(unsigned size, char value)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+    memset(p->data, value, sizeof(char) * p->size);
+    return p;
+}
+
+static inline void vec_char_free(vec_char_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_char_size(vec_char_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_char_resize(vec_char_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(char, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_char_shrink(vec_char_t *p, unsigned new_size)
+{
+    assert(p->cap > new_size);
+    p->size = new_size;
+}
+
+static inline void vec_char_reserve(vec_char_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(char, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_char_capacity(vec_char_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_char_empty(vec_char_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_char_erase(vec_char_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline char vec_char_at(vec_char_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data[idx];
+}
+
+static inline char * vec_char_at_ptr(vec_char_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data + idx;
+}
+
+static inline char * vec_char_data(vec_char_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_char_duplicate(vec_char_t *dest, const vec_char_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_char_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(char) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_char_copy(vec_char_t *dest, const vec_char_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_char_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(char) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_char_push_back(vec_char_t *p, char value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_char_reserve(p, 16);
+        else
+            vec_char_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline char vec_char_pop_back(vec_char_t *p)
+{
+    assert(p && p->size);
+    return p->data[--p->size];
+}
+
+static inline void vec_char_assign(vec_char_t *p, unsigned idx, char value)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    p->data[idx] = value;
+}
+
+static inline void vec_char_insert(vec_char_t *p, unsigned idx, char value)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    vec_char_push_back(p, 0);
+    memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(char));
+    p->data[idx] = value;
+}
+
+static inline void vec_char_drop(vec_char_t *p, unsigned idx)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(char));
+    p->size -= 1;
+}
+
+static inline void vec_char_clear(vec_char_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_char_asc_compare(const void *p1, const void *p2)
+{
+    const char *pp1 = (const char *)p1;
+    const char *pp2 = (const char *)p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_char_desc_compare(const void *p1, const void *p2)
+{
+    const char *pp1 = (const char *)p1;
+    const char *pp2 = (const char *)p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_char_sort(vec_char_t *p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(char),
+              (int (*)(const void *, const void *)) vec_char_asc_compare);
+    else
+        qsort((void*) p->data, p->size, sizeof(char),
+              (int (*)(const void *, const void *)) vec_char_desc_compare);
+}
+
+
+static inline long vec_char_memory(vec_char_t *p)
+{
+    return p == NULL ? 0 : sizeof(char) * p->cap + sizeof(vec_char_t);
+}
+
+static inline void vec_char_print(vec_char_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, " %d", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_char_h */
diff --git a/src/sat/satoko/utils/vec/vec_flt.h b/src/sat/satoko/utils/vec/vec_flt.h
new file mode 100644
index 00000000..d7c896d9
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_flt.h
@@ -0,0 +1,246 @@
+//===--- 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_flt_h
+#define satoko__utils__vec__vec_flt_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_flt_t_ vec_flt_t;
+struct vec_flt_t_ {
+    unsigned cap;
+    unsigned size;
+    float *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_flt_foreach(vec, entry, i) \
+    for (i = 0; (i < vec->size) && (((entry) = vec_flt_at(vec, i)), 1); i++)
+
+#define vec_flt_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_flt_size(vec)) && (((entry) = vec_flt_at(vec, i)), 1); i++)
+
+#define vec_flt_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_flt_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_flt_t *vec_flt_alloc(unsigned cap)
+{
+    vec_flt_t* p = satoko_alloc(vec_flt_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(float, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_flt_t *vec_flt_alloc_exact(unsigned cap)
+{
+    vec_flt_t* p = satoko_alloc(vec_flt_t, 1);
+
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(float, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_flt_t *vec_flt_init(unsigned size, float value)
+{
+    vec_flt_t* p = satoko_alloc(vec_flt_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(float, p->cap) : NULL;
+    memset(p->data, value, sizeof(float) * p->size);
+    return p;
+}
+
+static inline void vec_flt_free(vec_flt_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_flt_size(vec_flt_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_flt_resize(vec_flt_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(float, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_flt_reserve(vec_flt_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(float, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_flt_capacity(vec_flt_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_flt_empty(vec_flt_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_flt_erase(vec_flt_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline float vec_flt_at(vec_flt_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data[i];
+}
+
+static inline float *vec_flt_at_ptr(vec_flt_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data + i;
+}
+
+static inline float *vec_flt_data(vec_flt_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_flt_duplicate(vec_flt_t *dest, const vec_flt_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_flt_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(float) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_flt_copy(vec_flt_t *dest, const vec_flt_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_flt_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(float) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_flt_push_back(vec_flt_t *p, float value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_flt_reserve(p, 16);
+        else
+            vec_flt_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline void vec_flt_assign(vec_flt_t *p, unsigned i, float value)
+{
+    assert((i >= 0) && (i < vec_flt_size(p)));
+    p->data[i] = value;
+}
+
+static inline void vec_flt_insert(vec_flt_t *p, unsigned i, float value)
+{
+    assert((i >= 0) && (i < vec_flt_size(p)));
+    vec_flt_push_back(p, 0);
+    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(float));
+    p->data[i] = value;
+}
+
+static inline void vec_flt_drop(vec_flt_t *p, unsigned i)
+{
+    assert((i >= 0) && (i < vec_flt_size(p)));
+    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(float));
+    p->size -= 1;
+}
+
+static inline void vec_flt_clear(vec_flt_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_flt_asc_compare(const void *p1, const void *p2)
+{
+    const float *pp1 = (const float *) p1;
+    const float *pp2 = (const float *) p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_flt_desc_compare(const void* p1, const void* p2)
+{
+    const float *pp1 = (const float *) p1;
+    const float *pp2 = (const float *) p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_flt_sort(vec_flt_t* p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(float),
+              (int (*)(const void*, const void*)) vec_flt_asc_compare);
+    else
+        qsort((void *) p->data, p->size, sizeof(float),
+              (int (*)(const void*, const void*)) vec_flt_desc_compare);
+}
+
+static inline long vec_flt_memory(vec_flt_t *p)
+{
+    return p == NULL ? 0 : sizeof(float) * p->cap + sizeof(vec_flt_t);
+}
+
+static inline void vec_flt_print(vec_flt_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_flt_h */
diff --git a/src/sat/satoko/utils/vec/vec_int.h b/src/sat/satoko/utils/vec/vec_int.h
new file mode 100755
index 00000000..75c5d134
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_int.h
@@ -0,0 +1,240 @@
+//===--- 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_int_h
+#define satoko__utils__vec__vec_int_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_int_t_ vec_int_t;
+struct vec_int_t_ {
+    unsigned cap;
+    unsigned size;
+    int *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_int_foreach(vec, entry, i) \
+    for (i = 0; (i < vec->size) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_int_size(vec)) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_int_t *vec_int_alloc(unsigned cap)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_int_t *vec_int_alloc_exact(unsigned cap)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_int_t *vec_int_init(unsigned size, int value)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    memset(p->data, value, sizeof(int) * p->size);
+    return p;
+}
+
+static inline void vec_int_free(vec_int_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_int_size(vec_int_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_int_resize(vec_int_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(int, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_int_reserve(vec_int_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(int, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_int_capacity(vec_int_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_int_empty(vec_int_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_int_erase(vec_int_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline int vec_int_at(vec_int_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data[i];
+}
+
+static inline int *vec_int_at_ptr(vec_int_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data + i;
+}
+
+static inline void vec_int_duplicate(vec_int_t *dest, const vec_int_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_int_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(int) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_int_copy(vec_int_t *dest, const vec_int_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_int_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(int) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_int_push_back(vec_int_t *p, int value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_int_reserve(p, 16);
+        else
+            vec_int_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline void vec_int_assign(vec_int_t *p, unsigned i, int value)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    p->data[i] = value;
+}
+
+static inline void vec_int_insert(vec_int_t *p, unsigned i, int value)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    vec_int_push_back(p, 0);
+    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(int));
+    p->data[i] = value;
+}
+
+static inline void vec_int_drop(vec_int_t *p, unsigned i)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(int));
+    p->size -= 1;
+}
+
+static inline void vec_int_clear(vec_int_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_int_asc_compare(const void *p1, const void *p2)
+{
+    const int *pp1 = (const int *) p1;
+    const int *pp2 = (const int *) p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_int_desc_compare(const void* p1, const void* p2)
+{
+    const int *pp1 = (const int *) p1;
+    const int *pp2 = (const int *) p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_int_sort(vec_int_t* p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(int),
+              (int (*)(const void*, const void*)) vec_int_asc_compare);
+    else
+        qsort((void *) p->data, p->size, sizeof(int),
+              (int (*)(const void*, const void*)) vec_int_desc_compare);
+}
+
+static inline long vec_int_memory(vec_int_t *p)
+{
+    return p == NULL ? 0 : sizeof(int) * p->cap + sizeof(vec_int_t);
+}
+
+static inline void vec_int_print(vec_int_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, " %d", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_int_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..ec1c731c
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_sdbl.h
@@ -0,0 +1,253 @@
+//===--- 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_shrink(vec_sdbl_t *p, unsigned new_size)
+{
+    assert(new_size <= p->cap);
+    p->size = new_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 */
diff --git a/src/sat/satoko/utils/vec/vec_uint.h b/src/sat/satoko/utils/vec/vec_uint.h
new file mode 100755
index 00000000..e6719ca3
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_uint.h
@@ -0,0 +1,268 @@
+//===--- vec_uint.h ---------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_uint_h
+#define satoko__utils__vec__vec_uint_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_uint_t_ vec_uint_t;
+struct vec_uint_t_ {
+    unsigned cap;
+    unsigned size;
+    unsigned* data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_uint_foreach(vec, entry, i) \
+    for (i = 0; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_uint_t * vec_uint_alloc(unsigned cap)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_uint_t * vec_uint_alloc_exact(unsigned cap)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    cap = 0;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+    return p;
+}
+
+static inline vec_uint_t * vec_uint_init(unsigned size, unsigned value)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+    memset(p->data, value, sizeof(unsigned) * p->size);
+    return p;
+}
+
+static inline void vec_uint_free(vec_uint_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_uint_size(vec_uint_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_uint_resize(vec_uint_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(unsigned, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_uint_shrink(vec_uint_t *p, unsigned new_size)
+{
+    assert(p->cap >= new_size);
+    p->size = new_size;
+}
+
+static inline void vec_uint_reserve(vec_uint_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(unsigned, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_uint_capacity(vec_uint_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_uint_empty(vec_uint_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_uint_erase(vec_uint_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline unsigned vec_uint_at(vec_uint_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data[idx];
+}
+
+static inline unsigned * vec_uint_at_ptr(vec_uint_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data + idx;
+}
+
+static inline unsigned vec_uint_find(vec_uint_t *p, unsigned entry)
+{
+    unsigned i;
+    for (i = 0; i < p->size; i++)
+        if (p->data[i] == entry)
+            return 1;
+    return 0;
+}
+
+static inline unsigned * vec_uint_data(vec_uint_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_uint_duplicate(vec_uint_t *dest, const vec_uint_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_uint_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(unsigned) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_uint_copy(vec_uint_t *dest, const vec_uint_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_uint_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(unsigned) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_uint_push_back(vec_uint_t *p, unsigned value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_uint_reserve(p, 16);
+        else
+            vec_uint_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline unsigned vec_uint_pop_back(vec_uint_t *p)
+{
+    assert(p && p->size);
+    return p->data[--p->size];
+}
+
+static inline void vec_uint_assign(vec_uint_t *p, unsigned idx, unsigned value)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    p->data[idx] = value;
+}
+
+static inline void vec_uint_insert(vec_uint_t *p, unsigned idx, unsigned value)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    vec_uint_push_back(p, 0);
+    memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(unsigned));
+    p->data[idx] = value;
+}
+
+static inline void vec_uint_drop(vec_uint_t *p, unsigned idx)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(unsigned));
+    p->size -= 1;
+}
+
+static inline void vec_uint_clear(vec_uint_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_uint_asc_compare(const void *p1, const void *p2)
+{
+    const unsigned *pp1 = (const unsigned *) p1;
+    const unsigned *pp2 = (const unsigned *) p2;
+
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+static inline int vec_uint_desc_compare(const void *p1, const void *p2)
+{
+    const unsigned *pp1 = (const unsigned *) p1;
+    const unsigned *pp2 = (const unsigned *) p2;
+
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 )
+        return 1;
+    return 0;
+}
+
+static inline void vec_uint_sort(vec_uint_t *p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(unsigned),
+              (int (*)(const void *, const void *)) vec_uint_asc_compare);
+    else
+        qsort((void*) p->data, p->size, sizeof(unsigned),
+              (int (*)(const void *, const void *)) vec_uint_desc_compare);
+}
+
+static inline long vec_uint_memory(vec_uint_t *p)
+{
+    return p == NULL ? 0 : sizeof(unsigned) * p->cap + sizeof(vec_uint_t);
+}
+
+static inline void vec_uint_print(vec_uint_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, " %u", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_uint_h */