z3 4.8.17 · OCaml Package

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 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 interrupt : 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 -> int -> 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 -> int -> sort -> ast

val mk_unsigned_int64 : context -> int -> 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 * int

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 * int * int

val get_numeral_int : context -> ast -> bool * int

val get_numeral_uint : context -> ast -> bool * int

val get_numeral_uint64 : context -> ast -> bool * int

val get_numeral_int64 : context -> ast -> bool * int

val get_numeral_rational_int64 : context -> ast -> bool * int * int

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 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 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_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 -> int

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 -> int -> int -> 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 * int

val fpa_get_numeral_exponent_string : context -> ast -> bool -> string

val fpa_get_numeral_exponent_int64 : context -> ast -> bool -> bool * int

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

package z3