Index

_ | A | B | C | D | E | F | I | M | N | O | P | R | S | T | U | V | W | Y

_

__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_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_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_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)
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_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_data (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_clear_error (C function)
yices_clear_term_name (C function)
yices_clear_type_name (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_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_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_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_value (C function)
yices_get_value_as_term (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_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_from_map (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_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_term (C function)
yices_pp_term_array (C function)
yices_pp_type (C function)
yices_print_error (C function)
yices_print_model (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_memory_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_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_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_BOOL (C enum)
YVAL_BV (C enum)
YVAL_FUNCTION (C enum)
YVAL_INVALID_OP (C enum)
YVAL_MAPPING (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)