Index

_

__YICES_VERSION (C macro) __YICES_VERSION_MAJOR (C macro)

__YICES_VERSION_PATCHLEVEL (C macro)

A

ARITH_ERROR (C enum) ARITHCONSTANT_REQUIRED (C enum)

ARITHTERM_REQUIRED (C enum)

B

BAD_TERM_DECREF (C enum) BAD_TYPE_DECREF (C enum) BITVECTOR_REQUIRED (C enum)

BVARITH_ERROR (C enum) BVTYPE_REQUIRED (C enum)

C

context_t (C type) CTX_ARITH_NOT_SUPPORTED (C enum) CTX_ARITH_SOLVER_EXCEPTION (C enum) CTX_ARRAY_SOLVER_EXCEPTION (C enum) CTX_ARRAYS_NOT_SUPPORTED (C enum) CTX_BV_NOT_SUPPORTED (C enum) CTX_BV_SOLVER_EXCEPTION (C enum) ctx_config_t (C type) CTX_DELEGATE_NOT_AVAILABLE (C enum) CTX_FORMULA_NOT_IDL (C enum) CTX_FORMULA_NOT_RDL (C enum) CTX_FREE_VAR_IN_FORMULA (C enum) CTX_INVALID_CONFIG (C enum) CTX_INVALID_OPERATION (C enum) CTX_INVALID_PARAMETER_VALUE (C enum) CTX_LAMBDAS_NOT_SUPPORTED (C enum)

CTX_LOGIC_NOT_SUPPORTED (C enum) CTX_NONLINEAR_ARITH_NOT_SUPPORTED (C enum) CTX_OPERATION_NOT_SUPPORTED (C enum) CTX_QUANTIFIERS_NOT_SUPPORTED (C enum) CTX_SCALAR_NOT_SUPPORTED (C enum) CTX_TOO_MANY_ARITH_ATOMS (C enum) CTX_TOO_MANY_ARITH_VARS (C enum) CTX_TOO_MANY_BV_ATOMS (C enum) CTX_TOO_MANY_BV_VARS (C enum) CTX_TUPLE_NOT_SUPPORTED (C enum) CTX_UF_NOT_SUPPORTED (C enum) CTX_UNKNOWN_DELEGATE (C enum) CTX_UNKNOWN_LOGIC (C enum) CTX_UNKNOWN_PARAMETER (C enum) CTX_UTYPE_NOT_SUPPORTED (C enum)

D

DEGREE_OVERFLOW (C enum) DIVISION_BY_ZERO (C enum) DUPLICATE_NAME_IN_SCALAR (C enum)

DUPLICATE_VAR_NAME (C enum) DUPLICATE_VARIABLE (C enum)

E

EMPTY_BITVECTOR (C enum) error_code_t (C type) error_report_t (C type) EVAL_CONVERSION_FAILED (C enum) EVAL_FAILED (C enum) EVAL_FREEVAR_IN_TERM (C enum)

EVAL_LAMBDA (C enum) EVAL_NO_IMPLICANT (C enum) EVAL_NOT_SUPPORTED (C enum) EVAL_OVERFLOW (C enum) EVAL_QUANTIFIER (C enum) EVAL_UNKNOWN_TERM (C enum)

F

FUNCTION_REQUIRED (C enum)

I

INCOMPATIBLE_TYPES (C enum) INTEGER_OVERFLOW (C enum) INTEGER_REQUIRED (C enum) INTERNAL_EXCEPTION (C enum) INVALID_BITEXTRACT (C enum) INVALID_BITSHIFT (C enum) INVALID_BVBIN_FORMAT (C enum) INVALID_BVCONSTANT (C enum) INVALID_BVEXTRACT (C enum) INVALID_BVHEX_FORMAT (C enum)

INVALID_CONSTANT_INDEX (C enum) INVALID_FLOAT_FORMAT (C enum) INVALID_RATIONAL_FORMAT (C enum) INVALID_TERM (C enum) INVALID_TERM_OP (C enum) INVALID_TOKEN (C enum) INVALID_TUPLE_INDEX (C enum) INVALID_TYPE (C enum) INVALID_TYPE_OP (C enum)

M

MAX_BVSIZE_EXCEEDED (C enum) MCSAT_ERROR_UNSUPPORTED_THEORY (C enum) MDL_CONSTANT_REQUIRED (C enum) MDL_CONSTRUCTION_FAILED (C enum) MDL_DUPLICATE_VAR (C enum) MDL_FTYPE_NOT_ALLOWED (C enum)

MDL_GEN_FAILED (C enum) MDL_GEN_NONLINEAR (C enum) MDL_GEN_TYPE_NOT_SUPPORTED (C enum) MDL_UNINT_REQUIRED (C enum) model_t (C type)

N

NEGATIVE_BVSIZE (C enum) NO_ERROR (C enum) NON_CONSTANT_DIVISOR (C enum)

NONNEG_INT_REQUIRED (C enum) NULL_TERM (C macro) NULL_TYPE (C macro)

O

OUTPUT_ERROR (C enum)

P

param_t (C type)

POS_INT_REQUIRED (C enum)

R

RATIONAL_REQUIRED (C enum) REDEFINED_TERM_NAME (C enum)

REDEFINED_TYPE_NAME (C enum)

S

SCALAR_OR_UTYPE_REQUIRED (C enum) SCALAR_TERM_REQUIRED (C enum) smt_status_t (C type) STATUS_ERROR (C enum) STATUS_IDLE (C enum) STATUS_INTERRUPTED (C enum)

STATUS_SAT (C enum) STATUS_SEARCHING (C enum) STATUS_UNKNOWN (C enum) STATUS_UNSAT (C enum) SYMBOL_REQUIRED (C enum) SYNTAX_ERROR (C enum)

T

term_constructor_t (C type) term_t (C type) term_vector_t (C type) TOO_MANY_ARGUMENTS (C enum) TOO_MANY_VARS (C enum) TUPLE_REQUIRED (C enum)

TYPE_MISMATCH (C enum) TYPE_MISMATCH_IN_DEF (C enum) TYPE_REQUIRED (C enum) type_t (C type) type_vector_t (C type)

U

UNDEFINED_TERM_NAME (C enum)

UNDEFINED_TYPE_NAME (C enum)

V

VARIABLE_REQUIRED (C enum)

W

WRONG_NUMBER_OF_ARGUMENTS (C enum)

Y

YICES_ABS (C enum) yices_abs (C function) yices_add (C function) yices_and (C function) yices_and2 (C function) yices_and3 (C function) YICES_APP_TERM (C enum) yices_application (C function) yices_application1 (C function) yices_application2 (C function) yices_application3 (C function) YICES_ARITH_CONSTANT (C enum) yices_arith_eq0_atom (C function) yices_arith_eq_atom (C function) YICES_ARITH_GE_ATOM (C enum) yices_arith_geq0_atom (C function) yices_arith_geq_atom (C function) yices_arith_gt0_atom (C function) yices_arith_gt_atom (C function) yices_arith_leq0_atom (C function) yices_arith_leq_atom (C function) yices_arith_lt0_atom (C function) yices_arith_lt_atom (C function) yices_arith_neq0_atom (C function) yices_arith_neq_atom (C function) YICES_ARITH_ROOT_ATOM (C enum) YICES_ARITH_SUM (C enum) yices_ashift_right (C function) yices_assert_blocking_clause (C function) yices_assert_formula (C function) yices_assert_formulas (C function) YICES_BIT_TERM (C enum) yices_bitextract (C function) yices_bool_const_value (C function) YICES_BOOL_CONSTANT (C enum) yices_bool_type (C function) yices_build_arch (C variable) yices_build_date (C variable) yices_build_mode (C variable) YICES_BV_ARRAY (C enum) YICES_BV_ASHR (C enum) yices_bv_const_value (C function) YICES_BV_CONSTANT (C enum) YICES_BV_DIV (C enum) YICES_BV_GE_ATOM (C enum) YICES_BV_LSHR (C enum) YICES_BV_REM (C enum) YICES_BV_SDIV (C enum) YICES_BV_SGE_ATOM (C enum) YICES_BV_SHL (C enum) YICES_BV_SMOD (C enum) YICES_BV_SREM (C enum) YICES_BV_SUM (C enum) yices_bv_type (C function) yices_bvadd (C function) yices_bvand (C function) yices_bvand2 (C function) yices_bvand3 (C function) yices_bvarray (C function) yices_bvashr (C function) yices_bvconcat (C function) yices_bvconcat2 (C function) yices_bvconst_from_array (C function) yices_bvconst_int32 (C function) yices_bvconst_int64 (C function) yices_bvconst_minus_one (C function) yices_bvconst_mpz (C function) yices_bvconst_one (C function) yices_bvconst_uint32 (C function) yices_bvconst_uint64 (C function) yices_bvconst_zero (C function) yices_bvdiv (C function) yices_bveq_atom (C function) yices_bvextract (C function) yices_bvge_atom (C function) yices_bvgt_atom (C function) yices_bvle_atom (C function) yices_bvlshr (C function) yices_bvlt_atom (C function) yices_bvmul (C function) yices_bvnand (C function) yices_bvneg (C function) yices_bvneq_atom (C function) yices_bvnor (C function) yices_bvnot (C function) yices_bvor (C function) yices_bvor2 (C function) yices_bvor3 (C function) yices_bvpower (C function) yices_bvproduct (C function) yices_bvrem (C function) yices_bvrepeat (C function) yices_bvsdiv (C function) yices_bvsge_atom (C function) yices_bvsgt_atom (C function) yices_bvshl (C function) yices_bvsle_atom (C function) yices_bvslt_atom (C function) yices_bvsmod (C function) yices_bvsquare (C function) yices_bvsrem (C function) yices_bvsub (C function) yices_bvsum (C function) yices_bvsum_component (C function) yices_bvtype_size (C function) yices_bvxnor (C function) yices_bvxor (C function) yices_bvxor2 (C function) yices_bvxor3 (C function) YICES_CEIL (C enum) yices_ceil (C function) yices_check_context (C function) yices_check_context_with_assumptions (C function) yices_check_formula (C function) yices_check_formulas (C function) yices_clear_error (C function) yices_clear_term_name (C function) yices_clear_type_name (C function) yices_compatible_types (C function) yices_constant (C function) YICES_CONSTRUCTOR_ERROR (C enum) yices_context_disable_option (C function) yices_context_enable_option (C function) yices_context_status (C function) yices_decref_term (C function) yices_decref_type (C function) yices_default_config_for_logic (C function) yices_default_params_for_context (C function) yices_delete_term_vector (C function) yices_delete_type_vector (C function) yices_delete_yval_vector (C function) yices_distinct (C function) YICES_DISTINCT_TERM (C enum) YICES_DIVIDES_ATOM (C enum) yices_divides_atom (C function) yices_division (C function) yices_eq (C function) YICES_EQ_TERM (C enum) yices_error_code (C function) yices_error_report (C function) yices_error_string (C function) yices_exists (C function) yices_exit (C function) yices_export_formula_to_dimacs (C function) yices_export_formulas_to_dimacs (C function) yices_false (C function) YICES_FLOOR (C enum) yices_floor (C function) yices_forall (C function) YICES_FORALL_TERM (C enum) yices_formula_true_in_model (C function) yices_formulas_true_in_model (C function) yices_free_config (C function) yices_free_context (C function) yices_free_model (C function) yices_free_param_record (C function) yices_free_string (C function) yices_function_type (C function) yices_function_type1 (C function) yices_function_type2 (C function) yices_function_type3 (C function) yices_garbage_collect (C function) YICES_GEN_BY_PROJ (C enum) YICES_GEN_BY_SUBST (C enum) YICES_GEN_DEFAULT (C enum) yices_gen_mode_t (C type) yices_generalize_model (C function) yices_generalize_model_array (C function) yices_get_algebraic_number_value (C function) yices_get_bool_value (C function) yices_get_bv_value (C function) yices_get_double_value (C function) yices_get_int32_value (C function) yices_get_int64_value (C function) yices_get_model (C function) yices_get_mpq_value (C function) yices_get_mpz_value (C function) yices_get_rational32_value (C function) yices_get_rational64_value (C function) yices_get_scalar_value (C function) yices_get_term_by_name (C function) yices_get_term_name (C function) yices_get_type_by_name (C function) yices_get_type_name (C function) yices_get_unsat_core (C function) yices_get_value (C function) yices_get_value_as_term (C function) yices_has_delegate (C function) yices_has_mcsat (C function) YICES_IDIV (C enum) yices_idiv (C function) yices_iff (C function) YICES_IMOD (C enum) yices_imod (C function) yices_implicant_for_formula (C function) yices_implicant_for_formulas (C function) yices_implies (C function) yices_incref_term (C function) yices_incref_type (C function) yices_init (C function) yices_init_term_vector (C function) yices_init_type_vector (C function) yices_init_yval_vector (C function) yices_int32 (C function) yices_int64 (C function) yices_int_type (C function) YICES_IS_INT_ATOM (C enum) yices_is_int_atom (C function) yices_is_thread_safe (C function) yices_ite (C function) YICES_ITE_TERM (C enum)

yices_lambda (C function) YICES_LAMBDA_TERM (C enum) YICES_MAX_ARITY (C macro) YICES_MAX_BVSIZE (C macro) YICES_MAX_DEGREE (C macro) YICES_MAX_TERMS (C macro) YICES_MAX_TYPES (C macro) YICES_MAX_VARS (C macro) yices_model_collect_defined_terms (C function) yices_model_from_map (C function) yices_model_term_array_support (C function) yices_model_term_support (C function) yices_model_to_string (C function) yices_mpq (C function) yices_mpz (C function) yices_mul (C function) yices_neg (C function) yices_neq (C function) yices_new_config (C function) yices_new_context (C function) yices_new_param_record (C function) yices_new_scalar_type (C function) yices_new_uninterpreted_term (C function) yices_new_uninterpreted_type (C function) yices_new_variable (C function) yices_not (C function) YICES_NOT_TERM (C enum) yices_num_posref_terms (C function) yices_num_posref_types (C function) yices_num_terms (C function) yices_num_types (C function) yices_or (C function) yices_or2 (C function) yices_or3 (C function) YICES_OR_TERM (C enum) yices_pair (C function) yices_parse_bvbin (C function) yices_parse_bvhex (C function) yices_parse_float (C function) yices_parse_rational (C function) yices_parse_term (C function) yices_parse_type (C function) yices_poly_int32 (C function) yices_poly_int64 (C function) yices_poly_mpq (C function) yices_poly_mpz (C function) yices_poly_rational32 (C function) yices_poly_rational64 (C function) yices_pop (C function) yices_power (C function) YICES_POWER_PRODUCT (C enum) yices_pp_model (C function) yices_pp_model_fd (C function) yices_pp_term (C function) yices_pp_term_array (C function) yices_pp_term_array_fd (C function) yices_pp_term_fd (C function) yices_pp_term_values (C function) yices_pp_term_values_fd (C function) yices_pp_type (C function) yices_pp_type_fd (C function) yices_print_error (C function) yices_print_error_fd (C function) yices_print_model (C function) yices_print_model_fd (C function) yices_print_term_values (C function) yices_print_term_values_fd (C function) yices_product (C function) yices_product_component (C function) yices_proj_arg (C function) yices_proj_index (C function) yices_push (C function) yices_rational32 (C function) yices_rational64 (C function) yices_rational_const_value (C function) YICES_RDIV (C enum) yices_real_type (C function) yices_redand (C function) yices_redcomp (C function) yices_redor (C function) yices_remove_term_name (C function) yices_remove_type_name (C function) yices_reset (C function) yices_reset_context (C function) yices_reset_term_vector (C function) yices_reset_type_vector (C function) yices_reset_yval_vector (C function) yices_rotate_left (C function) yices_rotate_right (C function) yices_scalar_const_value (C function) YICES_SCALAR_CONSTANT (C enum) yices_scalar_type_card (C function) yices_select (C function) YICES_SELECT_TERM (C enum) yices_set_config (C function) yices_set_out_of_mem_callback (C function) yices_set_param (C function) yices_set_term_name (C function) yices_set_type_name (C function) yices_shift_left0 (C function) yices_shift_left1 (C function) yices_shift_right0 (C function) yices_shift_right1 (C function) yices_sign_extend (C function) yices_square (C function) yices_stop_search (C function) yices_sub (C function) yices_subst_term (C function) yices_subst_term_array (C function) yices_sum (C function) yices_sum_component (C function) yices_term_array_value (C function) yices_term_bitsize (C function) yices_term_child (C function) yices_term_children (C function) yices_term_constructor (C function) yices_term_is_arithmetic (C function) yices_term_is_atomic (C function) yices_term_is_bitvector (C function) yices_term_is_bool (C function) yices_term_is_bvsum (C function) yices_term_is_composite (C function) yices_term_is_function (C function) yices_term_is_ground (C function) yices_term_is_int (C function) yices_term_is_product (C function) yices_term_is_projection (C function) yices_term_is_real (C function) yices_term_is_scalar (C function) yices_term_is_sum (C function) yices_term_is_tuple (C function) yices_term_num_children (C function) yices_term_to_string (C function) yices_test_subtype (C function) yices_triple (C function) yices_true (C function) yices_tuple (C function) YICES_TUPLE_TERM (C enum) yices_tuple_type (C function) yices_tuple_type1 (C function) yices_tuple_type2 (C function) yices_tuple_type3 (C function) yices_tuple_update (C function) yices_type_child (C function) yices_type_children (C function) yices_type_is_arithmetic (C function) yices_type_is_bitvector (C function) yices_type_is_bool (C function) yices_type_is_function (C function) yices_type_is_int (C function) yices_type_is_real (C function) yices_type_is_scalar (C function) yices_type_is_tuple (C function) yices_type_is_uninterpreted (C function) yices_type_num_children (C function) yices_type_of_term (C function) yices_type_to_string (C function) YICES_UNINTERPRETED_TERM (C enum) yices_update (C function) yices_update1 (C function) yices_update2 (C function) yices_update3 (C function) YICES_UPDATE_TERM (C enum) yices_val_bitsize (C function) yices_val_expand_function (C function) yices_val_expand_mapping (C function) yices_val_expand_tuple (C function) yices_val_function_arity (C function) yices_val_function_type (C function) yices_val_get_algebraic_number (C function) yices_val_get_bool (C function) yices_val_get_bv (C function) yices_val_get_double (C function) yices_val_get_int32 (C function) yices_val_get_int64 (C function) yices_val_get_mpq (C function) yices_val_get_mpz (C function) yices_val_get_rational32 (C function) yices_val_get_rational64 (C function) yices_val_get_scalar (C function) yices_val_is_int32 (C function) yices_val_is_int64 (C function) yices_val_is_integer (C function) yices_val_is_rational32 (C function) yices_val_is_rational64 (C function) yices_val_mapping_arity (C function) yices_val_tuple_arity (C function) YICES_VARIABLE (C enum) yices_version (C variable) yices_xor (C function) yices_xor2 (C function) yices_xor3 (C function) YICES_XOR_TERM (C enum) yices_zero (C function) yices_zero_extend (C function) YVAL_ALGEBRAIC (C enum) YVAL_BOOL (C enum) YVAL_BV (C enum) YVAL_FUNCTION (C enum) YVAL_INVALID_OP (C enum) YVAL_MAPPING (C enum) YVAL_NOT_SUPPORTED (C enum) YVAL_OVERFLOW (C enum) YVAL_RATIONAL (C enum) YVAL_SCALAR (C enum) yval_t (C type) yval_tag_t (C type) YVAL_TUPLE (C enum) YVAL_UNKNOWN (C enum) yval_vector_t (C type)