opensmt/src/common/FastInteger.cc at 8118e1659346af3fe9cebfabb4f1dfb273130a9a · usi-verification-and-security/opensmt · GitHub

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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
#include "FastInteger.h"

namespace opensmt {
FastInteger::FastInteger(const char* str, const int base) : FastRational(str, base) {
    assert(isInteger());
}

FastInteger gcd(FastInteger const & a, FastInteger const & b)
{
    assert(a.isInteger() and b.isInteger());
    if (a.wordPartValid() && b.wordPartValid()) {
        // Refers to FastRational.h:gcd
        return FastInteger(gcd(a.num, b.num));
    }
    else {
        a.ensure_mpq_valid();
        b.ensure_mpq_valid();
        mpz_gcd(FastInteger::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq));
        return FastInteger(FastInteger::mpz());
    }
}

FastInteger lcm(FastInteger const & a, FastInteger const & b)
{
    assert(a.isInteger() and b.isInteger());
    if (a.wordPartValid() && b.wordPartValid()) {
        // Refers to FastRational.h:lcm
        return lcm(a.num, b.num);
    }
    else {
        a.ensure_mpq_valid();
        b.ensure_mpq_valid();
        mpz_lcm(FastInteger::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq));
        return FastInteger(FastInteger::mpz());
    }
}

// The quotient of n and d using the fast rationals.
// Divide n by d, forming a quotient q.
// Rounds q down towards -infinity, and q will satisfy n = q*d + r for some 0 <= abs(r) <= abs(d)
FastInteger fastint_fdiv_q(FastInteger const & n, FastInteger const & d) {
    assert(n.isInteger() && d.isInteger());
    if (n.wordPartValid() && d.wordPartValid()) {
        word num = n.num;
        word den = d.num;
        word quo;
        if (num == INT_MIN) // The abs is guaranteed to overflow.  Otherwise this is always fine
            goto overflow;
        // After this -INT_MIN+1 <= numerator <= INT_MAX, and therefore the result always fits into a word.
        quo = num / den;
        if (num % den != 0 && ((num < 0 && den >=0) || (den < 0 && num >= 0))) // The result should be negative
            quo--; // INT_MAX-1 >= quo >= -INT_MIN

        return quo;
    }
overflow:
    n.ensure_mpq_valid();
    d.ensure_mpq_valid();
    mpz_fdiv_q(FastInteger::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq));
    return FastInteger(FastInteger::mpz());
}

//void mpz_divexact (mpz_ptr, mpz_srcptr, mpz_srcptr);
FastInteger divexact(FastInteger const & n, FastInteger const & d) {
    assert(d != 0);
    assert(n.isInteger() && d.isInteger());
    if (n.wordPartValid() && d.wordPartValid()) {
        word num = n.num;
        word den = d.num;
        word quo;
        if (den != 0){
            quo = num / den;
            return quo;
        }
        else {
            // Division by zero
            assert(false);
            return FastInteger(0);
        }
    } else {
        assert(n.mpqPartValid() || d.mpqPartValid());
        n.ensure_mpq_valid();
        d.ensure_mpq_valid();
        mpz_divexact(FastInteger::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq));
        return FastInteger(FastInteger::mpz());
    }
}
}