Index

_

__init__() (bitwuzla.Bitwuzla method) (bitwuzla.Parser method) (bitwuzla.TermManager method)

A

AND (bitwuzla.Kind attribute) APPLY (bitwuzla.Kind attribute) array_element() (bitwuzla.Sort method)

array_index() (bitwuzla.Sort method) ARRAY_SELECT (bitwuzla.Kind attribute) ARRAY_STORE (bitwuzla.Kind attribute) assert_formula() (bitwuzla.Bitwuzla method)

B

Bitwuzla (C++ type) (class in bitwuzla) bitwuzla() (bitwuzla.Parser method) bitwuzla::Bitwuzla (C++ class) bitwuzla::Bitwuzla::assert_formula (C++ function) bitwuzla::Bitwuzla::Bitwuzla (C++ function), [1], [2] bitwuzla::Bitwuzla::check_sat (C++ function) bitwuzla::Bitwuzla::configure_terminator (C++ function) bitwuzla::Bitwuzla::get_assertions (C++ function) bitwuzla::Bitwuzla::get_unsat_assumptions (C++ function) bitwuzla::Bitwuzla::get_unsat_core (C++ function) bitwuzla::Bitwuzla::get_value (C++ function) bitwuzla::Bitwuzla::is_unsat_assumption (C++ function) bitwuzla::Bitwuzla::operator= (C++ function) bitwuzla::Bitwuzla::pop (C++ function) bitwuzla::Bitwuzla::print_formula (C++ function) bitwuzla::Bitwuzla::push (C++ function) bitwuzla::Bitwuzla::simplify (C++ function) bitwuzla::Bitwuzla::statistics (C++ function) bitwuzla::Bitwuzla::term_mgr (C++ function) bitwuzla::Bitwuzla::~Bitwuzla (C++ function) bitwuzla::Exception (C++ class) bitwuzla::Exception::Exception (C++ function), [1] bitwuzla::Exception::msg (C++ function) bitwuzla::Kind (C++ enum) bitwuzla::Kind::AND (C++ enumerator) bitwuzla::Kind::APPLY (C++ enumerator) bitwuzla::Kind::ARRAY_SELECT (C++ enumerator) bitwuzla::Kind::ARRAY_STORE (C++ enumerator) bitwuzla::Kind::BV_ADD (C++ enumerator) bitwuzla::Kind::BV_AND (C++ enumerator) bitwuzla::Kind::BV_ASHR (C++ enumerator) bitwuzla::Kind::BV_COMP (C++ enumerator) bitwuzla::Kind::BV_CONCAT (C++ enumerator) bitwuzla::Kind::BV_DEC (C++ enumerator) bitwuzla::Kind::BV_EXTRACT (C++ enumerator) bitwuzla::Kind::BV_INC (C++ enumerator) bitwuzla::Kind::BV_MUL (C++ enumerator) bitwuzla::Kind::BV_NAND (C++ enumerator) bitwuzla::Kind::BV_NEG (C++ enumerator) bitwuzla::Kind::BV_NEG_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_NOR (C++ enumerator) bitwuzla::Kind::BV_NOT (C++ enumerator) bitwuzla::Kind::BV_OR (C++ enumerator) bitwuzla::Kind::BV_REDAND (C++ enumerator) bitwuzla::Kind::BV_REDOR (C++ enumerator) bitwuzla::Kind::BV_REDXOR (C++ enumerator) bitwuzla::Kind::BV_REPEAT (C++ enumerator) bitwuzla::Kind::BV_ROL (C++ enumerator) bitwuzla::Kind::BV_ROLI (C++ enumerator) bitwuzla::Kind::BV_ROR (C++ enumerator) bitwuzla::Kind::BV_RORI (C++ enumerator) bitwuzla::Kind::BV_SADD_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_SDIV (C++ enumerator) bitwuzla::Kind::BV_SDIV_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_SGE (C++ enumerator) bitwuzla::Kind::BV_SGT (C++ enumerator) bitwuzla::Kind::BV_SHL (C++ enumerator) bitwuzla::Kind::BV_SHR (C++ enumerator) bitwuzla::Kind::BV_SIGN_EXTEND (C++ enumerator) bitwuzla::Kind::BV_SLE (C++ enumerator) bitwuzla::Kind::BV_SLT (C++ enumerator) bitwuzla::Kind::BV_SMOD (C++ enumerator) bitwuzla::Kind::BV_SMUL_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_SREM (C++ enumerator) bitwuzla::Kind::BV_SSUB_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_SUB (C++ enumerator) bitwuzla::Kind::BV_UADD_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_UDIV (C++ enumerator) bitwuzla::Kind::BV_UGE (C++ enumerator) bitwuzla::Kind::BV_UGT (C++ enumerator) bitwuzla::Kind::BV_ULE (C++ enumerator) bitwuzla::Kind::BV_ULT (C++ enumerator) bitwuzla::Kind::BV_UMUL_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_UREM (C++ enumerator) bitwuzla::Kind::BV_USUB_OVERFLOW (C++ enumerator) bitwuzla::Kind::BV_XNOR (C++ enumerator) bitwuzla::Kind::BV_XOR (C++ enumerator) bitwuzla::Kind::BV_ZERO_EXTEND (C++ enumerator) bitwuzla::Kind::CONST_ARRAY (C++ enumerator) bitwuzla::Kind::CONSTANT (C++ enumerator) bitwuzla::Kind::DISTINCT (C++ enumerator) bitwuzla::Kind::EQUAL (C++ enumerator) bitwuzla::Kind::EXISTS (C++ enumerator) bitwuzla::Kind::FORALL (C++ enumerator) bitwuzla::Kind::FP_ABS (C++ enumerator) bitwuzla::Kind::FP_ADD (C++ enumerator) bitwuzla::Kind::FP_DIV (C++ enumerator) bitwuzla::Kind::FP_EQUAL (C++ enumerator) bitwuzla::Kind::FP_FMA (C++ enumerator) bitwuzla::Kind::FP_FP (C++ enumerator) bitwuzla::Kind::FP_GEQ (C++ enumerator) bitwuzla::Kind::FP_GT (C++ enumerator) bitwuzla::Kind::FP_IS_INF (C++ enumerator) bitwuzla::Kind::FP_IS_NAN (C++ enumerator) bitwuzla::Kind::FP_IS_NEG (C++ enumerator) bitwuzla::Kind::FP_IS_NORMAL (C++ enumerator) bitwuzla::Kind::FP_IS_POS (C++ enumerator) bitwuzla::Kind::FP_IS_SUBNORMAL (C++ enumerator) bitwuzla::Kind::FP_IS_ZERO (C++ enumerator) bitwuzla::Kind::FP_LEQ (C++ enumerator) bitwuzla::Kind::FP_LT (C++ enumerator) bitwuzla::Kind::FP_MAX (C++ enumerator) bitwuzla::Kind::FP_MIN (C++ enumerator) bitwuzla::Kind::FP_MUL (C++ enumerator) bitwuzla::Kind::FP_NEG (C++ enumerator) bitwuzla::Kind::FP_REM (C++ enumerator) bitwuzla::Kind::FP_RTI (C++ enumerator) bitwuzla::Kind::FP_SQRT (C++ enumerator) bitwuzla::Kind::FP_SUB (C++ enumerator) bitwuzla::Kind::FP_TO_FP_FROM_BV (C++ enumerator) bitwuzla::Kind::FP_TO_FP_FROM_FP (C++ enumerator) bitwuzla::Kind::FP_TO_FP_FROM_SBV (C++ enumerator) bitwuzla::Kind::FP_TO_FP_FROM_UBV (C++ enumerator) bitwuzla::Kind::FP_TO_SBV (C++ enumerator) bitwuzla::Kind::FP_TO_UBV (C++ enumerator) bitwuzla::Kind::IFF (C++ enumerator) bitwuzla::Kind::IMPLIES (C++ enumerator) bitwuzla::Kind::ITE (C++ enumerator) bitwuzla::Kind::LAMBDA (C++ enumerator) bitwuzla::Kind::NOT (C++ enumerator) bitwuzla::Kind::OR (C++ enumerator) bitwuzla::Kind::VALUE (C++ enumerator) bitwuzla::Kind::VARIABLE (C++ enumerator) bitwuzla::Kind::XOR (C++ enumerator) bitwuzla::operator!= (C++ function), [1] bitwuzla::operator<< (C++ function), [1], [2], [3] bitwuzla::operator== (C++ function), [1] bitwuzla::Option (C++ enum) bitwuzla::Option::BV_SOLVER (C++ enumerator) bitwuzla::Option::DBG_CHECK_MODEL (C++ enumerator) bitwuzla::Option::DBG_CHECK_UNSAT_CORE (C++ enumerator) bitwuzla::Option::DBG_PP_NODE_THRESH (C++ enumerator) bitwuzla::Option::DBG_RW_NODE_THRESH (C++ enumerator) bitwuzla::Option::LOGLEVEL (C++ enumerator) bitwuzla::Option::MEMORY_LIMIT (C++ enumerator) bitwuzla::Option::PP_CONTRADICTING_ANDS (C++ enumerator) bitwuzla::Option::PP_ELIM_BV_EXTRACTS (C++ enumerator) bitwuzla::Option::PP_EMBEDDED_CONSTR (C++ enumerator) bitwuzla::Option::PP_FLATTEN_AND (C++ enumerator) bitwuzla::Option::PP_NORMALIZE (C++ enumerator) bitwuzla::Option::PP_NORMALIZE_SHARE_AWARE (C++ enumerator) bitwuzla::Option::PP_SKELETON_PREPROC (C++ enumerator) bitwuzla::Option::PP_VARIABLE_SUBST (C++ enumerator) bitwuzla::Option::PP_VARIABLE_SUBST_NORM_BV_INEQ (C++ enumerator) bitwuzla::Option::PP_VARIABLE_SUBST_NORM_DISEQ (C++ enumerator) bitwuzla::Option::PP_VARIABLE_SUBST_NORM_EQ (C++ enumerator) bitwuzla::Option::PREPROCESS (C++ enumerator) bitwuzla::Option::PRODUCE_MODELS (C++ enumerator) bitwuzla::Option::PRODUCE_UNSAT_ASSUMPTIONS (C++ enumerator) bitwuzla::Option::PRODUCE_UNSAT_CORES (C++ enumerator) bitwuzla::Option::PROP_CONST_BITS (C++ enumerator) bitwuzla::Option::PROP_INFER_INEQ_BOUNDS (C++ enumerator) bitwuzla::Option::PROP_NORMALIZE (C++ enumerator) bitwuzla::Option::PROP_NPROPS (C++ enumerator) bitwuzla::Option::PROP_NUPDATES (C++ enumerator) bitwuzla::Option::PROP_OPT_LT_CONCAT_SEXT (C++ enumerator) bitwuzla::Option::PROP_PATH_SEL (C++ enumerator) bitwuzla::Option::PROP_PROB_RANDOM_INPUT (C++ enumerator) bitwuzla::Option::PROP_PROB_USE_INV_VALUE (C++ enumerator) bitwuzla::Option::PROP_SEXT (C++ enumerator) bitwuzla::Option::REWRITE_LEVEL (C++ enumerator) bitwuzla::Option::SAT_SOLVER (C++ enumerator) bitwuzla::Option::SEED (C++ enumerator) bitwuzla::Option::TIME_LIMIT_PER (C++ enumerator) bitwuzla::Option::VERBOSITY (C++ enumerator) bitwuzla::OptionInfo (C++ struct) bitwuzla::OptionInfo::Bool (C++ struct) bitwuzla::OptionInfo::Bool::cur (C++ member) bitwuzla::OptionInfo::Bool::dflt (C++ member) bitwuzla::OptionInfo::description (C++ member) bitwuzla::OptionInfo::Kind (C++ enum) bitwuzla::OptionInfo::kind (C++ member) bitwuzla::OptionInfo::Kind::BOOL (C++ enumerator) bitwuzla::OptionInfo::Kind::MODE (C++ enumerator) bitwuzla::OptionInfo::Kind::NUMERIC (C++ enumerator) bitwuzla::OptionInfo::lng (C++ member) bitwuzla::OptionInfo::Mode (C++ struct) bitwuzla::OptionInfo::Mode::cur (C++ member) bitwuzla::OptionInfo::Mode::dflt (C++ member) bitwuzla::OptionInfo::Mode::modes (C++ member) bitwuzla::OptionInfo::Numeric (C++ struct) bitwuzla::OptionInfo::Numeric::cur (C++ member) bitwuzla::OptionInfo::Numeric::dflt (C++ member) bitwuzla::OptionInfo::Numeric::max (C++ member) bitwuzla::OptionInfo::Numeric::min (C++ member) bitwuzla::OptionInfo::opt (C++ member) bitwuzla::OptionInfo::OptionInfo (C++ function), [1] bitwuzla::OptionInfo::shrt (C++ member) bitwuzla::OptionInfo::value (C++ function), [1], [2], [3] bitwuzla::OptionInfo::values (C++ member) bitwuzla::OptionInfo::~OptionInfo (C++ function) bitwuzla::Options (C++ class) bitwuzla::Options::description (C++ function) bitwuzla::Options::get (C++ function) bitwuzla::Options::get_mode (C++ function) bitwuzla::Options::is_bool (C++ function) bitwuzla::Options::is_mode (C++ function) bitwuzla::Options::is_numeric (C++ function) bitwuzla::Options::is_valid (C++ function) bitwuzla::Options::lng (C++ function) bitwuzla::Options::modes (C++ function) bitwuzla::Options::operator= (C++ function) bitwuzla::Options::option (C++ function) bitwuzla::Options::Options (C++ function), [1] bitwuzla::Options::set (C++ function), [1], [2], [3], [4] bitwuzla::Options::shrt (C++ function) bitwuzla::Options::~Options (C++ function) bitwuzla::parser::Parser (C++ class) bitwuzla::parser::Parser::bitwuzla (C++ function) bitwuzla::parser::Parser::parse (C++ function), [1] bitwuzla::parser::Parser::parse_sort (C++ function) bitwuzla::parser::Parser::parse_term (C++ function) bitwuzla::parser::Parser::Parser (C++ function) bitwuzla::parser::Parser::~Parser (C++ function) bitwuzla::Result (C++ enum) bitwuzla::Result::SAT (C++ enumerator) bitwuzla::Result::UNKNOWN (C++ enumerator) bitwuzla::Result::UNSAT (C++ enumerator) bitwuzla::RoundingMode (C++ enum) bitwuzla::RoundingMode::RNA (C++ enumerator) bitwuzla::RoundingMode::RNE (C++ enumerator) bitwuzla::RoundingMode::RTN (C++ enumerator) bitwuzla::RoundingMode::RTP (C++ enumerator) bitwuzla::RoundingMode::RTZ (C++ enumerator) bitwuzla::Sort (C++ class) bitwuzla::Sort::array_element (C++ function) bitwuzla::Sort::array_index (C++ function) bitwuzla::Sort::bv_size (C++ function) bitwuzla::Sort::fp_exp_size (C++ function) bitwuzla::Sort::fp_sig_size (C++ function) bitwuzla::Sort::fun_arity (C++ function) bitwuzla::Sort::fun_codomain (C++ function) bitwuzla::Sort::fun_domain (C++ function) bitwuzla::Sort::id (C++ function) bitwuzla::Sort::is_array (C++ function) bitwuzla::Sort::is_bool (C++ function) bitwuzla::Sort::is_bv (C++ function) bitwuzla::Sort::is_fp (C++ function) bitwuzla::Sort::is_fun (C++ function) bitwuzla::Sort::is_null (C++ function) bitwuzla::Sort::is_rm (C++ function) bitwuzla::Sort::is_uninterpreted (C++ function) bitwuzla::Sort::Sort (C++ function) bitwuzla::Sort::str (C++ function) bitwuzla::Sort::uninterpreted_symbol (C++ function) bitwuzla::Sort::~Sort (C++ function) bitwuzla::Term (C++ class) bitwuzla::Term::children (C++ function) bitwuzla::Term::id (C++ function) bitwuzla::Term::indices (C++ function) bitwuzla::Term::is_bv_value_max_signed (C++ function) bitwuzla::Term::is_bv_value_min_signed (C++ function) bitwuzla::Term::is_bv_value_one (C++ function) bitwuzla::Term::is_bv_value_ones (C++ function) bitwuzla::Term::is_bv_value_zero (C++ function) bitwuzla::Term::is_const (C++ function) bitwuzla::Term::is_false (C++ function) bitwuzla::Term::is_fp_value_nan (C++ function) bitwuzla::Term::is_fp_value_neg_inf (C++ function) bitwuzla::Term::is_fp_value_neg_zero (C++ function) bitwuzla::Term::is_fp_value_pos_inf (C++ function) bitwuzla::Term::is_fp_value_pos_zero (C++ function) bitwuzla::Term::is_null (C++ function) bitwuzla::Term::is_rm_value_rna (C++ function) bitwuzla::Term::is_rm_value_rne (C++ function) bitwuzla::Term::is_rm_value_rtn (C++ function) bitwuzla::Term::is_rm_value_rtp (C++ function) bitwuzla::Term::is_rm_value_rtz (C++ function) bitwuzla::Term::is_true (C++ function) bitwuzla::Term::is_value (C++ function) bitwuzla::Term::is_variable (C++ function) bitwuzla::Term::kind (C++ function) bitwuzla::Term::num_children (C++ function) bitwuzla::Term::num_indices (C++ function) bitwuzla::Term::operator[] (C++ function) bitwuzla::Term::sort (C++ function) bitwuzla::Term::str (C++ function) bitwuzla::Term::symbol (C++ function) bitwuzla::Term::Term (C++ function) bitwuzla::Term::value (C++ function) bitwuzla::Term::~Term (C++ function) bitwuzla::Terminator (C++ class) bitwuzla::Terminator::terminate (C++ function) bitwuzla::Terminator::~Terminator (C++ function) bitwuzla::TermManager (C++ class) bitwuzla::TermManager::mk_bv_max_signed (C++ function) bitwuzla::TermManager::mk_bv_min_signed (C++ function) bitwuzla::TermManager::mk_bv_one (C++ function) bitwuzla::TermManager::mk_bv_ones (C++ function) bitwuzla::TermManager::mk_bv_value (C++ function) bitwuzla::TermManager::mk_bv_value_int64 (C++ function) bitwuzla::TermManager::mk_bv_value_uint64 (C++ function) bitwuzla::TermManager::mk_bv_zero (C++ function) bitwuzla::TermManager::mk_const (C++ function) bitwuzla::TermManager::mk_const_array (C++ function) bitwuzla::TermManager::mk_false (C++ function) bitwuzla::TermManager::mk_fp_nan (C++ function) bitwuzla::TermManager::mk_fp_neg_inf (C++ function) bitwuzla::TermManager::mk_fp_neg_zero (C++ function) bitwuzla::TermManager::mk_fp_pos_inf (C++ function) bitwuzla::TermManager::mk_fp_pos_zero (C++ function) bitwuzla::TermManager::mk_fp_value (C++ function), [1], [2] bitwuzla::TermManager::mk_rm_value (C++ function) bitwuzla::TermManager::mk_term (C++ function) bitwuzla::TermManager::mk_true (C++ function) bitwuzla::TermManager::mk_var (C++ function) bitwuzla::TermManager::operator= (C++ function) bitwuzla::TermManager::substitute_term (C++ function) bitwuzla::TermManager::substitute_terms (C++ function) bitwuzla::TermManager::TermManager (C++ function) bitwuzla_assert (C++ function) bitwuzla_check_sat (C++ function) bitwuzla_check_sat_assuming (C++ function) bitwuzla_copyright (C++ function) bitwuzla_delete (C++ function) bitwuzla_get_assertions (C++ function) bitwuzla_get_option (C++ function) bitwuzla_get_option_info (C++ function) bitwuzla_get_option_mode (C++ function) bitwuzla_get_statistics (C++ function) bitwuzla_get_term_mgr (C++ function) bitwuzla_get_termination_callback_state (C++ function) bitwuzla_get_unsat_assumptions (C++ function) bitwuzla_get_unsat_core (C++ function) bitwuzla_get_value (C++ function) bitwuzla_git_id (C++ function) bitwuzla_is_unsat_assumption (C++ function) bitwuzla_kind_to_string (C++ function) bitwuzla_mk_array_sort (C++ function) bitwuzla_mk_bool_sort (C++ function) bitwuzla_mk_bv_max_signed (C++ function) bitwuzla_mk_bv_min_signed (C++ function) bitwuzla_mk_bv_one (C++ function) bitwuzla_mk_bv_ones (C++ function) bitwuzla_mk_bv_sort (C++ function) bitwuzla_mk_bv_value (C++ function) bitwuzla_mk_bv_value_int64 (C++ function) bitwuzla_mk_bv_value_uint64 (C++ function) bitwuzla_mk_bv_zero (C++ function) bitwuzla_mk_const (C++ function) bitwuzla_mk_const_array (C++ function) bitwuzla_mk_false (C++ function) bitwuzla_mk_fp_from_rational (C++ function) bitwuzla_mk_fp_from_real (C++ function) bitwuzla_mk_fp_nan (C++ function) bitwuzla_mk_fp_neg_inf (C++ function) bitwuzla_mk_fp_neg_zero (C++ function)

bitwuzla_mk_fp_pos_inf (C++ function) bitwuzla_mk_fp_pos_zero (C++ function) bitwuzla_mk_fp_sort (C++ function) bitwuzla_mk_fp_value (C++ function) bitwuzla_mk_fun_sort (C++ function) bitwuzla_mk_rm_sort (C++ function) bitwuzla_mk_rm_value (C++ function) bitwuzla_mk_term (C++ function) bitwuzla_mk_term1 (C++ function) bitwuzla_mk_term1_indexed1 (C++ function) bitwuzla_mk_term1_indexed2 (C++ function) bitwuzla_mk_term2 (C++ function) bitwuzla_mk_term2_indexed1 (C++ function) bitwuzla_mk_term2_indexed2 (C++ function) bitwuzla_mk_term3 (C++ function) bitwuzla_mk_term_indexed (C++ function) bitwuzla_mk_true (C++ function) bitwuzla_mk_uninterpreted_sort (C++ function) bitwuzla_mk_var (C++ function) bitwuzla_new (C++ function) bitwuzla_option_is_mode (C++ function) bitwuzla_option_is_numeric (C++ function) bitwuzla_option_is_valid (C++ function) bitwuzla_options_delete (C++ function) bitwuzla_options_new (C++ function) bitwuzla_parser_delete (C++ function) bitwuzla_parser_get_bitwuzla (C++ function) bitwuzla_parser_get_error_msg (C++ function) bitwuzla_parser_new (C++ function) bitwuzla_parser_parse (C++ function) bitwuzla_parser_parse_sort (C++ function) bitwuzla_parser_parse_term (C++ function) bitwuzla_pop (C++ function) bitwuzla_print_formula (C++ function) bitwuzla_push (C++ function) bitwuzla_result_to_string (C++ function) bitwuzla_rm_to_string (C++ function) bitwuzla_set_abort_callback (C++ function) bitwuzla_set_option (C++ function) bitwuzla_set_option_mode (C++ function) bitwuzla_set_termination_callback (C++ function) bitwuzla_simplify (C++ function) bitwuzla_sort_array_get_element (C++ function) bitwuzla_sort_array_get_index (C++ function) bitwuzla_sort_bv_get_size (C++ function) bitwuzla_sort_copy (C++ function) bitwuzla_sort_fp_get_exp_size (C++ function) bitwuzla_sort_fp_get_sig_size (C++ function) bitwuzla_sort_fun_get_arity (C++ function) bitwuzla_sort_fun_get_codomain (C++ function) bitwuzla_sort_fun_get_domain_sorts (C++ function) bitwuzla_sort_get_uninterpreted_symbol (C++ function) bitwuzla_sort_hash (C++ function) bitwuzla_sort_is_array (C++ function) bitwuzla_sort_is_bool (C++ function) bitwuzla_sort_is_bv (C++ function) bitwuzla_sort_is_fp (C++ function) bitwuzla_sort_is_fun (C++ function) bitwuzla_sort_is_rm (C++ function) bitwuzla_sort_is_uninterpreted (C++ function) bitwuzla_sort_print (C++ function) bitwuzla_sort_release (C++ function) bitwuzla_sort_to_string (C++ function) bitwuzla_substitute_term (C++ function) bitwuzla_substitute_terms (C++ function) bitwuzla_term_array_get_element_sort (C++ function) bitwuzla_term_array_get_index_sort (C++ function) bitwuzla_term_bv_get_size (C++ function) bitwuzla_term_copy (C++ function) bitwuzla_term_fp_get_exp_size (C++ function) bitwuzla_term_fp_get_sig_size (C++ function) bitwuzla_term_fun_get_arity (C++ function) bitwuzla_term_fun_get_codomain_sort (C++ function) bitwuzla_term_fun_get_domain_sorts (C++ function) bitwuzla_term_get_children (C++ function) bitwuzla_term_get_indices (C++ function) bitwuzla_term_get_kind (C++ function) bitwuzla_term_get_sort (C++ function) bitwuzla_term_get_symbol (C++ function) bitwuzla_term_hash (C++ function) bitwuzla_term_is_array (C++ function) bitwuzla_term_is_bool (C++ function) bitwuzla_term_is_bv (C++ function) bitwuzla_term_is_bv_value (C++ function) bitwuzla_term_is_bv_value_max_signed (C++ function) bitwuzla_term_is_bv_value_min_signed (C++ function) bitwuzla_term_is_bv_value_one (C++ function) bitwuzla_term_is_bv_value_ones (C++ function) bitwuzla_term_is_bv_value_zero (C++ function) bitwuzla_term_is_const (C++ function) bitwuzla_term_is_equal_sort (C++ function) bitwuzla_term_is_false (C++ function) bitwuzla_term_is_fp (C++ function) bitwuzla_term_is_fp_value (C++ function) bitwuzla_term_is_fp_value_nan (C++ function) bitwuzla_term_is_fp_value_neg_inf (C++ function) bitwuzla_term_is_fp_value_neg_zero (C++ function) bitwuzla_term_is_fp_value_pos_inf (C++ function) bitwuzla_term_is_fp_value_pos_zero (C++ function) bitwuzla_term_is_fun (C++ function) bitwuzla_term_is_indexed (C++ function) bitwuzla_term_is_rm (C++ function) bitwuzla_term_is_rm_value (C++ function) bitwuzla_term_is_rm_value_rna (C++ function) bitwuzla_term_is_rm_value_rne (C++ function) bitwuzla_term_is_rm_value_rtn (C++ function) bitwuzla_term_is_rm_value_rtp (C++ function) bitwuzla_term_is_rm_value_rtz (C++ function) bitwuzla_term_is_true (C++ function) bitwuzla_term_is_uninterpreted (C++ function) bitwuzla_term_is_value (C++ function) bitwuzla_term_is_var (C++ function) bitwuzla_term_manager_delete (C++ function) bitwuzla_term_manager_new (C++ function) bitwuzla_term_manager_release (C++ function) bitwuzla_term_print (C++ function) bitwuzla_term_print_fmt (C++ function) bitwuzla_term_release (C++ function) bitwuzla_term_to_string (C++ function) bitwuzla_term_to_string_fmt (C++ function) bitwuzla_term_value_get_bool (C++ function) bitwuzla_term_value_get_fp_ieee (C++ function) bitwuzla_term_value_get_rm (C++ function) bitwuzla_term_value_get_str (C++ function) bitwuzla_term_value_get_str_fmt (C++ function) bitwuzla_version (C++ function) BitwuzlaKind (C++ enum) BitwuzlaKind::BITWUZLA_KIND_AND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_APPLY (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_ARRAY_SELECT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_ARRAY_STORE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ADD (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_AND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ASHR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_COMP (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_CONCAT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_DEC (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_EXTRACT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_INC (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_MUL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_NAND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_NEG (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_NEG_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_NOR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_NOT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_OR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_REDAND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_REDOR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_REDXOR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_REPEAT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ROL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ROLI (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ROR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_RORI (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SADD_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SDIV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SDIV_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SGE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SGT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SHL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SHR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SIGN_EXTEND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SLE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SLT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SMOD (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SMUL_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SREM (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SSUB_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_SUB (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UADD_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UDIV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UGE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UGT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ULE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ULT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UMUL_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_UREM (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_USUB_OVERFLOW (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_XNOR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_XOR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_BV_ZERO_EXTEND (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_CONST_ARRAY (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_CONSTANT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_DISTINCT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_EQUAL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_EXISTS (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FORALL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_ABS (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_ADD (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_DIV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_EQUAL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_FMA (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_FP (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_GEQ (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_GT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_INF (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_NAN (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_NEG (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_NORMAL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_POS (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_SUBNORMAL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_IS_ZERO (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_LEQ (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_LT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_MAX (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_MIN (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_MUL (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_NEG (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_REM (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_RTI (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_SQRT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_SUB (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_FP_FROM_BV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_FP_FROM_FP (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_FP_FROM_SBV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_FP_FROM_UBV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_SBV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_FP_TO_UBV (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_IFF (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_IMPLIES (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_ITE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_LAMBDA (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_NOT (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_OR (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_VALUE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_VARIABLE (C++ enumerator) BitwuzlaKind::BITWUZLA_KIND_XOR (C++ enumerator) BitwuzlaOption (C++ enum) BitwuzlaOption::BITWUZLA_OPT_BV_SOLVER (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_DBG_CHECK_MODEL (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_DBG_CHECK_UNSAT_CORE (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_DBG_PP_NODE_THRESH (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_DBG_RW_NODE_THRESH (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_LOGLEVEL (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_MEMORY_LIMIT (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_CONTRADICTING_ANDS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_ELIM_BV_EXTRACTS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_EMBEDDED_CONSTR (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_FLATTEN_AND (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_NORMALIZE (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_NORMALIZE_SHARE_AWARE (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_SKELETON_PREPROC (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_VARIABLE_SUBST (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_BV_INEQ (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_DISEQ (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_EQ (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PREPROCESS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PRODUCE_MODELS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PRODUCE_UNSAT_CORES (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_CONST_BITS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_INFER_INEQ_BOUNDS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_NORMALIZE (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_NPROPS (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_NUPDATES (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_OPT_LT_CONCAT_SEXT (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_PATH_SEL (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_PROB_RANDOM_INPUT (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_PROB_USE_INV_VALUE (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_PROP_SEXT (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_REWRITE_LEVEL (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_SAT_SOLVER (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_SEED (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_TIME_LIMIT_PER (C++ enumerator) BitwuzlaOption::BITWUZLA_OPT_VERBOSITY (C++ enumerator) BitwuzlaOptionInfo (C++ struct) BitwuzlaOptionInfo::description (C++ member) BitwuzlaOptionInfo::is_numeric (C++ member) BitwuzlaOptionInfo::lng (C++ member) BitwuzlaOptionInfo::ModeValue (C++ struct) BitwuzlaOptionInfo::ModeValue::cur (C++ member) BitwuzlaOptionInfo::ModeValue::dflt (C++ member) BitwuzlaOptionInfo::ModeValue::modes (C++ member) BitwuzlaOptionInfo::ModeValue::num_modes (C++ member) BitwuzlaOptionInfo::NumericValue (C++ struct) BitwuzlaOptionInfo::NumericValue::cur (C++ member) BitwuzlaOptionInfo::NumericValue::dflt (C++ member) BitwuzlaOptionInfo::NumericValue::max (C++ member) BitwuzlaOptionInfo::NumericValue::min (C++ member) BitwuzlaOptionInfo::opt (C++ member) BitwuzlaOptionInfo::shrt (C++ member) BitwuzlaOptions (C++ type) BitwuzlaParser (C++ type) BitwuzlaResult (C++ enum) BitwuzlaResult::BITWUZLA_SAT (C++ enumerator) BitwuzlaResult::BITWUZLA_UNKNOWN (C++ enumerator) BitwuzlaResult::BITWUZLA_UNSAT (C++ enumerator) BitwuzlaRoundingMode (C++ enum) BitwuzlaRoundingMode::BITWUZLA_RM_RNA (C++ enumerator) BitwuzlaRoundingMode::BITWUZLA_RM_RNE (C++ enumerator) BitwuzlaRoundingMode::BITWUZLA_RM_RTN (C++ enumerator) BitwuzlaRoundingMode::BITWUZLA_RM_RTP (C++ enumerator) BitwuzlaRoundingMode::BITWUZLA_RM_RTZ (C++ enumerator) BitwuzlaSort (C++ type) BitwuzlaTerm (C++ type) BitwuzlaTermManager (C++ type) BOOL (bitwuzla.OptionInfoKind attribute) BV_ADD (bitwuzla.Kind attribute) BV_AND (bitwuzla.Kind attribute) BV_ASHR (bitwuzla.Kind attribute) BV_COMP (bitwuzla.Kind attribute) BV_CONCAT (bitwuzla.Kind attribute) BV_DEC (bitwuzla.Kind attribute) BV_EXTRACT (bitwuzla.Kind attribute) BV_INC (bitwuzla.Kind attribute) BV_MUL (bitwuzla.Kind attribute) BV_NAND (bitwuzla.Kind attribute) BV_NEG (bitwuzla.Kind attribute) BV_NEG_OVERFLOW (bitwuzla.Kind attribute) BV_NOR (bitwuzla.Kind attribute) BV_NOT (bitwuzla.Kind attribute) BV_OR (bitwuzla.Kind attribute) BV_REDAND (bitwuzla.Kind attribute) BV_REDOR (bitwuzla.Kind attribute) BV_REDXOR (bitwuzla.Kind attribute) BV_REPEAT (bitwuzla.Kind attribute) BV_ROL (bitwuzla.Kind attribute) BV_ROLI (bitwuzla.Kind attribute) BV_ROR (bitwuzla.Kind attribute) BV_RORI (bitwuzla.Kind attribute) BV_SADD_OVERFLOW (bitwuzla.Kind attribute) BV_SDIV (bitwuzla.Kind attribute) BV_SDIV_OVERFLOW (bitwuzla.Kind attribute) BV_SGE (bitwuzla.Kind attribute) BV_SGT (bitwuzla.Kind attribute) BV_SHL (bitwuzla.Kind attribute) BV_SHR (bitwuzla.Kind attribute) BV_SIGN_EXTEND (bitwuzla.Kind attribute) bv_size() (bitwuzla.Sort method) BV_SLE (bitwuzla.Kind attribute) BV_SLT (bitwuzla.Kind attribute) BV_SMOD (bitwuzla.Kind attribute) BV_SMUL_OVERFLOW (bitwuzla.Kind attribute) BV_SOLVER (bitwuzla.Option attribute) BV_SREM (bitwuzla.Kind attribute) BV_SSUB_OVERFLOW (bitwuzla.Kind attribute) BV_SUB (bitwuzla.Kind attribute) BV_UADD_OVERFLOW (bitwuzla.Kind attribute) BV_UDIV (bitwuzla.Kind attribute) BV_UGE (bitwuzla.Kind attribute) BV_UGT (bitwuzla.Kind attribute) BV_ULE (bitwuzla.Kind attribute) BV_ULT (bitwuzla.Kind attribute) BV_UMUL_OVERFLOW (bitwuzla.Kind attribute) BV_UREM (bitwuzla.Kind attribute) BV_USUB_OVERFLOW (bitwuzla.Kind attribute) BV_XNOR (bitwuzla.Kind attribute) BV_XOR (bitwuzla.Kind attribute) BV_ZERO_EXTEND (bitwuzla.Kind attribute)

C

check_sat() (bitwuzla.Bitwuzla method) children() (bitwuzla.Term method) configure_terminator() (bitwuzla.Bitwuzla method)

CONST_ARRAY (bitwuzla.Kind attribute) CONSTANT (bitwuzla.Kind attribute) copyright (C++ function) cur() (bitwuzla.OptionInfo method)

D

DBG_CHECK_MODEL (bitwuzla.Option attribute) DBG_CHECK_UNSAT_CORE (bitwuzla.Option attribute) DBG_PP_NODE_THRESH (bitwuzla.Option attribute) DBG_RW_NODE_THRESH (bitwuzla.Option attribute)

description() (bitwuzla.OptionInfo method) (bitwuzla.Options method) dflt() (bitwuzla.OptionInfo method) DISTINCT (bitwuzla.Kind attribute)

E

EQUAL (bitwuzla.Kind attribute)

EXISTS (bitwuzla.Kind attribute)

F

FORALL (bitwuzla.Kind attribute) FP_ABS (bitwuzla.Kind attribute) FP_ADD (bitwuzla.Kind attribute) FP_DIV (bitwuzla.Kind attribute) FP_EQUAL (bitwuzla.Kind attribute) fp_exp_size() (bitwuzla.Sort method) FP_FMA (bitwuzla.Kind attribute) FP_FP (bitwuzla.Kind attribute) FP_GEQ (bitwuzla.Kind attribute) FP_GT (bitwuzla.Kind attribute) FP_IS_INF (bitwuzla.Kind attribute) FP_IS_NAN (bitwuzla.Kind attribute) FP_IS_NEG (bitwuzla.Kind attribute) FP_IS_NORMAL (bitwuzla.Kind attribute) FP_IS_POS (bitwuzla.Kind attribute) FP_IS_SUBNORMAL (bitwuzla.Kind attribute) FP_IS_ZERO (bitwuzla.Kind attribute) FP_LEQ (bitwuzla.Kind attribute)

FP_LT (bitwuzla.Kind attribute) FP_MAX (bitwuzla.Kind attribute) FP_MIN (bitwuzla.Kind attribute) FP_MUL (bitwuzla.Kind attribute) FP_NEG (bitwuzla.Kind attribute) FP_REM (bitwuzla.Kind attribute) FP_RTI (bitwuzla.Kind attribute) fp_sig_size() (bitwuzla.Sort method) FP_SQRT (bitwuzla.Kind attribute) FP_SUB (bitwuzla.Kind attribute) FP_TO_FP_FROM_BV (bitwuzla.Kind attribute) FP_TO_FP_FROM_FP (bitwuzla.Kind attribute) FP_TO_FP_FROM_SBV (bitwuzla.Kind attribute) FP_TO_FP_FROM_UBV (bitwuzla.Kind attribute) FP_TO_SBV (bitwuzla.Kind attribute) FP_TO_UBV (bitwuzla.Kind attribute) fun_arity() (bitwuzla.Sort method) fun_codomain() (bitwuzla.Sort method) fun_domain() (bitwuzla.Sort method)

G

get() (bitwuzla.Options method) get_assertions() (bitwuzla.Bitwuzla method) get_unsat_assumptions() (bitwuzla.Bitwuzla method)

get_unsat_core() (bitwuzla.Bitwuzla method) get_value() (bitwuzla.Bitwuzla method) git_id (C++ function)

I

id() (bitwuzla.Sort method) (bitwuzla.Term method) IFF (bitwuzla.Kind attribute) IMPLIES (bitwuzla.Kind attribute) indices() (bitwuzla.Term method) is_array() (bitwuzla.Sort method) is_bool() (bitwuzla.Options method) (bitwuzla.Sort method) is_bv() (bitwuzla.Sort method) is_bv_value_max_signed() (bitwuzla.Term method) is_bv_value_min_signed() (bitwuzla.Term method) is_bv_value_one() (bitwuzla.Term method) is_bv_value_ones() (bitwuzla.Term method) is_bv_value_zero() (bitwuzla.Term method) is_const() (bitwuzla.Term method) is_false() (bitwuzla.Term method) is_fp() (bitwuzla.Sort method) is_fp_value_nan() (bitwuzla.Term method) is_fp_value_neg_inf() (bitwuzla.Term method) is_fp_value_neg_zero() (bitwuzla.Term method)

is_fp_value_pos_inf() (bitwuzla.Term method) is_fp_value_pos_zero() (bitwuzla.Term method) is_fun() (bitwuzla.Sort method) is_mode() (bitwuzla.Options method) is_null() (bitwuzla.Sort method) (bitwuzla.Term method) is_numeric() (bitwuzla.Options method) is_rm() (bitwuzla.Sort method) is_rm_value_rna() (bitwuzla.Term method) is_rm_value_rne() (bitwuzla.Term method) is_rm_value_rtn() (bitwuzla.Term method) is_rm_value_rtp() (bitwuzla.Term method) is_rm_value_rtz() (bitwuzla.Term method) is_true() (bitwuzla.Term method) is_uninterpreted() (bitwuzla.Sort method) is_unsat_assumption() (bitwuzla.Bitwuzla method) is_valid() (bitwuzla.Options method) is_value() (bitwuzla.Term method) is_variable() (bitwuzla.Term method) ITE (bitwuzla.Kind attribute)

K

Kind (class in bitwuzla)

kind() (bitwuzla.OptionInfo method) (bitwuzla.Term method)

L

LAMBDA (bitwuzla.Kind attribute) lng() (bitwuzla.OptionInfo method) (bitwuzla.Options method)

LOGLEVEL (bitwuzla.Option attribute)

M

max() (bitwuzla.OptionInfo method) MEMORY_LIMIT (bitwuzla.Option attribute) min() (bitwuzla.OptionInfo method) mk_array_sort() (bitwuzla.TermManager method) mk_bool_sort() (bitwuzla.TermManager method) mk_bv_max_signed() (bitwuzla.TermManager method) mk_bv_min_signed() (bitwuzla.TermManager method) mk_bv_one() (bitwuzla.TermManager method) mk_bv_ones() (bitwuzla.TermManager method) mk_bv_sort() (bitwuzla.TermManager method) mk_bv_value() (bitwuzla.TermManager method) mk_bv_zero() (bitwuzla.TermManager method) mk_const() (bitwuzla.TermManager method) mk_const_array() (bitwuzla.TermManager method) mk_false() (bitwuzla.TermManager method) mk_fp_nan() (bitwuzla.TermManager method)

mk_fp_neg_inf() (bitwuzla.TermManager method) mk_fp_neg_zero() (bitwuzla.TermManager method) mk_fp_pos_inf() (bitwuzla.TermManager method) mk_fp_pos_zero() (bitwuzla.TermManager method) mk_fp_sort() (bitwuzla.TermManager method) mk_fp_value() (bitwuzla.TermManager method) mk_fun_sort() (bitwuzla.TermManager method) mk_rm_sort() (bitwuzla.TermManager method) mk_rm_value() (bitwuzla.TermManager method) mk_term() (bitwuzla.TermManager method) mk_true() (bitwuzla.TermManager method) mk_uninterpreted_sort() (bitwuzla.TermManager method) mk_var() (bitwuzla.TermManager method) MODE (bitwuzla.OptionInfoKind attribute) modes() (bitwuzla.OptionInfo method) (bitwuzla.Options method)

N

NOT (bitwuzla.Kind attribute) num_children() (bitwuzla.Term method)

num_indices() (bitwuzla.Term method) NUMERIC (bitwuzla.OptionInfoKind attribute)

O

Option (class in bitwuzla) option() (bitwuzla.Options method) OptionInfo (class in bitwuzla)

OptionInfoKind (class in bitwuzla) Options (class in bitwuzla) OR (bitwuzla.Kind attribute)

P

parse() (bitwuzla.Parser method) parse_sort() (bitwuzla.Parser method) parse_term() (bitwuzla.Parser method) Parser (class in bitwuzla) pop() (bitwuzla.Bitwuzla method) PP_CONTRADICTING_ANDS (bitwuzla.Option attribute) PP_ELIM_BV_EXTRACTS (bitwuzla.Option attribute) PP_EMBEDDED_CONSTR (bitwuzla.Option attribute) PP_FLATTEN_AND (bitwuzla.Option attribute) PP_NORMALIZE (bitwuzla.Option attribute) PP_NORMALIZE_SHARE_AWARE (bitwuzla.Option attribute) PP_SKELETON_PREPROC (bitwuzla.Option attribute) PP_VARIABLE_SUBST (bitwuzla.Option attribute) PP_VARIABLE_SUBST_NORM_BV_INEQ (bitwuzla.Option attribute) PP_VARIABLE_SUBST_NORM_DISEQ (bitwuzla.Option attribute) PP_VARIABLE_SUBST_NORM_EQ (bitwuzla.Option attribute)

PREPROCESS (bitwuzla.Option attribute) print_formula() (bitwuzla.Bitwuzla method) PRODUCE_MODELS (bitwuzla.Option attribute) PRODUCE_UNSAT_ASSUMPTIONS (bitwuzla.Option attribute) PRODUCE_UNSAT_CORES (bitwuzla.Option attribute) PROP_CONST_BITS (bitwuzla.Option attribute) PROP_INFER_INEQ_BOUNDS (bitwuzla.Option attribute) PROP_NORMALIZE (bitwuzla.Option attribute) PROP_NPROPS (bitwuzla.Option attribute) PROP_NUPDATES (bitwuzla.Option attribute) PROP_OPT_LT_CONCAT_SEXT (bitwuzla.Option attribute) PROP_PATH_SEL (bitwuzla.Option attribute) PROP_PROB_RANDOM_INPUT (bitwuzla.Option attribute) PROP_PROB_USE_INV_VALUE (bitwuzla.Option attribute) PROP_SEXT (bitwuzla.Option attribute) push() (bitwuzla.Bitwuzla method)

R

Result (class in bitwuzla) REWRITE_LEVEL (bitwuzla.Option attribute) RNA (bitwuzla.RoundingMode attribute) RNE (bitwuzla.RoundingMode attribute)

RoundingMode (class in bitwuzla) RTN (bitwuzla.RoundingMode attribute) RTP (bitwuzla.RoundingMode attribute) RTZ (bitwuzla.RoundingMode attribute)

S

SAT (bitwuzla.Result attribute) SAT_SOLVER (bitwuzla.Option attribute) SEED (bitwuzla.Option attribute) set() (bitwuzla.Options method) set_args() (bitwuzla.Options method) shrt() (bitwuzla.OptionInfo method) (bitwuzla.Options method) simplify() (bitwuzla.Bitwuzla method) Sort (class in bitwuzla) sort() (bitwuzla.Term method)

statistics() (bitwuzla.Bitwuzla method) std::hash<bitwuzla::Sort> (C++ struct) std::hash<bitwuzla::Sort>::operator() (C++ function) std::hash<bitwuzla::Term> (C++ struct) std::hash<bitwuzla::Term>::operator() (C++ function) std::to_string (C++ function), [1], [2] str() (bitwuzla.Term method) substitute_term() (bitwuzla.TermManager method) substitute_terms() (bitwuzla.TermManager method) symbol() (bitwuzla.Term method)

T

Term (class in bitwuzla) term_mgr() (bitwuzla.Bitwuzla method)

TermManager (class in bitwuzla) TIME_LIMIT_PER (bitwuzla.Option attribute)

U

uninterpreted_symbol() (bitwuzla.Sort method)

UNKNOWN (bitwuzla.Result attribute) UNSAT (bitwuzla.Result attribute)

V

VALUE (bitwuzla.Kind attribute) value() (bitwuzla.Term method)

VARIABLE (bitwuzla.Kind attribute) VERBOSITY (bitwuzla.Option attribute) version (C++ function)

X

XOR (bitwuzla.Kind attribute)