z3-src 503.0.0

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

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    optsmt.h

Abstract:
   
    Objective optimization method.

Author:

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

Notes:

--*/
#pragma once

#include "opt/opt_solver.h"

namespace opt {
    /**
       Takes solver with hard constraints added.
       Returns an optimal assignment to objective functions.
    */

    class context;

    class optsmt {
        ast_manager&     m;
        context&         m_context;
        opt_solver*      m_s;
        vector<objective_value> m_lower;
        vector<objective_value> m_upper;
        app_ref_vector   m_objs;
        expr_ref_vector  m_lower_fmls;
        svector<smt::theory_var> m_vars;
        symbol           m_optsmt_engine;
        unsigned         m_bisect_rounds = 64;
        bool             m_optsmt_nlsat = true;
        bool             m_dual_bounds = true;
        unsigned         m_nlsat_supremum_rlimit = 100000;
        bool             m_lex_after_unbounded = true;
        model_ref        m_model, m_best_model;
        svector<symbol>  m_labels;
        sref_vector<model> m_models;
    public:
        optsmt(ast_manager& m, context& ctx): 
            m(m), m_context(ctx), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}

        void setup(opt_solver& solver);

        lbool box();

        lbool lex(unsigned obj_index, bool is_maximize);

        // Objective unbounded_index has the supremum +oo. Objective obj_index
        // then takes the limit of its suprema as the unbounded objective grows.
        lbool lex_after_unbounded(unsigned unbounded_index, unsigned obj_index, bool is_maximize);

        bool is_unbounded(unsigned obj_index, bool is_maximize);

        unsigned add(app* t);

        void updt_params(params_ref& p);

        unsigned get_num_objectives() const { return m_objs.size(); }
        void commit_assignment(unsigned index);
        objective_value get_lower(unsigned index) const;
        objective_value get_upper(unsigned index) const;
        // A finite, unattained limit certified by the nlsat-cell engine.
        bool    has_open_bound(unsigned index) const {
            return m_lower[index].exact_finite() && m_lower[index].has_infinitesimal();
        }
        void    get_model(model_ref& mdl, svector<symbol>& labels);
        model*  get_model(unsigned index) const { return m_models[index]; }


        void update_lower(unsigned idx, inf_eps const& r);

        void update_upper(unsigned idx, inf_eps const& r);

        void reset();

        bool can_increment_delta(vector<inf_eps> const& lower, unsigned i);

    private:

        enum class nlsat_outcome { no_result, certified, incomplete };

        inf_eps const& lower(unsigned index) const { return m_lower[index].rational_bound(); }
        inf_eps const& upper(unsigned index) const { return m_upper[index].rational_bound(); }

        lbool geometric_opt();

        lbool symba_opt();

        lbool geometric_search(unsigned idx, bool is_maximize, unsigned unbounded_check_rounds = 8);

        lbool refine_real_objective(unsigned idx, bool is_maximize, inf_eps const& hi, bool smt_gave_up);
        lbool bisect(unsigned idx, bool is_maximize, inf_eps hi);
        nlsat_outcome nlsat_cells(unsigned idx, bool is_maximize, inf_eps const& hi);
        bool prove_unbounded_above(unsigned idx, unsigned rlimit_budget);

        lbool reaches_infinity(unsigned idx, model_ref& witness);

        bool model_objective_value(unsigned idx, model_ref& mdl, rational& value);

        void publish_best_model();

        void set_best(unsigned idx, inf_eps const& v, bool is_maximize);

        void set_max(vector<objective_value>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls);

        expr_ref update_lower();

        void update_lower_lex(unsigned idx, inf_eps const& r, bool is_maximize);

    };

}