boolector_sys/src-generated/
bindings.rs

1/* automatically generated by rust-bindgen 0.59.1 */
2
3use libc::FILE;
4
5#[repr(C)]
6#[derive(Debug, Copy, Clone)]
7pub struct Btor {
8    _unused: [u8; 0],
9}
10#[repr(C)]
11#[derive(Debug, Copy, Clone)]
12pub struct BtorNode {
13    _unused: [u8; 0],
14}
15pub const BtorSolverResult_BTOR_RESULT_SAT: BtorSolverResult = 10;
16pub const BtorSolverResult_BTOR_RESULT_UNSAT: BtorSolverResult = 20;
17pub const BtorSolverResult_BTOR_RESULT_UNKNOWN: BtorSolverResult = 0;
18pub type BtorSolverResult = ::std::os::raw::c_uint;
19#[repr(C)]
20#[derive(Debug, Copy, Clone)]
21pub struct BoolectorNode {
22    _unused: [u8; 0],
23}
24#[repr(C)]
25#[derive(Debug, Copy, Clone)]
26pub struct BoolectorAnonymous {
27    _unused: [u8; 0],
28}
29pub type BoolectorSort = *mut BoolectorAnonymous;
30#[repr(C)]
31#[derive(Debug, Copy, Clone)]
32pub struct BtorAbortCallback {
33    pub abort_fun: ::std::option::Option<unsafe extern "C" fn(msg: *const ::std::os::raw::c_char)>,
34    pub cb_fun: *mut ::std::os::raw::c_void,
35}
36#[test]
37fn bindgen_test_layout_BtorAbortCallback() {
38    assert_eq!(
39        ::std::mem::size_of::<BtorAbortCallback>(),
40        16usize,
41        concat!("Size of: ", stringify!(BtorAbortCallback))
42    );
43    assert_eq!(
44        ::std::mem::align_of::<BtorAbortCallback>(),
45        8usize,
46        concat!("Alignment of ", stringify!(BtorAbortCallback))
47    );
48    assert_eq!(
49        unsafe { &(*(::std::ptr::null::<BtorAbortCallback>())).abort_fun as *const _ as usize },
50        0usize,
51        concat!(
52            "Offset of field: ",
53            stringify!(BtorAbortCallback),
54            "::",
55            stringify!(abort_fun)
56        )
57    );
58    assert_eq!(
59        unsafe { &(*(::std::ptr::null::<BtorAbortCallback>())).cb_fun as *const _ as usize },
60        8usize,
61        concat!(
62            "Offset of field: ",
63            stringify!(BtorAbortCallback),
64            "::",
65            stringify!(cb_fun)
66        )
67    );
68}
69extern "C" {
70    pub fn boolector_new() -> *mut Btor;
71}
72extern "C" {
73    pub fn boolector_clone(btor: *mut Btor) -> *mut Btor;
74}
75extern "C" {
76    pub fn boolector_delete(btor: *mut Btor);
77}
78extern "C" {
79    pub fn boolector_set_term(
80        btor: *mut Btor,
81        fun: ::std::option::Option<unsafe extern "C" fn(arg1: *mut ::std::os::raw::c_void) -> i32>,
82        state: *mut ::std::os::raw::c_void,
83    );
84}
85extern "C" {
86    pub fn boolector_terminate(btor: *mut Btor) -> i32;
87}
88extern "C" {
89    pub fn boolector_set_abort(
90        fun: ::std::option::Option<unsafe extern "C" fn(msg: *const ::std::os::raw::c_char)>,
91    );
92}
93extern "C" {
94    pub fn boolector_set_msg_prefix(btor: *mut Btor, prefix: *const ::std::os::raw::c_char);
95}
96extern "C" {
97    pub fn boolector_get_refs(btor: *mut Btor) -> u32;
98}
99extern "C" {
100    pub fn boolector_reset_time(btor: *mut Btor);
101}
102extern "C" {
103    pub fn boolector_reset_stats(btor: *mut Btor);
104}
105extern "C" {
106    pub fn boolector_print_stats(btor: *mut Btor);
107}
108extern "C" {
109    pub fn boolector_set_trapi(btor: *mut Btor, apitrace: *mut FILE);
110}
111extern "C" {
112    pub fn boolector_get_trapi(btor: *mut Btor) -> *mut FILE;
113}
114extern "C" {
115    pub fn boolector_push(btor: *mut Btor, level: u32);
116}
117extern "C" {
118    pub fn boolector_pop(btor: *mut Btor, level: u32);
119}
120extern "C" {
121    pub fn boolector_assert(btor: *mut Btor, node: *mut BoolectorNode);
122}
123extern "C" {
124    pub fn boolector_assume(btor: *mut Btor, node: *mut BoolectorNode);
125}
126extern "C" {
127    pub fn boolector_failed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
128}
129extern "C" {
130    pub fn boolector_get_failed_assumptions(btor: *mut Btor) -> *mut *mut BoolectorNode;
131}
132extern "C" {
133    pub fn boolector_fixate_assumptions(btor: *mut Btor);
134}
135extern "C" {
136    pub fn boolector_reset_assumptions(btor: *mut Btor);
137}
138extern "C" {
139    pub fn boolector_sat(btor: *mut Btor) -> i32;
140}
141extern "C" {
142    pub fn boolector_limited_sat(btor: *mut Btor, lod_limit: i32, sat_limit: i32) -> i32;
143}
144extern "C" {
145    pub fn boolector_simplify(btor: *mut Btor) -> i32;
146}
147extern "C" {
148    pub fn boolector_set_sat_solver(btor: *mut Btor, solver: *const ::std::os::raw::c_char);
149}
150extern "C" {
151    pub fn boolector_set_opt(btor: *mut Btor, opt: BtorOption, val: u32);
152}
153extern "C" {
154    pub fn boolector_get_opt(btor: *mut Btor, opt: BtorOption) -> u32;
155}
156extern "C" {
157    pub fn boolector_get_opt_min(btor: *mut Btor, opt: BtorOption) -> u32;
158}
159extern "C" {
160    pub fn boolector_get_opt_max(btor: *mut Btor, opt: BtorOption) -> u32;
161}
162extern "C" {
163    pub fn boolector_get_opt_dflt(btor: *mut Btor, opt: BtorOption) -> u32;
164}
165extern "C" {
166    pub fn boolector_get_opt_lng(btor: *mut Btor, opt: BtorOption)
167        -> *const ::std::os::raw::c_char;
168}
169extern "C" {
170    pub fn boolector_get_opt_shrt(
171        btor: *mut Btor,
172        opt: BtorOption,
173    ) -> *const ::std::os::raw::c_char;
174}
175extern "C" {
176    pub fn boolector_get_opt_desc(
177        btor: *mut Btor,
178        opt: BtorOption,
179    ) -> *const ::std::os::raw::c_char;
180}
181extern "C" {
182    pub fn boolector_has_opt(Btor: *mut Btor, opt: BtorOption) -> bool;
183}
184extern "C" {
185    pub fn boolector_first_opt(btor: *mut Btor) -> BtorOption;
186}
187extern "C" {
188    pub fn boolector_next_opt(btor: *mut Btor, opt: BtorOption) -> BtorOption;
189}
190extern "C" {
191    pub fn boolector_copy(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
192}
193extern "C" {
194    pub fn boolector_release(btor: *mut Btor, node: *mut BoolectorNode);
195}
196extern "C" {
197    pub fn boolector_release_all(btor: *mut Btor);
198}
199extern "C" {
200    pub fn boolector_true(btor: *mut Btor) -> *mut BoolectorNode;
201}
202extern "C" {
203    pub fn boolector_false(btor: *mut Btor) -> *mut BoolectorNode;
204}
205extern "C" {
206    pub fn boolector_implies(
207        btor: *mut Btor,
208        n0: *mut BoolectorNode,
209        n1: *mut BoolectorNode,
210    ) -> *mut BoolectorNode;
211}
212extern "C" {
213    pub fn boolector_iff(
214        btor: *mut Btor,
215        n0: *mut BoolectorNode,
216        n1: *mut BoolectorNode,
217    ) -> *mut BoolectorNode;
218}
219extern "C" {
220    pub fn boolector_eq(
221        btor: *mut Btor,
222        n0: *mut BoolectorNode,
223        n1: *mut BoolectorNode,
224    ) -> *mut BoolectorNode;
225}
226extern "C" {
227    pub fn boolector_ne(
228        btor: *mut Btor,
229        n0: *mut BoolectorNode,
230        n1: *mut BoolectorNode,
231    ) -> *mut BoolectorNode;
232}
233extern "C" {
234    pub fn boolector_is_bv_const_zero(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
235}
236extern "C" {
237    pub fn boolector_is_bv_const_one(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
238}
239extern "C" {
240    pub fn boolector_is_bv_const_ones(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
241}
242extern "C" {
243    pub fn boolector_is_bv_const_max_signed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
244}
245extern "C" {
246    pub fn boolector_is_bv_const_min_signed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
247}
248extern "C" {
249    pub fn boolector_const(
250        btor: *mut Btor,
251        bits: *const ::std::os::raw::c_char,
252    ) -> *mut BoolectorNode;
253}
254extern "C" {
255    pub fn boolector_constd(
256        btor: *mut Btor,
257        sort: BoolectorSort,
258        str_: *const ::std::os::raw::c_char,
259    ) -> *mut BoolectorNode;
260}
261extern "C" {
262    pub fn boolector_consth(
263        btor: *mut Btor,
264        sort: BoolectorSort,
265        str_: *const ::std::os::raw::c_char,
266    ) -> *mut BoolectorNode;
267}
268extern "C" {
269    pub fn boolector_zero(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
270}
271extern "C" {
272    pub fn boolector_ones(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
273}
274extern "C" {
275    pub fn boolector_one(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
276}
277extern "C" {
278    pub fn boolector_min_signed(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
279}
280extern "C" {
281    pub fn boolector_max_signed(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
282}
283extern "C" {
284    pub fn boolector_unsigned_int(
285        btor: *mut Btor,
286        u: u32,
287        sort: BoolectorSort,
288    ) -> *mut BoolectorNode;
289}
290extern "C" {
291    pub fn boolector_int(btor: *mut Btor, i: i32, sort: BoolectorSort) -> *mut BoolectorNode;
292}
293extern "C" {
294    pub fn boolector_var(
295        btor: *mut Btor,
296        sort: BoolectorSort,
297        symbol: *const ::std::os::raw::c_char,
298    ) -> *mut BoolectorNode;
299}
300extern "C" {
301    pub fn boolector_array(
302        btor: *mut Btor,
303        sort: BoolectorSort,
304        symbol: *const ::std::os::raw::c_char,
305    ) -> *mut BoolectorNode;
306}
307extern "C" {
308    pub fn boolector_const_array(
309        btor: *mut Btor,
310        sort: BoolectorSort,
311        value: *mut BoolectorNode,
312    ) -> *mut BoolectorNode;
313}
314extern "C" {
315    pub fn boolector_uf(
316        btor: *mut Btor,
317        sort: BoolectorSort,
318        symbol: *const ::std::os::raw::c_char,
319    ) -> *mut BoolectorNode;
320}
321extern "C" {
322    pub fn boolector_not(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
323}
324extern "C" {
325    pub fn boolector_neg(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
326}
327extern "C" {
328    pub fn boolector_redor(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
329}
330extern "C" {
331    pub fn boolector_redxor(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
332}
333extern "C" {
334    pub fn boolector_redand(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
335}
336extern "C" {
337    pub fn boolector_slice(
338        btor: *mut Btor,
339        node: *mut BoolectorNode,
340        upper: u32,
341        lower: u32,
342    ) -> *mut BoolectorNode;
343}
344extern "C" {
345    pub fn boolector_uext(
346        btor: *mut Btor,
347        node: *mut BoolectorNode,
348        width: u32,
349    ) -> *mut BoolectorNode;
350}
351extern "C" {
352    pub fn boolector_sext(
353        btor: *mut Btor,
354        node: *mut BoolectorNode,
355        width: u32,
356    ) -> *mut BoolectorNode;
357}
358extern "C" {
359    pub fn boolector_xor(
360        btor: *mut Btor,
361        n0: *mut BoolectorNode,
362        n1: *mut BoolectorNode,
363    ) -> *mut BoolectorNode;
364}
365extern "C" {
366    pub fn boolector_xnor(
367        btor: *mut Btor,
368        n0: *mut BoolectorNode,
369        n1: *mut BoolectorNode,
370    ) -> *mut BoolectorNode;
371}
372extern "C" {
373    pub fn boolector_and(
374        btor: *mut Btor,
375        n0: *mut BoolectorNode,
376        n1: *mut BoolectorNode,
377    ) -> *mut BoolectorNode;
378}
379extern "C" {
380    pub fn boolector_nand(
381        btor: *mut Btor,
382        n0: *mut BoolectorNode,
383        n1: *mut BoolectorNode,
384    ) -> *mut BoolectorNode;
385}
386extern "C" {
387    pub fn boolector_or(
388        btor: *mut Btor,
389        n0: *mut BoolectorNode,
390        n1: *mut BoolectorNode,
391    ) -> *mut BoolectorNode;
392}
393extern "C" {
394    pub fn boolector_nor(
395        btor: *mut Btor,
396        n0: *mut BoolectorNode,
397        n1: *mut BoolectorNode,
398    ) -> *mut BoolectorNode;
399}
400extern "C" {
401    pub fn boolector_add(
402        btor: *mut Btor,
403        n0: *mut BoolectorNode,
404        n1: *mut BoolectorNode,
405    ) -> *mut BoolectorNode;
406}
407extern "C" {
408    pub fn boolector_uaddo(
409        btor: *mut Btor,
410        n0: *mut BoolectorNode,
411        n1: *mut BoolectorNode,
412    ) -> *mut BoolectorNode;
413}
414extern "C" {
415    pub fn boolector_saddo(
416        btor: *mut Btor,
417        n0: *mut BoolectorNode,
418        n1: *mut BoolectorNode,
419    ) -> *mut BoolectorNode;
420}
421extern "C" {
422    pub fn boolector_mul(
423        btor: *mut Btor,
424        n0: *mut BoolectorNode,
425        n1: *mut BoolectorNode,
426    ) -> *mut BoolectorNode;
427}
428extern "C" {
429    pub fn boolector_umulo(
430        btor: *mut Btor,
431        n0: *mut BoolectorNode,
432        n1: *mut BoolectorNode,
433    ) -> *mut BoolectorNode;
434}
435extern "C" {
436    pub fn boolector_smulo(
437        btor: *mut Btor,
438        n0: *mut BoolectorNode,
439        n1: *mut BoolectorNode,
440    ) -> *mut BoolectorNode;
441}
442extern "C" {
443    pub fn boolector_ult(
444        btor: *mut Btor,
445        n0: *mut BoolectorNode,
446        n1: *mut BoolectorNode,
447    ) -> *mut BoolectorNode;
448}
449extern "C" {
450    pub fn boolector_slt(
451        btor: *mut Btor,
452        n0: *mut BoolectorNode,
453        n1: *mut BoolectorNode,
454    ) -> *mut BoolectorNode;
455}
456extern "C" {
457    pub fn boolector_ulte(
458        btor: *mut Btor,
459        n0: *mut BoolectorNode,
460        n1: *mut BoolectorNode,
461    ) -> *mut BoolectorNode;
462}
463extern "C" {
464    pub fn boolector_slte(
465        btor: *mut Btor,
466        n0: *mut BoolectorNode,
467        n1: *mut BoolectorNode,
468    ) -> *mut BoolectorNode;
469}
470extern "C" {
471    pub fn boolector_ugt(
472        btor: *mut Btor,
473        n0: *mut BoolectorNode,
474        n1: *mut BoolectorNode,
475    ) -> *mut BoolectorNode;
476}
477extern "C" {
478    pub fn boolector_sgt(
479        btor: *mut Btor,
480        n0: *mut BoolectorNode,
481        n1: *mut BoolectorNode,
482    ) -> *mut BoolectorNode;
483}
484extern "C" {
485    pub fn boolector_ugte(
486        btor: *mut Btor,
487        n0: *mut BoolectorNode,
488        n1: *mut BoolectorNode,
489    ) -> *mut BoolectorNode;
490}
491extern "C" {
492    pub fn boolector_sgte(
493        btor: *mut Btor,
494        n0: *mut BoolectorNode,
495        n1: *mut BoolectorNode,
496    ) -> *mut BoolectorNode;
497}
498extern "C" {
499    pub fn boolector_sll(
500        btor: *mut Btor,
501        n0: *mut BoolectorNode,
502        n1: *mut BoolectorNode,
503    ) -> *mut BoolectorNode;
504}
505extern "C" {
506    pub fn boolector_srl(
507        btor: *mut Btor,
508        n0: *mut BoolectorNode,
509        n1: *mut BoolectorNode,
510    ) -> *mut BoolectorNode;
511}
512extern "C" {
513    pub fn boolector_sra(
514        btor: *mut Btor,
515        n0: *mut BoolectorNode,
516        n1: *mut BoolectorNode,
517    ) -> *mut BoolectorNode;
518}
519extern "C" {
520    pub fn boolector_rol(
521        btor: *mut Btor,
522        n0: *mut BoolectorNode,
523        n1: *mut BoolectorNode,
524    ) -> *mut BoolectorNode;
525}
526extern "C" {
527    pub fn boolector_ror(
528        btor: *mut Btor,
529        n0: *mut BoolectorNode,
530        n1: *mut BoolectorNode,
531    ) -> *mut BoolectorNode;
532}
533extern "C" {
534    pub fn boolector_roli(btor: *mut Btor, n: *mut BoolectorNode, nbits: u32)
535        -> *mut BoolectorNode;
536}
537extern "C" {
538    pub fn boolector_rori(btor: *mut Btor, n: *mut BoolectorNode, nbits: u32)
539        -> *mut BoolectorNode;
540}
541extern "C" {
542    pub fn boolector_sub(
543        btor: *mut Btor,
544        n0: *mut BoolectorNode,
545        n1: *mut BoolectorNode,
546    ) -> *mut BoolectorNode;
547}
548extern "C" {
549    pub fn boolector_usubo(
550        btor: *mut Btor,
551        n0: *mut BoolectorNode,
552        n1: *mut BoolectorNode,
553    ) -> *mut BoolectorNode;
554}
555extern "C" {
556    pub fn boolector_ssubo(
557        btor: *mut Btor,
558        n0: *mut BoolectorNode,
559        n1: *mut BoolectorNode,
560    ) -> *mut BoolectorNode;
561}
562extern "C" {
563    pub fn boolector_udiv(
564        btor: *mut Btor,
565        n0: *mut BoolectorNode,
566        n1: *mut BoolectorNode,
567    ) -> *mut BoolectorNode;
568}
569extern "C" {
570    pub fn boolector_sdiv(
571        btor: *mut Btor,
572        n0: *mut BoolectorNode,
573        n1: *mut BoolectorNode,
574    ) -> *mut BoolectorNode;
575}
576extern "C" {
577    pub fn boolector_sdivo(
578        btor: *mut Btor,
579        n0: *mut BoolectorNode,
580        n1: *mut BoolectorNode,
581    ) -> *mut BoolectorNode;
582}
583extern "C" {
584    pub fn boolector_urem(
585        btor: *mut Btor,
586        n0: *mut BoolectorNode,
587        n1: *mut BoolectorNode,
588    ) -> *mut BoolectorNode;
589}
590extern "C" {
591    pub fn boolector_srem(
592        btor: *mut Btor,
593        n0: *mut BoolectorNode,
594        n1: *mut BoolectorNode,
595    ) -> *mut BoolectorNode;
596}
597extern "C" {
598    pub fn boolector_smod(
599        btor: *mut Btor,
600        n0: *mut BoolectorNode,
601        n1: *mut BoolectorNode,
602    ) -> *mut BoolectorNode;
603}
604extern "C" {
605    pub fn boolector_concat(
606        btor: *mut Btor,
607        n0: *mut BoolectorNode,
608        n1: *mut BoolectorNode,
609    ) -> *mut BoolectorNode;
610}
611extern "C" {
612    pub fn boolector_repeat(
613        btor: *mut Btor,
614        node: *mut BoolectorNode,
615        n: u32,
616    ) -> *mut BoolectorNode;
617}
618extern "C" {
619    pub fn boolector_read(
620        btor: *mut Btor,
621        n_array: *mut BoolectorNode,
622        n_index: *mut BoolectorNode,
623    ) -> *mut BoolectorNode;
624}
625extern "C" {
626    pub fn boolector_write(
627        btor: *mut Btor,
628        n_array: *mut BoolectorNode,
629        n_index: *mut BoolectorNode,
630        n_value: *mut BoolectorNode,
631    ) -> *mut BoolectorNode;
632}
633extern "C" {
634    pub fn boolector_cond(
635        btor: *mut Btor,
636        n_cond: *mut BoolectorNode,
637        n_then: *mut BoolectorNode,
638        n_else: *mut BoolectorNode,
639    ) -> *mut BoolectorNode;
640}
641extern "C" {
642    pub fn boolector_param(
643        btor: *mut Btor,
644        sort: BoolectorSort,
645        symbol: *const ::std::os::raw::c_char,
646    ) -> *mut BoolectorNode;
647}
648extern "C" {
649    pub fn boolector_fun(
650        btor: *mut Btor,
651        param_nodes: *mut *mut BoolectorNode,
652        paramc: u32,
653        node: *mut BoolectorNode,
654    ) -> *mut BoolectorNode;
655}
656extern "C" {
657    pub fn boolector_apply(
658        btor: *mut Btor,
659        arg_nodes: *mut *mut BoolectorNode,
660        argc: u32,
661        n_fun: *mut BoolectorNode,
662    ) -> *mut BoolectorNode;
663}
664extern "C" {
665    pub fn boolector_inc(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
666}
667extern "C" {
668    pub fn boolector_dec(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
669}
670extern "C" {
671    pub fn boolector_forall(
672        btor: *mut Btor,
673        params: *mut *mut BoolectorNode,
674        paramc: u32,
675        body: *mut BoolectorNode,
676    ) -> *mut BoolectorNode;
677}
678extern "C" {
679    pub fn boolector_exists(
680        btor: *mut Btor,
681        param: *mut *mut BoolectorNode,
682        paramc: u32,
683        body: *mut BoolectorNode,
684    ) -> *mut BoolectorNode;
685}
686extern "C" {
687    pub fn boolector_get_btor(node: *mut BoolectorNode) -> *mut Btor;
688}
689extern "C" {
690    pub fn boolector_get_node_id(btor: *mut Btor, node: *mut BoolectorNode) -> i32;
691}
692extern "C" {
693    pub fn boolector_get_sort(btor: *mut Btor, node: *const BoolectorNode) -> BoolectorSort;
694}
695extern "C" {
696    pub fn boolector_fun_get_domain_sort(
697        btor: *mut Btor,
698        node: *const BoolectorNode,
699    ) -> BoolectorSort;
700}
701extern "C" {
702    pub fn boolector_fun_get_codomain_sort(
703        btor: *mut Btor,
704        node: *const BoolectorNode,
705    ) -> BoolectorSort;
706}
707extern "C" {
708    pub fn boolector_match_node_by_id(btor: *mut Btor, id: i32) -> *mut BoolectorNode;
709}
710extern "C" {
711    pub fn boolector_match_node_by_symbol(
712        btor: *mut Btor,
713        symbol: *const ::std::os::raw::c_char,
714    ) -> *mut BoolectorNode;
715}
716extern "C" {
717    pub fn boolector_match_node(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
718}
719extern "C" {
720    pub fn boolector_get_symbol(
721        btor: *mut Btor,
722        node: *mut BoolectorNode,
723    ) -> *const ::std::os::raw::c_char;
724}
725extern "C" {
726    pub fn boolector_set_symbol(
727        btor: *mut Btor,
728        node: *mut BoolectorNode,
729        symbol: *const ::std::os::raw::c_char,
730    );
731}
732extern "C" {
733    pub fn boolector_get_width(btor: *mut Btor, node: *mut BoolectorNode) -> u32;
734}
735extern "C" {
736    pub fn boolector_get_index_width(btor: *mut Btor, n_array: *mut BoolectorNode) -> u32;
737}
738extern "C" {
739    pub fn boolector_get_bits(
740        btor: *mut Btor,
741        node: *mut BoolectorNode,
742    ) -> *const ::std::os::raw::c_char;
743}
744extern "C" {
745    pub fn boolector_free_bits(btor: *mut Btor, bits: *const ::std::os::raw::c_char);
746}
747extern "C" {
748    pub fn boolector_get_fun_arity(btor: *mut Btor, node: *mut BoolectorNode) -> u32;
749}
750extern "C" {
751    pub fn boolector_is_const(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
752}
753extern "C" {
754    pub fn boolector_is_var(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
755}
756extern "C" {
757    pub fn boolector_is_array(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
758}
759extern "C" {
760    pub fn boolector_is_array_var(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
761}
762extern "C" {
763    pub fn boolector_is_param(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
764}
765extern "C" {
766    pub fn boolector_is_bound_param(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
767}
768extern "C" {
769    pub fn boolector_is_uf(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
770}
771extern "C" {
772    pub fn boolector_is_fun(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
773}
774extern "C" {
775    pub fn boolector_fun_sort_check(
776        btor: *mut Btor,
777        arg_nodes: *mut *mut BoolectorNode,
778        argc: u32,
779        n_fun: *mut BoolectorNode,
780    ) -> i32;
781}
782extern "C" {
783    pub fn boolector_get_value(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
784}
785extern "C" {
786    pub fn boolector_bv_assignment(
787        btor: *mut Btor,
788        node: *mut BoolectorNode,
789    ) -> *const ::std::os::raw::c_char;
790}
791extern "C" {
792    pub fn boolector_free_bv_assignment(btor: *mut Btor, assignment: *const ::std::os::raw::c_char);
793}
794extern "C" {
795    pub fn boolector_array_assignment(
796        btor: *mut Btor,
797        n_array: *mut BoolectorNode,
798        indices: *mut *mut *mut ::std::os::raw::c_char,
799        values: *mut *mut *mut ::std::os::raw::c_char,
800        size: *mut u32,
801    );
802}
803extern "C" {
804    pub fn boolector_free_array_assignment(
805        btor: *mut Btor,
806        indices: *mut *mut ::std::os::raw::c_char,
807        values: *mut *mut ::std::os::raw::c_char,
808        size: u32,
809    );
810}
811extern "C" {
812    pub fn boolector_uf_assignment(
813        btor: *mut Btor,
814        n_uf: *mut BoolectorNode,
815        args: *mut *mut *mut ::std::os::raw::c_char,
816        values: *mut *mut *mut ::std::os::raw::c_char,
817        size: *mut u32,
818    );
819}
820extern "C" {
821    pub fn boolector_free_uf_assignment(
822        btor: *mut Btor,
823        args: *mut *mut ::std::os::raw::c_char,
824        values: *mut *mut ::std::os::raw::c_char,
825        size: u32,
826    );
827}
828extern "C" {
829    pub fn boolector_print_model(
830        btor: *mut Btor,
831        format: *mut ::std::os::raw::c_char,
832        file: *mut FILE,
833    );
834}
835extern "C" {
836    pub fn boolector_bool_sort(btor: *mut Btor) -> BoolectorSort;
837}
838extern "C" {
839    pub fn boolector_bitvec_sort(btor: *mut Btor, width: u32) -> BoolectorSort;
840}
841extern "C" {
842    pub fn boolector_fun_sort(
843        btor: *mut Btor,
844        domain: *mut BoolectorSort,
845        arity: u32,
846        codomain: BoolectorSort,
847    ) -> BoolectorSort;
848}
849extern "C" {
850    pub fn boolector_array_sort(
851        btor: *mut Btor,
852        index: BoolectorSort,
853        element: BoolectorSort,
854    ) -> BoolectorSort;
855}
856extern "C" {
857    pub fn boolector_copy_sort(btor: *mut Btor, sort: BoolectorSort) -> BoolectorSort;
858}
859extern "C" {
860    pub fn boolector_release_sort(btor: *mut Btor, sort: BoolectorSort);
861}
862extern "C" {
863    pub fn boolector_is_equal_sort(
864        btor: *mut Btor,
865        n0: *mut BoolectorNode,
866        n1: *mut BoolectorNode,
867    ) -> bool;
868}
869extern "C" {
870    pub fn boolector_is_array_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
871}
872extern "C" {
873    pub fn boolector_is_bitvec_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
874}
875extern "C" {
876    pub fn boolector_is_fun_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
877}
878extern "C" {
879    pub fn boolector_bitvec_sort_get_width(btor: *mut Btor, sort: BoolectorSort) -> u32;
880}
881extern "C" {
882    pub fn boolector_parse(
883        btor: *mut Btor,
884        infile: *mut FILE,
885        infile_name: *const ::std::os::raw::c_char,
886        outfile: *mut FILE,
887        error_msg: *mut *mut ::std::os::raw::c_char,
888        status: *mut i32,
889        parsed_smt2: *mut bool,
890    ) -> i32;
891}
892extern "C" {
893    pub fn boolector_parse_btor(
894        btor: *mut Btor,
895        infile: *mut FILE,
896        infile_name: *const ::std::os::raw::c_char,
897        outfile: *mut FILE,
898        error_msg: *mut *mut ::std::os::raw::c_char,
899        status: *mut i32,
900    ) -> i32;
901}
902extern "C" {
903    pub fn boolector_parse_btor2(
904        btor: *mut Btor,
905        infile: *mut FILE,
906        infile_name: *const ::std::os::raw::c_char,
907        outfile: *mut FILE,
908        error_msg: *mut *mut ::std::os::raw::c_char,
909        status: *mut i32,
910    ) -> i32;
911}
912extern "C" {
913    pub fn boolector_parse_smt1(
914        btor: *mut Btor,
915        infile: *mut FILE,
916        infile_name: *const ::std::os::raw::c_char,
917        outfile: *mut FILE,
918        error_msg: *mut *mut ::std::os::raw::c_char,
919        status: *mut i32,
920    ) -> i32;
921}
922extern "C" {
923    pub fn boolector_parse_smt2(
924        btor: *mut Btor,
925        infile: *mut FILE,
926        infile_name: *const ::std::os::raw::c_char,
927        outfile: *mut FILE,
928        error_msg: *mut *mut ::std::os::raw::c_char,
929        status: *mut i32,
930    ) -> i32;
931}
932extern "C" {
933    pub fn boolector_dump_btor_node(btor: *mut Btor, file: *mut FILE, node: *mut BoolectorNode);
934}
935extern "C" {
936    pub fn boolector_dump_btor(btor: *mut Btor, file: *mut FILE);
937}
938extern "C" {
939    pub fn boolector_dump_smt2_node(btor: *mut Btor, file: *mut FILE, node: *mut BoolectorNode);
940}
941extern "C" {
942    pub fn boolector_dump_smt2(btor: *mut Btor, file: *mut FILE);
943}
944extern "C" {
945    pub fn boolector_dump_aiger_ascii(btor: *mut Btor, file: *mut FILE, merge_roots: bool);
946}
947extern "C" {
948    pub fn boolector_dump_aiger_binary(btor: *mut Btor, file: *mut FILE, merge_roots: bool);
949}
950extern "C" {
951    pub fn boolector_copyright(btor: *mut Btor) -> *const ::std::os::raw::c_char;
952}
953extern "C" {
954    pub fn boolector_version(btor: *mut Btor) -> *const ::std::os::raw::c_char;
955}
956extern "C" {
957    pub fn boolector_git_id(btor: *mut Btor) -> *const ::std::os::raw::c_char;
958}
boolector_sys/src-generated/bindings.rs

boolector_sys/src-generated/
bindings.rs
