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
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    opt_solver.h

Abstract:

    Wraps smt::kernel as a solver for optimization

Author:

    Anh-Dung Phan (t-anphan) 2013-10-16

Notes:

    Based directly on smt_solver.
   
--*/
#pragma once

#include "opt/opt_search.h"
#include "ast/ast.h"
#include "util/params.h"
#include "solver/solver_na2as.h"
#include "smt/smt_kernel.h"
#include "params/smt_params.h"
#include "smt/smt_types.h"
#include "smt/theory_opt.h"
#include "ast/converters/generic_model_converter.h"

class arith_util;

namespace opt {

    // Extract from a model value of an objective term a rational bound on it:
    // the value itself when it is a rational numeral, otherwise, for an
    // irrational algebraic value (e.g. sqrt(2) for an objective pinned by
    // x^2 = 2), the requested side of its isolating interval.
    bool model_value_bound(arith_util& a, expr* val, bool lower, rational& n);

    // Adjust bound bound |-> m_offset + (m_negate?-1:1)*bound
    class adjust_value {
        rational m_offset;
        bool     m_negate;
    public:
        adjust_value(rational const& offset, bool neg):
            m_offset(offset),
            m_negate(neg)
        {}
        adjust_value(): m_offset(0), m_negate(false) {}
        void set_offset(rational const& o) { m_offset = o; }
        void set_negate(bool neg) { m_negate = neg; }
        rational const& get_offset() const { return m_offset; }
        void add_offset(rational const& o) { if (m_negate) m_offset -= o; else m_offset += o; }
        bool get_negate() const { return m_negate; }
        inf_eps operator()(inf_eps const& r) const {
            inf_eps result = r;
            if (m_negate) result.neg();
            result += m_offset;
            return result;
        }
        objective_value operator()(objective_value const& r) const {
            return r.adjusted(m_offset, m_negate);
        }
        rational operator()(rational const& r) const {
            rational result = r;
            if (m_negate) result.neg();
            result += m_offset;
            return result;
        }
    };


    class opt_solver : public solver_na2as {
    private:
        smt_params          m_params;
        smt::kernel         m_context;
        ast_manager&        m;
        generic_model_converter& m_fm;
        progress_callback * m_callback;
        symbol              m_logic;
        model_ref           m_model;
        svector<smt::theory_var>  m_objective_vars;
        vector<inf_eps>     m_objective_values;
        sref_vector<model>  m_objective_models;
        expr_ref_vector     m_objective_terms;
        bool                m_dump_benchmarks;
        static unsigned     m_dump_count;
        statistics          m_stats;
        bool                m_first;
        bool                m_was_unknown;
        unsigned            m_dual_bound_rlimit;
        unsigned            m_dual_bound_checks = 0;
        unsigned            m_dual_bound_refutations = 0;
    public:
        opt_solver(ast_manager & m, params_ref const & p, generic_model_converter& fm);

        solver* translate(ast_manager& m, params_ref const& p) override;
        void updt_params(params_ref const& p) override;
        void collect_param_descrs(param_descrs & r) override;
        void collect_statistics_core(statistics & st) const override;
        void assert_expr_core(expr * t) override;
        void push_core() override;
        void pop_core(unsigned n) override;
        lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override;
        void get_unsat_core(expr_ref_vector & r) override;
        void get_model_core(model_ref & _m) override;
        proof * get_proof_core() override;
        std::string reason_unknown() const override;
        void set_reason_unknown(char const* msg) override;
        void get_labels(svector<symbol> & r) override;
        void set_progress_callback(progress_callback * callback) override;
        unsigned get_num_assertions() const override;
        expr * get_assertion(unsigned idx) const override;
        ast_manager& get_manager() const override { return m; }
        lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
        lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override;
        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
        expr_ref_vector get_trail(unsigned max_level) override { return m_context.get_trail(max_level); }
        expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
        expr* congruence_root(expr* e) override { return e; }
        expr* congruence_next(expr* e) override { return e; }
        expr_ref congruence_explain(expr* a, expr* b) override { return expr_ref(m.mk_eq(a, b), m); }
        void set_phase(expr* e) override { m_context.set_phase(e); }
        phase* get_phase() override { return m_context.get_phase(); }
        void set_phase(phase* p) override { m_context.set_phase(p); }
        void move_to_front(expr* e) override { m_context.move_to_front(e); }
        void user_propagate_initialize_value(expr* var, expr* value) override { m_context.user_propagate_initialize_value(var, value); }
        void user_propagate_init(void *ctx, user_propagator::push_eh_t &push_eh, user_propagator::pop_eh_t &pop_eh, user_propagator::fresh_eh_t &fresh_eh) override {
            m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
            m_first = false;
        }

        void user_propagate_register_fixed(user_propagator::fixed_eh_t &fixed_eh) override {
            m_context.user_propagate_register_fixed(fixed_eh);
        }

        void user_propagate_register_final(user_propagator::final_eh_t &final_eh) override {
            m_context.user_propagate_register_final(final_eh);
        }

        void user_propagate_register_eq(user_propagator::eq_eh_t &eq_eh) override {
            m_context.user_propagate_register_eq(eq_eh);
        }

        void user_propagate_register_diseq(user_propagator::eq_eh_t &diseq_eh) override {
            m_context.user_propagate_register_diseq(diseq_eh);
        }

        void user_propagate_register_expr(expr *e) override {
            m_context.user_propagate_register_expr(e);
        }

        void user_propagate_register_created(user_propagator::created_eh_t &r) override {
            m_context.user_propagate_register_created(r);   
        }

        void user_propagate_register_decide(user_propagator::decide_eh_t &r) override {
            m_context.user_propagate_register_decide(r);
        }

        void user_propagate_register_on_binding(user_propagator::binding_eh_t &r) override {
            m_context.user_propagate_register_on_binding(r);
        }

         void user_propagate_clear() override {
        }

        void register_on_clause(void *, user_propagator::on_clause_eh_t &r) override {
            m_context.register_on_clause(nullptr, r);
        }

        void set_logic(symbol const& logic);

        smt::theory_var add_objective(app* term);
        void reset_objectives();
        maximize_result maximize_objective(unsigned i, expr_ref& blocker, bool dual_bounds = false, bool probe_bound = true);
        bool maximize_objectives1(expr_ref_vector& blockers);
        bool maximize_objective_isolated(unsigned i, model_ref& baseline_model, expr_ref& blocker);
        void update_from_baseline_model(unsigned i, model_ref& baseline_model, expr_ref& blocker);
        inf_eps const & saved_objective_value(unsigned obj_index);
        inf_eps current_objective_value(unsigned obj_index);
        model* get_model_idx(unsigned obj_index) { return m_objective_models[obj_index]; }

        bool was_unknown() const { return m_was_unknown; }

        vector<inf_eps> const& get_objective_values();
        expr_ref mk_ge(unsigned obj_index, inf_eps const& val);

        static opt_solver& to_opt(solver& s);
        bool dump_benchmarks();

        smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
        void ensure_pb();
        
        smt::theory_opt& get_optimizer();

        void to_smt2_benchmark(std::ofstream & buffer, 
                               unsigned num_assumptions, expr * const * assumptions,
                               char const * name = "benchmarks", 
                               symbol const& logic = symbol::null, char const * status = "unknown", char const * attributes = "");

    private:
        lbool check_upper_bound(unsigned i, rational const& value);
        lbool bound_value(unsigned i, inf_eps& val);
        void set_model(unsigned i);
        lbool adjust_result(lbool r);
    };
}