Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / MiscSolver.ml @ 7c4d2eb4

History | View | Annotate | Download (21.4 KB)

1
(** Common functions and data structures (e.g. bitsets)
2
    which are shared by most of the decision procedures.
3
    @author Florian Widmann
4
 *)
5

    
6

    
7
(** This value must be (smaller than or) equal to the bit width
8
    of the architecture on which this code is running.
9
 *)
10
let bitwidth = Sys.word_size
11

    
12

    
13
(** This table maps formulae (represented as integers)
14
    to their "types" (i.e. and, or, <>, etc;
15
    represented as integers).
16
 *)
17
let arrayType = ref (Array.make 0 (-1))
18

    
19
(** These lookup tables map formulae (represented as integers)
20
    to their decompositions (represented as integers).
21
    This is done according to the rules of the tableau procedure
22
    and depends on the type of the formulae.
23
 *)
24
let arrayDest1 = ref (Array.make 0 (-1))
25
let arrayDest2 = ref (Array.make 0 (-1))
26

    
27
(** This lookup table maps formulae (represented as integers)
28
    to their negation (in negation normal form).
29
 *)
30
let arrayNeg = ref (Array.make 0 (-1))
31

    
32

    
33
(** The number of nodes in a tableau.
34
 *)
35
let nodecount = ref 0
36

    
37
(** The longest path in a tableau.
38
 *)
39
let pathlength = ref 0
40

    
41
(** Counter that is used to assign unique id numbers to nodes.
42
 *)
43
let idcount = ref 0
44

    
45
(** Returns an unused id number.
46
 *)
47
let getNewId () =
48
  if !idcount < max_int then begin incr idcount; !idcount end
49
  else raise (Failure "Id overflow!")
50

    
51
(** A running number which is increased for each invocation of some functions.
52
    Hence each such invocation is mapped to a unique value of this variable.
53
    The variable is used to determine
54
    whether a function (e.g. detPrsEntry) has already been invoked
55
    with the same arguments under the same invocation of detStatusSpecial.
56
 *) 
57
let cacherun = ref 0
58

    
59
(** Counter that is used to assign time stamps
60
    reflecting the postfix order of the nodes.
61
 *)
62
let postfixcount = ref 0
63

    
64

    
65
(** An instantiation of a set (of the standard library)
66
    for formulae (in integer representation).
67
 *)
68
module FSet = Set.Make(
69
  struct
70
    type t = int
71
    let compare (i1 : int) i2 = compare i1 i2
72
  end
73
 )
74

    
75
(** An instantiation of a map (of the standard library)
76
    for formulae (in integer representation).
77
 *)
78
module FMap = Map.Make(
79
  struct
80
    type t = int
81
    let compare (i1 : int) i2 = compare i1 i2
82
  end
83
 )
84

    
85

    
86
(** The number of formulae which must be positive.
87
    The formulae are represented by the integers 0..(nrFormulae-1).
88
    It is assumed that formulae of the same type are grouped together
89
    (e.g. EX-formulae are exactly the formulae with index in [lposEX..hposEX]).
90
    It is further assumed that all principal formulae (e.g. or-formulae) come first,
91
    then come the EX-formulae, then the AX-formulae, and finally all remaining formulae.
92
 *)
93
let nrFormulae = ref (-1)
94

    
95
(** The lowest integer representing an EX-formula.
96
    If there are no EX-formulae, we distinguish two cases:
97
    1) If there are no principal formulae
98
    then it must hold lposEX = 0 and hposEX = (-1).
99
    2) If idx is the greatest index of a principal formulae
100
    then it must hold lposEX = idx + 1 and hposEX = idx.
101
 *)
102
let lposEX = ref (-1)
103

    
104
(** The greatest integer representing an EX-formula (see also lposEX).
105
 *)
106
let hposEX = ref (-1)
107

    
108
(** The greatest index in the bit vector
109
    that contains an EX-formula or a principal formula.
110
    It must be (-1) if no such formula exists.
111
 *)
112
let idxPF = ref (-1)
113

    
114
(** The lowest integer representing an AX-formula.
115
    The AX-formulae have to follow the EX-formulae directly,
116
    that is lposAX = hposEX + 1, even when there does not exists an AX-formula.
117
 *)
118
let lposAX = ref (-1)
119

    
120
(** The greatest integer representing an AX-formula.
121
    If there are no AX-formulae then it must hold hposAX = lposAX - 1.
122
 *)
123
let hposAX = ref (-1)
124

    
125
(** The integer representing the formula False.
126
    It must hold that !arrayNeg.(bsfalse) = bstrue.
127
 *)
128
let bsfalse = ref (-1)
129

    
130
(** The integer representing the formula True.
131
    It must hold that !arrayNeg.(bstrue) = bsfalse.
132
 *)
133
let bstrue = ref (-1)
134

    
135

    
136
(** Represents a set of formulae as a bit vector.
137
    All sets contain the formula True, that is bstrue,
138
    which is needed to detect whether False, that is bsfalse,
139
    is inserted.
140
 *)
141
type bitset = int array
142

    
143
(** The number of elements that are stored in one integer of the array.
144
    It has to be strictly smaller than the bit width of the system
145
    (due to the way ocaml handles integers).
146
 *)
147
let bsintsize = bitwidth - 1
148

    
149
(** The size of the arrays implementing the bitsets.
150
 *)
151
let bssize = ref (-1)
152

    
153
(** The greatest index of the arrays implementing the bitsets.
154
    It must hold that bssize = bsindex + 1.
155
 *)
156
let bsindex = ref (-1)
157

    
158
(** A dummy bitset that can be used if a bitset is needed
159
    before this module is initialised.
160
    It must never been actually used.
161
 *)
162
let dummyBS = Array.make 0 0
163

    
164
(** Copies the content of one bitset to another bitset.
165
    @param src The source bitset.
166
    @param trg The target bitset.
167
 *)
168
let blitBS (src : bitset) trg = Array.blit src 0 trg 0 !bssize
169

    
170
(** Creates a clone of a bitset.
171
    @param bs A bitset.
172
    @return A new bitset with the same content as bs.
173
 *)
174
let copyBS (bs : bitset) = Array.copy bs
175

    
176
(** Compares two bitsets. The order is (more or less) lexicographic.
177
    @param bs1 The first bitset.
178
    @param bs2 The second bitset.
179
    @param i The current index of the array.
180
    @return -1 if bs1 is smaller than bs2, 1 if bs1 is greater than bs2,
181
    and 0 if the sets are equal.
182
 *)
183
let rec intern_compBS (bs1 : bitset) bs2 i =
184
  if i >= 0 then
185
    let n1 = bs1.(i) in
186
    let n2 = bs2.(i) in
187
    if n1 = n2 then intern_compBS bs1 bs2 (pred i)
188
    else if n1 < n2 then (-1) else 1
189
  else 0
190

    
191
let compareBS (bs1 : bitset) bs2 = intern_compBS bs1 bs2 !bsindex
192

    
193
(** Computes a hash value for a bitset.
194
    It implements the One-at-a-Time hash invented by Bob Jenkins.
195
    @param bs A bitset.
196
    @param acc The hash value computed so far.
197
    @param i The current index of the array.
198
    @return The hash value of bs.
199
 *)
200
let rec intern_hashBS bs acc i =
201
  if i >= 0 then
202
    let acc1 = acc + bs.(i) in
203
    let acc2 = acc1 + (acc1 lsl 10) in
204
    let acc3 = acc2 lxor (acc2 lsr 6) in
205
    intern_hashBS bs acc3 (pred i)
206
  else
207
    let acc1 = acc + (acc lsl 3) in
208
    let acc2 = acc1 lxor (acc1 lsr 11) in
209
    acc2 + (acc lsl 15)
210

    
211
let hashBS bs = intern_hashBS bs 0 !bsindex
212

    
213
(** Tests whether a formula is an element of a set of formulae.
214
    @param bs A bitset of formulae.
215
    @param f The integer representation of a formula.
216
    @return True iff f is an element of bs.
217
 *)
218
let memBS bs f =
219
  let idx = f / bsintsize in
220
  let pos = f mod bsintsize in
221
  (bs.(idx) land (1 lsl pos)) <> 0
222

    
223
(** Removes a formula from a bitset.
224
    @param bs A bitset of formulae.
225
    @param f The integer representation of a formula
226
    which must not be bstrue.
227
 *)
228
let remBS bs f =
229
  let idx = f / bsintsize in
230
  let pos = f mod bsintsize in
231
  let pset = bs.(idx) in
232
  let pattern = (-1) lxor (1 lsl pos) in
233
  let npset = pset land pattern in
234
  if npset <> pset then bs.(idx) <- npset else ()
235

    
236
(** Adds a formula to a set of formulae.
237
    @param bs A bitset of formulae.
238
    @param f The integer representation of a formula that is to be added to bs.
239
    @return True iff inserting f leads to a new contradiction.
240
 *)
241
let addBS bs f =
242
  let idx = f / bsintsize in
243
  let pos = f mod bsintsize in
244
  let pset = bs.(idx) in
245
  let pattern = 1 lsl pos in
246
  let npset = pset lor pattern in
247
  if npset <> pset then begin
248
    bs.(idx) <- npset;
249
    let f1 = !arrayNeg.(f) in
250
    f1 >= 0 && f1 < !nrFormulae && memBS bs f1
251
  end
252
  else false
253

    
254
(** Adds a formula to a set of formulae.
255
    @param bs A bitset of formulae.
256
    @param f The integer representation of a formula that is to be added to bs.
257
 *)
258
let addBSNoChk bs f =
259
  let idx = f / bsintsize in
260
  let pos = f mod bsintsize in
261
  let pset = bs.(idx) in
262
  let pattern = 1 lsl pos in
263
  let npset = pset lor pattern in
264
  if npset <> pset then bs.(idx) <- npset else ()
265

    
266
(** Adds a formula to two sets of formulae
267
    if it is not already contained in the second one.
268
    @param bs A bitset of formulae.
269
    @param bsc The saturated bitset of bs.
270
    @param f The integer representation of a formula that is to be added to bs and bsc.
271
    @return True iff inserting f into bsc leads to a new contradiction.
272
 *)
273
let addBSc bs bsc f =
274
  let idx = f / bsintsize in
275
  let pos = f mod bsintsize in
276
  let psetc = bsc.(idx) in
277
  let pattern = 1 lsl pos in
278
  let npsetc = psetc lor pattern in
279
  if npsetc <> psetc then begin
280
    bsc.(idx) <- npsetc;
281
    bs.(idx) <- bs.(idx) lor pattern;
282
    let f1 = !arrayNeg.(f) in
283
    f1 >= 0 && f1 < !nrFormulae && memBS bsc f1
284
  end
285
  else false
286

    
287
(** Creates an "empty" bitset.
288
    @return A bitset which only contains bstrue.
289
 *)
290
let makeBS () =
291
  let bs = Array.make !bssize 0 in
292
  addBSNoChk bs !bstrue;
293
  bs
294

    
295
(** "Empties" a bitset such that it only contains bstrue.
296
    @param bs A bitset.
297
 *)
298
let emptyBS bs =
299
  Array.fill bs 0 !bssize 0;
300
  addBSNoChk bs !bstrue
301

    
302
(** Creates the union of two bitsets without checking for contradictions.
303
    @param bs1 The first bitset.
304
    @param bs2 The second bitset.
305
    @return A bitset representing the union of bs1 and bs2.
306
 *)    
307
let unionBSNoChk bs1 bs2 =
308
  let res = makeBS () in
309
  for i = 0 to !bsindex do
310
    res.(i) <- bs1.(i) lor bs2.(i)
311
  done;
312
  res
313

    
314
(** Iterates through a set of formulae and invokes a given function
315
    on each formula in the set.
316
    @param f A function from integers (representing formulae) to unit.
317
    @param bs A bitset of formulae.
318
 *)
319
let iterBS f bs =
320
  for i = 0 to pred !nrFormulae do
321
    if memBS bs i then f i else ()
322
  done
323

    
324
(* Folds over the formulae in a set of formulae.
325
   @param f A function taking an integer (presenting a formula)
326
   and an intermediate result and returning a new result.
327
   @param bs A bitset of formulae {e_1, e_2, ..., e_n}.
328
   @param init An initial value.
329
   @return The value f e_n ( ... f e_2 (f e_1 init))
330
 *)
331
let foldBS f bs init =
332
  let res = ref init in
333
  for i = 0 to pred !nrFormulae do
334
    if memBS bs i then res := f i !res else ()
335
  done;
336
  !res
337

    
338

    
339
(** Represents a set of annotated formulae as a bit vector.
340
    All sets contain the formula True, that is bstrue,
341
    which is needed to detect whether False, that is bsfalse,
342
    is inserted.
343
 *)
344
type annbitset = int array
345

    
346
(** The number of elements that are stored in one integer of the array.
347
    It has to be strictly smaller than the bitsize of the system
348
    divided by two since we need two bits per entry
349
    (the "strictly" is due to the way ocaml handles integers).
350
 *)
351
let annbsintsize = bsintsize / 2
352

    
353
(** Constant for "element not contained in annotated bitset".
354
 *)
355
let absNotIn = 0
356

    
357
(** Constant for "element contained but not annotated in annotated bitset".
358
 *)
359
let absUnAnn = 3
360

    
361
(** Constant for "element contained and annotated with 1 in annotated bitset".
362
 *)
363
let absAnn1 = 1
364

    
365
(** Constant for "element contained and annotated with 2 in annotated bitset".
366
 *)
367
let absAnn2 = 2
368

    
369
(** The size of the arrays implementing the annotated bitsets.
370
 *)
371
let abssize = ref (-1)
372

    
373
(** The greatest index of the arrays implementing the annotated bitsets.
374
    It must hold that abssize = absindex + 1.
375
 *)
376
let absindex = ref (-1)
377

    
378
(** A dummy annotated bitset that can be used if an annotated bitset is needed
379
    before this module is initialised.
380
    It must never been actually used.
381
 *)
382
let dummyABS = Array.make 0 0
383

    
384
(** Copies the content of one annotated bitset to another annotated bitset.
385
    @param src The source annotated bitset.
386
    @param trg The target annotated bitset.
387
 *)
388
let blitABS (src : annbitset) trg = Array.blit src 0 trg 0 !abssize
389

    
390
(** Creates a clone of an annotated bitset.
391
    @param abs An annotated bitset.
392
    @return A new annotated bitset with the same content as abs.
393
 *)
394
let copyABS (abs : annbitset) = Array.copy abs
395

    
396
(** Compares two annotated bitsets. The order is (more or less) lexicographic.
397
    @param abs1 The first annotated bitset.
398
    @param abs2 The second annotated bitset.
399
    @param i The current index of the array.
400
    @return -1 if abs1 is smaller than abs2, 1 if abs1 is greater than abs2,
401
    and 0 if the sets are equal.
402
 *)
403
let rec intern_compABS (abs1 : annbitset) abs2 i =
404
  if i >= 0 then
405
    let n1 = abs1.(i) in
406
    let n2 = abs2.(i) in
407
    if n1 = n2 then intern_compABS abs1 abs2 (pred i)
408
    else if n1 < n2 then (-1) else 1
409
  else 0
410

    
411
let compareABS (abs1 : annbitset) abs2 = intern_compABS abs1 abs2 !absindex
412

    
413
(** Computes a hash value for an annotated bitset.
414
    It implements the One-at-a-Time hash invented by Bob Jenkins.
415
    @param abs An annotated bitset.
416
    @param acc The hash value computed so far.
417
    @param i The current index of the array.
418
    @return The hash value of bs.
419
 *)
420
let rec intern_hashABS abs acc i =
421
  if i >= 0 then
422
    let acc1 = acc + abs.(i) in
423
    let acc2 = acc1 + (acc1 lsl 10) in
424
    let acc3 = acc2 lxor (acc2 lsr 6) in
425
    intern_hashABS abs acc3 (pred i)
426
  else
427
    let acc1 = acc + (acc lsl 3) in
428
    let acc2 = acc1 lxor (acc1 lsr 11) in
429
    acc2 + (acc lsl 15)
430

    
431
let hashABS abs = intern_hashABS abs 0 !absindex
432

    
433
(** Tests whether a formula is an element of an annotated set of formulae
434
    and, if yes, determines its annotation.
435
    @param abs An annotated bitset of formulae.
436
    @param f The integer representation of a formula.
437
    @return The appropriate return code
438
    (one of absNotIn, absUnAnn, absAnn1, absAnn2).
439
 *)
440
let getAnnABS abs f =
441
  let idx = f / annbsintsize in
442
  let pos = (f mod annbsintsize) lsl 1 in
443
  (abs.(idx) lsr pos) land 3
444

    
445
(** Sets the annotation status of a formula in an annotated set of formulae.
446
    The old annotation status is overridden.
447
    @param abs An annotated bitset of formulae.
448
    @param f The integer representation of a formula
449
    whose annotation status is to be set.
450
    @param ann The (new) annotation status of f
451
    (must be one of absNotIn, absUnAnn, absAnn1, absAnn2).
452
 *)
453
let setAnnABS abs f ann =
454
  let idx = f / annbsintsize in
455
  let pos = (f mod annbsintsize) lsl 1 in
456
  let pset = abs.(idx) in
457
  let pset1 = pset land ((-1) lxor (3 lsl pos)) in
458
  let pattern = (ann land 3) lsl pos in
459
  let npset = pset1 lor pattern in
460
  if npset <> pset then abs.(idx) <- npset else ()
461

    
462
(** Tests whether a formula is an element of an annotated set of formulae.
463
    @param abs An annotated bitset of formulae.
464
    @param f The integer representation of a formula.
465
    @return True iff f is an element of abs (annotated or not).
466
 *)
467
let memABS abs f =
468
  let idx = f / annbsintsize in
469
  let pos = (f mod annbsintsize) lsl 1 in
470
  (abs.(idx) land (3 lsl pos)) <> 0
471

    
472
(** Removes a formula from an annotated bitset.
473
    @param abs An annotated bitset of formulae.
474
    @param f The integer representation of a formula
475
    which must not be bstrue.
476
 *)
477
let remABS abs f =
478
  let idx = f / annbsintsize in
479
  let pos = (f mod annbsintsize) lsl 1 in
480
  let pset = abs.(idx) in
481
  let pattern = (-1) lxor (3 lsl pos) in
482
  let npset = pset land pattern in
483
  if npset <> pset then abs.(idx) <- npset else ()
484

    
485
(** Adds a formula without annotation to an annotated set of formulae
486
    if it is not already contained in the set (annotated or not).
487
    @param abs An annotated bitset of formulae.
488
    @param f The integer representation of a formula that is to be added to abs.
489
    @return True iff inserting f leads to a new contradiction.
490
 *)
491
let addABS abs f =
492
  let idx = f / annbsintsize in
493
  let pos = (f mod annbsintsize) lsl 1 in
494
  let pset = abs.(idx) in
495
  let pattern = 3 lsl pos in
496
  if (pset land pattern) = 0 then begin
497
    abs.(idx) <- pset lor pattern;
498
    let f1 = !arrayNeg.(f) in
499
    f1 >= 0 && f1 < !nrFormulae && memABS abs f1
500
  end
501
  else false
502

    
503
(** Adds a formula to two sets of formulae
504
    if it is not already contained in the second one.
505
    @param bs A bitset of formulae.
506
    @param abs An annotated bitset of formulae.
507
    @param f The integer representation of a formula that is to be added to bs and abs.
508
    @return True iff inserting f into abs leads to a new contradiction.
509
 *)
510
let addBSa bs abs f =
511
  let idx = f / annbsintsize in
512
  let pos = (f mod annbsintsize) lsl 1 in
513
  let apset = abs.(idx) in
514
  let pattern = 3 lsl pos in
515
  if (apset land pattern) = 0 then begin
516
    abs.(idx) <- apset lor pattern;
517
    addBSNoChk bs f;
518
    let f1 = !arrayNeg.(f) in
519
    f1 >= 0 && f1 < !nrFormulae && memABS abs f1
520
  end
521
  else false
522

    
523
(** Creates an "empty" annotated bitset.
524
    @return An annotated bitset which only contains bstrue (unannotated).
525
 *)
526
let makeABS () =
527
  let abs = Array.make !abssize 0 in
528
  setAnnABS abs !bstrue absUnAnn;
529
  abs
530

    
531
(** "Empties" an annotated bitset such that it only contains bstrue (unannotated).
532
    @param abs An annotated bitset.
533
 *)
534
let emptyABS abs =
535
  Array.fill abs 0 !abssize 0;
536
  setAnnABS abs !bstrue absUnAnn
537

    
538
(** Copies the content of an annotated bitset to a bitset.
539
    @param src The annotated source bitset.
540
    @param trg The target bitset.
541
 *)
542
let blitBSa (src : annbitset) (trg : bitset) =
543
  for i = 0 to pred !nrFormulae do
544
    if memABS src i then addBSNoChk trg i else ()
545
  done
546

    
547

    
548
(** Selects a principal formula from a set of formulae if possible.
549
    @param bs A bitset of formulae.
550
    @param maxpf The greatest integer that represents a principal formula.
551
    @param bnd The greatest index in the array that contains a principal formula.
552
    @param i The current index of the array.
553
    @return -1 iff no principal formula is found,
554
    the principal formula otherwise.
555
 *)
556
let rec intern_getPF bs maxpf bnd i =
557
  if i <= bnd then
558
    let n = bs.(i) in
559
    if n = 0 then intern_getPF bs maxpf bnd (succ i)
560
    else
561
      let j = ref 0 in
562
      let notfound = ref true in
563
      let _ =
564
        while !notfound do
565
          if (n land (1 lsl !j)) = 0 then incr j
566
          else notfound := false
567
        done
568
      in
569
      let res = i * bsintsize + !j in
570
      if res <= maxpf then res else (-1)
571
  else (-1)
572

    
573
let getPFinclEX bs = intern_getPF bs !hposEX !idxPF 0
574

    
575
let getPFexclEX bs = intern_getPF bs (pred !lposEX) !idxPF 0
576

    
577

    
578
(** Constructs a list of all EX-formulae of a set of formulae.
579
    @param bs The bitset of formulae.
580
    @param bnd The greatest integer representing an EX-formula.
581
    @param acc A list of EX-formulae gathered till now.
582
    @param i The current index of the array.
583
    @return A list of all EX-formulae f (in decreasing order) in bs.
584
 *)
585
let rec intern_mkEXList bs bnd acc i =
586
  if i >= bnd then
587
    if memBS bs i then intern_mkEXList bs bnd (i::acc) (pred i) 
588
    else intern_mkEXList bs bnd acc (pred i)
589
  else acc
590

    
591
let mkEXList bs = intern_mkEXList bs !lposEX [] !hposEX
592

    
593
(** Constructs a list of all EX-formulae of a set of annotated formulae.
594
    @param abs The annotated bitset of formulae.
595
    @param bnd The greatest integer representing an EX-formula.
596
    @param acc A list of EX-formulae gathered till now.
597
    @param i The current index of the array.
598
    @return A list of all EX-formulae f (in decreasing order) in abs.
599
 *)
600
let rec intern_mkEXListAnn abs bnd acc i =
601
  if i >= bnd then
602
    if memABS abs i then intern_mkEXListAnn abs bnd (i::acc) (pred i) 
603
    else intern_mkEXListAnn abs bnd acc (pred i)
604
  else acc
605

    
606
let mkEXListAnn abs = intern_mkEXListAnn abs !lposEX [] !hposEX
607

    
608

    
609
(** Prints a "collection" as a set.
610
    @param ps A string prefixing the set.
611
    @param f A function converting the collection c into a list of strings.
612
    @param c A "collection".
613
    @return If f c = [a1, ..., an] then the resulting string
614
    will be "ps { a1, ..., an }".
615
 *)
616
let exportAsSet ps f c =
617
  let rec fold acc = function
618
    | [] -> acc
619
    | [h] -> acc ^ h
620
    | h::t -> fold (acc ^ h ^ ", ") t
621
  in
622
  ps ^ "{ " ^ (fold "" (f c)) ^ " }"
623

    
624
(** Converts a set of formulae into a list of strings
625
    where each string represents one formula of the set.
626
    @param expF A function which converts the formula in integer
627
    representations into a readable string.
628
    @param bs A bitset of formulae.
629
    @return A list of string representations of the formulae in bs.
630
 *)
631
let exportFSet expF bs = foldBS (fun i acc -> (expF i)::acc) bs []
632
(*
633
  let res = ref [] in
634
  for i = 0 to pred !nrFormulae do
635
    if memBS bs i then res := (expF i)::!res else ()
636
  done;
637
  !res
638
 *)
639

    
640
(** Converts an annotated set of formulae into a list of strings
641
    where each string represents one formula of the set and its annotation.
642
    @param expF A function which converts the formula in integer
643
    representations into a readable string.
644
    @param abs An annotated bitset of formulae.
645
    @return A list of string representations of the formulae in abs
646
    and their annotation.
647
 *)
648
let exportAnnFSet expF abs =
649
  let res = ref [] in
650
  for i = 0 to pred !nrFormulae do
651
    let ann = getAnnABS abs i in
652
    if ann <> absNotIn then
653
      let fstr = expF i in
654
      let afstr =
655
        if ann = absAnn1 then fstr ^ "(1)"
656
        else if ann = absAnn2 then fstr ^ "(2)"
657
        else fstr
658
      in
659
      res := afstr::!res
660
    else ()
661
  done;
662
  !res
663

    
664

    
665
(** Initialises the global fields of this module
666
    with the exception of the tables.
667
    This procedure must only be invoked once.
668
    @param size The number of formulae which must be positive (cf. nrFormulae).
669
    @param bsf cf. bsfalse
670
    @param bst cf. bstrue
671
    @param lEX cf. lposEX
672
    @param nrEX The number of EX-formulae.
673
    @param nrAX The number of AX-formulae.
674
 *)
675
let initMisc size bsf bst lEX nrEX nrAX =
676
  assert (size > 0);
677
  nrFormulae := size;
678
  bssize := (size - 1) / bsintsize + 1;
679
  assert (!bssize <= Sys.max_array_length);
680
  bsindex := pred !bssize;
681
  abssize := (size - 1) / annbsintsize + 1;
682
  assert (!abssize <= Sys.max_array_length);
683
  absindex := pred !abssize;
684
  bsfalse := bsf;
685
  bstrue := bst;
686
  lposEX := lEX;
687
  hposEX := !lposEX + nrEX - 1;
688
  idxPF := if !hposEX >= 0 then !hposEX / bsintsize else (-1);
689
  lposAX := succ !hposEX;
690
  hposAX := !lposAX + nrAX - 1;
691
  nodecount := 0;
692
  pathlength := 0;
693
  idcount := 0;
694
  cacherun := 0;
695
  postfixcount := 0