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_params.h

Abstract:

    Binds ff::engine Groebner-basis algebra options (basis storage, reduction
    strategy, resource bounds) to the global SMT parameter defaults.

Author:

    Romain Soulat

--*/
#pragma once

#include "math/ff/ff_polynomial.h"
#include "params/smt_params_helper.hpp"

namespace ff {
    // Resolve local overrides and the global SMT defaults from one snapshot.
    inline void configure_engine(engine &algebra, smt_params_helper const &options) {
        algebra.linear_split = options.ff_linear_split();
        algebra.basis_bits = options.ff_basis_bits();
        algebra.compact_matrix = options.ff_compact_matrix();
        algebra.model_search = options.ff_model_search();
        algebra.root_completion = options.ff_root_completion();
        algebra.quotient_field = options.ff_quotient_field();
        algebra.bit_bounds = options.ff_bit_bounds();
        algebra.adaptive_reduction = options.ff_adaptive_reduction();
        algebra.adaptive_matrix = options.ff_adaptive_matrix();
        algebra.adaptive_basis = options.ff_adaptive_basis();
        algebra.set_basis_storage_limit(options.ff_basis_max_bytes());
        algebra.lazy_matrix = options.ff_lazy_matrix();
        algebra.sparse_matrix_reducers = options.ff_sparse_matrix_reducers();
        algebra.fused_reduction = options.ff_fused_reduction();
        algebra.bounded_elimination = options.ff_bounded_elimination();
        algebra.sugar_pairs = options.ff_sugar_pairs();
        algebra.gm_pairs = options.ff_gm_pairs();
        algebra.div_masks = options.ff_div_masks();
        algebra.geobucket = options.ff_geobucket();
        algebra.small_coefficients = options.ff_small_coefficients();
        algebra.compact_encoding = options.ff_compact_encoding();
        algebra.f4 = options.ff_f4();
        algebra.f4_max_quotient = options.ff_f4_max_quotient();
        algebra.f4_budget_factor = options.ff_f4_budget();
        algebra.f4_short_budget = options.ff_f4_short_budget();
        algebra.f4_value_split = options.ff_f4_value_split();
        algebra.f4_slice = options.ff_f4_slice();
        algebra.tiny_search = options.ff_tiny();
        algebra.tiny_budget = options.ff_tiny_budget();
    }
}