diff options
Diffstat (limited to 'src/sat/satoko/utils')
| -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 |
5 files changed, 381 insertions, 314 deletions
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 */ |