-
Notifications
You must be signed in to change notification settings - Fork 1
/
idd.mli
173 lines (121 loc) · 5.07 KB
/
idd.mli
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
(**************************************************************************)
(* *)
(* Copyright (C) Jean-Christophe Filliatre *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** {1 Integer Dichotomy Diagrams}
This module implements very large natural numbers following this paper:
Jean Vuillemin.
Efficient Data Structure and Algorithms for Sparse Integers,
Sets and Predicates, ARITH 2009.
Internally, it represents a number as a triple [x,y,z], that stands
for [x + 2^(2^y) * z], where [x, y, z] are three other numbers.
Such triples are hash-consed, and thus we get ternary dags, similar
to binary decision diagrams, hence the name. Leaves are the numbers
0 and 1.
*)
type idd
(** The abstract type of natural numbers. Persistent. *)
(** {2 Arithmetic operations} *)
val zero: idd
val one : idd
val two : idd
val three: idd
val four: idd
val five: idd
val pred: idd -> idd
(** pred(n) = n-1 *)
val succ: idd -> idd
(** succ(n) = n+1 *)
val add: idd -> idd -> idd
(** addition *)
val sub: idd -> idd -> idd
(** subtraction, assuming a >= b.
Raises [Invalid_argument] if [a < b]. *)
val mul: idd -> idd -> idd
(** multiplication *)
val twice: idd -> idd
(** 2n *)
val rmsb: idd -> idd * idd
(** remove most significant bit i.e.
rmsb n = (n - 2^i, i = l(n) - 1) for n > 0
Raises [Invalid_argument] is [n] is 0. *)
(** {2 Bitwise operations} *)
val logand: idd -> idd -> idd
val logor : idd -> idd -> idd
val logxor: idd -> idd -> idd
(** {2 Some particular numbers} *)
val x: idd -> idd
(** x(p) = 2^(2^p) *)
val x': idd -> idd
(** x'(q) = x(q) - 1 = 2^(2^q) - 1 *)
val c: idd -> idd -> idd -> idd
(** [c lo p hi] returns [lo + x(p) * hi], with no constraint on [p],
[lo] and [hi]. *)
val h: int -> idd
(** huge numbers: h(0) = 1, h(n) = c h(n-1) h(n-1) h(n-1)
largest number that can be represented using n nodes *)
val power2: idd -> idd
(** 2^i *)
(** {2 Sizes} *)
val l: idd -> idd
(** binary length = number of significant bits *)
val ll: idd -> idd
(** binary depth ll(n) = if n < 2 then 0 else l(l(n) - 1) *)
val size: idd -> int
(** number of distinct nodes (zero and one excluded) *)
val tree_size: idd -> int
(** number of nodes when considered as a tree (zero and one excluded)
CAVEAT: the result can be large and can overflow type int *)
(** {2 Comparisons} *)
val equal: idd -> idd -> bool
(** equality test (constant time!) *)
val compare: idd -> idd -> int
(** sign of the difference, that is -1, 0, or 1 *)
(** {2 Bitwise operations} *)
val pop: idd -> idd
(** population count *)
val xor1: idd -> idd
(** n xor 1 *)
(** {2 Conversions and pretty-printing} *)
val idd_max_int: idd
val to_int: idd -> int
(** raises [Invalid_argument] if [n] is too large *)
val of_int: int -> idd
val print: Format.formatter -> idd -> unit
(** prints a number n>1 in the following format {[
2 = (0, 0, 1)
3 = (1, 0, 1)
4 = (2, 2, 3)
5 = (4, 3, 3)
]} where [0] and [1] means [zero] and [one], and other numbers
stand for node references (so [4] above does not stand for the number
4 but for a node named [4] and built by applying function [c]
to nodes named [2], [2], and [3] that were previsouly built. *)
val parse: string list -> idd
(** parses a list of strings in the format used by [print] (see above) *)
val printer: Format.formatter -> idd -> unit
(** prints a number as a value of type [int], when possible,
and with function [print] above in any case *)
val print2: max_digits:int -> Format.formatter -> idd -> unit
(** Prints a number in base 2.
Raises [Invalid_argument] if the number of digits exceeds [max_digits].
This is a guard against any attempt at printing a too large number. *)
(** {2 Hash tables and memo functions} *)
val hash: idd -> int
(** runs in O(1) *)
module H1: Hashtbl.S with type key = idd
module H2: Hashtbl.S with type key = idd * idd
(** efficient hash tables, with O(1) hash and equality *)
val memo_rec1: ((idd -> 'a) -> idd -> 'a) -> idd -> 'a
val memo_rec2: ((idd -> idd -> 'a) -> idd -> idd -> 'a) -> idd -> idd -> 'a
(** memoization fixpoint operators, based on [H1] and [H2] *)