New fixed point data type.

Expose all options to command line.
Expose search statistics to users.

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 */