z3-src 501.0.0

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
62
63
64

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    im_float_config.h

Abstract:

    Auxiliary class for testing intervals with software floats end points.

Author:

    Leonardo de Moura (leonardo) 2012-08-21.

Revision History:

--*/
#pragma once

#include "util/f2n.h"
#include "util/mpf.h"
#include "util/hwf.h"

template<typename f_manager>
class im_float_config {
    f2n<f_manager>  m_manager;
public:
    typedef f2n<f_manager>              numeral_manager;
    typedef typename f_manager::numeral numeral;

    im_float_config(f_manager & m, unsigned ebits = 11, unsigned sbits = 53):m_manager(m, ebits, sbits) {}
    
    struct interval {
        numeral   m_lower;
        numeral   m_upper;
    };

    void round_to_minus_inf() { m_manager.round_to_minus_inf(); }
    void round_to_plus_inf() { m_manager.round_to_plus_inf(); }
    void set_rounding(bool up) { m_manager.set_rounding(up); }

    // Getters
    numeral const & lower(interval const & a) const { return a.m_lower; }
    numeral const & upper(interval const & a) const { return a.m_upper; }
    numeral & lower(interval & a) { return a.m_lower; }
    numeral & upper(interval & a) { return a.m_upper; }
    bool lower_is_inf(interval const & a) const { return m_manager.m().is_ninf(a.m_lower); }
    bool upper_is_inf(interval const & a) const { return m_manager.m().is_pinf(a.m_upper); }
    bool lower_is_open(interval const & a) const { return lower_is_inf(a); }
    bool upper_is_open(interval const & a) const { return upper_is_inf(a); }

    // Setters
    void set_lower(interval & a, numeral const & n) { m_manager.set(a.m_lower, n); }
    void set_upper(interval & a, numeral const & n) { m_manager.set(a.m_upper, n); }
    void set_lower_is_open(interval & a, bool v) {}
    void set_upper_is_open(interval & a, bool v) {}
    void set_lower_is_inf(interval & a, bool v) { if (v) m_manager.m().mk_ninf(m_manager.ebits(), m_manager.sbits(), a.m_lower); }
    void set_upper_is_inf(interval & a, bool v) { if (v) m_manager.m().mk_pinf(m_manager.ebits(), m_manager.sbits(), a.m_upper); }
    
    // Reference to numeral manager
    numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); }
};