/* automatically generated by rust-bindgen 0.69.4 */ use libc::FILE; pub const BITWUZLA_SAT: BitwuzlaResult = 10; pub const BITWUZLA_UNSAT: BitwuzlaResult = 20; pub const BITWUZLA_UNKNOWN: BitwuzlaResult = 0; pub type BitwuzlaResult = ::std::os::raw::c_uint; pub const BITWUZLA_RM_RNE: BitwuzlaRoundingMode = 0; pub const BITWUZLA_RM_RNA: BitwuzlaRoundingMode = 1; pub const BITWUZLA_RM_RTN: BitwuzlaRoundingMode = 2; pub const BITWUZLA_RM_RTP: BitwuzlaRoundingMode = 3; pub const BITWUZLA_RM_RTZ: BitwuzlaRoundingMode = 4; pub const BITWUZLA_RM_MAX: BitwuzlaRoundingMode = 5; pub type BitwuzlaRoundingMode = ::std::os::raw::c_uint; pub const BITWUZLA_KIND_CONSTANT: BitwuzlaKind = 0; pub const BITWUZLA_KIND_CONST_ARRAY: BitwuzlaKind = 1; pub const BITWUZLA_KIND_VALUE: BitwuzlaKind = 2; pub const BITWUZLA_KIND_VARIABLE: BitwuzlaKind = 3; pub const BITWUZLA_KIND_AND: BitwuzlaKind = 4; pub const BITWUZLA_KIND_DISTINCT: BitwuzlaKind = 5; pub const BITWUZLA_KIND_EQUAL: BitwuzlaKind = 6; pub const BITWUZLA_KIND_IFF: BitwuzlaKind = 7; pub const BITWUZLA_KIND_IMPLIES: BitwuzlaKind = 8; pub const BITWUZLA_KIND_NOT: BitwuzlaKind = 9; pub const BITWUZLA_KIND_OR: BitwuzlaKind = 10; pub const BITWUZLA_KIND_XOR: BitwuzlaKind = 11; pub const BITWUZLA_KIND_ITE: BitwuzlaKind = 12; pub const BITWUZLA_KIND_EXISTS: BitwuzlaKind = 13; pub const BITWUZLA_KIND_FORALL: BitwuzlaKind = 14; pub const BITWUZLA_KIND_APPLY: BitwuzlaKind = 15; pub const BITWUZLA_KIND_LAMBDA: BitwuzlaKind = 16; pub const BITWUZLA_KIND_ARRAY_SELECT: BitwuzlaKind = 17; pub const BITWUZLA_KIND_ARRAY_STORE: BitwuzlaKind = 18; pub const BITWUZLA_KIND_BV_ADD: BitwuzlaKind = 19; pub const BITWUZLA_KIND_BV_AND: BitwuzlaKind = 20; pub const BITWUZLA_KIND_BV_ASHR: BitwuzlaKind = 21; pub const BITWUZLA_KIND_BV_COMP: BitwuzlaKind = 22; pub const BITWUZLA_KIND_BV_CONCAT: BitwuzlaKind = 23; pub const BITWUZLA_KIND_BV_DEC: BitwuzlaKind = 24; pub const BITWUZLA_KIND_BV_INC: BitwuzlaKind = 25; pub const BITWUZLA_KIND_BV_MUL: BitwuzlaKind = 26; pub const BITWUZLA_KIND_BV_NAND: BitwuzlaKind = 27; pub const BITWUZLA_KIND_BV_NEG: BitwuzlaKind = 28; pub const BITWUZLA_KIND_BV_NEG_OVERFLOW: BitwuzlaKind = 29; pub const BITWUZLA_KIND_BV_NOR: BitwuzlaKind = 30; pub const BITWUZLA_KIND_BV_NOT: BitwuzlaKind = 31; pub const BITWUZLA_KIND_BV_OR: BitwuzlaKind = 32; pub const BITWUZLA_KIND_BV_REDAND: BitwuzlaKind = 33; pub const BITWUZLA_KIND_BV_REDOR: BitwuzlaKind = 34; pub const BITWUZLA_KIND_BV_REDXOR: BitwuzlaKind = 35; pub const BITWUZLA_KIND_BV_ROL: BitwuzlaKind = 36; pub const BITWUZLA_KIND_BV_ROR: BitwuzlaKind = 37; pub const BITWUZLA_KIND_BV_SADD_OVERFLOW: BitwuzlaKind = 38; pub const BITWUZLA_KIND_BV_SDIV_OVERFLOW: BitwuzlaKind = 39; pub const BITWUZLA_KIND_BV_SDIV: BitwuzlaKind = 40; pub const BITWUZLA_KIND_BV_SGE: BitwuzlaKind = 41; pub const BITWUZLA_KIND_BV_SGT: BitwuzlaKind = 42; pub const BITWUZLA_KIND_BV_SHL: BitwuzlaKind = 43; pub const BITWUZLA_KIND_BV_SHR: BitwuzlaKind = 44; pub const BITWUZLA_KIND_BV_SLE: BitwuzlaKind = 45; pub const BITWUZLA_KIND_BV_SLT: BitwuzlaKind = 46; pub const BITWUZLA_KIND_BV_SMOD: BitwuzlaKind = 47; pub const BITWUZLA_KIND_BV_SMUL_OVERFLOW: BitwuzlaKind = 48; pub const BITWUZLA_KIND_BV_SREM: BitwuzlaKind = 49; pub const BITWUZLA_KIND_BV_SSUB_OVERFLOW: BitwuzlaKind = 50; pub const BITWUZLA_KIND_BV_SUB: BitwuzlaKind = 51; pub const BITWUZLA_KIND_BV_UADD_OVERFLOW: BitwuzlaKind = 52; pub const BITWUZLA_KIND_BV_UDIV: BitwuzlaKind = 53; pub const BITWUZLA_KIND_BV_UGE: BitwuzlaKind = 54; pub const BITWUZLA_KIND_BV_UGT: BitwuzlaKind = 55; pub const BITWUZLA_KIND_BV_ULE: BitwuzlaKind = 56; pub const BITWUZLA_KIND_BV_ULT: BitwuzlaKind = 57; pub const BITWUZLA_KIND_BV_UMUL_OVERFLOW: BitwuzlaKind = 58; pub const BITWUZLA_KIND_BV_UREM: BitwuzlaKind = 59; pub const BITWUZLA_KIND_BV_USUB_OVERFLOW: BitwuzlaKind = 60; pub const BITWUZLA_KIND_BV_XNOR: BitwuzlaKind = 61; pub const BITWUZLA_KIND_BV_XOR: BitwuzlaKind = 62; pub const BITWUZLA_KIND_BV_EXTRACT: BitwuzlaKind = 63; pub const BITWUZLA_KIND_BV_REPEAT: BitwuzlaKind = 64; pub const BITWUZLA_KIND_BV_ROLI: BitwuzlaKind = 65; pub const BITWUZLA_KIND_BV_RORI: BitwuzlaKind = 66; pub const BITWUZLA_KIND_BV_SIGN_EXTEND: BitwuzlaKind = 67; pub const BITWUZLA_KIND_BV_ZERO_EXTEND: BitwuzlaKind = 68; pub const BITWUZLA_KIND_FP_ABS: BitwuzlaKind = 69; pub const BITWUZLA_KIND_FP_ADD: BitwuzlaKind = 70; pub const BITWUZLA_KIND_FP_DIV: BitwuzlaKind = 71; pub const BITWUZLA_KIND_FP_EQUAL: BitwuzlaKind = 72; pub const BITWUZLA_KIND_FP_FMA: BitwuzlaKind = 73; pub const BITWUZLA_KIND_FP_FP: BitwuzlaKind = 74; pub const BITWUZLA_KIND_FP_GEQ: BitwuzlaKind = 75; pub const BITWUZLA_KIND_FP_GT: BitwuzlaKind = 76; pub const BITWUZLA_KIND_FP_IS_INF: BitwuzlaKind = 77; pub const BITWUZLA_KIND_FP_IS_NAN: BitwuzlaKind = 78; pub const BITWUZLA_KIND_FP_IS_NEG: BitwuzlaKind = 79; pub const BITWUZLA_KIND_FP_IS_NORMAL: BitwuzlaKind = 80; pub const BITWUZLA_KIND_FP_IS_POS: BitwuzlaKind = 81; pub const BITWUZLA_KIND_FP_IS_SUBNORMAL: BitwuzlaKind = 82; pub const BITWUZLA_KIND_FP_IS_ZERO: BitwuzlaKind = 83; pub const BITWUZLA_KIND_FP_LEQ: BitwuzlaKind = 84; pub const BITWUZLA_KIND_FP_LT: BitwuzlaKind = 85; pub const BITWUZLA_KIND_FP_MAX: BitwuzlaKind = 86; pub const BITWUZLA_KIND_FP_MIN: BitwuzlaKind = 87; pub const BITWUZLA_KIND_FP_MUL: BitwuzlaKind = 88; pub const BITWUZLA_KIND_FP_NEG: BitwuzlaKind = 89; pub const BITWUZLA_KIND_FP_REM: BitwuzlaKind = 90; pub const BITWUZLA_KIND_FP_RTI: BitwuzlaKind = 91; pub const BITWUZLA_KIND_FP_SQRT: BitwuzlaKind = 92; pub const BITWUZLA_KIND_FP_SUB: BitwuzlaKind = 93; pub const BITWUZLA_KIND_FP_TO_FP_FROM_BV: BitwuzlaKind = 94; pub const BITWUZLA_KIND_FP_TO_FP_FROM_FP: BitwuzlaKind = 95; pub const BITWUZLA_KIND_FP_TO_FP_FROM_SBV: BitwuzlaKind = 96; pub const BITWUZLA_KIND_FP_TO_FP_FROM_UBV: BitwuzlaKind = 97; pub const BITWUZLA_KIND_FP_TO_SBV: BitwuzlaKind = 98; pub const BITWUZLA_KIND_FP_TO_UBV: BitwuzlaKind = 99; pub const BITWUZLA_KIND_NUM_KINDS: BitwuzlaKind = 100; pub type BitwuzlaKind = ::std::os::raw::c_uint; pub const BITWUZLA_OPT_LOGLEVEL: BitwuzlaOption = 0; pub const BITWUZLA_OPT_PRODUCE_MODELS: BitwuzlaOption = 1; pub const BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS: BitwuzlaOption = 2; pub const BITWUZLA_OPT_PRODUCE_UNSAT_CORES: BitwuzlaOption = 3; pub const BITWUZLA_OPT_SEED: BitwuzlaOption = 4; pub const BITWUZLA_OPT_VERBOSITY: BitwuzlaOption = 5; pub const BITWUZLA_OPT_TIME_LIMIT_PER: BitwuzlaOption = 6; pub const BITWUZLA_OPT_MEMORY_LIMIT: BitwuzlaOption = 7; pub const BITWUZLA_OPT_BV_SOLVER: BitwuzlaOption = 8; pub const BITWUZLA_OPT_REWRITE_LEVEL: BitwuzlaOption = 9; pub const BITWUZLA_OPT_SAT_SOLVER: BitwuzlaOption = 10; pub const BITWUZLA_OPT_PROP_CONST_BITS: BitwuzlaOption = 11; pub const BITWUZLA_OPT_PROP_INFER_INEQ_BOUNDS: BitwuzlaOption = 12; pub const BITWUZLA_OPT_PROP_NPROPS: BitwuzlaOption = 13; pub const BITWUZLA_OPT_PROP_NUPDATES: BitwuzlaOption = 14; pub const BITWUZLA_OPT_PROP_OPT_LT_CONCAT_SEXT: BitwuzlaOption = 15; pub const BITWUZLA_OPT_PROP_PATH_SEL: BitwuzlaOption = 16; pub const BITWUZLA_OPT_PROP_PROB_RANDOM_INPUT: BitwuzlaOption = 17; pub const BITWUZLA_OPT_PROP_PROB_USE_INV_VALUE: BitwuzlaOption = 18; pub const BITWUZLA_OPT_PROP_SEXT: BitwuzlaOption = 19; pub const BITWUZLA_OPT_PROP_NORMALIZE: BitwuzlaOption = 20; pub const BITWUZLA_OPT_PREPROCESS: BitwuzlaOption = 21; pub const BITWUZLA_OPT_PP_CONTRADICTING_ANDS: BitwuzlaOption = 22; pub const BITWUZLA_OPT_PP_ELIM_BV_EXTRACTS: BitwuzlaOption = 23; pub const BITWUZLA_OPT_PP_EMBEDDED_CONSTR: BitwuzlaOption = 24; pub const BITWUZLA_OPT_PP_FLATTEN_AND: BitwuzlaOption = 25; pub const BITWUZLA_OPT_PP_NORMALIZE: BitwuzlaOption = 26; pub const BITWUZLA_OPT_PP_NORMALIZE_SHARE_AWARE: BitwuzlaOption = 27; pub const BITWUZLA_OPT_PP_SKELETON_PREPROC: BitwuzlaOption = 28; pub const BITWUZLA_OPT_PP_VARIABLE_SUBST: BitwuzlaOption = 29; pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_EQ: BitwuzlaOption = 30; pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_DISEQ: BitwuzlaOption = 31; pub const BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_BV_INEQ: BitwuzlaOption = 32; pub const BITWUZLA_OPT_DBG_RW_NODE_THRESH: BitwuzlaOption = 33; pub const BITWUZLA_OPT_DBG_PP_NODE_THRESH: BitwuzlaOption = 34; pub const BITWUZLA_OPT_DBG_CHECK_MODEL: BitwuzlaOption = 35; pub const BITWUZLA_OPT_DBG_CHECK_UNSAT_CORE: BitwuzlaOption = 36; pub const BITWUZLA_OPT_NUM_OPTS: BitwuzlaOption = 37; pub type BitwuzlaOption = ::std::os::raw::c_uint; extern "C" { pub fn bitwuzla_copyright() -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_version() -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_git_id() -> *const ::std::os::raw::c_char; } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct BitwuzlaOptionInfo { pub opt: BitwuzlaOption, pub shrt: *const ::std::os::raw::c_char, pub lng: *const ::std::os::raw::c_char, pub description: *const ::std::os::raw::c_char, pub is_numeric: bool, pub numeric: BitwuzlaOptionInfo_NumericValue, pub mode: BitwuzlaOptionInfo_ModeValue, } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct BitwuzlaOptionInfo_NumericValue { pub cur: u64, pub dflt: u64, pub min: u64, pub max: u64, } #[test] fn bindgen_test_layout_BitwuzlaOptionInfo_NumericValue() { const UNINIT: ::std::mem::MaybeUninit = ::std::mem::MaybeUninit::uninit(); let ptr = UNINIT.as_ptr(); assert_eq!( ::std::mem::size_of::(), 32usize, concat!("Size of: ", stringify!(BitwuzlaOptionInfo_NumericValue)) ); assert_eq!( ::std::mem::align_of::(), 8usize, concat!("Alignment of ", stringify!(BitwuzlaOptionInfo_NumericValue)) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).cur) as usize - ptr as usize }, 0usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_NumericValue), "::", stringify!(cur) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).dflt) as usize - ptr as usize }, 8usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_NumericValue), "::", stringify!(dflt) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).min) as usize - ptr as usize }, 16usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_NumericValue), "::", stringify!(min) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).max) as usize - ptr as usize }, 24usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_NumericValue), "::", stringify!(max) ) ); } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct BitwuzlaOptionInfo_ModeValue { pub cur: *const ::std::os::raw::c_char, pub dflt: *const ::std::os::raw::c_char, pub num_modes: usize, pub modes: *mut *const ::std::os::raw::c_char, } #[test] fn bindgen_test_layout_BitwuzlaOptionInfo_ModeValue() { const UNINIT: ::std::mem::MaybeUninit = ::std::mem::MaybeUninit::uninit(); let ptr = UNINIT.as_ptr(); assert_eq!( ::std::mem::size_of::(), 32usize, concat!("Size of: ", stringify!(BitwuzlaOptionInfo_ModeValue)) ); assert_eq!( ::std::mem::align_of::(), 8usize, concat!("Alignment of ", stringify!(BitwuzlaOptionInfo_ModeValue)) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).cur) as usize - ptr as usize }, 0usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_ModeValue), "::", stringify!(cur) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).dflt) as usize - ptr as usize }, 8usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_ModeValue), "::", stringify!(dflt) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).num_modes) as usize - ptr as usize }, 16usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_ModeValue), "::", stringify!(num_modes) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).modes) as usize - ptr as usize }, 24usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo_ModeValue), "::", stringify!(modes) ) ); } #[test] fn bindgen_test_layout_BitwuzlaOptionInfo() { const UNINIT: ::std::mem::MaybeUninit = ::std::mem::MaybeUninit::uninit(); let ptr = UNINIT.as_ptr(); assert_eq!( ::std::mem::size_of::(), 104usize, concat!("Size of: ", stringify!(BitwuzlaOptionInfo)) ); assert_eq!( ::std::mem::align_of::(), 8usize, concat!("Alignment of ", stringify!(BitwuzlaOptionInfo)) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).opt) as usize - ptr as usize }, 0usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(opt) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).shrt) as usize - ptr as usize }, 8usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(shrt) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).lng) as usize - ptr as usize }, 16usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(lng) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).description) as usize - ptr as usize }, 24usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(description) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).is_numeric) as usize - ptr as usize }, 32usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(is_numeric) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).numeric) as usize - ptr as usize }, 40usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(numeric) ) ); assert_eq!( unsafe { ::std::ptr::addr_of!((*ptr).mode) as usize - ptr as usize }, 72usize, concat!( "Offset of field: ", stringify!(BitwuzlaOptionInfo), "::", stringify!(mode) ) ); } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct BitwuzlaOptions { _unused: [u8; 0], } extern "C" { pub fn bitwuzla_options_new() -> *mut BitwuzlaOptions; } extern "C" { pub fn bitwuzla_options_delete(options: *mut BitwuzlaOptions); } extern "C" { pub fn bitwuzla_option_is_valid( options: *mut BitwuzlaOptions, name: *const ::std::os::raw::c_char, ) -> bool; } extern "C" { pub fn bitwuzla_option_is_numeric( options: *mut BitwuzlaOptions, option: BitwuzlaOption, ) -> bool; } extern "C" { pub fn bitwuzla_option_is_mode(options: *mut BitwuzlaOptions, option: BitwuzlaOption) -> bool; } extern "C" { pub fn bitwuzla_set_option(options: *mut BitwuzlaOptions, option: BitwuzlaOption, val: u64); } extern "C" { pub fn bitwuzla_set_option_mode( options: *mut BitwuzlaOptions, option: BitwuzlaOption, val: *const ::std::os::raw::c_char, ); } extern "C" { pub fn bitwuzla_get_option(options: *mut BitwuzlaOptions, option: BitwuzlaOption) -> u64; } extern "C" { pub fn bitwuzla_get_option_mode( options: *mut BitwuzlaOptions, option: BitwuzlaOption, ) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_get_option_info( options: *mut BitwuzlaOptions, option: BitwuzlaOption, info: *mut BitwuzlaOptionInfo, ); } extern "C" { pub fn bitwuzla_result_to_string(result: BitwuzlaResult) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_rm_to_string(rm: BitwuzlaRoundingMode) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_kind_to_string(kind: BitwuzlaKind) -> *const ::std::os::raw::c_char; } pub type BitwuzlaSort = u64; extern "C" { pub fn bitwuzla_sort_hash(sort: BitwuzlaSort) -> usize; } extern "C" { pub fn bitwuzla_sort_copy(sort: BitwuzlaSort) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_sort_release(sort: BitwuzlaSort); } extern "C" { pub fn bitwuzla_sort_bv_get_size(sort: BitwuzlaSort) -> u64; } extern "C" { pub fn bitwuzla_sort_fp_get_exp_size(sort: BitwuzlaSort) -> u64; } extern "C" { pub fn bitwuzla_sort_fp_get_sig_size(sort: BitwuzlaSort) -> u64; } extern "C" { pub fn bitwuzla_sort_array_get_index(sort: BitwuzlaSort) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_sort_array_get_element(sort: BitwuzlaSort) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_sort_fun_get_domain_sorts( sort: BitwuzlaSort, size: *mut usize, ) -> *mut BitwuzlaSort; } extern "C" { pub fn bitwuzla_sort_fun_get_codomain(sort: BitwuzlaSort) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_sort_fun_get_arity(sort: BitwuzlaSort) -> u64; } extern "C" { pub fn bitwuzla_sort_get_uninterpreted_symbol( sort: BitwuzlaSort, ) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_sort_is_array(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_bool(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_bv(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_fp(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_fun(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_rm(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_is_uninterpreted(sort: BitwuzlaSort) -> bool; } extern "C" { pub fn bitwuzla_sort_to_string(sort: BitwuzlaSort) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_sort_print(sort: BitwuzlaSort, file: *mut FILE); } pub type BitwuzlaTerm = u64; extern "C" { pub fn bitwuzla_term_hash(term: BitwuzlaTerm) -> usize; } extern "C" { pub fn bitwuzla_term_copy(term: BitwuzlaTerm) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_term_release(term: BitwuzlaTerm); } extern "C" { pub fn bitwuzla_term_get_kind(term: BitwuzlaTerm) -> BitwuzlaKind; } extern "C" { pub fn bitwuzla_term_get_children(term: BitwuzlaTerm, size: *mut usize) -> *mut BitwuzlaTerm; } extern "C" { pub fn bitwuzla_term_get_indices(term: BitwuzlaTerm, size: *mut usize) -> *mut u64; } extern "C" { pub fn bitwuzla_term_is_indexed(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_get_sort(term: BitwuzlaTerm) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_term_array_get_index_sort(term: BitwuzlaTerm) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_term_array_get_element_sort(term: BitwuzlaTerm) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_term_fun_get_domain_sorts( term: BitwuzlaTerm, size: *mut usize, ) -> *mut BitwuzlaSort; } extern "C" { pub fn bitwuzla_term_fun_get_codomain_sort(term: BitwuzlaTerm) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_term_bv_get_size(term: BitwuzlaTerm) -> u64; } extern "C" { pub fn bitwuzla_term_fp_get_exp_size(term: BitwuzlaTerm) -> u64; } extern "C" { pub fn bitwuzla_term_fp_get_sig_size(term: BitwuzlaTerm) -> u64; } extern "C" { pub fn bitwuzla_term_fun_get_arity(term: BitwuzlaTerm) -> u64; } extern "C" { pub fn bitwuzla_term_get_symbol(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_term_is_equal_sort(term0: BitwuzlaTerm, term1: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_array(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_const(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fun(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_var(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_value(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bool(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_uninterpreted(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_true(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_false(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value_zero(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value_one(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value_ones(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value_min_signed(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_bv_value_max_signed(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value_pos_zero(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value_neg_zero(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value_pos_inf(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value_neg_inf(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_fp_value_nan(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value_rna(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value_rne(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value_rtn(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value_rtp(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_is_rm_value_rtz(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_value_get_bool(term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_term_value_get_str(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_term_value_get_str_fmt( term: BitwuzlaTerm, base: u8, ) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_term_value_get_fp_ieee( term: BitwuzlaTerm, sign: *mut *const ::std::os::raw::c_char, exponent: *mut *const ::std::os::raw::c_char, significand: *mut *const ::std::os::raw::c_char, base: u8, ); } extern "C" { pub fn bitwuzla_term_value_get_rm(term: BitwuzlaTerm) -> BitwuzlaRoundingMode; } extern "C" { pub fn bitwuzla_term_to_string(term: BitwuzlaTerm) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_term_to_string_fmt( term: BitwuzlaTerm, base: u8, ) -> *const ::std::os::raw::c_char; } extern "C" { pub fn bitwuzla_term_print(term: BitwuzlaTerm, file: *mut FILE); } extern "C" { pub fn bitwuzla_term_print_fmt(term: BitwuzlaTerm, file: *mut FILE, base: u8); } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct BitwuzlaTermManager { _unused: [u8; 0], } #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct Bitwuzla { _unused: [u8; 0], } extern "C" { pub fn bitwuzla_new( tm: *mut BitwuzlaTermManager, options: *const BitwuzlaOptions, ) -> *mut Bitwuzla; } extern "C" { pub fn bitwuzla_delete(bitwuzla: *mut Bitwuzla); } extern "C" { pub fn bitwuzla_set_termination_callback( bitwuzla: *mut Bitwuzla, fun: ::std::option::Option i32>, state: *mut ::std::os::raw::c_void, ); } extern "C" { pub fn bitwuzla_get_termination_callback_state( bitwuzla: *mut Bitwuzla, ) -> *mut ::std::os::raw::c_void; } extern "C" { pub fn bitwuzla_set_abort_callback( fun: ::std::option::Option, ); } extern "C" { pub fn bitwuzla_push(bitwuzla: *mut Bitwuzla, nlevels: u64); } extern "C" { pub fn bitwuzla_pop(bitwuzla: *mut Bitwuzla, nlevels: u64); } extern "C" { pub fn bitwuzla_assert(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm); } extern "C" { pub fn bitwuzla_get_assertions(bitwuzla: *mut Bitwuzla, size: *mut usize) -> *mut BitwuzlaTerm; } extern "C" { pub fn bitwuzla_is_unsat_assumption(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> bool; } extern "C" { pub fn bitwuzla_get_unsat_assumptions( bitwuzla: *mut Bitwuzla, size: *mut usize, ) -> *mut BitwuzlaTerm; } extern "C" { pub fn bitwuzla_get_unsat_core(bitwuzla: *mut Bitwuzla, size: *mut usize) -> *mut BitwuzlaTerm; } extern "C" { pub fn bitwuzla_simplify(bitwuzla: *mut Bitwuzla); } extern "C" { pub fn bitwuzla_check_sat(bitwuzla: *mut Bitwuzla) -> BitwuzlaResult; } extern "C" { pub fn bitwuzla_check_sat_assuming( bitwuzla: *mut Bitwuzla, argc: u32, args: *mut BitwuzlaTerm, ) -> BitwuzlaResult; } extern "C" { pub fn bitwuzla_get_value(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_print_formula( bitwuzla: *mut Bitwuzla, format: *const ::std::os::raw::c_char, file: *mut FILE, base: u8, ); } extern "C" { pub fn bitwuzla_get_statistics( bitwuzla: *mut Bitwuzla, keys: *mut *mut *const ::std::os::raw::c_char, values: *mut *mut *const ::std::os::raw::c_char, size: *mut usize, ); } extern "C" { pub fn bitwuzla_get_term_mgr(bitwuzla: *mut Bitwuzla) -> *mut BitwuzlaTermManager; } extern "C" { pub fn bitwuzla_term_manager_new() -> *mut BitwuzlaTermManager; } extern "C" { pub fn bitwuzla_term_manager_delete(tm: *mut BitwuzlaTermManager); } extern "C" { pub fn bitwuzla_term_manager_release(tm: *mut BitwuzlaTermManager); } extern "C" { pub fn bitwuzla_mk_array_sort( tm: *mut BitwuzlaTermManager, index: BitwuzlaSort, element: BitwuzlaSort, ) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_bool_sort(tm: *mut BitwuzlaTermManager) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_bv_sort(tm: *mut BitwuzlaTermManager, size: u64) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_fp_sort( tm: *mut BitwuzlaTermManager, exp_size: u64, sig_size: u64, ) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_fun_sort( tm: *mut BitwuzlaTermManager, arity: u64, domain: *mut BitwuzlaSort, codomain: BitwuzlaSort, ) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_rm_sort(tm: *mut BitwuzlaTermManager) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_uninterpreted_sort( tm: *mut BitwuzlaTermManager, symbol: *const ::std::os::raw::c_char, ) -> BitwuzlaSort; } extern "C" { pub fn bitwuzla_mk_true(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_false(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_zero(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_one(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_ones(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_min_signed( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_max_signed( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_pos_zero( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_neg_zero( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_pos_inf(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_neg_inf(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_nan(tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_value( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, value: *const ::std::os::raw::c_char, base: u8, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_value_uint64( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, value: u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_bv_value_int64( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, value: i64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_value( tm: *mut BitwuzlaTermManager, bv_sign: BitwuzlaTerm, bv_exponent: BitwuzlaTerm, bv_significand: BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_from_real( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, rm: BitwuzlaTerm, real: *const ::std::os::raw::c_char, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_fp_from_rational( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, rm: BitwuzlaTerm, num: *const ::std::os::raw::c_char, den: *const ::std::os::raw::c_char, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_rm_value( tm: *mut BitwuzlaTermManager, rm: BitwuzlaRoundingMode, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term1( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg: BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term2( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg0: BitwuzlaTerm, arg1: BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term3( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg0: BitwuzlaTerm, arg1: BitwuzlaTerm, arg2: BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, argc: u32, args: *mut BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term1_indexed1( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg: BitwuzlaTerm, idx: u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term1_indexed2( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg: BitwuzlaTerm, idx0: u64, idx1: u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term2_indexed1( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg0: BitwuzlaTerm, arg1: BitwuzlaTerm, idx: u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term2_indexed2( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, arg0: BitwuzlaTerm, arg1: BitwuzlaTerm, idx0: u64, idx1: u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_term_indexed( tm: *mut BitwuzlaTermManager, kind: BitwuzlaKind, argc: u32, args: *mut BitwuzlaTerm, idxc: u32, idxs: *const u64, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_const( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, symbol: *const ::std::os::raw::c_char, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_const_array( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, value: BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_mk_var( tm: *mut BitwuzlaTermManager, sort: BitwuzlaSort, symbol: *const ::std::os::raw::c_char, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_substitute_term( term: BitwuzlaTerm, map_size: usize, map_keys: *mut BitwuzlaTerm, map_values: *mut BitwuzlaTerm, ) -> BitwuzlaTerm; } extern "C" { pub fn bitwuzla_substitute_terms( terms_size: usize, terms: *mut BitwuzlaTerm, map_size: usize, map_keys: *mut BitwuzlaTerm, map_values: *mut BitwuzlaTerm, ); }