z3
  1. Overview
  2. Docs
type ptr
and symbol = ptr
and config = ptr
and context = ptr
and ast = ptr
and app = ast
and sort = ast
and func_decl = ast
and pattern = ast
and model = ptr
and literals = ptr
and constructor = ptr
and constructor_list = ptr
and solver = ptr
and solver_callback = ptr
and goal = ptr
and tactic = ptr
and params = ptr
and parser_context = ptr
and probe = ptr
and stats = ptr
and ast_vector = ptr
and ast_map = ptr
and apply_result = ptr
and func_interp = ptr
and func_entry = ptr
and fixedpoint = ptr
and optimize = ptr
and param_descrs = ptr
and rcf_num = ptr
val set_internal_error_handler : ptr -> unit
val global_param_set : string -> string -> unit
val global_param_reset_all : unit -> unit
val global_param_get : string -> bool * string
val mk_config : unit -> config
val del_config : config -> unit
val set_param_value : config -> string -> string -> unit
val mk_context : config -> context
val mk_context_rc : config -> context
val del_context : context -> unit
val inc_ref : context -> ast -> unit
val dec_ref : context -> ast -> unit
val update_param_value : context -> string -> string -> unit
val get_global_param_descrs : context -> param_descrs
val interrupt : context -> unit
val enable_concurrent_dec_ref : context -> unit
val mk_params : context -> params
val params_inc_ref : context -> params -> unit
val params_dec_ref : context -> params -> unit
val params_set_bool : context -> params -> symbol -> bool -> unit
val params_set_uint : context -> params -> symbol -> int -> unit
val params_set_double : context -> params -> symbol -> float -> unit
val params_set_symbol : context -> params -> symbol -> symbol -> unit
val params_to_string : context -> params -> string
val params_validate : context -> params -> param_descrs -> unit
val param_descrs_inc_ref : context -> param_descrs -> unit
val param_descrs_dec_ref : context -> param_descrs -> unit
val param_descrs_get_kind : context -> param_descrs -> symbol -> int
val param_descrs_size : context -> param_descrs -> int
val param_descrs_get_name : context -> param_descrs -> int -> symbol
val param_descrs_get_documentation : context -> param_descrs -> symbol -> string
val param_descrs_to_string : context -> param_descrs -> string
val mk_int_symbol : context -> int -> symbol
val mk_string_symbol : context -> string -> symbol
val mk_uninterpreted_sort : context -> symbol -> sort
val mk_bool_sort : context -> sort
val mk_int_sort : context -> sort
val mk_real_sort : context -> sort
val mk_bv_sort : context -> int -> sort
val mk_finite_domain_sort : context -> symbol -> int64 -> sort
val mk_array_sort : context -> sort -> sort -> sort
val mk_array_sort_n : context -> int -> sort list -> sort -> sort
val mk_tuple_sort : context -> symbol -> int -> symbol list -> sort list -> sort * ptr * func_decl list
val mk_enumeration_sort : context -> symbol -> int -> symbol list -> sort * func_decl list * func_decl list
val mk_list_sort : context -> symbol -> sort -> sort * ptr * ptr * ptr * ptr * ptr * ptr
val mk_constructor : context -> symbol -> symbol -> int -> symbol list -> sort list -> int list -> constructor
val del_constructor : context -> constructor -> unit
val mk_datatype : context -> symbol -> int -> constructor list -> sort * constructor list
val mk_datatype_sort : context -> symbol -> sort
val mk_constructor_list : context -> int -> constructor list -> constructor_list
val del_constructor_list : context -> constructor_list -> unit
val mk_datatypes : context -> int -> symbol list -> constructor_list list -> sort list * constructor_list list
val query_constructor : context -> constructor -> int -> ptr * ptr * func_decl list
val mk_func_decl : context -> symbol -> int -> sort list -> sort -> func_decl
val mk_app : context -> func_decl -> int -> ast list -> ast
val mk_const : context -> symbol -> sort -> ast
val mk_fresh_func_decl : context -> string -> int -> sort list -> sort -> func_decl
val mk_fresh_const : context -> string -> sort -> ast
val mk_rec_func_decl : context -> symbol -> int -> sort list -> sort -> func_decl
val add_rec_def : context -> func_decl -> int -> ast list -> ast -> unit
val mk_true : context -> ast
val mk_false : context -> ast
val mk_eq : context -> ast -> ast -> ast
val mk_distinct : context -> int -> ast list -> ast
val mk_not : context -> ast -> ast
val mk_ite : context -> ast -> ast -> ast -> ast
val mk_iff : context -> ast -> ast -> ast
val mk_implies : context -> ast -> ast -> ast
val mk_xor : context -> ast -> ast -> ast
val mk_and : context -> int -> ast list -> ast
val mk_or : context -> int -> ast list -> ast
val mk_add : context -> int -> ast list -> ast
val mk_mul : context -> int -> ast list -> ast
val mk_sub : context -> int -> ast list -> ast
val mk_unary_minus : context -> ast -> ast
val mk_div : context -> ast -> ast -> ast
val mk_mod : context -> ast -> ast -> ast
val mk_rem : context -> ast -> ast -> ast
val mk_power : context -> ast -> ast -> ast
val mk_lt : context -> ast -> ast -> ast
val mk_le : context -> ast -> ast -> ast
val mk_gt : context -> ast -> ast -> ast
val mk_ge : context -> ast -> ast -> ast
val mk_divides : context -> ast -> ast -> ast
val mk_int2real : context -> ast -> ast
val mk_real2int : context -> ast -> ast
val mk_is_int : context -> ast -> ast
val mk_bvnot : context -> ast -> ast
val mk_bvredand : context -> ast -> ast
val mk_bvredor : context -> ast -> ast
val mk_bvand : context -> ast -> ast -> ast
val mk_bvor : context -> ast -> ast -> ast
val mk_bvxor : context -> ast -> ast -> ast
val mk_bvnand : context -> ast -> ast -> ast
val mk_bvnor : context -> ast -> ast -> ast
val mk_bvxnor : context -> ast -> ast -> ast
val mk_bvneg : context -> ast -> ast
val mk_bvadd : context -> ast -> ast -> ast
val mk_bvsub : context -> ast -> ast -> ast
val mk_bvmul : context -> ast -> ast -> ast
val mk_bvudiv : context -> ast -> ast -> ast
val mk_bvsdiv : context -> ast -> ast -> ast
val mk_bvurem : context -> ast -> ast -> ast
val mk_bvsrem : context -> ast -> ast -> ast
val mk_bvsmod : context -> ast -> ast -> ast
val mk_bvult : context -> ast -> ast -> ast
val mk_bvslt : context -> ast -> ast -> ast
val mk_bvule : context -> ast -> ast -> ast
val mk_bvsle : context -> ast -> ast -> ast
val mk_bvuge : context -> ast -> ast -> ast
val mk_bvsge : context -> ast -> ast -> ast
val mk_bvugt : context -> ast -> ast -> ast
val mk_bvsgt : context -> ast -> ast -> ast
val mk_concat : context -> ast -> ast -> ast
val mk_extract : context -> int -> int -> ast -> ast
val mk_sign_ext : context -> int -> ast -> ast
val mk_zero_ext : context -> int -> ast -> ast
val mk_repeat : context -> int -> ast -> ast
val mk_bit2bool : context -> int -> ast -> ast
val mk_bvshl : context -> ast -> ast -> ast
val mk_bvlshr : context -> ast -> ast -> ast
val mk_bvashr : context -> ast -> ast -> ast
val mk_rotate_left : context -> int -> ast -> ast
val mk_rotate_right : context -> int -> ast -> ast
val mk_ext_rotate_left : context -> ast -> ast -> ast
val mk_ext_rotate_right : context -> ast -> ast -> ast
val mk_int2bv : context -> int -> ast -> ast
val mk_bv2int : context -> ast -> bool -> ast
val mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast
val mk_bvadd_no_underflow : context -> ast -> ast -> ast
val mk_bvsub_no_overflow : context -> ast -> ast -> ast
val mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast
val mk_bvsdiv_no_overflow : context -> ast -> ast -> ast
val mk_bvneg_no_overflow : context -> ast -> ast
val mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast
val mk_bvmul_no_underflow : context -> ast -> ast -> ast
val mk_select : context -> ast -> ast -> ast
val mk_select_n : context -> ast -> int -> ast list -> ast
val mk_store : context -> ast -> ast -> ast -> ast
val mk_store_n : context -> ast -> int -> ast list -> ast -> ast
val mk_const_array : context -> sort -> ast -> ast
val mk_map : context -> func_decl -> int -> ast list -> ast
val mk_array_default : context -> ast -> ast
val mk_as_array : context -> func_decl -> ast
val mk_set_has_size : context -> ast -> ast -> ast
val mk_set_sort : context -> sort -> sort
val mk_empty_set : context -> sort -> ast
val mk_full_set : context -> sort -> ast
val mk_set_add : context -> ast -> ast -> ast
val mk_set_del : context -> ast -> ast -> ast
val mk_set_union : context -> int -> ast list -> ast
val mk_set_intersect : context -> int -> ast list -> ast
val mk_set_difference : context -> ast -> ast -> ast
val mk_set_complement : context -> ast -> ast
val mk_set_member : context -> ast -> ast -> ast
val mk_set_subset : context -> ast -> ast -> ast
val mk_array_ext : context -> ast -> ast -> ast
val mk_numeral : context -> string -> sort -> ast
val mk_real : context -> int -> int -> ast
val mk_int : context -> int -> sort -> ast
val mk_unsigned_int : context -> int -> sort -> ast
val mk_int64 : context -> int64 -> sort -> ast
val mk_unsigned_int64 : context -> int64 -> sort -> ast
val mk_bv_numeral : context -> int -> bool list -> ast
val mk_seq_sort : context -> sort -> sort
val is_seq_sort : context -> sort -> bool
val get_seq_sort_basis : context -> sort -> sort
val mk_re_sort : context -> sort -> sort
val is_re_sort : context -> sort -> bool
val get_re_sort_basis : context -> sort -> sort
val mk_string_sort : context -> sort
val mk_char_sort : context -> sort
val is_string_sort : context -> sort -> bool
val is_char_sort : context -> sort -> bool
val mk_string : context -> string -> ast
val mk_lstring : context -> int -> string -> ast
val mk_u32string : context -> int -> int list -> ast
val is_string : context -> ast -> bool
val get_string : context -> ast -> string
val get_lstring : context -> ast -> string * int
val get_string_length : context -> ast -> int
val get_string_contents : context -> ast -> int -> int list
val mk_seq_empty : context -> sort -> ast
val mk_seq_unit : context -> ast -> ast
val mk_seq_concat : context -> int -> ast list -> ast
val mk_seq_prefix : context -> ast -> ast -> ast
val mk_seq_suffix : context -> ast -> ast -> ast
val mk_seq_contains : context -> ast -> ast -> ast
val mk_str_lt : context -> ast -> ast -> ast
val mk_str_le : context -> ast -> ast -> ast
val mk_seq_extract : context -> ast -> ast -> ast -> ast
val mk_seq_replace : context -> ast -> ast -> ast -> ast
val mk_seq_at : context -> ast -> ast -> ast
val mk_seq_nth : context -> ast -> ast -> ast
val mk_seq_length : context -> ast -> ast
val mk_seq_index : context -> ast -> ast -> ast -> ast
val mk_seq_last_index : context -> ast -> ast -> ast
val mk_str_to_int : context -> ast -> ast
val mk_int_to_str : context -> ast -> ast
val mk_string_to_code : context -> ast -> ast
val mk_string_from_code : context -> ast -> ast
val mk_ubv_to_str : context -> ast -> ast
val mk_sbv_to_str : context -> ast -> ast
val mk_seq_to_re : context -> ast -> ast
val mk_seq_in_re : context -> ast -> ast -> ast
val mk_re_plus : context -> ast -> ast
val mk_re_star : context -> ast -> ast
val mk_re_option : context -> ast -> ast
val mk_re_union : context -> int -> ast list -> ast
val mk_re_concat : context -> int -> ast list -> ast
val mk_re_range : context -> ast -> ast -> ast
val mk_re_allchar : context -> sort -> ast
val mk_re_loop : context -> ast -> int -> int -> ast
val mk_re_power : context -> ast -> int -> ast
val mk_re_intersect : context -> int -> ast list -> ast
val mk_re_complement : context -> ast -> ast
val mk_re_diff : context -> ast -> ast -> ast
val mk_re_empty : context -> sort -> ast
val mk_re_full : context -> sort -> ast
val mk_char : context -> int -> ast
val mk_char_le : context -> ast -> ast -> ast
val mk_char_to_int : context -> ast -> ast
val mk_char_to_bv : context -> ast -> ast
val mk_char_from_bv : context -> ast -> ast
val mk_char_is_digit : context -> ast -> ast
val mk_linear_order : context -> sort -> int -> func_decl
val mk_partial_order : context -> sort -> int -> func_decl
val mk_piecewise_linear_order : context -> sort -> int -> func_decl
val mk_tree_order : context -> sort -> int -> func_decl
val mk_transitive_closure : context -> func_decl -> func_decl
val mk_pattern : context -> int -> ast list -> pattern
val mk_bound : context -> int -> sort -> ast
val mk_forall : context -> int -> int -> pattern list -> int -> sort list -> symbol list -> ast -> ast
val mk_exists : context -> int -> int -> pattern list -> int -> sort list -> symbol list -> ast -> ast
val mk_quantifier : context -> bool -> int -> int -> pattern list -> int -> sort list -> symbol list -> ast -> ast
val mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> int -> pattern list -> int -> ast list -> int -> sort list -> symbol list -> ast -> ast
val mk_forall_const : context -> int -> int -> app list -> int -> pattern list -> ast -> ast
val mk_exists_const : context -> int -> int -> app list -> int -> pattern list -> ast -> ast
val mk_quantifier_const : context -> bool -> int -> int -> app list -> int -> pattern list -> ast -> ast
val mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> int -> app list -> int -> pattern list -> int -> ast list -> ast -> ast
val mk_lambda : context -> int -> sort list -> symbol list -> ast -> ast
val mk_lambda_const : context -> int -> app list -> ast -> ast
val get_symbol_kind : context -> symbol -> int
val get_symbol_int : context -> symbol -> int
val get_symbol_string : context -> symbol -> string
val get_sort_name : context -> sort -> symbol
val get_sort_id : context -> sort -> int
val sort_to_ast : context -> sort -> ast
val is_eq_sort : context -> sort -> sort -> bool
val get_sort_kind : context -> sort -> int
val get_bv_sort_size : context -> sort -> int
val get_finite_domain_sort_size : context -> sort -> bool * int64
val get_array_sort_domain : context -> sort -> sort
val get_array_sort_domain_n : context -> sort -> int -> sort
val get_array_sort_range : context -> sort -> sort
val get_tuple_sort_mk_decl : context -> sort -> func_decl
val get_tuple_sort_num_fields : context -> sort -> int
val get_tuple_sort_field_decl : context -> sort -> int -> func_decl
val get_datatype_sort_num_constructors : context -> sort -> int
val get_datatype_sort_constructor : context -> sort -> int -> func_decl
val get_datatype_sort_recognizer : context -> sort -> int -> func_decl
val get_datatype_sort_constructor_accessor : context -> sort -> int -> int -> func_decl
val datatype_update_field : context -> func_decl -> ast -> ast -> ast
val get_relation_arity : context -> sort -> int
val get_relation_column : context -> sort -> int -> sort
val mk_atmost : context -> int -> ast list -> int -> ast
val mk_atleast : context -> int -> ast list -> int -> ast
val mk_pble : context -> int -> ast list -> int list -> int -> ast
val mk_pbge : context -> int -> ast list -> int list -> int -> ast
val mk_pbeq : context -> int -> ast list -> int list -> int -> ast
val func_decl_to_ast : context -> func_decl -> ast
val is_eq_func_decl : context -> func_decl -> func_decl -> bool
val get_func_decl_id : context -> func_decl -> int
val get_decl_name : context -> func_decl -> symbol
val get_decl_kind : context -> func_decl -> int
val get_domain_size : context -> func_decl -> int
val get_arity : context -> func_decl -> int
val get_domain : context -> func_decl -> int -> sort
val get_range : context -> func_decl -> sort
val get_decl_num_parameters : context -> func_decl -> int
val get_decl_parameter_kind : context -> func_decl -> int -> int
val get_decl_int_parameter : context -> func_decl -> int -> int
val get_decl_double_parameter : context -> func_decl -> int -> float
val get_decl_symbol_parameter : context -> func_decl -> int -> symbol
val get_decl_sort_parameter : context -> func_decl -> int -> sort
val get_decl_ast_parameter : context -> func_decl -> int -> ast
val get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl
val get_decl_rational_parameter : context -> func_decl -> int -> string
val app_to_ast : context -> app -> ast
val get_app_decl : context -> app -> func_decl
val get_app_num_args : context -> app -> int
val get_app_arg : context -> app -> int -> ast
val is_eq_ast : context -> ast -> ast -> bool
val get_ast_id : context -> ast -> int
val get_ast_hash : context -> ast -> int
val get_sort : context -> ast -> sort
val is_well_sorted : context -> ast -> bool
val get_bool_value : context -> ast -> int
val get_ast_kind : context -> ast -> int
val is_app : context -> ast -> bool
val is_numeral_ast : context -> ast -> bool
val is_algebraic_number : context -> ast -> bool
val to_app : context -> ast -> app
val to_func_decl : context -> ast -> func_decl
val get_numeral_string : context -> ast -> string
val get_numeral_binary_string : context -> ast -> string
val get_numeral_decimal_string : context -> ast -> int -> string
val get_numeral_double : context -> ast -> float
val get_numerator : context -> ast -> ast
val get_denominator : context -> ast -> ast
val get_numeral_small : context -> ast -> bool * int64 * int64
val get_numeral_int : context -> ast -> bool * int
val get_numeral_uint : context -> ast -> bool * int
val get_numeral_uint64 : context -> ast -> bool * int64
val get_numeral_int64 : context -> ast -> bool * int64
val get_numeral_rational_int64 : context -> ast -> bool * int64 * int64
val get_algebraic_number_lower : context -> ast -> int -> ast
val get_algebraic_number_upper : context -> ast -> int -> ast
val pattern_to_ast : context -> pattern -> ast
val get_pattern_num_terms : context -> pattern -> int
val get_pattern : context -> pattern -> int -> ast
val get_index_value : context -> ast -> int
val is_quantifier_forall : context -> ast -> bool
val is_quantifier_exists : context -> ast -> bool
val is_lambda : context -> ast -> bool
val get_quantifier_weight : context -> ast -> int
val get_quantifier_num_patterns : context -> ast -> int
val get_quantifier_pattern_ast : context -> ast -> int -> pattern
val get_quantifier_num_no_patterns : context -> ast -> int
val get_quantifier_no_pattern_ast : context -> ast -> int -> ast
val get_quantifier_num_bound : context -> ast -> int
val get_quantifier_bound_name : context -> ast -> int -> symbol
val get_quantifier_bound_sort : context -> ast -> int -> sort
val get_quantifier_body : context -> ast -> ast
val simplify : context -> ast -> ast
val simplify_ex : context -> ast -> params -> ast
val simplify_get_help : context -> string
val simplify_get_param_descrs : context -> param_descrs
val update_term : context -> ast -> int -> ast list -> ast
val substitute : context -> ast -> int -> ast list -> ast list -> ast
val substitute_vars : context -> ast -> int -> ast list -> ast
val substitute_funs : context -> ast -> int -> func_decl list -> ast list -> ast
val translate : context -> ast -> context -> ast
val mk_model : context -> model
val model_inc_ref : context -> model -> unit
val model_dec_ref : context -> model -> unit
val model_eval : context -> model -> ast -> bool -> bool * ptr
val model_get_const_interp : context -> model -> func_decl -> ast
val model_has_interp : context -> model -> func_decl -> bool
val model_get_func_interp : context -> model -> func_decl -> func_interp
val model_get_num_consts : context -> model -> int
val model_get_const_decl : context -> model -> int -> func_decl
val model_get_num_funcs : context -> model -> int
val model_get_func_decl : context -> model -> int -> func_decl
val model_get_num_sorts : context -> model -> int
val model_get_sort : context -> model -> int -> sort
val model_get_sort_universe : context -> model -> sort -> ast_vector
val model_translate : context -> model -> context -> model
val is_as_array : context -> ast -> bool
val get_as_array_func_decl : context -> ast -> func_decl
val add_func_interp : context -> model -> func_decl -> ast -> func_interp
val add_const_interp : context -> model -> func_decl -> ast -> unit
val func_interp_inc_ref : context -> func_interp -> unit
val func_interp_dec_ref : context -> func_interp -> unit
val func_interp_get_num_entries : context -> func_interp -> int
val func_interp_get_entry : context -> func_interp -> int -> func_entry
val func_interp_get_else : context -> func_interp -> ast
val func_interp_set_else : context -> func_interp -> ast -> unit
val func_interp_get_arity : context -> func_interp -> int
val func_interp_add_entry : context -> func_interp -> ast_vector -> ast -> unit
val func_entry_inc_ref : context -> func_entry -> unit
val func_entry_dec_ref : context -> func_entry -> unit
val func_entry_get_value : context -> func_entry -> ast
val func_entry_get_num_args : context -> func_entry -> int
val func_entry_get_arg : context -> func_entry -> int -> ast
val open_log : string -> int
val append_log : string -> unit
val close_log : unit -> unit
val toggle_warning_messages : bool -> unit
val set_ast_print_mode : context -> int -> unit
val ast_to_string : context -> ast -> string
val pattern_to_string : context -> pattern -> string
val sort_to_string : context -> sort -> string
val func_decl_to_string : context -> func_decl -> string
val model_to_string : context -> model -> string
val benchmark_to_smtlib_string : context -> string -> string -> string -> string -> int -> ast list -> ast -> string
val parse_smtlib2_string : context -> string -> int -> symbol list -> sort list -> int -> symbol list -> func_decl list -> ast_vector
val parse_smtlib2_file : context -> string -> int -> symbol list -> sort list -> int -> symbol list -> func_decl list -> ast_vector
val eval_smtlib2_string : context -> string -> string
val mk_parser_context : context -> parser_context
val parser_context_inc_ref : context -> parser_context -> unit
val parser_context_dec_ref : context -> parser_context -> unit
val parser_context_add_sort : context -> parser_context -> sort -> unit
val parser_context_add_decl : context -> parser_context -> func_decl -> unit
val parser_context_from_string : context -> parser_context -> string -> ast_vector
val get_error_code : context -> int
val set_error : context -> int -> unit
val get_error_msg : context -> int -> string
val get_version : unit -> int * int * int * int
val get_full_version : unit -> string
val enable_trace : string -> unit
val disable_trace : string -> unit
val reset_memory : unit -> unit
val finalize_memory : unit -> unit
val mk_goal : context -> bool -> bool -> bool -> goal
val goal_inc_ref : context -> goal -> unit
val goal_dec_ref : context -> goal -> unit
val goal_precision : context -> goal -> int
val goal_assert : context -> goal -> ast -> unit
val goal_inconsistent : context -> goal -> bool
val goal_depth : context -> goal -> int
val goal_reset : context -> goal -> unit
val goal_size : context -> goal -> int
val goal_formula : context -> goal -> int -> ast
val goal_num_exprs : context -> goal -> int
val goal_is_decided_sat : context -> goal -> bool
val goal_is_decided_unsat : context -> goal -> bool
val goal_translate : context -> goal -> context -> goal
val goal_convert_model : context -> goal -> model -> model
val goal_to_string : context -> goal -> string
val goal_to_dimacs_string : context -> goal -> bool -> string
val mk_tactic : context -> string -> tactic
val tactic_inc_ref : context -> tactic -> unit
val tactic_dec_ref : context -> tactic -> unit
val mk_probe : context -> string -> probe
val probe_inc_ref : context -> probe -> unit
val probe_dec_ref : context -> probe -> unit
val tactic_and_then : context -> tactic -> tactic -> tactic
val tactic_or_else : context -> tactic -> tactic -> tactic
val tactic_par_or : context -> int -> tactic list -> tactic
val tactic_par_and_then : context -> tactic -> tactic -> tactic
val tactic_try_for : context -> tactic -> int -> tactic
val tactic_when : context -> probe -> tactic -> tactic
val tactic_cond : context -> probe -> tactic -> tactic -> tactic
val tactic_repeat : context -> tactic -> int -> tactic
val tactic_skip : context -> tactic
val tactic_fail : context -> tactic
val tactic_fail_if : context -> probe -> tactic
val tactic_fail_if_not_decided : context -> tactic
val tactic_using_params : context -> tactic -> params -> tactic
val probe_const : context -> float -> probe
val probe_lt : context -> probe -> probe -> probe
val probe_gt : context -> probe -> probe -> probe
val probe_le : context -> probe -> probe -> probe
val probe_ge : context -> probe -> probe -> probe
val probe_eq : context -> probe -> probe -> probe
val probe_and : context -> probe -> probe -> probe
val probe_or : context -> probe -> probe -> probe
val probe_not : context -> probe -> probe
val get_num_tactics : context -> int
val get_tactic_name : context -> int -> string
val get_num_probes : context -> int
val get_probe_name : context -> int -> string
val tactic_get_help : context -> tactic -> string
val tactic_get_param_descrs : context -> tactic -> param_descrs
val tactic_get_descr : context -> string -> string
val probe_get_descr : context -> string -> string
val probe_apply : context -> probe -> goal -> float
val tactic_apply : context -> tactic -> goal -> apply_result
val tactic_apply_ex : context -> tactic -> goal -> params -> apply_result
val apply_result_inc_ref : context -> apply_result -> unit
val apply_result_dec_ref : context -> apply_result -> unit
val apply_result_to_string : context -> apply_result -> string
val apply_result_get_num_subgoals : context -> apply_result -> int
val apply_result_get_subgoal : context -> apply_result -> int -> goal
val mk_solver : context -> solver
val mk_simple_solver : context -> solver
val mk_solver_for_logic : context -> symbol -> solver
val mk_solver_from_tactic : context -> tactic -> solver
val solver_translate : context -> solver -> context -> solver
val solver_import_model_converter : context -> solver -> solver -> unit
val solver_get_help : context -> solver -> string
val solver_get_param_descrs : context -> solver -> param_descrs
val solver_set_params : context -> solver -> params -> unit
val solver_inc_ref : context -> solver -> unit
val solver_dec_ref : context -> solver -> unit
val solver_interrupt : context -> solver -> unit
val solver_push : context -> solver -> unit
val solver_pop : context -> solver -> int -> unit
val solver_reset : context -> solver -> unit
val solver_get_num_scopes : context -> solver -> int
val solver_assert : context -> solver -> ast -> unit
val solver_assert_and_track : context -> solver -> ast -> ast -> unit
val solver_from_file : context -> solver -> string -> unit
val solver_from_string : context -> solver -> string -> unit
val solver_get_assertions : context -> solver -> ast_vector
val solver_get_units : context -> solver -> ast_vector
val solver_get_trail : context -> solver -> ast_vector
val solver_get_non_units : context -> solver -> ast_vector
val solver_get_levels : context -> solver -> ast_vector -> int -> int list -> unit
val solver_next_split : context -> solver_callback -> ast -> int -> int -> unit
val solver_propagate_declare : context -> symbol -> int -> sort list -> sort -> func_decl
val solver_propagate_register : context -> solver -> ast -> unit
val solver_propagate_register_cb : context -> solver_callback -> ast -> unit
val solver_propagate_consequence : context -> solver_callback -> int -> ast list -> int -> ast list -> ast list -> ast -> unit
val solver_check : context -> solver -> int
val solver_check_assumptions : context -> solver -> int -> ast list -> int
val get_implied_equalities : context -> solver -> int -> ast list -> int * int list
val solver_get_consequences : context -> solver -> ast_vector -> ast_vector -> ast_vector -> int
val solver_cube : context -> solver -> ast_vector -> int -> ast_vector
val solver_get_model : context -> solver -> model
val solver_get_proof : context -> solver -> ast
val solver_get_unsat_core : context -> solver -> ast_vector
val solver_get_reason_unknown : context -> solver -> string
val solver_get_statistics : context -> solver -> stats
val solver_to_string : context -> solver -> string
val solver_to_dimacs_string : context -> solver -> bool -> string
val stats_to_string : context -> stats -> string
val stats_inc_ref : context -> stats -> unit
val stats_dec_ref : context -> stats -> unit
val stats_size : context -> stats -> int
val stats_get_key : context -> stats -> int -> string
val stats_is_uint : context -> stats -> int -> bool
val stats_is_double : context -> stats -> int -> bool
val stats_get_uint_value : context -> stats -> int -> int
val stats_get_double_value : context -> stats -> int -> float
val get_estimated_alloc_size : unit -> int64
val mk_ast_vector : context -> ast_vector
val ast_vector_inc_ref : context -> ast_vector -> unit
val ast_vector_dec_ref : context -> ast_vector -> unit
val ast_vector_size : context -> ast_vector -> int
val ast_vector_get : context -> ast_vector -> int -> ast
val ast_vector_set : context -> ast_vector -> int -> ast -> unit
val ast_vector_resize : context -> ast_vector -> int -> unit
val ast_vector_push : context -> ast_vector -> ast -> unit
val ast_vector_translate : context -> ast_vector -> context -> ast_vector
val ast_vector_to_string : context -> ast_vector -> string
val mk_ast_map : context -> ast_map
val ast_map_inc_ref : context -> ast_map -> unit
val ast_map_dec_ref : context -> ast_map -> unit
val ast_map_contains : context -> ast_map -> ast -> bool
val ast_map_find : context -> ast_map -> ast -> ast
val ast_map_insert : context -> ast_map -> ast -> ast -> unit
val ast_map_erase : context -> ast_map -> ast -> unit
val ast_map_reset : context -> ast_map -> unit
val ast_map_size : context -> ast_map -> int
val ast_map_keys : context -> ast_map -> ast_vector
val ast_map_to_string : context -> ast_map -> string
val algebraic_is_value : context -> ast -> bool
val algebraic_is_pos : context -> ast -> bool
val algebraic_is_neg : context -> ast -> bool
val algebraic_is_zero : context -> ast -> bool
val algebraic_sign : context -> ast -> int
val algebraic_add : context -> ast -> ast -> ast
val algebraic_sub : context -> ast -> ast -> ast
val algebraic_mul : context -> ast -> ast -> ast
val algebraic_div : context -> ast -> ast -> ast
val algebraic_root : context -> ast -> int -> ast
val algebraic_power : context -> ast -> int -> ast
val algebraic_lt : context -> ast -> ast -> bool
val algebraic_gt : context -> ast -> ast -> bool
val algebraic_le : context -> ast -> ast -> bool
val algebraic_ge : context -> ast -> ast -> bool
val algebraic_eq : context -> ast -> ast -> bool
val algebraic_neq : context -> ast -> ast -> bool
val algebraic_roots : context -> ast -> int -> ast list -> ast_vector
val algebraic_eval : context -> ast -> int -> ast list -> int
val algebraic_get_poly : context -> ast -> ast_vector
val algebraic_get_i : context -> ast -> int
val polynomial_subresultants : context -> ast -> ast -> ast -> ast_vector
val rcf_del : context -> rcf_num -> unit
val rcf_mk_rational : context -> string -> rcf_num
val rcf_mk_small_int : context -> int -> rcf_num
val rcf_mk_pi : context -> rcf_num
val rcf_mk_e : context -> rcf_num
val rcf_mk_infinitesimal : context -> rcf_num
val rcf_mk_roots : context -> int -> rcf_num list -> int * rcf_num list
val rcf_add : context -> rcf_num -> rcf_num -> rcf_num
val rcf_sub : context -> rcf_num -> rcf_num -> rcf_num
val rcf_mul : context -> rcf_num -> rcf_num -> rcf_num
val rcf_div : context -> rcf_num -> rcf_num -> rcf_num
val rcf_neg : context -> rcf_num -> rcf_num
val rcf_inv : context -> rcf_num -> rcf_num
val rcf_power : context -> rcf_num -> int -> rcf_num
val rcf_lt : context -> rcf_num -> rcf_num -> bool
val rcf_gt : context -> rcf_num -> rcf_num -> bool
val rcf_le : context -> rcf_num -> rcf_num -> bool
val rcf_ge : context -> rcf_num -> rcf_num -> bool
val rcf_eq : context -> rcf_num -> rcf_num -> bool
val rcf_neq : context -> rcf_num -> rcf_num -> bool
val rcf_num_to_string : context -> rcf_num -> bool -> bool -> string
val rcf_num_to_decimal_string : context -> rcf_num -> int -> string
val rcf_get_numerator_denominator : context -> rcf_num -> ptr * ptr
val mk_fixedpoint : context -> fixedpoint
val fixedpoint_inc_ref : context -> fixedpoint -> unit
val fixedpoint_dec_ref : context -> fixedpoint -> unit
val fixedpoint_add_rule : context -> fixedpoint -> ast -> symbol -> unit
val fixedpoint_add_fact : context -> fixedpoint -> func_decl -> int -> int list -> unit
val fixedpoint_assert : context -> fixedpoint -> ast -> unit
val fixedpoint_query : context -> fixedpoint -> ast -> int
val fixedpoint_query_relations : context -> fixedpoint -> int -> func_decl list -> int
val fixedpoint_get_answer : context -> fixedpoint -> ast
val fixedpoint_get_reason_unknown : context -> fixedpoint -> string
val fixedpoint_update_rule : context -> fixedpoint -> ast -> symbol -> unit
val fixedpoint_get_num_levels : context -> fixedpoint -> func_decl -> int
val fixedpoint_get_cover_delta : context -> fixedpoint -> int -> func_decl -> ast
val fixedpoint_add_cover : context -> fixedpoint -> int -> func_decl -> ast -> unit
val fixedpoint_get_statistics : context -> fixedpoint -> stats
val fixedpoint_register_relation : context -> fixedpoint -> func_decl -> unit
val fixedpoint_set_predicate_representation : context -> fixedpoint -> func_decl -> int -> symbol list -> unit
val fixedpoint_get_rules : context -> fixedpoint -> ast_vector
val fixedpoint_get_assertions : context -> fixedpoint -> ast_vector
val fixedpoint_set_params : context -> fixedpoint -> params -> unit
val fixedpoint_get_help : context -> fixedpoint -> string
val fixedpoint_get_param_descrs : context -> fixedpoint -> param_descrs
val fixedpoint_to_string : context -> fixedpoint -> int -> ast list -> string
val fixedpoint_from_string : context -> fixedpoint -> string -> ast_vector
val fixedpoint_from_file : context -> fixedpoint -> string -> ast_vector
val mk_optimize : context -> optimize
val optimize_inc_ref : context -> optimize -> unit
val optimize_dec_ref : context -> optimize -> unit
val optimize_assert : context -> optimize -> ast -> unit
val optimize_assert_and_track : context -> optimize -> ast -> ast -> unit
val optimize_assert_soft : context -> optimize -> ast -> string -> symbol -> int
val optimize_maximize : context -> optimize -> ast -> int
val optimize_minimize : context -> optimize -> ast -> int
val optimize_push : context -> optimize -> unit
val optimize_pop : context -> optimize -> unit
val optimize_check : context -> optimize -> int -> ast list -> int
val optimize_get_reason_unknown : context -> optimize -> string
val optimize_get_model : context -> optimize -> model
val optimize_get_unsat_core : context -> optimize -> ast_vector
val optimize_set_params : context -> optimize -> params -> unit
val optimize_get_param_descrs : context -> optimize -> param_descrs
val optimize_get_lower : context -> optimize -> int -> ast
val optimize_get_upper : context -> optimize -> int -> ast
val optimize_get_lower_as_vector : context -> optimize -> int -> ast_vector
val optimize_get_upper_as_vector : context -> optimize -> int -> ast_vector
val optimize_to_string : context -> optimize -> string
val optimize_from_string : context -> optimize -> string -> unit
val optimize_from_file : context -> optimize -> string -> unit
val optimize_get_help : context -> optimize -> string
val optimize_get_statistics : context -> optimize -> stats
val optimize_get_assertions : context -> optimize -> ast_vector
val optimize_get_objectives : context -> optimize -> ast_vector
val mk_fpa_rounding_mode_sort : context -> sort
val mk_fpa_round_nearest_ties_to_even : context -> ast
val mk_fpa_rne : context -> ast
val mk_fpa_round_nearest_ties_to_away : context -> ast
val mk_fpa_rna : context -> ast
val mk_fpa_round_toward_positive : context -> ast
val mk_fpa_rtp : context -> ast
val mk_fpa_round_toward_negative : context -> ast
val mk_fpa_rtn : context -> ast
val mk_fpa_round_toward_zero : context -> ast
val mk_fpa_rtz : context -> ast
val mk_fpa_sort : context -> int -> int -> sort
val mk_fpa_sort_half : context -> sort
val mk_fpa_sort_16 : context -> sort
val mk_fpa_sort_single : context -> sort
val mk_fpa_sort_32 : context -> sort
val mk_fpa_sort_double : context -> sort
val mk_fpa_sort_64 : context -> sort
val mk_fpa_sort_quadruple : context -> sort
val mk_fpa_sort_128 : context -> sort
val mk_fpa_nan : context -> sort -> ast
val mk_fpa_inf : context -> sort -> bool -> ast
val mk_fpa_zero : context -> sort -> bool -> ast
val mk_fpa_fp : context -> ast -> ast -> ast -> ast
val mk_fpa_numeral_float : context -> float -> sort -> ast
val mk_fpa_numeral_double : context -> float -> sort -> ast
val mk_fpa_numeral_int : context -> int -> sort -> ast
val mk_fpa_numeral_int_uint : context -> bool -> int -> int -> sort -> ast
val mk_fpa_numeral_int64_uint64 : context -> bool -> int64 -> int64 -> sort -> ast
val mk_fpa_abs : context -> ast -> ast
val mk_fpa_neg : context -> ast -> ast
val mk_fpa_add : context -> ast -> ast -> ast -> ast
val mk_fpa_sub : context -> ast -> ast -> ast -> ast
val mk_fpa_mul : context -> ast -> ast -> ast -> ast
val mk_fpa_div : context -> ast -> ast -> ast -> ast
val mk_fpa_fma : context -> ast -> ast -> ast -> ast -> ast
val mk_fpa_sqrt : context -> ast -> ast -> ast
val mk_fpa_rem : context -> ast -> ast -> ast
val mk_fpa_round_to_integral : context -> ast -> ast -> ast
val mk_fpa_min : context -> ast -> ast -> ast
val mk_fpa_max : context -> ast -> ast -> ast
val mk_fpa_leq : context -> ast -> ast -> ast
val mk_fpa_lt : context -> ast -> ast -> ast
val mk_fpa_geq : context -> ast -> ast -> ast
val mk_fpa_gt : context -> ast -> ast -> ast
val mk_fpa_eq : context -> ast -> ast -> ast
val mk_fpa_is_normal : context -> ast -> ast
val mk_fpa_is_subnormal : context -> ast -> ast
val mk_fpa_is_zero : context -> ast -> ast
val mk_fpa_is_infinite : context -> ast -> ast
val mk_fpa_is_nan : context -> ast -> ast
val mk_fpa_is_negative : context -> ast -> ast
val mk_fpa_is_positive : context -> ast -> ast
val mk_fpa_to_fp_bv : context -> ast -> sort -> ast
val mk_fpa_to_fp_float : context -> ast -> ast -> sort -> ast
val mk_fpa_to_fp_real : context -> ast -> ast -> sort -> ast
val mk_fpa_to_fp_signed : context -> ast -> ast -> sort -> ast
val mk_fpa_to_fp_unsigned : context -> ast -> ast -> sort -> ast
val mk_fpa_to_ubv : context -> ast -> ast -> int -> ast
val mk_fpa_to_sbv : context -> ast -> ast -> int -> ast
val mk_fpa_to_real : context -> ast -> ast
val fpa_get_ebits : context -> sort -> int
val fpa_get_sbits : context -> sort -> int
val fpa_is_numeral_nan : context -> ast -> bool
val fpa_is_numeral_inf : context -> ast -> bool
val fpa_is_numeral_zero : context -> ast -> bool
val fpa_is_numeral_normal : context -> ast -> bool
val fpa_is_numeral_subnormal : context -> ast -> bool
val fpa_is_numeral_positive : context -> ast -> bool
val fpa_is_numeral_negative : context -> ast -> bool
val fpa_get_numeral_sign_bv : context -> ast -> ast
val fpa_get_numeral_significand_bv : context -> ast -> ast
val fpa_get_numeral_sign : context -> ast -> bool * int
val fpa_get_numeral_significand_string : context -> ast -> string
val fpa_get_numeral_significand_uint64 : context -> ast -> bool * int64
val fpa_get_numeral_exponent_string : context -> ast -> bool -> string
val fpa_get_numeral_exponent_int64 : context -> ast -> bool -> bool * int64
val fpa_get_numeral_exponent_bv : context -> ast -> bool -> ast
val mk_fpa_to_ieee_bv : context -> ast -> ast
val mk_fpa_to_fp_int_real : context -> ast -> ast -> ast -> sort -> ast
val fixedpoint_query_from_lvl : context -> fixedpoint -> ast -> int -> int
val fixedpoint_get_ground_sat_answer : context -> fixedpoint -> ast
val fixedpoint_get_rules_along_trace : context -> fixedpoint -> ast_vector
val fixedpoint_get_rule_names_along_trace : context -> fixedpoint -> symbol
val fixedpoint_add_invariant : context -> fixedpoint -> func_decl -> ast -> unit
val fixedpoint_get_reachable : context -> fixedpoint -> func_decl -> ast
val qe_model_project : context -> model -> int -> app list -> ast -> ast
val qe_model_project_skolem : context -> model -> int -> app list -> ast -> ast_map -> ast
val model_extrapolate : context -> model -> ast -> ast
val qe_lite : context -> ast_vector -> ast -> ast
val context_of_symbol : symbol -> context
val is_null_symbol : symbol -> bool
val mk_null_symbol : context -> symbol
val context_of_ast : ast -> context
val is_null_ast : ast -> bool
val mk_null_ast : context -> ast
val context_of_model : model -> context
val is_null_model : model -> bool
val mk_null_model : context -> model
val context_of_constructor : constructor -> context
val is_null_constructor : constructor -> bool
val mk_null_constructor : context -> constructor
val context_of_constructor_list : constructor_list -> context
val is_null_constructor_list : constructor_list -> bool
val mk_null_constructor_list : context -> constructor_list
val context_of_solver : solver -> context
val is_null_solver : solver -> bool
val mk_null_solver : context -> solver
val context_of_goal : goal -> context
val is_null_goal : goal -> bool
val mk_null_goal : context -> goal
val context_of_tactic : tactic -> context
val is_null_tactic : tactic -> bool
val mk_null_tactic : context -> tactic
val context_of_params : params -> context
val is_null_params : params -> bool
val mk_null_params : context -> params
val context_of_probe : probe -> context
val is_null_probe : probe -> bool
val mk_null_probe : context -> probe
val context_of_stats : stats -> context
val is_null_stats : stats -> bool
val mk_null_stats : context -> stats
val context_of_ast_vector : ast_vector -> context
val is_null_ast_vector : ast_vector -> bool
val mk_null_ast_vector : context -> ast_vector
val context_of_ast_map : ast_map -> context
val is_null_ast_map : ast_map -> bool
val mk_null_ast_map : context -> ast_map
val context_of_apply_result : apply_result -> context
val is_null_apply_result : apply_result -> bool
val mk_null_apply_result : context -> apply_result
val context_of_func_interp : func_interp -> context
val is_null_func_interp : func_interp -> bool
val mk_null_func_interp : context -> func_interp
val context_of_func_entry : func_entry -> context
val is_null_func_entry : func_entry -> bool
val mk_null_func_entry : context -> func_entry
val context_of_fixedpoint : fixedpoint -> context
val is_null_fixedpoint : fixedpoint -> bool
val mk_null_fixedpoint : context -> fixedpoint
val context_of_optimize : optimize -> context
val is_null_optimize : optimize -> bool
val mk_null_optimize : context -> optimize
val context_of_param_descrs : param_descrs -> context
val is_null_param_descrs : param_descrs -> bool
val mk_null_param_descrs : context -> param_descrs
val context_of_rcf_num : rcf_num -> context
val is_null_rcf_num : rcf_num -> bool
val mk_null_rcf_num : context -> rcf_num