summaryrefslogtreecommitdiffstats
path: root/src/sat/satoko/utils/fixed.h
blob: 91fc9b79c2970b16db5b87991864bc3d1e81c7b6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
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 */