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


/*++
Copyright (c) 2025 Microsoft Corporation

Module Name:

    theory_finite_set_size.h

Abstract:

    sub-solver for cardinality constraints of finite sets

--*/

#pragma once

#include "ast/ast.h"
#include "ast/ast_pp.h"
#include "ast/finite_set_decl_plugin.h"
#include "ast/rewriter/finite_set_axioms.h"
#include "util/obj_pair_hashtable.h"
#include "util/union_find.h"
#include "smt/smt_theory.h"
#include "model/finite_set_factory.h"

namespace smt {
    class context;
    class theory_finite_set;

    class theory_finite_set_size {
        struct diseq {
            theory_var x, y;
        };
        struct eq {
            theory_var x, y;
        };
        struct in {
            enode *n;
            bool is_pos;
        };
        using tracking_literal = std::variant<diseq, eq, in>;
        ast_manager          &m;
        context             &ctx;
        theory_finite_set   &th;
        finite_set_util u;
        scoped_ptr<context> m_solver;
        bool m_solver_ran = false;
        ptr_vector<func_decl> m_set_size_decls;
        expr_ref_vector bs;
        obj_map<enode, expr *> n2b;
        obj_map<expr, tracking_literal> m_assumptions;
        expr_ref m_assumption;
        expr_ref_vector m_slacks;
        vector<ptr_vector<expr>> m_slack_members;
        obj_map<expr, app *> m_unique_values;
        app_ref_vector m_pinned;

        void collect_subexpressions(enode_vector& ns);
        void add_def_axioms(enode_vector const &ns);
        void add_singleton_axioms(enode_vector const &ns);
        void add_eq_axioms(enode_vector const &ns);
        void add_diseq_axioms(enode_vector const &ns);
        enode *mk_singleton(enode* n);
        enode *mk_diff(enode *a, enode *b);
        void initialize_solver();

        lbool run_solver();

    public:
        theory_finite_set_size(theory_finite_set &th);
        void add_set_size(func_decl *f);
        lbool final_check(); 
        std::ostream &display(std::ostream &out) const;
        void init_model(model_generator &mg);
        app *get_unique_value(expr *n) {
            return m_unique_values.contains(n) ? m_unique_values[n] : nullptr;
        }
    };
}