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

/*++
Copyright (c) 2026 Romain Soulat

Module Name:

    ff_solver.h

Abstract:

    Ground prime-field reasoning over AST terms, independent of SAT and SMT
    contexts. Frontends supply equality/disequality premises, justify foreign
    congruence, and arrange candidate values shared with other theories.

--*/
#pragma once
#include "ast/ff_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "math/ff/ff_polynomial.h"
#include <memory>

namespace ff {
    class solver;

    // Pure term encodings only; no assertions, assignments or conflict evidence.
    // A cache belongs to one manager/field. It pins its keys and may be shared
    // across sequential checks/scopes. Do not reset it while a solver borrows it.
    class ff_encoding_cache {
        struct imp;
        std::unique_ptr<imp> m_imp;
        friend class solver;
    public:
        ff_encoding_cache(ast_manager &m, sort *field);
        ~ff_encoding_cache();
        unsigned size() const;
        void reset();
    };

    // One field problem per check: add ground field constraints, call check once,
    // then consume either conflict indices or candidate values. Recreate the
    // problem for new assignments/scopes; only the pure encoding cache survives.
    // Foreign field terms are opaque leaves, NOT freely assignable UF models.
    // With solve_eqs enabled, rewriting and solve-eqs run on a private dependent-
    // expression state; its model trail restores eliminated constants. Tactic
    // pipelines disable this repeated preprocessing for their branch queries.
    // Dependencies
    // use private labels mapped to the exact signed input premises.
    // SAT here means a field candidate: the frontend must enforce congruence,
    // other-theory semantics and finite-field model arrangements before accepting.
    class solver {
        struct imp;
        std::unique_ptr<imp> m_imp;
    public:
        solver(ast_manager &m, sort *field, params_ref const &p,
                      ff_encoding_cache *cache = nullptr, basis_cache *basis = nullptr);
        ~solver();
        void add(expr *a, expr *b, bool equality);
        // May throw exhausted on resource limits, just like the algebra engine.
        // SAT candidates are rechecked against every supplied original constraint.
        lbool check(bool record_proof = false);
        // Evidence from the same proof-enabled check. The frontend remains
        // responsible for justifying the signed assignment premises.
        app* evidence() const;
        bool refute();
        rational value(expr *term);
        expr *premise(unsigned index) const;
        // Exact input indices supporting UNSAT. These are explanations, NOT
        // checked proof objects. A future evidence recorder must also certify
        // normalization, substitution and the frontend's premise justifications.
        std::set<unsigned> const &conflict() const;
        void collect_statistics(statistics &st) const;
        // True only when encoding (not search) exceeded the polynomial limit.
        bool encoding_limit_hit() const;
        unsigned encoding_steps() const;
    };

}