diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-10 17:26:45 -0800 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-10 17:26:45 -0800 |
commit | 342d2d9f5cd3f89289d84e2dc695516ec959e252 (patch) | |
tree | 08aba0251e73be1b223c6f13bbbeca7b7dbe6528 /src/sat/satoko/utils | |
parent | d335ee096e902844b9a94076e8ce5855f74d9bde (diff) | |
download | abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.tar.gz abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.tar.bz2 abc-342d2d9f5cd3f89289d84e2dc695516ec959e252.zip |
New fixed point data type.
Expose all options to command line.
Expose search statistics to users.
Diffstat (limited to 'src/sat/satoko/utils')
-rw-r--r-- | src/sat/satoko/utils/fixed.h | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/src/sat/satoko/utils/fixed.h b/src/sat/satoko/utils/fixed.h new file mode 100644 index 00000000..91fc9b79 --- /dev/null +++ b/src/sat/satoko/utils/fixed.h @@ -0,0 +1,67 @@ +//===--- 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 = 32 - FIXED_W_BITS; +static const int FIXED_F_MASK = (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 = (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 */ |