z3-src 501.0.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
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149

/*++
Copyright (c) 2017 Microsoft Corporation

Author:

    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)

--*/
#pragma once

#include "util/inf_rational.h"
#include <optional>

namespace lp_api {

    typedef int bool_var;
    typedef int theory_var;

    enum bound_kind { lower_t, upper_t };

    inline std::ostream& operator<<(std::ostream& out, bound_kind const& k) {
        switch (k) {
        case lower_t: return out << "<=";
        case upper_t: return out << ">=";
        }
        return out;
    }

    template<typename Literal>
    class bound {
        Literal          m_bv;
        theory_var       m_var;
        lp::lpvar        m_column_index;
        bool             m_is_int;
        rational         m_value;
        bound_kind       m_bound_kind;
        lp::constraint_index m_constraints[2];
        // Infinitesimal coefficient of the asserted (positive-literal) bound
        // value: the bound means  v (>=|<=) m_value + m_eps*delta.  Non-zero
        // only for the delta-rational bounds used to validate strict
        // optimization optima (e.g. a lower bound (r, -1) for a maximize
        // supremum).  Kept so get_value reports the true delta value and no
        // spurious rational fixed-variable equality is propagated to EUF.
        rational         m_eps;

    public:
        bound(Literal bv, theory_var v, lp::lpvar vi, bool is_int, rational const& val, bound_kind k, lp::constraint_index ct, lp::constraint_index cf, rational const& eps = rational::zero()) :
            m_bv(bv),
            m_var(v),
            m_column_index(vi),
            m_is_int(is_int),
            m_value(val),
            m_bound_kind(k),
            m_eps(eps) {
            m_constraints[0] = cf;
            m_constraints[1] = ct;
        }

        virtual ~bound() = default;

        theory_var get_var() const { return m_var; }

        lp::lpvar column_index() const { return m_column_index; }

        Literal get_lit() const { return m_bv; }        

        bound_kind get_bound_kind() const { return m_bound_kind; }

        bool is_int() const { return m_is_int; }

        rational const& get_value() const { return m_value; }

        bool has_infinitesimal() const { return !m_eps.is_zero(); }

        lp::constraint_index get_constraint(bool b) const { return m_constraints[b]; }

        inf_rational get_value(bool is_true) const {
            if (is_true != get_lit().sign()) 
                return inf_rational(m_value, m_eps);                  // v >= value (+ eps*delta) or v <= value (+ eps*delta)
            if (m_is_int) {
                SASSERT(m_value.is_int());
                rational const& offset = (m_bound_kind == lower_t) ? rational::minus_one() : rational::one();
                return inf_rational(m_value + offset); // v <= value - 1 or v >= value + 1
            }
            else {
                return inf_rational(m_value, m_bound_kind != lower_t);  // v <= value - epsilon or v >= value + epsilon
            }
        }

        virtual std::ostream& display(std::ostream& out) const {
            return out << m_value << "  " << get_bound_kind() << " v" << get_var();
        }
    };

    template<typename Literal>
    inline std::ostream& operator<<(std::ostream& out, bound<Literal> const& b) {
        return b.display(out);
    }


    typedef std::optional<inf_rational> opt_inf_rational;


    struct stats {
        unsigned m_assert_lower;
        unsigned m_assert_upper;
        unsigned m_bounds_propagations;
        unsigned m_num_iterations;
        unsigned m_num_iterations_with_no_progress;
        unsigned m_need_to_solve_inf;
        unsigned m_fixed_eqs;
        unsigned m_offset_eqs;
        unsigned m_conflicts;
        unsigned m_bound_propagations1;
        unsigned m_bound_propagations2;
        unsigned m_assert_diseq;
        unsigned m_assert_eq;
        unsigned m_cuts;
        unsigned m_assume_eqs;
        unsigned m_branch;
        unsigned m_bv_axioms;
        stats() { reset(); }
        void reset() {
            memset(this, 0, sizeof(*this));
        }
        void collect_statistics(statistics& st) const {
            st.update("arith-lower", m_assert_lower);
            st.update("arith-upper", m_assert_upper);
            st.update("arith-propagations", m_bounds_propagations);
            st.update("arith-iterations", m_num_iterations);
            st.update("arith-pivots", m_need_to_solve_inf);
            st.update("arith-plateau-iterations", m_num_iterations_with_no_progress);
            st.update("arith-fixed-eqs", m_fixed_eqs);
            st.update("arith-offset-eqs", m_offset_eqs);
            st.update("arith-conflicts", m_conflicts);
            st.update("arith-bound-propagations-lp", m_bound_propagations1);
            st.update("arith-bound-propagations-cheap", m_bound_propagations2);
            st.update("arith-diseq", m_assert_diseq);
            st.update("arith-eq",    m_assert_eq);
            st.update("arith-cuts", m_cuts);
            st.update("arith-assume-eqs", m_assume_eqs);
            st.update("arith-branch", m_branch);
            st.update("arith-bv-axioms", m_bv_axioms);
        }
    };


}