1use 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}