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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
(* TEST *)
(* Translated to OCaml by Xavier Leroy *)
(* Original code written in SML by ... *)
type bdd = One | Zero | Node of bdd * int * int * bdd
let rec eval bdd vars =
match bdd with
Zero -> false
| One -> true
| Node(l, v, _, h) ->
if vars.(v) then eval h vars else eval l vars
let getId bdd =
match bdd with
Node(_,_,id,_) -> id
| Zero -> 0
| One -> 1
let initSize_1 = 8*1024 - 1
let nodeC = ref 1
let sz_1 = ref initSize_1
let htab = ref(Array.make (!sz_1+1) [])
let n_items = ref 0
let hashVal x y v = x lsl 1 + y + v lsl 2
let resize newSize =
let arr = !htab in
let newSz_1 = newSize-1 in
let newArr = Array.make newSize [] in
let rec copyBucket bucket =
match bucket with
[] -> ()
| n :: ns ->
match n with
| Node(l,v,_,h) ->
let ind = hashVal (getId l) (getId h) v land newSz_1
in
newArr.(ind) <- (n :: newArr.(ind));
copyBucket ns
| _ -> assert false
in
for n = 0 to !sz_1 do
copyBucket(arr.(n))
done;
htab := newArr;
sz_1 := newSz_1
let rec insert idl idh v ind bucket newNode =
if !n_items <= !sz_1
then ( (!htab).(ind) <- (newNode :: bucket);
incr n_items )
else ( resize(!sz_1 + !sz_1 + 2);
let ind = hashVal idl idh v land (!sz_1)
in
(!htab).(ind) <- newNode :: (!htab).(ind)
)
let resetUnique () = (
sz_1 := initSize_1;
htab := Array.make (!sz_1+1) [];
n_items := 0;
nodeC := 1
)
let mkNode low v high =
let idl = getId low in
let idh = getId high
in
if idl = idh
then low
else let ind = hashVal idl idh v land (!sz_1) in
let bucket = (!htab).(ind) in
let rec lookup b =
match b with
[] -> let n = Node(low, v, (incr nodeC; !nodeC), high)
in
insert (getId low) (getId high) v ind bucket n; n
| n :: ns ->
match n with
| Node(l,v',id,h) ->
if v = v' && idl = getId l && idh = getId h
then n else lookup ns
| _ -> assert false
in
lookup bucket
type ordering = LESS | EQUAL | GREATER
let cmpVar (x : int) (y : int) =
if x<y then LESS else if x>y then GREATER else EQUAL
let zero = Zero
let one = One
let mkVar x = mkNode zero x one
let cacheSize = 1999
let andslot1 = Array.make cacheSize 0
let andslot2 = Array.make cacheSize 0
let andslot3 = Array.make cacheSize zero
let xorslot1 = Array.make cacheSize 0
let xorslot2 = Array.make cacheSize 0
let xorslot3 = Array.make cacheSize zero
let notslot1 = Array.make cacheSize 0
let notslot2 = Array.make cacheSize one
let hash x y = ((x lsl 1)+y) mod cacheSize
let rec not n =
match n with
Zero -> One
| One -> Zero
| Node(l, v, id, r) -> let h = id mod cacheSize
in
if id=notslot1.(h) then notslot2.(h)
else let f = mkNode (not l) v (not r)
in
notslot1.(h) <- id; notslot2.(h) <- f; f
let rec and2 n1 n2 =
match n1 with
Node(l1, v1, i1, r1)
-> (match n2 with
Node(l2, v2, i2, r2)
-> let h = hash i1 i2
in
if i1=andslot1.(h) && i2=andslot2.(h) then andslot3.(h)
else let f = match cmpVar v1 v2 with
EQUAL -> mkNode (and2 l1 l2) v1 (and2 r1 r2)
| LESS -> mkNode (and2 l1 n2) v1 (and2 r1 n2)
| GREATER -> mkNode (and2 n1 l2) v2 (and2 n1 r2)
in
andslot1.(h) <- i1;
andslot2.(h) <- i2;
andslot3.(h) <- f;
f
| Zero -> Zero
| One -> n1)
| Zero -> Zero
| One -> n2
let rec xor n1 n2 =
match n1 with
Node(l1, v1, i1, r1)
-> (match n2 with
Node(l2, v2, i2, r2)
-> let h = hash i1 i2
in
if i1=andslot1.(h) && i2=andslot2.(h) then andslot3.(h)
else let f = match cmpVar v1 v2 with
EQUAL -> mkNode (xor l1 l2) v1 (xor r1 r2)
| LESS -> mkNode (xor l1 n2) v1 (xor r1 n2)
| GREATER -> mkNode (xor n1 l2) v2 (xor n1 r2)
in
andslot1.(h) <- i1;
andslot2.(h) <- i2;
andslot3.(h) <- f;
f
| Zero -> n1
| One -> not n1)
| Zero -> n2
| One -> not n2
let hwb n =
let rec h i j = if i=j
then mkVar i
else xor (and2 (not(mkVar j)) (h i (j-1)))
(and2 (mkVar j) (g i (j-1)))
and g i j = if i=j
then mkVar i
else xor (and2 (not(mkVar i)) (h (i+1) j))
(and2 (mkVar i) (g (i+1) j))
in
h 0 (n-1)
(* Testing *)
let seed = ref 0
let random() =
seed := !seed * 25173 + 17431; !seed land 1 > 0
let random_vars n =
let vars = Array.make n false in
for i = 0 to n - 1 do vars.(i) <- random() done;
vars
let test_hwb bdd vars =
(* We should have
eval bdd vars = vars.(n-1) if n > 0
eval bdd vars = false if n = 0
where n is the number of "true" elements in vars. *)
let ntrue = ref 0 in
for i = 0 to Array.length vars - 1 do
if vars.(i) then incr ntrue
done;
eval bdd vars = (if !ntrue > 0 then vars.(!ntrue-1) else false)
let main () =
let n =
if Array.length Sys.argv >= 2 then int_of_string Sys.argv.(1) else 20 in
let ntests =
if Array.length Sys.argv >= 3 then int_of_string Sys.argv.(2) else 10 in
let bdd = hwb n in
let succeeded = ref true in
for i = 1 to ntests do
succeeded := !succeeded && test_hwb bdd (random_vars n)
done;
if !succeeded
then print_string "OK\n"
else print_string "FAILED\n";
exit 0
let _ = main()
|
