z3-src 503.2.1

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
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

/*++
Copyright (c) 2007 Microsoft Corporation

Module Name:

    approx_nat.cpp

Abstract:

    Approximated natural numbers. It performs operations on the set [0, ..., 2^{n-2}, huge].
    Where huge represents all numbers greater than 2^{n-2}. 

Author:

    Leonardo (leonardo) 2008-01-11

Notes:

--*/
#include "util/approx_nat.h"

approx_nat::approx_nat(unsigned val) {
    m_value = val > m_limit ? UINT_MAX : val;
}

approx_nat & approx_nat::operator=(unsigned val) {
    m_value = val > m_limit ? UINT_MAX : val;
    return *this;
}

approx_nat & approx_nat::operator+=(unsigned w) {
    if (is_huge()) 
        return *this;
    if (w > m_limit) {
        m_value = UINT_MAX;
        return *this;
    }
    m_value += w;
    if (m_value > m_limit)
        m_value = UINT_MAX;
    return *this;
}

approx_nat & approx_nat::operator*=(unsigned w) {
    if (is_huge()) 
        return *this;
    unsigned long long r = static_cast<unsigned long long>(m_value) * static_cast<unsigned long long>(w);
    if (r > m_limit)
        m_value = UINT_MAX;
    else
        m_value = static_cast<unsigned>(r);
    return *this;
}

std::ostream & operator<<(std::ostream & target, approx_nat const & w) {
    if (w.is_huge()) 
        target << "[huge]";
    else
        target << w.get_value();
    return target;
}