bitwuzla_sys/src-generated/
bindings.rs

1/* automatically generated by rust-bindgen 0.71.1 */
2
3use libc::FILE;
4
5pub const BITWUZLA_SAT: BitwuzlaResult = 10;
6pub const BITWUZLA_UNSAT: BitwuzlaResult = 20;
7pub const BITWUZLA_UNKNOWN: BitwuzlaResult = 0;
8pub type BitwuzlaResult = ::std::os::raw::c_uint;
9pub const BITWUZLA_RM_RNE: BitwuzlaRoundingMode = 0;
10pub const BITWUZLA_RM_RNA: BitwuzlaRoundingMode = 1;
11pub const BITWUZLA_RM_RTN: BitwuzlaRoundingMode = 2;
12pub const BITWUZLA_RM_RTP: BitwuzlaRoundingMode = 3;
13pub const BITWUZLA_RM_RTZ: BitwuzlaRoundingMode = 4;
14pub const BITWUZLA_RM_MAX: BitwuzlaRoundingMode = 5;
15pub type BitwuzlaRoundingMode = ::std::os::raw::c_uint;
16pub const BITWUZLA_KIND_CONSTANT: BitwuzlaKind = 0;
17pub const BITWUZLA_KIND_CONST_ARRAY: BitwuzlaKind = 1;
18pub const BITWUZLA_KIND_VALUE: BitwuzlaKind = 2;
19pub const BITWUZLA_KIND_VARIABLE: BitwuzlaKind = 3;
20pub const BITWUZLA_KIND_AND: BitwuzlaKind = 4;
21pub const BITWUZLA_KIND_DISTINCT: BitwuzlaKind = 5;
22pub const BITWUZLA_KIND_EQUAL: BitwuzlaKind = 6;
23pub const BITWUZLA_KIND_IFF: BitwuzlaKind = 7;
24pub const BITWUZLA_KIND_IMPLIES: BitwuzlaKind = 8;
25pub const BITWUZLA_KIND_NOT: BitwuzlaKind = 9;
26pub const BITWUZLA_KIND_OR: BitwuzlaKind = 10;
27pub const BITWUZLA_KIND_XOR: BitwuzlaKind = 11;
28pub const BITWUZLA_KIND_ITE: BitwuzlaKind = 12;
29pub const BITWUZLA_KIND_EXISTS: BitwuzlaKind = 13;
30pub const BITWUZLA_KIND_FORALL: BitwuzlaKind = 14;
31pub const BITWUZLA_KIND_APPLY: BitwuzlaKind = 15;
32pub const BITWUZLA_KIND_LAMBDA: BitwuzlaKind = 16;
33pub const BITWUZLA_KIND_ARRAY_SELECT: BitwuzlaKind = 17;
34pub const BITWUZLA_KIND_ARRAY_STORE: BitwuzlaKind = 18;
35pub const BITWUZLA_KIND_BV_ADD: BitwuzlaKind = 19;
36pub const BITWUZLA_KIND_BV_AND: BitwuzlaKind = 20;
37pub const BITWUZLA_KIND_BV_ASHR: BitwuzlaKind = 21;
38pub const BITWUZLA_KIND_BV_COMP: BitwuzlaKind = 22;
39pub const BITWUZLA_KIND_BV_CONCAT: BitwuzlaKind = 23;
40pub const BITWUZLA_KIND_BV_DEC: BitwuzlaKind = 24;
41pub const BITWUZLA_KIND_BV_INC: BitwuzlaKind = 25;
42pub const BITWUZLA_KIND_BV_MUL: BitwuzlaKind = 26;
43pub const BITWUZLA_KIND_BV_NAND: BitwuzlaKind = 27;
44pub const BITWUZLA_KIND_BV_NEG: BitwuzlaKind = 28;
45pub const BITWUZLA_KIND_BV_NEG_OVERFLOW: BitwuzlaKind = 29;
46pub const BITWUZLA_KIND_BV_NOR: BitwuzlaKind = 30;
47pub const BITWUZLA_KIND_BV_NOT: BitwuzlaKind = 31;
48pub const BITWUZLA_KIND_BV_OR: BitwuzlaKind = 32;
49pub const BITWUZLA_KIND_BV_REDAND: BitwuzlaKind = 33;
50pub const BITWUZLA_KIND_BV_REDOR: BitwuzlaKind = 34;
51pub const BITWUZLA_KIND_BV_REDXOR: BitwuzlaKind = 35;
52pub const BITWUZLA_KIND_BV_ROL: BitwuzlaKind = 36;
53pub const BITWUZLA_KIND_BV_ROR: BitwuzlaKind = 37;
54pub const BITWUZLA_KIND_BV_SADD_OVERFLOW: BitwuzlaKind = 38;
55pub const BITWUZLA_KIND_BV_SDIV_OVERFLOW: BitwuzlaKind = 39;
56pub const BITWUZLA_KIND_BV_SDIV: BitwuzlaKind = 40;
57pub const BITWUZLA_KIND_BV_SGE: BitwuzlaKind = 41;
58pub const BITWUZLA_KIND_BV_SGT: BitwuzlaKind = 42;
59pub const BITWUZLA_KIND_BV_SHL: BitwuzlaKind = 43;
60pub const BITWUZLA_KIND_BV_SHR: BitwuzlaKind = 44;
61pub const BITWUZLA_KIND_BV_SLE: BitwuzlaKind = 45;
62pub const BITWUZLA_KIND_BV_SLT: BitwuzlaKind = 46;
63pub const BITWUZLA_KIND_BV_SMOD: BitwuzlaKind = 47;
64pub const BITWUZLA_KIND_BV_SMUL_OVERFLOW: BitwuzlaKind = 48;
65pub const BITWUZLA_KIND_BV_SREM: BitwuzlaKind = 49;
66pub const BITWUZLA_KIND_BV_SSUB_OVERFLOW: BitwuzlaKind = 50;
67pub const BITWUZLA_KIND_BV_SUB: BitwuzlaKind = 51;
68pub const BITWUZLA_KIND_BV_UADD_OVERFLOW: BitwuzlaKind = 52;
69pub const BITWUZLA_KIND_BV_UDIV: BitwuzlaKind = 53;
70pub const BITWUZLA_KIND_BV_UGE: BitwuzlaKind = 54;
71pub const BITWUZLA_KIND_BV_UGT: BitwuzlaKind = 55;
72pub const BITWUZLA_KIND_BV_ULE: BitwuzlaKind = 56;
73pub const BITWUZLA_KIND_BV_ULT: BitwuzlaKind = 57;
74pub const BITWUZLA_KIND_BV_UMUL_OVERFLOW: BitwuzlaKind = 58;
75pub const BITWUZLA_KIND_BV_UREM: BitwuzlaKind = 59;
76pub const BITWUZLA_KIND_BV_USUB_OVERFLOW: BitwuzlaKind = 60;
77pub const BITWUZLA_KIND_BV_XNOR: BitwuzlaKind = 61;
78pub const BITWUZLA_KIND_BV_XOR: BitwuzlaKind = 62;
79pub const BITWUZLA_KIND_BV_EXTRACT: BitwuzlaKind = 63;
80pub const BITWUZLA_KIND_BV_REPEAT: BitwuzlaKind = 64;
81pub const BITWUZLA_KIND_BV_ROLI: BitwuzlaKind = 65;
82pub const BITWUZLA_KIND_BV_RORI: BitwuzlaKind = 66;
83pub const BITWUZLA_KIND_BV_SIGN_EXTEND: BitwuzlaKind = 67;
84pub const BITWUZLA_KIND_BV_ZERO_EXTEND: BitwuzlaKind = 68;
85pub const BITWUZLA_KIND_FP_ABS: BitwuzlaKind = 69;
86pub const BITWUZLA_KIND_FP_ADD: BitwuzlaKind = 70;
87pub const BITWUZLA_KIND_FP_DIV: BitwuzlaKind = 71;
88pub const BITWUZLA_KIND_FP_EQUAL: BitwuzlaKind = 72;
89pub const BITWUZLA_KIND_FP_FMA: BitwuzlaKind = 73;
90pub const BITWUZLA_KIND_FP_FP: BitwuzlaKind = 74;
91pub const BITWUZLA_KIND_FP_GEQ: BitwuzlaKind = 75;
92pub const BITWUZLA_KIND_FP_GT: BitwuzlaKind = 76;
93pub const BITWUZLA_KIND_FP_IS_INF: BitwuzlaKind = 77;
94pub const BITWUZLA_KIND_FP_IS_NAN: BitwuzlaKind = 78;
95pub const BITWUZLA_KIND_FP_IS_NEG: BitwuzlaKind = 79;
96pub const BITWUZLA_KIND_FP_IS_NORMAL: BitwuzlaKind = 80;
97pub const BITWUZLA_KIND_FP_IS_POS: BitwuzlaKind = 81;
98pub const BITWUZLA_KIND_FP_IS_SUBNORMAL: BitwuzlaKind = 82;
99pub const BITWUZLA_KIND_FP_IS_ZERO: BitwuzlaKind = 83;
100pub const BITWUZLA_KIND_FP_LEQ: BitwuzlaKind = 84;
101pub const BITWUZLA_KIND_FP_LT: BitwuzlaKind = 85;
102pub const BITWUZLA_KIND_FP_MAX: BitwuzlaKind = 86;
103pub const BITWUZLA_KIND_FP_MIN: BitwuzlaKind = 87;
104pub const BITWUZLA_KIND_FP_MUL: BitwuzlaKind = 88;
105pub const BITWUZLA_KIND_FP_NEG: BitwuzlaKind = 89;
106pub const BITWUZLA_KIND_FP_REM: BitwuzlaKind = 90;
107pub const BITWUZLA_KIND_FP_RTI: BitwuzlaKind = 91;
108pub const BITWUZLA_KIND_FP_SQRT: BitwuzlaKind = 92;
109pub const BITWUZLA_KIND_FP_SUB: BitwuzlaKind = 93;
110pub const BITWUZLA_KIND_FP_TO_FP_FROM_BV: BitwuzlaKind = 94;
111pub const BITWUZLA_KIND_FP_TO_FP_FROM_FP: BitwuzlaKind = 95;
112pub const BITWUZLA_KIND_FP_TO_FP_FROM_SBV: BitwuzlaKind = 96;
113pub const BITWUZLA_KIND_FP_TO_FP_FROM_UBV: BitwuzlaKind = 97;
114pub const BITWUZLA_KIND_FP_TO_SBV: BitwuzlaKind = 98;
115pub const BITWUZLA_KIND_FP_TO_UBV: BitwuzlaKind = 99;
116pub const BITWUZLA_KIND_NUM_KINDS: BitwuzlaKind = 100;
117pub type BitwuzlaKind = ::std::os::raw::c_uint;
118pub const BITWUZLA_OPT_LOGLEVEL: BitwuzlaOption = 0;
119pub const BITWUZLA_OPT_PRODUCE_MODELS: BitwuzlaOption = 1;
120pub const BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS: BitwuzlaOption = 2;
121pub const BITWUZLA_OPT_PRODUCE_UNSAT_CORES: BitwuzlaOption = 3;
122pub const BITWUZLA_OPT_SEED: BitwuzlaOption = 4;
123pub const BITWUZLA_OPT_VERBOSITY: BitwuzlaOption = 5;
124pub const BITWUZLA_OPT_TIME_LIMIT_PER: BitwuzlaOption = 6;
125pub const BITWUZLA_OPT_MEMORY_LIMIT: BitwuzlaOption = 7;
126pub const BITWUZLA_OPT_NTHREADS: BitwuzlaOption = 8;
127pub const BITWUZLA_OPT_BV_SOLVER: BitwuzlaOption = 9;
128pub const BITWUZLA_OPT_REWRITE_LEVEL: BitwuzlaOption = 10;
129pub const BITWUZLA_OPT_SAT_SOLVER: BitwuzlaOption = 11;
130pub const BITWUZLA_OPT_WRITE_AIGER: BitwuzlaOption = 12;
131pub const BITWUZLA_OPT_WRITE_CNF: BitwuzlaOption = 13;
132pub const BITWUZLA_OPT_PROP_CONST_BITS: BitwuzlaOption = 14;
133pub const BITWUZLA_OPT_PROP_INFER_INEQ_BOUNDS: BitwuzlaOption = 15;
134pub const BITWUZLA_OPT_PROP_NPROPS: BitwuzlaOption = 16;
135pub const BITWUZLA_OPT_PROP_NUPDATES: BitwuzlaOption = 17;
136pub const BITWUZLA_OPT_PROP_OPT_LT_CONCAT_SEXT: BitwuzlaOption = 18;
137pub const BITWUZLA_OPT_PROP_PATH_SEL: BitwuzlaOption = 19;
138pub const BITWUZLA_OPT_PROP_PROB_RANDOM_INPUT: BitwuzlaOption = 20;
139pub const BITWUZLA_OPT_PROP_PROB_USE_INV_VALUE: BitwuzlaOption = 21;
140pub const BITWUZLA_OPT_PROP_SEXT: BitwuzlaOption = 22;
141pub const BITWUZLA_OPT_ABSTRACTION: BitwuzlaOption = 23;
142pub const BITWUZLA_OPT_ABSTRACTION_BV_SIZE: BitwuzlaOption = 24;
143pub const BITWUZLA_OPT_ABSTRACTION_EAGER_REFINE: BitwuzlaOption = 25;
144pub const BITWUZLA_OPT_ABSTRACTION_VALUE_LIMIT: BitwuzlaOption = 26;
145pub const BITWUZLA_OPT_ABSTRACTION_VALUE_ONLY: BitwuzlaOption = 27;
146pub const BITWUZLA_OPT_ABSTRACTION_ASSERT: BitwuzlaOption = 28;
147pub const BITWUZLA_OPT_ABSTRACTION_ASSERT_REFS: BitwuzlaOption = 29;
148pub const BITWUZLA_OPT_ABSTRACTION_INITIAL_LEMMAS: BitwuzlaOption = 30;
149pub const BITWUZLA_OPT_ABSTRACTION_INC_BITBLAST: BitwuzlaOption = 31;
150pub const BITWUZLA_OPT_ABSTRACTION_BV_ADD: BitwuzlaOption = 32;
151pub const BITWUZLA_OPT_ABSTRACTION_BV_MUL: BitwuzlaOption = 33;
152pub const BITWUZLA_OPT_ABSTRACTION_BV_UDIV: BitwuzlaOption = 34;
153pub const BITWUZLA_OPT_ABSTRACTION_BV_UREM: BitwuzlaOption = 35;
154pub const BITWUZLA_OPT_ABSTRACTION_EQUAL: BitwuzlaOption = 36;
155pub const BITWUZLA_OPT_ABSTRACTION_ITE: BitwuzlaOption = 37;
156pub const BITWUZLA_OPT_PREPROCESS: BitwuzlaOption = 38;
157pub const BITWUZLA_OPT_PP_CONTRADICTING_ANDS: BitwuzlaOption = 39;
158pub const BITWUZLA_OPT_PP_ELIM_BV_EXTRACTS: BitwuzlaOption = 40;
159pub const BITWUZLA_OPT_PP_ELIM_BV_UDIV: BitwuzlaOption = 41;
160pub const BITWUZLA_OPT_PP_EMBEDDED_CONSTR: BitwuzlaOption = 42;
161pub const BITWUZLA_OPT_PP_FLATTEN_AND: BitwuzlaOption = 43;
162pub const BITWUZLA_OPT_PP_NORMALIZE: BitwuzlaOption = 44;
163pub const BITWUZLA_OPT_PP_SKELETON_PREPROC: BitwuzlaOption = 45;
164pub const BITWUZLA_OPT_PP_VARIABLE_SUBST: BitwuzlaOption = 46;
165pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_EQ: BitwuzlaOption = 47;
166pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_DISEQ: BitwuzlaOption = 48;
167pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_BV_INEQ: BitwuzlaOption = 49;
168pub const BITWUZLA_OPT_DBG_RW_NODE_THRESH: BitwuzlaOption = 50;
169pub const BITWUZLA_OPT_DBG_PP_NODE_THRESH: BitwuzlaOption = 51;
170pub const BITWUZLA_OPT_DBG_CHECK_MODEL: BitwuzlaOption = 52;
171pub const BITWUZLA_OPT_DBG_CHECK_UNSAT_CORE: BitwuzlaOption = 53;
172pub const BITWUZLA_OPT_NUM_OPTS: BitwuzlaOption = 54;
173pub type BitwuzlaOption = ::std::os::raw::c_uint;
174unsafe extern "C" {
175    pub fn bitwuzla_copyright() -> *const ::std::os::raw::c_char;
176}
177unsafe extern "C" {
178    pub fn bitwuzla_version() -> *const ::std::os::raw::c_char;
179}
180unsafe extern "C" {
181    pub fn bitwuzla_git_id() -> *const ::std::os::raw::c_char;
182}
183#[repr(C)]
184#[derive(Debug, Copy, Clone)]
185pub struct BitwuzlaOptionInfo {
186    pub opt: BitwuzlaOption,
187    pub shrt: *const ::std::os::raw::c_char,
188    pub lng: *const ::std::os::raw::c_char,
189    pub description: *const ::std::os::raw::c_char,
190    pub is_numeric: bool,
191    pub is_mode: bool,
192    pub is_string: bool,
193    pub numeric: BitwuzlaOptionInfo_NumericValue,
194    pub mode: BitwuzlaOptionInfo_ModeValue,
195    pub string: BitwuzlaOptionInfo_StringValue,
196}
197#[repr(C)]
198#[derive(Debug, Copy, Clone)]
199pub struct BitwuzlaOptionInfo_NumericValue {
200    pub cur: u64,
201    pub dflt: u64,
202    pub min: u64,
203    pub max: u64,
204}
205#[allow(clippy::unnecessary_operation, clippy::identity_op)]
206const _: () = {
207    ["Size of BitwuzlaOptionInfo_NumericValue"]
208        [::std::mem::size_of::<BitwuzlaOptionInfo_NumericValue>() - 32usize];
209    ["Alignment of BitwuzlaOptionInfo_NumericValue"]
210        [::std::mem::align_of::<BitwuzlaOptionInfo_NumericValue>() - 8usize];
211    ["Offset of field: BitwuzlaOptionInfo_NumericValue::cur"]
212        [::std::mem::offset_of!(BitwuzlaOptionInfo_NumericValue, cur) - 0usize];
213    ["Offset of field: BitwuzlaOptionInfo_NumericValue::dflt"]
214        [::std::mem::offset_of!(BitwuzlaOptionInfo_NumericValue, dflt) - 8usize];
215    ["Offset of field: BitwuzlaOptionInfo_NumericValue::min"]
216        [::std::mem::offset_of!(BitwuzlaOptionInfo_NumericValue, min) - 16usize];
217    ["Offset of field: BitwuzlaOptionInfo_NumericValue::max"]
218        [::std::mem::offset_of!(BitwuzlaOptionInfo_NumericValue, max) - 24usize];
219};
220#[repr(C)]
221#[derive(Debug, Copy, Clone)]
222pub struct BitwuzlaOptionInfo_ModeValue {
223    pub cur: *const ::std::os::raw::c_char,
224    pub dflt: *const ::std::os::raw::c_char,
225    pub num_modes: usize,
226    pub modes: *mut *const ::std::os::raw::c_char,
227}
228#[allow(clippy::unnecessary_operation, clippy::identity_op)]
229const _: () = {
230    ["Size of BitwuzlaOptionInfo_ModeValue"]
231        [::std::mem::size_of::<BitwuzlaOptionInfo_ModeValue>() - 32usize];
232    ["Alignment of BitwuzlaOptionInfo_ModeValue"]
233        [::std::mem::align_of::<BitwuzlaOptionInfo_ModeValue>() - 8usize];
234    ["Offset of field: BitwuzlaOptionInfo_ModeValue::cur"]
235        [::std::mem::offset_of!(BitwuzlaOptionInfo_ModeValue, cur) - 0usize];
236    ["Offset of field: BitwuzlaOptionInfo_ModeValue::dflt"]
237        [::std::mem::offset_of!(BitwuzlaOptionInfo_ModeValue, dflt) - 8usize];
238    ["Offset of field: BitwuzlaOptionInfo_ModeValue::num_modes"]
239        [::std::mem::offset_of!(BitwuzlaOptionInfo_ModeValue, num_modes) - 16usize];
240    ["Offset of field: BitwuzlaOptionInfo_ModeValue::modes"]
241        [::std::mem::offset_of!(BitwuzlaOptionInfo_ModeValue, modes) - 24usize];
242};
243#[repr(C)]
244#[derive(Debug, Copy, Clone)]
245pub struct BitwuzlaOptionInfo_StringValue {
246    pub cur: *const ::std::os::raw::c_char,
247    pub dflt: *const ::std::os::raw::c_char,
248}
249#[allow(clippy::unnecessary_operation, clippy::identity_op)]
250const _: () = {
251    ["Size of BitwuzlaOptionInfo_StringValue"]
252        [::std::mem::size_of::<BitwuzlaOptionInfo_StringValue>() - 16usize];
253    ["Alignment of BitwuzlaOptionInfo_StringValue"]
254        [::std::mem::align_of::<BitwuzlaOptionInfo_StringValue>() - 8usize];
255    ["Offset of field: BitwuzlaOptionInfo_StringValue::cur"]
256        [::std::mem::offset_of!(BitwuzlaOptionInfo_StringValue, cur) - 0usize];
257    ["Offset of field: BitwuzlaOptionInfo_StringValue::dflt"]
258        [::std::mem::offset_of!(BitwuzlaOptionInfo_StringValue, dflt) - 8usize];
259};
260#[allow(clippy::unnecessary_operation, clippy::identity_op)]
261const _: () = {
262    ["Size of BitwuzlaOptionInfo"][::std::mem::size_of::<BitwuzlaOptionInfo>() - 120usize];
263    ["Alignment of BitwuzlaOptionInfo"][::std::mem::align_of::<BitwuzlaOptionInfo>() - 8usize];
264    ["Offset of field: BitwuzlaOptionInfo::opt"]
265        [::std::mem::offset_of!(BitwuzlaOptionInfo, opt) - 0usize];
266    ["Offset of field: BitwuzlaOptionInfo::shrt"]
267        [::std::mem::offset_of!(BitwuzlaOptionInfo, shrt) - 8usize];
268    ["Offset of field: BitwuzlaOptionInfo::lng"]
269        [::std::mem::offset_of!(BitwuzlaOptionInfo, lng) - 16usize];
270    ["Offset of field: BitwuzlaOptionInfo::description"]
271        [::std::mem::offset_of!(BitwuzlaOptionInfo, description) - 24usize];
272    ["Offset of field: BitwuzlaOptionInfo::is_numeric"]
273        [::std::mem::offset_of!(BitwuzlaOptionInfo, is_numeric) - 32usize];
274    ["Offset of field: BitwuzlaOptionInfo::is_mode"]
275        [::std::mem::offset_of!(BitwuzlaOptionInfo, is_mode) - 33usize];
276    ["Offset of field: BitwuzlaOptionInfo::is_string"]
277        [::std::mem::offset_of!(BitwuzlaOptionInfo, is_string) - 34usize];
278    ["Offset of field: BitwuzlaOptionInfo::numeric"]
279        [::std::mem::offset_of!(BitwuzlaOptionInfo, numeric) - 40usize];
280    ["Offset of field: BitwuzlaOptionInfo::mode"]
281        [::std::mem::offset_of!(BitwuzlaOptionInfo, mode) - 72usize];
282    ["Offset of field: BitwuzlaOptionInfo::string"]
283        [::std::mem::offset_of!(BitwuzlaOptionInfo, string) - 104usize];
284};
285#[repr(C)]
286#[derive(Debug, Copy, Clone)]
287pub struct BitwuzlaOptions {
288    _unused: [u8; 0],
289}
290unsafe extern "C" {
291    pub fn bitwuzla_options_new() -> *mut BitwuzlaOptions;
292}
293unsafe extern "C" {
294    pub fn bitwuzla_options_delete(options: *mut BitwuzlaOptions);
295}
296unsafe extern "C" {
297    pub fn bitwuzla_option_is_valid(
298        options: *mut BitwuzlaOptions,
299        name: *const ::std::os::raw::c_char,
300    ) -> bool;
301}
302unsafe extern "C" {
303    pub fn bitwuzla_option_is_numeric(
304        options: *mut BitwuzlaOptions,
305        option: BitwuzlaOption,
306    ) -> bool;
307}
308unsafe extern "C" {
309    pub fn bitwuzla_option_is_mode(options: *mut BitwuzlaOptions, option: BitwuzlaOption) -> bool;
310}
311unsafe extern "C" {
312    pub fn bitwuzla_option_is_string(options: *mut BitwuzlaOptions, option: BitwuzlaOption)
313        -> bool;
314}
315unsafe extern "C" {
316    pub fn bitwuzla_set_option(options: *mut BitwuzlaOptions, option: BitwuzlaOption, val: u64);
317}
318unsafe extern "C" {
319    pub fn bitwuzla_set_option_mode(
320        options: *mut BitwuzlaOptions,
321        option: BitwuzlaOption,
322        val: *const ::std::os::raw::c_char,
323    );
324}
325unsafe extern "C" {
326    pub fn bitwuzla_set_option_string(
327        options: *mut BitwuzlaOptions,
328        option: BitwuzlaOption,
329        val: *const ::std::os::raw::c_char,
330    );
331}
332unsafe extern "C" {
333    pub fn bitwuzla_get_option(options: *mut BitwuzlaOptions, option: BitwuzlaOption) -> u64;
334}
335unsafe extern "C" {
336    pub fn bitwuzla_get_option_mode(
337        options: *mut BitwuzlaOptions,
338        option: BitwuzlaOption,
339    ) -> *const ::std::os::raw::c_char;
340}
341unsafe extern "C" {
342    pub fn bitwuzla_get_option_string(
343        options: *mut BitwuzlaOptions,
344        option: BitwuzlaOption,
345    ) -> *const ::std::os::raw::c_char;
346}
347unsafe extern "C" {
348    pub fn bitwuzla_get_option_info(
349        options: *mut BitwuzlaOptions,
350        option: BitwuzlaOption,
351        info: *mut BitwuzlaOptionInfo,
352    );
353}
354unsafe extern "C" {
355    pub fn bitwuzla_result_to_string(result: BitwuzlaResult) -> *const ::std::os::raw::c_char;
356}
357unsafe extern "C" {
358    pub fn bitwuzla_rm_to_string(rm: BitwuzlaRoundingMode) -> *const ::std::os::raw::c_char;
359}
360unsafe extern "C" {
361    pub fn bitwuzla_kind_to_string(kind: BitwuzlaKind) -> *const ::std::os::raw::c_char;
362}
363pub type BitwuzlaSort = u64;
364unsafe extern "C" {
365    pub fn bitwuzla_sort_hash(sort: BitwuzlaSort) -> usize;
366}
367unsafe extern "C" {
368    pub fn bitwuzla_sort_copy(sort: BitwuzlaSort) -> BitwuzlaSort;
369}
370unsafe extern "C" {
371    pub fn bitwuzla_sort_release(sort: BitwuzlaSort);
372}
373unsafe extern "C" {
374    pub fn bitwuzla_sort_bv_get_size(sort: BitwuzlaSort) -> u64;
375}
376unsafe extern "C" {
377    pub fn bitwuzla_sort_fp_get_exp_size(sort: BitwuzlaSort) -> u64;
378}
379unsafe extern "C" {
380    pub fn bitwuzla_sort_fp_get_sig_size(sort: BitwuzlaSort) -> u64;
381}
382unsafe extern "C" {
383    pub fn bitwuzla_sort_array_get_index(sort: BitwuzlaSort) -> BitwuzlaSort;
384}
385unsafe extern "C" {
386    pub fn bitwuzla_sort_array_get_element(sort: BitwuzlaSort) -> BitwuzlaSort;
387}
388unsafe extern "C" {
389    pub fn bitwuzla_sort_fun_get_domain_sorts(
390        sort: BitwuzlaSort,
391        size: *mut usize,
392    ) -> *mut BitwuzlaSort;
393}
394unsafe extern "C" {
395    pub fn bitwuzla_sort_fun_get_codomain(sort: BitwuzlaSort) -> BitwuzlaSort;
396}
397unsafe extern "C" {
398    pub fn bitwuzla_sort_fun_get_arity(sort: BitwuzlaSort) -> u64;
399}
400unsafe extern "C" {
401    pub fn bitwuzla_sort_get_uninterpreted_symbol(
402        sort: BitwuzlaSort,
403    ) -> *const ::std::os::raw::c_char;
404}
405unsafe extern "C" {
406    pub fn bitwuzla_sort_is_array(sort: BitwuzlaSort) -> bool;
407}
408unsafe extern "C" {
409    pub fn bitwuzla_sort_is_bool(sort: BitwuzlaSort) -> bool;
410}
411unsafe extern "C" {
412    pub fn bitwuzla_sort_is_bv(sort: BitwuzlaSort) -> bool;
413}
414unsafe extern "C" {
415    pub fn bitwuzla_sort_is_fp(sort: BitwuzlaSort) -> bool;
416}
417unsafe extern "C" {
418    pub fn bitwuzla_sort_is_fun(sort: BitwuzlaSort) -> bool;
419}
420unsafe extern "C" {
421    pub fn bitwuzla_sort_is_rm(sort: BitwuzlaSort) -> bool;
422}
423unsafe extern "C" {
424    pub fn bitwuzla_sort_is_uninterpreted(sort: BitwuzlaSort) -> bool;
425}
426unsafe extern "C" {
427    pub fn bitwuzla_sort_to_string(sort: BitwuzlaSort) -> *const ::std::os::raw::c_char;
428}
429unsafe extern "C" {
430    pub fn bitwuzla_sort_print(sort: BitwuzlaSort, file: *mut FILE);
431}
432pub type BitwuzlaTerm = u64;
433unsafe extern "C" {
434    pub fn bitwuzla_term_hash(term: BitwuzlaTerm) -> usize;
435}
436unsafe extern "C" {
437    pub fn bitwuzla_term_copy(term: BitwuzlaTerm) -> BitwuzlaTerm;
438}
439unsafe extern "C" {
440    pub fn bitwuzla_term_release(term: BitwuzlaTerm);
441}
442unsafe extern "C" {
443    pub fn bitwuzla_term_get_kind(term: BitwuzlaTerm) -> BitwuzlaKind;
444}
445unsafe extern "C" {
446    pub fn bitwuzla_term_get_children(term: BitwuzlaTerm, size: *mut usize) -> *mut BitwuzlaTerm;
447}
448unsafe extern "C" {
449    pub fn bitwuzla_term_get_indices(term: BitwuzlaTerm, size: *mut usize) -> *mut u64;
450}
451unsafe extern "C" {
452    pub fn bitwuzla_term_is_indexed(term: BitwuzlaTerm) -> bool;
453}
454unsafe extern "C" {
455    pub fn bitwuzla_term_get_sort(term: BitwuzlaTerm) -> BitwuzlaSort;
456}
457unsafe extern "C" {
458    pub fn bitwuzla_term_array_get_index_sort(term: BitwuzlaTerm) -> BitwuzlaSort;
459}
460unsafe extern "C" {
461    pub fn bitwuzla_term_array_get_element_sort(term: BitwuzlaTerm) -> BitwuzlaSort;
462}
463unsafe extern "C" {
464    pub fn bitwuzla_term_fun_get_domain_sorts(
465        term: BitwuzlaTerm,
466        size: *mut usize,
467    ) -> *mut BitwuzlaSort;
468}
469unsafe extern "C" {
470    pub fn bitwuzla_term_fun_get_codomain_sort(term: BitwuzlaTerm) -> BitwuzlaSort;
471}
472unsafe extern "C" {
473    pub fn bitwuzla_term_bv_get_size(term: BitwuzlaTerm) -> u64;
474}
475unsafe extern "C" {
476    pub fn bitwuzla_term_fp_get_exp_size(term: BitwuzlaTerm) -> u64;
477}
478unsafe extern "C" {
479    pub fn bitwuzla_term_fp_get_sig_size(term: BitwuzlaTerm) -> u64;
480}
481unsafe extern "C" {
482    pub fn bitwuzla_term_fun_get_arity(term: BitwuzlaTerm) -> u64;
483}
484unsafe extern "C" {
485    pub fn bitwuzla_term_get_symbol(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char;
486}
487unsafe extern "C" {
488    pub fn bitwuzla_term_is_equal_sort(term0: BitwuzlaTerm, term1: BitwuzlaTerm) -> bool;
489}
490unsafe extern "C" {
491    pub fn bitwuzla_term_is_array(term: BitwuzlaTerm) -> bool;
492}
493unsafe extern "C" {
494    pub fn bitwuzla_term_is_const(term: BitwuzlaTerm) -> bool;
495}
496unsafe extern "C" {
497    pub fn bitwuzla_term_is_fun(term: BitwuzlaTerm) -> bool;
498}
499unsafe extern "C" {
500    pub fn bitwuzla_term_is_var(term: BitwuzlaTerm) -> bool;
501}
502unsafe extern "C" {
503    pub fn bitwuzla_term_is_value(term: BitwuzlaTerm) -> bool;
504}
505unsafe extern "C" {
506    pub fn bitwuzla_term_is_bv_value(term: BitwuzlaTerm) -> bool;
507}
508unsafe extern "C" {
509    pub fn bitwuzla_term_is_fp_value(term: BitwuzlaTerm) -> bool;
510}
511unsafe extern "C" {
512    pub fn bitwuzla_term_is_rm_value(term: BitwuzlaTerm) -> bool;
513}
514unsafe extern "C" {
515    pub fn bitwuzla_term_is_bool(term: BitwuzlaTerm) -> bool;
516}
517unsafe extern "C" {
518    pub fn bitwuzla_term_is_bv(term: BitwuzlaTerm) -> bool;
519}
520unsafe extern "C" {
521    pub fn bitwuzla_term_is_fp(term: BitwuzlaTerm) -> bool;
522}
523unsafe extern "C" {
524    pub fn bitwuzla_term_is_rm(term: BitwuzlaTerm) -> bool;
525}
526unsafe extern "C" {
527    pub fn bitwuzla_term_is_uninterpreted(term: BitwuzlaTerm) -> bool;
528}
529unsafe extern "C" {
530    pub fn bitwuzla_term_is_true(term: BitwuzlaTerm) -> bool;
531}
532unsafe extern "C" {
533    pub fn bitwuzla_term_is_false(term: BitwuzlaTerm) -> bool;
534}
535unsafe extern "C" {
536    pub fn bitwuzla_term_is_bv_value_zero(term: BitwuzlaTerm) -> bool;
537}
538unsafe extern "C" {
539    pub fn bitwuzla_term_is_bv_value_one(term: BitwuzlaTerm) -> bool;
540}
541unsafe extern "C" {
542    pub fn bitwuzla_term_is_bv_value_ones(term: BitwuzlaTerm) -> bool;
543}
544unsafe extern "C" {
545    pub fn bitwuzla_term_is_bv_value_min_signed(term: BitwuzlaTerm) -> bool;
546}
547unsafe extern "C" {
548    pub fn bitwuzla_term_is_bv_value_max_signed(term: BitwuzlaTerm) -> bool;
549}
550unsafe extern "C" {
551    pub fn bitwuzla_term_is_fp_value_pos_zero(term: BitwuzlaTerm) -> bool;
552}
553unsafe extern "C" {
554    pub fn bitwuzla_term_is_fp_value_neg_zero(term: BitwuzlaTerm) -> bool;
555}
556unsafe extern "C" {
557    pub fn bitwuzla_term_is_fp_value_pos_inf(term: BitwuzlaTerm) -> bool;
558}
559unsafe extern "C" {
560    pub fn bitwuzla_term_is_fp_value_neg_inf(term: BitwuzlaTerm) -> bool;
561}
562unsafe extern "C" {
563    pub fn bitwuzla_term_is_fp_value_nan(term: BitwuzlaTerm) -> bool;
564}
565unsafe extern "C" {
566    pub fn bitwuzla_term_is_rm_value_rna(term: BitwuzlaTerm) -> bool;
567}
568unsafe extern "C" {
569    pub fn bitwuzla_term_is_rm_value_rne(term: BitwuzlaTerm) -> bool;
570}
571unsafe extern "C" {
572    pub fn bitwuzla_term_is_rm_value_rtn(term: BitwuzlaTerm) -> bool;
573}
574unsafe extern "C" {
575    pub fn bitwuzla_term_is_rm_value_rtp(term: BitwuzlaTerm) -> bool;
576}
577unsafe extern "C" {
578    pub fn bitwuzla_term_is_rm_value_rtz(term: BitwuzlaTerm) -> bool;
579}
580unsafe extern "C" {
581    pub fn bitwuzla_term_value_get_bool(term: BitwuzlaTerm) -> bool;
582}
583unsafe extern "C" {
584    pub fn bitwuzla_term_value_get_str(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char;
585}
586unsafe extern "C" {
587    pub fn bitwuzla_term_value_get_str_fmt(
588        term: BitwuzlaTerm,
589        base: u8,
590    ) -> *const ::std::os::raw::c_char;
591}
592unsafe extern "C" {
593    pub fn bitwuzla_term_value_get_fp_ieee(
594        term: BitwuzlaTerm,
595        sign: *mut *const ::std::os::raw::c_char,
596        exponent: *mut *const ::std::os::raw::c_char,
597        significand: *mut *const ::std::os::raw::c_char,
598        base: u8,
599    );
600}
601unsafe extern "C" {
602    pub fn bitwuzla_term_value_get_rm(term: BitwuzlaTerm) -> BitwuzlaRoundingMode;
603}
604unsafe extern "C" {
605    pub fn bitwuzla_term_to_string(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char;
606}
607unsafe extern "C" {
608    pub fn bitwuzla_term_to_string_fmt(
609        term: BitwuzlaTerm,
610        base: u8,
611    ) -> *const ::std::os::raw::c_char;
612}
613unsafe extern "C" {
614    pub fn bitwuzla_term_fp_value_to_real_string(
615        term: BitwuzlaTerm,
616    ) -> *const ::std::os::raw::c_char;
617}
618unsafe extern "C" {
619    pub fn bitwuzla_term_print(term: BitwuzlaTerm, file: *mut FILE);
620}
621unsafe extern "C" {
622    pub fn bitwuzla_term_print_fmt(term: BitwuzlaTerm, file: *mut FILE, base: u8);
623}
624#[repr(C)]
625#[derive(Debug, Copy, Clone)]
626pub struct BitwuzlaTermManager {
627    _unused: [u8; 0],
628}
629#[repr(C)]
630#[derive(Debug, Copy, Clone)]
631pub struct Bitwuzla {
632    _unused: [u8; 0],
633}
634unsafe extern "C" {
635    pub fn bitwuzla_new(
636        tm: *mut BitwuzlaTermManager,
637        options: *const BitwuzlaOptions,
638    ) -> *mut Bitwuzla;
639}
640unsafe extern "C" {
641    pub fn bitwuzla_delete(bitwuzla: *mut Bitwuzla);
642}
643unsafe extern "C" {
644    pub fn bitwuzla_set_termination_callback(
645        bitwuzla: *mut Bitwuzla,
646        fun: ::std::option::Option<unsafe extern "C" fn(arg1: *mut ::std::os::raw::c_void) -> i32>,
647        state: *mut ::std::os::raw::c_void,
648    );
649}
650unsafe extern "C" {
651    pub fn bitwuzla_get_termination_callback_state(
652        bitwuzla: *mut Bitwuzla,
653    ) -> *mut ::std::os::raw::c_void;
654}
655unsafe extern "C" {
656    pub fn bitwuzla_set_abort_callback(
657        fun: ::std::option::Option<unsafe extern "C" fn(msg: *const ::std::os::raw::c_char)>,
658    );
659}
660unsafe extern "C" {
661    pub fn bitwuzla_push(bitwuzla: *mut Bitwuzla, nlevels: u64);
662}
663unsafe extern "C" {
664    pub fn bitwuzla_pop(bitwuzla: *mut Bitwuzla, nlevels: u64);
665}
666unsafe extern "C" {
667    pub fn bitwuzla_assert(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm);
668}
669unsafe extern "C" {
670    pub fn bitwuzla_get_assertions(
671        bitwuzla: *mut Bitwuzla,
672        size: *mut usize,
673    ) -> *const BitwuzlaTerm;
674}
675unsafe extern "C" {
676    pub fn bitwuzla_is_unsat_assumption(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> bool;
677}
678unsafe extern "C" {
679    pub fn bitwuzla_get_unsat_assumptions(
680        bitwuzla: *mut Bitwuzla,
681        size: *mut usize,
682    ) -> *const BitwuzlaTerm;
683}
684unsafe extern "C" {
685    pub fn bitwuzla_get_unsat_core(
686        bitwuzla: *mut Bitwuzla,
687        size: *mut usize,
688    ) -> *const BitwuzlaTerm;
689}
690unsafe extern "C" {
691    pub fn bitwuzla_simplify(bitwuzla: *mut Bitwuzla);
692}
693unsafe extern "C" {
694    pub fn bitwuzla_simplify_term(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> BitwuzlaTerm;
695}
696unsafe extern "C" {
697    pub fn bitwuzla_check_sat(bitwuzla: *mut Bitwuzla) -> BitwuzlaResult;
698}
699unsafe extern "C" {
700    pub fn bitwuzla_check_sat_assuming(
701        bitwuzla: *mut Bitwuzla,
702        argc: u32,
703        args: *mut BitwuzlaTerm,
704    ) -> BitwuzlaResult;
705}
706unsafe extern "C" {
707    pub fn bitwuzla_get_value(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> BitwuzlaTerm;
708}
709unsafe extern "C" {
710    pub fn bitwuzla_print_formula(
711        bitwuzla: *mut Bitwuzla,
712        format: *const ::std::os::raw::c_char,
713        file: *mut FILE,
714        base: u8,
715    );
716}
717unsafe extern "C" {
718    pub fn bitwuzla_print_unsat_core(
719        bitwuzla: *mut Bitwuzla,
720        format: *const ::std::os::raw::c_char,
721        file: *mut FILE,
722        base: u8,
723    );
724}
725unsafe extern "C" {
726    pub fn bitwuzla_get_statistics(
727        bitwuzla: *mut Bitwuzla,
728        keys: *mut *mut *const ::std::os::raw::c_char,
729        values: *mut *mut *const ::std::os::raw::c_char,
730        size: *mut usize,
731    );
732}
733unsafe extern "C" {
734    pub fn bitwuzla_get_term_mgr(bitwuzla: *mut Bitwuzla) -> *mut BitwuzlaTermManager;
735}
736unsafe extern "C" {
737    pub fn bitwuzla_term_manager_new() -> *mut BitwuzlaTermManager;
738}
739unsafe extern "C" {
740    pub fn bitwuzla_term_manager_delete(tm: *mut BitwuzlaTermManager);
741}
742unsafe extern "C" {
743    pub fn bitwuzla_term_manager_release(tm: *mut BitwuzlaTermManager);
744}
745unsafe extern "C" {
746    pub fn bitwuzla_mk_array_sort(
747        tm: *mut BitwuzlaTermManager,
748        index: BitwuzlaSort,
749        element: BitwuzlaSort,
750    ) -> BitwuzlaSort;
751}
752unsafe extern "C" {
753    pub fn bitwuzla_mk_bool_sort(tm: *mut BitwuzlaTermManager) -> BitwuzlaSort;
754}
755unsafe extern "C" {
756    pub fn bitwuzla_mk_bv_sort(tm: *mut BitwuzlaTermManager, size: u64) -> BitwuzlaSort;
757}
758unsafe extern "C" {
759    pub fn bitwuzla_mk_fp_sort(
760        tm: *mut BitwuzlaTermManager,
761        exp_size: u64,
762        sig_size: u64,
763    ) -> BitwuzlaSort;
764}
765unsafe extern "C" {
766    pub fn bitwuzla_mk_fun_sort(
767        tm: *mut BitwuzlaTermManager,
768        arity: u64,
769        domain: *mut BitwuzlaSort,
770        codomain: BitwuzlaSort,
771    ) -> BitwuzlaSort;
772}
773unsafe extern "C" {
774    pub fn bitwuzla_mk_rm_sort(tm: *mut BitwuzlaTermManager) -> BitwuzlaSort;
775}
776unsafe extern "C" {
777    pub fn bitwuzla_mk_uninterpreted_sort(
778        tm: *mut BitwuzlaTermManager,
779        symbol: *const ::std::os::raw::c_char,
780    ) -> BitwuzlaSort;
781}
782unsafe extern "C" {
783    pub fn bitwuzla_mk_true(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm;
784}
785unsafe extern "C" {
786    pub fn bitwuzla_mk_false(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm;
787}
788unsafe extern "C" {
789    pub fn bitwuzla_mk_bv_zero(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm;
790}
791unsafe extern "C" {
792    pub fn bitwuzla_mk_bv_one(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm;
793}
794unsafe extern "C" {
795    pub fn bitwuzla_mk_bv_ones(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm;
796}
797unsafe extern "C" {
798    pub fn bitwuzla_mk_bv_min_signed(
799        tm: *mut BitwuzlaTermManager,
800        sort: BitwuzlaSort,
801    ) -> BitwuzlaTerm;
802}
803unsafe extern "C" {
804    pub fn bitwuzla_mk_bv_max_signed(
805        tm: *mut BitwuzlaTermManager,
806        sort: BitwuzlaSort,
807    ) -> BitwuzlaTerm;
808}
809unsafe extern "C" {
810    pub fn bitwuzla_mk_fp_pos_zero(
811        tm: *mut BitwuzlaTermManager,
812        sort: BitwuzlaSort,
813    ) -> BitwuzlaTerm;
814}
815unsafe extern "C" {
816    pub fn bitwuzla_mk_fp_neg_zero(
817        tm: *mut BitwuzlaTermManager,
818        sort: BitwuzlaSort,
819    ) -> BitwuzlaTerm;
820}
821unsafe extern "C" {
822    pub fn bitwuzla_mk_fp_pos_inf(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort)
823        -> BitwuzlaTerm;
824}
825unsafe extern "C" {
826    pub fn bitwuzla_mk_fp_neg_inf(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort)
827        -> BitwuzlaTerm;
828}
829unsafe extern "C" {
830    pub fn bitwuzla_mk_fp_nan(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm;
831}
832unsafe extern "C" {
833    pub fn bitwuzla_mk_bv_value(
834        tm: *mut BitwuzlaTermManager,
835        sort: BitwuzlaSort,
836        value: *const ::std::os::raw::c_char,
837        base: u8,
838    ) -> BitwuzlaTerm;
839}
840unsafe extern "C" {
841    pub fn bitwuzla_mk_bv_value_uint64(
842        tm: *mut BitwuzlaTermManager,
843        sort: BitwuzlaSort,
844        value: u64,
845    ) -> BitwuzlaTerm;
846}
847unsafe extern "C" {
848    pub fn bitwuzla_mk_bv_value_int64(
849        tm: *mut BitwuzlaTermManager,
850        sort: BitwuzlaSort,
851        value: i64,
852    ) -> BitwuzlaTerm;
853}
854unsafe extern "C" {
855    pub fn bitwuzla_mk_fp_value(
856        tm: *mut BitwuzlaTermManager,
857        bv_sign: BitwuzlaTerm,
858        bv_exponent: BitwuzlaTerm,
859        bv_significand: BitwuzlaTerm,
860    ) -> BitwuzlaTerm;
861}
862unsafe extern "C" {
863    pub fn bitwuzla_mk_fp_from_real(
864        tm: *mut BitwuzlaTermManager,
865        sort: BitwuzlaSort,
866        rm: BitwuzlaTerm,
867        real: *const ::std::os::raw::c_char,
868    ) -> BitwuzlaTerm;
869}
870unsafe extern "C" {
871    pub fn bitwuzla_mk_fp_from_rational(
872        tm: *mut BitwuzlaTermManager,
873        sort: BitwuzlaSort,
874        rm: BitwuzlaTerm,
875        num: *const ::std::os::raw::c_char,
876        den: *const ::std::os::raw::c_char,
877    ) -> BitwuzlaTerm;
878}
879unsafe extern "C" {
880    pub fn bitwuzla_mk_rm_value(
881        tm: *mut BitwuzlaTermManager,
882        rm: BitwuzlaRoundingMode,
883    ) -> BitwuzlaTerm;
884}
885unsafe extern "C" {
886    pub fn bitwuzla_mk_term1(
887        tm: *mut BitwuzlaTermManager,
888        kind: BitwuzlaKind,
889        arg: BitwuzlaTerm,
890    ) -> BitwuzlaTerm;
891}
892unsafe extern "C" {
893    pub fn bitwuzla_mk_term2(
894        tm: *mut BitwuzlaTermManager,
895        kind: BitwuzlaKind,
896        arg0: BitwuzlaTerm,
897        arg1: BitwuzlaTerm,
898    ) -> BitwuzlaTerm;
899}
900unsafe extern "C" {
901    pub fn bitwuzla_mk_term3(
902        tm: *mut BitwuzlaTermManager,
903        kind: BitwuzlaKind,
904        arg0: BitwuzlaTerm,
905        arg1: BitwuzlaTerm,
906        arg2: BitwuzlaTerm,
907    ) -> BitwuzlaTerm;
908}
909unsafe extern "C" {
910    pub fn bitwuzla_mk_term(
911        tm: *mut BitwuzlaTermManager,
912        kind: BitwuzlaKind,
913        argc: u32,
914        args: *mut BitwuzlaTerm,
915    ) -> BitwuzlaTerm;
916}
917unsafe extern "C" {
918    pub fn bitwuzla_mk_term1_indexed1(
919        tm: *mut BitwuzlaTermManager,
920        kind: BitwuzlaKind,
921        arg: BitwuzlaTerm,
922        idx: u64,
923    ) -> BitwuzlaTerm;
924}
925unsafe extern "C" {
926    pub fn bitwuzla_mk_term1_indexed2(
927        tm: *mut BitwuzlaTermManager,
928        kind: BitwuzlaKind,
929        arg: BitwuzlaTerm,
930        idx0: u64,
931        idx1: u64,
932    ) -> BitwuzlaTerm;
933}
934unsafe extern "C" {
935    pub fn bitwuzla_mk_term2_indexed1(
936        tm: *mut BitwuzlaTermManager,
937        kind: BitwuzlaKind,
938        arg0: BitwuzlaTerm,
939        arg1: BitwuzlaTerm,
940        idx: u64,
941    ) -> BitwuzlaTerm;
942}
943unsafe extern "C" {
944    pub fn bitwuzla_mk_term2_indexed2(
945        tm: *mut BitwuzlaTermManager,
946        kind: BitwuzlaKind,
947        arg0: BitwuzlaTerm,
948        arg1: BitwuzlaTerm,
949        idx0: u64,
950        idx1: u64,
951    ) -> BitwuzlaTerm;
952}
953unsafe extern "C" {
954    pub fn bitwuzla_mk_term_indexed(
955        tm: *mut BitwuzlaTermManager,
956        kind: BitwuzlaKind,
957        argc: u32,
958        args: *mut BitwuzlaTerm,
959        idxc: u32,
960        idxs: *const u64,
961    ) -> BitwuzlaTerm;
962}
963unsafe extern "C" {
964    pub fn bitwuzla_mk_const(
965        tm: *mut BitwuzlaTermManager,
966        sort: BitwuzlaSort,
967        symbol: *const ::std::os::raw::c_char,
968    ) -> BitwuzlaTerm;
969}
970unsafe extern "C" {
971    pub fn bitwuzla_mk_const_array(
972        tm: *mut BitwuzlaTermManager,
973        sort: BitwuzlaSort,
974        value: BitwuzlaTerm,
975    ) -> BitwuzlaTerm;
976}
977unsafe extern "C" {
978    pub fn bitwuzla_mk_var(
979        tm: *mut BitwuzlaTermManager,
980        sort: BitwuzlaSort,
981        symbol: *const ::std::os::raw::c_char,
982    ) -> BitwuzlaTerm;
983}
984unsafe extern "C" {
985    pub fn bitwuzla_substitute_term(
986        term: BitwuzlaTerm,
987        map_size: usize,
988        map_keys: *mut BitwuzlaTerm,
989        map_values: *mut BitwuzlaTerm,
990    ) -> BitwuzlaTerm;
991}
992unsafe extern "C" {
993    pub fn bitwuzla_substitute_terms(
994        terms_size: usize,
995        terms: *mut BitwuzlaTerm,
996        map_size: usize,
997        map_keys: *mut BitwuzlaTerm,
998        map_values: *mut BitwuzlaTerm,
999    );
1000}