## cool / src / lib / CoAlgMisc.ml @ de84f40d

History | View | Annotate | Download (45.8 KB)

1 | 4fd28192 | Thorsten Wißmann | (** Common types, functions, and data structures for the CoAlgebraic reasoner. |
---|---|---|---|

2 | @author Florian Widmann |
||

3 | *) |
||

4 | |||

5 | |||

6 | module S = MiscSolver |
||

7 | f1fa9ad5 | Thorsten Wißmann | module L = List |

8 | 4fd28192 | Thorsten Wißmann | module C = CoAlgFormula |

9 | module HC = HashConsing |
||

10 | |||

11 | |||

12 | (** An instantiation of a set (of the standard library) for bitsets. |
||

13 | *) |
||

14 | module BsSet = Set.Make( |
||

15 | struct |
||

16 | type t = S.bitset |
||

17 | let (compare : t -> t -> int) = S.compareBS |
||

18 | end |
||

19 | ) |
||

20 | |||

21 | (** An instantiation of a hash table (of the standard library) for bitsets. |
||

22 | *) |
||

23 | module GHt = Hashtbl.Make( |
||

24 | struct |
||

25 | 16af388e | Christoph Egger | type t = S.bitset * S.bitset |

26 | let equal ((bs1l, bs1r) : t) (bs2l, bs2r) = |
||

27 | (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0) |
||

28 | let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr) |
||

29 | end |
||

30 | ) |
||

31 | |||

32 | (** An instantiation of a hash table (of the standard library) for bitsets. |
||

33 | *) |
||

34 | module GHtS = Hashtbl.Make( |
||

35 | struct |
||

36 | 4fd28192 | Thorsten Wißmann | type t = S.bitset |

37 | let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0 |
||

38 | let hash (bs : t) = S.hashBS bs |
||

39 | end |
||

40 | ) |
||

41 | |||

42 | (** An instantiation of a hash table (of the standard library) for literals. |
||

43 | *) |
||

44 | module LHt = Hashtbl.Make( |
||

45 | struct |
||

46 | type t = Minisat.lit |
||

47 | let equal (l1 : t) l2 = l1 = l2 |
||

48 | let hash (l : t) = (l :> int) |
||

49 | end |
||

50 | ) |
||

51 | |||

52 | (** An instantiation of a hash table (of the standard library) for formulae. |
||

53 | *) |
||

54 | module FHt = Hashtbl.Make( |
||

55 | struct |
||

56 | type t = int |
||

57 | let equal (f1 : t) f2 = f1 = f2 |
||

58 | let hash (f : t) = f |
||

59 | end |
||

60 | ) |
||

61 | |||

62 | (** An instantiation of a hash table (of the standard library) for nominals. |
||

63 | *) |
||

64 | module NHt = Hashtbl.Make( |
||

65 | struct |
||

66 | type t = int * int |
||

67 | let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2) |
||

68 | let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f |
||

69 | end |
||

70 | ) |
||

71 | |||

72 | |||

73 | (*****************************************************************************) |
||

74 | (* Types that can be modified rather easily *) |
||

75 | (* (of course you then have to modify the implementations below too) *) |
||

76 | (*****************************************************************************) |
||

77 | |||

78 | (* This type must be extended for additional logics. *) |
||

79 | type functors = |
||

80 | | MultiModalK |
||

81 | a87192e8 | Thorsten Wißmann | | MultiModalKD |

82 | f1fa9ad5 | Thorsten Wißmann | | CoalitionLogic |

83 | 29b2e3f3 | Thorsten Wißmann | | GML |

84 | 86b07be8 | Thorsten Wißmann | | PML |

85 | 5e0983fe | Thorsten Wißmann | | Constant of string list |

86 | 19f5dad0 | Dirk Pattinson | | Identity |

87 | | DefaultImplication |
||

88 | 4fd28192 | Thorsten Wißmann | | Choice |

89 | | Fusion |
||

90 | |||

91 | 5e0983fe | Thorsten Wißmann | (* functors whose constructor takes additional parameters *) |

92 | type parametricFunctorName = |
||

93 | | NameConstant |
||

94 | |||

95 | (* this type should only be used in the following few helper functions *) |
||

96 | type functorName = |
||

97 | | NPa of functors (* No Parameters = functor without parameters *) |
||

98 | | Pa of parametricFunctorName (* Parameters = functor with parameters *) |
||

99 | |||

100 | let unaryfunctor2name : (functorName*string) list = |
||

101 | [ (NPa MultiModalK , "MultiModalK") |
||

102 | ; (NPa MultiModalKD , "MultiModalKD") |
||

103 | ; (NPa GML , "GML") |
||

104 | ; (NPa PML , "PML") |
||

105 | ; (NPa CoalitionLogic , "CoalitionLogic") |
||

106 | ; (NPa MultiModalK , "K") |
||

107 | ; (NPa MultiModalKD , "KD") |
||

108 | ; (NPa CoalitionLogic , "CL") |
||

109 | ; (Pa NameConstant , "Const") |
||

110 | ; (Pa NameConstant , "Constant") |
||

111 | 19f5dad0 | Dirk Pattinson | ; (NPa Identity, "Id") |

112 | ; (NPa Identity, "Identity") |
||

113 | db23edf7 | Thorsten Wißmann | ] |

114 | |||

115 | 5e0983fe | Thorsten Wißmann | let functor2name : (functorName*string) list = |

116 | db23edf7 | Thorsten Wißmann | L.append unaryfunctor2name |

117 | 5e0983fe | Thorsten Wißmann | [ (NPa Choice , "Choice") |

118 | ; (NPa Fusion , "Fusion") |
||

119 | db23edf7 | Thorsten Wißmann | ] |

120 | |||

121 | 5e0983fe | Thorsten Wißmann | let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option = |

122 | (* apply parameter list to the constructor, denoted by the functor name func *) |
||

123 | (* return None, if the parameters somehow don't match the required parameters *) |
||

124 | match func with |
||

125 | | NameConstant -> Some (Constant params) |
||

126 | |||

127 | |||

128 | let functor_of_string str params : functors option = |
||

129 | db23edf7 | Thorsten Wißmann | let fst (a,b) = a in |

130 | try |
||

131 | 5e0983fe | Thorsten Wißmann | let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in |

132 | match functorName with |
||

133 | | NPa x -> Some x |
||

134 | | Pa f -> functor_apply_parameters f params |
||

135 | db23edf7 | Thorsten Wißmann | with Not_found -> None |

136 | |||

137 | 5e0983fe | Thorsten Wißmann | let unaryfunctor_of_string str params = |

138 | match (functor_of_string str params) with |
||

139 | db23edf7 | Thorsten Wißmann | | Some Choice -> None |

140 | | Some Fusion -> None |
||

141 | | x -> x |
||

142 | |||

143 | let string_of_functor (f: functors) : string = |
||

144 | 5e0983fe | Thorsten Wißmann | (* replace f orrectly with possibly some Pa wrapper *) |

145 | (* also put the parameters into some suffix which will be appended later *) |
||

146 | let f,suffix = match f with |
||

147 | | Constant params -> Pa NameConstant, " "^(String.concat " " params) |
||

148 | | _ -> NPa f, "" |
||

149 | in |
||

150 | db23edf7 | Thorsten Wißmann | let snd (a,b) = b in |

151 | try |
||

152 | 5e0983fe | Thorsten Wißmann | let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in |

153 | name ^ suffix |
||

154 | db23edf7 | Thorsten Wißmann | with Not_found -> assert false |

155 | |||

156 | 4fd28192 | Thorsten Wißmann | (* This type may be extended for additional logics. *) |

157 | type formulaType = |
||

158 | | Other |
||

159 | 3b055ae8 | dirk | | TrueFalseF (* constant true or false *) |

160 | 4fd28192 | Thorsten Wißmann | | AndF |

161 | | OrF |
||

162 | | AtF |
||

163 | | NomF |
||

164 | 559819d7 | Thorsten Wißmann | | ExF (* Existential / diamond *) |

165 | | AxF (* Universal / box *) |
||

166 | 29b2e3f3 | Thorsten Wißmann | | EnforcesF (* diamond of CL *) |

167 | | AllowsF (* box of CL *) |
||

168 | af276a36 | Thorsten Wißmann | | MoreThanF (* more than n successors = diamond in gml *) |

169 | | MaxExceptF(* at most n exceptions = box in gml *) |
||

170 | 86b07be8 | Thorsten Wißmann | | AtLeastProbF (* for PML *) |

171 | 9bae2c4f | Thorsten Wißmann | | LessProbFailF (* box for PML *) |

172 | c49eea11 | Thorsten Wißmann | | ConstF (* constant functor *) |

173 | | ConstnF (* constant functor *) |
||

174 | 19f5dad0 | Dirk Pattinson | | IdF (* Identity functor *) |

175 | | NormF (* Default Implication *) |
||

176 | | NormnF (* negation normal form of default implication *) |
||

177 | 559819d7 | Thorsten Wißmann | | ChcF (* Choice *) |

178 | | FusF (* Fusion *) |
||

179 | 3b407438 | Christoph Egger | | MuF |

180 | | NuF |
||

181 | 4fd28192 | Thorsten Wißmann | |

182 | type localFormula = int |
||

183 | type bset = S.bitset |
||

184 | |||

185 | type atFormula = int |
||

186 | type cset = S.bitset |
||

187 | type csetSet = BsSet.t |
||

188 | |||

189 | type lht = localFormula LHt.t |
||

190 | type fht = Minisat.lit FHt.t |
||

191 | type nht = bset NHt.t |
||

192 | |||

193 | e0f19999 | Thorsten Wißmann | type state = { sortS : sort; |

194 | mutable bsS : bset; (* a set of formulas who are either literals or |
||

195 | modalities (TODO: also @-formulas?). |
||

196 | the state is satisfiable if /\bsS is satisfiable. |
||

197 | *) |
||

198 | 3285ac30 | Christoph Egger | mutable deferralS : bset; (* which formulas still have deferrals *) |

199 | e0f19999 | Thorsten Wißmann | mutable statusS : nodeStatus; |

200 | 4fd28192 | Thorsten Wißmann | mutable parentsS : core list; mutable childrenS : (dependencies * core list) list; |

201 | 73762b19 | Thorsten Wißmann | mutable constraintsS : csetSet; expandFkt : stateExpander; |

202 | idx: int } |
||

203 | 4fd28192 | Thorsten Wißmann | |

204 | e0f19999 | Thorsten Wißmann | and core = { (* for details, see documentation of newCore *) |

205 | sortC : sort; |
||

206 | mutable bsC : bset; (* a set of arbitrary formulas. |
||

207 | the present core is satisfiable if /\ bsC is satisfiable *) |
||

208 | 3285ac30 | Christoph Egger | mutable deferralC : bset; (* which formulas still have deferrals *) |

209 | e0f19999 | Thorsten Wißmann | mutable statusC : nodeStatus; |

210 | mutable parentsC : (state * int) list; |
||

211 | mutable childrenC : state list; |
||

212 | mutable constraintsC : csetSet; |
||

213 | solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC. |
||

214 | the solver returns "satisfiable" iff |
||

215 | there is a satisfying assignment of |
||

216 | bsC which is not represented by some state from the |
||

217 | childrenC yet. |
||

218 | *) |
||

219 | fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals |
||

220 | of the Minisat solver |
||

221 | *) |
||

222 | 73762b19 | Thorsten Wißmann | mutable constraintParents : cset list; |

223 | idx : int } |
||

224 | 4fd28192 | Thorsten Wißmann | |

225 | d283bf7a | Thorsten Wißmann | and setState = state GHt.t array |

226 | 4fd28192 | Thorsten Wißmann | |

227 | d283bf7a | Thorsten Wißmann | and setCore = core GHt.t array |

228 | 4fd28192 | Thorsten Wißmann | |

229 | 16af388e | Christoph Egger | and setCnstr = unit GHtS.t |

230 | 4fd28192 | Thorsten Wißmann | |

231 | |||

232 | (*****************************************************************************) |
||

233 | (* Types that are hard coded into the algorithm *) |
||

234 | (*****************************************************************************) |
||

235 | |||

236 | 269d93e5 | Thorsten Wißmann | and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *) |

237 | | Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *) |
||

238 | |||

239 | a9949a25 | Thorsten Wißmann | and stateExpander = rule lazylist |

240 | 4fd28192 | Thorsten Wißmann | |

241 | and sort = C.sort |
||

242 | |||

243 | and nodeStatus = |
||

244 | | Expandable |
||

245 | | Open |
||

246 | | Sat |
||

247 | | Unsat |
||

248 | |||

249 | f4498ed1 | Christoph Egger | (* In K, given the singleton list [bs] returns the list of all Ax'es |

250 | responsible for the individual members of bs being part of the core |
||

251 | as well as the Ex. |
||

252 | |||

253 | So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η }, |
||

254 | dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ } |
||

255 | *) |
||

256 | 4fd28192 | Thorsten Wißmann | and dependencies = bset list -> bset |

257 | 269d93e5 | Thorsten Wißmann | |

258 | f4498ed1 | Christoph Egger | (* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *) |

259 | 16af388e | Christoph Egger | and rule = (dependencies * (sort * bset * bset) lazylist) |

260 | 269d93e5 | Thorsten Wißmann | |

261 | a9949a25 | Thorsten Wißmann | and 'a lazyliststep = |

262 | 69243f7f | Thorsten Wißmann | | MultipleElements of 'a list |

263 | | SingleElement of 'a |
||

264 | | NoMoreElements |
||

265 | |||

266 | a9949a25 | Thorsten Wißmann | and 'a lazylist = unit -> 'a lazyliststep |

267 | |||

268 | and ruleEnumeration = rule lazyliststep |
||

269 | |||

270 | f335015f | Thorsten Wißmann | let nodeStatusToString : nodeStatus -> string = function |

271 | | Expandable -> "Expandable" |
||

272 | | Open -> "Open" |
||

273 | | Sat -> "Sat" |
||

274 | | Unsat -> "Unsat" |
||

275 | |||

276 | a9949a25 | Thorsten Wißmann | let lazylistFromList a_list = |

277 | let list_state = ref (Some a_list) in |
||

278 | fun () -> begin match !list_state with |
||

279 | | Some (a_list) -> begin |
||

280 | list_state := None; |
||

281 | MultipleElements a_list |
||

282 | end |
||

283 | | None -> NoMoreElements |
||

284 | end |
||

285 | 4fd28192 | Thorsten Wißmann | |

286 | 672429b4 | Thorsten Wißmann | let rec listFromLazylist evalfunc = |

287 | let step = evalfunc () in |
||

288 | match step with |
||

289 | | NoMoreElements -> [] |
||

290 | | SingleElement x -> x::(listFromLazylist evalfunc) |
||

291 | | MultipleElements xs -> List.append xs (listFromLazylist evalfunc) |
||

292 | |||

293 | 4fd28192 | Thorsten Wißmann | type nominal = sort * localFormula |

294 | |||

295 | type node = |
||

296 | | State of state |
||

297 | | Core of core |
||

298 | |||

299 | type constrnt = |
||

300 | | UnsatC |
||

301 | | SatC |
||

302 | | OpenC of node list |
||

303 | | UnexpandedC of node list |
||

304 | |||

305 | type propagateElement = |
||

306 | | UState of state * int option |
||

307 | | UCore of core * bool |
||

308 | | UCnstr of cset |
||

309 | |||

310 | type queueElement = |
||

311 | | QState of state |
||

312 | | QCore of core |
||

313 | | QCnstr of cset |
||

314 | | QEmpty |
||

315 | |||

316 | type sortTable = (functors * int list) array |
||

317 | |||

318 | exception CoAlg_finished of bool |
||

319 | |||

320 | |||

321 | let sortTable = ref (Array.make 0 (MultiModalK, [1])) |
||

322 | |||

323 | 269d93e5 | Thorsten Wißmann | let junctionEvalBool : (bool list junction) -> bool = function |

324 | | Disjunctive l -> List.fold_right (||) l false |
||

325 | | Conjunctive l -> List.fold_right (&&) l true |
||

326 | |||

327 | let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function |
||

328 | | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false |
||

329 | | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true |
||

330 | |||

331 | let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option = |
||

332 | match x with |
||

333 | | None -> None |
||

334 | | Some x -> (match y with |
||

335 | | None -> None |
||

336 | | Some y -> Some (f x y)) |
||

337 | |||

338 | let junctionEvalBoolOption : bool option list junction -> bool option = |
||

339 | let f extreme op x y = (* ensure that: (Some True) || None = Some True *) |
||

340 | if x = extreme || y = extreme |
||

341 | then extreme |
||

342 | else optionalizeOperator op x y |
||

343 | in function |
||

344 | | Disjunctive l -> |
||

345 | List.fold_right (f (Some true) (||)) l (Some false) |
||

346 | | Conjunctive l -> |
||

347 | List.fold_right (f (Some false) (&&)) l (Some true) |
||

348 | |||

349 | let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function |
||

350 | | Disjunctive l -> (l, fun x -> Disjunctive x) |
||

351 | | Conjunctive l -> (l, fun x -> Conjunctive x) |
||

352 | 4fd28192 | Thorsten Wißmann | |

353 | (*****************************************************************************) |
||

354 | (* "Module type" and a specific implementation of the main queue *) |
||

355 | (*****************************************************************************) |
||

356 | |||

357 | let queueStates = ref ([] : state list) |
||

358 | let queueCores1 = ref ([] : core list) |
||

359 | let queueCores2 = ref ([] : core list) |
||

360 | let queueCnstrs = ref ([] : cset list) |
||

361 | let doPropagation = ref false |
||

362 | |||

363 | let queueInit () = |
||

364 | queueStates := []; |
||

365 | queueCores1 := []; |
||

366 | queueCores2 := []; |
||

367 | queueCnstrs := []; |
||

368 | doPropagation := false |
||

369 | |||

370 | let queueIsEmpty () = |
||

371 | !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = [] |
||

372 | |||

373 | let queueInsertState state = queueStates := state::!queueStates |
||

374 | |||

375 | d58bba0f | Dirk Pattinson | (* original version: breadth-first *) |

376 | 4fd28192 | Thorsten Wißmann | let queueInsertCore core = queueCores2 := core::!queueCores2 |

377 | |||

378 | 034a8dea | Christoph Egger | (* experiment: depth first |

379 | d58bba0f | Dirk Pattinson | let queueInsertCore core = queueCores1 := core::!queueCores1 |

380 | *) |
||

381 | |||

382 | 4fd28192 | Thorsten Wißmann | let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs |

383 | |||

384 | let queueGetElement () = |
||

385 | if !queueCnstrs <> [] then |
||

386 | let res = List.hd !queueCnstrs in |
||

387 | queueCnstrs := List.tl !queueCnstrs; |
||

388 | QCnstr res |
||

389 | else if !queueStates <> [] then |
||

390 | let res = List.hd !queueStates in |
||

391 | queueStates := List.tl !queueStates; |
||

392 | QState res |
||

393 | else if !queueCores1 <> [] then |
||

394 | let res = List.hd !queueCores1 in |
||

395 | queueCores1 := List.tl !queueCores1; |
||

396 | QCore res |
||

397 | else if !queueCores2 = [] then QEmpty |
||

398 | else |
||

399 | let res = List.hd !queueCores2 in |
||

400 | doPropagation := true; |
||

401 | queueCores1 := List.tl !queueCores2; |
||

402 | queueCores2 := []; |
||

403 | QCore res |
||

404 | |||

405 | let doNominalPropagation () = !doPropagation |
||

406 | |||

407 | let doSatPropagation () = |
||

408 | let res = !doPropagation in |
||

409 | doPropagation := false; |
||

410 | res |
||

411 | |||

412 | (*****************************************************************************) |
||

413 | (* "Module type" and a specific implementation of the graph *) |
||

414 | (*****************************************************************************) |
||

415 | |||

416 | let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t)) |
||

417 | let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t)) |
||

418 | 16af388e | Christoph Egger | let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t) |

419 | 4fd28192 | Thorsten Wißmann | let graphRoot = ref (None : core option) |

420 | |||

421 | let graphInit () = |
||

422 | let size = Array.length !sortTable in |
||

423 | graphStates := Array.init size (fun _ -> GHt.create 128); |
||

424 | graphCores := Array.init size (fun _ -> GHt.create 128); |
||

425 | 16af388e | Christoph Egger | graphCnstrs := GHtS.create 128; |

426 | 4fd28192 | Thorsten Wißmann | graphRoot := None |

427 | |||

428 | let graphIterStates fkt = |
||

429 | Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates |
||

430 | |||

431 | let graphIterCores fkt = |
||

432 | Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores |
||

433 | |||

434 | 16af388e | Christoph Egger | let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs |

435 | 4fd28192 | Thorsten Wißmann | |

436 | let graphClearCnstr () = |
||

437 | 16af388e | Christoph Egger | let newGraph = GHtS.create (GHtS.length !graphCnstrs) in |

438 | 4fd28192 | Thorsten Wißmann | let copyCnstr cset cnstr = |

439 | match cnstr with |
||

440 | | UnsatC |
||

441 | 16af388e | Christoph Egger | | SatC -> GHtS.add newGraph cset cnstr |

442 | | OpenC _ -> GHtS.add newGraph cset (OpenC []) |
||

443 | | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC []) |
||

444 | 4fd28192 | Thorsten Wißmann | in |

445 | 16af388e | Christoph Egger | GHtS.iter copyCnstr !graphCnstrs; |

446 | 4fd28192 | Thorsten Wißmann | graphCnstrs := newGraph |

447 | |||

448 | let graphFindState sort bs = |
||

449 | try |
||

450 | Some (GHt.find !graphStates.(sort) bs) |
||

451 | with Not_found -> None |
||

452 | |||

453 | let graphFindCore sort bs = |
||

454 | try |
||

455 | Some (GHt.find !graphCores.(sort) bs) |
||

456 | with Not_found -> None |
||

457 | |||

458 | let graphFindCnstr cset = |
||

459 | try |
||

460 | 16af388e | Christoph Egger | Some (GHtS.find !graphCnstrs cset) |

461 | 4fd28192 | Thorsten Wißmann | with Not_found -> None |

462 | |||

463 | let graphInsertState sort bs state = |
||

464 | assert (not (GHt.mem !graphStates.(sort) bs)); |
||

465 | GHt.add !graphStates.(sort) bs state |
||

466 | |||

467 | let graphInsertCore sort bs core = |
||

468 | assert (not (GHt.mem !graphCores.(sort) bs)); |
||

469 | GHt.add !graphCores.(sort) bs core |
||

470 | |||

471 | let graphInsertCnstr cset cnstr = |
||

472 | 16af388e | Christoph Egger | assert (not (GHtS.mem !graphCnstrs cset)); |

473 | GHtS.add !graphCnstrs cset cnstr |
||

474 | 4fd28192 | Thorsten Wißmann | |

475 | let graphReplaceCnstr cset cnstr = |
||

476 | 16af388e | Christoph Egger | GHtS.replace !graphCnstrs cset cnstr |

477 | 4fd28192 | Thorsten Wißmann | |

478 | let graphSizeState () = |
||

479 | Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates |
||

480 | let graphSizeCore () = |
||

481 | Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores |
||

482 | 16af388e | Christoph Egger | let graphSizeCnstr () = GHtS.length !graphCnstrs |

483 | 4fd28192 | Thorsten Wißmann | |

484 | let graphAddRoot core = |
||

485 | if !graphRoot = None then graphRoot := Some core |
||

486 | else raise (C.CoAlgException "Root of graph is already set.") |
||

487 | |||

488 | let graphGetRoot () = |
||

489 | match !graphRoot with |
||

490 | | None -> raise (C.CoAlgException "Root of graph is not set.") |
||

491 | | Some core -> core |
||

492 | |||

493 | |||

494 | (*****************************************************************************) |
||

495 | (* "Module type" and a specific implementation of sets of constraints *) |
||

496 | (*****************************************************************************) |
||

497 | |||

498 | let cssEmpty = BsSet.empty |
||

499 | let cssExists fkt css = BsSet.exists fkt css |
||

500 | let cssForall fkt css = BsSet.for_all fkt css |
||

501 | let cssUnion css1 css2 = BsSet.union css1 css2 |
||

502 | let cssAdd cset css = BsSet.add cset css |
||

503 | let cssFold fkt css init = BsSet.fold fkt css init |
||

504 | let cssSingleton cset = BsSet.singleton cset |
||

505 | let cssEqual css1 css2 = BsSet.equal css1 css2 |
||

506 | f335015f | Thorsten Wißmann | let cssIter (action: cset -> unit) css = |

507 | BsSet.iter action css |
||

508 | 4fd28192 | Thorsten Wißmann | |

509 | |||

510 | (*****************************************************************************) |
||

511 | (* "Module type" and a specific implementation of state nodes *) |
||

512 | (*****************************************************************************) |
||

513 | 73762b19 | Thorsten Wißmann | let nodeCounter = ref 0 |

514 | let nextNodeIdx () : int = |
||

515 | let oldVal = !nodeCounter in |
||

516 | nodeCounter := oldVal + 1; |
||

517 | oldVal |
||

518 | |||

519 | 3285ac30 | Christoph Egger | let stateMake sort bs defer exp = |

520 | { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = []; |
||

521 | 73762b19 | Thorsten Wißmann | constraintsS = cssEmpty; expandFkt = exp; |

522 | idx = nextNodeIdx() |
||

523 | } |
||

524 | 4fd28192 | Thorsten Wißmann | let stateGetSort state = state.sortS |

525 | let stateGetBs state = state.bsS |
||

526 | let stateSetBs state bs = state.bsS <- bs |
||

527 | 3285ac30 | Christoph Egger | let stateGetDeferral state = state.deferralS |

528 | let stateSetDeferral state bs = state.deferralS <- bs |
||

529 | 4fd28192 | Thorsten Wißmann | let stateGetStatus state = state.statusS |

530 | let stateSetStatus state status = state.statusS <- status |
||

531 | let stateGetParents state = state.parentsS |
||

532 | let stateAddParent state parent = state.parentsS <- parent::state.parentsS |
||

533 | let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx) |
||

534 | let stateGetRules state = state.childrenS |
||

535 | let stateAddRule state dep children = |
||

536 | state.childrenS <- (dep, children)::state.childrenS; |
||

537 | List.length state.childrenS |
||

538 | let stateGetConstraints state = state.constraintsS |
||

539 | let stateSetConstraints state csets = state.constraintsS <- csets |
||

540 | let stateNextRule state = state.expandFkt () |
||

541 | 73762b19 | Thorsten Wißmann | let stateGetIdx (state:state) = state.idx |

542 | 4fd28192 | Thorsten Wißmann | |

543 | |||

544 | (*****************************************************************************) |
||

545 | (* "Module type" and a specific implementation of core nodes *) |
||

546 | (*****************************************************************************) |
||

547 | |||

548 | 3285ac30 | Christoph Egger | let coreMake sort bs defer solver fht = |

549 | { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = []; |
||

550 | 73762b19 | Thorsten Wißmann | constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = []; |

551 | idx = nextNodeIdx() |
||

552 | } |
||

553 | 4fd28192 | Thorsten Wißmann | let coreGetSort core = core.sortC |

554 | let coreGetBs core = core.bsC |
||

555 | let coreSetBs core bs = core.bsC <- bs |
||

556 | 3285ac30 | Christoph Egger | let coreGetDeferral core = core.deferralC |

557 | let coreSetDeferral core bs = core.deferralC <- bs |
||

558 | 4fd28192 | Thorsten Wißmann | let coreGetStatus core = core.statusC |

559 | let coreSetStatus core status = core.statusC <- status |
||

560 | let coreGetParents core = core.parentsC |
||

561 | let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC |
||

562 | let coreGetChildren core = core.childrenC |
||

563 | let coreAddChild core child = core.childrenC <- child::core.childrenC |
||

564 | let coreGetConstraints core = core.constraintsC |
||

565 | let coreSetConstraints core csets = core.constraintsC <- csets |
||

566 | let coreGetSolver core = core.solver |
||

567 | let coreGetFht core = core.fht |
||

568 | 73762b19 | Thorsten Wißmann | let coreGetIdx (core:core) = core.idx |

569 | 4fd28192 | Thorsten Wißmann | let coreGetConstraintParents core = core.constraintParents |

570 | let coreAddConstraintParent core cset = |
||

571 | core.constraintParents <- cset::core.constraintParents |
||

572 | |||

573 | |||

574 | (*****************************************************************************) |
||

575 | (* "Module type" and a specific implementation of sets of *) |
||

576 | (* states, cores, and constraints for the sat propagation *) |
||

577 | (*****************************************************************************) |
||

578 | |||

579 | d283bf7a | Thorsten Wißmann | let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128) |

580 | let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128) |
||

581 | 16af388e | Christoph Egger | let setEmptyCnstr () = GHtS.create 128 |

582 | let setAddState set state = |
||

583 | GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state |
||

584 | let setAddCore set core = |
||

585 | GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core |
||

586 | let setAddCnstr set cset = GHtS.add set cset () |
||

587 | let setMemState set state = |
||

588 | GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) |
||

589 | let setMemCore set core = |
||

590 | GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) |
||

591 | let setMemCnstr set cset = GHtS.mem set cset |
||

592 | let setRemoveState set state = |
||

593 | GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) |
||

594 | let setRemoveCore set core = |
||

595 | GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) |
||

596 | let setRemoveCnstr set cset = GHtS.remove set cset |
||

597 | d283bf7a | Thorsten Wißmann | let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set |

598 | let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set |
||

599 | 16af388e | Christoph Egger | let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set |

600 | 50df1dc2 | Christoph Egger | let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta |

601 | let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta |
||

602 | 4fd28192 | Thorsten Wißmann | |

603 | |||

604 | (*****************************************************************************) |
||

605 | (* "Module type" and a specific implementation of the mapping *) |
||

606 | (* between (local) formulae and literals of the sat solver, *) |
||

607 | (* and of a mapping of nominals to sets of formulae *) |
||

608 | (*****************************************************************************) |
||

609 | |||

610 | let lhtInit () = LHt.create 16 |
||

611 | let lhtAdd lht lit f = LHt.add lht lit f |
||

612 | let lhtFind lht lit = |
||

613 | try |
||

614 | Some (LHt.find lht lit) |
||

615 | with Not_found -> None |
||

616 | |||

617 | let fhtInit () = FHt.create 16 |
||

618 | let fhtAdd fht f lit = FHt.add fht f lit |
||

619 | let fhtFind fht f = |
||

620 | try |
||

621 | Some (FHt.find fht f) |
||

622 | with Not_found -> None |
||

623 | |||

624 | let nhtInit () = NHt.create 8 |
||

625 | let nhtAdd nht nom bs = NHt.add nht nom bs |
||

626 | let nhtFind nht nom = |
||

627 | try |
||

628 | Some (NHt.find nht nom) |
||

629 | with Not_found -> None |
||

630 | let nhtFold fkt nht init = NHt.fold fkt nht init |
||

631 | |||

632 | (*****************************************************************************) |
||

633 | (* "Module type" and a specific implementation of sets of *) |
||

634 | (* local formulae and @-formulae *) |
||

635 | (*****************************************************************************) |
||

636 | |||

637 | let tboxTable = ref (Array.make 0 S.dummyBS) |
||

638 | |||

639 | let bsetMake () = S.makeBS () |
||

640 | let bsetAdd bs lf = S.addBSNoChk bs lf |
||

641 | let bsetMem bs lf = S.memBS bs lf |
||

642 | b7445f7e | Thorsten Wißmann | let bsetRem bs lf = S.remBS bs lf |

643 | 16af388e | Christoph Egger | let bsetCompare bs1 bs2 = S.compareBS bs1 bs2 |

644 | 45d554b0 | Thorsten Wißmann | let bsetMakeRealEmpty () = |

645 | let res = bsetMake () in |
||

646 | bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *) |
||

647 | res |
||

648 | b7c3a47e | Thorsten Wißmann | let bsetCopy bs = S.copyBS bs |

649 | 4fd28192 | Thorsten Wißmann | let bsetFold fkt bs init = S.foldBS fkt bs init |

650 | let bsetIter fkt bset = S.iterBS fkt bset |
||

651 | e4cd869a | Thorsten Wißmann | let bsetFilter (a: bset) (f: localFormula -> bool) : bset = |

652 | 45d554b0 | Thorsten Wißmann | let res = bsetMakeRealEmpty () in |

653 | e4cd869a | Thorsten Wißmann | bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a; |

654 | res |
||

655 | |||

656 | 4fd28192 | Thorsten Wißmann | let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort) |

657 | |||

658 | let csetCompare cs1 cs2 = S.compareBS cs1 cs2 |
||

659 | let csetMake () = S.makeBS () |
||

660 | let csetAdd cs lf = S.addBSNoChk cs lf |
||

661 | let csetCopy cs = S.copyBS cs |
||

662 | let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2 |
||

663 | let csetHasDot cs = S.memBS cs !S.bsfalse |
||

664 | let csetAddDot cs = S.addBSNoChk cs !S.bsfalse |
||

665 | let csetRemDot cs = S.remBS cs !S.bsfalse |
||

666 | let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort) |
||

667 | let csetIter cs fkt = |
||

668 | let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in |
||

669 | S.iterBS fkt2 cs |
||

670 | |||

671 | |||

672 | (*****************************************************************************) |
||

673 | (* "Module type" and a specific implementation of *) |
||

674 | (* local formulae and @-formulae *) |
||

675 | (*****************************************************************************) |
||

676 | |||

677 | (** This table maps integers (representing formulae) to their corresponding formulae. |
||

678 | *) |
||

679 | let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE)) |
||

680 | |||

681 | (** This table maps integers (representing formulae) to their corresponding type. |
||

682 | *) |
||

683 | let arrayType = ref (Array.make 0 (Array.make 0 Other)) |
||

684 | |||

685 | (** This lookup table maps formulae (represented as integers) |
||

686 | to their negation (in negation normal form). |
||

687 | *) |
||

688 | let arrayNeg = ref (Array.make 0 (Array.make 0 (-1))) |
||

689 | |||

690 | (** These lookup tables map formulae (represented as integers) |
||

691 | to their decompositions (represented as integers). |
||

692 | This is done according to the rules of the tableau procedure |
||

693 | and depends on the type of the formulae. |
||

694 | *) |
||

695 | 86b07be8 | Thorsten Wißmann | (* |

696 | for PML: arrayDest1 = the subformula |
||

697 | eda515b6 | Thorsten Wißmann | arrayNum = the nominator of the probability |

698 | arrayNum2 = the denominator of the probability |
||

699 | 86b07be8 | Thorsten Wißmann | *) |

700 | f1fa9ad5 | Thorsten Wißmann | let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *) |

701 | let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1))) (* second subformula *) |
||

702 | let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1))) (* a role *) |
||

703 | d9f4e4af | Christoph Egger | let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1))) (* deferral at point *) |

704 | 29b2e3f3 | Thorsten Wißmann | let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *) |

705 | eda515b6 | Thorsten Wißmann | let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1))) (* another integer *) |

706 | f1fa9ad5 | Thorsten Wißmann | let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *) |

707 | 4fd28192 | Thorsten Wißmann | |

708 | (** This lookup table maps formulae (represented as integers) |
||

709 | to their @-wrapper. |
||

710 | *) |
||

711 | let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64))) |
||

712 | |||

713 | let lfGetType sort f = !arrayType.(sort).(f) |
||

714 | let lfGetDest1 sort f = !arrayDest1.(sort).(f) |
||

715 | let lfGetDest2 sort f = !arrayDest2.(sort).(f) |
||

716 | let lfGetDest3 sort f = !arrayDest3.(sort).(f) |
||

717 | c67aca42 | Christoph Egger | let lfGetDeferral sort f = !arrayDeferral.(sort).(f) |

718 | 29b2e3f3 | Thorsten Wißmann | let lfGetDestNum sort f = !arrayDestNum.(sort).(f) |

719 | eda515b6 | Thorsten Wißmann | let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f) |

720 | f1fa9ad5 | Thorsten Wißmann | let lfGetDestAg sort f = !arrayDestAg.(sort).(f) |

721 | 4fd28192 | Thorsten Wißmann | let lfGetNeg sort f = |

722 | let nf = !arrayNeg.(sort).(f) in |
||

723 | if nf >= 0 then Some nf else None |
||

724 | let lfGetAt (sort, nom) f = |
||

725 | FHt.find !arrayAt.(sort).(f) nom |
||

726 | a0cffef0 | Thorsten Wißmann | let lfToInt lf = lf |

727 | let lfFromInt num = num |
||

728 | f335015f | Thorsten Wißmann | let lfGetFormula sort f = !arrayFormula.(sort).(f) |

729 | |||

730 | de84f40d | Christoph Egger | let escapeHtml (input : string) : string = |

731 | List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str) |
||

732 | [("<", "<") ; (">", ">") ; ("&", "&")] |
||

733 | input |
||

734 | |||

735 | f335015f | Thorsten Wißmann | let bsetToString sort bset : string = |

736 | let toFormula (lf:localFormula) (lst: string list) : string list = |
||

737 | let formula: C.formula = lfGetFormula sort lf in |
||

738 | (C.string_of_formula formula) :: lst |
||

739 | in |
||

740 | let formulaList = bsetFold toFormula bset [] in |
||

741 | "{ "^(String.concat ", " formulaList)^" }" |
||

742 | |||

743 | let csetToString sort cset = bsetToString sort cset |
||

744 | |||

745 | 8d6bf016 | Christoph Egger | let coreToString (core:core): string = |

746 | f335015f | Thorsten Wißmann | let helper cset lst : string list = |

747 | (csetToString core.sortC cset):: lst |
||

748 | in |
||

749 | let constraints = cssFold helper core.constraintsC [] in |
||

750 | 488cea0f | Thorsten Wißmann | let children = |

751 | List.map (fun (st:state) -> string_of_int st.idx) core.childrenC |
||

752 | in |
||

753 | 4164c8e1 | Thorsten Wißmann | let parents = |

754 | List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC |
||

755 | in |
||

756 | 73762b19 | Thorsten Wißmann | "Core "^(string_of_int core.idx)^" {\n"^ |

757 | f335015f | Thorsten Wißmann | " Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^ |

758 | " " ^ bsetToString core.sortC core.bsC ^ "\n" ^ |
||

759 | 16af388e | Christoph Egger | " Deferrals: \n" ^ |

760 | " " ^ bsetToString core.sortC core.deferralC ^ "\n" ^ |
||

761 | 73762b19 | Thorsten Wißmann | " Constraints: { "^(String.concat |

762 | "\n " constraints)^" }\n"^ |
||

763 | 488cea0f | Thorsten Wißmann | " Children: { "^(String.concat |

764 | ", " children)^" }\n"^ |
||

765 | 4164c8e1 | Thorsten Wißmann | " Parents: { "^(String.concat ", " parents)^" }\n"^ |

766 | f335015f | Thorsten Wißmann | "}" |

767 | 73762b19 | Thorsten Wißmann | |

768 | let stateToString (state:state): string = |
||

769 | let helper cset lst : string list = |
||

770 | (csetToString state.sortS cset):: lst |
||

771 | in |
||

772 | let constraints = cssFold helper state.constraintsS [] in |
||

773 | let core2idx core = core.idx in |
||

774 | let fst (a,b) = a in |
||

775 | let conclusionList = |
||

776 | List.map (fun (_,lst) -> |
||

777 | List.map (fun (core:core) -> string_of_int core.idx) lst |
||

778 | ) state.childrenS |
||

779 | in |
||

780 | let conclusionList = |
||

781 | List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList |
||

782 | in |
||

783 | 4164c8e1 | Thorsten Wißmann | let parents = |

784 | List.map (fun (co:core) -> string_of_int co.idx) state.parentsS |
||

785 | in |
||

786 | 73762b19 | Thorsten Wißmann | "State "^(string_of_int state.idx)^" {\n"^ |

787 | " Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^ |
||

788 | " " ^ bsetToString state.sortS state.bsS ^ "\n" ^ |
||

789 | 16af388e | Christoph Egger | " Deferrals: \n" ^ |

790 | " " ^ bsetToString state.sortS state.deferralS ^ "\n" ^ |
||

791 | 73762b19 | Thorsten Wißmann | " Constraints: { "^(String.concat |

792 | "\n " constraints)^" }\n"^ |
||

793 | " Children: { "^(String.concat |
||

794 | "\n " conclusionList)^" }\n"^ |
||

795 | 4164c8e1 | Thorsten Wißmann | " Parents: { "^(String.concat ", " parents)^" }\n"^ |

796 | 73762b19 | Thorsten Wißmann | "}" |

797 | |||

798 | 8d6bf016 | Christoph Egger | let stateToDot (state:state): string = |

799 | c13029a3 | Christoph Egger | let color = match state.statusS with |

800 | | Sat -> "green" |
||

801 | | Unsat -> "red" |
||

802 | | Open -> "yellow" |
||

803 | | Expandable -> "white" |
||

804 | in |
||

805 | de84f40d | Christoph Egger | let toFormula (lf:localFormula) (lst: string list) : string list = |

806 | let formula: C.formula = lfGetFormula state.sortS lf in |
||

807 | if (bsetMem state.deferralS lf) |
||

808 | then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst |
||

809 | else (escapeHtml (C.string_of_formula formula)) :: lst |
||

810 | in |
||

811 | let formulaList = bsetFold toFormula state.bsS [] in |
||

812 | 8d6bf016 | Christoph Egger | let ownidx = (string_of_int state.idx) in |

813 | let parents = |
||

814 | c13029a3 | Christoph Egger | List.map (fun (co:core) -> |

815 | "Node"^string_of_int co.idx^" -> Node"^ownidx^";") |
||

816 | 8d6bf016 | Christoph Egger | state.parentsS |

817 | in |
||

818 | c13029a3 | Christoph Egger | "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color |

819 | de84f40d | Christoph Egger | ^ ",label=<State " ^ ownidx |

820 | ^ "<BR/>" ^ (String.concat "<BR/>" formulaList) |
||

821 | ^ ">];\n" |
||

822 | 8d6bf016 | Christoph Egger | ^ (String.concat "\n" parents) |

823 | |||

824 | |||

825 | let coreToDot (core:core): string = |
||

826 | c13029a3 | Christoph Egger | let color = match core.statusC with |

827 | | Sat -> "green" |
||

828 | | Unsat -> "red" |
||

829 | | Open -> "yellow" |
||

830 | | Expandable -> "white" |
||

831 | in |
||

832 | de84f40d | Christoph Egger | let toFormula (lf:localFormula) (lst: string list) : string list = |

833 | let formula: C.formula = lfGetFormula core.sortC lf in |
||

834 | if (bsetMem core.deferralC lf) |
||

835 | then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst |
||

836 | else (escapeHtml (C.string_of_formula formula)) :: lst |
||

837 | in |
||

838 | let formulaList = bsetFold toFormula core.bsC [] in |
||

839 | 8d6bf016 | Christoph Egger | let ownidx = (string_of_int core.idx) in |

840 | let parents = |
||

841 | c13029a3 | Christoph Egger | List.map (fun (st,_:state*int) -> |

842 | "Node"^string_of_int st.idx^" -> Node"^ownidx^";") |
||

843 | 8d6bf016 | Christoph Egger | core.parentsC |

844 | in |
||

845 | c13029a3 | Christoph Egger | "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color |

846 | de84f40d | Christoph Egger | ^ ",label=<Core " ^ ownidx |

847 | ^ "<BR/>" ^ (String.concat "<BR/>" formulaList) |
||

848 | ^ ">];\n" |
||

849 | 8d6bf016 | Christoph Egger | ^ (String.concat "\n" parents) |

850 | |||

851 | |||

852 | 488cea0f | Thorsten Wißmann | let queuePrettyStatus () = |

853 | let printList (sl : int list) : string = |
||

854 | String.concat ", " (List.map string_of_int sl) |
||

855 | in |
||

856 | (* TODO: are atFormulas always look-up-able for sort 0? *) |
||

857 | (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs)) |
||

858 | ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs)) |
||

859 | ^(Printf.sprintf "\n%d States: " (List.length !queueStates)) |
||

860 | ^(printList (List.map (fun (st:state) -> st.idx) !queueStates)) |
||

861 | ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1)) |
||

862 | ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1)) |
||

863 | ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2)) |
||

864 | ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2)) |
||

865 | ^"\n" |
||

866 | |||

867 | 73762b19 | Thorsten Wißmann | |

868 | |||

869 | 4fd28192 | Thorsten Wißmann | |

870 | let atFormulaGetSubformula f = !arrayDest1.(0).(f) |
||

871 | let atFormulaGetNominal f = |
||

872 | let s = !arrayDest3.(0).(f) in |
||

873 | let n = !arrayDest2.(0).(f) in |
||

874 | (s, n) |
||

875 | |||

876 | let lfToAt _ lf = lf |
||

877 | |||

878 | 4b0d0388 | Christoph Egger | (* Calculate all possible formulae. This includes all subformulae and |

879 | in the case of μ-Calculus the Fischer-Ladner closure. |
||

880 | 4fd28192 | Thorsten Wißmann | |

881 | 4b0d0388 | Christoph Egger | TODO: variable sort needs to match epected sort |

882 | *) |
||

883 | cb12f8a5 | Christoph Egger | let rec detClosure vars nomTbl hcF fset vset atset nomset s f = |

884 | let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in |
||

885 | let detClosure_ = detClosure newvars in |
||

886 | let deferral = if List.length newvars > 0 |
||

887 | then (List.hd newvars) |
||

888 | else "ε" in |
||

889 | 4fd28192 | Thorsten Wißmann | if s < 0 || s >= Array.length fset then |

890 | let sstr = string_of_int s in |
||

891 | raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr)) |
||

892 | else (); |
||

893 | 653eaa4b | Christoph Egger | if C.HcFHt.mem vset.(s) f && |

894 | compare (C.HcFHt.find vset.(s) f) deferral = 0 then () |
||

895 | 4fd28192 | Thorsten Wißmann | else |

896 | cb12f8a5 | Christoph Egger | let () = C.HcFHt.add vset.(s) f deferral in |

897 | 4fd28192 | Thorsten Wißmann | let () = C.HcFHt.add fset.(s) f () in |

898 | let (func, sortlst) = !sortTable.(s) in |
||

899 | match f.HC.node with |
||

900 | | C.HCTRUE |
||

901 | 43194ed2 | Christoph Egger | | C.HCFALSE |

902 | | C.HCVAR _ -> () |
||

903 | 4fd28192 | Thorsten Wißmann | | C.HCAP name -> |

904 | if C.isNominal name then begin |
||

905 | Hashtbl.replace nomset name s; |
||

906 | match nomTbl name with |
||

907 | | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) |
||

908 | | Some sort -> |
||

909 | if sort <> s then |
||

910 | let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in |
||

911 | let str2 = " is used in sort " ^ (string_of_int s) ^ "." in |
||

912 | raise (C.CoAlgException (str1 ^ str2)) |
||

913 | else () |
||

914 | end else () |
||

915 | | C.HCNOT _ -> () |
||

916 | | C.HCAT (name, f1) -> |
||

917 | C.HcFHt.replace atset f (); |
||

918 | let s1 = |
||

919 | match nomTbl name with |
||

920 | | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) |
||

921 | | Some sort -> sort |
||

922 | in |
||

923 | let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in |
||

924 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom; |

925 | detClosure_ nomTbl hcF fset vset atset nomset s1 f1 |
||

926 | 4fd28192 | Thorsten Wißmann | | C.HCOR (f1, f2) |

927 | | C.HCAND (f1, f2) -> |
||

928 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset s f1; |

929 | detClosure_ nomTbl hcF fset vset atset nomset s f2 |
||

930 | 4fd28192 | Thorsten Wißmann | | C.HCEX (_, f1) |

931 | | C.HCAX (_, f1) -> |
||

932 | 2a84977e | Thorsten Wißmann | if (func <> MultiModalK && func <> MultiModalKD) |

933 | || List.length sortlst <> 1 |
||

934 | then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.") |
||

935 | 4fd28192 | Thorsten Wißmann | else (); |

936 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 |

937 | f1fa9ad5 | Thorsten Wißmann | | C.HCENFORCES (_, f1) |

938 | | C.HCALLOWS (_, f1) -> |
||

939 | if func <> CoalitionLogic || List.length sortlst <> 1 |
||

940 | then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.") |
||

941 | else (); |
||

942 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 |

943 | af276a36 | Thorsten Wißmann | | C.HCMORETHAN (_,_,f1) |

944 | | C.HCMAXEXCEPT (_,_,f1) -> |
||

945 | 29b2e3f3 | Thorsten Wißmann | if func <> GML || List.length sortlst <> 1 |

946 | then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.") |
||

947 | else (); |
||

948 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 |

949 | 86b07be8 | Thorsten Wißmann | | C.HCATLEASTPROB (_,f1) |

950 | 9bae2c4f | Thorsten Wißmann | | C.HCLESSPROBFAIL (_,f1) -> |

951 | 86b07be8 | Thorsten Wißmann | if func <> PML || List.length sortlst <> 1 |

952 | c855ba91 | Thorsten Wißmann | then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.") |

953 | 86b07be8 | Thorsten Wißmann | else (); |

954 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1; |

955 | 9bae2c4f | Thorsten Wißmann | (* |

956 | TODO: add ¬ f1 to the closure! |
||

957 | detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde) |
||

958 | *) |
||

959 | 5e0983fe | Thorsten Wißmann | | C.HCCONST color |

960 | | C.HCCONSTN color -> |
||

961 | begin match func with |
||

962 | | Constant params -> |
||

963 | if not (List.exists ((=) color) params) |
||

964 | then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only" |
||

965 | ^" choices are: "^(String.concat ", " params))) |
||

966 | | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.") |
||

967 | end; |
||

968 | if List.length sortlst <> 1 |
||

969 | c49eea11 | Thorsten Wißmann | then raise (C.CoAlgException "=-formula is used in wrong sort.") |

970 | else (); |
||

971 | (* NB: =-formulae have no subformlae hence no closure *) |
||

972 | 19f5dad0 | Dirk Pattinson | | C.HCID f1 -> |

973 | if func <> Identity || List.length sortlst <> 1 |
||

974 | then raise (C.CoAlgException "Identity operator applied to |
||

975 | formula of wrong sort.") |
||

976 | else (); |
||

977 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1; |

978 | 19f5dad0 | Dirk Pattinson | | C.HCNORM (f1, f2) |

979 | | C.HCNORMN(f1, f2) -> |
||

980 | if func <> DefaultImplication || List.length sortlst <> 1 then |
||

981 | raise (C.CoAlgException "Default Implication applied to |
||

982 | formulae of wrong sort.") |
||

983 | else (); |
||

984 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1; |

985 | detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2 |
||

986 | 19f5dad0 | Dirk Pattinson | |

987 | d58bba0f | Dirk Pattinson | | C.HCCHC (f1, f2) -> |

988 | 4fd28192 | Thorsten Wißmann | if func <> Choice || List.length sortlst <> 2 then |

989 | raise (C.CoAlgException "Choice formula is used in wrong sort.") |
||

990 | else (); |
||

991 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1; |

992 | detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2 |
||

993 | 4fd28192 | Thorsten Wißmann | | C.HCFUS (first, f1) -> |

994 | if func <> Fusion || List.length sortlst <> 2 then |
||

995 | raise (C.CoAlgException "Fusion formula is used in wrong sort.") |
||

996 | else (); |
||

997 | let s1 = List.nth sortlst (if first then 0 else 1) in |
||

998 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset s1 f1 |

999 | 034a8dea | Christoph Egger | (* |

1000 | 6553983f | Christoph Egger | FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ]) |

1001 | 034a8dea | Christoph Egger | *) |

1002 | | C.HCMU (name, f1) -> |
||

1003 | cb12f8a5 | Christoph Egger | let () = C.HcFHt.replace vset.(s) f name in |

1004 | 034a8dea | Christoph Egger | let unfold = C.hc_replace hcF name f f1 in |

1005 | cb12f8a5 | Christoph Egger | let appendvars = List.append newvars [name] in |

1006 | detClosure appendvars nomTbl hcF fset vset atset nomset s unfold |
||

1007 | 034a8dea | Christoph Egger | | C.HCNU (name, f1) -> |

1008 | let unfold = C.hc_replace hcF name f f1 in |
||

1009 | cb12f8a5 | Christoph Egger | detClosure_ nomTbl hcF fset vset atset nomset s unfold |

1010 | 6553983f | Christoph Egger | |

1011 | 4fd28192 | Thorsten Wißmann | |

1012 | let detClosureAt hcF atset name f () = |
||

1013 | match f.HC.node with |
||

1014 | | C.HCTRUE |
||

1015 | | C.HCFALSE |
||

1016 | | C.HCOR _ |
||

1017 | | C.HCAND _ |
||

1018 | | C.HCAT _ -> () |
||

1019 | | _ -> |
||

1020 | 034a8dea | Christoph Egger | let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in |

1021 | 4fd28192 | Thorsten Wißmann | C.HcFHt.replace atset at () |

1022 | |||

1023 | (** Initialises the arrays for a formula and its integer representation. |
||

1024 | *) |
||

1025 | d9f4e4af | Christoph Egger | let initTables nomTbl hcF htF htR vset s f n = |

1026 | 4fd28192 | Thorsten Wißmann | !arrayFormula.(s).(n) <- f.HC.fml; |

1027 | d9f4e4af | Christoph Egger | !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f); |

1028 | 4fd28192 | Thorsten Wißmann | let fneg = f.HC.neg in |

1029 | if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg; |
||

1030 | let (_, sortlst) = !sortTable.(s) in |
||

1031 | match f.HC.node with |
||

1032 | | C.HCTRUE |
||

1033 | 3b055ae8 | dirk | | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF |

1034 | 4fd28192 | Thorsten Wißmann | | C.HCAP name -> |

1035 | if C.isNominal name then !arrayType.(s).(n) <- NomF |
||

1036 | else !arrayType.(s).(n) <- Other |
||

1037 | | C.HCNOT _ -> !arrayType.(s).(n) <- Other |
||

1038 | | C.HCAT (name, f1) -> |
||

1039 | !arrayType.(s).(n) <- AtF; |
||

1040 | let s1 = |
||

1041 | match nomTbl name with |
||

1042 | | None -> assert false |
||

1043 | | Some sort -> sort |
||

1044 | in |
||

1045 | let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in |
||

1046 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; |
||

1047 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom; |
||

1048 | !arrayDest3.(s).(n) <- s1 |
||

1049 | | C.HCOR (f1, f2) -> |
||

1050 | !arrayType.(s).(n) <- OrF; |
||

1051 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; |
||

1052 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 |
||

1053 | | C.HCAND (f1, f2) -> |
||

1054 | !arrayType.(s).(n) <- AndF; |
||

1055 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; |
||

1056 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 |
||

1057 | 034a8dea | Christoph Egger | | C.HCEX (role, f1) -> |

1058 | 4fd28192 | Thorsten Wißmann | !arrayType.(s).(n) <- ExF; |

1059 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |
||

1060 | 034a8dea | Christoph Egger | !arrayDest3.(s).(n) <- |

1061 | 4fd28192 | Thorsten Wißmann | if Hashtbl.mem htR role then Hashtbl.find htR role |

1062 | else |
||

1063 | let size = Hashtbl.length htR in |
||

1064 | Hashtbl.add htR role size; |
||

1065 | size |
||

1066 | | C.HCAX (role, f1) -> |
||

1067 | !arrayType.(s).(n) <- AxF; |
||

1068 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |
||

1069 | !arrayDest3.(s).(n) <- |
||

1070 | if Hashtbl.mem htR role then Hashtbl.find htR role |
||

1071 | else |
||

1072 | let size = Hashtbl.length htR in |
||

1073 | Hashtbl.add htR role size; |
||

1074 | size |
||

1075 | f1fa9ad5 | Thorsten Wißmann | | C.HCENFORCES (aglist, f1) -> (* aglist = list of agents *) |

1076 | !arrayType.(s).(n) <- EnforcesF; |
||

1077 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |
||

1078 | !arrayDestAg.(s).(n) <- Array.of_list aglist |
||

1079 | | C.HCALLOWS (aglist, f1) -> (* aglist = list of agents *) |
||

1080 | !arrayType.(s).(n) <- AllowsF; |
||

1081 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |
||

1082 | !arrayDestAg.(s).(n) <- Array.of_list aglist |
||

1083 | af276a36 | Thorsten Wißmann | | C.HCMORETHAN (cnt,role,f1) -> |

1084 | !arrayType.(s).(n) <- MoreThanF; |
||

1085 | 29b2e3f3 | Thorsten Wißmann | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |

1086 | !arrayDestNum.(s).(n) <- cnt; |
||

1087 | !arrayDest3.(s).(n) <- |
||

1088 | if Hashtbl.mem htR role then Hashtbl.find htR role |
||

1089 | else |
||

1090 | let size = Hashtbl.length htR in |
||

1091 | Hashtbl.add htR role size; |
||

1092 | size |
||

1093 | af276a36 | Thorsten Wißmann | | C.HCMAXEXCEPT (cnt,role,f1) -> |

1094 | !arrayType.(s).(n) <- MaxExceptF; |
||

1095 | 29b2e3f3 | Thorsten Wißmann | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |

1096 | !arrayDestNum.(s).(n) <- cnt; |
||

1097 | !arrayDest3.(s).(n) <- |
||

1098 | if Hashtbl.mem htR role then Hashtbl.find htR role |
||

1099 | else |
||

1100 | let size = Hashtbl.length htR in |
||

1101 | Hashtbl.add htR role size; |
||

1102 | size |
||

1103 | 86b07be8 | Thorsten Wißmann | | C.HCATLEASTPROB (p,f1) -> |

1104 | !arrayType.(s).(n) <- AtLeastProbF; |
||

1105 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |
||

1106 | eda515b6 | Thorsten Wißmann | !arrayDestNum.(s).(n) <- p.C.nominator; |

1107 | !arrayDestNum2.(s).(n) <- p.C.denominator |
||

1108 | 9bae2c4f | Thorsten Wißmann | | C.HCLESSPROBFAIL (p,f1) -> |

1109 | !arrayType.(s).(n) <- LessProbFailF; |
||

1110 | 86b07be8 | Thorsten Wißmann | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; |

1111 | eda515b6 | Thorsten Wißmann | !arrayDestNum.(s).(n) <- p.C.nominator; |

1112 | !arrayDestNum2.(s).(n) <- p.C.denominator |
||

1113 | c49eea11 | Thorsten Wißmann | | C.HCCONST str -> |

1114 | !arrayType.(s).(n) <- ConstF; (* type of modality *) |
||

1115 | (* Dest1 and Dest2 are the arguments, here: none *) |
||

1116 | (* DestNum and DestNum2 are the numerators and denonimators of |
||

1117 | fractions, here: none *) |
||

1118 | !arrayDest3.(s).(n) <- |
||

1119 | if Hashtbl.mem htR str then Hashtbl.find htR str |
||

1120 | else |
||

1121 | let size = Hashtbl.length htR in |
||

1122 | Hashtbl.add htR str size; |
||

1123 | size |
||

1124 | (* Dest3 are the role names / identifiers for constant values *) |
||

1125 | (* idea: hash identifier names *) |
||

1126 | | C.HCCONSTN str -> |
||

1127 | !arrayType.(s).(n) <- ConstnF; (* type of modality *) |
||

1128 | (* Dest1 and Dest2 are the arguments, here: none *) |
||

1129 | (* DestNum and DestNum2 are the numerators and denonimators of |
||

1130 | fractions, here: none *) |
||

1131 | !arrayDest3.(s).(n) <- |
||

1132 | if Hashtbl.mem htR str then Hashtbl.find htR str |
||

1133 | else |
||

1134 | let size = Hashtbl.length htR in |
||

1135 | Hashtbl.add htR str size; |
||

1136 | size |
||

1137 | (* Dest3 are the role names / identifiers for constant values *) |
||

1138 | (* idea: hash identifier names *) |
||

1139 | 19f5dad0 | Dirk Pattinson | | C.HCID (f1) -> |

1140 | !arrayType.(s).(n) <- IdF; |
||

1141 | d58bba0f | Dirk Pattinson | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1 |

1142 | 034a8dea | Christoph Egger | | C.HCNORM (f1, f2) -> |

1143 | 19f5dad0 | Dirk Pattinson | !arrayType.(s).(n) <- NormF; |

1144 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; |
||

1145 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 |
||

1146 | 034a8dea | Christoph Egger | | C.HCNORMN (f1, f2) -> |

1147 | 19f5dad0 | Dirk Pattinson | !arrayType.(s).(n) <- NormnF; |

1148 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; |
||

1149 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 |
||

1150 | (* note that choice is self-dual *) |
||

1151 | d58bba0f | Dirk Pattinson | | C.HCCHC (f1, f2) -> |

1152 | 4fd28192 | Thorsten Wißmann | !arrayType.(s).(n) <- ChcF; |

1153 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; |
||

1154 | !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 |
||

1155 | | C.HCFUS (first, f1) -> |
||

1156 | !arrayType.(s).(n) <- FusF; |
||

1157 | let s1 = List.nth sortlst (if first then 0 else 1) in |
||

1158 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; |
||

1159 | !arrayDest3.(s).(n) <- if first then 0 else 1 |
||

1160 | 5ec97220 | Christoph Egger | | C.HCMU (name, f1) -> |

1161 | !arrayType.(s).(n) <- MuF; |
||

1162 | 034a8dea | Christoph Egger | let unfold = C.hc_replace hcF name f f1 in |

1163 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold |
||

1164 | 5ec97220 | Christoph Egger | | C.HCNU (name, f1) -> |

1165 | 034a8dea | Christoph Egger | !arrayType.(s).(n) <- NuF; |

1166 | let unfold = C.hc_replace hcF name f f1 in |
||

1167 | !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold |
||

1168 | 5ec97220 | Christoph Egger | | C.HCVAR _ -> !arrayType.(s).(n) <- Other |

1169 | |||

1170 | 4fd28192 | Thorsten Wißmann | |

1171 | let initTablesAt hcF htF name sort = |
||

1172 | let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in |
||

1173 | let nom = C.HcFHt.find htF.(sort) hcnom in |
||

1174 | let addAt f n = |
||

1175 | match f.HC.node with |
||

1176 | | C.HCTRUE |
||

1177 | | C.HCFALSE |
||

1178 | | C.HCOR _ |
||

1179 | | C.HCAND _ |
||

1180 | | C.HCAT _ -> () |
||

1181 | | _ -> |
||

1182 | 034a8dea | Christoph Egger | let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in |

1183 | 4fd28192 | Thorsten Wißmann | let atn = C.HcFHt.find htF.(0) at in |

1184 | FHt.add !arrayAt.(sort).(n) nom atn |
||

1185 | in |
||

1186 | C.HcFHt.iter addAt htF.(sort) |
||

1187 | |||

1188 | let ppFormulae nomTbl tbox (s, f) = |
||

1189 | let card = Array.length !sortTable in |
||

1190 | if card <= 0 then |
||

1191 | raise (C.CoAlgException "Number of sorts must be positive.") |
||

1192 | else (); |
||

1193 | let nnfAndSimplify f = C.simplify (C.nnf f) in |
||

1194 | f828ad2f | Thorsten Wißmann | let f1 = nnfAndSimplify f in |

1195 | let nf1 = nnfAndSimplify (C.NOT f) in |
||

1196 | let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in |
||

1197 | let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in |
||

1198 | |||

1199 | let hcF = C.HcFormula.create true in |
||

1200 | let hcf = C.hc_formula hcF f1 in |
||

1201 | let nhcf = C.hc_formula hcF nf1 in |
||

1202 | let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in |
||

1203 | let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in |
||

1204 | 4fd28192 | Thorsten Wißmann | let hcfalse = C.hc_formula hcF C.FALSE in |

1205 | f828ad2f | Thorsten Wißmann | let hctrue = C.hc_formula hcF C.TRUE in |

1206 | 4fd28192 | Thorsten Wißmann | |

1207 | let fset = Array.init card (fun _ -> C.HcFHt.create 128) in |
||

1208 | cb12f8a5 | Christoph Egger | let vset = Array.init card (fun _ -> C.HcFHt.create 128) in |

1209 | 4fd28192 | Thorsten Wißmann | let atset = C.HcFHt.create 64 in |

1210 | let nomset = Hashtbl.create 16 in |
||

1211 | for i = 0 to card-1 do |
||

1212 | cb12f8a5 | Christoph Egger | detClosure [] nomTbl hcF fset vset atset nomset i hcfalse; |

1213 | detClosure [] nomTbl hcF fset vset atset nomset i hctrue; |
||

1214 | 4fd28192 | Thorsten Wißmann | done; |

1215 | cb12f8a5 | Christoph Egger | detClosure [] nomTbl hcF fset vset atset nomset s hcf; |

1216 | detClosure [] nomTbl hcF fset vset atset nomset s nhcf; |
||

1217 | List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f) |
||

1218 | hctbox; |
||

1219 | List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f) |
||

1220 | nhctbox; |
||

1221 | 4fd28192 | Thorsten Wißmann | Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset; |

1222 | |||

1223 | let htF = Array.init card (fun _ -> C.HcFHt.create 128) in |
||

1224 | for i = 0 to card-1 do |
||

1225 | C.HcFHt.add htF.(i) hcfalse 0; |
||

1226 | C.HcFHt.add htF.(i) hctrue 1 |
||

1227 | done; |
||

1228 | let addAts f () idx = |
||

1229 | for i = 0 to card-1 do |
||

1230 | C.HcFHt.add htF.(i) f idx |
||

1231 | done; |
||

1232 | idx + 1 |
||

1233 | in |
||

1234 | let sizeAt = C.HcFHt.fold addAts atset 2 in |
||

1235 | let addFml i f () idx = |
||

1236 | if C.HcFHt.mem htF.(i) f then idx |
||

1237 | else begin |
||

1238 | C.HcFHt.add htF.(i) f idx; |
||

1239 | idx+1 |
||

1240 | end |
||

1241 | in |
||

1242 | let size = ref 0 in |
||

1243 | for i = 0 to card-1 do |
||

1244 | let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in |
||

1245 | if size2 > !size then size := size2 else () |
||

1246 | done; |
||

1247 | |||

1248 | arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); |
||

1249 | arrayType := Array.init card (fun _ -> Array.make !size Other); |
||

1250 | arrayDest1 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1251 | arrayDest2 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1252 | arrayDest3 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1253 | d9f4e4af | Christoph Egger | arrayDeferral := Array.init card (fun _-> Array.make !size(-1)); |

1254 | 4fd28192 | Thorsten Wißmann | arrayNeg := Array.init card (fun _ -> Array.make !size (-1)); |

1255 | 29b2e3f3 | Thorsten Wißmann | arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); |

1256 | eda515b6 | Thorsten Wißmann | arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1)); |

1257 | 98af95fb | Thorsten Wißmann | arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); |

1258 | 4fd28192 | Thorsten Wißmann | let htR = Hashtbl.create 128 in |

1259 | d9f4e4af | Christoph Egger | Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF; |

1260 | 4fd28192 | Thorsten Wißmann | arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8)); |

1261 | Hashtbl.iter (initTablesAt hcF htF) nomset; |
||

1262 | |||

1263 | S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1); |
||

1264 | let initbs = bsetMake () in |
||

1265 | bsetAdd initbs (C.HcFHt.find htF.(s) hcf); |
||

1266 | let tboxTbl = Array.init card (fun _ -> bsetMake ()) in |
||

1267 | List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox; |
||

1268 | tboxTable := tboxTbl; |
||

1269 | (tbox1, (s, f1), initbs) |