z3-src 503.2.2

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

/*++
Copyright (c) 2026 Microsoft Corporation

Module Name:

    seq_view.h

Abstract:

    A view: a constraint on one sequence value, stated against a derivative
    automaton instead of as a concrete word.  Reading the value drives the
    automaton from m_state; the view holds when

        m_target ? the run ends at m_target      (reach view)
                 : the end state is nullable     (membership view)

    Views on the same value are conjunctive: the admissible values are the
    intersection of their languages.  See seq_monadic, which reports the
    decomposition it commits to as views.

    A REACH view is relative to a transition relation, and therefore to the
    seq::transition_mode of the engine that produced it: under light_antimirov_tm a
    derivative is split over its top-level unions, so reaching m_target means SOME run
    ends there, whereas under brzozowski_tm the derivative is a single state and the
    run is the deterministic one.  A client that evaluates views with the producing
    engine (product_nonempty, materialize) never sees the difference; a client that
    re-states them against an automaton of its own must build the engine in the mode
    that automaton steps in.  A MEMBERSHIP view is mode-independent: m_state denotes a
    language either way.

Author:

    Clemens Eisenhofer 2026

--*/
#pragma once

#include "ast/ast.h"
#include "ast/rewriter/seq_rewriter.h"
#include "util/lbool.h"
#include "util/vector.h"

namespace seq {

    struct view {
        expr_ref        m_state;
        expr_ref        m_target;     // null: membership view

        // identity for dedup/memoization; covers the same fields as operator==
        struct sig {
            unsigned        state, target;
        };

        view(ast_manager& m) : m_state(m), m_target(m) {}
        view(expr* state, expr* target, ast_manager& m) :
            m_state(state, m), m_target(target, m) {}

        static view membership(expr* state, ast_manager& m) {
            return view(state, nullptr, m);
        }

        static view reach(expr* state, expr* target, ast_manager& m) {
            return view(state, target, m);
        }

        bool is_membership() const { return m_target.get() == nullptr; }
        bool is_reach() const { return m_target.get() != nullptr; }

        sig key() const {
            return { m_state ? m_state->get_id() : UINT_MAX,
                     m_target ? m_target->get_id() : UINT_MAX };
        }

        bool operator==(view const& other) const {
            return m_state.get() == other.m_state.get() && m_target.get() == other.m_target.get();
        }

        bool operator!=(view const& other) const { return !(*this == other); }
    };

    inline bool operator<(view::sig const& a, view::sig const& b) {
        if (a.state != b.state) return a.state < b.state;
        return a.target < b.target;
    }

    inline bool operator==(view::sig const& a, view::sig const& b) {
        return a.state == b.state && a.target == b.target;
    }

    using view_vector = vector<view>;

    // Uncached reference semantics; an engine with its own caches has to agree with these.
    // l_undef when nullability is undecided.
    lbool accepts(view const& v, seq_rewriter& rw);

    // Empty language: no value satisfies the view.
    bool is_dead(view const& v, seq_rewriter& rw);

}