/* automatically generated by rust-bindgen 0.59.1 */

use libc::FILE;

#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct Btor {
    _unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct BtorNode {
    _unused: [u8; 0],
}
pub const BtorSolverResult_BTOR_RESULT_SAT: BtorSolverResult = 10;
pub const BtorSolverResult_BTOR_RESULT_UNSAT: BtorSolverResult = 20;
pub const BtorSolverResult_BTOR_RESULT_UNKNOWN: BtorSolverResult = 0;
pub type BtorSolverResult = ::std::os::raw::c_uint;
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct BoolectorNode {
    _unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct BoolectorAnonymous {
    _unused: [u8; 0],
}
pub type BoolectorSort = *mut BoolectorAnonymous;
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct BtorAbortCallback {
    pub abort_fun: ::std::option::Option<unsafe extern "C" fn(msg: *const ::std::os::raw::c_char)>,
    pub cb_fun: *mut ::std::os::raw::c_void,
}
#[test]
fn bindgen_test_layout_BtorAbortCallback() {
    assert_eq!(
        ::std::mem::size_of::<BtorAbortCallback>(),
        16usize,
        concat!("Size of: ", stringify!(BtorAbortCallback))
    );
    assert_eq!(
        ::std::mem::align_of::<BtorAbortCallback>(),
        8usize,
        concat!("Alignment of ", stringify!(BtorAbortCallback))
    );
    assert_eq!(
        unsafe { &(*(::std::ptr::null::<BtorAbortCallback>())).abort_fun as *const _ as usize },
        0usize,
        concat!(
            "Offset of field: ",
            stringify!(BtorAbortCallback),
            "::",
            stringify!(abort_fun)
        )
    );
    assert_eq!(
        unsafe { &(*(::std::ptr::null::<BtorAbortCallback>())).cb_fun as *const _ as usize },
        8usize,
        concat!(
            "Offset of field: ",
            stringify!(BtorAbortCallback),
            "::",
            stringify!(cb_fun)
        )
    );
}
extern "C" {
    pub fn boolector_new() -> *mut Btor;
}
extern "C" {
    pub fn boolector_clone(btor: *mut Btor) -> *mut Btor;
}
extern "C" {
    pub fn boolector_delete(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_set_term(
        btor: *mut Btor,
        fun: ::std::option::Option<unsafe extern "C" fn(arg1: *mut ::std::os::raw::c_void) -> i32>,
        state: *mut ::std::os::raw::c_void,
    );
}
extern "C" {
    pub fn boolector_terminate(btor: *mut Btor) -> i32;
}
extern "C" {
    pub fn boolector_set_abort(
        fun: ::std::option::Option<unsafe extern "C" fn(msg: *const ::std::os::raw::c_char)>,
    );
}
extern "C" {
    pub fn boolector_set_msg_prefix(btor: *mut Btor, prefix: *const ::std::os::raw::c_char);
}
extern "C" {
    pub fn boolector_get_refs(btor: *mut Btor) -> u32;
}
extern "C" {
    pub fn boolector_reset_time(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_reset_stats(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_print_stats(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_set_trapi(btor: *mut Btor, apitrace: *mut FILE);
}
extern "C" {
    pub fn boolector_get_trapi(btor: *mut Btor) -> *mut FILE;
}
extern "C" {
    pub fn boolector_push(btor: *mut Btor, level: u32);
}
extern "C" {
    pub fn boolector_pop(btor: *mut Btor, level: u32);
}
extern "C" {
    pub fn boolector_assert(btor: *mut Btor, node: *mut BoolectorNode);
}
extern "C" {
    pub fn boolector_assume(btor: *mut Btor, node: *mut BoolectorNode);
}
extern "C" {
    pub fn boolector_failed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_get_failed_assumptions(btor: *mut Btor) -> *mut *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_fixate_assumptions(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_reset_assumptions(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_sat(btor: *mut Btor) -> i32;
}
extern "C" {
    pub fn boolector_limited_sat(btor: *mut Btor, lod_limit: i32, sat_limit: i32) -> i32;
}
extern "C" {
    pub fn boolector_simplify(btor: *mut Btor) -> i32;
}
extern "C" {
    pub fn boolector_set_sat_solver(btor: *mut Btor, solver: *const ::std::os::raw::c_char);
}
extern "C" {
    pub fn boolector_set_opt(btor: *mut Btor, opt: BtorOption, val: u32);
}
extern "C" {
    pub fn boolector_get_opt(btor: *mut Btor, opt: BtorOption) -> u32;
}
extern "C" {
    pub fn boolector_get_opt_min(btor: *mut Btor, opt: BtorOption) -> u32;
}
extern "C" {
    pub fn boolector_get_opt_max(btor: *mut Btor, opt: BtorOption) -> u32;
}
extern "C" {
    pub fn boolector_get_opt_dflt(btor: *mut Btor, opt: BtorOption) -> u32;
}
extern "C" {
    pub fn boolector_get_opt_lng(btor: *mut Btor, opt: BtorOption)
        -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_get_opt_shrt(
        btor: *mut Btor,
        opt: BtorOption,
    ) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_get_opt_desc(
        btor: *mut Btor,
        opt: BtorOption,
    ) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_has_opt(Btor: *mut Btor, opt: BtorOption) -> bool;
}
extern "C" {
    pub fn boolector_first_opt(btor: *mut Btor) -> BtorOption;
}
extern "C" {
    pub fn boolector_next_opt(btor: *mut Btor, opt: BtorOption) -> BtorOption;
}
extern "C" {
    pub fn boolector_copy(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_release(btor: *mut Btor, node: *mut BoolectorNode);
}
extern "C" {
    pub fn boolector_release_all(btor: *mut Btor);
}
extern "C" {
    pub fn boolector_true(btor: *mut Btor) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_false(btor: *mut Btor) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_implies(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_iff(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_eq(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ne(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_is_bv_const_zero(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_bv_const_one(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_bv_const_ones(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_bv_const_max_signed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_bv_const_min_signed(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_const(
        btor: *mut Btor,
        bits: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_constd(
        btor: *mut Btor,
        sort: BoolectorSort,
        str_: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_consth(
        btor: *mut Btor,
        sort: BoolectorSort,
        str_: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_zero(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ones(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_one(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_min_signed(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_max_signed(btor: *mut Btor, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_unsigned_int(
        btor: *mut Btor,
        u: u32,
        sort: BoolectorSort,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_int(btor: *mut Btor, i: i32, sort: BoolectorSort) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_var(
        btor: *mut Btor,
        sort: BoolectorSort,
        symbol: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_array(
        btor: *mut Btor,
        sort: BoolectorSort,
        symbol: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_const_array(
        btor: *mut Btor,
        sort: BoolectorSort,
        value: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_uf(
        btor: *mut Btor,
        sort: BoolectorSort,
        symbol: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_not(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_neg(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_redor(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_redxor(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_redand(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_slice(
        btor: *mut Btor,
        node: *mut BoolectorNode,
        upper: u32,
        lower: u32,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_uext(
        btor: *mut Btor,
        node: *mut BoolectorNode,
        width: u32,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sext(
        btor: *mut Btor,
        node: *mut BoolectorNode,
        width: u32,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_xor(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_xnor(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_and(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_nand(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_or(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_nor(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_add(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_uaddo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_saddo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_mul(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_umulo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_smulo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ult(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_slt(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ulte(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_slte(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ugt(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sgt(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ugte(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sgte(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sll(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_srl(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sra(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_rol(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ror(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_roli(btor: *mut Btor, n: *mut BoolectorNode, nbits: u32)
        -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_rori(btor: *mut Btor, n: *mut BoolectorNode, nbits: u32)
        -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sub(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_usubo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_ssubo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_udiv(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sdiv(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_sdivo(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_urem(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_srem(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_smod(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_concat(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_repeat(
        btor: *mut Btor,
        node: *mut BoolectorNode,
        n: u32,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_read(
        btor: *mut Btor,
        n_array: *mut BoolectorNode,
        n_index: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_write(
        btor: *mut Btor,
        n_array: *mut BoolectorNode,
        n_index: *mut BoolectorNode,
        n_value: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_cond(
        btor: *mut Btor,
        n_cond: *mut BoolectorNode,
        n_then: *mut BoolectorNode,
        n_else: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_param(
        btor: *mut Btor,
        sort: BoolectorSort,
        symbol: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_fun(
        btor: *mut Btor,
        param_nodes: *mut *mut BoolectorNode,
        paramc: u32,
        node: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_apply(
        btor: *mut Btor,
        arg_nodes: *mut *mut BoolectorNode,
        argc: u32,
        n_fun: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_inc(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_dec(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_forall(
        btor: *mut Btor,
        params: *mut *mut BoolectorNode,
        paramc: u32,
        body: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_exists(
        btor: *mut Btor,
        param: *mut *mut BoolectorNode,
        paramc: u32,
        body: *mut BoolectorNode,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_get_btor(node: *mut BoolectorNode) -> *mut Btor;
}
extern "C" {
    pub fn boolector_get_node_id(btor: *mut Btor, node: *mut BoolectorNode) -> i32;
}
extern "C" {
    pub fn boolector_get_sort(btor: *mut Btor, node: *const BoolectorNode) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_fun_get_domain_sort(
        btor: *mut Btor,
        node: *const BoolectorNode,
    ) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_fun_get_codomain_sort(
        btor: *mut Btor,
        node: *const BoolectorNode,
    ) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_match_node_by_id(btor: *mut Btor, id: i32) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_match_node_by_symbol(
        btor: *mut Btor,
        symbol: *const ::std::os::raw::c_char,
    ) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_match_node(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_get_symbol(
        btor: *mut Btor,
        node: *mut BoolectorNode,
    ) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_set_symbol(
        btor: *mut Btor,
        node: *mut BoolectorNode,
        symbol: *const ::std::os::raw::c_char,
    );
}
extern "C" {
    pub fn boolector_get_width(btor: *mut Btor, node: *mut BoolectorNode) -> u32;
}
extern "C" {
    pub fn boolector_get_index_width(btor: *mut Btor, n_array: *mut BoolectorNode) -> u32;
}
extern "C" {
    pub fn boolector_get_bits(
        btor: *mut Btor,
        node: *mut BoolectorNode,
    ) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_free_bits(btor: *mut Btor, bits: *const ::std::os::raw::c_char);
}
extern "C" {
    pub fn boolector_get_fun_arity(btor: *mut Btor, node: *mut BoolectorNode) -> u32;
}
extern "C" {
    pub fn boolector_is_const(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_var(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_array(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_array_var(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_param(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_bound_param(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_uf(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_is_fun(btor: *mut Btor, node: *mut BoolectorNode) -> bool;
}
extern "C" {
    pub fn boolector_fun_sort_check(
        btor: *mut Btor,
        arg_nodes: *mut *mut BoolectorNode,
        argc: u32,
        n_fun: *mut BoolectorNode,
    ) -> i32;
}
extern "C" {
    pub fn boolector_get_value(btor: *mut Btor, node: *mut BoolectorNode) -> *mut BoolectorNode;
}
extern "C" {
    pub fn boolector_bv_assignment(
        btor: *mut Btor,
        node: *mut BoolectorNode,
    ) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_free_bv_assignment(btor: *mut Btor, assignment: *const ::std::os::raw::c_char);
}
extern "C" {
    pub fn boolector_array_assignment(
        btor: *mut Btor,
        n_array: *mut BoolectorNode,
        indices: *mut *mut *mut ::std::os::raw::c_char,
        values: *mut *mut *mut ::std::os::raw::c_char,
        size: *mut u32,
    );
}
extern "C" {
    pub fn boolector_free_array_assignment(
        btor: *mut Btor,
        indices: *mut *mut ::std::os::raw::c_char,
        values: *mut *mut ::std::os::raw::c_char,
        size: u32,
    );
}
extern "C" {
    pub fn boolector_uf_assignment(
        btor: *mut Btor,
        n_uf: *mut BoolectorNode,
        args: *mut *mut *mut ::std::os::raw::c_char,
        values: *mut *mut *mut ::std::os::raw::c_char,
        size: *mut u32,
    );
}
extern "C" {
    pub fn boolector_free_uf_assignment(
        btor: *mut Btor,
        args: *mut *mut ::std::os::raw::c_char,
        values: *mut *mut ::std::os::raw::c_char,
        size: u32,
    );
}
extern "C" {
    pub fn boolector_print_model(
        btor: *mut Btor,
        format: *mut ::std::os::raw::c_char,
        file: *mut FILE,
    );
}
extern "C" {
    pub fn boolector_bool_sort(btor: *mut Btor) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_bitvec_sort(btor: *mut Btor, width: u32) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_fun_sort(
        btor: *mut Btor,
        domain: *mut BoolectorSort,
        arity: u32,
        codomain: BoolectorSort,
    ) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_array_sort(
        btor: *mut Btor,
        index: BoolectorSort,
        element: BoolectorSort,
    ) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_copy_sort(btor: *mut Btor, sort: BoolectorSort) -> BoolectorSort;
}
extern "C" {
    pub fn boolector_release_sort(btor: *mut Btor, sort: BoolectorSort);
}
extern "C" {
    pub fn boolector_is_equal_sort(
        btor: *mut Btor,
        n0: *mut BoolectorNode,
        n1: *mut BoolectorNode,
    ) -> bool;
}
extern "C" {
    pub fn boolector_is_array_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
}
extern "C" {
    pub fn boolector_is_bitvec_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
}
extern "C" {
    pub fn boolector_is_fun_sort(btor: *mut Btor, sort: BoolectorSort) -> bool;
}
extern "C" {
    pub fn boolector_bitvec_sort_get_width(btor: *mut Btor, sort: BoolectorSort) -> u32;
}
extern "C" {
    pub fn boolector_parse(
        btor: *mut Btor,
        infile: *mut FILE,
        infile_name: *const ::std::os::raw::c_char,
        outfile: *mut FILE,
        error_msg: *mut *mut ::std::os::raw::c_char,
        status: *mut i32,
        parsed_smt2: *mut bool,
    ) -> i32;
}
extern "C" {
    pub fn boolector_parse_btor(
        btor: *mut Btor,
        infile: *mut FILE,
        infile_name: *const ::std::os::raw::c_char,
        outfile: *mut FILE,
        error_msg: *mut *mut ::std::os::raw::c_char,
        status: *mut i32,
    ) -> i32;
}
extern "C" {
    pub fn boolector_parse_btor2(
        btor: *mut Btor,
        infile: *mut FILE,
        infile_name: *const ::std::os::raw::c_char,
        outfile: *mut FILE,
        error_msg: *mut *mut ::std::os::raw::c_char,
        status: *mut i32,
    ) -> i32;
}
extern "C" {
    pub fn boolector_parse_smt1(
        btor: *mut Btor,
        infile: *mut FILE,
        infile_name: *const ::std::os::raw::c_char,
        outfile: *mut FILE,
        error_msg: *mut *mut ::std::os::raw::c_char,
        status: *mut i32,
    ) -> i32;
}
extern "C" {
    pub fn boolector_parse_smt2(
        btor: *mut Btor,
        infile: *mut FILE,
        infile_name: *const ::std::os::raw::c_char,
        outfile: *mut FILE,
        error_msg: *mut *mut ::std::os::raw::c_char,
        status: *mut i32,
    ) -> i32;
}
extern "C" {
    pub fn boolector_dump_btor_node(btor: *mut Btor, file: *mut FILE, node: *mut BoolectorNode);
}
extern "C" {
    pub fn boolector_dump_btor(btor: *mut Btor, file: *mut FILE);
}
extern "C" {
    pub fn boolector_dump_smt2_node(btor: *mut Btor, file: *mut FILE, node: *mut BoolectorNode);
}
extern "C" {
    pub fn boolector_dump_smt2(btor: *mut Btor, file: *mut FILE);
}
extern "C" {
    pub fn boolector_dump_aiger_ascii(btor: *mut Btor, file: *mut FILE, merge_roots: bool);
}
extern "C" {
    pub fn boolector_dump_aiger_binary(btor: *mut Btor, file: *mut FILE, merge_roots: bool);
}
extern "C" {
    pub fn boolector_copyright(btor: *mut Btor) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_version(btor: *mut Btor) -> *const ::std::os::raw::c_char;
}
extern "C" {
    pub fn boolector_git_id(btor: *mut Btor) -> *const ::std::os::raw::c_char;
}