Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / MiscSolver.ml @ 946e8213

History | View | Annotate | Download (13.2 KB)

1 4fd28192 Thorsten WiƟmann
(** 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
(** Selects a principal formula from a set of formulae if possible.
340
    @param bs A bitset of formulae.
341
    @param maxpf The greatest integer that represents a principal formula.
342
    @param bnd The greatest index in the array that contains a principal formula.
343
    @param i The current index of the array.
344
    @return -1 iff no principal formula is found,
345
    the principal formula otherwise.
346
 *)
347
let rec intern_getPF bs maxpf bnd i =
348
  if i <= bnd then
349
    let n = bs.(i) in
350
    if n = 0 then intern_getPF bs maxpf bnd (succ i)
351
    else
352
      let j = ref 0 in
353
      let notfound = ref true in
354
      let _ =
355
        while !notfound do
356
          if (n land (1 lsl !j)) = 0 then incr j
357
          else notfound := false
358
        done
359
      in
360
      let res = i * bsintsize + !j in
361
      if res <= maxpf then res else (-1)
362
  else (-1)
363
364
let getPFinclEX bs = intern_getPF bs !hposEX !idxPF 0
365
366
let getPFexclEX bs = intern_getPF bs (pred !lposEX) !idxPF 0
367
368
369
(** Constructs a list of all EX-formulae of a set of formulae.
370
    @param bs The bitset of formulae.
371
    @param bnd The greatest integer representing an EX-formula.
372
    @param acc A list of EX-formulae gathered till now.
373
    @param i The current index of the array.
374
    @return A list of all EX-formulae f (in decreasing order) in bs.
375
 *)
376
let rec intern_mkEXList bs bnd acc i =
377
  if i >= bnd then
378
    if memBS bs i then intern_mkEXList bs bnd (i::acc) (pred i) 
379
    else intern_mkEXList bs bnd acc (pred i)
380
  else acc
381
382
let mkEXList bs = intern_mkEXList bs !lposEX [] !hposEX
383
384
(** Prints a "collection" as a set.
385
    @param ps A string prefixing the set.
386
    @param f A function converting the collection c into a list of strings.
387
    @param c A "collection".
388
    @return If f c = [a1, ..., an] then the resulting string
389
    will be "ps { a1, ..., an }".
390
 *)
391
let exportAsSet ps f c =
392
  let rec fold acc = function
393
    | [] -> acc
394
    | [h] -> acc ^ h
395
    | h::t -> fold (acc ^ h ^ ", ") t
396
  in
397
  ps ^ "{ " ^ (fold "" (f c)) ^ " }"
398
399
(** Converts a set of formulae into a list of strings
400
    where each string represents one formula of the set.
401
    @param expF A function which converts the formula in integer
402
    representations into a readable string.
403
    @param bs A bitset of formulae.
404
    @return A list of string representations of the formulae in bs.
405
 *)
406
let exportFSet expF bs = foldBS (fun i acc -> (expF i)::acc) bs []
407
(*
408
  let res = ref [] in
409
  for i = 0 to pred !nrFormulae do
410
    if memBS bs i then res := (expF i)::!res else ()
411
  done;
412
  !res
413
 *)
414
415
416
(** Initialises the global fields of this module
417
    with the exception of the tables.
418
    This procedure must only be invoked once.
419
    @param size The number of formulae which must be positive (cf. nrFormulae).
420
    @param bsf cf. bsfalse
421
    @param bst cf. bstrue
422
    @param lEX cf. lposEX
423
    @param nrEX The number of EX-formulae.
424
    @param nrAX The number of AX-formulae.
425
 *)
426
let initMisc size bsf bst lEX nrEX nrAX =
427
  assert (size > 0);
428
  nrFormulae := size;
429
  bssize := (size - 1) / bsintsize + 1;
430
  assert (!bssize <= Sys.max_array_length);
431
  bsindex := pred !bssize;
432
  bsfalse := bsf;
433
  bstrue := bst;
434
  lposEX := lEX;
435
  hposEX := !lposEX + nrEX - 1;
436
  idxPF := if !hposEX >= 0 then !hposEX / bsintsize else (-1);
437
  lposAX := succ !hposEX;
438
  hposAX := !lposAX + nrAX - 1;
439
  nodecount := 0;
440
  pathlength := 0;
441
  idcount := 0;
442
  cacherun := 0;
443
  postfixcount := 0
444 a57eb439 Hans-Peter Deifel
445
(* vim: set et sw=2 sts=2 ts=8 : *)