sig
  exception Error of string
  type context
  val mk_context : (string * string) list -> Z3.context
  val interrupt : Z3.context -> unit
  module Log :
    sig
      val open_ : string -> bool
      val close : unit -> unit
      val append : string -> unit
    end
  module Version :
    sig
      val major : int
      val minor : int
      val build : int
      val revision : int
      val full_version : string
      val to_string : string
    end
  module Symbol :
    sig
      type symbol
      val kind : Z3.Symbol.symbol -> Z3enums.symbol_kind
      val is_int_symbol : Z3.Symbol.symbol -> bool
      val is_string_symbol : Z3.Symbol.symbol -> bool
      val get_int : Z3.Symbol.symbol -> int
      val get_string : Z3.Symbol.symbol -> string
      val to_string : Z3.Symbol.symbol -> string
      val mk_int : Z3.context -> int -> Z3.Symbol.symbol
      val mk_string : Z3.context -> string -> Z3.Symbol.symbol
      val mk_ints : Z3.context -> int list -> Z3.Symbol.symbol list
      val mk_strings : Z3.context -> string list -> Z3.Symbol.symbol list
    end
  module rec AST :
    sig
      type ast
      module ASTVector :
        sig
          type ast_vector
          val mk_ast_vector : Z3.context -> Z3.AST.ASTVector.ast_vector
          val get_size : Z3.AST.ASTVector.ast_vector -> int
          val get : Z3.AST.ASTVector.ast_vector -> int -> Z3.AST.ast
          val set : Z3.AST.ASTVector.ast_vector -> int -> Z3.AST.ast -> unit
          val resize : Z3.AST.ASTVector.ast_vector -> int -> unit
          val push : Z3.AST.ASTVector.ast_vector -> Z3.AST.ast -> unit
          val translate :
            Z3.AST.ASTVector.ast_vector ->
            Z3.context -> Z3.AST.ASTVector.ast_vector
          val to_list : Z3.AST.ASTVector.ast_vector -> Z3.AST.ast list
          val to_expr_list : Z3.AST.ASTVector.ast_vector -> Z3.Expr.expr list
          val to_string : Z3.AST.ASTVector.ast_vector -> string
        end
      module ASTMap :
        sig
          type ast_map
          val mk_ast_map : Z3.context -> Z3.AST.ASTMap.ast_map
          val contains : Z3.AST.ASTMap.ast_map -> Z3.AST.ast -> bool
          val find : Z3.AST.ASTMap.ast_map -> Z3.AST.ast -> Z3.AST.ast
          val insert :
            Z3.AST.ASTMap.ast_map -> Z3.AST.ast -> Z3.AST.ast -> unit
          val erase : Z3.AST.ASTMap.ast_map -> Z3.AST.ast -> unit
          val reset : Z3.AST.ASTMap.ast_map -> unit
          val get_size : Z3.AST.ASTMap.ast_map -> int
          val get_keys : Z3.AST.ASTMap.ast_map -> Z3.AST.ast list
          val to_string : Z3.AST.ASTMap.ast_map -> string
        end
      val hash : Z3.AST.ast -> int
      val get_id : Z3.AST.ast -> int
      val get_ast_kind : Z3.AST.ast -> Z3enums.ast_kind
      val is_expr : Z3.AST.ast -> bool
      val is_var : Z3.AST.ast -> bool
      val is_quantifier : Z3.AST.ast -> bool
      val is_sort : Z3.AST.ast -> bool
      val is_func_decl : Z3.AST.ast -> bool
      val to_string : Z3.AST.ast -> string
      val to_sexpr : Z3.AST.ast -> string
      val equal : Z3.AST.ast -> Z3.AST.ast -> bool
      val compare : Z3.AST.ast -> Z3.AST.ast -> int
      val translate : Z3.AST.ast -> Z3.context -> Z3.AST.ast
    end
  and Sort :
    sig
      type sort
      val equal : Z3.Sort.sort -> Z3.Sort.sort -> bool
      val get_id : Z3.Sort.sort -> int
      val get_sort_kind : Z3.Sort.sort -> Z3enums.sort_kind
      val get_name : Z3.Sort.sort -> Z3.Symbol.symbol
      val to_string : Z3.Sort.sort -> string
      val mk_uninterpreted : Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort
      val mk_uninterpreted_s : Z3.context -> string -> Z3.Sort.sort
    end
  and FuncDecl :
    sig
      type func_decl
      module Parameter :
        sig
          type parameter =
              P_Int of int
            | P_Dbl of float
            | P_Sym of Z3.Symbol.symbol
            | P_Srt of Z3.Sort.sort
            | P_Ast of Z3.AST.ast
            | P_Fdl of Z3.FuncDecl.func_decl
            | P_Rat of string
          val get_kind :
            Z3.FuncDecl.Parameter.parameter -> Z3enums.parameter_kind
          val get_int : Z3.FuncDecl.Parameter.parameter -> int
          val get_float : Z3.FuncDecl.Parameter.parameter -> float
          val get_symbol :
            Z3.FuncDecl.Parameter.parameter -> Z3.Symbol.symbol
          val get_sort : Z3.FuncDecl.Parameter.parameter -> Z3.Sort.sort
          val get_ast : Z3.FuncDecl.Parameter.parameter -> Z3.AST.ast
          val get_func_decl :
            Z3.FuncDecl.Parameter.parameter -> Z3.FuncDecl.func_decl
          val get_rational : Z3.FuncDecl.Parameter.parameter -> string
        end
      val mk_func_decl :
        Z3.context ->
        Z3.Symbol.symbol ->
        Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_func_decl_s :
        Z3.context ->
        string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_rec_func_decl :
        Z3.context ->
        Z3.Symbol.symbol ->
        Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_rec_func_decl_s :
        Z3.context ->
        string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val add_rec_def :
        Z3.context ->
        Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr -> unit
      val mk_fresh_func_decl :
        Z3.context ->
        string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_const_decl :
        Z3.context ->
        Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_const_decl_s :
        Z3.context -> string -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val mk_fresh_const_decl :
        Z3.context -> string -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val equal : Z3.FuncDecl.func_decl -> Z3.FuncDecl.func_decl -> bool
      val to_string : Z3.FuncDecl.func_decl -> string
      val get_id : Z3.FuncDecl.func_decl -> int
      val get_arity : Z3.FuncDecl.func_decl -> int
      val get_domain_size : Z3.FuncDecl.func_decl -> int
      val get_domain : Z3.FuncDecl.func_decl -> Z3.Sort.sort list
      val get_range : Z3.FuncDecl.func_decl -> Z3.Sort.sort
      val get_decl_kind : Z3.FuncDecl.func_decl -> Z3enums.decl_kind
      val get_name : Z3.FuncDecl.func_decl -> Z3.Symbol.symbol
      val get_num_parameters : Z3.FuncDecl.func_decl -> int
      val get_parameters :
        Z3.FuncDecl.func_decl -> Z3.FuncDecl.Parameter.parameter list
      val apply : Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
    end
  and Params :
    sig
      type params
      module ParamDescrs :
        sig
          type param_descrs
          val validate :
            Z3.Params.ParamDescrs.param_descrs -> Z3.Params.params -> unit
          val get_kind :
            Z3.Params.ParamDescrs.param_descrs ->
            Z3.Symbol.symbol -> Z3enums.param_kind
          val get_names :
            Z3.Params.ParamDescrs.param_descrs -> Z3.Symbol.symbol list
          val get_size : Z3.Params.ParamDescrs.param_descrs -> int
          val to_string : Z3.Params.ParamDescrs.param_descrs -> string
        end
      val add_bool : Z3.Params.params -> Z3.Symbol.symbol -> bool -> unit
      val add_int : Z3.Params.params -> Z3.Symbol.symbol -> int -> unit
      val add_float : Z3.Params.params -> Z3.Symbol.symbol -> float -> unit
      val add_symbol :
        Z3.Params.params -> Z3.Symbol.symbol -> Z3.Symbol.symbol -> unit
      val mk_params : Z3.context -> Z3.Params.params
      val to_string : Z3.Params.params -> string
      val update_param_value : Z3.context -> string -> string -> unit
      val set_print_mode : Z3.context -> Z3enums.ast_print_mode -> unit
    end
  and Expr :
    sig
      type expr
      val ast_of_expr : Z3.Expr.expr -> Z3.AST.ast
      val expr_of_ast : Z3.AST.ast -> Z3.Expr.expr
      val simplify : Z3.Expr.expr -> Z3.Params.params option -> Z3.Expr.expr
      val get_simplify_help : Z3.context -> string
      val get_simplify_parameter_descrs :
        Z3.context -> Z3.Params.ParamDescrs.param_descrs
      val get_func_decl : Z3.Expr.expr -> Z3.FuncDecl.func_decl
      val get_num_args : Z3.Expr.expr -> int
      val get_args : Z3.Expr.expr -> Z3.Expr.expr list
      val update : Z3.Expr.expr -> Z3.Expr.expr list -> Z3.Expr.expr
      val substitute :
        Z3.Expr.expr ->
        Z3.Expr.expr list -> Z3.Expr.expr list -> Z3.Expr.expr
      val substitute_one :
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val substitute_vars : Z3.Expr.expr -> Z3.Expr.expr list -> Z3.Expr.expr
      val translate : Z3.Expr.expr -> Z3.context -> Z3.Expr.expr
      val to_string : Z3.Expr.expr -> string
      val is_numeral : Z3.Expr.expr -> bool
      val is_well_sorted : Z3.Expr.expr -> bool
      val get_sort : Z3.Expr.expr -> Z3.Sort.sort
      val is_const : Z3.Expr.expr -> bool
      val mk_const :
        Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_const_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_const_f : Z3.context -> Z3.FuncDecl.func_decl -> Z3.Expr.expr
      val mk_fresh_const :
        Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_app :
        Z3.context ->
        Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_numeral_string :
        Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_numeral_int : Z3.context -> int -> Z3.Sort.sort -> Z3.Expr.expr
      val equal : Z3.Expr.expr -> Z3.Expr.expr -> bool
      val compare : Z3.Expr.expr -> Z3.Expr.expr -> int
    end
  module Boolean :
    sig
      val mk_sort : Z3.context -> Z3.Sort.sort
      val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
      val mk_const_s : Z3.context -> string -> Z3.Expr.expr
      val mk_true : Z3.context -> Z3.Expr.expr
      val mk_false : Z3.context -> Z3.Expr.expr
      val mk_val : Z3.context -> bool -> Z3.Expr.expr
      val mk_not : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ite :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_iff : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_implies :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_xor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_and : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_or : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_eq : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_distinct : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val get_bool_value : Z3.Expr.expr -> Z3enums.lbool
      val is_bool : Z3.Expr.expr -> bool
      val is_true : Z3.Expr.expr -> bool
      val is_false : Z3.Expr.expr -> bool
      val is_eq : Z3.Expr.expr -> bool
      val is_distinct : Z3.Expr.expr -> bool
      val is_ite : Z3.Expr.expr -> bool
      val is_and : Z3.Expr.expr -> bool
      val is_or : Z3.Expr.expr -> bool
      val is_iff : Z3.Expr.expr -> bool
      val is_xor : Z3.Expr.expr -> bool
      val is_not : Z3.Expr.expr -> bool
      val is_implies : Z3.Expr.expr -> bool
    end
  module Quantifier :
    sig
      type quantifier
      val expr_of_quantifier : Z3.Quantifier.quantifier -> Z3.Expr.expr
      val quantifier_of_expr : Z3.Expr.expr -> Z3.Quantifier.quantifier
      module Pattern :
        sig
          type pattern
          val get_num_terms : Z3.Quantifier.Pattern.pattern -> int
          val get_terms : Z3.Quantifier.Pattern.pattern -> Z3.Expr.expr list
          val to_string : Z3.Quantifier.Pattern.pattern -> string
        end
      val get_index : Z3.Expr.expr -> int
      val is_universal : Z3.Quantifier.quantifier -> bool
      val is_existential : Z3.Quantifier.quantifier -> bool
      val get_weight : Z3.Quantifier.quantifier -> int
      val get_num_patterns : Z3.Quantifier.quantifier -> int
      val get_patterns :
        Z3.Quantifier.quantifier -> Z3.Quantifier.Pattern.pattern list
      val get_num_no_patterns : Z3.Quantifier.quantifier -> int
      val get_no_patterns :
        Z3.Quantifier.quantifier -> Z3.Quantifier.Pattern.pattern list
      val get_num_bound : Z3.Quantifier.quantifier -> int
      val get_bound_variable_names :
        Z3.Quantifier.quantifier -> Z3.Symbol.symbol list
      val get_bound_variable_sorts :
        Z3.Quantifier.quantifier -> Z3.Sort.sort list
      val get_body : Z3.Quantifier.quantifier -> Z3.Expr.expr
      val mk_bound : Z3.context -> int -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_pattern :
        Z3.context -> Z3.Expr.expr list -> Z3.Quantifier.Pattern.pattern
      val mk_forall :
        Z3.context ->
        Z3.Sort.sort list ->
        Z3.Symbol.symbol list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val mk_forall_const :
        Z3.context ->
        Z3.Expr.expr list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val mk_exists :
        Z3.context ->
        Z3.Sort.sort list ->
        Z3.Symbol.symbol list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val mk_exists_const :
        Z3.context ->
        Z3.Expr.expr list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val mk_lambda_const :
        Z3.context ->
        Z3.Expr.expr list -> Z3.Expr.expr -> Z3.Quantifier.quantifier
      val mk_lambda :
        Z3.context ->
        (Z3.Symbol.symbol * Z3.Sort.sort) list ->
        Z3.Expr.expr -> Z3.Quantifier.quantifier
      val mk_quantifier :
        Z3.context ->
        bool ->
        Z3.Sort.sort list ->
        Z3.Symbol.symbol list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val mk_quantifier_const :
        Z3.context ->
        bool ->
        Z3.Expr.expr list ->
        Z3.Expr.expr ->
        int option ->
        Z3.Quantifier.Pattern.pattern list ->
        Z3.Expr.expr list ->
        Z3.Symbol.symbol option ->
        Z3.Symbol.symbol option -> Z3.Quantifier.quantifier
      val to_string : Z3.Quantifier.quantifier -> string
    end
  module Z3Array :
    sig
      val mk_sort :
        Z3.context -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Sort.sort
      val is_store : Z3.Expr.expr -> bool
      val is_select : Z3.Expr.expr -> bool
      val is_constant_array : Z3.Expr.expr -> bool
      val is_default_array : Z3.Expr.expr -> bool
      val is_array_map : Z3.Expr.expr -> bool
      val is_as_array : Z3.Expr.expr -> bool
      val is_array : Z3.Expr.expr -> bool
      val get_domain : Z3.Sort.sort -> Z3.Sort.sort
      val get_range : Z3.Sort.sort -> Z3.Sort.sort
      val mk_const :
        Z3.context ->
        Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_const_s :
        Z3.context -> string -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_select :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_store :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_const_array :
        Z3.context -> Z3.Sort.sort -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_map :
        Z3.context ->
        Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_term_array : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_array_ext :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
    end
  module Set :
    sig
      val mk_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
      val is_union : Z3.Expr.expr -> bool
      val is_intersect : Z3.Expr.expr -> bool
      val is_difference : Z3.Expr.expr -> bool
      val is_complement : Z3.Expr.expr -> bool
      val is_subset : Z3.Expr.expr -> bool
      val mk_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_full : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_set_add :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_del : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_union : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_intersection : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_difference :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_complement : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_membership :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_subset :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
    end
  module FiniteDomain :
    sig
      val mk_sort : Z3.context -> Z3.Symbol.symbol -> int64 -> Z3.Sort.sort
      val mk_sort_s : Z3.context -> string -> int64 -> Z3.Sort.sort
      val is_finite_domain : Z3.Expr.expr -> bool
      val is_lt : Z3.Expr.expr -> bool
      val get_size : Z3.Sort.sort -> int64
    end
  module Relation :
    sig
      val is_relation : Z3.Expr.expr -> bool
      val is_store : Z3.Expr.expr -> bool
      val is_empty : Z3.Expr.expr -> bool
      val is_is_empty : Z3.Expr.expr -> bool
      val is_join : Z3.Expr.expr -> bool
      val is_union : Z3.Expr.expr -> bool
      val is_widen : Z3.Expr.expr -> bool
      val is_project : Z3.Expr.expr -> bool
      val is_filter : Z3.Expr.expr -> bool
      val is_negation_filter : Z3.Expr.expr -> bool
      val is_rename : Z3.Expr.expr -> bool
      val is_complement : Z3.Expr.expr -> bool
      val is_select : Z3.Expr.expr -> bool
      val is_clone : Z3.Expr.expr -> bool
      val get_arity : Z3.Sort.sort -> int
      val get_column_sorts : Z3.Sort.sort -> Z3.Sort.sort list
    end
  module Datatype :
    sig
      module Constructor :
        sig
          type constructor
          val get_num_fields : Z3.Datatype.Constructor.constructor -> int
          val get_constructor_decl :
            Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl
          val get_tester_decl :
            Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl
          val get_accessor_decls :
            Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl list
        end
      val mk_constructor :
        Z3.context ->
        Z3.Symbol.symbol ->
        Z3.Symbol.symbol ->
        Z3.Symbol.symbol list ->
        Z3.Sort.sort option list ->
        int list -> Z3.Datatype.Constructor.constructor
      val mk_constructor_s :
        Z3.context ->
        string ->
        Z3.Symbol.symbol ->
        Z3.Symbol.symbol list ->
        Z3.Sort.sort option list ->
        int list -> Z3.Datatype.Constructor.constructor
      val mk_sort_ref : Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort
      val mk_sort_ref_s : Z3.context -> string -> Z3.Sort.sort
      val mk_sort :
        Z3.context ->
        Z3.Symbol.symbol ->
        Z3.Datatype.Constructor.constructor list -> Z3.Sort.sort
      val mk_sort_s :
        Z3.context ->
        string -> Z3.Datatype.Constructor.constructor list -> Z3.Sort.sort
      val mk_sorts :
        Z3.context ->
        Z3.Symbol.symbol list ->
        Z3.Datatype.Constructor.constructor list list -> Z3.Sort.sort list
      val mk_sorts_s :
        Z3.context ->
        string list ->
        Z3.Datatype.Constructor.constructor list list -> Z3.Sort.sort list
      val get_num_constructors : Z3.Sort.sort -> int
      val get_constructors : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
      val get_recognizers : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
      val get_accessors : Z3.Sort.sort -> Z3.FuncDecl.func_decl list list
    end
  module Enumeration :
    sig
      val mk_sort :
        Z3.context ->
        Z3.Symbol.symbol -> Z3.Symbol.symbol list -> Z3.Sort.sort
      val mk_sort_s : Z3.context -> string -> string list -> Z3.Sort.sort
      val get_const_decls : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
      val get_const_decl : Z3.Sort.sort -> int -> Z3.FuncDecl.func_decl
      val get_consts : Z3.Sort.sort -> Z3.Expr.expr list
      val get_const : Z3.Sort.sort -> int -> Z3.Expr.expr
      val get_tester_decls : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
      val get_tester_decl : Z3.Sort.sort -> int -> Z3.FuncDecl.func_decl
    end
  module Z3List :
    sig
      val mk_sort :
        Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Sort.sort
      val mk_list_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Sort.sort
      val get_nil_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_is_nil_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_cons_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_is_cons_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_head_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_tail_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val nil : Z3.Sort.sort -> Z3.Expr.expr
    end
  module Tuple :
    sig
      val mk_sort :
        Z3.context ->
        Z3.Symbol.symbol ->
        Z3.Symbol.symbol list -> Z3.Sort.sort list -> Z3.Sort.sort
      val get_mk_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
      val get_num_fields : Z3.Sort.sort -> int
      val get_field_decls : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
    end
  module Arithmetic :
    sig
      module Integer :
        sig
          val mk_sort : Z3.context -> Z3.Sort.sort
          val get_big_int : Z3.Expr.expr -> Z.t
          val numeral_to_string : Z3.Expr.expr -> string
          val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
          val mk_const_s : Z3.context -> string -> Z3.Expr.expr
          val mk_mod :
            Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
          val mk_rem :
            Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
          val mk_numeral_s : Z3.context -> string -> Z3.Expr.expr
          val mk_numeral_i : Z3.context -> int -> Z3.Expr.expr
          val mk_int2real : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
          val mk_int2bv : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
        end
      module Real :
        sig
          val mk_sort : Z3.context -> Z3.Sort.sort
          val get_numerator : Z3.Expr.expr -> Z3.Expr.expr
          val get_denominator : Z3.Expr.expr -> Z3.Expr.expr
          val get_ratio : Z3.Expr.expr -> Q.t
          val to_decimal_string : Z3.Expr.expr -> int -> string
          val numeral_to_string : Z3.Expr.expr -> string
          val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
          val mk_const_s : Z3.context -> string -> Z3.Expr.expr
          val mk_numeral_nd : Z3.context -> int -> int -> Z3.Expr.expr
          val mk_numeral_s : Z3.context -> string -> Z3.Expr.expr
          val mk_numeral_i : Z3.context -> int -> Z3.Expr.expr
          val mk_is_integer : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
          val mk_real2int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
          module AlgebraicNumber :
            sig
              val to_upper : Z3.Expr.expr -> int -> Z3.Expr.expr
              val to_lower : Z3.Expr.expr -> int -> Z3.Expr.expr
              val to_decimal_string : Z3.Expr.expr -> int -> string
              val numeral_to_string : Z3.Expr.expr -> string
            end
        end
      val is_int : Z3.Expr.expr -> bool
      val is_arithmetic_numeral : Z3.Expr.expr -> bool
      val is_le : Z3.Expr.expr -> bool
      val is_ge : Z3.Expr.expr -> bool
      val is_lt : Z3.Expr.expr -> bool
      val is_gt : Z3.Expr.expr -> bool
      val is_add : Z3.Expr.expr -> bool
      val is_sub : Z3.Expr.expr -> bool
      val is_uminus : Z3.Expr.expr -> bool
      val is_mul : Z3.Expr.expr -> bool
      val is_div : Z3.Expr.expr -> bool
      val is_idiv : Z3.Expr.expr -> bool
      val is_remainder : Z3.Expr.expr -> bool
      val is_modulus : Z3.Expr.expr -> bool
      val is_int2real : Z3.Expr.expr -> bool
      val is_real2int : Z3.Expr.expr -> bool
      val is_real_is_int : Z3.Expr.expr -> bool
      val is_real : Z3.Expr.expr -> bool
      val is_int_numeral : Z3.Expr.expr -> bool
      val is_rat_numeral : Z3.Expr.expr -> bool
      val is_algebraic_number : Z3.Expr.expr -> bool
      val mk_add : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_mul : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_sub : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_unary_minus : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_div : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_power :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_lt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_le : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_gt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
    end
  module BitVector :
    sig
      val mk_sort : Z3.context -> int -> Z3.Sort.sort
      val is_bv : Z3.Expr.expr -> bool
      val is_bv_numeral : Z3.Expr.expr -> bool
      val is_bv_bit1 : Z3.Expr.expr -> bool
      val is_bv_bit0 : Z3.Expr.expr -> bool
      val is_bv_uminus : Z3.Expr.expr -> bool
      val is_bv_add : Z3.Expr.expr -> bool
      val is_bv_sub : Z3.Expr.expr -> bool
      val is_bv_mul : Z3.Expr.expr -> bool
      val is_bv_sdiv : Z3.Expr.expr -> bool
      val is_bv_udiv : Z3.Expr.expr -> bool
      val is_bv_SRem : Z3.Expr.expr -> bool
      val is_bv_urem : Z3.Expr.expr -> bool
      val is_bv_smod : Z3.Expr.expr -> bool
      val is_bv_sdiv0 : Z3.Expr.expr -> bool
      val is_bv_udiv0 : Z3.Expr.expr -> bool
      val is_bv_srem0 : Z3.Expr.expr -> bool
      val is_bv_urem0 : Z3.Expr.expr -> bool
      val is_bv_smod0 : Z3.Expr.expr -> bool
      val is_bv_ule : Z3.Expr.expr -> bool
      val is_bv_sle : Z3.Expr.expr -> bool
      val is_bv_uge : Z3.Expr.expr -> bool
      val is_bv_sge : Z3.Expr.expr -> bool
      val is_bv_ult : Z3.Expr.expr -> bool
      val is_bv_slt : Z3.Expr.expr -> bool
      val is_bv_ugt : Z3.Expr.expr -> bool
      val is_bv_sgt : Z3.Expr.expr -> bool
      val is_bv_and : Z3.Expr.expr -> bool
      val is_bv_or : Z3.Expr.expr -> bool
      val is_bv_not : Z3.Expr.expr -> bool
      val is_bv_xor : Z3.Expr.expr -> bool
      val is_bv_nand : Z3.Expr.expr -> bool
      val is_bv_nor : Z3.Expr.expr -> bool
      val is_bv_xnor : Z3.Expr.expr -> bool
      val is_bv_concat : Z3.Expr.expr -> bool
      val is_bv_signextension : Z3.Expr.expr -> bool
      val is_bv_zeroextension : Z3.Expr.expr -> bool
      val is_bv_extract : Z3.Expr.expr -> bool
      val is_bv_repeat : Z3.Expr.expr -> bool
      val is_bv_reduceor : Z3.Expr.expr -> bool
      val is_bv_reduceand : Z3.Expr.expr -> bool
      val is_bv_comp : Z3.Expr.expr -> bool
      val is_bv_shiftleft : Z3.Expr.expr -> bool
      val is_bv_shiftrightlogical : Z3.Expr.expr -> bool
      val is_bv_shiftrightarithmetic : Z3.Expr.expr -> bool
      val is_bv_rotateleft : Z3.Expr.expr -> bool
      val is_bv_rotateright : Z3.Expr.expr -> bool
      val is_bv_rotateleftextended : Z3.Expr.expr -> bool
      val is_bv_rotaterightextended : Z3.Expr.expr -> bool
      val is_int2bv : Z3.Expr.expr -> bool
      val is_bv2int : Z3.Expr.expr -> bool
      val is_bv_carry : Z3.Expr.expr -> bool
      val is_bv_xor3 : Z3.Expr.expr -> bool
      val get_size : Z3.Sort.sort -> int
      val numeral_to_string : Z3.Expr.expr -> string
      val mk_const : Z3.context -> Z3.Symbol.symbol -> int -> Z3.Expr.expr
      val mk_const_s : Z3.context -> string -> int -> Z3.Expr.expr
      val mk_not : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_redand : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_redor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_and : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_or : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_xor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_nand :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_nor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_xnor :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_neg : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_add : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sub : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_mul : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_udiv :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sdiv :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_urem :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_srem :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_smod :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ult : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_slt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ule : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sle : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_uge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ugt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sgt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_concat :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_extract :
        Z3.context -> int -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sign_ext : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_zero_ext : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_repeat : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_shl : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_lshr :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ashr :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_rotate_left : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_rotate_right : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ext_rotate_left :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ext_rotate_right :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_bv2int : Z3.context -> Z3.Expr.expr -> bool -> Z3.Expr.expr
      val mk_add_no_overflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
      val mk_add_no_underflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sub_no_overflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sub_no_underflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
      val mk_sdiv_no_overflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_neg_no_overflow : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_mul_no_overflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
      val mk_mul_no_underflow :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_numeral : Z3.context -> string -> int -> Z3.Expr.expr
    end
  module Seq :
    sig
      val mk_seq_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
      val is_seq_sort : Z3.context -> Z3.Sort.sort -> bool
      val mk_re_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
      val is_re_sort : Z3.context -> Z3.Sort.sort -> bool
      val mk_string_sort : Z3.context -> Z3.Sort.sort
      val mk_char_sort : Z3.context -> Z3.Sort.sort
      val is_string_sort : Z3.context -> Z3.Sort.sort -> bool
      val is_char_sort : Z3.context -> Z3.Sort.sort -> bool
      val mk_string : Z3.context -> string -> Z3.Expr.expr
      val is_string : Z3.context -> Z3.Expr.expr -> bool
      val get_string : Z3.context -> Z3.Expr.expr -> string
      val mk_seq_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_seq_unit : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_concat : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_seq_prefix :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_suffix :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_contains :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_extract :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_replace :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_at :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_length : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_nth :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_index :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_last_index :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_str_to_int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_str_le :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_str_lt :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_int_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_string_to_code : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_string_from_code : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_ubv_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sbv_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_to_re : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_seq_in_re :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_plus : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_star : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_option : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_union : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_re_concat : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_re_range :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_loop :
        Z3.context -> Z3.Expr.expr -> int -> int -> Z3.Expr.expr
      val mk_re_intersect : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
      val mk_re_complement : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_re_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_re_full : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_char : Z3.context -> int -> Z3.Expr.expr
      val mk_char_le :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_char_to_int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_char_to_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_char_from_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_char_is_digit : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
    end
  module FloatingPoint :
    sig
      module RoundingMode :
        sig
          val mk_sort : Z3.context -> Z3.Sort.sort
          val is_fprm : Z3.Expr.expr -> bool
          val mk_round_nearest_ties_to_even : Z3.context -> Z3.Expr.expr
          val mk_rne : Z3.context -> Z3.Expr.expr
          val mk_round_nearest_ties_to_away : Z3.context -> Z3.Expr.expr
          val mk_rna : Z3.context -> Z3.Expr.expr
          val mk_round_toward_positive : Z3.context -> Z3.Expr.expr
          val mk_rtp : Z3.context -> Z3.Expr.expr
          val mk_round_toward_negative : Z3.context -> Z3.Expr.expr
          val mk_rtn : Z3.context -> Z3.Expr.expr
          val mk_round_toward_zero : Z3.context -> Z3.Expr.expr
          val mk_rtz : Z3.context -> Z3.Expr.expr
        end
      val mk_sort : Z3.context -> int -> int -> Z3.Sort.sort
      val mk_sort_half : Z3.context -> Z3.Sort.sort
      val mk_sort_16 : Z3.context -> Z3.Sort.sort
      val mk_sort_single : Z3.context -> Z3.Sort.sort
      val mk_sort_32 : Z3.context -> Z3.Sort.sort
      val mk_sort_double : Z3.context -> Z3.Sort.sort
      val mk_sort_64 : Z3.context -> Z3.Sort.sort
      val mk_sort_quadruple : Z3.context -> Z3.Sort.sort
      val mk_sort_128 : Z3.context -> Z3.Sort.sort
      val mk_nan : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_inf : Z3.context -> Z3.Sort.sort -> bool -> Z3.Expr.expr
      val mk_zero : Z3.context -> Z3.Sort.sort -> bool -> Z3.Expr.expr
      val mk_fp :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_numeral_f : Z3.context -> float -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_numeral_i : Z3.context -> int -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_numeral_i_u :
        Z3.context -> bool -> int64 -> int64 -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_numeral_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
      val is_fp : Z3.Expr.expr -> bool
      val is_abs : Z3.Expr.expr -> bool
      val is_neg : Z3.Expr.expr -> bool
      val is_add : Z3.Expr.expr -> bool
      val is_sub : Z3.Expr.expr -> bool
      val is_mul : Z3.Expr.expr -> bool
      val is_div : Z3.Expr.expr -> bool
      val is_fma : Z3.Expr.expr -> bool
      val is_sqrt : Z3.Expr.expr -> bool
      val is_rem : Z3.Expr.expr -> bool
      val is_round_to_integral : Z3.Expr.expr -> bool
      val is_min : Z3.Expr.expr -> bool
      val is_max : Z3.Expr.expr -> bool
      val is_leq : Z3.Expr.expr -> bool
      val is_lt : Z3.Expr.expr -> bool
      val is_geq : Z3.Expr.expr -> bool
      val is_gt : Z3.Expr.expr -> bool
      val is_eq : Z3.Expr.expr -> bool
      val is_is_normal : Z3.Expr.expr -> bool
      val is_is_subnormal : Z3.Expr.expr -> bool
      val is_is_zero : Z3.Expr.expr -> bool
      val is_is_infinite : Z3.Expr.expr -> bool
      val is_is_nan : Z3.Expr.expr -> bool
      val is_is_negative : Z3.Expr.expr -> bool
      val is_is_positive : Z3.Expr.expr -> bool
      val is_to_fp : Z3.Expr.expr -> bool
      val is_to_fp_unsigned : Z3.Expr.expr -> bool
      val is_to_ubv : Z3.Expr.expr -> bool
      val is_to_sbv : Z3.Expr.expr -> bool
      val is_to_real : Z3.Expr.expr -> bool
      val is_to_ieee_bv : Z3.Expr.expr -> bool
      val mk_const :
        Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_const_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_abs : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_neg : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_add :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sub :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_mul :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_div :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_fma :
        Z3.context ->
        Z3.Expr.expr ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_sqrt :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_rem : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_round_to_integral :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_min : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_max : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_leq : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_lt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_geq : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_gt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_eq : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_normal : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_subnormal : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_zero : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_infinite : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_nan : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_negative : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_is_positive : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_to_fp_bv :
        Z3.context -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_to_fp_float :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_to_fp_real :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_to_fp_signed :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_to_fp_unsigned :
        Z3.context ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val mk_to_ubv :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> int -> Z3.Expr.expr
      val mk_to_sbv :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> int -> Z3.Expr.expr
      val mk_to_real : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val get_ebits : Z3.context -> Z3.Sort.sort -> int
      val get_sbits : Z3.context -> Z3.Sort.sort -> int
      val get_numeral_sign : Z3.context -> Z3.Expr.expr -> bool * int
      val get_numeral_sign_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val get_numeral_exponent_string :
        Z3.context -> Z3.Expr.expr -> bool -> string
      val get_numeral_exponent_int :
        Z3.context -> Z3.Expr.expr -> bool -> bool * int64
      val get_numeral_exponent_bv :
        Z3.context -> Z3.Expr.expr -> bool -> Z3.Expr.expr
      val get_numeral_significand_bv :
        Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val get_numeral_significand_string :
        Z3.context -> Z3.Expr.expr -> string
      val get_numeral_significand_uint :
        Z3.context -> Z3.Expr.expr -> bool * int64
      val is_numeral_nan : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_inf : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_zero : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_normal : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_subnormal : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_positive : Z3.context -> Z3.Expr.expr -> bool
      val is_numeral_negative : Z3.context -> Z3.Expr.expr -> bool
      val mk_to_ieee_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_to_fp_int_real :
        Z3.context ->
        Z3.Expr.expr ->
        Z3.Expr.expr -> Z3.Expr.expr -> Z3.Sort.sort -> Z3.Expr.expr
      val numeral_to_string : Z3.Expr.expr -> string
    end
  module Proof :
    sig
      val is_true : Z3.Expr.expr -> bool
      val is_asserted : Z3.Expr.expr -> bool
      val is_goal : Z3.Expr.expr -> bool
      val is_oeq : Z3.Expr.expr -> bool
      val is_modus_ponens : Z3.Expr.expr -> bool
      val is_reflexivity : Z3.Expr.expr -> bool
      val is_symmetry : Z3.Expr.expr -> bool
      val is_transitivity : Z3.Expr.expr -> bool
      val is_Transitivity_star : Z3.Expr.expr -> bool
      val is_monotonicity : Z3.Expr.expr -> bool
      val is_quant_intro : Z3.Expr.expr -> bool
      val is_distributivity : Z3.Expr.expr -> bool
      val is_and_elimination : Z3.Expr.expr -> bool
      val is_or_elimination : Z3.Expr.expr -> bool
      val is_rewrite : Z3.Expr.expr -> bool
      val is_rewrite_star : Z3.Expr.expr -> bool
      val is_pull_quant : Z3.Expr.expr -> bool
      val is_push_quant : Z3.Expr.expr -> bool
      val is_elim_unused_vars : Z3.Expr.expr -> bool
      val is_der : Z3.Expr.expr -> bool
      val is_quant_inst : Z3.Expr.expr -> bool
      val is_hypothesis : Z3.Expr.expr -> bool
      val is_lemma : Z3.Expr.expr -> bool
      val is_unit_resolution : Z3.Expr.expr -> bool
      val is_iff_true : Z3.Expr.expr -> bool
      val is_iff_false : Z3.Expr.expr -> bool
      val is_commutativity : Z3.Expr.expr -> bool
      val is_def_axiom : Z3.Expr.expr -> bool
      val is_def_intro : Z3.Expr.expr -> bool
      val is_apply_def : Z3.Expr.expr -> bool
      val is_iff_oeq : Z3.Expr.expr -> bool
      val is_nnf_pos : Z3.Expr.expr -> bool
      val is_nnf_neg : Z3.Expr.expr -> bool
      val is_skolemize : Z3.Expr.expr -> bool
      val is_modus_ponens_oeq : Z3.Expr.expr -> bool
      val is_theory_lemma : Z3.Expr.expr -> bool
    end
  module Goal :
    sig
      type goal
      val get_precision : Z3.Goal.goal -> Z3enums.goal_prec
      val is_precise : Z3.Goal.goal -> bool
      val is_underapproximation : Z3.Goal.goal -> bool
      val is_overapproximation : Z3.Goal.goal -> bool
      val is_garbage : Z3.Goal.goal -> bool
      val add : Z3.Goal.goal -> Z3.Expr.expr list -> unit
      val is_inconsistent : Z3.Goal.goal -> bool
      val get_depth : Z3.Goal.goal -> int
      val reset : Z3.Goal.goal -> unit
      val get_size : Z3.Goal.goal -> int
      val get_formulas : Z3.Goal.goal -> Z3.Expr.expr list
      val get_num_exprs : Z3.Goal.goal -> int
      val is_decided_sat : Z3.Goal.goal -> bool
      val is_decided_unsat : Z3.Goal.goal -> bool
      val translate : Z3.Goal.goal -> Z3.context -> Z3.Goal.goal
      val simplify : Z3.Goal.goal -> Z3.Params.params option -> Z3.Goal.goal
      val mk_goal : Z3.context -> bool -> bool -> bool -> Z3.Goal.goal
      val to_string : Z3.Goal.goal -> string
      val as_expr : Z3.Goal.goal -> Z3.Expr.expr
    end
  module Model :
    sig
      type model
      module FuncInterp :
        sig
          type func_interp
          module FuncEntry :
            sig
              type func_entry
              val get_value :
                Z3.Model.FuncInterp.FuncEntry.func_entry -> Z3.Expr.expr
              val get_num_args :
                Z3.Model.FuncInterp.FuncEntry.func_entry -> int
              val get_args :
                Z3.Model.FuncInterp.FuncEntry.func_entry -> Z3.Expr.expr list
              val to_string :
                Z3.Model.FuncInterp.FuncEntry.func_entry -> string
            end
          val get_num_entries : Z3.Model.FuncInterp.func_interp -> int
          val get_entries :
            Z3.Model.FuncInterp.func_interp ->
            Z3.Model.FuncInterp.FuncEntry.func_entry list
          val get_else : Z3.Model.FuncInterp.func_interp -> Z3.Expr.expr
          val get_arity : Z3.Model.FuncInterp.func_interp -> int
          val to_string : Z3.Model.FuncInterp.func_interp -> string
        end
      val get_const_interp :
        Z3.Model.model -> Z3.FuncDecl.func_decl -> Z3.Expr.expr option
      val get_const_interp_e :
        Z3.Model.model -> Z3.Expr.expr -> Z3.Expr.expr option
      val get_func_interp :
        Z3.Model.model ->
        Z3.FuncDecl.func_decl -> Z3.Model.FuncInterp.func_interp option
      val get_num_consts : Z3.Model.model -> int
      val get_const_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
      val get_num_funcs : Z3.Model.model -> int
      val get_func_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
      val get_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
      val eval :
        Z3.Model.model -> Z3.Expr.expr -> bool -> Z3.Expr.expr option
      val evaluate :
        Z3.Model.model -> Z3.Expr.expr -> bool -> Z3.Expr.expr option
      val get_num_sorts : Z3.Model.model -> int
      val get_sorts : Z3.Model.model -> Z3.Sort.sort list
      val sort_universe : Z3.Model.model -> Z3.Sort.sort -> Z3.Expr.expr list
      val to_string : Z3.Model.model -> string
    end
  module Probe :
    sig
      type probe
      val apply : Z3.Probe.probe -> Z3.Goal.goal -> float
      val get_num_probes : Z3.context -> int
      val get_probe_names : Z3.context -> string list
      val get_probe_description : Z3.context -> string -> string
      val mk_probe : Z3.context -> string -> Z3.Probe.probe
      val const : Z3.context -> float -> Z3.Probe.probe
      val lt :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val gt :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val le :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val ge :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val eq :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val and_ :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val or_ :
        Z3.context -> Z3.Probe.probe -> Z3.Probe.probe -> Z3.Probe.probe
      val not_ : Z3.context -> Z3.Probe.probe -> Z3.Probe.probe
    end
  module Tactic :
    sig
      type tactic
      module ApplyResult :
        sig
          type apply_result
          val get_num_subgoals : Z3.Tactic.ApplyResult.apply_result -> int
          val get_subgoals :
            Z3.Tactic.ApplyResult.apply_result -> Z3.Goal.goal list
          val get_subgoal :
            Z3.Tactic.ApplyResult.apply_result -> int -> Z3.Goal.goal
          val to_string : Z3.Tactic.ApplyResult.apply_result -> string
        end
      val get_help : Z3.Tactic.tactic -> string
      val get_param_descrs :
        Z3.Tactic.tactic -> Z3.Params.ParamDescrs.param_descrs
      val apply :
        Z3.Tactic.tactic ->
        Z3.Goal.goal ->
        Z3.Params.params option -> Z3.Tactic.ApplyResult.apply_result
      val get_num_tactics : Z3.context -> int
      val get_tactic_names : Z3.context -> string list
      val get_tactic_description : Z3.context -> string -> string
      val mk_tactic : Z3.context -> string -> Z3.Tactic.tactic
      val and_then :
        Z3.context ->
        Z3.Tactic.tactic ->
        Z3.Tactic.tactic -> Z3.Tactic.tactic list -> Z3.Tactic.tactic
      val or_else :
        Z3.context ->
        Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
      val try_for : Z3.context -> Z3.Tactic.tactic -> int -> Z3.Tactic.tactic
      val when_ :
        Z3.context -> Z3.Probe.probe -> Z3.Tactic.tactic -> Z3.Tactic.tactic
      val cond :
        Z3.context ->
        Z3.Probe.probe ->
        Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
      val repeat : Z3.context -> Z3.Tactic.tactic -> int -> Z3.Tactic.tactic
      val skip : Z3.context -> Z3.Tactic.tactic
      val fail : Z3.context -> Z3.Tactic.tactic
      val fail_if : Z3.context -> Z3.Probe.probe -> Z3.Tactic.tactic
      val fail_if_not_decided : Z3.context -> Z3.Tactic.tactic
      val using_params :
        Z3.context ->
        Z3.Tactic.tactic -> Z3.Params.params -> Z3.Tactic.tactic
      val with_ :
        Z3.context ->
        Z3.Tactic.tactic -> Z3.Params.params -> Z3.Tactic.tactic
      val par_or : Z3.context -> Z3.Tactic.tactic list -> Z3.Tactic.tactic
      val par_and_then :
        Z3.context ->
        Z3.Tactic.tactic -> Z3.Tactic.tactic -> Z3.Tactic.tactic
      val interrupt : Z3.context -> unit
    end
  module Simplifier :
    sig
      type simplifier
      val get_help : Z3.Simplifier.simplifier -> string
      val get_param_descrs :
        Z3.Simplifier.simplifier -> Z3.Params.ParamDescrs.param_descrs
      val get_num_simplifiers : Z3.context -> int
      val get_simplifier_names : Z3.context -> string list
      val get_simplifier_description : Z3.context -> string -> string
      val mk_simplifier : Z3.context -> string -> Z3.Simplifier.simplifier
      val and_then :
        Z3.context ->
        Z3.Simplifier.simplifier ->
        Z3.Simplifier.simplifier ->
        Z3.Simplifier.simplifier list -> Z3.Simplifier.simplifier
      val using_params :
        Z3.context ->
        Z3.Simplifier.simplifier ->
        Z3.Params.params -> Z3.Simplifier.simplifier
      val with_ :
        Z3.context ->
        Z3.Simplifier.simplifier ->
        Z3.Params.params -> Z3.Simplifier.simplifier
    end
  module Statistics :
    sig
      type statistics
      module Entry :
        sig
          type statistics_entry
          val get_key : Z3.Statistics.Entry.statistics_entry -> string
          val get_int : Z3.Statistics.Entry.statistics_entry -> int
          val get_float : Z3.Statistics.Entry.statistics_entry -> float
          val is_int : Z3.Statistics.Entry.statistics_entry -> bool
          val is_float : Z3.Statistics.Entry.statistics_entry -> bool
          val to_string_value :
            Z3.Statistics.Entry.statistics_entry -> string
          val to_string : Z3.Statistics.Entry.statistics_entry -> string
        end
      val to_string : Z3.Statistics.statistics -> string
      val get_size : Z3.Statistics.statistics -> int
      val get_entries :
        Z3.Statistics.statistics -> Z3.Statistics.Entry.statistics_entry list
      val get_keys : Z3.Statistics.statistics -> string list
      val get :
        Z3.Statistics.statistics ->
        string -> Z3.Statistics.Entry.statistics_entry option
      val get_estimated_alloc_size : unit -> int64
    end
  module Solver :
    sig
      type solver
      type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
      val string_of_status : Z3.Solver.status -> string
      val get_help : Z3.Solver.solver -> string
      val set_parameters : Z3.Solver.solver -> Z3.Params.params -> unit
      val get_param_descrs :
        Z3.Solver.solver -> Z3.Params.ParamDescrs.param_descrs
      val get_num_scopes : Z3.Solver.solver -> int
      val push : Z3.Solver.solver -> unit
      val pop : Z3.Solver.solver -> int -> unit
      val reset : Z3.Solver.solver -> unit
      val add : Z3.Solver.solver -> Z3.Expr.expr list -> unit
      val assert_and_track_l :
        Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Expr.expr list -> unit
      val assert_and_track :
        Z3.Solver.solver -> Z3.Expr.expr -> Z3.Expr.expr -> unit
      val get_num_assertions : Z3.Solver.solver -> int
      val get_assertions : Z3.Solver.solver -> Z3.Expr.expr list
      val check : Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Solver.status
      val get_model : Z3.Solver.solver -> Z3.Model.model option
      val get_proof : Z3.Solver.solver -> Z3.Expr.expr option
      val get_unsat_core : Z3.Solver.solver -> Z3.Expr.expr list
      val get_reason_unknown : Z3.Solver.solver -> string
      val get_statistics : Z3.Solver.solver -> Z3.Statistics.statistics
      val mk_solver :
        Z3.context -> Z3.Symbol.symbol option -> Z3.Solver.solver
      val mk_solver_s : Z3.context -> string -> Z3.Solver.solver
      val mk_simple_solver : Z3.context -> Z3.Solver.solver
      val mk_solver_t : Z3.context -> Z3.Tactic.tactic -> Z3.Solver.solver
      val add_simplifier :
        Z3.context ->
        Z3.Solver.solver -> Z3.Simplifier.simplifier -> Z3.Solver.solver
      val translate : Z3.Solver.solver -> Z3.context -> Z3.Solver.solver
      val to_string : Z3.Solver.solver -> string
      val interrupt : Z3.context -> Z3.Solver.solver -> unit
    end
  module Fixedpoint :
    sig
      type fixedpoint
      val get_help : Z3.Fixedpoint.fixedpoint -> string
      val set_parameters :
        Z3.Fixedpoint.fixedpoint -> Z3.Params.params -> unit
      val get_param_descrs :
        Z3.Fixedpoint.fixedpoint -> Z3.Params.ParamDescrs.param_descrs
      val add : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list -> unit
      val register_relation :
        Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> unit
      val add_rule :
        Z3.Fixedpoint.fixedpoint ->
        Z3.Expr.expr -> Z3.Symbol.symbol option -> unit
      val add_fact :
        Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> int list -> unit
      val query :
        Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr -> Z3.Solver.status
      val query_r :
        Z3.Fixedpoint.fixedpoint ->
        Z3.FuncDecl.func_decl list -> Z3.Solver.status
      val update_rule :
        Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr -> Z3.Symbol.symbol -> unit
      val get_answer : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr option
      val get_reason_unknown : Z3.Fixedpoint.fixedpoint -> string
      val get_num_levels :
        Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> int
      val get_cover_delta :
        Z3.Fixedpoint.fixedpoint ->
        int -> Z3.FuncDecl.func_decl -> Z3.Expr.expr option
      val add_cover :
        Z3.Fixedpoint.fixedpoint ->
        int -> Z3.FuncDecl.func_decl -> Z3.Expr.expr -> unit
      val to_string : Z3.Fixedpoint.fixedpoint -> string
      val set_predicate_representation :
        Z3.Fixedpoint.fixedpoint ->
        Z3.FuncDecl.func_decl -> Z3.Symbol.symbol list -> unit
      val to_string_q :
        Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list -> string
      val get_rules : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list
      val get_assertions : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list
      val mk_fixedpoint : Z3.context -> Z3.Fixedpoint.fixedpoint
      val get_statistics :
        Z3.Fixedpoint.fixedpoint -> Z3.Statistics.statistics
      val parse_string :
        Z3.Fixedpoint.fixedpoint -> string -> Z3.Expr.expr list
      val parse_file :
        Z3.Fixedpoint.fixedpoint -> string -> Z3.Expr.expr list
    end
  module Optimize :
    sig
      type optimize
      type handle
      val mk_opt : Z3.context -> Z3.Optimize.optimize
      val get_help : Z3.Optimize.optimize -> string
      val set_parameters : Z3.Optimize.optimize -> Z3.Params.params -> unit
      val get_param_descrs :
        Z3.Optimize.optimize -> Z3.Params.ParamDescrs.param_descrs
      val add : Z3.Optimize.optimize -> Z3.Expr.expr list -> unit
      val add_soft :
        Z3.Optimize.optimize ->
        Z3.Expr.expr -> string -> Z3.Symbol.symbol -> Z3.Optimize.handle
      val maximize :
        Z3.Optimize.optimize -> Z3.Expr.expr -> Z3.Optimize.handle
      val minimize :
        Z3.Optimize.optimize -> Z3.Expr.expr -> Z3.Optimize.handle
      val check : Z3.Optimize.optimize -> Z3.Solver.status
      val get_model : Z3.Optimize.optimize -> Z3.Model.model option
      val get_lower : Z3.Optimize.handle -> Z3.Expr.expr
      val get_upper : Z3.Optimize.handle -> Z3.Expr.expr
      val push : Z3.Optimize.optimize -> unit
      val pop : Z3.Optimize.optimize -> unit
      val get_reason_unknown : Z3.Optimize.optimize -> string
      val to_string : Z3.Optimize.optimize -> string
      val get_statistics : Z3.Optimize.optimize -> Z3.Statistics.statistics
      val from_file : Z3.Optimize.optimize -> string -> unit
      val from_string : Z3.Optimize.optimize -> string -> unit
      val get_assertions : Z3.Optimize.optimize -> Z3.Expr.expr list
      val get_objectives : Z3.Optimize.optimize -> Z3.Expr.expr list
    end
  module SMT :
    sig
      val benchmark_to_smtstring :
        Z3.context ->
        string ->
        string ->
        string -> string -> Z3.Expr.expr list -> Z3.Expr.expr -> string
      val parse_smtlib2_string :
        Z3.context ->
        string ->
        Z3.Symbol.symbol list ->
        Z3.Sort.sort list ->
        Z3.Symbol.symbol list ->
        Z3.FuncDecl.func_decl list -> Z3.AST.ASTVector.ast_vector
      val parse_smtlib2_file :
        Z3.context ->
        string ->
        Z3.Symbol.symbol list ->
        Z3.Sort.sort list ->
        Z3.Symbol.symbol list ->
        Z3.FuncDecl.func_decl list -> Z3.AST.ASTVector.ast_vector
    end
  module RCF :
    sig
      type rcf_num
      val del : Z3.context -> Z3.RCF.rcf_num -> unit
      val del_list : Z3.context -> Z3.RCF.rcf_num list -> unit
      val mk_rational : Z3.context -> string -> Z3.RCF.rcf_num
      val mk_small_int : Z3.context -> int -> Z3.RCF.rcf_num
      val mk_pi : Z3.context -> Z3.RCF.rcf_num
      val mk_e : Z3.context -> Z3.RCF.rcf_num
      val mk_infinitesimal : Z3.context -> Z3.RCF.rcf_num
      val mk_roots : Z3.context -> Z3.RCF.rcf_num list -> Z3.RCF.rcf_num list
      val add :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val sub :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val mul :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val div :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val neg : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val inv : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
      val power : Z3.context -> Z3.RCF.rcf_num -> int -> Z3.RCF.rcf_num
      val lt : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val gt : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val le : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val ge : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val eq : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val neq : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
      val num_to_string :
        Z3.context -> Z3.RCF.rcf_num -> bool -> bool -> string
      val num_to_decimal_string :
        Z3.context -> Z3.RCF.rcf_num -> int -> string
      val get_numerator_denominator :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num * Z3.RCF.rcf_num
      val is_rational : Z3.context -> Z3.RCF.rcf_num -> bool
      val is_algebraic : Z3.context -> Z3.RCF.rcf_num -> bool
      val is_infinitesimal : Z3.context -> Z3.RCF.rcf_num -> bool
      val is_transcendental : Z3.context -> Z3.RCF.rcf_num -> bool
      val extension_index : Z3.context -> Z3.RCF.rcf_num -> int
      val transcendental_name :
        Z3.context -> Z3.RCF.rcf_num -> Z3.Symbol.symbol
      val infinitesimal_name :
        Z3.context -> Z3.RCF.rcf_num -> Z3.Symbol.symbol
      val num_coefficients : Z3.context -> Z3.RCF.rcf_num -> int
      val get_coefficient :
        Z3.context -> Z3.RCF.rcf_num -> int -> Z3.RCF.rcf_num
      val coefficients : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num list
      val sign_condition_sign : Z3.context -> Z3.RCF.rcf_num -> int -> int
      val num_sign_condition_coefficients :
        Z3.context -> Z3.RCF.rcf_num -> int -> int
      val sign_condition_coefficient :
        Z3.context -> Z3.RCF.rcf_num -> int -> int -> Z3.RCF.rcf_num
      val sign_conditions :
        Z3.context -> Z3.RCF.rcf_num -> (Z3.RCF.rcf_num list * int) list
      type interval = {
        lower_is_inf : bool;
        lower_is_open : bool;
        lower : Z3.RCF.rcf_num;
        upper_is_inf : bool;
        upper_is_open : bool;
        upper : Z3.RCF.rcf_num;
      }
      val root_interval :
        Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.interval option
      type root = {
        obj : Z3.RCF.rcf_num;
        polynomial : Z3.RCF.rcf_num list;
        interval : Z3.RCF.interval option;
        sign_conditions : (Z3.RCF.rcf_num list * int) list;
      }
      val roots : Z3.context -> Z3.RCF.rcf_num list -> Z3.RCF.root list
      val del_root : Z3.context -> Z3.RCF.root -> unit
      val del_roots : Z3.context -> Z3.RCF.root list -> unit
    end
  val set_global_param : string -> string -> unit
  val get_global_param : string -> string option
  val global_param_reset_all : unit -> unit
  val toggle_warning_messages : bool -> unit
  val enable_trace : string -> unit
  val disable_trace : string -> unit
  module Memory : sig val reset : unit -> unit end
end