List of all items
Structs
- OptionInfo
- OptionInfo_BoolInfo
- OptionInfo_DoubleInfo
- OptionInfo_IntInfo
- OptionInfo_ModeInfo
- OptionInfo_StringInfo
- OptionInfo_UIntInfo
- Plugin
- Solver
- TermManager
- cvc5_dt_cons_decl_t
- cvc5_dt_cons_t
- cvc5_dt_decl_t
- cvc5_dt_sel_t
- cvc5_dt_t
- cvc5_grammar_t
- cvc5_op_t
- cvc5_proof_t
- cvc5_result_t
- cvc5_sort_t
- cvc5_stat_t
- cvc5_stats_t
- cvc5_synth_result_t
- cvc5_term_t
- parser::InputParser
- parser::SymbolManager
- parser::cvc5_cmd_t
Enums
- BlockModelsMode
- FindSynthTarget
- InputLanguage
- Kind
- LearnedLitType
- OptionCategory
- OptionInfoKind
- ProofComponent
- ProofFormat
- ProofRewriteRule
- ProofRule
- RoundingMode
- SkolemId
- SortKind
- UnknownExplanation
Functions
- add_plugin
- add_sygus_assume
- add_sygus_constraint
- add_sygus_inv_constraint
- assert_formula
- block_model
- block_model_values
- check_sat
- check_sat_assuming
- check_synth
- check_synth_next
- close_output
- declare_dt
- declare_fun
- declare_oracle_fun
- declare_pool
- declare_sep_heap
- declare_sort
- declare_sygus_var
- define_fun
- define_fun_rec
- define_fun_rec_from_const
- define_funs_rec
- delete
- dt_cons_copy
- dt_cons_decl_add_selector
- dt_cons_decl_add_selector_self
- dt_cons_decl_add_selector_unresolved
- dt_cons_decl_copy
- dt_cons_decl_hash
- dt_cons_decl_is_equal
- dt_cons_decl_release
- dt_cons_decl_to_string
- dt_cons_get_instantiated_term
- dt_cons_get_name
- dt_cons_get_num_selectors
- dt_cons_get_selector
- dt_cons_get_selector_by_name
- dt_cons_get_term
- dt_cons_get_tester_term
- dt_cons_hash
- dt_cons_is_equal
- dt_cons_release
- dt_cons_to_string
- dt_copy
- dt_decl_add_constructor
- dt_decl_copy
- dt_decl_get_name
- dt_decl_get_num_constructors
- dt_decl_hash
- dt_decl_is_equal
- dt_decl_is_parametric
- dt_decl_is_resolved
- dt_decl_release
- dt_decl_to_string
- dt_get_constructor
- dt_get_constructor_by_name
- dt_get_name
- dt_get_num_constructors
- dt_get_parameters
- dt_get_selector
- dt_hash
- dt_is_codatatype
- dt_is_equal
- dt_is_finite
- dt_is_parametric
- dt_is_record
- dt_is_tuple
- dt_is_well_founded
- dt_release
- dt_sel_copy
- dt_sel_get_codomain_sort
- dt_sel_get_name
- dt_sel_get_term
- dt_sel_get_updater_term
- dt_sel_hash
- dt_sel_is_equal
- dt_sel_release
- dt_sel_to_string
- dt_to_string
- find_synth
- find_synth_next
- find_synth_with_grammar
- get_abduct
- get_abduct_next
- get_abduct_with_grammar
- get_assertions
- get_boolean_sort
- get_difficulty
- get_info
- get_instantiations
- get_integer_sort
- get_interpolant
- get_interpolant_next
- get_interpolant_with_grammar
- get_learned_literals
- get_logic
- get_model
- get_model_domain_elements
- get_num_idxs_for_skolem_id
- get_option
- get_option_info
- get_option_names
- get_output
- get_proof
- get_quantifier_elimination
- get_quantifier_elimination_disjunct
- get_real_sort
- get_regexp_sort
- get_rm_sort
- get_statistics
- get_string_sort
- get_sygus_assumptions
- get_sygus_constraints
- get_synth_solution
- get_synth_solutions
- get_timeout_core
- get_timeout_core_assuming
- get_tm
- get_unsat_assumptions
- get_unsat_core
- get_unsat_core_lemmas
- get_value
- get_value_sep_heap
- get_value_sep_nil
- get_values
- get_version
- grammar_add_any_constant
- grammar_add_any_variable
- grammar_add_rule
- grammar_add_rules
- grammar_copy
- grammar_hash
- grammar_is_disequal
- grammar_is_equal
- grammar_release
- grammar_to_string
- is_logic_set
- is_model_core_symbol
- is_output_on
- kind_hash
- kind_to_string
- mk_abstract_sort
- mk_array_sort
- mk_bag_sort
- mk_boolean
- mk_bv
- mk_bv_sort
- mk_bv_uint64
- mk_cardinality_constraint
- mk_const
- mk_const_array
- mk_dt_cons_decl
- mk_dt_decl
- mk_dt_decl_with_params
- mk_dt_sort
- mk_dt_sorts
- mk_empty_bag
- mk_empty_sequence
- mk_empty_set
- mk_false
- mk_ff_elem
- mk_ff_sort
- mk_fp
- mk_fp_from_ieee
- mk_fp_nan
- mk_fp_neg_inf
- mk_fp_neg_zero
- mk_fp_pos_inf
- mk_fp_pos_zero
- mk_fp_sort
- mk_fun_sort
- mk_grammar
- mk_integer
- mk_integer_int64
- mk_nullable_is_null
- mk_nullable_is_some
- mk_nullable_lift
- mk_nullable_null
- mk_nullable_some
- mk_nullable_sort
- mk_nullable_val
- mk_op
- mk_op_from_str
- mk_param_sort
- mk_pi
- mk_predicate_sort
- mk_real
- mk_real_int64
- mk_real_num_den
- mk_record_sort
- mk_regexp_all
- mk_regexp_allchar
- mk_regexp_none
- mk_rm
- mk_sep_emp
- mk_sep_nil
- mk_sequence_sort
- mk_set_sort
- mk_skolem
- mk_string
- mk_string_from_char32
- mk_string_from_wchar
- mk_term
- mk_term_from_op
- mk_true
- mk_tuple
- mk_tuple_sort
- mk_uninterpreted_sort
- mk_uninterpreted_sort_constructor_sort
- mk_universe_set
- mk_unresolved_dt_sort
- mk_var
- modes_block_models_mode_to_string
- modes_find_synth_target_to_string
- modes_input_language_to_string
- modes_learned_lit_type_to_string
- modes_option_category_to_string
- modes_proof_component_to_string
- modes_proof_format_to_string
- new
- op_copy
- op_get_index
- op_get_kind
- op_get_num_indices
- op_hash
- op_is_disequal
- op_is_equal
- op_is_indexed
- op_release
- op_to_string
- option_info_to_string
- parser::cmd_get_name
- parser::cmd_invoke
- parser::cmd_to_string
- parser::parser_append_inc_str_input
- parser::parser_delete
- parser::parser_done
- parser::parser_get_sm
- parser::parser_get_solver
- parser::parser_new
- parser::parser_next_command
- parser::parser_next_term
- parser::parser_release
- parser::parser_set_file_input
- parser::parser_set_inc_str_input
- parser::parser_set_str_input
- parser::sm_get_declared_sorts
- parser::sm_get_declared_terms
- parser::sm_get_logic
- parser::sm_get_named_terms
- parser::sm_is_logic_set
- parser::symbol_manager_delete
- parser::symbol_manager_new
- pop
- print_stats_safe
- proof_copy
- proof_get_arguments
- proof_get_children
- proof_get_result
- proof_get_rewrite_rule
- proof_get_rule
- proof_hash
- proof_is_disequal
- proof_is_equal
- proof_release
- proof_rewrite_rule_hash
- proof_rewrite_rule_to_string
- proof_rule_hash
- proof_rule_to_string
- proof_to_string
- push
- reset_assertions
- result_copy
- result_get_unknown_explanation
- result_hash
- result_is_disequal
- result_is_equal
- result_is_null
- result_is_sat
- result_is_unknown
- result_is_unsat
- result_release
- result_to_string
- rm_to_string
- set_info
- set_logic
- set_option
- simplify
- skolem_id_hash
- skolem_id_to_string
- sort_abstract_get_kind
- sort_array_get_element_sort
- sort_array_get_index_sort
- sort_bag_get_element_sort
- sort_bv_get_size
- sort_compare
- sort_copy
- sort_dt_constructor_get_arity
- sort_dt_constructor_get_codomain
- sort_dt_constructor_get_domain
- sort_dt_get_arity
- sort_dt_selector_get_codomain
- sort_dt_selector_get_domain
- sort_dt_tester_get_codomain
- sort_dt_tester_get_domain
- sort_ff_get_size
- sort_fp_get_exp_size
- sort_fp_get_sig_size
- sort_fun_get_arity
- sort_fun_get_codomain
- sort_fun_get_domain
- sort_get_datatype
- sort_get_instantiated_parameters
- sort_get_kind
- sort_get_symbol
- sort_get_uninterpreted_sort_constructor
- sort_has_symbol
- sort_hash
- sort_instantiate
- sort_is_abstract
- sort_is_array
- sort_is_bag
- sort_is_boolean
- sort_is_bv
- sort_is_disequal
- sort_is_dt
- sort_is_dt_constructor
- sort_is_dt_selector
- sort_is_dt_tester
- sort_is_dt_updater
- sort_is_equal
- sort_is_ff
- sort_is_fp
- sort_is_fun
- sort_is_instantiated
- sort_is_integer
- sort_is_nullable
- sort_is_predicate
- sort_is_real
- sort_is_record
- sort_is_regexp
- sort_is_rm
- sort_is_sequence
- sort_is_set
- sort_is_string
- sort_is_tuple
- sort_is_uninterpreted_sort
- sort_is_uninterpreted_sort_constructor
- sort_kind_hash
- sort_kind_to_string
- sort_nullable_get_element_sort
- sort_release
- sort_sequence_get_element_sort
- sort_set_get_element_sort
- sort_substitute
- sort_substitute_sorts
- sort_to_string
- sort_tuple_get_element_sorts
- sort_tuple_get_length
- sort_uninterpreted_sort_constructor_get_arity
- stat_get_double
- stat_get_histogram
- stat_get_int
- stat_get_string
- stat_is_default
- stat_is_double
- stat_is_histogram
- stat_is_int
- stat_is_internal
- stat_is_string
- stat_to_string
- stats_get
- stats_iter_has_next
- stats_iter_init
- stats_iter_next
- stats_to_string
- synth_fun
- synth_fun_with_grammar
- synth_result_copy
- synth_result_has_no_solution
- synth_result_has_solution
- synth_result_hash
- synth_result_is_disequal
- synth_result_is_equal
- synth_result_is_null
- synth_result_is_unknown
- synth_result_release
- synth_result_to_string
- term_compare
- term_copy
- term_get_boolean_value
- term_get_bv_value
- term_get_cardinality_constraint
- term_get_child
- term_get_const_array_base
- term_get_ff_value
- term_get_fp_value
- term_get_id
- term_get_int32_value
- term_get_int64_value
- term_get_integer_value
- term_get_kind
- term_get_num_children
- term_get_op
- term_get_real32_value
- term_get_real64_value
- term_get_real_algebraic_number_defining_polynomial
- term_get_real_algebraic_number_lower_bound
- term_get_real_algebraic_number_upper_bound
- term_get_real_or_integer_value_sign
- term_get_real_value
- term_get_rm_value
- term_get_sequence_value
- term_get_set_value
- term_get_skolem_id
- term_get_skolem_indices
- term_get_sort
- term_get_string_value
- term_get_symbol
- term_get_tuple_value
- term_get_u32string_value
- term_get_uint32_value
- term_get_uint64_value
- term_get_uninterpreted_sort_value
- term_has_op
- term_has_symbol
- term_hash
- term_is_boolean_value
- term_is_bv_value
- term_is_cardinality_constraint
- term_is_const_array
- term_is_disequal
- term_is_equal
- term_is_ff_value
- term_is_fp_nan
- term_is_fp_neg_inf
- term_is_fp_neg_zero
- term_is_fp_pos_inf
- term_is_fp_pos_zero
- term_is_fp_value
- term_is_int32_value
- term_is_int64_value
- term_is_integer_value
- term_is_real32_value
- term_is_real64_value
- term_is_real_algebraic_number
- term_is_real_value
- term_is_rm_value
- term_is_sequence_value
- term_is_set_value
- term_is_skolem
- term_is_string_value
- term_is_tuple_value
- term_is_uint32_value
- term_is_uint64_value
- term_is_uninterpreted_sort_value
- term_manager_delete
- term_manager_get_statistics
- term_manager_new
- term_manager_print_stats_safe
- term_manager_release
- term_release
- term_substitute_term
- term_substitute_terms
- term_to_string
- unknown_explanation_to_string