Source file `sort.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(**************************************************************************)
(*  Bitwuzla: Satisfiability Modulo Theories (SMT) solver.                *)
(*                                                                        *)
(*  Copyright (C) 2023 by the authors listed in the AUTHORS file at       *)
(*  https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS                *)
(*                                                                        *)
(*  This file is part of Bitwuzla under the MIT license.                  *)
(*  See COPYING for more information at                                   *)
(*  https://github.com/bitwuzla/bitwuzla/blob/main/COPYING                *)
(**************************************************************************)

type t

external id : t -> (int64[@unboxed])
  = "ocaml_bitwuzla_cxx_sort_id" "native_bitwuzla_cxx_sort_id"

external compare : t -> t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_compare" "native_bitwuzla_cxx_sort_compare"

external equal : t -> t -> bool = "ocaml_bitwuzla_cxx_sort_equal"

external hash : t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_hash" "native_bitwuzla_cxx_sort_hash"

external bv_size : t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_bv_size" "native_bitwuzla_cxx_sort_bv_size"

external fp_exp_size : t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_fp_exp_size" "native_bitwuzla_cxx_sort_fp_exp_size"

external fp_sig_size : t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_fp_sig_size" "native_bitwuzla_cxx_sort_fp_sig_size"

external array_index : t -> t = "ocaml_bitwuzla_cxx_sort_array_index"

external array_element : t -> t = "ocaml_bitwuzla_cxx_sort_array_element"

external fun_domain : t -> t array = "ocaml_bitwuzla_cxx_sort_fun_domain"

external fun_codomain : t -> t = "ocaml_bitwuzla_cxx_sort_fun_codomain"

external fun_arity : t -> (int[@untagged])
  = "ocaml_bitwuzla_cxx_sort_fun_arity" "native_bitwuzla_cxx_sort_fun_arity"

external uninterpreted_symbol : t -> string
  = "ocaml_bitwuzla_cxx_sort_uninterpreted_symbol"

external is_array : t -> bool = "ocaml_bitwuzla_cxx_sort_is_array" [@@noalloc]

external is_bool : t -> bool = "ocaml_bitwuzla_cxx_sort_is_bool" [@@noalloc]

external is_bv : t -> bool = "ocaml_bitwuzla_cxx_sort_is_bv" [@@noalloc]

external is_fp : t -> bool = "ocaml_bitwuzla_cxx_sort_is_fp" [@@noalloc]

external is_fun : t -> bool = "ocaml_bitwuzla_cxx_sort_is_fun" [@@noalloc]

external is_rm : t -> bool = "ocaml_bitwuzla_cxx_sort_is_rm" [@@noalloc]

external is_uninterpreted : t -> bool
  = "ocaml_bitwuzla_cxx_sort_is_uninterpreted"
  [@@noalloc]

external to_string : t -> string = "ocaml_bitwuzla_cxx_sort_to_string"

external pp : Format.formatter -> t -> unit = "ocaml_bitwuzla_cxx_sort_pp"