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

/*++
Copyright (c) 2026 Romain Soulat

Module Name:

    ff_tiny.h

Abstract:

    Complete finite-domain search for polynomial systems over tiny prime
    fields (p < 64). Every variable ranges over F_p, represented as a 64-bit
    domain mask; the search branches on the variable with the smallest domain
    and filters domains by forward checking: a constraint with a single
    unassigned variable is restricted to the univariate polynomial left after
    substituting the assigned values, and evaluated on the remaining domain.

    SAT answers are total assignments that satisfy every constraint. UNSAT
    answers follow from exhausting the finite search space, so every input
    constraint is a premise.

Author:

    Romain Soulat

--*/
#pragma once
#include "util/lbool.h"
#include <cstdint>
#include <functional>
#include <vector>

namespace ff {

    struct tiny_term {
        uint32_t coef;                // in [0, p)
        std::vector<uint32_t> vars;   // local variable indices, repeated for powers
    };

    struct tiny_constraint {
        bool is_neq = false;          // f != 0 instead of f = 0
        std::vector<tiny_term> terms;
    };

    struct tiny_stats {
        uint64_t nodes = 0;
        uint64_t filters = 0;
    };

    // Decide the constraints over F_p for variables 0..num_vars-1. On l_true,
    // model holds a satisfying assignment. `charge` is called with work units
    // and may throw to abort the search.
    lbool tiny_search(uint32_t p, unsigned num_vars, std::vector<tiny_constraint> const &cs,
                      std::vector<uint32_t> &model, std::function<void(unsigned)> const &charge,
                      tiny_stats &st);

}  // namespace ff