z3-src 503.2.1

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

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    qi_queue.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-06-15.

Revision History:

--*/
#pragma once

#include "ast/ast.h"
#include "ast/quantifier_stat.h"
#include "ast/rewriter/cached_var_subst.h"
#include "parsers/util/cost_parser.h"
#include "smt/smt_checker.h"
#include "smt/smt_quantifier.h"
#include "smt/fingerprints.h"
#include "params/qi_params.h"
#include "ast/cost_evaluator.h"
#include "util/statistics.h"
#include "tactic/user_propagator_base.h"

namespace smt {
    class context;

    struct qi_queue_stats {
        unsigned m_num_instances, m_num_lazy_instances;
        void reset() { memset(this, 0, sizeof(qi_queue_stats)); }
        qi_queue_stats() { reset(); }
    };

    class qi_queue {
        quantifier_manager &          m_qm;
        context &                     m_context;
        ast_manager &                 m;
        qi_params &                   m_params;
        qi_queue_stats                m_stats;
        checker                       m_checker;
        expr_ref                      m_cost_function;
        expr_ref                      m_new_gen_function;
        cost_parser                   m_parser;
        cost_evaluator                m_evaluator;
        cached_var_subst              m_subst;
        svector<float>                m_vals;
        double                        m_eager_cost_threshold = 0;
        std::function<bool(quantifier*,expr*)> m_on_binding;
        struct entry {
            fingerprint * m_qb;
            float         m_cost;
            unsigned      m_generation:31;
            unsigned      m_instantiated:1;
            unsigned      m_model_based:1; // produced by model-based quantifier instantiation
            entry(fingerprint * f, float c, unsigned g, bool mb = false):m_qb(f), m_cost(c), m_generation(g), m_instantiated(false), m_model_based(mb) {}
        };
        svector<entry>                m_new_entries;
        svector<entry>                m_delayed_entries;
        expr_ref_vector               m_instances;
        vector<std::pair<expr_ref, app_ref>> m_persistent_instances; // (lemma, proof); proof is null when proofs are disabled
        unsigned_vector               m_instantiated_trail;
        struct scope {
            unsigned   m_delayed_entries_lim;
            unsigned   m_instances_lim;
            unsigned   m_instantiated_trail_lim;
        };
        svector<scope>                m_scopes;

        void init_parser_vars();
        q::quantifier_stat * set_values(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation, float cost);
        float get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation);
        unsigned get_new_gen(quantifier * q, unsigned generation, float cost);
        void instantiate(entry & ent);
        void get_min_max_costs(float & min, float & max) const;
        void display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation);

    public:
        qi_queue(quantifier_manager & qm, context & ctx, qi_params & params);
        void setup();
        /**
           \brief Insert a new quantifier in the queue, f contains the quantifier and bindings.
           f->get_data() is the quantifier.
        */
        void insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation, bool mbqi_instance = false);
        void instantiate();
        bool has_work() const { return !m_new_entries.empty(); }
        void init_search_eh();
        bool final_check_eh();
        void push_scope();
        void pop_scope(unsigned num_scopes);
        void reset();
        void display_delayed_instances_stats(std::ostream & out) const;
        void collect_statistics(::statistics & st) const;
        // instances (lemmas of the form (or (not q) inst)) produced so far in the current search,
        // paired with their proofs when proofs are enabled (proof component is null otherwise).
        // model-based instances produced since the last call, kept across backtracking (see context::check)
        void collect_instances(vector<std::pair<expr_ref, app_ref>> & out) { out.append(m_persistent_instances); m_persistent_instances.reset(); }
        void register_on_binding(std::function<bool(quantifier* q, expr* e)> & on_binding) {
            m_on_binding = on_binding;
        }
    };
}