z3-src 503.3.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
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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    pattern_inference.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2006-12-08.

Revision History:

--*/
#pragma once

#include "ast/ast.h"
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "params/pattern_inference_params.h"
#include "util/vector.h"
#include "util/uint_set.h"
#include "util/nat_set.h"
#include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h"
#include "util/map.h"
#include "ast/pattern/expr_pattern_match.h"

/**
   \brief A pattern p_1 is smaller than a pattern p_2 iff 
   every instance of p_2 is also an instance of p_1.

   Example: f(X) is smaller than f(g(X)) because
   every instance of f(g(X)) is also an instance of f(X).
*/
class smaller_pattern {
    ptr_vector<expr> m_bindings;

    typedef std::pair<expr *, expr *> expr_pair;
    typedef obj_pair_hashtable<expr, expr> cache;

    svector<expr_pair> m_todo;
    cache              m_cache;
    void save(expr * p1, expr * p2);
    bool process(expr * p1, expr * p2);

public:

    smaller_pattern & operator=(smaller_pattern const &) = delete;

    bool operator()(unsigned num_bindings, expr * p1, expr * p2);
};

class pattern_inference_cfg :  public default_rewriter_cfg {
    ast_manager&               m;
    pattern_inference_params const & m_params;
    family_id                  m_bfid;
    family_id                  m_afid;
    svector<family_id>         m_forbidden;
    obj_hashtable<func_decl>   m_preferred;        
    smaller_pattern            m_le;
    unsigned                   m_num_bindings;
    unsigned                   m_num_no_patterns;
    expr * const *             m_no_patterns;
    bool                       m_nested_arith_only;
    bool                       m_block_loop_patterns;
    bool                       m_decompose_patterns;

    struct info {
        uint_set m_free_vars;
        unsigned m_size;
        info(uint_set const & vars, unsigned size):
            m_free_vars(vars),
            m_size(size) {
        }
        info():
            m_free_vars(),
            m_size(0) {
        }
    };

    typedef obj_map<expr, info> expr2info;

    expr2info                 m_candidates_info; // candidate -> set of free vars + size
    app_ref_vector            m_candidates;

    ptr_vector<app>           m_tmp1;
    ptr_vector<app>           m_tmp2;
    ptr_vector<app>           m_todo;

    // Compare candidates patterns based on their usefulness
    // p1 < p2 if
    //  - p1 has more free variables than p2
    //  - p1 and p2 has the same number of free variables,
    //    and p1 is smaller than p2.
    struct pattern_weight_lt {
        expr2info & m_candidates_info;
        pattern_weight_lt(expr2info & i):
            m_candidates_info(i) {
        }
        bool operator()(expr * n1, expr * n2) const;
    };

    pattern_weight_lt          m_pattern_weight_lt;

    //
    // Functor for collecting candidates.
    //
    class collect {
        struct entry {
            expr *    m_node = nullptr;
            unsigned  m_delta = 0;
            entry() = default;
            entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
            unsigned hash() const { 
                return hash_u_u(m_node->get_id(), m_delta);
            }
            bool operator==(entry const & e) const { 
                return m_node == e.m_node && m_delta == e.m_delta; 
            }
        };
        
        struct info {
            uint_set    m_free_vars, m_bound_vars;
            unsigned    m_size;
            info(uint_set const & fvars, uint_set const& bvars, unsigned sz):
                m_free_vars(fvars), m_bound_vars(bvars), m_size(sz) {}
        };
        
        ast_manager &            m;
        pattern_inference_cfg &     m_owner;
        family_id                m_afid = null_family_id;
        unsigned                 m_num_bindings = 0;
        typedef map<entry, info *, obj_hash<entry>, default_eq<entry> > cache;
        cache                    m_cache;
        ptr_vector<info>         m_info;
        svector<entry>           m_todo;

        void visit(expr * n, unsigned delta, bool & visited);
        bool visit_children(expr * n, unsigned delta);
        void save(expr * n, unsigned delta, info * i);
        void save_candidate(expr * n, unsigned delta);
        void reset();
    public:
        collect(ast_manager & m, pattern_inference_cfg & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
        void operator()(expr * n, unsigned num_bindings);
    };

    collect                    m_collect;
    
    void add_candidate(app * n, uint_set const & s, unsigned size);

    void filter_looping_patterns(ptr_vector<app> & result);

    bool has_preferred_patterns(ptr_vector<app> & candidate_patterns, app_ref_buffer & result);

    void filter_bigger_patterns(ptr_vector<app> const & patterns, ptr_vector<app> & result);

    class contains_subpattern {
        pattern_inference_cfg & m_owner;
        nat_set              m_already_processed; 
        ptr_vector<expr>     m_todo;
        void save(expr * n);
    public:
        contains_subpattern(pattern_inference_cfg & owner):
            m_owner(owner) {}
        bool operator()(expr * n);
    };

    contains_subpattern        m_contains_subpattern;
        
    bool contains_subpattern(expr * n);
    
    struct pre_pattern {
        ptr_vector<app>  m_exprs;     // elements of the pattern.
        uint_set         m_free_vars; // set of free variables in m_exprs
        unsigned         m_idx;       // idx of the next candidate to process.
        pre_pattern():
            m_idx(0) {
        }
    };

    ptr_vector<pre_pattern>      m_pre_patterns;
    expr_pattern_match           m_database;

    ptr_buffer<app> m_args;
    app* mk_pattern(app* candidate);

    void candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
                                   ptr_vector<app> & remaining_candidate_patterns,
                                   app_ref_buffer & result);
    
    void candidates2multi_patterns(unsigned max_num_patterns, 
                                   ptr_vector<app> const & candidate_patterns, 
                                   app_ref_buffer & result);
    
    void reset_pre_patterns();

    /**
       \brief All minimal unary patterns (i.e., expressions that
       contain all bound variables) are copied to result.  If there
       are unary patterns, then at most num_extra_multi_patterns multi
       patterns are created.  If there are no unary pattern, then at
       most 1 + num_extra_multi_patterns multi_patterns are created.
    */
    void mk_patterns(unsigned num_bindings,              // IN number of bindings.
                     expr * n,                           // IN node where the patterns are going to be extracted.
                     unsigned num_no_patterns,           // IN num. patterns that should not be used.
                     expr * const * no_patterns,         // IN patterns that should not be used.
                     app_ref_buffer & result);           // OUT result
    
public:
    pattern_inference_cfg(ast_manager & m, pattern_inference_params const & params);
    
    void register_forbidden_family(family_id fid) {
        SASSERT(fid != m_bfid);
        m_forbidden.push_back(fid);
    }

    /**
       \brief Register f as a preferred function symbol. The inference algorithm
       gives preference to patterns rooted by this kind of function symbol.
    */
    void register_preferred(func_decl * f) {
        m_preferred.insert(f);
    }

    bool reduce_quantifier(quantifier * old_q, 
                           expr * new_body, 
                           expr * const * new_patterns, 
                           expr * const * new_no_patterns,
                           expr_ref & result,
                           proof_ref & result_pr);

    void register_preferred(unsigned num, func_decl * const * fs) { for (unsigned i = 0; i < num; ++i) register_preferred(fs[i]); }
    
    bool is_forbidden(func_decl const * decl) const {
        family_id fid = decl->get_family_id();
        if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE) 
            return true;
        return std::find(m_forbidden.begin(), m_forbidden.end(), fid) != m_forbidden.end();
    }

    bool is_forbidden(app * n) const;
};

class pattern_inference_rw : public rewriter_tpl<pattern_inference_cfg> {
    pattern_inference_cfg m_cfg;
public:
    pattern_inference_rw(ast_manager& m, pattern_inference_params const & params);
};