z3-src 503.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
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
114
115
116
117
118
119
120
121
122
123
124
125
126

/*++
Copyright (c) 2026 Romain Soulat

Module Name:

    theory_ff.h

Abstract:

    Ground theory combination for prime fields using modular algebra and
    model arrangements, with an exact bounded bit-vector representation
    when algebra is inconclusive. Original field sorts/terms stay in the
    equality engine, so arrays, datatypes and uninterpreted functions
    retain their original signatures.

Author:

    Romain Soulat

--*/
#pragma once

#include "smt/smt_theory.h"
#include "math/ff/ff_polynomial.h"
#include "ast/ff/ff_solver.h"
#include "ast/ff_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/ff_bv_operations.h"
#include "util/obj_pair_hashtable.h"
#include <memory>

namespace smt {
    // Ground theory combination using modular algebra and model arrangements,
    // with an exact bounded BV representation when algebra is inconclusive.
    // Original field sorts/terms stay in the equality engine, so arrays,
    // datatypes and uninterpreted functions retain their original signatures.
    class theory_ff : public theory {
        ff_util ff;
        bv_util bv;
        th_rewriter rw;
        ff_bv_operations operations;
        func_decl_ref_vector helpers;
        obj_map<sort, func_decl *> wraps, unwraps;
        obj_hashtable<func_decl> decoders;
        unsigned axioms = 0;
        unsigned native_checks = 0, native_conflicts = 0, arrangements = 0, fallbacks = 0;
        unsigned root_clauses = 0;
        unsigned factor_split_candidates = 0;
        unsigned factor_split_clauses = 0;
        obj_hashtable<sort> bv_fields; // fallback is local to a field, never the whole context
        void refresh_bv_fields();
        ff::basis_cache memo;
        obj_map<sort, std::unique_ptr<ff::ff_encoding_cache>> encodings;
        obj_hashtable<expr> constrained;
        // Deduplicates root-splitting by the merged terms' original operands,
        // which are already kept alive by their enodes.
        obj_pair_hashtable<expr, expr> split_atoms;
        obj_map<expr, expr *> root_norm;   // bounded pure-rewriting cache; cleared on pop
        expr_ref_vector root_norm_pins;
        obj_map<expr, rational> native_values;
        expr_ref_vector model_values;
        // Optional root-splitting hints only. Algebra still collects complete
        // active constraints: field-valued ITEs need not trigger this callback.
        svector<std::pair<theory_var, theory_var>> eqs, diseqs;

        void ensure_helpers(sort *s);
        expr_ref wrap(expr *e);
        void assert_axiom(expr *e, bool simplify = true);
        void constrain(expr *e);
        expr_ref square_root_term(expr *e);
        bool factor_split(expr *a, expr *b, expr_ref_vector &branches);
        bool propagate_roots();
        final_check_status check_native();
        final_check_status final_check_eh(unsigned) override;
        void pop_scope_eh(unsigned n) override;
        void reset_eh() override;
        void init_search_eh() override {
            // A canceled internalization may have stopped halfway through a
            // bridge definition. Retry all live definitions on the next check.
            constrained.reset();
            split_atoms.reset();
            factor_split_clauses = 0;
            refresh_bv_fields();
        }

        bool internalize_atom(app *, bool) override {
            return false;
        }
        bool internalize_term(app *e) override;
        void apply_sort_cnstr(enode *n, sort *s) override;
        void internalize_eq_eh(app *atom, bool_var v) override;
        void relevant_eh(expr *e) override;
        void new_eq_eh(theory_var v1, theory_var v2) override;
        void new_diseq_eh(theory_var, theory_var) override;
        void init_model(model_generator &mg) override;
        model_value_proc *mk_value(enode *n, model_generator &mg) override;
        void finalize_model(model_generator &mg) override;

    public:
        explicit theory_ff(context &ctx);
        ~theory_ff() override;
        theory *mk_fresh(context *ctx) override {
            return alloc(theory_ff, *ctx);
        }
        char const *get_name() const override {
            return "finite-field";
        }
        void display(std::ostream &out) const override {
            display_var2enode(out);
        }
        void collect_statistics(::statistics &st) const override {
            st.update("ff combination axioms", axioms);
            st.update("ff native checks", native_checks);
            st.update("ff native conflicts", native_conflicts);
            st.update("ff arrangements", arrangements);
            st.update("ff bv fallbacks", fallbacks);
            st.update("ff root clauses", root_clauses);
            st.update("ff factor split candidates", factor_split_candidates);
            st.update("ff factor split clauses", factor_split_clauses);
            st.update("ff normalization cache entries", root_norm_pins.size() / 2);
            st.update("ff basis cache hits", memo.hits);
            st.update("ff basis cache misses", memo.misses);
        }
    };
}  // namespace smt