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
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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    bound_manager.h

Abstract:

    Collect bounds.

Author:

    Leonardo (leonardo) 2011-05-16

Notes:

--*/
#pragma once

#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"


class bound_manager {
public:
    typedef rational     numeral;
private:
    typedef std::pair<numeral, bool> limit;
    arith_util           m_util;
    obj_map<expr, limit> m_lowers;
    obj_map<expr, limit> m_uppers;
    obj_map<expr, expr_dependency*> m_lower_deps;
    obj_map<expr, expr_dependency*> m_upper_deps;
    expr_ref_vector     m_bounded_vars;
    bool is_disjunctive_bound(expr * f, expr_dependency * d);
    bool is_equality_bound(expr * f, expr_dependency * d);
    bool is_numeral(expr* v, rational& n, bool& is_int);
    void insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d);
    void insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d);
public:
    static decl_kind neg(decl_kind k);
    static void norm(numeral & n, decl_kind & k);

    bound_manager(ast_manager & m);
    ~bound_manager();
    
    bound_manager* translate(ast_manager& dst_m);
    void translate(bound_manager const& src, ast_translation& tr);

    ast_manager & m() const { return m_util.get_manager(); }
    
    void operator()(expr * n, expr_dependency * d, proof* p);
    
    bool has_lower(expr * c, numeral & v, bool & strict) const {
        limit l;
        if (m_lowers.find(c, l)) {
            v = l.first;
            strict = l.second;
            return true;
        }
        return false;
    }

    bool has_upper(expr * c, numeral & v, bool & strict) const {
        limit l;
        if (m_uppers.find(c, l)) {
            v = l.first;
            strict = l.second;
            return true;
        }
        return false;
    }

    expr_dependency * lower_dep(expr * c) const {
        expr_dependency * d;
        if (m_lower_deps.find(c, d))
            return d;
        return nullptr;
    }

    expr_dependency * upper_dep(expr * c) const {
        expr_dependency * d;
        if (m_upper_deps.find(c, d))
            return d;
        return nullptr;
    }

    bool inconsistent() const;
    
    bool has_lower(expr * c) const {
        return m_lowers.contains(c);
    }

    bool has_upper(expr * c) const {
        return m_uppers.contains(c);
    }
    
    typedef ptr_vector<expr>::const_iterator iterator;
    
    /**
       \brief Iterator for all bounded constants.
    */
    iterator begin() const { return m_bounded_vars.begin(); }
    iterator end() const { return m_bounded_vars.end(); }
    
    void reset();

    // for debugging purposes
    void display(std::ostream & out) const;
};