z3-src 503.2.2

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

/*++
Copyright (c) 2017 Microsoft Corporation

Module Name:

    <name>

Abstract:

    <abstract>

Author:

    Lev Nachmanson (levnach)

Revision History:


--*/
#pragma once
#include <utility>
#include "math/lp/lp_settings.h"
#include "math/lp/lar_constraints.h"
namespace lp {
class implied_bound {
    public:
    mpq m_bound;
    // It is either the column for which the bound has been found, or,
    // in the case the column was created as
    // the slack variable to a term, it is the term index.
    // It is the same index that was returned by lar_solver::add_var(), or
    // by lar_solver::add_term()
    unsigned m_j; 
    bool m_is_lower_bound;
    bool m_strict;
    // consumer of one weighted premise: the Farkas coefficient with which the
    // constraints under the dependency enter the derivation of the bound.
    using weighted_consumer = std::function<void(mpq const&, u_dependency*)>;
    using weighted_explain = std::function<void(weighted_consumer const&)>;
    using dependency_explain = std::function<u_dependency*()>;
    private:
    dependency_explain m_explain_bound = nullptr;
    weighted_explain m_explain_weighted = nullptr;
    public:
    // s is expected to be the pointer to lp_bound_propagator.
    u_dependency* explain_implied() const { return m_explain_bound(); }
    // like explain_implied, but delivers each premise with its Farkas coefficient,
    // normalized so that the bounded column has coefficient 1.
    void explain_weighted(weighted_consumer const& consume) const { m_explain_weighted(consume); }
    void set_explain(dependency_explain f, weighted_explain w) { m_explain_bound = std::move(f); m_explain_weighted = std::move(w); }
    lconstraint_kind kind() const {
        lconstraint_kind k = m_is_lower_bound? GE : LE;
        if (m_strict)
            k = static_cast<lconstraint_kind>(k / 2);
        return k;
    }
    implied_bound() = default;
    implied_bound(const mpq & a,
                  unsigned j,
                  bool is_lower_bound,
                  bool is_strict,
                  dependency_explain get_dep,
                  weighted_explain get_weighted):
        m_bound(a),
        m_j(j),
        m_is_lower_bound(is_lower_bound),
        m_strict(is_strict),
        m_explain_bound(std::move(get_dep)),
        m_explain_weighted(std::move(get_weighted)) {
    }
};
}