z3_sys/
functions_patched.rs

1// Hand-written declarations for functions with nullable parameters that require
2// Option<T> in their signatures. These are excluded from the bindgen-generated
3// functions.rs via blocklist_function in build.rs.
4
5unsafe extern "C" {
6    /// Create a constructor.
7    ///
8    /// - `c`: logical context.
9    /// - `name`: constructor name.
10    /// - `recognizer`: name of recognizer function.
11    /// - `num_fields`: number of fields in constructor.
12    /// - `field_names`: names of the constructor fields.
13    /// - `sorts`: field sorts, `None` if the field sort refers to a recursive sort.
14    /// - `sort_refs`: reference to datatype sort that is an argument to the constructor; if the
15    ///   corresponding sort reference is 0, then the value in sort_refs should be an index
16    ///   referring to one of the recursive datatypes that is declared.
17    ///
18    /// # See also
19    ///
20    /// - [`Z3_del_constructor`]
21    /// - [`Z3_mk_constructor_list`]
22    /// - [`Z3_query_constructor`]
23    pub fn Z3_mk_constructor(
24        c: Z3_context,
25        name: Z3_symbol,
26        recognizer: Z3_symbol,
27        num_fields: ::core::ffi::c_uint,
28        field_names: *const Z3_symbol,
29        sorts: *const Option<Z3_sort>,
30        sort_refs: *mut ::core::ffi::c_uint,
31    ) -> Option<Z3_constructor>;
32
33    /// Add a universal Horn clause as a named rule.
34    /// The `horn_rule` should be of the form:
35    ///
36    /// ```text
37    /// horn_rule ::= (forall (bound-vars) horn_rule)
38    /// |  (=> atoms horn_rule)
39    /// |  atom
40    /// ```
41    pub fn Z3_fixedpoint_add_rule(
42        c: Z3_context,
43        d: Z3_fixedpoint,
44        rule: Z3_ast,
45        name: Option<Z3_symbol>,
46    );
47
48    /// Assert soft constraint to the optimization context.
49    ///
50    /// - `c`: context
51    /// - `o`: optimization context
52    /// - `a`: formula
53    /// - `weight`: a penalty for violating soft constraint. Negative weights convert into rewards.
54    /// - `id`: optional identifier to group soft constraints
55    ///
56    /// # See also
57    ///
58    /// - [`Z3_optimize_assert`]
59    /// - [`Z3_optimize_assert_and_track`]
60    pub fn Z3_optimize_assert_soft(
61        c: Z3_context,
62        o: Z3_optimize,
63        a: Z3_ast,
64        weight: Z3_string,
65        id: Option<Z3_symbol>,
66    ) -> ::core::ffi::c_uint;
67}
z3_sys/functions_patched.rs

z3_sys/
functions_patched.rs
