Index

A

AbsSort (C++ class) AbsSort::d_associated_sort (C++ member) AbsSort::d_dt_ctors (C++ member) AbsSort::d_dt_is_instantiated (C++ member) AbsSort::d_id (C++ member) AbsSort::d_kind (C++ member) AbsSort::d_sorts (C++ member) AbsSort::DatatypeConstructorMap (C++ type) AbsSort::equals (C++ function) AbsSort::get_array_element_sort (C++ function) AbsSort::get_array_index_sort (C++ function) AbsSort::get_associated_sort (C++ function) AbsSort::get_bag_element_sort (C++ function) AbsSort::get_bv_size (C++ function) AbsSort::get_dt_cons_names (C++ function) AbsSort::get_dt_cons_num_sels (C++ function) AbsSort::get_dt_cons_sel_names (C++ function) AbsSort::get_dt_ctor_names (C++ function) AbsSort::get_dt_ctors (C++ function) AbsSort::get_dt_name (C++ function) AbsSort::get_dt_num_cons (C++ function) AbsSort::get_dt_sel_names (C++ function) AbsSort::get_dt_sel_sort (C++ function) AbsSort::get_ff_size (C++ function) AbsSort::get_fp_exp_size (C++ function) AbsSort::get_fp_sig_size (C++ function) AbsSort::get_fun_arity (C++ function) AbsSort::get_fun_codomain_sort (C++ function) AbsSort::get_fun_domain_sorts (C++ function) AbsSort::get_id (C++ function) AbsSort::get_kind (C++ function) AbsSort::get_seq_element_sort (C++ function) AbsSort::get_set_element_sort (C++ function) AbsSort::get_sorts (C++ function) AbsSort::hash (C++ function) AbsSort::instantiate_dt_param_sort (C++ function) AbsSort::is_array (C++ function) AbsSort::is_bag (C++ function) AbsSort::is_bool (C++ function) AbsSort::is_bv (C++ function) AbsSort::is_dt (C++ function) AbsSort::is_dt_instantiated (C++ function) AbsSort::is_dt_parametric (C++ function) AbsSort::is_dt_well_founded (C++ function) AbsSort::is_ff (C++ function) AbsSort::is_fp (C++ function) AbsSort::is_fun (C++ function) AbsSort::is_int (C++ function) AbsSort::is_param_sort (C++ function) AbsSort::is_real (C++ function) AbsSort::is_reglan (C++ function) AbsSort::is_rm (C++ function) AbsSort::is_seq (C++ function) AbsSort::is_set (C++ function) AbsSort::is_string (C++ function) AbsSort::is_uninterpreted (C++ function) AbsSort::is_unresolved_sort (C++ function) AbsSort::not_equals (C++ function) AbsSort::set_associated_sort (C++ function) AbsSort::set_dt_ctors (C++ function) AbsSort::set_dt_is_instantiated (C++ function) AbsSort::set_id (C++ function) AbsSort::set_kind (C++ function) AbsSort::set_sorts (C++ function) AbsSort::to_string (C++ function) AbsSort::~AbsSort (C++ function) AbsTerm (C++ class) AbsTerm::AbsTerm (C++ function) AbsTerm::equals (C++ function) AbsTerm::get_array_element_sort (C++ function) AbsTerm::get_array_index_sort (C++ function) AbsTerm::get_bv_size (C++ function) AbsTerm::get_children (C++ function) AbsTerm::get_ff_size (C++ function) AbsTerm::get_fp_exp_size (C++ function) AbsTerm::get_fp_sig_size (C++ function) AbsTerm::get_fun_arity (C++ function) AbsTerm::get_fun_codomain_sort (C++ function) AbsTerm::get_fun_domain_sorts (C++ function) AbsTerm::get_id (C++ function) AbsTerm::get_indices (C++ function) AbsTerm::get_kind (C++ function) AbsTerm::get_leaf_kind (C++ function) AbsTerm::get_num_indices (C++ function) AbsTerm::get_sort (C++ function) AbsTerm::hash (C++ function) AbsTerm::is_array (C++ function) AbsTerm::is_bag (C++ function) AbsTerm::is_bag_value (C++ function) AbsTerm::is_bool (C++ function) AbsTerm::is_bool_value (C++ function) AbsTerm::is_bv (C++ function) AbsTerm::is_bv_value (C++ function) AbsTerm::is_const (C++ function) AbsTerm::is_dt (C++ function) AbsTerm::is_dt_value (C++ function) AbsTerm::is_ff (C++ function) AbsTerm::is_ff_value (C++ function) AbsTerm::is_fp (C++ function) AbsTerm::is_fp_value (C++ function) AbsTerm::is_fun (C++ function) AbsTerm::is_indexed (C++ function) AbsTerm::is_int (C++ function) AbsTerm::is_int_value (C++ function) AbsTerm::is_real (C++ function) AbsTerm::is_real_value (C++ function) AbsTerm::is_reglan (C++ function) AbsTerm::is_reglan_value (C++ function) AbsTerm::is_rm (C++ function) AbsTerm::is_rm_value (C++ function) AbsTerm::is_seq (C++ function) AbsTerm::is_seq_value (C++ function) AbsTerm::is_set (C++ function) AbsTerm::is_set_value (C++ function) AbsTerm::is_special_value (C++ function) AbsTerm::is_string (C++ function) AbsTerm::is_string_value (C++ function) AbsTerm::is_uninterpreted (C++ function) AbsTerm::is_value (C++ function) AbsTerm::is_var (C++ function) AbsTerm::LeafKind (C++ enum) AbsTerm::LeafKind::CONSTANT (C++ enumerator) AbsTerm::LeafKind::NONE (C++ enumerator) AbsTerm::LeafKind::VALUE (C++ enumerator) AbsTerm::LeafKind::VARIABLE (C++ enumerator) AbsTerm::not_equals (C++ function) AbsTerm::set_id (C++ function) AbsTerm::set_leaf_kind (C++ function) AbsTerm::set_sort (C++ function) AbsTerm::set_special_value_kind (C++ function) AbsTerm::SpecialValueKind (C++ type) AbsTerm::to_string (C++ function) AbsTerm::~AbsTerm (C++ function) Action (C++ class) Action::Action (C++ function), [1] Action::disabled (C++ function) Action::empty (C++ function) Action::generate (C++ function) Action::get_id (C++ function) Action::get_kind (C++ function) Action::get_sort_kind_from_str (C++ function) Action::get_untraced_sort (C++ function) Action::get_untraced_term (C++ function) Action::Kind (C++ type) Action::returns (C++ function) Action::ReturnValue (C++ enum)

Action::ReturnValue::ID (C++ enumerator) Action::ReturnValue::ID_LIST (C++ enumerator) Action::ReturnValue::NONE (C++ enumerator) Action::seed_solver_rng (C++ function) Action::set_id (C++ function) Action::TraceStream (C++ class) Action::TraceStream::stream (C++ function) Action::TraceStream::TraceStream (C++ function), [1] Action::TraceStream::~TraceStream (C++ function) Action::UNDEFINED (C++ member) Action::untrace (C++ function) Action::untrace_str_to_id (C++ function) Action::~Action (C++ function) ActionAssertFormula (C++ class) ActionAssertFormula::ActionAssertFormula (C++ function) ActionAssertFormula::generate (C++ function) ActionAssertFormula::s_name (C++ member) ActionAssertFormula::untrace (C++ function) ActionCheckSat (C++ class) ActionCheckSat::ActionCheckSat (C++ function) ActionCheckSat::generate (C++ function) ActionCheckSat::s_name (C++ member) ActionCheckSat::untrace (C++ function) ActionCheckSatAssuming (C++ class) ActionCheckSatAssuming::ActionCheckSatAssuming (C++ function) ActionCheckSatAssuming::generate (C++ function) ActionCheckSatAssuming::s_name (C++ member) ActionCheckSatAssuming::untrace (C++ function) ActionDelete (C++ class) ActionDelete::ActionDelete (C++ function) ActionDelete::generate (C++ function) ActionDelete::s_name (C++ member) ActionDelete::untrace (C++ function) ActionGetUnsatAssumptions (C++ class) ActionGetUnsatAssumptions::ActionGetUnsatAssumptions (C++ function) ActionGetUnsatAssumptions::generate (C++ function) ActionGetUnsatAssumptions::s_name (C++ member) ActionGetUnsatAssumptions::untrace (C++ function) ActionGetUnsatCore (C++ class) ActionGetUnsatCore::ActionGetUnsatCore (C++ function) ActionGetUnsatCore::generate (C++ function) ActionGetUnsatCore::s_name (C++ member) ActionGetUnsatCore::untrace (C++ function) ActionGetValue (C++ class) ActionGetValue::ActionGetValue (C++ function) ActionGetValue::generate (C++ function) ActionGetValue::s_name (C++ member) ActionGetValue::untrace (C++ function) ActionInstantiateSort (C++ class) ActionInstantiateSort::ActionInstantiateSort (C++ function) ActionInstantiateSort::generate (C++ function) ActionInstantiateSort::run (C++ function) ActionInstantiateSort::s_name (C++ member) ActionInstantiateSort::untrace (C++ function) ActionMkConst (C++ class) ActionMkConst::ActionMkConst (C++ function) ActionMkConst::generate (C++ function), [1] ActionMkConst::s_name (C++ member) ActionMkConst::untrace (C++ function) ActionMkFun (C++ class) ActionMkFun::ActionMkFun (C++ function) ActionMkFun::generate (C++ function) ActionMkFun::s_name (C++ member) ActionMkFun::untrace (C++ function) ActionMkSort (C++ class) ActionMkSort::ActionMkSort (C++ function) ActionMkSort::generate (C++ function) ActionMkSort::s_name (C++ member) ActionMkSort::untrace (C++ function) ActionMkSpecialValue (C++ class) ActionMkSpecialValue::ActionMkSpecialValue (C++ function) ActionMkSpecialValue::generate (C++ function), [1] ActionMkSpecialValue::s_name (C++ member) ActionMkSpecialValue::untrace (C++ function) ActionMkTerm (C++ class) ActionMkTerm::ActionMkTerm (C++ function) ActionMkTerm::check_term (C++ function) ActionMkTerm::generate (C++ function), [1], [2] ActionMkTerm::s_name (C++ member) ActionMkTerm::untrace (C++ function) ActionMkValue (C++ class) ActionMkValue::ActionMkValue (C++ function) ActionMkValue::check_value (C++ function) ActionMkValue::generate (C++ function), [1] ActionMkValue::s_name (C++ member) ActionMkValue::untrace (C++ function) ActionMkVar (C++ class) ActionMkVar::ActionMkVar (C++ function) ActionMkVar::generate (C++ function) ActionMkVar::run (C++ function) ActionMkVar::s_name (C++ member) ActionMkVar::untrace (C++ function) ActionNew (C++ class) ActionNew::ActionNew (C++ function) ActionNew::generate (C++ function) ActionNew::s_name (C++ member) ActionNew::untrace (C++ function) ActionPop (C++ class) ActionPop::ActionPop (C++ function) ActionPop::generate (C++ function) ActionPop::s_name (C++ member) ActionPop::untrace (C++ function) ActionPrintModel (C++ class) ActionPrintModel::ActionPrintModel (C++ function) ActionPrintModel::generate (C++ function) ActionPrintModel::s_name (C++ member) ActionPrintModel::untrace (C++ function) ActionPush (C++ class) ActionPush::ActionPush (C++ function) ActionPush::generate (C++ function) ActionPush::s_name (C++ member) ActionPush::untrace (C++ function) ActionReset (C++ class) ActionReset::ActionReset (C++ function) ActionReset::generate (C++ function) ActionReset::s_name (C++ member) ActionReset::untrace (C++ function) ActionResetAssertions (C++ class) ActionResetAssertions::ActionResetAssertions (C++ function) ActionResetAssertions::generate (C++ function) ActionResetAssertions::s_name (C++ member) ActionResetAssertions::untrace (C++ function) ActionSetLogic (C++ class) ActionSetLogic::ActionSetLogic (C++ function) ActionSetLogic::generate (C++ function) ActionSetLogic::s_name (C++ member) ActionSetLogic::untrace (C++ function) ActionSetOption (C++ class) ActionSetOption::ActionSetOption (C++ function) ActionSetOption::generate (C++ function) ActionSetOption::s_name (C++ member) ActionSetOption::untrace (C++ function) ActionSetOptionReq (C++ class) ActionSetOptionReq::ActionSetOptionReq (C++ function) ActionSetOptionReq::generate (C++ function) ActionSetOptionReq::init (C++ function) ActionSetOptionReq::s_name (C++ member) ActionSetOptionReq::untrace (C++ function) ActionTermGetChildren (C++ class) ActionTermGetChildren::ActionTermGetChildren (C++ function) ActionTermGetChildren::generate (C++ function) ActionTermGetChildren::s_name (C++ member) ActionTermGetChildren::untrace (C++ function) AND (C++ member) ARRAY_SELECT (C++ member) ARRAY_STORE (C++ member)

B

BAG_CARD (C++ member) BAG_CHOOSE (C++ member) BAG_COUNT (C++ member) BAG_DIFFERENCE_REMOVE (C++ member) BAG_DIFFERENCE_SUBTRACT (C++ member) BAG_DUPLICATE_REMOVAL (C++ member) BAG_EMPTY (C++ member) BAG_FROM_SET (C++ member) BAG_INTERSECTION_MIN (C++ member) BAG_IS_SINGLETON (C++ member) BAG_MAKE (C++ member) BAG_MAP (C++ member) BAG_SUBBAG (C++ member) BAG_TO_SET (C++ member) BAG_UNION_DISJOINT (C++ member) BAG_UNION_MAX (C++ member) BV_ADD (C++ member) BV_AND (C++ member) BV_ASHR (C++ member) BV_COMP (C++ member) BV_CONCAT (C++ member) BV_EXTRACT (C++ member) BV_LSHR (C++ member) BV_MULT (C++ member) BV_NAND (C++ member)

BV_NEG (C++ member) BV_NOR (C++ member) BV_NOT (C++ member) BV_OR (C++ member) BV_REPEAT (C++ member) BV_ROTATE_LEFT (C++ member) BV_ROTATE_RIGHT (C++ member) BV_SDIV (C++ member) BV_SGE (C++ member) BV_SGT (C++ member) BV_SHL (C++ member) BV_SIGN_EXTEND (C++ member) BV_SLE (C++ member) BV_SLT (C++ member) BV_SMOD (C++ member) BV_SREM (C++ member) BV_SUB (C++ member) BV_UDIV (C++ member) BV_UGE (C++ member) BV_UGT (C++ member) BV_ULE (C++ member) BV_ULT (C++ member) BV_UREM (C++ member) BV_XNOR (C++ member) BV_XOR (C++ member) BV_ZERO_EXTEND (C++ member)

C

CONST_ARRAY (C++ member)

CONSTANT (C++ member)

D

DISTINCT (C++ member) DT_APPLY_CONS (C++ member) DT_APPLY_SEL (C++ member) DT_APPLY_TESTER (C++ member)

DT_APPLY_UPDATER (C++ member) DT_MATCH (C++ member) DT_MATCH_BIND_CASE (C++ member) DT_MATCH_CASE (C++ member)

E

EQUAL (C++ member)

EXISTS (C++ member)

F

FINITE_FIELD_ADD (C++ member) FINITE_FIELD_MULT (C++ member) FINITE_FIELD_NEG (C++ member) FORALL (C++ member) FP_ABS (C++ member) FP_ADD (C++ member) FP_DIV (C++ member) FP_EQ (C++ member) FP_FMA (C++ member) FP_FP (C++ member) FP_GEQ (C++ member) FP_GT (C++ member) FP_IS_INF (C++ member) FP_IS_NAN (C++ member) FP_IS_NEG (C++ member) FP_IS_NORMAL (C++ member) FP_IS_POS (C++ member) FP_IS_SUBNORMAL (C++ member) FP_IS_ZERO (C++ member) FP_LEQ (C++ member) FP_LT (C++ member) FP_MAX (C++ member) FP_MIN (C++ member) FP_MUL (C++ member) FP_NEG (C++ member) FP_REM (C++ member) FP_RTI (C++ member) FP_SQRT (C++ member)

FP_SUB (C++ member) FP_TO_FP_FROM_BV (C++ member) FP_TO_FP_FROM_FP (C++ member) FP_TO_FP_FROM_REAL (C++ member) FP_TO_FP_FROM_SBV (C++ member) FP_TO_FP_FROM_UBV (C++ member) FP_TO_REAL (C++ member) FP_TO_SBV (C++ member) FP_TO_UBV (C++ member) FSM (C++ class) FSM::add_action_to_all_states (C++ function), [1] FSM::add_action_to_all_states_next (C++ function), [1] FSM::check_states (C++ function) FSM::configure (C++ function) FSM::disable_action (C++ function) FSM::FSM (C++ function), [1] FSM::get_action_id_mapping (C++ function) FSM::get_smgr (C++ function) FSM::get_state (C++ function) FSM::new_action (C++ function) FSM::new_choice_state (C++ function) FSM::new_decision_state (C++ function) FSM::new_final_state (C++ function) FSM::new_state (C++ function) FSM::print (C++ function) FSM::run (C++ function) FSM::set_init_state (C++ function) FSM::untrace (C++ function) FUN (C++ member)

I

IFF (C++ member) IMPLIES (C++ member) INT_ABS (C++ member) INT_ADD (C++ member) INT_DIV (C++ member) INT_GT (C++ member) INT_GTE (C++ member) INT_IS_DIV (C++ member)

INT_LT (C++ member) INT_LTE (C++ member) INT_MOD (C++ member) INT_MUL (C++ member) INT_NEG (C++ member) INT_SUB (C++ member) INT_TO_REAL (C++ member) INTERNAL (C++ member) ITE (C++ member)

M

MURXLA_CHECK_TRACE (C macro) MURXLA_CHECK_TRACE_EMPTY (C macro) MURXLA_CHECK_TRACE_NOT_EMPTY (C macro) MURXLA_CHECK_TRACE_NTOKENS (C macro) MURXLA_CHECK_TRACE_NTOKENS_MIN (C macro) MURXLA_CHECK_TRACE_NTOKENS_OF_SORT (C macro) MURXLA_CHECK_TRACE_SORT (C macro) MURXLA_CHECK_TRACE_TERM (C macro) MURXLA_MK_TERM_N_ARGS (C macro) MURXLA_MK_TERM_N_ARGS_BIN (C macro) MURXLA_TEST (C macro) MURXLA_TRACE (C macro) MURXLA_TRACE_RETURN (C macro)

MurxlaActionUntraceException (C++ class) MurxlaActionUntraceException::MurxlaActionUntraceException (C++ function), [1] MurxlaConfigException (C++ class) MurxlaConfigException::MurxlaConfigException (C++ function), [1] MurxlaException (C++ class) MurxlaException::get_msg (C++ function) MurxlaException::MurxlaException (C++ function), [1] MurxlaSolverOptionException (C++ class) MurxlaSolverOptionException::MurxlaSolverOptionException (C++ function), [1] MurxlaUntraceException (C++ class) MurxlaUntraceException::MurxlaUntraceException (C++ function), [1] MurxlaUntraceIdException (C++ class) MurxlaUntraceIdException::MurxlaUntraceIdException (C++ function), [1]

N

NOT (C++ member)

O

Op (C++ struct) Op::d_arity (C++ member) Op::d_id (C++ member) Op::d_kind (C++ member) Op::d_nidxs (C++ member) Op::d_sort_kinds (C++ member) Op::d_theory (C++ member) Op::get_arg_sort_kind (C++ function) Op::Kind (C++ type) Op::Op (C++ function) Op::operator== (C++ function) operator!= (C++ function), [1]

operator<< (C++ function), [1], [2], [3], [4] operator== (C++ function), [1] OpKindManager (C++ class) OpKindManager::add_op_kind (C++ function) OpKindManager::get_op (C++ function) OpKindManager::get_op_kinds (C++ function) OpKindManager::OpKindManager (C++ function) OpKindMap (C++ type) OpKinds (C++ type) OpKindSet (C++ type) OpKindVector (C++ type) OR (C++ member)

P

ParamSort (C++ class) ParamSort::equals (C++ function) ParamSort::get_symbol (C++ function) ParamSort::hash (C++ function) ParamSort::is_array (C++ function) ParamSort::is_bag (C++ function) ParamSort::is_bool (C++ function) ParamSort::is_bv (C++ function) ParamSort::is_dt (C++ function) ParamSort::is_dt_parametric (C++ function) ParamSort::is_ff (C++ function)

ParamSort::is_fp (C++ function) ParamSort::is_fun (C++ function) ParamSort::is_int (C++ function) ParamSort::is_param_sort (C++ function) ParamSort::is_real (C++ function) ParamSort::is_reglan (C++ function) ParamSort::is_rm (C++ function) ParamSort::is_seq (C++ function) ParamSort::is_set (C++ function) ParamSort::is_string (C++ function) ParamSort::ParamSort (C++ function) ParamSort::to_string (C++ function)

R

RE_ALL (C++ member) RE_ALLCHAR (C++ member) RE_COMP (C++ member) RE_CONCAT (C++ member) RE_DIFF (C++ member) RE_INTER (C++ member) RE_LOOP (C++ member) RE_NONE (C++ member) RE_OPT (C++ member) RE_PLUS (C++ member) RE_POW (C++ member) RE_RANGE (C++ member) RE_STAR (C++ member) RE_UNION (C++ member) REAL_ADD (C++ member)

REAL_DIV (C++ member) REAL_GT (C++ member) REAL_GTE (C++ member) REAL_IS_INT (C++ member) REAL_LT (C++ member) REAL_LTE (C++ member) REAL_MUL (C++ member) REAL_NEG (C++ member) REAL_SUB (C++ member) REAL_TO_INT (C++ member) REL_IDEN (C++ member) REL_JOIN (C++ member) REL_JOIN_IMAGE (C++ member) REL_PRODUCT (C++ member) REL_TCLOSURE (C++ member) REL_TRANSPOSE (C++ member)

S

SEQ_AT (C++ member) SEQ_CONCAT (C++ member) SEQ_CONTAINS (C++ member) SEQ_EXTRACT (C++ member) SEQ_INDEXOF (C++ member) SEQ_LENGTH (C++ member) SEQ_NTH (C++ member) SEQ_PREFIX (C++ member) SEQ_REPLACE (C++ member) SEQ_REPLACE_ALL (C++ member) SEQ_REV (C++ member) SEQ_SUFFIX (C++ member) SEQ_UNIT (C++ member) SEQ_UPDATE (C++ member) SET_CARD (C++ member) SET_CHOOSE (C++ member) SET_COMPLEMENT (C++ member) SET_COMPREHENSION (C++ member) SET_INSERT (C++ member) SET_INTERSECTION (C++ member) SET_IS_SINGLETON (C++ member) SET_MEMBER (C++ member) SET_MINUS (C++ member) SET_SINGLETON (C++ member) SET_SUBSET (C++ member) SET_UNION (C++ member) Solver (C++ class) Solver::add_special_value (C++ function) Solver::assert_formula (C++ function) Solver::Base (C++ enum) Solver::Base::BIN (C++ enumerator) Solver::Base::DEC (C++ enumerator) Solver::Base::HEX (C++ enumerator) Solver::check_sat (C++ function) Solver::check_sat_assuming (C++ function) Solver::check_sort (C++ function) Solver::check_term (C++ function), [1] Solver::check_value (C++ function) Solver::configure_fsm (C++ function) Solver::configure_opmgr (C++ function) Solver::configure_options (C++ function) Solver::d_rng (C++ member) Solver::d_special_values (C++ member) Solver::d_special_values_sort_kinds (C++ member) Solver::delete_solver (C++ function) Solver::disable_unsupported_actions (C++ function) Solver::get_name (C++ function) Solver::get_option_name_incremental (C++ function) Solver::get_option_name_model_gen (C++ function) Solver::get_option_name_unsat_assumptions (C++ function) Solver::get_option_name_unsat_cores (C++ function) Solver::get_profile (C++ function) Solver::get_required_options (C++ function) Solver::get_rng (C++ function) Solver::get_sort (C++ function) Solver::get_special_values (C++ function) Solver::get_special_values_sort_kinds (C++ function) Solver::get_unsat_assumptions (C++ function) Solver::get_unsat_core (C++ function) Solver::get_value (C++ function) Solver::instantiate_sort (C++ function) Solver::is_initialized (C++ function) Solver::is_unsat_assumption (C++ function) Solver::mk_const (C++ function) Solver::mk_fun (C++ function) Solver::mk_sort (C++ function), [1], [2], [3], [4], [5], [6] Solver::mk_special_value (C++ function) Solver::mk_term (C++ function), [1], [2] Solver::mk_value (C++ function), [1], [2], [3] Solver::mk_var (C++ function) Solver::new_solver (C++ function) Solver::OpKindSortKindMap (C++ type) Solver::option_incremental_enabled (C++ function) Solver::option_model_gen_enabled (C++ function) Solver::option_unsat_assumptions_enabled (C++ function) Solver::option_unsat_cores_enabled (C++ function) Solver::pop (C++ function) Solver::print_model (C++ function) Solver::push (C++ function) Solver::reset (C++ function) Solver::reset_assertions (C++ function) Solver::reset_sat (C++ function) Solver::Result (C++ enum) Solver::Result::SAT (C++ enumerator) Solver::Result::UNKNOWN (C++ enumerator) Solver::Result::UNSAT (C++ enumerator) Solver::set_logic (C++ function) Solver::set_opt (C++ function) Solver::Solver (C++ function), [1] Solver::~Solver (C++ function) SolverManager (C++ class) SolverManager::add_assumption (C++ function) SolverManager::add_const (C++ function) SolverManager::add_input (C++ function) SolverManager::add_option (C++ function) SolverManager::add_sort (C++ function) SolverManager::add_string_char_value (C++ function) SolverManager::add_term (C++ function) SolverManager::add_value (C++ function) SolverManager::add_var (C++ function) SolverManager::clear (C++ function) SolverManager::clear_assumptions (C++ function) SolverManager::d_arith_linear (C++ member) SolverManager::d_incremental (C++ member) SolverManager::d_mbt_stats (C++ member) SolverManager::d_model_gen (C++ member) SolverManager::d_n_push_levels (C++ member) SolverManager::d_n_sat_calls (C++ member) SolverManager::d_sat_called (C++ member) SolverManager::d_sat_result (C++ member) SolverManager::d_simple_symbols (C++ member) SolverManager::d_stats (C++ member) SolverManager::d_unsat_assumptions (C++ member) SolverManager::d_unsat_cores (C++ member) SolverManager::find_sort (C++ function) SolverManager::find_term (C++ function) SolverManager::get_enabled_theories (C++ function) SolverManager::get_num_terms_max_level (C++ function) SolverManager::get_num_vars (C++ function) SolverManager::get_op (C++ function) SolverManager::get_profile (C++ function) SolverManager::get_rng (C++ function) SolverManager::get_sng (C++ function) SolverManager::get_solver (C++ function) SolverManager::get_term (C++ function) SolverManager::get_trace (C++ function) SolverManager::get_untraced_sort (C++ function) SolverManager::get_untraced_term (C++ function) SolverManager::has_assumed (C++ function) SolverManager::has_fun (C++ function) SolverManager::has_quant_body (C++ function) SolverManager::has_quant_term (C++ function), [1] SolverManager::has_sort (C++ function), [1], [2], [3] SolverManager::has_sort_bv (C++ function) SolverManager::has_sort_bv_max (C++ function) SolverManager::has_sort_dt_parametric (C++ function) SolverManager::has_sort_excluding (C++ function), [1] SolverManager::has_sort_with_sort_params (C++ function) SolverManager::has_string_char_value (C++ function) SolverManager::has_term (C++ function), [1], [2], [3], [4], [5] SolverManager::has_value (C++ function), [1] SolverManager::has_var (C++ function) SolverManager::mark_option_used (C++ function) SolverManager::pick_assumed_assumption (C++ function) SolverManager::pick_fun (C++ function) SolverManager::pick_op_kind (C++ function)

SolverManager::pick_option (C++ function) SolverManager::pick_quant_body (C++ function) SolverManager::pick_quant_term (C++ function), [1] SolverManager::pick_sort (C++ function), [1], [2] SolverManager::pick_sort_bv (C++ function) SolverManager::pick_sort_bv_max (C++ function) SolverManager::pick_sort_dt_param (C++ function) SolverManager::pick_sort_excluding (C++ function) SolverManager::pick_sort_kind (C++ function), [1], [2] SolverManager::pick_sort_kind_data (C++ function) SolverManager::pick_sort_kind_excluding (C++ function) SolverManager::pick_sort_with_sort_params (C++ function) SolverManager::pick_string_char_value (C++ function) SolverManager::pick_symbol (C++ function) SolverManager::pick_term (C++ function), [1], [2], [3], [4] SolverManager::pick_term_min_level (C++ function) SolverManager::pick_value (C++ function), [1] SolverManager::pick_var (C++ function) SolverManager::pick_vars (C++ function) SolverManager::remove_var (C++ function) SolverManager::report_result (C++ function) SolverManager::reset (C++ function) SolverManager::reset_sat (C++ function) SolverManager::Stats (C++ struct) SolverOption (C++ class) SolverOption::d_name (C++ member) SolverOption::get_name (C++ function) SolverOption::pick_value (C++ function) SolverOptionBool (C++ class) SolverOptionBool::d_default (C++ member) SolverOptionBool::pick_value (C++ function) SolverOptionBool::SolverOptionBool (C++ function) SolverOptionList (C++ class) SolverOptionList::d_default (C++ member) SolverOptionList::d_values (C++ member) SolverOptionList::pick_value (C++ function) SolverOptionList::SolverOptionList (C++ function) SolverOptionNum (C++ class) SolverOptionNum::d_default (C++ member) SolverOptionNum::d_max (C++ member) SolverOptionNum::d_min (C++ member) SolverOptionNum::pick_value (C++ function) SolverOptionNum::SolverOptionNum (C++ function) Sort (C++ type) SortKind (C++ enum) SortKind::SORT_ANY (C++ enumerator) SortKind::SORT_ARRAY (C++ enumerator) SortKind::SORT_BAG (C++ enumerator) SortKind::SORT_BOOL (C++ enumerator) SortKind::SORT_BV (C++ enumerator) SortKind::SORT_DT (C++ enumerator) SortKind::SORT_FF (C++ enumerator) SortKind::SORT_FP (C++ enumerator) SortKind::SORT_FUN (C++ enumerator) SortKind::SORT_INT (C++ enumerator) SortKind::SORT_REAL (C++ enumerator) SortKind::SORT_REGLAN (C++ enumerator) SortKind::SORT_RM (C++ enumerator) SortKind::SORT_SEQ (C++ enumerator) SortKind::SORT_SET (C++ enumerator) SortKind::SORT_STRING (C++ enumerator) SortKind::SORT_UNINTERPRETED (C++ enumerator) SortKindSet (C++ type) SortKindVector (C++ type) SPECIAL_VALUE_BAG_EMPTY (C++ member) SPECIAL_VALUE_BV_MAX_SIGNED (C++ member) SPECIAL_VALUE_BV_MIN_SIGNED (C++ member) SPECIAL_VALUE_BV_ONE (C++ member) SPECIAL_VALUE_BV_ONES (C++ member) SPECIAL_VALUE_BV_ZERO (C++ member) SPECIAL_VALUE_FF_NEG_ONE (C++ member) SPECIAL_VALUE_FF_ONE (C++ member) SPECIAL_VALUE_FF_ZERO (C++ member) SPECIAL_VALUE_FP_NAN (C++ member) SPECIAL_VALUE_FP_NEG_INF (C++ member) SPECIAL_VALUE_FP_NEG_ZERO (C++ member) SPECIAL_VALUE_FP_POS_INF (C++ member) SPECIAL_VALUE_FP_POS_ZERO (C++ member) SPECIAL_VALUE_NONE (C++ member) SPECIAL_VALUE_RM_RNA (C++ member) SPECIAL_VALUE_RM_RNE (C++ member) SPECIAL_VALUE_RM_RTN (C++ member) SPECIAL_VALUE_RM_RTP (C++ member) SPECIAL_VALUE_RM_RTZ (C++ member) SPECIAL_VALUE_SEQ_EMPTY (C++ member) SPECIAL_VALUE_SET_EMPTY (C++ member) SPECIAL_VALUE_SET_UNIVERSE (C++ member) State (C++ class) State::add_action (C++ function) State::ASSERT (C++ member) State::CHECK_SAT (C++ member) State::ConfigKind (C++ enum) State::ConfigKind::CHOICE (C++ enumerator) State::ConfigKind::DECISION (C++ enumerator) State::ConfigKind::REGULAR (C++ enumerator) State::CREATE_INPUTS (C++ member) State::CREATE_SORTS (C++ member) State::CREATE_TERMS (C++ member) State::DECIDE_SAT_UNSAT (C++ member) State::DELETE (C++ member) State::disable_action (C++ function) State::FINAL (C++ member) State::get_config (C++ function) State::get_id (C++ function) State::get_kind (C++ function) State::is_final (C++ function) State::Kind (C++ type) State::NEW (C++ member) State::OPT (C++ member) State::OPT_REQ (C++ member) State::PUSH_POP (C++ member) State::run (C++ function) State::SAT (C++ member) State::set_id (C++ function) State::SET_LOGIC (C++ member) State::State (C++ function), [1] State::UNDEFINED (C++ member) State::UNSAT (C++ member) State::update_precondition (C++ function) std::hash<murxla::Sort> (C++ struct) std::hash<murxla::Sort>::operator() (C++ function) std::hash<murxla::SortKind> (C++ struct) std::hash<murxla::SortKind>::operator() (C++ function) std::hash<murxla::Term> (C++ struct) std::hash<murxla::Term>::operator() (C++ function) STR_AT (C++ member) STR_CONCAT (C++ member) STR_CONTAINS (C++ member) STR_FROM_CODE (C++ member) STR_FROM_INT (C++ member) STR_IN_RE (C++ member) STR_INDEXOF (C++ member) STR_IS_DIGIT (C++ member) STR_LE (C++ member) STR_LEN (C++ member) STR_LT (C++ member) STR_PREFIXOF (C++ member) STR_REPLACE (C++ member) STR_REPLACE_ALL (C++ member) STR_REPLACE_RE (C++ member) STR_REPLACE_RE_ALL (C++ member) STR_SUBSTR (C++ member) STR_SUFFIXOF (C++ member) STR_TO_CODE (C++ member) STR_TO_INT (C++ member) STR_TO_RE (C++ member)

T

Term (C++ type) Theory (C++ enum) Theory::THEORY_ALL (C++ enumerator) Theory::THEORY_ARRAY (C++ enumerator) Theory::THEORY_BAG (C++ enumerator) Theory::THEORY_BOOL (C++ enumerator) Theory::THEORY_BV (C++ enumerator) Theory::THEORY_DT (C++ enumerator) Theory::THEORY_FF (C++ enumerator) Theory::THEORY_FP (C++ enumerator) Theory::THEORY_INT (C++ enumerator) Theory::THEORY_QUANT (C++ enumerator) Theory::THEORY_REAL (C++ enumerator) Theory::THEORY_SEQ (C++ enumerator) Theory::THEORY_SET (C++ enumerator) Theory::THEORY_STRING (C++ enumerator) Theory::THEORY_TRANSCENDENTAL (C++ enumerator) Theory::THEORY_UF (C++ enumerator) TheorySet (C++ type)

TheoryVector (C++ type) TRANS_ARCCOSECANT (C++ member) TRANS_ARCCOSINE (C++ member) TRANS_ARCCOTANGENT (C++ member) TRANS_ARCSECANT (C++ member) TRANS_ARCSINE (C++ member) TRANS_ARCTANGENT (C++ member) TRANS_COSECANT (C++ member) TRANS_COSINE (C++ member) TRANS_COTANGENT (C++ member) TRANS_PI (C++ member) TRANS_SECANT (C++ member) TRANS_SINE (C++ member) TRANS_SQRT (C++ member) TRANS_TANGENT (C++ member) Transition (C++ class) TransitionCreateInputs (C++ class) TransitionCreateSorts (C++ class) TransitionDefault (C++ class)

U

UF_APPLY (C++ member) UNDEFINED (C++ member) UnresolvedSort (C++ class) UnresolvedSort::equals (C++ function) UnresolvedSort::get_symbol (C++ function) UnresolvedSort::hash (C++ function) UnresolvedSort::is_array (C++ function) UnresolvedSort::is_bag (C++ function) UnresolvedSort::is_bool (C++ function) UnresolvedSort::is_bv (C++ function) UnresolvedSort::is_dt (C++ function) UnresolvedSort::is_dt_parametric (C++ function)

UnresolvedSort::is_ff (C++ function) UnresolvedSort::is_fp (C++ function) UnresolvedSort::is_fun (C++ function) UnresolvedSort::is_int (C++ function) UnresolvedSort::is_real (C++ function) UnresolvedSort::is_reglan (C++ function) UnresolvedSort::is_rm (C++ function) UnresolvedSort::is_seq (C++ function) UnresolvedSort::is_set (C++ function) UnresolvedSort::is_string (C++ function) UnresolvedSort::is_unresolved_sort (C++ function) UnresolvedSort::to_string (C++ function) UnresolvedSort::UnresolvedSort (C++ function)

V

VALUE (C++ member)

VARIABLE (C++ member)

X

XOR (C++ member)