## 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 : *) |