z3-src 503.3.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
127
128
129
130

/*++
Copyright (c) 2026 Romain Soulat

Module Name:

    ff_simplify.h

Abstract:

    Simplifiers for prime-field ("QF_FF") goals:

    - ff_disjunctive_simplifier rewrites disjunctive Boolean field domains
      `(a=b) or (c=d)` as the polynomial equation `(a-b)*(c-d)=0`, when doing
      so does not hide a univariate Boolean-domain candidate.
    - ff_zero_test_simplifier derives Boolean zero-test indicator
      definitions from `x*z=0`-shaped equations.
    - ff_wire_simplifier eliminates acyclic "wire" definitions `x = t`
      (definitions whose right-hand side does not (transitively) mention
      `x`), substituting `x` by `t` and recording the elimination on the
      model reconstruction trail.

    ff_basic_simplifier composes the above together with the generic
    simplify/propagate-values/solve-eqs simplifiers into the "ff-simplify"
    preprocessing pipeline used ahead of the QF_FF decision procedures
    (ff-solve, ff-sat, ff-unique). It preserves compact theory atoms for
    lazy Boolean search by skipping simplification entirely when a goal
    contains a Boolean uninterpreted constant anywhere (the algebraic
    decision procedures normalize circuits on their own), and declines to
    run when proofs are requested (QF_FF certificates are not supported in
    v1).

Author:

    Romain Soulat

--*/
#pragma once

#include "util/stopwatch.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/simplifiers/then_simplifier.h"

// Preserve candidate digit variables during substitution, without assuming
// Booleanity. The original domain constraints remain in the problem.
void freeze_ff_domain_variables(ast_manager &m, dependent_expr_state &s);

class ff_disjunctive_simplifier : public dependent_expr_simplifier {
    params_ref m_params;

public:
    ff_disjunctive_simplifier(ast_manager &m, params_ref const &p, dependent_expr_state &s);
    char const *name() const override { return "ff-disjunctive"; }
    bool supports_proofs() const override { return true; }
    void reduce() override;
    void updt_params(params_ref const &p) override;
    void collect_param_descrs(param_descrs &r) override;
};

class ff_zero_test_simplifier : public dependent_expr_simplifier {
    unsigned m_added = 0;

public:
    ff_zero_test_simplifier(ast_manager &m, dependent_expr_state &s) : dependent_expr_simplifier(m, s) {}
    char const *name() const override { return "ff-zero-test"; }
    bool supports_proofs() const override { return true; }
    void reduce() override;
    void collect_statistics(statistics &st) const override;
    void reset_statistics() override { m_added = 0; }
};

class ff_wire_simplifier : public dependent_expr_simplifier {
    unsigned  m_eliminated = 0;
    stopwatch m_elapsed;

public:
    ff_wire_simplifier(ast_manager &m, dependent_expr_state &s) : dependent_expr_simplifier(m, s) {}
    char const *name() const override { return "ff-wires"; }
    bool supports_proofs() const override { return true; }
    void reduce() override;
    void collect_statistics(statistics &st) const override;
    void reset_statistics() override {
        m_eliminated = 0;
        m_elapsed.reset();
    }
};

bool ff_simplify_circuit(ast_manager &m, expr *source, expr_ref &target,
                         proof_ref &proof, bool proofs);

class ff_circuit_simplifier : public dependent_expr_simplifier {
    unsigned m_rewritten = 0;
public:
    ff_circuit_simplifier(ast_manager &m, dependent_expr_state &s)
        : dependent_expr_simplifier(m, s) {}
    char const *name() const override { return "ff-circuits"; }
    bool supports_proofs() const override { return true; }
    void reduce() override;
    void collect_statistics(statistics &st) const override {
        st.update("ff circuit rewrites", m_rewritten);
    }
    void reset_statistics() override { m_rewritten = 0; }
};

class ff_basic_simplifier : public dependent_expr_simplifier {
    params_ref                  m_params;
    scoped_ptr<then_simplifier> m_impl;
    stopwatch                   m_elapsed;
    unsigned                    m_boolean_skips = 0;

    bool skip_boolean_goal();

public:
    ff_basic_simplifier(ast_manager &m, params_ref const &p, dependent_expr_state &s);
    char const *name() const override { return "ff-simplify"; }
    bool supports_proofs() const override { return true; }
    void reduce() override;
    void collect_statistics(statistics &st) const override;
    void reset_statistics() override;
    void updt_params(params_ref const &p) override;
    void collect_param_descrs(param_descrs &r) override;
};

Z3_ADD_SIMPLIFIER(ff_disjunctive, "ff-disjunctive", "rewrite disjunctive Boolean field domains as polynomial equations.",
                  alloc(ff_disjunctive_simplifier, m, p, s));
Z3_ADD_SIMPLIFIER(ff_zero_test, "ff-zero-test", "derive Boolean zero-test indicators for prime-field goals.",
                  alloc(ff_zero_test_simplifier, m, s));
Z3_ADD_SIMPLIFIER(ff_wires, "ff-wires", "eliminate acyclic wire definitions in prime-field goals.",
                  alloc(ff_wire_simplifier, m, s));
Z3_ADD_SIMPLIFIER(ff_simplify, "ff-simplify", "simplify prime-field goals ahead of QF_FF decision procedures.",
                  alloc(ff_basic_simplifier, m, p, s));