package z3

  1. Overview
  2. Docs
type ptr
type symbol = ptr
type config = ptr
type context = ptr
type ast = ptr
type app = ast
type sort = ast
type func_decl = ast
type pattern = ast
type model = ptr
type literals = ptr
type constructor = ptr
type constructor_list = ptr
type solver = ptr
type solver_callback = ptr
type goal = ptr
type tactic = ptr
type simplifier = ptr
type params = ptr
type parser_context = ptr
type probe = ptr
type stats = ptr
type ast_vector = ptr
type ast_map = ptr
type apply_result = ptr
type func_interp = ptr
type func_entry = ptr
type fixedpoint = ptr
type optimize = ptr
type param_descrs = ptr
type 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_type_variable : 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 constructor_num_fields : context -> constructor -> int
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_abs : context -> 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_real_int64 : context -> int64 -> int64 -> 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_seq_map : context -> ast -> ast -> ast
val mk_seq_mapi : context -> ast -> ast -> ast -> ast
val mk_seq_foldl : context -> ast -> ast -> ast -> ast
val mk_seq_foldli : context -> ast -> ast -> 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_skolem_id : context -> ast -> symbol
val get_quantifier_id : context -> ast -> symbol
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 mk_simplifier : context -> string -> simplifier
val simplifier_inc_ref : context -> simplifier -> unit
val simplifier_dec_ref : context -> simplifier -> unit
val solver_add_simplifier : context -> solver -> simplifier -> solver
val simplifier_and_then : context -> simplifier -> simplifier -> simplifier
val simplifier_using_params : context -> simplifier -> params -> simplifier
val get_num_simplifiers : context -> int
val get_simplifier_name : context -> int -> string
val simplifier_get_help : context -> simplifier -> string
val simplifier_get_param_descrs : context -> simplifier -> param_descrs
val simplifier_get_descr : context -> string -> string
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_congruence_root : context -> solver -> ast -> ast
val solver_congruence_next : context -> solver -> ast -> ast
val solver_next_split : context -> solver_callback -> ast -> int -> int -> bool
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 -> bool
val solver_set_initial_value : context -> solver -> ast -> 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 rcf_is_rational : context -> rcf_num -> bool
val rcf_is_algebraic : context -> rcf_num -> bool
val rcf_is_infinitesimal : context -> rcf_num -> bool
val rcf_is_transcendental : context -> rcf_num -> bool
val rcf_extension_index : context -> rcf_num -> int
val rcf_transcendental_name : context -> rcf_num -> symbol
val rcf_infinitesimal_name : context -> rcf_num -> symbol
val rcf_num_coefficients : context -> rcf_num -> int
val rcf_coefficient : context -> rcf_num -> int -> rcf_num
val rcf_interval : context -> rcf_num -> int * int * int * ptr * int * int * ptr
val rcf_num_sign_conditions : context -> rcf_num -> int
val rcf_sign_condition_sign : context -> rcf_num -> int -> int
val rcf_num_sign_condition_coefficients : context -> rcf_num -> int -> int
val rcf_sign_condition_coefficient : context -> rcf_num -> int -> int -> rcf_num
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_set_initial_value : context -> optimize -> ast -> ast -> 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_simplifier : simplifier -> context
val is_null_simplifier : simplifier -> bool
val mk_null_simplifier : context -> simplifier
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct