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

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    q_queue.h

Abstract:

    Instantiation queue for quantifiers

Author:

    Nikolaj Bjorner (nbjorner) 2021-01-24

--*/
#pragma once

#include "ast/quantifier_stat.h"
#include "ast/cost_evaluator.h"
#include "ast/rewriter/cached_var_subst.h"
#include "parsers/util/cost_parser.h"
#include "sat/smt/q_clause.h"



namespace euf {
    class solver;
}

namespace q {

    class ematch;

    class queue {

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

        ematch&                       em;
        euf::solver&                  ctx;
        ast_manager &                 m;
        qi_params const &             m_params;
        stats                         m_stats;
        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;
        struct entry {
            binding *     m_qb;
            float         m_cost;
            bool          m_instantiated = false;
            entry(binding * f, float c):m_qb(f), m_cost(c) {}
        };
        struct reset_new_entries;
        struct reset_instantiated;

        svector<entry>                m_new_entries;
        svector<entry>                m_delayed_entries;

        float get_cost(binding& f);
        void set_values(binding& f, float cost);
        void init_parser_vars();
        void setup();
        unsigned get_new_gen(binding& f, float cost);
        void instantiate(entry& e);

    public:

        queue(ematch& em, euf::solver& ctx);
            
        void insert(binding* f);

        bool propagate();

        bool lazy_propagate();

        void collect_statistics(::statistics & st) const;

    };
}