Bitwuzla
0.7.0
Installation and Build Instructions
Command Line Interface
API Documentation
References
Bitwuzla
Index
Index
B
|
C
|
G
|
S
|
V
B
Bitwuzla (C++ type)
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::print_unsat_core (C++ function)
bitwuzla::Bitwuzla::push (C++ function)
bitwuzla::Bitwuzla::simplify (C++ function)
,
[1]
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::ABSTRACTION (C++ enumerator)
bitwuzla::Option::ABSTRACTION_ASSERT (C++ enumerator)
bitwuzla::Option::ABSTRACTION_ASSERT_REFS (C++ enumerator)
bitwuzla::Option::ABSTRACTION_BV_ADD (C++ enumerator)
bitwuzla::Option::ABSTRACTION_BV_MUL (C++ enumerator)
bitwuzla::Option::ABSTRACTION_BV_SIZE (C++ enumerator)
bitwuzla::Option::ABSTRACTION_BV_UDIV (C++ enumerator)
bitwuzla::Option::ABSTRACTION_BV_UREM (C++ enumerator)
bitwuzla::Option::ABSTRACTION_EAGER_REFINE (C++ enumerator)
bitwuzla::Option::ABSTRACTION_EQUAL (C++ enumerator)
bitwuzla::Option::ABSTRACTION_INC_BITBLAST (C++ enumerator)
bitwuzla::Option::ABSTRACTION_INITIAL_LEMMAS (C++ enumerator)
bitwuzla::Option::ABSTRACTION_ITE (C++ enumerator)
bitwuzla::Option::ABSTRACTION_VALUE_LIMIT (C++ enumerator)
bitwuzla::Option::ABSTRACTION_VALUE_ONLY (C++ enumerator)
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::Exception (C++ class)
bitwuzla::option::Exception::Exception (C++ function)
,
[1]
bitwuzla::Option::LOGLEVEL (C++ enumerator)
bitwuzla::Option::MEMORY_LIMIT (C++ enumerator)
bitwuzla::Option::NTHREADS (C++ enumerator)
bitwuzla::Option::PP_CONTRADICTING_ANDS (C++ enumerator)
bitwuzla::Option::PP_ELIM_BV_EXTRACTS (C++ enumerator)
bitwuzla::Option::PP_ELIM_BV_UDIV (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_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::RELEVANT_TERMS (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::Exception (C++ class)
bitwuzla::parser::Exception::Exception (C++ function)
,
[1]
bitwuzla::parser::Parser (C++ class)
bitwuzla::parser::Parser::bitwuzla (C++ function)
bitwuzla::parser::Parser::configure_auto_print_model (C++ function)
bitwuzla::parser::Parser::get_declared_funs (C++ function)
bitwuzla::parser::Parser::get_declared_sorts (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_configure_auto_print_model (C++ function)
bitwuzla_parser_delete (C++ function)
bitwuzla_parser_get_bitwuzla (C++ function)
bitwuzla_parser_get_declared_funs (C++ function)
bitwuzla_parser_get_declared_sorts (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_print_unsat_core (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_simplify_term (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_ABSTRACTION (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_ASSERT (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_ASSERT_REFS (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_BV_ADD (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_BV_MUL (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_BV_SIZE (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_BV_UDIV (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_BV_UREM (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_EAGER_REFINE (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_EQUAL (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_INC_BITBLAST (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_INITIAL_LEMMAS (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_ITE (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_VALUE_LIMIT (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_ABSTRACTION_VALUE_ONLY (C++ enumerator)
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_NTHREADS (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_PP_CONTRADICTING_ANDS (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_PP_ELIM_BV_EXTRACTS (C++ enumerator)
BitwuzlaOption::BITWUZLA_OPT_PP_ELIM_BV_UDIV (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_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_RELEVANT_TERMS (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)
C
copyright (C++ function)
G
git_id (C++ function)
S
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]
V
version (C++ function)