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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
type value =
| Integer
| Rational
| Real
| Binary
| Hexadecimal
| Bitvector
| String
type t =
| Var
| Sort
| Term
| Attr
| Decl
| Track
| Value of value
let var = Var
let sort = Sort
let term = Term
let attr = Attr
let decl = Decl
let track = Track
let value_discr = function
| Integer -> 0
| Rational -> 1
| Real -> 2
| Binary -> 3
| Hexadecimal -> 4
| Bitvector -> 5
| String -> 6
let discr = function
| Var -> 0
| Sort -> 1
| Term -> 2
| Attr -> 3
| Decl -> 4
| Track -> 5
| Value v -> 6 + value_discr v
let hash a = Hashtbl.hash a
let compare a b = compare (discr a) (discr b)
let equal a b = a == b || compare a b = 0
let print_value fmt = function
| Integer -> Format.fprintf fmt "int"
| Rational -> Format.fprintf fmt "rat"
| Real -> Format.fprintf fmt "real"
| Binary -> Format.fprintf fmt "bin"
| Hexadecimal -> Format.fprintf fmt "hex"
| Bitvector -> Format.fprintf fmt "bitv"
| String -> Format.fprintf fmt "string"
let print fmt = function
| Var -> Format.fprintf fmt "var"
| Sort -> Format.fprintf fmt "sort"
| Term -> Format.fprintf fmt "term"
| Attr -> Format.fprintf fmt "attr"
| Decl -> Format.fprintf fmt "decl"
| Track -> Format.fprintf fmt "track"
| Value value -> Format.fprintf fmt "value:%a" print_value value
module Map = Maps.Make(struct
type nonrec t = t
let compare = compare
end)