z3-src 415.4.4

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) 2016 Microsoft Corporation

Module Name:

    theory_lra.h

Abstract:

    <abstract>

Author:

    Lev Nachmanson (levnach) 2016-25-3
    Nikolaj Bjorner (nbjorner)

Revision History:


--*/
#pragma once

#include "smt/theory_opt.h"

namespace smt {
    class theory_lra : public theory, public theory_opt {
    public:
        class imp;
    private:
        imp* m_imp;

    public:
        theory_lra(context& ctx);
        ~theory_lra() override;
        theory* mk_fresh(context* new_ctx) override;
        char const* get_name() const override { return "arithmetic"; }

        void init() override;
        
        bool internalize_atom(app * atom, bool gate_ctx) override;
                                                     
        bool internalize_term(app * term) override;

        void internalize_eq_eh(app * atom, bool_var v) override;

        void assign_eh(bool_var v, bool is_true) override;

        lbool get_phase(bool_var v) override;

        void new_eq_eh(theory_var v1, theory_var v2) override;

        bool use_diseqs() const override;

        void new_diseq_eh(theory_var v1, theory_var v2) override;

        void push_scope_eh() override;

        void pop_scope_eh(unsigned num_scopes) override;

        void restart_eh() override;

        void relevant_eh(app* e) override;

        void init_search_eh() override;

        final_check_status final_check_eh() override;

        bool is_shared(theory_var v) const override;
    
        bool can_propagate() override;
        
        void propagate() override;
        
        justification * why_is_diseq(theory_var v1, theory_var v2) override;

        // virtual void flush_eh();

        void reset_eh() override;

        void apply_sort_cnstr(enode * n, sort * s) override;

        void init_model(model_generator & m) override;

        void initialize_value(expr* var, expr* value) override;
        
        model_value_proc * mk_value(enode * n, model_generator & mg) override;
        void validate_model(proto_model& mdl) override;

        bool get_value(enode* n, expr_ref& r) override;
        bool include_func_interp(func_decl* f) override;
        bool get_value(enode* n, rational& r);
        bool get_lower(enode* n, expr_ref& r);
        bool get_upper(enode* n, expr_ref& r);
        bool get_lower(enode* n, rational& r, bool& is_strict);
        bool get_upper(enode* n, rational& r, bool& is_strict);
        void solve_for(vector<solution>& s) override;
                
        void display(std::ostream & out) const override;
        
        void collect_statistics(::statistics & st) const override;

        void setup() override;

        // optimization
        expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val);
        inf_eps value(theory_var) override;
        inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) override;
        theory_var add_objective(app* term) override;
    };

}