List of all items
Structs
- Bitwuzla
- BitwuzlaOptionInfo
- BitwuzlaOptionInfo_ModeValue
- BitwuzlaOptionInfo_NumericValue
- BitwuzlaOptionInfo_StringValue
- BitwuzlaOptions
- BitwuzlaTermManager
Functions
- bitwuzla_assert
- bitwuzla_check_sat
- bitwuzla_check_sat_assuming
- bitwuzla_copyright
- bitwuzla_delete
- bitwuzla_get_assertions
- bitwuzla_get_option
- bitwuzla_get_option_info
- bitwuzla_get_option_mode
- bitwuzla_get_option_string
- bitwuzla_get_statistics
- bitwuzla_get_term_mgr
- bitwuzla_get_termination_callback_state
- bitwuzla_get_unsat_assumptions
- bitwuzla_get_unsat_core
- bitwuzla_get_value
- bitwuzla_git_id
- bitwuzla_is_unsat_assumption
- bitwuzla_kind_to_string
- bitwuzla_mk_array_sort
- bitwuzla_mk_bool_sort
- bitwuzla_mk_bv_max_signed
- bitwuzla_mk_bv_min_signed
- bitwuzla_mk_bv_one
- bitwuzla_mk_bv_ones
- bitwuzla_mk_bv_sort
- bitwuzla_mk_bv_value
- bitwuzla_mk_bv_value_int64
- bitwuzla_mk_bv_value_uint64
- bitwuzla_mk_bv_zero
- bitwuzla_mk_const
- bitwuzla_mk_const_array
- bitwuzla_mk_false
- bitwuzla_mk_fp_from_rational
- bitwuzla_mk_fp_from_real
- bitwuzla_mk_fp_nan
- bitwuzla_mk_fp_neg_inf
- bitwuzla_mk_fp_neg_zero
- bitwuzla_mk_fp_pos_inf
- bitwuzla_mk_fp_pos_zero
- bitwuzla_mk_fp_sort
- bitwuzla_mk_fp_value
- bitwuzla_mk_fun_sort
- bitwuzla_mk_rm_sort
- bitwuzla_mk_rm_value
- bitwuzla_mk_term
- bitwuzla_mk_term1
- bitwuzla_mk_term1_indexed1
- bitwuzla_mk_term1_indexed2
- bitwuzla_mk_term2
- bitwuzla_mk_term2_indexed1
- bitwuzla_mk_term2_indexed2
- bitwuzla_mk_term3
- bitwuzla_mk_term_indexed
- bitwuzla_mk_true
- bitwuzla_mk_uninterpreted_sort
- bitwuzla_mk_var
- bitwuzla_new
- bitwuzla_option_is_mode
- bitwuzla_option_is_numeric
- bitwuzla_option_is_string
- bitwuzla_option_is_valid
- bitwuzla_options_delete
- bitwuzla_options_new
- bitwuzla_pop
- bitwuzla_print_formula
- bitwuzla_print_unsat_core
- bitwuzla_push
- bitwuzla_result_to_string
- bitwuzla_rm_to_string
- bitwuzla_set_abort_callback
- bitwuzla_set_option
- bitwuzla_set_option_mode
- bitwuzla_set_option_string
- bitwuzla_set_termination_callback
- bitwuzla_simplify
- bitwuzla_simplify_term
- bitwuzla_sort_array_get_element
- bitwuzla_sort_array_get_index
- bitwuzla_sort_bv_get_size
- bitwuzla_sort_copy
- bitwuzla_sort_fp_get_exp_size
- bitwuzla_sort_fp_get_sig_size
- bitwuzla_sort_fun_get_arity
- bitwuzla_sort_fun_get_codomain
- bitwuzla_sort_fun_get_domain_sorts
- bitwuzla_sort_get_uninterpreted_symbol
- bitwuzla_sort_hash
- bitwuzla_sort_is_array
- bitwuzla_sort_is_bool
- bitwuzla_sort_is_bv
- bitwuzla_sort_is_fp
- bitwuzla_sort_is_fun
- bitwuzla_sort_is_rm
- bitwuzla_sort_is_uninterpreted
- bitwuzla_sort_print
- bitwuzla_sort_release
- bitwuzla_sort_to_string
- bitwuzla_substitute_term
- bitwuzla_substitute_terms
- bitwuzla_term_array_get_element_sort
- bitwuzla_term_array_get_index_sort
- bitwuzla_term_bv_get_size
- bitwuzla_term_copy
- bitwuzla_term_fp_get_exp_size
- bitwuzla_term_fp_get_sig_size
- bitwuzla_term_fp_value_to_real_string
- bitwuzla_term_fun_get_arity
- bitwuzla_term_fun_get_codomain_sort
- bitwuzla_term_fun_get_domain_sorts
- bitwuzla_term_get_children
- bitwuzla_term_get_indices
- bitwuzla_term_get_kind
- bitwuzla_term_get_sort
- bitwuzla_term_get_symbol
- bitwuzla_term_hash
- bitwuzla_term_is_array
- bitwuzla_term_is_bool
- bitwuzla_term_is_bv
- bitwuzla_term_is_bv_value
- bitwuzla_term_is_bv_value_max_signed
- bitwuzla_term_is_bv_value_min_signed
- bitwuzla_term_is_bv_value_one
- bitwuzla_term_is_bv_value_ones
- bitwuzla_term_is_bv_value_zero
- bitwuzla_term_is_const
- bitwuzla_term_is_equal_sort
- bitwuzla_term_is_false
- bitwuzla_term_is_fp
- bitwuzla_term_is_fp_value
- bitwuzla_term_is_fp_value_nan
- bitwuzla_term_is_fp_value_neg_inf
- bitwuzla_term_is_fp_value_neg_zero
- bitwuzla_term_is_fp_value_pos_inf
- bitwuzla_term_is_fp_value_pos_zero
- bitwuzla_term_is_fun
- bitwuzla_term_is_indexed
- bitwuzla_term_is_rm
- bitwuzla_term_is_rm_value
- bitwuzla_term_is_rm_value_rna
- bitwuzla_term_is_rm_value_rne
- bitwuzla_term_is_rm_value_rtn
- bitwuzla_term_is_rm_value_rtp
- bitwuzla_term_is_rm_value_rtz
- bitwuzla_term_is_true
- bitwuzla_term_is_uninterpreted
- bitwuzla_term_is_value
- bitwuzla_term_is_var
- bitwuzla_term_manager_delete
- bitwuzla_term_manager_new
- bitwuzla_term_manager_release
- bitwuzla_term_print
- bitwuzla_term_print_fmt
- bitwuzla_term_release
- bitwuzla_term_to_string
- bitwuzla_term_to_string_fmt
- bitwuzla_term_value_get_bool
- bitwuzla_term_value_get_fp_ieee
- bitwuzla_term_value_get_rm
- bitwuzla_term_value_get_str
- bitwuzla_term_value_get_str_fmt
- bitwuzla_version
Type Aliases
Constants
- BITWUZLA_KIND_AND
- BITWUZLA_KIND_APPLY
- BITWUZLA_KIND_ARRAY_SELECT
- BITWUZLA_KIND_ARRAY_STORE
- BITWUZLA_KIND_BV_ADD
- BITWUZLA_KIND_BV_AND
- BITWUZLA_KIND_BV_ASHR
- BITWUZLA_KIND_BV_COMP
- BITWUZLA_KIND_BV_CONCAT
- BITWUZLA_KIND_BV_DEC
- BITWUZLA_KIND_BV_EXTRACT
- BITWUZLA_KIND_BV_INC
- BITWUZLA_KIND_BV_MUL
- BITWUZLA_KIND_BV_NAND
- BITWUZLA_KIND_BV_NEG
- BITWUZLA_KIND_BV_NEG_OVERFLOW
- BITWUZLA_KIND_BV_NOR
- BITWUZLA_KIND_BV_NOT
- BITWUZLA_KIND_BV_OR
- BITWUZLA_KIND_BV_REDAND
- BITWUZLA_KIND_BV_REDOR
- BITWUZLA_KIND_BV_REDXOR
- BITWUZLA_KIND_BV_REPEAT
- BITWUZLA_KIND_BV_ROL
- BITWUZLA_KIND_BV_ROLI
- BITWUZLA_KIND_BV_ROR
- BITWUZLA_KIND_BV_RORI
- BITWUZLA_KIND_BV_SADD_OVERFLOW
- BITWUZLA_KIND_BV_SDIV
- BITWUZLA_KIND_BV_SDIV_OVERFLOW
- BITWUZLA_KIND_BV_SGE
- BITWUZLA_KIND_BV_SGT
- BITWUZLA_KIND_BV_SHL
- BITWUZLA_KIND_BV_SHR
- BITWUZLA_KIND_BV_SIGN_EXTEND
- BITWUZLA_KIND_BV_SLE
- BITWUZLA_KIND_BV_SLT
- BITWUZLA_KIND_BV_SMOD
- BITWUZLA_KIND_BV_SMUL_OVERFLOW
- BITWUZLA_KIND_BV_SREM
- BITWUZLA_KIND_BV_SSUB_OVERFLOW
- BITWUZLA_KIND_BV_SUB
- BITWUZLA_KIND_BV_UADD_OVERFLOW
- BITWUZLA_KIND_BV_UDIV
- BITWUZLA_KIND_BV_UGE
- BITWUZLA_KIND_BV_UGT
- BITWUZLA_KIND_BV_ULE
- BITWUZLA_KIND_BV_ULT
- BITWUZLA_KIND_BV_UMUL_OVERFLOW
- BITWUZLA_KIND_BV_UREM
- BITWUZLA_KIND_BV_USUB_OVERFLOW
- BITWUZLA_KIND_BV_XNOR
- BITWUZLA_KIND_BV_XOR
- BITWUZLA_KIND_BV_ZERO_EXTEND
- BITWUZLA_KIND_CONSTANT
- BITWUZLA_KIND_CONST_ARRAY
- BITWUZLA_KIND_DISTINCT
- BITWUZLA_KIND_EQUAL
- BITWUZLA_KIND_EXISTS
- BITWUZLA_KIND_FORALL
- BITWUZLA_KIND_FP_ABS
- BITWUZLA_KIND_FP_ADD
- BITWUZLA_KIND_FP_DIV
- BITWUZLA_KIND_FP_EQUAL
- BITWUZLA_KIND_FP_FMA
- BITWUZLA_KIND_FP_FP
- BITWUZLA_KIND_FP_GEQ
- BITWUZLA_KIND_FP_GT
- BITWUZLA_KIND_FP_IS_INF
- BITWUZLA_KIND_FP_IS_NAN
- BITWUZLA_KIND_FP_IS_NEG
- BITWUZLA_KIND_FP_IS_NORMAL
- BITWUZLA_KIND_FP_IS_POS
- BITWUZLA_KIND_FP_IS_SUBNORMAL
- BITWUZLA_KIND_FP_IS_ZERO
- BITWUZLA_KIND_FP_LEQ
- BITWUZLA_KIND_FP_LT
- BITWUZLA_KIND_FP_MAX
- BITWUZLA_KIND_FP_MIN
- BITWUZLA_KIND_FP_MUL
- BITWUZLA_KIND_FP_NEG
- BITWUZLA_KIND_FP_REM
- BITWUZLA_KIND_FP_RTI
- BITWUZLA_KIND_FP_SQRT
- BITWUZLA_KIND_FP_SUB
- BITWUZLA_KIND_FP_TO_FP_FROM_BV
- BITWUZLA_KIND_FP_TO_FP_FROM_FP
- BITWUZLA_KIND_FP_TO_FP_FROM_SBV
- BITWUZLA_KIND_FP_TO_FP_FROM_UBV
- BITWUZLA_KIND_FP_TO_SBV
- BITWUZLA_KIND_FP_TO_UBV
- BITWUZLA_KIND_IFF
- BITWUZLA_KIND_IMPLIES
- BITWUZLA_KIND_ITE
- BITWUZLA_KIND_LAMBDA
- BITWUZLA_KIND_NOT
- BITWUZLA_KIND_NUM_KINDS
- BITWUZLA_KIND_OR
- BITWUZLA_KIND_VALUE
- BITWUZLA_KIND_VARIABLE
- BITWUZLA_KIND_XOR
- BITWUZLA_OPT_ABSTRACTION
- BITWUZLA_OPT_ABSTRACTION_ASSERT
- BITWUZLA_OPT_ABSTRACTION_ASSERT_REFS
- BITWUZLA_OPT_ABSTRACTION_BV_ADD
- BITWUZLA_OPT_ABSTRACTION_BV_MUL
- BITWUZLA_OPT_ABSTRACTION_BV_SIZE
- BITWUZLA_OPT_ABSTRACTION_BV_UDIV
- BITWUZLA_OPT_ABSTRACTION_BV_UREM
- BITWUZLA_OPT_ABSTRACTION_EAGER_REFINE
- BITWUZLA_OPT_ABSTRACTION_EQUAL
- BITWUZLA_OPT_ABSTRACTION_INC_BITBLAST
- BITWUZLA_OPT_ABSTRACTION_INITIAL_LEMMAS
- BITWUZLA_OPT_ABSTRACTION_ITE
- BITWUZLA_OPT_ABSTRACTION_VALUE_LIMIT
- BITWUZLA_OPT_ABSTRACTION_VALUE_ONLY
- BITWUZLA_OPT_BV_SOLVER
- BITWUZLA_OPT_DBG_CHECK_MODEL
- BITWUZLA_OPT_DBG_CHECK_UNSAT_CORE
- BITWUZLA_OPT_DBG_PP_NODE_THRESH
- BITWUZLA_OPT_DBG_RW_NODE_THRESH
- BITWUZLA_OPT_LOGLEVEL
- BITWUZLA_OPT_MEMORY_LIMIT
- BITWUZLA_OPT_NTHREADS
- BITWUZLA_OPT_NUM_OPTS
- BITWUZLA_OPT_PP_CONTRADICTING_ANDS
- BITWUZLA_OPT_PP_ELIM_BV_EXTRACTS
- BITWUZLA_OPT_PP_ELIM_BV_UDIV
- BITWUZLA_OPT_PP_EMBEDDED_CONSTR
- BITWUZLA_OPT_PP_FLATTEN_AND
- BITWUZLA_OPT_PP_NORMALIZE
- BITWUZLA_OPT_PP_SKELETON_PREPROC
- BITWUZLA_OPT_PP_VARIABLE_SUBST
- BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_BV_INEQ
- BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_DISEQ
- BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_EQ
- BITWUZLA_OPT_PREPROCESS
- BITWUZLA_OPT_PRODUCE_MODELS
- BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS
- BITWUZLA_OPT_PRODUCE_UNSAT_CORES
- BITWUZLA_OPT_PROP_CONST_BITS
- BITWUZLA_OPT_PROP_INFER_INEQ_BOUNDS
- BITWUZLA_OPT_PROP_NPROPS
- BITWUZLA_OPT_PROP_NUPDATES
- BITWUZLA_OPT_PROP_OPT_LT_CONCAT_SEXT
- BITWUZLA_OPT_PROP_PATH_SEL
- BITWUZLA_OPT_PROP_PROB_RANDOM_INPUT
- BITWUZLA_OPT_PROP_PROB_USE_INV_VALUE
- BITWUZLA_OPT_PROP_SEXT
- BITWUZLA_OPT_REWRITE_LEVEL
- BITWUZLA_OPT_SAT_SOLVER
- BITWUZLA_OPT_SEED
- BITWUZLA_OPT_TIME_LIMIT_PER
- BITWUZLA_OPT_VERBOSITY
- BITWUZLA_OPT_WRITE_AIGER
- BITWUZLA_OPT_WRITE_CNF
- BITWUZLA_RM_MAX
- BITWUZLA_RM_RNA
- BITWUZLA_RM_RNE
- BITWUZLA_RM_RTN
- BITWUZLA_RM_RTP
- BITWUZLA_RM_RTZ
- BITWUZLA_SAT
- BITWUZLA_UNKNOWN
- BITWUZLA_UNSAT