z3-src 503.2.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

/*++
Copyright (c) 2026 Microsoft Corporation

Module Name:

    euf_assoc_plugin.h

Abstract:

    Completion plugin for associative functions.

--*/

#pragma once

#include <functional>
#include "ast/euf/euf_plugin.h"

namespace euf {

    class assoc_plugin : public plugin {
    public:
        using recognizer = std::function<bool(enode const*)>;

    private:
        using word = enode_vector;

        struct rule {
            word lhs;
            word rhs;
            justification j;
        };

        struct shared {
            enode* n;
            word w;
        };

        struct stats {
            unsigned m_num_rules = 0;
            unsigned m_num_superpositions = 0;
        };

        enum class undo_kind {
            is_queue_eq,
            is_register_shared,
            is_add_rule,
            is_push_scope
        };

        theory_id m_fid;
        recognizer m_is_assoc;
        recognizer m_is_variable;
        recognizer m_is_unit;
        justification::dependency_manager m_dep_manager;
        vector<rule> m_rules;
        vector<shared> m_shared;
        enode_pair_vector m_queued;
        bool_vector m_is_shared;
        svector<undo_kind> m_undo;
        unsigned_vector m_superposition_lim;
        unsigned m_num_superpositions = 0;
        unsigned m_queue_head = 0;
        unsigned m_completion_head = 0;
        unsigned m_max_rules = 64;
        unsigned m_max_superpositions = 256;
        unsigned m_max_word_size = 64;
        unsigned m_max_rewrite_steps = 1024;
        stats m_stats;
        std::function<void(void)> m_undo_notify;

        bool is_assoc(enode const* n) const { return m_is_assoc && m_is_assoc(n); }
        bool is_variable(enode const* n) const { return m_is_variable && m_is_variable(n); }
        bool is_unit(enode const* n) const { return m_is_unit && m_is_unit(n); }

        void push_undo(undo_kind k);
        void flatten(enode* n, word& w) const;
        bool equal(word const& a, word const& b) const;
        bool match(word const& w, unsigned offset, word const& pattern) const;
        int compare(word const& a, word const& b) const;
        bool orient(word& lhs, word& rhs) const;
        justification join(justification j1, justification j2);
        bool reduce(word& w, justification& j, rule const* except = nullptr);
        bool add_rule(word lhs, word rhs, justification j);
        void add_overlaps(rule const& r1, rule const& r2);
        void complete();
        void propagate_shared();

    public:
        assoc_plugin(egraph& g, theory_id fid);

        theory_id get_id() const override { return m_fid; }

        void register_associative(recognizer f) { m_is_assoc = std::move(f); }
        void register_variable(recognizer f) { m_is_variable = std::move(f); }
        void register_unit(recognizer f) { m_is_unit = std::move(f); }

        void set_completion_limits(unsigned max_rules, unsigned max_superpositions,
                                   unsigned max_word_size = 64, unsigned max_rewrite_steps = 1024);

        unsigned num_rules() const { return m_rules.size(); }

        void register_node(enode* n) override;
        void merge_eh(enode* n1, enode* n2) override;
        void undo() override;
        void push_scope_eh() override;
        void propagate() override;
        std::ostream& display(std::ostream& out) const override;
        void collect_statistics(statistics& st) const override;

        void set_undo(std::function<void(void)> u) { m_undo_notify = std::move(u); }
    };
}