diff options
| -rw-r--r-- | src/sat/satoko/act_clause.h | 36 | ||||
| -rw-r--r-- | src/sat/satoko/act_var.h | 70 | ||||
| -rw-r--r-- | src/sat/satoko/satoko.h | 5 | ||||
| -rw-r--r-- | src/sat/satoko/solver.h | 2 | ||||
| -rw-r--r-- | src/sat/satoko/solver_api.c | 6 | ||||
| -rw-r--r-- | src/sat/satoko/types.h | 67 | ||||
| -rw-r--r-- | src/sat/satoko/utils/fixed.h | 67 | ||||
| -rw-r--r-- | src/sat/satoko/utils/heap.h | 2 | ||||
| -rw-r--r-- | src/sat/satoko/utils/sdbl.h | 133 | ||||
| -rwxr-xr-x | src/sat/satoko/utils/vec/vec_dble.h | 246 | ||||
| -rwxr-xr-x | src/sat/satoko/utils/vec/vec_sdbl.h | 247 |
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 */ |