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