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

History | View | Annotate | Download (48.1 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 | f4e43751 | Christoph Egger | | Monotone |

83 | f1fa9ad5 | Thorsten Wißmann | | CoalitionLogic |

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

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

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

87 | 19f5dad0 | Dirk Pattinson | | Identity |

88 | | DefaultImplication |
||

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

90 | | Fusion |
||

91 | |||

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

93 | type parametricFunctorName = |
||

94 | | NameConstant |
||

95 | |||

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

97 | type functorName = |
||

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

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

100 | |||

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

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

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

104 | f4e43751 | Christoph Egger | ; (NPa Monotone , "Monotone") |

105 | 5e0983fe | Thorsten Wißmann | ; (NPa GML , "GML") |

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

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

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

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

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

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

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

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

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

115 | db23edf7 | Thorsten Wißmann | ] |

116 | |||

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

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

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

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

121 | db23edf7 | Thorsten Wißmann | ] |

122 | |||

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

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

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

126 | match func with |
||

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

128 | |||

129 | |||

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

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

132 | try |
||

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

134 | match functorName with |
||

135 | | NPa x -> Some x |
||

136 | | Pa f -> functor_apply_parameters f params |
||

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

138 | |||

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

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

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

142 | | Some Fusion -> None |
||

143 | | x -> x |
||

144 | |||

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

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

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

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

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

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

151 | in |
||

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

153 | try |
||

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

155 | name ^ suffix |
||

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

157 | |||

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

159 | type formulaType = |
||

160 | | Other |
||

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

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

163 | | OrF |
||

164 | | AtF |
||

165 | | NomF |
||

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

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

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

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

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

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

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

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

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

175 | | ConstnF (* constant functor *) |
||

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

177 | | NormF (* Default Implication *) |
||

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

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

180 | | FusF (* Fusion *) |
||

181 | 3b407438 | Christoph Egger | | MuF |

182 | | NuF |
||

183 | 4fd28192 | Thorsten Wißmann | |

184 | type localFormula = int |
||

185 | type bset = S.bitset |
||

186 | |||

187 | type atFormula = int |
||

188 | type cset = S.bitset |
||

189 | type csetSet = BsSet.t |
||

190 | |||

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

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

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

194 | |||

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

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

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

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

199 | *) |
||

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

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

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

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

204 | 7eb41195 | Hans-Peter Deifel | idxS: int } |

205 | 4fd28192 | Thorsten Wißmann | |

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

207 | sortC : sort; |
||

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

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

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

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

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

213 | mutable childrenC : state list; |
||

214 | mutable constraintsC : csetSet; |
||

215 | 9f1263ec | Christoph Egger | mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC. |

216 | e0f19999 | Thorsten Wißmann | the solver returns "satisfiable" iff |

217 | there is a satisfying assignment of |
||

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

219 | childrenC yet. |
||

220 | *) |
||

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

222 | of the Minisat solver |
||

223 | *) |
||

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

225 | 7eb41195 | Hans-Peter Deifel | idxC : int } |

226 | 4fd28192 | Thorsten Wißmann | |

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

228 | 4fd28192 | Thorsten Wißmann | |

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

230 | 4fd28192 | Thorsten Wißmann | |

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

232 | 4fd28192 | Thorsten Wißmann | |

233 | |||

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

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

236 | (*****************************************************************************) |
||

237 | |||

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

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

240 | |||

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

242 | 4fd28192 | Thorsten Wißmann | |

243 | and sort = C.sort |
||

244 | |||

245 | and nodeStatus = |
||

246 | | Expandable |
||

247 | | Open |
||

248 | | Sat |
||

249 | | Unsat |
||

250 | |||

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

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

253 | as well as the Ex. |
||

254 | |||

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

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

257 | *) |
||

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

259 | 269d93e5 | Thorsten Wißmann | |

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

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

262 | 269d93e5 | Thorsten Wißmann | |

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

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

265 | | SingleElement of 'a |
||

266 | | NoMoreElements |
||

267 | |||

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

269 | |||

270 | and ruleEnumeration = rule lazyliststep |
||

271 | |||

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

273 | | Expandable -> "Expandable" |
||

274 | | Open -> "Open" |
||

275 | | Sat -> "Sat" |
||

276 | | Unsat -> "Unsat" |
||

277 | |||

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

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

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

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

282 | list_state := None; |
||

283 | MultipleElements a_list |
||

284 | end |
||

285 | | None -> NoMoreElements |
||

286 | end |
||

287 | 4fd28192 | Thorsten Wißmann | |

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

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

290 | match step with |
||

291 | | NoMoreElements -> [] |
||

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

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

294 | |||

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

296 | |||

297 | type node = |
||

298 | | State of state |
||

299 | | Core of core |
||

300 | |||

301 | type constrnt = |
||

302 | | UnsatC |
||

303 | | SatC |
||

304 | | OpenC of node list |
||

305 | | UnexpandedC of node list |
||

306 | |||

307 | type propagateElement = |
||

308 | | UState of state * int option |
||

309 | | UCore of core * bool |
||

310 | | UCnstr of cset |
||

311 | |||

312 | type queueElement = |
||

313 | | QState of state |
||

314 | | QCore of core |
||

315 | | QCnstr of cset |
||

316 | | QEmpty |
||

317 | |||

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

319 | |||

320 | exception CoAlg_finished of bool |
||

321 | |||

322 | |||

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

324 | |||

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

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

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

328 | |||

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

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

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

332 | |||

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

334 | match x with |
||

335 | | None -> None |
||

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

337 | | None -> None |
||

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

339 | |||

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

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

342 | if x = extreme || y = extreme |
||

343 | then extreme |
||

344 | else optionalizeOperator op x y |
||

345 | in function |
||

346 | | Disjunctive l -> |
||

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

348 | | Conjunctive l -> |
||

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

350 | |||

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

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

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

354 | 4fd28192 | Thorsten Wißmann | |

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

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

357 | (*****************************************************************************) |
||

358 | |||

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

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

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

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

363 | let doPropagation = ref false |
||

364 | 61c5af02 | Christoph Egger | let doPropagationCounter = ref 0 |

365 | 4fd28192 | Thorsten Wißmann | |

366 | let queueInit () = |
||

367 | queueStates := []; |
||

368 | queueCores1 := []; |
||

369 | queueCores2 := []; |
||

370 | queueCnstrs := []; |
||

371 | doPropagation := false |
||

372 | |||

373 | let queueIsEmpty () = |
||

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

375 | |||

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

377 | |||

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

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

380 | |||

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

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

383 | *) |
||

384 | |||

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

386 | |||

387 | let queueGetElement () = |
||

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

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

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

391 | QCnstr res |
||

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

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

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

395 | QState res |
||

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

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

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

399 | QCore res |
||

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

401 | else |
||

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

403 | doPropagation := true; |
||

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

405 | queueCores2 := []; |
||

406 | QCore res |
||

407 | |||

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

409 | |||

410 | 55dc0a64 | Christoph Egger | let setPropagationCounter count = |

411 | doPropagationCounter := count |
||

412 | |||

413 | 4fd28192 | Thorsten Wißmann | let doSatPropagation () = |

414 | 61c5af02 | Christoph Egger | if !doPropagationCounter == 0 |

415 | 55dc0a64 | Christoph Egger | then true |

416 | 61c5af02 | Christoph Egger | else begin |

417 | doPropagationCounter := !doPropagationCounter - 1; |
||

418 | false |
||

419 | end |
||

420 | (* let res = !doPropagation in *) |
||

421 | (* doPropagation := false; *) |
||

422 | (* res *) |
||

423 | 4fd28192 | Thorsten Wißmann | |

424 | (*****************************************************************************) |
||

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

426 | (*****************************************************************************) |
||

427 | |||

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

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

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

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

432 | |||

433 | let graphInit () = |
||

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

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

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

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

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

439 | |||

440 | let graphIterStates fkt = |
||

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

442 | |||

443 | let graphIterCores fkt = |
||

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

445 | |||

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

447 | 4fd28192 | Thorsten Wißmann | |

448 | let graphClearCnstr () = |
||

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

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

451 | match cnstr with |
||

452 | | UnsatC |
||

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

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

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

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

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

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

459 | |||

460 | let graphFindState sort bs = |
||

461 | try |
||

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

463 | with Not_found -> None |
||

464 | |||

465 | let graphFindCore sort bs = |
||

466 | try |
||

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

468 | with Not_found -> None |
||

469 | |||

470 | let graphFindCnstr cset = |
||

471 | try |
||

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

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

474 | |||

475 | let graphInsertState sort bs state = |
||

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

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

478 | |||

479 | let graphInsertCore sort bs core = |
||

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

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

482 | |||

483 | let graphInsertCnstr cset cnstr = |
||

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

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

486 | 4fd28192 | Thorsten Wißmann | |

487 | let graphReplaceCnstr cset cnstr = |
||

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

489 | 4fd28192 | Thorsten Wißmann | |

490 | let graphSizeState () = |
||

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

492 | let graphSizeCore () = |
||

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

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

495 | 4fd28192 | Thorsten Wißmann | |

496 | let graphAddRoot core = |
||

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

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

499 | |||

500 | let graphGetRoot () = |
||

501 | match !graphRoot with |
||

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

503 | | Some core -> core |
||

504 | |||

505 | |||

506 | (*****************************************************************************) |
||

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

508 | (*****************************************************************************) |
||

509 | |||

510 | let cssEmpty = BsSet.empty |
||

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

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

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

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

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

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

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

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

519 | BsSet.iter action css |
||

520 | 4fd28192 | Thorsten Wißmann | |

521 | |||

522 | (*****************************************************************************) |
||

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

524 | (*****************************************************************************) |
||

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

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

527 | let oldVal = !nodeCounter in |
||

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

529 | oldVal |
||

530 | |||

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

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

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

534 | 7eb41195 | Hans-Peter Deifel | idxS = nextNodeIdx() |

535 | 73762b19 | Thorsten Wißmann | } |

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

537 | let stateGetBs state = state.bsS |
||

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

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

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

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

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

543 | let stateGetParents state = state.parentsS |
||

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

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

546 | let stateGetRules state = state.childrenS |
||

547 | let stateAddRule state dep children = |
||

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

549 | List.length state.childrenS |
||

550 | let stateGetConstraints state = state.constraintsS |
||

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

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

553 | 7eb41195 | Hans-Peter Deifel | let stateGetIdx (state:state) = state.idxS |

554 | 4fd28192 | Thorsten Wißmann | |

555 | |||

556 | (*****************************************************************************) |
||

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

558 | (*****************************************************************************) |
||

559 | |||

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

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

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

563 | 7eb41195 | Hans-Peter Deifel | idxC = nextNodeIdx() |

564 | 73762b19 | Thorsten Wißmann | } |

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

566 | let coreGetBs core = core.bsC |
||

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

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

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

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

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

572 | let coreGetParents core = core.parentsC |
||

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

574 | let coreGetChildren core = core.childrenC |
||

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

576 | let coreGetConstraints core = core.constraintsC |
||

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

578 | e0e6eb62 | Hans-Peter Deifel | let coreGetSolver core = |

579 | match core.solver with |
||

580 | | Some solver -> solver |
||

581 | | None -> raise (Failure "Sat solver not allocated") |
||

582 | 9f1263ec | Christoph Egger | let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht |

583 | 4fd28192 | Thorsten Wißmann | let coreGetFht core = core.fht |

584 | 7eb41195 | Hans-Peter Deifel | let coreGetIdx (core:core) = core.idxC |

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

586 | let coreAddConstraintParent core cset = |
||

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

588 | |||

589 | |||

590 | (*****************************************************************************) |
||

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

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

593 | (*****************************************************************************) |
||

594 | |||

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

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

597 | 5956a56d | Christoph Egger | let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx)) |

598 | let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx)) |
||

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

600 | let setAddState set state = |
||

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

602 | let setAddCore set core = |
||

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

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

605 | let setMemState set state = |
||

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

607 | let setMemCore set core = |
||

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

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

610 | let setRemoveState set state = |
||

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

612 | let setRemoveCore set core = |
||

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

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

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

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

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

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

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

620 | 4fd28192 | Thorsten Wißmann | |

621 | |||

622 | (*****************************************************************************) |
||

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

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

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

626 | (*****************************************************************************) |
||

627 | |||

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

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

630 | let lhtFind lht lit = |
||

631 | try |
||

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

633 | with Not_found -> None |
||

634 | |||

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

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

637 | let fhtFind fht f = |
||

638 | try |
||

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

640 | with Not_found -> None |
||

641 | |||

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

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

644 | let nhtFind nht nom = |
||

645 | try |
||

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

647 | with Not_found -> None |
||

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

649 | |||

650 | (*****************************************************************************) |
||

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

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

653 | (*****************************************************************************) |
||

654 | |||

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

656 | |||

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

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

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

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

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

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

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

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

665 | res |
||

666 | e7aaefa9 | Hans-Peter Deifel | let bsetSingleton lf = |

667 | let res = bsetMakeRealEmpty () in |
||

668 | bsetAdd res lf; |
||

669 | res |
||

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

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

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

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

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

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

676 | res |
||

677 | |||

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

679 | |||

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

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

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

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

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

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

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

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

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

689 | let csetIter cs fkt = |
||

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

691 | S.iterBS fkt2 cs |
||

692 | |||

693 | |||

694 | (*****************************************************************************) |
||

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

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

697 | (*****************************************************************************) |
||

698 | |||

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

700 | *) |
||

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

702 | |||

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

704 | *) |
||

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

706 | |||

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

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

709 | *) |
||

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

711 | |||

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

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

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

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

716 | *) |
||

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

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

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

720 | arrayNum2 = the denominator of the probability |
||

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

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

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

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

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

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

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

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

729 | 4fd28192 | Thorsten Wißmann | |

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

731 | to their @-wrapper. |
||

732 | *) |
||

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

734 | |||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

749 | let lfFromInt num = num |
||

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

751 | |||

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

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

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

755 | input |
||

756 | |||

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

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

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

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

761 | in |
||

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

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

764 | |||

765 | let csetToString sort cset = bsetToString sort cset |
||

766 | |||

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

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

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

770 | in |
||

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

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

773 | 7eb41195 | Hans-Peter Deifel | List.map (fun (st:state) -> string_of_int st.idxS) core.childrenC |

774 | 488cea0f | Thorsten Wißmann | in |

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

776 | 7eb41195 | Hans-Peter Deifel | List.map (fun (st,_:state*int) -> string_of_int st.idxS) core.parentsC |

777 | 4164c8e1 | Thorsten Wißmann | in |

778 | 7eb41195 | Hans-Peter Deifel | "Core "^(string_of_int core.idxC)^" {\n"^ |

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

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

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

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

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

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

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

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

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

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

789 | 73762b19 | Thorsten Wißmann | |

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

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

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

793 | in |
||

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

795 | let conclusionList = |
||

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

797 | 7eb41195 | Hans-Peter Deifel | List.map (fun (core:core) -> string_of_int core.idxC) lst |

798 | 73762b19 | Thorsten Wißmann | ) state.childrenS |

799 | in |
||

800 | let conclusionList = |
||

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

802 | in |
||

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

804 | 7eb41195 | Hans-Peter Deifel | List.map (fun (co:core) -> string_of_int co.idxC) state.parentsS |

805 | 4164c8e1 | Thorsten Wißmann | in |

806 | 7eb41195 | Hans-Peter Deifel | "State "^(string_of_int state.idxS)^" {\n"^ |

807 | 73762b19 | Thorsten Wißmann | " Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^ |

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

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

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

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

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

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

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

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

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

817 | |||

818 | 86c2c2ee | Hans-Peter Deifel | let nodeToDot idx typ sort formulas deferrals status parentIdxs : string = |

819 | let color = match status with |
||

820 | | Sat -> "#8ae234" |
||

821 | | Unsat -> "#ef2929" |
||

822 | | Open -> "#729fcf" |
||

823 | c13029a3 | Christoph Egger | | Expandable -> "white" |

824 | in |
||

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

826 | 86c2c2ee | Hans-Peter Deifel | let formula: C.formula = lfGetFormula sort lf in |

827 | if (bsetMem deferrals lf) |
||

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

829 | de84f40d | Christoph Egger | else (escapeHtml (C.string_of_formula formula)) :: lst |

830 | in |
||

831 | 86c2c2ee | Hans-Peter Deifel | let formulaList = bsetFold toFormula formulas [] in |

832 | let ownidx = (string_of_int idx) in |
||

833 | 8d6bf016 | Christoph Egger | let parents = |

834 | 86c2c2ee | Hans-Peter Deifel | List.map (fun (parentIdx) -> |

835 | "Node"^string_of_int parentIdx^" -> Node"^ownidx^";") |
||

836 | parentIdxs |
||

837 | 8d6bf016 | Christoph Egger | in |

838 | 86c2c2ee | Hans-Peter Deifel | let style = if typ = "Core" then "filled,rounded" else "filled" in |

839 | "Node" ^ ownidx ^ " [shape=box,style=\"" ^ style |
||

840 | ^ "\",fillcolor=\"" ^ color ^ "\"" |
||

841 | ^ ",label=<<B>" ^ typ ^ " " ^ ownidx ^ "</B>" |
||

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

843 | de84f40d | Christoph Egger | ^ ">];\n" |

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

845 | |||

846 | 86c2c2ee | Hans-Peter Deifel | let stateToDot (state:state): string = |

847 | nodeToDot state.idxS "State" state.sortS state.bsS state.deferralS |
||

848 | state.statusS (List.map (fun c -> c.idxC) state.parentsS) |
||

849 | 8d6bf016 | Christoph Egger | |

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

851 | 86c2c2ee | Hans-Peter Deifel | nodeToDot core.idxC "Core" core.sortC core.bsC core.deferralC |

852 | core.statusC (List.map (fun (s,_) -> s.idxS) core.parentsC) |
||

853 | |||

854 | let graphToDot () : string = |
||

855 | let lines = ref ["digraph reasonerstate {"] in |
||

856 | graphIterCores (fun core -> lines := (coreToDot core)::!lines); |
||

857 | graphIterStates (fun state -> lines := (stateToDot state)::!lines); |
||

858 | |||

859 | let legend = |
||

860 | "subgraph legend {\n" |
||

861 | ^ "key [label=<<TABLE CELLBORDER=\"0\" BGCOLOR=\"#d3d7cf\">\n" |
||

862 | ^ "<TR><TD>Color:</TD><TD BGCOLOR=\"#8ae234\">sat</TD><TD BGCOLOR=\"#ef2929\">unsat</TD><TD BGCOLOR=\"#729fcf\">open</TD><TD BGCOLOR=\"white\">expandable</TD></TR>" |
||

863 | ^ "<TR><TD>Rounded:</TD><TD>cores</TD></TR>" |
||

864 | ^ "<TR><TD>Boxed:</TD><TD>states</TD></TR>" |
||

865 | ^ "<TR><TD>Underlined:</TD><TD>focus</TD></TR>" |
||

866 | ^ "</TABLE>>, shape=none];}" in |
||

867 | |||

868 | lines := "}"::legend::!lines; |
||

869 | String.concat "\n" (List.rev !lines) |
||

870 | 8d6bf016 | Christoph Egger | |

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

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

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

874 | in |
||

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

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

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

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

879 | 7eb41195 | Hans-Peter Deifel | ^(printList (List.map (fun (st:state) -> st.idxS) !queueStates)) |

880 | 488cea0f | Thorsten Wißmann | ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1)) |

881 | 7eb41195 | Hans-Peter Deifel | ^(printList (List.map (fun (co:core) -> co.idxC) !queueCores1)) |

882 | 488cea0f | Thorsten Wißmann | ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2)) |

883 | 7eb41195 | Hans-Peter Deifel | ^(printList (List.map (fun (co:core) -> co.idxC) !queueCores2)) |

884 | 488cea0f | Thorsten Wißmann | ^"\n" |

885 | |||

886 | 73762b19 | Thorsten Wißmann | |

887 | |||

888 | 4fd28192 | Thorsten Wißmann | |

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

890 | let atFormulaGetNominal f = |
||

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

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

893 | (s, n) |
||

894 | |||

895 | let lfToAt _ lf = lf |
||

896 | |||

897 | b6653b96 | Hans-Peter Deifel | |

898 | type fragment = AlternationFree | AconjunctiveAltFree |
||

899 | f24367c4 | Hans-Peter Deifel | type fragment_spec = Auto | Fragment of fragment |

900 | b6653b96 | Hans-Peter Deifel | let fragment = ref AlternationFree |

901 | let getFragment () = !fragment |
||

902 | |||

903 | |||

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

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

906 | 4fd28192 | Thorsten Wißmann | |

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

908 | *) |
||

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

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

911 | let detClosure_ = detClosure newvars in |
||

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

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

914 | else "ε" in |
||

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

916 | let sstr = string_of_int s in |
||

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

918 | else (); |
||

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

920 | 066ed7b8 | Christoph Egger | (compare (C.HcFHt.find vset.(s) f) deferral = 0 || |

921 | compare deferral "ε" = 0) |
||

922 | 1b17ef3c | Christoph Egger | then () |

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

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

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

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

927 | match f.HC.node with |
||

928 | | C.HCTRUE |
||

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

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

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

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

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

934 | match nomTbl name with |
||

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

936 | | Some sort -> |
||

937 | if sort <> s then |
||

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

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

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

941 | else () |
||

942 | end else () |
||

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

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

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

946 | let s1 = |
||

947 | match nomTbl name with |
||

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

949 | | Some sort -> sort |
||

950 | in |
||

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

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

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

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

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

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

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

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

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

960 | f4e43751 | Christoph Egger | if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone) |

961 | 2a84977e | Thorsten Wißmann | || List.length sortlst <> 1 |

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

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

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

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

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

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

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

969 | else (); |
||

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

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

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

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

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

975 | else (); |
||

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

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

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

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

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

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

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

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

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

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

986 | *) |
||

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

988 | | C.HCCONSTN color -> |
||

989 | begin match func with |
||

990 | | Constant params -> |
||

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

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

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

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

995 | end; |
||

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

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

998 | else (); |
||

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

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

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

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

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

1004 | else (); |
||

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

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

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

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

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

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

1011 | else (); |
||

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

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

1014 | 19f5dad0 | Dirk Pattinson | |

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

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

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

1018 | else (); |
||

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

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

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

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

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

1024 | else (); |
||

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

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

1027 | 034a8dea | Christoph Egger | (* |

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

1029 | 034a8dea | Christoph Egger | *) |

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

1031 | e08cd8a9 | Christoph Egger | begin |

1032 | if C.hc_freeIn name f1 |
||

1033 | then |
||

1034 | C.HcFHt.replace vset.(s) f name |
||

1035 | else (); |
||

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

1037 | let appendvars = List.append newvars [name] in |
||

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

1039 | end |
||

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

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

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

1043 | 6553983f | Christoph Egger | |

1044 | 4fd28192 | Thorsten Wißmann | |

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

1046 | match f.HC.node with |
||

1047 | | C.HCTRUE |
||

1048 | | C.HCFALSE |
||

1049 | | C.HCOR _ |
||

1050 | | C.HCAND _ |
||

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

1052 | | _ -> |
||

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

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

1055 | |||

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

1057 | *) |
||

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

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

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

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

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

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

1064 | match f.HC.node with |
||

1065 | | C.HCTRUE |
||

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

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

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

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

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

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

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

1073 | let s1 = |
||

1074 | match nomTbl name with |
||

1075 | | None -> assert false |
||

1076 | | Some sort -> sort |
||

1077 | in |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1095 | else |
||

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

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

1098 | size |
||

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

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

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

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

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

1104 | else |
||

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

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

1107 | size |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1122 | else |
||

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

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

1125 | size |
||

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

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

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

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

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

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

1132 | else |
||

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

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

1135 | size |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1153 | else |
||

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

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

1156 | size |
||

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

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

1159 | | C.HCCONSTN str -> |
||

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

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

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

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

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

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

1166 | else |
||

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

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

1169 | size |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1202 | |||

1203 | 4fd28192 | Thorsten Wißmann | |

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

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

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

1207 | let addAt f n = |
||

1208 | match f.HC.node with |
||

1209 | | C.HCTRUE |
||

1210 | | C.HCFALSE |
||

1211 | | C.HCOR _ |
||

1212 | | C.HCAND _ |
||

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

1214 | | _ -> |
||

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

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

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

1218 | in |
||

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

1220 | |||

1221 | f24367c4 | Hans-Peter Deifel | let ppFormulae fragSpec nomTbl tbox (s, f) = |

1222 | 4fd28192 | Thorsten Wißmann | let card = Array.length !sortTable in |

1223 | if card <= 0 then |
||

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

1225 | else (); |
||

1226 | bc8db289 | Christoph Egger | C.verifyFormula f; |

1227 | 4fd28192 | Thorsten Wißmann | let nnfAndSimplify f = C.simplify (C.nnf f) in |

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

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

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

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

1232 | |||

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

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

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

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

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

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

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

1240 | 4fd28192 | Thorsten Wißmann | |

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

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

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

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

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

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

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

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

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

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

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

1252 | hctbox; |
||

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

1254 | nhctbox; |
||

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

1256 | |||

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

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

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

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

1261 | done; |
||

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

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

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

1265 | done; |
||

1266 | idx + 1 |
||

1267 | in |
||

1268 | let sizeAt = C.HcFHt.fold addAts atset 2 in |
||

1269 | let addFml i f () idx = |
||

1270 | if C.HcFHt.mem htF.(i) f then idx |
||

1271 | else begin |
||

1272 | C.HcFHt.add htF.(i) f idx; |
||

1273 | idx+1 |
||

1274 | end |
||

1275 | in |
||

1276 | let size = ref 0 in |
||

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

1278 | let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in |
||

1279 | if size2 > !size then size := size2 else () |
||

1280 | done; |
||

1281 | |||

1282 | f24367c4 | Hans-Peter Deifel | begin match fragSpec with |

1283 | | Auto -> if C.isMuAconjunctive f then |
||

1284 | fragment := AconjunctiveAltFree |
||

1285 | else |
||

1286 | fragment := AlternationFree |
||

1287 | | Fragment AconjunctiveAltFree -> |
||

1288 | if not (C.isMuAconjunctive f) then |
||

1289 | raise (CoAlgFormula.CoAlgException "Formula not in required fragment") |
||

1290 | else fragment := AconjunctiveAltFree |
||

1291 | | Fragment AlternationFree -> |
||

1292 | if C.isMuAconjunctive f then |
||

1293 | raise (CoAlgFormula.CoAlgException "Formula not in required fragment") |
||

1294 | else fragment := AlternationFree |
||

1295 | end; |
||

1296 | |||

1297 | (* if (fragSpec = Auto || fragSpec = Fragment AconjunctiveAltFree) && C.isMuAconjunctive f then *) |
||

1298 | (* fragment := AconjunctiveAltFree; *) |
||

1299 | (* else if (fragSpec = Auto || fragSpec = Fragment AlternationFree) && (not (C.isMuAconjunctive f)) *) |
||

1300 | (* fragment := AlternationFree; *) |
||

1301 | (* else *) |
||

1302 | (* raise (CoAlgFormula.CoAlgException "Formula not in required fragment"); *) |
||

1303 | b6653b96 | Hans-Peter Deifel | |

1304 | 4fd28192 | Thorsten Wißmann | arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); |

1305 | arrayType := Array.init card (fun _ -> Array.make !size Other); |
||

1306 | arrayDest1 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1307 | arrayDest2 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1308 | arrayDest3 := Array.init card (fun _ -> Array.make !size (-1)); |
||

1309 | d9f4e4af | Christoph Egger | arrayDeferral := Array.init card (fun _-> Array.make !size(-1)); |

1310 | 4fd28192 | Thorsten Wißmann | arrayNeg := Array.init card (fun _ -> Array.make !size (-1)); |

1311 | 29b2e3f3 | Thorsten Wißmann | arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); |

1312 | eda515b6 | Thorsten Wißmann | arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1)); |

1313 | 98af95fb | Thorsten Wißmann | arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); |

1314 | 4fd28192 | Thorsten Wißmann | let htR = Hashtbl.create 128 in |

1315 | d9f4e4af | Christoph Egger | Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF; |

1316 | 4fd28192 | Thorsten Wißmann | arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8)); |

1317 | Hashtbl.iter (initTablesAt hcF htF) nomset; |
||

1318 | |||

1319 | S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1); |
||

1320 | let initbs = bsetMake () in |
||

1321 | bsetAdd initbs (C.HcFHt.find htF.(s) hcf); |
||

1322 | let tboxTbl = Array.init card (fun _ -> bsetMake ()) in |
||

1323 | List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox; |
||

1324 | tboxTable := tboxTbl; |
||

1325 | (tbox1, (s, f1), initbs) |
||

1326 | a57eb439 | Hans-Peter Deifel | |

1327 | (* vim: set et sw=2 sts=2 ts=8 : *) |